2.1 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.