A separation theorem for discrete-time interval temporal logic

References

• Allen, J. F. (1983). Maintaining knowledge about temporal intervals. Communications of the ACM, 26(11), 832–843. https://doi.org/10.1145/182.358434
   Web of Science ®Google Scholar
• Boulé, M., & Zilic, Z. (2008). Psl and sva assertion languages. In Generating hardware assertion checkers: For hardware verification, emulation, post-fabrication debugging and on-line monitoring (pp. 55–82). Springer Netherlands.
   Google Scholar
• Bowman, H., Cameron, H., King, P., & Thompson, S. (2000). Specification and prototyping of structured multimedia documents using interval temporal logic. In H. Barringer, M. Fisher, D. Gabbay, and G. Gough (Eds.), Advances in temporal logic (pp. 435–453). Springer Netherlands.
   Google Scholar
• Bowman, H., & Thompson, S. (2003). A decision procedure and complete axiomatisation of finite interval temporal logic with projection. Journal of Logic and Computation, 13(2), 195–239. https://doi.org/10.1093/logcom/13.2.195
   Web of Science ®Google Scholar
• Bozzelli, L., Molinari, A., Montanari, A., Peron, A., & Sala, P. (2016). Interval vs. point temporal logic model checking: An expressiveness comparison. In A. Lal, S. Akshay, S. Saurabh, & S. Sen (Eds.), FSTTCS 2016 (Vol. 65 of LIPIcs, pp. 26:1–26:14). Schloss Dagstuhl -- Leibniz-Zentrum für Informatik.
   Google Scholar
• Bozzelli, L., Molinari, A., Montanari, A., Peron, A., & Sala, P. (2019a). Interval vs. point temporal logic model checking: An expressiveness comparison. ACM Transactions on Computational Logic, 20(1), 4:1–43:1. https://doi.org/10.1145/3281028
   Google Scholar
• Bozzelli, L., Molinari, A., Montanari, A., Peron, A., & Sala, P. (2019b). Which fragments of the interval temporal logic HS are tractable in model checking? Theoretical Computer Science, 764(11), 125–144. https://doi.org/10.1016/j.tcs.2018.04.011
   Google Scholar
• Bozzelli, L., Murano, A., & Sorrentino, L. (2020). Alternating-time temporal logics with linear past. Theoretical Computer Science, 813(1), 199–217. https://doi.org/10.1016/j.tcs.2019.11.028
   Google Scholar
• Bresolin, D., Goranko, V., Montanari, A., & Sciavicco, G. (2009). Propositional interval neighborhood logics: Expressiveness, decidability, and undecidable extensions. Annals of Pure and Applied Logic, 161(3), 289–304. https://doi.org/10.1016/j.apal.2009.07.003
   Google Scholar
• Bresolin, D., Montanari, A., & Sala, P. (2007). An optimal tableau-based decision algorithm for propositional neighborhood logic. In W. Thomas & P. Weil (Eds.), STACS 2007, Proceedings (Vol. 4393 of LNCS, pp. 549–560). Springer.
   Google Scholar
• Bresolin, D., Montanari, A., Sala, P., & Sciavicco, G. (2013). Optimal decision procedures for MPNL over finite structures, the natural numbers, and the integers. Theoretical Computer Science, 493, 98–115. https://doi.org/10.1016/j.tcs.2012.10.043
   Google Scholar
• Bresolin, D., Montanari, A., & Sciavicco, G. (2007). An optimal decision procedure for right propositional neighborhood logic. Journal of Automated Reasoning, 38(1-3), 173–199. https://doi.org/10.1007/s10817-006-9051-0
   Google Scholar
• Brzozowski, J. A. (1964). Derivatives of regular expressions. Journal of the ACM, 11(4), 481–494. https://doi.org/10.1145/321239.321249
   Google Scholar
• Cau, A., Moszkowski, B., & Zedan, H. (2022). ITL web pages. http://www.antonio-cau.co.uk/ITL/
   Google Scholar
• Clarke, E. M., Grumberg, O., & Peled, D. A (2001). Model checking. MIT Press.
   Google Scholar
• Ésik, Z. (2000). A proof of the Krohn-Rhodes decomposition theorem. Theoretical Computer Science, 234(1–2), 287–300. https://doi.org/10.1016/S0304-3975(99)00315-1
   Google Scholar
• Farwer, B. (2001). ω-automata. In E. Grädel, W. Thomas, & T. Wilke (Eds.), Automata, logics, and infinite games: A guide to current research (Vol. 2500 of LNCS, pp. 3–20). Springer.
   Google Scholar
• Fischer, M., & Ladner, R. (1979). Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18(2), 194–211. https://doi.org/10.1016/0022-0000(79)90046-1
   Web of Science ®Google Scholar
• Fisher, M. (1997). A normal form for temporal logics and its applications in theorem-proving and execution. Journal of Logic and Computation, 7(4), 429–456. https://doi.org/10.1093/logcom/7.4.429
   Web of Science ®Google Scholar
• Gabbay, D., Hodkinson, I., & Reynolds, M (1994). Temporal logic: Mathematical foundations and computational aspects (Vol. I). Oxford University Press.
   Google Scholar
• Gabbay, D. M. (1989). Declarative past and imperative future: Executable temporal logic for interactive systems. In B. Banieqbal, H. Barringer & A. Pnueli (Eds.), Proceedings of the Colloquium of Temporal Logic in Specification (Vol. 398 of LNCS, pp. 67–89). Springer.
   Google Scholar
• Goranko, V., Montanari, A., & Sciavicco, G. (2003). Propositional interval neighborhood temporal logics. Journal of Universal Computer Science, 9(9), 1137–1167.
   Web of Science ®Google Scholar
• Goranko, V., Montanari, A., & Sciavicco, G. (2004). A road map of interval temporal logics and duration calculi. Journal of Applied Non-Classical Logics, 14(1–2), 9–54. https://doi.org/10.3166/jancl.14.9-54
   Google Scholar
• Guelev, D. P. (2007). Probabilistic interval temporal logic and duration calculus with infinite intervals: Complete proof systems. Logical Methods in Computer Science, 3(3).
   Google Scholar
• Guelev, D. P. (2008). A syntactical proof of the canonical reactivity form for past linear temporal logic. Journal of Logic and Computation, 18(4), 615–623. https://doi.org/10.1093/logcom/exn002
   Google Scholar
• Halpern, J. Y., Manna, Z., & Moszkowski, B. C. (1983). A hardware semantics based on temporal intervals. In J. Dıaz (Ed.), ICALP 1983, Proceedings (Vol. 154 of LNCS, pp. 278–291). Springer.
   Google Scholar
• Halpern, J. Y., & Shoham, Y. (1986). A propositional logic of time intervals. In Proceedings of LICS'86 (pp. 279–292). IEEE Computer Society Press.
   Google Scholar
• IEEE. (2010). Standard for property specification language (PSL), standard 1850–2010. ANSI/IEEE.
   Google Scholar
• IEEE. (2018). Standard for SystemVerilog–Unified hardware design, specification, and verification language, standard 1800–2017. ANSI/IEEE.
   Google Scholar
• Krohn, K., & Rhodes, J. (1965). The algebraic theory of machines I. Transactions of the American Mathematical Society, 116, 450–464. https://doi.org/10.1090/tran/1965-116-00
   Web of Science ®Google Scholar
• Laroussinie, F., Markey, N., & Schnoebelen, P. (2002). Temporal logic with forgettable past. In LICS 2002, Proceedings (pp. 383–392). IEEE Computer Society.
   Google Scholar
• Lomuscio, A., & Michaliszyn, J. (2013). An epistemic Halpern-Shoham logic. In F. Rossi (Ed.), Proceedings of IJCAI 2013 (pp. 1010–1016). IJCAI/AAAI.
   Google Scholar
• Lomuscio, A., & Michaliszyn, J. (2016). Model checking multi-agent systems against epistemic HS specifications with regular expressions. In C. Baral, J. P. Delgrande, & F. Wolter (Eds.), Proceedings of KR 2016 (pp. 298–308). AAAI Press.
   Google Scholar
• Lomuscio, A. R., & Michaliszyn, J. (2014). Decidability of model checking multi-agent systems against a class of EHS specifications. In T. Schaub, G. Friedrich, & B. O'Sullivan (Eds.), Proceedings of ECAI 2014 (Vol. 263 of Frontiers in Artificial Intelligence and Applications, pp. 543–548). IOS Press.
   Google Scholar
• Maler, O., & Pnueli, A. (1990). Tight bounds on the complexity of cascaded decomposition of automata. In FOCS 1990, Volume II (pp. 672–682). IEEE Computer Society.
   Google Scholar
• Manna, Z., & Pnueli, A. (1990). A hierarchy of temporal properties. In C. Dwork (Ed.), 9th Symposium on Principles of Distributed Computing (pp. 377–408). ACM Press.
   Google Scholar
• Molinari, A., Montanari, A., Murano, A., Perelli, G., & Peron, A. (2016). Checking interval properties of computations. Acta Informatica, 53(6–8), 587–619. https://doi.org/10.1007/s00236-015-0250-1
   Google Scholar
• Monica, D. D., Goranko, V., Montanari, A., & Sciavicco, G. (2011). Interval temporal logics: A journey. Bulletin of the EATCS, 105, 73–99.
   Google Scholar
• Montanari, A., Murano, A., Perelli, G., & Peron, A. (2014). Checking interval properties of computations. In A. Cesta, C. Combi, & F. Laroussinie (Eds.), Proceedings of TIME 2014 (pp. 59–68). IEEE Computer Society.
   Google Scholar
• Moszkowski, B. (1983). Reasoning about digital circuits [Ph.D. thesis, Department of Computer Science, Stanford University]. http://www.antonio-cau.co.uk/ITL/publications/reports/thesis-ben.pdf, Accessed in March, 2022.
   Google Scholar
• Moszkowski, B. (1985). Temporal logic for multilevel reasoning about hardware. IEEE Computer, 18(2), 10–19. https://doi.org/10.1109/MC.1985.1662795
   Google Scholar
• Moszkowski, B (1986). Executing temporal logic programs. Cambridge University Press. http://www.antonio-cau.co.uk/ITL/publications/reports/tempura-book.pdf, Accessed in March, 2022.
   Google Scholar
• Moszkowski, B. C. (2004). A hierarchical completeness proof for propositional interval temporal logic with finite time. Journal of Applied Non-Classical Logics, 14(1–2), 55–104. https://doi.org/10.3166/jancl.14.55-104
   Google Scholar
• Pandya, P. K. (1995). Some extensions to propositional mean-value calculus: Expressiveness and decidability. In H. K. Büning (Ed.), CSL '95, selected papers (Vol. 1092 of LNCS, pp. 434–451). Springer.
   Google Scholar
• Pnueli, A. (1977). The temporal logic of programs. In Proceedings of the 18th IEEE Symposium Foundations of Computer Science (pp. 46–57). IEEE.
   Google Scholar
• Pratt, V. R. (1979). Process logic. In A. V. Aho, S. N. Zilles, & B. K. Rosen (Eds.), Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, San Antonio, Texas, USA, January 1979 (pp. 93–100). ACM Press.
   Google Scholar
• Rasmussen, T. M. (1999). Signed interval logic. In J. Flum & M. Rodrıguez-Artalejo (Eds.), CSL '99, Proceedings (Vol. 1683 of LNCS, pp. 157–171). Springer.
   Google Scholar
• Venema, Y. (1991). A modal logic for chopping intervals. Journal of Logic and Computation, 1(4), 453–476. https://doi.org/10.1093/logcom/1.4.453
   Google Scholar
• Zhou, C., & Hansen, M. R (2004). Duration calculus. A formal approach to real-Time systems. Springer.
   Google Scholar
• Zhou, C., Hoare, C. A. R., & Ravn, A. P. (1991). A calculus of durations. Information Processing Letters, 40(5), 269–276. https://doi.org/10.1016/0020-0190(91)90122-X
   Web of Science ®Google Scholar
• Zuck, L. (1986). Past temporal logic [Ph.D. thesis, Weizmann Institute of Science].
   Google Scholar