Affiliations: [a] University of Chieti-Pescara, Viale Pindaro 42, 65127, Pescara, Italy. {emanuele.deangelis,fabio.fioravanti,cmeo}@unich.it | [b] University of Rome Tor Vergata, Via del Politecnico 1, 00133 Rome, Italy. pettorossi@info.uniroma2.it | [c] IASI-CNR, Via dei Taurini 19, 00185 Rome, Italy. maurizio.proietti@iasi.cnr.it
Correspondence:
[†]
Address for correspondence: University of Chieti-Pescara, Viale Pindaro 42, 65127, Pescara, Italy.
Note: [*] This work has been partially supported by the National Group of Computing Science (GNCS-INdAM). E. De Angelis, F. Fioravanti, and A. Pettorossi are research associates at IASI-CNR, Rome, Italy. All authors are members of the INdAM Research group GNCS.
Abstract: We present an operational semantics for time-aware business processes, that is, processes modeling the execution of business activities, whose durations are subject to linear constraints over the integers. We assume that some of the durations are controllable, that is, they can be determined by the organization that executes the process, while others are uncontrollable, that is, they are determined by the external world. Then, we consider controllability properties, which guarantee the completion of the execution of the process, satisfying the given duration constraints, independently of the values of the uncontrollable durations. Controllability properties are encoded by quantified reachability formulas, where the reachability predicate is recursively defined by means of constrained Horn clauses (CHCs). These clauses are automatically derived from the operational semantics of the process. Finally, we present two algorithms for solving the so called weak and strong controllability problems. Our algorithms reduce these problems to the verification of a set of quantified integer constraints, which are simpler than the original quantified reachability formulas, and can effectively be handled by state-of-the-art CHC solvers.
