Разделенная нормальная форма для логики линейного времени LTL: условные обязательства и построение автомата
Introduction to Verification