QCTL: A Logic for Reasoning about Inconsistent Concurrent Systems

It has been widely recognized that inconsistencies of- ten appear and are inevitable when specifying large and complex concurrent systems. In this paper, a non-classical temporal logic QCTL (quasi-classical temporal logic) is introduced, which subsumes both QCL and CTL. It is para- consistent, i.e., it can be used to reason non-trivially about system specifications containing inconsistent information. A semantics for QCTL is proposed in terms of paraKripke structures (the extended Kripke strucutres). Furthermore, a sound and complete proof system for QCTL is presented. Although the models and proof theory of QCTL are different comparing with classical logics like CTL, most natural and intuitive properties are preserved. This work bridges the gap between the specification and verification of temporal aspects and non-trivial reasoning under inconsistency.