Glushkova V.  

Полиномиально вычислимые СИГМА спецификации иерархизированных моделей реагирующих систем

Рассматривается полиномиально-реализуемый класс Delta–формул, интерпретируемый на многосортных моделях с иерархическими надстройками. Структура надстройки описывается произвольной КС-грамматикой. Для теорий из Delta– квазитождеств, обладающих свойством нётеровости и конфлюентности, можно построить константную модель. Предикаты и функции сигнатуры модели интерпретируются на исходном КС-списке, достраиваемом в процессе интерпретации. Этот класс формул можно использовать для моделирования систем реального времени. Приводится пример логической спецификации управляющего устройства поведением робота.

The polynomial realized Delta –formulas are considered with quantifiers acting on hierarchy lists described by CF-grammars. These formulas are interpreted on a many-sorted model with the hierarchy list superstructure. The constant model is constructed for the Noether confluent theory based on quasi-identities. The signature predicates and functions are interpreted on input CF-list extended on the interpretation process. The Delta –formulas theories might be used to model real-time systems. As example a logic specification of robot behaviour is given.

Abstracts file: Глушкова.pdf


To reports list