Verification and behavioral synthesis of agent-based systems

Thumbnail Image
Date
2020-10
Authors
Asteasuain, Fernando
Gamboa, Pablo Daniel
D’Angiolo, Federico
Dubinsky, Manuel
Journal Title
Journal ISSN
Volume Title
Publisher
Sociedad Argentina de Informática, SADIO
Abstract
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.
Description
Keywords
agent-based systems, behavioral synthesis, formal verification
Citation
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