Paraconsistent Temporal Logic And Its Model Checking

Traditionally, it is a foundational requirement for a development processof software systems to retain consistency. But the fact that large and complexconcurrent systems become increasingly a mainstream, is challenging the princi-ple. Further, because of the open distributed process and evolving requirements,checking consistency is very expensive-cost. Therefore, we should handle formalor informal speci?cations of concurrent systems containing inconsistent informa-tion in a more rational and opener fashion.To the best of our knowledge, classical logic, such as predicate logic, is veryappealing for the formal representation of speci?cations of concurrent systemsdue to its expressivity and reasoning power. Moreover, classical logic has somevery important and useful properties, i.e., classical reasoning is intuitive and nat-ural. But the trivial inference problem makes inconsistent speci?cations no sense.Motivated by this, the dissertation presents a temporal logic based on the para-consistent logic methodology, termed quasi-classical temporal logic (abbreviatedQCTL), which both avoids the trivial inference problem and is used to specifytemporal properties of concurrent systems.The proof system of QCTL, di?erent from those of classical logics, is com-posed of decompositional rules and compositional rules, moreover, which are in-tuitive and natural. The proof of soundness and completeness of the proof systemis also provided. ParaKripke structures, an extension of standard Kripke struc-tures, de?ne the semantics of QCTL. By the extension, the relationship betweena formula and its negation is decoupled at the level of semantics, and inconsistentspeci?cations of concurrent systems can be speci?ed and non-trivially reasoned.In recent decade years, model checking technique, as a means of verifyingthe correctness of concurrent systems, has played an important role in the devel-opment of software and hardware. Especially, the model checking problem overclassical logics, such as CTL and LTL, has been deeply investigated and widelyapplied, but as to paraconsistent logics, it is not the case. At present, a majorityof work is limited to paraconsistent logics themselves, and little work is concen-trated on the model checking problem, say nothing of their applications in the?eld of computer science. Using paraKripke structures and the entailment rela-tion of QCTL, we propose a novel notion of models, termed paraKripke models(or super Kripke models). The notion of paraKripke models is de?ned by theentailment relation (|=t). But when implementing the model checking algorithm,we argue that it is unaccepted to directly transform a model checking problemto an inference problem according to the notion of paraKripke models. We candescribe the algorithm of model checking over QCTL in a way similar to the tra-ditional methodology: traversing the parse tree of a formula, on the basis of fullyunderstanding the properties of QCTL. Further, some case studies are conducted,showing that how QCTL is to be used to specify and verify concurrent systemscontaining inconsistent information.Basically, the work in the dissertation contributes to build the framework ofhandling inconsistent concurrent systems, including three aspects: speci?cation,reasoning and veri?cation. The framework dismisses the unnecessary restrictionto the development process in some period, i.e., in some period, it is not thenecessary task to retain consistency any longer, and provides the support of amore rational and more e?cient process.