State-Boundedness in Data-Aware Dynamic Systems

verification turns out to be undecidable even for propositional reachability properties (Deutsch et al. 2009; Belardinelli, Lomuscio, and Patrizi 2012; Bagheri Hariri et al. 2013b; 2013a). To mitigate this problem, an extensive amount of research has been devoted to find suitable classes of data-aware dynamic systems for which verification of first-order temporal properties becomes decidable. In particular, a plethora of recent works has shown that verification of data-aware dynamic systems working over unboundedly many data is decidable even for very rich temporal logics, provided that the system is state-bounded. For example, Belardinelli, Lomuscio, and Patrizi (2012) show decidability of verification of state-bounded (there called b-bounded) artifact centric multiagent systems (ACMASs) for a first-order, epistemic variant of CTL, with active domain quantification that applies across time points. Bagheri Hariri et al. (2013b) give a key decidability result for the verification of state-bounded Data-Centric Dynamic Systems (DCDSs) against a first-order variant of the µ-calculus with a limited form of quantification across time. Within the research line of reasoning about actions, De Giacomo, Lesperance, and Patrizi (2012) show that (state-)bounded Situation Calculus theories can be verified against a first-order variant of the µ-calculus, without quantification across states. Notably, in all these cases stateboundedness guarantees the existence of a faithful (sound and complete) finite-state abstraction of the system, paving the way for the application of standard model checking tools. Verification of dynamic systems that manipulate data, stored in a database or ontology, has lately received increasing attention. A plethora of recent works has shown that verification of systems working over unboundedly many data is decidable even for very rich temporal properties, provided that the system is state-bounded. This condition requires the existence of an overall bound on the amount of data stored in each single state along the system evolution. In general, checking stateboundedness is undecidable. An open question is whether it is possible to isolate significant classes of dynamic systems for which state-boundedness is decidable. In this paper we provide a strong negative answer, by resorting to a novel connection with variants of Petri nets. In particular, we show undecidability for systems whose data component contains unary relations only, and whose action component queries and updates such relations in a very limited way. To contrast this result, we propose interesting relaxations of the sufficient conditions proposed in the concrete setting of Data-Centric Dynamic Systems, building on recent results on chase termination for tuple-generating dependencies.

Authors

• Babak Bagheri Hariri
• Diego Calvanese
• Marco Montali
• Alin Deutsch

Keywords

No keywords are indexed for this paper.