Document Open Access Logo

On a Temporal Logic of Prefixes and Infixes

Authors Laura Bozzelli, Angelo Montanari, Adriano Peron, Pietro Sala

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2020.21.pdf
  • Filesize: 0.51 MB
  • 14 pages

Document Identifiers

Author Details

Laura Bozzelli
  • Department of Electric Engineering and Information Technology, University Federico II, Naples, Italy
Angelo Montanari
  • Department of Computer Science, Mathematics, and Physics, University of Udine, Italy
Adriano Peron
  • Department of Electric Engineering and Information Technology, University Federico II, Naples, Italy
Pietro Sala
  • Department of Computer Science, University of Verona, Italy

Cite As Get 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

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)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. 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. Google Scholar
  6. Joseph Y. Halpern and Yoav Shoham. A propositional modal logic of time intervals. Journal of the ACM, 38:279-292, 1996. Google Scholar
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  11. 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.
  12. 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.
  13. Ben Moszkowski. Reasoning About Digital Circuits. PhD thesis, Stanford University, CA, 1983. Google Scholar
  14. Peter Roeper. Intervals and tenses. Journal of Philosophical Logic, 9:451-469, 1980. URL: https://doi.org/10.1007/BF00262866.
  15. 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.
  16. Larry Joseph Stockmeyer. The complexity of decision problems in automata theory and logic. PhD thesis, Massachusetts Institute of Technology, 1974. Google Scholar
  17. 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.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact