General (infinite-state) transition systems are defined using records. This makes it possible to define intersection and renaming operations on the transition systems, which we call state-machines, and these operations have nice properties. We define notions such as reachable states, invariants, stable properties, etc. and prove theorems about their preservation under intersection and renaming.

IO-Automata provide a syntax for state-machines and we define this syntax and the meaning functions that give the semantics of IO-Automata as state machines. We also provide a syntax for a specification logic and a verification-generation algorithm that produces conditions sufficient for a given formula in our logic to be an invariant of an IO-Automaton. The VC-generation algorithm is proved correct.

mb automata 4
mb automata 3
mb automata 2
mb hybrid
mb automata 1
mb structures
mb list 2	More list stuff.
mb state machine	General transition systems and operations such as intersection and renaming.
mb events
mb record	Definitions of records and the dual sigma types and their properties.
mb declaration	Declarations are assignments of types to labels.
mb label	Labels are patterns without variables in them, ie ground patterns.
mb list 1	Filter, initial-segment, list-member, interleaving, etc. Lemmas related to map, append, cons, select.
mb nat
mb basic	Generally useful devices.
mb tree	Binary Trees.
mb collection	Collections as properties of objects.