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