Document Open Access Logo

Non-deterministic Weighted Automata on Random Words

Authors Jakub Michaliszyn, Jan Otop

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2018.10.pdf
  • Filesize: 474 kB
  • 16 pages

Document Identifiers

Author Details

Jakub Michaliszyn
  • University of Wrocław
Jan Otop
  • University of Wrocław

Cite AsGet BibTex

Jakub Michaliszyn and Jan Otop. Non-deterministic Weighted Automata on Random Words. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.CONCUR.2018.10

Abstract

We present the first study of non-deterministic weighted automata under probabilistic semantics. In this semantics words are random events, generated by a Markov chain, and functions computed by weighted automata are random variables. We consider the probabilistic questions of computing the expected value and the cumulative distribution for such random variables. The exact answers to the probabilistic questions for non-deterministic automata can be irrational and are uncomputable in general. To overcome this limitation, we propose an approximation algorithm for the probabilistic questions, which works in exponential time in the automaton and polynomial time in the Markov chain. We apply this result to show that non-deterministic automata can be effectively determinised with respect to the standard deviation metric.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Quantitative automata
  • Mathematics of computing → Markov networks
Keywords
  • quantitative verification
  • weighted automata
  • expected value

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. What’s decidable about weighted automata? In ATVA, pages 482-491. LNCS 6996, Springer, 2011. Google Scholar
  2. Benjamin Aminof, Orna Kupferman, and Robby Lampert. Reasoning about online algorithms with weighted automata. ACM Transactions on Algorithms (TALG), 6(2):28, 2010. Google Scholar
  3. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  4. Christel Baier, Stefan Kiefer, Joachim Klein, Sascha Klüppelholz, David Müller, and James Worrell. Markov chains and unambiguous büchi automata. In CAV 2016, pages 23-42. Springer, 2016. Google Scholar
  5. Michael Benedikt, Gabriele Puppis, and Cristian Riveros. Regular repair of specifications. In LICS 2011, pages 335-344, 2011. Google Scholar
  6. Udi Boker and Thomas A. Henzinger. Approximate determinization of quantitative automata. In FSTTCS 2012, pages 362-373. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012. Google Scholar
  7. Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. A survey of stochastic games with limsup and liminf objectives. In ICALP 2009, pages 1-15, 2009. Google Scholar
  8. Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Quantitative languages. ACM TOCL, 11(4):23, 2010. Google Scholar
  9. Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Quantitative automata under probabilistic semantics. In LICS 2016, pages 76-85. ACM, 2016. Google Scholar
  10. Krishnendu Chatterjee, Mickael Randour, and Jean-François Raskin. Strategy synthesis for multi-dimensional quantitative objectives. In CONCUR 2012, pages 115-131, 2012. Google Scholar
  11. Edmund Clarke, Thomas Henzinger, Helmut Veith, and Roderick. Bloem. Handbook of Model Checking. Springer International Publishing, 2016. Google Scholar
  12. Costas Courcoubetis and Mihalis Yannakakis. The complexity of probabilistic verification. J. ACM, 42(4):857-907, 1995. Google Scholar
  13. Manfred Droste, Werner Kuich, and Heiko Vogler. Handbook of Weighted Automata. Springer, 1st edition, 2009. Google Scholar
  14. William Feller. An introduction to probability theory and its applications. Wiley, 1971. Google Scholar
  15. Jerzy Filar and Koos Vrieze. Competitive Markov decision processes. Springer, 1996. Google Scholar
  16. Charles Miller Grinstead and James Laurie Snell. Introduction to probability. American Mathematical Soc., 2012. Google Scholar
  17. Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko. Predicate abstraction and refinement for verifying multi-threaded programs. In POPL 2011, pages 331-344, 2011. Google Scholar
  18. Thomas A. Henzinger and Jan Otop. Model measuring for discrete and hybrid systems. Nonlinear Analysis: Hybrid Systems, 23:166-190, 2017. Google Scholar
  19. Andrew Hinton, Marta Z. Kwiatkowska, Gethin Norman, and David Parker. PRISM: A tool for automatic verification of probabilistic systems. In TACAS 2006, pages 441-444, 2006. Google Scholar
  20. Alexander Kechris. Classical descriptive set theory, volume 156. Springer Science &Business Media, 2012. Google Scholar
  21. Daniel Krob. The equality problem for rational series with multiplicities in the tropical semiring is undecidable. Int. J. Algebr. Comput., 4(3):405-426, 1994. URL: http://dx.doi.org/10.1142/S0218196794000063.
  22. Marta Z. Kwiatkowska, Gethin Norman, and David Parker. Quantitative analysis with the probabilistic model checker PRISM. Electr. Notes Theor. Comput. Sci., 153(2):5-31, 2006. Google Scholar
  23. Christos H Papadimitriou. Computational complexity. Wiley, 2003. Google Scholar
  24. Mickael Randour, Jean-François Raskin, and Ocan Sankur. Percentile queries in multi-dimensional markov decision processes. In CAV 2015, pages 123-139, 2015. Google Scholar
  25. Leslie G. Valiant. The complexity of computing the permanent. Theor. Comput. Sci., 8(2):189-201, 1979. Google Scholar
  26. Moshe Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In FOCS 1985, pages 327-338. IEEE Computer Society, 1985. 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