We provide an overview of the main attempts to formalize and reason about the evolution over time of complex domains, through the lens of first-order temporal logics . Diferent communities have studied similar problems for decades, and some unification of concepts, problems and formalisms is a much needed but not simple task.
Linear temporal logic (LTL) is a well-known extension of classical propositional logic by means
of time-related modalities, such as ‘tomorrow’, ‘eventually’, ‘always’, and ‘until’ [
First-order linear temporal logic (FOLTL), in turn, lifts LTL from propositional to first-order logic [11, 12, 13, 14, 15, 16]. Unfortunately, its increased expressive power comes at a high computational cost, compared to its propositional counterpart. As FOLTL contains first-order logic, its validity problem is clearly undecidable. Not only that: the set of valid formulas in the full FOLTL language is not even recursively enumerable, and this result holds already for the fragments where only two variables, or only unary predicates (so-called monadic) are allowed [11].
Such limitations, however, have not impaired the research on FOLTL-based formalisms that combine reasoning over a time dimension, on the one hand, and over an object dimension, on the other. Given this two-dimensional essence, FOLTL is indeed a natural choice when it comes to modelling and verification of dynamic systems in presence of data that evolve over time, or whenever the task is to formalise, and reason about, the temporal properties of objects in a changing domain. Over the last couple of decades, multiple research trends that involve FOLTL and its fragments have been developed. Based on their primary focus, we attempt to categorise such diverse directions in terms of the following (neither mutually exclusive, nor collectively exhaustive) family resemblances: on the one hand, research approaches that focus on modeling and verification of infinite-state systems ; on the other hand, a line of study oriented towards temporal ontology-based knowledge representation and reasoning.
Given the diferences in goals and objectives between these communities, it is a non-trivial task to provide detailed comparisons of the respective results within a uniform framework. As a first step in this direction, we use the privileged viewpoint of FOLTL to illustrate formalisms from the two communities—by focusing, in particular, on two recent representatives thereof, namely, LTL modulo theories and temporal free description logics without the rigid designator assumption (RDA), respectively.
In FOLTL, on the syntactic level of the first-order component, function and constant symbols can be either introduced by suitable definitions starting from predicate symbols [ 12], or taken as primitive elements of the language [17, 13]. FOLTL both with and without equality has also been considered [11]. Semantically, other than the choice of structure representing the designated flow of time (e.g. reals, integers, natural numbers, or initial segments of the latter), a number of options are available. Regarding the domain of interpretation, a standard solution is to equip models with a constant domain, which is shared by all time points. This assumption is the most general, since semantics based on varying or expanding domains can be simulated in constant domain models by means of a suitable existence predicate [11, 14].
When it comes to the interpretation over time of the non-logical symbols (i.e., constant, function, and predicate symbols, excluding equality), it is possible to either allow the extension of function and predicate symbols (other than equality) to change from one instant to another, making them flexible , or to impose instead a rigidity condition that fixes the same interpretation at all times [17]. This is in contrast with the assignment of variables, and with the interpretation of constants, in a FOLTL model, since their mapping into elements of the domain typically is not relative to any time point [13]. When a rigidity condition is imposed on constant and function symbols, they are said to behave as rigid designators [14], meaning that they are forced to designate the same object at all time points.
In order to drop such a rigid designator assumption, the syntactic and semantic machineries need to be somewhat modified. Several approaches in first-order modal and intensional logic, other than in FOLTL [18, 12, 13, 14], have devised mechanisms to introduce constant and function symbols, as well as (possibly quantifiable) variables, as flexible individual concepts that can change their interpretation over time. Standard examples of non-rigid designators in a temporal setting are time-dependent definite descriptions , such as ‘the value that variable will take tomorrow’. First-order modal formalisms involving definite description as terms of the language have been investigated as well [19, 20, 21, 22]. In light of these FOLTL features, in the following we illustrate formalisms that have been proposed in the communities of infinite-state verification and of temporal ontology-based knowledge representation, respectively.
Modelling and verification of infinite-state systems. A significant line of research in verification of data-driven systems has focussed on the extension of LTL with concrete domains [23]. Concrete domains are relational structures, such as the natural or the rational numbers equipped with the the binary relations of strict linear order and identity over them. By replacing proposition letters with atomic constraints over terms of the language, expressed by means of the relational signature, LTL with concrete domains can express comparisons between term values that are allowed to change over time. For instance, taking as concrete domain the linear order of the natural numbers, the formula 2( < ○ ) can be used to express that, at all future time points, the value of will always be less than the value of at the subsequent instant (represented by ○ ). In this setting, a variable like plays the role of a non-rigid designator with a time-dependent interpretation over the constant domain. The interpretation of relational symbols, on the other hand, is rigid, hence fixed at all time points.
More recently, LTL modulo theories (LTLMT) has been introduced as a fragment of FOLTL, to leverage SMT-based techniques (see the BLACK framework [24]) for applications in the context of verification of data-aware processes [25, 26, 27, 28, 29, 30, 31] and, in general, infinite-state systems [32, 33, 34, 35]. Syntactically, LTLMT is obtained by replacing LTL propositional letters with purely first-order formulas, and similarly allowing for “timed” variables of the form ○ , used to refer to the value of at the next time point [36]. As such, it allows to express temporal constraints and perform reasoning tasks under the axioms of given first-order theories, such as linear integer or rational arithmetic, or equality and uninterpreted functions. For instance, given the first-order theory of linear integer arithmetic, with + as function and ≤ as relation symbols (plus the natural definitions for = and <), we can state the value of variable is initially set up to 0 and it is incremented by one until it reaches the value of 42, with the formula = 0 ∧ ((○ = + 1) = 42). Whenever the underlining first-order theory is decidable (as in the examples mentioned above), satisfiability in LTL MT is semi-decidable, and several decidable fragments have been identified as well in this setting [ 37]. While the first papers introducing this formalism have considered only rigid predicates and functions over a common domain, some ongoing work on LTLMT is moving in the direction of dropping this assumption. Temporal ontology-based knowledge representation and reasoning. The study of so-called monodic fragments of FOLTL has shown that decidability of the satisfiability problem can be regained by combining a decidable purely first-order fragment (such as the two-variable, or the monadic one) with a restriction on temporal operators that allows their application only over formulas with at most one free variable [38, 11, 39]. As an example,
∃Alive() ∧ 2∀(Alive() → ○ (¬Alive() ∧ ∃(isRememberedBy(, ) ∧ Alive()) is a monodic two-variable formula, stating that someone is currently alive and, at any time point in the future, anyone alive will not be anymore so in the next generation, but will be remembered by someone alive [40].
Strictly related to monodic fragments are temporal description logics [40], obtained by combining description logic (DL) formalisms (that can be seen as fragments of first-order logic) with linear temporal operators. For instance, the formula given above can be rephrased in a temporalised extension of the standard DL ℒ by means of an assertion stating that Alice, , is alive, Alive() and with the following concept inclusion, holding at all points in time, to capture the second conjunct above:
2(Alive ⊑ ○ (¬Alive ⊓ ∃isRememberedBy.Alive)).
For these formalisms, a quite neat complexity picture is available (we do not provide here a full
survey of the results; see [
However, to the best of our knowledge, despite the extensive research on temporal extensions
of DLs [
As it is often the case, diferent communities may have diferent perspectives on a class of closely related problems. In this context, we believe that an attempt at unifying techniques and formalisms might be beneficial to both communities. In this position paper, we notice the need of such an efort. On the one hand, techniques from the formal verification community might help knowledge representation with eficient reasoning techniques, given suitable fragments of FOLTL. On the other hand, existing work about FOLTL from the knowledge representation community might shed light on foundational issues of the formalisms used for verification of infinite-state systems, improving our understanding of the matter. A future initial step to establish a bridge between the two communities may be that of investigating the connections between temporal DLs without the RDA, on one side, and LTLMT, on the other.
A. Mazzullo acknowledges the support of the MUR PNRR project FAIR - Future AI Research (PE00000013), funded by the NextGenerationEU. [11] D. M. Gabbay, A. Kurucz, F. Wolter, M. Zakharyaschev, Many-dimensional Modal Logics:
Theory and Applications, North Holland Publishing Company, 2003. [12] T. Braüner, S. Ghilardi, First-order Modal Logic, in: Handbook of Modal Logic, Elsevier, 2007, pp. 549–620. [13] F. Kröger, S. Merz, Temporal Logic and State Systems, Texts in Theoretical Computer
Science. An EATCS Series, Springer, 2008. [14] M. Fitting, R. L. Mendelsohn, First-order Modal Logic, Springer Science & Business Media, 2012. [15] A. Artale, A. Mazzullo, A. Ozaki, Do you need infinite time?, in: Proceedings of the 28th International Joint Conference on Artificial Intelligence (IJCAI-19), ijcai.org, 2019, pp. 1516–1522. [16] A. Artale, A. Mazzullo, A. Ozaki, First-order temporal logic on finite traces: Semantic properties, decidable fragments, and applications, CoRR abs/2202.00610 (2022). [17] M. Abadi, Temporal-logic theorem proving, Ph.D. thesis, Stanford University, USA, 1987. [18] M. Fitting, First-order intensional logic, Ann. Pure Appl. Log. 127 (2004) 171–193. [19] G. E. Hughes, M. J. Cresswell, A New Introduction to Modal Logic, Routledge, 1996. [20] E. Orlandelli, Labelled calculi for quantified modal logics with definite descriptions, CoRR abs/2002.04855 (2020). URL: https://arxiv.org/abs/2002.04855. [21] A. Indrzejczak, Existence, definedness and definite descriptions in hybrid modal logic, in: Proceedings of the 13th Conference on Advances in Modal Logic (AiML-20), College Publications, 2020, pp. 349–368. [22] A. Artale, A. Mazzullo, Non-rigid designators in epistemic and temporal free description logics, in: Proceedings of the 2023 International Workshop on Description Logics (DL-23), CEUR Workshop Proceedings, CEUR-WS.org, 2023. [23] S. Demri, K. Quaas, Concrete domains in logics: a survey, ACM SIGLOG News 8 (2021) 6–29. [24] L. Geatti, N. Gigante, A. Montanari, A sat-based encoding of the one-pass and treeshaped tableau system for LTL, in: S. Cerrito, A. Popescu (Eds.), Proceedings of the 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, volume 11714 of Lecture Notes in Computer Science, Springer, 2019, pp. 3–20. doi:10.1007/978-3-030-29026-9\_1. [25] D. Calvanese, G. D. Giacomo, M. Montali, Foundations of data-aware process analysis: a database theory perspective, in: R. Hull, W. Fan (Eds.), Proceedings of the 32nd ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS 2013), ACM, 2013, pp. 1–12. [26] A. Deutsch, R. Hull, Y. Li, V. Vianu, Automatic verification of database-centric systems,
ACM SIGLOG News 5 (2018) 37–56. [27] A. Deutsch, Y. Li, V. Vianu, Verification of hierarchical artifact systems, ACM Trans.
Database Syst. 44 (2019) 12:1–12:68. [28] D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, A. Rivkin, Formal modeling and smtbased parameterized verification of data-aware BPMN, in: T. T. Hildebrandt, B. F. van Dongen, M. Röglinger, J. Mendling (Eds.), Business Process Management - 17th International Conference, BPM 2019, Vienna, Austria, September 1-6, 2019, Proceedings, volume 11675 of Lecture Notes in Computer Science, Springer, 2019, pp. 157–175. [29] D. Calvanese, G. D. Giacomo, M. Montali, F. Patrizi, Verification and monitoring for ifrst-order LTL with persistence-preserving quantification over finite and infinite traces, in: L. D. Raedt (Ed.), Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI 2022, Vienna, Austria, 23-29 July 2022, ijcai.org, 2022, pp. 2553–2560. [30] D. Calvanese, A. Gianola, A. Mazzullo, M. Montali, SMT safety verification of ontologybased processes, in: B. Williams, Y. Chen, J. Neville (Eds.), Thirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023, Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence, IAAI 2023, Thirteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2023, Washington, DC, USA, February 7-14, 2023, AAAI Press, 2023, pp. 6271–6279. [31] S. Ghilardi, A. Gianola, M. Montali, A. Rivkin, Safety verification and universal invariants for relational action bases, in: Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SAR, China, ijcai.org, 2023, pp. 3248–3257. [32] M. Abadi, The power of temporal proofs, Theor. Comput. Sci. 65 (1989) 35–83. [33] Y. Kesten, O. Maler, M. Marcus, A. Pnueli, E. Shahar, Symbolic model checking with rich assertional languages, Theor. Comput. Sci. 256 (2001) 93–112. [34] S. Ghilardi, S. Ranise, Backward reachability of array-based systems by SMT solving:
Termination and invariant synthesis, Log. Methods Comput. Sci. 6 (2010). [35] D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, A. Rivkin, Smt-based verification of data-aware processes: a model-theoretic approach, Math. Struct. Comput. Sci. 30 (2020) 271–313. [36] L. Geatti, A. Gianola, N. Gigante, Linear temporal logic modulo theories over finite traces, in: L. D. Raedt (Ed.), Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI 2022, Vienna, Austria, 23-29 July 2022, ijcai.org, 2022, pp. 2641–2647. [37] L. Geatti, A. Gianola, N. Gigante, S. Winkler, Decidable fragments of ltlf modulo theories, in: K. Gal, A. Nowé, G. J. Nalepa, R. Fairstein, R. Radulescu (Eds.), Proceedings of the 26th European Conference on Artificial Intelligence, volume 372 of Frontiers in Artificial Intelligence and Applications, IOS Press, 2023, pp. 811–818. doi:10.3233/FAIA230348. [38] F. Wolter, M. Zakharyaschev, Axiomatizing the monodic fragment of first-order temporal logic, Ann. Pure Appl. Log. 118 (2002) 133–145. [39] A. Degtyarev, M. Fisher, B. Konev, Monodic temporal resolution, ACM Trans. Comput.
Log. 7 (2006) 108–150. [40] C. Lutz, F. Wolter, M. Zakharyaschev, Temporal description logics: A survey, in: Proceedings of the 15th International Symposium on Temporal Representation and Reasoning (TIME-08), IEEE Computer Society, 2008, pp. 3–14. [41] I. M. Hodkinson, R. Kontchakov, A. Kurucz, F. Wolter, M. Zakharyaschev, On the computational complexity of decidable fragments of first-order linear temporal logics, in: Proceedings of the 10th International Symposium on Temporal Representation and Reasoning and of the 4th International Conference on Temporal Logic (TIME-ICTL-03), IEEE Computer Society, 2003, pp. 91–98. [42] A. Artale, R. Kontchakov, C. Lutz, F. Wolter, M. Zakharyaschev, Temporalising tractable description logics, in: Proceedings of the 14th International Symposium on Temporal Representation and Reasoning (TIME-07), IEEE Computer Society, 2007, pp. 11–22. [43] F. Baader, S. Ghilardi, C. Lutz, LTL over description logic axioms, ACM Trans. Comput.
Log. 13 (2012). [44] A. Artale, R. Kontchakov, F. Wolter, M. Zakharyaschev, Temporal description logic for ontology-based data access, in: F. Rossi (Ed.), Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI-13), IJCAI/AAAI, 2013, pp. 711–717. URL: http://www.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/view/6824. [45] A. Artale, R. Kontchakov, V. Ryzhikov, M. Zakharyaschev, A cookbook for temporal conceptual data modelling with description logics, ACM Trans. Comput. Log. 15 (2014) 25:1–25:50. [46] A. Artale, R. Kontchakov, A. Kovtunova, V. Ryzhikov, F. Wolter, M. Zakharyaschev, Firstorder rewritability of ontology-mediated queries in linear temporal logic, Artificial Intelligence (AIJ) 299 (2021). doi:https://doi.org/10.1016/j.artint.2021.103536. [47] A. Artale, R. Kontchakov, A. Kovtunova, V. Ryzhikov, F. Wolter, M. Zakharyaschev, First-order rewritability and complexity of two-dimensional temporal ontology-mediated queries, JAIR 75 (2022) 1223–1291. doi:10.1613/jair.1.13511. [48] V. Gutiérrez-Basulto, J. C. Jung, T. Schneider, Lightweight temporal description logics with rigid roles and restricted tboxes, in: Q. Yang, M. J. Wooldridge (Eds.), Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI-15), AAAI Press, 2015, pp. 3015–3021. URL: http://ijcai.org/Abstract/15/426. [49] F. Wolter, M. Zakharyaschev, Temporalizing description logics, in: Proceedings of the 2nd International Symposium on Frontiers of Combining Systems (FroCoS-98), Research Studies Press/Wiley, 1998, pp. 104–109. [50] A. Artale, R. Kontchakov, A. Kovtunova, V. Ryzhikov, F. Wolter, M. Zakharyaschev, Ontology-mediated query answering over temporal data: A survey, in: Proc. of the 24th Int. Symposium on Temporal Representation and Reasoning (TIME-17), volume 90 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Mons, Belgium, 2017, pp. 1:1–1:37. doi:10.4230/LIPIcs.TIME.2017.1. [51] A. Artale, A. Mazzullo, A. Ozaki, F. Wolter, On free description logics with definite descriptions, in: Proceedings of the 33rd International Workshop on Description Logics (DL-20), volume 2663 of CEUR Workshop Proceedings, CEUR-WS.org, 2020. [52] A. Artale, A. Mazzullo, A. Ozaki, F. Wolter, On free description logics with definite descriptions, in: Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning (KR-21), 2021, pp. 63–73. [53] A. Degtyarev, M. Fisher, A. Lisitsa, Equality and monodic first-order temporal logic, Studia Logica 72 (2002) 147–156.