Project topics and materials
Get Complete Project Material File(s) Now! »
Bisimilarity for CCP
Concurrency is concerned with the fundamental aspects of systems of multiple computing agents, usually called processes, that interact with each other. Proc-ess calculi treat processes much like the λ-calculus treats computable functions. They provide a language in which processes are represented by terms, and com-putational steps are represented as transitions between them.
Co-induction [JR97, San09, San11] is the most natural and powerful approach to define and reason about infinite or circular structures and computations, bring-ing in tools and methods that are dual and complementary to those of induc-tion. In particular, coinduction is central in concurrency, where processes are naturally seen as entities that continuously interact with their environment. Co-induction, in the form of bisimulation, is used to define equality between proc-esses, and the coinduction proof method, in the form of the bisimulation proof method, is employed to prove such equalities. The largest bisimulation, bisim-ilarity [Mil80, Mil99], captures an intuitive notion of process equivalence; two processes are equivalent if they can match each other’s moves. Concurrent Constraint Programming (ccp) [SR90] is a well-established for-malism that combines the traditional algebraic and operational view of process calculi with a declarative one based upon first-order logic. In ccp, processes in-teract by posting (or telling) and asking information (traditionally referred to as constraints) in a medium (referred to as the store). Ccp is parametric in a cons-traint system indicating interdependencies (entailment) between constraints and providing for the specification of data types and other rich structures. The above features have recently attracted a renewed attention as witnessed by the works [PSVV06, BM08, BJPV09, BZ10] on calculi exhibiting data-types, logic asser-tions as well as tell and ask operations.
Surprisingly, the development of co-inductive techniques, in particular, of bisimulation for ccp has been so far too little considered. There have been few attempts to define a notion of bisimilarity for ccp. The ones we are aware of are those in [SR90] and [MPSS95] upon which we build. These equivalences are not completely satisfactory: We shall demonstrate in this thesis that the first one may tell apart processes with identical observable behavior, while the second quantifies over all possible inputs from the environment, and hence it is not clear whether it can lead to a feasible proof technique.
In this dissertation we shall introduce a notion of bisimilarity for ccp that al-lows us to benefit of the feasible proof and verification techniques typically asso-ciated with bisimilarity. Furthermore, we aim at studying the relationship between this equivalence and other existing semantic notions for ccp. In particular, its el-egant denotational characterization based on closure operators [SRP91] and the connection with logic [MPSS95].
Labeled Semantics
Bisimilarity relies on labeled transitions: each evolution step of a system is tagged by some information aimed at capturing the possible interactions of a process with the environment. Nowadays process calculi tend to adopt reduction semantics based on unlabeled transitions and barbed congruence [MS92a]. The main draw-back of this approach is that to verify barbed congruences it is often necessary to analyze the behavior of processes under every context.
This scenario has motivated a novel stream of research [Sew98, LM00, EK04, SS05, BKM06, RS08, GHL08, BGM09] aimed at defining techniques for “deriv-ing labels and bisimilarity” from unlabeled reduction semantics. The main intu-ition is that labels should represent the “minimal contexts allowing a process to reduce”. The theory of reactive systems by Leifer and Milner [LM00] provides a formal characterization (by means of a categorical construction) of such “minimal contexts” and it focuses on the bisimilarity over transition systems labeled as:
C
P −→ P ′ iff C[P ] −→ P ′
where C is the minimal context allowing such reduction.
In [BKM06, BGM09], it is argued that the above bisimilarity is often too fine grained and an alternative, coarser, notion of bisimilarity is provided. Intuitively
in the bisimulation game each move (transition) C ′ has to be matched with P −→P
a move C[Q] −→ Q′, where C[−] is not necessarily the minimal.
Labeled Semantics for ccp. The operational semantics of ccp is expressed by reductions between configurations of the form P, d −→ P ′, d′ meaning that the process P with store d may reduce to P ′ with store d′. From this semantics we shall derive a labeled transition system for ccp by exploiting the intuition of [Sew98, LM00] means that e is a “minimal constraint” (from the environment) that needs to be added to d to reduce from P, d into P ′, d′ .
Similar ideas were already proposed in [SR90], but the recent developments in [BGM09] enlighten the way for obtaining a fully abstract equivalence. Indeed, the standard notion of bisimilarity defined on our labeled semantics can be seen as an instance of the one proposed in [LM00]. As for the bisimilarity in [SR90], it is too fine grained, i.e., it separates processes which are behaviorally indistinguishable. Instead, the notion of bisimulation from [BGM09] (instantiated to the case of ccp) is fully abstract with respect to the standard observational equivalence given in [SRP91]. Our work can therefore be also regarded as a compelling application of the theory of reactive systems.
Algorithms
A fundamental issue in concurrency concerns the analysis techniques. That is, methods and tools to decide equivalence between behaviours, or more generally to prove behavioural properties of a concurrent system. The tractability of a tech-nique is important: we need techniques which make proofs shorter, and reduce the number of cases to be examined when analysing a behaviour. Tools may be derived out of the techniques, to permit automatic or semi-automatic analysis.
Many efficient algorithms and tools for bisimilarity checking have been devel-oped [VM94, Fer89, FGM+98]. Among these, the partition refinement algorithm [KS83] is the best known: first it generates the state space of a labeled transi-tion system (LTS), i.e., the set of states reachable through the transitions; then, it creates a partition equating all states and afterwards, iteratively, refines these par-titions by splitting non equivalent states. At the end, the resulting partition equates all and only bisimilar states.
The ccp formalism has been widely investigated and tested in terms of the-oretical studies and the implementation of several ccp programming languages. From the applied computing point of view, however, ccp lacks algorithms and tools to automatically verify program equivalence. Furthermore, the absence of a well-behaved notion of bisimilarity for ccp made the development of tools for automatic verification in ccp somewhat a pointless effort. Therefore, after intro-ducing a suitable definition of bisimilarity for ccp, we shall give the first step towards automatic verification of ccp program equivalences by presenting an al-gorithm based on an alternative notion of bisimilarity, namely saturated barbed bisimilarity (∼˙sb) for ccp.
Two configurations are equivalent according to ∼˙sb if (i) they have the same store, (ii) their transitions go into equivalent states and (iii) they are still equivalent when adding an arbitrary constraint to the store. We shall also prove that the weak variant of ∼˙sb is shown to be fully abstract w.r.t. the standard observational equivalence of [SRP91].
Table of contents :
Abstract
Acknowledgments
1 Introduction
1.1 Bisimilarity for CCP
1.2 Labeled Semantics
1.3 Algorithms
1.4 From Weak to Strong Bisimilarity
1.5 Summary of Contributions and Organization
1.6 Publications from this Dissertation
2 Deriving Labels and Bisimilarity for CCP
2.1 Background
2.1.1 Constraint Systems
2.1.2 Syntax
2.1.3 Reduction Semantics
2.1.4 Observational Equivalence
2.2 Saturated Bisimilarity for CCP
2.2.1 Saturated Barbed Bisimilarity
2.2.2 Correspondence with Observational Equivalence
2.3 Labeled Semantics
2.4 Strong and Weak Bisimilarity
2.5 Summary of Contributions and Related Work
3 Partition Refinement for Bisimilarity in CCP
3.1 Background
3.1.1 Partition Refinement
3.2 Irredundant Bisimilarity
3.2.1 Reduction Semantics for Non-deterministic CCP
3.2.2 Labeled Semantics for Non-deterministic CCP
3.2.3 Saturated Bisimilarity in a Non-deterministic CCP Fragment
3.2.4 Soundness and Completeness
3.2.5 Syntactic Bisimilarity and Redundancy
3.2.6 Symbolic and Irredundant Bisimilarity
3.3 Partition Refinement for CCP
3.3.1 Termination
3.3.2 Complexity of the Algorithm
3.4 Summary of Contributions and Related Work
4 ReducingWeak to Strong Bisimilarity in CCP
4.1 Background
4.1.1 Reducing Weak to Strong Bisimilarity
4.2 Defining a New Saturation Method for CCP
4.2.1 A New Saturation Method
4.2.2 A Remark about our Saturation in CCS
4.2.3 Soundness and Completeness
4.3 Correspondence between ≈˙ sb, ∼˙ sym, ∼˙ I
4.4 Algorithm for the Weak Notion of the CCP Partition Refinement Algorithm
4.5 Summary of Contributions and Related Work
5 Conclusions
A Implementation and Experiments for the CCP Partition Refinement
A.1 Programming Language
A.2 Abstract Data Types
A.2.1 Implementation Layout
A.2.2 Layout of the Automaton
A.2.3 Layout of the Redundant Class
A.2.4 Layout of a Tool to Verify Bisimilarity in CCP
A.3 Procedures and Functions
A.3.1 Calculating Irredundancy
A.3.2 Strong Prerefinement
A.3.3 Weak Prerefinement
A.3.4 Final Algorithm
A.3.5 Final Strong Algorithm
A.3.6 Saturation
A.3.7 Final Weak Algorithm
A.4 Results and Examples
A.4.1 Transitions/Nodes
A.4.2 Percentage of Same Labels
A.4.3 Percentage of Configurations Satisfying the Same Barb
A.4.4 Percentage of Dominated Transitions
A.4.5 Time vs Branches
A.5 Summary of Contributions and Related Work .
