LIPIcs.MFCS.2020.21.pdf
- Filesize: 0.51 MB
- 14 pages
Document
On a Temporal Logic of Prefixes and Infixes
Authors
-
Part of:
Volume:
45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Mathematical Foundations of Computer Science (MFCS) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2020-08-18
Cite AsGet BibTex
Laura Bozzelli, Angelo Montanari, Adriano Peron, and Pietro Sala. On a Temporal Logic of Prefixes and Infixes. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 21:1-21:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.MFCS.2020.21
https://doi.org/10.4230/LIPIcs.MFCS.2020.21
Abstract
A classic result by Stockmeyer [Stockmeyer, 1974] gives a non-elementary lower bound to the emptiness problem for star-free generalized regular expressions. This result is intimately connected to the satisfiability problem for interval temporal logic, notably for formulas that make use of the so-called chop operator. Such an operator can indeed be interpreted as the inverse of the concatenation operation on regular languages, and this correspondence enables reductions between non-emptiness of star-free generalized regular expressions and satisfiability of formulas of the interval temporal logic of the chop operator under the homogeneity assumption [Halpern et al., 1983]. In this paper, we study the complexity of the satisfiability problem for a suitable weakening of the chop interval temporal logic, that can be equivalently viewed as a fragment of Halpern and Shoham interval logic featuring the operators B, for "begins", corresponding to the prefix relation on pairs of intervals, and D, for "during", corresponding to the infix relation. The homogeneous models of the considered logic naturally correspond to languages defined by restricted forms of regular expressions, that use union, complementation, and the inverses of the prefix and infix relations.
Subject Classification
ACM Subject Classification
- Theory of computation → Logic and verification
- Theory of computation
Keywords
- Interval Temporal Logic
- Star-Free Regular Languages
- Satisfiability
- Complexity
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron, and Pietro Sala. Satisfiability and model checking for the logic of sub-intervals under the homogeneity assumption. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, volume 80 of LIPIcs, pages 120:1-120:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.120.
- Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron, and Pietro Sala. Which fragments of the interval temporal logic HS are tractable in model checking? Theor. Comput. Sci., 764:125-144, 2019. URL: https://doi.org/10.1016/j.tcs.2018.04.011.
- Laura Bozzelli, Angelo Montanari, and Adriano Peron. Complexity analysis of a unifying algorithm for model checking interval temporal logic. In Johann Gamper, Sophie Pinchinat, and Guido Sciavicco, editors, 26th International Symposium on Temporal Representation and Reasoning, TIME 2019, October 16-19, 2019, Málaga, Spain, volume 147 of LIPIcs, pages 18:1-18:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.TIME.2019.18.
- Valentin Goranko, Angelo Montanari, and Guido Sciavicco. A road map of interval temporal logics and duration calculi. Journal of Applied Non-Classical Logics, 14(1-2):9-54, 2004. URL: https://doi.org/10.3166/jancl.14.9-54.
-
Joseph Halpern, Zohar Manna, and Ben Moszkowski. A hardware semantics based on temporal intervals. In Josep Diaz, editor, Automata, Languages and Programming, pages 278-291, Berlin, Heidelberg, 1983. Springer Berlin Heidelberg.
-
Joseph Y. Halpern and Yoav Shoham. A propositional modal logic of time intervals. Journal of the ACM, 38:279-292, 1996.
- Ian Hodkinson, Angelo Montanari, and Guido Sciavicco. Non-finite axiomatizability and undecidability of interval temporal logics with C, D, and T. In CSL, volume 5213 of LNCS, pages 308-322. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-87531-4_23.
- Jerzy Marcinkowski and Jakub Michaliszyn. The undecidability of the logic of subintervals. Fundam. Inform., 131(2):217-240, 2014. URL: https://doi.org/10.3233/FI-2014-1011.
- Jerzy Marcinkowski, Jakub Michaliszyn, and Emanuel Kieronski. B and D are enough to make the Halpern-Shoham logic undecidable. In Samson Abramsky, Cyril Gavoille, Claude Kirchner, Friedhelm Meyer auf der Heide, and Paul G. Spirakis, editors, Automata, Languages and Programming, 37th International Colloquium, ICALP, Bordeaux, France, July 6-10, Proceedings, Part II, volume 6199 of LNCS, pages 357-368. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14162-1_30.
- Alberto Molinari, Angelo Montanari, Aniello Murano, Giuseppe Perelli, and Adriano Peron. Checking interval properties of computations. Acta Inf., 53(6-8):587-619, 2016. URL: https://doi.org/10.1007/s00236-015-0250-1.
- Angelo Montanari and Pietro Sala. Adding an equivalence relation to the interval logic A B ̅B: Complexity and expressiveness. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013, pages 193-202. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/LICS.2013.25.
- Angelo Montanari and Pietro Sala. Interval logics and ωB-regular languages. In Adrian-Horia Dediu, Carlos Martín-Vide, and Bianca Truthe, editors, Language and Automata Theory and Applications - 7th International Conference, LATA 2013, Bilbao, Spain, April 2-5, 2013. Proceedings, volume 7810 of Lecture Notes in Computer Science, pages 431-443. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-37064-9_38.
-
Ben Moszkowski. Reasoning About Digital Circuits. PhD thesis, Stanford University, CA, 1983.
- Peter Roeper. Intervals and tenses. Journal of Philosophical Logic, 9:451-469, 1980. URL: https://doi.org/10.1007/BF00262866.
- Sylvain Schmitz. Complexity hierarchies beyond elementary. ACM Transactions on Computation Theory, 8(1):3:1-3:36, 2016. URL: https://doi.org/10.1145/2858784.
-
Larry Joseph Stockmeyer. The complexity of decision problems in automata theory and logic. PhD thesis, Massachusetts Institute of Technology, 1974.
- Yde Venema. A modal logic for chopping intervals. Journal of Logic and Computation, 1(4):453-476, 1991. URL: https://doi.org/10.1093/logcom/1.4.453.