<figure><img src="image_1.png" /></figure>

ifip

International Federation for Information Processing

This document is the original author manuscript of a paper submitted to an IFIP
conference proceedings or other IFIP publication by Springer Nature. As such, there
may be some differences in the official published version of the paper. Such
differences, if any, are usually due to reformatting during preparation for publication or
minor corrections made by the author(s) during final proofreading of the publication
manuscript.
# On the Use of Model and Logical Embeddings for Model Checking of Probabilistic Systems

Susmoy Das(✉) and Arpit Sharma

Department of Electrical Engineering and Computer Science,
Indian Institute of Science Education and Research Bhopal, Bhopal, India
{susmoy18,arpit}@iiserb.ac.in

**Abstract.** Logics for probabilistic process algebraic models are either not very expressive or cannot be intuitively used for specifying interesting performance and reliability properties due to the presence of fixed-point operators. Moreover, the model checking machinery for these logics is very limited and is not as efficient as their state-based counterparts. Recently, new probabilistic logics and a formal framework of embeddings has been proposed which enables one to seamlessly move between state and action-based probabilistic logics. Similarly, this framework also bridges the gap between these two modeling communities by relating the state and action-based probabilistic models. We focus on implementing this framework and studying the effect of applying it on several interesting case studies from the process algebraic domain. Our results show that it enables one to efficiently verify probabilistic process algebraic models using tools and methods developed in the state-based setting. Additionally, it also enables analyzing and model checking interesting reward-based properties.

**Keywords:** Markov chain · Verification · Logic · Probabilistic · Model checking · Embedding · Process algebra

## 1 Introduction

Action-labeled discrete-time Markov chains (ADTMCs) are widely used as semantic model for amongst others probabilistic variants of ACP [6], CCS [16], CSP [23], LOTOS [26] and Petri nets [24]. Similarly, probabilistic variants of Hennessy-Milner logic, e.g. [19,30] and modal $\mu$-calculus [21,22,27,28] can be used for specifying performance and reliability properties that need to be verified. An issue with these logical formalisms is that they are either not very expressive, e.g. prHML [19,30] or cannot be easily (and intuitively) used for specifying interesting probabilistic properties due to the presence of fixed-point operators, e.g. [21,22,27,28]. Moreover, due to the limited tool support, e.g. mCRL2 [9,15] and CADP [14], probabilistic model checking of these logics is either not possible or is not as efficient as their state-based counterparts like
PRISM [20] and Storm [13,18]. For example, the mCRL2 toolset allows modeling and minimization of probabilistic systems but does not provide support for the verification or model checking of these systems and the same remains a challenge. This has also been highlighted in [9] where developers of the mCRL2 have mentioned that “*the semantic and axiomatic underpinning of the process theory for probabilities is demanding*”. Additionally, existing tools in the probabilistic process algebraic setting also do not provide support for the verification of interesting reward-based properties [3], e.g. the expected cumulative cost.

Recently, in [11,12], we have defined a theoretical framework of model and logical embeddings which can be used to bridge the gap between these two modeling and verification communities. These model embeddings can be used to construct an ADTMC from a state-labeled discrete-time Markov chain (SDTMC) [7] and an SDTMC from an ADTMC, respectively. The inverse of these embeddings have also been defined [11] which can reverse the effects of their application. Our model embeddings also support model minimization by preserving forward bisimulation, backward bisimulation and trace equivalence relations. Additionally, in order to enable these model embeddings to support probabilistic model checking of randomized systems, we have proposed the syntax and semantics of an action-based Probabilistic Computation Tree Logic (APCTL) and an action-based PCTL* (APCTL*) both of which are interpreted over ADTMCs [12]. These logics are strictly more expressive than the probabilistic variant of Hennessy-Milner logic (prHML) [12] and the property specification becomes more intuitive as compared to the variants of probabilistic modal μ-calculus. Finally, we have defined the logical embeddings between APCTL↔PCTL, APCTL*↔PCTL*, and proved that these logical embeddings combined with the model embeddings can be used for analyzing and verifying models of one domain using the tools and techniques developed for the other domain.

This paper aims to validate the efficacy and usefulness of this theoretical framework by first implementing the model embeddings and then applying it on several interesting case studies. More specifically, our implementation accepts an ADTMC model encoded in mCRL2 [9] and transforms it to an equivalent SDTMC model used by the PRISM model checker [20]. This is achieved by preprocesssing and scanning the lts file generated by the mCRL2 toolset and applying the model embeddings defined in [12] to obtain the PRISM machine readable files (MRFs) which contain information about the states, their labels, transitions and their associated probabilities. These files can be directly used for building the SDTMC models in PRISM. Additionally, we also provide the option of generating a human readable source code file in PRISM which can be opened using its graphical user interface (GUI) to inspect, parse and build the small-sized models. In order to model check the behavior, properties can be specified using the newly defined APCTL logic which are subsequently transformed into PCTL [7,17] formulae by applying our logical embeddings [12]. In the last step, the SDTMC model can be verified using PRISM model checker. Our experimental results show that this framework enables one to efficiently model check ADTMC models which otherwise cannot be verified using the mCRL2 toolset. Moreover, this framework also enables analyzing and model checking interesting reward-based properties
on probabilistic models. These observations combined with the fact that property specification in the action-based setting has become very intuitive (thanks to APCTL and APCTL*) would encourage the researchers working in the process algebraic setting to model the probabilistic behavior using mCRL2 and verify it using the state-of-the-art machinery provided by the PRISM toolset.

We believe this paper is an important step forward in the direction of seamlessly connecting the state-based and action-based probabilistic modeling and verification tools, e.g. PRISM ↔ mCRL2, and Storm ↔ mCRL2. This is possible as our theoretical framework also allows moving from SDTMCs to ADTMCs and PCTL (PCTL* [5], resp.) to APCTL (APCTL*, resp.). Our long-term goal is to enable these two important modeling and verification communities which as of now have independently developed their methods and tools to leverage the advancements made by the other community. For example, using our framework, PRISM models can be minimized by applying the bisimulation minimization algorithms of mCRL2. In the last step, inverse embeddings can be applied to obtain the reduced model in PRISM.

*Organization of the paper.* The rest of this paper is organized as follows: Sect. 2 recalls the basic concepts of DTMCs and probabilistic logics. Section 3 presents the model and logical embeddings. Section 4 presents the overall architecture of our approach followed by Sect. 5 which presents and analyzes the experimental results. Finally, Sect. 6 concludes the paper and provides pointers for future research.

## 2 Preliminaries

This section recalls the basic concepts of discrete-time Markov chains with finite state space and probabilistic logics used for specifying properties over these models.

**Definition 1.** An ADTMC is a tuple $\mathcal{D} = (S, \mathcal{A}, \mathcal{P}, s_0)$ where: (a) $S$ is a countable, nonempty set of states; (b) $\mathcal{A}$ is a set of actions which contains the special action $\tau$; (c) $\mathcal{P}: S \times \mathcal{A} \times S \to [0, 1]$ is the transition probability function satisfying $\sum_{s' \in S, a \in \mathcal{A}} \mathcal{P}(s, a, s') = 1 \ \forall s \in S$; and (d) $s_0$ is the initial state.

$\mathcal{D}$ is called finite if $S$ and $\mathcal{A}$ are finite. $\tau$ is a special action used to denote an invisible computation. Let $\rightarrow = \{(s, a; p, s') | \mathcal{P}(s, a, s') = p > 0\}$ denote the set of all the transitions for an ADTMC $\mathcal{D}$. We denote $s \xrightarrow{a,p} s'$ if $(s, a; p, s') \in \rightarrow$. An alternating sequence of states and actions $s_0\alpha_1, s_1\alpha_2, s_2\alpha_3, \dots$ s.t. $\mathcal{P}(s_i, \alpha_{i+1}, s_{i+1}) > 0 \ \forall i$ is an infinite run in an ADTMC. We denote a run by $\rho$. A finite run is of the form: $s_0\alpha_1, s_1\alpha_2, s_2\alpha_3, \dots, s_{n-1}\alpha_n, s_n$ where $\mathcal{P}(s_i, \alpha_{i+1}, s_{i+1}) > 0$ for $0 \le i < n$. The length of a finite run, denoted by $len(\rho)$ is given by the number of transitions along that run. Length of the finite run given above is $len(\rho) = n$. For an infinite run $\rho$, we have, $len(\rho) = \infty$. We denote the $n$-th state along a run $\rho$ by $\rho[n-1]$ ($\rho[0]$ denotes the first state from which the run starts) and the $n$-th action along the run by $\rho_\alpha[n]$ ($\rho_\alpha[1]$ denotes
the first transition label of the run). Let Runs(s) denote the set of all infinite
runs starting in s. Let Runs<sub>fin</sub>(s) denote the set of all finite runs starting in s.

**Definition 2 (Cylinder set [11]).** Let $s_0, \dots, s_k \in S$ with $\mathcal{P}(s_i, a_{i+1}, s_{i+1}) > 0$ for $0 \le i < k$. $\text{Cyl}(s_0 a_1, \dots, s_{k-1} a_k, s_k)$ denotes the cylinder set consisting of all runs $\rho \in \text{Runs}(s_0)$ s.t. $\rho[i] = s_i$ for $0 \le i \le k$ and $\rho_\alpha[i] = a_i$ for $1 \le i \le k$.

Let $\mathcal{F}(\text{Runs}(s_0))$ denote the smallest $\sigma$-algebra on $\text{Runs}(s_0)$ which contains all sets of the form $\text{Cyl}(s_0 a_1, \dots, s_{k-1} a_k, s_k)$ s.t. $s_0 a_1, \dots, s_{k-1} a_k, s_k$ is an alternating sequence of states and actions with $\mathcal{P}(s_i, a_{i+1}, s_{i+1}) > 0$, $(0 \le i < k)$. The probability measure $\text{Pr}$ on $\mathcal{F}(\text{Runs}(s_0))$ is the unique measure defined by induction on $k$ in the following way. Let $\text{Pr}(\text{Cyl}(s_0)) = 1$ and for $k > 0$: $\text{Pr}(\text{Cyl}(s_0 a_1, \dots, s_{k-1} a_k, s')) = \text{Pr}(\text{Cyl}(s_0 a_1, \dots, s_{k-2} a_{k-1}, s_{k-1})) \cdot \mathcal{P}(s_{k-1}, a_k, s')$. Next, we present the necessary definitions and basic concepts related to state-labeled discrete-time Markov chains (SDTMCs).

**Definition 3.** An SDTMC is a tuple $\mathcal{D} = (S, \mathcal{A}, \mathcal{P}, s_0, L)$ where: (a) $S$ is a countable, nonempty set of states; (b) $\mathcal{A}$ is the set of atomic propositions; (c) $\mathcal{P}$ is the transition probability function satisfying $\mathcal{P}: S \times S \to [0, 1]$ s.t. $\forall s \in S: \sum_{s' \in S} \mathcal{P}(s, s') = 1$; (d) $s_0$ is the initial state; and (d) $L: S \to 2^{\mathcal{A}}$ is a labeling function.

$\mathcal{D}$ is called finite if $S$ and $\mathcal{A}$ are finite. Let $\rightarrow = \{(s, p, s') \mid \mathcal{P}(s, s') = p > 0\}$ denote the set of all transitions for an SDTMC $\mathcal{D}$. We denote $s \xrightarrow{p} s'$ if $(s, p, s') \in \rightarrow$. A sequence of states $s_0, s_1, s_2, \dots$ where $\mathcal{P}(s_i, s_{i+1}) > 0 \forall i$ is an infinite path in an SDTMC. We denote a path by $\pi$. A finite path is of the form : $s_0, s_1, s_2, \dots, s_n$ where $\mathcal{P}(s_i, s_{i+1}) > 0$ for $0 \le i < n$. The length of a finite path, denoted by $\text{len}(\pi)$ is given by the number of transitions along that path. Length of the finite path given above is $\text{len}(\pi) = n$. For an infinite path $\pi$, we have, $\text{len}(\pi) = \infty$. We denote the $n$-th state along a path $\pi$ by $\pi[n-1]$ ($\pi[0]$ denotes the first state from which the path starts). Let $\text{Paths}(s)$ denote the set of all infinite paths starting in $s$. Let $\text{Paths}_{\text{fin}}(s)$ denote the set of all finite paths starting in $s$.

**Definition 4 (Cylinder set [7,31]).** Let $s_0, \dots, s_k \in S$ with $\mathcal{P}(s_i, s_{i+1}) > 0$ for $0 \le i < k$. $\text{Cyl}(s_0, \dots, s_k)$ denotes the cylinder set consisting of all paths $\pi \in \text{Paths}(s_0)$ s.t. $\pi[i] = s_i$ for $0 \le i \le k$.

Let $\mathcal{F}(\text{Paths}(s_0))$ be the smallest $\sigma$-algebra on $\text{Paths}(s_0)$ which contains all sets $\text{Cyl}(s_0, \dots, s_k)$ s.t. $s_0, \dots, s_k$ is a state sequence with $\mathcal{P}(s_i, s_{i+1}) > 0$, $(0 \le i < k)$. The probability measure $\text{Pr}$ on $\mathcal{F}(\text{Path}(s_0))$ is the unique measure defined by induction on $k$ in the following way. Let $\text{Pr}(\text{Cyl}(s_0)) = 1$ and for $k > 0$: $\text{Pr}(\text{Cyl}(s_0, \dots, s_k, s')) = \text{Pr}(\text{Cyl}(s_0, \dots, s_k)) \cdot \mathcal{P}(s_k, s')$.

Next, we recall the definition of an auxiliary logic of actions *ActFor* [12,29] which will be subsequently used for defining APCTL. The collection *ActFor* of action formulae is defined as:

$$ \chi ::= a \mid \neg\chi \mid \chi_1 \lor \chi_2 \text{ where } a \in \text{Act} \setminus \{\tau\} $$
where $\chi, \chi_1, \chi_2$ range over action formulae. We write **true** as $a \lor \neg a$, where $a$ is some arbitrarily chosen action, and **false** as $\neg \textbf{true}$. An action formula allows us to express constraints on actions that are visible (along a run or after the next step), e.g. $a \lor b$ implies that only actions $a$ or $b$ are allowed in the run. Here, **true** stands for 'all the visible actions are allowed'. The satisfaction relation for ActFor is given by: (a) $a \models_A b \Leftrightarrow a = b$; (b) $a \models_A \neg \chi \Leftrightarrow a \not\models_A \chi$; and (c) $a \models_A \chi_1 \lor \chi_2 \Leftrightarrow a \models_A \chi_1$ or $a \models_A \chi_2$. The syntax of APCTL is defined by the state formulae generated by the following grammar, where $\Phi, \Phi', \dots$ range over state formulae, $\Psi$ over run formulae and $\chi$ and $\chi'$ are action formulae (generated by ActFor):

- State Formulae: $\Phi ::= \mathbf{true} | \neg\Phi | \Phi \land \Phi' | \mathcal{P}_J(\Psi)$

- Run Formulae: $\Psi ::= \mathbf{X}_{\chi}\Phi | \mathbf{X}_{\tau}\Phi | \Phi_{\chi}\mathbf{U}\Phi' | \Phi_{\chi}\mathbf{U}_{\chi'}\Phi'$

where $J \subseteq [0, 1] \subset \mathbb{R}$ is an interval. Satisfaction of a APCTL state formula $\Phi$ by a state $s$ or a run formula $\Psi$ by a run $\rho$, notation, $\mathcal{D}, s \models_A \Phi$ ($\mathcal{D}, \rho \models_A \Psi$, resp.) or just $s \models_A \Phi$ ($\rho \models_A \Psi$, resp.) is defined inductively by:

$s \models_A \mathbf{true}$ always;

$s \models_A \neg\Phi$ iff $s \not\models_A \Phi$;

$s \models_A \Phi \land \Phi'$ iff $s \models_A \Phi$ and $s \models_A \Phi'$;

$s \models_A \mathcal{P}_J(\Psi)$ iff $\sum_{\rho \in \text{Runs}(s), \rho \models_A \Psi} \text{Pr}(\rho) \in J$;

$\rho \models_A \mathbf{X}_{\chi}\Phi$ iff $\rho_{\alpha}[1] \models_A \chi$ and $\rho[1] \models_A \Phi$;

$\rho \models_A \mathbf{X}_{\tau}\Phi$ iff $\rho_{\alpha}[1] = \tau$ and $\rho[1] \models_A \Phi$;

$\rho \models_A \Phi_{\chi}\mathbf{U}\Phi'$ iff $\exists k \ge 0$, s.t. $\rho[k] \models_A \Phi'$ and $\forall 0 \le i < k, \rho[i] \models_A \Phi$ and $\forall 1 \le j \le k, \rho_{\alpha}[j] \models_A \chi$ or $\rho_{\alpha}[j] = \tau$; and

$\rho \models_A \Phi_{\chi}\mathbf{U}_{\chi'}\Phi'$ iff $\exists k > 0$, s.t. $\rho[k] \models_A \Phi'$ and $\rho_{\alpha}[k] \models_A \chi'$, and $\forall 0 \le i < k, \rho[i] \models_A \Phi$ and $\forall 1 \le j < k, \rho_{\alpha}[j] \models_A \chi$ or $\rho_{\alpha}[j] = \tau$.

Next, we present the syntax and semantics of Probabilistic Computation Tree Logic (PCTL) [7,17]. PCTL is a probabilistic branching-time temporal logic that allows one to express the probability measures of satisfaction for a temporal property by a state in an SDTMC. The syntax is given by the following grammar where $\Phi, \Phi', \dots$ range over PCTL state formulae and $\Psi, \Psi', \dots$ range over path formulae:

- State Formulae: $\Phi ::= \mathbf{true} | a | \neg\Phi | \Phi \land \Phi' | \mathcal{P}_J(\Psi)$, for some $a \in \text{AP}$

- Path Formulae: $\Psi ::= \mathbf{X}\Phi | \Phi\mathbf{U}\Phi'$

where $J \subseteq [0, 1] \subset \mathbb{R}$ is an interval. Satisfaction of a PCTL state formula $\Phi$ by a state $s$ or a path formula $\Psi$ by a path $\pi$, notation, $s \models_S \Phi$ or $\pi \models_S \Psi$ is defined inductively by:
$$s \models_S \mathbf{true} \quad \text{always;}$$

$$s \models_S a \quad \text{iff } a \in L(s);$$

$$s \models_S \neg\Phi \quad \text{iff } s \not\models_S \Phi;$$

$$s \models_S \Phi \wedge \Phi' \quad \text{iff } s \models_S \Phi \text{ and } s \models_S \Phi';$$

$$s \models_S \mathcal{P}_J(\Psi) \quad \text{iff} \quad \sum_{\pi \in \text{Paths}(s), \pi \models_S \Psi} \text{Pr}(\pi) \in J;$$

$$\pi \models_S \mathbf{X}\Phi \quad \text{iff } \pi[1] \models_S \Phi; \text{ and}$$

$$\pi \models_S \Phi\mathbf{U}\Phi' \quad \text{iff } \exists k \ge 0, \text{ s.t. } \pi[k] \models_S \Phi' \text{ and } \forall 0 \le i < k, \pi[i] \models_S \Phi.$$

**Proposition 1.** [12] The logic APCTL is strictly more expressive than prHML.

**Theorem 1.** [12] PCTL and APCTL are equally expressive.

## 3 Model and Logical Embeddings

This section presents the model embeddings [12] which can be used to construct an SDTMC from an ADTMC. Note that these embeddings preserve strong forward, strong backward bisimulation and trace equivalence relations [11, 12]. Additionally, we also present the logical embeddings which allows one to construct an equivalent PCTL property from an APCTL formula.

**Definition 5 (sld).** Let $\mathcal{D} = (S, \mathcal{A}, \mathcal{P}, s_0)$ be an ADTMC. The embedding sld: ADTMC $\rightarrow$ SDTMC is formally defined as $\text{sld}(\mathcal{D}) = (S', \mathcal{A}'', \mathcal{P}'', s_0', L')$ s.t.

- $S' = S \cup \{(a,t) \mid \mathcal{P}(s,a,t) > 0 \text{ for some } s,t \in S \text{ and } a \neq \tau\}$,

- $\mathcal{A}' = (\mathcal{A} \setminus \{\tau\}) \cup \{\perp\}$ where $\perp \notin \mathcal{A}$,

- The rate function $\mathcal{P}'$ is defined by:

$$\mathcal{P}'(s, (a,t)) = \mathcal{P}(s, a, t) \quad \text{for all } s, t \in S \text{ s.t. } \mathcal{P}(s, a, t) > 0 \text{ and } a \neq \tau,$$

$$\mathcal{P}'(s, t) = \mathcal{P}(s, \tau, t) \quad \text{for all } s, t \in S \text{ s.t. } \mathcal{P}(s, \tau, t) > 0, \text{ and}$$

$$\mathcal{P}'((a,t), t) = 1 \quad \text{for all } (a,t) \in S' \setminus S,$$

- $s_0' = s_0$, and

- $L'(s) = \{\perp\} \quad \forall s \in S \text{ and } L'((a,t)) = \{a\}$.

Given an ADTMC $\mathcal{D}$ and an APCTL formula $\Phi$, the logical embedding $sld'_{\Phi}$ constructs an equivalent PCTL property which can be interpreted over the embedded SDTMC, i.e. $\text{sld}(\mathcal{D})$. We define the embedding $sld'_{\Phi}: \text{APCTL} \rightarrow \text{PCTL}$ inductively as follows:
$$
\begin{align*}
sdl'('true') &= true; \\
sdl'('\neg \Phi') &= '\neg sdl'('\Phi'); \\
sdl'('\Phi \wedge \Phi') &= sdl'('\Phi') \wedge sdl'('\Phi'); \\
sdl'('P_J(X_\chi \Phi)') &= P_J(X('\neg \perp \wedge \chi \wedge P_{[1,1]}(X(\perp \wedge sdl'('\Phi'))))); \\
sdl'('P_J(X_\gamma \Phi)') &= ('\perp \wedge P_J(X(\perp \wedge sdl'('\Phi')))); \\
sdl'('P_J(\Phi_\chi U \Phi')') &= P_J(((\perp \wedge sdl'('\Phi')) \vee ('\neg \perp \wedge \chi'))U(\perp \wedge sdl'('\Phi))); \text{ and} \\
sdl'('P_J(\Phi_\chi U_{\chi'} \Phi')') &= P_J(((\perp \wedge sdl'('\Phi')) \vee ('\neg \perp \wedge \chi'))U('\neg \perp \wedge \chi') \wedge \\
& \qquad P_{[1,1]}(X(\perp \wedge sdl'('\Phi')))).
\end{align*}
$$

4 Implementation

Fig. 1 shows the overall architecture of our approach. We have automated
the process of converting an ADTMC model encoded in mCRL2 [1,9] to an
SDTMC model of PRISM [2,20] by applying the model embeddings defined in
Def. 5. The code has been written in the Python programming language. For a
model encoded in mCRL2, we first construct its corresponding LPS using the
'mcrl22lps' tool supported by the mCRL2. Next, we use the 'lps' file to con-
struct an 'lts' file using the 'lps2lts' tool also supported by the mCRL2 toolset.
For both these cases, we assume that the user is going to work with the default
parameters and no other additional options of the toolset would be selected while
making these conversions. We use the .aut extension (Aldebaran format) as the
output choice for the lts file generated by the mCRL2. The lts file contains the
information about the state space and the transitions of the ADTMC model.
Our implementation (automated encoder shown in Fig. 1) takes this machine-
readable lts file in the .aut extension as its input, and then pre-processes it to
obtain the information regarding the number of states, transitions, and initial
states. This is followed by the creation of new states and transitions according to

<figure><img src="image_2.png" /><figcaption>Fig. 1. Framework Overview</figcaption></figure>
the definition of the model embedding given in Def. 5. This is done by scanning
the lts file where each line of this file has to be in one of the following forms :

(origin_state,action,destination_state)

(origin_state,action,destination_distribution)

Here, destination_distribution<fnref n="1" /> is of the form $[d_1 p_1 d_2 p_2 \dots p_{n-1} d_n]$ which means origin_state reaches state $d_i$ ($1 \le i \le n-1$) via action action with probability $p_i$ and quote origin_state reaches $d_n$ via action with probability $1 - \sum_{i=1}^{n-1} p_i$. Lines of the form $(origin\_state, action, destination\_state)$ refers to a transition from the origin_state to the destination_state via action and with probability 1. We consider the pair $(action, destination)$ for every transition and check if the action is $\tau$ (invisible) or not. If it is a $\tau$ transition, we add the transition origin_state to destination_state directly in the embedded model, copy the original probability and label both the states with the atomic proposition $\perp$. If the action $\neq \tau$, we check if the pair $(action, destination)$ has already been generated or not. If not, then we add it as a new state in the model and label it with action. Subsequently, we add two new transitions to the embedded model. The first transition goes from the origin_state to the new state with the original probability and the second transition goes from the new state to the destination_state with the probability 1. We also label the origin_state and the destination_state with the atomic proposition $\perp$. In a similar vein, we scan all the lines of the lts file and apply the above mentioned transformations.

Finally, these transformations are encoded into a set of MRFs, viz., a states
file (.sta) containing information about the states of the model, a transitions
file (.tra) containing information about all the transitions of the model and their
associated probabilities, and a labels file (.lab) which contains all the information
about the state labels. These three MRFs can be used to build the required
PRISM model directly. Additionally, we also provide the option of generating a
human readable source code file in PRISM which can be opened using its GUI to
inspect, parse and build the model. Note that it is advisable to build the models
directly using the machine-readable files of PRISM as this step is much quicker
as compared to the model building step which uses the source code files.

*Time Complexity.* In the worst case, every state of the model can reach all the other states including itself in one step (as per the design of the lts file). This means that the outer loop would be executed $|S|$ times and the inner loop searching for the *destination_state* will also be executed $|S|$ times. Hence, the worst-case time complexity of the encoding presented in this paper would be of the order of $|S|^2$. Note that this is not a limitation as our encoding can be considered as a one-time investment where the embedded PRISM model can be used for verifying multiple probabilistic and reward-based properties. Moreover, as our experiments would demonstrate (e.g. see Table 1, Table 2 and Table 3), in

<footnote n="1">¹ Note that every distribution is internally represented as a single transition in the mCRL2.</footnote>
practice the time required for transforming an lts file to the set of MRFs grows linearly with the size of the ADTMC model.

# 5 Case Studies

In order to validate the efficacy and usefulness of our approach, we have conducted detailed experiments with multiple case studies involving randomized systems. We have only selected those case studies which have already been modeled in the mCRL2 toolset. All the experiments were conducted on a workstation having 2.2 GHz 'Intel(R) Xeon(R) CPU E5-2650 v4' processor with 64 GB System Memory (4 x 16 GB DDR4) running Ubuntu 20.04 LTS. We have used the default settings of the PRISM toolset for evaluating our models. All reported times are in seconds and are obtained by taking the average of running the experiment 10 times. We report the encoding time for both the source code files and MRFs. Note that the source code files are only suitable for small-sized models as the time required for building PRISM models using these files is much higher as compared to the MRFs. Similarly, the time required for transforming an lts file to the source code files is also much higher as compared to the transformation from an lts to the MRFs. For this reason, we have used the MRFs for building the probabilistic models and for verifying them in PRISM. The detailed report of our experiments including the replication package (artefact) can be found in this repository<fnref n="2" />.

## 5.1 Monty Hall TV Show Problem

In the Monty Hall problem, there are three doors, behind one of which lies a prize. The game begins when the player selects a door with probability $\frac{1}{3}$. Next, the host of the game opens one of the remaining doors showing that it does not hide the prize. Now, the player can decide to either stick to the original choice or switch doors. If the player decides to switch doors and select the third door, the probability of winning the prize is $\frac{2}{3}$. In the mCRL2 model of this problem, the player switches his choice once the first door has been opened. It has two actions, the action prize-true indicates that the prize is won and the action prize-false has the obvious complement interpretation. Hence, the prize can be won if the door selected initially did not contain the prize. The ADTMC modeled in mCRL2 has 10 states and 9 transitions. This property can be specified in APCTL as follows:

$$ \mathcal{P} =?[(\mathbf{true})_{\mathbf{true}}\mathbf{U}_{\mathit{price}-\mathit{true}}(\mathbf{true})] $$

The corresponding PCTL formula obtained by applying our logical embeddings is as follows :

$$ \mathcal{P} =?[(\bot \land \mathbf{true}) \lor (\neg \bot \land \mathbf{true}))\mathbf{U}((\neg \bot \land \mathit{price}-\mathit{true}) \land \mathcal{P}_{[1,1]}[\mathbf{X}(\bot \land \mathbf{true})])] $$

<footnote n="2">² https://doi.org/10.5281/zenodo.7813997.</footnote>
This ADTMC can be transformed to an SDTMC using our model embeddings where the time required for generating MRFs is 0.00093 seconds. Similarly, the time required for generating the PRISM source code file is 0.00075 seconds. The SDTMC model was built in 0.0155 seconds and the time required for model checking this query was 0.0005 seconds. We also calculated the probability of not getting the prize which is $\frac{1}{3}$. This property was also verified in 0.0005 seconds.

## 5.2 Simulating a Dice Using Fair Coins

This problem aims to simulate the behavior of a 6-sided dice using a fair coin. In every step of the algorithm, a coin is tossed and there is 50% chance of taking each of the two possible choices. The algorithm terminates when you reach one of the values in the die. The mCRL2 model of this problem has 26 states and 26 transitions. By applying our model embeddings, the PRISM code file was generated in 0.00142 seconds and the MRFs were generated in 0.00188 seconds. The corresponding SDTMC has 63 states and 90 transitions. To show the correctness of this model, we need to ensure that each value from 1 to 6 should appear on the dice with a probability of $\frac{1}{6}$. This property can be specified in APCTL as follows:

$$ \mathcal{P} =?[(\mathbf{true})_{flip-true} \lor flip-false \mathbf{U}_{dice-i}(\mathbf{true})] $$

where $i = 1...6$. The corresponding PCTL formula is as follows:

$$ \mathcal{P} =?[(\bot \land \mathbf{true}) \lor (\neg \bot \land (flip - true \lor flip - false)))\mathbf{U}((\neg \bot \land dice - i) \land \mathcal{P}_{[1,1]}[\mathbf{X}(\bot \land \mathbf{true})])] $$

PRISM took 0.022 seconds to build the model and the time required for model checking each of these properties was 0.00072 seconds. The case studies section of the PRISM model checking toolset discusses an additional important property, viz., 'What are the expected number of coin tosses required for an output of the dice throw?'. The answer to this query is $\frac{11}{3}$. This is a reward-based property and it cannot be specified and verified using mCRL2. In our embedded model, we have added a reward 'Flip' with value 1 for all the states which were labeled 'flip-true' or 'flip-false' as these states indicate that a coin toss has happened in the original model. Accordingly, we calculated the following formula:

$$ R\{Flip\} =? [F(dice - 1|dice - 2|dice - 3|dice - 4|dice - 5|dice - 6)] = \frac{11}{3} $$

The result of this query was obtained in 0.00165 seconds.

## 5.3 Ant on a Grid

Richard Chatwin's famous 'Ant on a Grid' puzzle appeared in The New York Times [4] and the puzzle has also been modeled in mCRL2. The puzzle is as follows: an ant is sitting on an 8×8 2-D grid board. Initially, the ant is at the intersection of the third horizontal line and the fifth vertical line (see Fig. 2).
The ant can move to an adja-
cent intersection along the grid
lines, and it is equally likely to
move in any one of the four
directions. If the ant manages
to reach the horizontal bound-
ary, it survives; if the ant
reaches the vertical boundary,
it dies. What is the probabil-
ity that the ant survives? The
state-space of the correspond-
ing model encoded in mCRL2
has 240 states and 240 transi-
tions. The actions ‘step’, ‘live’,
and ‘dead’ model that the ant
takes a step, survives or dies,
respectively. Using the model
embeddings, we converted the
ADTMC model to an SDTMC

<figure><img src="image_3.png" /><figcaption>Fig. 2. Ant on a Grid</figcaption></figure>

model where 0.0133 and 0.0165 seconds were required for generating the source
code file and the set of MRFs, respectively. The embedded model has 577 states
and 1300 transitions. The query ‘What is the probability that the ant survives?’
and its complement can be written in APCTL as follows:

$$
\mathcal{P} =?[(\mathbf{true})_{step} \mathbf{U}_{live}(\mathbf{true})] \text{ and } \mathcal{P} =?[(\mathbf{true})_{step} \mathbf{U}_{dead}(\mathbf{true})]
$$

Another interesting query that has emerged from the discussion forum for this
puzzle is : ‘What is the probability that the ant keeps moving inside the grid,
never going to any of the edges?’. The complement of this property in APCTL
is as follows :

$$
\mathcal{P} =?[(\mathbf{true})_{\mathbf{true}} \mathbf{U}_{(\mathit{live} \lor \mathit{dead})}(\mathbf{true})]
$$

Let *p* be the probability of satisfying this property. Then the probability that the ant keeps moving inside the grid never going to any of the edges is 1 − *p*. After applying the logical embeddings, the corresponding PCTL properties are as follows :

$$
P_1 : \mathcal{P} =?[(\bot \land \mathbf{true}) \lor (\neg \bot \land \mathit{step}))\mathbf{U}((\neg \bot \land \mathit{live}) \land \mathcal{P}_{[1,1]}[\mathbf{X}(\bot \land \mathbf{true})])]
$$

$$
P_2 : \mathcal{P} =?[(\bot \land \mathbf{true}) \lor (\neg \bot \land \mathit{step}))\mathbf{U}((\neg \bot \land \mathit{dead}) \land \mathcal{P}_{[1,1]}[\mathbf{X}(\bot \land \mathbf{true})])]
$$

$$
P_3 : \mathcal{P} =?[(\bot) \lor (\neg \bot))\mathbf{U}((\neg \bot \land (\mathit{live} \lor \mathit{dead}))) \land \mathcal{P}_{[1,1]}[\mathbf{X}(\bot \land \mathbf{true})]]
$$

The probability of satisfying these PCTL properties and the time required for
encoding, model building and model checking for different grid sizes has been
shown in Table 1. Note that as we change the grid size, we have also changed the
initial position of the ant by multiplying it with the same factor by which the grid
size was increased. It can be observed that no matter what the grid is and what is
<table><caption>**Table 1.** Results for Ant on a Grid</caption><thead><tr><th rowspan="2">Grid Size</th><th rowspan="2">Initial Position</th><th colspan="2">ADTMC</th><th colspan="2">Encoding Time</th><th colspan="2">SDTMC</th><th rowspan="2">Build Time</th><th rowspan="2">Property</th><th rowspan="2">Value</th><th rowspan="2">Time</th></tr><tr><th>|S| = |T|</th><th>Code</th><th>MRF</th><th>|S'|</th><th>|T'|</th></tr></thead><tbody><tr><td rowspan="3">8 × 8</td><td rowspan="3">(5,3)</td><td rowspan="3">240</td><td rowspan="3">0.0133</td><td rowspan="3">0.0165</td><td rowspan="3">577</td><td rowspan="3">1300</td><td rowspan="3">0.066</td><td>P<sub>1</sub></td><td>0.5862</td><td>0.009</td></tr><tr><td>P<sub>2</sub></td><td>0.4138</td><td>0.011</td></tr><tr><td>P<sub>3</sub></td><td>1.0</td><td>0.006</td></tr><tr><td rowspan="3">16 × 16</td><td rowspan="3">(10,6)</td><td rowspan="3">1008</td><td rowspan="3">0.0664</td><td rowspan="3">0.069</td><td rowspan="3">2241</td><td rowspan="3">5268</td><td rowspan="3">0.195</td><td>P<sub>1</sub></td><td>0.5387</td><td>0.043</td></tr><tr><td>P<sub>2</sub></td><td>0.4613</td><td>0.044</td></tr><tr><td>P<sub>3</sub></td><td>1.00</td><td>0.015</td></tr><tr><td rowspan="3">64 × 64</td><td rowspan="3">(40,24)</td><td rowspan="3">16368</td><td rowspan="3">15.27</td><td rowspan="3">0.9998</td><td rowspan="3">33729</td><td rowspan="3">82836</td><td rowspan="3">3.375</td><td>P<sub>1</sub></td><td>0.508</td><td>4.503</td></tr><tr><td>P<sub>2</sub></td><td>0.4908</td><td>4.511</td></tr><tr><td>P<sub>3</sub></td><td>1.0</td><td>0.113</td></tr><tr><td rowspan="3">256 × 256</td><td rowspan="3">(160,96)</td><td rowspan="3">262128</td><td rowspan="3">5134.615</td><td rowspan="3">16.8762</td><td rowspan="3">528321</td><td rowspan="3">1314708</td><td rowspan="3">76.745</td><td>P<sub>1</sub></td><td>0.4967</td><td>1157.645</td></tr><tr><td>P<sub>2</sub></td><td>0.4923</td><td>1165.757</td></tr><tr><td>P<sub>3</sub></td><td>1.0</td><td>2.955</td></tr></tbody></table>

the initial position of the ant, the probability that the ant is stuck inside the grid and never arrives at any of the edges is $1 - p = 0$, where $p$ is the probability of satisfying $P_3$. We also see that as the grid size increases, the probability that the ant is going to survive decreases and goes close to a 50–50 scenario. An additional interesting query that has emerged from the discussions of the New York Times column is ‘What are the expected number of steps required by the ant to hit the boundary (dead/alive)?’. As mentioned earlier, such properties cannot be specified or analyzed using mCRL2. By adding rewards to our embedded model, we can analyze this property in PRISM. We have associated a reward structure that gives a reward of 1 to all states where ‘step’ was true. Next, we computed the following PRISM query :

$$R\{"step"\}=?\left[F\left(\{"dead"\}|\{"alive"\}\right)\right]$$

The result of this query was 11.724 and the verification time was 0.008 seconds. The result of our query matches the value obtained via other techniques reported in [4].

## 5.4 Lost Boarding Pass Problem

There is a plane with $N$ seats. The first passenger boarding the plane lost his boarding ticket and selects a random seat. Each subsequent passenger will use his own seat unless it is already occupied. In that case, he also selects a random seat. The question is ‘What is the probability that the last passenger entering the plane will sit in his own seat?’. The mCRL2 model of this problem has actions ‘enter’, ‘enter-plane’, and ‘last-passenger-his-his-own-seat’ which refer to entering the plane, picking a seat, and whether the last person boarding is sitting on his own seat, respectively. The APCTL formula for this property is as follows :

$$\mathcal{P} =?\left[(\text{true})_{\text{enter} \lor \text{enter-plane}} \land \text{last-passenger-his-his-own-seat} \land \text{true}\right]$$
The corresponding embedded formula in PCTL is :

$$
\mathcal{P} =? [((\perp \land \mathbf{true}) \lor (\neg \perp \land (\mathit{enter} \lor \mathit{enter} - \mathit{plane}))) \mathbf{U}((\neg \perp \land \mathit{last} - \mathit{passenger} - \mathit{has} - \mathit{his} - \mathit{own} - \mathit{seat} - \mathit{true}) \land \mathcal{P}_{[1,1]}[\mathbf{X}(\perp \land \mathbf{true})])]
$$

<table><caption>Table 2. Results for Lost Boarding Pass Problem</caption>
  <thead>
    <tr>
      <th rowspan="2">10<sup>N</sup></th>
      <th>ADTMC</th>
      <th colspan="2">Encoding Time</th>
      <th colspan="2">SDTMC</th>
      <th rowspan="2">Build Time</th>
      <th rowspan="2">Value</th>
      <th rowspan="2">Time</th>
    </tr>
    <tr>
      <th>|S| = |T| + 1</th>
      <th>Code</th>
      <th>MRF</th>
      <th>|S'|</th>
      <th>|T'|</th>
    </tr>
  </thead>
  <tbody>
    <tr>
      <td>1</td>
      <td>71</td>
      <td>0.0032</td>
      <td>0.0041</td>
      <td>158</td>
      <td>191</td>
      <td>0.0295</td>
      <td>0.5</td>
      <td>0.006</td>
    </tr>
    <tr>
      <td>2</td>
      <td>791</td>
      <td>0.036</td>
      <td>0.0412</td>
      <td>1778</td>
      <td>2171</td>
      <td>0.133</td>
      <td>0.5</td>
      <td>0.039</td>
    </tr>
    <tr>
      <td>3</td>
      <td>7991</td>
      <td>1.351</td>
      <td>0.3685</td>
      <td>17978</td>
      <td>21971</td>
      <td>1.525</td>
      <td>0.5</td>
      <td>1.195</td>
    </tr>
    <tr>
      <td>4</td>
      <td>79991</td>
      <td>262.2</td>
      <td>3.8421</td>
      <td>179978</td>
      <td>219971</td>
      <td>20.736</td>
      <td>0.5</td>
      <td>93.031</td>
    </tr>
    <tr>
      <td>5</td>
      <td>799991</td>
      <td>50460.889</td>
      <td>39.7816</td>
      <td>1799978</td>
      <td>2199971</td>
      <td>303.93</td>
      <td>0.5</td>
      <td>38752.431</td>
    </tr>
  </tbody>
</table>

The time required for model encoding, model building, and model checking for different values of *N* has been shown in Table 2. A reward query for the given problem is: ‘what is the expected value of “enter” at the instance when the last passenger chooses his/her seat?’. For a plane with *N* seats, this should always be *N* − 1. We have verified this reward property in PRISM using the following query :

R{"enter"}=?[F "last-passenger-has-his-own-seat-true" | "last-passenger-has-his-own-seat-false"]

The time required for verifying this query in PRISM for $N = 10, 100$, and $1000$ is 0.0007, 0.025, and 1.416 seconds, respectively.

5.5 Bounded Re-transmission Protocol (BRP)

BRP is a data link protocol for transmitting partitioned files over unreliable channels [10]. It sends a file in a number of chunks, but allows only a bounded number of re-transmissions of each chunk. Let *N* denote the number of chunks and *MAX* be the maximum allowed number of re-transmissions of each chunk. There is a channel (*K*) which facilitates this send and receive process of each chunk but the channel has a failure rate of 10%. As a result, we need another channel (*L*) which sends an acknowledgment to the sender when the sent chunk has been received successfully. Let the failure rate of *L* be 20%. Whenever a failure occurs, the sender re-attempts to send the chunk. As mentioned earlier, the number of re-attempts is bounded by *MAX* and after this the process is considered to have failed and needs to be restarted.

A ADTMC which models this protocol has been given as one of the example case studies in the mCRL2 toolset. The model hides a number of actions by labeling them as τ transitions. Here, action ‘c-aF’ denote that the sender is starting an attempt to send a chunk; ‘success-frame’ models that a chunk was
acknowledged successfully; 'c-success-file' models that all parts of the file were sent and acknowledged (transmission complete); and 'fail-transmission' models that maximum attempts have been made and the process needs to be restarted. We will check the following queries on this model: (a) 'What is the probability that the file will be sent successfully without losing a chunk more than MAX times?', (b) 'What is the probability that the file will be sent successfully after starting over a finite number of times?'. These queries can be encoded in APCTL as follows:

$$P_1 : \mathcal{P} =?[(\mathbf{true})_{(c-aF \lor \text{success-frame})} \mathbf{U}_{c-\text{success-file}}(\mathbf{true})]$$

$$P_2 : \mathcal{P} =?[(\mathbf{true})_{(c-aF \lor \text{success-frame} \lor \text{fail-transmission})} \mathbf{U}_{c-\text{success-file}}(\mathbf{true})]$$

<table><caption>**Table 3.** 'Results for BRP Problem</caption><thead><tr><th rowspan="2">(N,MAX)</th><th colspan="2">ADTMC</th><th colspan="2">Encoding Time</th><th colspan="2">SDTMC</th><th rowspan="2">Build Time</th><th rowspan="2">Property</th><th rowspan="2">Value</th><th rowspan="2">Time</th></tr><tr><th>|S| = |T|</th><th>Code</th><th>MRF</th><th>|S'|</th><th>|T'|</th></tr></thead><tbody><tr><td rowspan="2">(16,2)</td><td rowspan="2">387</td><td rowspan="2">0.0101</td><td rowspan="2">0.0122</td><td rowspan="2">516</td><td rowspan="2">612</td><td rowspan="2">0.051</td><td>P<sub>1</sub></td><td>0.952</td><td>0.016</td></tr><tr><td>P<sub>2</sub></td><td>1.0</td><td>0.005</td></tr><tr><td rowspan="2">(16,3)</td><td rowspan="2">499</td><td rowspan="2">0.0129</td><td rowspan="2">0.015</td><td rowspan="2">660</td><td rowspan="2">788</td><td rowspan="2">0.063</td><td>P<sub>1</sub></td><td>0.993</td><td>0.024</td></tr><tr><td>P<sub>2</sub></td><td>1.0</td><td>0.008</td></tr><tr><td rowspan="2">(16,4)</td><td rowspan="2">611</td><td rowspan="2">0.0187</td><td rowspan="2">0.0187</td><td rowspan="2">804</td><td rowspan="2">964</td><td rowspan="2">0.067</td><td>P<sub>1</sub></td><td>0.999</td><td>0.025</td></tr><tr><td>P<sub>2</sub></td><td>1.0</td><td>0.01</td></tr><tr><td rowspan="2">(16,5)</td><td rowspan="2">723</td><td rowspan="2">0.0187</td><td rowspan="2">0.0222</td><td rowspan="2">948</td><td rowspan="2">1140</td><td rowspan="2">0.084</td><td>P<sub>1</sub></td><td>1.0</td><td>0.031</td></tr><tr><td>P<sub>2</sub></td><td>1.0</td><td>0.015</td></tr><tr><td rowspan="2">(32,2)</td><td rowspan="2">771</td><td rowspan="2">0.0201</td><td rowspan="2">0.0236</td><td rowspan="2">1028</td><td rowspan="2">1220</td><td rowspan="2">0.085</td><td>P<sub>1</sub></td><td>0.907</td><td>0.021</td></tr><tr><td>P<sub>2</sub></td><td>1.0</td><td>0.01</td></tr><tr><td rowspan="2">(32,3)</td><td rowspan="2">995</td><td rowspan="2">0.0261</td><td rowspan="2">0.0299</td><td rowspan="2">1316</td><td rowspan="2">1572</td><td rowspan="2">0.101</td><td>P<sub>1</sub></td><td>0.986</td><td>0.049</td></tr><tr><td>P<sub>2</sub></td><td>1.0</td><td>0.029</td></tr><tr><td rowspan="2">(32,4)</td><td rowspan="2">1219</td><td rowspan="2">0.0327</td><td rowspan="2">0.0374</td><td rowspan="2">1604</td><td rowspan="2">1924</td><td rowspan="2">0.125</td><td>P<sub>1</sub></td><td>0.998</td><td>0.046</td></tr><tr><td>P<sub>2</sub></td><td>1.0</td><td>0.029</td></tr><tr><td rowspan="2">(32,5)</td><td rowspan="2">1443</td><td rowspan="2">0.0398</td><td rowspan="2">0.0442</td><td rowspan="2">1892</td><td rowspan="2">2276</td><td rowspan="2">0.164</td><td>P<sub>1</sub></td><td>1.0</td><td>0.049</td></tr><tr><td>P<sub>2</sub></td><td>1.0</td><td>0.023</td></tr><tr><td rowspan="2">(64,2)</td><td rowspan="2">1539</td><td rowspan="2">0.0430</td><td rowspan="2">0.0474</td><td rowspan="2">2052</td><td rowspan="2">2436</td><td rowspan="2">0.218</td><td>P<sub>1</sub></td><td>0.822</td><td>0.101</td></tr><tr><td>P<sub>2</sub></td><td>1.0</td><td>0.071</td></tr><tr><td rowspan="2">(64,3)</td><td rowspan="2">1987</td><td rowspan="2">0.0599</td><td rowspan="2">0.0613</td><td rowspan="2">2628</td><td rowspan="2">3140</td><td rowspan="2">0.217</td><td>P<sub>1</sub></td><td>0.972</td><td>0.105</td></tr><tr><td>P<sub>2</sub></td><td>1.0</td><td>0.071</td></tr><tr><td rowspan="2">(64,4)</td><td rowspan="2">2435</td><td rowspan="2">0.0790</td><td rowspan="2">0.0740</td><td rowspan="2">3204</td><td rowspan="2">3844</td><td rowspan="2">0.225</td><td>P<sub>1</sub></td><td>0.996</td><td>0.112</td></tr><tr><td>P<sub>2</sub></td><td>1.0</td><td>0.065</td></tr><tr><td rowspan="2">(64,5)</td><td rowspan="2">2883</td><td rowspan="2">0.0956</td><td rowspan="2">0.0876</td><td rowspan="2">3780</td><td rowspan="2">4548</td><td rowspan="2">0.305</td><td>P<sub>1</sub></td><td>1.0</td><td>0.152</td></tr><tr><td>P<sub>2</sub></td><td>1.0</td><td>0.111</td></tr></tbody></table>
The embedded PCTL formulas can be constructed by applying the logical embeddings. We report the time required for encoding, building the model, and model checking for different values of N and MAX in Table 3. An interesting reward-based property is: What are the expected number of attempts made by the sender before all the chunks of the file were sent and acknowledged, i.e. reaching a state labeled ‘c-success-file’?. We define a reward ‘caF’ and associate a reward of 1 with all the states whose label is ‘c-aF’. Next, we can formulate the query in PRISM as follows :

$$R\{"caF"\}=?\left[F \ "c\text{-}\text{success-file}\"\right]$$

For N = 16, MAX = 2, this query is verified in 0.005 seconds and the answer is 19.148. Similarly, for N = 32, MAX = 2 and N = 64, MAX = 2, the values are 39.254, and 82.53, respectively. The time required for verifying these properties is : 0.014 seconds and 0.056 seconds, respectively.

# 6 Conclusion

This paper studies the effect of applying model and logical embeddings to probabilistic process algebraic models. Our approach accepts ADTMC models encoded in mCRL2 and transforms it to an SDTMC model which can be used by the PRISM toolset for verification. The user has the flexibility to either generate the set of machine readable files (MRFs) or human readable source code files both of which can be used for building the PRISM models. Our approach enables verifying the probabilistic behavior modeled using mCRL2 by transforming the APCTL properties to the PCTL formulae and checking them on the embedded SDTMC using PRISM. Note that mCRL2 does not provide support for the verification of probabilistic models, and therefore our approach would be very useful for the performance and reliability evaluation of such systems. In a similar vein, our approach can also be used to verify interesting reward-based properties which cannot be specified using mCRL2. This research work can be extended in several interesting directions which are as follows: 1) Implement a prototypical tool that allows converting PRISM models to mCRL2 models and vice versa. This tool should also provide support for the automatic translation of logical specifications, e.g. PCTL (PCTL*, resp.) to APCTL (APCTL*, resp.) and vice versa. For example, such a tool would enable minimizing PRISM models using bisimulation algorithms implemented in mCRL2. 2) Investigate the possibility of developing similar toolsets for connecting other probabilistic model checkers, e.g. one can try to develop a tool which would allow verifying CADP models [25] using PRISM toolset and vice versa. 3) Motivated by the fact that our embeddings can also be used for analyzing reward-based properties, we also plan to extend APCTL and APCTL* with rewards and accordingly modify the logical embeddings. Finally, it would also be interesting to investigate if these model embeddings preserve weighted probabilistic equivalence [31, 32] and weak equivalence relations, e.g. weak forward bisimulation [8].
References

1. https://www.mcrl2.org/web/user_manual/index.html#

2. https://www.prismmodelchecker.org/

3. Andova, S., Hermanns, H., Katoen, J.-P.: Discrete-time rewards model-checked. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 88–104. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-40903-8_8

4. Antonick, G.: Ant on a grid. Wordplay : the crossword blog of the New York Times (2013). https://archive.nytimes.com/wordplay.blogs.nytimes.com/2013/08/12/ants-2/

5. Aziz, A., Singhal, V., Balarin, F.: It usually works: the temporal logic of stochastic systems. In: Computer Aided Verification, 7th International Conference, Liège, Belgium, 3–5 July 1995, Proceedings, pp. 155–165 (1995)

6. Baeten, J.C.M., Bergstra, J.A., Smolka, S.A.: Axiomatizing probabilistic processes: ACP with generative probabilities. Inf. Comput. **121**(2), 234–255 (1995)

7. Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)

8. Baier, C., Katoen, J.P., Hermanns, H., Wolf, V.: Comparative branching-time semantics for Markov chains. Inf. Comput. **200**(2), 149–214 (2005)

9. Bunte, O., et al.: The mCRL2 toolset for analysing concurrent systems. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 21–39. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17465-1_2

10. D'Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reachability analysis of probabilistic systems by successive refinements. In: de Alfaro, L., Gilmore, S. (eds.) PAPM-PROBMIV 2001. LNCS, vol. 2165, pp. 39–56. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44804-7_3

11. Das, S., Sharma, A.: Embeddings between state and action labeled probabilistic systems. In: SAC 2021: The 36th ACM/SIGAPP Symposium on Applied Computing, Virtual Event, Republic of Korea, 22–26 March 2021, pp. 1759–1767 (2021)

12. Das, S., Sharma, A.: Embeddings between state and action based probabilistic logics. In: Formal Aspects of Component Software - 18th International Conference, FACS 2022, Virtual Event, 10–11 November 2022, Proceedings, pp. 121–140 (2022)

13. Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A s coming: a modern probabilistic model checker. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592–600. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9_31

14. Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2010: a toolbox for the construction and analysis of distributed processes. In: Tools and Algorithms for the Construction and Analysis of Systems - 17th International Conference, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, 26–April 3 March 2011, Proceedings, pp. 372–387 (2011)

15. Groote, J.F., Keiren, J.J.A., Luttik, B., de Vink, E.P., Willemse, T.A.C.: Modelling and analysing software in mCRL2. In: Arbab, F., Jongmans, S.-S. (eds.) FACS 2019. LNCS, vol. 12018, pp. 25–48. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-40914-2_2

16. Hansson, H., Jonsson, B.: A calculus for communicating systems with time and probabilities. In: RTSS, pp. 278–287. IEEE Computer Society (1990)

17. Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Asp. Comput. **6**(5), 512–535 (1994)
18. Hensel, C., Junges, S., Katoen, J., Quatmann, T., Volk, M.: The probabilistic model checker storm. Int. J. Softw. Tools Technol. Transf. **24**(4), 589–610 (2022)

19. Hermanns, H., Parma, A., Segala, R., Wachter, B., Zhang, L.: Probabilistic logical characterization. Inf. Comput. **209**(2), 154–172 (2011)

20. Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_47

21. Larsen, K.G., Mardare, R., Xue, B.: Probabilistic mu-calculus: decidability and complete axiomatization. In: 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016, 13–15 December 2016, Chennai, India. LIPIcs, vol. 65, pp. 25:1–25:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)

22. Liu, W., Song, L., Wang, J., Zhang, L.: A simple probabilistic extension of modal mu-calculus. In: Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, 25–31 July 2015, pp. 882–888 (2015)

23. Lowe, G.: Probabilistic and prioritized models of timed CSP. Theor. Comput. Sci. **138**(2), 315–352 (1995)

24. Marsan, M.A., Conte, G., Balbo, G.: A class of generalized stochastic Petri nets for the performance evaluation of multiprocessor systems. ACM Trans. Comput. Syst. **2**(2), 93–122 (1984)

25. Mateescu, R., Requeno, J.I.: On-the-fly model checking for extended action-based probabilistic operators. Int. J. Softw. Tools Technol. Transf. **20**(5), 563–587 (2018)

26. Miguel, C., Fernández, A., Vidaller, L.: LOTOS extended with probabilistic behaviours. Formal Asp. Comput. **5**(3), 253–281 (1993)

27. Mio, M.: Game semantics for probabilistic modal μ-calculi. The University of Edinburgh, Edinburgh (2012)

28. Mio, M.: Probabilistic modal mu-calculus with independent product. Log. Methods Comput. Sci. **8**(4) (2012)

29. De Nicola, R., Vaandrager, F.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 407–419. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-53479-2_17

30. Parma, A., Segala, R.: Logical characterizations of bisimulations for discrete probabilistic systems. In: Foundations of Software Science and Computational Structures, 10th International Conference, FOSSACS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007, Braga, Portugal, March 24-April 1, 2007, Proceedings, pp. 287–301 (2007)

31. Sharma, A.: Weighted probabilistic equivalence preserves ω-regular properties. In: Schmitt, J.B. (ed.) MMB&DFT 2012. LNCS, vol. 7201, pp. 121–135. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28540-0_9

32. Sharma, A.: Reduction Techniques for Nondeterministic and Probabilistic Systems. Ph.D. thesis, RWTH Aachen University, Germany (2015)