Sixth Workshop on
Model Checking and Artificial Intelligence
(MoChArt 2010)

At AAAI-2010, Twenty-Fourth AAAI Conference on
Artificial Intelligence
Atlanta, Georgia, USA, July 11, 2010


Model checking is the process of determining whether or not a formula of some logic is satisfied by a model for the logic. For many logics of interest -- particularly temporal and other modal logics -- model checking procedures can be efficiently automated. This has led to widespread interest in the use of model checking as a technique for verifying properties of systems, and the development of a number of widely used model checking tools (e.g., Carnegie-Mellon's SMV, Cadence-SMV, Uppaal, PHAVer, PRISM, and AT&T's SPIN).

The success of model checking in the computer aided verification community has led to a growth of interest in the use of model checking in artificial intelligence. Automated verification technologies such as model checking are increasingly of interest from the perspective of safety and reliability of autonomous systems. There has been a strong interest in this area from, e.g. NASA, which has applied it in the context of the Mars rovers and other autonomous robotics systems.

On the other hand, model checking, in particular if viewed in the wider context of system verification, falsification and development, has recently benefited from the use of AI techniques, e.g. search heuristics, abstraction techniques, and constraint satisfaction (particularly SAT solving, which underlies "bounded model checking").

One of the principal benefits of model checkers in verification is their ability to return error traces when the specification is false. Dually, such traces can be viewed as plans for falsifying the specification: this duality means that there is a close relationship with planning. In the area known as directed model checking, AI planning techniques are applied in the search for error traces.

The MoChArt workshop brings together researchers in AI with an interest in model checking, and researchers in model checking who are interested in AI techniques.

Previous editions of the workshop were held in Patras in 2008 (as a satellite workshop of ECAI), Riva del Garda in 2006 (as a satellite workshop of ECAI), San Francisco in 2005 (as a satellite workshop of CONCUR), Acapulco in 2003 (as a satellite workshop of IJCAI), and Lyon in 2002 (as a satellite workshop of ECAI).

Topics of Interest

Topics of interest include (but are not limited to): Preliminary papers and papers on applications are strongly encouraged.

Important Dates

Submission Procedures

Submissions must be no more than 15 pages in length. Papers must be submitted through the EasyChair web-based conference management system, preferably in LNCS format. All papers will be peer reviewed, and evaluated on the basis of relevance, technical quality, significance, evaluation, and presentation.

Invited Speaker

We are proud to announce that our invited speaker will be Hector Geffner. He will present a talk on Planning with Incomplete Information.

Accepted Papers

K*: Heuristics-Guided, On-the-Fly k Shortest Paths SearchHusain Aljazzar and Stefan Leue
External Memory BFS with Delayed Duplicate Detection on the GPUStefan Edelkamp and Damian Sulewski
Computing Applicability Conditions for Plans with Loops: New ResultsSiddharth Srivastava and Neil Immerman and Shlomo Zilberstein
Action Planning for Automated Program VerificationStefan Edelkamp and Mark Kellershoff and Damian Sulewski
Automatic data abstraction in model checking Multi-Agent SystemsAlessio Lomuscio and Hongyang Qu and Francesco Russo
An Approach to Compositional Verification of Reactive Multiagent SystemsJean-Michel Contet and Pablo Gruer and Franck Gechter and Abderrafiaa Koukam
Automated verification of resource requirements in multi-agent systems using abstractionNatasha Alechina and Brian Logan and Hoang Nga Nguyen and Abdur Rakib
Improved Bounded Model Checking for a Fair Branching-Time Temporal Epistemic LogicXiaowei Huang and Cheng Luo and Ron van der Meyden
Symbolic Model Checking the Knowledge in Herbivore ProtocolXiangyu Luo and Kaile Su and Ming Gu and Lijun Wu and Jinji Yang


During the workshop, informal proceedings (working notes) were available. As with previous editions of MoChArt, post-proceedings based on selected papers from the meeting and invited papers have been published in the LNCS/LNAI series of Springer-Verlag. You can find information about volume LNAI 6572 or access the online version.



The workshop is open to anyone interested in the topic. Please register soon! It would be appreciated if you could let us know about your interest in the workshop.

The workshop forms part of the AAAI-2010 workshop programme. Registration and accomodation booking is now available.

Program Chairs and Organising Committee

Programme Committee


We are fully aware that there are things in life more important than model checking and artificial intelligence. Therefore we will schedule the workshop so that there will a break from 14:00 to 17:00 (2pm to 5 pm), to give everyone the opportunity to watch the Footbaal World Cup Final. The game will be screened in the Lobby Bar of the conference hotel.