This paper studies the following problem: given a relational data schema, a temporal property over the schema, and a process that modifies the data instances, how can we enforce the property during each step of the process execution? Temporal properties are defined using a first-order future time LTL (FO-LTL) and they are evaluated under finite and fixed domain assumptions. Under such restrictions, existing techniques for monitoring propositional formulas can be used, but they would require exponential space in the size of the domain. Our approach is based on the construction of a first-order automaton that is able to perform the monitoring incrementally and by using exponential space in the size of the property. Technically, we show that our mechanism captures the semantics of FO-LTL on finite but progressing sequences of instances, and it reports satisfaction or dissatisfaction of the property at the earliest possible time. © 2013 Springer-Verlag.
Runtime enforcement of first-order LTL properties on data-aware business processes / DE MASELLIS, Riccardo; Jianwen, Su. - 8274 LNCS:(2013), pp. 54-68. (Intervento presentato al convegno 11th International Conference on Service-Oriented Computing, ICSOC 2013 tenutosi a Berlin nel 2 December 2013 through 5 December 2013) [10.1007/978-3-642-45005-1_5].
Runtime enforcement of first-order LTL properties on data-aware business processes
DE MASELLIS, RICCARDO;
2013
Abstract
This paper studies the following problem: given a relational data schema, a temporal property over the schema, and a process that modifies the data instances, how can we enforce the property during each step of the process execution? Temporal properties are defined using a first-order future time LTL (FO-LTL) and they are evaluated under finite and fixed domain assumptions. Under such restrictions, existing techniques for monitoring propositional formulas can be used, but they would require exponential space in the size of the domain. Our approach is based on the construction of a first-order automaton that is able to perform the monitoring incrementally and by using exponential space in the size of the property. Technically, we show that our mechanism captures the semantics of FO-LTL on finite but progressing sequences of instances, and it reports satisfaction or dissatisfaction of the property at the earliest possible time. © 2013 Springer-Verlag.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
