STeLP - A tool for temporal answer set programming

Abstract

In this paper we present STeLP, a solver for Answer Set Programming with temporal operators. Taking as an input a particular kind of logic program with modal operators (called Splitable Temporal Logic Program), STeLP obtains its set of temporal equilibrium models (a generalisation of stable models for this extended syntax). The obtained set of models is represented in terms of a deterministic Büchi automaton capturing the complete program behaviour. In small examples, this automaton can be graphically displayed in a direct and readable way. The input language provides a set of constructs which allow a simple definition of temporal logic programs, including a special syntax for action domains that can be exploited to simplify the graphical output. STeLP combines the use of a standard ASP solver with a linear temporal logic model checker in order to find all models of the input theory. © 2011 Springer-Verlag Berlin Heidelberg.