Синтез ∑-автоматов, специфицированных в логических языках LP и LF первого порядка

Abstract

Приведены методы синтеза ∑-автоматов по спецификации в языке LP с детерминированной семантикой и в языке LF с недетерминированной семантикой. В основе этих методов лежит эквивалентное преобразование формулы вида ∀tF(t) в так называемую нормальную форму, структура которой соответствует графу переходов специфицированного ∑-автомата.

Наведено методи синтезу ∑-автоматів за специфікаціями у мові LP з детермінованою семантикою і у мові LF з недетермінованою семантикою. В основі цих методів лежить еквівалентне перетворення формули вигляду ∀tF(t) в так звану нормальну форму, структура якої відповідає графу переходів специфікованого ∑-автомата.

This paper presents methods for synthesizing ∑-automata from specifications in the language LP with deterministic semantics and in the language LF with nondeterministic semantics. These methods are based on the equivalent transformation of the formula of the form ∀tF(t) into a so called normal form whose structure corresponds to the state transition graph of a specified automaton.