  Probabilistic model checking is a useful technique for specifying and
verifying properties of stochastic systems including randomized protocols and
reinforcement learning models. Existing methods rely on the assumed structure
and probabilities of certain system transitions. These assumptions may be
incorrect, and may even be violated by an adversary who gains control of system
components.
  In this paper, we develop a formal framework for adversarial robustness in
systems modeled as discrete time Markov chains (DTMCs). We base our framework
on existing methods for verifying probabilistic temporal logic properties and
extend it to include deterministic, memoryless policies acting in Markov
decision processes (MDPs). Our framework includes a flexible approach for
specifying structure-preserving and non structure-preserving adversarial
models. We outline a class of threat models under which adversaries can perturb
system transitions, constrained by an $\varepsilon$ ball around the original
transition probabilities.
  We define three main DTMC adversarial robustness problems: adversarial
robustness verification, maximal $\delta$ synthesis, and worst case attack
synthesis. We present two optimization-based solutions to these three problems,
leveraging traditional and parametric probabilistic model checking techniques.
We then evaluate our solutions on two stochastic protocols and a collection of
Grid World case studies, which model an agent acting in an environment
described as an MDP. We find that the parametric solution results in fast
computation for small parameter spaces. In the case of less restrictive
(stronger) adversaries, the number of parameters increases, and directly
computing property satisfaction probabilities is more scalable. We demonstrate
the usefulness of our definitions and solutions by comparing system outcomes
over various properties, threat models, and case studies.
