Synthesis of Partially Observed Jump-Diffusion Systems via Control Barrier Functions

TL;DR

This paper develops a discretization-free method for synthesizing control policies for partially observed jump-diffusion systems to satisfy complex specifications, without needing estimation accuracy knowledge.

Contribution

It introduces a novel approach using control barrier functions for formal synthesis of control policies in partially observed jump-diffusion systems, bypassing discretization and estimation accuracy requirements.

Findings

Synthesized a control policy for a jet engine example.

Achieved a lower bound on the probability of satisfying specifications.

Demonstrated effectiveness of the approach in complex scenarios.

Abstract

In this paper, we study formal synthesis of control policies for partially observed jump-diffusion systems against complex logic specifications. Given a state estimator, we utilize a discretization-free approach for formal synthesis of control policies by using a notation of control barrier functions without requiring any knowledge of the estimation accuracy. Our goal is to synthesize an offline control policy providing (potentially maximizing) a lower bound on the probability that the trajectories of the partially observed jump-diffusion system satisfy some complex specifications expressed by deterministic finite automata. Finally, we illustrate the effectiveness of the proposed results by synthesizing a policy for a jet engine example.