STeLP - A Tool for Temporal Answer Set P rogramming

摘要

In this paper we present STeLP, a solver for Answer Set Pro gramming 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 gen eralisation of stable models for this extended syntax). The obtained set of models is represented in terms of a deterministic Biichi automaton capturing the complete program behaviour. In small examples, this au tomaton can be graphically displayed in a direct and readable way. The input language provides a set of constructs which allow a simple defi nition 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.