Темпоральные логики для спецификации свойств программных и аппаратных систем

Abstract

Linear temporal logic (LTL) is presented and its formulas are explained by numerous examples. It is demonstrated how behavior properties of discrete dynamic systems, in particular reactive systems, may be presented in LTL. The paper is a brief exposition of a chapter from the author’s book «Model checking. Verification of parallel and distributed programs», to be published at BHV St. Petersburg Publishing office.