First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE '07)
QCTL: A Logic for Reasoning about Inconsistent Concurrent Systems
Shanghai, China
June 06-June 08
ISBN: 0-7695-2856-2
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 in- troduced, 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 differ- ent comparing with classical logics like CTL, most natural and intuitive properties are preserved. This work bridges the gap between the specification and verification of tempo- ral aspects and non-trivial reasoning under inconsistency.
Citation:
Donghuo Chen, Guangquan Zhang, Jinzhao Wu, "QCTL: A Logic for Reasoning about Inconsistent Concurrent Systems," tase, pp.241-250, First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE '07), 2007