Automata-Theoretic LTL Model-CheckingArie [email protected]/CMUAutomata-Theoretic LTL Model-Checking – p.1Determines Patterns on Infinite Traces Atomic Propositions Boolean Operations Temporal operators a “a is true now” X a “a is true in the neXt state” Fa “a will be true in the Future” Ga “a will be Globally true in the future” a U b “a will hold true Until b becomes true” LTL - Linear Time Logic (Pn 77) aDetermines Patterns on Infinite Traces Atomic Propositions Boolean Operations Temporal operators a “a is true now” X a “a is true in the neXt state” Fa “a will be true in the Future” Ga “a will be Globally true in the future” a U b “a will hold true Until b becomes true” LTL - Linear Time Logic (Pn 77) aDetermines Patterns on Infinite Traces Atomic Propositions Boolean Operations Temporal operators a “a is true now” X a “a is true in the neXt state” Fa “a will be true in the Future” Ga “a will be Globally true in the future” a U b “a will hold true Until b becomes true” LTL - Linear Time Logic (Pn 77) aDetermines Patterns on Infinite Traces Atomic Propositions Boolean Operations Temporal operators a “a is true now” X a “a is true in the neXt state” Fa “a will be true in the Future” Ga “a will be Globally true in the future” a U b “a will hold true Until b becomes true” LTL - Linear Time Logic (Pn 77) a a a a aDetermines Patterns on Infinite Traces Atomic Propositions Boolean Operations Temporal operators a “a is true now” X a “a is true in the neXt state” Fa “a will be true in the Future” Ga “a will be Globally true in the future” a U b “a will hold true Until b becomes true” LTL - Linear Time Logic (Pn 77) a a a a bOutline•Automata-Theoretic Model-Checking◦Finite Automata and Regular Languages◦Automata over infinite words: Büchi Automata◦Representing models and formulas with automata◦Model checking as language emptinessAutomata-Theoretic LTL Model-Checking – p.2Finite AutomataA finite automaton A (over finite words) is a tuple(Σ, Q, ∆, Q0, F ), where•Σ is a finite alphabet•Q is a finite set of states•∆ ⊆ Q × Σ × Q is a transition relation•Q0⊆ Q is a set of initial states•F ⊆ Q is a set of final statesAutomata-Theoretic LTL Model-Checking – p.3Finite Automaton: An Exampleabb, ca, cq0q1Σ = {a, b, c}, Q = {q0, q1}, Q0= {q0}, F = {q1}Automata-Theoretic LTL Model-Checking – p.4A Run•A run of A over a word v ∈ Σ∗of length |v| is a mappingρ : {0, 1, ..., |v|} → Q s.t.◦First state is the initial state: ρ(0) ∈ Q0◦States are related by transition relation:∀0 ≤ i ≤ |v| · (ρ(i), v(i), ρ(i + 1)) ∈ ∆•A run is a path in A from q0to a state ρ(|v|) s.t. the edgesare labeled with letters in v•A run is accepting if it ends in an accepting state: ρ(|v|) ∈ F .•A accepts v iff exists an accepting run of A on v.Automata-Theoretic LTL Model-Checking – p.5An Example of a Runabb, ca, cq0q1•A run q0, q1, q1, q1, q0on aacb is accepting•A run q0, q0, q0, q0, q0on bbbb is accepting•A run q0, q0, q1, q1, q1on baac is rejectingAutomata-Theoretic LTL Model-Checking – p.6LanguageThe language L(A) ⊆ Σ∗is the set of all words in Σ∗acceptedby A .abb, ca, cq0q1The language is {ǫ, b, bb, ccc, bab, . . .}That is, a regular expression: ǫ + a(a + c)∗b(b + c)∗Automata-Theoretic LTL Model-Checking – p.7Regular Languages•A set of strings is regular if is a language of a finiteautomaton (i.e., recognizable by a finite automaton)•An automaton is deterministic if the transition relation isdeterministic for every letter in the alphabet:∀a · (q, a, q′) ∈ ∆ ∧ (q, a, q′′) ∈ ∆ ⇒ q′= q′′otherwise, it is non-deterministic.•NFA = DFA: Every non-deterministic finite automaton (NFA)can be translated into a language-equivalent deterministicautomaton (DFA)Automata-Theoretic LTL Model-Checking – p.8Automata on Infinite Words•Reactive programs execute forever – need infinitesequences of states to model them!•Solution: finite automata over infinite words.•Simplest case: Büchi automata◦Same structure as automata on finite words•... but different notion of acceptance◦Recognize words from Σω(not Σ∗!)•Σ = {a, b} v = abaa baaab...•Σ = {a, b, c}L1= {v | in v after every a there is a b}Some words in L1:ababab · · · aaabaaab · · ·abbabbabb · · · accbaccb · · ·Automata-Theoretic LTL Model-Checking – p.9Infinite Run and Acceptance•Recall, F is the set of accepting states•A run ρ of a Büchi automaton A is over an infinite wordv ∈ Σω. Domain of the run is the set of all natural numbers.•Let inf(ρ) be the set of states that appear infinitely often in ρ:inf(ρ) = {q | ∀i ∈ N · ∃ j ≥ i · ρ(j) = q}•A run ρ is accepting (Büchi accepting) iff inf(ρ) ∩ F 6= ∅.•A set of strings is ω-regular iff it is recognizable by a BüchiautomatonAutomata-Theoretic LTL Model-Checking – p.10Exampleabb, ca, cq0q1Automata-Theoretic LTL Model-Checking – p.11Exampleabb, ca, cq0q1Language of the automaton is: ((b + c)ωa(a + c)∗b)ωThis is an ω-regular expressionAutomata-Theoretic LTL Model-Checking – p.11ExamplesLet Σ = {0, 1}. Define Büchi automata for the followinglanguages:1. L = {v | 0 occurs in v exactly once}2. L = {v | after each 0 in v there is a 1}3. L = {v | v contains finitely many 1’s}4. L = (01)nΣω5. L = {v | 0 occurs in every even position of v}Automata-Theoretic LTL Model-Checking – p.12Closure PropertiesBüchi-recognizable languages are closed under ...•(alphabet) projection and union◦Same algorithms as Finite Automata•intersection◦Different construction from Finite Automata•complement◦i.e., from a Büchi automaton A recognizing L one canconstruct an automatonA recognizing Σω− L.◦A has order of O(2QlogQ)) states, where Q are states inA [Safra’s construction]Automata-Theoretic LTL Model-Checking – p.13Complementation: ExampleComplement is easy for deterministic Büchi automata:Aabb, ca, cq0q1Automata-Theoretic LTL Model-Checking – p.14Complementation: ExampleComplement is easy for deterministic Büchi automata:Aabb, ca, cq0q1Aaa, b, ca, cAutomata-Theoretic LTL Model-Checking – p.14Complementation: ExampleComplement is easy for deterministic Büchi automata:Aabb, ca, cq0q1Aaa, b, ca, cBut, Büchi
View Full Document