Zulip Chat Archive

Stream: Program verification

Topic: Transition Systems


view this post on Zulip Logan Murphy (Sep 04 2020 at 16:05):

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}

view this post on Zulip Simon Hudon (Sep 04 2020 at 16:18):

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

view this post on Zulip Logan Murphy (Sep 04 2020 at 16:20):

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


Last updated: May 08 2021 at 21:09 UTC