ВЕРИФИКАЦИЯ НА ОСНОВЕ МОДЕЛЕЙ С ОДНИМ НЕОГРАНИЧЕННЫМ СЧЕТЧИКОМ

Предлагается новый метод доказательства свойств систем, моделируемых при помощи односчетчиковых сетей Петри (параллельных и распределенных процессов, алгоритмов и протоколов). Подобные модели позволяют представлять системы как с конечными, так и с бесконечными множествами состояний. Проверяемые свойства предлагается записывать при помощи формул теморальной логики EF (логики достижимости). Новизна метода состоит в использовании некоторых конструктивных теоретико-числовых свойств бесконечной части одномерных линейных и полулинейных множеств. Представлен алгоритм формальной верификации темпоральных формул логики EF, использующий декомпозицию формулы и вычисления над однопериодическими полулинейными базисами специального вида

• Башкин В.А.

• Общий отдел

• Технические науки. Промышленность
• Физико-математические науки