О верификации конечных автоматов-преобразователей над полугруппами

Последовательные реагирующие системы - это программы, которые взаимодействуют с окружением, получая от него сигналы или запросы, и реагируют на эти запросы, проводя операции с данными. Подобные системы могут служить моделью для многих программ: драйверов, систем реального времени, сетевых протоколов и др. В статье исследуются задача верификации программ такого вида. В качестве формальных моделей для реагирующих систем мы используем конечные автоматы-преобразователи, работающие над полугруппами. Для описания поведения автоматов-преобразователей введён новый язык спецификаций LP-CTL*. В его основу положена темпоральная логика CTL*. Этот язык спецификаций имеет две характерные особенности: 1) каждый темпоральный оператор снабжён регулярным выражением над входным алфавитом автомата, и 2) каждое атомарное высказывание задается регулярным выражением над выходным алфавитом автомата-преобразователя. В данной работе представлен табличный алгоритм проверки выполнимости формул LP-CTL* на моделях конечных автоматов-преобразователей, работающих над свободными полугруппами. Доказана корректность предложенного алгоритма и получена оценка его сложности. Кроме того, рассмотрен специальный фрагмент языка LP-CTL*, содержащий в качестве параметров темпоральных операторов только регулярные выражения над однобуквенным алфавитом. Показано, что этот фрагмента применим для спецификаций обычных моделей Крипке, и при этом его выразительные возможности превосходят обычную логику CTL*.

реагирующая система, автомат-преобразователь, верификация, проверка на модели, темпоральная логика, конечный автомат, регулярный язык

1. Alur R., Cerny P. Streaming transducers for algorithmic verification of single-pass list-processing programs. In Proceedings of 38-th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 2011, pp. 599-610

2. Alur R., Moarref S., and Topcu U. Pattern-based refinement of assume-guarantee specifications in reactive synthesis. In Proceedings of 21-st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2015, pp. 501-516.

3. Baier C., Katoen J. Principles of Model Checking, 2008, MIT Press.

4. Blattner M., Head T. The decidability of equivalence for deterministic finite transducers. Journal of Computer and System Sciences, 1979, vol. 1, pp. 45-49.

5. Blattner M., T. Head T. Single-valued a-transducers. Journal of Computer and System Sciences, vol. 15, 1977, pp. 310-327.

6. Culik K, Karhumaki J. The equivalence of finite-valued transducers (on HDTOL languages) is decidable. Theoretical Computer Science, 1986, vol. 47, pp. 71-84.

7. Bouajjani A., Jonsson B., Nilsson M., Touili T. Regular Model Checking. Proceedings of 12-th International Conference on Computer Aided Verification, 2000, p. 403-418.

8. Clarke (Jr.) E. M., Grumberg O., Peled D. A. Model Checking. MIT Press, 1999.

9. Diekert V., Rozenberg G. eds. The Book of Traces, 1995, World Scientific, Singapore.

10. Emerson E.A., Halpern J.Y. Decision procedures and expressiveness in the temporal logic of branching time. Journal of Computer and System Sciences, vol. 30, N 1, 1985, pp. 1–24.

11. Etessami K., WilkeT. An Until Hierarchy and Other Applications of and Ehrenfeucht-Fraisse Game for Temporal Logic. Information and Computation, vol. 160, 2000, pp. 88-108.

12. Гнатенко А.Р., Захаров В.А. О сложности верификации конечных автоматов-преобразователей над коммутативными полугруппами. Материалы XVIII международной конференции «Проблемы теоретической кибернетики»' (Пенза, 20-24 июня, 2017), стр. 68-70.

13. Griffiths T. The unsolvability of the equivalence problem for free nondeterministic generalized machines. Journal of the ACM, vol. 15, 1968, pp. 409-413.

14. HenriksenJ. G., Thiagarajan P.S. Dynamic linear time temporal logic. Annals of Pure and Applied Logic, vol. 96, 1999, pp.187-207.

15. Hu Q., D'Antoni L. Automatic Program Inversion using Symbolic Transducers. In Proceedings of the 38-th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017, pp. 376-389.

16. Ibarra O. The unsolvability of the equivalence problem for Efree NGSM’s with unary input (output) alphabet and applications. SIAM Journal on Computing, vol. 4, 1978, pp. 524-532.

17. Kozlova D. G., Zakharov V. A. On the model checking of sequential reactive systems. Proceedings of the25-th International Workshop on Concurrency, Specification and Programming (CS&P 2016), CEUR Workshop Proceedings, vol. 1698, 2016, pp. 233-244.

18. Kupferman O., Piterman N., Vardi M.Y. Extended Temporal Logic Revisited. In Proceedings of 12-th International Conference on Concurrency Theory, 2001, pp. 519-535.

19. Schutzenberger M. P. Sur les relations rationnelles. In Proceedings of Conference on Automata Theory and Formal Languages, 1975, pp. 209-213.

20. Sakarovitch J., de Souza R. On the decomposition of k-valued rational relations. In Proceedings of 25-th International Symposium on Theoretical Aspects of Computer Science, 2008, pp. 621-632.

21. Sakarovitch J., de Souza R. On the decidability of bounded valuedness for transducers. In Proceedings of the 33-rd International Symposium on Mathematical Foundations of Computer Science, 2008, pp. 588-600.

22. De Souza R. On the decidability of the equivalence for k-valued transducers. In Proceedings of 12-th International Conference on Developments in Language Theory, 2008, pp. 252-263.

23. Thakkar J., Kanade A., Alur R. A transducer-based algorithmic verification of retransmission protocols over noisy channels. In Proceedings of IFIP Joint International Conference on Formal Techniques for Distributed Systems, 2013, pp. 209-224.

24. Vardi M.Y., Wolper P. Yet Another Process Logic. Logic of Programs, 1983, pp. 501-512.

25. Veanes M., Hooimeijer P., Livshits B. et al. Symbolic finite state transducers: algorithms and applications. In Proceedings of the 39-th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, ACM SIGPLAN Notices, vol. 147, 2012, pp. 137-150.

26. Weber A. Decomposing finite-valued transducers and deciding their equivalence. SIAM Journal on Computing. vol. 22, 1993, pp. 175-202.

27. Wolper P. Temporal Logic Can Be More Expressive. Information and Control, vol. 56, N 1/2, 1983, pp. 72-99.

28. Wolper P., Boigelot B. Verifying systems with infinite but regular state spaces. In Proceedings of the 10-th Int. Conf. on Computer Aided Verification (CAV-1998), 1998, pp. 88-97.

29. Zakharov V.A. Equivalence checking problem for finite state transducers over semigroups. In Proceedings of the~6-th International Conference on Algebraic Informatics (CAI-2015), 2015, pp. 208-221.