Журнал
Научно-технический вестник информационных технологий, механики и оптики
УДК:004.4’242
Номер:6 (64)
В статье рассматриваются способы преобразования программ, разработанных на основе автоматного подхода, в модели Крипке, предназначенные для проверки свойств, относящихся к поведению системы. Эти свойства задаются формулами темпоральной логики. Предложен эффективный метод такого преобразования и формулировки указанных свойств, который позволяет строить небольшие модели Крипке и достаточно быстро проводить их проверку.