Theory Stuttering_Equivalence.PLTL
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›
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 φ)"
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?
from fin fin_UNT psi at_chi have "atoms_pltl (OR ?UNT) ⊆ A"
by auto (blast+)?
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+)?
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+)?
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