Document Open Access Logo

Strategic Dominance: A New Preorder for Nondeterministic Processes

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

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2024.29.pdf
  • Filesize: 0.91 MB
  • 20 pages

Document Identifiers

Author Details

Thomas A. Henzinger
  • Institute of Science and Technology Austria (ISTA), Klosterneuburg, Austria
Nicolas Mazzocchi
  • Slovak University of Technology in Bratislava, Slovak Republic
  • 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. N. Mazzocchi was affiliated with ISTA when this work was submitted for publication.

Acknowledgements

We thank the anonymous reviewers for their helpful comments.

Cite AsGet BibTex

Thomas A. Henzinger, Nicolas Mazzocchi, and N. Ege Saraç. Strategic Dominance: A New Preorder for Nondeterministic Processes. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CONCUR.2024.29

Abstract

We study the following refinement relation between nondeterministic state-transition models: model ℬ strategically dominates model 𝒜 iff every deterministic refinement of 𝒜 is language contained in some deterministic refinement of ℬ. While language containment is trace inclusion, and the (fair) simulation preorder coincides with tree inclusion, strategic dominance falls strictly between the two and can be characterized as "strategy inclusion" between 𝒜 and ℬ: every strategy that resolves the nondeterminism of 𝒜 is dominated by a strategy that resolves the nondeterminism of ℬ. Strategic dominance can be checked in 2-ExpTime by a decidable first-order Presburger logic with quantification over words and strategies, called resolver logic. We give several other applications of resolver logic, including checking the co-safety, co-liveness, and history-determinism of boolean and quantitative automata, and checking the inclusion between hyperproperties that are specified by nondeterministic boolean and quantitative automata.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
  • Theory of computation → Logic and verification
  • Theory of computation → Program reasoning
Keywords
  • quantitative automata
  • refinement relation
  • resolver
  • strategy
  • history-determinism

Metrics

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

References

  1. 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.
  2. Bowen Alpern and Fred B. Schneider. Recognizing safety and liveness. Distributed Comput., 2(3):117-126, 1987. URL: https://doi.org/10.1007/BF01782772.
  3. Rajeev Alur, Thomas A. Henzinger, Orna Kupferman, and Moshe Y. Vardi. Alternating refinement relations. In Davide Sangiorgi and Robert de Simone, editors, CONCUR '98: Concurrency Theory, 9th International Conference, Nice, France, September 8-11, 1998, Proceedings, volume 1466 of Lecture Notes in Computer Science, pages 163-178. Springer, 1998. URL: https://doi.org/10.1007/BFB0055622.
  4. Ralph-Johan Back and Joakim von Wright. Refinement Calculus - A Systematic Introduction. Graduate Texts in Computer Science. Springer, 1998. URL: https://doi.org/10.1007/978-1-4612-1674-2.
  5. Udi Boker, Thomas A. Henzinger, Nicolas Mazzocchi, and N. Ege Saraç. Safety and liveness of quantitative automata. In Guillermo A. Pérez and Jean-François Raskin, editors, 34th International Conference on Concurrency Theory, CONCUR 2023, September 18-23, 2023, Antwerp, Belgium, volume 279 of LIPIcs, pages 17:1-17:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.CONCUR.2023.17.
  6. Udi Boker and Karoliina Lehtinen. History determinism vs. good for gameness in quantitative automata. In Mikolaj Bojanczyk and Chandra Chekuri, editors, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2021, December 15-17, 2021, Virtual Conference, volume 213 of LIPIcs, pages 38:1-38:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.FSTTCS.2021.38.
  7. Udi Boker and Karoliina Lehtinen. Token games and history-deterministic quantitative-automata. Log. Methods Comput. Sci., 19(4), 2023. URL: https://doi.org/10.46298/LMCS-19(4:8)2023.
  8. Udi Boker and Karoliina Lehtinen. When a little nondeterminism goes a long way: An introduction to history-determinism. ACM SIGLOG News, 10(1):24-51, 2023. URL: https://doi.org/10.1145/3584676.3584682.
  9. Stephen Brookes. A semantics for concurrent separation logic. Theor. Comput. Sci., 375(1-3):227-270, 2007. URL: https://doi.org/10.1016/J.TCS.2006.12.034.
  10. Krishnendu Chatterjee, Laurent Doyen, Herbert Edelsbrunner, Thomas A. Henzinger, and Philippe Rannou. Mean-payoff automaton expressions. In Paul Gastin and François Laroussinie, editors, CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings, volume 6269 of Lecture Notes in Computer Science, pages 269-283. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15375-4_19.
  11. 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.
  12. Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. Strategy logic. Inf. Comput., 208(6):677-693, 2010. URL: https://doi.org/10.1016/J.IC.2009.07.004.
  13. Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez. Temporal logics for hyperproperties. In Martín Abadi and Steve Kremer, editors, Principles of Security and Trust - Third International Conference, POST 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 8414 of Lecture Notes in Computer Science, pages 265-284. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54792-8_15.
  14. Michael R. Clarkson and Fred B. Schneider. Hyperproperties. J. Comput. Secur., 18(6):1157-1210, 2010. URL: https://doi.org/10.3233/JCS-2009-0393.
  15. Thomas Colcombet. The theory of stabilisation monoids and regular cost functions. In Susanne Albers, Alberto Marchetti-Spaccamela, Yossi Matias, Sotiris E. Nikoletseas, and Wolfgang Thomas, editors, Automata, Languages and Programming, 36th Internatilonal Colloquium, ICALP 2009, Rhodes, Greece, July 5-12, 2009, Proceedings, Part II, volume 5556 of Lecture Notes in Computer Science, pages 139-150. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02930-1_12.
  16. 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.
  17. Nathanaël Fijalkow, Nathalie Bertrand, Patricia Bouyer-Decitre, Romain Brenguier, Arnaud Carayol, John Fearnley, Hugo Gimbert, Florian Horn, Rasmus Ibsen-Jensen, Nicolas Markey, Benjamin Monmege, Petr Novotný, Mickael Randour, Ocan Sankur, Sylvain Schmitz, Olivier Serre, and Mateusz Skomra. Games on graphs. CoRR, abs/2305.10546, 2023. URL: https://doi.org/10.48550/arXiv.2305.10546.
  18. Joseph A. Goguen and José Meseguer. Security policies and security models. In 1982 IEEE Symposium on Security and Privacy, Oakland, CA, USA, April 26-28, 1982, pages 11-20. IEEE Computer Society, 1982. URL: https://doi.org/10.1109/SP.1982.10014.
  19. Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann. A bit of nondeterminism makes pushdown automata expressive and succinct. Log. Methods Comput. Sci., 20(1), 2024. URL: https://doi.org/10.46298/LMCS-20(1:3)2024.
  20. Thomas A. Henzinger, Orna Kupferman, and Sriram K. Rajamani. Fair simulation. Inf. Comput., 173(1):64-81, 2002. URL: https://doi.org/10.1006/INCO.2001.3085.
  21. 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.
  22. Thomas A. Henzinger and Nir Piterman. Solving games without determinization. In Zoltán Ésik, editor, Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, Proceedings, volume 4207 of Lecture Notes in Computer Science, pages 395-410. Springer, 2006. URL: https://doi.org/10.1007/11874683_26.
  23. Denis Kuperberg and Michal Skrzypczak. On determinisation of good-for-games automata. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, volume 9135 of Lecture Notes in Computer Science, pages 299-310. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-47666-6_24.
  24. Christof Löding. Automata on infinite trees. In Jean-Éric Pin, editor, Handbook of Automata Theory, pages 265-302. European Mathematical Society Publishing House, Zürich, Switzerland, 2021. URL: https://doi.org/10.4171/AUTOMATA-1/8.
  25. Fabio Mogavero, Aniello Murano, and Moshe Y. Vardi. Reasoning about strategies. In Kamal Lodaya and Meena Mahajan, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010, December 15-18, 2010, Chennai, India, volume 8 of LIPIcs, pages 133-144. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. URL: https://doi.org/10.4230/LIPICS.FSTTCS.2010.133.
  26. Peter W. O'Hearn. Resources, concurrency, and local reasoning. Theor. Comput. Sci., 375(1-3):271-307, 2007. URL: https://doi.org/10.1016/J.TCS.2006.12.035.
  27. Bruno Scarpellini. Complexity of subcases of presburger arithmetic. Transactions of the American Mathematical Society, 284(1):203-218, 1984. URL: http://www.jstor.org/stable/1999283.
  28. Sanjit A. Seshia, Ankush Desai, Tommaso Dreossi, Daniel J. Fremont, Shromona Ghosh, Edward Kim, Sumukh Shivakumar, Marcell Vazquez-Chanlatte, and Xiangyu Yue. Formal specification for deep neural networks. In Shuvendu K. Lahiri and Chao Wang, editors, Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings, volume 11138 of Lecture Notes in Computer Science, pages 20-34. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-01090-4_2.
  29. Rob J. van Glabbeek. The linear time - branching time spectrum II. In Eike Best, editor, CONCUR '93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings, volume 715 of Lecture Notes in Computer Science, pages 66-81. Springer, 1993. URL: https://doi.org/10.1007/3-540-57208-2_6.
  30. Rob J. van Glabbeek. The linear time - branching time spectrum I. In Jan A. Bergstra, Alban Ponse, and Scott A. Smolka, editors, Handbook of Process Algebra, pages 3-99. North-Holland / Elsevier, 2001. URL: https://doi.org/10.1016/B978-044482830-9/50019-9.
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