Прототипирование верификации поведения интеллектуальных агентов в языке логического программирования ПРОЛОГ

Рассмотрены современные подходы к верификации поведения интеллектуальных агентов. Кратко изложены особенности формальных языков, применяемых для описания спецификаций поведения агентов,
и принципы проверки корректности этих спецификаций. Приведены формулировки типичных условий корректности спецификаций поведения агентов. Показано, как сравнительно простыми средствами языка
ПРОЛОГ можно осуществлять прототипирование верификации мультиагентных интеллектуальных систем, используя предварительно составленную спецификацию и сформулированные на языке модальной
логики условия их корректности.

Для студентов бакалавриата, обучающихся по направлению подготовки 09.03.02 «Информационные системы и технологии» и изучающих дисциплину «Интеллектуальные системы и технологии».

Список литературы

1. Bharti M.V., Kumar S. Survey of network protocol verification techniques // International Journal of Scientific and Research Publications. 2012. 2 (4). P. 228–231.
2. Дейкстра Э. Дисциплина программирования. М.: Мир, 1978.
3. Paulson T.N.L.C., Wenzel M. A Proof Assistant for Higher-Order Logic. URL: http://www.cl.cam.ac.uk/research/hvg/isabelle/dist/Isabelle2011-1/doc/tutorial.pdf (дата обращения 25.01.2021 г.)
4. Owre S., Rushby J., Shankar N. PVS: A prototype verification system // 11th International Conference on Automated Deduction (CADE) / Ed. by D. Kapur. Vol. 607 of Lecture Notes in Artificial Intelligence. Saratoga, NY : Springer-Verlag, 1992. P. 748–752
5. Medvidovic N., Taylor R.M. A Classification and Comparison Framework for Software Architecture Description Languages // IEEE Transactions on Software Engineering. 2000. Vol. 26. No. 1. P. 70–93.
6. Braga C., Sztajnberg A. Towards a Rewriting Semantics for a Software Architecture Description Language // Proceedings of WMF 2003, 6th Workshop on Formal Methods. Campina Grande, Brazil, E.N.T.C.S. 2003. 95. P. 148–168.
7. Milner R. Communicating and Mobile Systems: the π-calculus. Cambridge. UK: Cambridge University Press, 2003. 159 p.
8. Pandey R. Architectural description languages (ADL): a review. ACM SIGSOFT Software Engineering Notes. 2010. 35.3. P. 1–5.
9. Bruni R., Fiadeiro J.L., Lanese I., Lopes A., Montanari U.. New Insight into the Algebraic Properties of Architectural Connectors // IFIP TCS. 2004. P. 367–380.
10. Choutri A., Belala F., Barkaoui K. A Tile Logic Based Approach for Software Architecture Description Analysis// USA., J. Software Engineering & Applications. 2010. 3. P. 1067–1079.
11. Bouanaka C., Choutri A., Belala F. On Generating Tile System for a Software Architecture: Case of a Collaborative Application Session // ICSOFT 2007. The Second Conference on Software and Data Technologies. July 22–25. 2007. P. 123–128.
12. Bouanaka C., Belala F., Barkaoui K. A Tile Logic Based Semantics for Mobile Software Architectures // International Journal of Critical Computer-Based Systems 01. 2011. 2 (3). P. 288–308.
13. Kleene S.C. Representation of events in nerve nets and finite automata // C.E. Shannon, J. McCarthy. Automata Studies. Princeton University Press, 1956. P. 3–42.
14. Abadi M., Manna Z. Temporal logic programming //Journal of Symbolic computation. 1989. Vol. 8. Iss. 3. P. 277–295.
15. Hudak P. Modular domain specific languages and tools // Proceedings of Fifth International Conference on Software Reuse. Cat. No. 98TB100203. 1998. P. 134–142.
16. Kamin S.N. Research on domain-specific embedded languages and program generators // Electronic Notes in Theoretical Computer Science. 1998. 14. P. 149–168.
17. Kollár J., Václavík P., Porubän J. The Classification of Programming Environments. Acta Universitatis Matthiae Belii. 2003. 10. P. 51–64.
18. Elliott C. An embedded modeling language approach to interactive 3D and multimedia animation // IEEE transactions on software engineering. 1999. 25 (3). P. 291–308.
19. Peterson J., Hudak P., Elliott C. Lambda in motion: Controlling robots with Haskell // International Symposium on Practical Aspects of Declarative Languages. Berlin: Springer, 1999. P. 91–105
20. Девятков В.В., Мьё Т.Н. Формальный логический анализ корректности спецификаций сетевых SIP-протоколов // Инженерный журнал: наука и инновации. 2013. № 11. C. 55–65.
21. Zave P. Understanding SIP Through Model-Checking // Proc. of the 2nd International Conference of Principles, Systems and Applications of IP Telecommunications. URL: https://pdfs.semanticscholar.org/2051/e9d36188f2ba910147b738214e6809dce306.pdf (дата обращения 25.01.2021 г.)
22. Qadir J., Hasan O. Applying formal methods to networking: theory, techniques, and applications // IEEE Communications Surveys & Tutorials. 2014. 17 (1). P. 256–291.
23. Bong Wan Choi. Petri net approaches for modeling, controlling, and validating flexible manufacturing systems. Iowa State University, 1994.
24. Cuffaro M.E. Inductory notes on predicate logic. 2014.
25. Simonak S., Hudak Š., Korecko Š. Protocol specification and verification using process algebra and Petri nets // International Conference on Computational Intelligence, Modelling and Simulation. 2009. P. 110–114.