Abstract
Timed games are an essential formalism for modeling time-sensitive reactive systems that must respond to uncontrollable events triggered by the (hostile) environment. However, the control synthesis problem for these systems is often resource-demanding due to the state space explosion problem. To counter this problem, we present an extension of partial order reduction, based on stubborn sets, into timed games. We introduce the theoretical foundations on the general formalism of timed game labeled transition systems and then instantiate it to the model of timed-arc Petri net games. We provide an efficient implementation of our method as part of the model checker TAPAAL and discuss an experimental evaluation on several case studies that show increasing (sometimes even exponential) savings in time and memory as the case studies scale to larger instances. To the best of our knowledge, this is the first application of partial order reductions to a game formalism that includes time.
Original language | English |
---|---|
Title of host publication | Formal Modeling and Analysis of Timed Systems - 19th International Conference, FORMATS 2021, Proceedings |
Editors | Catalin Dima, Mahsa Shirmohammadi |
Number of pages | 18 |
Volume | 12860 |
Publisher | Springer |
Publication date | 2021 |
Pages | 32-49 |
ISBN (Print) | 9783030850364 |
DOIs | |
Publication status | Published - 2021 |
Event | 19th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2021 - Virtual, Online Duration: 24 Aug 2021 → 26 Aug 2021 |
Conference
Conference | 19th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2021 |
---|---|
City | Virtual, Online |
Period | 24/08/2021 → 26/08/2021 |
Series | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 12860 LNCS |
ISSN | 0302-9743 |
Bibliographical note
Publisher Copyright:© 2021, Springer Nature Switzerland AG.