Dr. Martin Wehrle – Publications

Stubborn sets are a pruning technique for state-space search which is well established in optimal classical planning. In this paper, we show that weak stubborn sets introduced in recent work in planning are actually not weak stubborn sets in Valmari's original sense. Based on this finding, we introduce weak stubborn sets in the original sense for planning by providing a generalized definition analogously to generalized strong stubborn sets in previous work. We discuss the relationship of strong, weak and the previously called weak stubborn sets, thus providing a further step in getting an overall picture of the stubborn set approach in planning.

Planning as model checking based on source-to-source compilations has found increasing attention. Previously proposed approaches for temporal and hybrid planning are based on static translations, in the sense that the resulting model checking problems are uniquely defined by the given input planning problems. As a drawback, the translations can become too large to be efficiently solvable. In this paper, we address propositional temporal planning, lifting static translations to a more flexible framework. Our framework is based on a refinement cycle that allows for adaptively computing suitable translations of increasing size. Our experiments on temporal IPC domains show that the resulting translations to timed automata often become succinct, resulting in promising performance when applied with the directed model checker MCTA.

We transfer the notion of structural symmetries to lifted planning task representations, based on abstract structures which we define to model planning tasks. We show that symmetries are preserved by common grounding methods and we shed some light on the relation to previous symmetry concepts used in planning. Using a suitable graph representation of lifted tasks, our experimental analysis of common planning benchmarks reveals that symmetries occur in the lifted representation of many domains. Our work establishes the theoretical ground for exploiting symmetries beyond their previous scope, such as for faster grounding and mutex generation, as well as for state space transformations and reductions.

Analyzing reachability in large discrete transition systems is an important sub-problem in several areas of AI, and of CS in general. State space search is a basic method for conducting such an analysis. A wealth of techniques have been proposed to reduce the search space without affecting the existence of (optimal) solution paths. In particular, strong stubborn set (SSS) pruning is a prominent such method, analyzing action dependencies to prune commutative parts of the search space. We herein show how to apply this idea to star-topology decoupled state space search, a recent search reformulation method invented in the context of classical AI planning.

Star-topology decoupled state space search, short decoupled search, addresses planning tasks where a single center component interacts with several leaf components. The search exploits a form of conditional independence arising in this setting: given a fixed path p of transitions by the center, the possible leaf moves compliant with p are independent across the leaves. Decoupled search thus searches over center paths only, maintaining the compliant paths for each leaf separately. This avoids the enumeration of combined states across leaves.

Just like standard search, decoupled search is adversely affected by commutative parts of its search space. The adaptation of strong stubborn set pruning is challenging due to the more complex structure of the search space, and the resulting ways in which action dependencies may affect the search. We spell out how to address this challenge, designing optimality-preserving decoupled strong stubborn set (DSSS) pruning methods. We introduce a design for star topologies in full generality, as well as simpler design variants for the practically relevant fork and inverted fork special cases. We show that there are cases where DSSS pruning is exponentially more effective than both, decoupled search and SSS pruning, exhibiting true synergy where the whole is more than the sum of its parts. Empirically, DSSS pruning reliably inherits the best of its components, and sometimes outperforms both.

Pruning techniques based on strong stubborn sets have recently shown their potential for SAS+ planning as heuristic search. Strong stubborn sets exploit operator independency to safely prune the search space. Like SAS+ planning, fully observable nondeterministic (FOND) planning faces the state explosion problem. However, it is unclear how stubborn set techniques carry over to the nondeterministic setting. In this paper, we introduce stubborn set pruning to FOND planning. We lift the notion of strong stubborn sets and introduce the conceptually more powerful notion of weak stubborn sets to FOND planning. Our experimental analysis shows that weak stubborn sets are beneficial to an LAO* search, and in particular show favorable performance when combined with symmetries and active operator pruning.

We transfer the notion of structural symmetries to lifted planning task representations, based on a generalizing concept of abstract structures we use to model planning tasks. We show that symmetries are preserved by common grounding methods and shed some light on the relation to previous symmetry concepts. An analysis of common planning benchmarks reveals that symmetries occur in the lifted representation of many domains. Our concept prepares the ground for exploiting symmetries beyond their current scope, such as for faster grounding and mutex generation, as well as for state space transformations and state space reductions.

Symmetry-based state space pruning techniques have proved to greatly improve heuristic search based classical planners. Similarly, abstraction heuristics in general and pattern databases in particular are key ingredients of such planners. However, only little work has dealt with how the abstraction heuristics behave under symmetries. In this work, we investigate the symmetry properties of the popular canonical pattern databases heuristic. Exploiting structural symmetries, we strengthen the canonical pattern databases by adding symmetric pattern databases, making the resulting heuristic invariant under structural symmetry, thus making it especially attractive for symmetry-based pruning search methods. Further, we prove that this heuristic is at least as informative as using symmetric lookups over the original heuristic. An experimental evaluation confirms these theoretical results.

Symmetry-based state space pruning techniques have proved to greatly improve heuristic search based classical planners. Similarly, abstraction heuristics in general and pattern databases in particular are key ingredients of such planners. However, only little work has dealt with how the abstraction heuristics behave under symmetries. In this work, we investigate the symmetry properties of the popular canonical pattern databases heuristic. Exploiting structural symmetries, we strengthen the canonical pattern databases by adding symmetric pattern databases, making the resulting heuristic invariant under structural symmetry, thus making it especially attractive for symmetry-based pruning search methods. Further, we prove that this heuristic is at least as informative as using symmetric lookups over the original heuristic. An experimental evaluation confirms these theoretical results.

In domain-independent planning, dependencies of operators and variables often prevent the effective application of planning techniques that rely on "loosely coupled" problems (like factored planning or partial order reduction). In this paper, we propose a generic approach for factorizing a classical planning problem into an equivalent problem with fewer operator and variable dependencies. Our approach is based on variable factorization, which can be reduced to the well-studied problem of graph factorization. While the state spaces of the original and the factorized problems are isomorphic, the factorization offers the potential to exponentially reduce the complexity of planning techniques like factored planning and partial order reduction.

Hybrid systems represent an important and powerful formalism for modeling real-world applications such as embedded systems. A verification tool like SpaceEx is based on the exploration of a symbolic search space (the region space). As a verification tool, it is typically optimized towards proving the absence of errors. In some settings, e.g., when the verification tool is employed in a feedback-directed design cycle, one would like to have the option to call a version that is optimized towards finding an error trajectory in the region space. A recent approach in this direction is based on guided search. Guided search relies on a cost function that indicates which states are promising to be explored, and preferably explores more promising states first. In this paper, we propose an abstraction-based cost function based on coarse-grained space abstractions for guiding the reachability analysis. For this purpose, a suitable abstraction technique that exploits the flexible granularity of modern reachability analysis algorithms is introduced. The new cost function is an effective extension of pattern database approaches that have been successfully applied in other areas. The approach has been implemented in the SpaceEx model checker. The evaluation shows its practical potential.

Recent work has introduced fork-decoupled search, addressing classical planning problems where a single center component provides preconditions for several leaf components. Given a fixed center path π^C, the leaf moves compliant with π^C can then be scheduled independently for each leaf. Fork-decoupled search thus searches over center paths only, maintaining the compliant paths for each leaf separately. This can yield dramatic benefits. It is empirically complementary to partial order reduction via strong stubborn sets, in that each method yields its strongest reductions in different benchmarks. Here we show that the two methods can be combined, in the form of strong stubborn sets for fork-decoupled search. This can yield exponential advantages relative to both methods. Empirically, the combination reliably inherits the best of its components, and often outperforms both.

Symmetry reduction has significantly contributed to the success of classical planning as heuristic search. However, it is an open question if symmetry reduction techniques can be lifted to fully observable nondeterministic (FOND) planning. We generalize the concepts of structural symmetries and symmetry reduction to FOND planning and specifically to the LAO* algorithm. Our base implementation of LAO* in the Fast Downward planner is competitive with the LAO*-based FOND planner myND. Our experiments further show that symmetry reduction can yield strong performance gains compared to our base implementation of LAO*.

The sleep sets technique is a path-dependent pruning method for state space search. In the past, the combination of sleep sets with graph search algorithms that perform duplicate elimination has often shown to be error-prone. In this paper, we provide the theoretical basis for the integration of sleep sets with common search algorithms in AI that perform duplicate elimination. Specifically, we investigate approaches to safely integrate sleep sets with optimal (best-first) search algorithms. Based on this theory, we provide an initial step towards integrating sleep sets within A* and additional state pruning techniques like strong stubborn sets. Our experiments show slight, yet consistent improvements on the number of generated search nodes across a large number of standard domains from the international planning competitions.

The merge-and-shrink framework provides a general basis for the computation of abstraction heuristics for factored transition systems. Recent experimental and theoretical research demonstrated the utility of non-linear merge strategies, which have not been studied in depth. We experimentally analyze the quality of state-of-the-art merge strategies by comparing them to random strategies and with respect to tie-breaking, showing that there is considerable room for improvement. We finally describe a new merge strategy that experimentally outperforms the current state of the art.

Directed model checking is a well-established approach for detecting error states in concurrent systems. A popular variant to find shortest error traces is to apply the A* search algorithm with distance heuristics that never overestimate the real error distance. An important class of such distance heuristics is the class of pattern database heuristics. Pattern database heuristics are built on abstractions of the system under consideration. In this paper, we propose downward pattern refinement, a systematic approach for the construction of pattern database heuristics for concurrent systems of timed automata. First, we propose a general framework for pattern databases in the context of timed automata and show that desirable theoretical properties hold for the resulting pattern database. Afterward, we formally define a concept to measure the accuracy of abstractions. Based on this concept, we propose an algorithm for computing succinct abstractions that are still accurate to produce informed pattern databases. We evaluate our approach on large and complex industrial problems. The experiments show the practical potential of the resulting pattern database heuristic.

Symmetries provide the basis for well-established approaches to tackle the state explosion problem in state space search and in AI planning. However, although by now there are various symmetry-based techniques available, these techniques have not yet been empirically evaluated and compared to each other in a common setting. In particular, it is unclear which of them should be preferably applied, and whether there are techniques with stronger performance than others. In this paper, we shed light on this issue by providing an empirical case study. We combine and evaluate several symmetry-based techniques for cost-optimal planning as heuristic search. For our evaluation, we use state-of-the-art abstraction heuristics on a large set of benchmarks from the international planning competitions.

Directed model checking uses distance functions to guide the state space exploration to efficiently find short error paths. Distance functions based on delete-relaxation have successfully been used for, e.g., model checking timed automata. However, such distance functions have not been investigated for formalisms with rich expression languages as provided by PROMELA. We present a generalization of delete-relaxation-based distance functions to a subclass of PROMELA. We have evaluated the resulting search behavior on a large number of models from the BEEM database within the HSF-SPIN model checker. Our experiments show significantly better guidance compared to the previously best distance function available in HSF-SPIN.

Pruning techniques based on partial order reduction and symmetry elimination have recently found increasing attention for optimal planning. Although these techniques appear to be rather different, they base their pruning decisions on similar ideas from a high level perspective. In this paper, we propose safe integrations of partial order reduction and symmetry elimination for cost-optimal classical planning. We show that previously proposed symmetry-based search algorithms can safely be applied with strong stubborn sets. In addition, we derive the notion of symmetrical strong stubborn sets as a more tightly integrated concept. Our experiments show the potential of our approaches.

We propose the application of variable neighborhood search to address the problem of local optima during the hill-climbing procedure of iPDB.

Planning in hybrid domains poses a special challenge due to the involved mixed discrete-continuous dynamics. A recent solving approach for such domains is based on applying model checking techniques on a translation of PDDL+ planning problems to hybrid automata. However, the proposed translation is limited because must behavior is only over-approximated, and hence, processes and events are not reflected exactly. In this paper, we present the theoretical foundation of an exact PDDL+ translation. We propose a schema to convert a hybrid automaton with must transitions into an equivalent hybrid automaton featuring only may transitions.

The stubborn set method is a state-space reduction technique, originally introduced in model checking and then transfered to classical planning. It was shown that stubborn sets significantly improve the performance of optimal deterministic planners by considering only a subset of applicable operators in a state. Fully observable nondeterministic planning (FOND) extends the formalism of classical planning by nondeterministic operators. We show that stubborn sets are also beneficial for FOND problems. We introduce nondeterministic stubborn sets, stubborn sets which preserve strong cyclic plans. We follow two approaches: Fast Incremental Planning with stubborn sets from classical planning and LAO* search with nondeterministic stubborn sets. Our experiments show that both approaches increase coverage and decrease node generations when compared to their respective baselines.

Heuristic search is a state-of-the-art approach to classical planning. Several heuristic families were developed over the years to automatically estimate goal distance information from problem descriptions. Orthogonally to the development of better heuristics, recent years have seen an increasing interest in symmetry-based state space pruning techniques that aim at reducing the search effort. However, little work has dealt with how the heuristics behave under symmetries. We investigate the symmetry properties of existing heuristics and reveal that many of them are invariant under symmetries.

Merge-and-shrink heuristics crucially rely on effective reduction techniques, such as bisimulation-based shrinking, to avoid the combinatorial explosion of abstractions. We propose the concept of factored symmetries for merge-and-shrink abstractions based on the established concept of symmetry reduction for state-space search. We investigate under which conditions factored symmetry reduction yields perfect heuristics and discuss the relationship to bisimulation. We also devise practical merging strategies based on this concept and experimentally validate their utility.

Pruning techniques have recently been shown to speed up search algorithms by reducing the branching factor of large search spaces. One such technique is sleep sets, which were originally introduced as a pruning technique for model checking, and which have recently been investigated on a theoretical level for planning. In this paper, we propose a generalization of sleep sets and prove its correctness. While the original sleep sets were based on the commutativity of operators, generalized sleep sets are based on a more general notion of operator sequence redundancy. As a result, our approach dominates the original sleep sets variant in terms of pruning power. On a practical level, our experimental evaluation shows the potential of sleep sets and their generalizations on a large and common set of planning benchmarks.

Bounded intention planning provides a pruning technique for optimal planning that has been proposed several years ago. In addition, partial order reduction techniques based on stubborn sets have recently been investigated for this purpose. In this paper, we revisit bounded intention planning in the view of stubborn sets.

Label reduction is a technique for simplifying families of labeled transition systems by dropping distinctions between certain transition labels. While label reduction is critical to the efficient computation of merge-and-shrink heuristics, current theory only permits reducing labels in a limited number of cases. We generalize this theory so that labels can be reduced in every intermediate abstraction of a merge-and-shrink tree. This is particularly important for efficiently computing merge-and-shrink abstractions based on non-linear merge strategies. As a case study, we implement a non-linear merge strategy based on the original work on merge-and-shrink heuristics in model checking by Dräger et al.

Planning in hybrid domains is an important and challenging task, and various planning algorithms have been proposed in the last years. From an abstract point of view, hybrid planning domains are based on hybrid automata, which have been studied intensively in the model checking community. In particular, powerful model checking algorithms and tools have emerged for this formalism. However, despite the quest for more scalable planning approaches, model checking algorithms have not been applied to planning in hybrid domains so far. In this paper, we make a first step in bridging the gap between these two worlds. We provide a formal translation scheme from PDDL+ to the standard formalism of hybrid automata, as a solid basis for using hybrid system model-checking tools for dealing with hybrid planning domains. As a case study, we use the SpaceEx model checker, showing how we can address PDDL+ domains that are out of the scope of state-of-the-art planners.

Planning-based methods to guide switched hybrid systems from an initial state into a desired goal region opens an interesting field for control. The idea of the Domain Predictive Control (DPC) approach is to generate input signals affecting both the numerical states and the modes of the system by stringing together atomic actions to a logically consistent plan. However, the existing DPC approach is restricted in the sense that a discrete and pre-defined input signal is required for each action. In this paper, we extend the approach to deal with symbolic states. This allows for the propagation of reachable regions of the state space emerging from actions with inputs that can be arbitrarily chosen within specified input bounds. This symbolic extension enables the applicability of DPC to systems with bounded inputs sets and increases its robustness due to the implicitly reduced search space. Moreover, precise numeric goal states instead of goal regions become reachable.

A crucial problem in GUI testing is the identification of accurate event sequences that encode corresponding user interactions with the GUI. Ultimately, event sequences should be both feasible (i.e., executable on the GUI) and relevant (i.e., cover as much of the code as possible). So far, most work on GUI testing focused on approaches to generate feasible event sequences. In addition, based on event dependency analyses, a recently proposed static analysis approach systematically aims at selecting both relevant and feasible event sequences. However, statically analysing event dependencies can cause the generation of a huge number of event sequences, leading to unmanageable GUI test suites that are not executable within reasonable time.

In this paper we propose a refined static analysis approach based on program slicing. On the theoretical side, our approach identifies and eliminates redundant event sequences in GUI test suites. Redundant event sequences have the property that they are guaranteed to not affect the test effectiveness. On the practical side, we have implemented a slicing-based test suite reduction algorithm that approximatively identifies redundant event sequences. Our experiments on six open source GUI applications show that our reduction algorithm significantly reduces the size of GUI test suites. As a result, the overall execution time could significantly be reduced without losing test effectiveness.

Strong stubborn sets have recently been analyzed and successfully applied as a pruning technique for planning as heuristic search. Strong stubborn sets are defined declaratively as constraints over operator sets. We show how these constraints can be relaxed to offer more freedom in choosing stubborn sets while maintaining the correctness and optimality of the approach. In general, many operator sets satisfy the definition of stubborn sets. We study different strategies for selecting among these possibilities and show that existing approaches can be considerably improved by rather simple strategies, eliminating most of the overhead of the previous state of the art.

A general and important problem of search-based planning techniques is the state explosion problem, which is usually tackled with approaches to reduce the branching factor of the planning task. Such approaches often implicitly exploit the observation that the number of available operators is higher than the number of operators that are actually needed to find a plan. In this paper, we propose a simple, but general under-approximation refinement framework for satisficing planning that explicitly exploits this observation. Our approach iteratively searches for plans with operator subsets, which are refined if necessary by adding operators that appear to be needed. Our evaluation shows that even a straight-forward instantiation of this framework yields a competitive planner that often finds plans with small operator sets.

Label reduction is a technique for simplifying families of labeled transition systems by dropping distinctions between certain transition labels. While label reduction is critical to the efficient computation of merge-and-shrink heuristics, current theory only permits reducing labels in a limited number of cases. We generalize this theory so that labels can be reduced in every intermediate abstraction of a merge-and-shrink tree. This is particularly important for efficiently computing merge-and-shrink abstractions based on non-linear merge strategies. As a case study, we implement a non-linear merge strategy based on the original work on merge-and-shrink heuristics in model checking by Dräger et al.

Hybrid systems represent an important and powerful formalism for modeling real-world applications such as embedded systems. A verification tool like SpaceEx is based on the exploration of a symbolic search space (the region space). As a verification tool, it is typically optimized towards proving the absence of errors. In some settings, e.g., when the verification tool is employed in a feedback-directed design cycle, one would like to have the option to call a version that is optimized towards finding an error path in the region space. A recent approach in this direction is based on guided search. Guided search relies on a cost function that indicates which states are promising to be explored, and preferably explores more promising states first. In this paper, an abstraction-based cost function based on pattern databases for guiding the reachability analysis is proposed. For this purpose, a suitable abstraction technique that exploits the flexible granularity of modern reachability analysis algorithms is introduced. The new cost function is an effective extension of pattern database approaches that have been successfully applied in other areas. The approach has been implemented in the SpaceEx model checker. The evaluation shows its practical potential.

In the last years, pruning techniques based on partial order reduction have found increasing attention in the planning community. One recent result is that the expansion core method is a special case of the strong stubborn sets method proposed in model checking. However, it is still an open question if there exist efficiently computable strong stubborn sets with strictly higher pruning power than expansion core. In this paper, we prove that the pruning power of strong stubborn sets is strictly higher than the pruning power of expansion core even for a straight-forward instantiation of strong stubborn sets. This instantiation is as efficiently computable as expansion core. Hence, our theoretical results suggest that strong stubborn sets should be preferred to expansion core. Our empirical evaluation on all optimal benchmarks from the international planning competitions up to 2011 supports the theoretical results.

Mcta is a directed model checking tool for concurrent systems of timed automata. This paper reviews Mcta and its new developments from an implementation point of view. The new developments include both heuristics and search techniques that define the state of the art in directed model checking. In particular, Mcta features the powerful class of pattern database heuristics for efficiently finding shortest possible error traces. Furthermore, Mcta offers new search techniques based on multi-queue search algorithms. Our evaluation demonstrates that Mcta is able to significantly outperform previous versions of Mcta as well as related state-of-the-art tools like Uppaal and Uppaal/Dmc.

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.

A recent technique used in falsification methods for hybrid systems relies on distance-based heuristics for guiding the search towards a goal state. The question is whether the technique can be carried over to reachability analyses that use regions as their basic data structure. In this paper, we introduce a box-based distance measure between regions. We present an algorithm that, given two regions, efficiently computes the box-based distance between them. We have implemented the algorithm in SpaceEx and use it for guiding the region-based reachability analysis of SpaceEx. We illustrate the practical potential of our approach in a case study for the navigation benchmark.

Partial order reduction is a state space pruning approach that has been originally introduced in computer aided verification. Recently, various partial order reduction techniques have also been proposed for planning. Despite very similar underlying ideas, the relevant literature from computer aided verification has hardly been analyzed in the planning area so far, and it is unclear how these techniques are formally related. We provide an analysis of existing partial order reduction techniques and their relationships. We show that recently proposed approaches in planning are instances of general partial order reduction approaches from computer aided verification. Our analysis reveals a hierarchy of dominance relationships and shows that there is still room for improvement for partial order reduction techniques in planning. Overall, we provide a first step towards a better understanding and a unifying theory of partial order reduction techniques from different areas.

Directed model checking is a well-established technique for detecting error states in concurrent systems efficiently. As error traces are important for debugging purposes, it is preferable to find as short error traces as possible. A wide spread method to find provably shortest error traces is to apply the A* search algorithm with distance heuristics that never overestimate the real error distance. An important class of such distance estimators is the class of pattern database heuristics, which are built on abstractions of the system under consideration. In this paper, we propose a systematic approach for the construction of pattern database heuristics. We formally define a concept to measure the accuracy of abstractions. Based on this technique, we address the challenge of finding abstractions that are succinct on the one hand, and accurate to produce informed pattern databases on the other hand. We evaluate our approach on large and complex industrial problems. The experiments show that the resulting distance heuristic impressively advances the state of the art.

Directed model checking is a well-established technique to efficiently tackle the state explosion problem when the aim is to find error states in concurrent systems. Although directed model checking has proved to be very successful in the past, additional search techniques provide much potential to efficiently handle larger and larger systems. In this work, we propose a novel technique for traversing the state space based on interference contexts. The basic idea is to preferably explore transitions that interfere with previously applied transitions, whereas other transitions are deferred accordingly. Our approach is orthogonal to the model checking process and can be applied to a wide range of search methods. We have implemented our method and empirically evaluated its potential on a range of non-trivial case studies. Compared to standard model checking techniques, we are able to detect subtle bugs with shorter error traces, consuming less memory and time.

Directed model checking is a well-established technique to tackle the state explosion problem when the aim is to find error states in large systems. In this approach, the state space traversal is guided through a function that estimates the distance to nearest error states. States with lower estimates are preferably expanded during the search. Obviously, the challenge is to develop distance functions that are efficiently computable on the one hand and as informative as possible on the other hand. In this paper, we introduce the causal graph structure to the context of directed model checking. Based on causal graph analysis, we first adapt a distance estimation function from AI planning to directed model checking. Furthermore, we investigate an abstraction that is guaranteed to preserve error states. The experimental evaluation shows the practical potential of these techniques.

Directed model checking is a well-established technique that is tailored to fast detection of system states that violate a given safety property. This is achieved by influencing the order in which states are explored during the state space traversal. The order is typically determined by an abstract distance function that estimates a state's distance to a nearest error state. In this paper, we propose a general enhancement to directed model checking based on the evaluation of state transitions. We present a schema, parametrized by an abstract distance function, to evaluate transitions and propose a new method for the state space traversal. Our framework can be applied automatically to a wide range of abstract distance functions. The empirical evaluation impressively shows its practical potential. Apparently, the new method identifies a sweet spot in the trade-off between scalability (memory consumption) and short error traces.

Planning as heuristic search is a powerful approach to solving domain independent planning problems. In recent years, various successful heuristics and planners like FF, LPG, Fast Downward or SGPlan have been proposed in this context. However, as heuristics only estimate the distance to goal states, a general problem of heuristic search is the existence of plateaus in the search space topology which can cause the search process to degenerate. Additional techniques like helpful actions or preferred operators that evaluate the "usefulness" of actions are often successful strategies to support the search in such situations.

In this paper, we introduce a general method to evaluate the usefulness of actions. We propose a technique to enhance heuristic search by identifying "useless" actions that are not needed to find optimal plans. In contrast to helpful actions or preferred operators that are specific to the FF and Causal Graph heuristic, respectively, our method can be combined with arbitrary heuristics. We show that this technique often yields significant performance improvements.

It is probably very hard to develop a new model checker that is faster than Uppaal for verifying correct timed automata. In fact, our tool Mcta does not even try to compete with Uppaal in this (i.e., Uppaal's) arena. Instead, Mcta is geared towards analyzing incorrect specifications of timed automata. It returns (shorter) error traces faster.

Planning as satisfiability is a powerful approach to solving domain independent planning problems. In this paper, we consider a relaxed semantics for plans with parallel operator application based on E-step semantics. Operators can be applied in parallel if there is at least one ordering in which they can be sequentially executed. Under certain conditions, we allow them to be executed simultaneously in a state s even if not all of them are applicable in s. In this case, we guarantee that they are enabled by other operators that are applied at the same time point. We formalize the semantics of parallel plans in this setting, and propose an effective translation for STRIPS problems into the propositional logic. We finally show that this relaxed semantics yields an approach to classical planning that is sometimes much more efficient than the existing SAT-based planners.