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. ---------------------------------------