august 9 to 15, 2003

Workshop on
Model Checking and Artificial Intelligence

August 10, 2003 - Acapulco, Mexico.

List of accepted papers

Workshop Schedule

Model checking (MC) is the name given to the process of determining whether or not a formula of some logic is satisfied by a model for the logic. Model checking is limited by its exponential complexity with respect to the size of the system being verified. Nevertheless, MC procedures for many classes of models and logics of interest have been efficiently automated and successfully applied to a broad range of real-size applications in the last decade. These recent advances have lead to a growth of interest in the use of the technology in Artificial Intelligence (AI). In the meantime, state space exploration is a central aspect of AI, and the AI community has a long and impressive line of research in developing and improving search algorithms over very large state spaces under a broad range of assumptions. MC researchers are showing a growing interest in this vast body of knowledge, as a way to mitigate the state-space explosion problem.
Under a slightly different perspective there is growing interest in the use of model checking techniques for verifying and validating AI applications (as opposed to inside these applications themselves). This is becoming a critical issue, as AI techniques are increasingly considered for safety-critical applications such as space missions. AI software typically features unconventional architectures and requirements that ask for specific verification solutions. These solutions will only emerge from a sustained dialogue between the AI and V&V communities, through forums such as this one.

The purpose of the Second MoChArt workshop is therefore to bring together researchers with an interest in both MC and AI. The goals are to tease out common themes and differences, identify common problems and their solutions, share experiences with the applicability of techniques from one field to problems from the other, and to identify the key issues to be addressed in increasing the convergence between MC and AI. The workshop will welcome submissions on all ideas, research, experiments and tools that relate to both MC and AI fields.

Topics of interest include:

  • Foundations
    • Comparisons between MC and AI problems, approaches and algorithms.
    • Model checking for combined modal/temporal logics
    • Model checking for logics of common sense reasoning
  • Model checking approaches to AI
    • Planning via model checking
    • Model checking for multi-agent systems
    • Model checking for diagnosis
    • Model checking for games
    • Using concurrency models in AI (Process Algebras, Petri Nets, Statecharts,...)
  • AI approaches to model checking
    • AI approaches to the state explosion problem
    • Heuristics for model checking
    • AI approaches to automatic abstraction
  • Model checking for verification of AI systems
    • Requirements/specifications/properties for AI systems
    • Automated verification of AI systems
    • Model checking of multi-agent systems
    • Model checking of model-based systems
    • Model checking of knowledge-based systems
  • Tools related to any of these topics
  • Case studies related to any of these topics


The workshop notes will include original material. Archived material will also be considered for presentation but will not appear in the proceedings. Shorter papers are encouraged, particularly those exposing novel ideas or work in progress.

Authors are invited to submit papers (11pt, letter or A4, no more than 12 pages long) in PostScript format or Adobe PDF by March 17, 2003 to the following e-mail address: mochart03@na.infn.it.

The first page of each submission should carry the contact details of a nominated contact person, including email address.


Participation will be by invitation. Potentially interested participants must submit a *short* position statement, indicating the reasons for their interest in the topics of the workshop to the e-mail address mochart03@na.infn.it, by April 1, 2003.

Important Dates and Deadlines

  • Deadline for the submission of papers: March 17, 2003
  • Notification of acceptance/rejection: March 30, 2003.
  • Deadline for the position statement: April 1, 2003.
  • Deadline for the receipt of camera-ready: May 15, 2003.
  • Workshop: August 10, 2003.

Organizing Committee

Massimo Benerecetti
Dipartimento di Scienze Fisiche
Universita di Napoli ``Federico II''
Via Cintia, Complesso Monte S. Angelo
I-80126 Napoli, Italy

Charles Pecheur
NASA Ames Research Center, M/S 269-2
Moffett Field, CA 94035, U.S.A.

Programme Committee

Alessandro Cimatti (ITC-IRST)
Dimitra Giannakopoulou (RIACS / NASA Ames)
Enrico Giunchiglia (University of Genoa)
Allen Goldberg (KT / NASA Ames)
Robert Goldman (Smart Information Flow Technologies)
Lina Khatib (KT / NASA Ames)
Christine Largouet (ENSAR / IRISA)
Alessio Lomuscio (King's College)
Ilkka Niemela (Helsinki University of Technology)
Claudia Picardi (University of Torino)
Mark Ryan (University of Birmingham)
Reid Simmons (Carnegie Mellon)
Sylvie Thiebaux (Australian National University Camberra)
Paolo Traverso (ITC-IRST)
Ron Van der Meyden (University of New South Wales)
Mike Wooldridge (University of Liverpool)

PostScript, PDF and ASCII version of the Call For Papers.

Link to past editions: MoChArt-02 held in Lyon, France - July 22/23, 2002 (co-located with ECAI-2002).