Theory Safety_Perfect
section‹Safety for Cars with Perfect Sensors›
text‹
This section contains the definition of requirements for
lane change and distance controllers for cars, with the assumption
of perfect sensors. Using these definitions, we show that safety
is an invariant along all possible behaviour of cars.
›
theory Safety_Perfect
imports HMLSL_Perfect
begin
context hmlsl_perfect
begin
interpretation hmlsl : hmlsl "perfect :: cars ⇒ traffic ⇒ cars ⇒ real"
proof unfold_locales
fix e ts c
show " 0 < perfect e ts c"
by (metis less_add_same_cancel2 less_trans perfect_def traffic.psGeZero
traffic.sdGeZero)
qed
notation hmlsl.re (‹re'(_')›)
notation hmlsl.cl(‹cl'(_')›)
notation hmlsl.len (‹len›)
text‹
Safety in the context of HMLSL means the absence of overlapping
reservations. Using the somewhere modality, this is easy to formalise.
›
abbreviation safe::"cars⇒σ"
where "safe e ≡ ❙∀ c. ❙¬(c ❙= e) ❙→ ❙¬ ❙⟨re(c) ❙∧ re(e) ❙⟩"
text‹
The distance controller ensures, that as long as the cars do not try
to change their lane, they keep their distance. More formally,
if the reservations of two cars do not overlap, they will also not
overlap after an arbitrary amount of time passed. Observe that
the cars are allowed to change their dynamical behaviour, i.e.,
to accelerate and brake.
›
abbreviation DC::"σ"
where "DC ≡ ❙G(❙∀ c d. ❙¬(c ❙= d) ❙→
❙¬❙⟨re(c) ❙∧ re(d)❙⟩ ❙→ ❙□❙τ ❙¬❙⟨re(c) ❙∧ re(d)❙⟩)"
text‹
To identify possibly dangerous situations during a lane change manoeuvre,
we use the \emph{potential collision check}. It allows us to identify
situations, where the claim of a car \(d\) overlaps with
any part of the car \(c\).
›
abbreviation pcc::"cars ⇒ cars ⇒ σ"
where "pcc c d ≡ ❙¬ (c ❙= d) ❙∧ ❙⟨ cl(d) ❙∧ (re(c) ❙∨ cl(c)) ❙⟩"
text ‹
The only restriction the lane change controller imposes onto the cars is
that in the case of a potential collision, they are not allowed to change
the claim into a reservation.
›
abbreviation LC::"σ"
where "LC ≡ ❙G ( ❙∀d.( ❙∃ c. pcc c d) ❙→ ❙□r(d) ❙⊥) "
text‹
The safety theorem is as follows. If the controllers of all
cars adhere to the specifications given by \(LC\) and \(DC\),
and we start with an initially safe traffic snapshot, then
all reachable traffic snapshots are also safe.
›
theorem safety:"⊨( ❙∀e. safe e ) ❙∧ DC ❙∧ LC ❙→ ❙G (❙∀ e. safe e)"
proof (rule allI|rule impI)+
fix ts v ts'
fix e c::cars
assume assm:"ts,v ⊨ ( ❙∀e. safe e ) ❙∧ DC ❙∧ LC"
assume abs:"ts ❙⇒ ts'"
assume nequals: "ts,v ⊨❙¬(c ❙=e)"
from assm have init:"ts,v ⊨ ( ❙∀e. safe e )" by simp
from assm have DC :"ts,v ⊨ DC" by simp
from assm have LC: "ts,v ⊨ LC" by simp
from abs show "ts',move ts ts' v ⊨ ❙¬ ❙⟨re(c) ❙∧ re(e)❙⟩ "
proof (induction)
case (refl)
have "move ts ts v = v" using traffic.move_nothing by simp
thus ?case using init traffic.move_nothing nequals by auto
next
case (evolve ts' ts'' )
have local_DC:
"ts',move ts ts' v ⊨ ❙∀ c d. ❙¬(c ❙= d) ❙→
❙¬❙⟨re(c) ❙∧ re(d)❙⟩ ❙→ ❙□❙τ ❙¬❙⟨re(c) ❙∧ re(d)❙⟩"
using "evolve.hyps" DC by simp
show ?case
proof
assume e_def:" (ts'',move ts ts'' v ⊨ ❙⟨re(c) ❙∧ re(e) ❙⟩)"
from "evolve.IH" and nequals have
ts'_safe:"ts',move ts ts' v ⊨ ❙¬(c ❙= e) ❙∧ ❙¬❙⟨re(c) ❙∧ re(e)❙⟩" by fastforce
hence no_coll_after_evol:"ts',move ts ts' v ⊨ ❙□❙τ ❙¬❙⟨re(c) ❙∧ re(e)❙⟩"
using local_DC by blast
have move_eq:"move ts' ts'' (move ts ts' v) = move ts ts'' v"
using "evolve.hyps" traffic.abstract.evolve traffic.abstract.refl
traffic.move_trans
by blast
from no_coll_after_evol and "evolve.hyps" have
"ts'',move ts' ts'' (move ts ts' v) ⊨ ❙¬❙⟨re(c) ❙∧ re(e)❙⟩"
by blast
thus False using e_def using move_eq by fastforce
qed
next
case (cr_res ts' ts'')
have local_LC: "ts',move ts ts' v ⊨( ❙∀d.( ❙∃ c. pcc c d) ❙→ ❙□r(d) ❙⊥)"
using LC "cr_res.hyps" by blast
have "move ts ts' v = move ts' ts'' (move ts ts' v)"
using traffic.move_stability_res "cr_res.hyps" traffic.move_trans
move_stability_clm by auto
hence move_stab: "move ts ts' v = move ts ts'' v"
by (metis traffic.abstract.simps cr_res.hyps traffic.move_trans)
show ?case
proof (rule)
assume e_def:" (ts'',move ts ts'' v ⊨ ❙⟨re(c) ❙∧ re(e) ❙⟩)"
obtain d where d_def: "ts' ❙─r(d) ❙→ ts''" using "cr_res.hyps" by best
have "d = e ∨ d ≠ e" by simp
thus False
proof
assume eq:"d = e"
hence e_trans:"ts' ❙─r(e) ❙→ ts''" using d_def by simp
from e_def have "ts'',move ts ts'' v ⊨ ❙⟨ re(c) ❙∧ re(e)❙⟩" by auto
hence "∃v'. (v' ≤ move ts ts'' v) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
using view.somewhere_leq
by meson
then obtain v' where v'_def:
"(v' ≤ move ts ts'' v) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
by blast
with backwards_res_act have "ts',v' ⊨ re(c) ❙∧ (re(e) ❙∨ cl(e))"
using e_def backwards_res_stab nequals
by (metis (no_types, lifting) d_def eq)
hence "∃v'. (v' ≤ move ts ts'' v) ∧ (ts',v' ⊨ re(c) ❙∧ (re(e) ❙∨ cl(e)))"
using v'_def by blast
hence "ts',move ts ts'' v ⊨❙⟨ re(c) ❙∧ (re(e) ❙∨ cl(e)) ❙⟩"
using view.somewhere_leq by meson
hence "ts',move ts ts'' v ⊨ ❙⟨ re(c) ❙∧ re(e)❙⟩ ❙∨ ❙⟨ re(c) ❙∧ cl(e)❙⟩ "
using hmlsl.somewhere_and_or_distr by blast
thus False
proof
assume assm':"ts',move ts ts'' v ⊨ ❙⟨ re(c) ❙∧ re(e)❙⟩"
have "ts',move ts ts' v ⊨ ❙¬ (c ❙= e)" using nequals by blast
thus False using assm' cr_res.IH e_def move_stab by force
next
assume assm':"ts',move ts ts'' v ⊨ ❙⟨ re(c) ❙∧ cl(e)❙⟩"
hence "ts',move ts ts'' v ⊨ ❙¬ (c ❙=e) ❙∧ ❙⟨ re(c) ❙∧ cl(e)❙⟩"
using e_def nequals by force
hence "ts',move ts ts'' v ⊨❙¬ (c ❙=e) ❙∧ ❙⟨ cl(e) ❙∧ (re(c) ❙∨ cl(c)) ❙⟩" by blast
hence pcc:"ts',move ts ts'' v ⊨ pcc c e" by blast
have "ts',move ts ts'' v ⊨( ❙∃ c. pcc c e) ❙→ ❙□r(e) ❙⊥ "
using local_LC move_stab by fastforce
hence "ts',move ts ts'' v ⊨ ❙□r(e) ❙⊥" using pcc by blast
thus "ts'',move ts ts'' v ⊨ ❙⊥" using e_trans by blast
qed
next
assume neq:"d ≠ e"
have "c=d ∨ c ≠ d" by simp
thus False
proof
assume neq2:"c ≠ d"
from e_def have "ts'',move ts ts'' v ⊨ ❙⟨ re(c) ❙∧ re(e)❙⟩" by auto
hence "∃v'. (v' ≤ move ts ts'' v) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
using view.somewhere_leq
by meson
then obtain v' where v'_def:
"(v' ≤ move ts ts'' v) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
by blast
with backwards_res_stab have overlap: "ts',v' ⊨ re(c) ❙∧ re(e)"
using e_def backwards_res_stab nequals neq2
by (metis (no_types, lifting) d_def neq)
hence unsafe2:"ts',move ts ts'' v ⊨ ❙⟨re(c) ❙∧ re(e)❙⟩"
using nequals view.somewhere_leq v'_def by blast
from cr_res.IH have "ts',move ts ts'' v ⊨ ❙¬❙⟨re(c) ❙∧ re(e)❙⟩"
using move_stab by force
thus False using unsafe2 by best
next
assume eq2:"c = d"
hence e_trans:"ts' ❙─r(c) ❙→ ts''" using d_def by simp
from e_def have "ts'',move ts ts'' v ⊨ ❙⟨ re(c) ❙∧ re(e)❙⟩" by auto
hence "∃v'. (v' ≤ move ts ts'' v) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
using view.somewhere_leq
by meson
then obtain v' where v'_def:
"(v' ≤ move ts ts'' v) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
by blast
with backwards_res_act have "ts',v' ⊨ (re(c) ❙∨ cl(c)) ❙∧ re(e)"
using e_def backwards_res_stab nequals
by (metis (no_types, lifting) d_def eq2)
hence "∃v'. (v' ≤ move ts ts'' v) ∧ (ts',v' ⊨ (re(c) ❙∨ cl(c)) ❙∧ (re(e)))"
using v'_def by blast
hence "ts',move ts ts'' v ⊨❙⟨ (re(c) ❙∨ cl(c)) ❙∧ (re(e) ) ❙⟩"
using view.somewhere_leq by meson
hence "ts',move ts ts'' v ⊨ ❙⟨ re(c) ❙∧ re(e)❙⟩ ❙∨ ❙⟨ cl(c) ❙∧ re(e)❙⟩ "
using hmlsl.somewhere_and_or_distr by blast
thus False
proof
assume assm':"ts',move ts ts'' v ⊨ ❙⟨ re(c) ❙∧ re(e)❙⟩"
have "ts',move ts ts'' v ⊨ ❙¬ (c ❙= e)" using nequals by blast
thus False using assm' cr_res.IH e_def move_stab by fastforce
next
assume assm':"ts',move ts ts'' v ⊨ ❙⟨ cl(c) ❙∧ re(e)❙⟩"
hence "ts',move ts ts'' v ⊨ ❙¬ (c ❙=e) ❙∧ ❙⟨ cl(c) ❙∧ re(e)❙⟩"
using e_def nequals by blast
hence "ts',move ts ts'' v ⊨❙¬ (c ❙=e) ❙∧ ❙⟨ cl(c) ❙∧ (re(e) ❙∨ cl(e)) ❙⟩"
by blast
hence pcc:"ts',move ts ts'' v ⊨ pcc e c" by blast
have "ts',move ts ts'' v ⊨( ❙∃ d. pcc d c) ❙→ ❙□r(c) ❙⊥ "
using local_LC move_stab by fastforce
hence "ts',move ts ts'' v ⊨ ❙□r(c) ❙⊥" using pcc by blast
thus "ts'',move ts ts'' v ⊨ ❙⊥" using e_trans by blast
qed
qed
qed
qed
next
case (cr_clm ts' ts'')
have "move ts ts' v = move ts' ts'' (move ts ts' v)"
using traffic.move_stability_clm cr_clm.hyps traffic.move_trans
by auto
hence move_stab: "move ts ts' v = move ts ts'' v"
by (metis traffic.abstract.simps cr_clm.hyps traffic.move_trans)
show ?case
proof (rule)
assume e_def:"(ts'',move ts ts'' v ⊨ ❙⟨re(c) ❙∧ re(e)❙⟩)"
obtain d where d_def: "∃n. (ts' ❙─c(d,n) ❙→ ts'')"
using cr_clm.hyps by blast
from this obtain n where n_def:" (ts' ❙─c(d,n) ❙→ ts'')" by blast
from e_def have "∃v'. (v' ≤ move ts ts'' v) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
using view.somewhere_leq by fastforce
then obtain v' where v'_def:"(v' ≤ move ts ts'' v) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
by blast
then have " (ts',v' ⊨ re(c) ❙∧ re(e))"
using n_def backwards_c_res_stab by blast
then have "ts', move ts ts'' v ⊨ ❙⟨re(c) ❙∧ re(e)❙⟩"
using v'_def view.somewhere_leq by meson
thus False using cr_clm.IH move_stab e_def nequals by fastforce
qed
next
case (wd_res ts' ts'')
have "move ts ts' v = move ts' ts'' (move ts ts' v)"
using traffic.move_stability_wdr wd_res.hyps traffic.move_trans
by auto
hence move_stab: "move ts ts' v = move ts ts'' v"
by (metis traffic.abstract.simps wd_res.hyps traffic.move_trans)
show ?case
proof (rule )
assume e_def: " (ts'',move ts ts'' v ⊨ ❙⟨re(c) ❙∧ re(e)❙⟩)"
obtain d where d_def:"∃n. (ts' ❙─wdr(d,n) ❙→ ts'')"
using wd_res.hyps by blast
from this obtain n where n_def:" (ts' ❙─wdr(d,n) ❙→ ts'')" by blast
from e_def have "∃v'. (v' ≤ move ts ts'' v) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
using view.somewhere_leq by fastforce
then obtain v' where v'_def:"(v' ≤ move ts ts'' v) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
by blast
then have " (ts',v' ⊨ re(c) ❙∧ re(e))"
using n_def backwards_wdr_res_stab by blast
then have " (ts',move ts ts'' v ⊨ ❙⟨re(c) ❙∧ re(e)❙⟩)"
using v'_def view.somewhere_leq by meson
thus False using wd_res.IH move_stab by fastforce
qed
next
case (wd_clm ts' ts'')
have "move ts ts' v = move ts' ts'' (move ts ts' v)"
using traffic.move_stability_wdc wd_clm.hyps traffic.move_trans
by auto
hence move_stab: "move ts ts' v = move ts ts'' v"
by (metis traffic.abstract.simps wd_clm.hyps traffic.move_trans)
show ?case
proof (rule)
assume e_def: " (ts'',move ts ts'' v ⊨ ❙⟨re(c) ❙∧ re(e) ❙⟩)"
obtain d where d_def: " (ts' ❙─wdc(d) ❙→ ts'')"
using wd_clm.hyps by blast
from e_def have "∃v'. (v' ≤ move ts ts'' v) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
using view.somewhere_leq by fastforce
then obtain v' where v'_def:"(v' ≤ move ts ts'' v) ∧ (ts'',v' ⊨ re(c) ❙∧ re(e))"
by blast
then have " (ts',v' ⊨ re(c) ❙∧ re(e))"
using d_def backwards_wdc_res_stab by blast
hence "ts',move ts ts'' v ⊨ ❙⟨re(c) ❙∧ re(e)❙⟩"
using v'_def view.somewhere_leq by meson
thus False using wd_clm.IH move_stab by fastforce
qed
qed
qed
text‹
While the safety theorem was only proven for a single car, we can
show that the choice of this car is irrelevant. That is, if we have
a safe situation, and switch the perspective to another car,
the resulting situation is also safe.
›
lemma safety_switch_invariant:"⊨(❙∀e. safe(e)) ❙→ ❙@c (❙∀e. safe(e))"
proof (rule allI|rule impI)+
fix ts v v'
fix e d :: cars
assume assm: "ts,v ⊨ ❙∀e. safe(e)"
and v'_def:"(v=c>v')"
and nequals:"ts,v ⊨ ❙¬(d ❙= e)"
show "ts,v' ⊨ ❙¬ ❙⟨re(d) ❙∧ re(e)❙⟩"
proof(rule)
assume e_def: "ts,v' ⊨ ❙⟨re(d) ❙∧ re(e)❙⟩"
from e_def obtain v'sub where v'sub_def:
"(v'sub ≤ v') ∧ (ts,v'sub ⊨ re(d) ❙∧ re(e))"
using view.somewhere_leq by fastforce
have "own v' = c" using v'_def view.switch_def by auto
hence "own v'sub = c" using v'sub_def less_eq_view_ext_def by auto
obtain vsub where vsub:"(vsub =c> v'sub) ∧ (vsub ≤ v)"
using v'_def v'sub_def view.switch_leq by blast
from v'sub_def and vsub have "ts,vsub ⊨ ❙@c re(d)"
by (metis view.switch_unique)
hence vsub_re_d:"ts,vsub ⊨ re(d)" using at_res_inst by blast
from v'sub_def and vsub have "ts,vsub ⊨ ❙@c re(e)"
by (metis view.switch_unique)
hence vsub_re_e:"ts,vsub ⊨ re(e)" using at_res_inst by blast
hence "ts,vsub⊨re(d) ❙∧ re(e)" using vsub_re_e vsub_re_d by blast
hence "ts,v ⊨❙⟨ re(d) ❙∧ re(e) ❙⟩"
using vsub view.somewhere_leq by fastforce
then show False using assm nequals by blast
qed
qed
end
end