Глушкова Валентина Николаевна - доцент кафедры Математика, кандидат физикоматематических наук, старший научный сотрудник.
344003, Ростов-на-Дону, пл. Гагарина, 1
Коровина Ксения Сергеевна - старший преподаватель кафедры Математика.
344003, Ростов-на-Дону, пл. Гагарина, 1
Introduction. Verification packages design and analyze the correctness of parallel and distributed systems within the framework of various classes of temporal logics of linear and branching time. The paper discusses a polynomially realizable class of ∆0T -formulas interpreted on multi-sorted models with hierarchical suspensions. The suspensionstructure is described by an arbitrary context-free (CF) grammar. The predicates and functions of the model signature are interpreted on the original CF-list, which is completed during the interpretation process.
Materials and Methods. A constant model is constructed for theories from ∆0T-quasiidentities with Noetherian and confluence properties. We consider formulas of the multi-sorted first-order predicate calculus (PC) language with variables of the “list” sort interpreted on models with a hierarchized suspension. The theory is interpreted in terms of grammar inference trees describing the behavior of the specified system. The CF-grammar rules hierarchize the action space of the modeled system. It is noted that the expressive capabilities of Д0T-formulas are insufficient for modeling real-time systems. Therefore, expressions with unbounded universal quantifier V, known as PT formulas, are used for the specification.
Results. The logical specification of an automated complex which consists of a workpiece manipulator is given as an example. The location of the positions is fixed by sensors. The operating cycle of the manipulator is described. The specification of its operation consists in the hierarchization of actions by the rules of the CF-grammar and their description by the first-order PT-formulas taking into account the time values.
Discussion and Conclusions. The paper shows that the class of the considered formulas can be used to model real-time systems. An example of the logical specification of a manipulator behavior control device is given.
Введение. Пакеты верификации проектируют и анализируют корректность параллельных и распределенных систем в рамках различных классов темпоральных логик линейного и ветвящегося времени. В статье рассматривается полиномиально реализуемый класс ∆0T-формул, интерпретируемый на многосортных моделях с иерархическими надстройками. Структура надстройки описывается произвольной контекстно-свободной (КС) грамматикой. Предикаты и функции сигнатуры модели интерпретируются на исходном КС-списке, достраиваемом в процессе интерпретации.
Материалы и методы. Для теорий из ∆0T-квазитождеств, обладающих свойствами нётеровости и конфлюент-ности, строится константная модель. Рассматриваются формулы многосортного языка исчисления предикатов (ИП) 1-го порядка с переменными сорта «список», интерпретируемые на моделях с иерархизированной надстройкой. Теория интерпретируется на деревьях вывода грамматики, описывающих поведение специфицируемой системы. Правила КС-грамматики иерархизируют пространство действий моделируемой системы. Отмечено, что для моделирования систем реального времени недостаточно выразительных возможностей Д0 T-формул. Поэтому для спецификации используются выражения с неограниченным квантором всеобщности V, известные как ПТ-формулы.
Результаты исследования. В качестве примера приводится логическая спецификация автоматизированного комплекса, который состоит из манипулятора, обрабатывающего детали. Положение позиций фиксируется датчиками. Описывается цикл работы манипулятора. Спецификация его функционирования состоит в иерархиза-ции действий правилами КС-грамматики и их описании формулами ИП 1-го порядка с учетом значений времени.
Обсуждение и заключения. В статье показано, что класс рассмотренных формул можно использовать для моделирования систем реального времени. Приводится пример логической спецификации управляющего устройства поведением манипулятора.
The authors declare that there are no conflicts of interest present.