# Search Results

## 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].

## 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: MODELC 3, version: 7.9.03 4.108.1028

## 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].

## Summary

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 we extensively use technical Mizar functors like BaseFunc or RecFunc. The remaining part builds the background for information engineering approach for lists, namely recursive call for posets [21].We formalized some facts from Chapter 8 of this book as an introduction to the next two sections where we concentrate on binary product of posets rather than on a more general case.