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