东华大学学报（英文版）2008，Vol.25Issue(5)：571-580,10.
Model Checking over Paraconsistent Temporal Logic
Model Checking over Paraconsistent Temporal Logic
摘要
Abstract
Classical logic cannot be used to effectively reason about concurrent systems with inconsistencies (inconsistencies often occur, especially in the early stage of the development, when large and complex concurrent systems are developed). In this paper, we propose the use of a guasi-classical temporal logic (QCTL) for supporting the verification of temporal properties of such systems even where the consistent model is not available. Our models are paraKripke structures ( extended standard Kripke structures), in which both a formula and its negation are satisfied in a same state, and properties to be verified are expressed by QCTL with paraKripke structures semantics. We introduce a novel notion of paraKripke models, which grasps the paraconsistent character of the entailment relation of QCTL. Furthermore, we explore the methodology of model checking over QCTL, and describe the detailed algorithm of implementing QCTL model checker. In the sequel, a simple example is presented, showing how to exploit the proposed model checking technique to verify the temporal properties of inconsistent concurrent systems.关键词
inconsistency/concurrent systems/paraconsistent temporal logic/model checkingKey words
inconsistency/concurrent systems/paraconsistent temporal logic/model checking分类
信息技术与安全科学引用本文复制引用
CHEN Dong-huo,WANG Lin-zhang,CUI Jia-lin..Model Checking over Paraconsistent Temporal Logic[J].东华大学学报（英文版）,2008,25(5):571-580,10.基金项目
Supported by the National Natural Science Foundation of China (No. 60603036) and by the Jiangsu Province Research Foundation (No. BK2007139). （No. 60603036）
