Privacy Verification in POMDPs via Barrier Certificates

TL;DR

This paper introduces a novel barrier certificate-based method for verifying privacy in cyber-physical systems modeled by POMDPs and MDPs, using belief state analysis and semi-definite programming.

Contribution

It develops a new approach for privacy verification in POMDPs and MDPs using barrier certificates and belief state representations, with computational methods based on semi-definite and sum-of-squares programming.

Findings

Method effectively verifies privacy in cyber-physical systems.

Belief update equations can be represented as switched systems.

Application demonstrated on inventory management system.

Abstract

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.