Verification and behavioral synthesis of agent-based systems

Thumbnail Image
Asteasuain, Fernando
Gamboa, Pablo Daniel
D’Angiolo, Federico
Dubinsky, Manuel
Journal Title
Journal ISSN
Volume Title
Sociedad Argentina de Informática, SADIO
In this work we explore the FVS language as a formalism to express, validate and synthesize behavior in the agent-based systems'world. Recent work relates Behavioral Synthesis with agent-based systems, opening the possibility for formalisms in the formal verification area to make an impact in the artificial intelligence domain. In this work we analyze FVS as a potential candidate to make a contribution given its desirable characteristics such as exibility, great expressive power and its ability to perform behavioral synthesis in Open Systems. A very well known case of study is analyzed: the Dining Cryptographers protocol, including one variation of the protocol. FVS was able to fully specify,validate and synthesize the behavior of the protocol.
agent-based systems, behavioral synthesis, formal verification
Asteasuain, F.; D'Angiolo, F.; Dubinsky, M.; Gamboa, P.D. (2020). Verification and behavioral synthesis of agent-based systems. En: Jornadas Argentinas de Informática virtuales, JAIIO, 49, 19-30 oct 2020. Simposio Argentlno de Inteligencia Artificial, ASAI. 21. Anales de ASAI 2020. p.:100-113