Semantics and controllability of time-aware business processes

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