Project topics and materials
Get Complete Project Material File(s) Now! »
Preliminaries
In this chapter we introduce the background we shall use throughout the disserta-tion. In Section 2.1 we recall some basic notions about domain theory. In Section 2.2 we define the notions of labeled transition system (LTS), partition and the graph induced by an LTS. In Section 2.3 we proceed to present the standard par-tition refinement algorithm used to check bisimilarity between two LTSs. Finally, in Section 2.4, we present in detail the concurrent constraint programming (CCP) formalism. We introduce its syntax together with its reduction and labeled seman-tics, as well as several equivalence relations including strong, weak bisimilarity and the standard observational equivalence for CCP. The reader familiar with these concepts may skip directly to Chapter 3.
Domain theory
Here we present the basic elements from domain theory that we shall use through-out the dissertation. Most definitions are presented as in [35]. For a more detailed explanation, see for instance [1].
We start with the notion of partially ordered set. Intuitively, a set is partially ordered if it is equipped with a binary relation that is reflexive, transitive and antisymmetric. Its name comes from the fact that the relation indicates the partial order of the elements in the set.
Definition 2.1.1 (Partially ordered set). For a set S with a binary relation v, we say that (S; v) is a partially ordered set, or a poset, if the following three properties hold for all x; y; z 2 S:
1. Reflexivity: x v x.
2. Transitivity: if x v y and y v z then x v z.
3. Antisymmetry: if x v y and y v x then x = y.
If S with relation v is a partially ordered set then v is called a partial order.
Now we define the concept of upper bound. Roughly speaking, given a poset (S; v), an upper bound for a subset A of S is an element u that belongs to S and is greater or equal, w.r.t. the order v, than any element in A.
Definition 2.1.2 (Upper bound). If (S; v) is a poset and A S, then u 2 S is an upper bound for A if for all a 2 A, a v u.
The next definition is that of least upper bound. Intuitively, for a poset (S; v) and a subset A of S, the least upper bound of A is the smallest, w.r.t. v, of all possible upper bounds for A.
Definition 2.1.3 (Least upper bound). If (S; v) is a poset and A S, then u 2 S is the supremum or least upper bound of A if u is an upper bound for A and for all u0 2 S, if u0 is an upper bound for A then u v u0. We denote the least upper bound of a set A as A, and we denote the least upper bound of the set fa1; a2g as a1 t a2. We also refer to a1 t a2 as the lub of a1 and a2.
Now we shall define the directed set: a set is directed if for any pair of elements of the set one can find another element in the set that is above them.
Definition 2.1.4 (Directed set). Suppose (S; v) is a poset, and D S. We say that D is directed if for all a; b 2 D there exists c 2 D such that a v c and b v c.
Using this notion we proceed to define the concept of directed-complete par-tial order.
Definition 2.1.5 (Directed-complete partial order). Suppose (S; v) is a poset. (S; v) is a directed-complete partial order, or dcpo, if every directed subset of S has a least upper bound.
Next we define the concept of compact element. Intuitively, an element is compact if whenever it is smaller than the least upper bound of a directed set D then it is smaller than some element in D. In other words, an element is compact if it can be finitely approximated by one of the elements in D.
Definition 2.1.6 (Compact element). Suppose (S; v) is a dcpo and d 2 S. Then d is a compact element of S if whenever D is a directed subset of S and d v D then there exists d 2 D such that d v d .
The proposition below states that the least upper bound of a finite set of com-pact elements is also compact.
Proposition 2.1.7. If (S; v) is a dcpo and C is a finite set of compact elements of S, then if C exists, it is a compact element of S as well.
The following notion says that a dcpo is algebraic if each element c is the least upper bound of the compact elements below c.
Definition 2.1.8 (Algebraic dcpo). Suppose (S; v) is a dcpo. Let K(S) denote the compact elements of S. (S; v) is algebraic if for every a 2 S, a = fd j d v a and d 2 K(S)g:
Finally, the notion of complete lattice.
Definition 2.1.9 (Complete lattice). (S; v) is a complete lattice if (S; v) is a poset and for every subset A of S, A has a least upper bound.
Note that a complete lattice is always a dcpo. We finish this section with the following proposition. Proposition 2.1.10. Every complete lattice has a unique greatest element and a unique least element.
Labeled Transition System, Partition and Graphs
In this section we present the basic notions of labeled transition system, partition and graphs. Intuitively, a transition system consists of a set of states and arrows between those states representing a transition from one state to the other. Addi-tionally, its labeled version uses a set of labels to tag the transitions typically to denote an interaction with the environment using this piece of information.
Definition 2.2.1 (Labeled Transition System). A labeled transition system (LTS) is a triple (S; L; ) where S is a set of states, L a set of labels and S L S a transition relation. We shall use s a r to denote the transition (s; a; r) 2 . Given a transition t = (s; a; r) we define the source, the target and the label as follows: src(t) = s, tar(t) = r and lab(t) = a. For a transition s a r, we shall often say that s performs the action a and then becomes t.
We now proceed to define the notion of partition of a set. Roughly speaking, a partition of a set S is a division of the set into blocks such that no element is in two blocks at the same time and where the union of all blocks is S.
Definition 2.2.2 (Partition). Given a set S, a partition P of S is a set of non-empty blocks, i.e., subsets of S, that are all disjoint and whose union is S. We write fB1g : : : fBng to denote a partition consisting of (non-empty) blocks B1; : : : ; Bn. A partition represents an equivalence relation where equivalent elements belong to the same block. We write sPr to mean that s and r are equivalent in the partition P:
Finally, we adopt some notation relating LTSs and regular graphs.
Definition 2.2.3 (LTSs and Graphs). Given a LTS (S; L; ), we write LTS for
the directed graph whose vertices are the states in S and edges are the transitions in . Given a set of initial states IS S, we write LTS (IS ) for the subgraph of LTS reachable from IS . Given a graph G we write V(G) and E(G) for the set of vertices and edges of G, respectively.
Partition Refinement
In this section we recall the partition refinement algorithm [34, 50] for checking bisimilarity over the states of an LTS (S; L; ).
First let us introduce the standard notion of strong bisimilarity. Intuitively, two states s and t are considered strongly bisimilar if whenever s performs an action a and becomes s0, i.e. s a s0, then t is able to perform a and reach a t0, i.e. t a t0, such that t0 is equivalent to s0. In short, s and t are bisimilar if they are able to mimic each other’s moves.
Definition 2.3.1 (Standard Strong Bisimilarity). A symmetric relation R is a stan-dard strong bisimulation if for every (s; t) 2 R:
If s a s0 then there exists t0 s.t. t a t0 and (s0; t0) 2 R.
We say that s and t are standard strong bisimilar, written s t, iff there is a standard strong bisimulation containing (s; t).
Given a set of initial states IS S, the partition refinement algorithm (see Algorithm 2.3.1) checks bisimilarity on IS as follows. First, it computes IS ? , that is the set of all states that are reachable from IS using . Then it creates the partition P0 where all the elements of IS ? belong to the same block (i.e., they are all equivalent). After the initialization, it iteratively refines the partitions by employing the function on partitions F ( ), defined as follows:
Definition 2.3.2 (Refinement Function). Given a partition P we define F (P) as follows: sF (P)r iff
if s a s0 then exists r0 s.t. r a r0 and s0Pr0.
The Figure 2.3.1 shows an example of F (P). Algorithm 2.3.1 terminates whenever two consecutive partitions are equivalent. In such a partition two states (reachable from IS ) belong to the same block iff they are bisimilar (using the standard notion of bisimilarity [41]).
Concurrent Constraint Programming (CCP)
We dedicate this section entirely to presenting the Concurrent Constraint Program-ming (CCP) formalism. We begin this section by recalling the notion of constraint system. We then introduce the syntax of CCP, its operational and labeled seman-tics as well as several notions of equivalence for CCP.
Constraint Systems
The CCP model is parametric in a constraint system (cs) specifying the structure and interdependencies of the information that processes can ask or add to a central shared store. This information is represented as assertions traditionally referred to as constraints.
Following [21, 40] we regard a cs as a complete algebraic lattice (Definitions 2.1.8 and 2.1.9) in which the ordering v is the reverse of an entailment relation: c v d means d entails c, i.e., d contains “more information” than c. The top element false represents inconsistency, the bottom element true is the empty con-straint, and the least upper bound (lub) t is the join of information.
Definition 2.4.1 (Constraint Systems). A constraint system (cs) C is a complete algebraic lattice (Con; Con0; v; t; true; false) where Con; the set of constraints, is a partially ordered set w.r.t. v, Con0 is the subset of compact elements of Con,t is the lub operation defined on all subsets, and true, false are the least and greatest elements of Con, respectively.
Recall that C is a complete lattice if every subset of Con has a least upper bound in Con. An element c 2 Con is compact if for any directed subset D of 2 is F Con, c v D implies c v d for some d 2 D. C is algebraic if each element c Con the least upper bound of the compact elements below c.
In order to model hiding of local variables and parameter passing, in [63]
the notion of constraint system is enriched with cylindrification operators and diagonal elements, concepts borrowed from the theory of cylindric algebras [45].
Let us consider a (denumerable) set of variables Var with typical elements x; y; z; : : : and let us define 9Var as the family of operators and DVar as the set as follows:
9Var = f9x j x 2 Varg (cylindric operators)
DVar = fdxy j x; y 2 Varg (diagonal elements)
A cylindric constraint system over a set of variables Var is a constraint system whose underlying support set Con DVar is closed under the cylindric operators 9Var and quotiented by Axioms C1 C4, and whose ordering v satisfies Axioms
C5 C7:
C1: 9x9yc = 9y9xc C2: dxx = true
C3: if z 6= x; y then dxy = 9z(dxz t dzy) C4: 9x(c t 9xd) = 9xc t 9xd
C5: 9xc v c C6: if c v d then 9xc v 9xd
C7: if x 6= y then c v dxy t 9x(c t dxy)
where c and d indicate compact constraints, and 9xc t d stands for (9xc) t d. For our purposes, it is enough to think of the operator 9x as existential quantifier and the constraint dxy as the equality x = y.
Cylindrification and diagonal elements allow us to model the variable renam-ing of a formula ; in fact, by the aforementioned axioms, we have that the for-mula 9x(dxy t ) can be depicted as the formula [y=x], i.e., the formula obtained from by replacing all free occurrences of x by y.
We assume notions of free variable and of substitution that satisfy the following conditions, where c[y=x] is the constraint obtained by substituting x by y in c and fv(c) is the set of free variables of c:
(1) if y 2= fv(c) then (c[y=x])[x=y] = c;
(2) (c t d)[y=x] = c[y=x] t d[y=x];
(3) x 2= fv(c[y=x]);
(4) fv(c t d) = fv(c) [ fv(d).
Table of contents :
Abstract
Résumé
1 Introduction
1.1 Motivation
1.2 Context
1.2.1 Concurrent Constraint Programming (CCP)
1.2.2 Equivalences for CCP
1.3 This Dissertation
1.3.1 Checking Strong Bisimilarity in CCP
1.3.2 Reducing Weak to Strong Bisimilarity
1.3.3 Computing Bisimilarity in choice-free CCP
1.3.4 A Behavioral Congruence for CCP
1.4 Contributions and Organization
1.5 Publications from this Dissertation
2 Preliminaries
2.1 Domain theory
2.2 Labeled Transition System, Partition and Graphs
2.3 Partition Refinement
2.4 Concurrent Constraint Programming (CCP)
2.4.1 Constraint Systems
2.4.2 Syntax of CCP
2.4.3 Reduction Semantics
2.4.4 Barbed Semantics and Barbed Bisimilarity
2.4.5 Observational Equivalence
2.4.6 Labeled Semantics
2.4.7 Soundness and Completeness
2.4.8 Strong and Weak Labeled Bisimilarity
3 Verifying Strong Bisimilarity in CCP
3.1 Partition Refinement for CCP
3.1.1 Derivation and Domination
3.1.2 The Algorithm
3.2 Correctness and Complexity
3.2.1 Irredundant and Symbolic Bisimilarity
3.2.2 Proof of Correctness and Complexity
3.3 Summary and Related Work
4 A Weak Semantics for CCP
4.1 The standard reduction from weak to strong
4.1.1 Incompleteness of Milner’s saturation method in CCP
4.2 Reducing Weak Bisimilarity to Strong in CCP
4.2.1 Defining a new saturation method for CCP
4.2.2 The new saturation method is finitely branching
4.2.3 A Remark about our Saturation in CCS
4.2.4 Soundness and Completeness
4.3 Deciding Weak Bisimilarity
4.3.1 Weak Irredundant andWeak Saturated Bisimilarity coincide
4.3.2 Algorithm for weak bisimilarity in CCP
4.4 Summary and Related Work
5 Computing bisimilarity in Choice-Free CCP
5.1 Using Partition Refinement in choice-free CCP
5.1.1 Properties of CCP without choice
5.1.2 Optimizing partition refinement for choice-free CCP
5.2 The compact input-output sets approach
5.2.1 Weak bisimilarity and barb equivalence
5.2.2 A canonical representation of choice-free configurations
5.3 Improving the general partition refinement for CCP
5.4 Summary and Related Work
6 A Behavioral Congruence for CCP
6.1 Congruence issues
6.2 Weak full bisimilarity
6.2.1 More than weak barbs
6.2.2 Full Bisimilarity is a Congruence
6.2.3 Relation with observational equivalence
6.2.4 Behavioral congruence
6.3 Summary and Related Work
7 Conclusions
7.1 Summary
7.2 Future Work
