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.
@InProceedings{bozzelli_et_al:LIPIcs.TIME.2017.6, author = {Bozzelli, Laura and Murano, Aniello and Perelli, Giuseppe and Sorrentino, Loredana}, title = {{Hierarchical Cost-Parity Games}}, booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)}, pages = {6:1--6:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-052-1}, ISSN = {1868-8969}, year = {2017}, volume = {90}, editor = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.6}, URN = {urn:nbn:de:0030-drops-79175}, doi = {10.4230/LIPIcs.TIME.2017.6}, annote = {Keywords: Parity Games, Cost-Parity Games, Hierarchical Systems, System Verification} }
Feedback for Dagstuhl Publishing