Verification of Human Driven Data-Centric Dynamic Systems

Babak Bagheri Hariri, Diego Calvanese, Giuseppe De Giacomo, Marco Montali, and Alin Deutsch

Proc. of the 2014 AAAI Spring Symposium on Formal Verification and Modeling in Human-Machine Systems. Volume SS-14-02 of AAAI Technical Reports. 2014.

We study the foundations of human driven, data-aware business processes, by leveraging on the recently proposed framework of Data-Centric Dynamic Systems (DCDSs). The processes we consider simultaneously capture the control-flow of activities, the manipulation of data maintained in a full-fledged relational database, and the interaction with human users. In particular, users can input new data into the system by relying on different interaction modalities: deterministic input, nondeterministic input, and value selection, considering both finite or countably infinite domains for the input data. With this extended framework, we reassessed the decidability results obtained for the formal verification of DCDSs against rich temporal properties, specified using first-order variants of the mu-calculus.


@inproceedings{AAAI-Symp-2014,
   title = "Verification of Human Driven Data-Centric Dynamic Systems",
   year = "2014",
   author = "Bagheri Hariri, Babak and Diego Calvanese and De Giacomo,
Giuseppe and Marco Montali and Alin Deutsch",
   booktitle = "Proc. of the 2014 AAAI Spring Symposium on Formal
Verification and Modeling in Human-Machine Systems",
   volume = "SS-14-02",
   publisher = "AAAI Press",
   series = "AAAI Technical Reports",
}
pdf url