Optimal Synthesis for Stochastic Systems with Information Security Preservation Under Temporal Logic Constraints

In this paper, we present a method for synthesizing optimal policies for stochastic systems under high-level mission specifications while maintaining information security. The stochastic systems are modeled as probabilistic labeling Markov decision processes (PLMDPs), and the high-level mission specifications are represented by linear temporal logic (LTL) formulas, which must be satisfied repeatedly, infinitely often. Meanwhile, an intruder is modeled as an observer who knows the exact structure of the system and passively monitors its behavior, aiming to infer the high-level mission specifications. Our objective is to synthesize an optimal policy that minimizes the mean payoff cost while preventing the intruder from definitively determining the given mission specifications. We begin by extending the PLMDP model by incorporating an observation function and the corresponding probability function, and we introduce the concept of LTL opacity for stochastic systems. Next, by proposing a new structure called the synchronous accepting maximally end component, we identify the subset of the accepting end components that satisfy the LTL opacity requirement. Finally, we develop a modified linear program with information security constraints to synthesize an optimal policy that ensures both formal correctness and LTL opacity.