Real-time specification and modeling with joint actions (Q685613)

The paper is based on the notion of joint action systems, used for the modeling of reactive systems. A joint action is understood as a logically atomic event, executed by one or more objects (or execution agents) in cooperation. The execution model that is used for reasoning is an interleaving model with fairness as a basic ``force'' for imposing liveness properties. Real time is added on this basis by appending a local clock variable to each execution agent, and associating durations with each action. A clock is assumed to be updated only when its owner participates in an action. A scheduling is then understood as a mapping that, based on these principles, associates timings to computations of the underlying non- timed model. The main properties of schedulings that are discussed include, whether ``partial-order equivalent'' computations are scheduled identically (soundness), whether all computations of the non-timed model get scheduled (completeness), and to which degree a scheduling preserves the liveness properties of the underlying non-timed model (correctness). In particular, it is noted that the liveness properties can easily be violated by an incomplete scheduling, like maximal parallelism or other general-purpose scheduling policies. The most natural scheduling elaborated for this approach is one that is sound and complete. The addition of time then adds no purely logical properties to computations, and the original interleaving model can be used for reasoning on all properties. The real-time properties that can be proved are weaker than with incomplete schedulings, but they are less sensitive to changes in action durations. To make use of this insensitivity also in situations where stronger real-time properties are required, undesirable computations can often be removed already at the non-timed level, rather than relying on an incomplete scheduling policy to do this.