TEMPORAL LOGIC MODEL CHECKERS AS APPLIED IN COMPUTER SCIENCE

• Authors: Trzesicki Kazimierz
• 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

EN

MODEL CHECKING; TEMPORAL LOGIC

Discipline

• LIBRARY_&_INFORMATION_SCIENCE: LIBRARY & INFORMATION SCIENCE

• Publisher: Sciendo
• Journal: Studies in Logic, Grammar and Rhetoric
• Year: 2009
• Issue: 17(30)
• Pages: 13-125
• Document type: ARTICLE

Contributors

author

Trzesicki Kazimierz

• Trzesicki Kazimierz, University of Bialystok, Poland

Identifiers

CEJSH db identifier

11PLAAAA101518