5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 33
Текст из файла (страница 33)
Queille andSifakis [348] consider fairness for transition systems. An overview of the fairness notionshas been provided by Kwiatkowska [252]. An extensive treatment of fairness can be found144Linear-Time Propertiesin the monograph by Francez [155]. A recent characterization of fairness in terms oftopology, language theory, and game theory has been provided by Völzer, Varacca, andKindler [415].3.8ExercisesExercise 3.1. Give the traces on the set of atomic propositions { a, b } of the following transitionsystem:{a}∅{a}{ a, b }Exercise 3.2.
On page 97, a transformation is described of a transition system TS with possibleterminal states into an “equivalent” transition system TS∗ without terminal states. Questions:(a) Give a formal definition of this transformation TS → TS∗(b) Prove that the transformation preserves trace-equivalence, i.e., show that if TS1 , TS2 aretransition systems (possibly with terminal states) such that Traces(TS1 ) = Traces(TS2 ),then Traces(TS∗1 ) = Traces(TS∗2 ).8Exercise 3.3.Give an algorithm (in pseudocode) for invariant checking such that in casethe invariant is refuted, a minimal counterexample, i.e., a counterexample of minimal length, isprovided as an error indication.Exercise 3.4. Recall the definition of AP-deterministic transition systems (Definition 2.5 onpage 24). Let TS and TS be transition systems with the same set of atomic propositions AP.Prove the following relationship between trace inclusion and finite trace inclusion:(a) For AP-deterministic TS and TS :Traces(TS) = Traces(TS ) if and only if Tracesfin (TS) = Tracesfin (TS ).8If TS is a transition system with terminal states, then Traces(TS) is defined as the set of all wordstrace(π) where π is an initial, maximal path fragment in TS.Exercises145(b) Give concrete examples of TS and TS where at least one of the transition systems is notAP-deterministic, butTraces(TS) ⊆ Traces(TS ) and Tracesfin (TS) = Tracesfin (TS ).Exercise 3.5.
Consider the set AP of atomic propositions defined by AP = { x = 0, x > 1 }and consider a nonterminating sequential computer program P that manipulates the variable x.Formulate the following informally stated properties as LT properties:(a) false(b) initially x is equal to zero(c) initially x differs from zero(d) initially x is equal to zero, but at some point x exceeds one(e) x exceeds one only finitely many times(f) x exceeds one infinitely often(g) the value of x alternates between zero and two(h) true(This exercise has been adopted from [355].) Determine which of the provided LT properties aresafety properties. Justify your answers.Exercise 3.6.
Consider the set AP = { A, B } of atomic propositions. Formulate the followingproperties as LT properties and characterize each of them as being either an invariance, safetyproperty, or liveness property, or none of these.(a) A should never occur,(b) A should occur exactly once,(c) A and B alternate infinitely often,(d) A should eventually be followed by B.(This exercise has been inspired by [312].)Exercise 3.7. Consider the following sequential hardware circuit:146Linear-Time PropertiesXORyxXORANDORANDORr1r2The circuit has input variable x, output variable y, and registers r1 and r2 with initial valuesr1 = 0 and r2 = 1.
The set AP of atomic propositions equals { x, r1 , r2 , y }. Besides, consider thefollowing informally formulated LT properties over AP:P1 : Whenever the input x is continuously high (i.e., x=1), then the output y is infinitely oftenhigh.P2 : Whenever currently r2 =0, then it will never be the case that after the next input, r1 =1.P3 : It is never the case that two successive outputs are high.P4 : The configuration with x=1 and r1 =0 never occurs.Questions:(a) Give for each of these properties an example of an infinite word that belongs to Pi .
Do theωsame for the property 2AP \ Pi , i.e., the complement of Pi .(b) Determine which properties are satisfied by the hardware circuit that is given above.(c) Determine which of the properties are safety properties. Indicate which properties are invariants.(i) For each safety property Pi , determine the (regular) language of bad prefixes.(ii) For each invariant, provide the propositional logic formula that specifies the propertythat should be fulfilled by each state.Exercise 3.8. Let LT properties P and P be equivalent, notation P ∼= P , if and only if∼pref(P ) = pref(P ).
Prove or disprove: P = P if and only if closure(P ) = closure(P ).Exercises147Exercise 3.9. Show that for any transition system TS, the set closure(Traces(TS)) is a safetyproperty such that TS |= closure(Traces(TS)).Exercise 3.10. Let P be an LT property. Prove: pref(closure(P )) = pref(P ).Exercise 3.11.claims:Let P and P be liveness properties over AP. Prove or disprove the following(a) P ∪ P is a liveness property,(b) P ∩ P is a liveness property.Answer the same question for P and P being safety properties.Exercise 3.12. Prove Lemma 3.38 on page 125.Exercise 3.13.AP = { a, b } and let P be the LT property of all infinite words σ =LetωA0 A1 A2 .
. . ∈ 2APsuch that there exists n 0 with a ∈ Ai for 0 i < n, { a, b } = An andb ∈ Aj for infinitely many j 0. Provide a decomposition P = Psaf e ∩ Plive into a safety and aliveness property.Exercise 3.14. Let TSSem and TSPet be the transition systems for the semaphore-based mutualexclusion algorithm (Example 2.24 on page 43) and Peterson’s algorithm (Example 2.25 on page45), respectively. Let AP = { waiti , criti | i = 1, 2 }. Prove or disprove:Traces(TSSem ) = Traces(TSP et ).If the property does not hold, provide an example trace of one transition system that is not a traceof the other one.Exercise 3.15.
Consider the transition system TS outlined on the right and the sets of actionsB1 = { α }, B2 = { α, β }, and B3 = { β }. Further, let Eb , Ea and E be the following LTproperties:148Linear-Time Propertiesω• Eb = the set of all words A0 A1 · · · ∈ 2{a,b} withAi ∈ {{a, b}, {b}} for infinitely many i(i.e., infinitely often b).ω• Ea = the set of all words A0 A1 · · · ∈ 2{a,b} withAi ∈ {{a, b}, {a}} for infinitely many i{a} s2(i.e., infinitely often a).ω• E = set of all words A0 A1 · · · ∈ 2{a,b} for whichthere does not exist an i ∈ N s.t. Ai = {a}, Ai+1 ={a, b} and Ai+2 = ∅.s1γ∅αγβs3 {b}αγs4α{a, b}Questions:(a) For which sets of actions Bi (i ∈ { 1, 2, 3 }) and LT properties E ∈ { Ea , Eb , E } it holdsthat TS |=Fi E? Here, Fi is a strong fairness condition with respect to Bi that does notimpose any unconditional or weak fairness conditions (i.e., Fi = (∅, { Bi }, ∅)).(b) Answer the same question in the case of weak fairness (instead of strong fairness, i.e., Fi =(∅, ∅, { Bi })).Exercise 3.16.
Let TSi (for i=1, 2) be the transition system (Si , Act, → i , Ii , APi , Li ) andF = (Fucond , Fstrong , Fweak ) be a fairness assumption with Fucond = ∅. Prove or disprove (i.e.,give a counterexample for) the following claims:(a) Traces(TS1 ) ⊆ Traces(TS1 TS2 ) where Syn ⊆ Act(b) Traces(TS1 ) ⊆ Traces(TS1 ||| TS2 )(c) Traces(TS1 TS2 ) ⊆ Traces(TS1 ) where Syn ⊆ Act(d) Traces(TS1 ) ⊆ Traces(TS2 ) ⇒ FairTracesF (TS1 ) ⊆ FairTracesF (TS2 )(e) For liveness property P with TS2 |=F P we haveTraces(TS1 ) ⊆ Traces(TS2 ) ⇒ TS1 |=F P.Assume that in items (a) through (c), we have AP2 = ∅ and that TS1 TS2 and TS1 ||| TS2 ,respectively, have AP = AP1 as atomic propositions and L(s, s ) = L1 (s) as labeling function.In items (d) and (e) you may assume that AP1 = AP2 .Exercise 3.17. Consider the following transition system TS with the set of atomic propositions{ a }:Exercises149{a}s1ααs2ββs3γβαs4βs5αs6Let the fairness assumptionF = (∅, {{α}, {β}} , {{β}}) .Determine whether TS |=F “eventually a”.
Justify your answer!Exercise 3.18. Consider the following transition system T S (without atomic propositions):s0αδαs1αββs2βδs3αs4Decide which of the following fairness assumptions Fi are realizable for TS. Justify your answers!(a) F1 = ({{α}} , {{δ}} , {{α, β}})(b) F2 = ({{δ, α}} , {{α, β}} , {{δ}})(c) F3 = ({{α, δ}, {β}} , {{α, β}} , {{δ}})Exercise 3.19. Let AP = { a, b }.ω(a) P1 denotes the LT property that consists of all infinite words σ = A0 A1 A2 . . . ∈ 2APsuch that there exists n 0 with∀j < n.
Aj = ∅∧An = {a}∧∀k > n. (Ak = { a } ⇒ Ak+1 = { b }) .(i) Give an ω–regular expression for P1 .(ii) Apply the decomposition theorem and give expressions for Psafe and Plive .150Linear-Time Properties(iii) Justify that Plive is a liveness and that Psafe is a safety property.ω(b) Let P2 denote the set of traces of the form σ = A0 A1 A2 . . .
∈ 2APsuch that∞∃ k. Ak = { a, b }∧∃n 0. ∀k > n. a ∈ Ak ⇒ b ∈ Ak+1 .Consider the following transition system TS:α{a}s0αs1 { b }γβ{ a, b } s2γδαs3∅ηs4 { a, b }αββConsider the following fairness assumptions: (a) F1 = {α} , {β}, {δ, γ}, {η} , ∅ . Decide whether TS |=F1 P2 . (b) F2 = {α} , {β}, {γ} , {η} . Decide whether T S |=F2 P2 .Justify your answers.Exercise 3.20. Let TS = (S, Act, →, I, AP, L) be a transition system without terminal statesand let A1 , .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
