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.