Specifying and verifying multiagent systems using the cognitive agents specification language (CASL).
Published: 2005
Language: eng
Number of pages: 239
Description: In this thesis, we introduce a specification language (CASL) and verification environment (CASLve) for multiagent systems. We use the situation calculus [52] with Reiter's solution to the frame problem [62]---enhanced with predicates to describe agents' knowledge [64], beliefs, and goals---to formally, perspicuously, and systematically describe the effects of actions on the world and the mental states of agents. We add INFORM,  REQUEST, and CANCELREQUEST actions to model inter-agent communication, and investigate properties of multiagent knowledge change and goal change, as well as belief change. We use the notation of the concurrent, logic programming language ConGolog [17] to specify the behaviour of agents. ConGolog has a formal semantics defined in the situation calculus, which facilitates the process of reasoning about the behaviour of individual agents and the system as a whole. We provide an environment for verifying properties of CASL specifications, by encoding the situation calculus, its extensions to handle mental states, and ConGolog in the PVS verification system [54], and proving lemmas which are useful for verifying CASL specifications. These include proving that bounded-loop ConGolog programs terminate, and providing a framework far compositional verification of ConGolog programs. We then specify three multiagent systems using CASL and prove some properties of the specifications.
Notes: Thesis (Ph.D.)--University of Toronto, 2005.

Electronic version licensed for access by U. of T. users.

Source: Dissertation Abstracts International, Volume: 66-06, Section: B, page: 3242.

ENGI copy differs in paging: viii, 244 p.