Abstract
In our contribution, we study the effects of adding past operators to interval temporal logics. We focus our attention on the representative case of Propositional Neighborhood Logic (\(\mathsf{A \overline A}\) for short), taking into consideration different temporal domains. \(\mathsf{A \overline A}\) is the proper fragment of Halpern and Shoham’s modal logic of intervals with modalities for Allen’s relations meets (future modality) and met by (past modality). We first prove that, unlike what happens with point-based linear temporal logic, \(\mathsf{A \overline A}\) is strictly more expressive than its future fragment A. Then, we show that there is a log-space reduction from the satisfiability problem for \(\mathsf{A \overline A}\) over ℤ to its satisfiability problem over ℕ. Compared to the corresponding reduction for point-based linear temporal logic, the one for \(\mathsf{A \overline A}\) turns out to be much more involved. Finally, we prove that \(\mathsf{A \overline A}\) is able to separate ℚ and ℝ, while A is not.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Allen, J.: Maintaining knowledge about temporal intervals. Communications of the ACM 26(11), 832–843 (1983)
Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, Cambridge (2002)
Bresolin, D., Della Monica, D., Goranko, V., Montanari, A., Sciavicco, G.: Decidable and Undecidable Fragments of Halpern and Shoham’s Interval Temporal Logic: Towards a Complete Classification. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 590–604. Springer, Heidelberg (2008)
Bresolin, D., Goranko, V., Montanari, A., Sala, P.: Tableaux for logics of subinterval structures over dense orderings. Journal of Logic and Computation 20(1), 133–166 (2010)
Bresolin, D., Goranko, V., Montanari, A., Sciavicco, G.: Propositional interval neighborhood logics: Expressiveness, decidability, and undecidable extensions. Annals of Pure and Applied Logic 161(3), 289–304 (2009)
Bresolin, D., Montanari, A., Sala, P.: An Optimal Tableau-Based Decision Algorithm for Propositional Neighborhood Logic. In: Thomas, W., Weil, P. (eds.) STACS 2007. LNCS, vol. 4393, pp. 549–560. Springer, Heidelberg (2007)
Bresolin, D., Montanari, A., Sala, P., Sciavicco, G.: Optimal Tableau Systems for Propositional Neighborhood Logic over All, Dense, and Discrete Linear Orders. In: Brünnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS (LNAI), vol. 6793, pp. 73–87. Springer, Heidelberg (2011)
Bresolin, D., Montanari, A., Sala, P., Sciavicco, G.: What’s decidable about Halpern and Shoham’s interval logic? The maximal fragment \(\mathsf{AB \overline{BL}}\). In: Proc. of the 26th Symposium on Logic in Computer Science, pp. 387–396. IEEE Computer Society Press (2011)
Bresolin, D., Montanari, A., Sciavicco, G.: An optimal decision procedure for Right Propositional Neighborhood Logic. Journal of Automated Reasoning 38(1-3), 173–199 (2007)
Emerson, E.A.: Temporal and modal logic. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp. 995–1072. Elsevier, MIT Press (1990)
Gabbay, D.M.: The Declarative Past and Imperative Future: Executable Temporal Logic for Interactive Systems. In: Banieqbal, B., Pnueli, A., Barringer, H. (eds.) Temporal Logic in Specification. LNCS, vol. 398, pp. 409–448. Springer, Heidelberg (1989)
Gabbay, D.M., Hodkinson, I.M., Reynolds, M.A.: Temporal expressive completeness in the presence of gaps. In: Väänänen, J., Oikkonen, J. (eds.) Logic Colloquium 90. Lecture Notes in Logic, vol. 2, pp. 89–121. Springer, Heidelberg (1993)
Gabbay, D.M., Pnueli, A., Shelah, S., Stavi, J.: On the temporal basis of fairness. In: Proc. of the 7th Annual ACM Symposium on Principles of Programming Languages, pp. 163–173 (1980)
Goranko, V., Montanari, A., Sciavicco, G.: A road map of interval temporal logics and duration calculi. Journal of Applied Non-Classical Logics 14(1-2), 9–54 (2004)
Halpern, J., Shoham, Y.: A propositional modal logic of time intervals. Journal of the ACM 38(4), 935–962 (1991)
Laroussinie, F., Markey, N., Schnoebelen, P.: Temporal logic with forgettable past. In: Proc. of the 17th Symposium on Logic in Computer Science, pp. 383–392. IEEE Computer Society Press (2002)
Lichtenstein, O., Pnueli, A., Zuck, L.D.: The Glory of the Past. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol. 193, pp. 196–218. Springer, Heidelberg (1985)
Lodaya, K.: Sharpening the Undecidability of Interval Temporal Logic. In: Kleinberg, R.D., Sato, M. (eds.) ASIAN 2000. LNCS, vol. 1961, pp. 290–298. Springer, Heidelberg (2000)
Maler, O., Pnueli, A.: Tight bounds on the complexity of cascaded decomposition of automata. In: Proc. of the 31st Annual Symposium on Foundations of Computer Science, vol. II, pp. 672–682. IEEE Computer Society Press (1990)
Marcinkowski, J., Michaliszyn, J.: The ultimate undecidability result for the Halpern-Shoham logic. In: Proc. of the 26th Symposium on Logic in Computer Science, pp. 377–386. IEEE Computer Society Press (2011)
Markey, N.: Temporal logic with past is exponentially more succinct. Bulletin of the EATCS 79, 122–128 (2003)
Montanari, A., Puppis, G., Sala, P.: A Decidable Spatial Logic with Cone-Shaped Cardinal Directions. In: Grädel, E., Kahle, R. (eds.) CSL 2009. LNCS, vol. 5771, pp. 394–408. Springer, Heidelberg (2009)
Montanari, A., Puppis, G., Sala, P.: Maximal Decidable Fragments of Halpern and Shoham’s Modal Logic of Intervals. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010, Part II. LNCS, vol. 6199, pp. 345–356. Springer, Heidelberg (2010)
Moszkowski, B.: Reasoning about digital circuits. Tech. rep. stan-cs-83-970, Dept. of Computer Science, Stanford University, Stanford, CA (1983)
Otto, M.: Two variable first-order logic over ordered domains. Journal of Symbolic Logic 66(2), 685–702 (2001)
Reynolds, M.: The complexity of temporal logic over the reals. Annals of Pure and Applied Logic 161(8), 1063–1096 (2010)
Shapirovsky, I.: On PSPACE-decidability in Transitive Modal Logic. In: Advances in Modal Logic, vol. 5, pp. 269–287. King’s College Publications (2005)
Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp. 133–192. Elsevier, MIT Press (1990)
Thomason, S.K.: Reduction of tense logic to modal logic I. Journal of Symbolic Logic 39(3), 549–551 (1974)
Thomason, S.K.: Reduction of tense logic to modal logic II. Theoria 41(3), 154–169 (1975)
Venema, Y.: A modal logic for chopping intervals. Journal of Logic and Computation 1(4), 453–476 (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Della Monica, D., Montanari, A., Sala, P. (2012). The Importance of the Past in Interval Temporal Logics: The Case of Propositional Neighborhood Logic. In: Artikis, A., Craven, R., Kesim Çiçekli, N., Sadighi, B., Stathis, K. (eds) Logic Programs, Norms and Action. Lecture Notes in Computer Science(), vol 7360. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-29414-3_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-29414-3_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-29413-6
Online ISBN: 978-3-642-29414-3
eBook Packages: Computer ScienceComputer Science (R0)