Abstract
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.