Third
Workshop on
Model Checking and Artificial Intelligence
MoChArt '05
(Revised) Announcement
and Call for Papers
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
- Foundations
- Comparisons between MC
and AI problems, approaches and
algorithms.
- Model checking for
combined modal/temporal logics
- Model checking for
logics of common sense reasoning
- Model
checking approaches to AI
- Model checking for
planning and scheduling
- Model checking for
multi-agent systems
- Model checking for
diagnosis
- Model checking for games
- Using concurrency models
in AI (Process Algebras, Petri
Nets,
Statecharts,...)
- AI
approaches to model checking
- Planning and scheduling
for model checking
- AI approaches to the
state explosion problem
- Heuristics for model
checking
- AI approaches to
automated decomposition/abstraction/approximation
- Using AI reasoners for
model checking
- Model
checking for verification of AI systems
- Requirements/specifications/properties
for AI systems
- Automated verification
of AI systems
- Model checking of
multi-agent systems
- Model checking of
model-based systems
- Model checking of
knowledge-based systems
- Tools
related to any of these topics
- Case
studies related to any of these topics
Proceedings
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.
Submission
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: mochart05@info.ucl.ac.be.
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
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
- Deadline for submission of
papers: June 7, 2005 (extended).
- Notification of
acceptance/rejection: July 5, 2005
(postponed).
- Deadline for final version
of accepted papers: July
29, 2005.
- Workshop: August 27, 2005.
Organized
by
Charles
Pecheur
Université Catholique de Louvain
pecheur@info.ucl.ac.be
Programme
Committee
- Massimo Benerecetti, Universita di Napoli (Italy)
- Alessandro Cimatti, ITC-IRST (Italy)
- Stefan Edelkamp, Universität Dortmund (Germany)
- Enrico Giunchiglia, University of Genoa (Italy)
- Robert Goldman, Smart Information Flow Technologies (USA)
- Gerard Holzmann, JPL (USA)
- Froduald Kabanza, Université de Sherbrooke (Canada)
- Alessio Lomuscio, University College London (UK)
- Tim Menzies, Portland State University (USA)
- David Musliner, Honeywell (USA)
- Ilkka Niemela, Helsinki University of Technology (Finland)
- Ulf Nilsson, University of Linköping (Sweden)
- Charles Pecheur, Université catholique de Louvain (Belgium)
- Mark Ryan, University of Birmingham (UK)
- Sylvie Thiebaux, Australian National University / NICTA
(Australia)
- Ron Van der Meyden, University of New South Wales / NICTA
(Australia)
- Brian Williams, MIT (USA)
- Mike Wooldridge, University of Liverpool (UK)
Contact
Please
contact Charles Pecheur
for any additional information:
Charles Pecheur
UCL, Dept. Computing Science and Engineering
Place Sainte Barbe 2
1348 Louvain La Neuve
Belgique
Phone: +32-10-47 87 79