SMT-Based Diagnosis of Multi-Agent Temporal Plans

The paper proposes a model and methodology for diagnosing action failures in the execution of Temporal Multi-Agent Plans (TMAPs). Contrary to previous proposals in the literature, we characterize actions with a finite set of possible execution modes, where each mode prescribes not only the logic post-conditions of the actions, but also an interval of possible durations. Diagnoses are defined as assignments of modes to the actions that are consistent with the received observations and have the highest likelihood. We propose an algorithm that exploits a Satisfiability Modulo Theories (SMT) solver for the efficient computation of diagnoses. Preliminary experimental results are also presented.