Transcript Model Checking - Teaching-WIKI

Intelligent Systems
Model Checking and Theorem Proving
slides by Gulay Unel
©www.sti-innsbruck.at
Copyright 2008 STI INNSBRUCK www.sti-innsbruck.at
Overview
• Model Checking
• Theorem Proving
www.sti-innsbruck.at
2
Model Checking - Overview
•
•
•
•
•
•
Introduction
Models
LTL
CTL
Other logics
Model Checking
www.sti-innsbruck.at
3
Introduction
• Model checking is an automated technique that, given a finite-state
model of a system and a formal property, checks whether this
property holds for (a given state in) that model
• Formally: M ⊨ Ф where the model M represents a design, and the
property Ф formalizes its correctness criteria
• Model checking focuses mostly on automatic decision procedures
• The model is often restricted to a finite state transition system
• Properties are expressed in a propositional logic such as: LTL, CTL
for which finite-state model checking is known to be decidable
• Note that model checking problem is not limited to finite state
systems or propositional logics
www.sti-innsbruck.at
4
Model: Transition System
• A transition system TS is a tuple (S, →, I, AP, L) where
–
–
–
–
–
S is a set of states
→⊆S×S
I ⊆ S is a set of initial states
AP is a set of atomic propositions
L: S → 2AP is a labeling function
• An execution: π = s0, s1, ... such that
– for every i ≥ 0, si → si+1
– s0 ∈ I
• Trace of an execution: sequence of sets of atomic propositions,
trace (π) = L(s0), L(s1), ...
• Traces(TS): set of all traces of all executions of TS, it defines the
observable behaviour of TS
www.sti-innsbruck.at
5
Property: Temporal Logic
• The properties of transition systems are expressed in temporal
logics, most often in propositional:
– Linear Time Temporal Logic (LTL)
– Branching Time Temporal Logic (CTL)
• In all of the logics the atomic formulas are the atomic propositions
from AP
• Each state s in a model TS has a set of atomic propositions L(s) that
are true in that state, all the other atomic propositions are false in s
www.sti-innsbruck.at
6
Syntax of LTL
• propositional logic
– true
– a, b, …∈ AP
–  α, α β
• temporal operators
– Xα
: neXt step fulfills α
– Fα
: sometimes in the Future α will hold
– Gα
: α Globally holds
– α U β : α holds Until β holds
• linear temporal logic is a logic for describing linear time properties
www.sti-innsbruck.at
7
Derived Operators
false ≡ true
α  β ≡ (α  β)
α  β ≡ α  β
α  β ≡ (α  β)  (β  α)
precedence order:
the unary operators bind stronger than the binary ones. and X bind
equally strong. U takes precedence over , , and 
, X, F, G
www.sti-innsbruck.at
>
U
>
, , , 
8
Examples – Properties of a traffic light
• the light is never red and green:
(red green)
• whenever the light is red, it cannot become green immediately
afterwards:
red   X green
• eventually, the light becomes green:
F green
www.sti-innsbruck.at
9
Practical properties in LTL
• Reachability
– reachability: F α
– conditional reachability: α U β
– reachability from any state: not expressible
• Safety: G α
• Liveness: G(α  F β) and others
• Fairness: G F α and others
www.sti-innsbruck.at
10
Semantics over Words
The language induced by LTL formula α over AP = {a1, …, an} is:
L(α) = { w ∈ (2AP)w | M ⊨ α } where ⊨ is defined as follows:
(let w=A0A1A2... and w[i] = AiAi+1Ai+2...)
w ⊨ true
w ⊨ ai
iff ai ∈ A0
w ⊨ α β
iff w ⊨ α and w ⊨ β
w⊨α
iff w ⊭ α
w⊨Xα
iff w[1]=A1A2A3... ⊨ α
w⊨Fα
iff j ≥ 0. w[j] ⊨ α
w⊨Gα
iff j ≥ 0. w[j] ⊨ α
w ⊨αUβ
iff j ≥ 0. w[j] ⊨ β and 0 ≤ i < j. w[i] ⊨ α
www.sti-innsbruck.at
11
Semantics for Transition Systems
Semantics is defined via set inclusion, a system satisfies a formula iff
all traces are allowed w.r.t. The formula
TS ⊨ α iff Traces(TS) ⊆ L(α)
www.sti-innsbruck.at
12
CTL in a nutshell
• Branching time model
• Path quantifiers (in addition to LTL)
– A = “for all future paths”
– E = “for some future path”
• Example: A F a = “inevitably a”
a
a
AFa
a
www.sti-innsbruck.at
13
Other logics : Mu - Calculus
• Logic of relations with fixed point operator
• Can express transitive closure
• Good for describing algorithms
www.sti-innsbruck.at
14
Model Checking
G(a F b)
yes
• input:
no
• output
MC
a
b
www.sti-innsbruck.at
a
b
– temporal logic
(property)
– transition system
(model)
– yes
– no +
counterexample
15
LTL Model Checking
• Vardi and Wolper
– Apply Büchi’s technique to LTL
– Automaton construction yields optimal decision algorithm
• Kurshan
– Specify properties directly as automata
• example: infinitely often a (G F a)
a
a
true
www.sti-innsbruck.at
16
CTL Model Checking
• Reasoning about properties of non-deterministic programs
– branching time properties of programs
– fixed point characterizations (Tarski)
• every monotonic function has least/greatest fixed point
– key idea: apply to finite graphs, not infinite trees
• can directly calculate Tarski fixed points
• Applications
– finite state machines in hardware
– protocols
– proved incorrectness of some published designs
www.sti-innsbruck.at
17
Theorem Proving (Resolution) - Overview
•
•
•
•
•
•
Introduction
Proof System
Resolution
Heuristic Search
Applications
Other Topics
www.sti-innsbruck.at
18
Introduction
Unlike in model checking, theorem proving solves the general validity of
a formula (whether a formula α holds in all models)
⊨α
• Utilizes the proof inference technique in some proof system
• Problem is transformed to a sequent, a working representation for
the theorem proving problem
• The simplest sequent used in natural deduction: ⊢ α
• A sequent holds when it satisfies its intended semantics
• For example, ⊢ α is derivable in natural deduction only if the formula
α holds in any model
www.sti-innsbruck.at
19
Proof System
A proof system is collection of inference rules of the form:
P1 … Pn
name
C
where C is a conclusion sequent, and Pi‘s are premises sequents .
If an infererence rule does not have any premises (called an axiom), its
conclusion automatically holds.
www.sti-innsbruck.at
20
Proof Tree
• A proof of a sequent is a proof tree whose nodes are sequents
• The root is the sequent to be proven (the theorem)
• For each sequent in the tree, all of its children are premises of some
inference rule in which that sequent is a conclusion
• A proof is complete when each sequent in the proof tree has an
associated inference rule
• There are two ways for building a proof tree:
– Bottom-up
– Top-down
www.sti-innsbruck.at
21
Proof by Refutation
• (Proof by contradiction, reductio ad absurdum)
• Method:
– Negate the theorem statement & add to axioms
– Show that this set of sentences is self-inconsistent
• Use rules of inference to derive the False statement
• This means that the sentences can’t all be true at same time
• But the axioms are true
• Hence the negated theorem must be false
• Hence the theorem must be true
www.sti-innsbruck.at
22
The Resolution Method
• Uses proof by refutation
• Requires sentences to be in a particular format
– Conjunctive Normal Form [CNF]
• Uses a single inference rule
– Generalised resolution rule
• Need to understand the unification method (this lecture)
• Method is refutation-complete
– If a theorem is true and representable in first order logic
• Then this method will prove it [amazing result by Robinson,
1965]
• No guarantees given about how long it will take
– Actually takes a long time to prove even fairly trivial theorems
– Can use heuristics to speed it up
www.sti-innsbruck.at
23
The Resolution Method - Overview
• Maintain a knowledge base of clauses
– Start with the axioms and negation of theorem
• Resolve pairs of clauses
– Using single rule of inference (generalised resolution)
– Resolved sentence contains fewer literals
• Proof ends with the empty clause
– Signifies a contradiction
– Must mean the negated theorem is false
• Because the axioms are consistent
– Therefore the original theorem was true
www.sti-innsbruck.at
24
Resolution Rule
• Takes two clauses in Conjunctive Normal Form
– Finds a literal L1 in one and and a literal L2 in the other
– Such that the L1 unifies with ¬L2 (with substitution mu)
– In the resolved clause, L1 and L2 are omitted
– And the substitution is applied to the whole disjunction
p1 ∨ ... ∨ pj ∨ ... ∨ pm,
q1 ∨ ... ∨ qk ∨ ... ∨ qn,
Subst(mu, (p1 ∨ ... ∨ pj-1 ∨ pj+1 ∨ ... ∨ pm ∨ q1 ∨ ... qk-1 ∨ qk+1 ∨ ... ∨ qn))
www.sti-innsbruck.at
25
Empty Clause Signifies False
• Resolution theorem proving ends
– When the resolved clause has no literals (empty)
• This can only be because:
– Two unit clauses were resolved
• One was the negation of the other (after substitution)
– Example: q(X) and ¬q(X) or: p(X) and ¬p(simon)
• Hence if we see the empty clause
– This was because there was an inconsistency
– Hence the proof by contradiction has occurred
www.sti-innsbruck.at
26
Aristotle Example
• All men are mortal and Socrates is a man
• Therefore Socrates is mortal
• Initial Knowledge Base
– is_man(X) → is_mortal(X) [universal quant. assumed]
– is_man(socrates)
• In Conjunctive Normal Form
– ¬is_man(X) ∨ mortal(X)
– is_man(socrates)
– ¬is_mortal(socrates) [negation of theorem]
www.sti-innsbruck.at
27
Reading off a Proof
Backtrack and then Read Forward
• You said that all men were mortal.
• That means that for all things X, either X is not a man, or X is mortal
[CNF step].
• If we assume that Socrates is not mortal, then, given your previous
statement, this means Socrates is not a man [first resolution step].
• But you said that Socrates is a man, which means that our
assumption was false [second resolution step], so Socrates must be
mortal.
www.sti-innsbruck.at
28
Alternative Search Tree
How do you read the
proof for this
search tree?
www.sti-innsbruck.at
29
Dealing with Equality
Approach 1: Add Knowledge
• Problem with equality:
– was_president(george_bush) and was_president(g_bush)
– will not unify (syntactically different constants)
• unification algorithm does not allow this unification
– Even if we add to the knowledge base:
• george_bush = g_bush
• One alternative: add extra knowledge to KB
– Axioms of equality (X=X, X=Y → Y=X, etc.)
– Equality statements for each predicate:
• X = Y → P(X) = P(Y)
– Must be done for all predicates
www.sti-innsbruck.at
30
Dealing with Equality
Approach 2: Add Demodulation rule
• Demodulation rule of inference
– Takes two input sentences, one expressing an equality
• That sentence X = sentence Y
– Finds a unification, mu, for X with a term, Z, in other clause
– Applies mu to Y (not X)
– Replaces occurrence of Z with Subst(mu, Y)
X=Y, (…Z…)
(…Subst(mu,Y)…)
www.sti-innsbruck.at
31
Heuristic Search Overview
• Pure Resolution Search tends to be slow
• For interesting problems
– Lots of clauses in the initial knowledge base
– Each step adds a new clause (which can be used)
– The search space gets too big
• We can choose any pair of clauses to try to resolve
• Heuristic type 1:
– Intelligently choose which pair to resolve at any time
• Heuristic type 2:
– Prune the space:
• Don’t allow resolution with certain clauses
www.sti-innsbruck.at
32
Unit Preference Strategy
• Greedy search
– Prefer to resolve certain clause types when possible
• Unit clauses:
– Contain only a single literal, e.g., C = is_pm(tony)
• Idea:
– We are looking for the smallest (empty) clause
– Resolving with the unit clause keeps clauses small
• Effectiveness
– Was very effective early on for simple problems
– Doesn’t reduce branching rate for medium problems
www.sti-innsbruck.at
33
Set of Support Strategy
• Maintain a set of (support) clauses, SOS
– Only allow resolution steps involving members of SOS
• Idea: choose clauses not in SOS to be consistent
– Hence a clause in SOS must eventually be resolved
• In order to find a path to the solution
• In practice:
– Initially choose the SOS to be the negated theorem
– Add any newly resolved clause to the SOS
– Otter theorem prover uses this strategy
www.sti-innsbruck.at
34
Input Resolution Strategy
• Special case of the SOS strategy
• Restrict the SOS to include
– Only the clauses in the initial knowledge base
• Clearly brings down the search space size
• However, it is not complete for first order logic
• But it is complete for
– Horn-clause knowledge bases
– such as Prolog programs
www.sti-innsbruck.at
35
Subsumption of Clauses
• One clause, C, subsumes clause D
– If D is more specific than C (or, C is more general)
• Naïve check for subsumption
– Find a unifying substitution
• allowing us to write D as a subset of the literals of C
• such that variables and constants in D become variables in C
• Example:
– p(george) ∨ q(X) is subsumed by p(A) ∨ q(B) ∨ r(C)
– Substitution: {george/A, X/B}
– Second clause is clearly more general
www.sti-innsbruck.at
36
Subsumption Strategy
• Whenever a new clause is found
– Check that there is no existing clause
• which subsumes the new clause
• Idea: removing more specific clauses
– Will not change the inconsistency in the database
• Because specific clauses can be inferred by the general ones
– Hence the theorem will still be provable
– But the search space will be reduced
• Have to be careful:
– Subsumption checking can be expensive
• must be outweighed by the reduction in search space
www.sti-innsbruck.at
37
Applications of Resolution
Algebraic Theorem Proving
• Bill McCune and Larry Wos
– Argonne National Laboratories
– Writing first order provers such as EQP & Otter
• Solution of the Robbins Problem (boolean algs)
– Stated over 60 years ago, mathematicians tried & failed
– EQP solved this in 8 days in 1996 (after much devel)
• Also nice: axiomatisations of algebras
– Attempt to find more succinct ways of describing algebras
– Use Otter to prove that the new way
• Is equivalent to the normal way of axiomatising algebras
www.sti-innsbruck.at
38
Applications
Automated Conjecture Making
• Automated Theory Formation (HR)
– Used in mathematical (and bioinformatics) domains
• Theories contain
– concepts, examples, conjectures, proofs
• HR uses Otter to prove its theorems
– Effective in algebraic domains
– See notes for anti-associative algebra results
• In number theory
– Otter is used as a filter (discard theorems it can prove)
– Example conjectures made by HR (and proved by me):
• Sum of divisors is prime → number of divisors is prime
• Sum of divisors of a square is an odd number
• Perfect numbers are pernicious [and many more…..]
www.sti-innsbruck.at
39
Other Topics in Automated Reasoning:
Interactive Proving
• Interactive theorem proving
– Necessary to interact with humans in order to prove theorems of
any difficulty
• Two (of many) approaches:
– Let a theorem prover do simple tasks while you develop a theory
(e.g., Buchberger’s Theorema)
– Allow user to follow a proof attempt and step in to guide the
prover
• Needs visualisation tools to draw and annotate proof trees
www.sti-innsbruck.at
40
Other Topics
Higher Order Theorem Proving
• Exactly what you would expect
– Expressing theorems in higher order logic
• See lecture 4
– And proving them (possibly interactively)
• HOL theorem prover
– Larry Paulson’s group in cambridge
– Has been used for verification tasks
• type safety for Java
• verification of crytographic protocols
www.sti-innsbruck.at
41
Other Topics
Databases and Competitions
• TPTP library by Geoff Sutcliffe & Christian Suttner
– Thousands of problems for theorem provers
– Used to benchmark first order theorem provers
– Contains 6973 theorems at present
– HR is only non-human to add to this library
• CASC competition by Sutcliffe et al.
– Every year: who has the fastest/most accurate first order
theorem prover on the planet?
– Uses blind test from the TPTP library
– Current chamption: Vampire
• By Voronkov and Riazonov in Manchester
www.sti-innsbruck.at
42
Bibliography
•
•
•
•
Model Checking and Theorem Proving: a Unified Framework, Thesis by
Sergey Berezin, http://reportsarchive.adm.cs.cmu.edu/anon/2002/CMU-CS-02-100.pdf.
A brief history of model checking, Talk by Ken McMillan,
http://www.cs.uiowa.edu/~tinelli/classes/196/Spring07/notes/McMillan.p
df.
Artificial Intelligence, Course by Jeremy Gow,
http://www.doc.ic.ac.uk/~sgc/teaching/v231/.
Introduction to Model Checking, Course by René Thiemann, http://clinformatik.uibk.ac.at/teaching/ws07/imc/schedule.php .
www.sti-innsbruck.at
43