В контексте проверки ограниченной модели система описывается как система переходов состояний и свойства, которые необходимо проверить. 
Когда нужно предоставить несколько системных описаний и свойств инструменту проверки модели, может стать утомительным писать свойство вручную. В моем случае я использую LTL (линейную временную логику) в сочетании с логикой первого порядка. Как автоматизировать процесс перевода/анализа описания системы и получения из него проверяемых свойств (в идеале, набора начальных состояний, переходов, набора состояний). Например, рассмотрим пример микроволн, приведенный здесь
Преобразование системы переходов состояний в формулы свойств LTL
Ответы (2)
Вы не можете автоматически выводить формулы LTL из автоматов, как вы предлагаете, потому что автоматы более выразительны, чем формулы LTL.
Это оставляет вам в основном два варианта: 1. найти инструмент проверки, который принимает спецификации, которые непосредственно выражены в виде автоматов (я не уверен, какие именно, но я подозреваю, что стоит проверить SPIN и NuSMV для этой функции.) или 2. использовать язык метаспецификаций, который делает написание спецификаций легче; например, https://www.isp.uni-luebeck.de/salt (doi: 10.1007/11901433_41) или IEE1850/PSL. В то время как PSL — это скорее определение языка для разработчиков инструментов, SALT уже предлагает веб-интерфейс, который переводит ваш ввод прямо в LTL.
(Кстати, я нахожу ваш подход методологически сложным: вы должны выводить формулы не из вашей модели, а из вашего исходного описания системы, так как именно эту модель вы собираетесь проверять. Но я не специалист. На 100% уверен, если я правильно понял этот момент в вашем вопросе.)
Я думаю, что свойства системы, например. Микроволновая система исходит из технических и здравых ожиданий и требований, а не модели. Например. микроволновка должна готовить еду. Но готовить с открытой дверью нельзя. Тем не менее репозиторий типичного шаблона LTL может быть полезен для определения свойств. В нем также перечислены свойства наряду с более знакомыми свойствами регулярных выражений и автоматов.
Если вы уверены, что все еще хотите автоматически переводить автоматы в LTL, проверьте https://mathoverflow.net/questions/96963/translate-a-buchi-automaton-to-ltl
Канзасский репозиторий свойств спецификаций http://patterns.projects.cs.ksu.edu/documentation/patterns.shtml
