Document Open Access Logo

Black-Box Testing Liveness Properties of Partially Observable Stochastic Systems

Authors Javier Esparza , Vincent P. Grande

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2023.126.pdf
  • Filesize: 0.96 MB
  • 17 pages

Document Identifiers

Author Details

Javier Esparza
  • Technische Universiät München, Germany
Vincent P. Grande
  • RWTH Aachen University, Germany

Funding

  • Esparza, Javier: Partially funded by the smaller{DFG} within Research Training Group 2428 smaller{CONVEY}.
  • Grande, Vincent P.: Funded by the smaller{DFG} (German Research Foundation) under Research Training Group 2236/2 smaller{UnRAVeL}.

Acknowledgements

The authors thank the anonymous reviewers for helpful feedback that improved the paper.

Cite AsGet BibTex

Javier Esparza and Vincent P. Grande. Black-Box Testing Liveness Properties of Partially Observable Stochastic Systems. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 126:1-126:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ICALP.2023.126

Abstract

We study black-box testing for stochastic systems and arbitrary ω-regular specifications, explicitly including liveness properties. We are given a finite-state probabilistic system that we can only execute from the initial state. We have no information on the number of reachable states, or on the probabilities; further, we can only partially observe the states. The only action we can take is to restart the system. We design restart strategies guaranteeing that, if the specification is violated with non-zero probability, then w.p.1 the number of restarts is finite, and the infinite run executed after the last restart violates the specification. This improves on previous work that required full observability. We obtain asymptotically optimal upper bounds on the expected number of steps until the last restart. We conduct experiments on a number of benchmarks, and show that our strategies allow one to find violations in Markov chains much larger than the ones considered in previous work.

Subject Classification

ACM Subject Classification
  • Theory of computation → Verification by model checking
Keywords
  • Partially observable Markov chains
  • ω-regular properties
  • black-box testing

Metrics

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

Related Versions

Supplementary Materials

References

  1. Dana Angluin, James Aspnes, Zoë Diamadi, Michael J. Fischer, and René Peralta. Computation in networks of passively mobile finite-state sensors. Distributed Comput., 18(4):235-253, 2006. Google Scholar
  2. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, Cambridge, Massachusetts, 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. Michael Blondin, Javier Esparza, and Stefan Jaax. Peregrine: A tool for the analysis of population protocols. In CAV (1), volume 10981 of Lecture Notes in Computer Science, pages 604-611. Springer, 2018. Google Scholar
  5. Javier Esparza, Martin Helfrich, Stefan Jaax, and Philipp J. Meyer. Peregrine 2.0: Explaining correctness of population protocols through stage graphs. In ATVA, volume 12302 of Lecture Notes in Computer Science, pages 550-556. Springer, 2020. Google Scholar
  6. Javier Esparza, Stefan Kiefer, Jan Kretínský, and Maximilian Weininger. Enforcing ω-regular properties in markov chains by restarting. In CONCUR, volume 203 of LIPIcs, pages 5:1-5:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. Google Scholar
  7. 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
  8. 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
  9. Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, and Matthias Volk. The probabilistic model checker storm. CoRR, abs/2002.07080, 2020. URL: https://arxiv.org/abs/2002.07080.
  10. Marta Z. Kwiatkowska, Gethin Norman, and David Parker. The PRISM benchmark suite. In QEST, pages 203-204. IEEE Computer Society, 2012. Google Scholar
  11. Kim G. Larsen and Axel Legay. On the power of statistical model checking. In ISoLA (2), volume 9953 of Lecture Notes in Computer Science, pages 843-862, 2016. Google Scholar
  12. David Lee and Mihalis Yannakakis. Principles and methods of testing finite state machines-a survey. Proc. IEEE, 84(8):1090-1123, 1996. Google Scholar
  13. Axel Legay, Benoît Delahaye, and Saddek Bensalem. Statistical model checking: An overview. In RV, volume 6418 of Lecture Notes in Computer Science, pages 122-135. Springer, 2010. Google Scholar
  14. 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
  15. Doron A. Peled, Moshe Y. Vardi, and Mihalis Yannakakis. Black box checking. J. Autom. Lang. Comb., 7(2):225-246, 2002. Google Scholar
  16. Fred B. Schneider. Enforceable security policies. ACM Trans. Inf. Syst. Secur., 3(1):30-50, 2000. Google Scholar
  17. Koushik Sen, Mahesh Viswanathan, and Gul Agha. Statistical model checking of black-box probabilistic systems. In CAV, pages 202-215, 2004. URL: https://doi.org/10.1007/978-3-540-27813-9_16.
  18. Koushik Sen, Mahesh Viswanathan, and Gul Agha. On statistical model checking of stochastic systems. In CAV, volume 3576 of Lecture Notes in Computer Science, pages 266-280. Springer, 2005. Google Scholar
  19. Maximilian Weininger. Personal communication, 2022. Google Scholar
  20. Håkan L. S. Younes. Probabilistic verification for "black-box" systems. In CAV, volume 3576 of Lecture Notes in Computer Science, pages 253-265. Springer, 2005. Google Scholar
  21. Håkan L. S. Younes, Edmund M. Clarke, and Paolo Zuliani. Statistical verification of probabilistic properties with unbounded until. In SBMF, volume 6527 of Lecture Notes in Computer Science, pages 144-160. Springer, 2010. Google Scholar
  22. Håkan L. S. Younes and Reid G. Simmons. Probabilistic verification of discrete event systems using acceptance sampling. In CAV, volume 2404 of Lecture Notes in Computer Science, pages 223-235. Springer, 2002. 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