Privacy Verification in POMDPs via Barrier Certificates
It addresses privacy verification for cyber-physical systems, but the approach is incremental, extending barrier certificate techniques to opacity-based privacy in POMDPs.
The paper proposes a method for privacy verification in cyber-physical systems modeled as MDPs and POMDPs using barrier certificates, demonstrating computational implementation via semi-definite and sum-of-squares programs, with application to an inventory management system.
Privacy is an increasing concern in cyber-physical systems that operates over a shared network. In this paper, we propose a method for privacy verification of cyber- physical systems modeled by Markov decision processes (MDPs) and partially-observable Markov decision processes (POMDPs) based on barrier certificates. To this end, we consider an opacity-based notion of privacy, which is characterized by the beliefs in system states. We show that the belief update equations can be represented as discrete-time switched systems, for which we propose a set of conditions for privacy verification in terms of barrier certificates. We further demonstrate that, for MDPs and for POMDPs, privacy verification can be computationally implemented by solving a set of semi-definite programs and sum-of-squares programs, respectively. The method is illustrated by an application to privacy verification of an inventory management system.