Журнал
Научно-технический вестник информационных технологий, механики и оптики
УДК:
Номер:8 (53)
Скачать PDF0 Кбайт
This article discusses ways of converting automata-based programs to Kripke models, designed to check the properties related to the behavior of the system. These properties are described with temporal logic formulas. Several methods of such a transformation are proposed.