A Definitional Fragment of Temporal Equilibrium Logic: from Temporal Programs to Compact Automata

Abstract

We consider a definitional fragment of Temporal Equilibrium Logic (TEL), which allows to capture temporal rules that contain complex (implication-free) temporal formulas in rule bodies. We focus on the setting where formulas are interpreted over finite traces. We show that the basic reasoning tasks in the definitional fragment are PSpace-complete, showing a significant drop from the ExpSpace-completeness of the unrestricted case. Our method is based on characterizing stable models in terms of different kinds of type sequences, which allow to reason both about the existence and non-existence of stable models. In addition to handling tasks like stable model existence, we also show how the set of all stable models of a theory can be represented as a non-deterministic finite state automaton (NFA). Our method is self-contained in the sense that, in contrast to previous approaches, it does not rely on technical automata-theoretic results as black boxes. Our method can be implemented using SAT solving techniques and a prototype system is available.