Processes with local and global liveness requirements

The deterministic QS model, introduced in in Costa and Sernadas [J.F. Costa, A. Sernadas, Progress assumption in concurrent systems, Formal Aspects Comput. 7 (1) (1995) 18–36], captures (local) liveness properties, commonly specified in Temporal Logic, and not fully captured by non-deterministic process models. Liveness explains how some processes engage spontaneously in some actions and wait passively for the triggering of other actions by other processes. In this paper, we extend the QS model to describe liveness properties, through the introduction of a new operator deeply influenced by Temporal Logic, and denoting a global liveness requirement. The new operator applied to a process term induces a transactional behaviour until the execution of some specified action. We define the suitable denotational, axiomatic, and operational semantic domains to obtain a trinity of semantics in the sense of Hennessy. We prove that this extended model is a conservative extension of the previous one.