A logic for the specification of multi-object systems

We present Multi-Object Dynamic Logic (MODL), a generalization of Dynamic Logic of which the intended use is the declarative specication of systems that are conceptually described by a multitude of objects. The semantics and entailment properties of MODL are based on some a priori requirements for a modal multi-object specication logic. In an example specication of the controls of a railroad crossing we demonstrate how MODL can be used to give semantics and reasoning capacity to graphical languages for communicating multi-object systems. In this example we introduce the idea of identifying the concept of event-triggering, which is used in the graphical languages, with the concept of action implication (action calling) in MODL. Finally we study to what extend temporal and mixed dynamic/temporal properties can be expressed in MODL