Dynamic controllability via Timed Game Automata

Temporal networks are data structures for representing and reasoning about temporalconstraints on activities. Many kinds of temporal networks have been defined in theliterature, differing in their expressiveness. The simplest kinds of networks have polynomialalgorithms for determining their temporal consistency or different levels of controllability,but corresponding algorithms for more expressive networks (e.g., those that include observationnodes or disjunctive constraints) have so far been unavailable. This paper introduces anew approach to determine the dynamic controllability of a very expressive class of temporalnetworks that accommodates observation nodes and disjunctive constraints. The approach isbased on encoding the dynamic controllability problem into a reachability game for TimedGame Automata (TGAs). This is the first sound and complete approach for determining thedynamic controllability of such networks. The encoding also highlights the theoretical relationshipsbetween various kinds of temporal networks and TGAs. The new algorithms haveimmediate applications in the design and analysis of workflow models being developed toautomate business processes, including workflows in the healthcare domain.