Model Checking. Part I
This text includes definitions of the Kripke structure, CTL (Computation Tree Logic), and verification of the basic algorithm for Model Checking based on CTL in [10].
Model Checking. Part II
This article provides the definition of linear temporal logic (LTL) and its properties relevant to model checking based on [9]. Mizar formalization of LTL language and satisfiability is based on [2, 3].
Fixpoint Theorem for Continuous Functions on Chain-Complete Posets
This text includes the definition of chain-complete poset, fix-point theorem on it, and the definition of the function space of continuous functions on chain-complete posets [10].
Model Checking. Part III
This text includes verification of the basic algorithm in Simple On-the-fly Automatic Verification of Linear Temporal Logic (LTL). LTL formula can be transformed to Buchi automaton, and this transforming algorithm is mainly used at Simple On-the-fly Automatic Verification. In this article, we verified the transforming algorithm itself. At first, we prepared some definitions and operations for transforming. And then, we defined the Buchi automaton and verified the transforming algorithm.MML identifier:...
Definition of Flat Poset and Existence Theorems for Recursive Call
This text includes the definition and basic notions of product of posets, chain-complete and flat posets, flattening operation, and the existence theorems of recursive call using the flattening operator. First part of the article, devoted to product and flat posets has a purely mathematical quality. Definition 3 allows to construct a flat poset from arbitrary non-empty set [12] in order to provide formal apparatus which eanbles to work with recursive calls within the Mizar langauge. To achieve this...
Page 1