Document Open Access Logo

Nested Weighted Limit-Average Automata of Bounded Width

Authors Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2016.24.pdf
  • Filesize: 0.53 MB
  • 14 pages

Document Identifiers

Author Details

Krishnendu Chatterjee
Thomas A. Henzinger
Jan Otop

Cite AsGet BibTex

Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Nested Weighted Limit-Average Automata of Bounded Width. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 24:1-24:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.MFCS.2016.24

Abstract

While weighted automata provide a natural framework to express quantitative properties, many basic properties like average response time cannot be expressed with weighted automata. Nested weighted automata extend weighted automata and consist of a master automaton and a set of slave automata that are invoked by the master automaton. Nested weighted automata are strictly more expressive than weighted automata (e.g., average response time can be expressed with nested weighted automata), but the basic decision questions have higher complexity (e.g., for deterministic automata, the emptiness question for nested weighted automata is PSPACE-hard, whereas the corresponding complexity for weighted automata is PTIME). We consider a natural subclass of nested weighted automata where at any point at most a bounded number k of slave automata can be active. We focus on automata whose master value function is the limit average. We show that these nested weighted automata with bounded width are strictly more expressive than weighted automata (e.g., average response time with no overlapping requests can be expressed with bound k=1, but not with non-nested weighted automata). We show that the complexity of the basic decision problems (i.e., emptiness and universality) for the subclass with k constant matches the complexity for weighted automata. Moreover, when k is part of the input given in unary we establish PSPACE-completeness.
Keywords
  • weighted automata
  • nested weighted automata
  • complexity
  • mean-payoff

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Shaull Almagor, Udi Boker, and Orna Kupferman. Discounting in LTL. In TACAS, 2014, pages 424-439, 2014. Google Scholar
  2. Rajeev Alur, Loris D'Antoni, Jyotirmoy V. Deshmukh, Mukund Raghothaman, and Yifei Yuan. Regular functions and cost register automata. In LICS 2013, pages 13-22, 2013. Google Scholar
  3. Christel Baier, Clemens Dubslaff, and Sascha Klüppelholz. Trade-off analysis meets probabilistic model checking. In CSL-LICS 2014, pages 1:1-1:10, 2014. Google Scholar
  4. Christel Baier, Joachim Klein, Sascha Klüppelholz, and Sascha Wunderlich. Weight monitoring with linear temporal logic: complexity and decidability. In CSL-LICS 2014, pages 11:1-11:10, 2014. Google Scholar
  5. Udi Boker, Krishnendu Chatterjee, Thomas A. Henzinger, and Orna Kupferman. Temporal specifications with accumulative values. ACM TOCL, 15(4):27:1-27:25, 2014. Google Scholar
  6. Benedikt Bollig, Paul Gastin, Benjamin Monmege, and Marc Zeitoun. Pebble weighted automata and transitive closure logics. In ICALP 2010, Part II, pages 587-598. Springer, 2010. Google Scholar
  7. Patricia Bouyer, Nicolas Markey, and Raj Mohan Matteplackel. Averaging in LTL. In CONCUR 2014, pages 266-280, 2014. Google Scholar
  8. Tomás Brázdil, Václav Brozek, Krishnendu Chatterjee, Vojtech Forejt, and Antonín Kucera. Two views on multiple mean-payoff objectives in Markov decision processes. In LICS 2011, pages 33-42, 2011. Google Scholar
  9. Tomás Brázdil, Krishnendu Chatterjee, Vojtech Forejt, and Antonín Kucera. Multigain: A controller synthesis tool for MDPs with multiple mean-payoff objectives. In TACAS 2015, pages 181-187, 2015. Google Scholar
  10. Krishnendu Chatterjee. Markov decision processes with multiple long-run average objectives. In FSTTCS, pages 473-484, 2007. Google Scholar
  11. Krishnendu Chatterjee and Laurent Doyen. Energy and mean-payoff parity Markov Decision Processes. In MFCS 2011, pages 206-218, 2011. Google Scholar
  12. Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Alternating weighted automata. In FCT'09, pages 3-13. Springer, 2009. Google Scholar
  13. Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Expressiveness and closure properties for quantitative languages. LMCS, 6(3), 2010. Google Scholar
  14. Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Quantitative languages. ACM TOCL, 11(4):23, 2010. Google Scholar
  15. Krishnendu Chatterjee, Vojtech Forejt, and Dominik Wojtczak. Multi-objective discounted reward verification in graphs and MDPs. In LPAR, pages 228-242, 2013. Google Scholar
  16. Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Nested weighted automata. In LICS 2015, pages 725-737, 2015. Google Scholar
  17. Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Nested weighted limit-average automata of bounded width. CoRR, abs/1606.03598, 2016. A conference version accepted to MFCS 2016. URL: http://arxiv.org/abs/1606.03598.
  18. Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Quantitative automata under probabilistic semantics. CoRR, abs/1604.06764, 2016. A conference version accepted to LICS 2016. URL: http://arxiv.org/abs/1604.06764.
  19. Krishnendu Chatterjee, Zuzana Komárková, and Jan Kretínský. Unifying two views on multiple mean-payoff objectives in Markov Decision Processes. In LICS 2015, pages 244-256, 2015. Google Scholar
  20. Krishnendu Chatterjee, Rupak Majumdar, and Thomas A. Henzinger. Markov Decision Processes with multiple objectives. In STACS 2006, pages 325-336, 2006. Google Scholar
  21. Manfred Droste, Werner Kuich, and Heiko Vogler. Handbook of Weighted Automata. Springer, 1st edition, 2009. Google Scholar
  22. Manfred Droste and George Rahonis. Weighted automata and weighted logics on infinite words. In DLT 2006, pages 49-58, 2006. Google Scholar
  23. Jerzy Filar and Koos Vrieze. Competitive Markov decision processes. Springer, 1996. Google Scholar
  24. Vojtech Forejt, Marta Z. Kwiatkowska, Gethin Norman, David Parker, and Hongyang Qu. Quantitative multi-objective verification for probabilistic systems. In TACAS, pages 112-127, 2011. Google Scholar
  25. Thomas A. Henzinger and Jan Otop. From model checking to model measuring. In CONCUR 2013, pages 273-287, 2013. Google Scholar
  26. Dexter Kozen. Lower bounds for natural proof systems. In FOCS, pages 254-266. IEEE Computer Society, 1977. Google Scholar
  27. Mehryar Mohri. Semiring frameworks and algorithms for shortest-distance problems. J. Aut. Lang. &Comb., 7(3):321-350, 2002. Google Scholar
  28. Martin L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, 1st edition, 1994. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact