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).
K*: Heuristics-Guided, On-the-Fly k Shortest Paths Search | Husain Aljazzar and Stefan Leue |
External Memory BFS with Delayed Duplicate Detection on the GPU | Stefan Edelkamp and Damian Sulewski |
Computing Applicability Conditions for Plans with Loops: New Results | Siddharth Srivastava and Neil Immerman and Shlomo Zilberstein |
Action Planning for Automated Program Verification | Stefan Edelkamp and Mark Kellershoff and Damian Sulewski |
Automatic data abstraction in model checking Multi-Agent Systems | Alessio Lomuscio and Hongyang Qu and Francesco Russo |
An Approach to Compositional Verification of Reactive Multiagent Systems | Jean-Michel Contet and Pablo Gruer and Franck Gechter and Abderrafiaa Koukam |
Automated verification of resource requirements in multi-agent systems using abstraction | Natasha Alechina and Brian Logan and Hoang Nga Nguyen and Abdur Rakib |
Improved Bounded Model Checking for a Fair Branching-Time Temporal Epistemic Logic | Xiaowei Huang and Cheng Luo and Ron van der Meyden |
Symbolic Model Checking the Knowledge in Herbivore Protocol | Xiangyu 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.