PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
2009 | 17(30) | 13-125
Tytuł artykułu

TEMPORAL LOGIC MODEL CHECKERS AS APPLIED IN COMPUTER SCIENCE

Wybrane pełne teksty z tego czasopisma
Warianty tytułu
Języki publikacji
EN
Abstrakty
EN
Various logics are applied to specification and verification of both hardware and software systems. Since systems are operating in time, temporal logic is a proper tool. The problem with finding the proof is the most important disadvantage of the proof-theoretical method. The proof-theoretical method presupposes the axiomatization of logic. Proprieties of a system can also be checked using a model of the system. A model is constructed with the pecification language and checked using automatic model checkers. The model checking application presupposes the decidability of the task. The explosion of the cases that have to be explored is the main disadvantage of this method. Temporal logic model checking is an algorithmic method that can be used to check whether a given model (representing a system) satisfies certain properties (expressed as temporal logic formulas).
Słowa kluczowe
Rocznik
Numer
Strony
13-125
Opis fizyczny
Rodzaj publikacji
ARTICLE
Twórcy
  • Trzesicki Kazimierz, University of Bialystok, Poland
Bibliografia
Typ dokumentu
Bibliografia
Identyfikatory
CEJSH db identifier
11PLAAAA101518
Identyfikator YADDA
bwmeta1.element.2dbcc5b1-cfd7-3e03-a39f-57bd82f2ff76
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ć.