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