Transcript slides

Model Checking
Rajeev Alur
Requirements
 Requirement: Desirable property of the executions of the system
 Informal: Either implicit, or stated in English in documents
 Formal: Stated explicitly in a mathematically precise manner
 High assurance / safety-critical systems: Formal requirements
 Model/design/system meets the requirements if every execution
satisfies all the requirements
 Clear separation between requirements (what needs to be
implemented) and system (how it is implemented)
 Verification problem: Given a requirement j and a system/model C,
prove/disprove that the system C satisfies the requirement j
Safety Requirements
 A safety requirement states that a system always stays within
“good’ states (i.e. a nothing bad ever happens)
 Leader election: it is never the case that two nodes consider them to
be leaders
 Collision avoidance: Distance between two cars is always greater
than some minimum threshold
 Different class of requirements: Liveness
 System eventually attains its goal
 Leader election: Each node eventually makes a decision
 Cruise controller: Actual speed eventually equals desired speed
 Formalization and analysis techniques for safety and liveness differ
significantly, so let us first focus on safety
Transition Systems
States + Initial states + Transitions between states
Definition of Transition System
 Syntax: a transition system T has
1. a set S of (typed) state variables
2. Initialization Init for state variables
3. Transition description Trans given by code to update state vars
 Semantics:
1. Set QS of states
2. Set [Init] of initial states (this is a subset of QS)
3. Set [Trans] of transitions, subset of QS x QS
 Circuits, distributed algorithms, programs, and more generally
systems, all have an underlying transition system
Example Transition System
(press=0 & x<10)
 x:=x+1
(press=0) ?
int x:=0
(press=1) ?
off
on
State variables:
{off, on} mode, int x
(press=1 | x>=10)
 x:=0
(off,0)
(on, 56)
(on, 2)
(on, 0)
(on, 3)
(off, 17)
Initialization:
mode = off; x = 0
Transitions:
(off,n) -> (off,n);
(off,n) -> (on,n);
(on,n) -> (on,n+1) if n<10;
(on,n) -> (off,0)
(on, 17)
Values for input var Press chosen nondeterministically
Euclid’s GCD Algorithm
Classical program to compute greatest common divisor of (non-negative)
input numbers m and n
(x>0 & y>0) 
if (x>y) then x:=x-y else y:=y-x
nat x:=m; y:=n
loop
stop
~ (x>0 & y>0) 
if (x=0) then x:=y
Reachable States
(press=0 & x<10)
 x:=x+1
(press=0) ?
int x:=0
(press=1) ?
off
on
(press=1 | x>=10)
 x:=0
(on, 56)
(off,0)
(on, 0)
(on, 1)
(off, 17)
(on, 17)
(on, 10)
Reachable States of Transition Systems
A state s of a transition system is reachable if there is an execution
starting in an initial state and ending in the state s
Invariants
(on, 56)
(off,0)
(on, 0)
(on, 1)
(off, 17)
(on, 10)
(off, 10)
(on, 17)
 Property of a transition system: Boolean-valued expression j over state variables
 Property j is an invariant of T if every reachable state satisfies j
 Examples of invariants: (x <= 10); ( x <= 50); ( mode= off -> x=0 )
 Examples of properties that are not invariants: (x < 10); (mode=off)
Invariants
 Express desired safety requirement as property j of state variables
 If j is an invariant then the system is safe
 If j is not an invariant, then some state satisfying ~j is reachable
(execution leading to such a state is counterexample)
 Euclid’s GCD Program:
(mode=stop -> x = gcd(m,n))
Formal Verification
Model/Program
Requirement
Verifier
Grand challenge:
Automate verification as much as possible !
yes/proof
no/bug
Analysis Techniques
 Dynamic Analysis (runtime)
 Execute the system, possibly multiple times with different inputs
 Check if every execution meets the desired requirement
 Static Analysis (design time)
 Analyze the source code or the model for possible bugs
 Trade-offs
 Dynamic analysis is incomplete, but accurate (checks real system,
and bugs discovered are real bugs
 Static analysis can catch design bugs early !
 Many static analysis techniques are not scalable (solution: analyze
approximate versions, can lead to false warnings)
Invariant Verification
 Simulation
 Simulate the model, possibly multiple times with different inputs
 Easy to implement, scalable, but no correctness guarantees
 Proof based
 Construct a proof that system satisfies the invariant
 Requires manual effort (partial automation possible)
 State-space analysis (Model checking)
 Algorithm explores “all” reachable states to check invariants
 Not scalable, but current tools can analyze many real-world
designs (relies on many interesting theoretical advances)
Inductive Invariant
 A property j is an inductive invariant of transition system T if
1. Every initial state of T satisfies j
2. If a state satisfies j and (s,t) is a transition of T, then t must
satisfy j
 If j is an inductive invariant, then all reachable states of T must
satisfy j, and thus, it is an invariant
Proof Rule for Proving Invariants
 To establish that a property j is an invariant of transition system T
 Find another property y such that
1. y implies j (that is, a state satisfying y must satisfy j)
2. y is an inductive invariant
 Show that every initial state satisfies y
 Assume that a state s satisfies y. Consider a state t such that
(s,t) is a transition. Show that t must satisfy y
 This is a sound and complete strategy for establishing invariants
1. Sound means this is a correct proof technique
2. Complete: If j is an invariant, then there must exist some
inductive strengthening y satisfying above conditions
Inductive Invariants
Initial
States
Property j
Reachable
States
Strengthening y
Correctness of GCD
(x>0 & y>0) 
if (x>y) then x:=x-y else y:=y-x
nat x:=m; y:=n
loop
stop
~ (x>0 & y>0) 
if (x=0) then x:=y
 Property j : gcd(x,y) = gcd (m,n)
 Verify that this property is indeed an inductive invariant!
 Captures the core logic of the program: Even though x and y are
updated at every step, their gcd stays unchanged
 When switching to “stop”, if x is 0, then gcd(0,y) is y; if y=0, then
gcd(x,0)=x, and thus x=gcd(m,n) upon switching to stop
 Note that (mode=stop -> y=gcd(m,n)) is invariant, but not inductive
Back To Invariant Verification Problem
Transition System T
Property j
Verifier
Is j an invariant of T?
yes
no/bug
Theorem: Invariant verification problem is undecidable.
If some state variables in T are of type int, then T can correspond
to an arbitrary program (or Turing machine).
Intuition: there is no a priori bound on number of reachable states in
such case, so examining all reachable states is not possible
Finite-State Invariant Verification Problem
Finite-state
Transition System T
Property j
Verifier
Is j an invariant of T?
yes
no/bug
Theorem: Invariant verification problem for finite-state systems is
decidable.
If T has k Boolean variables, then total number of states is 2k.
Verifier can systematically search through all possible states.
Complexity is exponential, more precisely, PSPACE (a class of
problems a bit harder than NP-complete problems such as SAT).
Solving Invariant Verification
 Establishing that the system is safe is important, but there is no
efficient algorithm to solve the verification problem!!
 Solution 1: Use Simulation-based analysis
 Simulate the model multiple times, and check that each state
encountered on each execution satisfies desired safety property
 Useful, practical in real-world, but gives only partial guarantee (and
is known to miss hard-to-find bugs)
 Solution 2: Write a formal proof using inductive invariants
 Only partial tool support possible, so requires considerable effort
 Recent successes: verified microprocessor, web browser, JVM
 Solution 3: Exhaustive search through state-space
 Fully automated, but has scalability limitations (may not work!)
 Complementary to simulation, increasingly used in industry
 Two approaches: On-the-fly enumerative search, Symbolic search
Computing Reachable States
 Search algorithm can start with initial states, and explore
transitions out of initial states, in a systematic manner
 Example: state vars are integers x, y; initially we know that 0<=x<=2
and 1<y<=2, and a single transition increments x and decrements y
y
y
x
Enumerative:
Consider individual states
x
Symbolic:
Consider set of states
Towards Symbolic Search Algorithm
 We need a way to represent and manipulate sets of states
 Basic data structure: region
 For now, a region is given by a Boolean-valued expression/formula
 Example 1: (x & y ) | z, where x,y,z are boolean vars
 Example 2: (x <= y+1) & (0 <= x <= 3), where x,y are int/real vars
 What operations are needed on regions?
 Will become apparent as we develop the algorithm
 Is there a “better” implementation of regions other than formulas?
 Yes! Ordered Binary Decision Diagrams (OBDDs) for boolean vars
 Polyhedra (matrices) for real-valued vars
Symbolic Representation of Transition Systems
 Consider a transition system T with variables S
 How to represent the set of initial states?
 By a formula jI over variables S
 Easy to obtain this from the initialization description Init
 For example, for the GCD program, jI is (x=m) &(y=n) &(mode=loop)
 How to represent the set of transitions?
 Convention: Primed variable denotes updated value (that is, value in
the target state of a transition)
 Transitions are given by a formula over jT variables S U S’
 Example: In one transition, increment x and decrement y:
 (x’ = x+1) & (y’ = y-1)
 A pair of states (s,t) over x,y satisfies this formula exactly when
t(x)=s(x)+1 and t(y)=s(y)-1
 Benefit: Uniformity. If T has k variables, then a set of states given by
a region over k vars, and transitions given by a region over 2k vars
Transition Formula for GCD
 Suppose a single step is given by:
if (x>0 & y>0) then if (x>y) then x:=x-y else y:=y-x
 We want to get a formula jT over variables x, y, x’, y’ to capture this
 Assignment x := x-y corresponds to constraint x’ = x-y
 But this is not enough. In code, if y is not assigned explicitly, it stays
unchanged. In formulas, we must say y’=y to enforce this
 Assignment x := x-y corresponds to formula (x’=x-y & y’=y)
 Assignment y:=y-x corresponds to formula (x’=x & y’=y-x)
 Conditional statement if (x>y) then x:=x-y else y:=y-x becomes
f: [(x>y) & (x’=x-y) & (y’=y)] | [ ~(x>y) & (x’=x) & (y’=y-x)]
 Desired transition formula jT for the entire statement is
[(x>0 & y>0) & f] | [~(x>0 & y>0) & (x’=x) & (y’=y)]
Recap: Symbolic Transition Systems
 Region over variables X is a data structure that represents a set of
states assigning values to X
 Transition system T with state variables S represented by
 Region jI over S for initial states
 Region jT over S U S’ for transitions
 Symbolic representation can be compiled automatically from code for
updating variables
Image Computation
 Given a region A, define Post(A) to be set of successors of states in A
Post(A) = { t | there exists a state s in A and a transition (s,t)}
 Core problem in symbolic search: Given A and the transition formula,
how to compute Post (A)?
 If we can implement this, the set of all reachable states can be
computed iteratively by breadth-first search
reach0 = Initial states and
each reachi+1 obtained from
reachi by applying Post
Image Computation: Example 1
Suppose T has a single variable x of type real
Consider transition formula jT : (x’ = 2x+1)
How to compute Post(A) systematically, where A given by 0<=x<=10
Step 1: Conjoin (i.e. intersect) A with jT
 Result: (0 <= x <= 10) & (x’=2x+1)
 Intuition: this represents all transitions (x,x’) starting in region A
 Step 2: Existentially quantify x
 Result: Exists x. (0 <= x <= 10) & (x’=2x+1)
 Result simplifies to (0 <= (x’-1)/2 <= 10), which is same as (1<=x’<=21)
 Intuition: Result is a formula involving only x’, for which there exist
some x such that x is in A and (x,x’) is a transition
 Step 3: We want Post(A) to be a formula involving x, so rename x’ to x
 Result: 1 <= x <= 21
 Check [1,21] is exactly the image of [0,10] if x goes to 2x+1




Image Computation: Example 2
 Suppose T has variables x and y of type real
 Consider transition formula jT : (x’ = x+1 & y’=x)
 Suppose A is given by 0<=x<=4 & y <=7
 Step 1: Conjoin (i.e. intersect) A with jT
 Result: (0<=x<=4) & (y<=7) & (x’=x+1) & (y’=x)
 Step 2: Existentially quantify x and y
 Let’s first project out x; we get: (0<=y’<=4) & (y<=7) & (x’=y’+1)
 Now project out y; we get: (0<=y’<=4) & (x’=y’+1)
 Step 3: Rename x’ to x and y’ to y
 Result: (0<=y<=4) & (x=y+1)
Operations on Regions
 In general, we want to represent sets of states by a data type reg,
which should support following operations
 Disj(A,B): Returns region that contains states either in A or in B
 For formulas, this is just “A | B”
 Conj(A,B): Returns region containing states that are in both A and B
 For formulas, this is just “A & B”
 Diff(A,B): Returns region containing states in A but not in B
 For formulas, this is “A & ~B”
 IsEmpty(A): Returns 0 if region A contains some state, and 1 otherwise
 For formulas, this requires testing “satisfiability”: can the
variables in the formulas assigned values to make formula true
 Exists(A,X): Returns projection of A by quantifying variables in X
 For formulas, this requires “quantifier elimination”
 Rename(A,X,Y): Rename variables in X to corresponding vars in Y
 For formulas, this is textual substitution
Symbolic Image Computation
 Given:
 A of type reg over state variables S
 Trans of type reg over S U S’
 Post(A, Trans) = Rename(Exists(Conj(A,Trans),S), S’, S)
1. Take conjunction of A and Trans
2. Project out the variables in S using existential quantification
3. Rename primed variables to get a region over S
Symbolic Breadth-First-Search Algorithm
reach0 = Initial states and
each reachi+1 obtained from
reachi by applying Post




Algorithm for checking if a property j is an invariant of T?
Same as checking if the “error” states ~j is reachable?
We need to check at every step if error states reached; if so, stop.
If no new states are encountered, then also stop (invariant satisfied)
Symbolic BFS Algorithm
Given region Init over S, region Trans over S U S’, and region j over S, if j
is reachable in T then return 1, else return 0
reg Reach := Init; /* States found reachable */
reg New := Init; /* States not yet explored for outgoing transitions */
while IsEmpty(New) = 0 { /* while there are states to be explored */
if IsEmpty(Conj(New,j)) =0 /* Property j found reachable */
then return 1 (and stop);
New := Diff(Post(New,Trans),Reach);
/*These are states in post-image of New, but not
previously found reachable, so to be explored */
Reach := Disj(Reach, New); /* Update Reach by newly found states*/
};
return 0; /* All states explored without encountering j */
Frontier Computation in Symbolic BFS
Reach
New Post(New)
New
Reach
Symbolic Search
 Correctness: When the algorithm stops, its answer (whether the
property j is reachable or not) is correct
 Termination: Number of iterations depends on
 length of shortest execution leading to a state satisfying j
 Diameter: smallest d such that all states reachable within d steps
(this may not be bounded, if system is not finite-state)
 In practice, terminates if one of these numbers is small
 Used in practice for hardware verification, protocol verification
 Industrial-strength symbolic model checker: Cadence
 Open-source widely used academic tool: NuSMV
Implementation of Regions
 Key to efficient implementation: How to represent regions?
 Operations: Disj, Conj, Diff, IsEmpty, Exists, Rename
 Suppose all variables are Booleans
 Can we represent regions with formulas (with &, |, ~)
 Disj, Conj, Diff, Rename easy
 Exists (j,x) same as j [x->0] | j [x->1]
 IsEmpty(j) requires test for satisfiability (SAT)
 SAT is computationally demanding (NP-complete), but more
importantly, size of formula representing Reach keeps growing as we
apply operations such as Conj, Disj, Exists…
 Key to performance: Simplify formulas as much as possible
 Solution: Data structure of ROBDDs
Ordered Binary Decision Diagram
x
1
0
y
y
1
0
z
0
0
1
1
0
0
z
z
z
1
1
0
0
1
1 0
0
0
1
Formula: ( x | ~ y) & (y | z)
1
1
Reduced Ordered Binary Decision Diagram
Formula: ( x | ~ y) & (y | z)
x
1
0
y
y
1
0
z
0
0
1
1
0
0
z
z
z
1
1
0
0
1
1 0
0
0
1
1
1
Reduce size:
Rule 1: Merge isomorphic vertices
Rule 2: Eliminate a node if left child = Right child
Reduced Ordered Binary Decision Diagram
Formula: ( x | ~ y) & (y | z)
Rule 1: Merge isomorphic vertices
Rule 2: Eliminate a node if
left child = Right child
x
1
0
y
y
1
0
z
0
1
z
Can be merged by Rule 1
0
0 1
0
1
0
1
1
z
z
0
1
Can be eliminated by Rule 2
Reduced Ordered Binary Decision Diagram
Formula: ( x | ~ y) & (y | z)
x
1
0
~y | z
y
0
0
z
z
Rule 1: Merge isomorphic vertices
Rule 2: Eliminate a node if
left child = Right child
y
y|z
1
1
1
0
0
1
No more reduction possible!
ROBDD Properties
 Key restriction: Variables appear in same order on each path
 Not every variable needs to appear on every path
 The order in which reductions are applied does not matter
 Final result depends only on the function being represented
 Once we fix variable ordering, corresponding ROBDD is canonical
 Minimal: Smallest possible decision graph given the ordering restriction
 No other reductions possible
 One does not have to first build the complete tree, and then reduce
Example Constructing ROBDD
Formula: ( x & y) | (x’ & y’)
Ordering: x < y < x’ < y’
x
1
0
(x’ & y’)
0
x’
y
1
0
y’
0
0
y’
1
1
1
y | (x’ & y’)
ROBDD Definition
Given a set X of Boolean vars ordered by <, ROBDD B consists of
 Finite set U of vertices partitioned into internal and terminal
 Labeling function: for internal vertex u, label(u) is a variable in X and
for terminal vertex u, label(u) is a constant 0/1
 Left-child function for internal vertices such that either left(u) is
terminal, or label(u) < label(left(u))
 Right-child function for internal vertices such that either right(u) is
terminal, or label(u) < label(right(u))
 Meets the reduction rules:
1. If u and v are distinct terminal vertices then label(u) != label(v)
2. If u and v are distinct internal vertices then either label(u) !=
label(v) or left(u) != left(v) or right(u) != right(v)
3. If u is internal vertex, then left(u) != right(u)
 Semantics of a vertex: Boolean function associated with it
Example: Ordering Affects Size
Formula: ( x <-> y) & (x’ <-> y’)
Ordering: x < y < x’ < y’
Ordering: x < x’ < y < y’
ROBDD Properties
 For every Boolean function/formula f over variables V, given an
ordering <, there exists a unique ROBDD for f over (V,<)
 To test if two formulas/circuits f and g are equivalent, we can build
ROBDDs for f and g, check if they are the same
 Satisfiability/emptiness test: Given an ROBDD B, is the corresponding
function satisfiable?
 B is satisfiable if it does not equal terminal vertex 0
 Validity test: Given an ROBDD B, is the corresponding function valid
(that is, always 1 no matter what the values of variables are)
 B is valid if it equals terminal vertex 1
 How to reconcile this with the computational difficulty of checking
satisfiability/validity of formulas/circuits?
 ROBDD corresponding to a formula can be exponentially large!
 For some functions, no matter what ordering we choose, the
ROBDD is guaranteed to be large! (Hope: this is not a common case)
ROBDD Implementation
 Efficient data structures and implementations known
 Algorithms for operations such as Conj, Disj, Diff
 Given ROBDDs B1 and B2, construct ROBDD representing the AND
of corresponding functions directly
 Given a formula/circuit/program-text construct ROBDD representing
the corresponding transition relation
 How to choose a “good” variable ordering?
Formal Verification
Model/Program
Requirement
Verifier
How to formalize requirements?
1. Safety requirements: Invariants, monitors
2. Liveness requirements: Temporal logic
yes/proof
no/bug
Liveness Requirements
 Something good eventually happens
 A waiting train is eventually allowed to enter the bridge
 Each process eventually decides to be a leader/follower
 No finite execution demonstrates violation of such properties
 Counterexample should show a cycle in which the system may get
stuck without achieving the goal
 Formalization:
 Need to consider infinite executions (also called w-executions)
 Need a logic to state properties of infinite executions
Temporal Logic
 Logics proposed to reason about time
 Origins in philosophy
 Tense logic: Prior (1920)
 Linear temporal logic (LTL) proposed for reasoning about executions of
reactive systems
 Pnueli (1977), later selected for Turing award (1996)
 Industrial adoption
 Property Specification Language (PSL) IEEE standard
 LTL enriched with many additional constructs for usability
 Supported by CAD tools for simulation/analysis of Verilog/VHDL
Valuations and Base Formulas
 V: set of typed variables
 Example: nat x, bool y
 Valuation: Type-consistent assignment of values to variables in V
 q0 : (x=6, y=0)
 q1 : (x=11, y=1)
 Base formula: Boolean-valued expression over V
 even(x)
 y=0  even(x)
 Valuation q satisfies formula j, written q |= j, if q(j) evaluates to 1
 q0 |= even(x)
 q0 |= y=0  even(x)
 q1 does not satisfy even(x)
 q1 |= y=0  even(x)
Traces
 Base formula states a property of a single valuation
 Trace: Infinite sequence of valuations
 r : (0,0), (1,1), (2,0), (3,1), (4,0), (5,1)…
 r’ : (0,0), (21,1), (13,1), (43,0) …
 In context of system specification and verification:
 V can be set of state variables, and then a trace corresponds to a
possible infinite execution of the system
 V can be set of input and output variables, and then a trace
corresponds to an observed input/output behavior of system
 V can include all of state, input, and output variables
LTL Basics
 Base formula states a property of a single valuation
 Trace: Infinite sequence of valuations
 LTL formula is evaluated with respect to a trace
 LTL formulas are built from base formulas using
 Logical connectives (&, |, , ~)
 Temporal operators
 A trace r = q1, q2, q3, … satisfies a base formula j if q1 |= j
Always Operator
 Always j means j holds at all times
 Trace r = q1, q2, q3, … satisfies Always j if for all j, qj |= j
 Example trace
x: 0
y: 0
1
1
2
0
3
1
4
0
5 …
1 …
 Does not satisfy Always [ even(x)]
 Satisfies Always [ y=0  even(x) ]
 State property j is an invariant of a transition system T iff every
infinite execution of T satisfies Always j
Eventually Operator
 Eventually j means j holds at some position (at least once)
 Trace r = q1, q2, q3, … satisfies Eventually j if for some j, qj |= j
 Example trace
x: 0
y: 0
1
1
2
0
3
1
4
0
5 …
1 …
 Satisfies Eventually [ y = 1 ]
 Satisfies Eventually [ x = 45 ]
 Does not satisfy Eventually [ x=10 & y=1 ]
 Logical dual of Always: A trace satisfies Eventually j if and only if it
does not satisfy Always ~j
Next Operator
 Next j means j holds at “next” time
 Trace r = q1, q2, q3, … satisfies Next j if q2 |= j
 Example trace
x: 0
y: 0
1
1
2
0
3
1
4
0
5…
1…
 Satisfies Next [ y = 1 ]
 Does not satisfy Next [ x=2 ]
Until Operator
 j Until y means y holds at some position and j holds at all positions
till then
 Trace r = q1, q2, q3, … satisfies j U y if for some j, qj |= y and for all
i < j, qi |= j
 Example trace:
x: 0
0
0
2
2
5 …
 Satisfies (x=0) U (x=2)
 Satisfies (x<5) U (x=5)
 If a trace satisfies j U y then it must also satisfy Eventually y
Nested Operators
 What does Next Always j mean?
 Trace r = q1, q2, q3, … satisfies Next Always j if for all j>=2, qj |= j
 To formalize this, we have to define the relation (r, j) |= j
 Trace r satisfies formula j at position j
 Same as suffix trace qj, qj+1, qj+2, … starting at position j satisfies j
 Trace r satisfies j is same as (r, 1) |= j
 (r, j) |= Always j if (r, k) |= j for every position k >=j
 (r, j) |= Next j if (r, j+1) |= j
 (r, j) |= Eventually j if (r, k) |= j for some position k>= j
 (r, j) |= j U y if there exists position k>=j such that (r, k)|= y and for
all positions i such that j<=i<k, (r, i)|= j
Multiple Eventualities
 Example: Multi-agent system where multiple goals have to be satisfied
 Goal1: Robot 1 has finished its mission
 Goal2: Robot 2 has finished its mission
 Spec: (Eventually Goal1) & (Eventually Goal2)
 Trace r satisfies this spec if there exist positions i and j such that
(r, i) |= Goal1 and (r, j)|= Goal2
 No specific order specified in which goals are achieved
 Spec: Eventually [Goal1 & (Eventually Goal2)]
 Trace r satisfies this spec if there exist positions i and j such that
i<=j and (r, i) |= Goal1 and (r, j)|= Goal2
 Spec: Eventually [Goal1 & Next (Eventually Goal2)]
 Trace r satisfies this spec if there exist positions i and j such that
i<j and (r, i) |= Goal1 and (r, j)|= Goal2
Recurrence and Persistence
 Repeatedly j = Always Eventually j
 For every position j, (r,j) |= Eventually j
 For every j, there exists a position i>=j such that (r,i) |= j
 There are infinitely many positions where j holds
 Persistently j = Eventually Always j
 For some position j, (r,j) |= Always j
 There exists j such that for all positions i>=j, (r,i) |= j
 Formula j becomes true eventually and stays true
 The two patterns are logical duals: A trace satisfies Repeatedly j if
and only if it does not satisfy Persistently ~ j
Examples
 Example trace
x: 0
y: 0
1
1
2
0
3
1
4
0
5…
1…
Repeatedly (y=0)
Persistently (x >= 10)
Always [ even(x)  Next odd(x) ]
Repeatedly prime(x)
Requirements-based Design
 Given:
 Input/output interface of system C to be designed
 Model E of the environment
 LTL-formula j over input/output variables and also state variables
of the environment model E
 Design problem: Fill in details of C so that every infinite execution of
the composite system satisfies the LTL-formula j

Applies to synchronous as well as asynchronous designs
Temporal Implications and Equivalences
 Understanding subtle differences among different variants of LTL
formulas can be tricky
 Formula j is stronger than the formula y : whenever a trace
satisfies j, it is guaranteed to satisfy y
 Every trace satisfies the implication j  y
 Formula j is equivalent to the formula y : a trace satisfies j if and
only if it satisfies y
 Two formulas express exactly the same requirement
 Knowing some standard equivalences can be useful for simplifying
formulas
Temporal Implications and Equivalences
 Always j is stronger than j
 Repeatedly j is equivalent to ~ Persistently ~ j
 Persistently j is stronger than Repeatedly j
 Always j is equivalent to [j & Next Always j ]
 What’s the relationship between

Always Eventually j

Next Always Eventually j

Eventually Always Eventually j
 Are these equivalent?
Eventually (j | y) and Eventually j | Eventually y
 Are these equivalent?
Eventually (j & y) and Eventually j & Eventually y
Model Checking
System Model
LTL Requirement
Model Checker
yes
no/bug
 Performed using enumerative or symbolic search through the statespace of the program
 Success story for transitioning academic research to industrial
practice
 2007 Turing Award to Ed Clarke, Alan Emerson, and Joseph Sifakis
 Used to debug multicore protocols, pipelined processors, device driver
code, distributed algorithms in Intel, Microsoft, IBM …
Buchi Automata
 A safety monitor classifies finite executions into good and bad
 Verification of safety requirements is done by analyzing reachable
states of the system composed with the monitor
 Bug: An execution that drives the monitor into an error state
 How can a monitor (also called an automaton) classify “infinite”
executions into good and bad?
 Theoretical model of Buchi automata proposed by Richard Buchi (1960)
 Model checking application (1990s) using Buchi automata
 Automatically translate LTL formula j to a Buchi monitor M
 Consider the composition of system C and monitor M
 Reachable cycles in this composite correspond to counter-examples
(if no such cycle is found, system satisfies spec)
 Implemented in many model checkers including SPIN
Buchi Automaton: Example 1
e
~e
e
b
a
~e
 Inputs: boolean variable e
 Of two states a and b, a is initial and b is accepting
 Given a trace r over e (i.e. infinite sequence of 0/1 values to e),
there is a corresponding execution of M
 The trace r is accepted if accepting state appears repeatedly
 Language of M = Set of traces in which e is satisfied repeatedly
 M accepts r iff r |= Repeatedly e
Buchi Automaton: Example 2
e
a
b
 Automaton is nondeterministic: as long as it is in state a, at each
step it can either stay in state a, or switch to state b
 On a given input trace, many possible executions
 An execution is accepting if it visits accepting state repeatedly
 M accepts an input trace if there exists some accepting
execution on that input
 M accepts r iff r |= Persistently e
Buchi Automaton: Example 3
 Design a Buchi automaton such that
M accepts r iff r |= Always [ e  Eventually f ]
 Inputs: Boolean conditions e and f
 In an accepting execution, every e must be followed by f
~f
~e|f
e & ~f
b
a
f
Buchi Automaton: Example 4
a
e
b
f
c
Which traces does this accept? Express it in LTL
M accepts r iff r |= Repeatedly e & Repeatedly f
Buchi Automaton M Definition
V: set of Boolean input variables
Finite set Q of states
Set Init of initial states
Set F of accepting states
Set of edges/transitions, where each edge is of the form q –Guard q’
where Guard is a Boolean-valued condition over input vars V
 Given an input trace r = v1, v2, v3, … over V, an accepting run/execution
of M over r is an infinite sequence of states q0, q1, q2, … such that
1. State q0 is initial
2. For each i, there exists an edge qi-Guard qi+1 such that input vi
satisfies Guard
3. There are infinitely many positions i such that state qi is in F
 The automaton M accepts the input trace r if there exists an
accepting run of M over r





Buchi Automata: More Examples
~e
e
Eventually e
e
Eventually e
Buchi Automata Examples
a
e
b
f
c
Eventually e | Eventually f
Eventually [e & Next Eventually f]
a
e
b
f
c
Nondeterministic Buchi Automaton
e
Persistently e
Can we construct an equivalent deterministic Buchi automaton ?
No! Nondeterminism is sometimes necessary!
Omega-Regular Languages
The language of a Buchi automaton is the set of traces it accepts
Such languages are called omega-regular
Well-developed theory of omega-regular languages
Analogous the classical theory of regular languages (i.e. languages of
finite strings of input characters accepted by finite automata)
 Relevance to us: Given an LTL formula j, there is an algorithm to
construct a Buchi automaton Mj that accepts exactly those traces that
satisfy the formula j




Safety Monitors
System
Is there an execution of the System
for which the Monitor can enter an
error state?
Monitor is designed so that such an
execution indicates a bug!
Verification => Reachability
Monitor
Check if error state is reachable in
composition of System and Monitor
Buchi Monitors
System
Is there an infinite execution of the
System which is accepted by M? that
is, an execution in which some error
state appears repeatedly?
Monitor is designed so that such an
execution indicates a bug!
Verification => Search for cycles
Buchi Monitor M
Check if there is a reachable cycle
containing an error state in the
composition of System and Monitor
Example Buchi Monitor
RailRoadController
mode
signal
signal = red
mode = wait
Buchi Monitor M
Correctness requirement:
Always ( Train waiting 
Eventually Signal is green)
Violation of requirement:
Infinite execution where, at some step,
west train is waiting and in all
subsequent times west signal is red
Verification => Search for reachable
cycle containing red monitor state in the
composite system
From LTL to Buchi Automata
LTL Formula j
Tableau
Construction
Buchi Automaton Mj
Automaton Mj accepts exactly those traces that satisfy formula j
To check if a system C satisfies the LTL correctness requirement j
 Construct the Buchi automaton M~j corresponding to negated spec
 Search for cycles in composition of C and M~j
Reachability Problem for Transition Systems
Transition System T
Property j
Verifier
Is j reachable?
Yes/Counterexample
no
 Is there a (finite) execution from an initial state to a state satisfying j
 Checking whether j is an invariant of T => Checking if ~ j is reachable
 Verification techniques
1. Proof-based: Inductive invariants
2. Enumerative on-the-fly search
3. Symbolic search based on iterative image computation
Repeatable Property for Transition Systems
Transition System = States, Initial states, Transitions
Property j : Subset of states
Property j is repeatable if there
exists an infinite execution that
satisfies Repeatedly j
Is there a state s such that
1. s is reachable
2. s satisfies j
3. there is a cycle containing s
Repeatability Problem for Transition Systems
Transition System T
Property j
Verifier
Is j repeatable?
Yes/Counterexample
no
 Is there an infinite execution along which states satisfying j appear
repeatedly?
 To check whether a system C satisfies an LTL formula j, check if Mode
is Accepting is repeatable in composition of C and Buchi monitor M~j
 Verification techniques
1. Proof-based: Ranking functions
2. Enumerative: Nested Depth-first Search
3. Symbolic search
Recap: Symbolic Transition Systems
 Region over variables X is a data structure that represents a set of
states assigning values to X
 Transition system T with state variables S represented by
 Region jI over S for initial states
 Region jT over S U S’ for transitions
 Symbolic representation can be compiled automatically from code for
updating variables
Towards Symbolic Algorithm
Init
Find states that are reachable and
satisfy the property j
Find set of reachable states using
symbolic reachability algorithm,
and intersect it with j
Property j
Symbolic Image Computation
 Core problem in symbolic search: Compute the post-image (i.e. the set
of successors) of states in a given region
 Given:
 A of type reg over state variables S
 Trans of type reg over S U S’
 Post(A, Trans) = Rename(Exists(Conj(A,Trans),S), S’, S)
1. Take conjunction of A and Trans
2. Project out the variables in S using existential quantification
3. Rename primed variables to get a region over S
Symbolic BFS Algorithm
Given region Init over S and region Trans over S U S’, compute the region
representing all reachable states
reg Reach := Empty; /* States found reachable */
reg New := Init; /* States not yet explored for outgoing transitions */
while IsEmpty(New) = 0 { /* while there are states to be explored */
Reach := Disj(Reach,New); /* add new states to reachable states */
New := Diff(Post(New,Trans),Reach);
/*These are states in post-image of New, but not
previously found reachable, so to be explored */
};
First phase of Symbolic Repeatability Check involves computing Reach
Symbolic Repeatability Check
Find states s in Recur0 such that
from s there is a path with 1 or more
transitions to some state in Recur0
Repeat to get Recur2 from Recur1
Recur2 = Reachable & j &
Next Eventually (j & Next Eventually j )
Recur1 = Reachable & j & Next Eventually j
Property j
Recur0 = Reachable & j
Repeat to get Recuri+1 from Recuri
Symbolic Repeatability Check
What can we conclude if Recuri+1 is empty
What can we conclude if Recuri+1 = Recuri
Symbolic Repeatability Check
 Key step: Given a region A, find the sub-region
{ s in A | there exists t in A that is reachable from s in >=1 transitions}
 Recall: To compute states reachable from Init, we repeatedly apply
Post-image operator
 Symmetrically, to find from which states A is reachable, we can
repeatedly apply pre-image operator
 To get desired result, intersect this set with A
Symbolic Pre-Image Computation
 Pre-image of a region A = Set of predecessors of states in A
Pre(A,Trans) = { s | there exists a state t in A s.t. s  t is a transition}
 Given:
 A of type reg over state variables S
 Trans of type reg over S U S’
 Pre(A, Trans) = Exists(Conj(Rename(A,S,S’),Trans),S’)
1. Rename variables in A to primed copies to get a region over S’
2. Take conjunction of the result with Trans (this captures the set of
transitions whose target states belong to A)
3. Project out the variables in S’ using existential quantification
Symbolic Repeatability Algorithm
Phase 1: Compute Reach as shown before
reg Recur := Conj(Reach, j); /* Potential candidate states for cycle */
while IsEmpty(Recur) = 0 { /* while there are potential candidates */
/* Compute from which states Recur is reachable */
Reach := Empty;
New := Pre(Recur, Trans); /*Ensure at least one transition */
While IsEmpty(New)=0 {
Reach := Disj(Reach,New);
if IsSubset(Recur,Reach)=1
then return 1; /*Recur won’t change; Property repeatable */
New := Diff(Pre(New,Trans),Reach);
};
Recur := Conj(Recur, Reach); /*Subset from which Recur is reachable
};
return 0. /* No execution with property repeating */
Example
A
B
C
D
E
F
H
Analysis of Symbolic Repeatability
 Correctness (1): If there is a reachable state s that satisfies j, and
there is an infinite execution starting in s satisfying Repeatedly j,
then s will always stay in Recur (and thus, Recur cannot get empty)
 Correctness (2): If inner loop finds that from every state in Recur,
some state in Recur is reachable with >=1 transitions, then indeed there
is an infinite execution satisfying Repeatedly j
 Algorithm is sound: cannot give wrong answers
 If transition system has n reachable states of which k satisfy j, then
algorithm terminates with O(nk) region operations
 In practice, depends on how effective is data structure for regions