Verification and Behavioral Synthesis of Agent-Based Systems

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 veri cation area to make an impact in the arti cial 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.