IA159 Formal Verification Methods Model Checking: An Overview Jan Strejček Department of Computer Science Faculty of Informatics Masaryk University Focus and sources Focus ■ model checking in general ■ specifications, linear temporal logic (LTL), Büchi automata ■ models, Kripke structure, process rewrite systems (PRS) ■ model checking problems and decidability ■ LTL model checking of finite systems ■ state explosion problem Sources ■ Chapters 1,2,3 and 9 of E. M. Clarke, O. Grumberg, and D. A. Peled: Model Checking, MIT, 1999. m R. Mayr: Decidability and Complexity of Model Checking Problems for Infinite-State Systems. PhD thesis, 1998. IA159 Formal Verification Methods: Model Checking: An Overview 2/30 Model checking schema model M specification S model checking algorithm NO, M does not satisfy S (+ counterexample) IA159 Formal Verification Methods: Model Checking: An Overview Model checking Specification IA159 Formal Verification Methods: Model Checking: An Overview 4/30 Specification a finite formal description of some property that should be satisfied by all behaviours of the system usually does not fully specify the system typically given by a formula of some temporal logic ■ Linear Temporal Logic (LTL) (linear time) ■ Computational Tree Logic (CTL) (branching time) ■ CTL*, Hennessy-Milner logic, /x calculus, ... can be given also by a Büchi automaton, etc. IA159 Formal Verification Methods: Model Checking: An Overview 5/30 The hierarchy of basic temporal logics. modal /x-calculus CTL* LTL Henessy-Milner logic The hierarchy of selected temporal logics according to their expressive power. IA159 Formal Verification Methods: Model Checking: An Overview State-based vs. action-based logics state-based These logics talk about properties of states of a system. Properties of a single state are reflected by validity of atomic propositions in the state. State-based logic are interpreted over behaviours of the system represented by sequences (or trees) of sets of valid atomic propositions. action-based Every transition of a system is labelled with an action. Action-based logic are interpreted over behaviours of the system represented only by sequences (or trees) of actions. We provide definition of both state-based and action-based LTL. IA159 Formal Verification Methods: Model Checking: An Overview 7/30 Syntax of state-based LTL State-based Linear Temporal Logic (LTL) is defined by if ::= T | a | -itf | | aa ... ab» • • ... Fa eventually •• ... • a • • • ... Ga always a a a a ... IA159 Formal Verification Methods: Model Checking: An Overview 8/30 Semantics of state-based LTL Let T. = 2AP', where AP' c AP is a finite subset. We interpret LTL on infinite words w = i/i/(0)i/i/(1)... g Zw. By w-, we denote the suffix of w of the form w(i)w(i + 1)w(i + 2).... The validity of an LTL formula

1 A 1/1/ = (/?2 \=Xip ff l/l/| = t£> 1= <£1 U 1 Given an alphabet Z, an LTL formula ip defines the language Lz(j3) = {wer | w\=tp}. IA159 Formal Verification Methods: Model Checking: An Overview 9/30 Action-based LTL Differences between action-based and state-based LTL ■ In the syntax, a ranges over countable set of actions Act. ■ Formulae of action-based LTL are then interpreted over infinite sequences w of actions from a finite subset Act' c Act. ■ Semantics of formula a is defined as follows: w |= a iff a = i/i/(0) IA159 Formal Verification Methods: Model Checking: An Overview 10/30 Examples of LTL formulae G-ie/ror - safety property G(p => Fq) - response property GFp - liveness property IA159 Formal Verification Methods: Model Checking: An Overview Büchi automata A Büchi automaton (BA) is a tuple A = (I, Q, 5, q0, F), where ■ I is a finite alphabet, ■ Q is a finite set of states, ■ 5 : Q xl -^ 2Q is a transition function, ■ qo e Q is an initial states, ■ F c Q is a set of accepting states. A run of A on inifnite word w = i/i/(0)i/i/(1)... g Zw is an infinite sequence of states a = a(0)a(1)..., where o-(O) = q0 and a(i + 1) g 5(a(i), w(i)) holds for all /'. A run a is acceptir g if Inf (a) n F 7^ 0, where Inf (a) is the set of the states appearing in a infinitely often. An automaton A accepts a word w if there is an accepting run of A on w. We set L{A) = {w g iy | A accepts w}. IA159 Formal Verification Methods: Model Checking: An Overview 12/30 Example of a Büchi automaton IA159 Formal Verification Methods: Model Checking: An Overview 13/30 Example of a Büchi automaton Accepts the words with infinitely many occurences of a. IA159 Formal Verification Methods: Model Checking: An Overview Model checking Model IA159 Formal Verification Methods: Model Checking: An Overview 15/30 a finite formal description of all possible behaviours of the system to be verified behaviour is a sequence (or a tree) of states/actions state is an image of the system in a certain moment (current values of variables, program counter, etc.) a state is characterized by validity of atomic propositions (e.g. PC == start, x > 5) many possible formalisms ■ standard languages C, Java, VHDL, ... ■ dedicated languages, e.g. ProMeLa (Process or Protocol Meta Language) ■ process algebras (infinite-state systems) BPA, BPP, PA, pushdown processes, Petri nets, ... ■ low-level formalisms: Kripke structure (for state-based approach) and labelled transition systems (for action-based approach) IA159 Formal Verification Methods: Model Checking: An Overview 16/30 Example: mutual exclusion in ProMeLa byte cnt = 0; // number of processes in critical sections byte turn = 0; // token for entering a critical section mit { run (P0) ; run (PI) ; // parallel execution of P0 a PI proctype P0( proctype PI // s0 do // NCO (noncritical section) : : do :: (turn ==0) -> break; :: else; od; // CSO (critical section) cnt = cnt + 1; cnt = cnt - 1; turn = 1; od; //si do // NCI (noncritical section) : : do :: (turn ==1) -> break; : : else; od; // CS1 (critical section) cnt = cnt + 1; cnt = cnt - 1; turn = 0; od; IA159 Formal Verification Methods: Model Checking: An Overview 17/30 Kripke structure Let AP be a countable set of atomic propositions. A Kripke structure is a tuple M = (S, R, S0, Ľ), where ■ S is a set of states R c S x S is transitions relation ■ So c S is a set of initial states ■ L : S -► 2AP is a labellii function associating to each state s g S the set of atomic propositions that are true in s. A path in M starting in a state s is an infinite sequence 7T = s0s-\ s2... of states such that s0 = s and (s,, s/+1) g R holds for every /'. IA159 Formal Verification Methods: Model Checking: An Overview 18/30 Example: mutual exclusion as a Kripke structure IA159 Formal Verification Methods: Model Checking: An Overview Process rewrite systems hierarchy (PRS-hierarchy) The hierarchy compares expressive power of many classes of infinite-state systems including BPA, BPP, PA, Petri nets (PN), and pushdown processes (PDA). FS stands for finite systems. PRS PAD PDA BPA PAN PN BPP IA159 Formal Verification Methods: Model Checking: An Overview 20/30 Model checking Decidability of model checking IA159 Formal Verification Methods: Model Checking: An Overview 21/30 Model checking Model checking problem is to decide whether all behaviours of a given system satisfy a given specification. ■ specific problems for specific input ■ state-based LTL model checking of finite systems ■ action-based CTL model checking of finite systems ■ state-based LTL model checking of pushdown processes ■ action-based LTL model checking of pushdown processes ■ ... ■ model checking problem is not decidable for some kinds of input (e.g. action-based LTL model checking of PA processes) ■ all model checking problems are decidable for finite systems IA159 Formal Verification Methods: Model Checking: An Overview 22/30 The decidability boundary The decidability boundary of the action-based LTL model checking in the PRS-hierarchy. PRS PAD undecidable decidable PDA PA PAN PN BPP FS IA159 Formal Verification Methods: Model Checking: An Overview 23/30 Model checking Automata-based LTL model checking of finite systems IA159 Formal Verification Methods: Model Checking: An Overview 24/30 Automata-based LTL model checking of finite systems Kripke structure M with finitely many states Büchi automaton Am accepts paths of M starting in initial states and projected by L to 2AP^) LTL formula ip Büchi automaton A^v words over 2Ap(v) violating ip product Büchi automaton B L{B) = L(Am) n L(A^) L{B) = 0 e.g. nested DFS algorithm YES NO + counterexample IA159 Formal Verification Methods: Model Checking: An Overview 25/30 Complexity notes Complexity Time and space complexity of the LTL model checking algorithm is 0(\M\ • 2°(|¥,|)), where \M\ is the number of states and transitions in the Kripke structure M. LTL model checking problem is PSPACE-complete. state explosion problem - \M\ is often exponential in the size of implicit description of the system due to ■ parallelism ■ large data domains dynamically allocated memory IA159 Formal Verification Methods: Model Checking: An Overview 26/30 State explosion problem - an example byte x = 0; byte y = 0; proctype A() x = x + 1; proctype B() x = x + 2; proctype C () y = y + 5; x=x+2 IA159 Formal Verification Methods: Model Checking: An Overview 27/30 Partial solutions of the state explosion problem abstraction partial order reduction symmetry reduction on-the-fly algorithms symbolic model checking distributed algorithms IA159 Formal Verification Methods: Model Checking: An Overview 28/30 Our topics translation LTL^BA (via alternating 1-weak BA) partial order reduction state-based LTL model checking of pushdown processes abstraction counterexample guided abstraction refinement (CEGAR) IA159 Formal Verification Methods: Model Checking: An Overview 29/30 Coming next week LTL^BA via alternating 1-weak BA What is an alternating 1-weak Büchi automaton? Can we see it? IA159 Formal Verification Methods: Model Checking: An Overview 30/30