Modeling and verification of dynamic systems operating over a relational representation of states are increasingly investigated problems in AI, Business Process Management and Database Theory. To make these systems amenable to verification, the amount of information stored in each state needs to be bounded, or restrictions are imposed on the preconditions and effects of actions. We lift these restrictions by introducing the framework of relational action bases (RABs), which generalizes existing frameworks and in which unbounded relational states are evolved through actions that can (1) quantify both existentially and universally over the data, and (2) use arithmetic constraints.We then study parameterized safety of RABs via (approximated) SMT-based backward search, singling out essential meta-properties of the resulting procedure, and showing how it can be realized by an offthe-shelf combination of existing verification mod- ules of the state-of-the-art MCMT model checker. We demonstrate the effectiveness of this approach on a benchmark of data-aware business processes. Finally, we show how universal invariants can be exploited to make this procedure fully correct.
Safety Verification and Universal Invariants for Relational Action Bases / S. Ghilardi, A. Gianola, M. Montali, A. Rivkin - In: Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence / [a cura di] E. Elkind. - [s.l] : International Joint Conferences on Artificial Intelligence Organization, 2023. - ISBN 978-1-956792-03-4. - pp. 3248-3257 (( Intervento presentato al 32. convegno International Joint Conference on Artificial Intelligence tenutosi a Macao nel 2023 [10.24963/ijcai.2023/362].
Safety Verification and Universal Invariants for Relational Action Bases
S. GhilardiPrimo
;
2023
Abstract
Modeling and verification of dynamic systems operating over a relational representation of states are increasingly investigated problems in AI, Business Process Management and Database Theory. To make these systems amenable to verification, the amount of information stored in each state needs to be bounded, or restrictions are imposed on the preconditions and effects of actions. We lift these restrictions by introducing the framework of relational action bases (RABs), which generalizes existing frameworks and in which unbounded relational states are evolved through actions that can (1) quantify both existentially and universally over the data, and (2) use arithmetic constraints.We then study parameterized safety of RABs via (approximated) SMT-based backward search, singling out essential meta-properties of the resulting procedure, and showing how it can be realized by an offthe-shelf combination of existing verification mod- ules of the state-of-the-art MCMT model checker. We demonstrate the effectiveness of this approach on a benchmark of data-aware business processes. Finally, we show how universal invariants can be exploited to make this procedure fully correct.File | Dimensione | Formato | |
---|---|---|---|
0362.pdf
accesso aperto
Tipologia:
Publisher's version/PDF
Dimensione
230.85 kB
Formato
Adobe PDF
|
230.85 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.