Selected Publications
S. Biundo, B. Schattenberg:
From Abstract Crisis to Concrete Relief -
A Preliminary Report on Combining State Abstraction and
HTN Planning
Proceedings of the 6th European Conference on Planning (ECP-01), Toledo, Spain, September 2001.
Abstract:
Flexible support for crisis management can definitely be improved by
making use of advanced planning capabilities. However, the complexity
of the underlying domain often causes intractable efforts in modelling
the domain as well as a huge search space to be explored by the
system. A way to overcome these problems is to impose a sophisticated
structure not only according to tasks but also according to
relationships between and properties of the objects involved. We
outline the prototype of a system that is capable of tackling planning
for complex application domains. It is based on a well-founded
combination of action and state abstractions. The paper presents the
basic techniques and provides a formal semantic foundation of the
approach. It introduces the planning system and illustrates the
underlying principles by examples taken from the crisis management
domain used in our ongoing project.
S. Biundo, M. Fox (Eds.):
Recent Advances in AI Planning.
Proceedings of the 5th European Conference on Planning (ECP-99), Durham, UK, September 1999.
Lecture Notes in Artificial Intelligence LNAI 1809, Springer Verlag, 2000.
Abstract:
The European Conferences on Planning (ECP) are a major forum for the
presentation of new research in Artificial Intelligence Planning and
Scheduling. This volume contains the 27 papers that were presented at
the conference. They cover a variety of aspects in current AI Planning
and Scheduling. Several prominent planning paradigms are represented,
including planning as satisfiability and other model checking
strategies, planning as heuristic state-space search, and
Graphplan-based approaches. Moreover, various new scheduling
approaches and combinations of planning and scheduling methods are introduced.
S. Biundo, W. Stephan:
System Assistance in Structured Domain Model Development.
IJCAI-97, pages 1240-1245.
Abstract:
In this paper, we introduce a domain modeling tool that supports
users in the incremental and modular development of verified
models of planning domains. It relies on a logic-based concept for
systematic domain model construction that provides well-defined, safe
operations for the union, extension, and refinement of already
existing models. The system is equiped with a deductive component. It
automatically performs the proofs necessary to guarantee both the
consistency of single models and the safety of operations on models.
By means of detailed examples, it is shown how the system has been
used for the structured development of a model for a complex,
safety-critical planning domain.
S. Biundo, W. Stephan:
Modeling Planning Domains Systematically.
ECAI-96, pages 599-603.
Abstract:
We present a systematic approach to the modular and incremental construction of provably consistent domain models for planning. It is based on a temporal logic framework that in particular allows for the introduction of abstract datatypes which can usefully be applied to mirror the computational aspects of planning problems and their solutions. A formal concept is developed that enables the construction as well as the modification of already existing domain models in a sound manner. This includes well-defined operations for the union, extension, and refinement of domain models.
W. Stephan, S. Biundo:
Deduction-based Refinement Planning.
AIPS-96, pages 213-220.
Abstract:
We introduce a method of deduction-based refinement planning where prefabricated general solutions are adapted to special problems.
Refinement proceeds by stepwise transforming non-constructive problem specifications into executable plans. For each refinement step there is a correctness proof guaranteeing the soundness of refinement and with that the generation of provably correct plans.
By solving the hard deduction problems once and for all on the abstract level, planning on the concrete level becomes more efficient. With that, our approach aims at making deductive planning feasible in realistic contexts.
Our approach is based on a temporal logic framework that allows for the representation of specifications and plans on the same linguistic level. Basic actions and plans are specified using a programming language the constructs of which are formulae of the logic. Abstract solutions are represented as - possibly
recursive - procedures. It is this common level of representation and the fluid transition between specifications and plans our refinement process basically relies upon.
S. Biundo:
Present-Day Deductive Planning. Invited Talk.
Current Trends in AI Planning (EWSP-93), pages 1-5.
Abstract:
The paper presents an overview of the current state of the art in deductive planning. Here, deductive planning is understood as solving the planning problem by the application of theorem proving methods. The paper briefly sketches the various logics and calculi which have been used for deductive planning up to now.
W. Stephan, S. Biundo:
A New Logical Framework for Deductive Planning.
IJCAI-93, pages 32-38.
Abstract:
In this paper we present a logical framework for defining consistent
axiomatizations of planning domains. A language to define
basic actions and structured plans is embedded in a logic.
This allows general properties of a whole planning
scenario to be proved as well as plans to be formed deductively. In
particular, frame assertions and domain constraints as invariants of
the basic actions can be formulated and proved. Even for complex plans
most frame assertions are obtained by purely syntactic analysis. In such
cases the formal proof can be generated in a uniform way. The formalism
we introduce is especially useful when treating recursive plans.
A tactical theorem
prover, the Karlsruhe Interactive Verifier KIV is used to
implement this logical framework.
M. Bauer, S. Biundo, D. Dengler, J. Koehler, G. Merziger:
PHI - A Logic-Based Tool for Intelligent Help Systems.
IJCAI-93, pages 460-466.
Abstract:
We introduce a logic-based system which improves the performance of
intelligent help systems by supplying them with plan generation and
plan recognition components. Both components work in close mutual
cooperation. There are two modes of cross-talk between them, one where
plan recognition is done on the basis of abstract plans provided by
the planner and the other where optimal plans are generated based on
recognition results. The examples which are presented are taken from
an operating system domain, namely from the Unix mail domain.
S. Biundo, D. Dengler, J. Koehler:
Deductive Planning and Plan Reuse in a Command Language
Environment.
ECAI-92, pages 628-632.
Abstract:
We introduce a deductive planning system intended to supply
intelligent help systems. It consists of a deductive planner and a
plan reuse component, providing planning from first as well as
planning from second principles. Both components rely on an
interval-based temporal logic. The deductive formalisms realizing plan
formation from formal specifications and the reuse of already existing
plans are presented and demonstrated by examples taken from the domain
of operating systems.
S. Biundo:
Automatische Synthese rekursiver Programme als Beweisverfahren..
Informatik Fachberichte IFB 302, Springer Verlag, 1992.
Abstract:
In diesem Buch wird ein Verfahren vorgestellt, mit dem Induktionsbeweise von Existenzaussagen automatisch geführt werden können. Es ist ein deduktives Programmsyntheseverfahren, das, ausgehend von Existenzaussagen, die als formale Spezifikationen von Programmen aufgefaßt werden, rekursive Programme erzeugt. Kann ein solches Programm korrekt erstellt werden, so beschreibt der Syntheseprozeß gleichzeitig einen Induktionsbeweis der entsprechenden Existenzaussage. Auf der Basis dieses Verfahrens wurde ein automatisches Programmsynthesesystem entwickelt, das als Komponente des Karlsruher Induktionsbeweisers INKA implementiert worden ist und dort zum Beweis von Existenzaussagen eingesetzt wird.
Back to Susanne Biundo's homepage
biundo@ki.informatik.uni-ulm.de
Susanne Biundo, last update: November 19, 2001