Dynamic controllability via Timed Game Automata

Temporal networks are data structures for representing and reasoning about temporal constraints on activities. Many kinds of temporal networks have been defined in the literature, differing in their expressiveness. The simplest kinds of networks have polynomial algorithms for determining their temporal consistency or different levels of controllability, but corresponding algorithms for more expressive networks (e.g., those that include observation nodes or disjunctive constraints) have so far been unavailable. This paper introduces a new approach to determine the dynamic controllability of a very expressive class of temporal networks that accommodates observation nodes and disjunctive constraints. The approach is based on encoding the dynamic controllability problem into a reachability game for Timed Game Automata (TGAs). This is the first sound and complete approach for determining the dynamic controllability of such networks. The encoding also highlights the theoretical relationships between various kinds of temporal networks and TGAs. The new algorithms have immediate applications in the design and analysis of workflow models being developed to automate business processes, including workflows in the health-care domain.