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.
This research was partially supported by Spanish MEC project TIN2009-14562-C05-04 and Xunta de Galicia project INCITE08-PXIB105159PR.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Cabalar, P., Vega, G.P.: Temporal equilibrium logic: a first approach. In: Moreno Díaz, R., Pichler, F., Quesada Arencibia, A. (eds.) EUROCAST 2007. LNCS, vol. 4739, pp. 241–248. Springer, Heidelberg (2007)
Pearce, D.: A new logical characterisation of stable models and answer sets. In: Dix, J., Przymusinski, T.C., Moniz Pereira, L. (eds.) NMELP 1996. LNCS, vol. 1216. Springer, Heidelberg (1997)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1991)
Aguado, F., Cabalar, P., Pérez, G., Vidal, C.: Loop formulas for splitable temporal logic programs. In: Delgrande, J., Faber, W. (eds.) LPNMR 2011. LNCS (LNAI), vol. 6645, pp. 78–90. Springer, Heidelberg (2011), http://www.dc.fi.udc.es/~cabalar/lfstlp.pdf
Cabalar, P.: A normal form for linear temporal equilibrium logic. In: Janhunen, T., Niemelä, I. (eds.) JELIA 2010. LNCS, vol. 6341, pp. 64–76. Springer, Heidelberg (2010)
Ferraris, P., Lee, J., Lifschitz, V.: A generalization of the Lin-Zhao theorem. Annals of Mathematics and Artificial Intelligence 47, 79–101 (2006)
Tarjan, R.: Depth-first search and linear graph algorithms. SIAM Journal on Computing 1(2), 146–160 (1972)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cabalar, P., Diéguez, M. (2011). STeLP – A Tool for Temporal Answer Set Programming. In: Delgrande, J.P., Faber, W. (eds) Logic Programming and Nonmonotonic Reasoning. LPNMR 2011. Lecture Notes in Computer Science(), vol 6645. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20895-9_43
Download citation
DOI: https://doi.org/10.1007/978-3-642-20895-9_43
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-20894-2
Online ISBN: 978-3-642-20895-9
eBook Packages: Computer ScienceComputer Science (R0)