Dynamic controllability of temporal networks with instantaneous reaction

A Conditional Simple Temporal Network with Uncertainty and Decisions (CSTNUD) is a formalism to model, validate, and execute temporal plans subject to controllable and uncontrollable events as well as controllable and uncontrollable choices simultaneously. Dynamic Controllability implies the existence of a strategy scheduling the events and fixing the controllable choices in real time in a way that only depends on the already executed uncontrollable events and already fixed uncontrollable choices. This paper unifies CSTNUDs with other temporal network formalisms by providing Conditional Temporal Networks with Uncertainty and Decisions (CTNUDs) and proposes a semantics for dynamic controllability modeled as a two-player game between Controller and Nature where each player can react instantaneously to the other player moves. Such a game is designed to guarantee termination with exactly one winner (i.e., the game is determined). We prove that adopting the instantaneous reaction semantics allows for modeling any possible reaction time, absorbing de facto previous proposed semantics of dynamic controllability. We provide an encoding into Timed Game Automata to synthesize an execution strategy for any dynamically controllable CTNUD. We implement our approach to synthesize C++ programs for the execution of dynamically controllable CTNUDs. We test our software on a set of randomly-generated instances.