. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics , 1( 3 ):529-536, 1990.
 Czesław Bylinski. Functions and their basic properties. Formalized Mathematics , 1( 1 ):55-65, 1990.
 Czesław Bylinski. Functions from a set to a set. Formalized Mathematics , 1( 1 ):153-164, 1990.
 Czesław Bylinski. Partial functions. Formalized Mathematics , 1( 2 ):357-367, 1990.
 Mariusz Giero. The axiomatization of propositional linear time temporal logic. Formalized Mathematics
1 This work was supported by the University of Bialystok grants: BST447 Formalization of temporal logics in a proof-assistant. Application to System Verification , and BST225 Database of mathematical texts checked by computer .
 Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics , 1( 1 ):41–46, 1990.
 Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics , 1( 1 ):91–96, 1990.
 Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite
This article provides the definition of linear temporal logic (LTL) and its properties relevant to model checking based on . Mizar formalization of LTL language and satisfiability is based on [2, 3].
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.