Krishnendu Chatterjee
ABSTRACT
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.
- S. Almagor, U. Boker, and O. Kupferman. Discounting in LTL. In TACAS, 2014, pages 424--439, 2014.Google Scholar
Cross Ref
- R. Alur, L. D'Antoni, J. V. Deshmukh, M. Raghothaman, and Y. Yuan. Regular functions and cost register automata. In LICS 2013, pages 13--22, 2013. Google ScholarDigital Library
- C. Baier and J. Katoen. Principles of model checking. MIT Press, 2008. ISBN 978-0-262-02649-9. Google ScholarDigital Library
- C. Baier, C. Dubslaff, and S. Klüppelholz. Trade-off analysis meets probabilistic model checking. In CSL-LICS 2014, pages 1:1--1:10, 2014. Google ScholarDigital Library
- C. Baier, J. Klein, S. Klüppelholz, and S. Wunderlich. Weight monitoring with linear temporal logic: complexity and decidability. In CSL-LICS 2014, pages 11:1--11:10, 2014. Google ScholarDigital Library
- U. Boker, K. Chatterjee, T. A. Henzinger, and O. Kupferman. Temporal specifications with accumulative values. ACM TOCL, 15(4):27:1--27:25, 2014. Google ScholarDigital Library
- B. Bollig, P. Gastin, B. Monmege, and M. Zeitoun. Pebble weighted automata and transitive closure logics. In ICALP 2010, Part II, pages 587--598. Springer, 2010. Google ScholarDigital Library
- P. Bouyer, N. Markey, and R. M. Matteplackel. Averaging in LTL. In CONCUR 2014, pages 266--280, 2014.Google Scholar
- T. Brázdil, V. Brozek, K. Chatterjee, V. Forejt, and A. Kucera. Two views on multiple mean-payoff objectives in Markov decision processes. In LICS 2011, pages 33--42, 2011. Google ScholarDigital Library
- T. Brázdil, K. Chatterjee, V. Forejt, and A. Kucera. Multigain: A controller synthesis tool for MDPs with multiple mean-payoff objectives. In TACAS 2015, pages 181--187, 2015. Google ScholarDigital Library
- K. Chatterjee. Markov decision processes with multiple long-run average objectives. In FSTTCS, pages 473--484, 2007. Google ScholarDigital Library
- K. Chatterjee and L. Doyen. Energy and mean-payoff parity Markov Decision Processes. In MFCS 2011, pages 206--218, 2011. Google ScholarDigital Library
- K. Chatterjee, R. Majumdar, and T. A. Henzinger. Markov Decision Processes with multiple objectives. In STACS 2006, pages 325--336, 2006. Google ScholarDigital Library
- K. Chatterjee, L. Doyen, and T. A. Henzinger. Alternating weighted automata. In FCT'09, pages 3--13. Springer, 2009. Google ScholarDigital Library
- K. Chatterjee, L. Doyen, and T. A. Henzinger. A survey of stochastic games with limsup and liminf objectives. In ICALP 2009, Part II, pages 1--15, 2009. Google ScholarDigital Library
- K. Chatterjee, L. Doyen, and T. A. Henzinger. Quantitative languages. ACM TOCL, 11(4):23, 2010. Google ScholarDigital Library
- K. Chatterjee, L. Doyen, and T. A. Henzinger. Expressiveness and closure properties for quantitative languages. LMCS, 6(3), 2010.Google Scholar
- K. Chatterjee, V. Forejt, and D. Wojtczak. Multi-objective discounted reward verification in graphs and MDPs. In LPAR, pages 228--242, 2013.Google ScholarCross Ref
- K. Chatterjee, T. A. Henzinger, B. Jobstmann, and R. Singh. Measuring and synthesizing systems in probabilistic environments. J. ACM, 62(1):9:1--9:34, 2015. Google ScholarDigital Library
- K. Chatterjee, T. A. Henzinger, and J. Otop. Nested weighted automata. In LICS 2015, pages 725--737, 2015. Google ScholarDigital Library
- K. Chatterjee, Z. Komárková, and J. Kretínský. Unifying two views on multiple mean-payoff objectives in Markov Decision Processes. In LICS 2015, pages 244--256, 2015. Google ScholarDigital Library
- K. Chatterjee, T. A. Henzinger, and J. Otop. Quantitative automata under probabilistic semantics. CoRR, abs/1604.06764, 2016. URL http://arxiv.org/abs/1604.06764.Google Scholar
- M. Droste and G. Rahonis. Weighted automata and weighted logics on infinite words. In DLT 2006, pages 49--58, 2006. Google ScholarDigital Library
- M. Droste, W. Kuich, and H. Vogler. Handbook of Weighted Automata. Springer, 1st edition, 2009. Google ScholarDigital Library
- W. Feller. An introduction to probability theory and its applications. Wiley, 1971. ISBN 9780471257097.Google Scholar
- J. Filar and K. Vrieze. Competitive Markov decision processes. Springer, 1996. Google ScholarDigital Library
- V. Forejt, M. Z. Kwiatkowska, G. Norman, D. Parker, and H. Qu. Quantitative multi-objective verification for probabilistic systems. In TACAS, pages 112--127, 2011. Google ScholarDigital Library
- A. Hinton, M. Z. Kwiatkowska, G. Norman, and D. Parker. PRISM: A tool for automatic verification of probabilistic systems. In TACAS 2006, pages 441--444, 2006. Google ScholarDigital Library
- M. Mohri. Semiring frameworks and algorithms for shortest-distance problems. J. Aut. Lang. & Comb., 7(3):321--350, 2002. Google ScholarDigital Library
- C. H. Papadimitriou. Computational complexity. Wiley, 2003.Google Scholar
- M. L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, 1st edition, 1994. Google ScholarDigital Library
- L. G. Valiant. The complexity of computing the permanent. Theoretical computer science, 8(2):189--201, 1979.Google Scholar
Index Terms
- Quantitative Automata under Probabilistic Semantics
Recommendations
Nested Weighted Automata
Recently there has been a significant effort to handle quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, ...
Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics
QEST '08: Proceedings of the 2008 Fifth International Conference on Quantitative Evaluation of SystemsIn [BBBBG08] a probabilistic semantics for timed automata has been defined in order to rule out unlikely (sequences of) events. The qualitative model-checking problem for LTL properties has been investigated, where the aim is to check whether a given ...
Quantitative vs. Weighted Automata
Reachability ProblemsAbstractWeighted automata are widely researched, but with a variety of different semantics, which mostly fit into either the “quantitative view” or the “algebraic view”. We argue that the two views result with incomparable automata families, each ...
Comments