Document Open Access Logo

Partial Order Reduction for Reachability Games

Authors Frederik Meyer Bønneland, Peter Gjøl Jensen , Kim G. Larsen, Marco Muñiz , Jiří Srba

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2019.23.pdf
  • Filesize: 0.55 MB
  • 15 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Algorithmic game theory
Keywords
  • Petri nets
  • games
  • synthesis
  • partial order reduction
  • stubborn sets

Metrics

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

Abstract

Partial order reductions have been successfully applied to model checking of concurrent systems and practical applications of the technique show nontrivial reduction in the size of the explored state space. We present a theory of partial order reduction based on stubborn sets in the game-theoretical setting of 2-player games with reachability/safety objectives. Our stubborn reduction allows us to prune the interleaving behaviour of both players in the game, and we formally prove its correctness on the class of games played on general labelled transition systems. We then instantiate the framework to the class of weighted Petri net games with inhibitor arcs and provide its efficient implementation in the model checker TAPAAL. Finally, we evaluate our stubborn reduction on several case studies and demonstrate its efficiency.

Cite As Get BibTex

Frederik Meyer Bønneland, Peter Gjøl Jensen, Kim G. Larsen, Marco Muñiz, and Jiří Srba. Partial Order Reduction for Reachability Games. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 23:1-23:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.CONCUR.2019.23

Author Details

Frederik Meyer Bønneland
  • Department of Computer Science, Aalborg University, Denmark
Peter Gjøl Jensen
  • Department of Computer Science, Aalborg University, Denmark
Kim G. Larsen
  • Department of Computer Science, Aalborg University, Denmark
Marco Muñiz
  • Department of Computer Science, Aalborg University, Denmark
Jiří Srba
  • Department of Computer Science, Aalborg University, Denmark

Funding

The research leading to these results has received funding from the project DiCyPS funded by the Innovation Fund Denmark and the ERC Advanced Grant LASSO. The last author is partially affiliated with FI MU, Brno, Czech Republic.

References

  1. N. Alechina, N. Bulling, S. Demri, and B. Logan. On the complexity of resource-bounded logics. In Reachability Problems, volume 9899 of LNCS, pages 36-50. Springer-Verlag, 2016. Google Scholar
  2. B. Bérard, S. Haddad, M. Sassolas, and N. Sznajder. Concurrent Games on VASS with Inhibition. In International Conference on Concurrency Theory, volume 7454 of LNCS, pages 39-52. Springer-Verlag, 2012. Google Scholar
  3. F. M. Bønneland, P. G. Jensen, K. G. Larsen, M. Mũniz, and J. Srba. Artifact for "Partial Order Reduction for Reachability Games", June 2019. URL: https://doi.org/10.5281/zenodo.3252104.
  4. F.M. Bønneland, J. Dyhr, P.G. Jensen, M. Johannsen, and J. Srba. Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems. In Computer Aided Verification, volume 10981 of LNCS, pages 527-546. Springer-Verlag, 2018. Google Scholar
  5. A.E. Dalsgaard, S. Enevoldsen, P. Fogh, L.S. Jensen, P.G. Jensen, T.S. Jepsen, I. Kaufmann, K.G. Larsen, S.M. Nielsen, M.Chr. Olesen, S. Pastva, and J. Srba. A Distributed Fixed-Point Algorithm for Extended Dependency Graphs. Fundamenta Informaticae, 161(4):351-381, 2018. URL: https://doi.org/10.3233/FI-2018-1707.
  6. A. David, L. Jacobsen, M. Jacobsen, K.Y. Jørgensen, M.H. Møller, and J. Srba. TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri Nets. In Tools and Algorithms for the Construction and Analysis of Systems, volume 7214 of LNCS, pages 492-497. Springer-Verlag, 2012. Google Scholar
  7. R. Davidrajuh. Detecting Existence of Cycles in Petri Nets. In International Joint Conference SOCO'16-CISIS'16-ICEUTE'16, volume 527 of AISC, pages 376-385. Springer-Verlag, 2016. Google Scholar
  8. J. Dehnert and A. Zimmermann. Making Workflow Models Sound Using Petri Net Controller Synthesis. In On the Move to Meaningful Internet Systems 2004: CoopIS, DOA, and ODBASE, volume 3290 of LNCS, pages 139-154. Springer-Verlag, 2004. Google Scholar
  9. M. Huhn, P. Niebert, and H. Wehrheim. Partial Order Reductions for Bisimulation Checking. In Foundations of Software Technology and Theoretical Computer Science, volume 1530 of LNCS, pages 271-282. Springer-Verlag, 1998. Google Scholar
  10. W. Jamroga, W. Penczek, P. Dembiński, and A. Mazurkiewicz. Towards Partial Order Reductions for Strategic Ability. In Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2018, pages 156-165, Richland, SC, 2018. ACM. Google Scholar
  11. E. Javier. Decidability and Complexity of Petri Net Problems - An Introduction, volume 1491 of LNCS, pages 374-428. Springer-Verlag, 1998. Google Scholar
  12. J.F Jensen, T. Nielsen, L.K. Oestergaard, and J. Srba. TAPAAL and Reachability Analysis of P/T Nets. In Transactions on Petri Nets and Other Models of Concurrency XI, volume 9930 of LNCS, pages 307-318. Springer-Verlag, 2016. Google Scholar
  13. P. G. Jensen, K. G. Larsen, and J. Srba. PTrie: Data Structure for Compressing and Storing Sets via Prefix Sharing. In Proceedings of the 14th International Colloquium on Theoretical Aspects of Computing (ICTAC'17), volume 10580 of LNCS, pages 248-265. Springer-Verlag, 2017. URL: https://doi.org/10.1007/978-3-319-67729-3_15.
  14. P.G. Jensen, K.G. Larsen, and J. Srba. Real-Time Strategy Synthesis for Timed-Arc Petri Net Games via Discretization. In International Symposium on Model Checking Software, volume 9641 of LNCS, pages 129-146. Springer-Verlag, 2016. Google Scholar
  15. P.G. Jensen, K.G. Larsen, and J. Srba. Discrete and continuous strategies for timed-arc Petri net games. International Journal on Software Tools for Technology Transfer, 20(5):529-546, October 2018. Google Scholar
  16. P. Kasting, M.R. Hansen, and S. Vester. Synthesis of Railway-Signaling Plans using Reachability Games. In Proceedings of the 28th Symposium on the Implementation and Application of Functional Programming Languages, IFL 2016, pages 9:1-9:13, New York, NY, USA, 2016. ACM. URL: https://doi.org/10.1145/3064899.3064908.
  17. A. Laarman and A. Wijs. Partial-Order Reduction for Multi-core LTL Model Checking. In Hardware and Software: Verification and Testing, volume 8855 of LNCS, pages 267-283. Springer-Verlag, 2014. Google Scholar
  18. A. Lehmann, N. Lohmann, and K. Wolf. Stubborn Sets for Simple Linear Time Properties. In Application and Theory of Petri Nets, volume 7347 of LNCS, pages 228-247. Springer-Verlag, 2012. Google Scholar
  19. D. Peled. All from One, One for All: on Model Checking Using Representatives. In Computer Aided Verification, volume 697 of LNCS, pages 409-423. Springer-Verlag, 1993. Google Scholar
  20. F.G. Quintanilla, S. Kubler, O. Cardin, and P. Castagna. Product Specification in a Service-Oriented Holonic Manufacturing System using Petri-Nets. IFAC Proceedings Volumes, 46(7):342-347, May 2013. URL: https://doi.org/10.3182/20130522-3-BR-4036.00094.
  21. Y.S. Ramakrishna and S.A. Smolka. Partial-Order Reduction in the Weak Modal Mu-Calculus. In Antoni Mazurkiewicz and Józef Winkowski, editors, International Conference on Concurrency Theory, volume 1243 of LNCS, pages 5-24. Springer-Verlag, 1997. Google Scholar
  22. R. Tagiew. Multi-Agent Petri-Games. In International Conference on Computational Intelligence for Modeling Control Automation, volume 10981 of LNCS, pages 130-135. IEEE Computer Society, 2008. URL: https://doi.org/10.1109/CIMCA.2008.15.
  23. A. Valmari. A Stubborn Attack on State Explosion. Formal Methods in System Design, 1(4):297-322, December 1992. Google Scholar
  24. A. Valmari. On-The-Fly Verification with Stubborn Sets. In Computer Aided Verification, volume 697 of LNCS, pages 397-408. Springer-Verlag, 1993. Google Scholar
  25. A. Valmari and H. Hansen. Stubborn Set Intuition Explained. In Transactions on Petri Nets and Other Models of Concurrency XII, volume 10470 of LNCS, pages 140-165. Springer-Verlag, 2017. Google Scholar
  26. B. Willems and P. Wolper. Partial-Order Methods for Model Checking: From Linear Time to Branching Time. In Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, pages 294-303, July 1996. URL: https://doi.org/10.1109/LICS.1996.561357.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact