Polynomially computable Σ-specifications of hierarchical models of reacting systems

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.