8 papers
Kofola 1.0: A Modular Approach to Ï-Regular Complementation and Inclusion Checking (Technical Report)
Ondrej Alexaj, VojtÄch Havlena, Lukáš HolÃk +3
We present Kofola, an efficient tool for complementation and inclusion checking of Büchi automata, two central tasks in automata-theoretic verification with applications in model…
Complementing Emerson-Lei Elevator Automata (Technical Report)
Ondrej Alexaj, VojtÄch Havlena, OndÅej Lengál +2
Büchi elevator automata naturally appear in several areas of formal methods as a structural expressibly-equivalent subclass of Büchi automata where every strongly connected compo…
Extending QuAK with Nested Quantitative Automata
Thomas A. Henzinger, Nicolas Mazzocchi, N. Ege Saraç +1
Quantitative automata (QAs) extend finite-state automata on infinite words with weighted transitions to specify quantitative system properties. However, their finite weight sets ru…
Quantitative Language Automata
Thomas A. Henzinger, Pavol Kebis, Nicolas Mazzocchi +1
A quantitative word automaton (QWA) defines a function from infinite words to values. For example, every infinite run of a limit-average QWA A obtains a mean payoff, and every word…
QuAK: Quantitative Automata Kit
Marek Chalupa, Thomas A. Henzinger, Nicolas Mazzocchi +1
System behaviors are traditionally evaluated through binary classifications of correctness, which do not suffice for properties involving quantitative aspects of systems and execut…
Temporal Explorability Games
Pete Austin, Nicolas Mazzocchi, Sougata Bose +1
Temporal graphs extend ordinary graphs with discrete time that affects the availability of edges. We consider solving games played on temporal graphs where one player aims to explo…