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