### 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.

### License

BSD License

### Topics

- Computer science/Automata and formal languages

### Session Transition_Systems_and_Automata

- Basic
- Sequence
- Sequence_LTL
- Sequence_Zip
- Maps
- Acceptance
- Degeneralization
- Transition_System
- Transition_System_Extra
- Transition_System_Construction
- Deterministic
- DFA
- Nondeterministic
- NFA
- DBA
- DGBA
- DBA_Combine
- DBTA
- DGBTA
- DBTA_Combine
- DCA
- DGCA
- DCA_Combine
- DRA
- DRA_Combine
- Refine
- Acceptance_Refine
- Transition_System_Refine
- DRA_Refine
- Implement
- DRA_Implement
- DRA_Nodes
- DRA_Explicit
- DRA_Translate
- NBA
- NGBA
- NBA_Combine
- NBA_Graphs
- NBA_Refine
- NBA_Implement
- NBA_Algorithms
- NBA_Explicit
- NBA_Translate
- NGBA_Graphs
- NGBA_Refine
- NGBA_Implement
- Degeneralization_Refine
- NGBA_Algorithms
- NBTA
- NGBTA
- NBTA_Combine

### Depends on

- Collections Framework
- A Framework for Verifying Depth-First Search Algorithms
- Verified Efficient Implementation of Gabow’s Strongly Connected Components Algorithm

### Used by

- Formalisation of an Adaptive State Counting Algorithm
- A Compositional and Unified Translation of LTL into ω-Automata
- Partial Order Reduction
- Büchi Complementation

### Auto-related entries

- Labeled Transition Systems
- Promela Formalization

## Cite

×

Transition_Systems_and_Automata-AFP

    @article{Transition_Systems_and_Automata-AFP,
      author  = {Julian Brunner},
      title   = {Transition Systems and Automata},
      journal = {Archive of Formal Proofs},
      month   = {October},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/Transition_Systems_and_Automata.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 27, 2017 : Isabelle2017