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

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 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,
AG (a -> AX (b -> AX (c -> AX d))))
becomes
{a ; b ; c ; !d} (false)
Perhaps the Wolper paper is clearer, perhaps not. Two reasons why it may not be clearer are:
1. it describes a Büchi automaton construction (automata on infinite words) rather than NFA (non-deterministic finite automata on finite words) construction;
2. it tackes all of LTL, rather than just safety properties of a certain syntactic form.
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:

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

• N denotes the set of natural numbers {0,1,2,...}
• 2^P is the powerset of P (i.e. set of all subsets of 2^P).
• x in X means x is a member of set X.
• x,y,z,... in X means x in X and y in X and z in X etc.
• (x1,x2,...xn) in X means the n-tuple (x1,x2,...,xn) is in X.
• X will be identified with it's characteristic function, so x in X iff X(x).
• X <= Y means set X is included in set Y.
• X U Y denotes the usual set union of sets X and Y.
• X + Y denotes the disjoint union of sets X and Y.
• X x Y denotes the Cartesian product of sets X and Y.
• w^i is the ith element of w counting from 0 (so w^0 is the first element).
• w1.w2 denotes the concatenation of w1 and w2.
• |w| denotes the length of w, which may be finite or infinite.
• p occurs_in w means there is an i such that p in w^i.

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

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

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))
```
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:
S is the cross product of the states of M with the states of A. That is, the set of states (s,t) such that s is a state in M and t a state in A. So is the set of states (s,t) such that s is in the initial states of M and t is in the initial states of A. R((s,t),(s',t')) iff (s,s') is in the relation of M, and (t,a,t') is in the relation of A, where a is the labeling of s. P are the propositions of M and L(s,t) = L(s).
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