3 citations · 4 across the 12 of their papers we have counts for
15 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 c…
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 compone…
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…
Automating the Analysis of Quantitative Automata with QuAK
Marek Chalupa, Thomas A. Henzinger, Nicolas Mazzocchi +1
Quantitative automata model beyond-boolean aspects of systems: every execution is mapped to a real number by incorporating weighted transitions and value functions that generalize…
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…
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…
Strategic Dominance: A New Preorder for Nondeterministic Processes
Thomas A. Henzinger, Nicolas Mazzocchi, N. Ege Saraç
We study the following refinement relation between nondeterministic state-transition models: model B strategically dominates model A iff every deterministic refinement of A is lang…
Safety and Liveness of Quantitative Properties and Automata
Udi Boker, Thomas A. Henzinger, Nicolas Mazzocchi +1
Safety and liveness stand as fundamental concepts in formal languages, playing a key role in verification. The safety-liveness classification of boolean properties characterizes wh…
Quantitative Safety and Liveness
Thomas A. Henzinger, Nicolas Mazzocchi, N. Ege Saraç
Safety and liveness are elementary concepts of computation, and the foundation of many verification paradigms. The safety-liveness classification of boolean properties characterize…
FORQ-based Language Inclusion Formal Testing
Kyveli Doveri, Pierre Ganty, Nicolas Mazzocchi
We propose a novel algorithm to decide the language inclusion between (nondeterministic) Büchi automata, a PSPACE-complete problem. Our approach, like others before, leverage a not…
Decomposing Permutation Automata
Ismaël Jecker, Nicolas Mazzocchi, Petra Wolf
A deterministic finite automaton (DFA) is composite if its language can be decomposed into an intersection of languages of smaller DFAs. Otherwise, A is prime. This notion of prima…
Two-way Parikh Automata
Emmanuel Filiot, Shibashis Guha, Nicolas Mazzocchi
Parikh automata extend automata with counters whose values can only be tested at the end of the computation, with respect to membership into a semi-linear set. Parikh automata have…
A Pattern Logic for Automata with Outputs
Emmanuel Filiot, Nicolas Mazzocchi, Jean-François Raskin
We introduce a logic to express structural properties of automata with string inputs and, possibly, outputs in some monoid. In this logic, the set of predicates talking about the o…
Decidable Weighted Expressions with Presburger Combinators
Emmanuel Filiot, Nicolas Mazzocchi, Jean-François Raskin
In this paper, we investigate the expressive power and the algorithmic properties of weighted expressions, which define functions from finite words to integers. First, we consider…