main.tex

\documentclass{llncs}

\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{xspace}
\pagestyle{plain}
\usepackage{multirow}
\usepackage{algorithm,algpseudocode}
\usepackage{caption}
\usepackage{subcaption}
\captionsetup{compatibility=false}
\usepackage{wrapfig}
\usepackage{mathtools}
\usepackage{tikz}
\usetikzlibrary{arrows,calc}
\usepackage{url}
\usepackage{times}
\usepackage[symbol]{footmisc}
\renewcommand{\thefootnote}{\fnsymbol{footnote}}

\algtext*{EndWhile}% Remove "end while" text
\algtext*{EndIf}% Remove "end if" text
\algtext*{EndFor}% Remove "end if" text

\input{macros}

\newif\ifpublic
\publictrue

\title{Model Checking Differentially Private Properties}
\ifpublic
\author{
Depeng Liu\inst{1,2}
\and
Bow-Yaw Wang\inst{3}
\and
Lijun Zhang\inst{1,2,4}}
\institute{
State Key Laboratory of Computer Science, Institute of Software,
Chinese Academy of Sciences
\footnotemark[1]
\and
University of Chinese Academy of Sciences
\footnotemark[1]
\and
Institute of Information Science, Academia Sinica
\footnotemark[2]
\and
Institute of Intelligent Software, Guangzhou
\footnotemark[1]
}
\else
\author{Author}
\institute{Institute}
\fi

\begin{document}

\maketitle

\footnotetext[1]{Partially supported by 
the National Natural Science Foundation of China (Grants No.\ 61532019, 61761136011, 61472473).}
\footnotetext[2]{Partially supported by the Academia
Sinica Thematic Project: Socially Accountable Privacy Framework for
Secondary Data Usage.}

\begin{abstract}
  We introduce the branching time temporal logic $\dpCTLstar$ for
  specifying differential privacy. Several differentially private
  mechanisms are formalized as Markov chains or Markov decision
  processes. Using our formal models, subtle privacy conditions
  are specified by $\dpCTLstar$. In order to verify privacy properties
  automatically, model checking problems are investigated.  We
  give a model checking algorithm for Markov chains. Model checking
  $\dpCTLstar$ properties on Markov decision processes however is
  shown to be undecidable.
\end{abstract}

\section{Introduction}
\label{section:introduction}
\input{introduction}

\noindent
\emph{Organization of the paper.}
Preliminaries are given in Section~\ref{section:preliminaries}.
In Section~\ref{section:examples} we discuss how offline differentially private mechanisms are modeled as Markov chains.
The logic $\dpCTLstar$ and its syntax are presented in Section~\ref{section:dpCTL}. The semantics over Markov chains and its model checking algorithm are given in Section~\ref{section:semantics}.
Section~\ref{section:specifying-properties} discusses differential privacy properties using $\dpCTLstar$.
More examples of online differentially private mechanisms as Markov decision processes are given in Section~\ref{section:mdp}.
The semantics over Markov decision processes and undecidability of model checking is given in Section~\ref{section:semantics-mdp}.
Finally,
Section~\ref{section:conclusions} concludes our presentation.

\section{Preliminaries}
\label{section:preliminaries}
\input{preliminaries}

\section{Differentially Private Mechanisms as Markov Chains}
\label{section:examples}
\input{examples}

\subsection{Subsampling Majority}
\label{subsection:subsampling}

\input{subsampling}

\section{The Logic $\dpCTLstar$}
\label{section:dpCTL}
\input{dpCTL}

\subsection{Syntax}
\label{subsection:syntax}
\input{syntax}

\section{$\dpCTLstar$ for Markov Chains}
\label{section:semantics}
\input{semantics}

\section{Specifying Properties in $\dpCTLstar$}
\label{section:specifying-properties}
\input{specifications}

\section{Differentially Private Mechanisms as Markov Decision Processes}
\label{section:mdp}
\input{mdp}

\subsection{Above Threshold Mechanism}
\label{subsec:threshold}
\input{above-threshold}

\section{$\dpCTLstar$ for Markov Decision Processes}
\label{section:semantics-mdp}
\input{semantics-mdp}

%\section{Model Checking Algorithms}
%\label{section:model-checking-algorithms}
%\input{algorithms}


%\subsection{MDPs for Stream Processing}
%\label{section:applications}
%\input{applications}

\section{Conclusions}
\label{section:conclusions}
We have introduced $\dpCTLstar$ to reason about properties in differential privacy, and investigated its model checking problems. For Markov chains, the model checking problem has the same complexity as for $\PCTLstar$. The general MDP model checking problem however is undecidable.
We have discussed some decidable special cases and a sufficient yet efficient condition to check differentially private subformulae.
An interesting future work is to identify more
decidable subclasses and sufficient conditions.
As an example, consider the extended $\dpCTLstar$ formula $\bigwedge_{k \in \bbfZ^{\geq 0}}
\dpriv{\epsilon}{\delta} (\X^k  \top)$. For the case $\epsilon=\delta=0$, it reduces to a language equivalence problem for probabilistic automata. It is interesting to characterize other cases as well.
Another interesting line of further works is to consider continuous perturbation (such as Laplace distribution used in \cite{DR:14:AFDP}). We would need Markov models with continuous state space.


\bibliographystyle{splncs03}
\bibliography{refs}

\newpage
\appendix

\section{Proof of Theorem~\ref{theorem:mdp-model-checking}}
\input{proof}

\end{document}