REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: http://hdl.handle.net/11320/21062
Pełny rekord metadanych
Pole DCWartośćJęzyk
dc.contributor.authorIshida, Kazuhisa-
dc.date.accessioned2026-09-18T09:47:35Z-
dc.date.available2026-09-18T09:47:35Z-
dc.date.issued2008-
dc.identifier.citationFormalized Mathematics, Volume 16, Issue 3, 2008, Pages 231-245pl
dc.identifier.issn1426-2630-
dc.identifier.urihttp://hdl.handle.net/11320/21062-
dc.description.abstractThis article provides the definition of linear temporal logic (LTL) and its properties relevant to model checking based on [9]. Mizar formali zation of LTL language and satisfiability is based on [2, 3].pl
dc.language.isoenpl
dc.publisherUniversity of Białystokpl
dc.rightsAttribution-ShareAlike 4.0 Internationalpl
dc.rights.urihttps://creativecommons.org/licenses/by-sa/4.0/-
dc.titleModel Checking. Part IIpl
dc.typeArticlepl
dc.rights.holder© 2009 Kazuhisa Ishida, published by University of Białystokpl
dc.rights.holderThis work is licensed under the Creative Commons License.pl
dc.identifier.doi10.2478/v10037-008-0028-9-
dc.description.AffiliationShinshu University, Nagano, Japanpl
dc.description.referencesGrzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.pl
dc.description.referencesGrzegorz Bancerek. A model of ZF set theory language. Formalized Mathematics, 1(1):131–145, 1990.pl
dc.description.referencesGrzegorz Bancerek. Models and satisfiability. Formalized Mathematics, 1(1):191–199, 1990.pl
dc.description.referencesGrzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finitesequences. Formalized Mathematics, 1(1):107–114, 1990.pl
dc.description.referencesCzesław Byliński. Binary operations. Formalized Mathematics, 1(1):175–180, 1990.pl
dc.description.referencesCzesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990.pl
dc.description.referencesCzesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.pl
dc.description.referencesCzesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990.pl
dc.description.referencesE. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 2000.pl
dc.description.referencesKazuhisa Ishida. Model checking. Part I. Formalized Mathematics, 14(4):171–186, 2006.pl
dc.description.referencesZinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.pl
dc.description.referencesEdmund Woronowicz. Many–argument relations. Formalized Mathematics, 1(4):733–737, 1990.pl
dc.identifier.eissn1898-9934-
dc.description.volume16pl
dc.description.issue3pl
dc.description.firstpage231pl
dc.description.lastpage245pl
dc.identifier.citation2Formalized Mathematicspl
Występuje w kolekcji(ach):Formalized Mathematics, 2008, Volume 16, Issue 3

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
Model_Checking._Part_II.pdf246,02 kBAdobe PDFOtwórz
Pokaż uproszczony widok rekordu Zobacz statystyki


Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL Creative Commons