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

Abstract

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