В статье вводится темпоральная логика линейного времени (LTL), ее формулы объясняются на многочисленных примерах. Объясняется, как свойства поведения дискретных динамических систем, в частности, реагирующих систем (reactive systems) могут быть заданы в этой логике. Статья является изложением одной из глав книги автора «Model checking. Верификация параллельных и распределенных программных систем», которая выходит в издательтве БХВ Петербург.

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.