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. © 2020
Hierarchical cost-parity games / Bozzelli, L.; Murano, A.; Perelli, G.; Sorrentino, L.. - In: THEORETICAL COMPUTER SCIENCE. - ISSN 0304-3975. - 847:(2020), pp. 147-174. [10.1016/j.tcs.2020.10.002]
Hierarchical cost-parity games
Bozzelli, L.;Murano, A.
;Perelli, G.;Sorrentino, L.
2020
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. © 2020I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
