MoChArt 2010: Call for Participation

[Jan-Georg Smaus]

                           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-12, 2010

                 http://mochart.informatik.uni-freiburg.de/

                              CALL FOR PARTICIPATION

We are happy to announce that our invited speaker will be Hector Geffner!

INTRODUCTION

Model checking is the process of determining whether a logic formula
is satisfied by a model. For many logics of interest, model checking
can be efficiently automated. This has led to widespread interest in
model checking as a technique for verifying properties of systems, and
the development of model checking tools (e.g., SMV, Uppaal, PHAVer,
and 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 are
increasingly relevant for 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 directed model checking, AI planning techniques are
applied in the search for error traces.

The MoChArt workshop brings together researchers from AI and model
checking. Apart from presentations of accepted papers, the programme
will include an invited talk. We expect around 25 participants.

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

ACCEPTED PAPERS

- 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

PARTICIPATION
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,
see:

http://www.aaai.org/Conferences/AAAI/aaai10.php

INVITED SPEAKER
Hector Geffner
DTIC, Universitat Pompeu Fabra
Barcelona, Spain

PROGRAM CHAIRS AND ORGANISING COMMITTEE

* Ron van der Meyden
   School of Computer Science and Engineering
   University of New South Wales
   meyden at cse.unsw.edu.au

* Jan-Georg Smaus
   Institut für Informatik
   Albert-Ludwigs-Universität Freiburg
   smaus at informatik.uni-freiburg.de

PROGRAM COMMITTEE

Rajeev Alur, University of Pennsylvania
Massimo Benerecetti, Università di Napoli "Federico II",
Alessandro Cimatti, IRST, Trento
Stefan Edelkamp, Universität Bremen
Enrico Giunchiglia, Università di Genova
Patrice Godefroid, Microsoft Research, Redmond
Aarti Gupta, NEC Laboratories America, Princeton
Klaus Havelund, NASA Jet Propulsion Laboratory & Caltech
Orna Kupferman, Hebrew University
Marta Kwiatkowska, University of Oxford
Alessio Lomuscio, Imperial College London
Charles Pecheur, Université Catholique de Louvain
Doron Peled, Bar Ilan University
Jussi Rintanen, NICTA & Australian National University
Michael Wooldridge, University of Liverpool