The cognitive agents specification language and verification environment for multiagent systems

ABSTRACT

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.

REFERENCES

• 1: M. Benerecetti, F. Giunchiglia, and L. Serafini. Model checking multiagent systems. Journal of Logic and Computation, 8(3):401--423, 1998.
• 2: Giuseppe de Giacomo , Yves Lespérance , Hector J. Levesque, ConGolog, a concurrent programming language based on the situation calculus, Artificial Intelligence, v.121 n.1-2, p.109-169, Aug. 2000 [doi>10.1016/S0004-3702(00)00031-X]
• 3: Giuseppe De Giacomo , Hector J. Levesque, Projection Using Regression and Sensors, Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence, p.160-165, July 31-August 06, 1999
• 4: Joeri Engelfriet , Catholijn M. Jonker , Jan Treur, Compositional Verification of Multi-Agent Systems in Temporal Multi-Epistemic Logic, Proceedings of the 5th International Workshop on Intelligent Agents V, Agent Theories, Architectures, and Languages, p.177-193, July 04-07, 1998
• 5: Nissim Francez, Fairness, Springer-Verlag New York, Inc., New York, NY, 1986
• 6: Matthew Hennessy, The semantics of programming languages: an elementary introduction using structural operational semantics, John Wiley & Sons, Inc., New York, NY, 1990
• 7: G. Lakemeyer and H. J. Levesque. AOL: a logic of acting, sensing, knowing, and only knowing. In Principles of Knowledge Representation and Reasoning: Proceedings of the Sixth International Conference (KR-98), pages 316--327, 1998.
• 8: H. J. Levesque, R. Reiter, Y. Lespérance, F. Lin, and R. B. Scherl. GOLOG: A logic programming language for dynamic domains. Journal of Logic Programming, 31:59--84, 1997.
• 9: J. McCarthy and P. J. Hayes. Some philosophical problems from the standpoint of artificial intelligence. In B. Meltzer and D. Michie, editors, Machine Intelligence 4. Edinburgh University Press, 1969.
• 10: Sam Owre , S. Rajan , John M. Rushby , Natarajan Shankar , Mandayam K. Srivas, PVS: Combining Specification, Proof Checking, and Model Checking, Proceedings of the 8th International Conference on Computer Aided Verification, p.411-414, August 03, 1996
• 11: Raymond Reiter, The frame problem in situation the calculus: a simple solution (sometimes) and a completeness result for goal regression, Artificial intelligence and mathematical theory of computation: papers in honor of John McCarthy, Academic Press Professional, Inc., San Diego, CA, 1991
• 12: R. B. Scherl and H. J. Levesque. The frame problem and knowledge-producing actions. In Proceedings of the Eleventh National Conference on Artificial Intelligence, pages 689--695, Washington, DC, July 1993. AAAI Press/The MIT Press.
• 13: S. Shapiro. PhD thesis. In preparation.
• 14: Steven Shapiro , Yves Lespérance, Modeling Multiagent Systems with CASL - A Feature Interaction Resolution Application, Proceedings of the 7th International Workshop on Intelligent Agents VII. Agent Theories Architectures and Languages, p.244-259, July 07-09, 2000
• 15: Steven Shapiro , Yves Lespérance , Hector J. Levesque, Specifying Communicative Multi-Agent Systems (Invited Paper), Proceedings of the Workshops on Commonsense Reasoning, Intelligent Agents, and Distributed Artificial Intelligence: Agents and Multi-Agent Systems Formalisms, Methodologies, and Applications, p.1-14, December 01, 1997
• 16: S. Shapiro, M. Pagnucco, Y. Lespérance, and H. J. Levesque. Iterated belief change in the situation calculus. In A. G. Cohn, F. Giunchiglia, and B. Selman, editors, Principles of Knowledge Representation and Reasoning: Proceedings of the Seventh International Conference (KR2000), pages 527--538, San Francisco, CA, 2000. Morgan Kaufmann Publishers.

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
        I.2.11 Distributed Artificial Intelligence
            Subjects: Multiagent systems

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Tools; Languages
      D.2.4 Software/Program Verification
          Subjects: Formal methods

General Terms:
Languages, Reliability, Verification

Keywords:
agent specification languages, proof assistants, theorem proving, verification tools