Notes on using HOL to validate translation of PSL/FL to CTL


Contents Significant new or revised material is highlighted like this.

Comments and questions are in red and highlighted like this.


 

Goal

To help validate conformance to the PSL 1.1 semantics of a tool that converts a PSL checking problem for formulas in the LTL Foundation Language (FL)
M |=ltl f
(where f lies in a subset of FL) into a CTL checking problem
M || A1 |=ctl always b1
where satellite automaton A1 and boolean expression b1 (which only involves the state variables of M and A1) are generated by the tool from f. The model M || A1 is defined below.

Method

We give a high level overview followed by more details.

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.

Overview

The method of validating the PSL-to-CTL tool using HOL is as follows.
  1. The tool is applied to a model M and a PSL formula f to compute an automaton A1 and boolean expression b1.

  2. A HOL proof script is applied to f to compute an automaton A2, boolean expression b2 and theorem
    |- forall w: (w |=ltl f) <=> (w || A2 |=ltl always b2)

    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.

  3. A CTL model checker, like the one in RuleBase, is invoked to verify
    MO || A1 || A2 |= ctl always(b1 <-> b2)
    where MO is the open model over the propositions that occur in the labels of the transitions in A1 and A2.

  4. The model checked theorem is then imported into HOL using its oracle mechanism, so we have two theorems
    |- forall w:  (w |=ltl f) <=>  (w || A2 |=ltl always b2)
    
    |- MO || A1 || A2 |= ctl always(b1 <-> b2)  
    
    A proof script then deduces from these a further HOL theorem that validates the run of the tool on M and f:
    |- (M |=ltl f)  <=>  (M || A1 |=ctl always b1)
The main HOL work is 2 and 4 above, which are discussed further in the following two sections.

Computing automata

The derivation of A2 and b2 is expected to be achieved using ideas from On-The-Fly Model Checking of RCTL Formulas (Beer et al) together with standard methods for Constructing Automata from Temporal Logic Formulas (Wolper). The most relevant HOL work is the CHARME2003 paper, but it is unclear how useful the ideas in this will be.

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:

|- forall w: (w |=ltl f) <=> (w || A2 |=ltl always b2)

Checking tool runs

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]
where [1] is generated by a HOL script and [2] is generated by a model checker oracle and imported into HOL, and MO is the open model over the propositions used in A1 and A2.

The goal is to deduce from [1] and [2] that

|- (M |=ltl f)  <=>  (M || A1 |=ctl always b1)
This deduction consists in a number of steps.

Step 1.
Since always(b1 <-> b2) is in the Common Fragment, from [2] one can deduce:

|- MO || A1 || A2 |=ltl always(b1 <-> b2) [2.1]
which means:
|- 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:

|- forall w: w || A1 || A2 |=ltl always(b1 <-> b2)
and then since always(b1 <-> b2) is in the Common Fragment:
|- forall w: w || A1 || A2 |=ctl always(b1 <-> b2) [2.4]

Step 4.
It then follows from [2.4] that:

|- forall w: w || A1 || A2 |=ctl always b1 <-> always b2 [3]
This step has been validated in HOL by proving for arbitrary model M and boolean expressions b1, b2 that M |=ctl AG(b1 <-> b2) implies M |=ctl (AG b1 <-> AG b2).

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:

|- forall w: (w || A1 |=ctl always b1) <=> (w || A2 |=ctl always b2) [4]

Now, since always b2 lies in the Common Fragment, it follows from [4] that:

|- forall w: (w || A1 |=ctl always b1) <=> (w || A2 |=ltl always b2) [5]
and hence from [5] and [1] we get:
|- forall w: (w || A1 |=ctl always b1) <=> (w |=ltl f) [6]

Step 6.
From [6] it follows that:

|- (M |=ltl f)  <=>  (M || A1 |=ctl always b1)
which establishes the correctness of A1 and b1 computed from f by the tool.

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)
It remains to show that we can assume A1 is total without loss of generality.

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.

Evolving details of HOL formalisation

Notation

Models (Kripke structures)

Models are defined in B.2.2 of the PSL 1.1 LRM (they are also called Kripke structures in the literature). A model is a five tuple (S,So,R,P,L), where S is the set of states, So the set of initial states (included in S), R the transition relation, a subset of S x S, P is a non-empty set of atomic propositions and L:S->2^P is a valuation function that maps a state s to the set L(s) of atomic propositions true at s. If M is a model, then the set of states, initial state, transition relation, set of atomic propositions and valuation function are denoted by M.S, M.So, M.R, M.P and M.L, respectively.

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)
Given a set of states S, a common special case is a model in which propositions are taken to be sets of states. Suppose B <= S and R <= S x S, then
SimpleModel B R = (S, B, R, 2^S, lambda s {p | s in p})
It follows that |- Model(SimpleModel B R).

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) 
LTL (PSL FL) path formulas f are evaluated with respect to computations.
M |=ltl f  <=>  forall pi: pi in Computation M ==> Lhat(pi) |=ltl f
where Lhat maps L over a path (see B.2.2 of the PSL 1.1 LRM).

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

Open models

The open model over a set of states S and a set of atomic propositions P is denoted by MO(P) and defined by:
MO(P) = (2^P, 2^P, 2^P x 2^P, P, lambda s {p | p in s})

Automata

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
If A is an automaton then the alphabet, set of states, transition relation, initial states and final states are denoted by A.Sigma, A.Q, A.Delta, A.Qo and A.F, respectively.

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

Converting models to automata

In Section 9.2 of Clarke, Grumberg and Peled's book there is a method of transforming a model into an automaton:
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},
)
Here iota is just an arbitrary element not in the set of states (in HOL I have used an option type).

Some commentary from Cindy (edited by Mike):

It follows easily that

|- Model(M) ==> Automaton(ModelToAutomaton(M))
and rather less easily that
|- Model(M) /\ w^0 in M.So
   ==>
   (w in (Path M w^0) <=> (iota.w) in (Language(ModelToAutomaton(M))))
The proof in HOL is very tedious for finite paths, though completely straightforward.

Product of two models

It is not clear whether we will need to take the product of Kripke structures (models), but I have made a guess at a definition: the product M1 || M2 of models M1 = (S1,So1,R1,P1,L1) and M1 = (S2,So2,R2,P2,L2) is defined by:
(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)} 
)
It follows that
|- Model(M1) and Model(M2) ==> Model(M1 || M2)

Product of a model with an automaton

For our project we should directly convert the Kripke structure we have (call it M) plus the automaton we have (call it A) into a new Kripke structure as follows: Thus:
(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)
)
It follows that
|- Automaton(A) and Model(M) ==> Model(A || M)
An automaton created from a formula will have states with names and the letters from 2^P will label the transitions.

Product of two automata

For our application we can assume both automata have the same alphabet, hence we define:
(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
)
It follows that
|- Automaton(A1) and Automaton(A2) ==> Automaton(A1 || A2)

Converting paths to models

A path, with respect to a model M = (S,So,R,P,L), is a (finite or infinite) sequence of letters, where a letter is TOP, BOTTOM or a subset of the set of propositions P of the model.

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 |---> ...
|----|    |----|    |----|    |----|
The model representing this is defined as follows. Let l |= p mean that proposition p (where p in P) is true with respect to letter l as follows: TOP |= p is always true, BOTTOM |= p is always false, and s |= p is true, where s in 2^P (i.e. s is a set of propositions), iff p in s. The model PathToModel(w) corresponding to a path w is defined by:
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} 
) 
It follows that
|- 0 < |w| ==> Model(PathToModel(w))

Sanity checking examples

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

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},)
)
and PathToModel(w) || (S,So,R,P,L) evaluates to the model:
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}
)
and PathToModel(w) || (Sigma,Q,Delta,Qo,F) evaluates to the model:
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}
)
If we convert w to a model, then take the product with model (S,So,R,P,L) and then convert the resulting product model to an automaton, we get:
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},
)
If we convert w to a model, then take the product with the automaton (Sigma,Q,Delta,Qo,F) and then convert the resulting product model to an automaton, we get:
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}
)
With the definition of an open model above and if Automaton(2^P,Q,Delta,Qo,F) then we have
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 next sanity check will be to take the product of the Kripke structure of the open model MO with an automaton A, convert the result to an automaton, then check that the language of the automaton we started with is the language of the automaton we end up with.


Page maintained by Mike Gordon with major contributions of content from Cindy Eisner.
Version 1.22, Tue Jan 4 2005