[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS] Model Checking and Artificial Intelligence (MoChArt 2010):call for papers
Sixth Workshop on
MODEL CHECKING and ARTIFICIAL INTELLIGENCE (MoChArt 2010)
At AAAI-2010, Twenty-Fourth AAAI Conference on
Atlanta, Georgia, USA, July 11-12, 2010
CALL FOR PAPERS
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,
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
TOPICS OF INTEREST
Topics of interest include (a more detailed list can be found on the
- Application of model checking techniques to AI problems.
- Model Checking and AI logics.
- Relations between different techniques used in the two fields for
similar purposes (e.g., reducing state explosion).
- New model checking techniques specifically for AI problems.
- Exploitation of AI techniques in model checking.
- Software tools for model checking in AI.
- Model checking for verification of AI systems.
Preliminary papers and papers on applications are strongly encouraged.
Deadline for submissions: March 31, 2010
Notification: April 23, 2010
Camera-ready paper due: May 4, 2010
Workshop: July 11 or 12, 2010
Submissions must be no more than 15 pages in length. Papers must be
submitted through the EasyChair web-based conference management
system: follow the link from the workshop web page. All papers will be
During the workshop, informal proceedings (working notes) will be
available. As with previous editions of MoChArt, post-proceedings
based on selected papers from the meeting (after a second round of
reviewing) and invited papers will be published in the LNCS/LNAI
series of Springer-Verlag.
The workshop forms part of the AAAI-2010 workshop programme. For full
information about AAAI-2010, including registration, travel &
to be anncounced
PROGRAM CHAIRS AND ORGANISING COMMITTEE
* Ron van der Meyden
School of Computer Science and Engineering
University of New South Wales
* Jan-Georg Smaus
Institut für Informatik
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