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 ∆₀T -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 ∆₀T-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.

1. Goguen, J. A. Models and equality for logical programming / J. A. Goguen, J. Meseguer // Lecture Notes in Computer Science. — 1987. — Vol. 250. — P. 1-22.

2. Kowalski, R. Logic for Problem Solving, Revisited / R. Kowalski. London : Imperial College, 2014. — P. 321.

3. Кларк, Э. М. Верификация моделей программ / Э. М. Кларк, О. Грамберг мл., Д. Пелед // Москва : Изд-во Московского центра непрерывного математического образования, 2002. — 416 с.

4. Reps, T. Automating Abstract Interpretation / T. Reps, A. Thakur // In: 17th International Conference, VMCAI 2016, on Verification, Model Checking and Abstract Interpretation. St. Petersburg, FL, USA, January 17-19, 2016. — Paris : Springer, 2016. — P. 3-40.

5. Bloem, R. SAT-Based Synthesis Methods for Safety Specs / R. Bloem, R. Konighofer, M. Seidl // In: 15th International Conference, VMCAI 2014, on Verification, Model Checking and Abstract Interpretation. San Diego, CA, USA, January 2014. — San Diego : Springer, 2014. — P. 1-20.

6. Beyer, D. Reuse of Verification Results / D. Beyer, Ph. Wendler // In: 20th International Symposium, SPIN 2013, on Model Checking Software. Stony Brook, July 8-9, 2013. — Stony Brook : Springer, 2013. — P. 1-15.

7. Alur, R. Model-cheking for real-time system / R. Alur, C. Courcoubetis, D. L. Dill // Information and Computation. — 1993. — Vol. 104 (1). — P. 2-34.

8. Morbe, G. Fully Symbolic TCTL Model Checking for Incomplete Timed Systems // G. Morbe, Ch. Scholl // In: Proceedings of the Automated Verification of Critical Systems (AVoCS 2013). — 2013. — Vol. 66. — P. 1-9.

9. D'Silva, V. Independence Abstractions and Models of Concurrency / V. D'Silva, D. Kroening, M. Sousa // In: 18th International Conference, VMCAI 2017, on Verification, Model Checking and Abstract Interpretation. Paris, France, January 15-17, 2017. — Paris : Springer, 2017. — P. 149-168.

10. Goncharov, S. S. Theoretical aspects of S-programming / S. S. Goncharov, D. I. Sviridenko //: In: Proc. of the International Spring School, April 1985, on Mathematical Methods of Specification and Synthesis of Software Systems' 85. Berlin ; Heidelberg : Springer-Verlag, 1985. — P. 169-179.

11. Гончаров, С. С. Модели данных и языки их описаний / С. С. Гончаров // Вычислительные системы. Логико-математические основы проблемы МОЗ. — 1985. — Вып. 107. — С. 52-70.

12. Мальцев, А. И. Алгебраические системы. Москва : Наука, 1976. — С. 392.

13. Глушкова, В. Н. Оценка сложности реализации логических спецификаций на основе контекстносвободных грамматик / В. Н. Глушкова // Кибернетика и системный анализ. — 1996. — № 4. — С. 50-58.

14. Горбатов, В. А. Логическое управление распределенными системами / В. А. Горбатов, М. И. Смирнов, И. С. Хлытчиев. — Москва : Энергоатомиздат, 1991. — 288 с.