;; These functions are used in the compositional model-checking work to prove
;; compositional reductions. These are only for reference purposes and might
;; sometimes be simplified, but the essence of each function is in here.
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+++++++++++++++ Properties of ltl syntax ++++++++++++++++++++++++++++++++++++++
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
;; So an LTL formula is either (i) a constant 'True or 'False, (ii) a variable
;; which is a quote or a symbol other than the LTL operator symbol, or of the
;; form (P + Q), (P & Q), (P U Q), (P W Q), (~ P), (F P), (G P), (X P), where P
;; and Q are LTL formulas.
(defun ltl-formulap (f)
(cond ((atom f) (or (ltl-constantp f)
(ltl-variablep f)))
((equal (len f) 3)
(and (memberp (second f) '(+ & U W))
(ltl-formulap (first f))
(ltl-formulap (third f))))
((equal (len f) 2)
(and (memberp (first f) '(~ X F G))
(ltl-formulap (second f))))
(t nil)))
;; A formula is called resctricted with respect to a collection vars of
;; variables if it mentions no variable other than those in vars. Here is the
;; recursive definition.
(defun restricted-formulap (f v-list)
(cond ((atom f) (or (ltl-constantp f)
(and (ltl-variablep f)
(memberp f v-list))))
((equal (len f) 3) (and (memberp (second f) '(& + U W))
(restricted-formulap (first f) v-list)
(restricted-formulap (third f) v-list)))
((equal (len f) 2) (and (memberp (first f) '(~ X F G))
(restricted-formulap (second f) v-list)))
(t nil)))))
;; Now we show the obvious thing that a restricted formula is also an ltl
;; formula.
(defthm restricted-formula-is-an-ltl-formula
(implies (restricted-formulap f v-list)
(ltl-formulap f))
:rule-classes :forward-chaining)
;; Given an LTL formula, can we create a v-list such that the LTL-formula is a
;; restricted formula over the variables in v-list? The function
;; create-restricted-var-set attempts that.
(defun create-restricted-var-set (f)
(cond ((atom f) (if (ltl-constantp f) nil (list f)))
((equal (len f) 3) (set-union (create-restricted-var-set (first f))
(create-restricted-var-set (third f))))
((equal (len f) 2) (create-restricted-var-set (second f)))
(t nil)))
;; And show that we have been successful
(defthm ltl-formula-is-a-restricted-formula
(implies (ltl-formulap f)
(restricted-formulap f (create-restricted-var-set f)))
:rule-classes :forward-chaining)
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+++++++++++++ The LTL semantics function ++++++++++++++++++++++++++++++++++
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
(mutual-recursion
(defun ltl-periodic-path-semantics (f init prefix cycle label)
(cond ((atom f)
(if (ltl-constantp f)
(equal f 'true)
(memberp f (<- label init))))
((equal (len f) 3)
(case (second f)
(& (and (ltl-periodic-path-semantics (first f) init prefix cycle
label)
(ltl-periodic-path-semantics (third f) init prefix cycle
label)))
(+ (or (ltl-periodic-path-semantics (first f) init prefix cycle
label)
(ltl-periodic-path-semantics (third f) init prefix cycle
label)))
(U (let* ((found-and-index
(find-state-satisfying-formula
(third f) init prefix cycle label
(+ 1 (len prefix) (len cycle))))
(found (first found-and-index))
(index (second found-and-index)))
(if (not found)
nil
(ltl-periodic-path-semantics* (first f) init prefix
cycle label index))))
(W (let* ((found-and-index
(find-state-satisfying-formula
(third f) init prefix cycle label
(+ 1 (len prefix) (len cycle))))
(found (first found-and-index))
(index (second found-and-index)))
(if (not found)
(ltl-periodic-path-semantics* (first f) init prefix
cycle label
(+ 1 (len prefix) (len cycle)))
(ltl-periodic-path-semantics* (first f) init prefix
cycle label index))))
(t nil)))
((equal (len f) 2)
(case (first f)
(~ (not (ltl-periodic-path-semantics (second f) init prefix cycle
label)))
(G (ltl-periodic-path-semantics* (second f) init prefix
cycle label
(+ 1 (len prefix) (len cycle))))
(F (let* ((found-and-index
(find-state-satisfying-formula
(second f) init prefix cycle label
(+ 1 (len prefix) (len cycle))))
(found (first found-and-index)))
(if found t nil)))
(X (ltl-periodic-path-semantics (second f) (first prefix)
(if (endp (rest prefix))
cycle
(rest prefix))
cycle
label))
(t nil)))
(t nil)))
(defun ltl-periodic-path-semantics* (f init prefix cycle label dist)
(if (zp dist) t
(and (ltl-periodic-path-semantics f init prefix cycle label)
(ltl-periodic-path-semantics* f (first prefix)
(if (endp (rest prefix))
cycle
(rest prefix))
cycle label (1- dist)))))
(defun find-state-satisfying-formula (f init prefix cycle label dist)
(cond ((zp dist) (list nil 0))
((ltl-periodic-path-semantics f init prefix cycle label)
(list t 0))
(t (let* ((found-and-index
(find-state-satisfying-formula
f (first prefix)
(if (endp (rest prefix)) cycle (rest prefix))
cycle label (1- dist)))
(found (first found-and-index))
(ndx (second found-and-index)))
(list found (1+ ndx))))))
)
(defun ltl-ppath-semantics (f ppath m)
(ltl-periodic-path-semantics f (initial-state ppath)
(prefix ppath) (cycle ppath)
(label-fn m)))
(defun-sk ltl-semantics (f m)
(forall ppath
(implies (compatible-ppath-p ppath m)
(ltl-ppath-semantics f ppath m))))
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+++++++++++++++++ Bisimilarity Arguments +++++++++++++++++++++++++++++++
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
(encapsulate
(((bisimilar * * * * *) => *)
((bisimilar-transition-witness-m->n * * * * * *) => *)
((bisimilar-initial-state-witness-m->n * * * *) => *)
((bisimilar-transition-witness-n->m * * * * * *) => *)
((bisimilar-initial-state-witness-n->m * * * *) => *)
((bisimilar-equiv * * *) => *))
(local
(defun bisimilar (p m q n vars)
(declare (ignore vars))
(and (equal p q)
(equal m n)))
)
(local
(defun bisimilar-transition-witness-m->n (p r m q n vars)
(declare (ignore p m q n vars))
r)
)
(local
(defun bisimilar-initial-state-witness-m->n (s m n vars)
(declare (ignore m n vars))
s)
)
(local
(defun bisimilar-transition-witness-n->m (p m q r n vars)
(declare (ignore p m q n vars))
r)
)
(local
(defun bisimilar-initial-state-witness-n->m (m s n vars)
(declare (ignore m n vars))
s)
)
(local
(defun bisimilar-equiv (m n vars)
(declare (ignore vars))
(equal m n))
)
;; If two Kripke Structures m and n are equivalent with respect to a bisimilar
;; relation B, then for every initial-state of m there is a initial-state of n
;; that is bisimilar.
(defthm bisimilar-equiv-implies-init->init-m->n
(implies (and (bisimilar-equiv m n vars)
(memberp s (initial-states m)))
(memberp (bisimilar-initial-state-witness-m->n s m n vars)
(initial-states n))))
(defthm bisimilar-equiv-implies-bisimilar-initial-states-m->n
(implies (and (bisimilar-equiv m n vars)
(memberp s (initial-states m)))
(bisimilar s m
(bisimilar-initial-state-witness-m->n s m n vars)
n vars)))
;; And the same result holds for n to m
(defthm bisimilar-equiv-implies-init->init-n->m
(implies (and (bisimilar-equiv m n vars)
(memberp s (initial-states n)))
(memberp (bisimilar-initial-state-witness-n->m m s n vars)
(initial-states m))))
(defthm bisimilar-equiv-implies-bisimilar-initial-states-n->m
(implies (and (bisimilar-equiv m n vars)
(memberp s (initial-states n)))
(bisimilar (bisimilar-initial-state-witness-n->m m s n vars)
m s n vars)))
;; Bisimilar states have the same label with respect to vars. I just use
;; set-equality because they might not have "equal" labels. BTW, I might not
;; need the modelp hypothesis here. But I plug it in, just so that I can keep
;; the (functional instance of) bisimilarity relation as simple as possible.
(defthm bisimilar-states-have-labels-equal
(implies (and (bisimilar p m q n vars)
(modelp m)
(modelp n))
(set-equal (set-intersect (label-of p m) vars)
(set-intersect (label-of q n) vars))))
;; Of course bisimilarity witness is a member of states of the corresponding model.
(defthm bisimilar-witness-member-of-states-m->n
(implies (and (bisimilar p m q n vars)
(next-statep p r m)
(memberp r (states m)))
(memberp (bisimilar-transition-witness-m->n p r m q n vars)
(states n))))
;; Again this part may not be required.
(defthm bisimilar-witness-member-of-states-n->m
(implies (and (bisimilar p m q n vars)
(next-statep q r n)
(memberp r (states n)))
(memberp (bisimilar-transition-witness-n->m p m q r n vars)
(states m))))
;; And if two states are bisimilar, then for every next state of one, there is
;; a next state of another which is bisimilar.
(defthm bisimilar-witness-matches-transition-m->n
(implies (and (bisimilar p m q n vars)
(next-statep p r m))
(next-statep q (bisimilar-transition-witness-m->n p r m q n vars)
n)))
(defthm bisimilar-witness-produces-bisimilar-states-m->n
(implies (and (bisimilar p m q n vars)
(next-statep p r m))
(bisimilar r m
(bisimilar-transition-witness-m->n p r m q n vars)
n vars)))
;; Again this part may not be required.
(defthm bisimilar-witness-matches-transition-n->m
(implies (and (bisimilar p m q n vars)
(next-statep q r n))
(next-statep p (bisimilar-transition-witness-n->m p m q r n vars)
m)))
(defthm bisimilar-witness-produces-bisimilar-states-n->m
(implies (and (bisimilar p m q n vars)
(next-statep q r n))
(bisimilar (bisimilar-transition-witness-n->m p m q r n vars)
m r n vars)))
)
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+++++++++++++++++++++++ Proofs on bisimilary ++++++++++++++++++++++++++++++++
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
;; The following function determines a weird path in n, when given a cycle in
;; m. The weird path is a finite path compatible with n, and can be thought of
;; as the append of the prefix and cycle.
(defun find-matching-prefix-and-cycle-for-cycle-m->n (cycle m seen q states n vars path)
(declare (xargs :measure (nfix (- (1+ (len states)) (len seen)))))
;; for termination using Pigeon-hole arguments
(if (< (len states) (len seen)) (mv seen q path)
(let* ((path-produced (find-matching-path-for-path-m->n
cycle m q n vars))
(node-witness (bisimilar-transition-witness-m->n
(last-val cycle) (first cycle) m
(last-val path-produced) n vars)))
(if (memberp node-witness seen)
(mv (snoc seen node-witness) node-witness (append path path-produced))
(find-matching-prefix-and-cycle-for-cycle-m->n cycle m (snoc seen node-witness)
node-witness states n
vars (append path
path-produced))))))
;; And we pick up the prefix from the weird path
(defun find-matching-prefix-for-cycle-m->n (cycle m q n vars)
(mv-let (seen witness path)
(find-matching-prefix-and-cycle-for-cycle-m->n
cycle m (list q) q (states n) n vars nil)
(find-prefix cycle (del-last seen) witness path)))
; and also the cycle.
(defun find-matching-cycle-for-cycle-m->n (cycle m q n vars)
(mv-let (seen witness path)
(find-matching-prefix-and-cycle-for-cycle-m->n
cycle m (list q) q (states n) n vars nil)
(find-cycle cycle (del-last seen) witness path)))
(defun find-matching-periodic-path-m->n (ppath m n vars)
(let* ((init-p (initial-state ppath))
(prefix-p (prefix ppath))
(first-p (first prefix-p))
(cycle-p (cycle ppath))
(init-q (bisimilar-initial-state-witness-m->n init-p m n vars))
(first-q (bisimilar-transition-witness-m->n init-p first-p m init-q n
vars))
(match-path (find-matching-path-for-path-m->n prefix-p m first-q n
vars))
(last-p (last-val prefix-p))
(last-q (last-val match-path))
(first-cp (first cycle-p))
(first-cq (bisimilar-transition-witness-m->n last-p first-cp m last-q
n vars))
(match-prefix (find-matching-prefix-for-cycle-m->n
cycle-p m first-cq n vars))
(match-cycle (find-matching-cycle-for-cycle-m->n
cycle-p m first-cq n vars)))
(>_ :initial-state init-q
:prefix (append match-path match-prefix)
:cycle match-cycle)))