LTL Temporal Operators via ToKripke Type Class

Defines Always (□), Eventually (◇), and Leads (⇒◇) through the ToKripke type class, so that Always sm P, Always psm P, and Always ct P share a single API across StateMachine, product state machines, and continuous-time systems.

Dispatch via ToKripke

When Always x P receives x : α, the ToKripke α State Data instance is resolved and State / Data are determined via outParam. The predicate P : State → Data → Prop is elaborated with its domain pinned down, so lambdas such as fun s d => Q s d have definite domain types and subsequent tactics like omega or simp operate without ambiguity.

Next and Until

Next (◯) and Until (P U Q) depend on the explicit transition structure of StateMachine and do not fit the KripkeStructure abstraction. They live in StateMachineLTL.lean.

@[reducible, inline]

abbrev VerifiedMBSE.Behavior.Always {α State Data : Type} [ToKripke α State Data] (x : α) (P : State → Data → Prop) : Prop

Always (□ P): P s d holds at every reachable (s, d).

Defined as abbrev via the type class so that after intro s d hr the goal lambda β-reduces automatically.

Equations

• VerifiedMBSE.Behavior.Always x P = ∀ (s : State) (d : Data), (VerifiedMBSE.Behavior.ToKripke.toKripke x).reachable s d → P s d

@[reducible, inline]

abbrev VerifiedMBSE.Behavior.Eventually {α State Data : Type} [ToKripke α State Data] (x : α) (P : State → Data → Prop) : Prop

Eventually (◇ P): some reachable (s, d) satisfies P s d.

Equations

• VerifiedMBSE.Behavior.Eventually x P = ∃ (s : State), ∃ (d : Data), (VerifiedMBSE.Behavior.ToKripke.toKripke x).reachable s d ∧ P s d

@[reducible, inline]

abbrev VerifiedMBSE.Behavior.Leads {α State Data : Type} [ToKripke α State Data] (x : α) (P Q : State → Data → Prop) : Prop

Leads (P ⇒ ◇ Q): the weak semantics — at every reachable state satisfying P, a reachable state satisfying Q exists.

Equations

• VerifiedMBSE.Behavior.Leads x P Q = VerifiedMBSE.Behavior.Always x fun (s : State) (d : Data) => P s d → VerifiedMBSE.Behavior.Eventually x Q

theorem VerifiedMBSE.Behavior.always_and {α State Data : Type} [ToKripke α State Data] {x : α} {P Q : State → Data → Prop} (hP : Always x P) (hQ : Always x Q) : Always x fun (s : State) (d : Data) => P s d ∧ Q s d

□ P ∧ □ Q → □(P ∧ Q).

theorem VerifiedMBSE.Behavior.always_implies_eventually {α State Data : Type} [ToKripke α State Data] {x : α} {P : State → Data → Prop} (hne : (ToKripke.toKripke x).NonEmpty) (h : Always x P) : Eventually x P

NonEmpty together with □ P implies ◇ P.

theorem VerifiedMBSE.Behavior.always_leads {α State Data : Type} [ToKripke α State Data] {x : α} {P : State → Data → Prop} : Leads x P P

Leads P P: reflexivity of Leads.