11institutetext:  Brno University of Technology, Brno, Czech Republic
22institutetext: TU Wien, Wien, Austria

#  Deductive Controller Synthesis for Probabilistic Hyperproperties††thanks:
This work has been supported by the Czech Science Foundation grant GA23-06963S
(VESCAA), the European Union’s Horizon 2020 project No 101034440 and by the
Vienna Science and Technology Fund 10.47379/ICT19018.

Roman Andriushchenko 11 Ezio Bartocci 22 Milan Češka 11 Francesco Pontiggia 22
Sarah Sallinger 22

###### Abstract

Probabilistic hyperproperties specify quantitative relations between the
probabilities of reaching different target sets of states from different
initial sets of states. This class of behavioral properties is suitable for
capturing important security, privacy, and system-level requirements. We
propose a new approach to solve the controller synthesis problem for Markov
decision processes (MDPs) and probabilistic hyperproperties. Our specification
language builds on top of the logic HyperPCTL and enhances it with structural
constraints over the synthesized controllers. Our approach starts from a
family of controllers represented symbolically and defined over the same copy
of an MDP. We then introduce an abstraction refinement strategy that can
relate multiple computation trees and that we employ to prune the search space
deductively. The experimental evaluation demonstrates that the proposed
approach considerably outperforms HyperProb, a state-of-the-art SMT-based
model checking tool for HyperPCTL. Moreover, our approach is the first one
that is able to effectively combine probabilistic hyperproperties with
additional intra-controller constraints (e.g. partial observability) as well
as inter-controller constraints (e.g. agreements on a common action).

##  1 Introduction

Controller synthesis in a probabilistic environment [9] is a well-known and
highly addressed problem. There exist several off-the-shelf tools (e.g. PRISM
[32] or STORM [28]) that are able to to synthesize optimal policies for large
Markov decision processes (MDPs) with respect to probability measures over a
given set of paths. However, recent studies [3, 2, 20, 19, 17] have brought up
the necessity to investigate a new class of properties that relate probability
measures over different sets of executions. This class of requirements is
called probabilistic hyperproperties [2], and standard logics, such as
Probabilistic Computation Tree Logic (PCTL) [27], are not expressive enough
for them. Classical examples include security and privacy requirements, such
as quantitative information-flow [31], probabilistic noninterference [26, 35]
and differential privacy for databases [22]. Probabilistic hyperproperties can
be expressed using Probabilistic HyperLogic (PHL) [17] and HyperPCTL [2]. Both
are probabilistic temporal logics that extends PCTL with i) quantifiers over
schedulers and ii) predicates over functions of probability expressions.
Verification of HyperPCTL or PHL formulae can be formalized as the synthesis
of multiple, correlated strategies that represent a witness or a
counterexample to the specification. Furthermore, pioneering studies have
shown that probabilistic hyperproperties have novel applications in robotics
and planning [17], and in causality analysis for probabilistic systems [8]. To
deal with these new constraints, it is necessary to establish a connection not
only between the probabilities of different strategies, but also between the
choices they make in corresponding states, i.e. reasoning about the structural
characteristics of the resulting controllers. Finally, the study of
probabilistic hyperproperties in a partially observable setting is mostly
unexplored.

##### Motivating Example 1.

Figure 1: Planning under probabilistic noninterference.

Consider a planning problem depicted in Figure 1: a robot in a probabilistic
environment attempts to reach the target location $T$. A controller for the
robot is a program that, for each position, selects the next action to take.
Consider the synthesis of two distinct controllers for two possible initial
states $s_{a}$ and $s_{b}$. In a confidential setting, we want to combine
performance constraints on success probabilities with additional privacy and
structural requirements. _Probabilistic noninterference_ is a hyperproperty
asserting that the success probability must be the same for $s_{a}$ and
$s_{b}$, so that an attacker cannot infer any information about the selected
initial location by observing the percentage of successful robots. If further
the choice made in some state $s_{\chi}$ is assumed to be observable to the
attacker, the two strategies must agree on their action choices in $s_{\chi}$.
Finally, the _partial observability_ constraint requires a controller to make
the same choice in states $s_{c}$ and $s_{d}$ having the same observation.

##### Related Work.

In [3] and [1], the authors introduce, respectively, the model-checking
problem and the parameter synthesis problem for discrete-time Markov chains
satisfying probabilistic hyperproperties. The works in [2, 17] have recently
studied the verification of probabilistic hyperproperties in the context of
MDPs and proposed two suitable logics: HyperPCTL and Probabilistic HyperLogic
(PHL), respectively. However, in both cases the model-checking problem is
undecidable. The solution proposed for the former logic is to consider only
the class of deterministic memoryless controllers, where the problem is shown
to be NP-complete by a suitable SMT encoding. Despite recent improvements of
HyperProb [18, 20], a state-of-the-art tool implementing this approach, its
scalability remains very limited: the complexity of the encoding gets out of
reach even for modest models. For instance, a simple side-channel analysis
introduced in [2] (checking that the probability of certain outcomes is equal)
on an MDP with 244 states leads to an SMT problem with over a million
variables, which HyperProb fails to solve. Finally, HyperProb does not provide
support for structural constraints describing non-probabilistic relations
between controllers, and the presented techniques cannot principally handle
neither partial observability.

On the other hand, PHL is able to express such structural constraints using
HyperCTL* [15] formulae in conjunction with probability expressions. Hence,
with PHL, it is possible to require different paths to take the same (or a
different) choice in a certain state. However, the model checking procedure
developed in [17] employs a bounded synthesis algorithm which supports only
_qualitative_ constraints, and cannot effectively handle the probability
expressions of a PHL formula - the synthesis loop has to check them a
posteriori. As a result, when the qualitative constraints do not restrict the
controllers sufficiently, a large part of the search space has to be
explicitly enumerated.

Various works have addressed (reactive) synthesis problems in non
probabilistic settings [13, 36, 23, 24]. In particular, decidability for
HyperLTL [15] specifications and finite-state plants has been shown in [13].

##### Our contribution.

To mitigate the limitations of the existing approaches, we propose a novel
controller synthesis framework for MDPs and probabilistic hyperproperties. We
enrich expressive power of HyperPCTL with structural constraints to support
additional requirements on the controllers (Section 2). We treat the synthesis
problem as an exploration problem over a symbolic representation of a family
of controllers defined over the original MDP (Section 3). Inspired by recent
advances in the synthesis of probabilistic systems [4], we tailor a deductive
exploration method to support hyper-reasoning. In particular, we propose an
abstraction refinement strategy that relates multiple computation trees and
allows us to deductively identify sets of violating controllers that can be
safely removed from the search space (Section 4). A detailed experimental
evaluation (Section 5) demonstrates that our approach considerably outperforms
the state-of-the-art tool HyperProb [18]. In particular, our approach scales
to more complicated synthesis problems where HyperProb times out, and
supports, for the first time, various structural constraints.

##  2 Problem Formulation

In this section we present the formalisms involved in our synthesis framework
as well as the problem statement. We refer to [7, 10] for further background.

###  2.1 Probabilistic models

A (discrete) _probabilistic distribution_ over a finite set $X$ is
$\mu\,:X\rightarrow[0,1]$, where $\sum_{x\in X}\mu(x)=1$. The set of all
distributions on $X$ is denoted as $Distr(X)$.

######  Definition 1 (MDP)

A _Markov Decision Process (MDP)_ is a tuple $(S,Act,\mathcal{P})$ with a
finite set $S$ of states, a finite set $Act$ of actions and a transition
function $\mathcal{P}:S\times Act\rightarrow Distr(S)$. An MDP with $|Act|=1$
is a _Markov chain (MC)_ $(S,\mathcal{P})$ with $\mathcal{P}:S\rightarrow
Distr(S)$.

We depart from the standard notion of MDP [10] and do not specify initial
states: those will be derived from the context given by the specification.
Additionally, to simplify the presentation, we enable all actions in every
state. An MDP can be equipped with a state-action reward (or cost) function
$rew:S{\times}Act\rightarrow\mathbb{R}_{\geqslant 0}$, where reward
$rew(s,\alpha)$ is earned upon executing action $\alpha$ in state $s$. A
(memoryless, deterministic) _controller_ $\sigma\colon S\rightarrow Act$
selects in each state $s$ an action $\sigma(s)$; let $\Sigma^{M}$ denote the
set of all such controllers in $M$. Imposing controller $\sigma$ onto MDP
$M=(S,Act,\mathcal{P})$ yields MC
$M^{\sigma}=\left(S,\mathcal{P}^{\sigma}\right)$ where
$\mathcal{P}^{\sigma}(s)=\mathcal{P}(s,\sigma(s))$. For an MC $M$,
$\mathbb{P}(M,s\models\Diamond T)$ denotes the probability of reaching the set
$T\subseteq S$ of target states when starting in state $s\in S$. If
$\mathbb{P}(M,s\models\Diamond T)=1$, then $\mathbb{R}({M,s\models\Diamond
T})$ denotes the expected reward accumulated from $s$ before reaching $T$.
Using the standard techniques, one can effectively compute a minimizing
controller $\sigma_{\min}$ that minimizes the probability to reach $T$, i.e.
$\forall\sigma\in\Sigma^{M}:$ $\mathbb{P}(M^{\sigma_{\min}},s\models\Diamond
T)$ $\leq\mathbb{P}(M^{\sigma},s\models\Diamond T)$. Naturally, this can be
lifted to the expected rewards.

###  2.2 HyperPCTL with Structural Constraints

Assume an MDP $M=(S,Act,\mathcal{P})$. Our specification language builds on
the syntax of HyperPCTL [2], enriched by structural constraints. For both
principal and technical reasons discussed below, we support only the following
fragment of the original hyperlogic:

$\displaystyle\varphi$
$\displaystyle\coloneqq\exists\,\sigma_{1},\ldots,\sigma_{n}\in\Sigma^{M}\colon\varphi^{struc}\land\varphi^{state}$
$\displaystyle\varphi^{struc}$
$\displaystyle\coloneqq\varphi^{struc}\land\varphi^{struc}\mid\mathcal{X}_{s}(\Sigma)\mid\mathcal{O}_{S^{\prime}}(\sigma_{i})$
$\displaystyle\varphi^{state}$
$\displaystyle\coloneqq\mathcal{Q}_{1}{s_{1}}{\in}I_{1}[\sigma^{1}]\dots\mathcal{Q}_{m}{s_{m}}{\in}I_{m}[\sigma^{m}]\colon\varphi^{prob}$
$\displaystyle\varphi^{prob}$
$\displaystyle\coloneqq\neg\varphi^{prob}\mid\varphi^{prob}\land\varphi^{prob}\mid\varphi^{atom}$
$\displaystyle\varphi^{atom}$
$\displaystyle\coloneqq\mathbb{P}(M^{\sigma^{i}},{s_{i}}\models\Diamond
T)\bowtie\lambda\mid\mathbb{P}(M^{\sigma^{i}},{s_{i}}\models\Diamond
T_{i})\bowtie\mathbb{P}(M^{\sigma^{j}},{s_{j}}\models\Diamond T_{j})\mid$
$\displaystyle\hskip
16.99998pt\mathbb{R}({M^{\sigma^{i}},{s_{i}}\models\Diamond
T})\bowtie\rho\mid\mathbb{R}({M^{\sigma^{i}},{s_{i}}\models\Diamond
T_{i}})\bowtie\mathbb{R}({M^{\sigma^{j}},{s_{j}}\models\Diamond T_{j}})$

where $\mathcal{Q}\in\\{\exists,\forall\\}$,
$\bowtie\,\in{\\{<,\leq,=,>,\geq\\}}$, $k\in\mathbb{N}$, $\lambda\in[0,1]$ and
$\rho\in\mathbb{R}_{\geq 0}$. The individual parts of the syntax and semantics
are described below.

Controller quantification ($\varphi$):

We consider the _synthesis_ problem, i.e. only the existential quantification
over the controllers $\sigma_{i}$ is supported.111A _verification_ problem
defined using universal quantification can be treated as synthesis of a
counterexample. Alternation in the controller quantification is not supported
as it principally complicates the inductive synthesis strategy. To the best of
our knowledge, only very few techniques so far practically support alternation
[29, 12].

Structural constraints ($\varphi^{struc}$):

In contrast to HyperPCTL [2], we support conjunctions of structural
constraints of two types: i) intra-controller constraint
$\mathcal{O}_{S^{\prime}}(\sigma_{i})$ requiring that the controller
$\sigma_{i}$ takes the same action in all states from the set
$S^{\prime}\subseteq S$ (this can effectively encode partial observability)
and ii) inter-controller constraint $\mathcal{X}_{s}(\Sigma)$ requiring that
all controllers in $\Sigma\subseteq\\{\sigma_{1},\dots,\sigma_{n}\\}$ take the
same action in state $s\in S$.

State quantification ($\varphi^{state}$):

Allows to quantify over the computational trees rooted in the given initial
states. We support an arbitrary quantification
$\mathcal{Q}_{i}{s_{i}}{\in}I_{i}[\sigma^{i}]$, where each ${s_{i}}$ is
associated with its domain $I_{i}\subseteq S$ and some controller
$\sigma^{i}\in\\{\sigma_{1},\dots,\sigma_{n}\\}$. Note that multiple state
variables can be associated with the same controller ($n\leq m$).

Probability constraints ($\varphi^{prob}$):

We consider a Boolean combination of the standard inequalities between the
reachability probability (reward) and a threshold as well as the inequalities
that correspond to the class of 2-hyperproperties [16], where a relationship
between two computation trees is considered222An extension to nested-free PCTL
path formulae is straightforward. Principally, we can extend the probability
constraints to allow more complicated expressions (e.g. sum/difference of
reachability probabilities from different states) eventually requiring
reasoning about more than two computation trees..

To evaluate whether given $n$ controllers for MDP $M$ satisfy a state formula
$\varphi^{state}$, we instantiate the initial states on the probabilistic
constraint $\varphi^{prob}$.

######  Definition 2 (Instantiation of state quantifiers)

Assume a state formula
$\mathcal{Q}_{1}{s_{1}}{\in}I_{1}[\sigma^{1}]\dots\mathcal{Q}_{m}{s_{m}}{\in}I_{m}[\sigma^{m}]\colon\varphi^{prob}$.
Each quantifier $\mathcal{Q}_{i}{s_{i}}{\in}I_{i}[\sigma^{i}]$ is instantiated
on $\varphi^{prob}$ by substituting $\varphi^{prob}$ with ${\nabla_{s\in
I_{i}}\varphi^{prob}[{s_{i}}\mapsto s]}$, where $\nabla\equiv\bigvee$ if
$\mathcal{Q}_{i}\equiv\exists$ and $\nabla\equiv\bigwedge$ otherwise.

Upon instantiation, we obtain a Boolean combination of inequalities over
probabilities and rewards in the corresponding MCs having the given initial
states.

##### Remark 1.

HyperPCTL syntax also allows to reason about stepwise _paired_ multiple traces
by associating the atomic propositions in the path formulae of probability
expressions with state variables (i.e the initial state of a particular
computation). Then, to evaluate a formula with $m$ state quantifications, the
semantics requires to build the $m$-cross-product (also called _self-
composition_ [2, 17], or _trivial coupling_ [11]), of the original model $M$.
In this paper, for the sake of simplicity, we avoid such an involved
construction and consider only single, uncoupled computation trees, where all
atomic propositions share the same state variable specified in the probability
expression. However, handling such constraints would require only an
additional technical step performing the cross-product when needed [37], and
no principle obstacles.

##### Problem statement.

The key problem statement in this paper is _feasibility_ :  Given an MDP $M$
and a hyperspecification
$\exists\,\sigma_{1},\ldots,\sigma_{n}\in\Sigma^{M}\colon\varphi^{struc}\land\mathcal{Q}_{1}{s_{1}}{\in}I_{1}[\sigma^{1}]\dots\mathcal{Q}_{m}{s_{m}}{\in}I_{m}[\sigma^{m}]\colon\varphi^{prob}$
find controllers $\sigma_{1},\ldots,\sigma_{n}$ in $\Sigma^{M}$ that satisfy
$\varphi^{struc}$ and the instantiated $\varphi^{prob}$.

##### Remark 2.

We follow existing approaches [2, 19, 20] and consider only the class of
deterministic memoryless controllers where synthesis is decidable. These
controllers are, however, too weak for some synthesis problems considered in
the experimental evaluation. Therefore, we enhance the underlying MDPs with a
memory to explore a richer class of controllers, as in [17].

##### Example 2.

Consider Example 1 from the introduction. The probabilistic noninterference
specification for the synthesis of two controllers can be expressed as

$\displaystyle\exists\,\sigma_{1},\sigma_{2}$
$\displaystyle\colon\varphi^{struc}\land\forall{s_{1}}\in\\{s_{a}\\}[\sigma_{1}]\;\forall{s_{2}}\in\\{s_{b}\\}[\sigma_{2}]\colon\varphi^{prob}\mbox{,
where }$ $\displaystyle\varphi^{struc}$
$\displaystyle\equiv\mathcal{X}_{s_{\chi}}(\\{\sigma_{1},\sigma_{2}\\})\land\mathcal{O}_{\\{s_{c},s_{d}\\}}(\sigma_{1})\land\mathcal{O}_{\\{s_{c},s_{d}\\}}(\sigma_{2})$
$\displaystyle\varphi^{prob}$
$\displaystyle\equiv\mathbb{P}(M^{\sigma_{1}},{s_{1}}\models\Diamond
T)=\mathbb{P}(M^{\sigma_{2}},{s_{2}}\models\Diamond
T)\land\mathbb{P}(M^{\sigma_{1}},{s_{1}}\models\Diamond T)\geq\lambda$

Given $\sigma_{1}$ and $\sigma_{2}$, the instantiation of the state
quantifiers on $\varphi^{prob}$ yields the following probability constraint
$\mathbb{P}(M^{\sigma_{1}},s_{a}\models\Diamond
T)=\mathbb{P}(M^{\sigma_{2}},s_{b}\models\Diamond
T)\land\mathbb{P}(M^{\sigma_{1}},s_{a}\models\Diamond T)\geq\lambda$.

##### Remark 3.

Our approach also supports various variants of optimal synthesis problems,
where an additional minimizing/maximizing objective over a reachability
probability or reward is considered. For example, we can maximize the
difference $\mathbb{P}(M^{\sigma_{1}},{s_{1}}\models\Diamond
T_{1})-\mathbb{P}(M^{\sigma_{2}},{s_{2}}\models\Diamond T_{2})$. To simplify
the technical exposition of the paper, we will omit the precise formalisation
of these problems.

##  3 Family of Controllers

Consider an MDP $M$ for which we wish to synthesize $n$ controllers
$\sigma_{1},\ldots\sigma_{n}$, further referred to as an _$n$ -controller_
$\overline{\sigma}=(\sigma_{1},\dots,\sigma_{n})$, that satisfy a
hyperproperty $\varphi^{struc}\land\varphi^{state}$. Motivated by the
inductive synthesis method presented in [4], we base our approach on a
symbolic representation of a _family of $n$-controllers_ over MDP $M$. The
following definition allows us to efficiently represent all $n$-controllers
that satisfy $\varphi^{struc}$.

######  Definition 3 (Parameter space)

Assume an MDP $M=(S,Act,\mathcal{P})$ and a hyperspecification
$\exists\,\sigma_{1},\ldots,\sigma_{n}\colon\varphi^{struc}\land\varphi^{state}$.
For each $i\in\\{1,\ldots,n\\}$ and $s\in S$, we introduce a parameter
$k(i,s)$ with domain $\mathrm{dom}(i,s)=Act$. Relation $k\simeq k^{\prime}$
denotes that parameters $k,k^{\prime}$ are _synonymous_ , i.e. $k$ and
$k^{\prime}$ are different names for the same parameter. For each
$\mathcal{O}_{S^{\prime}}(\sigma_{i})\in\varphi^{struc}$ we require that
$\forall\,s,s^{\prime}\in S^{\prime}:$ $k(i,s)\simeq k(i,s^{\prime})$.
Additionally, for each $\mathcal{X}_{s}(\Sigma)\in\varphi^{struc}$ we require
that $\forall\,\sigma_{i},\sigma_{j}\in\Sigma:$ $k(i,s)\simeq k(j,s)$. Let
$\mathcal{K}$ denote the set of all parameters.

Parameter $k(i,s)$ essentially encodes possible action selections available to
$\sigma_{i}$ at state $s$. A realisation then encodes a specific assignment of
these parameters.

######  Definition 4 (Realisation)

A _realisation_ is a mapping $r\colon\mathcal{K}\rightarrow Act$ such that
$r(k(i,s))\in\mathrm{dom}(i,s)$. $\mathcal{R}$ denotes the set of all
realisations. Realisation $r$ _induces_ $n$-controller
$\overline{\sigma}^{r}\coloneqq(\sigma_{1}^{r},\ldots,\sigma_{n}^{r})$ where
$\forall i\in\\{1,\ldots,n\\}\,\forall s\in
S\colon\sigma_{i}^{r}(s)=r(k(i,s))$.

Realisation $r\in\mathcal{R}$ specifies for each $\sigma_{i}$ a specific
action $r(k(i,s))$ to be selected in state $s$, and thus describes an
$n$-controller $\overline{\sigma}^{r}\in(\Sigma^{M})^{n}$. Using synonymous
parameters implies that $r$ always induces controller $\overline{\sigma}^{r}$
satisfying structural constraints $\varphi^{struc}$. Thus, the set
$\mathcal{R}$ of realisations directly corresponds to the family $\mathcal{F}$
of controllers that satisfy $\varphi^{struc}$.

######  Definition 5 (Family of controllers)

A _family of $i$-th controllers_ is the set
$\mathcal{F}_{i}=\\{\sigma_{i}^{r}\mid r\in\mathcal{R}\\}.$ A _family of
$n$-controllers_ is the set $\mathcal{F}\coloneqq\\{\overline{\sigma}^{r}\mid
r\in\mathcal{R}\\}$.

From this definition it is clear that $\mathcal{F}\subseteq(\Sigma^{M})^{n}$
and that
$\overline{\sigma}\in\mathcal{F}\Leftrightarrow\overline{\sigma}\models\varphi^{struc}$.
We say that an $n$-controller
$\overline{\sigma}=(\sigma_{1},\dots,\sigma_{n})$ from the set
$(\Sigma^{M})^{n}{\setminus}\mathcal{F}$ is _inconsistent_ , where we
distinguish between the following two types of inconsistency.

  * •

$\overline{\sigma}\not\models\mathcal{O}_{S^{\prime}}(\sigma_{i})$ is said to
be _intra-controller inconsistent_ : controller $\sigma_{i}$ diverges in its
choices $\sigma_{i}(s_{a})\neq\sigma_{i}(s_{b})$ for the action selection in
states $s_{a},s_{b}\in S^{\prime}$.

  * •

$\overline{\sigma}\not\models\mathcal{X}_{s}(\Sigma)$ is said to be _inter-
controller inconsistent_ : controllers $\sigma_{i},\sigma_{j}\in\Sigma$
diverge in their choices $\sigma_{i}(s)\neq\sigma_{j}(s)$ for the action
selection in state $s$.

Conversely, if $\overline{\sigma}\in\mathcal{F}$, then there exists exactly
one realisation $r\in\mathcal{R}$ s.t.
$\overline{\sigma}^{r}=\overline{\sigma}$. Subsequently, if
$\sigma_{i}\in\mathcal{F}_{i}$, then the following set of realisations:

$\mathcal{R}[\sigma_{i}]\coloneqq\left\\{r\in
R\mid\overline{\sigma}^{r}=(\sigma_{1},\ldots,\sigma_{i},\ldots,\sigma_{n})\right\\}$

is not empty and contains all realisations that induce $\sigma_{i}$. From
$\mathcal{F}\subseteq(\Sigma^{M})^{n}$ it follows that the size of the family
$|\mathcal{F}|\leq|Act|^{|S|n}$ is exponential in the number $|S|$ of states
and $n$, rendering enumeration of each $n$-controller
$\overline{\sigma}\in\mathcal{F}$ infeasible.

##  4 Deductive Exploration

We present a deductive method allowing for an efficient exploration of the
given family $\mathcal{F}$ of $n$-controllers. We adapt the abstraction
refinement approach for PCTL specifications presented in [14, 5] to the
synthesis against probabilistic hyperproperties. We explain the method on a
canonical synthesis problem
$\varphi_{c}\equiv\exists\,\sigma_{1},\sigma_{2}:\varphi^{struc}\land\exists\,s_{1}\\!\in\\!\\{s_{1}\\}[\sigma_{1}],\,\exists
s_{2}\\!\in\\!\\{s_{2}\\}[\sigma_{2}]:\varphi^{prob}$, where
$\varphi^{prob}\equiv\mathbb{P}(M^{\sigma_{1}},{s_{1}}\models\Diamond
T_{1})\leq\mathbb{P}(M^{\sigma_{2}},{s_{2}}\models\Diamond T_{2})$. A
generalisation to more complicated specifications is discussed in Subsection
4.3.

###  4.1 Guided Abstraction Refinement Scheme

MDP $M$ and the corresponding set $(\Sigma^{M})^{n}$ of controllers provide an
over-approximation of the set $\mathcal{F}$ of admissible controllers. The key
idea is to analyse $M$ using standard techniques to obtain the following four
controllers: $\sigma_{1}^{\min}$ ($\sigma_{1}^{\max}$) minimising (maximising)
the probability of reaching $T_{1}$ from $s_{1}$, and controllers
$\sigma_{2}^{\min}$ and $\sigma_{2}^{max}$ minimising (maximising) the
probability of reaching $T_{2}$ from $s_{2}$. Let
$l_{1}\coloneqq\mathbb{P}(M^{\sigma_{1}^{\min}},s_{1}\models\Diamond T_{1})$
denote the minimum probability of reaching $T_{1}$ from $s_{1}$ via
$\sigma_{1}^{\min}$; since the corresponding $\sigma_{1}^{\min}$ is not
necessarily in $\mathcal{F}_{1}$, then this probability is a lower bound on
$\min_{\sigma\in\mathcal{F}_{1}}\mathbb{P}(M^{\sigma},s_{1}\models\Diamond
T_{1})$. Let $u_{1}$ be the corresponding upper bound on the probability of
reaching $T_{1}$ from $s_{1}$, and similarly for $l_{2}$ and $u_{2}$. It is
clear that $l_{1}\leq u_{1}$ and $l_{2}\leq u_{2}$.

Comparing the corresponding numerical intervals $[l_{1},u_{1}]$ and
$[l_{2},u_{2}]$ may allow us to determine whether $(\Sigma^{M})^{n}$ (and, by
extension, $\mathcal{F}$) can satisfy $\varphi^{prob}$. The procedure is
summarised in Table 1. For instance, if the two intervals do not overlap, then
either all controllers satisfy $\varphi^{prob}$ (case (1)) or none do (case
(2)).

In the remaining cases (3)-(5), when the intervals do overlap, it is ambiguous
whether $\mathcal{F}$ contains feasible solutions, so additional analysis is
necessary. For example, if $l_{1}\leq l_{2}$ (case (3)) and
$\sigma_{1}^{\min}$ satisfies all intra-controller constrafints
$\mathcal{O}_{S^{\prime}}(\sigma_{1})\in\varphi^{struc}$, then
$\sigma_{1}^{\min}\in\mathcal{F}_{1}$ and thus there exists realisation
$r\in\mathcal{R}[\sigma_{1}^{\min}]$ such that
$\overline{\sigma}^{r}\models\varphi_{c}$. Analogous reasoning can be applied
to case (4). Finally, in case (5), an $n$-controller
$(\sigma_{1}^{\min},\sigma_{2}^{\max})$ represents a solution if it is
consistent; then, any realisation
$r\in\mathcal{R}[\sigma_{1}^{\min}]\cap\mathcal{R}[\sigma_{2}^{\max}]$ that
induces both of these controllers is accepting. In all of these cases (3)-(5),
if the consistency requirements are not met, $\mathcal{R}$ may still contain
feasible solutions, but not involving $\sigma_{1}^{\min}$ or
$\sigma_{2}^{\max}$. In other terms, our over-approximation $M$ is too coarse
and needs to be _refined_ to obtain more precise results. Refinement will be
the focus of Subsection 4.2.

case | condition | feasibility | SAT realisations
---|---|---|---
(1) | $[l_{1},u_{1}]\leq[l_{2},u_{2}]$ | all SAT | $\mathcal{R}$
(2) | $[l_{2},u_{2}]<[l_{1},u_{1}]$ | all UNSAT | $\emptyset$
(3) | $l_{1}\leq[l_{2},u_{2}]$ | ambiguous | $\mathcal{R}[\sigma_{1}^{\min}]$
(4) | $[l_{1},u_{1}]\leq u_{2}$ | ambiguous | $\mathcal{R}[\sigma_{2}^{\max}]$
(5) | $l_{2}\leq l_{1}\leq u_{2}\leq u_{1}$ | ambiguous | $\mathcal{R}[\sigma_{1}^{\min}]\cap\mathcal{R}[\sigma_{2}^{\max}]$
Table 1: Reasoning about feasibility of family $\mathcal{F}$ using interval
logic.

##### Special cases of $\varphi_{c}$.

Note that if $T_{1}=T_{2}$, then $\sigma_{1}^{\min}=\sigma_{2}^{\min}$: the
controller minimising the reachability probability for state $s_{1}$ also
minimises the reachability probability from state $s_{2}$. Therefore, only two
model checking queries are required, as opposed to four. Finally, if
$T_{1}\neq T_{2}$ but the property quantifies over a single controller, e.g.
$\varphi^{struc}\land\exists\,\sigma:\exists\,s_{1}\in\\{s_{1}\\}[\sigma],\,\exists
s_{2}\in\\{s_{2}\\}[\sigma]:\varphi^{prob}$, then again four controllers are
computed. However, additional care must be taken in case (5). If
$\sigma_{1}^{\min}$ and $\sigma_{2}^{\max}$ are consistent, note that the
property calls for a 1-controller, so we need
$\sigma_{1}^{\min}=\sigma_{2}^{\max}$. If this is not the case, i.e.
$\sigma_{1}^{\min}(s)\neq\sigma_{2}^{\max}(s)$ for some $s\in S$, it might
happen that for one controller this action selection is not relevant to
guarantee feasibility, so we can ensure
$\sigma_{1}^{\min}(s)=\sigma_{2}^{\max}(s)$. If the two controllers cannot
reach an agreement for all action selections, we say that these controllers
are _incompatible_.

###  4.2 Splitting strategy

Consider controller $\sigma\in\Sigma^{M}$ provided by the model checker from
which a feasible realisation $r\in\mathcal{R}$ could not have been deduced
because $\sigma$ is (intra-controller) inconsistent (cases (3)-(4),
$\mathcal{R}[\sigma]=\emptyset$)333Case (5), when $\sigma$ is consistent but
incompatible with another controller $\sigma^{\prime}$, is handled
analogously, as well as when they are inter-controller inconsistent.. Let $i$
be the index controller $\sigma$ is associated with in the set of controllers
to be synthesized. $\sigma$ being inconsistent means there exists a
_conflicting parameter_ $k\in\mathcal{K}$ associated with multiple states for
which $\sigma$ selected different actions. Formally, let
$\mathcal{S}_{k}\coloneqq\left\\{s^{\prime}\in S\mid k(i,s^{\prime})\simeq
k\right\\}$ denote the set of states associated with $k$ and let
$\mathcal{A}_{k}\coloneqq\left\\{\sigma(s)\mid s\in\mathcal{S}_{k}\right\\}$
be the set of actions selected by $\sigma$ in these states;
$|\mathcal{A}_{k}|>1$ iff $\sigma$ is inconsistent.

The goal is to partition $\mathcal{R}$ into subsets of realisations in which
this conflict cannot occur, i.e. $\sigma$ cannot be derived by the model
checker. Such a partition can be achieved by partitioning the domain
$\mathrm{dom}(i,s)$ of the conflicting parameter. We construct the partition
$\mathfrak{X}$ using singletons containing conflicting actions:
$\mathfrak{X}=\\{\\{a\\}\mid
a\in\mathcal{A}_{k}\\}\cup\\{\mathrm{dom}(i,s){\setminus}\mathcal{A}_{k}\\}$.
Let $\\{\mathcal{R}_{X}\\}_{X\in\mathfrak{X}}$ denote the corresponding
partition of the set $\mathcal{R}$ of realisations where
$\mathcal{R}_{X}\coloneqq\left\\{r\in\mathcal{R}\mid r(k(i,s))\in X\right\\}$.
Finally, for arbitrary $X\in\mathfrak{X}$, consider a _restriction_
$M[\mathcal{R}_{X}]$ of MDP $M$, in which only actions from the set $X$ are
available in states $\mathcal{S}_{k}$. It is easy to see that
$\sigma\not\in\Sigma^{M[\mathcal{R}_{X}]}$, indicating that over-approximation
$M[\mathcal{R}_{X}]$ is more precise.

When $\sigma$ violates multiple structural constraints, there are multiple
conflicting parameters. To select a single parameter to be used for splitting,
we employ a heuristic inspired by [5]. The heuristic is described in Appendix
0.A.

Algorithm 1 Deductive syntheses using abstraction refinement (AR loop).

Input: MDP $M=(S,Act,\mathcal{P})$, specification
$\exists\,\sigma_{1},\ldots,\sigma_{n}\in\Sigma^{M}\colon\varphi^{struc}\land\varphi^{state}$
where
$\varphi^{state}=\mathcal{Q}_{1}{s_{1}}{\in}I_{1}[\sigma^{1}]\dots\mathcal{Q}_{m}{s_{m}}{\in}I_{m}[\sigma^{m}]\colon\varphi^{prob}$
Output: $\overline{\sigma}=(\sigma_{1},\dots\sigma_{n})$ that satisfies
$\varphi^{struc}\wedge\varphi^{prob}$, or “unfeasible”.

1:$\Phi\leftarrow\texttt{instantiateQuantifiers}(\varphi^{state},\varphi^{prob})$
$\triangleright$ Use Def. 2

2:$\mathcal{R}\leftarrow\texttt{constructFamily}(M,n,\varphi^{struc})$
$\triangleright$ Use Def. 5

3:$\overline{\mathcal{R}}.\texttt{push}(\mathcal{R})$ $\triangleright$ Create
a stack of (sub-)families $\overline{\mathcal{R}}$

4:while $\texttt{nonEmpty}(\overline{\mathcal{R}})$ do

5: $\mathcal{R}\leftarrow\overline{\mathcal{R}}.\texttt{pop}()$

6: For each $\phi\in\texttt{atoms}(\Phi)$ do

7: $bounds,controllers\leftarrow\texttt{analyseMDP}(M[\mathcal{R}],\phi)$
$\triangleright$ Compute bounds wrt. $\phi$

8: $consistency\leftarrow\texttt{checkConsistency}(controllers)$

9: $results(\phi)\leftarrow\texttt{intervalLogic}(bounds,consistency)$
$\triangleright$ Apply Tab. 1

10: $\Phi^{\prime}=\texttt{replaceAndEvaluate}(\Phi,results)$

11: if $\Phi^{\prime}\ \equiv\top$ then return any $\overline{\sigma}^{r}$
s.t. $r\in\mathcal{R}$ $\triangleright$ $\mathcal{R}$ is feasible

12: if $\Phi^{\prime}\ \equiv\bot$ then continue $\triangleright$
$\mathcal{R}$ is unfeasible and thus pruned

13: if
$(\mathcal{R}^{\prime}=\texttt{compose}(\Phi^{\prime},results))\neq\varnothing$
then return any $\overline{\sigma}^{r}$ s.t. $r\in\mathcal{R}^{\prime}$
$\triangleright$ SAT

14: $\phi\leftarrow\texttt{ambiguousAtom}(\Phi^{\prime})$

15:
$\overline{\mathcal{R}}.\texttt{push}(\texttt{split}(\mathcal{R},results(\phi)))$
$\triangleright$ Use splitting wrt. $\phi$ as described in Sec. 4.2

16:return unfeasible

###  4.3 Synthesis algorithm (AR loop)

Algorithm 1 summarises the proposed synthesis approach, further denoted as
_abstraction refinement (AR) loop_. We first instantiate the state
quantifications of $\varphi^{state}$ on $\varphi^{prob}$ (see Def. 2). The
result is $\Phi$, a Boolean combination of constraints. Afterwards, we
construct the family of realisations $\mathcal{R}$ according to Def. 5 and
push $\mathcal{R}$ to the stack $\overline{\mathcal{R}}$ of families to be
processed. Then, the main synthesis loop starts: each iteration corresponds to
the analysis of one (sub-)family of realisations. Firstly, an iteration
analyses the restricted MDP $M[\mathcal{R}]$ wrt. each atomic property $\phi$
appearing in $\Phi$. This is the most computationally demanding part of the
algorithm, where bounds on particular reachability probabilities (rewards)
involved in $\phi$ are computed. The produced controllers are checked for
consistency, and together with bounds we use reasoning from Sec. 4.1, and in
particular Tab. 1, to mark feasibility of $\mathcal{R}$ wrt. $\phi$ as one of
‘all SAT’, ‘all UNSAT’ or ‘ambiguous’. To decide whether $\Phi$ can be
satisfied, on Line 10 we replace each (UN)SAT atom with $\top$ ($\bot$). If
the resulting formula $\Phi^{\prime}$ is trivially $\top$, then any
realisation in $\mathcal{R}$ is a satisfying solution. Conversely, if
$\Phi^{\prime}$ is $\bot$, there is no satisfying realisation, hence
$\mathcal{R}$ is discarded. Finally, if $\Phi^{\prime}$ is neither $\top$ nor
$\bot$, we try to compose a satisfying $n$-controller from individual
controllers (obtained when analysing atoms of $\Phi$) by performing
intersections or unions of the corresponding sets $\mathcal{R}[\sigma]$ of SAT
realisations. If such composition returns an empty set, then $\mathcal{R}$ is
partitioned (see Sec. 4.2) into sub-families that are put on top of stack
$\overline{\mathcal{R}}$.

##  5 Experiments

Our experimental evaluation focuses on the following key questions:

  * Q1:

_How does the proposed deductive approach perform in comparison to the state-
of-the-art SMT based approach implemented in HyperProb [18]?_

  * Q2:

_Can the deductive approach effectively handle synthesis problems that include
structural constraints?_

##### Implementation and experimental setting.

We have implemented the proposed AR loop on top of the tool Paynt [6] – a tool
for the synthesis of probabilistic programs. Paynt takes input models
expressed as extended PRISM [32] files, and relies on the probabilistic model
checker STORM [28] to analyse the underlying MDPs. All experiments were run on
a Linux Ubuntu 20.04.4 LTS server with a 3.60GHz Intel Xeon CPU and 64GB of
RAM. A timeout of 1 hour is enforced. All run-times are in seconds.

### Q1: Comparison with HyperProb

In this section, we present a detailed performance comparison of the proposed
approach with the SMT encoding implemented in HyperProb.

We first consider the main case studies presented in [18], namely, TA (timing
attack), PW (password leakage), TS (thread scheduling) and PC (probabilistic
conformance). A short description of the models and considered variants can be
found in Appendix 0.B. Note that the first three case studies are formulated
as _verification_ problems and thus the dual formulation, i.e., _synthesis of
a counter-example_ , is considered. Also note that all considered variants are
feasible, i.e. a counter-example exists as well as a valid solution for PC.

Case Study | MDP | AR loop | HyperProb
---|---|---|---
size | family | time | iters | vars | sub | e-time | s-time
PW $(n=4)$ | 298 | 5E21 | ${<}1s$ | 1 | 357898 | 597 | 93 | 40
PW∗ $(n=4)$ | 298 | 5E21 | ${<}1s$ | 1 | 1792172 | 597 | 548 | TO
TA $(n=4)$ | 244 | 5E21 | ${<}1s$ | 1 | 240340 | 489 | 63 | 491
TA∗ $(n=4)$ | 244 | 5E21 | ${<}1s$ | 1 | 1204628 | 489 | 373 | TO
TS ($h=(10,20)$) | 45 | 2E6 | ${<}1s$ | 1 | 12825 | 91 | 4 | ${<}1s$
PC ($s=0\dots 4$) | 20 | 3E9 |  TO(8%) | 452k | 6780 | 41 | 7 | ${<}1s$
Table 2: Comparison on HyperProb benchmarks. * denotes a more complicated
variant not considered in [18]. For more details, see Appendix 0.B.

Table 2 reports for each benchmark the size of the underlying MDP and the main
performance statistics of the proposed AR loop and HyperProb, respectively.
For AR loop, it reports the size of the family $\mathcal{R}$, the run-time and
the number of AR iterations (the number of investigated sub-families of
$\mathcal{R})$. For HyperProb, it reports the number of variables (vars) and
subformulae (sub) in the SMT encoding, together with the encoding time
(e-time) and the time to solve the formula (s-time).

We can observe that the first three case studies are trivial for the AR loop
as only a single iteration is required to find a counter-example that
disproves the specification. On the other hand, HyperProb has to construct and
solve non-trivial SMT formulae and, in some cases, fails to do so within the
1-hour timeout. The situation is very different for PC. HyperProb is able to
quickly find the solution due to the manageable size and compact structure of
the underlying SMT encoding. On the other hand, the AR loop fails to find a
valid solution (within the timeout it explores only 8% or the family members).
A deeper investigation indicates that, in this case, the current splitting
strategy is not effective.

These results are quite encouraging as they show that the proposed approach
can almost trivially solve a number of relevant verification problems
considered in the literature. On the other hand, they do not provide insight
into the performance of our approach because the very coarse abstraction is
already sufficient to find a satisfying solution. In the following section, we
consider synthesis problems that are principally much harder for our approach.

#### Stochastic Domination (SD)

[11] is a relation property that has been introduced for random variables. We
adapt it to the reachability problem in MDPs. We say that state $s_{2}$
_dominates_ state $s_{1}$ with respect to the target set $T$ if, for all
controllers $\sigma_{i}\in\Sigma^{M}$, it holds that
$\mathbb{P}(M^{\sigma},s_{1}\models\Diamond
T)>\mathbb{P}(M^{\sigma},s_{2}\models\Diamond T)$. To verify SD, we consider
synthesis of a counterexample, i.e. a controller proving that $s_{2}$ does not
dominate $s_{1}$ formulated using the following hyperproperty:

$\exists\,\sigma:\forall s_{1}\in\\{s_{a}\\}[\sigma]\,\forall
s_{2}\in\\{s_{b}\\}[\sigma]\;\,:\,\mathbb{P}(M^{\sigma},{s_{1}}\models\Diamond
T)\geq\mathbb{P}(M^{\sigma},{s_{2}}\models\Diamond T).$

Maze | Feasible | MDP | AR loop | HyperProb
---|---|---|---|---
size | family | time | iters | vars | sub | e-time | s-time
simple | x | 10 | 16k | 1 | 1.5k | 590 | 21 | ${<}1s$ | 1
splash-1 | $\surd$ | 16 | 1E7 | ${<}1s$ | 63(10%) | 1424 | 33 | ${<}1s$ | 50
larger-1 | $\surd$ | 25 | 3E11 | 177 | 171k(8%) | 3350 | 51 | 1 | TO
larger-2 | x | 25 | 7E10 | 443 | 442k | 3350 | 51 | 1 | TO
larger-3 | $\surd$ | 25 | 7E10 | ${<}1s$ | 119(10%) | 3350 | 51 | 1 | TO
splash-2 | x | 25 | 2E11 | 1731 | 1E6 | 3350 | 51 | ${<}1s$ | TO
train | x | 48 | 2E10 | 7 | 8.7k | 11952 | 97 | 3 | TO
Table 3: SD on different variants of maze problems.

We verify this specification against several variants of the problem from
Example 1, where we consider a robot navigating through a maze [34]. Due to
its faulty locomotion, after each step the robot may end up in a different
location than the one suggested by the controller. We assume full
observability of the maze, hence the controller uses the current state to
decide the next movement direction. Individual variants of the problem are
described in Appendix 0.B. Evaluation results are reported in Table 3, where
we explicitly report whether the problem is feasible. For feasible instances,
the column _iters_ also reports the portion of the family members explored
before the satisfying solution was found. Observe that HyperProb fails to
solve a majority of the problems within the 1-hour timeout, despite the fact
that the underlying SMT encoding is smaller comparing to the HyperProb
benchmarks investigated in Table 2. This is probably due to the fact that
these SD problems are either unfeasible or have only few satisfying solutions.
On the other hand, AR loop is able to solve all SD variants within the
timeout. Note that, although these benchmarks consider MDPs with tens of
states, the individual run-times differ significantly. This is because a
specific structure of the MDP can have a huge impact on the number of
iterations (splittings) required to obtain unambiguous cases.

Maze | AR loop | feasible
---|---|---
time | iters | instances
splash-1 | ${<}1s$ | 1233 |  1 ($\thicksim$0%)
larger-1 | 4771 | 4E6 |  4($\thicksim$0%)
larger-3 | 169 | 149k |  2590 ($\thicksim$0%)
Table 4: Complete synthesis for the feasible variants of the SD problem.

To further emphasise the capabilities as well as the limitations of the
proposed approach, we consider the _complete synthesis_ problem: instead of
synthesizing a single satisfying controller, we look for all controllers that
meet the specification, which requires exploration of the entire family. Note
that this problem is closely related to a construction of _permissive
controllers_ or _safety shields_ in the context of safe reinforcement learning
[21, 30]. Table 4 shows the performance of the AR loop as well as the number
of feasible instances. As expected, the complete synthesis for feasible
instances is significantly harder. Moreover, we observe that abstraction-based
pruning is typically less efficient comparing to the unfeasible instances. For
the variant larger-1, only 86% of the family members were explored in the
1-hour timeout (the entire exploration took 80 minutes). Complete synthesis is
also very challenging for the SMT approach since it requires multiple calls to
the SMT solver, where each subsequent call rules out the previously found
solution. HyperProb currently does not support complete synthesis.

### Q2 Synthesis under structural constraints

To investigate the performance of the proposed approach on more complicated
synthesis problems that include structural constraints on the resulting
controllers, we extend the robotic scenario from Example 1. We consider
_probabilistic noninterference_ [25] and _opacity_ [36], both ensuring
location privacy with respect to attacker observability. In both cases we
formulate the problem within a planning scenario in a maze. To demonstrate the
scalability with respect to the complexity of the underlying MDP, we consider
two larger variants of the maze, (see the MDP sizes in Table 5) and a more
complicated objective. The maze is equipped with checkpoint locations and the
robot earns a reward when repeatedly passing through at least two of these
locations. Hence, a good strategy makes the robot move back and forth among
two or more checkpoints. There are no traps, but every move has a small chance
of unrecoverable error. Additionally, we assume _partial observability_ \- the
robot can only observe the available directions (up, down, left, right). This
is encoded using intra-controller constraints
$\mathcal{O}_{S^{\prime}}(\sigma)$.

####  5.0.1 Probabilistic noninterference

is formulated as a 2-controller synthesis problem with two different initial
states that need to be kept private. We consider the specification containing
two PCTL properties requiring that both controllers achieve a reward exceeding
a minimum threshold $\lambda$ and a hyperproperty requiring that the achieved
values are almost the same (the attacker observes the final rewards).
Additionally, we define a set of sensitive states where both controllers have
to agree on their actions, encoded using inter-controller constraints
$\mathcal{X}_{s}(\Sigma)$. For both considered variants of the maze (larger-4
and larger-5), there is no pair of memoryless controllers that would satisfy
the specification with a non-zero threshold. In Table 5 (left) we report
experiments where threshold $\lambda$ is set to 0, already making the problem
unfeasible.

Furthermore, we enhance both MDPs with a 1-bit memory (denoted by suffix
+mem). A controller can now properly use the memory to distinguish between
otherwise indistinguishable states. With this extension, it is possible to
find 2-controllers satisfying probabilistic noninterference with non-zero
rewards. In the corresponding experiments in Table 5, the reward thresholds
$\lambda$ are set close (but not equal) to the respective maximal values. This
makes the PCTL part of the specification satisfiable, but the overall
specification unfeasible. This allows us to inspect how the hyperproperty is
leveraged to explore the entire search space. The results show that adding the
1-bit memory enormously enlarges the family size; however, the AR loop is
still able to fully explore the family in a reasonable time. Exploring the
family of 2-bit controllers is not tractable within the 1-hour timeout.

Maze | MDP | Noninterference | Opacity
---|---|---|---
size | family | time | iters | family | time | iters | distance
larger-4 | 434 | 221k | 1 | 337 | 3E9 | ${<}1s$ | 96 | 6/13
larger-5 | 1260 | 3E6 | ${<}1s$ | 7 | 5E11 | ${<}1s$ | 43 | 8/15
larger-4+mem | 866 | 8E20 | 1551 | 110K | 2E38 | 193 | 13k | 32/32
larger-5+mem | 2520 | 1E25 | 481 | 16k | 2E46 | 309 | 9k | 22/38
Table 5: Probabilistic Noninterference and Opacity specifications for more
complex variants of the maze problem.

####  5.0.2 Opacity

is a hyperproperty, used in non-probabilistic robot planning, specifying that
for a given state there exist two different paths that both give identical
observations to the attacker and reach the planning goal. We adapt opacity to
our setting in the following way. For a given initial state, we seek for two
controllers that i) achieve an expected reward above a threshold (performance
requirement), ii) achieve almost the same reward visible to the attacker
(anonymity requirement) and iii) take as many mutually different choices as
possible. If the two controllers are indistinguishable for the attacker and
yet do not agree on any choice, then anonymisation is fully guaranteed. We
encode the last objective as an optimisation over the intra-controller
characteristic, further denoted as _distance_ , where we maximise the number
of different choices.

In order to effectively search for the _optimal_ $n$-controller wrt. such a
specification, we need to completely explore the family $\mathcal{R}$. We
extend the AR loop to use the distance of the current optimum to improve the
pruning strategy: if the current sub-family does not include improving
solutions wrt. currently optimal distance, it is promptly pruned without
analysing the MDPs wrt. performance and anonymity properties. This way, we
extend the deductive reasoning over the families using an additional
structural constraint that iteratively changes during the synthesis process.

Table 5 (right) reports the results for memoryless and 1-bit controllers,
respectively. The last column reports the obtained maximal distance and the
number of choices that need to be synthesised per controller. Note that, due
to partial observability, there are fewer choices than states. We see again
that adding memory makes the synthesis problem much harder. On the other hand,
the memory not only allows us to significantly increase the threshold on the
reward, but also improves the achieved distance, i.e. the degree of
anonymisation. For the variant larger-4+mem, we synthesized a pair of
controllers that differ in all 32 choices, thus ensuring full anonymisation.

##  6 Conclusions

We proposed a deductive controller synthesis procedure for MDPs with respect
to probabilistic hyperproperties expressed in HyperPCTL enriched with
additional structural constraints on the resulting controllers. Our approach
builds on a symbolic representation of the family of the controllers and an
abstraction refinement strategy allowing for an effective exploration of the
families. A detailed experimental evaluation demonstrates that our approach
considerably outperforms HyperProb [18], a state-of-the-art tool based on SMT
reasoning. In particular, our approach scales to more complicated synthesis
problems where HyperProb times out, and, for the first time, effectively
supports in the synthesis procedure structural constraints on the resulting
controllers. As future work, we plan to improve our approach by investigating
counterexamples for probabilistic hyperproperties.

## References

  * [1] Ábrahám, E., Bartocci, E., Bonakdarpour, B., Dobe, O.: Parameter synthesis for probabilistic hyperproperties. In: LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, vol. 73, pp. 12–31. EasyChair (2020). https://doi.org/10.29007/37lf
  * [2] Ábrahám, E., Bartocci, E., Bonakdarpour, B., Dobe, O.: Probabilistic hyperproperties with nondeterminism. In: Proc. of ATVA 2019: the 17th International Symposium on Automated Technology for Verification and Analysis. LNCS, vol. 12302, pp. 518–534. Springer (2020). https://doi.org/10.1007/978-3-030-59152-6_29
  * [3] Ábrahám, E., Bonakdarpour, B.: HyperPCTL: A temporal logic for probabilistic hyperproperties. In: Proc. of QEST 2018: the 15th International Conference on Quantitative Evaluation of Systems. LNCS, vol. 11024, pp. 20–35. Springer (2018). https://doi.org/10.1007/978-3-319-99154-2_2
  * [4] Andriushchenko, R., Ceska, M., Junges, S., Katoen, J.: Inductive synthesis for probabilistic programs reaches new horizons. In: Proc. of TACAS 2021: the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 12651, pp. 191–209. Springer (2021). https://doi.org/10.1007/978-3-030-72016-2_11
  * [5] Andriushchenko, R., Ceska, M., Junges, S., Katoen, J.: Inductive synthesis of finite-state controllers for pomdps. In: Proc. of UAI 2022: the Thirty-Eighth Conference on Uncertainty in Artificial Intelligence. Proceedings of Machine Learning Research, vol. 180, pp. 85–95. PMLR (2022)
  * [6] Andriushchenko, R., Ceska, M., Junges, S., Katoen, J., Stupinský, S.: PAYNT: A tool for inductive synthesis of probabilistic programs. In: Proc. of CAV 2021: the 33rd International Conference on Computer Aided Verification. LNCS, vol. 12759, pp. 856–869. Springer (2021). https://doi.org/10.1007/978-3-030-81685-8_40
  * [7] Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Handbook of Model Checking, pp. 963–999. Springer (2018). https://doi.org/10.1007/978-3-319-10575-8_28
  * [8] Baier, C., Funke, F., Piribauer, J., Ziemek, R.: On probability-raising causality in Markov decision processes. In: Proc. of FoSSaCS 2022: the 25th Internat. Conference on Foundations of Software Science and Computation Structures. LNCS, vol. 13242, pp. 40–60. Springer (2022). https://doi.org/10.1007/978-3-030-99253-8_3
  * [9] Baier, C., Größer, M., Leucker, M., Bollig, B., Ciesinski, F.: Controller synthesis for probabilistic systems. In: Exploring New Frontiers of Theoretical Informatics, IFIP 18th World Computer Congress, TC1 3rd International Conference on Theoretical Computer Science (TCS2004). IFIP, vol. 155, pp. 493–506. Kluwer/Springer (2004). https://doi.org/10.1007/1-4020-8141-3_38
  * [10] Baier, C., Katoen, J.: Principles of model checking. MIT Press (2008)
  * [11] Barthe, G., Hsu, J.: Probabilistic Couplings from Program Logics, p. 145–184. Cambridge University Press (2020). https://doi.org/10.1017/9781108770750.006
  * [12] Beutner, R., Finkbeiner, B.: Software verification of hyperproperties beyond k-safety. In: Proc. of CAV 2022: the 34th International Conference on Computer Aided Verification. LNCS, vol. 13371, pp. 341–362. Springer (2022). https://doi.org/10.1007/978-3-031-13185-1_17
  * [13] Bonakdarpour, B., Finkbeiner, B.: Controller synthesis for hyperproperties. In: 33rd IEEE Computer Security Foundations Symposium. pp. 366–379. IEEE (2020). https://doi.org/10.1109/CSF49147.2020.00033
  * [14] Ceska, M., Jansen, N., Junges, S., Katoen, J.: Shepherding hordes of markov chains. In: Proc. of TACAS 2019: the 25th Internat. Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 11428, pp. 172–190. Springer (2019). https://doi.org/10.1007/978-3-030-17465-1_10
  * [15] Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., Sánchez, C.: Temporal logics for hyperproperties. In: Proc. of POST 2014: Principles of Security and Trust. Lecture Notes in Computer Science, vol. 8414, pp. 265–284. Springer (2014). https://doi.org/10.1007/978-3-642-54792-8_15
  * [16] Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157–1210 (2010). https://doi.org/10.3233/JCS-2009-0393
  * [17] Dimitrova, R., Finkbeiner, B., Torfah, H.: Probabilistic hyperproperties of Markov decision processes. In: Proc. of ATVA 2020: the 18th International Symposium on Automated Technology for Verification and Analysis. LNCS, vol. 12302, pp. 484–500. Springer (2020). https://doi.org/10.1007/978-3-030-59152-6_27
  * [18] Dobe, O., Ábrahám, E., Bartocci, E., Bonakdarpour, B.: HyperProb: A model checker for probabilistic hyperproperties. In: Proc. of FM 2021: the 24th International Symposium on Formal Methods. LNCS, vol. 13047, pp. 657–666. Springer (2021). https://doi.org/10.1007/978-3-030-90870-6_35
  * [19] Dobe, O., Wilke, L., Ábrahám, E., Bartocci, E., Bonakdarpour, B.: Probabilistic hyperproperties with rewards. In: Proc. of NFM 2022: the 14th International Symposium on NASA Formal Methods. LNCS, vol. 13260, pp. 656–673. Springer (2022). https://doi.org/10.1007/978-3-319-11936-6_11
  * [20] Dobe, O., Ábrahám, E., Bartocci, E., Bonakdarpour, B.: Model checking hyperproperties for markov decision processes. Information and Computation 289, 104978 (2022). https://doi.org/10.1016/j.ic.2022.104978
  * [21] Dräger, K., Forejt, V., Kwiatkowska, M., Parker, D., Ujma, M.: Permissive controller synthesis for probabilistic systems. In: Proc. of TACAS 2014: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 531–546. Springer (2014)
  * [22] Dwork, C.: Differential privacy. In: Proc. of ICALP (2) 2006: the 33rd International Colloquium on Automata, Languages and Programming. LNCS, vol. 4052, pp. 1–12. Springer (2006). https://doi.org/10.1007/11787006_1
  * [23] Finkbeiner, B., Hahn, C., Lukert, P., Stenger, M., Tentrup, L.: Synthesizing reactive systems from hyperproperties. In: Computer Aided Verification - 30th International Conference, CAV. Lecture Notes in Computer Science, vol. 10981, pp. 289–306. Springer (2018). https://doi.org/10.1007/978-3-319-96145-3_16
  * [24] Finkbeiner, B., Hahn, C., Lukert, P., Stenger, M., Tentrup, L.: Synthesis from hyperproperties. Acta Informatica 57(1-2), 137–163 (2020). https://doi.org/10.1007/s00236-019-00358-2
  * [25] Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy. pp. 11–20. IEEE Computer Society (1982)
  * [26] Gray, J.W., Syverson, P.F.: A logical approach to multilevel security of probabilistic systems. Distributed Comput. 11(2), 73–90 (1998). https://doi.org/10.1007/s004460050043
  * [27] Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512–535 (1994). https://doi.org/10.1007/BF01211866
  * [28] Hensel, C., Junges, S., Katoen, J., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Transf. 24(4), 589–610 (2022). https://doi.org/10.1007/s10009-021-00633-z
  * [29] Hsu, T., Bonakdarpour, B., Kang, E., Tripakis, S.: Mapping synthesis for hyperproperties. In: 35th IEEE Computer Security Foundations Symposium, CSF 2022, Haifa, Israel, August 7-10, 2022. pp. 486–500. IEEE. https://doi.org/10.1109/CSF54842.2022.9919679
  * [30] Jansen, N., Könighofer, B., Junges, S., Serban, A., Bloem, R.: Safe Reinforcement Learning Using Probabilistic Shields (Invited Paper). In: Proc. of CONCUR 2020: International Conference on Concurrency Theory. Leibniz International Proceedings in Informatics (LIPIcs), vol. 171, pp. 1–16 (2020). https://doi.org/10.4230/LIPIcs.CONCUR.2020.3
  * [31] Köpf, B., Basin, D.A.: An information-theoretic model for adaptive side-channel attacks. In: Proceedings of the 2007 ACM Conference on Computer and Communications Security (CCS). pp. 286–296. ACM (2007). https://doi.org/10.1145/1315245.1315282
  * [32] Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Proc. of CAV 2011: the 23rd International Conference on Computer Aided Verification. LNCS, vol. 6806, pp. 585–591. Springer (2011). https://doi.org/10.1007/978-3-642-22110-1_47
  * [33] Ngo, T.M., Stoelinga, M., Huisman, M.: Confidentiality for probabilistic multi-threaded programs and its verification. In: Proc. of ESSoS 2013: the 5th International Symposium on Engineering Secure Software and Systems. LNCS, vol. 7781, pp. 107–122. Springer (2013). https://doi.org/10.1145/1315245.1315282
  * [34] Norman, G., Parker, D., Zou, X.: Verification and control of partially observable probabilistic real-time systems. In: Formal Modeling and Analysis of Timed Systems - 13th International Conference, FORMATS 2015, Madrid, Spain, September 2-4, 2015, Proceedings. Lecture Notes in Computer Science, vol. 9268, pp. 240–255. Springer (2015). https://doi.org/10.1007/978-3-319-22975-1_16
  * [35] O’Neill, K.R., Clarkson, M.R., Chong, S.: Information-flow security for interactive programs. In: Proc. of CSFW: the 19th IEEE Computer Security Foundations Workshop. pp. 190–201. IEEE Computer Society (2006). https://doi.org/10.1109/CSFW.2006.16
  * [36] Wang, Y., Nalluri, S., Pajic, M.: Hyperproperties for robotics: Planning via hyperLTL. In: Proc of ICRA: the 2020 IEEE International Conference on Robotics and Automation. pp. 8462–8468. IEEE (2020). https://doi.org/10.1109/ICRA40945.2020.9196874
  * [37] Zaman, E., Ciardo, G., Ábrahám, E., Bonakdarpour, B.: HyperPCTL model checking by probabilistic decomposition. In: Proc. of IFM 2022: the 17th International Conference on Integrated Formal Methods. LNCS, vol. 13274, pp. 209–226. Springer (2022). https://doi.org/10.1007/978-3-031-07727-2_12

##  Appendix 0.A Selecting a conflicting parameter

Let $\mathcal{C}\subseteq\mathcal{K}$ denote the set of conflicting parameters
in minimizing or maximizing controller $\sigma$. For the purpose of splitting,
we wish to identify a single parameter $k^{*}\in\mathcal{C}$ that will produce
sub-families $\\{\mathcal{R}_{X}\\}_{X\in\mathfrak{X}}$ that are more likely
to fall into cases (1) or (2). Since predicting the exact analysis of
resulting sub-families is impossible, we propose the following heuristics
based on the results of the model check queries. For a probability constraint,
we introduce the _immediate impact_ of action $a$ in state $s$:

$\gamma(s,a)\coloneqq
exp(s)\cdot\Big{[}\sum_{s^{\prime}}\mathcal{P}(s,\alpha,s^{\prime})\cdot\mathbb{P}(M^{\sigma},s^{\prime}\models\Diamond
T)\Big{]},$

where $exp(s)$ is the expected number of visits of state $s$ in MC
$M^{\sigma}$. Likewise, for a reward constraint, we have:

$\gamma(s,a)\coloneqq
exp(s)\cdot\Big{[}rew(s,\alpha)+\sum_{s^{\prime}}\mathcal{P}(s,\alpha,s^{\prime})\cdot\mathbb{R}({M^{\sigma},s^{\prime}\models\Diamond
T})\Big{]},$

where $rew(s,a)$ denotes the reward associated with executing $a$ in $s$.
After having computed the immediate impact for each state $s\in S$ and action
$a\in Act$, the parameter with the highest average range of $\gamma$ is
selected for splitting:

$k^{*}\in\operatorname*{arg\,max}_{k\in\mathcal{C}}\operatorname*{avg}_{s\in\mathcal{S}_{k}}\left\\{\max_{a\in\mathcal{A}_{k}}\gamma(s,a)-\min_{a\in\mathcal{A}_{k}}\gamma(s,a)\right\\}.$

##  Appendix 0.B Short description of the experimental models

###  0.B.1 Models from [18]

Intuitively, TA and PW both require that for every nondeterministically-chosen
value of a secret (also called _high input_), the programs have the same
distribution over the set of measurable execution times (the _low output_).
This ensures the absence of _timing side channels_ that may disclosure
information about the sensitive input. On the other hand, TS, expresses the
_scheduler-specific probabilistic observational determinism_
($\mathsf{SSPOD}$) [33] hyperproperty: given a probabilistic multi-threaded
program, and a specific set of probabilistic schedulers under investigation,
any pair of executions from two low-equivalent initial states (i.e., states
that are indistinguishable with respect to the input secret information)
should terminate in low-equivalent states (i.e., produce the same output) with
equal probabilities. Finally, the PC seeks for a scheduler that induces a DTMC
which simulates the outcomes of 6-sided die (specified as a DTMC) using a fair
coin. The first three case studies are formulated as _verification_ problems
and thus we consider the dual formulation, i.e., _synthesis of a counter-
example_.

We report the results for selected instances of the case studies. Parameter
$n$ determines the number of bits representing the secret, and hence the set
of observable execution times. In [18], models up to $n=4$ are considered.
While replicating the experiments from the original benchmark, we also report
on two variants (PW${}^{*}(n=4)$ and TA${}^{*}(n=4)$) where the full set of
observable outputs is constrained. Despite having the same model, these
variants are significantly harder to solve due to a more complex (viz.
lengthier) specification. In TS, $h$ is a variable representing the secret.
Every instance of TS analyzes the same problem for the given two different
values of the secret. In PC, $s$ indicates the states where appropriate
actions have to be synthesized.

###  0.B.2 Models from SD Case Study

The simple model is the Maze presented as first Case Study in [6]. larger-1,
larger-2 and larger-3 are 5x5 Mazes, equipped with different sets of trap
states and different initial states. splash-1 and splash-2, resp. 4x4 and 5x5
Mazes, include some states with a high probability of error with respect to
the chosen direction. This increases the variance between the success
probabilities of different paths, hence it makes the planning problem harder.
Finally, in train (7x7) there are some fixed paths that, if taken, forbid the
robot to go back.


# Elastic properties and phase stability of AgBr under pressure.

P.T. Jochym<EMAIL_ADDRESS>K. Parlinski  Institute of Nuclear
Physics,
ul. Radzikowskiego 152, 31–342 Cracow, Poland

###### Abstract

Ab initio calculations have been used to derive the elastic constants,
equation of state and free energy of NaCl, KOH and CsCl-type structures of
AgBr. The elastic constants have been derived by the stress–strain relation.
The shear elastic constants C44 has proved to be exceptionally soft. We have
found that at temperature T=0 the phase transition from the low pressure NaCl-
type to the high-pressure CsCl-type structure goes over a monoclinic KOH-type
structure. The free energy comparison indicates that the monoclinic phase
ranges from 8 to 35 GPa.

###### pacs:

05.70.F, 64.60, 64.70, 71.15.Mb

Silver halide crystals are of considerable interest, since they exhibit
deviation from the ideal ionic character due to the presence of the
d-electrons in Ag+ ions. Numerous studies of these crystals have been
undertaken in the past years using various forms of interaction potentials
including three-body interactions and van der Waals forces,singh ; gupta  as
well as the ab initio total energy pseudopotential calculations.chelikowsky
There are also many experimental works studying various aspects of these
solids.loje ; bridgmanA ; bridgmanB ; slykhouse ; vaidya ; fjeldly ; mellander
; ves  The results of studies using phenomenological potentials generally show
good agreement with experiment.gupta  This studies use sophisticated schemes
involving three body interactions and van der Waals potentials. The ab initio
results for transition pressure seems to be less accuratechelikowsky . There
is one ab initio study of phase stability of silver bromide AgBr.nunes
Nevertheless, the transition mechanism is still unclear for this compound.
Several models have been proposed, bridgmanA ; bridgmanB ; slykhouse ; nunes ;
hull ; kusaba ; schock  but the transition mechanism remains still an open
problem. The ab initio study by Nunes, Allen and Martins,nunes  which
investigated the energy of several candidate structures, proposed an
intermediate trigonal phase with space group P$3_{1}21$. In contrary recent
experimental work of Hull and Keenhull  suggested an existence of an
intermediate phase with a monoclinic, KOH-type structure and shear instability
as the transition mechanism. The silver bromide AgBr is stable at ambient
temperature and pressure in the rocksalt structure Fm$\bar{3}$m. In ambient
temperature and high pressures it has a second stable phase with CsCl
structure Pm$\bar{3}$m. The phase transition in between these phases has been
reportedbridgmanB ; slykhouse ; bassett ; riggleman  to occur at Pt=8.3 GPa.
In this paper we are studying elastic properties and phase stability of the
AgBr as a function of pressure. For NaCl and CsCl structures we have scanned
pressures in the interval P=0–200 GPa, and calculated the free energies and
elastic constants. In the range of P=0–40 GPa we have also studied the phase
stability of the free, non-constrained by any symmetry, AgBr crystal ,
searching for any intermediate phases as well as general transition mechanism.
The non-constrained crystal was treated as having P1 symmetry, however, its
unit cell content was not allowed to change. Hence, phase transitions to
phases with multiplication unit cells were not taken into account.

##  I Methodology

The calculations have been performed using Density Functional Theory (DFT)
approach with ultrasoft pseudopotentials and Generalised Gradient
Approximation (GGA).lin ; goniakowski ; payene  We have used CASTEPcastep
implementation of this method and pseudopotentials provided with this package.
The elastic constants of the NaCl phase have been also verified by the
independent calculation using VASPvasp . The electronic minimisation used
density mixing scheme and pseudopotentials parametrised in the reciprocal
space. The summation over the Brillouin zone has been performed with weighted
summation over wave vectors generated by Monkhorst-Pack scheme.pack  All
computations were done in $1$$\times$$1$$\times$$1$ supercell with 8 or 2 or 8
atoms for NaCl or CsCl or KOH structures, respectively. Some tests for NaCl
has been carried out on the primitive, others on the face–centered cubic unit
cell.

Due to high demands of the accuracy of the free energy, we have conducted
extensive tests of convergence of the energy and pressure with respect to
energy cutoff and Brillouin zone grid spacing parameters. Thus, we have
performed a series of calculations with cutoff energies in the range of
$E_{cut}$=300 – 450eV and k-space grid spacing in the range $\Delta$k=0.02 –
0.1 Å-1. In the light of obtained results we have decided to use in our
computations a 0.4 Å-1 grid spacing and 340eV energy cutoff. The chosen grid
corresponds to 32 wave-vectors for NaCl structure and 256 wave-vectors for
CsCl structure. Such a large number of wave-vectors made calculations rather
time-consuming. But since we are comparing energies of different structures
with different unit cell volumes and Brillouin zone shapes, sizes and
k-sampling, we need a very good convergence of energy. At zero pressure the
lattice constants of the optimised NaCl structure is a= 5.7859 Å, while the
experimental lattice constants at P=0 GPa and T=300 K is A=5.7745 Å.

##  II Free Energy and Equation of State

Figure 1: Lower part: Free energy of AgBr in NaCl (+, solid line) and CsCl
($\times$, dashed line) structures. Upper part: Free energy difference
F${}_{\mathrm{C}sCl}-$GNaCl between CsCl and NaCl structures as a function of
pressure. The vertical arrow denotes predicted phase transition pressure.

To investigate the phase stability of the crystal and to estimate the phase
transition pressure, one must evaluate the free energy of all involved phases
and choose the one with the lowest energy as stable. Since in ab initio
calculations the temperature T=0, the free energy is: $F=E+PV$. We have
performed calculations of the crystal free energy $F$ for several pressures
from 0 to 50 GPa for both NaCl and CsCl structures. Fig 1 shows the results of
these computations. In the lower part the absolute values of free energies per
atom are plotted together with cubic polynomials fitted to these data. In the
upper part the difference of $F_{CsCl}-F_{NaCl}$ is plotted against pressure.
The difference changes sign at the pressure Pt=27 GPa (arrow). We see that our
calculations correctly predict that the rocksalt structure is more stable at
low pressure and that at higher pressures the stability passes to CsCl
structure . The large difference between experimental Pt=8.3 GPa and
calculated Pt=27 GPa transition pressure could be attributed to a few factors.
The main reason could be related to the appearance of the intermediate KOH-
type structure, discussed below. Here, we mention other possible factors.
First, the experimental data bridgmanA ; bridgmanB  are measured only at
ambient temperature, while the calculations were performed at T=0. At finite
temperature the entropy contribution to the Gibbs free energy $G=E+PV-TS$ can
also be different for the two structures, since the closest coordination
shells contain different number of ions. Another reason could be related to
the fact that the van der Waals interaction is neglected in DFT calculations,
and that leads to under-binding of the crystal. This effect has already been
noticed for silver iodide AgI crystal, where DFT predicts the phase transition
pressure to be 10 GPa,gupta ; chelikowsky  while experimentally it is 4 GPa.

Figure 2: Variation of relative volumes with pressure for NaCl(+) and CsCl
($\times$) structure. Experimental points ($\bullet,\blacktriangle$) are taken
from BridgmanbridgmanA ; bridgmanB  and Vaidyavaidya  respectively. The dashed
line shows results of theoretical study of Gupta and Singh gupta . The lines
are present calculations.

The data used to calculate free energy provide also the equation of state of
the crystals. Fig. 2 shows the calculated equation of state for NaCl and CsCl
structures as well as the experimental data measured by Bridgman and
Vaidya.bridgmanA ; bridgmanB ; vaidya  We have also included in figure 2 the
results of phenomenological study of Gupta and Singh.gupta  This work was able
to predict the transition pressure much better, but it fails to reproduce the
volume compression of the phase transition. Present calculations show
excellent agreement with experimental data for the low pressure range up to 6
GPa. In this interval the relative error in V(P)/V(0) ratio is below 0.5%. It
should be noted that the Bridgman measurements, are limited to 10 GPa and it
would be interesting to increase the pressures to at least 15 GPa. We have
also fitted the Murnaghan equation of state to rocksalt structure data below
15 GPa:

$V=V_{0}\exp\left[-\frac{\ln\left(\frac{PA_{2}}{A_{1}}+1\right)}{A_{2}}\right]$
(1)

achieving good fit for $A_{1}$=41.01 GPa and $A_{2}$=4.35.

As seen from Fig. 2 the calculated relative volume change from NaCl to CsCl
structure at the transition pressure Pt=8.3 GPa is a 6% compression. We are
not aware of any experimental measurements of this value, however, we can
estimate it from the Bridgman databridgmanB  to be at least 3%.

##  III Elastic constants

Figure 3: Bulk modulus of AgBr calculated for NaCl structure from $P(V)$
function (solid line) and $c_{ij}$ data (+) from Fig. 4. The bulk modulus for
CsCl structure is calculated from $P(V)$ function (dashed line) and from
$c_{ij}$ data ($\times$) as well. Experimental data for T=195 K ($\circ$) and
T=300 K ($\Box$) are taken from Lojeloje . The dotted lines denote
experimental pressure derivatives of B at zero pressure.

The behaviour of elastic properties of the AgBr is specially interesting in
the vicinity of the phase transition. Fig. 3 shows pressure dependence of the
bulk modulus as calculated from the equation of state, as well as from the
following relationship with elastic constants:

$B=-V\frac{\partial P(V)}{\partial V}=\frac{1}{3}(c_{11}+2c_{12})$ (2)

The difference in the bulk modulus B between NaCl and CsCl structures is quite
small. On the same figure 3 we have included two dotted lines showing
experimental pressure derivatives of the bulk modulus at P=0 and T=195 K and
T=300 K.loje  From these data we see that our calculations reproduce the
experimental bulk modulus quite well and that the results from different
methods are consistent within 10% .

We have used the standard stress–strain relationship to derive all three
elastic constants as a function of pressure. The method is based on
constructing a set of linear equations from stress–strain relationships for
several deformations of the unit cell. This set of equations represents a
general form of the Hook’s law and can be solved with respect to the elastic
constants. Since in practice this set of equations is over-determined, to
solve it we have used a singular value decomposition algorithm which
automatically provides a least squares solution of the setnumrec . For each
pressure three negative and three positive deformations of each kind, namely,
bulk, shear and tetragonal elongation, have been set up.

Figure 4: Elastic constants $c_{11}$, $c_{12}$, $c_{44}$ of AgBr in NaCl (solid lines and $\circ$, $\Box$, $\diamond$) and CsCl (dashed lines and $\vartriangle,\vartriangleleft,\triangledown$) structures respectively. The lines are cubic fits to the calculation data. The vertical solid arrow denotes predicted shear instability pressure. Table 1: Experimental and calculated bulk modulus $B$ and elastic constants $c_{ij}$ of the AgBr crystal, in GPa. Values in parenthesis are calculated from $B=\frac{1}{3}(c_{11}+2c_{12})$. Experimental data for T=195 K and T=300 K are taken from Lojeloje . Result | $B$ | $c_{11}$ | $c_{12}$ | $c_{44}$
---|---|---|---|---
Expt T=300 K | $40.5$ | $56.1$ | $32.7$ | $7.2$
Expt T=195 K | $43.81$ | $63.13$ | $34.14$ | $7.65$
Present | $(44.84)$ | $64.09$ | $35.21$ | $8.39$
$B=-V\partial P(V)/\partial V$ | $42.56$ |  |  |

Table 1 compares the calculated and experimental elastic constants at ambient
pressure and two temperatures: T=195 K and T=300 K. Present results show quite
good agreement with the measurements, although the calculations are performed
at T=0. The temperature data points allow to extrapolate the experimental
values to T=0. Thus, we have estimated that from T=195 K to T=0 K the elastic
constants might increase by about 5%. The mechanism of the phase transition
from NaCl to CsCl structure involves variation of the $c_{44}$ elastic
constant. We have calculated $c_{44}$ for both NaCl and CsCl structures and
for several pressures in the interval from 0 to 40 GPa . The results are shown
at Fig. 4. We can clearly see that the two lines representing the $c_{44}$
elastic constants , intersect at pressure P=21 GPa, and moreover at value
close to zero. The pressure P=21 GPa of the shear instability and P=27 GPa of
the free energy equality are not exactly the same. However, we shall see in
the next section that in this pressure interval another phase could be more
stable than the cubic NaCl or CsCl structures.

Figure 5: Relation between cubic NaCl and monoclinic KOH (left) and between
cubic CsCl and monoclinic KOH (right) unit cells. The KOH unit cell is drawn
with dashed lines.

In previous sections the calculation were performed for NaCl and CsCl
structures under constrains that both phases remain always cubic. Now, we
release this restrictions and allow the unit cell to deform to a structure of
P1 symmetry being intermediate configuration between the NaCl and CsCl ones.

##  IV Intermediate phase

Figure 6: Transition from NaCl to CsCl structure. Solid lines are guide to the
eye. Figure 7: Cell parameters in NaCl structure to CsCl structure transition
of AgBr. Solid lines are fourth degree fits to the data points.

When the intermediate configuration becomes monoclinic it resembles the KOH-
type structure. The relationship between NaCl, KOH and CsCl structures is
shown on Fig.5. Setting the monoclinic angle $\beta$=90∘ or $\beta$=125,27∘
one reestablishes the NaCl or CsCl structures, respectively. Hull and and
Keenhull  pointed out that this monoclinic phase, may provide a proper
transition path between NaCl and CsCl structures. A detailed study of the
above phase transition mechanism has been performed and we refer the results
below. We have prepared a model of the AgBr crystal in the KOH-type structure
with cell volume corresponding to the NaCl structure at P=0. The $\beta$ angle
of the monoclinic unit cell was set to 110∘. Then the crystal geometry
inducing atomic relaxations was optimised with respect to free energy for
various increasing pressures from 0 to 45 GPa.

Figure 8: Free energy difference in the transition of AgBr from NaCl (squares)
to CsCl structure (circles) through KOH structure (crosses). The polynomial
fit to the CsCl data points is taken as the reference line (zero level). The
lines are guide to the eye.

At each pressure the minimisation procedure was reiterated several times since
large changes in the unit cell size involved changes of the Brillouin zone
grid. The results are plotted in Fig 6. One notices that at about 8 GPa, there
is a clear tendency to depart from the pure NaCl structure to an intermediate
monoclinic structure. There is also a clear jump of lattice parameters at the
P=25–30 GPa range. Simultaneously, the $\alpha$, and $\gamma$ angles do not
change by more then 0.05∘ for the scanned pressure range. To verify the last
findings we have carried out two series of calculations each starting from the
same either low or high pressure configurations.

Table 2: Calculated elastic constants (in GPa) of the monoclinic, KOH-type structure of the AgBr under pressure of P=20 GPa. Pressure [GPa] | $c_{11}$ | $c_{22}$ | $c_{33}$ | $c_{12}$ | $c_{13}$ | $c_{23}$
---|---|---|---|---|---|---
$20$ | $156$ | $175$ | $229$ | $152$ | $84$ | $98$

The starting low and high pressure configurations were taken from optimised
monoclinic configurations at Plo=25 GPa or Phi=30 GPa, respectively. The
results are shown in Fig. 7. It is clear from this figure that both monoclinic
structures may show weak metastable behaviour. However, the energy difference
is small and it is possible that this effect will manifest itself only in low
temperatures.

Table 3: Calculated structural parameters of the intermediate KOH-type structure of the AgBr crystal. $P$ [GPa] |  $a$ [Å] |  $b$ [Å] |  $c$ [Å] |  $\beta$ [∘] | $b/a$ | $c/a$
---|---|---|---|---|---|---
$0$ | $4.0803$ | $4.1064$ | $5.7601$ | $90.0$ | $1.006$ | $1.412$
$5$ | $3.9521$ | $3.9819$ | $5.5982$ | $89.9$ | $1.008$ | $1.417$
$10$ | $3.8226$ | $3.9411$ | $5.4886$ | $91.6$ | $1.031$ | $1.436$
$15$ | $3.7368$ | $3.9091$ | $5.4100$ | $96.1$ | $1.046$ | $1.448$
$20$ | $3.5445$ | $4.0156$ | $5.3589$ | $101.4$ | $1.133$ | $1.512$
$25$ | $3.4033$ | $4.1011$ | $5.3403$ | $107.0$ | $1.205$ | $1.569$
$30$ | $3.2993$ | $4.1976$ | $6.7106$ | $132.7$ | $1.272$ | $2.034$
$35$ | $3.2316$ | $4.2612$ | $6.2892$ | $130.4$ | $1.319$ | $1.946$
$40$ | $3.1725$ | $4.4554$ | $5.5465$ | $125.6$ | $1.404$ | $1.748$
$45$ | $3.1489$ | $4.4375$ | $5.4855$ | $125.5$ | $1.409$ | $1.742$

Furthermore, the energy of the high-pressure configuration is always above the
low-pressure one. Consequently, the high-pressure structure is probably never
present in the real crystal, and we will omit this structure from now on.
Difference of the free energy of the three optimised candidate structures
(NaCl, KOH, CsCl) are shown in Fig. 8. The polynomial fit to the CsCl free
energy data is taken as the reference line (“0” level). At zero pressure the
NaCl structure is the most stable one. When we increase the pressure above
about 8 GPa, the cubic symmetry is broken, the monoclinic angle $\beta$ starts
to increase and the monoclinic phase is favoured. At the special point at P=21
GPa, at which the shear elastic constants $c_{44}$ of NaCl and CsCl structure
vanish on the Fig. 4, the monoclinic phase is still the most stable one. Only
above P=35 GPa the CsCl structure becomes the most stable phase. However, for
the finite temperature case this might change, since the NaCl and CsCl
structures have different number of atoms in coordination shells and hence
different entropy terms in the Gibbs free energies. Since there are no low
temperature measurements of pressure dependent behaviour of the AgBr we cannot
compare the present results with experimental findings.

We have also, for completeness, calculated some elastic constants of the
intermediate KOH phase of the crystal. The monoclinic phase has 13 independent
elastic constants. However, due to the small energy difference between phases
connected by the shear deformation, only 6 of them can be calculated
accurately. The remaining 7 constants are too small and could be only
estimated to be below 10 GPa. This is quite expected result. The 6 large
elastic constants, calculated under pressure of P=20 GPa are presented in the
Table 2. The values are consistent with the values of elastic constants of
NaCl and CsCl structures depicted on the Fig. 4.

Summarising, our results support the hypothesis formulated by Hull and
Keen,hull  that the phase transition from NaCl to CsCl phase, goes through the
intermediate KOH-type, monoclinic structure.

##  V Conclusions

The present DFT calculations show that at temperature T=0 K the cubic NaCl and
CsCl-type structures of AgBr are stable at pressures 0–8 GPa and above 35 GPa,
respectively. Moreover, the calculation performed in constrains of these two
cubic structures permit to find the equation of state and the elastic
constants in the whole interesting range of pressures from 0 to 45 GPa. It is
interesting to see that the shear elastic constants $c_{44}$ for both phases
NaCl and CsCl vanish close to 21 GPa. The derived equation of state and the
elastic constants characterise properly the stable cubic phase, and
additionally can provide an useful estimations of similar quantities within
the intermediate monoclinic phase. The calculation of the elastic constants of
the monoclinic KOH phase showed that, due to the small energy difference
between phases, the KOH phase is very soft to shear deformations and its
elastic constants are consistent with the elastic constants of the other two
phases.

The study of the intermediate phase has been done without point symmetry
elements constraints. This means that any deformation of the simulated
supercell could have taken place. The only imposed limitation was the number
of atoms in the supercell. Due to this approach the supercell remained always
monoclinic (or cubic for special values of monoclinic angle $\beta$). The
values of the free energy of the three candidate phases indicate that the
monoclinic phase becomes the most stable one in the pressure interval from 8
to 35 GPa. This structure has previously been proposed to be the
transformation path between NaCl and CsCl-type phases. And indeed, the free
energy of the intermediate monoclinic phase seems to be lower then these of
the cubic ones. However the difference in energy is quite small, which means
that defects and impurities present in the crystal could show a large impact
on the monoclinic phase.

###### Acknowledgements.

The use of facilities of the ACC “Cyfronet”, Cracow, where the calculations
have been done, are kindly acknowledged. This work was partially supported by
the Polish State Committee of Scientific Research (KBN), grant No 2 PO3B 004
14, and computational grant No. KBN/SGI_ORIGIN_2000/IFJ/128/1998.

## References

  * (1) R.K. Singh, P. Khare, phys. stat. sol. (b) 103, 337 (1981)
  * (2) D.C. Gupta and R.K. Singh, Phys. Rev. B, 43 11185 (1991).
  * (3) J.R. Chelikowsky, Phys. Rev. B 35, 1174 (1987)
  * (4) K.F. Loje and D.E. Schuele, J. Phys. Chem. Solids, 31 2051 (1970).
  * (5) P.W. Bridgman, Proc. Am. Acad. Arts Sci., 74, 21 (1940)
  * (6) P.W. Bridgman, Proc. Am. Acad. Arts Sci., 76, 1 (1945)
  * (7) T.E. Slykhouse and H.G. Drickamer, J. Phys. Chem. Solids 7, 207 (1958)
  * (8) W.A. Bassett and T. Takahashi, Am. Mineral. 50, 1576 (1965)
  * (9) B.M. Riggleman and H.G. Drickamer, J. Chem. Phys. 38, 2721 (1963)
  * (10) S.N. Vaidya and G.C. Kennedy, J. Phys. Chem. Solids, 32 951 (1971)
  * (11) T.A. Fjeldly and R.C. Hanson, Phys. Rev. B 10 3569 (1974)
  * (12) B.E. Mellander, Phys. Rev. B 26 5886 (1982)
  * (13) S. Ves, D. Glötzel, M. Cardona and H. Overhof, Phys. Rev. B 24 3073 (1981)
  * (14) G.S. Nunes, P.B. Allen, J.L. Martins, Phys. Rev. B 57, 5098 (1998)
  * (15) S. Hull, D.A. Keen, Phys. Rev. B 59, 750 (1999)
  * (16) K. Kusaba, Y. Syono, T. Kikegawa, O. Shimomura, J. Phys. Chem. Solids 56, 751 (1995)
  * (17) R.N. Schock and J.C. Jamieson, J. Phys. Chem. Solids 30, 1527 (1969)
  * (18) J.S. Lin, A. Qteish, M.C. Payne and V. Heine, Phys. Rev. B 47, 4174 (1993).
  * (19) J. Goniakowski, J.M. Holender, L.N. Kantorovich, M.J. Gillan and J.A. White, Phys. Rev. B 53, 957 (1996).
  * (20) M.C. Payene, M.P. Teter, D.C. Allan, T.A. Arias, J.D. Joannopoulos, Rev. of Mod. Phys. 64, 1045 (1992)
  * (21) CASTEP is a part of $Cerius^{2}$ system developed by Molecular Simulations.
  * (22) G. Kresse and J. Furthmüller, VASP program, Vienna (1999); Phys. Rev. B 54, 11169 (1996); Comput. Mat. Science 6, 15 (1996).
  * (23) H.J. Monkhorst and J.D. Pack, Phys. Rev. B 13, 5188 (1976).
  * (24) S. Froyen, M.L. Cohen, J. of Phys. C: Solid State Physics, 19, 2623 (1986).
  * (25) S. Froyen, M.L. Cohen, Phys. Rev. 29, 3770 (1984).
  * (26) W. H. Press, B.P. Flamery, S.A. Tenkolsky, and W.T. Vetterling, Numerical Recipes (Cambridge Univ. Press, 1988), p.301