Bounded Synthesis and Reinforcement Learning of Supervisors for Stochastic Discrete Event Systems with LTL Specifications

TL;DR

This paper presents a method combining bounded synthesis and reinforcement learning to design supervisors for stochastic discrete event systems that satisfy linear temporal logic specifications, maximizing satisfaction probability.

Contribution

It introduces a novel approach that reduces supervisor synthesis to safety conditions and employs model-free reinforcement learning for unknown systems.

Findings

Maximized satisfaction probability of supervisors.

Effective learning of winning regions in unknown systems.

Validated approach through simulation results.

Abstract

In this paper, we consider supervisory control of stochastic discrete event systems (SDESs) under linear temporal logic specifications. Applying the bounded synthesis, we reduce the supervisor synthesis into a problem of satisfying a safety condition. First, we consider a synthesis problem of a directed controller using the safety condition. We assign a negative reward to the unsafe states and introduce an expected return with a state-dependent discount factor. We compute a winning region and a directed controller with the maximum satisfaction probability using a dynamic programming method, where the expected return is used as a value function. Next, we construct a permissive supervisor via the optimal value function. We show that the supervisor accomplishes the maximum satisfaction probability and maximizes the reachable set within the winning region. Finally, for an unknown SDES, we propose a two-stage model-free reinforcement learning method for efficient learning of the winning region and the directed controllers with the maximum satisfaction probability. We also demonstrate the effectiveness of the proposed method by simulation.