×

On coarser interval temporal logics. (English) Zbl 1480.03010

Summary: The primary characteristic of interval temporal logic is that intervals, rather than points, are taken as the primitive ontological entities. Given their generally bad computational behavior of interval temporal logics, several techniques exist to produce decidable and computationally affordable temporal logics based on intervals. In this paper we take inspiration from Golumbic and Shamir’s coarser interval algebras, which generalize the classical Allen’s Interval Algebra, in order to define two previously unknown variants of Halpern and Shoham’s logic (HS) based on coarser relations. We prove that, perhaps surprisingly, the satisfiability problem for the coarsest of the two variants, namely \(\mathrm{HS}_3\), not only is decidable, but PSpace-complete in the finite/discrete case, and PSpace-hard in any other case; besides proving its complexity bounds, we implement a tableau-based satisfiability checker for it and test it against a systematically generated benchmark. Our results are strengthened by showing that not all coarser-than-Allen’s relations are a guarantee of decidability, as we prove that the second variant, namely \(\mathrm{HS}_7\), remains undecidable in all interesting cases.

MSC:

03B44 Temporal logic
68Q25 Analysis of algorithms and problem complexity
03B45 Modal logic (including the logic of norms)

Software:

LoTREC
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Aceto, L.; Della Monica, D.; Goranko, V.; Ingólfsdóttir, A.; Montanari, A.; Sciavicco, G., A complete classification of the expressiveness of interval logics of Allen’s relations: the general and the dense cases, Acta Inform., 53, 3, 207-246 (2016) · Zbl 1339.03018
[2] Allen, J. F., Maintaining knowledge about temporal intervals, Commun. ACM, 26, 11, 832-843 (1983) · Zbl 0519.68079
[3] Alluhaibi, R., Simple interval temporal logic for natural language assertion descriptions, (Proc. of the 11th International Conference on Computational Semantics. Proc. of the 11th International Conference on Computational Semantics, IWCS (2015)), 283-293
[4] Artale, A.; Bresolin, D.; Montanari, A.; Ryzhikov, V.; Sciavicco, G., DL-Lite and interval temporal logics: a marriage proposal, (Proc. of the 21st European Conference of Artificial Intelligence. Proc. of the 21st European Conference of Artificial Intelligence, ECAI (2014)), 957-958
[5] Artale, A.; Franconi, E., A temporal description logic for reasoning about actions and plans, J. Artif. Intell. Reason., 9, 463-506 (1998) · Zbl 0911.68190
[6] Artale, A.; Kontchakov, R.; Ryzhikov, V.; Zakharyaschev, M., A cookbook for temporal conceptual data modelling with description logics, ACM Trans. Comput. Log., 15, 3, 25:1-25:50 (2014) · Zbl 1354.68245
[7] Artale, A.; Kontchakov, R.; Ryzhikov, V.; Zakharyaschev, M., Tractable interval temporal propositional and description logics, (Proc. of the 29th AAAI Conference on Artificial Intelligence. Proc. of the 29th AAAI Conference on Artificial Intelligence, AAAI (2015)), 1417-1423
[8] Baeza-Yates, R. A., Challenges in the interaction of information retrieval and natural language processing, (Proc. of the 5th International on Computational Linguistics and Intelligent Text Processing. Proc. of the 5th International on Computational Linguistics and Intelligent Text Processing, CICLing (2004)), 445-456
[9] Balsiger, P.; Heuerding, A.; Schwendimann, S., A benchmark method for the propositional modal logics K, KT, S4, J. Autom. Reason., 24, 3, 297-317 (2000) · Zbl 0955.03013
[10] Bettini, C., Time-dependent concepts: representation and reasoning using temporal description logics, Data Knowl. Eng., 22, 1, 1-38 (1997) · Zbl 0907.68183
[11] Börger, E.; Grädel, E.; Gurevich, Y., The Classical Decision Problem, Perspectives of Mathematical Logic (1997), Springer · Zbl 0865.03004
[12] 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, (Proc. of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Proc. of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR. Proc. of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Proc. of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR, Lect. Notes Comput. Sci., vol. 5330 (2008), Springer), 590-604 · Zbl 1182.03037
[13] Bresolin, D.; Della Monica, D.; Goranko, V.; Montanari, A.; Sciavicco, G., The dark side of interval temporal logic: marking the undecidability border, Ann. Math. Artif. Intell., 71, 1-3, 41-83 (2014) · Zbl 1325.03014
[14] Bresolin, D.; Della Monica, D.; Montanari, A.; Sala, P.; Sciavicco, G., Interval temporal logics over strongly discrete linear orders: expressiveness and complexity, Theor. Comput. Sci., 560, 269-291 (2014) · Zbl 1335.03017
[15] Bresolin, D.; Della Monica, D.; Montanari, A.; Sala, P.; Sciavicco, G., On the complexity of fragments of the modal logic of Allen’s relations over dense structures, (Proc. of the 9th International Conference on Language and Automata Theory and Applications. Proc. of the 9th International Conference on Language and Automata Theory and Applications, LATA. Proc. of the 9th International Conference on Language and Automata Theory and Applications. Proc. of the 9th International Conference on Language and Automata Theory and Applications, LATA, Lect. Notes Comput. Sci., vol. 8977 (2015), Springer), 511-523 · Zbl 1451.03020
[16] Bresolin, D.; Della Monica, D.; Montanari, A.; Sciavicco, G., A tableau system for right propositional neighborhood logic over finite linear orders: an implementation, (Proc. of the 22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods. Proc. of the 22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX. Proc. of the 22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods. Proc. of the 22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX, Lect. Notes Comput. Sci., vol. 8123 (2013)), 74-80 · Zbl 1401.68275
[17] Bresolin, D.; Della Monica, D.; Montanari, A.; Sciavicco, G., The light side of interval temporal logic: the Bernays-Schönfinkel fragment of CDT, Ann. Math. Artif. Intell., 71, 1-3, 11-39 (2014) · Zbl 1325.03015
[18] Bresolin, D.; Goranko, V.; Montanari, A.; Sala, P., Tableaux for logics of subinterval structures over dense orderings, J. Log. Comput., 20, 1, 133-166 (2010) · Zbl 1188.03009
[19] Bresolin, D.; Kurucz, A.; Muñoz-Velasco, E.; Ryzhikov, V.; Sciavicco, G.; Zakharyaschev, M., Horn fragments of the Halpern-Shoham interval temporal logic, ACM Trans. Comput. Log., 18, 3, 22:1-22:39 (2017) · Zbl 1407.03029
[20] Bresolin, D.; Muñoz-Velasco, E.; Sciavicco, G., Sub-propositional fragments of the interval temporal logic of Allen’s relations, (Proc. of the 14th European Conference on Logics in Artificial Intelligence. Proc. of the 14th European Conference on Logics in Artificial Intelligence, JELIA. Proc. of the 14th European Conference on Logics in Artificial Intelligence. Proc. of the 14th European Conference on Logics in Artificial Intelligence, JELIA, Lect. Notes Comput. Sci., vol. 8761 (2014), Springer), 122-136 · Zbl 1432.03028
[21] Chaochen, Z.; Hansen, M. R., Duration Calculus: A Formal Approach to Real-Time Systems, EATCS: Monographs in Theoretical Computer Science (2004), Springer · Zbl 1071.68062
[22] Chomicki, J.; Toman, D., Temporal logic in information systems, (Logics for Databases and Information Systems (1998)), 31-70 · Zbl 0955.03513
[23] Della Monica, D.; Montanari, A.; Sciavicco, G.; Tishkovsky, D., First steps towards automated synthesis of tableau systems for interval temporal logics, (Proc. of the 5th International Conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking. Proc. of the 5th International Conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking, COMPUTATION TOOLS (2014)), 32-37
[24] Fariñas del Cerro, L.; Fauthoux, D.; Gasquet, O.; Herzig, A.; Longin, D.; Massacci, F., Lotrec: the generic tableau prover for modal and description logics, (Proc. of the 1st International Joint Conference on Automated Reasoning. Proc. of the 1st International Joint Conference on Automated Reasoning, IJCAR (2001)), 453-458 · Zbl 0988.68592
[25] Gent, I. P.; Walsh, T., The SAT phase transition, (Proc. of the 11th European Conference on Artificial Intelligence. Proc. of the 11th European Conference on Artificial Intelligence, ECAI (1994)), 105-109
[26] Golumbic, M. C.; Shamir, R., Complexity and algorithms for reasoning about time: a graph-theoretic approach, J. ACM, 40, 5, 1108-1133 (1993) · Zbl 0795.68095
[27] Goranko, V.; Montanari, A.; Sciavicco, G., Propositional interval neighborhood temporal logics, J. Univers. Comput. Sci., 9, 9, 1137-1167 (2003)
[28] Halpern, J.; Shoham, Y., A propositional modal logic of time intervals, J. ACM, 38, 4, 935-962 (1991) · Zbl 0799.68175
[29] Klarman, S., Practical querying of temporal data via OWL 2 QL and SQL:2011, (Proc. of the 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Proc. of the 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR. Proc. of the 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Proc. of the 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR, EPiC Series, vol. 26 (2014), Center for Artificial Intelligence Research), 52-61
[30] Marcinkowski, J.; Michaliszyn, J., The undecidability of the logic of subintervals, Fundam. Inform., 131, 2, 217-240 (2014) · Zbl 1315.03027
[31] Marx, M.; Reynolds, M., Undecidability of compass logic, J. Log. Comput., 9, 6, 897-914 (1999) · Zbl 0941.03018
[32] Molinari, A.; Montanari, A.; Murano, A.; Perelli, G.; Peron, A., Checking interval properties of computations, Acta Inform., 53, 6-8, 587-619 (2016) · Zbl 1350.68184
[33] Montanari, A.; Pratt-Hartmann, I.; Sala, P., Decidability of the logics of the reflexive sub-interval and super-interval relations over finite linear orders, (Proc. of the 17th International Symposium on Temporal Representation and Reasoning. Proc. of the 17th International Symposium on Temporal Representation and Reasoning, TIME (2010), IEEE Computer Society), 27-34
[34] Montanari, A.; Puppis, G.; Sala, P., Maximal decidable fragments of Halpern and Shoham’s modal logic of intervals, (Proc. of the 37th International Colloquium on Automata, Languages and Programming - Part II. Proc. of the 37th International Colloquium on Automata, Languages and Programming - Part II, ICALP. Proc. of the 37th International Colloquium on Automata, Languages and Programming - Part II. Proc. of the 37th International Colloquium on Automata, Languages and Programming - Part II, ICALP, Lect. Notes Comput. Sci., vol. 6199 (2010), Springer), 345-356 · Zbl 1288.03017
[35] Montanari, A.; Puppis, G.; Sala, P., A decidable weakening of compass logic based on cone-shaped cardinal directions, Log. Methods Comput. Sci., 11, 4 (2015) · Zbl 1351.03014
[36] Montanari, A.; Puppis, G.; Sala, P.; Sciavicco, G., Decidability of the interval temporal logic \(A B \overline{B}\) on natural numbers, (Proc. of the 27th Symposium on Theoretical Aspects of Computer Science. Proc. of the 27th Symposium on Theoretical Aspects of Computer Science, STACS (2010), Inria Nancy Grand Est & Loria), 597-608 · Zbl 1230.03047
[37] Montanari, A.; Sciavicco, G.; Vitacolonna, N., Decidability of interval temporal logics over split-frames via granularity, (Proc. of the 8th European Conference on Logics in Artificial Intelligence. Proc. of the 8th European Conference on Logics in Artificial Intelligence, JELIA. Proc. of the 8th European Conference on Logics in Artificial Intelligence. Proc. of the 8th European Conference on Logics in Artificial Intelligence, JELIA, Lect. Notes Artif. Intell., vol. 2424 (2002), Springer), 259-270 · Zbl 1013.03013
[38] Moszkowski, B., Reasoning About Digital Circuits (1983), Dept. of Computer Science, Stanford University: Dept. of Computer Science, Stanford University Stanford, CA, PhD thesis
[39] Papadimitriou, C. M., Computational Complexity (1994), Addison-Wesley Longman Publishing Co., Inc. · Zbl 0833.68049
[40] Pratt-Hartmann, I., Temporal prepositions and their logic, Artif. Intell., 166, 1-2, 1-36 (2005) · Zbl 1132.03334
[41] Schmiedel, A., Temporal terminological logic, (Proc. of the 8th National Conference on Artificial Intelligence. Proc. of the 8th National Conference on Artificial Intelligence, AAAI (1990), AAAI Press), 640-645
[42] Stockmeyer, L. J.; Meyer, A. R., Word problems requiring exponential time (Preliminary Report), (Proc. of the 5th Annual ACM Symposium on Theory of Computing. Proc. of the 5th Annual ACM Symposium on Theory of Computing, STOC (1973), ACM), 1-9 · Zbl 0359.68050
[43] Tishkovsky, D.; Schmidt, R. A.; Khodadadi, M., The tableau prover generator \(\textsc{MetTeL}^2\), (Proc. of the 13th European Conference on Logics in Artificial Intelligence. Proc. of the 13th European Conference on Logics in Artificial Intelligence, JELIA (2012)), 492-495
[44] Venema, Y., Expressiveness and completeness of an interval tense logic, Notre Dame J. Form. Log., 31, 4, 529-547 (1990) · Zbl 0725.03006
[45] Zemke, F., What’s new in SQL:2011, SIGMOD Rec., 41, 1, 67-73 (2012)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.