Lecture 4: Feasibility and Response A. PnueliChecking for FeasibilityBefore we discuss model checking response properties we discuss the problemof checking whether a given FDS is feasible.A run of an FDS is an infinite sequence of states which satisfies the requirementsof initiality and consecution but not necessarily any of the fairness requirements.A state s of an FDS D is called reachable if it participates in some run of D.A state s is called feasible if it participates in some computation. The FDS is calledfeasible if it has at least one computation.A set of states S is defined to be an F-set if it satisfies the followingrequirements:F1. All states in S are reachable.F2. Each state s ∈ S has a ρ-successor in S.F3. For every state s ∈ S and every justice requirement J ∈ J , there exists anS-path leading from s to some J-state.F4. For every state s ∈ S and every compassion requirement (p, q) ∈ C, eitherthere exists an S-path leading from s to some q-state, or s satisfies ¬p.Analysis of Reactive Systems, NYU, Spring, 2006 66Lecture 4: Feasibility and Response A. PnueliF-Sets Imply FeasibilityClaim 5. [F-sets]A reachable state s is feasible iff it has a path leading to some F-set.Proof:Assume that s is a feasible state. Then it participates in some computation σ. LetS be the (finite) set of all states that appear infinitely many times in σ. We willshow that S is an F-set. It is not difficult to see that there exists a cutoff positiont ≥ 0 such that S contains all the states that appear at positions beyond t.Obviously all states appearing in σ are reachable. If s ∈ S appears in σ atposition i > t then it has a successor si+1∈ σ which is also a member of S.Let s = si∈ σ, i > t be a member of S and J ∈ J be some justice requirement.Since σ is a computation it contains infinitely many J-positions. Let k ≥ i oneof the J-positions appearing later than i. Then the path si, . . . , skis an S-pathleading from s to a J-state.Let s = si∈ σ, i > t be a member of S and (p, q) ∈ C be some compassionrequirement. There are two possibilities by which σ may satisfy (p, q). Either σcontains only finitely many p-positions, or σ contains infinitely many q positions.It follows that either S contains no p-states, or it contains some q-states whichappear infinitely many times in σ. In the first case, s satisfies ¬p. In the secondcase, there exists a path leading from sito sk, a q-state such that k ≥ i.Analysis of Reactive Systems, NYU, Spring, 2006 67Lecture 4: Feasibility and Response A. PnueliProof ContinuedIn the other direction, assume the existence of an F-set S and a reachable states which has a path leading to some state s1∈ S. We will show that there exists acomputation σ which contains s.Since s is reachable and has a path leading to state s1∈ S, there exists a finitesequence of states π leading from an initial state to s1and passing through s. Wewill show how π can be extended to a computation by an infinite repetition of thefollowing steps. At any point in the construction, we denote by end(π) the statewhich currently appears last in π.• We know that end(π) ∈ S has a successor s ∈ S. Append s to the end of π.• Consider in turn each of the justice requirements J ∈ J . We append to π theS-path πJconnecting end(π) to a J-state.• Consider in turn each of the compassion requirements (p, q) ∈ C. If thereexists an S-path πq, connecting end(π) to a q-state, we append πqto the end of π.Otherwise, we do not modify π. We observe that if there does not exist an S-pathleading from end(π) to a q-state, then end(π) and all of its progeny within S mustsatisfy ¬p.It is not difficult to see that the infinite sequence constructed in this way is acomputation.Analysis of Reactive Systems, NYU, Spring, 2006 68Lecture 4: Feasibility and Response A. PnueliComputing F-SetsAssume an assertionϕwhich characterizes an F-set. Translating therequirements 1–4 into formulas, we obtain the following requirements:ϕ→ reachableDϕ→ ρϕEveryϕ-state has aϕ-successorϕ→ (ϕ∧ ρ)∗(ϕ∧ J) For every J ∈ Jϕ→ ¬p ∨ (ϕ∧ ρ)∗(ϕ∧ q) For every (p, q) ∈ CThis can be summarized asϕ→reachableD∧ ρϕ∧^J∈J(ϕ∧ ρ)∗(ϕ∧ J) ∧^(p,q)∈C¬p ∨ (ϕ∧ ρ)∗(ϕ∧ q)Since we are interested in a maximal F-set, the computation can be expressedas:νϕ.reachableD∧ ρϕ∧^J∈J(ϕ∧ ρ)∗(ϕ∧ J) ∧^(p,q)∈C¬p ∨ (ϕ∧ ρ)∗(ϕ∧ q)Analysis of Reactive Systems, NYU, Spring, 2006 69Lecture 4: Feasibility and Response A. PnueliAlgorithmic InterpretationComputing the maximal fix-point as a sequence of iterations, we can describe thecomputational process as follows:Start by lettingϕ:= reachableD. Then repeat the following steps:• Remove fromϕall states which do not have aϕ-successor.• For each J ∈ J , remove fromϕall states which do not have aϕ-path leadingto a J-state.• For each (p, q) ∈ C, remove fromϕall p-states which do not have aϕ-pathleading to a q-state.until no further change.To check whether an FDS D is feasible, we compute for it the maximal F-set andcheck whether it is empty. D is feasible iff the maximal F-set is not-empty.Analysis of Reactive Systems, NYU, Spring, 2006 70Lecture 4: Feasibility and Response A. PnueliExampleAs an example, consider the following FDS:x : 0 x : 1 x : 2x : 5x : 4x : 3with the fairness requirements:J1: x 6= 1C1: (x = 3, x = 5)C2: (x = 2, x = 1)We setϕ0: {0..5} and then proceed as follows:• Removing fromϕ0all (x = 2)-states which do not have aϕ0-path leading to an(x = 1)-state, we are left withϕ1: {0, 1, 3, 4, 5}.• Successively removing fromϕ1all states without successors, leavesϕ2: {3, 4}.• Removing fromϕ2all (x = 3)-states which do not have aϕ2-path leading to a(x = 5)-state, we are left withϕ3: {4}.• No reasons to remove any further states fromϕ3: {4}, so this is our final set.We conclude that the above FDS is feasible.Analysis of Reactive Systems, NYU, Spring, 2006 71Lecture 4: Feasibility and Response A. PnueliVerifying Response Properties Through Feasibility CheckingLet D : hV, Θ, ρ, J , Ci be an FDS and p ⇒ q be a response property we wishto verify over D. Let reachableDbe the assertion characterizing all the reachablestates in D.We define an auxiliary FDS Dp,q: hV, Θp,q, ρp,q, J , Ci, whereΘp,q: reachableD∧ p ∧ ¬qρp,q: ρ