Explaining the Behaviour of Hybrid Systems with PDDL+ Planning

The aim of this work is to explain the observed behaviour of a hybrid system (HS). The explanation problem is cast as finding a trajectory of the HS that matches some observations. By using the formalism of hybrid automata (HA), we characterize the explanations as the language of a network of HA that comprises one automaton for the HS and another one for the observations, thus restricting the behaviour of the HS exclusively to trajectories consistent with the observations. We observe that this problem corresponds to a reachability problem in model-checking, but that state-of-the-art model checkers struggle to find concrete trajectories. To overcome this issue we provide a formal mapping from HA to PDDL+ and rely on off-the-shelf automated planners. An experimental analysis over domains with piece-wise constant, linear and nonlinear dynamics reveals that the proposed PDDL+ approach is much more efficient than solving directly the explanation problem with model-checking solvers.