# Theory IO_Automaton

subsection ‹IO automata›
text ‹IO automata are defined. Since they are a particular kind of
transition systems, they inherit the notions of traces and reachability from those.
Various useful concepts and theorems are provided, including
invariants and the multi-step operator.›
theory IO_Automaton
imports Trivia Transition_System
begin
subsubsection ‹IO automata as transition systems›
text ‹In this context, transitions are quadruples consisting of
a source state, an action (input), and output and a target state.›