|
Transition
Systems
and
Automata
Title: |
Transition Systems and Automata |
Author:
|
Julian Brunner
|
Submission date: |
2017-10-19 |
Abstract: |
This entry provides a very abstract theory of transition systems that
can be instantiated to express various types of automata. A transition
system is typically instantiated by providing a set of initial states,
a predicate for enabled transitions, and a transition execution
function. From this, it defines the concepts of finite and infinite
paths as well as the set of reachable states, among other things. Many
useful theorems, from basic path manipulation rules to coinduction and
run construction rules, are proven in this abstract transition system
context. The library comes with instantiations for DFAs, NFAs, and
Büchi automata. |
BibTeX: |
@article{Transition_Systems_and_Automata-AFP,
author = {Julian Brunner},
title = {Transition Systems and Automata},
journal = {Archive of Formal Proofs},
month = oct,
year = 2017,
note = {\url{https://isa-afp.org/entries/Transition_Systems_and_Automata.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Depends on: |
Collections, DFS_Framework, Gabow_SCC |
Used by: |
Adaptive_State_Counting, Buchi_Complementation, LTL_Master_Theorem, Partial_Order_Reduction |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|