Transition Systems

Stream: Program verification

[Logan Murphy]

I've been using the following definitions to represent Labelled Transition Systems and their executions. It's been fine for my needs so far, but it's cumbersome having the valid predicate separate from the inductive definition of execution (no one would never want an invalid execution anyway). I'm hoping to find some way to incorporate the checking that a triple (s, a, s') is in the System's transition relation into the definition of execution, if that makes sense. I'm wondering if anyone here has any idea if this is possible.

import data.set
open set

structure LTS:=
(S : Type)
(A : Type)
(Rel : set (S × A × S))

inductive execution (M : LTS)
| init  :  M.S → execution
| cons  :  M.A × M.S → execution → execution
open execution

def head {M : LTS} (x : execution M) : M.S :=
execution.cases_on x (λ s,s) (λ p x', p.2)

def valid  {M : LTS} : execution M → Prop
| (init s) := true
| (cons p x) := ((head x, p.fst, p.snd) ∈ M.Rel) ∧ (valid x)

notation e ∘ p := cons p e

/-
example LTS:

(s₁) --l₁--> (s₂) --l₂--> (s₃) --l₃--> (s₄)

-/

inductive states
| s₁
| s₂
| s₃
| s₄
open states

inductive labels
| l₁
| l₂
| l₃
| l₄
open labels

@[reducible]
def M1 : LTS :=
LTS.mk states labels {(s₁, l₁, s₂), (s₂, l₂, s₃),  (s₃, l₃, s₄)}

notation e ∘ p := execution.cons p e

@[reducible]
def ex₀ : execution M1 := init s₁
@[reducible]
def ex₁: execution M1 := ex₀ ∘ (l₁, s₂)
@[reducible]
def ex₂: execution M1 := ex₁ ∘ (l₂, s₃)
@[reducible]
def ex₃: execution M1 := ex₂ ∘ (l₃, s₄)

#reduce ex₃

example : valid ex₃ :=
by {repeat {rw valid},repeat {rw head}, simp}

[Simon Hudon]

The simplest would be to define a subtype of valid executions. I think I would go for that one because internally, it allows you to separate definitions from their proofs of validity while exposing an API that bundles the two.

You may prefer to go the route of more dependent definitions. It can be worth exploring especially to understand what a pain an overly dependent definition can be. I would define it as:

inductive execution (M : LTS) : M.S -> Type
| init  (head :  M.S)  : execution head
| cons  (action : M.A) (s s' : M.S) : execution s' -> (s, action, s') \in M.Rel → execution s

def valid_execution (M : LTS) := \Sigma s, execution s

[Logan Murphy]

Somehow making a subtype never even occured to me. Thanks Simon