Mean-payoff Automaton Expressions
Krishnendu Chatterjee, Laurent Doyen, Herbert Edelsbrunner and, Thomas A. Henzinger, Philippe Rannou

TL;DR
This paper introduces mean-payoff automaton expressions, a new class of quantitative languages that are robust, closed under key operations, and have decidable decision problems, enhancing the analysis of quantitative automata.
Contribution
It defines a novel class of mean-payoff automaton expressions that overcome the limitations of existing automata classes in robustness and decidability.
Findings
The new class is closed under max, min, sum, and complement operations.
Decision problems are decidable for mean-payoff automaton expressions.
An algorithm to compute the distance between two quantitative languages is presented.
Abstract
Quantitative languages are an extension of boolean languages that assign to each word a real number. Mean-payoff automata are finite automata with numerical weights on transitions that assign to each infinite path the long-run average of the transition weights. When the mode of branching of the automaton is deterministic, nondeterministic, or alternating, the corresponding class of quantitative languages is not robust as it is not closed under the pointwise operations of max, min, sum, and numerical complement. Nondeterministic and alternating mean-payoff automata are not decidable either, as the quantitative generalization of the problems of universality and language inclusion is undecidable. We introduce a new class of quantitative languages, defined by mean-payoff automaton expressions, which is robust and decidable: it is closed under the four pointwise operations, and we show…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
