Labeled Transition Systems

Anders Schlichtkrull 🌐, Morten Konggaard Schou, Jiří Srba 🌐 and Dmitriy Traytel 🌐

October 31, 2023

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

Labeled transition systems are ubiquitous in computer science. They are used e.g. for automata and for program graphs in program analysis. We formalize labeled transition systems with and without epsilon transitions. The main difference between formalizations of labeled transition systems is in their choice of how to represent the transition system. In the present formalization the set of nodes is a type, and a labeled transition system is represented as a locale fixing a set of transitions where each transition is a triple of respectively a start node, a label and an end node. Wimmer [Wim20] provides an overview of formalizations of graphs and transition systems.

[Wim20] Simon Wimmer. Archive of graph formalizations. 2020. https://github.com/wimmers/archive-of-graph-formalizations.

License

BSD License

Topics

Related publications

Session Labeled_Transition_Systems

Depends on

Used by

Cite

× 
@article{Labeled_Transition_Systems-AFP,
  author  = {Anders Schlichtkrull and Morten Konggaard Schou and Jiří Srba and Dmitriy Traytel},
  title   = {Labeled Transition Systems},
  journal = {Archive of Formal Proofs},
  month   = {October},
  year    = {2023},
  note    = {\url{https://isa-afp.org/entries/Labeled_Transition_Systems.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: