Traditional approaches to modeling and verification of systems based on model checking of linear-time properties are usually propositional in nature (e.g., LTL). However, many real-world applications, such as business process management and knowledge-base-driven systems, handle data that intrinsically requires first-order formalisms. Recently, the LTLf Modulo Theory ( LTLfMT) has been introduced to model and verify such systems. LTLfMT extends LTLf by replacing propositions with first-order formulas over arbitrary theories, à la SMT. LTLfMT satisfiability is solved with the symbolic tableau modulo theories approach and implemented in the state-of-the-art BLACK satisfiability checker, relying on out-of-the-box SMT solvers. This paper recaps such recent developments and discuss open research directions.
Since the seminal work by Pnueli [
In the context of traditional model checking, the models under investigation are intrinsically
ifnite-state : the underlying assumption is that real-world systems can be abstracted by a finite
representation of their control-flow, disregarding any other source of infiniteness that can arise
from the presence of the actual data being manipulated (such as the values of program variables).
This abstraction allows one to employ explicit and exhaustive search procedures in the finite
space of all configurations [
This assumption matches with the expressive power of formalisms such as LTL and LTLf, which have in common one limitation: they can be employed to only represent transition systems whose states are finitely many and are characterized by evaluating propositional atoms.
However, in real-world scenario the propositional nature of LTL and LTLf can be problematic:
for instance, this is the case when modeling data-aware processes [
There is a plethora of similar situations where the data component comes to the picture,
turning the systems to the infinite-state case . For instance, one can consider the use case of
data-aware planning, i.e., planning problems [
In order to match the expressiveness needed for modeling and reasoning about such scenarios, a new logic called LTLf Modulo Theories (LTLfMT) was recently introduced [15]. This logic extends LTLf by replacing propositional symbols with first-order formulas over an arbitrary theory, in the spirit of Satisfiability Modulo Theories (SMT) [16]. While LTLfMT is easily seen to be undecidable in general, for decidable theories it is semi-decidable, i.e., a positive answer can always be obtained for satisfiable instances, while reasoning might not terminate over unsatisfiable ones. Given the complexity of the problems and scenarios such as those mentioned above, where reasoning is inherently undecidable anyway, being able to solve satisfiable instances is a compromise worth studying.
The satisfiability checking problem for LTLfMT is solved by using the symbolic tableau modulo theory (STMT) approach [15]. A one-pass and tree-shaped tableau [17, 18], where any accepted branch corresponds to a model of the formula, is symbolically traversed by means of suitable SMT encodings. This approach allows one to reason on LTLfMT by exploiting recent (and future) advancements in SMT solving techniques. The approach has been implemented in the state-of-the-art BLACK tool [19, 20], which builds on top of well-established and highly performing SMT solvers such as Z3 [21] and cvc5 [22], showing promising results [15].
In this paper, we describe LTLfMT and discuss the recent results related to this logic, we describe how interesting infinite-state systems can be expressed and verified, and we outline interesting future research directions that this approach naturally opens.
LTLfMT extends LTLf by replacing proposition letters with first-order formulas over arbitrary theories, à la Satisfiability Modulo Theories (SMT).
Instead of going into the details of syntax and semantics, let us discuss a few examples: = 0 ∧ ((○ = + 1) U = 42) = 0 ∧ G∼(○ > ∧ ∃( = + ))
Intuitively, the first formula says that the variable starts at zero, then increments at each time ste p∼ (○ = + 1), until it reaches the value 42 (. . . U = 42).
The second formula states that the variable similarly starts at 0, and that in any time point (G(. . .)), the value of increases∼ (○ > ), and is an even number (∃( = + )). In other words, forms a monotonically increasing sequence of even numbers.
The term constructo r∼s ○ and ○ are a crucial feature. They both represent, in a diferent
way, the value of at the next time point. The diference lies in how these terms behave at
the end of the finite trace. When a first-order formula contains some ○ , the next state is
required to exist, while it is not required to exist if it contains onl∼ y ○ terms. This replicates
the diference between the tomorrow and weak tomorrow temporal operators in LTLf [
The syntax of LTLfMT is based on arbitrary first-order formulas over a given theory, including quantified formulas, with the restriction that the only temporal operators that can appear inside a quantified formula are tomorrow (X) and weak tomorrow (X̃︀). First-order variables and next/weak next constructors can be freely combined into arbitrary first-order terms involving function symbols and constants. The semantics of LTLfMT is defined over finite sequences of standard ifrst-order models over the formula’s vocabulary. Each function symbol and relation can either be rigid, i.e., fixed over time, or not, i.e., time-evolving.
Satisfiability of LTLfMT is easily seen to be undecidable in general, but semi-decision procedures can be provided. In particular, LTLfMT can be semi-decided by a symbolic tableau modulo theory (STMT) approach [15]. Given an LTLfMT formula , a one-pass and tree-shaped tableau [17, 18] is symbolically traversed in a breadth-first fashion by means of an SMT encoding that represents all the accepted branches of the tree of at most length . If such a formula is satisfiable for some > 0, a model is found. Otherwise, is incremented. Unsatisfiable formulas may cause this procedure to loop infinitely, as expected for a semi-decidable problem. This procedure has been implemented in the state-of-the-art BLACK1 satisfiability checker [ 15].
LTLfMT specifications can be verified against knowledge-base-driven dynamic systems represented by symbolic transition systems whose transitions depend on the first-order states. These systems can be directly expressed as LTLfMT formulas (similarly to how standard finitestate transition systems can be expressed in LTL) and the model-checking problem of LTLfMT specifications over such systems can be reduced to a LTLfMT satisfiability check.
Such models can be employed to approach a diverse variety of real-world data-driven scenarios
including data-aware business processes [
Our framework is the first approach capable of representing such an ample set of diferent systems, while handling general linear-time temporal properties (i.e., not only safety or reachability objectives). Moreover, not only we leverage state-of-the-art SMT solving techniques, but we do so in a robust software tool (BLACK) that is engineered to be ready for real-world usage.
Many future directions are opened by the introduction of LTLfMT and our approach. From a
modeling perspective, it is important to classify precisely the kinds of systems discussed in
the literature that can be handled by our approach, comparing the eficiency of BLACK with
existing tools, such as VERIFAS [27] or MCMT [
While we focused on the satisfiability problem, the realizability problem is of foremost interest as well. This is the problem of deciding whether there exists a strategy to play a game against an adversary environment in such a way that an LTLfMT formula can be guaranteed to be satisefid. This problem, in the case of LTLf specifications, is already very hard ( 2EXPTIME-complete). In the case of LTLfMT, should it still be semi-decidable, it would open the doors to a large variety of applications in the context of the synthesis of infinite-state systems, rather than of their verification.
Then, applications of LTLfMT outside the verification field, and more oriented toward artificial intelligence, are natural developments. In particular, while LTLf can naturally express STRIPS automated planning problems [33], LTLfMT may be employed to approach a novel class of data-aware planning domains. In these models, agents can employ actions whose preconditions depend on the state of a full-fledged relational database, an ontology-based knowledge base, or complex first-order definable data structures (such as lists, trees, graphs, etc.), and whose efects actively modify such data containers.
By reducing such data-aware planning problems to LTLfMT satisfiability, one may leverage existing reasoning tools such as BLACK to solve them. Moreover, should LTLfMT realizability turn out to be semi-decidable as well, fully observable nondeterministic (FOND) data-aware planning domains could be handled as well. A practically applicable approach to data-aware FOND planning is one of the most promising long-term goal of this line of research.
This work is partially supported by the Italian Ministry of University and Research under the PRIN program, grant B87G22000450001 (PINPOINT), and by the Free University of BozenBolzano with the SMART-APP, ADAPTERS, and TOTA projects. in structured environments, in: Proc. of OVERLAY 2021, volume 2987 of CEUR Workshop Proceedings, CEUR-WS.org, 2021, pp. 43–48. URL: http://ceur-ws.org/Vol-2987/paper8.pdf. [15] L. Geatti, A. Gianola, N. Gigante, Linear temporal logic modulo theories over finite traces, in: Proc. of IJCAI 2022, ijcai.org, 2022, pp. 2641–2647. URL: https://doi.org/10.24963/ijcai. 2022/366. doi: 10.24963/ijcai.2022/366. [16] C. W. Barrett, C. Tinelli, Satisfiability modulo theories, in: Handbook of Model Checking, Springer, 2018, pp. 305–343. URL: https://doi.org/10.1007/978-3-319-10575-8_11. doi: 10.1007/978-3-319-10575-8_11. [17] M. Reynolds, A new rule for LTL tableaux, in: Proc. of GandALF 2016, 2016, pp. 287–301.
doi: 10.4204/EPTCS.226.20. [18] L. Geatti, N. Gigante, A. Montanari, M. Reynolds, One-pass and tree-shaped tableau systems for TPTL and TPTLb+ past, Information and Computation 278 (2021) 104599. [19] L. Geatti, N. Gigante, A. Montanari, A SAT-based encoding of the one-pass and treeshaped tableau system for LTL, in: Proc. of TABLEAUX 2019, 2019, pp. 3–20. URL: https://doi.org/10.1007/978-3-030-29026-9_1. doi: 10.1007/978-3-030-29026-9_1. [20] L. Geatti, N. Gigante, A. Montanari, G. Venturato, Past matters: Supporting LTL+Past in the BLACK satisfiability checker, in: Proc. of TIME 2021, 2021. [21] L. M. de Moura, N. S. Bjørner, Z3: an eficient SMT solver, in: Proc. of TACAS 2008, volume 4963 of Lecture Notes in Computer Science, Springer, 2008, pp. 337–340. URL: https://doi.org/10.1007/978-3-540-78800-3_24. doi: 10.1007/978-3-540-78800-3_24. [22] H. Barbosa, C. W. Barrett, M. Brain, G. Kremer, H. Lachnitt, M. Mann, A. Mohamed, M. Mohamed, A. Niemetz, A. Nötzli, A. Ozdemir, M. Preiner, A. Reynolds, Y. Sheng, C. Tinelli, Y. Zohar, cvc5: A versatile and industrial-strength SMT solver, in: Proc. of TACAS 2022, volume 13243 of Lecture Notes in Computer Science, Springer, 2022, pp. 415–442.
URL: https://doi.org/10.1007/978-3-030-99524-9_24. doi: 10.1007/978-3-030-99524-9_24. [23] G. De Giacomo, R. D. Masellis, M. Montali, Reasoning on LTL on finite traces: Insensitivity to infiniteness, in: Proc. of AAAI 2014, 2014, pp. 1027–1033. [24] D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, A. Rivkin, Formal modeling and SMTbased parameterized verification of data-aware BPMN, in: Proc. of BPM 2019, 2019, pp. 157–175. doi: 10.1007/978-3-030-26619-6_12. [25] A. Gianola, SMT-based safety verification of data-aware processes: Foundations and applications, in: Proc. of the Best Dissertation Award, Doctoral Consortium, and Demonstration & Resources Track at BPM 2022, volume 3216 of CEUR Workshop Proceedings, CEUR-WS.org, 2022, pp. 20–24. URL: http://ceur-ws.org/Vol-3216/paper_133.pdf. [26] M. Bojanczyk, L. Segoufin, S. Torunczyk, Verification of database-driven systems via amalgamation, in: Proc. of PODS 2013, ACM, 2013, pp. 63–74. doi: 10.1145/2463664.2465228. [27] Y. Li, A. Deutsch, V. Vianu, VERIFAS: A practical verifier for artifact systems, Proceedings of the VLDB Endowment 11 (2017) 283–296. [28] D. Calvanese, A. Gianola, A. Mazzullo, M. Montali, SMT-based safety verification of dataaware processes under ontologies (preliminary results), in: Proc. of DL 2021, volume 2954 of CEUR Workshop Proceedings, CEUR-WS.org, 2021. URL: http://ceur-ws.org/Vol-2954/ paper-9.pdf. [29] J. Claßen, M. Liebenberg, G. Lakemeyer, B. Zarrieß, Exploring the boundaries of decidable verification of non-terminating golog programs, in: Proc. of AAAI 2014, AAAI Press, 2014, pp. 1012–1019. URL: http://www.aaai.org/ocs/index.php/AAAI/AAAI14/paper/view/8625. [30] B. Zarrieß, J. Claßen, Decidable verification of golog programs over non-local efect actions, in: Proc. of AAAI 2016, AAAI Press, 2016, pp. 1109–1115. URL: http://www.aaai.org/ocs/ index.php/AAAI/AAAI16/paper/view/12283. [31] S. Ghilardi, A. Gianola, M. Montali, A. Rivkin, Delta-BPMN: A concrete language and veriifer for data-aware BPMN, in: Proc. of BPM 2021, volume 12875 of Lecture Notes in Computer Science, Springer, 2021, pp. 179–196. URL: https://doi.org/10.1007/978-3-030-85469-0_13. doi: 10.1007/978-3-030-85469-0_13. [32] D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, A. Rivkin, Model completeness, uniform interpolants and superposition calculus, J. Autom. Reason. 65 (2021) 941–969. doi: 10.1007/s10817-021-09596-x. [33] M. Cialdea Mayer, C. Limongelli, A. Orlandini, V. Poggioni, Linear temporal logic as an executable semantics for planning languages, J. Log. Lang. Inf. 16 (2007) 63–89. doi: 10.1007/s10849-006-9022-1.