Real-Time Conditional Commitment Logic

A considerably large class of multi-agent systems (MASs) employed in real-time environments requires the possibility to express time-critical properties. In this paper, we develop a system of temporal logic RTCTLcc, an extension of CTL modalities and interval bound until modalities with conditional commitment and their fulfillment modalities. This logic allows us to formally model the interaction among autonomous agents using conditional commitments and to combine qualitative temporal aspects together with real-time constraints (time instants or intervals) in order to permit reasoning about qualitative and quantitative requirements and their specifications. We point out that useful properties of MASs, which are required to express temporal constraints as a fundamental part of functional requirements can be expressed in RTCTLcc. We also argue that time-critical properties expressed in executable action languages in other contributed approaches can be expressed in RTCTLcc.