Third Workshop on
Model Checking and Artificial Intelligence
MoChArt '05

(Revised) Announcement and Call for Papers

August 27, 2005 - San Francisco, CA, USA
co-located with CONCUR 2005 and SPIN 2005

Extended Submission deadline: June 7, 2005

Aims and Scope

Exploration of very large search spaces is at the heart of many disciplines of computer science and engineering, and formal verification and artificial intelligence in particular.  On one hand, model checking (MC) is used to automatically verify logical properties over a model of a system, and 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 MC principles and tools in Artificial Intelligence (AI).  In the meantime, the AI community has had 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 interested in leveraging this vast body of knowledge, as a way to mitigate the state-space explosion problem. Under a slightly different perspective, there is also a demand for innovative verification approaches, such as model checking, for AI applications.  This is becoming a critical need, as AI technologies 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. All these trends call for an increased dialogue between the AI and V&V communities.

The purpose of the MoChArt workshop series 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.

MoChArt '05 follows on two very lively and productive editions: MoChArt '02 in Lyon (associated to ECAI) and MoChArt '03 in Acapulco (associated to IJCAI), both coupled to artificial intelligence conferences.  This time, MoChArt '05 will be co-located with two major international events in the field of formal verification: the 16th International Conference on Concurrency Theory (CONCUR 2005) and the 12th International SPIN Workshop on Model Checking of Software (SPIN 2005).  The event will be held at the Stanford Court Hotel in San Francisco, CA.

Topics of Interest


The proceedings of the workshop will be published electronically by Elsevier as a volume of Electronic Notes in Theoretical Computer Science (Editor's site).  The volume should be available before the workshop begins.  A hardcopy will be distributed to workshop participants.  Note that ENTCS requires submissions to be prepared using the LaTeX system with specific formatting files.


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 Adobe PDF format by June 7, 2005 (extended) to the following e-mail address:  The first page of each submission should carry the contact details of a nominated contact person, including email address. 

Important note: while any submission adhering to the above guidelines will be considered, please note that the final version of accepted papers will have to use LaTeX with provided formatting files for inclusion in the published ENTCS volume.  Other formats remain acceptable but cannot be included in the ENTCS proceedings and are therefore strongly discouraged.


Participation will be open to all, but limited to available seating (30 seats). Priority will be given to authors of presented papers and participants of past MoChArt events. Registration to CONCUR 2005 and/or SPIN 2005 is not required to attend the workshop (though we strongly recommend not to miss the opportunity).  Details on registration fees and modalities will be posted later.

Important Dates and Deadlines

Organized by

Charles Pecheur
Université Catholique de Louvain

Brian Williams
Massachusetts Institute of Technology

Programme Committee


Please contact Charles Pecheur for any additional information:

Charles Pecheur
UCL, Dept. Computing Science and Engineering
Place Sainte Barbe 2
1348 Louvain La Neuve
Phone: +32-10-47 87 79

Last updated May 24, 2005 – Curator: Charles Pecheur