[isabelle] new in the AFP: Transition Systems and Automata; BÃchi Complementation

Two new entries by Julian Brunner are available in the Archive:

Transition Systems and Automata
by Julian Brunner

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.


BÃchi Complementation
by Julian Brunner

This entry provides a verified implementation of rank-based BÃchi Complementation. The verification is done in three steps: 
 â Definition of odd rankings and proof that an automaton rejects a word iff there exists an odd ranking for it.
 â Definition of the complement automaton and proof that it accepts exactly those words for which there is an odd ranking.
 â Verified implementation 



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.