Разделенная нормальная форма для логики линейного времени LTL: определение и приведение к разделенной нормальной форме с условными обязательствами
Введение в моделирование и верификацию аппаратных и программных систем