Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userInference Systems with Corules for Combined Safety and Liveness Properties of Binary Session Types
60
0
0.0
(
0
)
Added by
Luca Padovani
Publication date
2021
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
Many properties of communication protocols combine safety and liveness aspects. Characterizing such combined properties by means of a single inference system is difficult because of the fundamentally different techniques (coinduction and induction, respectively) usually involved in defining and proving them. In this paper we show that Generalized Inference Systems allow for simple and insightful characterizations of (at least some of) these combined inductive/coinductive properties of binary session types. In particular, we illustrate the role of corules in characterizing fair termination (the property of protocols that can always eventually terminate), fair compliance (the property of interactions that can always be extended to reach client satisfaction) and fair subtyping, a liveness-preserving refinement relation for session types.
rate research
Read More
We present a sound and complete method for the verification of qualitative liveness properties of replicated systems under stochastic scheduling. These are systems consisting of a finite-state program, executed by an unknown number of indistinguishable agents, where the next agent to make a move is determined by the result of a random experiment. We show that if a property of such a system holds, then there is always a witness in the shape of a Presburger stage graph: a finite graph whose nodes are Presburger-definable sets of configurations. Due to the high complexity of the verification problem (non-elementary), we introduce an incomplete procedure for the construction of Presburger stage graphs, and implement it on top of an SMT solver. The procedure makes extensive use of the theory of well-quasi-orders, and of the structural theory of Petri nets and vector addition systems. We apply our results to a set of benchmarks, in particular to a large collection of population protocols, a model of distributed computation extensively studied by the distributed computing community.
Often fairness assumptions need to be made in order to establish liveness properties of distributed systems, but in many situations they lead to false conclusions. This document presents a research agenda aiming at laying the foundations of a theory of concurrency that is equipped to ensure liveness properties of distributed systems without making fairness assumptions. This theory will encompass process algebra, temporal logic and semantic models. The agenda also includes the development of a methodology and tools that allow successful application of this theory to the specification, analysis and verification of realistic distributed systems. Contemporary process algebras and temporal logics fail to make distinctions between systems of which one has a crucial liveness property and the other does not, at least when assuming justness, a strong progress property, but not assuming fairness. Setting up an alternative framework involves giving up on identifying strongly bisimilar systems, inventing new induction principles, developing new axiomatic bases for process algebras and new congruence formats for operational semantics, and creating matching treatments of time and probability. Even simple systems like fair schedulers or mutual exclusion protocols cannot be accurately specified in standard process algebras (or Petri nets) in the absence of fairness assumptions. Hence the work involves the study of adequate language or model extensions, and their expressive power.
83 -
Bogdan Aman (Romanian Academy
, Institute of Computer Science andn A.I.Cuza University
, Iasi
2019
This paper deals with the probabilistic behaviours of distributed systems described by a process calculus considering both probabilistic internal choices and nondeterministic external choices. For this calculus we define and study a typing system which extends the multiparty session types in order to deal also with probabilistic behaviours. The calculus and its typing system are motivated and illustrated by a running example.
Often fairness assumptions need to be made in order to establish liveness properties of distributed systems, but in many situations these lead to false conclusions. This document presents a research agenda aiming at laying the foundations of a theory of concurrency that is equipped to ensure liveness properties of distributed systems without making fairness assumptions. This theory will encompass process algebra, temporal logic and semantic models, as well as treatments of real-time. The agenda also includes developing a methodology that allows successful application of this theory to the specification, analysis and verification of realistic distributed systems, including routing protocols for wireless networks. Contemporary process algebras and temporal logics fail to make distinctions between systems of which one has a crucial liveness property and the other does not, at least when assuming justness, a strong progress property, but not assuming fairness. Setting up an alternative framework involves giving up on identifying strongly bisimilar systems, inventing new induction principles, developing new axiomatic bases for process algebras and new congruence formats for operational semantics, and creating new treatments of time and probability. Even simple systems like fair schedulers or mutual exclusion protocols cannot be accurately specified in standard process algebras (or Petri nets) in the absence of fairness assumptions. Hence the work involves the study of adequate language or model extensions, and their expressive power.
This paper poses that transition systems constitute a good model of distributed systems only in combination with a criterion telling which paths model complete runs of the represented systems. Among such criteria, progress is too weak to capture relevant liveness properties, and fairness is often too strong; for typical applications we advocate the intermediate criterion of justness. Previously, we proposed a definition of justness in terms of an asymmetric concurrency relation between transitions. Here we define such a concurrency relation for the transition systems associated to the process algebra CCS as well as its extensions with broadcast communication and signals, thereby making these process algebras suitable for capturing liveness properties requiring justness.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
