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