-
Modal Logics for Nominal Transition Systems
Authors:
Joachim Parrow,
Johannes Borgström,
Lars-Henrik Eriksson,
Ramūnas Forsberg Gutkovas,
Tjark Weber
Abstract:
We define a general notion of transition system where states and action labels can be from arbitrary nominal sets, actions may bind names, and state predicates from an arbitrary logic define properties of states. A Hennessy-Milner logic for these systems is introduced, and proved adequate and expressively complete for bisimulation equivalence. A main technical novelty is the use of finitely suppor…
▽ More
We define a general notion of transition system where states and action labels can be from arbitrary nominal sets, actions may bind names, and state predicates from an arbitrary logic define properties of states. A Hennessy-Milner logic for these systems is introduced, and proved adequate and expressively complete for bisimulation equivalence. A main technical novelty is the use of finitely supported infinite conjunctions. We show how to treat different bisimulation variants such as early, late, open and weak in a systematic way, explore the folklore theorem that state predicates can be replaced by actions, and make substantial comparisons with related work. The main definitions and theorems have been formalised in Nominal Isabelle.
△ Less
Submitted 27 January, 2021; v1 submitted 4 April, 2019;
originally announced April 2019.
-
A Session Type System for Asynchronous Unreliable Broadcast Communication
Authors:
Dimitrios Kouzapas,
Ramunas Forsberg Gutkovas,
A. Laura Voinea,
Simon J. Gay
Abstract:
Session types are formal specifications of communication protocols, allowing protocol implementations to be verified by typechecking. Up to now, session type disciplines have assumed that the communication medium is reliable, with no loss of messages. However, unreliable broadcast communication is common in a wide class of distributed systems such as ad-hoc and wireless sensor networks. Often such…
▽ More
Session types are formal specifications of communication protocols, allowing protocol implementations to be verified by typechecking. Up to now, session type disciplines have assumed that the communication medium is reliable, with no loss of messages. However, unreliable broadcast communication is common in a wide class of distributed systems such as ad-hoc and wireless sensor networks. Often such systems have structured communication patterns that should be amenable to analysis by means of session types, but the necessary theory has not previously been developed. We introduce the Unreliable Broadcast Session Calculus, a process calculus with unreliable broadcast communication, and equip it with a session type system that we show is sound. We capture two common operations, broadcast and gather, inhabiting dual session types. Message loss may lead to non-synchronised session endpoints. To further account for unreliability we provide with an autonomous recovery mechanism that does not require acknowledgements from session participants. Our type system ensures soundness, safety, and progress between the synchronised endpoints within a session. We demonstrate the expressiveness of our framework by implementing Paxos, the textbook protocol for reaching consensus in an unreliable, asynchronous network.
△ Less
Submitted 2 August, 2024; v1 submitted 4 February, 2019;
originally announced February 2019.
-
A Sorted Semantic Framework for Applied Process Calculi
Authors:
Johannes Borgström,
Ramūnas Gutkovas,
Joachim Parrow,
Björn Victor,
Johannes Åman Pohjola
Abstract:
Applied process calculi include advanced programming constructs such as type systems, communication with pattern matching, encryption primitives, concurrent constraints, nondeterminism, process creation, and dynamic connection topologies. Several such formalisms, e.g. the applied pi calculus, are extensions of the the pi-calculus; a growing number is geared towards particular applications or compu…
▽ More
Applied process calculi include advanced programming constructs such as type systems, communication with pattern matching, encryption primitives, concurrent constraints, nondeterminism, process creation, and dynamic connection topologies. Several such formalisms, e.g. the applied pi calculus, are extensions of the the pi-calculus; a growing number is geared towards particular applications or computational paradigms. Our goal is a unified framework to represent different process calculi and notions of computation. To this end, we extend our previous work on psi-calculi with novel abstract patterns and pattern matching, and add sorts to the data term language, giving sufficient criteria for subject reduction to hold. Our framework can directly represent several existing process calculi; the resulting transition systems are isomorphic to the originals up to strong bisimulation. We also demonstrate different notions of computation on data terms, including cryptographic primitives and a lambda-calculus with erratic choice. Finally, we prove standard congruence and structural properties of bisimulation; the proof has been machine-checked using Nominal Isabelle in the case of a single name sort.
△ Less
Submitted 30 March, 2016; v1 submitted 5 October, 2015;
originally announced October 2015.
-
Session Types for Broadcasting
Authors:
Dimitrios Kouzapas,
Ramūnas Gutkovas,
Simon J. Gay
Abstract:
Up to now session types have been used under the assumptions of point to point communication, to ensure the linearity of session endpoints, and reliable communication, to ensure send/receive duality. In this paper we define a session type theory for broadcast communication semantics that by definition do not assume point to point and reliable communication. Our session framework lies on top of the…
▽ More
Up to now session types have been used under the assumptions of point to point communication, to ensure the linearity of session endpoints, and reliable communication, to ensure send/receive duality. In this paper we define a session type theory for broadcast communication semantics that by definition do not assume point to point and reliable communication. Our session framework lies on top of the parametric framework of broadcasting psi-calculi, giving insights on developing session types within a parametric framework. Our session type theory enjoys the properties of soundness and safety. We further believe that the solutions proposed will eventually provide a deeper understanding of how session types principles should be applied in the general case of communication semantics.
△ Less
Submitted 13 June, 2014;
originally announced June 2014.
