Enforcing ω-Regular Properties in Markov Chains by Restarting

Authors Javier Esparza, Stefan Kiefer, Jan Křetínský, Maximilian Weininger



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2021.5.pdf
  • Filesize: 0.8 MB
  • 22 pages

Document Identifiers

Author Details

Javier Esparza
  • Technische Universität München, Germany
Stefan Kiefer
  • University of Oxford, UK
Jan Křetínský
  • Technische Universität München, Germany
Maximilian Weininger
  • Technische Universität München, Germany

Cite As Get BibTex

Javier Esparza, Stefan Kiefer, Jan Křetínský, and Maximilian Weininger. Enforcing ω-Regular Properties in Markov Chains by Restarting. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.CONCUR.2021.5

Abstract

Restarts are used in many computer systems to improve performance. Examples include reloading a webpage, reissuing a request, or restarting a randomized search. The design of restart strategies has been extensively studied by the performance evaluation community. In this paper, we address the problem of designing universal restart strategies, valid for arbitrary finite-state Markov chains, that enforce a given ω-regular property while not knowing the chain. A strategy enforces a property φ if, with probability 1, the number of restarts is finite, and the run of the Markov chain after the last restart satisfies φ. We design a simple "cautious" strategy that solves the problem, and a more sophisticated "bold" strategy with an almost optimal number of restarts.

Subject Classification

ACM Subject Classification
  • Theory of computation → Verification by model checking
Keywords
  • Markov chains
  • omega-regular properties
  • runtime enforcement

Metrics

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

References

  1. Pranav Ashok, Jan Kretínský, and Maximilian Weininger. PAC statistical model checking for Markov decision processes and stochastic games. In CAV (1), volume 11561 of Lecture Notes in Computer Science, pages 497-519. Springer, 2019. Google Scholar
  2. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  3. David A. Basin, Vincent Jugé, Felix Klaedtke, and Eugen Zalinescu. Enforceable security policies revisited. ACM Trans. Inf. Syst. Secur., 16(1):3:1-3:26, 2013. Google Scholar
  4. Hugo Bazille, Blaise Genest, Cyrille Jégourel, and Jun Sun. Global PAC bounds for learning discrete time Markov chains. In CAV (2), volume 12225 of Lecture Notes in Computer Science, pages 304-326. Springer, 2020. Google Scholar
  5. Yingke Chen, Hua Mao, Manfred Jaeger, Thomas Dyhre Nielsen, Kim Guldstrand Larsen, and Brian Nielsen. Learning Markov models for stationary system behaviors. In NASA Formal Methods, volume 7226 of Lecture Notes in Computer Science, pages 216-230. Springer, 2012. Google Scholar
  6. Przemyslaw Daca, Thomas A. Henzinger, Jan Kretínský, and Tatjana Petrov. Faster statistical model checking for unbounded temporal properties. ACM Trans. Comput. Log., 18(2):12:1-12:25, 2017. Google Scholar
  7. Tadashi Dohi, Kishor Trivedi, and Alberto Avritzer, editors. Handbook of Software Aging and Rejuvenation. World Scientific, 2020. Google Scholar
  8. Yliès Falcone, Laurent Mounier, Jean-Claude Fernandez, and Jean-Luc Richier. Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Formal Methods Syst. Des., 38(3):223-262, 2011. Google Scholar
  9. Yliès Falcone and Srinivas Pinisetty. On the runtime enforcement of timed properties. In RV, volume 11757 of Lecture Notes in Computer Science, pages 48-69. Springer, 2019. Google Scholar
  10. Matteo Gagliolo and Jürgen Schmidhuber. Learning restart strategies. In IJCAI, pages 792-797, 2007. Google Scholar
  11. Kalpana Gondi, Yogeshkumar Patel, and A. Prasad Sistla. Monitoring the full range of omega-regular properties of stochastic systems. In VMCAI, volume 5403 of Lecture Notes in Computer Science, pages 105-119. Springer, 2009. Google Scholar
  12. Yennun Huang, Chandra M. R. Kintala, Nick Kolettis, and N. Dudley Fulton. Software rejuvenation: Analysis, module and applications. In FTCS, pages 381-390. IEEE Computer Society, 1995. Google Scholar
  13. Thomas Jansen. On the analysis of dynamic restart strategies for evolutionary algorithms. In PPSN, volume 2439 of Lecture Notes in Computer Science, pages 33-43. Springer, 2002. Google Scholar
  14. Marta Z. Kwiatkowska, Gethin Norman, and David Parker. Prism 4.0: Verification of probabilistic real-time systems. In CAV, pages 585-591, 2011. Google Scholar
  15. Marta Z. Kwiatkowska, Gethin Norman, and David Parker. The PRISM benchmark suite. In QEST, pages 203-204. IEEE Computer Society, 2012. Google Scholar
  16. Jay Ligatti, Lujo Bauer, and David Walker. Run-time enforcement of nonsafety policies. ACM Trans. Inf. Syst. Secur., 12(3):19:1-19:41, 2009. Google Scholar
  17. Fred B. Schneider. Enforceable security policies. ACM Trans. Inf. Syst. Secur., 3(1):30-50, 2000. Google Scholar
  18. A. Prasad Sistla and Abhigna R. Srinivas. Monitoring temporal properties of stochastic systems. In VMCAI, volume 4905 of Lecture Notes in Computer Science, pages 294-308. Springer, 2008. Google Scholar
  19. A. Prasad Sistla, Milos Zefran, and Yao Feng. Runtime monitoring of stochastic cyber-physical systems with hybrid state. In RV, volume 7186 of Lecture Notes in Computer Science, pages 276-293. Springer, 2011. Google Scholar
  20. Aad P. A. van Moorsel and Katinka Wolter. Analysis of restart mechanisms in software systems. IEEE Trans. Software Eng., 32(8):547-558, 2006. Google Scholar
  21. Jingyi Wang, Jun Sun, Qixia Yuan, and Jun Pang. Should we learn probabilistic models for model checking? A new approach and an empirical study. In FASE, volume 10202 of Lecture Notes in Computer Science, pages 3-21. Springer, 2017. Google Scholar
  22. Katinka Wolter. Stochastic Models for Fault Tolerance - Restart, Rejuvenation and Checkpointing. Springer, 2010. 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