Я не очень понял...

[thesz]

...в чем там проблема, но есть отличная книга "Верификация моделей программ". Там про разные варианты рассказывается.

Если я всё правильно помню (а книга запихнута довольно далеко), то можно поменять темпоральную логику и взять её вариант попроще. Соответственно, сложность упадёт.