A Qualitative Temporal Extension of Here-and-There Logic

Abstract

Model-based Diagnosis (MBD) is an approach to diagnosis, where an (objective) model of a system is diagnosed to find a set of explanations revealing root causes for issues. Temporal behavioral models are prominent approach for temporal MBD, where their associated temporal formulas (TBFs) by Brusoni et al. (Artificial Intelligence, 102:39–79, 1998) can be used to relate explanations to observations under temporal constraints based on Allen’s Interval Algebra (IA). Due to expressive limitations of the constructs, we envision an extended language of TBFs that allows for complex formulas and nesting of formulas in temporal constraints. To this end, we present a language that extends propositional resp. FO logic with IA relations and provide semantics for it based on here-and-there (HT) logic as well as on Equilibrium Logic. Furthermore, we lift a well-known tableau calculus for propositional HT logic to the temporal setting and report about an experimental prototype implementation. Based on these results, rich notions of diagnostic explanations from temporal behavior models may be developed.