Quantitative Automata under Probabilistic SemanticsArticle
Authors: Krishnendu Chatterjee ; Thomas A. Henzinger ; Jan Otop
NULL##NULL##0000-0002-8804-8011
Krishnendu Chatterjee;Thomas A. Henzinger;Jan Otop
Automata with monitor counters, where the transitions do not depend on
counter values, and nested weighted automata are two expressive
automata-theoretic frameworks for quantitative properties. For a well-studied
and wide class of quantitative functions, we establish that automata with
monitor counters and nested weighted automata are equivalent. We study for the
first time such quantitative automata under probabilistic semantics. We show
that several problems that are undecidable for the classical questions of
emptiness and universality become decidable under the probabilistic semantics.
We present a complete picture of decidability for such automata, and even an
almost-complete picture of computational complexity, for the probabilistic
questions we consider.
Modern Graph Algorithmic Techniques in Formal Verification; Code: P 23499
Formal methodes for the design and analysis of complex systems; Code: Z 211
Quantitative Graph Games: Theory and Applications; Funder: European Commission; Code: 279307
Quantitative Reactive Modeling; Funder: European Commission; Code: 267989
Incentive - LA 2 - 2013; Funder: Fundação para a Ciência e a Tecnologia, I.P.; Code: Incentivo/SAU/LA0002/2013
Incentive - LA 1 - 2013; Funder: Fundação para a Ciência e a Tecnologia, I.P.; Code: Incentivo/SAU/LA0001/2013
Bibliographic References
2 Documents citing this article
Krishnendu Chatterjee;Thomas A. Henzinger;Jan Otop, International Conference on Concurrency Theory, Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States, 171, pp. 22-, 2020, 10.4230/lipics.concur.2020.23.
Krishnendu Chatterjee;Thomas A. Henzinger;Jan Otop, Mathematical Foundations of Computer Science, Nested Weighted Limit-Average Automata of Bounded Width, 58, pp. 14-, 2016, 10.4230/lipics.mfcs.2016.24.