Document Open Access Logo

Hierarchical Cost-Parity Games

Authors Laura Bozzelli, Aniello Murano, Giuseppe Perelli, Loredana Sorrentino

PDF
Thumbnail PDF

File

LIPIcs.TIME.2017.6.pdf
  • Filesize: 0.63 MB
  • 17 pages

Document Identifiers

Author Details

Laura Bozzelli
Aniello Murano
Giuseppe Perelli
Loredana Sorrentino

Cite As Get BibTex

Laura Bozzelli, Aniello Murano, Giuseppe Perelli, and Loredana Sorrentino. Hierarchical Cost-Parity Games. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.TIME.2017.6

Abstract

Cost-parity games are a fundamental tool in system design for the analysis of reactive and distributed systems that recently have received a lot of attention from the formal methods research community. They allow to reason about the time delay on the requests granted by systems, with a bounded consumption of resources, in their executions. 

In this paper, we contribute to research on Cost-parity games by combining them with hierarchical systems, a successful method for the succinct representation of models. We show that determining the winner of a Hierarchical Cost-parity Game is PSpace-Complete, thus matching the complexity of the proper special case of Hierarchical Parity Games. This shows that reasoning about temporal delay can be addressed at a free cost in terms of complexity.

Subject Classification

Keywords
  • Parity Games
  • Cost-Parity Games
  • Hierarchical Systems
  • System Verification

Metrics

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

References

  1. S. Almagor, Y. Hirshfeld, and O. Kupferman. Promptness in omega-Regular Automata. In ATVA'10, LNCS 7388, pages 22-36, 2010. Google Scholar
  2. R. Alur, M. Benedikt, K. Etessami, P. Godefroid, T. W. Reps, and M. Yannakakis. Analysis of recursive state machines. TOPLAS, 27(4):786-818, 2005. Google Scholar
  3. R. Alur, S. Kannan, and M. Yannakakis. Communicating hierarchical state machines. In Automata, Languages and Programming, 26th International Colloquium, ICALP'99, Prague, Czech Republic, July 11-15, 1999, Proceedings, pages 169-178, 1999. Google Scholar
  4. R. Alur and M. Yannakakis. Model checking of hierarchical state machines. ACM Trans. Program. Lang. Syst., 23(3):273-303, 2001. Google Scholar
  5. B. Aminof, O. Kupferman, and A. Murano. Improved Model Checking of Hierarchical Systems. Inf. Comput., 210:68-86, 2012. URL: http://dx.doi.org/10.1016/j.ic.2011.10.008.
  6. B. Aminof, F. Mogavero, and A. Murano. Synthesis of Hierarchical Systems. In FACS'11, LNCS 7253, pages 42-60. Springer, 2011. Google Scholar
  7. B. Aminof, F. Mogavero, and A. Murano. Synthesis of Hierarchical Systems. SCP, 83:56-79, 2014. Google Scholar
  8. K. Chatterjee and L. Doyen. Energy Parity Games. Theor. Comput. Sci., 458:49-60, 2012. Google Scholar
  9. K. Chatterjee, T. A. Henzinger, and M. Jurdzinski. Mean-Payoff Parity Games. In LICS'05, pages 178-187, 2005. Google Scholar
  10. K. Chatterjee, T. A. Henzinger, and F. Horn. Finitary winning in ω-regular games. ACM Trans. Comput. Logic, 11(1), 2009. Google Scholar
  11. E. M. Clarke and E. A. Emerson. Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. In LP'81, LNCS 131, pages 52-71. Springer, 1981. Google Scholar
  12. E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 2002. Google Scholar
  13. E. A. Emerson and C. Jutla. Tree Automata, μ-Calculus and Determinacy. In FOCS, pages 368-377, 1991. Google Scholar
  14. E. A. Emerson and C. S. Jutla. The Complexity of Tree Automata and Logics of Programs. SJM, 29(1):132-158, 1999. Google Scholar
  15. N. Fijalkow and M. Zimmermann. Parity and Streett Games with Costs. Logical Methods in Computer Science, 10(2), 2014. Google Scholar
  16. S. Göller and M. Lohrey. Fixpoint logics on hierarchical structures. In FSTTCS'05, LNCS 3821, pages 483-494. Springer, 2005. Google Scholar
  17. M. Jurdzinski, M. Paterson, and U. Zwick. A Deterministic Subexponential Algorithm for Solving Parity Games. SIAM J. Comput., 38(4):1519-1532, 2008. Google Scholar
  18. D. Kozen. Results on the Propositional muCalculus. TCS, 27(3):333-354, 1983. Google Scholar
  19. O. Kupferman, N. Piterman, and M. Y. Vardi. From Liveness to Promptness. Formal Methods in System Design, 34(2):83-103, 2009. Google Scholar
  20. O. Kupferman, M. Y. Vardi, and P. Wolper. An Automata Theoretic Approach to Branching-Time Model Checking. JACM, 47(2):312-360, 2000. Google Scholar
  21. O. Kupferman, M. Y. Vardi, and P. Wolper. Module Checking. IC, 164(2):322-344, 2001. Google Scholar
  22. V. Malvone, A. Murano, and L. Sorrentino. Concurrent Multi-Player Parity Games. In AAMAS'16, pages 689-697, 2016. Google Scholar
  23. F. Mogavero, A. Murano, and L. Sorrentino. On Promptness in Parity Games. In LPAR'13, LNCS 8312, pages 601-618. Springer, 2013. Google Scholar
  24. F. Mogavero, A. Murano, and L. Sorrentino. On Promptness in Parity Games. Fundam. Inform., 139(3):277-305, 2015. URL: http://dx.doi.org/10.3233/FI-2015-1235.
  25. A. Pnueli. The Temporal Logic of Programs. In FOCS'77, pages 46-57. IEEE Computer Society, 1977. Google Scholar
  26. J. P. Queille and J. Sifakis. Specification and Verification of Concurrent Programs in Cesar. In SP'81, LNCS 137, pages 337-351. Springer, 1981. 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 About DROPS Imprint Privacy Contact