По сути, проверка модели имеет дело с моделью «m» (описание поведения системы) и свойством «p», которому должна удовлетворять система. С обоими артефактами средство проверки модели определяет, удовлетворяет ли модель свойству.
Мой вопрос заключается в том, можно ли указать модель "m" как формулу LTL и проверить, удовлетворяет ли модель как LTL "m" свойству "p".
Теоретически я считаю, что этот подход должен работать, потому что мы можем сгенерировать два автомата Бюхи, один для формулы LTL «p», а другой для свойства LTL, описывающего модель «m». Если пересечение двух недетерминированных автоматов пусто, модель «m» как LTL удовлетворяет этому свойству.
Может кто-нибудь подсказать? Возможно ли это?
