Computational methods for stochastic control with metric interval temporal logic specifications
It provides a theoretical framework and numerical method for stochastic control under real-time temporal logic constraints, addressing a gap in handling dense-time semantics.
This paper proposes a method for synthesizing optimal control policies for continuous-time stochastic systems to maximize the probability of satisfying metric interval temporal logic specifications, using a discrete approximation that converges to the optimal solution as discretization refines.
This paper studies an optimal control problem for continuous-time stochastic systems subject to reachability objectives specified in a subclass of metric interval temporal logic specifications, a temporal logic with real-time constraints. We propose a probabilistic method for synthesizing an optimal control policy that maximizes the probability of satisfying a specification based on a discrete approximation of the underlying stochastic system. First, we show that the original problem can be formulated as a stochastic optimal control problem in a state space augmented with finite memory and states of some clock variables. Second, we present a numerical method for computing an optimal policy with which the given specification is satisfied with the maximal probability in point-based semantics in the discrete approximation of the underlying system. We show that the policy obtained in the discrete approximation converges to the optimal one for satisfying the specification in the continuous or dense-time semantics as the discretization becomes finer in both state and time. Finally, we illustrate our approach with a robotic motion planning example.