TEMPORAL LOGIC MODEL CHECKERS AS APPLIED IN COMPUTER SCIENCE

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).