Robert Mattmüller – Publications

(Show all abstracts) (Hide all abstracts)

2012

Yusra Alkhazraji, Martin Wehrle, Robert Mattmüller and Malte Helmert.
A Stubborn Set Algorithm for Optimal Planning.
In Proceedings of the 20th European Conference on Artificial Intelligence (ECAI 2012). 2012.
To appear.
(Show abstract) (Hide abstract) (PDF)

We adapt a partial order reduction technique based on stubborn sets, originally proposed for detecting dead ends in Petri Nets, to the setting of optimal planning. We demonstrate that stubborn sets can provide significant state space reductions on standard planning benchmarks, outperforming the expansion core method.

2011

Hans-Jörg Peter, Rüdiger Ehlers and Robert Mattmüller.
Synthia: Verification and Synthesis for Timed Automata.
In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV 2011), pp. 649-655. Springer-Verlag 2011.
(Show abstract) (Hide abstract) (PDF)

We present Synthia, a new tool for the verification and synthesis of open real-time systems modeled as timed automata. The key novelty of Synthia is the underlying abstraction refinement approach that combines the efficient symbolic treatment of timing information by difference bound matrices (DBMs) with the usage of binary decision diagrams (BDDs) for the discrete parts of the system description. Our experiments show that the analysis of both closed and open systems greatly benefits from identifying large relevant and irrelevant system parts on coarse abstractions early in the solution process. Synthia is licensed under the GNU GPL and available from our website.

2010

Rüdiger Ehlers, Robert Mattmüller and Hans-Jörg Peter.
Combining Symbolic Representations for Solving Timed Games.
In Proceedings of the 8th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS 2010), pp. 107-121. Springer-Verlag 2010.
(Show abstract) (Hide abstract) (PDF)

We present a general approach to combine symbolic state space representations for the discrete and continuous parts in the synthesis of winning strategies for timed reachability games. The combination is based on abstraction refinement where discrete symbolic techniques are used to produce a sequence of abstract timed game automata. After each refinement step, the resulting abstraction is used for computing an under- and an over-approximation of the timed winning states. The key idea is to identify large relevant and irrelevant parts of the precise weakest winning strategy already on coarse, and therefore simple, abstractions. If neither the existence nor nonexistence of a winning strategy can be established in the approximations, we use them to guide the refinement process. Based on a prototype that combines binary decision diagrams and difference bound matrices, we experimentally evaluate the technique on standard benchmarks from timed controller synthesis. The results clearly demonstrate the potential of the new approach concerning running time and memory consumption compared to the classical on-the-fly algorithm implemented in UPPAAL-Tiga.
J. Benton, Kartik Talamadupula, Patrick Eyerich, Robert Mattmüller and Subbarao Kambhampati.
G-value Plateaus: A Challenge for Planning.
In Ronen Brafman, Héctor Geffner, Jörg Hoffmann and Henry Kautz (eds.), Proceedings of the 20th International Conference on Automated Planning and Scheduling (ICAPS 2010), pp. 259-262. AAAI Press 2010.
(Show abstract) (Hide abstract) (PDF) (BIB)

Recent years have seen the development of several scalable planners, many of which follow the string of successes found in using heuristic, best-first search methods. While this provides positive reinforcement for continuing work along these lines, fundamental problems arise when handling objectives whose value does not change with each search operation. An extreme case of this occurs when handling the objective of generating a temporal plan with short makespan. Typically used heuristic search methods assume strictly positive edge costs for their guarantees on completeness and optimality to hold, while the usual "fattening" and "advance time" steps of heuristic search algorithms for temporal planning have the potential for zero-cost edges, resulting in "g-value plateaus". In this paper we point out some underlying difficulties with using modern heuristic search methods for optimizing makespan and discuss how the presence of these problems contributes to the poor performance of makespan-optimizing heuristic search planners. To further illustrate this, we show empirical results on recent benchmarks using a planner made with makespan optimization in mind.
Robert Mattmüller, Manuela Ortlieb, Malte Helmert and Pascal Bercher.
Pattern Database Heuristics for Fully Observable Nondeterministic Planning.
In Ronen Brafman, Héctor Geffner, Jörg Hoffmann and Henry Kautz (eds.), Proceedings of the 20th International Conference on Automated Planning and Scheduling (ICAPS 2010), pp. 105-112. AAAI Press 2010.
(Show abstract) (Hide abstract) (PDF) (slides; PDF) (BIB)

When planning in an uncertain environment, one is often interested in finding a contingent plan that prescribes appropriate actions for all possible states that may be encountered during the execution of the plan. We consider the problem of finding strong and strong cyclic plans for fully observable nondeterministic (FOND) planning problems. The algorithm we choose is LAO*, an informed explicit state search algorithm. We investigate the use of pattern database (PDB) heuristics to guide LAO* towards goal states. To obtain a fully domain-independent planning system, we use an automatic pattern selection procedure that performs local search in the space of pattern collections. The evaluation of our system on the FOND benchmarks of the Uncertainty Part of the International Planning Competition 2008 shows that our approach is competitive with symbolic regression search in terms of problem coverage and speed.

2009

Hans-Jörg Peter and Robert Mattmüller.
Component-based Abstraction Refinement for Timed Controller Synthesis.
In Theodore P. Baker (ed.), Proceedings of the 30th IEEE Real-Time Systems Symposium (RTSS 2009), pp. 364-374. IEEE Computer Society 2009.
(Show abstract) (Hide abstract) (PDF) (BIB)

We present a novel technique for synthesizing controllers for distributed real-time environments with safety requirements. Our approach is an abstraction refinement extension to the on-the-fly algorithm by Cassez et al. from 2005. Based on partial compositions of some environment components, each refinement cycle constructs a sound abstraction that can be used to obtain under- and over-approximations of all valid controller implementations. This enables (1) early termination if an implementation does not exist in the over-approximation, or, if one does exist in the under-approximation, and (2) pruning of irrelevant moves in subsequent refinement cycles. In our refinement loop, the precision of the abstractions incrementally increases and converges to all specification-critical components.

We implemented our approach in a prototype synthesis tool and evaluated it on an industrial benchmark. In comparison with the timed game solver UPPAAL-Tiga, our technique outperforms the nonincremental approach by an order of magnitude.
Patrick Eyerich, Robert Mattmüller and Gabriele Röger.
Using the Context-enhanced Additive Heuristic for Temporal and Numeric Planning.
In Proceedings of the 19th International Conference on Automated Planning and Scheduling (ICAPS 2009), pp. 130-137. AAAI Press 2009.
(Show abstract) (Hide abstract) (PDF) (slides; PDF) (BIB)

Planning systems for real-world applications need the ability to handle concurrency and numeric fluents. Nevertheless, the predominant approach to cope with concurrency followed by the most successful participants in the latest International Planning Competitions (IPC) is still to find a sequential plan that is rescheduled in a post-processing step. We present Temporal Fast Downward (TFD), a planning system for temporal problems that is capable of finding low-makespan plans by performing a heuristic search in a temporal search space. We show how the context-enhanced additive heuristic can be successfully used for temporal planning and how it can be extended to numeric fluents. TFD often produces plans of high quality and, evaluated according to the rating scheme of the last IPC, outperforms all state-of-the-art temporal planning systems.
Pascal Bercher and Robert Mattmüller.
Solving Non-deterministic Planning Problems with Pattern Database Heuristics.
In B. Mertsching, M. Hund and Z. Aziz (eds.), Proceedings of the 32nd Annual Conference on Artificial Intelligence (KI 2009), pp. 57-64. Springer-Verlag 2009.
(Show abstract) (Hide abstract) (PDF) (slides; PDF) (BIB)

Non-determinism arises naturally in many real-world applications of action planning. Strong plans for this type of problems can be found using AO* search guided by an appropriate heuristic function. Most domain-independent heuristics considered in this context so far are based on the idea of ignoring delete lists and do not properly take the non-determinism into account. Therefore, we investigate the applicability of pattern database (PDB) heuristics to non-deterministic planning. PDB heuristics have emerged as rather informative in a deterministic context. Our empirical results suggest that PDB heuristics can also perform reasonably well in non-deterministic planning. Additionally, we present a generalization of the pattern additivity criterion known from classical planning to the non-deterministic setting.

2008

Pascal Bercher and Robert Mattmüller.
A Planning Graph Heuristic for Forward-Chaining Adversarial Planning.
In Proceedings of the 18th European Conference on Artificial Intelligence (ECAI 2008), pp. 921-922. IOS Press 2008.
(Show abstract) (Hide abstract) (PDF) (slides; PDF) (poster; PDF) (BIB)

In contrast to classical planning, in adversarial planning, the planning agent has to face an adversary trying to prevent him from reaching his goals. In this paper, we investigate a forward-chaining approach to adversarial planning based on the AO* algorithm. The exploration of the underlying AND/OR graph is guided by a heuristic evaluation function, inspired by the relaxed planning graph heuristic used in the FF planner. Unlike FF, our heuristic uses an adversarial planning graph with distinct proposition and action layers for the protagonist and antagonist. First results suggest that in certain planning domains, our approach yields results competitive with the state of the art.
Malte Helmert and Robert Mattmüller.
Accuracy of Admissible Heuristic Functions in Selected Planning Domains.
In Proceedings of the 23rd AAAI Conference on Artificial Intelligence (AAAI 2008), pp. 938-943. AAAI Press 2008.
(Show abstract) (Hide abstract) (PDF) (slides; PDF) (BIB)

The efficiency of optimal planning algorithms based on heuristic search crucially depends on the accuracy of the heuristic function used to guide the search. Often, we are interested in domain-independent heuristics for planning. In order to assess the limitations of domain-independent heuristic planning, it appears interesting to analyse the (in)accuracy of common domain-independent planning heuristics in the IPC benchmark domains. For a selection of these domains, we analytically investigate the accuracy of the h⁺ heuristic, the h^m family of heuristics, and certain (additive) pattern database heuristics, compared to the perfect heuristic h^*. Whereas h⁺ and additive pattern database heuristics usually return cost estimates proportional to the true cost, non-additive h^m and non-additive pattern-database heuristics can yield results underestimating the true cost by arbitrarily large factors.

2007

Malte Helmert and Robert Mattmüller.
On the Accuracy of Admissible Heuristic Functions in Selected Planning Domains.
In Proceedings of the ICAPS-2007 Workshop on Heuristics for Domain-independent Planning: Progress, Ideas, Limitations, Challenges. 2007.
Superseded by the AAAI 2008 paper by the same name.
(Show abstract) (Hide abstract) (PDF)

The efficiency of optimal planning algorithms based on heuristic search crucially depends on the accuracy of the heuristic function used to guide the search. Often, we are interested in domain-independent heuristics for planning. In assessing the limitations of domain-independent heuristic planning, it appears interesting to analyse the (in)accuracy of common domain-independent planning heuristics in the IPC benchmark domains. For a selection of these domains, we analytically investigate the accuracy of the h⁺ heuristic, the h^k family of heuristics, and certain (additive) pattern database heuristics, compared to the optimal heuristic h^*. Whereas h⁺ and additive pattern database heuristics usually return cost estimates proportional to the true cost, non-additive h^k and non-additive pattern-database heuristics can yield results underestimating the true cost by arbitrarily large factors.
Robert Mattmüller and Jussi Rintanen.
Planning for Temporally Extended Goals as Propositional Satisfiability.
In Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI 2007), pp. 1966-1971. 2007.
(Show abstract) (Hide abstract) (PDF) (PS.GZ) (poster; PDF) (BIB)

Planning for temporally extended goals (TEGs) expressed as formulae of Linear-time Temporal Logic (LTL) is a proper generalization of classical planning, not only allowing to specify properties of a goal state but of the whole plan execution. Additionally, LTL formulae can be used to represent domain-specific control knowledge to speed up planning. In this paper we extend SAT-based planning for LTL goals (akin to bounded LTL model-checking in verification) to partially ordered plans, thus significantly increasing planning efficiency compared to purely sequential SAT planning. We consider a very relaxed notion of partial ordering and show how planning for LTL goals (without the next-time operator) can be translated into a SAT problem and solved very efficiently. The results extend the practical applicability of SAT-based planning to a wider class of planning problems. In addition, they could be applied to solving problems in bounded LTL model-checking more efficiently.

2006

Malte Helmert, Robert Mattmüller and Sven Schewe.
Selective Approaches for Solving Weak Games.
In Proceedings of the Fourth International Symposium on Automated Technology for Verification and Analysis (ATVA 2006), pp. 200-214. Springer-Verlag 2006.
(Show abstract) (Hide abstract) (PDF)

Model-checking alternating-time properties has recently attracted much interest in the verification of distributed protocols. While checking the validity of a specification in alternating-time temporal logic (ATL) against an explicit model is cheap (linear in the size of the formula and the model), the problem becomes EXPTIME-hard when symbolic models are considered. Practical ATL model-checking therefore often consumes too much computation time to be tractable.

In this paper, we describe a novel approach for ATL model-checking, which constructs an explicit weak model-checking game on-the-fly. This game is then evaluated using heuristic techniques inspired by efficient evaluation algorithms for and/or-trees.

To show the feasibility of our approach, we compare its performance to the ATL model-checking system MOCHA on some practical examples. Using very limited heuristic guidance, we achieve a significant speedup on these benchmarks.
Malte Helmert, Robert Mattmüller and Gabriele Röger.
Approximation Properties of Planning Benchmarks.
In Proceedings of the 17th European Conference on Artificial Intelligence (ECAI 2006), pp. 585-589. 2006.
(Show abstract) (Hide abstract) (PDF)

For many classical planning domains, the computational complexity of non-optimal and optimal planning is known. However, little is known about the area in between the two extremes of finding some plan and finding optimal plans. In this contribution, we provide a complete classification of the propositional domains from the first four International Planning Competitions with respect to the approximation classes PO, PTAS, APX, poly-APX, and NPO.
Robert Mattmüller.
Erfüllbarkeitsbasierte Handlungsplanung mit temporal erweiterten Zielen.
Diploma thesis, Albert-Ludwigs-Universität, Freiburg, Germany 2006.
In German.
(PDF)