Real-time conditional commitment logic and duration communication interpreted systems

Abstract

We propose a real-time conditional and unconditional commitment logic (RTCTLC) with semantics defined over the duration communication interpreted system – a system with arbitrary integer durations on transitions. The transitions with durations allow us to model different levels of temporal deadlines and to reduce extra verification work resulting from the use of unit measure steps. The whole framework allows us to formally model the behaviour of agents using (conditional, unconditional, and group) commitments and real-time constraints in order to permit reasoning about qualitative and quantitative requirements.