Expressive completeness by separation for discrete time interval temporal logic with expanding modalities. (English) Zbl 07861405
Summary: Recently we established an analog of Gabbay’s separation theorem about linear temporal logic (LTL) for the extension of Moszkowski’s discrete time propositional Interval Temporal Logic (ITL) by two sets of expanding modalities, namely the unary neighbourhood modalities and the binary weak inverses of ITL’s chop operator. One of the many useful applications of separation in LTL is the concise proof of LTL’s expressive completeness wrt the monadic first-order theory of \(\langle\omega,<\rangle\) it enables. In this paper we show how our separation theorem about ITL facilitates a similar proof of the expressive completeness of ITL with expanding modalities wrt the monadic first- and second-order theories of \(\langle\mathbb{Z},<\rangle\).
MSC:
| 03B44 | Temporal logic |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
Keywords:
expressive completeness; interval temporal logic; expanding modalities; Gabbay separation; theory of computationReferences:
| [1] | Pnueli, A., The temporal logic of programs, (Proceedings of the 18th IEEE Symposium Foundations of Computer Science, 1977, IEEE), 46-57 |
| [2] | Gabbay, D. M., Declarative past and imperative future: executable temporal logic for interactive systems, (Proceedings of the Colloquium of Temporal Logic in Specification. Proceedings of the Colloquium of Temporal Logic in Specification, LNCS, vol. 398, 1989, Springer), 67-89 |
| [3] | Gabbay, D.; Hodkinson, I.; Reynolds, M., Temporal Logic: Mathematical Foundations and Computational Aspects. Volume i, 1994, Oxford University Press · Zbl 0921.03023 |
| [4] | Guelev, D. P.; Moszkowski, B. C., A separation theorem for discrete-time interval temporal logic, J. Appl. Non-Class. Log., 32, 1, 28-54, 2022 · Zbl 1517.03014 |
| [5] | Moszkowski, B., Executing Temporal Logic Programs, 1986, Cambridge University Press |
| [6] | Cau, A.; Moszkowski, B.; Zedan, H., ITL web pages, URL: |
| [7] | Moszkowski, B. C., Reasoning about Digital Circuits, 1983, Stanford University: Stanford University Stanford, Ph.D. thesis |
| [8] | Goranko, V.; Montanari, A.; Sciavicco, G., A road map of interval temporal logics and duration calculi, J. Appl. Non-Class. Log., 14, 1-2, 9-54, 2004 · Zbl 1181.03012 |
| [9] | Monica, D. D.; Goranko, V.; Montanari, A.; Sciavicco, G., Interval temporal logics: a journey, Bull. Eur. Assoc. Theor. Comput. Sci., 105, 73-99, 2011 · Zbl 1275.03087 |
| [10] | Halpern, J. Y.; Shoham, Y., A propositional logic of time intervals, (Proceedings of LICS’86, 1986, IEEE Computer Society Press), 279-292 |
| [11] | Allen, J. F., Maintaining knowledge about temporal intervals, Commun. ACM, 26, 11, 832-843, 1983 · Zbl 0519.68079 |
| [12] | Venema, Y., A modal logic for chopping intervals, J. Log. Comput., 1, 4, 453-476, 1991 · Zbl 0744.03022 |
| [13] | Chaochen, Zhou; Hansen, M. R., Duration Calculus. A Formal Approach to Real-Time Systems, 2004, Springer · Zbl 1071.68062 |
| [14] | Moszkowski, B. C.; Guelev, D. P., An application of temporal projection to interleaving concurrency, Form. Asp. Comput., 29, 4, 705-750, 2017 · Zbl 1370.68216 |
| [15] | Rasmussen, T. M., Signed interval logic, (Flum, J.; Rodríguez-Artalejo, M., CSL ’99, Proceedings. CSL ’99, Proceedings, LNCS, vol. 1683, 1999, Springer), 157-171 · Zbl 0942.03027 |
| [16] | Hughes, G. E.; Cresswell, M. J., A Companion to Modal Logic, 1984, Methuen: Methuen London · Zbl 0625.03005 |
| [17] | Bowman, H.; Thompson, S., A decision procedure and complete axiomatisation of finite interval temporal logic with projection, J. Log. Comput., 13, 2, 195-239, 2003 · Zbl 1050.03012 |
| [18] | Kamp, J. A.W., Tense Logic and the Theory of Linear Order, 1968, University of California: University of California Los Angeles, Ph.D. thesis |
| [19] | Moszkowski, B. C., An automata-theoretic completeness proof for interval temporal logic, (Montanari, U.; Rolim, J. D.P.; Welzl, E., ICALP 2000, Proceedings. ICALP 2000, Proceedings, LNCS, vol. 1853, 2000, Springer), 223-234 · Zbl 0973.03508 |
| [20] | Moszkowski, B. C., A complete axiomatization of interval temporal logic with infinite time, (LICS, 2000, 2000, IEEE Computer Society), 241-252 |
| [21] | Thomas, W., Languages, automata, and logic, (Rozenberg, G.; Salomaa, A., Handbook of Formal Languages. Handbook of Formal Languages, Beyond Words, vol. 3, 1997, Springer), 389-455 · Zbl 0866.68057 |
| [22] | Brzozowski, J. A., Derivatives of regular expressions, J. ACM, 11, 4, 481-494, 1964 · Zbl 0225.94044 |
| [23] | Brzozowski, J. A., Canonical regular expressions and minimal state graphs for definite events, (Proc. Symposium of Mathematical Theory of Automata, 1962), 529-561 · Zbl 0116.33605 |
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.
