PL EN


2009 | 17(30) | 13-125
Article title

TEMPORAL LOGIC MODEL CHECKERS AS APPLIED IN COMPUTER SCIENCE

Selected contents from this journal
Title variants
Languages of publication
EN
Abstracts
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).
Keywords
Year
Issue
Pages
13-125
Physical description
Document type
ARTICLE
Contributors
  • Trzesicki Kazimierz, University of Bialystok, Poland
References
Document Type
Publication order reference
Identifiers
CEJSH db identifier
11PLAAAA101518
YADDA identifier
bwmeta1.element.2dbcc5b1-cfd7-3e03-a39f-57bd82f2ff76
JavaScript is turned off in your web browser. Turn it on to take full advantage of this site, then refresh the page.