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.
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
Quantitative Reactive Modeling; Funder: European Commission; Code: 267989
Modern Graph Algorithmic Techniques in Formal Verification; Funder: Austrian Science Fund (FWF); Code: P 23499
Formal methodes for the design and analysis of complex systems; Funder: Austrian Science Fund (FWF); Code: Z 211
Quantitative Graph Games: Theory and Applications; Funder: European Commission; Code: 279307
Bibliographic References
2 Documents citing this article
Krishnendu Chatterjee;Thomas A. Henzinger;Jan Otop, 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, Nested Weighted Limit-Average Automata of Bounded Width, 58, pp. 14-, 2016, 10.4230/lipics.mfcs.2016.24.