CONSISTENCY CHECKING OF AUTOMATA FUNCTIONAL SPECIFICATIONS

The use of a subset of a first order unary predicate language as a language for deterministic cyclic automata specification is considered. The formulas of the language are interpreted over the set of integers, which is regarded as a discrete time domain. An efficient algorithm for consistency checking of specifications in this language, based on modified resolution procedure, is suggested. This algorithm is implemented as a completion procedure. The use of the integers as the interpretation domain for the specification language made it possible to essentially simplify this procedure.