Temporal operators over event-language runs

Branching-time temporal operators, as in CTL, over the runs of an EventLang. Each turns a predicate on configurations into one, by quantifying over the runs from a configuration: over all runs or some run, and over every point of a run or some point.

Operator	CTL	Meaning
AllNext	AX	every successor satisfies S
SomeNext	EX	some successor satisfies S
AllPathsAlways	AG	every reachable configuration satisfies S
SomePathEventually	EF	some reachable configuration satisfies S
AllPathsEventually	AF	every run reaches a configuration satisfying S
SomePathAlways	EG	some infinite run stays in S

EveryStep and SomeStep read the events a step emits rather than the configuration it reaches, and TracesSatisfy the whole trace of every finite run, as a safety property does.

AllPathsEventually is inductive, so every run must actually reach the target: a run that diverges or gets stuck first does not satisfy it. SomePathAlways asks for a diverging sequence ℕ → CfgT that stays in S. TemporalProps relates them to each other and to MustTerminate.

def Strata.Logic.EventLang.Reaches {P : Imperative.PureExpr} {EventT : Type u_2} (EL : EventLang P EventT) (cfg cfg' : EL.CfgT) : Prop

cfg' is reachable from cfg in zero or more steps.

Equations

• EL.Reaches cfg cfg' = ∃ (trace : List EventT), EL.traceStar cfg trace cfg'

def Strata.Logic.EventLang.EveryStep {P : Imperative.PureExpr} {EventT : Type u_2} (EL : EventLang P EventT) (φ : List EventT → Prop) (cfg : EL.CfgT) : Prop

Every step from cfg emits events φ accepts.

Equations

• EL.EveryStep φ cfg = ∀ (emitted : List EventT) (cfg' : EL.CfgT), EL.step cfg emitted cfg' → φ emitted

def Strata.Logic.EventLang.SomeStep {P : Imperative.PureExpr} {EventT : Type u_2} (EL : EventLang P EventT) (φ : List EventT → Prop) (cfg : EL.CfgT) : Prop

Some step from cfg emits events φ accepts.

Equations

• EL.SomeStep φ cfg = ∃ (emitted : List EventT), ∃ (cfg' : EL.CfgT), EL.step cfg emitted cfg' ∧ φ emitted

def Strata.Logic.EventLang.AllNext {P : Imperative.PureExpr} {EventT : Type u_2} (EL : EventLang P EventT) (S : EL.CfgT → Prop) (cfg : EL.CfgT) : Prop

Every successor of cfg satisfies S.

Equations

• EL.AllNext S cfg = ∀ (emitted : List EventT) (cfg' : EL.CfgT), EL.step cfg emitted cfg' → S cfg'

def Strata.Logic.EventLang.SomeNext {P : Imperative.PureExpr} {EventT : Type u_2} (EL : EventLang P EventT) (S : EL.CfgT → Prop) (cfg : EL.CfgT) : Prop

Some successor of cfg satisfies S.

Equations

• EL.SomeNext S cfg = ∃ (emitted : List EventT), ∃ (cfg' : EL.CfgT), EL.step cfg emitted cfg' ∧ S cfg'

def Strata.Logic.EventLang.AllPathsAlways {P : Imperative.PureExpr} {EventT : Type u_2} (EL : EventLang P EventT) (S : EL.CfgT → Prop) (cfg : EL.CfgT) : Prop

Every configuration reachable from cfg satisfies S.

Equations

• EL.AllPathsAlways S cfg = ∀ (cfg' : EL.CfgT), EL.Reaches cfg cfg' → S cfg'

def Strata.Logic.EventLang.SomePathEventually {P : Imperative.PureExpr} {EventT : Type u_2} (EL : EventLang P EventT) (S : EL.CfgT → Prop) (cfg : EL.CfgT) : Prop

Some configuration reachable from cfg satisfies S.

Equations

• EL.SomePathEventually S cfg = ∃ (cfg' : EL.CfgT), EL.Reaches cfg cfg' ∧ S cfg'

inductive Strata.Logic.EventLang.AllPathsEventually {P : Imperative.PureExpr} {EventT : Type u_2} (EL : EventLang P EventT) (S : EL.CfgT → Prop) : EL.CfgT → Prop

Every run from cfg reaches a configuration satisfying S: cfg satisfies it, or cfg can step and every successor reaches one.

• now {P : Imperative.PureExpr} {EventT : Type u_2} {EL : EventLang P EventT} {S : EL.CfgT → Prop} {cfg : EL.CfgT} : S cfg → EL.AllPathsEventually S cfg
• step {P : Imperative.PureExpr} {EventT : Type u_2} {EL : EventLang P EventT} {S : EL.CfgT → Prop} {cfg : EL.CfgT} (progress : ∃ (emitted : List EventT), ∃ (cfg' : EL.CfgT), EL.step cfg emitted cfg') (successors : ∀ (emitted : List EventT) (cfg' : EL.CfgT), EL.step cfg emitted cfg' → EL.AllPathsEventually S cfg') : EL.AllPathsEventually S cfg

def Strata.Logic.EventLang.SomePathAlways {P : Imperative.PureExpr} {EventT : Type u_2} (EL : EventLang P EventT) (S : EL.CfgT → Prop) (cfg : EL.CfgT) : Prop

Some diverging sequence from cfg stays in configurations satisfying S.

Equations

• EL.SomePathAlways S cfg = ∃ (f : EL.Transitions), f 0 = cfg ∧ EL.Diverges f ∧ ∀ (i : Nat), S (f i)

def Strata.Logic.EventLang.TracesSatisfy {P : Imperative.PureExpr} {EventT : Type u_2} (EL : EventLang P EventT) (φ : List EventT → Prop) (cfg : EL.CfgT) : Prop

Every finite trace of a run from cfg satisfies φ.

Equations

• EL.TracesSatisfy φ cfg = ∀ (trace : List EventT) (c : EL.CfgT), EL.traceStar cfg trace c → φ trace