Comments and questions are in red and highlighted like this.
The notation |- f means f is a theorem in HOL. Such theorems can either be deduced from the axioms of higher order logic by applying rules of inference, or they can be created by external oracles. Theorems created by oracles are marked, and the marks propagated by deduction, so one can know if a theorem depends on results created by oracles.
where w || A2 is the model resulting from taking the product of the model resulting from w with the automaton A2. Note that we do not have to represent the model M, which may be enormous, inside HOL.
|- forall w: (w |=ltl f) <=> (w || A2 |=ltl always b2) |- MO || A1 || A2 |= ctl always(b1 <-> b2)
The following overview is based on email from Cindy Eisner.
The idea behind the Beer paper is to consider only CTL formulas in the Common
Fragment of CTL and LTL (actually, they look at a subset of these
properties - that paper predates the Common Fragment characterization
of Maidl).
Since these formulas have linear counter-examples, construct a regular
expression that describes those counterexamples, and turn it into a
suffix implication in PSL. For instance,
Note: it is likely that
Büchi automata, created as described in the Wolper tutorial for safety
formulas, can easily converted into finite automata.
The goal is to write a HOL proof script to compute from f a theorem:
Suppose we are given two theorems:
|- forall w: (w |=ltl f) <=> (w || A2 |=ltl always b2) [1] |- MO || A1 || A2 |= ctl always(b1 <-> b2) [2]
The goal is to deduce from [1] and [2] that
Step 1.
Since always(b1 <-> b2)
is in the Common Fragment, from [2] one can deduce:
|- forall pi: pi a computation of (MO || A1 || A2)
==>
Lhat(pi) |=ltl always(b1 <-> b2) [2.2]
where Lhat is the extension of L from states to paths (i.e. Lhat(s0.s1.s2...) = L(s0).L(s1).L(s2)...). See B.2.2 of the PSL 1.1 LRM.
This step has been validated in HOL by proving for arbitrary model M and boolean expression b that:
|- M |=ltl G b <=> M |=ctl AG b |- M |=ltl G b! <=> M |=ctl AG b!
Step 2.
We next (somehow) deduce from [2.2] that
|- forall pi: pi a computation of MO
==>
Lhat(pi) || A1 || A2 |=ltl always(b1 <-> b2) [2.3]
Step 3.
As M0 is the open model, all words w correspond to computations,
and hence it should follow that:
Step 4.
It then follows from [2.4] that:
Step 5.
Under suitable (to be determined) assumptions,
which may involve A1
and A2 not interacting, and maybe also
b1 not containing
variables of A2 and
b2 not containing
variables of A1, we would hope to deduce
from [3] that:
Now, since always b2 lies in the Common Fragment, it follows from [4] that:
Step 6.
From [6] it follows that:
This step has been partially validated in HOL by proving that if M is a model and A is a total automaton, then:
|- (forall w: w |=ltl f <=> w || A |=ctl always b) ==> (M |=ltl f <=> M || A |=ctl always b)
Cindy Eisner proposed the totality restriction on A when I got stuck, and she and Dana Fisman gave suggestions that helped me complete the proof.
The predicate Model is true of a five tuple iff it is a Model.
Model(S,So,R,P,L) <=> So <= S and (R <= S x S) and (forall s: s in S ==> L(s) <= P)
SimpleModel B R = (S, B, R, 2^S, lambda s {p | s in p})
Paths and computations pi are defined with respect to models.
pi in (Path (S,So,R,P,L) s) <=> |pi| > 0 and s = pi^0 and s in S and (forall i: i < |pi|-1 ==> pi^i,pi^(i+1) in S and (pi^i,pi^(i+1)) in R) and (forall s: |pi| finite ==> not(pi^(|pi|-1),s) in R)) pi in Computation(S,So,R,P,L) <=> exists s: s in So and pi in (Path (S,So,R,P,L) s)
M |=ltl f <=> forall pi: pi in Computation M ==> Lhat(pi) |=ltl f
CTL (PSL OBE) state formulas f are evaluated with respect to a model M and state s by defining M,s |=ctl f (see LRM B.2 2). A formula is true in a model iff it is true in all initial states of the model.
M |=ctl f <=> forall s: s in M.So ==> M,s |=ctl f
The PSL to CTL tool does not produce a satellite as a model (Kripke structure), but as an automaton. An automaton is defined in Clarke, Grumberg and Peled's book "Model Checking" to be a five tuple (Sigma,Q,Delta,Qo,F) where Sigma is the alphabet, Q the set of states, Delta the transition relation, which is is subset of Q x Sigma x Q, Qo the set of initial states (included in Q) and F the set of final state (included in Q).
The predicate Automaton is true of a five tuple iff it is an automaton.
Automaton(Sigma,Q,Delta,Qo,F) <=> Qo <= Q and Delta <= (Q x Sigma x Q) and F <= Q
The particular automata we shall use have alphabets consisting in sets of atomic propositions. We call these "propositional automata". All automata are assumed propositional, so A.Sigma will be a set of atomic propositions.
The language Language(A) accepted by an automaton A is defined by:
w in (Language(Sigma,Q,Delta,Qo,F)) <=> |w| > 0 and w^0 in Qo and (forall i: i < |w|-1 ==> exists a: (w^i, a, w^(i+1)) in Delta) and (|w| finite ==> forall a s: not(w^(|w|-1), a, s) in Delta))
ModelToAutomaton(S,So,R,P,L) = (2^P, S + {iota}, {(s,a,s') | R(s,s') and a = L(s')} U {(iota,a,s) | s in So and a = L(s)}, {iota}, S + {iota}, )
Some commentary from Cindy (edited by Mike):
A Büchi automaton looks exactly like a finite automaton, except
that instead of final states, the set F is
interpreted as accepting states, and a run is accepted iff some
accepting state appears infinitely often in the infinite word being
examined.
The point is that translating the Kripke structure into an
automaton, as they are doing in section 9.2, is for the purpose of
creating the cross-product of the automaton for the model and the
automaton for the formula being checked. You want words to be
rejected by the resulting automaton because of the automaton of the
formula, not the automaton of the Kripke structure, therefore, you
make all states in the automaton of the Kripke structure accepting
states.
In a Kripke structure, the transition relation is total, there there
is no state with no successor. The point is that they are
transforming a Kripke structure into a Büchi automaton (which is
used to describe languages over infinite words, that is, omega-regular
languages).
It follows easily that
|- Model(M) ==> Automaton(ModelToAutomaton(M))
|- Model(M) /\ w^0 in M.So ==> (w in (Path M w^0) <=> (iota.w) in (Language(ModelToAutomaton(M))))
(S1,So1,R1,P1,L1) || (S2,So2,R2,P2,L2) = (S1 x S2, -- Cartesian product So1 x So2, -- Cartesian product {((s1,s2),(s1',s2')) | R1(s1,s1') and R2(s2,s2'}, P1 + P2 -- disjoint union lambda (s1,s2) {p in (P1 + P2) | if (p in P1) then (p in L1 s1) else (p in L2 s2)} )
|- Model(M1) and Model(M2) ==> Model(M1 || M2)
(S,So,R,P,L) || (Sigma,Q,Delta,Qo,F) = (S x Q, So x Qo, {((s,t),(s',t')) | R(s,s') and Delta(t,L(s),t')}, P, lambda (s,t) L(s) )
|- Automaton(A) and Model(M) ==> Model(A || M)
(Sigma,Q1,Delta1,Qo1,F1) || (Sigma,Q2,Delta2,Qo2,F2) = (Sigma, Q1 x Q2, {((q1,q2), a, (q1',q2') | (q1, a, q1') in Delta1 and (q2, a, q2') in Delta2}, Qo1 x Qo2, F1 x F2 )
|- Automaton(A1) and Automaton(A2) ==> Automaton(A1 || A2)
Intuitively, the model resulting from a sequence of states w = s0 s1 s2 s3 ... is considered as a 'linear deterministic' behaviour
|----| |----| |----| |----| | s0 |--->| s1 |--->| s2 |--->| s3 |---> ... |----| |----| |----| |----|
PathToModel(w) = ({i | i < |w|}, -- states are natural numbers {0}, -- initial state is 0 {(i,i') | i,i' < |w| and i' = i + 1}, -- successor of a state is successor as a number {p | p occurs_in w}, -- the set of propositions occurring in the path lambda i {p | w^i |= p} )
|- 0 < |w| ==> Model(PathToModel(w))
With the definitions above, converting a path w first to a model and then to an automaton results in:
ModelToAutomaton(PathToModel(w)) = (2^{p | p occurs_in w}, {i | i < |w|} U {iota}, {(i,a,i') | i' = i+1 and i' < |w| and a = {p | p occurs_in w and w^(i') |= p}} U {(iota,a,0) | a = {p | p occurs_in w and w^0 |= p}}, {iota}, {i | i < |w|} U {iota},) )
PathToModel(w) || (S,So,R,P,L) = ({(i,s) | i < |w| and s in S}, {(i,s) | i = 0 and s in So}, {((i,s),(i',s')) | i' = i+1 and i' < |w| and (s,s') in R}, {p | p occurs_in w} U P, lambda(i,s) {p | if p occurs_in w then i < |w| and w^i |= p else p in L s} )
PathToModel(w) || (Sigma,Q,Delta,Qo,F) = ({(i,s) | i < |w| and s in Q}, {(i,s) | (i = 0) and s in Qo}, {((i,s),(i+1,s')) | i+1 < |w| and (s, {p | i < |w| and p occurs_in w and w^i |= p}, s') in delta}, {p | p occurs_in w}, lambda (i,s) {p | i < |w| and p occurs_in w and w^i |= p} )
ModelToAutomaton(PathToModel(w) || (S,So,R,P,L)) = (2^({p | p occurs in w} + P), {(i,s) | i < |w| and s in S} U {iota}, {((i,s),a,(i+1,s')) | i+1 < |w| and R(s,s') and a = {p | if p occurs_in w then i+1 < |w| and w^(i+1) |= p else p in L(s')}} U {(iota,a,(0,s)) | s in So and a = {p | if p occurs_in w then 0 < |w| and w^0 |= p else p in L(s)}}, {iota}, {(i,s) | i < |w| and s in S} U {iota}, )
ModelToAutomaton(PathToModel(w) || (Sigma,Q,Delta,Qo,F)) = (2^{p | p occurs in w}, {(i,s) | i < |w| and s in Q} U {iota}, {((i,s),a,(i+1,s')) | i+1 < |w| and (s, {p | p occurs_in w and w^i |= p}, s') in delta} U {(iota,a,(0,s)) | s in Qo and a = {p | 0 < |w| and p occurs_in w and w^0 |= p}} {iota}, {(i,s) | i < |w| and s in Q} U {iota} )
MO(Q,P) || (2^P,Q,Delta,Qo,F) = (2^P x Q, 2^P x Qo, {((s,t),(s',t')) | s,t,s',t' in 2^P and (t,s,t') in Delta}, P, lambda (s,t) s)
The examples below were quite tricky to manually convert to the form shown from the HOL system output. It is likely that I have made mistakes in both the HOL source and the conversion (several in both have already been spotted and fixed)!