AIPS2000 Workshop on Model-Theoretic Approaches to Planning: Preliminary Programme

["Carola Dori" <dori@itc.it>]

The time schedule is still preliminary and has to be decided with the
AIPS2000 organizers!


--------------------------------------------------------------------------
                      AIPS2000 Workshop on
               Model-Theoretic Approaches to Planning:
                     Preliminary Programme
--------------------------------------------------------------------------

     8.30 -  9.30 Invited Talk:
                  Automated Verification = Graphs, Automata, and Logic
                  (Moshe Y. Vardi)

     9.30 - 10.00 Using Model Checking to Plan Hard Real-Time Controllers
                  (R.P. Goldman, D.J. Musliner, M.J. Pelican)

    10.00 - 10.15 Coffee Break

    10.15 - 10.45 Propositional planning
                  (M.P. Fourman)

    10.45 - 11.15 On the Implementation of MIPS
                  (S. Edelkamp and M. Helmert)

    10.15 - 11.45 OBDD-based Deterministic Planning using the UMOP
                  Planning Framework
                  (R.M. Jensen, M.M Veloso)

    11.45 - 12.15  Solving the entailment problem in the fluent calculus
                   using Bynary Decision Diagrams (Extended Abstract)
                   (S. Hoelldobler and P. Stoerr)

    12.15 -  2.00 Lunch

     2.00 -  3.00 Invited Talk:
                  Planning with State Models, MDPs and POMDPs:
                  A general framework for planning and control in AI
                  (Hector Geffner)


     3.00 -  3.15 Coffee Break

     3.15 -  3.45 Forward conformant Planning via symbolic model checking
                  (A. Cimatti, M. Roveri)

     3.45 -  4.15 ZANDER: A model theoretic approach to planning in
                  partially observable stochastic domains
                  (S. Majerci and M. Littman)

     4.15 -  4.45 Planning as Satisfiability in simple
                  nondeterministic domains
                  (P. Ferraris, E. Giunchiglia)

     4.45 -  5.15 Planning with Domain and Control Knowledge in
                  Linear Time Logic
                  (M. Cialdea Meyer,A. Orlandini,G. Balestreri,C.
Limongelli)

     5.15 -  5.30 Conclusions

--------------------

INVITED TALK:
Automated Verification = Graphs, Automata, and Logic

Moshe Y. Vardi
Rice University

In automated verification one uses algorithmic techniques to
establish the correctness of the design with respect to a given
property. Automated verification is based on a small number of
key algorithmic ideas, tying together graph theory, automata
theory, and logic. In this self-contained talk I will describe how
this "holy trinity" gave rise to automated-verification tools.

--------------------
INVITED TALK:
Planning with State Models, MDPs and POMDPs:
A general framework for planning and control in AI

Hector Geffner
Depto de Computacion
Universidad Simon Bolivar
Caracas, Venezuela

We consider the problem of planning in a general setting
where actions can be deterministic, non-deterministic, or probabilistic,
and their effects can be fully or partially observable. The task is to
obtain
a  plan or closed-loop controller  given a suitable description
of the initial situation, actions, sensors,  and goals.

We approach this problem by distinguishing three elements:

- models (that help us to make the tasks mathematically precise)
- languages (that help us to state problems in a convenient way), and
- algorithms (that compute the desired solutions: plans, controllers, etc.)

We show that the models - State Models, Markov Decision Processes (MDPs)
and Partially Observable MDPs - can be conveniently described using
suitable logical action languages, and in many cases can be solved
by search algorithms that combine ideas from heuristic search and
dynamic programming.  We also present some empirical results,
and discuss limitations and challenges.

This is joint work with Blai Bonet.
---------------------------------------