Measurement Research And Its Application In Modal Logic Model Checking In

This thesis aims at exploring quantitative approaches for modal logic as well as model checking. As an application, it also attempts to find a way to simplify the complexity of model checking systems.Quantitative Logic focuses on the combination of formal inference and numerical calculation methods, such as probability and integral, in mathematical logic theory to make it more flexible and applicable. Such research was initially formed by grading basic logical concepts in several propositional logics in order to construct truth degree theory for formulae. Later on, a large number of subsequent research grew up, in-cluding topological and intrinsic structure analysis for logic metric spaces, divergence and consistence degree study for logical theories as well as construction of approxi-mate reasoning in propositional logic. Nowadays, Quantitative Logic not only owns systematic and mature theory within the scope of propositional logl its research sub-jects also cover more expressive logics, such as modal logic, temporal logic and even predicate logic. Besides, various kinds of investigation appear with innovation, which are devoted to combining Quantitative Logic and other related research fields. This thesis aims at exploring a new joint for Quantitative Logic and theoretical computer science. To be more specific, the quantitative approach used in propositional logic will be extended in the range of modal logic as well as temporal logic. As an application, similar approach will be investigated for model checking in order to find a way to simplify the complexity of model checking systems.Modal logic plays an important part in Artificial Intelligence and non-classic mathematical logic. It not only has theoretical roots in temporal logic and knowl-edge reasoning, but also owns applicable root in logic programming. As an expansion of propositional logic, modal logic possesses many particular and unique advantages. For example, there are distinguished types of modalities representing "possibility" and "necessity" together with "future" and "past". The more modalities it owns, the more ability of expression it is provided with. As a result, it seems necessary to extend the quantitative approach to the frame of modal logic, which also comes to one of the investigate assignments for Quantitative Logic. To meet this challenge, the thesis will construct localized truth degree as well as global truth degree for modal formu-lae by considering the locality of Kripke semantics in modal logic. Based on this, a quantitative approach for modal logic will be provided.Furthermore, as a formalized verification technique, model checking can automat- ically examine all relevant system states to check whether the system model satisfies the desired properties. Since it was proposed in1980s, this breakthrough was the first step towards the automated verification of concurrent programs. Over the last three decades, model checking has received a lot of attention and becomes a subject of rapid-1y growing research community. Since the specification in model checking is typically represented in several temporal logics, this thesis will similarly explore a quantitative approach for temporal logic and attempt to find a way to simplify the complexity of model checking systems based on this.The main contribution of this thesis is organized into five chapters.Chapter1provides an overview of several commonly used propositional logic sys-tems with syntax, semantics as well as completeness. Then basic concepts of Quan-titative Logic are recalled, such as truth degree, similarity degree and pseudo-metric for formulae together with the logic metric space.Chapter2recalls some preliminaries of classical modal logic. Then the Kripke semantics of classical modal logic is extended as lattice-valued ones, which also covers the notion of fuzzy-value ones. Moreover, based on Boolean algebras, a type of lattice-valued modal logic system, named as Boolean-type system B, is proposed. More importantly, this system is proved to be complete, i.e., a modal formula in B is valid if and only if it belongs to the scope of theorems. Lastly, the notion of QMR0algebra is introduced, and underlying logic system, QMR0-type lattice-valued modal logic system QML*, is constructed, whose completeness is ensured as well.Chapter3defines a certain finite subset of unit interval [0,1] as the valuation field for Kripke semantics of many-value modal logic. In fact, this Kripke semantics is a special case of lattice-valued ones and covers the notion of classical ones. Then by fixing the possible world W and binary relation R, the notion of<W, R>n frames is introduced. This notion contributes the construction of localized mappings induced by modal formulae as well as the definition of localized truth degree for modal formulae. More importantly, the localized truth degree satisfies the reduction theorem, i.e., for each modal formula, its localized truth degree equals the one of another formula con-taining no modalities w.r.t the same possible world. Besides, an aggregation method is adopted on localized truth degree, which comes to the notion of global truth degree for modal formulae. It is proved that this global truth degree satisfies the consistency theorem, i.e., for a modal formula containing no modalities, its global truth degree equals the value of truth degree in the propositional sense. Lastly, the concepts of similarity degree and pseudo-metric for modal formulae are proposed based on local- ized and global truth degrees, and the many-value modal logic metric space is also constructed, taking the propositional logic metric space as its subspace.Chapter4recalls some preliminaries of transition systems as well as linear tempo-ral logic (LTL for short) from model checking theory. Then for a transition system, the notion of satisfactory degree for LTL formulae is defined by adopting a certain kind of evenly distributed probability measure on the set of all its infinite initial paths. This satisfactory degree actually reflects the grade how a transition system satisfies an LTL formula in a quantitative sense. Based on this, the concepts of similarity degree and pseudo-metric are proposed for LTL formulae, and underlying logic metric space is also constructed. Although above notions are set up for transition systems, similar ideas can also be established for the randomized model, i.e., discrete-time Markov chains (DTMC for short). The difference lies in that the transition probability between states in a DTMC is no longer evenly distributed. Lastly, the notions of characters as well as temporal normal form for LTL formulae are introduced. It is pointed out that those LTL formulae with characters can always be checked within finite steps during model checking, even in some cases when the underlying transition system contains infinite states. What is more, the class of LTL formulae with characters can be characterized by full LTLn, the bounded case for LTLChapter5presents the concepts of deductive elements as well as maximal con-tractions in Boolean algebras. Then corresponding study of consistency and maximal contractions are considered, and an algorithm principle is proposed to compute all maximal contractions for a consistent set w.r.t. its refutation in Boolean algebras. It is proved that the quotient algebra of the first-order language w.r.t. its provable equivalence relation constitutes a Boolean algebra, and hence the computation of R-contractions for closed formulae in first-order language can be converted into the one in Boolean algebras proposed by this thesis. Furthermore, the notion of basic elements is introduced in Boolean algebras, which contributes to the definitions of clauses as well as Horn clauses transplanted from predicate logic to a special type of Boolean algebras. It is also pointed out that the computation of R-contractions for clauses in classical propositional logic can be converted into the one in Boolean algebras that is generated by basic elements proposed by this thesis.