theory PLTL imports Main LTL.LTL Samplers StutterEquivalence begin section ‹Stuttering Invariant LTL Formulas› text ‹ We show that the next-free fragment of propositional linear-time temporal logic PLTL is invariant to finite stuttering. › subsection ‹Finite Conjunctions and Disjunctions in PLTL› (* It would be tempting to define these operators as follows: definition OR where "OR Φ = Finite_Set.fold or false Φ" definition AND where "AND Φ = Finite_Set.fold and true Φ" However, this would only work if "or" and "and" were left-commutative, which they are not (syntactically). We must therefore resort to the more general fold_graph predicate, effectively picking a conjunction (or disjunction) in arbitrary order. An alternative would be to define these generalized operators over lists of formulas, but working with sets is more natural in the following. *) definition OR where "OR Φ ≡ SOME φ. fold_graph Or_ltlp False_ltlp Φ φ" definition AND where "AND Φ ≡ SOME φ. fold_graph And_ltlp True_ltlp Φ φ" lemma fold_graph_OR: "finite Φ ⟹ fold_graph Or_ltlp False_ltlp Φ (OR Φ)" unfolding OR_def by (rule someI2_ex[OF finite_imp_fold_graph]) lemma fold_graph_AND: "finite Φ ⟹ fold_graph And_ltlp True_ltlp Φ (AND Φ)" unfolding AND_def by (rule someI2_ex[OF finite_imp_fold_graph]) lemma holds_of_OR [simp]: assumes fin: "finite (Φ::'a pltl set)" shows "(σ ⊨⇩_{p}OR Φ) = (∃φ∈Φ. σ ⊨⇩_{p}φ)" proof - { fix ψ::"'a pltl" assume "fold_graph Or_ltlp False_ltlp Φ ψ" hence "(σ ⊨⇩_{p}ψ) = (∃φ∈Φ. σ ⊨⇩_{p}φ)" by (rule fold_graph.induct) auto } with fold_graph_OR[OF fin] show ?thesis by simp qed lemma holds_of_AND [simp]: assumes fin: "finite (Φ::'a pltl set)" shows "(σ ⊨⇩_{p}AND Φ) = (∀φ∈Φ. σ ⊨⇩_{p}φ)" proof - { fix ψ::"'a pltl" assume "fold_graph And_ltlp True_ltlp Φ ψ" hence "(σ ⊨⇩_{p}ψ) = (∀φ∈Φ. σ ⊨⇩_{p}φ)" by (rule fold_graph.induct) auto } with fold_graph_AND[OF fin] show ?thesis by simp qed subsection ‹Next-Free PLTL Formulas› text ‹ A PLTL formula is called \emph{next-free} if it does not contain any subformula. › fun next_free :: "'a pltl ⇒ bool" where "next_free false⇩_{p}= True" | "next_free (atom⇩_{p}(p)) = True" | "next_free (φ implies⇩_{p}ψ) = (next_free φ ∧ next_free ψ)" | "next_free (X⇩_{p}φ) = False" | "next_free (φ U⇩_{p}ψ) = (next_free φ ∧ next_free ψ)" lemma next_free_not [simp]: "next_free (not⇩_{p}φ) = next_free φ" by (simp add: Not_ltlp_def) lemma next_free_true [simp]: "next_free true⇩_{p}" by (simp add: True_ltlp_def) lemma next_free_or [simp]: "next_free (φ or⇩_{p}ψ) = (next_free φ ∧ next_free ψ)" by (simp add: Or_ltlp_def) lemma next_free_and [simp]: "next_free (φ and⇩_{p}ψ) = (next_free φ ∧ next_free ψ)" by (simp add: And_ltlp_def) lemma next_free_eventually [simp]: "next_free (F⇩_{p}φ) = next_free φ" by (simp add: Eventually_ltlp_def) lemma next_free_always [simp]: "next_free (G⇩_{p}φ) = next_free φ" by (simp add: Always_ltlp_def) lemma next_free_release [simp]: "next_free (φ R⇩_{p}ψ) = (next_free φ ∧ next_free ψ)" by (simp add: Release_ltlp_def) lemma next_free_weak_until [simp]: "next_free (φ W⇩_{p}ψ) = (next_free φ ∧ next_free ψ)" by (auto simp: WeakUntil_ltlp_def) lemma next_free_strong_release [simp]: "next_free (φ M⇩_{p}ψ) = (next_free φ ∧ next_free ψ)" by (auto simp: StrongRelease_ltlp_def) lemma next_free_OR [simp]: assumes fin: "finite (Φ::'a pltl set)" shows "next_free (OR Φ) = (∀φ∈Φ. next_free φ)" proof - { fix ψ::"'a pltl" assume "fold_graph Or_ltlp False_ltlp Φ ψ" hence "next_free ψ = (∀φ∈Φ. next_free φ)" by (rule fold_graph.induct) auto } with fold_graph_OR[OF fin] show ?thesis by simp qed lemma next_free_AND [simp]: assumes fin: "finite (Φ::'a pltl set)" shows "next_free (AND Φ) = (∀φ∈Φ. next_free φ)" proof - { fix ψ::"'a pltl" assume "fold_graph And_ltlp True_ltlp Φ ψ" hence "next_free ψ = (∀φ∈Φ. next_free φ)" by (rule fold_graph.induct) auto } with fold_graph_AND[OF fin] show ?thesis by simp qed subsection ‹Stuttering Invariance of PLTL Without ``Next''› text ‹ A PLTL formula is \emph{stuttering invariant} if for any stuttering equivalent state sequences ‹σ ≈ τ›, the formula holds of ‹σ› iff it holds of ‹τ›. › definition stutter_invariant where "stutter_invariant φ = (∀σ τ. (σ ≈ τ) ⟶ (σ ⊨⇩_{p}φ) = (τ ⊨⇩_{p}φ))" text ‹ Since stuttering equivalence is symmetric, it is enough to show an implication in the above definition instead of an equivalence. › lemma stutter_invariantI [intro!]: assumes "⋀σ τ. ⟦σ ≈ τ; σ ⊨⇩_{p}φ⟧ ⟹ τ ⊨⇩_{p}φ" shows "stutter_invariant φ" proof - { fix σ τ assume st: "σ ≈ τ" and f: "σ ⊨⇩_{p}φ" hence "τ ⊨⇩_{p}φ" by (rule assms) } moreover { fix σ τ assume st: "σ ≈ τ" and f: "τ ⊨⇩_{p}φ" from st have "τ ≈ σ" by (rule stutter_equiv_sym) from this f have "σ ⊨⇩_{p}φ" by (rule assms) } ultimately show ?thesis by (auto simp: stutter_invariant_def) qed lemma stutter_invariantD [dest]: assumes "stutter_invariant φ" and "σ ≈ τ" shows "(σ ⊨⇩_{p}φ) = (τ ⊨⇩_{p}φ)" using assms by (auto simp: stutter_invariant_def) text ‹ We first show that next-free PLTL formulas are indeed stuttering invariant. The proof proceeds by straightforward induction on the syntax of PLTL formulas. › theorem next_free_stutter_invariant: "next_free φ ⟹ stutter_invariant (φ::'a pltl)" proof (induct "φ") show "stutter_invariant false⇩_{p}" by auto next fix p :: "'a ⇒ bool" show "stutter_invariant (atom⇩_{p}(p))" proof fix σ τ assume "σ ≈ τ" "σ ⊨⇩_{p}atom⇩_{p}(p)" thus "τ ⊨⇩_{p}atom⇩_{p}(p)" by (simp add: stutter_equiv_0) qed next fix φ ψ :: "'a pltl" assume ih: "next_free φ ⟹ stutter_invariant φ" "next_free ψ ⟹ stutter_invariant ψ" assume "next_free (φ implies⇩_{p}ψ)" with ih show "stutter_invariant (φ implies⇩_{p}ψ)" by auto next fix φ :: "'a pltl" assume "next_free (X⇩_{p}φ)" ― ‹hence contradiction› thus "stutter_invariant (X⇩_{p}φ)" by simp next fix φ ψ :: "'a pltl" assume ih: "next_free φ ⟹ stutter_invariant φ" "next_free ψ ⟹ stutter_invariant ψ" assume "next_free (φ U⇩_{p}ψ)" with ih have stinv: "stutter_invariant φ" "stutter_invariant ψ" by auto show "stutter_invariant (φ U⇩_{p}ψ)" proof fix σ τ assume st: "σ ≈ τ" and unt: "σ ⊨⇩_{p}φ U⇩_{p}ψ" from unt obtain m where 1: "σ[m..] ⊨⇩_{p}ψ" and 2: "∀j<m. (σ[j..] ⊨⇩_{p}φ)" by auto from st obtain n where 3: "(σ[m..]) ≈ (τ[n..])" and 4: "∀i<n. ∃j<m. (σ[j..]) ≈ (τ[i..])" by (rule stutter_equiv_suffixes_right) from 1 3 stinv have "τ[n..] ⊨⇩_{p}ψ" by auto moreover from 2 4 stinv have "∀i<n. (τ[i..] ⊨⇩_{p}φ)" by force ultimately show "τ ⊨⇩_{p}φ U⇩_{p}ψ" by auto qed qed subsection ‹Atoms, Canonical State Sequences, and Characteristic Formulas› text ‹ We now address the converse implication: any stutter invariant PLTL formula ‹φ› can be equivalently expressed by a next-free formula. The construction of that formula requires attention to the atomic formulas that appear in ‹φ›. We will also prove that the next-free formula does not need any new atoms beyond those present in ‹φ›. The following function collects the atoms (of type ‹'a ⇒ bool›) of a PLTL formula. › lemma atoms_pltl_OR [simp]: assumes fin: "finite (Φ::'a pltl set)" shows "atoms_pltl (OR Φ) = (⋃φ∈Φ. atoms_pltl φ)" proof - { fix ψ::"'a pltl" assume "fold_graph Or_ltlp False_ltlp Φ ψ" hence "atoms_pltl ψ = (⋃φ∈Φ. atoms_pltl φ)" by (rule fold_graph.induct) auto } with fold_graph_OR[OF fin] show ?thesis by simp qed lemma atoms_pltl_AND [simp]: assumes fin: "finite (Φ::'a pltl set)" shows "atoms_pltl (AND Φ) = (⋃φ∈Φ. atoms_pltl φ)" proof - { fix ψ::"'a pltl" assume "fold_graph And_ltlp True_ltlp Φ ψ" hence "atoms_pltl ψ = (⋃φ∈Φ. atoms_pltl φ)" by (rule fold_graph.induct) auto } with fold_graph_AND[OF fin] show ?thesis by simp qed text ‹ Given a set of atoms ‹A› as above, we say that two states are ‹A›-similar if they agree on all atoms in ‹A›. Two state sequences ‹σ› and ‹τ› are ‹A›-similar if corresponding states are ‹A›-equal. › definition state_sim :: "['a, ('a ⇒ bool) set, 'a] ⇒ bool" (‹_ ~_~ _› [70,100,70] 50) where "s ~A~ t = (∀p∈A. p s ⟷ p t)" definition seq_sim :: "[nat ⇒ 'a, ('a ⇒ bool) set, nat ⇒ 'a] ⇒ bool" (‹_ ≃_≃ _› [70,100,70] 50) where "σ ≃A≃ τ = (∀n. (σ n) ~A~ (τ n))" text ‹ These relations are (indexed) equivalence relations. Moreover ‹s ~A~ t› implies ‹s ~B~ t› for ‹B ⊆ A›, and similar for ‹σ ≃A≃ τ› and ‹σ ≃B≃ τ›. › lemma state_sim_refl [simp]: "s ~A~ s" by (simp add: state_sim_def) lemma state_sim_sym: "s ~A~ t ⟹ t ~A~ s" by (auto simp: state_sim_def) lemma state_sim_trans[trans]: "s ~A~ t ⟹ t ~A~ u ⟹ s ~A~ u" unfolding state_sim_def by blast lemma state_sim_mono: assumes "s ~A~ t" and "B ⊆ A" shows "s ~B~ t" using assms unfolding state_sim_def by auto lemma seq_sim_refl [simp]: "σ ≃A≃ σ" by (simp add: seq_sim_def) lemma seq_sim_sym: "σ ≃A≃ τ ⟹ τ ≃A≃ σ" by (auto simp: seq_sim_def state_sim_sym) lemma seq_sim_trans[trans]: "ρ ≃A≃ σ ⟹ σ ≃A≃ τ ⟹ ρ ≃A≃ τ" unfolding seq_sim_def by (blast intro: state_sim_trans) lemma seq_sim_mono: assumes "σ ≃A≃ τ" and "B ⊆ A" shows "σ ≃B≃ τ" using assms unfolding seq_sim_def by (blast intro: state_sim_mono) text ‹ State sequences that are similar w.r.t. the atoms of a PLTL formula evaluate that formula to the same value. › lemma pltl_seq_sim: "σ ≃ atoms_pltl φ ≃ τ ⟹ (σ ⊨⇩_{p}φ) = (τ ⊨⇩_{p}φ)" (is "?sim σ φ τ ⟹ ?P σ φ τ") proof (induct φ arbitrary: σ τ) fix σ τ show "?P σ false⇩_{p}τ" by simp next fix p σ τ assume "?sim σ (atom⇩_{p}(p)) τ" thus "?P σ (atom⇩_{p}(p)) τ" by (auto simp: seq_sim_def state_sim_def) next fix φ ψ σ τ assume ih: "⋀σ τ. ?sim σ φ τ ⟹ ?P σ φ τ" "⋀σ τ. ?sim σ ψ τ ⟹ ?P σ ψ τ" and sim: "?sim σ (φ implies⇩_{p}ψ) τ" from sim have "?sim σ φ τ" "?sim σ ψ τ" by (auto elim: seq_sim_mono) with ih show "?P σ (φ implies⇩_{p}ψ) τ" by simp next fix φ σ τ assume ih: "⋀σ τ. ?sim σ φ τ ⟹ ?P σ φ τ" and sim: "σ ≃ atoms_pltl (X⇩_{p}φ) ≃ τ" from sim have "(σ[1..]) ≃ atoms_pltl φ ≃ (τ[1..])" by (auto simp: seq_sim_def) with ih show "?P σ (X⇩_{p}φ) τ" by auto next fix φ ψ σ τ assume ih: "⋀σ τ. ?sim σ φ τ ⟹ ?P σ φ τ" "⋀σ τ. ?sim σ ψ τ ⟹ ?P σ ψ τ" and sim: "?sim σ (φ U⇩_{p}ψ) τ" from sim have "∀i. (σ[i..]) ≃ atoms_pltl φ ≃ (τ[i..])" "∀j. (σ[j..]) ≃ atoms_pltl ψ ≃ (τ[j..])" by (auto simp: seq_sim_def state_sim_def) with ih have "∀i. ?P (σ[i..]) φ (τ[i..])" "∀j. ?P (σ[j..]) ψ (τ[j..])" by blast+ thus "?P σ (φ U⇩_{p}ψ) τ" by (meson semantics_pltl.simps(5)) qed text ‹ The following function picks an arbitrary representative among ‹A›-similar states. Because the choice is functional, any two ‹A›-similar states are mapped to the same state. › definition canonize where "canonize A s ≡ SOME t. t ~A~ s" lemma canonize_state_sim: "canonize A s ~A~ s" unfolding canonize_def by (rule someI, rule state_sim_refl) lemma canonize_canonical: assumes st: "s ~A~ t" shows "canonize A s = canonize A t" proof - from st have "∀u. (u ~A~s) = (u ~A~ t)" by (auto elim: state_sim_sym state_sim_trans) thus ?thesis unfolding canonize_def by simp qed lemma canonize_idempotent: "canonize A (canonize A s) = canonize A s" by (rule canonize_canonical[OF canonize_state_sim]) text ‹ In a canonical state sequence, any two ‹A›-similar states are in fact equal. › definition canonical_sequence where "canonical_sequence A σ ≡ ∀m (n::nat). σ m ~A~ σ n ⟶ σ m = σ n" text ‹ Every suffix of a canonical sequence is canonical, as is any (sampled) subsequence, in particular any stutter-sampling. › lemma canonical_suffix: "canonical_sequence A σ ⟹ canonical_sequence A (σ[k..])" by (auto simp: canonical_sequence_def) lemma canonical_sampled: "canonical_sequence A σ ⟹ canonical_sequence A (σ ∘ f)" by (auto simp: canonical_sequence_def) lemma canonical_reduced: "canonical_sequence A σ ⟹ canonical_sequence A (♮σ)" unfolding stutter_reduced_def by (rule canonical_sampled) text ‹ For any sequence ‹σ› there exists a canonical ‹A›-similar sequence ‹τ›. Such a ‹τ› can be obtained by canonizing all states of ‹σ›. › lemma canonical_exists: obtains τ where "τ ≃A≃ σ" "canonical_sequence A τ" proof - have "(canonize A ∘ σ) ≃A≃ σ" by (simp add: seq_sim_def canonize_state_sim) moreover have "canonical_sequence A (canonize A ∘ σ)" by (auto simp: canonical_sequence_def canonize_idempotent dest: canonize_canonical) ultimately show ?thesis using that by blast qed text ‹ Given a state ‹s› and a set ‹A› of atoms, we define the characteristic formula of ‹s› as the conjunction of all atoms in ‹A› that hold of ‹s› and the negation of the atoms in ‹A› that do not hold of ‹s›. › definition characteristic_formula where "characteristic_formula A s ≡ ((AND { atom⇩_{p}(p) | p . p ∈ A ∧ p s }) and⇩_{p}(AND { not⇩_{p}(atom⇩_{p}(p)) | p . p ∈ A ∧ ¬(p s) }))" lemma characteristic_holds: "finite A ⟹ σ ⊨⇩_{p}characteristic_formula A (σ 0)" by (auto simp: characteristic_formula_def) lemma characteristic_state_sim: assumes fin: "finite A" shows "(σ 0 ~A~ τ 0) = (τ ⊨⇩_{p}characteristic_formula A (σ (0::nat)))" proof assume sim: "σ 0 ~A~ τ 0" { fix p assume "p ∈ A" with sim have "p (τ 0) = p (σ 0)" by (auto simp: state_sim_def) } with fin show "τ ⊨⇩_{p}characteristic_formula A (σ 0)" by (auto simp: characteristic_formula_def) (blast+) next assume "τ ⊨⇩_{p}characteristic_formula A (σ 0)" with fin show "σ 0 ~A~ τ 0" by (auto simp: characteristic_formula_def state_sim_def) qed subsection ‹Stuttering Invariant PLTL Formulas Don't Need Next› text ‹ The following is the main lemma used in the proof of the completeness theorem: for any PLTL formula ‹φ› there exists a next-free formula ‹ψ› such that the two formulas evaluate to the same value over stutter-free and canonical sequences (w.r.t. some ‹A ⊇ atoms_pltl φ›). › lemma ex_next_free_stutter_free_canonical: assumes A: "atoms_pltl φ ⊆ A" and fin: "finite A" shows "∃ψ. next_free ψ ∧ atoms_pltl ψ ⊆ A ∧ (∀σ. stutter_free σ ∧ canonical_sequence A σ ⟶ (σ ⊨⇩_{p}ψ) = (σ ⊨⇩_{p}φ))" (is "∃ψ. ?P φ ψ") using A proof (induct φ) txt ‹The cases of ‹false› and atomic formulas are trivial.› have "?P false⇩_{p}false⇩_{p}" by auto thus "∃ψ. ?P false⇩_{p}ψ" .. next fix p assume "atoms_pltl (atom⇩_{p}(p)) ⊆ A" hence "?P (atom⇩_{p}(p)) (atom⇩_{p}(p))" by auto thus "∃ψ. ?P (atom⇩_{p}(p)) ψ" .. next txt ‹Implication is easy, using the induction hypothesis.› fix φ ψ assume "atoms_pltl φ ⊆ A ⟹ ∃φ'. ?P φ φ'" and "atoms_pltl ψ ⊆ A ⟹ ∃ψ'. ?P ψ ψ'" and "atoms_pltl (φ implies⇩_{p}ψ) ⊆ A" then obtain φ' ψ' where "?P φ φ'" "?P ψ ψ'" by auto hence "?P (φ implies⇩_{p}ψ) (φ' implies⇩_{p}ψ')" by auto thus "∃χ. ?P (φ implies⇩_{p}ψ) χ" .. next txt ‹The case of ‹until› follows similarly.› fix φ ψ assume "atoms_pltl φ ⊆ A ⟹ ∃φ'. ?P φ φ'" and "atoms_pltl ψ ⊆ A ⟹ ∃ψ'. ?P ψ ψ'" and "atoms_pltl (φ U⇩_{p}ψ) ⊆ A" then obtain φ' ψ' where 1: "?P φ φ'" and 2: "?P ψ ψ'" by auto { fix σ assume sigma: "stutter_free σ" "canonical_sequence A σ" hence "⋀k. stutter_free (σ[k..])" "⋀k. canonical_sequence A (σ[k..])" by (auto simp: stutter_free_suffix canonical_suffix) with 1 2 have "⋀k. (σ[k..] ⊨⇩_{p}φ') = (σ[k..] ⊨⇩_{p}φ)" and "⋀k. (σ[k..] ⊨⇩_{p}ψ') = (σ[k..] ⊨⇩_{p}ψ)" by (blast+) hence "(σ ⊨⇩_{p}φ' U⇩_{p}ψ') = (σ ⊨⇩_{p}φ U⇩_{p}ψ)" by auto } with 1 2 have "?P (φ U⇩_{p}ψ) (φ' U⇩_{p}ψ')" by auto thus "∃χ. ?P (φ U⇩_{p}ψ) χ" .. next txt ‹The interesting case is the one of the ‹next›-operator.› fix φ assume ih: "atoms_pltl φ ⊆ A ⟹ ∃ψ. ?P φ ψ" and at: "atoms_pltl (X⇩_{p}φ) ⊆ A" then obtain ψ where psi: "?P φ ψ" by auto txt ‹A valuation (over ‹A›) is a set ‹val ⊆ A› of atoms. We define some auxiliary notions: the valuation corresponding to a state and the characteristic formula for a valuation. Finally, we define the formula ‹psi'› that we will prove to be equivalent to ‹X⇩_{p}φ› over the stutter-free and canonical sequence ‹σ›.› define stval where "stval = (λs. { p ∈ A . p s })" define chi where "chi = (λval. ((AND {atom⇩_{p}(p) | p . p ∈ val}) and⇩_{p}(AND {not⇩_{p}(atom⇩_{p}(p)) | p . p ∈ A - val})))" define psi' where "psi' = ((ψ and⇩_{p}(OR {G⇩_{p}(chi val) | val . val ⊆ A })) or⇩_{p}(OR {(chi val) and⇩_{p}((chi val) U⇩_{p}( ψ and⇩_{p}(chi val'))) | val val'. val ⊆ A ∧ val' ⊆ A ∧ val' ≠ val }))" (is "_ = (( _ and⇩_{p}(OR ?ALW)) or⇩_{p}(OR ?UNT))") have "⋀s. {not⇩_{p}(atom⇩_{p}(p)) | p . p ∈ A - stval s} = {not⇩_{p}(atom⇩_{p}(p)) | p . p ∈ A ∧ ¬(p s)}" by (auto simp: stval_def) hence chi1: "⋀s. chi (stval s) = characteristic_formula A s" by (auto simp: chi_def stval_def characteristic_formula_def) { fix val τ assume val: "val ⊆ A" and tau: "τ ⊨⇩_{p}chi val" with fin have "val = stval (τ 0)" by (auto simp: stval_def chi_def finite_subset) } note chi2 = this have "?UNT ⊆ (λ(val,val'). (chi val) and⇩_{p}((chi val) U⇩_{p}(ψ and⇩_{p}(chi val')))) ` (Pow A × Pow A)" (is "_ ⊆ ?S") by auto with fin have fin_UNT: "finite ?UNT" by (auto simp: finite_subset) have nf: "next_free psi'" proof - from fin have "⋀val. val ⊆ A ⟹ next_free (chi val)" by (auto simp: chi_def finite_subset) with fin fin_UNT psi show ?thesis by (force simp: psi'_def finite_subset) qed have atoms_pltl: "atoms_pltl psi' ⊆ A" proof - from fin have at_chi: "⋀val. val ⊆ A ⟹ atoms_pltl (chi val) ⊆ A" by (auto simp: chi_def finite_subset) with fin psi have at_alw: "atoms_pltl (ψ and⇩_{p}(OR ?ALW)) ⊆ A" by auto blast? (** FRAGILE: auto leaves trivial goal about subset **) from fin fin_UNT psi at_chi have "atoms_pltl (OR ?UNT) ⊆ A" by auto (blast+)? (** FRAGILE: even more left-over goals here **) with at_alw show ?thesis by (auto simp: psi'_def) qed { fix σ assume st: "stutter_free σ" and can: "canonical_sequence A σ" have "(σ ⊨⇩_{p}X⇩_{p}φ) = (σ ⊨⇩_{p}psi')" proof (cases "σ (Suc 0) = σ 0") case True txt ‹In the case of a stuttering transition at the beginning, we must have infinite stuttering, and the first disjunct of ‹psi'› holds, whereas the second does not.› { fix n have "σ n = σ 0" proof (cases n) case 0 thus ?thesis by simp next case Suc hence "n > 0" by simp with True st show ?thesis unfolding stutter_free_def by blast qed } note alleq = this have suffix: "⋀n. σ[n..] = σ" proof (rule ext) fix n i have "(σ[n..]) i = σ 0" by (auto intro: alleq) moreover have "σ i = σ 0" by (rule alleq) ultimately show "(σ[n..]) i = σ i" by simp qed with st can psi have 1: "(σ ⊨⇩_{p}X⇩_{p}φ) = (σ ⊨⇩_{p}ψ)" by simp from fin have "σ ⊨⇩_{p}chi (stval (σ 0))" by (simp add: chi1 characteristic_holds) with suffix have "σ ⊨⇩_{p}G⇩_{p}(chi (stval (σ 0)))" (is "_ ⊨⇩_{p}?alw") by simp moreover have "?alw ∈ ?ALW" by (auto simp: stval_def) ultimately have 2: "σ ⊨⇩_{p}OR ?ALW" using fin by (auto simp: finite_subset simp del: semantics_pltl_sugar) have 3: "¬(σ ⊨⇩_{p}OR ?UNT)" proof assume unt: "σ ⊨⇩_{p}OR ?UNT" with fin_UNT obtain val val' k where val: "val ⊆ A" "val' ⊆ A" "val' ≠ val" and now: "σ ⊨⇩_{p}chi val" and k: "σ[k..] ⊨⇩_{p}chi val'" by auto (blast+)? (* FRAGILE: similar as above *) from ‹val ⊆ A› now have "val = stval (σ 0)" by (rule chi2) moreover from ‹val' ⊆ A› k suffix have "val' = stval (σ 0)" by (simp add: chi2) moreover note ‹val' ≠ val› ultimately show "False" by simp qed from 1 2 3 show ?thesis by (simp add: psi'_def) next case False txt ‹Otherwise, ‹σ ⊨⇩_{p}X⇩_{p}φ› is equivalent to ‹σ› satisfying the second disjunct of ‹psi'›. We show both implications separately.› let ?val = "stval (σ 0)" let ?val' = "stval (σ 1)" from False can have vals: "?val' ≠ ?val" by (auto simp: canonical_sequence_def state_sim_def stval_def) show ?thesis proof assume phi: "σ ⊨⇩_{p}X⇩_{p}φ" from fin have 1: "σ ⊨⇩_{p}chi ?val" by (simp add: chi1 characteristic_holds) from st can have "stutter_free (σ[1..])" "canonical_sequence A (σ[1..])" by (auto simp: stutter_free_suffix canonical_suffix) with phi psi have 2: "σ[1..] ⊨⇩_{p}ψ" by auto from fin have "σ[1..] ⊨⇩_{p}characteristic_formula A ((σ[1..]) 0)" by (rule characteristic_holds) hence 3: "σ[1..] ⊨⇩_{p}chi ?val'" by (simp add: chi1) from 1 2 3 have "σ ⊨⇩_{p}And_ltlp (chi ?val) ((chi ?val) U⇩_{p}(And_ltlp ψ (chi ?val')))" (is "_ ⊨⇩_{p}?unt") by auto moreover from vals have "?unt ∈ ?UNT" by (auto simp: stval_def) ultimately have "σ ⊨⇩_{p}OR ?UNT" using fin_UNT[THEN holds_of_OR] by blast thus "σ ⊨⇩_{p}psi'" by (simp add: psi'_def) next assume psi': "σ ⊨⇩_{p}psi'" have "¬(σ ⊨⇩_{p}OR ?ALW)" proof assume "σ ⊨⇩_{p}OR ?ALW" with fin obtain val where 1: "val ⊆ A" and 2: "∀n. (σ[n..] ⊨⇩_{p}chi val)" by (force simp: finite_subset) from 2 have "σ[0..] ⊨⇩_{p}chi val" .. with 1 have "val = ?val" by (simp add: chi2) moreover from 2 have "σ[1..] ⊨⇩_{p}chi val" .. with 1 have "val = ?val'" by (force dest: chi2) ultimately show "False" using vals by simp qed with psi' have "σ ⊨⇩_{p}OR ?UNT" by (simp add: psi'_def) with fin_UNT obtain val val' k where val: "val ⊆ A" "val' ⊆ A" "val' ≠ val" and now: "σ ⊨⇩_{p}chi val" and k: "σ[k..] ⊨⇩_{p}ψ" "σ[k..] ⊨⇩_{p}chi val'" and i: "∀i<k. (σ[i..] ⊨⇩_{p}chi val)" by auto (blast+)? (* FRAGILE: similar as above *) from val now have 1: "val = ?val" by (simp add: chi2) have 2: "k ≠ 0" proof assume "k=0" with val k have "val' = ?val" by (simp add: chi2) with 1 ‹val' ≠ val› show "False" by simp qed have 3: "k ≤ 1" proof (rule ccontr) assume "¬(k ≤ 1)" with i have "σ[1..] ⊨⇩_{p}chi val" by simp with 1 have "σ[1..] ⊨⇩_{p}characteristic_formula A (σ 0)" by (simp add: chi1) hence "(σ 0) ~A~ ((σ[1..]) 0)" using characteristic_state_sim[OF fin] by blast with can have "σ 0 = σ 1" by (simp add: canonical_sequence_def) with ‹σ (Suc 0) ≠ σ 0› show "False" by simp qed from 2 3 have "k=1" by simp moreover from st can have "stutter_free (σ[1..])" "canonical_sequence A (σ[1..])" by (auto simp: stutter_free_suffix canonical_suffix) ultimately show "σ ⊨⇩_{p}X⇩_{p}φ" using ‹σ[k..] ⊨⇩_{p}ψ› psi by auto qed qed } with nf atoms_pltl show "∃ψ'. ?P (X⇩_{p}φ) ψ'" by blast qed text ‹ Comparing the definition of the next-free formula in the case of formulas ‹X⇩_{p}φ› with the one that appears in~\<^cite>‹"peled:ltl-x"›, there is a subtle difference. Peled and Wilke define the second disjunct as a disjunction of formulas % \begin{center}\( ‹(chi val) U⇩_{p}(ψ and⇩_{p}(chi val'))› \)\end{center} % for subsets ‹val, val' ⊆ A› whereas we conjoin the formula ‹chi val› to the ``until'' formula. This conjunct is indeed necessary in order to rule out the case of the ``until'' formula being true because of ‹chi val'› being true immediately. The subtle error in the definition of the formula was acknowledged by Peled and Wilke and apparently had not been noticed since the publication of~\<^cite>‹"peled:ltl-x"› in 1996 (which has been cited more than a hundred times according to Google Scholar). Although the error was corrected easily, the fact that authors, reviewers, and readers appear to have missed it for so long underscores the usefulness of formal proofs. We now show that any stuttering invariant PLTL formula can be expressed without the ‹X⇩_{p}› operator. › theorem stutter_invariant_next_free: assumes phi: "stutter_invariant φ" obtains ψ where "next_free ψ" "atoms_pltl ψ ⊆ atoms_pltl φ" "∀σ. (σ ⊨⇩_{p}ψ) = (σ ⊨⇩_{p}φ)" proof - have "atoms_pltl φ ⊆ atoms_pltl φ" "finite (atoms_pltl φ)" by simp_all then obtain ψ where psi: "next_free ψ" "atoms_pltl ψ ⊆ atoms_pltl φ" and equiv: "∀σ. stutter_free σ ∧ canonical_sequence (atoms_pltl φ) σ ⟶ (σ ⊨⇩_{p}ψ) = (σ ⊨⇩_{p}φ)" by (blast dest: ex_next_free_stutter_free_canonical) from ‹next_free ψ› have sinv: "stutter_invariant ψ" by (rule next_free_stutter_invariant) { fix σ obtain τ where 1: "τ ≃ atoms_pltl φ ≃ σ" and 2: "canonical_sequence (atoms_pltl φ) τ" by (rule canonical_exists) from 1 ‹atoms_pltl ψ ⊆ atoms_pltl φ› have 3: "τ ≃ atoms_pltl ψ ≃ σ" by (rule seq_sim_mono) from 1 have "(σ ⊨⇩_{p}φ) = (τ ⊨⇩_{p}φ)" by (simp add: pltl_seq_sim) also from phi stutter_reduced_equivalent have "... = (♮τ ⊨⇩_{p}φ)" by auto also from 2[THEN canonical_reduced] equiv stutter_reduced_stutter_free have "... = (♮τ ⊨⇩_{p}ψ)" by auto also from sinv stutter_reduced_equivalent have "... = (τ ⊨⇩_{p}ψ)" by auto also from 3 have "... = (σ ⊨⇩_{p}ψ)" by (simp add: pltl_seq_sim) finally have "(σ ⊨⇩_{p}ψ) = (σ ⊨⇩_{p}φ)" by (rule sym) } with psi that show ?thesis by blast qed text ‹ Combining theorems ‹next_free_stutter_invariant› and ‹stutter_invariant_next_free›, it follows that a PLTL formula is stuttering invariant iff it is equivalent to a next-free formula. › theorem pltl_stutter_invariant: "stutter_invariant φ ⟷ (∃ψ. next_free ψ ∧ atoms_pltl ψ ⊆ atoms_pltl φ ∧ (∀σ. σ ⊨⇩_{p}ψ ⟷ σ ⊨⇩_{p}φ))" proof - { assume "stutter_invariant φ" hence "∃ψ. next_free ψ ∧ atoms_pltl ψ ⊆ atoms_pltl φ ∧ (∀σ. σ ⊨⇩_{p}ψ ⟷ σ ⊨⇩_{p}φ)" by (rule stutter_invariant_next_free) blast } moreover { fix ψ assume 1: "next_free ψ" and 2: "∀σ. σ ⊨⇩_{p}ψ ⟷ σ ⊨⇩_{p}φ" from 1 have "stutter_invariant ψ" by (rule next_free_stutter_invariant) with 2 have "stutter_invariant φ" by blast } ultimately show ?thesis by blast qed subsection ‹Stutter Invariance for LTL with Syntactic Sugar› text ‹We lift the results for PLTL to an extensive version of LTL.› primrec ltlc_next_free :: "'a ltlc ⇒ bool" where "ltlc_next_free true⇩_{c}= True" | "ltlc_next_free false⇩_{c}= True" | "ltlc_next_free (prop⇩_{c}(q)) = True" | "ltlc_next_free (not⇩_{c}φ) = ltlc_next_free φ" | "ltlc_next_free (φ and⇩_{c}ψ) = (ltlc_next_free φ ∧ ltlc_next_free ψ)" | "ltlc_next_free (φ or⇩_{c}ψ) = (ltlc_next_free φ ∧ ltlc_next_free ψ)" | "ltlc_next_free (φ implies⇩_{c}ψ) = (ltlc_next_free φ ∧ ltlc_next_free ψ)" | "ltlc_next_free (X⇩_{c}φ) = False" | "ltlc_next_free (F⇩_{c}φ) = ltlc_next_free φ" | "ltlc_next_free (G⇩_{c}φ) = ltlc_next_free φ" | "ltlc_next_free (φ U⇩_{c}ψ) = (ltlc_next_free φ ∧ ltlc_next_free ψ)" | "ltlc_next_free (φ R⇩_{c}ψ) = (ltlc_next_free φ ∧ ltlc_next_free ψ)" | "ltlc_next_free (φ W⇩_{c}ψ) = (ltlc_next_free φ ∧ ltlc_next_free ψ)" | "ltlc_next_free (φ M⇩_{c}ψ) = (ltlc_next_free φ ∧ ltlc_next_free ψ)" lemma ltlc_next_free_iff[simp]: "next_free (ltlc_to_pltl φ) ⟷ ltlc_next_free φ" by (induction φ) auto text ‹A next free formula cannot distinguish between stutter-equivalent runs.› theorem ltlc_next_free_stutter_invariant: assumes next_free: "ltlc_next_free φ" assumes eq: "r ≈ r'" shows "r ⊨⇩_{c}φ ⟷ r' ⊨⇩_{c}φ" proof - { fix r r' assume eq: "r ≈ r'" and holds: "r ⊨⇩_{c}φ" then have "r ⊨⇩_{p}(ltlc_to_pltl φ)"by simp from next_free_stutter_invariant[of "ltlc_to_pltl φ"] next_free have "PLTL.stutter_invariant (ltlc_to_pltl φ)" by simp from stutter_invariantD[OF this eq] holds have "r' ⊨⇩_{c}φ" by simp } note aux=this from aux[of r r'] aux[of r' r] eq stutter_equiv_sym[OF eq] show ?thesis by blast qed end