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 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.
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)!