Representing and exploring large and even infinite state spaces 
is a challenge for many subareas of computer science in
general and for Artificial Intelligence (AI) in particular. 
A possibly weighted state space graph is to be explored by 
successively applying state expansions starting from the initial
state to eventually reach a desired goal state. 

This thesis studies the theoretical foundations of guided
exploration algorithms and their impact in the following
application areas.

Puzzle Solving: Domain-dependent puzzle solving searches for
  optimal solution paths in solitaire games. Challenges are real-world
  problems like Rubik's Cube or the set of $(n^2-1)$-Puzzles, and
  computer games like Sokoban or Atomix. The thesis takes Atomix as a
  selected case study for which it refines storage structures to
  enhance duplicate detection.
Action Planning: In action planning, domains and problem instances
  are specified in a general description language (PDDL) with
  parameterized operators. Starting from propositional planning, in
  which each state is represented as a subset of atoms, planning
  problems have been extended with action duration, resource
  variables, and objective functions. The thesis proposes a successful
  metric and temporal heuristic search framework planner featuring a
  versatile static analyzer and different heuristic estimates.
Theorem Proving: Automated deduction considers object logics
  like first and higher-order logic to specify axioms and theorems,
  searching for according proofs. Many current theorem provers face
  infinite spaces of all possible proof states. The thesis proposes
  functional heuristic search to generate proofs fully automatically.
Hardware Verification: Hardware designs may contain subtle
  errors. These are to be found with automated verification techniques
  that validate if an implemented system is conformant to its
  specification. The thesis adds symbolic heuristic search to the
  algorithmic portfolio of an existing $\mu$-calculus model checker
  based on an estimate that propagates the error description through
  the circuit.
Software Verification: Asynchronous software systems like
  communication protocols or multi-threaded Java programs require
  involved concurrency maintenance e.g. to avoid deadlocks.  Automated
  validation simulates all possible executions traces and yields short
  witnesses in case of a failure.  This thesis contributes
  explicit-state directed model checking and shows how the control of
  flow can be inferred by supervised learning by example.
Route planning: Traffic information systems search for
  lowest-cost paths in explicit maps. If the map is provided on
  CD/DVD, it is likely too large to be kept in main memory. The thesis
  proposes a complete and optimal localized heuristic search
  exploration scheme that explicitly pages portions of the graph
  according to the spatial structure of the map. It further considers
  route planning and map inference aspects for a set of global
  positioning traces.

The central problem in all research areas is overcoming the state
(space) explosion problem: many puzzles are known to be at least
NP-hard, propositional planning is PSPACE-complete, while numeric
planning and automated theorem proving are both undecidable. Last but
not least, the state space size in concurrent systems grows often
exponentially in the number of state variables.

To cope with this intrinsic hardness, all contributed algorithms apply
heuristic search to focus the search process, where the estimates are
found by exploring abstracted state spaces.

Among other techniques to reduce the number of nodes to be looked at,
the thesis studies state compaction, symbolic representation, pattern
databases, and partial order reduction.  State compaction stores a
small signature of the state, symbolic representation assigns and
maintains characteristic formulae for sets of states, pre-computed
dictionaries serve refined estimates for the overall search engines,
and partial order reduction exploits the commutativity of concurrent
actions.

Beside theoretical work we provide implementations of heuristic search
algorithms in practical systems, including a commercial car navigation
system, an awarded action planner, an automated higher-order theorem
prover, a generic puzzle solver, a programming-by-example tool, a
symbolic and an explicit-state model checker.