From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/1453 Path: news.gmane.org!not-for-mail From: "Carola Dori" Newsgroups: gmane.science.mathematics.categories Subject: AIPS2000 Workshop on Model-Theoretic Approaches to Planning: Preliminary Programme Date: Wed, 22 Mar 2000 12:52:16 +0100 Message-ID: <004b01bf93f5$190323d0$24001e0a@itc.it> NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1241017841 31322 80.91.229.2 (29 Apr 2009 15:10:41 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:10:41 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Wed Mar 22 10:08:29 2000 -0400 Original-Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id KAA24610 for categories-list; Wed, 22 Mar 2000 10:03:06 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Priority: 3 X-MSMail-Priority: Normal X-Mailer: Microsoft Outlook Express 5.00.2014.211 X-MimeOLE: Produced By Microsoft MimeOLE V5.00.2014.211 Original-Sender: cat-dist@mta.ca Precedence: bulk Original-Lines: 110 Xref: news.gmane.org gmane.science.mathematics.categories:1453 Archived-At: 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. ---------------------------------------