×
Bozzelli, Laura; Molinari, Alberto; Montanari, Angelo; Peron, Adriano; Sala, Pietro

Interval vs. point temporal logic model checking. An expressiveness comparison. (English) Zbl 1407.68283

ACM Trans. Comput. Log. 20, No. 1, Article No. 4, 31 p. (2019).

Cited in 5 Documents

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic

Keywords:

interval temporal logics; expressiveness; model checking

Citations:

Zbl 1350.68184
Cite Review PDF
Full Text: DOI

References:

[1] J. F. Allen. 1983. Maintaining knowledge about temporal intervals. Communications of the ACM 26, 11 (1983), 832-843. · Zbl 0519.68079
[2] R. Alur, P. Cerný, and S. Zdancewic. 2006. Preserving secrecy under refinement. In ICALP, Lecture Notes in Computer Science, Vol. 4052. Springer, 107-118. · Zbl 1133.94307
[3] C. Baier and J. P. Katoen. 2008. Principles of Model Checking (Representation and Mind Series). The MIT Press. · Zbl 1179.68076
[4] P. Blackburn and J. Seligman. 1998. What are hybrid languages? In AiML. CSLI Publications, 41-62. · Zbl 0911.03009
[5] L. Bozzelli, A. Molinari, A. Montanari, and A. Peron. 2017. An in-depth investigation of interval temporal logic model checking with regular expressions. In SEFM, Lecture Notes in Computer Science, Vol. 10469. Springer, 104-119. · Zbl 1420.68120
[6] L. Bozzelli, A. Molinari, A. Montanari, and A. Peron. 2017. On the complexity of model checking for syntactically maximal fragments of the interval temporal logic HS with regular expressions. In GandALF, Electronic Proceedings in Theoretical Computer Science, Vol. 256. EPTCS, 31-45. · Zbl 1483.68186
[7] L. Bozzelli, A. Molinari, A. Montanari, A. Peron, and P. Sala. 2016. Interval temporal logic model checking: The border between good and bad HS fragments. In IJCAR Lecture Notes in Artificial Intelligence, Vol. 9706. Springer, 389-405. · Zbl 1475.68177
[8] L. Bozzelli, A. Molinari, A. Montanari, A. Peron, and P. Sala. 2016. Interval vs. point temporal logic model checking: An expressiveness comparison. In FSTTCS. LIPIcs, 26:1-26:14. · Zbl 1391.68075
[9] L. Bozzelli, A. Molinari, A. Montanari, A. Peron, and P. Sala. 2016. Model checking the logic of Allen’s relations meets and started-by is P<sup>NP</sup>-complete. In GandALF. EPTCS, 76-90. · Zbl 1478.68148
[10] L. Bozzelli, A. Molinari, A. Montanari, A. Peron, and P. Sala. 2017. Satisfiability and model checking for the logic of sub-intervals under the homogeneity assumption. In ICALP (LIPIcs), Vol. 80. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 120:1-120:14. · Zbl 1442.68103
[11] D. Bresolin, D. Della Monica, V. Goranko, A. Montanari, and G. Sciavicco. 2014. The dark side of interval temporal logic: Marking the undecidability border. Annals of Mathematics and Artificial Intelligence 71, 1-3 (2014), 41-83. · Zbl 1325.03014
[12] D. Bresolin, V. Goranko, A. Montanari, and P. Sala. 2010. Tableau-based decision procedures for the logics of subinterval structures over dense orderings. Journal of Logic and Computation 20, 1 (2010), 133-166. · Zbl 1188.03009
[13] D. Bresolin, V. Goranko, A. Montanari, and G. Sciavicco. 2009. Propositional interval neighborhood logics: Expressiveness, decidability, and undecidable extensions. Annals of Pure and Applied Logic 161, 3 (2009), 289-304. · Zbl 1221.03022
[14] D. Bresolin, A. Montanari, P. Sala, and G. Sciavicco. 2011. Optimal tableau systems for propositional neighborhood logic over all, dense, and discrete linear orders. In TABLEAUX, Lecture Notes in Computer Science, Vol. 6973. Springer, 73-87. · Zbl 1333.03006
[15] G. De Giacomo and M. Y. Vardi. 2013. Linear temporal logic and linear dynamic logic on finite traces. In IJCAI. IJCAI/AAAI, 854-860.
[16] S. Demri, V. Goranko, and M. Lange. 2016. Temporal Logics in Computer Science: Finite-State Systems. Cambridge University Press. · Zbl 1380.68003
[17] E. A. Emerson and J. Y. Halpern. 1986. “Sometimes” and “not never” revisited: On branching versus linear time temporal logic. Journal of the ACM 33, 1 (1986), 151-178. · Zbl 0629.68020
[18] E. A. Emerson and C. Lei. 1985. Modalities for model checking: Branching time strikes back. In PoPL. Elsevier, 84-96.
[19] D. M. Gabbay. 1987. The declarative past and imperative future: Executable temporal logic for interactive systems. In Temporal Logic in Specification, Lecture Notes in Computer Science, Vol. 398. Springer, 409-448.
[20] J. Y. Halpern and Y. Shoham. 1991. A propositional modal logic of time intervals. Journal of the ACM 38, 4 (1991), 935-962. · Zbl 0799.68175
[21] H. Kamp. 1968. Tense Logic and the Theory of Linear Order. Ph.D. dissertation. Ucla.
[22] O. Kupferman, A. Pnueli, and M. Y. Vardi. 2012. Once and for all. Journal of Computer and System Sciences 78, 3 (2012), 981-996. · Zbl 1245.03022
[23] F. Laroussinie and Ph. Schnoebelen. 1995. A hierarchy of temporal logics with past. Theoretical Computer Science 148, 2 (1995), 303-324. · Zbl 0873.68068
[24] O. Lichtenstein and A. Pnueli. 2000. Propositional temporal logics: Decidability and completeness. Logic Journal of the IGPL 8, 1 (2000), 55-85. · Zbl 1033.03009
[25] K. Lodaya. 2000. Sharpening the undecidability of interval temporal logic. In ASIAN, Lecture Notes in Computer Science, Vol. 1961. Springer, 290-298. · Zbl 0987.03015
[26] A. Lomuscio and J. Michaliszyn. 2013. An epistemic Halpern-Shoham logic. In IJCAI. IJCAI/AAAI, 1010-1016.
[27] A. Lomuscio and J. Michaliszyn. 2014. Decidability of model checking multi-agent systems against a class of EHS specifications. In ECAI. IOS Press, 543-548. · Zbl 1366.68179
[28] A. Lomuscio and J. Michaliszyn. 2016. Model checking multi-agent systems against epistemic HS specifications with regular expressions. In KR. AAAI Press, 298-308.
[29] J. Marcinkowski and J. Michaliszyn. 2014. The undecidability of the logic of subintervals. Fundamenta Informaticae 131, 2 (2014), 217-240. · Zbl 1315.03027
[30] A. Molinari, A. Montanari, A. Murano, G. Perelli, and A. Peron. 2016. Checking interval properties of computations. Acta Informatica 53, 6-8 (2016), 587-619. · Zbl 1350.68184
[31] A. Molinari, A. Montanari, and A. Peron. 2015. Complexity of ITL model checking: Some well-behaved fragments of the interval logic HS. In TIME. IEEE Computer Society, 90-100.
[32] A. Molinari, A. Montanari, and A. Peron. 2015. A model checking procedure for interval temporal logics based on track representatives. In CSL. LIPIcs, 193-210. · Zbl 1373.68289
[33] A. Molinari, A. Montanari, A. Peron, and P. Sala. 2016. Model checking well-behaved fragments of HS: The (almost) final picture. In KR. AAAI Press, 473-483.
[34] A. Montanari, A. Murano, G. Perelli, and A. Peron. 2014. Checking interval properties of computations. In TIME. IEEE Computer Society, 59-68. · Zbl 1350.68184
[35] A. Montanari, G. Puppis, and P. Sala. 2015. A decidable weakening of compass logic based on cone-shaped cardinal directions. Logical Methods in Computer Science 11, 4 (2015), 1-32. · Zbl 1351.03014
[36] B. Moszkowski. 1983. Reasoning About Digital Circuits. Ph.D. dissertation. Stanford University, CA.
[37] A. Pnueli. 1977. The temporal logic of programs. In FOCS. IEEE Computer Society, 46-57.
[38] I. Pratt-Hartmann. 2005. Temporal prepositions and their logic. Artificial Intelligence 166(1-2) (2005), 1-36. · Zbl 1132.03334
[39] P. Roeper. 1980. Intervals and tenses. Journal of Philosophical Logic 9 (1980), 451-469. · Zbl 0451.03007
[40] A. P. Sistla and E. M. Clarke. 1985. The complexity of propositional linear temporal logics. Journal of the ACM 32, 3 (1985), 733-749. · Zbl 0632.68034
[41] M. Y. Vardi. 1996. An automata-theoretic approach to linear temporal logic. In Logics for Concurrency. Springer, 238-266. · Zbl 07869808
[42] Y. Venema. 1990. Expressiveness and completeness of an interval tense logic. Notre Dame Journal of Formal Logic 31, 4 (1990), 529-547. · Zbl 0725.03006
[43] T. Wilke. 1999. Classifying discrete temporal properties. In STACS, (Lecture Notes in Computer Science, Vol. 1563). Springer, 32-46. · Zbl 0926.03018
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.