Technical Summary: Scaling Observation-aware Planning in Uncertain Domains

Problem Definition

The paper addresses the Optimal Observability Problem (OOP) within the context of Partially Observable Markov Decision Processes (POMDPs). The core engineering challenge is determining which sensing capabilities (observations) to deploy on an agent in uncertain domains to ensure a task is achievable without incurring prohibitive hardware or processing costs.

Formally, given an underlying Markov Decision Process (MDP) $M$, a budget $B$, and a reward threshold $\tau$, the OOP asks whether there exists an observation function $obs$ (mapping states to a set of observations with cardinality $\le B$) such that the minimal expected reward of the resulting POMDP is $\le \tau$.

While the general OOP is undecidable, the paper focuses on two decidable fragments:

1. Sensor Selection Problem (SSP): A variant where observations are binary (on/off) for specific location sensors.
2. Positional Observability Problem (POP): A variant considering positional strategies (actions depend only on the current observation, not history).

Previous work by Konsta et al. [19] formalized these problems and reduced them to Typed Parametric Markov Chains (tpMCs), solving them via SMT-based parameter synthesis. However, this approach struggles to scale to larger instance sizes.

Methodology

The authors propose a two-pronged approach to scale the solution of OOP fragments:

1. Enhancements to SMT-Based Parameter Synthesis

Building on the tpMC reduction from [19], the authors refine the SMT encoding to improve solver performance (specifically using Z3):

• Native Boolean Encoding: Instead of using real-valued parameters restricted to $\{0,1\}$, the authors replace them with native Boolean variables. This leverages SAT propagation and reduces non-linear arithmetic overhead.
• Constraint Relaxations:
  • Budget Repairing: A two-stage "relax-and-repair" approach where the solver first finds a solution ignoring the budget constraint, then attempts to refine it to satisfy the budget.
  • Invariant Upper Bound: Replacing exact Bellman equations with inequalities ($v_s \ge \text{Bellman}(v_s)$). This seeks a conservative over-approximation of the expected reward, which is sufficient for feasibility checks where the threshold $\tau$ is not necessarily the optimal minimum.
• Assertion Ordering: Empirical testing revealed that the order of SMT assertions significantly impacts performance; the authors identified an optimal ordering that dominates other permutations.

2. Heuristic-Based Decomposition via POMDP Oracles

Recognizing that solving the full tpMC encoding for every candidate observation function is inefficient, the authors introduce a decomposition paradigm. Instead of solving the global optimization problem directly, they search the space of observation functions using "oracles" to evaluate candidates.

• Oracles: The paper utilizes two types of oracles to evaluate a candidate observation function:
  1. SMT Oracle: A simplified tpMC encoding where observation variables are fixed, reducing complexity.
  2. PMC Oracle: Integration with the Storm probabilistic model checker to evaluate expected rewards.
• Atomic Distinguishability Groups: The authors define equivalence relations between states based on their "optimal signatures" (the set of optimal actions in the underlying MDP). States with identical optimal signatures form atomic distinguishability groups.
• AG Algorithm (Heuristic Enumeration):
  • The algorithm partitions the set of atomic distinguishability groups into observation classes.
  • It employs a ranking heuristic based on equivalence scores (how many states in a class share a common optimal action) and strategy constraints (how many action probabilities can be fixed to 0 or 1).
  • The algorithm evaluates candidates in decreasing order of promise. If a candidate satisfies the threshold, it returns the solution; otherwise, it proceeds to the next.
  • This approach is sound and complete for specific topologies (Line, Maze, Grid) under certain budget conditions, though it is generally incomplete as it does not split atomic groups.

Key Contributions

1. Optimized SMT Encodings: The authors developed native Boolean encodings and invariant relaxations that improve the performance of the original parameter synthesis approach by approximately 3 orders of magnitude in runtime and allow for solving instances ~75 times larger in size.
2. Decomposition Paradigm: They introduced a new method for solving OOP instances by decomposing the problem into the enumeration of observation functions evaluated via oracles, rather than solving a monolithic SMT problem.
3. Heuristic Enumeration (AG Algorithm): A specific algorithm that leverages state equivalence and optimal action signatures to prioritize the search space. This method improves upon the enhanced SMT approach by 3 orders of magnitude in runtime and scales to instances 100 times larger.
4. Empirical Validation: Extensive benchmarks on standard models (Grid, Maze, Line) demonstrate that the proposed methods significantly outperform the baseline from [19] and the authors' own intermediate SMT enhancements.

Results

The paper presents experimental results comparing the original approach [19], the enhanced SMT approach (Section 3), and the heuristic decomposition approach (Section 5):

• Runtime: The AG algorithm reduces solving time by factors of $10^3$ compared to the enhanced SMT method. For example, a Grid instance (G(20)) that timed out or took ~30 seconds with SMT was solved in milliseconds by AG.
• Scalability:
  • SMT Enhancements: Solved instances with up to ~10,000 states (Line) and ~1,296 states (Grid) for deterministic strategies, compared to ~377 and ~96 respectively in the baseline.
  • AG Decomposition: Solved instances with up to 200,001 states (Line) and 160,801 states (Grid) for deterministic strategies.
• Randomized Strategies: The improvements are also significant for randomized strategies, though deterministic strategies generally yield larger scaling factors due to the effectiveness of Boolean encoding.

Significance and Claims

The paper claims that by combining symbolic (SMT) and sub-symbolic (heuristic decomposition/oracle-based) techniques, it is possible to scale the solution of decidable fragments of the Optimal Observability Problem to sizes previously considered intractable.

The authors emphasize that their work shifts the focus from solving the entire tpMC encoding to searching the space of observation functions intelligently. They state that their heuristic-based enumeration algorithm is sound and, for the specific topologies studied (Line, Maze, Grid), appears to be complete for budgets greater than or equal to the minimal positional budget.

The paper concludes modestly, noting that while the current results are significant, future work could further improve predictability via Z3 tactics, extend parameter synthesis tools, and apply Reinforcement Learning techniques initialized by the proposed heuristics. The authors do not claim to have solved the general undecidable OOP but have significantly advanced the state-of-the-art for its decidable fragments.