Control Synthesis in Partially Observable Environments for Complex Perception-Related Objectives
This work addresses control synthesis for autonomous systems under partial observability, representing an incremental advance in formal methods for perception tasks.
The paper tackles the problem of synthesizing optimal policies for complex perception-related objectives in partially observable environments, introducing a new logic (sc-iLTL) and a Monte Carlo Tree Search method that converges to optimal policies, with a drone-probing case study demonstrating applicability.
Perception-related tasks often arise in autonomous systems operating under partial observability. This work studies the problem of synthesizing optimal policies for complex perception-related objectives in environments modeled by partially observable Markov decision processes. To formally specify such objectives, we introduce \emph{co-safe linear inequality temporal logic} (sc-iLTL), which can define complex tasks that are formed by the logical concatenation of atomic propositions as linear inequalities on the belief space of the POMDPs. Our solution to the control synthesis problem is to transform the \mbox{sc-iLTL} objectives into reachability objectives by constructing the product of the belief MDP and a deterministic finite automaton built from the sc-iLTL objective. To overcome the scalability challenge due to the product, we introduce a Monte Carlo Tree Search (MCTS) method that converges in probability to the optimal policy. Finally, a drone-probing case study demonstrates the applicability of our method.