Pełnotekstowe zasoby PLDML oraz innych baz dziedzinowych są już dostępne w nowej Bibliotece Nauki.
Zapraszamy na https://bibliotekanauki.pl
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 5

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last

Wyniki wyszukiwania

help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available remote

Model Checking. Part I

100%
Ishida K.
Formalized Mathematics
|
2006
|
tom 14
|
nr 4
171-186
EN
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].
2
Content available remote

Model Checking. Part II

100%
Ishida K.
Formalized Mathematics
|
2008
|
tom 16
|
nr 3
231-245
EN
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].
3
Content available remote

Fixpoint Theorem for Continuous Functions on Chain-Complete Posets

64%
Ishida K., Shidama Y.
Formalized Mathematics
|
2010
|
tom 18
|
nr 1
47-51
EN
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].
4
Content available remote

Model Checking. Part III

64%
Ishida K., Shidama Y.
Formalized Mathematics
|
2008
|
tom 16
|
nr 4
339-353
EN
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
5
Content available remote

Definition of Flat Poset and Existence Theorems for Recursive Call

51%
Ishida K., Shidama Y., Grabowski A.
Formalized Mathematics
|
2014
|
tom 22
|
nr 1
1-10
EN
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.
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.