The cognitive agents specification language and verification environment for multiagent systems
Steven Shapiro, Yves Lespérance, Hector J. Levesque · 2002
The Cognitive Agents Specification Language (CASL) is a frame-work for specifying multiagent systems. It has a mix of declarative and procedural components to facilitate the specification and verification of complex multiagent systems. In this paper, we describe CASL and a verification environment (CASLve) for it based on the PVS verification system. We give an example of a multiagent meeting scheduler application specified with CASL. To illustrate the verification system, we discuss a proof we carried out in it, namely, that all bounded-loop CASL specifications terminate.