Lines Matching defs:is
16 which is easy to get wrong and harder to prove theorems about, even if
20 discussions with Ernie Cohen. The idea is to define the semantics of LTL with
28 The current book is produced to prove compositional reductions for
29 model-checking. The goal is to verify that the composition reductions are
33 that are required to verify the reductions. The point in the case is that if
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
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
94 ;; Now we show the obvious thing that a restricted formula is also an ltl
97 (defthm restricted-formula-is-an-ltl-formula
102 ;; Given an LTL formula, can we create a v-list such that the LTL-formula is a
131 (defthm ltl-formula-is-a-restricted-formula
147 ;; Here are the accessors and updaters as macros. A Kripke structure is a
156 ;; A periodic path is a record of initial-state, (finite) prefix, and (finite)
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
165 ;; reason for this choice is that I think the stronger requirements of "without