Document Open Access Logo

Safety and Liveness of Quantitative Automata

Authors Udi Boker , Thomas A. Henzinger , Nicolas Mazzocchi , N. Ege Saraç

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2023.17.pdf
  • Filesize: 0.83 MB
  • 18 pages

Document Identifiers

Author Details

Udi Boker
  • Reichman University, Herzliya, Israel
Thomas A. Henzinger
  • Institute of Science and Technology Austria (ISTA), Klosterneuburg, Austria
Nicolas Mazzocchi
  • Institute of Science and Technology Austria (ISTA), Klosterneuburg, Austria
N. Ege Saraç
  • Institute of Science and Technology Austria (ISTA), Klosterneuburg, Austria

Funding

This work was supported in part by the ERC-2020-AdG 101020093 and the Israel Science Foundation grant 2410/22.

Acknowledgements

We thank Christof Löding for pointing us to some results on {{PSpace}-hard}ess of universality problems and the anonymous reviewers for their helpful comments.

Cite AsGet BibTex

Udi Boker, Thomas A. Henzinger, Nicolas Mazzocchi, and N. Ege Saraç. Safety and Liveness of Quantitative Automata. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 17:1-17:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CONCUR.2023.17

Abstract

The safety-liveness dichotomy is a fundamental concept in formal languages which plays a key role in verification. Recently, this dichotomy has been lifted to quantitative properties, which are arbitrary functions from infinite words to partially-ordered domains. We look into harnessing the dichotomy for the specific classes of quantitative properties expressed by quantitative automata. These automata contain finitely many states and rational-valued transition weights, and their common value functions Inf, Sup, LimInf, LimSup, LimInfAvg, LimSupAvg, and DSum map infinite words into the totally-ordered domain of real numbers. In this automata-theoretic setting, we establish a connection between quantitative safety and topological continuity and provide an alternative characterization of quantitative safety and liveness in terms of their boolean counterparts. For all common value functions, we show how the safety closure of a quantitative automaton can be constructed in PTime, and we provide PSpace-complete checks of whether a given quantitative automaton is safe or live, with the exception of LimInfAvg and LimSupAvg automata, for which the safety check is in ExpSpace. Moreover, for deterministic Sup, LimInf, and LimSup automata, we give PTime decompositions into safe and live automata. These decompositions enable the separation of techniques for safety and liveness verification for quantitative specifications.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Quantitative automata
Keywords
  • quantitative safety
  • quantitative liveness
  • quantitative automata

Metrics

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

Related Versions

References

  1. Shaull Almagor, Udi Boker, and Orna Kupferman. Discounting in LTL. In Erika Ábrahám and Klaus Havelund, editors, Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings, volume 8413 of Lecture Notes in Computer Science, pages 424-439. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54862-8_37.
  2. Bowen Alpern and Fred B. Schneider. Defining liveness. Inf. Process. Lett., 21(4):181-185, 1985. URL: https://doi.org/10.1016/0020-0190(85)90056-0.
  3. Bowen Alpern and Fred B. Schneider. Recognizing safety and liveness. Distributed Comput., 2(3):117-126, 1987. URL: https://doi.org/10.1007/BF01782772.
  4. Suguman Bansal and Moshe Y. Vardi. Safety and co-safety comparator automata for discounted-sum inclusion. In Isil Dillig and Serdar Tasiran, editors, Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I, volume 11561 of Lecture Notes in Computer Science, pages 60-78. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-25540-4_4.
  5. Roderick Bloem, Krishnendu Chatterjee, Thomas A. Henzinger, and Barbara Jobstmann. Better quality in synthesis through quantitative objectives. In Ahmed Bouajjani and Oded Maler, editors, Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, volume 5643 of Lecture Notes in Computer Science, pages 140-156. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02658-4_14.
  6. Roderick Bloem, Krishnendu Chatterjee, and Barbara Jobstmann. Graph games and reactive synthesis. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 921-962. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_27.
  7. Udi Boker. Quantitative vs. weighted automata. In Proc. of Reachbility Problems, pages 1-16, 2021. Google Scholar
  8. Udi Boker and Karoliina Lehtinen. Token games and history-deterministic quantitative automata. In Patricia Bouyer and Lutz Schröder, editors, Foundations of Software Science and Computation Structures - 25th International Conference, FOSSACS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, volume 13242 of Lecture Notes in Computer Science, pages 120-139. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99253-8_7.
  9. Patricia Bouyer, Nicolas Markey, Mickael Randour, Kim G. Larsen, and Simon Laursen. Average-energy games. Acta Informatica, 55(2):91-127, 2018. URL: https://doi.org/10.1007/s00236-016-0274-1.
  10. Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Quantitative languages. ACM Trans. Comput. Log., 11(4):23:1-23:38, 2010. URL: https://doi.org/10.1145/1805950.1805953.
  11. Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Quantitative monitor automata. In Xavier Rival, editor, Static Analysis - 23rd International Symposium, SAS 2016, Edinburgh, UK, September 8-10, 2016, Proceedings, volume 9837 of Lecture Notes in Computer Science, pages 23-38. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-53413-7_2.
  12. Loris D'Antoni, Roopsha Samanta, and Rishabh Singh. Qlose: Program repair with quantitative objectives. In Swarat Chaudhuri and Azadeh Farzan, editors, Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II, volume 9780 of Lecture Notes in Computer Science, pages 383-401. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-41540-6_21.
  13. Luca de Alfaro, Marco Faella, and Mariëlle Stoelinga. Linear and branching metrics for quantitative transition systems. In Josep Díaz, Juhani Karhumäki, Arto Lepistö, and Donald Sannella, editors, Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, Turku, Finland, July 12-16, 2004. Proceedings, volume 3142 of Lecture Notes in Computer Science, pages 97-109. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-27836-8_11.
  14. Luca de Alfaro, Thomas A. Henzinger, and Rupak Majumdar. Discounting the future in systems theory. In Jos C. M. Baeten, Jan Karel Lenstra, Joachim Parrow, and Gerhard J. Woeginger, editors, Automata, Languages and Programming, 30th International Colloquium, ICALP 2003, Eindhoven, The Netherlands, June 30 - July 4, 2003. Proceedings, volume 2719 of Lecture Notes in Computer Science, pages 1022-1037. Springer, 2003. URL: https://doi.org/10.1007/3-540-45061-0_79.
  15. Aldric Degorre, Laurent Doyen, Raffaella Gentilini, Jean-François Raskin, and Szymon Torunczyk. Energy and mean-payoff games with imperfect information. In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6247 of Lecture Notes in Computer Science, pages 260-274. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15205-4_22.
  16. Volker Diekert and Martin Leucker. Topology, monitorable properties and runtime verification. Theor. Comput. Sci., 537:29-41, 2014. URL: https://doi.org/10.1016/j.tcs.2014.02.052.
  17. Uli Fahrenberg. A generic approach to quantitative verification. CoRR, abs/2204.11302, 2022. URL: https://doi.org/10.48550/arXiv.2204.11302.
  18. Thomas Ferrère, Thomas A. Henzinger, and N. Ege Saraç. A theory of register monitors. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 394-403. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209194.
  19. Theodore W Gamelin and Robert Everist Greene. Introduction to topology. Courier Corporation, 1999. Google Scholar
  20. Felipe Gorostiaga and César Sánchez. Monitorability of expressive verdicts. In Jyotirmoy V. Deshmukh, Klaus Havelund, and Ivan Perez, editors, NASA Formal Methods - 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24-27, 2022, Proceedings, volume 13260 of Lecture Notes in Computer Science, pages 693-712. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-06773-0_37.
  21. K. Hashiguchi. Limitedness theorem on finite automata with distance functions. Journal of computer and system sciences, 24(2):233-244, 1982. Google Scholar
  22. K. Hashiguchi. New upper bounds to the limitedness of distance automata. Theoretical Computer Science, 233(1-2):19-32, 2000. Google Scholar
  23. Thomas A. Henzinger. Quantitative reactive modeling and verification. Comput. Sci. Res. Dev., 28(4):331-344, 2013. URL: https://doi.org/10.1007/s00450-013-0251-7.
  24. Thomas A. Henzinger, Nicolas Mazzocchi, and N. Ege Saraç. Abstract monitors for quantitative specifications. In Thao Dang and Volker Stolz, editors, Runtime Verification - 22nd International Conference, RV 2022, Tbilisi, Georgia, September 28-30, 2022, Proceedings, volume 13498 of Lecture Notes in Computer Science, pages 200-220. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-17196-3_11.
  25. Thomas A. Henzinger, Nicolas Mazzocchi, and N. Ege Saraç. Quantitative safety and liveness. In Orna Kupferman and Pawel Sobocinski, editors, Foundations of Software Science and Computation Structures - 26th International Conference, FoSSaCS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, volume 13992 of Lecture Notes in Computer Science, pages 349-370. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30829-1_17.
  26. Thomas A. Henzinger and N. Ege Saraç. Quantitative and approximate monitoring. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-14. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470547.
  27. Hendrik Jan Hoogeboom and Grzegorz Rozenberg. Infinitary languages: Basic theory an applications to concurrent systems. In J. W. de Bakker, Willem P. de Roever, and Grzegorz Rozenberg, editors, Current Trends in Concurrency, Overviews and Tutorials, volume 224 of Lecture Notes in Computer Science, pages 266-342. Springer, 1986. URL: https://doi.org/10.1007/BFb0027043.
  28. D. B. Johnson. Efficient algorithms for shortest paths in sparse networks. Journal of the ACM (JACM), 24(1):1-13, 1977. Google Scholar
  29. Orna Kupferman and Moshe Y. Vardi. Model checking of safety properties. Formal Methods Syst. Des., 19(3):291-314, 2001. URL: https://doi.org/10.1023/A:1011254632723.
  30. Leslie Lamport. Proving the correctness of multiprocess programs. IEEE Trans. Software Eng., 3(2):125-143, 1977. URL: https://doi.org/10.1109/TSE.1977.229904.
  31. H. Leung and V. Podolskiy. The limitedness problem on distance automata: Hashiguchi’s method revisited. Theoretical Computer Science, 310(1-3):147-158, 2004. Google Scholar
  32. Yongming Li, Manfred Droste, and Lihui Lei. Model checking of linear-time properties in multi-valued systems. Inf. Sci., 377:51-74, 2017. URL: https://doi.org/10.1016/j.ins.2016.10.030.
  33. Dejan Nickovic, Olivier Lebeltel, Oded Maler, Thomas Ferrère, and Dogan Ulus. AMT 2.0: qualitative and quantitative trace analysis with extended signal temporal logic. Int. J. Softw. Tools Technol. Transf., 22(6):741-758, 2020. URL: https://doi.org/10.1007/s10009-020-00582-z.
  34. Doron Peled and Klaus Havelund. Refining the safety-liveness classification of temporal properties according to monitorability. In Tiziana Margaria, Susanne Graf, and Kim G. Larsen, editors, Models, Mindsets, Meta: The What, the How, and the Why Not? - Essays Dedicated to Bernhard Steffen on the Occasion of His 60th Birthday, volume 11200 of Lecture Notes in Computer Science, pages 218-234. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-22348-9_14.
  35. Marcel Paul Schützenberger. On the definition of a family of automata. Inf. Control., 4(2-3):245-270, 1961. URL: https://doi.org/10.1016/S0019-9958(61)80020-X.
  36. I. Simon. On semigroups of matrices over the tropical semiring. RAIRO-Theoretical Informatics and Applications, 28(3-4):277-294, 1994. Google Scholar
  37. A. Prasad Sistla. Safety, liveness and fairness in temporal logic. Formal Aspects Comput., 6(5):495-512, 1994. URL: https://doi.org/10.1007/BF01211865.
  38. Sigal Weiner, Matan Hasson, Orna Kupferman, Eyal Pery, and Zohar Shevach. Weighted safety. In Dang Van Hung and Mizuhito Ogawa, editors, Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings, volume 8172 of Lecture Notes in Computer Science, pages 133-147. Springer, 2013. URL: https://doi.org/10.1007/978-3-319-02444-8_11.
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