text:
\section{Introduction}

\label{sec:intro}

The goal of program verification is to consolidate the user's trust that a given system works as intended, and if this is not the case, to provide her with useful diagnostic information.
Verification tools may, however, contain bugs and so a last grain of insecurity regarding their results always remains.
A widely acknowledged approach to overcome this dilemma has been made in the form of \emph{certifying algorithms}~\cite{BlumK95,McConnellMNS11}. These algorithms provide every result with an accompanying \emph{certificate}, i.e., a token that can be used to verify the result independently and with little ressources. In this way, certificates enable the user (or a third party) to quickly give a mathematically rigorous proof for the correctness of the result \emph{irrespective} of whether the algorithm itself works correctly.

\emph{Counterexamples}, i.e. certificates for the violation of a property, can often be obtained as a byproduct of verification procedures.
What constitutes a counterexample is highly context-dependent.
Finite executions suffice as counterexamples for safety properties and single, possibly infinite, executions are viable counterexamples for LTL~\cite{ClarkeV03}.
Tree-like counterexamples have been considered for fragments of CTL~\cite{ClarkeJLV02}. For a probabilistic system $\mathcal{M}$ and a linear time property $\phi$, the most prominent notion of counterexample to $\Pr_{\mathcal{M}}(\phi)< \lambda$ is a set of paths satisfying $\phi$ whose probability mass is at least $\lambda$ (see~\cite{AbrahamBDJKW14} for a survey).

Another notion of counterexample for probabilistic systems $\mathcal{M}$ and properties of the form $\Pr_{\mathcal{M}}(\phi)<  \lambda$ are \emph{critical subsystems}~\cite{AbrahamBDJKW14}.
We adopt the reverse perspective and call a subsystem $\mathcal{M}'$ of $\mathcal{M}$ a \emph{witnessing subsystem} for the property $\Pr_{\mathcal{M}}(\phi)\geq \lambda$ if $\Pr_{\mathcal{M}'}(\phi)\geq \lambda$. Small witnessing subsystems offer an insight into what parts of the system are responsible for the satisfaction of the property. Nonetheless, witnessing subsystems can hardly be regarded as viable certificates since verifying $\Pr_{\mathcal{M}'}(\phi)\geq \lambda$ is as hard as checking $\Pr_{\mathcal{M}}(\phi)\geq \lambda$ itself.

In this paper we build a solid bridge between certificates and witnessing subsystems. The systems we consider are modeled as Markov decision processes (MDP), which contain an absorbing goal state representing a desirable outcome. This approach is motivated by the fact that numerous model checking tasks can be reduced to reachability problems \cite{HartSP1983, Vardi1985, CourcoubetisY1995, CourcoubetisY1988, deAlfaro97, VardiW86}.

Using Farkas' Lemma, we introduce certificates for bounds on the minimal and maximal probability to reach the goal state.
We show that the set of these certificates forms a polytope and we provide a direct translation of a certificate to a witnessing subsystems for lower bounded threshold properties.
Thereby, we bridge the gap between an abstract gadget, serving solely as a proof that the result is correct, and a concrete object, containing crucial diagnostic information about \emph{why} the result holds.
Moreover, our translation reduces the computation of minimal witnessing subsystems to a purely geometric problem, for which we provide and evaluate new exact and heuristic algorithms.

\iflongversion
All omitted proofs can be found in the appendix.
\else
All omitted proofs can be found in the full version of this paper~\cite{FunkeJB19}.
\fi

\subsubsection{Contributions.}
\begin{itemize}
	\item Following the concept of certificates in certifying algorithms, we introduce \emph{Farkas certificates} for reachability problems in MDPs (\Cref{tab:overview}).
	\item We give a uniform notion of \emph{witnessing subsystem} (WS) for $\mathbf{Pr}^{\max}_{s_0}(\lozenge\operatorname{goal}) \geq \lambda$ and $\mathbf{Pr}^{\min}_{s_0}(\lozenge\operatorname{goal}) \geq \lambda$ (\Cref{def:subsystem}). To the best of our knowledge, witnesses for $\mathbf{Pr}^{\min}_{s_0}(\lozenge\operatorname{goal}) \geq \lambda$ have not been considered previously.
	\item We establish NP-completeness for finding minimal WS even for acyclic discrete time Markov chains (DTMC) (\Cref{thm:np-completeness}).
	\item Our main result establishes a strong connection between the polytopes of Farkas certificates for $\mathbf{Pr}^{\min}_{s_0}(\lozenge\operatorname{goal}) \geq \lambda$ and $\mathbf{Pr}^{\max}_{s_0}(\lozenge\operatorname{goal}) \geq \lambda$ and WS of the same property (\Cref{thm:MCS-polytope}).
	In particular, one can read off a minimal WS from a vertex of the polytope with a maximal number of zeros (\Cref{cor:main corollary}).
\item From our polytope characterizations we derive two algorithms for computing minimal WS: one based on vertex enumeration and one based on mixed integer linear programming (\Cref{sec:computing}).
  We also introduce a linear programming based heuristic aimed at computing small WS.
  We evaluate our approach on DTMC and MDP benchmarks, where particularly our heuristics show competitive results compared to state-of-the-art techniques (\Cref{sec:case studies}).
\end{itemize}
\renewcommand{\arraystretch}{1.4}
\renewcommand{\tabcolsep}{4mm}

\setlength{\textfloatsep}{0.5cm}
\begin{table}[tbp]
	\centering
	\captionsetup{width=.75\linewidth, labelfont={bf, up}}
  \begin{tabular}{ |c|c|c|}
		\hline
		Property& Certificate dimension&  Certificate condition  \\ \hline
		$\mathbf{Pr}^{\min}_{s_0}(\lozenge\operatorname{goal}) \gtrsim \lambda$ & $\mathbf{z}\in \mathbb{R}^{S}$ & $\mathbf{A} \mathbf{z} \leq \mathbf{b} \land \mathbf{z}(s_0) \gtrsim \lambda$  \\\hline
		$\mathbf{Pr}^{\max}_{s_0}(\lozenge\operatorname{goal}) \gtrsim \lambda$ &  $\mathbf{y} \in \mathbb{R}^{\mathcal{M}}_{\geq 0}$ & $\mathbf{y}\mathbf{A} \leq\delta_{s_0}\land \mathbf{y}\mathbf{b} \gtrsim \lambda$   \\\hline
		$\mathbf{Pr}^{\min}_{s_0}(\lozenge\operatorname{goal})\lesssim \lambda$ & $\mathbf{y} \in \mathbb{R}^{\mathcal{M}}_{\geq 0}$ & $\mathbf{y}\mathbf{A} \geq\delta_{s_0}\land \mathbf{y}\mathbf{b} \lesssim \lambda$   \\\hline
		$\mathbf{Pr}^{\max}_{s_0}(\lozenge\operatorname{goal}) \lesssim \lambda$ & $\mathbf{z}\in \mathbb{R}^{S}$ & $\mathbf{A} \mathbf{z} \geq \mathbf{b} \land \mathbf{z}(s_0) \lesssim \lambda$  \\\hline
	\end{tabular}
	 \caption{Overview of Farkas certificates for reachability properties in MDPs (where $\lesssim \; \in \{\leq, <\}$ and $\gtrsim \; \in\{\geq, > \}$).}\label{tab:overview}
\end{table}
\subsubsection{Related work.}
The fundament of certifying algorithms has been surveyed in \cite{McConnellMNS11}.
In the context of model checking, the most prominent approach for the certification of a positive result has been to construct a proof of the property in the system~\cite{Namjoshi01,PeledPZ01,BernasconiMSZG17}.
Rank-based certificates for the emptiness of a certain automaton ~\cite{KupfermanV04} can be used to certify positive model checking results.
Model checking MDPs in the presence of multiple objectives has been studied in~\cite{EtessamiKVY08, ForejtKNPQ11}.

Heuristic approaches for computing small witnessing subsystems in DTMCs have been proposed in~\cite{AljazzarL06,AljazzarL10,JansenAKWKB11, JansenAZWSKB12,JansenWAZKBS14} and implemented in the tool \textsc{Comics}{} \cite{JansenAVWKB12}.
Witnessing subsystems in MDPs have been considered in~\cite{AljazzarL09, AndresDR08} and~\cite{BrazdilCCFK15}, which focuses on succinctly representing witnessing schedulers.
The mixed integer linear programming (MILP) formulation of~\cite{WimmerJABK12,WimmerJAKB14} allows for an exact computation of minimal witnessing subsystems for the property $\mathbf{Pr}^{\max}_{s_0}(\lozenge\operatorname{goal}) \gtrsim \lambda$.
NP-completeness of computing minimal witnessing subsystems in MDPs was shown in \cite{ChadhaV10}, but the exact complexity has, to the best of our knowledge, not been determined for DTMCs (the problem was conjectured to be NP-complete in~\cite{WimmerJABK12}).

Minimal probabilistic counterexamples given as sets of paths can be computed by reframing the problem as a $k$-shortest-path problem~\cite{HanKD09,HanK07}.
Regular expressions have been considered to succinctly represent the set of paths in~\cite{DammanHK08}, and extensions were proposed in~\cite{WimmerBB09,BraitlingWBJA11}.
The tool \textsc{Dipro}{} \cite{AljazzarLLS11} computes probabilistic counterexamples, and a translation of these to fault trees was given in \cite{KuntzLL2011}.
Another, learning-based, approach~\cite{BrazdilCCFKKPU2014} also enumerates paths and produces a witnessing subsystem as a byproduct.
But none of these approaches considers state-based minimality.
Probabilistic counterexamples can be used to automatically guide iterative and refinement-based model checking techniques~\cite{ClarkeGJLV03, ChadhaV10,ChatterjeeCD14,CeskaHJK19,CeskaJJK19,HermannsWZ08}.

Farkas' Lemma is a well-known source of certificates for the (in)feasibility of tasks in combinatorial optimization, operations research, and economics, as presented in the detailed historical account given in \cite[pp. 209--226]{Schrijver1986} as well as \cite[Chapter 2]{Mangasarian94} and \cite{ColonSS03, Vohra2006, NaimanS2017}. The lecture notes \cite{Schrijver2017} contain a rich variety of applications of linear programming in general and Farkas' Lemma in particular.

\section{Preliminaries}
\label{sec:prelim}

\subsubsection{Polyhedra and Farkas' Lemma.}
Throughout the article we write the dot product of two vectors $\mathbf{x}, \mathbf{y}\in \mathbb{R}^n$ as $\mathbf{x}\mathbf{y}$ or $\mathbf{x}\cdot \mathbf{y}$.
A \emph{halfspace} in $\mathbb{R}^n$ is a set $H = \{\mathbf{v}\in \mathbb{R}^n\mid \mathbf{a}\cdot \mathbf{v}\leq b \}$ for some non-trivial $\mathbf{a}\in\mathbb{R}^n$ and $b\in\mathbb{R}$.
A \emph{polyhedron} is the intersection of finitely many halfspaces, and a \emph{polytope} is a bounded polyhedron. A \emph{face} of a polyhedron $P$ is a subset $F\subseteq P$ of the form $F= \{\mathbf{x}\in P\mid \mathbf{a}\cdot \mathbf{x}=\max\{ \mathbf{a}\cdot\mathbf{y} \mid \mathbf{y}\in P\}\}$ for some $\mathbf{a}\in \mathbb{R}^n$. A \emph{vertex} of $P$ is a face consisting of only one point.

Farkas' Lemma \cite{Farkas1902} is part of the fundament of polyhedra theory and linear programming. It provides a natural source of certificates showing the infeasibility of a given system of inequalites, or in other words, the emptiness of the polyhedron described by the system. We will use it in the following version.

\begin{lemma}[Farkas' Lemma, cf. {\cite[Corollary 7.1f on p. 90]{Schrijver1986}}]
	\label{lem:Farkas}
	Let $\mathbf{A}\in \mathbb{R}^{m\times n}$ and $\mathbf{b}\in \mathbb{R}^m$. Then there exists $\mathbf{z}\in \mathbb{R}^n_{\geq 0}$ with $\mathbf{A}\mathbf{z} \leq \mathbf{b}$ if and only if there does \emph{not} exist $\mathbf{y}\in \mathbb{R}^m_{\geq 0}$ with $\mathbf{y}\mathbf{A} \geq 0 \land \mathbf{y}\mathbf{b}< 0$.
	\iffalse
	\begin{alignat*}{3}
	 	&\text{(1)} \quad\exists\,\mathbf{z}\in \mathbb{R}^n_{\geq 0}. \;\; & \mathbf{A}\mathbf{z} = \mathbf{b} \;\;\iff\;\; &\neg\,\exists\, \mathbf{y}\in \mathbb{R}^m.\;\; \mathbf{y}\mathbf{A} \geq 0 \land \mathbf{y}\mathbf{b}< 0\\
		&\text{(2)} \quad\exists\,\mathbf{z}\in \mathbb{R}^n_{\geq 0}. \;\; & \mathbf{A}\mathbf{z} \leq \mathbf{b} \;\;\iff\;\; &\neg\,\exists\, \mathbf{y}\in \mathbb{R}^m_{\geq 0}.\;\; \mathbf{y}\mathbf{A} \geq 0 \land \mathbf{y}\mathbf{b}< 0\\
		&\text{(3)} \quad\exists\,\mathbf{z}\in \mathbb{R}^n. \;\; & \mathbf{A}\mathbf{z} \leq \mathbf{b} \;\;\iff\;\; &\neg\,\exists\, \mathbf{y}\in \mathbb{R}^m_{\geq 0}.\;\; \mathbf{y}\mathbf{A} = 0 \land \mathbf{y}\mathbf{b}< 0
	\end{alignat*}
	\fi
\end{lemma}

\subsubsection{Markov decision processes.}
A \emph{Markov decision process} (MDP) is a tuple $\mathcal{M} = (S, \operatorname{Act}, \iota, \mathbf{P})$, where $S$ is a finite set of \emph{states}, $\operatorname{Act}$ is a finite set of \emph{actions}, $\iota$ is a probability distribution on $S$ called the \emph{initial distribution} of $M$, and $\mathbf{P}\colon S\times\operatorname{Act}\times S\to [0,1]$ is the \emph{transition probability function} where we require $\sum_{s'\in S} \mathbf{P}(s, \alpha, s') \in\{0,1\}$ for all $s\in S$ and $\alpha\in\operatorname{Act}$. An action $\alpha$ is \emph{enabled} in state $s\in S$ if $\sum_{s'\in S} \mathbf{P}(s, \alpha, s') =1$. The set of enabled actions at state $s$ are denoted by $\operatorname{Act}(s)$, and we require $\operatorname{Act}(s) \neq \varnothing$ for all $s\in S$. A \emph{path} in an MDP $\mathcal{M}$ is an infinite sequence $s_0\alpha_0s_1\alpha_1...$ such that $\mathbf{P}(s_i,\alpha_i,s_{i+1})>0$ for all $i\geq 0$. A finite path is a finite sequence $\pi = s_0\alpha_0s_1\alpha_1... s_n$ with the same condition for all $0\leq i\leq n-1$. In this case, we define $\operatorname{last}(\pi) =s_n$. Denote by $\operatorname{Paths}(\mathcal{M})$ and $\operatorname{Paths}_{\operatorname{fin}}(\mathcal{M})$ the set of infinite and finite paths in $\mathcal{M}$.

A \emph{discrete-time Markov chain} (DTMC) is an MDP with a single action which is enabled at every state. If $\mathcal{M}$ is a DTMC, then $\operatorname{Paths}(\mathcal{M})$ carries a probability measure, where the associated $\sigma$-algebra is generated by the cylinder sets $\operatorname{Cyl}(\tau) = \{ \pi\in\operatorname{Paths}(\mathcal{M})\mid \pi\text{ has prefix } \tau\}$ of finite paths $\tau = s_0s_1...s_n$ in $\mathcal{M}$ with probability $\Pr(\operatorname{Cyl}(\tau)) = \iota(s_0)\cdot \prod_{0 \leq i < n} \mathbf{P}(s_i,s_{i+1})$ (fore more details see \cite[Section 10.1]{BaierK2008}).
In the following we denote for a finite set $X$ the set of probability distributions on $X$ by $\operatorname{Dist}(X)$. Given $\mu\in\operatorname{Dist}(X)$ let the \emph{support} of $\mu$ be $\operatorname{supp}(\mu) = \{x\in X\mid \mu(x) >0 \}$.

A \emph{deterministic scheduler} is a function $\S\colon \operatorname{Paths}_{\operatorname{fin}}(\mathcal{M}) \to \operatorname{Act}$ such that $\S(\pi)\in\operatorname{Act}(\operatorname{last}(\pi))$ and a \emph{randomized scheduler} is a function $\S\colon \operatorname{Paths}_{\operatorname{fin}}(\mathcal{M}) \to \operatorname{Dist}(\operatorname{Act})$ such that $\operatorname{supp}(\S(\pi))\subseteq \operatorname{Act}(\operatorname{last}(\pi))$ for all $\pi\in\operatorname{Paths}_{\operatorname{fin}}(\mathcal{M})$.
Given a deterministic (or randomized) scheduler $\S$, a path $\pi = s_0\alpha_0s_1\alpha_1...$ in $\mathcal{M}$ is an \emph{$\S$-path} if $\alpha_i = \S(s_0\alpha_0...s_i)$ (or $\alpha_i\in \operatorname{supp}(\S(s_0\alpha_0...s_i))$) for all $i\geq 0$.

 We denote by $\Pr^\S$ the probability measure on infinite $\S$-paths (see \cite[Definition 10.92 on page 843]{BaierK2008} for more details). If we replace $\iota$ with the distribution concentrated on state $s$, then we obtain a probability measure $\Pr^\S_{\mathcal{M}, s}$ or short $\Pr^\S_{s}$ on infinite $\S$-paths starting in $s$.
The scheduler is \emph{memoryless} if $\S(\pi) = \S(\operatorname{last}(\pi))$ for all $\pi\in\operatorname{Paths}_{\operatorname{fin}}(\mathcal{M})$. We abbreviate memoryless deterministic schedulers as \emph{MD-schedulers} and memoryless randomized schedulers as \emph{MR-schedulers}.

Given a state $t\in S$, we let
\[\mathbf{Pr}_s^{\max}(\lozenge t)= \sup_{\S} \; \Pr_s^\S(\lozenge t) \quad \text{and} \quad \mathbf{Pr}_s^{\min}(\lozenge t)= \inf_{\S} \; \Pr_s^\S(\lozenge t) \]
denote the maximal and minimal probability to reach $t$ eventually when starting in $s$
and set $\mathbf{Pr}^{\min}(\lozenge t) = (\mathbf{Pr}_s^{\min}(\lozenge t))_{s \in S}$ and $\mathbf{Pr}^{\max}(\lozenge t) = (\mathbf{Pr}_s^{\max}(\lozenge t))_{s \in S}$.
The supremum and infimum is indeed attained by an MD-scheduler \cite[Lemmata 10.102 and 10.113]{BaierK2008}, thus justifying the superscripts.
\begin{setting}
	\label{setting:mdp}
	Henceforth we will assume that $\mathcal{M} = (S_{\operatorname{all}}, \operatorname{Act}, \iota, \mathbf{P})$ has a unique initial state $s_0 \in S$ and two distinguished absorbing states $\operatorname{fail}$ and $\operatorname{goal}\in S_{\operatorname{all}}$, i.e., $\mathbf{P}(\operatorname{goal}, \alpha, s) = 0$ for all $\alpha\in\operatorname{Act}$ and $s\in S_{\operatorname{all}}$ with $s\neq\operatorname{goal}$, and likewise for $\operatorname{fail}$.
  Here $\operatorname{goal}$ represents a desirable outcome of the modeled system and $\operatorname{fail}$ an  outcome that is to be avoided. We use the notation $S = S_{\operatorname{all}} \setminus \{\operatorname{fail}, \operatorname{goal}\}$, we assume that every state $s\in S$ is reachable from $s_0$. We also assume that under every scheduler $\operatorname{fail}$ or $\operatorname{goal}$ is reachable from any state, i.e., $\mathbf{Pr}^{\min}_s(\lozenge (\operatorname{goal}\lor \operatorname{fail})) > 0$ for all $s\in S$. If $\mathcal{M}$ does not satisfy this condition from the start, we can apply a standard preprocessing step, which is essentially given by taking the MEC quotient of $\mathcal{M}$, see \cite{deAlfaro97b, deAlfaro97} and also \cite{Ciesinski08}. While it is often easier to verify the condition $\mathbf{Pr}^{\min}_s(\lozenge (\operatorname{goal}\lor\operatorname{fail})) > 0$, it is in fact equivalent to $\mathbf{Pr}^{\min}_s(\lozenge (\operatorname{goal}\lor\operatorname{fail})) = 1$ (see \citeapp{lem: almost sure BSCC}).

	Whenever suitable, we denote by $\mathcal{M}$ also the set of enabled state-action pairs, i.e., $\mathcal{M} =\{(s,\alpha)\in S\times\operatorname{Act}\mid \alpha\in\operatorname{Act}(s)\}$. Let $\mathbf{A} \in \mathbb{R}^{\mathcal{M} \times S}$ be defined by
	\[\mathbf{A}((s,\alpha),t) =
	\begin{cases}
	1 - \mathbf{P}(s,\alpha,s), & \text{if } s = t \\
	-\mathbf{P}(s,\alpha,t), & \text{if } s\neq t
	\end{cases}\]
  We denote by $\mathbf{b} = (\mathbf{b}(s,\alpha))_{(s,\alpha)\in\mathcal{M}}\in \mathbb{R}^{\mathcal{M}}$ with $\mathbf{b}(s, \alpha) = \mathbf{P}(s, \alpha, \operatorname{goal})$ and by $\delta_{s_0}$ the probability distribution that assigns $1$ to $s_0$, and $0$ to all other states.
\end{setting}

The vectors $\mathbf{Pr}^{\min}(\lozenge\operatorname{goal})$ and $\mathbf{Pr}^{\max}(\lozenge\operatorname{goal})$ can be characterized using the following linear programs. Although this characterization is well-known, we give a proof in the full version~\cite{FunkeJB19}{} due to slight differences with the standard literature.

\begin{restatable}[LP characterization, cf. {\cite[Lemma 8]{BiancoA95}}]{proposition}{prminmaxlp}
  \label{prop:LP version of pr_min}
	Let $\mathcal{M}$ be an MDP as in Setting \ref{setting:mdp} and let $\boldsymbol{\delta} \in \mathbb{R}^n_{>0}$. Then the vectors $\mathbf{Pr}^{\min}(\lozenge\operatorname{goal})$ and $\mathbf{Pr}^{\max}(\lozenge\operatorname{goal})$ are, respectively, the \emph{unique} solution of the LPs
	\begin{equation*} \label{eq: LP for min}
	\max \, \boldsymbol{\delta} \cdot \mathbf{z} \;\text{ s.t. } \; \mathbf{A} \mathbf{z} \leq \mathbf{b} \quad\;\; \text{ and } \quad\;\; \min \, \boldsymbol{\delta} \cdot \mathbf{z} \;\text{ s.t. } \; \mathbf{A} \mathbf{z} \geq \mathbf{b}.
	\end{equation*}
\end{restatable}

\section{Farkas certificates for reachability in MDPs}
\allowdisplaybreaks
\label{sec:certificates}

In this section we establish certificates for the following statements:
\begin{enumerate}[leftmargin =10mm]
	\item All schedulers $\S$ satisfy $\Pr_{s_0}^\S(\lozenge\operatorname{goal}) \gtrsim \lambda$ (i.e., $\mathbf{Pr}_{s_0}^{\min}(\lozenge\operatorname{goal}) \gtrsim \lambda$).
	\item Some scheduler $\S$ satisfies $\Pr_{s_0}^\S(\lozenge\operatorname{goal}) \gtrsim \lambda$ (i.e., $\mathbf{Pr}_{s_0}^{\max}(\lozenge\operatorname{goal}) \gtrsim \lambda$).
	\item All schedulers $\S$ satisfy $\Pr_{s_0}^\S(\lozenge\operatorname{goal}) \lesssim \lambda$ (i.e., $\mathbf{Pr}_{s_0}^{\max}(\lozenge\operatorname{goal}) \lesssim \lambda$).
	\item Some scheduler $\S$ satisfies $\Pr_{s_0}^\S(\lozenge\operatorname{goal}) \lesssim \lambda$ (i.e., $\mathbf{Pr}_{s_0}^{\min}(\lozenge\operatorname{goal}) \lesssim \lambda$).
\end{enumerate}
where $\lesssim \; \in \{\leq, <\}$ and $\gtrsim \; \in\{\geq, >\}$.
The basis of our construction is the LP characterization of the probabilities above and, crucially, Farkas' Lemma.

\subsubsection{Certificates for universally-quantified statements.}

In order to deal with the cases (1) and (3), we need the following lemma proved in the full version~\cite{FunkeJB19}{}.

\begin{restatable}{lemma}{monotonicityprminprmax}
	\label{lem:monotonicity}
	For $\mathbf{A} \in \mathbb{R}^{\mathcal{M} \times S}, \mathbf{b}\in \mathbb{R}^{\mathcal{M}}$ as in Setting \ref{setting:mdp}, we have for all $\mathbf{z}\in \mathbb{R}^{S}:$
\begin{gather*}
	\mathbf{A}\mathbf{z} \leq \mathbf{b} \implies \mathbf{z} \leq \mathbf{Pr}^{\min}(\lozenge\operatorname{goal})\\
	\mathbf{A}\mathbf{z} \geq \mathbf{b} \implies \mathbf{z} \geq \mathbf{Pr}^{\max}(\lozenge\operatorname{goal})
\end{gather*}
\end{restatable}

\begin{corollary}\label{cor:certificates for all quantified}
	For  $\gtrsim \; \in \{\geq , >\}$ and  $\lesssim \; \in \{\leq , <\}$ we have
\begin{gather*}
	\mathbf{Pr}^{\min}_{s_0}(\lozenge\operatorname{goal}) \gtrsim \lambda \iff \exists \mathbf{z}\in\mathbb{R}^S.\; \mathbf{A} \mathbf{z} \leq \mathbf{b} \land \mathbf{z}(s_0) \gtrsim  \lambda\\
	\mathbf{Pr}^{\max}_{s_0}(\lozenge\operatorname{goal}) \lesssim \lambda \iff \exists \mathbf{z}\in\mathbb{R}^S.\; \mathbf{A} \mathbf{z} \geq \mathbf{b} \land \mathbf{z}(s_0) \lesssim \lambda
\end{gather*}
\end{corollary}
\begin{proof}
  For the direction from left to right, we take $\mathbf{z}$ to be $\mathbf{Pr}^{\min}(\lozenge\operatorname{goal})$. The opposite direction follows from \Cref{lem:monotonicity}.
\qed\end{proof}

The right hand sides of \Cref{cor:certificates for all quantified} provide \emph{certifying} formulations for problems (1) and (3): to check whether the corresponding threshold statement holds, one must merely check whether $\mathbf{z}$ satisfies the inequalities, rather than checking whether $\mathbf{Pr}^{\min / \max}_{s_0}(\lozenge\operatorname{goal})$ was computed correctly.
If the threshold condition is satisfied, then the vectors $\mathbf{Pr}_{s_0}^{\min/\max}(\lozenge \operatorname{goal})$ are also valid certificates.

\subsubsection{Certificates for existentially-quantified statements.}\label{sec:certificates for E}

To find certificates for the cases (2) and (4), we calculate:
\begin{align*}
  &\quad\mathbf{Pr}^{\min}_{s_0}(\lozenge\operatorname{goal}) < \lambda \\
\overset{\text{Cor. \ref{cor:certificates for all quantified}}}{\iff} &\quad\neg \,\exists \mathbf{z}\in\mathbb{R}^S_{\geq 0}. \, \,\;  \mathbf{A}\mathbf{z} \leq  \mathbf{b} \land \mathbf{z}(s_0) \geq \lambda\\
\iff  &\quad\neg \,\exists \mathbf{z}\in\mathbb{R}^S_{\geq 0}. \, \,\;
\begin{pmatrix}
\mathbf{A} \\
-1 \:0 \ldots 0
\end{pmatrix}\mathbf{z} \leq
\begin{pmatrix}
\mathbf{b}\\
-\lambda
\end{pmatrix}\\
\overset{\text{Lem. \ref{lem:Farkas}}}{\iff}  &\quad\exists \mathbf{y} \in \mathbb{R}^{\mathcal{M}}_{\geq 0}, y^*\geq 0.\, \,\; (\mathbf{y}, y^*)
\begin{pmatrix}
\mathbf{A} \\
-1 \:0 \ldots 0
\end{pmatrix}\geq 0 \land
(\mathbf{y}, y^*)
\begin{pmatrix}
\mathbf{b}\\
-\lambda
\end{pmatrix} < 0\\
\iff &\quad\exists \mathbf{y} \in \mathbb{R}^{\mathcal{M}}_{\geq 0}.\, \,\; \mathbf{y}\mathbf{A} \geq\delta_{s_0}\land \mathbf{y}\mathbf{b} < \lambda.
\end{align*}
For non-strict inequalities, we apply Farkas' Lemma in the opposite direction:
\begin{align*}
   &\quad\mathbf{Pr}^{\min}_{s_0}(\lozenge\operatorname{goal}) \leq \lambda \\
\overset{\text{Cor. \ref{cor:certificates for all quantified}}}{\iff}  &\quad\neg \,\exists \mathbf{z}\in\mathbb{R}^S_{\geq 0}. \, \,\;  \mathbf{A}\mathbf{z} \leq  \mathbf{b} \land \mathbf{z}(s_0) > \lambda\\
  \iff &\quad\neg \,\exists \mathbf{z}\in\mathbb{R}^S_{\geq 0}, z^* \geq 0.\, \,\;  \begin{pmatrix}
   - \mathbf{A} & \mathbf{b}
    \end{pmatrix}
    \begin{pmatrix}
 	 \mathbf{z} \\
 	 z^*
 	 \end{pmatrix} \geq 0 \land
  \begin{pmatrix}
    -\delta_{s_0} &   \lambda
  \end{pmatrix}
   \begin{pmatrix}
  \mathbf{z} \\
  z^*
  \end{pmatrix} < 0
  \\
 \overset{\text{Lem. \ref{lem:Farkas}}}{\iff}&\quad\exists \mathbf{y} \in \mathbb{R}^{\mathcal{M}}_{\geq 0}.\, \,\; \mathbf{y} \begin{pmatrix}
    -\mathbf{A} & \mathbf{b}
    \end{pmatrix} \leq \begin{pmatrix}
    -\delta_{s_0} & \lambda
  \end{pmatrix} \\
    \iff &\quad\exists \mathbf{y} \in \mathbb{R}^{\mathcal{M}}_{\geq 0}.\, \,\; \mathbf{y}\mathbf{A} \geq\delta_{s_0}\land \mathbf{y}\mathbf{b} \leq \lambda.\label{eq:Farkas mdp}
\end{align*}
The deductions for $\mathbf{Pr}^{\max}(\lozenge\operatorname{goal})$ are analogous, so that we get:
\begin{proposition}\label{prop:certificates for ex quantified}
	For  $\gtrsim \; \in \{\geq , >\}$ and  $\lesssim \; \in \{\leq , <\}$ we have
	\begin{gather*}
	\mathbf{Pr}^{\min}_{s_0}(\lozenge\operatorname{goal}) \lesssim \lambda \iff \exists \mathbf{y}\in\mathbb{R}^{\mathcal{M}}_{\geq 0}.\, \,\; \mathbf{y}\mathbf{A} \geq \delta_{s_0} \land \mathbf{y}\mathbf{b} \lesssim  \lambda\\
	\mathbf{Pr}^{\max}_{s_0}(\lozenge\operatorname{goal}) \gtrsim \lambda \iff \exists \mathbf{y}\in\mathbb{R}^{\mathcal{M}}_{\geq 0}.\, \,\;\mathbf{y}\mathbf{A} \leq \delta_{s_0} \land \mathbf{y}\mathbf{b} \gtrsim  \lambda
	\end{gather*}
\end{proposition}
Together, \Cref{cor:certificates for all quantified} and \Cref{prop:certificates for ex quantified} give us all certificate conditions of~\Cref{tab:overview}.
\section{Minimal witnesses for reachability in MDPs}
\label{sec:mws}

In this section we consider the following problem: Given an MDP $\mathcal{M}$ that satisfies the property $\mathbf{Pr}_{\mathcal{M}, s_0}^{\min}(\lozenge\operatorname{goal})\geq \lambda$ (or $\mathbf{Pr}_{\mathcal{M}, s_0}^{\max}(\lozenge\operatorname{goal})\geq \lambda$), find a small subsystem $\mathcal{M}'$ of $\mathcal{M}$ that still satisfies these thresholds.
Such a subsystem is a witness to the satisfaction of the property in $\mathcal{M}$.
We first define subsystems and consider different measures of size which we show to be equivalent.
Then we deal with the question of finding minimal witnessing subsystems.

\subsubsection{Subsystems, witnesses and notions of minimality.}

Our definition of subsystem is essentially the same to the definition in~\cite{WimmerJABK12,WimmerJAKB14} that was used for witnessing subsystems of $\mathbf{Pr}_{\mathcal{M}, s_0}^{\max}(\lozenge\operatorname{goal})\gtrsim\lambda$. From now on we restrict our attention to properties of the form  $\mathbf{Pr}_{\mathcal{M}, s_0}^{\min/\max}(\lozenge\operatorname{goal})\gtrsim\lambda$.
One can deal with upper bounds by exchanging the roles of $\operatorname{fail}$ and $\operatorname{goal}$ and invoking the equality $\mathbf{Pr}_{\mathcal{M},s_0}^{\min}(\lozenge\operatorname{goal}) = 1 - \mathbf{Pr}_{\mathcal{M},s_0}^{\max}(\lozenge\operatorname{fail})$, which holds by the conditions of Setting~\ref{setting:mdp}.

Intuitively, a subsystem $\mathcal{M}'$ of $\mathcal{M}$ contains a subset of states of $\mathcal{M}$, and a transition of $\mathcal{M}$ originating in a state of $\mathcal{M}'$ remains unchanged in $\mathcal{M}'$ or is redirected to $\operatorname{fail}$ (instead of explicitely redirecting to $\operatorname{fail}$, sub-stochastic distributions are used in~\cite{WimmerJABK12,WimmerJAKB14} with the same effect).

\begin{definition}[Subsystem and witness]\label{def:subsystem}
	Let $\mathcal{M} = (S_{\operatorname{all}},\operatorname{Act},s_0, \mathbf{P})$ be an MDP as in Setting \ref{setting:mdp}. A \emph{subsystem} $\mathcal{M}' \subseteq\mathcal{M}$ is an MDP $\mathcal{M}' = (S'_{\operatorname{all}},\operatorname{Act},s_0,\mathbf{P}')$ with $\operatorname{fail}, \operatorname{goal} \in S'_{\operatorname{all}}\subseteq S_{\operatorname{all}}$, $\operatorname{Act}_{\mathcal{M}'}(s) = \operatorname{Act}_{\mathcal{M}}(s)$ for all $s\in S'_{\operatorname{all}}$, and for all $s,t \in S'_{\operatorname{all}}$ with $t\neq \operatorname{fail}$ and $\alpha\in\operatorname{Act}$ we have
	\[ \mathbf{P}'(s,\alpha, t) >0 \Longrightarrow \mathbf{P}'(s,\alpha, t) = \mathbf{P}(s,\alpha, t).\]
	We say that the states $S_{\operatorname{all}}\setminus S'_{\operatorname{all}}$ and the transitions $(s,\alpha, t)$ with $\mathbf{P}(s,\alpha, t) > 0$ and $\mathbf{P}'(s,\alpha, t) = 0$ have been \emph{deleted} in $\mathcal{M}'$. A \emph{witness} for $\mathbf{Pr}_{\mathcal{M}, s_0}^{\min/\max}(\lozenge\operatorname{goal})\gtrsim \lambda$ is a subsystem $\mathcal{M}'\subseteq\mathcal{M}$ such that $\mathbf{Pr}_{\mathcal{M}', s_0}^{\min/\max}(\lozenge\operatorname{goal})\gtrsim \lambda$.
\end{definition}
\begin{remark}
	The condition $\operatorname{Act}_{\mathcal{M}'}(s) = \operatorname{Act}_{\mathcal{M}}(s)$ ensures that the probability of a deleted transition $(s,\alpha, t)$ is added to $(s, \alpha, \operatorname{fail})$. This is essential for witnesses for $\mathbf{Pr}_{\mathcal{M}, s_0}^{\min}(\lozenge\operatorname{goal})\gtrsim \lambda$ as one could otherwise remove entire actions causing low probabilities and obtain greater $\mathbf{Pr}^{\min}$ in $\mathcal{M}'$ than in $\mathcal{M}$ as a result. For witnesses of $\mathbf{Pr}_{\mathcal{M}', s_0}^{\max}(\lozenge\operatorname{goal})\gtrsim \lambda$ one could delete this condition, thus leading to the notion of ~\cite{WimmerJABK12,WimmerJAKB14}.
\end{remark}

\begin{example} \Cref{fig:MDP} depicts an MDP and \Cref{fig:subsystem} indicates the subsystem that is obtained by deleting the state $t$ and additionally the transition $(u, \alpha, s_0)$.

\begin{figure}[tbp]
	\captionsetup{width=0.75\linewidth, labelfont={bf, up}}
  \begin{subfigure}[b]{0.5\columnwidth}
	\centering
  \scalebox{1.3}{

  		\begin{tikzpicture}[x=18mm,y=15mm,font=\scriptsize]

  		\node[state] (s) {$s_0$};
  		\node[state] (t) [above right = 0.8cm and 1.5cm of s]  {$t$};
  		\node[state] (u) [below right = 0.8cm and 1.5cm of s]  {$u$};
  		\node[state] (v) [below right = 1cm and 1cm of t]  {$v$};
  		\node[state] (f) [right = 1.3cm of u] {$\operatorname{fail}$};
  		\node[state] (g) [above = 2.1cm of f]  {$\operatorname{goal}$};

  		\node[bullet] (sst) [above right = 0.5cm and 0.7cm of s] {};
  		\node[bullet] (stu) [right = 0.5cm of s] {};
  		\node[bullet] (tuv) [below right = 0.5cm and 0.5cm of t] {};
  		\node[bullet] (uvws) [above right = 0.3cm and 0.5cm of u] {};
  		\node[bullet] (vgf) [right = 0.5cm of v] {};
  		\node[bullet] (wgv) [above right = 0.3cm and 0.5cm of v] {};

  		{\color{blue!50!black}
  			\draw [ntran] (s) -- node[above=12pt,pos=.6]{$\alpha$} (sst);
  			\draw (sst) edge[ptran, bend right, in=210] coordinate[pos=.3] (bss) (s);
  			\draw (sst) edge[ptran, bend right,out=40, in=150] coordinate[pos=.3] (bst1) (t);
  			\draw (bss) to[bend left] (bst1);}

  		{\color{green!50!black}
  			\draw [ntran] (s) -- node[above=-0.04,pos=.55]{$\beta$} (stu);
  			\draw (stu) edge[ptran, bend right, in=160] coordinate[pos=.3] (bst) (t);
  			\draw (stu) edge[ptran, bend right,out=0, in=160] coordinate[pos=.3] (bsu) (u);
  			\draw (bst) to[bend left] (bsu);}

  		{\color{blue!50!black}
  			\draw [ntran] (t) -- node[right=0.02,pos=.2]{$\alpha$} (tuv);
  			\draw (tuv) edge[ptran, bend right, in=175] coordinate[pos=.2] (btu) (u);
  			\draw (tuv) edge[ptran, bend right, out = 60, in=175] coordinate[pos=.5] (btv) (v);
  			\draw (btu) to[bend right] (btv);}

  		{\color{blue!50!black}
  			\draw [ntran] (u) -- node[right=7pt,pos=1]{$\alpha$} (uvws);
  			\draw (uvws) edge[ptran, bend left] coordinate[pos=.35] (buv) (v);
  			\draw [ptran] (uvws) -- node[left,pos=.5]{} ($(s) +(2.2cm,-1.7cm)$) -- ($(s) - (0,1.7cm)$) -- (s);
  			\draw (buv) to[bend left] ($(uvws) + (0.2cm,0)$);
  			\draw ($(uvws) + (0.2cm,0)$) to[bend left] ($(uvws) - (0,0.22cm)$);}

  		{\color{olive}
  			\draw [ntran] (v) -- node[above,pos=.8]{$\gamma$} (vgf);
  			\draw (vgf) edge[ptran, bend right, in=175] coordinate[pos=.4] (bvg) (g);
  			\draw (vgf) edge[ptran, bend left, out = 20, in=175] coordinate[pos=.2] (bvf) (f);
  			\draw (bvf) to[bend right] (bvg);}

  		{\color{blue!50!black}
  			\draw [ntran] (v) -- node[left=1pt,pos=.9]{$\alpha$} (wgv);
  			\draw (wgv) edge[ptran, bend right, in=175] coordinate[pos=.4] (bwg) (g);
  			\draw (wgv) edge[ptran, bend left, out = -20, in=200] coordinate[pos=.2] (bwv) (t);
  			\draw (bwg) to[bend right] (bwv);}

  		{\color{olive}\draw [ptran] (s) -- node[above=-.05,pos=.3]{$\gamma$} (u);}
  		{\color{green!50!black}\draw [ptran] (u) -- node[right=-.04,pos=.5]{$\beta$} (t);}
  		\end{tikzpicture}}
	\subcaption{}
  \label{fig:MDP}
  \end{subfigure}
  \begin{subfigure}[b]{0.5\columnwidth}
	\centering
	\scalebox{1.3}{

		\begin{tikzpicture}[x=18mm,y=15mm,font=\scriptsize]

		\node[state] (s) {$s_0$};
		\node[state] (u) [below right = 0.8cm and 1.5cm of s]  {$u$};
		\node[state] (v) [below right = 1cm and 1cm of t]  {$v$};
		\node[state] (f) [right = 1.3cm of u] {$\operatorname{fail}$};
		\node[state] (g) [above = 2.1cm of f]  {$\operatorname{goal}$};

		\node[bullet] (sst) [above right = 0.5cm and 0.7cm of s] {};
		\node[bullet] (stu) [right = 0.5cm of s] {};
		\node[bullet] (uvws) [above right = 0.3cm and 0.5cm of u] {};
		\node[bullet] (vgf) [right = 0.5cm of v] {};
		\node[bullet] (wgv) [above right = 0.3cm and 0.5cm of v] {};

		{\color{blue!50!black}
			\draw [ntran] (s) -- node[above=12pt,pos=.6]{$\alpha$} (sst);
			\draw (sst) edge[ptran, bend right, in=210] coordinate[pos=.3] (bss) (s);
			{\color{red} \draw[thick, dashed,ptran] (sst) -- ($(sst) + (0,1.03cm)$) -- ($(g) + (0.5cm,0.5cm)$) -- ($(f) + (0.5cm,0)$) -- (f);}
			\draw (bss) to[bend left] ($(bst1) - (0.08cm,0)$);}

		{\color{green!50!black}
			\draw [ntran] (s) -- node[above=-0.04,pos=.55]{$\beta$} (stu);
			{\color{red} \draw[thick, dashed,ptran] (stu) -- ($(stu) - (0,2cm)$) -- ($(f) - (0,0.69cm)$) -- (f);}
			\draw (stu) edge[ptran, bend right,out=0, in=160] coordinate[pos=.3] (bsu) (u);
			\draw (bsu) to[bend left] ($(stu) - (0,0.4cm)$);}

		{\color{blue!50!black}
			\draw [ntran] (u) -- node[right=7pt,pos=1]{$\alpha$} (uvws);
			\draw (uvws) edge[ptran, bend left] coordinate[pos=.35] (buv) (v);
			{\color{red}\draw [ptran,thick, dashed] (uvws) -- ($(uvws) +(0,-0.2cm)$) -- ($(uvws) + (1cm,-0.2cm)$) -- (f);}
			\draw (buv) to[bend left] ($(uvws) + (0.2cm,0)$);
			\draw ($(uvws) + (0.2cm,0)$) to[bend left] ($(uvws) + (0.08cm,-0.18cm)$);}

		{\color{olive}
			\draw [ntran] (v) -- node[above,pos=.8]{$\gamma$} (vgf);
			\draw (vgf) edge[ptran, bend right, in=175] coordinate[pos=.4] (bvg) (g);
			\draw (vgf) edge[ptran, bend left, out = 20, in=175] coordinate[pos=.2] (bvf) (f);
			\draw (bvf) to[bend right] (bvg);}

		{\color{blue!50!black}
			\draw [ntran] (v) -- node[left=1pt,pos=.9]{$\alpha$} (wgv);
			\draw (wgv) edge[ptran, bend right, in=175] coordinate[pos=.2] (bwg) (g);
			{\color{red}\draw[thick, dashed] (wgv) -- ($(wgv) + (0.73cm,0)$);}
			\draw (bwg) to[bend left] ($(wgv) + (0.2cm,0)$);}

		{\color{olive}\draw [ptran] (s) -- node[above=-.05,pos=.3]{$\gamma$} (u);}
		{\color{red}\draw[thick, dashed] [ptran] (u) -- node[below=-0.03,pos=.5]{\color{green!50!black}$\beta$} (f);}
		\end{tikzpicture}

	}
	\subcaption{}
  \label{fig:subsystem}
  \end{subfigure}
  \caption{An MDP (with omitted probabilities (\subref{fig:MDP})) and a subsystem (\subref{fig:subsystem}), where redirected transitions are dashed.}
\end{figure}
\end{example}
The following lemma ensures that we can use the subsystems as witnesses for both $\mathbf{Pr}_{\mathcal{M}, s_0}^{\max}(\lozenge\operatorname{goal})\gtrsim \lambda$ and $\mathbf{Pr}_{\mathcal{M}, s_0}^{\min}(\lozenge\operatorname{goal})\gtrsim \lambda$.
\begin{restatable}{lemma}{schedulerssubsys}
  Let $\mathcal{M}$ be an MDP as in Setting \ref{setting:mdp} and $\mathcal{M}' \subseteq \mathcal{M}$. Then:
     \[\mathbf{Pr}^{\min}_{\mathcal{M}', s_0}(\lozenge\operatorname{goal}) \leq \mathbf{Pr}^{\min}_{\mathcal{M}, s_0}(\lozenge\operatorname{goal}) \;\;\text{ and }\;\; \mathbf{Pr}^{\max}_{\mathcal{M}', s_0}(\lozenge\operatorname{goal}) \leq \mathbf{Pr}^{\max}_{\mathcal{M}, s_0}(\lozenge\operatorname{goal})\]
 \end{restatable}
\noindent We consider the following notions of minimality for subsystems:
\begin{enumerate}[leftmargin=12mm, rightmargin=8mm]
	\item \emph{State-minimality:} $|S'_{\operatorname{all}}|$ is minimal.
	\item \emph{Transition-minimality:} The number of transitions, i.e. triples $(s,\alpha,t)$ satisfying $\mathbf{P}'(s,\alpha, t) > 0$, is minimal;
	\item \emph{Size-minimality:} The sum of states and transitions is minimal.
\end{enumerate}

Depending on the situation, one notion might be more suitable than the others. However, in \citeapp{lem:minreductions} we show that finding transition-minimal (respectively, size-minimal) witnesses can be reduced to finding state-minimal witnesses with a linear (respectively, quadratic) blow-up. We will therefore restrict ourselves to state-minimality for the rest of this paper.

\subsubsection{NP-completeness of finding minimal witnesses for DTMCs.}
\label{sec:npcompleteness}
In this section we determine the computational complexity of the \emph{witness problem}: Given a DTMC $\mathcal{M}$, a positive integer $k$, and a rational number $\lambda\in[0,1]$, decide whether there exists a witness $\mathcal{M}'\subseteq \mathcal{M}$ for $\Pr_{\mathcal{M}, s_0}(\lozenge\operatorname{goal})\geq \lambda$ with at most $k$ states. The corresponding problem for MDPs is known to be NP-complete~\cite{ChadhaV10,WimmerJAKB14}\footnote{Although the framework in~\cite{ChadhaV10} considers a richer logic, the hardness proof uses only probabilistic reachability formulas such as the ones we consider.}. In this section we show that the witness problem is already NP-complete for acyclic DTMCs, where acyclicity means that the underlying graph with $V = S$ and $E = \{(s,t)\in S\times S\mid \mathbf{P}(s,t) > 0\}$ is acyclic (as before, we take $S = S_{\operatorname{all}} \setminus \{\operatorname{goal},\operatorname{fail}\}$). This answers a conjecture of \cite{WimmerJABK12} in the affirmative and also shows NP-completeness of finding minimal witnesses for $\mathbf{Pr}_{\mathcal{M}, s_0}^{\min}(\lozenge\operatorname{goal})\geq \lambda$.

\begin{restatable}{theorem}{mwanpcompleteness}
\label{thm:np-completeness}
	The witness problem is NP-complete for acyclic DTMCs.
\end{restatable}
\begin{proof}[Sketch]
	An NP-algorithm for the witness problem is given by guessing a set of states of size $k$ and verifying in polynomial time that the corresponding subsystem satisfies $\Pr_{\mathcal{M}', s_0}(\lozenge\operatorname{goal})\geq \lambda$.

	For hardness, we give a reduction from the \emph{clique problem}, which is among Karp's 21 NP-complete problems \cite{Karp1972}.
	The idea is the following: Given an instance of the clique problem with graph $G=(V,E)$ and integer $k$, construct an acyclic Markov chain $\mathcal{M}$ with states $S = \{s_0\}\cup V \cup E \cup\{\operatorname{goal}, \operatorname{fail}\}$ and edges from each vertex $v \in V$ to all edges to which it is incident.
	Then the existence of a $k$-clique can be reduced to the existence of a ``saturated'' subsystem in $\mathcal{M}$ with $k$ states in $V$.
	To check whether the subsystem is saturated, we require it to have more probability than a certain threshold, which depends on $k$ and $|V|$. Details can be found in the full version~\cite{FunkeJB19}{}.
\end{proof}

\begin{remark}
	NP-completeness of transition-minimal and size-minimal versions of the witness problem for acyclic DTMCs follows along the same lines, where only the sizes and thresholds for the subsystems need to be adapted.
\end{remark}

However, DTMCs whose underlying graph is a tree permit an efficient algorithm for computing minimal witnesses (for the proof see \citeapp{thm: tree-shaped algorithm}).

 \begin{restatable}{proposition}{treeshapeddtmc}
 	Minimal witnesses in tree-shaped DTMCs can be computed in polynomial time.
 \end{restatable}
\begin{proof}[Sketch]
	The algorithm first transforms the DTMC at hand into a binary (tree-shaped) DTMC, and then works bottom up by storing for each state the highest probability that can be obtained with a subsystem of size $k$, for all $k$ up to the size of the subtree.
\end{proof}

\section{Relating Farkas certificates and minimal witnesses}
\label{sec:relation}

In this section we establish a strong connection between Farkas certificates on the one hand and witnesses for probabilistic reachability constraints on the other hand. We first note that the set of Farkas certificates for non-strict lower bounds forms a polytope, i.e., a bounded polyhedron.

\begin{restatable}[Polytopes of Farkas certificates]{lemma}{polytope}\label{lem:polytope}
	Let $\mathcal{M} = (S_{\operatorname{all}},\operatorname{Act},s_0,\mathbf{P})$ be an MDP as in Setting \ref{setting:mdp} and consider $\mathbf{A}\in\mathbb{R}^{\mathcal{M}\times S}$ and $\mathbf{b}\in\mathbb{R}^S$ introduced there. Then for every $\lambda \in [0,1]$ the polyhedra
	\begin{gather*}
		\P^{\min}(\lambda) = \{ \mathbf{z}\in \mathbb{R}^{S}\mid \mathbf{A}\mathbf{z}\leq \mathbf{b} \land \mathbf{z}(s_0) \geq \lambda \}\\
		\P^{\max}(\lambda) = \{ \mathbf{y}\in \mathbb{R}^{\mathcal{M}}\mid \mathbf{y}\geq 0\land \mathbf{y}\mathbf{A}\leq \delta_{s_0} \land \mathbf{y}\mathbf{b} \geq\lambda \}
	\end{gather*}
	are both polytopes, called \emph{the polytopes of Farkas certificates}.
\end{restatable}

\begin{remark}
	For any vector $\mathbf{v}\in \mathbb{R}^n$ the support is defined as $\operatorname{supp}(\mathbf{v}) =\{i\in\{1,...,n\}\mid \mathbf{v}_i >0\}$, and analogously for the vector spaces $\mathbb{R}^S$ and $\mathbb{R}^{\mathcal{M}}$.
  As our connection between subsystems of $\mathcal{M}$ and points in $\P^{\min}(\lambda)$ is based on taking the support, we restrict our attention to the subpolytope $\P^{\min}_{\geq 0}(\lambda)  = \P^{\min}(\lambda)\cap \mathbb{R}^S_{\geq 0}$.
\end{remark}

\begin{notation}
	Given an MDP $\mathcal{M} = (S_{\operatorname{all}},\operatorname{Act},s_0,\mathbf{P})$ as in Setting \ref{setting:mdp} and a subset $R\subseteq \mathcal{M}$, where $\mathcal{M}$ also denotes the state-action pairs (compare with \Cref{sec:prelim}). We let $\mathcal{M}_R = (S'_{\operatorname{all}},\operatorname{Act},s_0,\mathbf{P}')$ be the subsystem where, roughly speaking, the state-action pairs in $R$ \emph{remain}. More precisely, let
	\begin{align*}
		S'_{\operatorname{all}} &= \{ s\in S\mid \exists \alpha\in\operatorname{Act}. \; (s, \alpha)\in R\}\cup\{\operatorname{goal}, \operatorname{fail}\}\\
		\mathbf{P}'(s,\alpha, t) &= \begin{cases}
			\mathbf{P}(s,\alpha, t) & \mbox{if } (s, \alpha)\in R\text{ and } t\in S'_{\operatorname{all}}\setminus \{\operatorname{fail}\}\\
			1-\sum_{t\in S'_{\operatorname{all}}\setminus\{\operatorname{fail}\}}\mathbf{P}(s, \alpha, t) & \mbox{if } (s, \alpha)\in R\text{ and } t=\operatorname{fail}\\
			1 & \mbox{if } (s, \alpha)\notin R, \alpha\in\operatorname{Act}(s) \text{ and } t=\operatorname{fail}\\
			0 & \mbox{else }
		\end{cases}
		\end{align*}
	For $R\subseteq S$ we set $\mathcal{M}_R = \mathcal{M}_{R'}$ for $R' = \bigcup_{s\in R} \{s\}\times \operatorname{Act}(s)$.
\end{notation}

\begin{restatable}[Farkas certificates yield witnesses]{theorem}{mainthm}\label{thm:MCS-polytope}
 	Let $\mathcal{M}$ be an MDP as in Setting \ref{setting:mdp} and $\lambda\in[0,1]$. Then for a set $R\subseteq S$ the following statements are equivalent:
	\begin{enumerate}[leftmargin = 13mm]
		\item The subsystem $\mathcal{M}_R$ is a witness for $\mathbf{Pr}^{\min}_{\mathcal{M}, s_0}(\lozenge\operatorname{goal}) \geq\lambda$.
		\item There is a point $\mathbf{p}$ in $\P^{\min}_{\geq 0}(\lambda)$ such that $\operatorname{supp}(\mathbf{p}) \subseteq  R$.
		\item There is a vertex $\mathbf{v}$ of $\P^{\min}_{\geq 0} (\lambda)$ such that $\operatorname{supp}(\mathbf{v})\subseteq R$.
	\end{enumerate}
	Moreover, for a set $R\subseteq \mathcal{M}$ the following statements are equivalent:
	\begin{enumerate}[leftmargin = 13mm, label=(\alph*)]
	\item The subsystem $\mathcal{M}_R$ is a witness for $\mathbf{Pr}^{\max}_{\mathcal{M}, s_0}(\lozenge\operatorname{goal}) \geq\lambda$.
	\item There is a point $\mathbf{p}$ in $\P^{\max}(\lambda)$ such that $\operatorname{supp}(\mathbf{p}) \subseteq  R$.
	\item There is a vertex $\mathbf{v}$ of $\P^{\max}(\lambda)$ such that $\operatorname{supp}(\mathbf{v})\subseteq R$.
	\end{enumerate}
\end{restatable}
\noindent One consequence of~\Cref{thm:MCS-polytope} is that every MD-scheduler $\S$ with $\Pr^{\S}_{s_0}(\lozenge\operatorname{goal}) \geq\lambda$ corresponds to a point in $\P^{\max}(\lambda)$, i.e. to a certificate for $\mathbf{Pr}^{\max}_{\mathcal{M}, s_0}(\lozenge\operatorname{goal}) \geq\lambda$.
\begin{restatable}[Detecting minimal witnesses by vertices of $\mathcal P$]{corollary}{verticestoMW}\label{cor:main corollary}
	Let $\mathcal{M} = (S_{\operatorname{all}},\operatorname{Act},s_0,\mathbf{P})$ be an MDP as in Setting \ref{setting:mdp} and $\lambda\in[0,1]$. Then a vertex $\mathbf{v}$ of $\P^{\min}_{\geq 0}(\lambda)$ has a maximal number of zeros among all vertices of $\P^{\min}_{\geq 0}(\lambda)$ if and only if $\mathcal{M}_{\operatorname{supp}(\mathbf{v})} $ is a minimal witness for $\mathbf{Pr}^{\min}_{s_0}(\lozenge\operatorname{goal})\geq \lambda$.

	Dually, a vertex $\mathbf{v}$ of $\P^{\max}(\lambda)$ has a maximal number of zeros among all vertices of $\P^{\max}(\lambda)$ if and only if all of the following hold:
	\begin{enumerate}[leftmargin =10mm]
		\item $\mathcal{M}_{\operatorname{supp}(\mathbf{v})} = (S'_{\operatorname{all}},\operatorname{Act},s_0,\mathbf{P}')$ is a minimal witness for $\mathbf{Pr}^{\max}_{s_0}(\lozenge\operatorname{goal})\geq \lambda$,
		\item for every $s\in S'$ there is precisely one $\alpha\in\operatorname{Act}(s)$ with $(s, \alpha)\in \operatorname{supp}(\mathbf{v})$,
		\item the corresponding map $\S\colon S'\to\operatorname{Act}$ is an MD-scheduler on $\mathcal{M}_{\operatorname{supp}(\mathbf{v})}$ with $\Pr^\S_{s_0}(\lozenge\operatorname{goal}) \geq \lambda$.
	\end{enumerate}
\end{restatable}

\section{Computing witnessing subsystems}
\label{sec:computing}

In this section we use the results of \Cref{sec:relation} to derive two algorithms for the computation of minimal witnesses for reachability constraints in MDPs.
As the problem is NP-hard, we also present a heuristic approach aimed at computing small witnessing subsystems.

\subsubsection{Vertex enumeration.}
\Cref{cor:main corollary} gives rise to the following approach of computing minimal witnessing subsystems: enumerate all vertices in the corresponding polytope and choose one with a maximal amount of zeros.
Vertex enumeration of polytopes has been studied extensively~\cite{AvisF93, AvisF92, Balinski61, BremnerFM98, BussiekL98, Dyer83, Dyer77, Mattheiss73, Provan1994, FukudaLM97, FukudaP95} and has been shown to be computationally hard \cite[Corollary 2]{Khachiyan2008}.

First experiments that we have conducted with the \texttt{SageMath}\footnote{\url{http://www.sagemath.org/}} toolkit which supports vertex enumeration have not scaled well in the dimension, which in our case is the number of states in the original system.
Also, we found no tool support for vertex enumeration that is able to handle sparse matrices, which is essential for bigger benchmarks.

\subsubsection{Mixed integer linear programming.}
An approach that computes minimal witnesses to the threshold problem $\mathbf{Pr}^{\max}_{s_0}(\lozenge\operatorname{goal})\geq \lambda$ using mixed integer linear programs (MILP) was presented in~\cite{WimmerJABK12,WimmerJAKB14}.
Using the following lemma, we can derive MILP formulations from our polytope formulations.
\begin{restatable}{lemma}{MILPformulation}\label{lem:MILP}
  \label{lem:MILPformulation}
  Let $\mathcal{P} = \{ \mathbf{x} \mid \mathbf{A} \mathbf{x} \leq \mathbf{b}, \mathbf{x} \geq 0 \} \subseteq \mathbb{R}^n$ be a polytope and $K \geq 0$ be such that for all $\mathbf{p} \in \mathcal{P}$ and $1\leq i\leq n$ we have  $\mathbf{p}(i) \leq K$.
  Consider the MILP
  \[ \min \sum_{1 \leq i \leq n} \boldsymbol{\sigma}(i) \quad\text{s.t.}\quad \mathbf{x} \in \mathcal{P}, \quad \mathbf{x} \leq K \cdot \boldsymbol{\sigma}, \quad\boldsymbol{\sigma}(i)\in\{0,1\}\]

  Then a vector $(\boldsymbol{\sigma},\mathbf{x})$ is an optimal solution of this MILP if and only if $\mathbf{x}$ is a point in $\mathcal{P}$ with a maximal number of zeros.
\end{restatable}

For $\mathcal{P}^{\min}_{\geq 0}(\lambda)$ we can use \Cref{lem:monotonicity} to derive that $K = 1$ is a viable bound.
By invoking again \Cref{cor:main corollary}, this means that a solution $(\mathbf{z}, \boldsymbol{\sigma})$ of the MILP
 \[ \min \sum_{s \in S} \boldsymbol{\sigma}(s) \;\text{ s.t. }\; \mathbf{z}\in  \mathcal{P}^{\min}_{\geq 0}(\lambda), \quad \mathbf{z} \leq \boldsymbol{\sigma}, \quad\boldsymbol{\sigma}(i)\in\{0,1\}\]
encodes a minimal witnessing subsystem in the integral variables $\boldsymbol{\sigma}$. This MILP was used in~\cite{WimmerJABK12,WimmerJAKB14} for the computation of minimal witnessing subsystems of DTMCs .

An upper bound $K$ as in \Cref{lem:MILP} for $\mathcal{P}^{\max}(\lambda)$ can be found in polynomial time by taking the objective value of an optimal solution to the LP
\[\max \sum_{(s,\alpha) \in \mathcal{M}} \mathbf{y}(s,\alpha) \;\text{ s.t. }\; \mathbf{y}\in \mathcal{P}^{\max}(\lambda) \]

\begin{remark}
\label{rem:ltlsubsys}
To compute minimal witnesses for $\mathbf{Pr}^{\max}_{s_0}(\lozenge \operatorname{goal}) \geq \lambda$,~\cite{WimmerJABK12,WimmerJAKB14} (witnesses for $\mathbf{Pr}^{\min}_{s_0}(\lozenge \operatorname{goal}) \geq \lambda$ were not considered) propose the MILP with objective: $\min \; \sum_{(s,\alpha) \in \mathcal{M}} \boldsymbol{\sigma}(s,\alpha)$, subject to the conditions
\begin{align}
 \forall (s,\alpha) \in \mathcal{M}. & \;\;\; \mathbf{z}(s) \leq 1 - \boldsymbol{\sigma}(s,\alpha) + \sum_{s' \in S} \mathbf{P}(s,\alpha,s') \cdot \mathbf{z}(s') + \mathbf{b}(s)\\
  \forall s \in S.&\;\;\;\mathbf{z}(s) \leq \sum_{\alpha \in \operatorname{Act}(s)} \boldsymbol{\sigma}(s,\alpha), \;\;\; \mathbf{z}(s_{0}) \geq \lambda
\end{align}
where $\boldsymbol{\sigma}(s,\alpha)$ are binary integer variables.
It was implemented in the tool \texttt{ltlsubsys}.
The idea is to directly encode a scheduler in the set of equations $\mathbf{A} \mathbf{z} \leq \mathbf{b}$ using $\boldsymbol{\sigma}$.
In~\cite{WimmerJABK12,WimmerJAKB14} a number of additional redundant constraints are given to guide the search.
In contrast to~\cite{WimmerJABK12,WimmerJAKB14} we do not need to handle so-called \emph{problematic states}, as our precondition $\mathbf{Pr}^{\min}_s(\lozenge(\operatorname{goal} \lor \operatorname{fail})) > 0$ guarantees that no such states exist.

\iffalse
Inequalities in (6.1) that do not belong to the subsystem representing the induced scheduler, i.e. the ones where $\boldsymbol{\sigma}(s,\alpha) = 0$, are ``discharged'' as $\mathbf{z}(s) \leq 1 + N$ holds for any positive $N$.
This again uses the insight that $1$ is an upper bound for $\mathbf{z}(s)$.
In the other inequalities, where $\boldsymbol{\sigma}(s,\alpha) = 1$, we get exactly the corresponding inequalities of $\mathbf{A} \mathbf{z} \leq \mathbf{b}$.
The constraints in (6.2) guarantee that at least one $\boldsymbol{\sigma}(s,\alpha)$ is $1$ if $\mathbf{z}(s) > 0$, and (6.3) ensures that the probability in $s_0$ under the given scheduler is above the threshold $\lambda$.
We have omitted the handling of what were called \emph{problematic states} in~\cite{WimmerJABK12,WimmerJAKB14}, as our assumption $\mathbf{Pr}^{\min}_s(\lozenge(\operatorname{goal} \lor \operatorname{fail})) > 0$ for all states $s$ guarantees that such states do not exist. In \Cref{sec:case studies} we give an experimental evaluation of these two different MILP formulations for $\mathbf{Pr}^{\max}_{s_0}(\lozenge \operatorname{goal}) \geq \lambda$.
\fi
\end{remark}

\subsubsection{$k$-step quotient sum ($\operatorname{QS}_k$) heuristics.}

\newcommand{\operatorname{QS}}{\operatorname{QS}}

Approximating the maximal number of zeros in a polytope is computationally hard in general~\cite{AmaldiK98}.
We now derive a heuristic approach for this problem called \emph{quotient sum heuristic} which is based on iteratively solving LPs over the polytope, where the objective function for each iteration depends on an optimal solution of the previous LP. More precisely, we take $\mathbf{o}_1 = (1,\ldots,1)$ and take an optimal solution $\operatorname{QS}_1$ of the LP $\min \mathbf{o}_1\cdot\mathbf{y} \;\text{ s.t. } \; \mathbf{y}\in\mathcal{P}^{\max}(\lambda)$.
Many entries in $\operatorname{QS}_1$ may be small, but still greater than zero.
In order to push as many of the small values of $\operatorname{QS}_1$ to zero, we define a new objective function by
\begin{equation}\label{eq:QS}
\mathbf{o}_2(i) =
\begin{cases}
  1/\operatorname{QS}_1(i), & \text{if } \operatorname{QS}_1(i) > 0 \\
  C, & \text{if } \operatorname{QS}_1(i) = 0
\end{cases}
\end{equation}
where $C$ is a value that is greater than any value $1/\operatorname{QS}_1(i)$.
We now take a solution $\operatorname{QS}_2$ of the new LP $\min \mathbf{o}_2\cdot\mathbf{y} \text{ s.t. } \mathbf{y}\in\mathcal{P}^{\max}(\lambda)$
and form the next objective function $\mathbf{o}_3$ as in (\ref{eq:QS}).
Inductively this generates a sequence of objective functions $(\mathbf{o}_k)_{k\geq 1}$ and corresponding optimal solutions $(\operatorname{QS}_k)_{k
  \geq 1}$ in $\mathcal{P}^{\max / \min}(\lambda)$.
By~\Cref{thm:MCS-polytope} we can construct a witnessing subsystem with as many states as the number of non-zero entries in $\operatorname{QS}_k$.

\section{Experiments}\label{sec:case studies}
In this section we evaluate our MILP formulations and heuristics on a number of DTMC and MDP benchmarks from the \textsc{Prism}{} benchmark-suite~\cite{KwiatkowskaNP11,KwiatkowskaNP12}.
We compare our results with the tool \textsc{Comics}{}~\cite{JansenAVWKB12}, which implements heuristic approaches to compute small subsystems for DTMCs.
It has two modes: the \emph{local search} extends a given subsystem by short paths that carry much probability, whereas the \emph{global search} searches for the next most probable path from the initial state to $\operatorname{goal}$, and adds it to the subsystem.
Both approaches iteratively extend a subsystem until it carries more probability than the given threshold and thus have to compute the probability of the subsystem at each iteration.

All computations were performed on a computer with two Intel E5-2680 8 cores at \(2.70\)\,GHz running Linux, with a time bound of $30$ minutes, a memory bound of 100\,GB and with each benchmark instance having access to 4 cores.
For the LP and MILP instances we use the Gurobi solver, version 8.1.1~\cite{gurobi}.
The recorded times of our computations include the construction of the LPs/MILPs and are wall clock times.
Pre-processing steps, such as collapsing states that cannot reach $\operatorname{goal}$, are not counted in the time consumption.
For \textsc{Comics}{}, we use the time that is reported as counterexample generation time by the tool.

To validate our implementation, we used \textsc{Prism}{} to verify that the subsystems that we compute indeed satisfy the probability thresholds.
We noticed that for a few instances ($< 0.5\%$) \textsc{Prism}{} reported a deviation of less than $10^{-8}$, which can be explained by the fact that both \textsc{Prism}{} and the solvers that we use rely on floating-point arithmetic, which is approximate by nature.

Our implementation, together with the models we use and benchmark results can be found at \url{https://github.com/simonjantsch/farkas}.

\begin{figure}[h]
	\captionsetup{width=.75\linewidth, labelfont={bf, up}}
  \begin{subfigure}[t]{0.5\columnwidth}
    \includegraphics[width=6cm]{crowds-2-8_heur_iter_yform.pdf}
    \subcaption{QS-heuristic applied to $\mathcal{P}^{\max}(\lambda)$.}
    \label{subfig:itpmax}
  \end{subfigure}
  \begin{subfigure}[t]{0.5\columnwidth}
    \includegraphics[width=6cm]{crowds-2-8_heur_iter_zform.pdf}
    \subcaption{QS-heuristic applied to $\mathcal{P}^{\min}_{\geq 0}(\lambda)$.}
  \end{subfigure}
  \caption{crowds-2-8: comparing $\operatorname{QS}_k$ for growing $k$.}
  \label{fig:expheuriter}
\end{figure}

\begin{figure}[t]
	\captionsetup{width=.9\linewidth, labelfont={bf, up}}
	\begin{subfigure}[h]{1\columnwidth}
		\begin{subfigure}{0.5\columnwidth}
			\includegraphics[width=6cm]{crowds-5-8_states.pdf}
		\end{subfigure}
		\begin{subfigure}{0.5\columnwidth}
			\includegraphics[width=6cm]{crowds-5-8_times.pdf}
		\end{subfigure}
		\captionsetup{width=.9\linewidth, labelfont={bf, up}}
		\subcaption{crowds-5-8 (46,873 states). \textsc{Comics}{}-global runs out of memory for $\lambda \geq 0.23$.}
		\label{fig:expheurcrowds}
	\end{subfigure}
	\vspace{0.1cm}
	\begin{subfigure}[h]{1\columnwidth}
		\begin{subfigure}{0.5\columnwidth}
			\includegraphics[width=6cm]{brp-512-2_states.pdf}
		\end{subfigure}
		\begin{subfigure}{0.5\columnwidth}
			\includegraphics[width=6cm]{brp-512-2_times.pdf}
		\end{subfigure}
		\captionsetup{width=.9\linewidth, labelfont={bf, up}}
		\subcaption{brp-512-2 (15,875 states). \textsc{Comics}{}-local reports an error for $\lambda \geq 2.1\cdot10^{-5}$ and \textsc{Comics}{}-global runs out of memory for $\lambda = 2.6 \cdot 10^{-5}$. }
		\label{fig:expheurbrp}
	\end{subfigure}
	\caption{Comparison of heuristic methods on DTMC benchmarks.}
	\label{fig:expheur}
\end{figure}

\subsubsection{DTMC benchmarks.}

As $\mathbf{Pr}^{\max}$ and $\mathbf{Pr}^{\min}$ coincide on DTMCs, we can use the heuristics and exact computations derived from either the $\mathcal{P}^{\max}$ or the $\mathcal{P}^{\min}_{\geq 0}$ polytope for DTMCs (in \textsc{Comics}{} we use the standard query $\Pr_{s_0}(\lozenge \operatorname{goal}) \geq \lambda$).
We consider two DTMC benchmarks: a model of the crowds-$N$-$K$ protocol~\cite{Shmatikov04,ReiterR98} for ensuring anonymous web browsing (with $N$ members and $K$ protocol runs) and a model of the bounded retransmission protocol~\cite{DArgenioJJL01,HelminkSV93} for file transfers (where brp-$N$-$K$ is the instance with $N$ chunks and $K$ retransmissions).

\Cref{fig:expheuriter} shows the effect of increasing the number of iterations of the $\operatorname{QS}$-heuristic for the model crowds-2-8.
While the first iteration (taking $\operatorname{QS}_2$ instead of $\operatorname{QS}_1$) has an impact on the number of states, more iterations do not improve the result significantly.
For $\operatorname{QS}_1$, the sizes of subsystems increase monotonically with growing $\lambda$. Starting with $\operatorname{QS}_2$ the results may, interestingly, have ``spikes'': increasing $\lambda$ can lead to smaller subsystems.

\Cref{fig:expheur} shows the results of the $\operatorname{QS}_2$-heuristic compared to the two modes of \textsc{Comics}{} for $\lambda$ that ranges between $0$ and the actual reachability probability of the model.
A general observation is that the runtime of the $\operatorname{QS}$-heuristic is independent of $\lambda$, whereas both modes of \textsc{Comics}{} use significantly more time with increasing $\lambda$.
The same observation can be done for memory consumption, which stayed below 200 MB for our heuristics.
Also, especially for crowds-5-8, one can see that relatively small subsystems are possible even for large $\lambda$.
The exact computations via MILPs hit the timeout for almost all instances.

In~\Cref{fig:expheur} it can be seen that the $\operatorname{QS}$ heuristics derived from the two polytopes $\P^{\max}$ and $\P_{\geq 0}^{\min}$ may produce different results.
However, for both models one of them gives monotonically growing subsystems and outperforms \textsc{Comics}{}.
While $\operatorname{QS}_2$ applied to $\mathcal{P}^{\min}_{\geq 0}$ performs better on crowds-5-8 (\Cref{fig:expheurcrowds}), it is the other way around on brp-512-2 (\Cref{fig:expheurbrp}).
In future work we intend to investigate what properties determine which of the two formulations performs better for a given DTMC.

\subsubsection{MDP benchmarks.}
\begin{figure}[tbp]
  \captionsetup{width=.75\linewidth, labelfont={bf, up}}
  \begin{subfigure}[t]{0.5\columnwidth}
    \includegraphics[width=6cm]{consensus-2-4_prmin_states.pdf}
    \subcaption{Witnesses for $\mathbf{Pr}^{\min}_{s_0}(\lozenge \operatorname{goal}) \geq \lambda$.}
    \label{subfig:mdpconsprmin}
  \end{subfigure}
  \begin{subfigure}[t]{0.5\columnwidth}
    \includegraphics[width=6cm]{consensus-2-4_prmax_states.pdf}
    \subcaption{Witnesses for $\mathbf{Pr}^{\max}_{s_0}(\lozenge \operatorname{goal}) \geq \lambda$.}
    \label{subfig:mdpconsprmax}
  \end{subfigure}
  \caption{MDP benchmark: consensus-2-4 (528 states)}
  \label{fig:expmdpconsensus}
\end{figure}

We consider two MDP models: the randomized consensus-$N$-$K$ protocol of~\cite{KwiatkowskaNS01,AspnesH90} (with $N$ processes and a bound $K$ on the random walk) and the CSMA-$N$-$K$ protocol for data channels~\cite{KwiatkowskaNSW07} (where $N$ is the number of stations, and $K$ is the maximal backoff count).
The results of both heuristic and exact computations can be seen in \Cref{fig:expmdpconsensus} and \Cref{fig:expmdpcsma}.
Whereas the heuristics all needed less than $5$ minutes, all MILP instances ran into the timeout except for the ones in \Cref{subfig:mdpconsprmin}.
Whenever a MILP instance could not be solved optimally in $30$ minutes, we plot both the found upper and lower bound, with the region in between shaded.
It should be noted that the condition $\mathbf{Pr}^{\min}(\lozenge (\operatorname{goal} \lor \operatorname{fail}))$ holds for the instances of these models, and reachability properties, that we consider.

\begin{figure}[tbp]
  \captionsetup{width=.75\linewidth, labelfont={bf, up}}
  \begin{subfigure}[t]{0.5\columnwidth}
    \includegraphics[width=6cm]{csma-3-2_prmin_states.pdf}
    \subcaption{Witnesses for $\mathbf{Pr}^{\min}_{s_0}(\lozenge \operatorname{goal}) \geq \lambda$.}
  \end{subfigure}
  \begin{subfigure}[t]{0.5\columnwidth}
    \includegraphics[width=6cm]{csma-3-2_prmax_states.pdf}
    \subcaption{Witnesses for $\mathbf{Pr}^{\max}_{s_0}(\lozenge \operatorname{goal}) \geq \lambda$.}
    \label{subfig:mdpcsmaprmax}
  \end{subfigure}
  \caption{MDP benchmark: CSMA-3-2 (36,850 states)}
  \label{fig:expmdpcsma}
\end{figure}

The comparison between the MILP formulation that we derived from $\mathcal{P}^{\max}(\lambda)$ and the one presented in~\cite{WimmerJABK12,WimmerJAKB14} (labeled by \texttt{ltlsubsys}, see also \Cref{sec:computing}) shows that both compute comparable upper and lower bounds in~\Cref{subfig:mdpconsprmax}, whereas \texttt{ltlsubsys} found worse upper bounds in~\Cref{subfig:mdpcsmaprmax}.
In all instances apart from \Cref{subfig:mdpconsprmax} the corresponding $\operatorname{QS}_2$ heuristics performs well and generates subsystems that are as good, or better, than the best upper bounds computed by the MILPs in 30 minutes.
As expected, the witnessing subsystems for $\mathbf{Pr}^{\min}_{s_0}(\lozenge \operatorname{goal}) \geq \lambda$ tend to the entire state space as $\lambda$ tends to the actual value $\mathbf{Pr}^{\min}_{s_0}(\lozenge \operatorname{goal})$ (which is $1$ in these two models).
However, subsystems for $\mathbf{Pr}^{\max}_{s_0}(\lozenge \operatorname{goal}) \geq \lambda$ may be substantially smaller even for large $\lambda$.

\section{Conclusion}
In this paper we brought together two a priori unrelated notions in the context of probabilistic reachability constraints: on the one hand Farkas certificates, which are vectors satisfying certain linear inequalities that we derive using MDP-specific variants of Farkas' Lemma, and on the other hand witnessing subsystems, which provide insight into which parts of the system are essential for the satisfaction of the considered property. This connection reduces the computation of minimal (respectively, small) witnessing subsystems to finding a Farkas certificate with a maximal (respectively, large) number of zeros.
Furthermore, it leads to a unified notion of witnessing subsystem for $\mathbf{Pr}^{\max}_{s_0}(\lozenge \operatorname{goal}) \geq \lambda$ and $\mathbf{Pr}^{\min}_{s_0}(\lozenge \operatorname{goal}) \geq \lambda$.

We showed that the decision version of computing minimal witnessing subsystems is NP-complete for acyclic DTMCs and introduced heuristics for the computation of small witnesses based on Farkas certificates.
Experiments of the heuristics exhibited competitive results compared to the approach implemented in \textsc{Comics}{} and showed that they scale well with the system size and threshold.
As expected, computing minimal subsystems using the derived MILP formulations consumed significantly more time than the heuristics and often triggered timeouts.
The upper and lower bounds that were computed in the given time by the new MILP formulation for $\mathbf{Pr}^{\max}_{s_0}(\lozenge \operatorname{goal}) \geq \lambda$ were comparable to known techniques.

We have considered MDPs in which the probability to reach $\operatorname{goal}$ or $\operatorname{fail}$ is positive under each scheduler.
In future work, we plan to extend our techniques to weaken this assumption.
Exploring how vertex enumeration techniques could be adapted to the MDP-specific form of the Farkas polytopes is another interesting line of future work.
We also plan to implement a tool for working with Farkas certificates in practice, which encompasses their generation as well as their independent validation.

\bibliographystyle{splncs04}

redpajama_set_name: RedPajamaArXiv


26 DHgate galaxy waterproof cell phone coupons - instant savings! With DHgate.com coupons, promos & sales, you can save more money on shopping Cell Phones & Accessories. Enjoy free shipping and exclusive deals cell phone products. Save more on your favorite galaxy waterproof cell phone,Cell Phone Cables and Cell Phone Chargers with an exclusive payless coupons. Shop cheaper items online now.


Every year, well over a million Australians travel to the United States, and many of them head to Las Vegas. There, aside from gambling, there are many things to do including a lifesize "sandbox" for grownups where you can play with diggers, bulldozers and other heavy equipment. If you want to have this kind of fun but don't want to spend the time crossing the pond, you can create your own personal fun.
Simply, invite some friends, hire a bobcat and plan one of these group activities.
If you want to emulate the Las Vegas attraction as closely as possible, you need a bit of sand. If you have a beachside property or can rent one where the owner doesn't mind you playing in the sand, that's the perfect location. Alternatively, hire a dump truck to bring the sand to you, or substitute fill dirt, freely available in many cases.
Once you have the sand or dirt, take turns in the bobcat with your mates. Just make sure the hire company is okay with multiple drivers. A bobcat is actually a better option than most of the heavy machines used in Vegas. It's one of the easiest and safest machines to drive, and as it's smaller than many machines, the hire price tends to be more reasonable.
Do you or any of your buddies need a new driveway or want to get rid of a retaining wall? Then, take the bobcat party in that direction. Bobcats don't just have to be for moving dirt. When you hire a bobcat, you can get a range of attachments including a concrete breaker.
This attachment allows you to hit concrete multiple times and watch it smash into pieces. As far as party events go, this is much more fun than smashing a pinata -- just make sure that the bystanders stand a safe distance away, and put some safety goggles in the bag of party favors so everyone has a pair.
If you cannot find any driveways, retaining walls or other concrete to smash, consider clearing a bit of nature. This is a great way to combine a party with actual work, and if you live in an area with fire risk, clearing the land with a bobcat helps to reduce the risk of the house burning.
Outside of the bush, you typically have to gain council approval if you want to clear trees and shrubs, but near the bush, you can typically clear areas close to buildings without getting special permission. Depending on where the property is, get the permission you need. Then, hire the bobcat, invite your friends over and take turns tearing stuff up. Attachments with teeth, claims, grapples and flail mowers can all help.


Of Course we can Reach the 1,5 Degree Target!
Of Course, we can Reach the 1.5 Degree Target!
Harari describes in Sapiens one of the things that makes us humans so great and powerful: we can unite behind stories. With unity comes collaboration and the achievement of incredible goals. What seems to be our most challenging task so far is making sure we limit global warming to no more than a 1.5 degree rise.
In the latest IPCC report, we learned that we need to cut all emissions in half before 2030. This is before my now newborn son turns 12 years old. It sounds impossible considering what we have achieved in the last decades. But what if there was a way we can all unite behind the same story of what we want our future to look like?
The first story that should unite us is how we can effectively reduce global emissions.
How do We Calculate Global Emissions?
First, we need to understand how global emissions can be reported from both a territorial perspective and a consumption perspective. The territorial perspective is the most common way to report on - where you basically add up all the emissions of a certain area under certain control. But it makes it easier to blame bigger countries, such as China, because they a lot of territorial emissions.
This is quite unfair because we have a much higher individual footprint in the Western world than the average Chinese, based on our consumption. The products we choose to spend money on are very often produced in another country. This adds to that country's territorial footprint, and we pass the blame somewhere else. But both our territorial-based footprint and our consumption-based footprint need to be cut in half by 2030.
See this short animation to better understand the difference between the territorial and consumption perspective.
On average we all need to cut our emissions in half the next 12 years, and it can be done if we reduce our footprints by about 5% every year.
How can we Reach the 1.5 Degree Target?
Like with all development, it starts with pioneers. First, a few individuals drastically reduce their personal footprints. They reduce it by up to 25% without reducing their quality of life. By focusing on the little things, like repairing more stuff instead of buying new goods. They increase their handprints by inspiring others to follow their lead. For example: Giving a Christmas gift voucher from a local craftsman to encourage a family member to buy locally.
When more people start prioritizing sustainability when buying, demand for sustainable solutions increases. Local craftsmen reduces their footprint making quality furniture last a lifetime, and increase their handprints repairing furniture made by others. Not only will this reduce our emissions drastically, but it will also create new local workplaces.
We already see these changes with large corporations. Just look at IKEA. They work hard to reduce their emissions from internal production and operations. They increase their handprint by selling only LED lights and launch campaigns like their Start at home campaign, where they gave concrete advice for how their customers could reduce their footprint at home.
In this way, industry will have a huge effect on all of our footprints, but only after we demand it. If we buy products that last longer, that can be repaired and that uses less energy we can force industry to develop these products. All of a sudden we have a feedback loop where your footprint is reduced without any extra effort.
And finally, we have our politicians, who can reinforce this transition incredibly fast. If they all push in the same direction. The most proactive politicians will be elected when demand for sustainable politics increase.
These politicians use their enormous public budgets to reduce footprints. For example by building schools with the lowest possible emissions. In this way, they are setting new building standards. They can increase their handprints by ensuring that we have access to bike roads, clean energy and societal regulations that make it easy for everyone to live a good life with minimum carbon emission.
If you make a few habit changes in the next three years you can easily reduce your footprint by 25%. If you use your consumer power to choose both politicians and industry that work for the same, you can help ensure structural changes.
This leads to a lower carbon society where others will live more sustainably by default. It's not going to be easy, but being part of the same optimistic story can be both meaningful and interesting. With this story I actually believe we will make the impossible possible!


YouTube has extensively evolved past being a web site for movies and audios. No matter if these parts are easy equipment, security features or entertainment methods – Mercedes make all of them to the very best they may very well be in every second. As a result of emergence of web and know-how, the world has shrunk to a world village. Google made a couple of acquisitions, online fraud firm and safe logon firm Slicklogin.\n\nHousing a fourth era Intel Atom Processor, it's swift as well as straightforward to use since it comes preinstalled with Windows 8. Another aspect value mentioning is the superb battery life that offers a consumer nice worth for money. Despite decreased household budgets within the recent economic turmoil, People are NOT downgrading from cable or satellite tv for pc to primary companies. \n\nMercedes started reaching for every thing buyers needed ranging from what is a very powerful aspect of those needs – safety systems. Now as of at present everyone knows that with changing instances we also must reform ourselves, keep us up-to-date and may comply with up the most recent development out there, not just for information, but in addition for our every day wants.\n\nThere are a significant variety of websites and blogs providing us newest tech news. Photo voltaic energy is a form of renewable-vitality which helps technologies. Nonetheless, the majority of promoting methods on the Web today sometimes cost a big quantity of funds to generate the required internet website traffic.\n\nMitigating risk and decreasing price by making use of "Electronic Discovery Methods" offered a myriad of concerns, for instance, matching time tables, securing outside IT specialists, propose and observe "E-Discovery" protocol, engagement of a special grasp to observe compliance and resolvement of disputes, use of checklist(s) containing vital steps and reminders for every step in and of a mission, working service providers, working with attorneys to find solutions to the appropriate questions, as managing vendors require particular consideration to service degree agreements (SLA'a).\n\nFor the primary time within the history of the world, atypical people may keep up on what was happening in foreign international locations with out having to attend for the next day's paper or spend money on it. Medical expertise supports and ensures continuity of life. Though the development of radio news packages was slowed somewhat by World Conflict I, it quickly made up for misplaced time, and by the 1930s the newspapers had come to worry the competition.\n\nWithin the bygone years the place internet hadn't developed into the integral part of our everyday lives and the chosen medium of relying news, breakthrough in know-how was conveyed to the masses by news papers which have been a slow, not very sturdy and cumbersome to archive medium.


text:
Feds end insider trading probe of Burr — The Department of Justice has closed its insider trading investigation of North Carolina Republican U.S. Sen. Richard Burr, who sold a large portion of his stock holdings shortly before the stock market collapsed in the early days of the pandemic.
10-year-old girl with Down syndrome held at border detention center, Mexico says
Posted June 20, 2018 1:45 a.m. EDT
By Nicole Chavez (CNN)
(CNN) — A 10-year-old Mexican girl with Down syndrome is among the thousands of children who have recently been separated from their parents at the southern US border, Mexico's foreign minister said.
The girl and her brother were sent to a detention center in McAllen,Texas, and their mother was sent to a facility about an hour away in Brownsville after the family attempted to cross the border.
Foreign Minister Luis Videgaray said the Mexican consulate along with the girl's father, a legal US resident, are working to get the girl released.
It's a "particularly painful case," Videgaray said.
The foreign minister said he was also aware of 21 Mexican children who have been separated from their parents. Most of the children have been sent back to Mexico but seven are still in US detention, he added.
At least 2,000 children have been separated from parents at the border as a result of the new "zero tolerance" policy, Department of Homeland Security officials said last week.
About 1% of the children detained at the US border were Mexican, Videgaray said, with the majority hailing from Guatemala, El Salvador and Honduras.
Videgaray condemned the practice, saying it was "cruel and inhumane."
"The Mexican government in no way promotes illegal migration," he said. "However, according to our constitutional principles and our convictions, we cannot be indifferent before an act that clearly represents a violation of human rights and that puts into a vulnerable position minors, children, including those with disabilities."
The National Down Syndrome Society said it will work with authorities to help the girl.
"Our hearts and prayers go out to this child and her family during this unprecedented and trying time. NDSS will work with the appropriate authorities to ensure she receives all the resources from us that she needs to help comfort her until she can be reunited with her father and eventually her whole family, where she belongs," the organization wrote on Facebook.
Corey Lewandowski, President Donald Trump's former campaign manager, dismissed the story of the girl while appearing Tuesday on Fox News.
"Womp womp," Lewandowski responded after former senior Democratic National Committee adviser Zac Petkanas mentioned the girl.

redpajama_set_name: RedPajamaCommonCrawl


According to a 2016 State of Small Business Report, companies across a variety of industries plan to use customer retention to grow revenue in 2017. How will they retain more customers? Their flagship strategy involves improving the customer experience.
The reasoning behind this strategy is simple. Happy customers are often loyal customers. A positive customer experience leads to reductions in churn, increases in customer advocacy, and can even create a competitive advantage over those lacking great customer satisfaction.
Here are 5 ways to improve the customer experience and grow your revenue in 2017.
Sometimes, you have a bad customer service. It does not define your brand. But, it is a great learning opportunity. What went wrong? Could it have been avoided? How will you prevent the same mistake from happening again?
While positive customer service stories can help you define your model for exceptional customer service, the negative ones are just as important. Negative customer experiences shape the way your customer experience changes to address potential or existing roadblocks to customer service success.
Here are 3 great examples of large companies who have lost customers due to a lack of great customer service. We'll also show you how to fix these issues before they happen to you (without having to spend a fortune!).
According to Gartner, product returns are on the rise, and the costs are often hidden making it difficult to address their true financial impact. You have to not only refund the customer but also pay to repack, restock, and resell the returned product(s). There is an upside to product returns that are managed correctly, however; customers who have a positive returns experience often make repeat purchases, and they are more likely to refer that retailer. That is why it is so important to identify return patterns, learn how to convert returns to future sales, and turn every RMA into a sales opportunity.


Great volunteers are a gift, especially at our Plant Sale and stream planting events. We appreciate their passion and dedication and are in awe of their energy! The Everett Herald recently featured an article about one of our most dedicated volunteers, Jim Weisenbach. Jim pops in to check in with us often and loves to talk native plants! According to Jim, "The native wildlife needs the native plants. You can't have one without the other".
Jim started working with the District when his church took on a restoration project. Wanting to learn more about native plants, he enrolled in the Backyard Habitat Steward training offered by the District. Jim was the one always snapping photos and documenting all he learned. He has been a regular, and cheerful, volunteer at the District's annual Native Plant Sale for the past four years. Snohomish Conservation District welcomes volunteers if you're interested in being added to our volunteer mailing list, use the button below.


In their weekly coffee discussion, Eric Rauch and Joe Darnell plunge into the depths of the world's favorite bevereage. It's all about recipes and brewing techniques, roasting beans to perfection, counter culture, and the fun we have together over a hot cup of joe.
Eric and Joe introduce the new coffee beverage, Cascara, which is brewed with the coffee fruit's pulpy cherry, and they help perfectionistic coffee enthusiasts take control of their angsty coffee brewing ritual. Whether you're making tea-like coffee, or seeking nirvana in every cup, the guys have thoughts for you.
Fancy Gesha coffee beans sell for more than $70 a 12 oz. bag. Eric and Joe discuss how they feel about high-end coffees and what place they deserve on your shopping list. Also, Eric discusses the process he used to create Thrasher's Christmas Blend, and Joe shares his first impressions of his new Kalita Wave dripper.
Eric and Joe enjoy an Irish coffee together and discuss its origins, how to perfect the recipe, find the right ingredients, use traditional Irish coffee mugs, and give some other tips for adventurous coffee enthusiasts to try at home.
Joe has bad news about his Chemex, Eric is weirded out by Joe's observational skills, and together they discuss ways a listener of the show could upgrade his coffee at home.
For the big Four Zero, Joe and Eric discuss changes in Joe's household that led him to switch from an AeroPress to a Chemex. In review, the guys debate the merits of a coffee-to-water ratio chart, and Joe names the factors of 'Eleven Things Only a Coffee Snob Would Understand', so you can grade yourself on your true level of eccentric coffee snobbery.
Eric and Joe wish you a happy 'Back to the Future' day, and introduce a segment of follow-up. They talk about human genes and how caffiene is metabolized, the plunging price of commodity coffee around the globe, the science behind flavoring a pumpkin spice latte, and how some coffee drinkers use salt to mask bitterness in their brew.
There are twelve Keurig coffee makers for sale at Joe's local Target. People love these devices, so what do we make of them? Eight years ago, Joe's java journey started with two of these machines. How did Keurigs lead him to artisinal coffee? Eric and Joe debate the pros and cons of K-cups and evaluate what coffee drinkers they serve best.
Believe it or not, Eric has never had a Starbucks' Pumpkin Spice Latte. So we sat down to have one of this year's pumpkin-puree-infused recipe and give it our review while we cringe at the number of toxic artificial and "natural" ingredients Starbucks uses for their fancy beverages.
Joe returns from vacation in Panama City thirsty for craft coffee in Atlanta, so he gives a report of his first visit to Octane Coffee in Midtown. Also, Eric and Joe review Stumptown Coffee Roaster's 'brew kits' intended for beginning to enthusiast levels of coffee prep at home and travel.


text:
Q: AS3 1084: Syntax error: expecting rightparen before colon i'm trying to make an AS3 shooting game, which is player right to left.
I want to make it so that, when i shoot (spawnKogel) shootAllow becomes false, and then initiates kogelCheck, which checks if the bullet (Kogel) is < -10. If that's true, shootAllow becomes True, and i can shoot again.
But i'm getting the error in the title, at the end of the spawnKogel, when I try to initialize kogelCheck. Here's my code:
package
{
import flash.display.MovieClip;
import flash.events.KeyboardEvent;
import flash.events.Event;
import flash.ui.Keyboard;
import flash.ui.Mouse;
import flash.events.MouseEvent;
import flash.display.Stage;
import flash.media.Sound;
import flash.utils.Timer;
import flash.events.TimerEvent;

public class amateurodius extends MovieClip
{
    public var schip:ruimteschip = new ruimteschip();
    public var Kogel = new Bullet();
    var sound = new lazor();
    var BGM = new Muziek();
    var backdrop = new background();
    var shootAllow:Boolean = true;

    public function amateurodius()
    {
        addEventListener(Event.ADDED_TO_STAGE, initialize);
        addEventListener(Event.ENTER_FRAME, vijandmaken);
        stage.addEventListener(KeyboardEvent.KEY_DOWN, spawnKogel);
        addEventListener(Event.ENTER_FRAME, kogelCheck);
        Mouse.hide();
    }

    function initialize(e:Event)
    {
        addChild(backdrop);
        addChild(schip);
        BGM.play();
    }

    function spawnKogel(e:KeyboardEvent):void
    {
        if (shootAllow == true)
        {
            if (e.keyCode == Keyboard.SPACE)
            {
                addChild(Kogel);
                Kogel.x = schip.x;
                Kogel.y = schip.y;
                sound.play();
                shootAllow = false;
                kogelCheck (e:Event);
            }
        }
    }

    function kogelCheck (e:Event)
    {
        if (Kogel.x < -30)
        {
        shootAllow == true;
        }
        else
        {
        shootAllow == false;
        }
    }

A: Remove the type from event when you call kogelCheck:
// Just passing on the event, doesn't need type declaration
kogelCheck (e);

redpajama_set_name: RedPajamaStackExchange


Being human calls you to experience the world in a sea of emotions. Some are life-giving, while others have stolen segments of your life from you. If you desire to live a life of abundance, happiness, and peace, you must first understand how your emotions impact your ability to do so, and most importantly, you must find a way to address painful emotions so they can be transformed. Understanding your Enneagram type will serve you in this area. Each Enneagram type carries an underlying dominant emotion. When you are under stress you will tend towards the emotion associated with your type. For example, types Eight, Nine, and One tend towards anger when they are under stress. Whereas types Two, Three, and Four tend towards shame. And types Five, Six, and Seven tend towards anxiety. While each of us will experience anger, shame, and anxiety there lies within a tendency to lean a certain way based on the Enneagram type we identify with. Understanding your unique internal voice, and the emotions that follow, is central to transformation. This voice is a combination of your life experiences, inherited tendencies, and interactions with others – all experienced through the lens of your Enneagram type.
To ignore or deny painful emotions only serves to set the stage for an emotional eruption or a disease state at some point in the future. Your body cannot ignore emotional distress any more than it can ignore the physical touch of a burning stove. You must either process the emotional pain in a timely manner or run the risk of burying the pain in your tissues. Whims of uncontrolled anger, shame, or anxiety experienced today most often find their impetus in previously experienced events in our lives. Undoubtedly, you have found it is almost unbearable to look behind the veil of anger, resentment, or fear without feeling shame and regret. However, no matter how painful life can be, you are never alone left without help. God has promised that he will strengthen you, he will help you, and he has told you that you do not need to be afraid.
Modern science is looking at the intimate connection between your emotions and disease. You may be surprised to learn that the emotions your ancestors experienced not only changed their DNA and biochemistry, but studies now show that this changed DNA is also passed onto subsequent generations when extreme trauma is experienced. Yes, you heard that correct. If your parents and grandparents experienced significant stressors in their lives, this could have a significant negative effect on your DNA.
With the use of EKGs (electrocardiographs, which are instruments that record the electrical activity of the heart) and EEGs (electroencephalographs, which record the electrical activity of the brain), scientists have observed that the heart's electrical activity is significantly greater than the electrical activity of the brain. Let's reflect for a moment on this. Our heart's energy is bigger than our brain's energy. Given this, shouldn't we be paying significant attention to our heart and the message it has for us? You know, our inner voice, our intuition? Yet, how many of us today walk around thinking, planning, and applying logic to our lives? Now, I am not saying it is bad to use our brain, quite the contrary. God gave us a human brain for a reason and it can accomplish great things! I for one, am grateful for the mind that created the computer I used to create this book. However, the modern person seems to have lost touch with their heart. We are a thinking generation, we have to see the proof, we have to see the science, and we highly value logic and reason to the point of idolizing it.
All the while we are missing the sweet spot! Our hearts hold our greatest power because they hold the healing emotion of love. Perhaps we hold our greatest power in our hearts because it is in our heart that Jesus lives. However, to trust in the power of our heart requires faith in a world beyond the world we know now, a world that we can come to know through our heart.
Hebrews 11:1-3 – Hebrews 11:1-3 – Now faith is the assurance of things hoped for, the conviction of things not seen. Indeed, by faith our ancestors received approval. By faith we understand that the worlds were prepared by the word of God, so that what is seen was made from things that are not visible.
There was another study done on the DNA changes resulting from the extreme trauma endured by Holocaust survivors. What the team found with these 32 men and women may surprise you. A marker attached to the DNA of the survivors as a result of the trauma of the Holocaust. In turn this marker altered their DNA. Additionally, this altered DNA was then passed down to their children. This is called epigenetic inheritance – the idea that one's environment imparts a change in DNA and this new DNA is then passed down to the children and grandchildren. So my thought is this – if science already reveals to us the negative change trauma has on our DNA and the DNA we pass on to the generations that follow us, is it possible that we can positively affect our DNA and pass a healthier DNA down to our children and the generations that follow? My reply is a resounding YES! And this is what The LIVE Method is all about, making a real change for today, tomorrow and all generations that follow.
Let's chat a little bit about your central nervous system, with a discussion about neuropeptides. Neuropeptides, chemical messengers in the body, team up with various biochemicals including serotonin, GABA, dopamine, and other biochemicals that all contribute to how you feel. When neuropeptides are released during emotions such as anger, shame, or anxiety, neuropeptides lock into a very specific pattern reflective of these emotions. The more you experience a particular emotion the deeper set this configuration becomes in your body's organs. This also holds true for emptions such as love, joy, and peace. Think of this akin to grooves in a record that has been played over and over again. Eventually, the grooves become rather deep. When you experience repeated emotions, your body behaves in a similar manner. If you have a long history of harmful emotions, then when life throws you a curveball, your knee-jerk reaction will be to experience harmful emotions again and again—unless you do something to interrupt this pattern.
Let's look briefly at your response to stress and how it affects your system in another way—the parasympathetic and sympathetic components of your nervous system. Consider for a moment your ability of fight or flight when exposed to a stressor. During exposure to a threatening stressor, your body will engage your sympathetic system—your fight or flight system. At this point, your body is sending most of its energy to your large muscle groups and your cardiovascular system so that you can take action. Stress hormones are released throughout your system, and your adrenals are switched into high gear. Needless to say, at this point, your body is not in a position to repair or heal itself. It is focused with survival.
A quick look at the world today and we can see that stress is the cause of many of our modern-day diseases. We are a group of people running on adrenaline! Remember, your body responds to stress when you are actually in the stressful moment and when you are thinking about a stressor—one more reason to not watch scary movies or listen to harmful gossip!
So when does your body heal itself? Healing and regeneration occur when your parasympathetic system is engaged. This happens during prayer, meditation, relaxation, and when the body is at peace. Additionally, while in a parasympathetic state, your body can digest your food optimally. Meal time can be one of the most healing moments in our lives, providing we take our time to enjoy our meal and engage in heartfelt conversation with those around our table.
It's obviously important to incorporate daily activities where you can enjoy yourself, whether that's reading, playing, praying, or spending time with your loved ones. I invite you to find a morning routine that sets a healthy intention for the day, one that is grounded in Christ. I also invite you to find a new way to deal with life's stressors. When I am upset, I often go to the perpetual adoration chapel at my parish and spend some time with Our Lord in prayer.
1 Peter 5:6, 7 – Humble yourselves therefore under the mighty hand of God, that in due time he may exalt you. Cast all your anxieties on him, for he cares about you.
If he who is in the world, Satan, created the trauma and pain that led to all the above mentioned physical and emotional responses, then do you believe that the One who is within, Jesus Christ, has the power to heal it all? Of course he does, and since this healing hasn't happened on a large, worldwide scale, we know that humanity has not yet found the right path for healing.