Email Gateway (Aug 22 2022 at 16:20): Email Gateway (Aug 22 2022 at 16:20):From: Gerwin.Klein@data61.csiro.au
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.
https://www.isa-afp.org/entries/Transition_Systems_and_Automata.html
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
https://www.isa-afp.org/entries/Buchi_Complementation.html
Enjoy!
Gerwin
Last updated: Apr 19 2024 at 20:15 UTC