Stubborn Set Reduction for Timed Reachability and Safety Games

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.