形式语言与自动机_笔记整理(五)_迁移系统

Transition System

Transition system homomorphism
The free product of transition systems

The synchronous product of transition systems
Modeling sequential circuits

Model logical dynamical system

Model a Mutual Exclusion Protocol

CTL
CTL formulas
Path quantifiers

Temporal operators

Two types of formulas in CTL

Semantics of CTL

Two sublogics of CTL

Ten basic CTL operators

Express Properties

Transition System

A transition systems is a tuple =<S,S0,T,α,β>, where

S is a finite or infinite set of states,

S0 is initial location

T is a finite or infinite set of transitions,

α and β are two mapping from T to S which take each transition t in T to the two states α(t) and β(t), respectively the source and the target of the transition t.

A transition t with some source s and target s′ is written t:s→s′.

Several transitions can have the same source and target.

A transition system is finite if S and T are finite.

A path of length n, n>0, in a transition system  is a sequence of transitions t1,t2,⋯,tn,such that ∀i:1≤i<n,β(ti)=α(ti+1),and α(t1)=S0

Similarly, an infinite path is an infinite sequence of transitions t1,t2,⋯,tn,⋯ such that ∀i:1≤i<n,β(ti)=α(ti+1),and α(t1)=S0

If ∃t∈T, α(t)=s∩β(t)=s′, we say s→s′, we define the generalized transition relation ↠⊆S×A×S such that

If s→s′, s↠s′

If s→s′, s′↠s″, we say s↠s″

Let =<S,S0,T,α,β> be a TS, we say s is reachable if s∈S, s0∈S0, s0↠s.

Let T be a transition system. A state s is a terminal state of T if there are no state s′ such that s→s′.

A state s is a deadlock state of T if s is reachable and terminal.

Write T+ for the set of finite paths and Tw for the set of infinite paths. The mappings α and β can be extended to T+ by defining α(t1…tn)=α(t1),β(t1…tn)=β(tn)

Similarly, the mapping α is extended to Tw by defining α(t1…)=α(t1)

A partial product over T+ is defined as

if c=t1…tn is a path of length n, if c′=t′1…t′n is a path of length m, and if β(c)=α(c′)

c⋅c′=t1…tnt′1…t′m is a finite path of length n+m and α(c⋅c′)=α(c), β(c⋅c′)=β(c′).

Empty path: for each state s of S, define the empty path εs of length zero, and αεs)=β(εs)=s.

A transition system labeled by an alphabet A is a 6-tuple =<S,S0,T,α,β,λ> where

=<S,S0,T,α,β> is a transition system,

λ is a mapping from T to A taking each transition t to its label λ(t).

Intuitively, the label of a transition indicates the action or event which triggers the transition.

If c=t1,t2⋯, is a path in a labeled transition system, the sequence of actions trace(c) = λ(t1),λ(t2)⋯ is called the trace of the path.

Transition system homomorphism

Definition:

Let =<S,S0,T,α,β> and ′=<S′,S′0,T′,α′,β′> be two transition systems. A homomorphism h from  to ′ is a pair (hσ,hτ) of mappings

hσ:S→S′, hτ:T→T′

which satisfies, for every transition t of T:

α′(hτ(t))=(hσα(t))

β′(hτ(t))=(hσβ(t))

Labeled transition system homomorphism

Let =<S,S0,T,α,β,λ> and ′=<S′,S′0,T′,α′,β′,λ′> be two transition systems labeled by the same alphabet. A labeled transition system homomorphism from  to ′ is a homomorphism h which also satisfies the condition λ′(hτ(t))=λ(t).

A homomorphism h is surjective if the two mappings hσ and hτ are surjective. If h is a surjective homomorphism from  to ′, the transition system ′ is the quotient of  under h.

A TS strong isomorphism is a TS homomorphism where hσ and hτ are bijective. In this case, the inverse mappings g=<hσ, hτ> is itself a isomorphism.

If two TS are strong isomorphic, the only difference can be how they are named.

Isomorphic is a kind of equivalence.

If the isomorphism function is defined on reach(T) = {s∈S|s0↠s} , then we call these two systems weak isomorphic with each other.

Theorem:

If two transition systems are isomorphic, then they are weakly isomorphic.

Weak isomorphism is an equivalence relation.

Let T and T′ be two TS, a bisimulation between T and T′ is a binary relation B⊆S×S′ such that

B(s0,s′0)

If B(s1,s′1) and s1→s2, then there is a s′2∈S′ such that s′1→s′2and B(s2,s′2)

If B(s1,s′1) and s′1→s′2, then there is a s2∈S such that s1→s2and B(s2,s′2)

T and T′ are bisimulation equivalent iff there exists a bisimulation between T and T′.

Strong Isomorphism: the transition systems are identical except for the names of the states.

Weak Isomorphism: the transition systems are strongly isomorphic provided that the transition systems are restricted to the reachable states.

Bisimulation Equivalence: the transition systems have the same behavior, and make choice at same time.

The free product of transition systems

The synchronous product of transition systems

When processes interact, not all possible global actions are useful, since the interaction is subject to communication and synchronization constraints.

The transition system associated with the system of processes must therefore be a subsystem of the free product of the component transition systems.

The synchronous product allows only those global transitions corresponding to action vectors included in the synchronization constraint.

Modeling sequential circuits

Model logical dynamical system

Model a Mutual Exclusion Protocol

State Space

The state space of a program can be captured by the valuations of the variables and the program counters

Each state of the program is a valuation of all the variables

CTL*

Temporal logic is a formalism for describing sequences of transitions between states in a reactive system.

Properties like eventually or never are specified using special temporal operators.

CTL* formulas

CTL* formulas describe properties of computation trees.

The computation tree shows all of the possible executions starting from the initial state.

Path quantifiers

A ( for all computation path )

E ( for some computation path )

Temporal operators

X (next time) requires the property holds in the second state of the path

F (finally) the property will hold at some state on the path

G (globally) the property holds at every state on the path

U (until) if there is a state on the path where the second property holds, at every preceding state, the first one holds

R (release) the second property holds along the path up to and including the first state where the first property holds. However, the first property is not required to hold eventually

Two types of formulas in CTL*

state formulas ( which are true in a special state )

path formulas ( which are true along a special path )

Syntax of state formulas rules:

if p∈AP, then p is sf

if f and g are sf, ¬f, f∧g, f∨g are sf

if f is a pf, then Ef and Af are sf

Syntax of path formulas

if f is a sf, then f is also a pf

if f and g are pf, ¬f, f∧g, f∨g, X f, F f, G f, f U g and f R g are pf

CTL* is the set of state formulas generated by the above rules

Semantics of CTL*

if f is a sf, M,s⊨f means that f holds at state s in the M

if g is a pf, M,π⊨g means that g holds along path π in the M

Two sublogics of CTL*

Branching-time logic

The temporal operators quantify over the paths that are possible from a given state.

Temporal operators must be immediately preceded by a path quantifier.

if f and g are sf, Xf, Ff, Gf, fUg and fRg are pf

A(FGp)

Linear temporal logic

operators are provided for describing events along a single computation path.

LTL implicitly quantifies universally over paths.

If p∈AP, then p is pf, Af where f is a pf

AG(EFp)

Ten basic CTL operators:

AX and EX

AF and EF

AG and EG

AU and EU

AR and ER

Express Properties

Safety: something bad will not happen

Usually: AG

Liveness: something good will happen

Usually: AF

Fairness: something is successful/allocated infinitely often.

Usually: AGAF

CTL and LTL have incomparable expressive power.

The choice between LTL and CTL depends on application and personal preferences.

http://www.cs.utexas.edu/users/moore/acl2/seminar/2010.05-19-krug/slides.pdf

http://www.inf.unibz.it/~artale/FM/slide4.pdf