Abstract
In this paper, we study a method for computing temporal equilibrium models, a generalisation of stable models for logic programs with temporal operators, as in Linear Temporal Logic (LTL). To this aim, we focus on a syntactic subclass of these temporal logic programs called splitable and whose main property is satisfying a kind of “future projected” dependence present in most dynamic scenarios in Answer Set Programming (ASP). Informally speaking, this property can be expressed as “past does not depend on the future.” We show that for this syntactic class, temporal equilibrium models can be captured by an LTL formula, that results from the combination of two well-known techniques in ASP: splitting and loop formulas. As a result, an LTL model checker can be used to obtain the temporal equilibrium models of the program.
This research was partially supported by Spanish MEC project TIN2009-14562-C05-04 and Xunta de Galicia project INCITE08-PXIB105159PR.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Niemelä, I.: Logic programs with stable model semantics as a constraint programming paradigm. Annals of Mathematics and Artificial Intelligence 25, 241–273 (1999)
Marek, V., Truszczyński, M.: Stable models and an alternative logic programming paradigm, pp. 169–181. Springer, Heidelberg (1999)
Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: Kowalski, R.A., Bowen, K.A. (eds.) Logic Programming: Proc. of the Fifth International Conference and Symposium, vol. 2, pp. 1070–1080. MIT Press, Cambridge (1988)
Cabalar, P., Pérez Vega, G.: 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 (LNAI), vol. 1216. Springer, Heidelberg (1997)
Pearce, D.: Equilibrium logic. Annals of Mathematics and Artificial Intelligence 47(1-2), 3–41 (2006)
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.: Strongly equivalent temporal logic programs. In: Hölldobler, S., Lutz, C., Wansing, H. (eds.) JELIA 2008. LNCS (LNAI), vol. 5293, pp. 8–20. Springer, Heidelberg (2008)
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)
Lifschitz, V., Turner, H.: Splitting a logic program. In: Proceedings of the 11th International Conference on Logic programming (ICLP 1994), pp. 23–37 (1994)
Lin, F., Zhao, Y.: ASSAT: Computing answer sets of a logic program by SAT solvers. In: Artificial Intelligence, pp. 112–117 (2002)
Ferraris, P., Lee, J., Lifschitz, V.: A generalization of the Lin-Zhao theorem. Annals of Mathematics and Artificial Intelligence 47, 79–101 (2006)
Heyting, A.: Die formalen Regeln der intuitionistischen Logik. In: Sitzungsberichte der Preussischen Akademie der Wissenschaften, Physikalisch-mathematische Klasse, pp. 42–56 (1930)
Ferraris, P.: Answer sets for propositional theories. In: Baral, C., Greco, G., Leone, N., Terracina, G. (eds.) LPNMR 2005. LNCS (LNAI), vol. 3662, pp. 119–131. Springer, Heidelberg (2005)
Fages, F.: Consistency of Clark’s completion and existence of stable models. Methods of Logic in Computer Science 1, 51–60 (1994)
Cabalar, P., Diéguez, M.: STeLP – a tool for temporal answer set programming. In: Delgrande, J., Faber, W. (eds.) LPNMR 2011. LNCS (LNAI), vol. 6645, pp. 359–364. Springer, Heidelberg (2011)
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
Aguado, F., Cabalar, P., Pérez, G., Vidal, C. (2011). Loop Formulas for Splitable Temporal Logic Programs. 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_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-20895-9_9
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)