1. Introduction
Relational transition systems (RTSs) are infinite-state transition systems whose states are labeled
by first-order (FO) interpretations [
1
]. Generic RTSs are RTSs with the property that states with
isomorphic interpretations induce the same transitions modulo renaming of objects [
2, 3
]. This
implies that, whenever the current state has a successor state where new, (locally) fresh objects
are injected, what matters about such fresh objects is only how they relate to each other and to
those already present in the current state. Genericity of an RTS is indeed reminiscent of the
well-known notion of genericity in first-order logic and relational databases [
4
].
Generic RTSs naturally capture the execution semantics of a variety of dynamic systems
operating over relational data (henceforth called data-aware dynamic systems), which have
been investigated in AI, BPM, and data management. Example of such systems are: (i) action
theories in the Situation Calculus [
5, 6, 7
], possibly operating over description-logic knowledge
bases [
8, 9, 10, 11
]; (ii) multiagent systems with data-aware, interacting agents [
12, 13, 14, 15
];
(iii) artifact- and data-centric business processes [
16, 17, 18
]; (iv) variants of colored Petri nets
where tokens carry (tuples of) data that can be compared by (in)equality [
19, 20, 21, 22
].
LGOBE
http://www.inf.unibz.it/~calvanese/ (D. Calvanese); http://www.diag.uniroma1.it/degiacomo/ (G. De Giacomo);
A long series of works has investigated how to analyze these systems, focusing in particular
on verification [
3, 13, 18, 23, 7
] and synthesis (typically, planning) [
24, 9, 11
]. Notably, properties
of interest have to combine, in this setting, temporal/dynamic operators with the ability of
querying the interpretations contained in the state, in turn making it possible to predicate on
the (un)desired evolution of objects and relations as the system unfolds. Natural candidates to
express such propreties are thus first-order temporal logics.
In this extended abstract, we summarize the main body of results on verification of first-order
temporal logics over generic RTSs that we have obtained in a decade-long research program.
2. Verification of Generic RTSs
Verification of generic RTSs is undecidable even under severe restrictions on the system dynamics
and on the signature of the FO interpretations. In fact, it is undecidable to even check reachability
of a proposition in data-aware dynamic systems that manipulate two unary relations through
simple actions that can (i) test whether one of the relations is empty, (ii) insert a new object in
one of them, (iii) remove an object from one of them provided that an object exists [
25, 26
].
State-boundedness. In this simple systems, undecidability resides in the ability of the system
to accumulate unboundedly many data in a single state. To control this ability, the notion of
state-boundedness has been introduced in [
12, 18
] and further studied in [
27
]. In a state-bounded
RTS, every state contains a bounded number of objects. Infinitely many distinct objects can be
potentially observed along a run, but only boundedly many can be accumulated in each state.
State-boundedness is a semantic property, decidable to check for a given bound and
undecidable to check if the bound is not known [
8, 7
]. In this light, diferent data-aware dynamic
systems that provide compact ways of specifying generic RTSs have been studied, with the
aim of identifying classes that guarantee that the corresponding RTS is indeed state-bounded.
This has been done considering: (i) suficient, syntactic conditions over the system
specification [
8, 27
]; (ii) action theories with fading memory [
7
]; (iii) resource-constrained colored Petri
nets [
20
]; (iv) controlled generation of fresh identifiers and other modeling guidelines [
28, 29
].
State-boundedness is essential towards singling out decidable classes for verification. Distinct
results are obtained for branching- vs linear-time first-order temporal logics.
Branching-time FO temporal logics. In [
2, 3
], it is shown that verification of the full FO
-calculus is decidable over state-bounded, generic RTSs. This is proved constructively, showing
how to compute a finite-state abstract RTSs that is guaranteed to satisfy all and only the FO
-calculus properties of the original one. The abstraction is built by considering the input
RTS, the bound, and the number of variables contained in the formula of interest. Notably, the
abstraction can be computed also without fixing a specific value for the bound [
8
].
In [
8, 2, 3
], fragments of the full FO -calculus are studied. Of particular interest is the one
with persistent quantification , where FO quantification tracks over time only the identity of
objects that remain active in consecutive states (whereas objects disappearing from a state are
not tracked anymore). For this fragment, it is shown that an abstract RTS can be constructed
independently from the formula to verify, that is, considering only the input RTS.
–
Linear-time FO temporal logics. In [
3
], it is shown that FO LTL behaves radically diferently
from the FO -calculus: verification of FO LTL properties is undecidable over generic,
statebounded RTSs with a bound of 1. This is particularly interesting, as it implies that in the
FO setting, the -calculus does not subsume LTL, diferently from the propositional setting.
In [
26
], the reason for undecidability is singled out, thanks to a reduction from LTL with freeze
quantifiers [
30
]: it resides in the ability of the logic to unrestrictedly quantify over objects that
may be arbitrarily far away from each other. This, in turn, hints that decidability may hold for
FO LTL with persistent quantification. As shown in [
26
], this is indeed the case, and further
decidability results are obtained for the problem of monitoring state-bounded, evolving traces.
Akcnowledgements
This work is partly supported by the ERC Advanced Grant WhiteMech (No. 834228), the
EU ICT-48 2020 project TAILOR (No. 952215), the Sapienza Project DRAPE, the Italian Basic
Research (PRIN) projects HOPE and PINPOINT, the unibz ID 2020 project SMART-APP, and the
Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and
Alice Wallenberg Foundation.