7.4 KiB
A (finite non-deterministic) automaton is a quintuple M = (Q,Act,q0,F,T), where:
- Q is the set of states
- Act is the set of actions
- q0 is the starting state
- F is the set of final states
- T is the transition relation (T ⊆ Q × Act × Q)
Automata Behaviour: language equivalence (where L(M) is the set of all the sequences of input characters that bring the automaton M from its starting state to a final one)
[!note] Language equivalence M1 and M2 are language equivalent if and only if L(M1)=L(M2)
By considering the starting states as also final, they both generate the same language, i.e.:
(20.(tea + 20.coffee))∗ = (20.tea + 20.20.coffee)∗But, do they behave the same from the point of view of an external observer??
The essence of the difference is WHEN the decision to branch is taken
- language equivalence gets rid of branching points
- it is too coarse for our purposes!
LTSs
In concurrency theory, we don’t use finite automata but Labeled Transition System (LTS). The main differences between the two formalisms are:
- automata usually rely on a finite number of states, whereas states of an LTS can be infinite
- automata fix one starting state, whereas in an LTS every state can be considered as initial (this corresponds to different possible behaviors of the process)
- automata rely on final states for describing the language accepted, whereas in LTS this notion is not very informative
[!note] LTS formal definition Fix a set of action names (or, simply, actions), written N.
A Labeled Transition System (LTS) is a pair (Q, T), where Q is the set of states and T is the transition relation (T ⊆ Q × N × Q).
We shall usually write s –a–> s′ instead of ⟨s,a,s′⟩ ∈ T.
Bisimulation
Intuitively, two states are equivalent if they can perform the same actions that lead them in states where this property still holds
P0 and Q0 are different because, after an a, the former can decide to do b or c, whereas the latter must decide this before performing a.
Let (Q,T) be an LTS. A binary relation S ⊆ Q×Q is a simulation if and only if ∀(p,q) ∈ S∀p –a–> p′∃q –a–> q′ s.t. (p′,q′) ∈ S
We say that p is simulated by q if there exists a simulation S such that (p,q) ∈ S
We say that S is a bisimulation if both S and S−1 are simulations (where S^{-1} = \{(p,q) : (q,p) ∈ S\})
Two states q and p are bisimulation equivalent (or, simply, bisimilar) if there exists a bisimulation S such that (p, q) ∈ S; we shall then write p ∼ q.
q0 is simulated by p0; this is shown by the following simulation relation: S = \{(q0,p0), (q1,p1), (q2,p1), (q3,p2), (q4,p3)\}
To let p0 be simulated by q0, we should have that p1 is simulated by q1 or q2.
If S contained one among (p1,q1) or (p1,q2), then it would not be a simulation: indeed, p1 can perform both a c (whereas q1 cannot) and a b (whereas q2 cannot).
Remark: for proving equivalence, it is NOT enough to find a simulation of p by q and a simulation of q by p
p0 is simulated by q0: S = {(p0, q0), (p1, q2), (p2, q3)}
q0 is simulated by p0: S′ ={(q0,p0),(q1,p1),(q2,p1),(q3,p2)}
However, p0 and q0 are not bisimilar: the transition q0 -> a -> q1 is not bisimulable by any transition from p0 (ndeed, p0 –a–> p1 does not suffice, because p1 can perform a b and so cannot be bisimilar to q1).
Bisimulation is NOT isomorfism
S = \{(p0,q0), (p1,q1), (p2,q1), (p0,q2)\}
S^{−1} = \{(q0,p0), (q1,p1), (q1,p2), (q2,p0)\}
[!def] Theorem Bisimilarity is an equivalence relation
Proof:
Reflexivity: we have to show that q ∼ q, for every q. Consider the following relation S ={(p,p):p∈Q} and observe that it is a bisimulation (the inverse is S itself).
Symmetry: we have to show that p ~ q implies q ~ p, for every p, q.
By hypothesis, there exists a bisimulation S that contains the pair (p, q). By definition of bisimulation, S^{-1} is a simulation; hence, (q, p) \in S^{-1} and, consequently, q ~ p.
Transitivity: we have to show that p ~ q and q ~ r imply p ~ r for all p, r, q. Let's consider the following relation: S = \{(x, y): \exists y : (x, y) \in S_{1} \land(y,z)\in S_{2}\}
where S1 and S2 are bisimulations, then we have to show that S is a bisimulation.
- let
(x, y) \in Sand x -a-> x' - if
(x, z)belongs to S, then, by definition, there exists y such that(x, y) \in S_{1}and(y, z) \in S_{2} - since S1 is a bisimulation, there exists y -a-> y' such that
(x', y') \in S_{1} - since S2 is a bisimulation, there exists z -a-> z' such that
(y', z') \in S_{2} - hence, from x -a-> x', we found z -a-> z' such that
(x', z') \in S, because there exists a y' such that(x', y') \in S_{1}and(y',z') \in S_{2}.
Theorem: ∼ is a bisimulation. Proof: The proof is done by showing that ∼ is a simulation.
By definition of similarity, we have to show that ∀(p,q)∈∼ ∀p –a–> p′ ∃q –a–> q′ s.t.(p′,q′)∈∼ Let us fix a pair (p,q) ∈∼ Bisimilarity of p and q implies the existence of a bisimulation S such that (p,q) ∈ S. Hence, for every transition p –a–> p′, there exists a transition q –a–> q′ such that (p′, q′) ∈ S. So, (p', q') ∈ ∼
Theorem: For every bisimulation S, it holds that S ⊆ ∼. Proof: Let (p,q) ∈ S. Then, there exists a bisimulation that contains the pair (p, q); thus, (p, q) ∈ ∼.
La parte difficile
The only ingredients we used to write down an LTS are:
- sequential compsition (of an action and a process)
- non-deterministic choice (between a finite set of prefixed processes)
- recursion
To simplify process writing, we shall assume to have a finite set Id of processes identifiers and that the definitions we shall give will be parametric
For every identifier (denoted with capital letters A,B,..), we shall assume a unique definition of the form A(x1,x2,..,xn) := P, where names x1,x2,..,xn are all distinct and all included in the names of P.
Let us denote with P{b1/x1 . . . bn/xn} the process obtained from P by replacing name xi with name bi, for every i = 1,..., n.
[!def] The set of non-deterministic processes is given by the following grammar:
P::= \sum \alpha_{i}.P_{i} | A(a_{1}\dots a_{n})where I is a finite set of indices and \alpha_{i} \in A for every i \in I.
Remark: we now fuse together in a unique operator sequential composition and nondeterministic choice.
If the index set I is empty, then \sum_{i\in I} \alpha_{i}.P_{i} is the terminated process, that cannot perform any action; this process will be represented with the symbol 0.
We shall usually omit tail occurrences of ‘.0’ and, for example, simply write a.b instead of a.b.0
From the syntax to the LTS
From the syntax to the LTS We have shown how it is possible, starting from an LTS, to generate a corresponding process
It is also possible the inverse translation and then the two formalisms do coincide; the rules that have to be used in this translation are:
examples