LTL Model Checking 15-820A LTL Model Checking 15-820A Flavio Lerda 1

LTL Model Checking 15-820A LTL Model Checking 15-820A Flavio Lerda 1

LTL Model Checking 15-820A LTL Model Checking LTL – Subset of CTL* of the form: Af where f is a path formula LTL model checking – Model checking of a property expressed as an LTL formula: – Given a model M and an initial state s0: M,s0 A f 2

LTL Model Checking 15-820A LTL Formulas Subset of CTL* – Distinct from CTL AFG p LTL f CTL . f AFG p Contains a single universal quantifier – The path formula f holds for every path Commonly: – A is omitted – G is replaced by (box or always) – F is replaced by (diamond or eventually) 3

LTL Model Checking 15-820A LTL Model Checking Given a model M and an LTL formula – Build the Buchi automaton B – Compute product of M and B Each state of M is labeled with propositions Each state of B is labeled with propositions Match states with the same labels – The product accepted the traces of M that are also traces of B ( M ) – If the product accepts any sequence We have found a counter-example 4

LTL Model Checking 15-820A Language Emptiness M Compute strongly connected components – Non trivial – Containing an accepting state None means no sequence is accepted – Proved the property Very expensive 5

LTL Model Checking 15-820A Nested Depth First Search The product is a Büchi automaton How do we find accepted sequences? – Accepted sequences must contain a cycle In order to contain accepting states infinitely often – We are interested only in cycles that contain at least an accepting state – During depth first search start a second search when we are in an accepting states If we can reach the same state again we have a cycle (and a counter-example) 6

LTL Model Checking 15-820A Example 7

LTL Model Checking 15-820A Example 8

LTL Model Checking 15-820A Nested Depth First Search procedure DFS(s) visited visited {s} for each successor s’ of s if s’ visited then DFS(s’) if s’ is accepting then DFS2(s’, s’) end if end if end for end procedure 9

LTL Model Checking 15-820A Nested Depth First Search procedure DFS2(s, seed) visited2 visited2 {s} for each successor s’ of s if s’ seed then return “Cycle Detect”; end if if s’ visited2 then DFS2(s’, seed) end if end for end procedure 10