scholarly journals Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types

2020 ◽  
pp. 251-279 ◽  
Author(s):  
Sung-Shik Jongmans ◽  
Nobuko Yoshida
Keyword(s):  
Parallel Composition ◽  
Model Checker ◽  
Practical Result ◽  
Session Types ◽  
Deadlock Freedom ◽  
Algebraic Framework ◽  
A New Technique ◽  
Global Type ◽  
Existential Quantification ◽  
Process Algebraic

AbstractA key open problem with multiparty session types (MPST) concerns their expressiveness: current MPST have inflexible choice, no existential quantification over participants, and limited parallel composition. This precludes many real protocols to be represented by MPST. To overcome these bottlenecks of MPST, we explore a new technique using weak bisimilarity between global types and endpoint types, which guarantees deadlock-freedom and absence of protocol violations. Based on a process algebraic framework, we present well-formed conditions for global types that guarantee weak bisimilarity between a global type and its endpoint types and prove their check is decidable. Our main practical result, obtained through benchmarks, is that our well-formedness conditions can be checked orders of magnitude faster than directly checking weak bisimilarity using a state-of-the-art model checker.

scholarly journals Relations among quantum processes: bisimilarity and congruence

2006 ◽  
Vol 16 (3) ◽  
pp. 407-428 ◽  
Author(s):  
MARIE LALIRE
Keyword(s):  
Quantum Communication ◽  
Operational Semantics ◽  
Parallel Composition ◽  
Quantum Processes ◽  
Algebraic Notation ◽  
Distributed Computations ◽  
Quantum Objects ◽  
Branching Bisimulation ◽  
Classical Computing ◽  
Process Algebraic

Full formal descriptions of algorithms making use of quantum principles must take into account both quantum and classical computing components, as well as communications between these components. Moreover, to model concurrent and distributed quantum computations and quantum communication protocols, communications over quantum channels that move qubits physically from one place to another must also be taken into account.Inspired by classical process algebras, which provide a framework for modelling cooperating computations, a process algebraic notation is defined. This notation provides a homogeneous style for formal descriptions of concurrent and distributed computations comprising both quantum and classical parts. Based upon an operational semantics that makes sure that quantum objects, operations and communications operate according to the postulates of quantum mechanics, an equivalence is defined among process states considered as having the same behaviour. This equivalence is a probabilistic branching bisimulation. From this relation, an equivalence on processes is defined. However, it is not a congruence because it is not preserved by parallel composition.

scholarly journals A process algebraic framework for specification and validation of real-time systems

2009 ◽  
Vol 22 (2) ◽  
pp. 153-191 ◽  
Author(s):  
Adnan Sherif ◽  
Ana Cavalcanti ◽  
He Jifeng ◽  
Augusto Sampaio
Keyword(s):  
Real Time ◽  
Real Time Systems ◽  
Algebraic Framework ◽  
Time Systems ◽  
Process Algebraic

scholarly journals Propositions as sessions

2014 ◽  
Vol 24 (2-3) ◽  
pp. 384-418 ◽  
Author(s):  
PHILIP WADLER
Keyword(s):  
Linear Functional ◽  
Linear Logic ◽  
Functional Language ◽  
Session Types ◽  
Deadlock Freedom ◽  
First Time ◽  
Standard Presentation

AbstractContinuing a line of work by Abramsky (1994), Bellin and Scott (1994), and Caires and Pfenning (2010), among others, this paper presents CP, a calculus, in which propositions of classical linear logic correspond to session types. Continuing a line of work by Honda (1993), Hondaet al. (1998), and Gay & Vasconcelos (2010), among others, this paper presents GV, a linear functional language with session types, and a translation from GV into CP. The translation formalises for the first time a connection between a standard presentation of session types and linear logic, and shows how a modification to the standard presentation yields a language free from races and deadlock, where race and deadlock freedom follows from the correspondence to linear logic.

scholarly journals On projecting processes into session types

2012 ◽  
Vol 22 (2) ◽  
pp. 237-289 ◽  
Author(s):  
LUCA PADOVANI
Keyword(s):  
Grounded Theory ◽  
Composition Operator ◽  
Parallel Composition ◽  
Session Types ◽  
Session Type ◽  
Type Preservation

We define session types as projections of the behaviour of processes with respect to the operations processes perform on channels. This calls for a parallel composition operator over session types denoting the simultaneous access to a channel by two or more processes. The proposed approach allows us to define a semantically grounded theory of session types that does not require the linear usage of channels. However, type preservation and progress can only be guaranteed for processes that never receive channels they already own. A number of examples show that the resulting framework validates existing session-type theories and unifies them to some extent.

scholarly journals Global progress for dynamically interleaved multiparty sessions

2014 ◽  
Vol 26 (2) ◽  
pp. 238-302 ◽  
Author(s):  
MARIO COPPO ◽  
MARIANGIOLA DEZANI-CIANCAGLINI ◽  
NOBUKO YOSHIDA ◽  
LUCA PADOVANI
Keyword(s):  
Type System ◽  
Single Session ◽  
Interaction Type ◽  
System A ◽  
Session Types ◽  
Global Type ◽  
Structured Communication

A multiparty session forms a unit of structured communication among many participants which follow communication sequences specified as a global type. When a process is engaged in two or more sessions simultaneously, different sessions can be interleaved and can interfere at runtime. Previous work on multiparty session types has ignored session interleaving, providing a limited progress property ensured only within a single session, by assuming non-interference among different sessions and by forbidding delegation. This paper develops, besides a more traditional, compositionalcommunicationtype system, a novel staticinteractiontype system for global progress in dynamically interleaved and interfered multiparty sessions. The interaction type system infers causalities of channels making sure that processes do not get stuck at intermediate stages of sessions also in presence of delegation.

Sign in / Sign up

Export Citation Format

Share Document