Lecture 7: CTS A. PnueliReal Time:CTSLet T be a totally ordered monoid, to which we refer as the time domain. Themost frequently used timed domains areR+, the non-negative reals, and IN, thenaturals.Aclocked transition system (CTS) Φ = hV, Θ, ρ, Πi consists of:• V – A finite set of state variables. The set V = D ∪ C is partitioned intoD = {u1, . . . , un} the set of discrete variables and C = {t1, . . . , tk} the set ofclocks. Clocks always have the type T . The discrete variables can be of anytype. Optionally,C may include a special clock T ∈ C, called the master clock.• Θ – An initial condition. A satisfiable assertion characterizing the initial states.In caseT ∈ C, it is required that Θ → T = 0, i.e., T = 0 at all initial states.• ρ – A transition relation. An assertion ρ(V, V′), referring to both unprimed(current) and primed (next) versions of the state variables.In case T ∈ C, it is required that ρ → T′= T , i.e., the master clock is modifiedby no transition.• Π – The time-progress condition. An assertion over V . The assertion is usedto specify a global restriction over the progress of time.Timed and Hybrid Systems, NYU, Spring, 2007 112Lecture 7: CTS A. PnueliThe Extended Transition RelationLet Φ : hV, Θ, ρ, Πi be a CTS. We define the extended transition relation ρTassociated with Φ asρT= ρ ∨ ρtick,whereρtickis given by:ρtick: ∃∆. Ω(∆) ∧ D′= D ∧ C′= C + ∆,andΩ(∆) is given byΩ(∆): ∆ > 0 ∧ ∀t ∈ [0, ∆). Π(D, C + t)Let D = {u1, . . . , um} be the set of discrete variables of Φ and C = {c1, . . . , ck}be the set of its clocks. Then, the expression C′= C + ∆ is an abbreviation forc′1= c1+ ∆ ∧ · · · ∧ c′k= ck+ ∆,andΠ(D, C + t) is an abbreviation forΠ(u1, . . . , um, c1+ t, . . . , ck+ t)Timed and Hybrid Systems, NYU, Spring, 2007 113Lecture 7: CTS A. PnueliRuns and ComputationsLet Φ : hV, Θ, ρ, Πi be a CTS. A run of Φ is a finite or infinite sequence of statesσ : s0, s1, . . . satisfying:• Initiality: s0|= Θ• Consecution: For each j ∈ [0, |σ|) sj+1is a ρT-successor of sj.A state is called(Φ-)accessible if it appears in a run of Φ.Acomputation of Φ is an infinite run satisfying:• Time Divergence: The sequence s0[T ], s1[T ], . . . grows beyond any bound.That is, asi increases, the value of T at siincreases beyond any bound.ACTS Φ is called non-zeno if every finite run of Φ can be extended into acomputation.Timed and Hybrid Systems, NYU, Spring, 2007 114Lecture 7: CTS A. PnueliA Frequently Occurring CaseIn many cases, the time-progress condition Π has the following special formΠ:^i∈I(pi→ ti< Ei),whereI is some finite index set and, for each i ∈ I, the assertion piand the T -valued expressionEido not depend on the clocks, and ti∈ C is some clock. Thisis, for example, the form of the time-progress condition for anyCTS representing areal-time program. For such cases, the time-increment limiting formulaΩ(∆) canbe significantly simplified and assumes the following form:Ω(∆): ∆ > 0 ∧^i∈I(pi→ ti+ ∆ ≤ Ei)Note, in particular, that this simpler form does not use quantifications over t.Timed and Hybrid Systems, NYU, Spring, 2007 115Lecture 7: CTS A. PnueliExamplesSystem Φ1can be presented by the following diagram:ℓ1ℓ0: t < 2y := y + 1Textually, this can be presented as:V : {π : {0, 1}, y, t, T }Θ : π = y = t = T = 0ρ : π = 0 ∧ pres(t, T ) ∧π′= 0 ∧ y′= y + 1∨ π′= 1 ∧ y′= yΠ : π = 0 → t < 2The tick transition is given byρtick: ∃ ∆ > 0(t′, T′) = (t + ∆, T + ∆) ∧pres(π, y)∧ (π = 0 → t + ∆ ≤ 2)Timed and Hybrid Systems, NYU, Spring, 2007 116Lecture 7: CTS A. PnueliA possible computation is:hπ: 0 , y: 0 , t: 0 , T : 0itick (1)−→ hπ: 0 , y: 0 , t: 1 , T : 1iℓ00−→hπ: 0 , y: 1 , t: 1 , T : 1iℓ00−→ hπ: 0 , y: 2 , t: 1 , T : 1itick (1)−→hπ: 0 , y: 2 , t: 2 , T : 2iℓ00−→ hπ: 0 , y: 3 , t: 2 , T : 2iℓ00−→hπ: 0 , y: 4 , t: 2 , T : 2iℓ01−→ hπ: 1 , y: 4 , t: 2 , T : 2itick (1)−→hπ: 1 , y: 4 , t: 3 , T : 3itick (1)−→ hπ: 1 , y: 4 , t: 4 , T : 4itick (1)−→· · ·Timed and Hybrid Systems, NYU, Spring, 2007 117Lecture 7: CTS A. PnueliSystemΦ2System Φ2can be presented by the following diagram:ℓ1ℓ0: t <110y+1(y, t) := (y + 1, 0)Textually, this can be presented as:V : {π : {0, 1}, y, t, T }Θ : π = y = t = T = 0ρ : π = 0 ∧ T′= T ∧π′= 0 ∧ (y′, t′) = (y + 1, 0)∨ π′= 1 ∧ (y′, t′) = (y, t)Π : π = 0 → t <110y+1The tick transition is given byρtick: ∃ ∆ > 0(t′, T′) = (t + ∆, T + ∆) ∧pres(π, y)∧ (π = 0 → t + ∆ ≤110y+1)Timed and Hybrid Systems, NYU, Spring, 2007 118Lecture 7: CTS A. PnueliA possible computation is:hπ: 0 , y: 0 , t: 0 , T : 0itick (.1)−→ hπ: 0 , y: 0 , t: .1 , T : .1iℓ00−→hπ: 0 , y: 1 , t: 0 , T : .1iℓ00−→ hπ: 0 , y: 2 , t: 0 , T : .1itick (.01)−→hπ: 0 , y: 2 , t: .01 , T : .11iℓ00−→ hπ: 0 , y: 3 , t: 0 , T : .11iℓ00−→hπ: 0 , y: 4 , t: 0 , T : .11iℓ01−→ hπ: 1 , y: 4 , t: 0 , T : .11itick (1)−→hπ: 1 , y: 4 , t: 1 , T : 1.11itick (1)−→ hπ: 1 , y: 4 , t: 2 , T : 2.11itick (1)−→· · ·Timed and Hybrid Systems, NYU, Spring, 2007 119Lecture 7: CTS A. PnueliSystemΦ3System Φ3below is not a non-zeno system.ℓ1ℓ0: t <110y+1y ≤ 5(y, t) := (y + 1, 0)Following is a finite run which cannot be extended to a computation:hπ: 0 , y: 0 , t: 0 , T : 0iℓ00−→hπ: 0 , y: 1 , t: 0 , T : 0iℓ00−→hπ: 0 , y: 2 , t: 0 , T : 0iℓ00−→hπ: 0 , y: 3 , t: 0 , T : 0iℓ00−→hπ: 0 , y: 4 , t: 0 , T : 0iℓ00−→hπ: 0 , y: 5 , t: 0 , T : 0iℓ00−→hπ: 0 , y: 6 , t: 0 , T : 0itick (10−7)−→hπ: 0 , y: 6 , t: 10−7, T : 10−7iℓ00−→hπ: 0 , y: 7 , t: 0 , T : 10−7itick (10−8)−→hπ: 0 , y: 6 , t: 10−8, T : 1.1 · 10−7iℓ00−→Timed …
View Full Document
Unlocking...