A Logical Formalization of Time-Critical Processes with Resources

Checking time-critical properties of concurrent process instances having a finite amount of allocated resources is a challenging task. Modelling and understanding at design time the interactions of concurrent activities along the time line can become quite cumbersome, even for expert designers. In this paper, we consider processes that are composed of activities having a constrained duration and a bounded number of allocated resources, and we rely on a well-studied first order formalism, called, FO2(∼ <, -) to model and verify the interdependencies among multiple and concurrent process instances. Then, we show the expressiveness of our approach by describing the temporal properties that may be expressed through it. Throughout all the paper, we refer to a real clinical scenario to motivate our approach and showcase its expressiveness.