Using Session Types for Reasoning About Boundedness in the Pi-Calculus
The classes of depth-bounded and name-bounded processes are fragments of the pi-calculus for which some of the decision problems that are undecidable for the full calculus become decidable. P is depth-bounded at level k if every reduction sequence for P contains successor processes with at most k ac...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2017-08-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1709.00829v1 |
| _version_ | 1830090276868194304 |
|---|---|
| author | Hans Hüttel |
| author_facet | Hans Hüttel |
| author_sort | Hans Hüttel |
| collection | DOAJ |
| description | The classes of depth-bounded and name-bounded processes are fragments of the pi-calculus for which some of the decision problems that are undecidable for the full calculus become decidable. P is depth-bounded at level k if every reduction sequence for P contains successor processes with at most k active nested restrictions. P is name-bounded at level k if every reduction sequence for P contains successor processes with at most k active bound names. Membership of these classes of processes is undecidable. In this paper we use binary session types to decise two type systems that give a sound characterization of the properties: If a process is well-typed in our first system, it is depth-bounded. If a process is well-typed in our second, more restrictive type system, it will also be name-bounded. |
| first_indexed | 2024-12-16T17:00:02Z |
| format | Article |
| id | doaj.art-23786c4181204632910412806e39049c |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-16T17:00:02Z |
| publishDate | 2017-08-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-23786c4181204632910412806e39049c2022-12-21T22:23:45ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802017-08-01255Proc. EXPRESS/SOS 2017678210.4204/EPTCS.255.5:10Using Session Types for Reasoning About Boundedness in the Pi-CalculusHans Hüttel0 Department of Computer Science, Aalborg University, Denmark The classes of depth-bounded and name-bounded processes are fragments of the pi-calculus for which some of the decision problems that are undecidable for the full calculus become decidable. P is depth-bounded at level k if every reduction sequence for P contains successor processes with at most k active nested restrictions. P is name-bounded at level k if every reduction sequence for P contains successor processes with at most k active bound names. Membership of these classes of processes is undecidable. In this paper we use binary session types to decise two type systems that give a sound characterization of the properties: If a process is well-typed in our first system, it is depth-bounded. If a process is well-typed in our second, more restrictive type system, it will also be name-bounded.http://arxiv.org/pdf/1709.00829v1 |
| spellingShingle | Hans Hüttel Using Session Types for Reasoning About Boundedness in the Pi-Calculus Electronic Proceedings in Theoretical Computer Science |
| title | Using Session Types for Reasoning About Boundedness in the Pi-Calculus |
| title_full | Using Session Types for Reasoning About Boundedness in the Pi-Calculus |
| title_fullStr | Using Session Types for Reasoning About Boundedness in the Pi-Calculus |
| title_full_unstemmed | Using Session Types for Reasoning About Boundedness in the Pi-Calculus |
| title_short | Using Session Types for Reasoning About Boundedness in the Pi-Calculus |
| title_sort | using session types for reasoning about boundedness in the pi calculus |
| url | http://arxiv.org/pdf/1709.00829v1 |
| work_keys_str_mv | AT hanshuttel usingsessiontypesforreasoningaboutboundednessinthepicalculus |