Krishnendu Chatterjee ; Thomas A. Henzinger ; Jan Otop - Quantitative Automata under Probabilistic Semantics

lmcs:4512 - Logical Methods in Computer Science, August 13, 2019, Volume 15, Issue 3 - https://doi.org/10.23638/LMCS-15(3:16)2019
Quantitative Automata under Probabilistic SemanticsArticle

Authors: Krishnendu Chatterjee ; Thomas A. Henzinger ; Jan Otop ORCID

    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.


    Volume: Volume 15, Issue 3
    Published on: August 13, 2019
    Accepted on: July 24, 2019
    Submitted on: May 16, 2018
    Keywords: Computer Science - Formal Languages and Automata Theory
    Funding:
      Source : OpenAIRE Graph
    • 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

    2 Documents citing this article

    Consultation statistics

    This page has been seen 1659 times.
    This article's PDF has been downloaded 339 times.