Fixing the Semantics for Dynamic Controllability and Providing a More Practical Characterization of Dynamic Execution Strategies

Morris, Muscettola and Vidal (MMV) presented an algorithm for checking the dynamic controllability (DC) of temporal networks in which certain temporal durations are beyond the control of the planning agent.Their DC-checking algorithm is based on rules for inferring new constraints based on the real-time context within which execution decisions must be made. This paper presents a counter-example to demonstrate that some of the inference rules are, in fact, not sound.The paper fixes the problem by strengthening the definition of dynamic execution strategies to correctly capture the central prohibition against advance knowledge of future events. The new definition enables MMV´s soundness proof to go through with minimal changes. It then uses the stronger definition to derive an equivalent, alternative characterization of dynamic execution strategies that highlights the real-time execution decisions that a planning agent must make. The procedural strategy used by MMV in their completeness proof is shown to satisfy the stronger definition,thus ensuring that the DC-checking algorithm is also complete with respect to the stronger definition. As a result, the paper puts MMV´s DC-checking algorithm on a more solid theoretical foundation, while also providing a more practical characterization of dynamic execution strategies.