structure EqCheckingAbstractInterpretation.CCS.FiniteLTS (Action : Type u) (State : Type v) [DecidableEq Action] [DecidableEq State] : Type (max u v)

A finite, executable labelled transition system.

• actions : List Action
• states : List State
• next : State → Action → List State

structure EqCheckingAbstractInterpretation.CCS.FiniteLTS.Realizes {Action : Type u} {State : Type v} [DecidableEq Action] [DecidableEq State] {Name : Type w} (lts : FiniteLTS Action State) (env : Env Action Name) (decode : State → CCS Action Name) : Prop

A finite transition system realizes a CCS environment when its transition table enumerates exactly the derivatives of the represented processes.

• actions_nodup : lts.actions.Nodup
• states_nodup : lts.states.Nodup
• action_complete (action : Action) : action ∈ lts.actions
• next_sound (state : State) (action : Action) (target : State) : target ∈ lts.next state action → Deriv env (decode state) action (decode target)
• next_closed (state : State) (action : Action) (target : State) : state ∈ lts.states → target ∈ lts.next state action → target ∈ lts.states
• next_complete (state : State) (action : Action) (process : CCS Action Name) : state ∈ lts.states → Deriv env (decode state) action process → ∃ target ∈ lts.states, target ∈ lts.next state action ∧ decode target = process

def EqCheckingAbstractInterpretation.CCS.FiniteLTS.decodeSet {Action : Type u} {State : Type v} {Name : Type w} (decode : State → CCS Action Name) (competitors : Finset State) : ProcSet Action Name

Interpret a finite competitor list as a predicate on decoded CCS processes.

Equations

• EqCheckingAbstractInterpretation.CCS.FiniteLTS.decodeSet decode competitors process = ∃ state ∈ competitors, decode state = process