Model Checking BasicsSomesh JhaComputer Science DepartmentUniversity of WisconsinMadison, WI 537031 IntroductionIn software engineering several formalism are in some form or another compositions of state ma-chines. For example, Statecharts are simply state machines. There is value in simply writing theseformal specifications down because it forces the designer to think carefully. However, in highlydistributed designs subtle errors (such as deadlocks or race conditions) are very hard to catch sim-ply by inspection. The difficulty stems from the fact that the global state space of the entire systemcan be very large and exhibit very complex behaviors. Therefore, there is a need for automaticanalysis of specifications expressed as composition of state machines. Model checking is a tech-nique for automatically analyzing whether a model of a distributed system has a desired property,e.g., absence of deadlocks.Model checking takes as its input a formal model of the system and a property expressed intemporal logic. Temporal logics are logics that have a notion of time. Using sophisticated statespace exploration techniques a model checker verifies that the model satisfies the desired property.If the property turns out to be false in the model, most model checkers output a counter-exampleor a trace of states in the model that shows “why” the property does not hold. Figure 1 gives aschematic description of a model-checker.Next we describe the two inputs to the model checker. The discussion is kept at an abstractlevel. We will discuss specific details when we describe the model checker NuSMV.2 Describing the modelA model M has two components V and R described below:• VariablesV is the set of state variables in the model. If the model has n state variables, we will denotethem by v1, · · · , vn. Each state variable vihas an associated domain Di. Notice that theentire state space of the system is simply the Cartesian product of the domains D1, · · · , Dn(denoted byQni=1Di). A state is simply an assignment to the variables in the set V fromtheir domain. For example, consider a model that has two variables x and y with domains{a, b, c} and {0, 1} respectively. Then (x = b, y = 1) is a state of the model. The set of allstates is called the state space of the model and will be denoted by S.1Model of the systemProperty usuallyexpressed intemporal logicModel checkerState space explorationYESNOcounter-exampleFigure 1: Schematic description of model checking• Transition relationR is the transition relation. Formally, R is the relation from S to S (denoted as R : S ↔ S).If (s, s0) ∈ R, this means that from state s it is possible or valid to transition to state s0. Thetransition relation R encapsulates all possible/valid transitions in the model.Usually, a set of initial states I ⊆ S is also specified. The model M can start in any ofthe initial states I. Therefore, we will write a model M as (V, R, I) emphasizing the fact that ithas three components, i.e., the set of variables, transition relation, and a set of initial states. Thespecific language used to describe the model is not very important to describe the concepts. Wewill describe a specific modeling language later. States of a model M were defined before. A pathis a finite or infinite sequence of states (s0, s1, · · · , si, · · ·) such that (si, si+1) is a valid transitionin the model. In other words a path describes a sequence of states were each step corresponds toa valid transition in the model. Usually we will denote a path using the Greek symbol π. Givena path π = (s0, s1, · · · , si, · · ·), πidenotes the suffix of π starting at the i-th state, or given by thefollowing sequence:(si, si+1, · · · , )Figure 2 shows a small model (can you guess what the model does?). A path π through the modelis shown below:((x = 0, y = −1), (x = 0, y = 0), (x = 0, y = 1), (x = 1, y = 1), (x = 0, y = 0))Path π2starts at the second state (remember we start counting from zero) and is shown below:((x = 0, y = 1), (x = 1, y = 1), (x = 0, y = 0))3 Temporal logicIn temporal logic one can talk about “time” in addition to atomic properties. As we will see later,it is important to have the notion of time to express properties about reactive systems. We willdescribe a powerful temporal logic called the Computation Tree Logic or CTL?for short.2x=0y=-1x=0x=0y=0y=1x=1x=1y=0y=1Figure 2: A small exampleFirst, we describe atomic properties for describing “local” properties about states. Throughoutthis section consider a model M = (V, I, R), where there are n state variables V = {v1, · · · , vn}.Let Dibe the domain associated with variable vi. A basic atomic property has the following form:• vi= x, vi∈ S, vi< x, and vi> x where x is another variable from the set V or a constantfrom the domain Diof the variable viand S is a subset of the domain Diassociated with x.A basic atomic property is an atomic property. More complicated atomic properties can be con-structed from other atomic properties using conjunction (denoted by ∧), disjunction (denoted by∨), and negation (denoted by ¬). An example of an atomic property is given below:p = (x = y) ∧ ¬(z > 3) (1)Recall that a state s is simply an assignment to all the variables v1, · · · , vn. Suppose there is aprogram with three variables x, y, and z. Consider the following two states:s1= (x = 3, y = 3, z = 2)s2= (x = 3, y = 2, z = 2)Consider the atomic property p shown in equation 1. The atomic property p shown in equation 1is true in state s1and false in state s2(why?). We denote this fact by s1|= p (or s1satisfies p) ands26|= p (or s2does not satisfy p). Hence given an atomic property p and a state s one can decidewhether or not s satisfies p.CTL?has two types of formulas state formulas (to express properties about states) and pathformulas (to express properties about paths). Let AP be the set of atomic properties. Grammars3SF → APSF → {¬SF | SF ∧ SF | SF ∨ SF }SF → {A(P F ) | E(P F )}Figure 3: Grammar for generating state formulasP F → SFP F → {¬P F | P F ∧ P F | P F ∨ P F }P F → {X P F | F P F | G P F | P F U P F | P F R P F }Figure 4: Grammar for generating path formulasfor generating state and path formulas in CTL?are shown in Figure 3 and 4 respectively. SF andP F are non-terminals that derive state and path formulas respectively. Recall that AP is the set ofatomic formulas.Exercise 1 Consider the formula f given below:f = A((x = 2) U