1(in-package "ACL2")
2
3;; The following two lines are added for portability to v2-7....
4
5
6#|
7
8  ltl.lisp
9  ~~~~~~~~
10
11In this book, we discuss the syntax of LTL formula and its semantics with
12respect to a Kripke Structure. The standard semantics of LTL involve operations
13with respect to an inifinitary object, namely the path. However, ACL2 does not
14allow such objects. Thus, we need to define the semantics of LTL with respect
15to a Kripke Structure directly. However, this requires a tableau construction
16which is easy to get wrong and harder to prove theorems about, even if
17specified correctly.
18
19We have chosen to take a middle ground based on (John Matthews's)
20discussions with Ernie Cohen. The idea is to define the semantics of LTL with
21respect to eventually periodic paths. (We defer the proof now that any
22verification of semantics over eventually periodic paths corresponds to a
23verification over infinite paths and this might not be possible to do in
24ACL2.) However, for the moment the semantics are with respect to eventually
25periodic paths and the semantics for a Kripke Structure are given by
26quantifying over all compatible paths.
27
28The current book is produced to prove compositional reductions for
29model-checking. The goal is to verify that the composition reductions are
30correct given that the underlying model-checking routines are correct. Given
31this assumption, we take further liberties and encapsulate the ltl semantics
32over periodic paths as an underlying model-checking routine, exporting theorems
33that are required to verify the reductions. The point in the case is that if
34for a real LTL semantics function these constraints are not satisfied for
35periodic paths, then the functions (and not the theorems) need to be changed,
36making encapsulate a viable option in order to not get bogged down in
37implementation of a model-checking routine for ltl.
38
39Questions and comments are welcome. -- Sandip.
40
41|#
42
43(set-match-free-default :once)
44
45(include-book "sets")
46
47
48
49
50;; We now define the syntax of an LTL formula. For purpose of reductions, we
51;; also define a restricted formula over a subset of variables.
52
53(defun ltl-constantp (f)
54  (or (equal f 'true)
55      (equal f 'false)))
56
57(defun ltl-variablep (f)
58  (and (symbolp f)
59       (not (memberp f '(+ & U W X F G)))))
60
61;; So an LTL formula is either (i) a constant 'True or 'False, (ii) a variable
62;; which is a quote or a symbol other than the LTL operator symbol, or of the
63;; form (P + Q), (P & Q), (P U Q), (P W Q), (~ P), (F P), (G P), (X P), where P
64;; and Q are LTL formulas.
65
66
67(defun ltl-formulap (f)
68  (cond ((atom f) (or (ltl-constantp f)
69                      (ltl-variablep f)))
70        ((equal (len f) 3)
71         (and (memberp (second f) '(+ & U W))
72              (ltl-formulap (first f))
73              (ltl-formulap (third f))))
74        ((equal (len f) 2)
75         (and (memberp (first f) '(~ X F G))
76              (ltl-formulap (second f))))
77        (t nil)))
78
79;; A formula is called resctricted with respect to a collection vars of
80;; variables if it mentions no variable other than those in vars. Here is the
81;; recursive definition.
82
83(defun restricted-formulap (f v-list)
84  (cond ((atom f) (or (ltl-constantp f)
85                      (and (ltl-variablep f)
86                           (memberp f v-list))))
87        ((equal (len f) 3) (and (memberp (second f) '(& + U W))
88                                (restricted-formulap (first f) v-list)
89                                (restricted-formulap (third f) v-list)))
90        ((equal (len f) 2) (and (memberp (first f) '(~ X F G))
91                                (restricted-formulap (second f) v-list)))
92        (t nil)))
93
94;; Now we show the obvious thing that a restricted formula is also an ltl
95;; formula.
96
97(defthm restricted-formula-is-an-ltl-formula
98  (implies (restricted-formulap f v-list)
99           (ltl-formulap f))
100  :rule-classes :forward-chaining)
101
102;; Given an LTL formula, can we create a v-list such that the LTL-formula is a
103;; restricted formula over the variables in v-list? The function
104;; create-restricted-var-set attempts that.
105
106(defun create-restricted-var-set (f)
107  (cond ((atom f) (if (ltl-constantp f) nil (list f)))
108        ((equal (len f) 3) (set-union (create-restricted-var-set (first f))
109                                      (create-restricted-var-set (third f))))
110        ((equal (len f) 2) (create-restricted-var-set (second f)))
111        (t nil)))
112
113;; And show that we have been successful
114
115(local
116(defthm restricted-formulap-append-reduction
117  (implies (restricted-formulap f vars)
118           (restricted-formulap f (set-union vars vars-prime)))
119  :hints (("Goal"
120           :in-theory (enable set-union))))
121)
122
123(local
124(defthm restricted-formulap-append-reduction-2
125  (implies (restricted-formulap f vars)
126           (restricted-formulap f (set-union vars-prime vars)))
127  :hints (("Goal"
128           :in-theory (enable set-union))))
129)
130
131(defthm ltl-formula-is-a-restricted-formula
132  (implies (ltl-formulap f)
133           (restricted-formulap f (create-restricted-var-set f)))
134  :rule-classes :forward-chaining)
135
136;; OK, so we are done with syntax of LTL for mow. We will revisit this section
137;; and add different restricted models when we do proofs of different
138;; reductions.
139
140;; We turn our attention to models.
141
142;; First this handy collection of functions that might help us.
143;; NOTE TO MYSELF: I should write some utilities in ACL2 that will allow me to
144;; load the accessor and updater macros easily. I will have to think about it
145;; at aome point.
146
147;; Here are the accessors and updaters as macros. A Kripke structure is a
148;; record of states, initial-states, transition and label-fn.
149
150(defmacro initial-states (m) `(<- ,m :initial-states))
151(defmacro transition     (m) `(<- ,m :transition))
152(defmacro label-fn       (m) `(<- ,m :label-fn))
153(defmacro states         (m) `(<- ,m :states))
154(defmacro variables      (m) `(<- ,m :variables))
155
156;; A periodic path is a record of initial-state, (finite) prefix, and (finite)
157;; cycle.
158
159;; NOTE TO MYSELF: The initial state might not be required. It is difficult to
160;; estimate what is considered standard for Kripke structures. I have heard
161;; Professor Emerson talk about Kripke Structures with initial states and
162;; Kripke Structures without initial states (and so in Dr. Clarke's Book). I
163;; follow the "with initial states" in that jargon, though I do believe that we
164;; can modify the theorems for Kripke Structures "without initial states". The
165;; reason for this choice is that I think the stronger requirements of "without
166;; initial states" should not bother us at this time.
167
168(defmacro initial-state  (p) `(<- ,p :initial-state))
169(defmacro cycle          (p) `(<- ,p :cycle))
170(defmacro prefix         (p) `(<- ,p :prefix))
171
172(defmacro >_ (&rest upds) `(update nil ,@upds))
173
174(defun next-statep (p q m)
175  (memberp q (<- (transition m) p)))
176
177(defun initial-statep (p m)
178  (memberp p (initial-states m)))
179
180(defun label-of (s m)
181  (<- (label-fn m) s))
182
183(in-theory (disable next-statep initial-statep label-of))
184
185;; The predicate modelp here precisely describes what we expect a Kripke
186;; Structure to look like.
187
188(defun next-states-in-states (m states)
189  (if (endp states) T
190    (and (subset (<- (transition m) (first states))
191                 (states m))
192         (next-states-in-states m (rest states)))))
193
194(defthm next-states-in-states-clarified-aux
195  (implies (and (memberp p states)
196                (next-states-in-states m states)
197                (next-statep p q m))
198           (memberp q (states m)))
199  :hints (("Goal"
200           :in-theory (enable next-statep))))
201
202(defthm next-states-in-states-clarified
203  (implies (and (next-states-in-states m (states m))
204                (memberp p (states m))
205                (next-statep p q m))
206           (memberp q (states m))))
207
208(in-theory (disable next-states-in-states-clarified-aux
209                    next-states-in-states))
210
211