A Probabilistic Logic for Verifying Continuous-time Markov Chains

As a popular model of probabilistic continuous-time systems, continuous-time Markov chains (CTMCs) have been extensively studied since Kolmogorov [1]. In the recent 20 years, probabilistic continuous-time model checking receives much attention. Adopting probabilistic computational tree logic (PCTL) [2] to this context with extra multiphase timed until formulas $\Phi_{1}U^{\mathcal{T}_{1}}\Phi_{2}\cdots U^{\mathcal{T}_{K}}\Phi_{K+1}$, for state formula $\Phi$ and time interval $\mathcal{T}$, Aziz et al. proposed continuous stochastic logic (CSL) to specify the branching-time properties of CTMCs and the model-checking problem for CSL is decidable [3]. After that, efficient model-checking algorithms were developed by transient analysis of CTMCs using uniformization [4] and stratification [5] for a restricted version (path formulas are restricted to single until formulas $\Phi_{1}U^{\mathcal{I}}\Phi_{2}$) and a full version of CSL, respectively. These algorithms have been practically implemented in model checkers PRISM [6], MRMC [7] and STORM [8]. Further details can be found in an excellent survey [9].

There are also different ways to specify the linear-time properties of CTMCs. Timed automata were first used to achieve this task [10, 11, 12, 13, 14], and then metric temporal logic (MTL) [15] was also considered in this context. Subsequently, the probability of “the system being in state $s_{0}$ within five-time units after having continuously remained in state $s_{1}$” can be computed. However, some statements cannot be specified and verified because of the lack of a probabilistic linear-time temporal logic, for instance “the system being in state $s_{0}$ with high probability ($\geq 0.9$) within five-time units after having continuously remained in state $s_{1}$ with low probability ($\leq 0.1$)”. Furthermore, this probabilistic property cannot be expressed by CSL because CSL cannot express properties that are defined across several state transitions of the same time length in the execution of a CTMC.

In this paper, targeting to express the mentioned probabilistic linear-time properties, we introduce continuous-time linear logic (CLL). In particular, we adopt the viewpoint used in  [16] by regarding CTMCs as transformers of probability distributions over states. CLL studies the properties of the probability distribution execution generated by a given initial probability distribution over time. By the fundamental difference between the views of state executions and probability distribution executions of CTMCs, CLL and CSL are incomparable and complementary, as the relation between probabilistic linear-time temporal logic (PLTL) and PCTL in model checking discrete-time Markov chains [16, Section 3.3].

The atomic propositions of CLL are explained on the space of probability distributions over states of CTMCs. We apply the method of symbolic dynamics to the probability distributions of CTMCs. To be specific, we symbolize the probability value space $[0,1]$ into a finite set of intervals $\mathscr{I}=\{\mathcal{I}_{k}\subseteq[0,1]\}_{k=1}^{m}$. A probability distribution $\mu$ over its set of states $S=\{s_{0},s_{2},\ldots,s_{d-1}\}$ is then represented symbolically as a set of symbols

$$\mathbb{S}(\mu)=\{\langle s,\mathcal{I}\rangle\in S\times\mathscr{I}:\mu(s)\in\mathcal{I}\}$$

where each symbol $\langle s,\mathcal{I}\rangle$ asserts $\mu(s)\in\mathcal{I}$, i.e., the probability of state $s$ in distribution $\mu$ falls in interval $\mathcal{I}$. For example, $\langle s_{0},[0.9,1]\rangle$ means the system is in state $s_{0}$ with a probability in $0.9$ to $1$. The symbolization idea of distributions has been considered in [16]: choosing a disjoint cover of $[0,1]$:

$$\mathcal{I}=\{[0,p_{1}),[p_{1},p_{2}),...,[p_{n},1]\}.$$

Here, we remove this restriction and enrich the expressiveness of $\mathscr{I}$. A crucial fact about this symbolization is that the set $S\times\mathscr{I}$ is finite. Consequently, the (probability distribution) execution path generated by an initial probability distribution $\mu$ induces a sequence of symbols in $S\times\mathscr{I}$ over time. Therefore, the dynamics of CTMCs can be studied in terms of a (real-time) language over the alphabet $S\times\mathscr{I}$, which is the set of atomic propositions of CLL.

Different from non-probabilistic linear-time temporal logics — linear-time temporal logic (LTL) and MTL, CLL has two types of formulas: state formulas and path formulas. The state formulas are constructed using propositional connectives. The path formulas are obtained by propositional connectives and a temporal modal operator timed until $U^{\mathcal{T}}$ for a bounded time interval $\mathcal{T}$, as in MTL and CSL. The standard next-step temporal operator in LTL is meaningless in continuous-time systems since the time domain (real numbers) is uncountable. As a result, CLL can express the above mentioned probabilistic property “the system is at state $s_{0}$ with high probability ($\geq 0.9$) within 5 time units after having continuously remained at state $s_{1}$ with low probability ($\leq 0.1$)” in a path formula:

$$\varphi=\langle s_{1},[0,0.1]\rangle U^{[0,5]}\langle s_{0},[0.9,1]\rangle.$$

In this single until formula, there is a time instant $0\leq t\leq 5$ at which state $s_{1}$ with low probability transits to state $s_{0}$ with high probability. Then we illustrate this on the following timeline.

Furthermore, CLL allows multiphase timed until formulas. The semantics of the formulas focuses on relative time intervals, i.e., time can be reset as in timed automata [17, 18], while those of CSL [3] are for absolute time intervals. Subsequently, CLL can express not only relatively but also absolutely temporal properties of CTMCs.

We illustrate the significant difference between relatively temporal properties and absolutely temporal properties of CTMCs. For instance, “before probability distributions transition $\varphi$ happening in 3 to 7 time units, the system always stays at state $s_{0}$ with a high probability $(\geq 0.9)$” can be formalized in path formulae

$$\varphi^{\prime}=\langle s_{0},[0.9,1]\rangle U^{[3,7]}(\langle s_{1},[0,0.1]\rangle U^{[0,5]}\langle s_{0},[0.9,1]\rangle).$$

As we can see, there are two time instants, namely $t_{1}$ and $t_{2}$, happening distribution transitions. Time is reset to 0 after the first distribution transition happens and thus $t_{2}$ is relative to $t_{1}$. More clearly, we depict this on the following timeline.

An absolute version is “probability distribution transition $\varphi$ happens and the system always stays at state $s_{0}$ with a high probability ($\geq$ 0.9) in 3 to 7 time units”

$$\varphi^{\prime\prime}=\Box^{[3,7]}\langle s_{0},[0.9,1]\rangle\land\langle s_{1},[0,0.1]\rangle U^{[0,5]}\langle s_{0},[0.9,1]\rangle).$$

We can get a clear timeline representation by simply adding $\Box^{[3,7]}\langle s_{0},[0.9,1]\rangle$ to that of $\varphi$. Assume that $t<3$,

Time reset enriches the expressiveness of CLL but introduces more difficulties to model checking CLL than CSL. We cross this by translating relative time to the absolute one. As a result, we develop an algorithm to model check CTMCs against CLL formulas. More precisely, we reduce the model-checking problem to a reachability problem of absolute time intervals. The reachability problem corresponds to the real root isolation problem of real polynomial-exponential functions (PEFs) over the field of algebraic numbers, an extensively studied question in recent symbolic and algebraic computation community (e.g. [19, 20, 21]). By developing a state-of-the-art real root isolation algorithm, we resolve the latter problem under the assumption of the validity of Schanuel’s conjecture, a central open question in transcendental number theory [22]. This conjecture has also been the footstone of the correctness of many recent model-checking algorithms, including the decidability of continuous-time Markov decision processes [23], the synthesizing inductive invariants for continuous linear dynamical systems [24], the termination analysis for probabilistic programs with delays [25], and reachability analysis for dynamical systems [20].

In summary, the main contributions of this paper are as follows.

• •

  Introducing a probabilistic logic, namely continuous-time linear logic (CLL), for reasoning about CTMCs;

• •

  Developing a state-of-the-art real root isolation algorithm for PEFs over the field of algebraic numbers for checking atomic propositions of CLL;

• •

  Proving that model checking CTMCs against CLL formulas is decidable subject to Schanuel’s conjecture.

Organization of this paper. In the next section, we give the mathematical preliminaries used in this paper. In Section 3, we recall the view of CTMCs as distribution transformers. After that, the symbolic dynamics of CTMCs are introduced by symbolizing distributions over states of CTMCs in Section 4. In the subsequent section, we present our continuous-time probabilistic temporal logic CLL. In Section 6, we develop an algorithm to solve the CLL model checking problem. A case study and related works are shown in Sections 7 and 8, respectively. We summarize our results and point out future research directions in the final section.

For the convenience of the readers, we review basic definitions and notations of number theory, particularly Schanuel’s conjecture.

Throughout this paper, we write $\mathbb{C},\mathbb{R},\mathbb{Q}$ and $\mathbb{A}$ for the fields of all complex, real, rational and algebraic numbers, respectively. In addition, $\mathbb{Z}$ denotes the set of all integer numbers. For $\mathbb{F}\in\{\mathbb{C},\mathbb{R},\mathbb{Q},\mathbb{Z},\mathbb{A}\}$, we use $\mathbb{F}[t]$ and $\mathbb{F}^{n\times m}$ to denote the set of polynomials in $t$ with coefficients in $\mathbb{F}$ and $n$-by-$m$ matrices with every entry in $\mathbb{F}$, respectively. Furthermore, for $\mathbb{F}\in\{\mathbb{R},\mathbb{Q},\mathbb{Z}\}$, we use $\mathbb{F}^{+}$ to denote the set of positive elements (including 0) of $\mathbb{F}$.

A bounded (time) interval $\mathcal{T}$ is a subset of $\mathbb{R}^{+}$, which may be open, half-open or closed with one of the following forms:

$$[t_{1},t_{2}],[t_{1},t_{2}),(t_{1},t_{2}],(t_{1},t_{2}),$$

where $t_{1},t_{2}\in\mathbb{R}^{+}$ and $t_{2}\geq t_{1}$ ($t_{1}=t_{2}$ is only allowed in the case of $[t_{1},t_{2}]$). Here, $t_{1}$ and $t_{2}$ are called the left and right endpoints of $\mathcal{T}$, respectively. Conveniently, we use $\inf\mathcal{T}$ and $\sup\mathcal{T}$ to denote $t_{1}$ and $t_{2}$, respectively. In this paper, we only consider bounded intervals.

For reasoning about the temporal properties, we further define the addition and subtraction of (time) intervals. The expression $\mathcal{T}+t$ or $t+\mathcal{T}$, for $t\in\mathbb{R}^{+}$, denotes the interval $\{t+t^{\prime}:t^{\prime}\in\mathcal{T}\}$. Similarly, $\mathcal{T}-t$ stands for the interval $\{-t+t^{\prime}:t^{\prime}\in\mathcal{T}\}$ if $t\leq\inf\mathcal{T}$. Furthermore, for two intervals $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$,

$$\mathcal{T}_{1}+\mathcal{T}_{2}=\{t\in(t^{\prime}+\mathcal{T}_{2}):t^{\prime}\in\mathcal{T}_{1}\}=\{t_{1}+t_{2}:t_{1}\in\mathcal{T}_{1}\textrm{ and }t_{2}\in\mathcal{T}_{2}\}.$$

Two intervals $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ are disjoint if their intersection is an empty set, i.e., $\mathcal{T}_{1}\cap\mathcal{T}_{2}=\emptyset$. Let us see some concrete examples: $1+(2,3)=(3,4)$, $(2,3)-1=(1,2)$, $(2,3)+[3,4]=(5,7)$ and $(2,3),[3,4]$ are disjoint. It is obvious that all calculations of time intervals in the above are easy to be computed.

An algebraic number is a complex number that is a root of a non-zero polynomial in one variable with rational coefficients (or equivalent to integer coefficients, by eliminating denominators). An algebraic number $\alpha$ is represented by $(P,(a,b),\varepsilon)$ where $P$ is the minimal polynomial of $\alpha$, $a,b\in\mathbb{Q}$ and $a+bi$ is an approximation of $\alpha$ such that $|\alpha-(a+bi)|<\varepsilon$ and $\alpha$ is the only root of $P$ in the open ball $B(a+bi,\varepsilon)$. The minimal polynomial of $\alpha$ is the polynomial with the smallest degree in $\mathbb{Q}[t]$ such that $\alpha$ is a root of the polynomial and the coefficient of the highest-degree term is 1. Any root of $f(t)\in\mathbb{A}[t]$ is algebraic. Moreover, given the representations of $a,b\in\mathbb{A}$, the representations of $a\pm b,\frac{a}{b}$ and $a\cdot b$ can be computed in polynomial time, so does the equality checking [26].

Furthermore, a complex number is called transcendental if it is not an algebraic number. In general, it is challenging to verify relationships between transcendental numbers [27]. On the other hand, one can use the Lindemann-Weierstrass theorem to compare some transcendental numbers. The transcendence of $e$ and $\pi$ are direct corollaries of this theorem.

The following concepts are introduced to study the general relation between transcendental numbers.

By the above definition, for any transcendental number $u$, $\{u\}$ is algebraically independent over $\mathbb{Q}$, while $\{a\}$ for any algebraic number $a\in\mathbb{A}$ is not. Thus, a set of complex numbers that is algebraically independent over $\mathbb{Q}$ must consist of transcendental numbers. $\{\pi,e^{\pi\sqrt{n}}\}$ is also algebraically independent over $\mathbb{Q}$ for any positive integer $n$ [28]. Checking the algebraic independence is challenging. For example, it is still widely open whether $\{e,\pi\}$ is algebraically independent over $\mathbb{Q}$.

For example, under the usual notions of addition and multiplication, the field of complex numbers is an extension field of real numbers.

For instance, let $\mathbb{Q}(e)/\mathbb{Q}=\{a+be\mid a,b\in\mathbb{Q}\}$ and $\mathbb{Q}(\sqrt{2})/\mathbb{Q}=\{a+b\sqrt{2}\mid a,b\in\mathbb{Q}\}$ be two extension fields of $\mathbb{Q}$. Then the transcendence degree of them are $1$ and $0$, respectively, by noting that $e$ is a transcendental number and $\sqrt{2}$ is an algebraic number.

Now, Schanuel’s conjecture is ready to be presented.

Stephen Schanuel proposed this conjecture during a course given by Serge Lang at Columbia in the 1960s [22]. Schanuel’s conjecture concerns the transcendence degree of certain field extensions of the rational numbers. The conjecture, if proven, would generalize the most well-known results in transcendental number theory significantly [29, 30]. For example, the algebraical independence of $\{e,\pi\}$ would simply follow by setting $z_{1}=1$ and $z_{2}=\pi i$, and using Euler’s identity $e^{\pi i}+1=0$.

We begin with the definition of continuous-time Markov chains (CTMCs). A CTMC is a Markovian (memoryless) stochastic process that takes values on a finite state set $S$ ($|S|=d<\infty$) and evolves in continuous-time $t\in\mathbb{R}^{+}$. Formally,

A transition rate matrix $Q$ is a matrix whose off-diagonal entries $\{Q_{i,j}\}_{i\not=j}$ are nonnegative rational numbers, representing the transition rate from state $i$ to state $j$, while the diagonal entries $\{Q_{j,j}\}$ are constrained to be $-\sum_{j\not=i}Q_{i,j}$ for all $1\leq j\leq d$. Consequently, the column summations of $Q$ are all zero.

The evolution of a CTMC can be regarded as a distribution transformer. Given initial distribution $\mu\in\mathbb{Q}^{d\times 1}\in\mathcal{D(S)}$, the distribution at time $t\in\mathbb{R}^{+}$ is:

$$\mu_{t}=e^{Qt}\mu,$$

where $\mathcal{D(S)}$ is denoted as the set of all probability distributions over $S$. We call $\mathcal{D(S)}$ the probability distribution space of CTMCs. An execution path of CTMCs is a continuous function indexed by initial distribution $\mu\in\mathcal{D(S)}$:

$$\sigma_{\mu}\colon\mathbb{R}^{+}\rightarrow\mathcal{D(S)},\qquad\sigma_{\mu}(t)=e^{Qt}\mu.$$

(1)

In this section, we introduce symbolic dynamics to characterize the properties of the probability distribution space of CTMCs.

First, we fix a finite set of intervals $\mathscr{I}=\{\mathcal{I}_{k}\subseteq[0,1]\}_{k\in K}$, where the endpoints of each $\mathcal{I}_{k}$ are rational numbers. With the states $S=\{s_{0},s_{1},\cdots,s_{d-1}\}$, we define the symbolization of distributions as a function:

$$\mathbb{S}:\mathcal{D(S)}\rightarrow 2^{S\times\mathscr{I}}\qquad\mathbb{S}(\mu)=\{\langle s,\mathcal{I}\rangle\in S\times\mathscr{I}:\mu(s)\in\mathcal{I}\},$$

(2)

where $\times$ denotes the Cartesian product, and $2^{S\times\mathscr{I}}$ is the power set of $S\times\mathscr{I}$. $\langle s,\mathcal{I}\rangle\in\mathbb{S}(\mu)$ asserts that the probability of state s in distribution $\mu$ is in the interval $\mathcal{I}$. The symbolization of distributions is a generalization of the discretization of distributions with $\mathcal{I}_{k}\cap\mathcal{I}_{m}=\emptyset$ for all $k\not=m$ which was studied in [16]. This generalization increases the expressiveness of our continuous linear-time logic introduced in the next section. Now, we can represent any given probability distribution by finite symbols from $S\times\mathscr{I}$. For example, suppose

$$\mathscr{I}=\{[0,0.1],(0.1,0.9),[0.9,1],[1,1],[0.4,0.4]\},$$

(3)

and then the initial distribution $\mu$ in Example 1 is symbolized as

	$\displaystyle\mathbb{S}(\mu)=\{$	$\displaystyle\langle s_{0},[0,0.1]\rangle,\langle s_{1},(0.1,0.9)\rangle,\langle s_{2},(0.1,0.9)\rangle,$		(4)
		$\displaystyle\langle s_{3},(0.1,0.9)\rangle,\langle s_{3},[0.4,0.4]\rangle,\langle s_{4},[0,0.1]\rangle\}.$

As we can see from the above example, the symbolization of distributions on states considers the exact probabilities (singleton intervals) of the states and the range of their possibilities.

Next, we introduce the symbolization to CTMCs,

As we can see, the set of intervals is picked depending on CTMCs. Then, we extend this symbolization to the path $\sigma_{\mu}$:

$$\mathbb{S}\circ\sigma_{\mu}:\mathbb{R}^{+}\rightarrow 2^{S\times\mathscr{I}}.$$

(5)

Given a symbolized CTMC $\mathcal{SM}=(S,Q,\mathscr{I})$, the path $\sigma_{\mu}$ of CTMC $\mathcal{M}=(S,Q)$ over real numbers $\mathbb{R}^{+}$ generated by probability distribution $\mu$ induces a symbolic execution path $\mathbb{S}\circ\sigma_{\mu}$ over finite symbols $S\times\mathscr{I}$. Subsequently, the dynamics of CTMCs can be studied in terms of a language over $S\times\mathscr{I}$. In other words, we can study the temporal properties of CTMCs in the context of symbolized CTMCs.

In this section, we introduce continuous linear-time logic (CLL), a probabilistic linear-time temporal logic, to specify the temporal properties of a symbolized CTMC $\mathcal{SM}=(S,Q,\mathscr{I})$.

CLL has two types of formulas: state formulas and path formulas. The state formulas are constructed using propositional connectives. The path formulas are obtained by propositional connectives and a temporal modal operator timed until $U^{\mathcal{T}}$ for a bounded time interval $\mathcal{T}$, as in MTL and CSL. Furthermore, multiphase timed until formulas $\Phi_{0}U^{\mathcal{T}_{1}}\Phi_{1}U^{\mathcal{T}_{2}}\Phi_{2}\ldots U^{\mathcal{T}_{n}}\Phi_{n}$ are allowed to enrich the expressiveness of CLL. More importantly, time reset is involved in these multiphase formulas. Thus absolutely and relatively temporal properties of CTMCs can be studied.

The semantics of CLL state formulas is defined on the set $\mathcal{D(S)}$ of probability distributions over $S$ with the symbolized function $\mathbb{S}$ in Eq.(2) of Section 4.

• (1)

  $\mu\models\mathbf{true}$ for all probability distributions $\mu\in\mathcal{D(S)}$;

• (2)

  $\mu\models a$ iff $a\in\mathbb{S}(\mu)$;

• (3)

  $\mu\models\neg\Phi$ iff it is not the case that $\mu\models\Phi$ (or written $\mu\not\models\Phi$ );

• (4)

  $\mu\models\Phi_{1}\land\Phi_{2}$ iff $\mu\models\Phi_{1}$ and $\mu\models\Phi_{2}$.

The semantics of CLL path formulas is defined on execution paths $\{\sigma_{\mu}\}_{\mu\in\mathcal{D(S)}}$ of CTMC $\mathcal{M}=(S,Q)$.

• (1)

  $\sigma_{\mu}\models\mathbf{true}$ for all probability distributions $\mu\in\mathcal{D(S)}$;

• (2)

  $\sigma_{\mu}\models\Phi_{0}U^{\mathcal{T}_{1}}\Phi_{1}U^{\mathcal{T}_{2}}\Phi_{2}\ldots U^{\mathcal{T}_{n}}\Phi_{n}$ iff there is a time instant $t\in\mathcal{T}_{1}$ such that $\sigma_{\mu_{t}}\models\Phi_{1}U^{\mathcal{T}_{2}}\Phi_{2}\ldots U^{\mathcal{T}_{n}}\Phi_{n}$, and for any $t^{\prime}\in\mathcal{T}_{1}\cap[0,t)$, ${\mu_{t^{\prime}}}\models\Phi_{0}$, where $\sigma_{\mu_{t}}\models\Phi$ iff $\mu_{t}\models\Phi$, and $\mu_{t}$ is the distribution of the chain at time instant $t$, i.e., $\mu_{t}=e^{Qt}\mu\ \forall t\in\mathbb{R}^{+}$;

• (3)

  $\sigma_{\mu}\models\neg\varphi$ iff it is not the case that $\sigma_{\mu}\models\varphi$ (written $\sigma_{\mu}\not\models\varphi$ );

• (4)

  $\sigma_{\mu}\models\varphi_{1}\land\varphi_{2}$ iff $\sigma_{\mu}\models\varphi_{1}$ and $\sigma_{\mu}\models\varphi_{2}$.

Not surprisingly, other Boolean connectives are derived in the standard way, i.e., $\mathbf{false}=\neg\mathbf{true}$, $\Phi_{1}\lor\Phi_{2}=\neg(\neg\Phi_{1}\land\neg\Phi_{2})$ and $\Phi_{1}\rightarrow\Phi_{2}=\neg\Phi_{1}\lor\Phi_{2},$ and the path formula $\varphi$ follows the same way. Furthermore, we generalize temporal operators $\Diamond$ (“eventually”) and $\Box$ (“always”) of discrete-time systems into their timed variant $\Diamond^{\mathcal{T}}$ and $\Box^{\mathcal{T}}$, respectively, in the following:

$$\Diamond^{\mathcal{T}}\Phi=\mathbf{true}U^{\mathcal{T}}\Phi\qquad\Box^{\mathcal{T}}\Phi=\neg\Diamond^{\mathcal{T}}\neg\Phi.$$

For $n=1$ in multiphase timed until formulas, the until operator $U^{\mathcal{T}_{1}}$ is a timed variant of the until operator of LTL; the path formula $\Phi_{0}U^{\mathcal{T}_{1}}\Phi_{1}$ asserts that $\Phi_{1}$ is satisfied at some time instant in the interval $\mathcal{T}_{1}$ and that at all preceding time instants in $\mathcal{T}_{1}$, $\Phi_{0}$ holds. For example,

$$\varphi=\langle s_{1},[0,0.1]\rangle U^{[0,5]}\langle s_{0},[0.9,1]\rangle,$$

as mentioned in introduction section.

For general $n$, the CLL path formula $\Phi_{0}U^{\mathcal{T}_{1}}\Phi_{1}U^{\mathcal{T}_{2}}\Phi_{2}\ldots U^{\mathcal{T}_{n}}\Phi_{n}$ is explained over the induction on $n$. We first mention that $U^{\mathcal{T}}$ is right-associative, e.g., $\Phi_{0}U^{\mathcal{T}_{1}}\Phi_{1}U^{\mathcal{T}_{2}}\Phi_{2}$ stands for $\Phi_{0}U^{\mathcal{T}_{1}}(\Phi_{1}U^{\mathcal{T}_{2}}\Phi_{2})$. This makes time reset, i.e., $\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ do not have to be disjoint, and the starting time point of $\mathcal{T}_{2}$ is based on some time instant in $\mathcal{T}_{1}$. Recall the multiphase timed until formula in introduction section and this formula expresses a relative time property:

$$\varphi^{\prime}=\langle s_{0},[0.9,1]\rangle U^{[3,7]}(\langle s_{1},[0,0.1]\rangle U^{[0,5]}\langle s_{0},[0.9,1]\rangle),$$

which is different to the following CLL path formula representing an absolutely temporal property of CTMCs:

$$\varphi^{\prime\prime}=\Box^{[3,7]}\langle s_{0},[0.9,1]\rangle\land\langle s_{1},[0,0.1]\rangle U^{[0,5]}\langle s_{0},[0.9,1]\rangle).$$

As an example, we clarify the semantics of CLL by comparing the above two path formulas in general forms:

$$\Phi_{0}U^{\mathcal{T}_{1}}\Phi_{1}U^{\mathcal{T}_{2}}\Phi_{2}\ \text{ and }\ \Phi_{0}U^{\mathcal{T}_{1}}\Phi_{1}\land\Phi_{1}U^{\mathcal{T}_{2}}\Phi_{2}.$$

• (1)

  $\sigma_{\mu}\models\Phi_{0}U^{\mathcal{T}_{1}}\Phi_{1}U^{\mathcal{T}_{2}}\Phi_{2}$ asserts that there are time instants $t_{1}\in\mathcal{T}_{1},t_{2}\in\mathcal{T}_{2}$ such that $\mu_{t_{1}+t_{2}}\models\Phi_{2}$ and for any $t_{1}^{\prime}\in\mathcal{T}_{1}\cap[0,t_{1})$ and $t_{2}^{\prime}\in\mathcal{T}_{2}\cap[0,t_{2})$, $\mu_{t_{1}^{\prime}}\models\Phi_{0}$ and $\mu_{t_{1}+t_{2}^{\prime}}\models\Phi_{1}$, where $\mu_{t}=e^{Qt}\mu\ \forall t\in\mathbb{R}^{+}.$ This is more clear in the following timeline.
• (2)

  $\sigma_{\mu}\models\Phi_{0}U^{\mathcal{T}_{1}}\Phi_{1}\land\Phi_{1}U^{\mathcal{T}_{2}}\Phi_{2}$ asserts that there are time instants $t_{1}\in\mathcal{T}_{1},t_{2}\in\mathcal{T}_{2}$ such that $\mu_{t_{1}}\models\Phi_{1}$ and $\mu_{t_{2}}\models\Phi_{2}$, and for any $t_{1}^{\prime}\in\mathcal{T}_{1}\cap[0,t_{1})$ and $t_{2}^{\prime}\in\mathcal{T}_{2}\cap[0,t_{2})$, $\mu_{t_{1}^{\prime}}\models\Phi_{0}$ and $\mu_{t_{2}^{\prime}}\models\Phi_{1}$, where $\mu_{t}=e^{Qt}\mu\ \forall t\in\mathbb{R}^{+}$.

Before solving the model-checking problem of CTMCs against CLL formulas in the next section, we shall first discuss what can be specified in our logic CLL.

Given a CTMC $(S,Q)$, CLL path formula $\Diamond^{[0,1000]}\langle s,[1,1]\rangle$ expresses a liveness property that state $s\in S$ is eventually reached with probability one before time instant $1000$. In terms of safety properties, formula $\Box^{[100,1000]}\langle s,[0,0]\rangle$ represents that state $s\in S$ is never reached (reached with probability zero) between time instants $100$ and $1000$. Furthermore, setting the intervals nontrivial (neither $[0,0]$ or $[1,1]$), liveness and safety properties can be asserted with probabilities, such as $\Diamond^{[0,1000]}\langle s,[0.5,1]\rangle$ and $\Box^{[100,1000]}\langle s,[0,0.5]\rangle$. For multiphase timed until formula $\langle s,[0.7,1]\rangle U^{[2,3]}\langle s,[0.7,1]\rangle\ldots U^{[2,3]}\langle s,[0.7,1]\rangle,$ where the number of $U^{[2,3]}$ is 100, asserts that the probability of state $s$ is beyond $0.7$ in every time instant $2$ to $3$, and this happens at least 100 times.

Next, we can classify members of $\mathscr{I}$ as representing “low” and “high” probabilities. For example, if $\mathscr{I}$ contains 3 intervals $\{[0,0.1],(0.1,0.9),[0.9,1]\}$, we can declare the first interval as “low” and the last interval as “high”. In this case $\Box^{[10,1000)}(\langle s_{0},[0,0.1]\rangle\rightarrow\langle s_{1},[0.9,1]\rangle)$ says that, in time interval $[10,1000)$, whenever the probability of state $s_{0}$ is low, the probability of state $s_{1}$ will be high.

In this section, we provide an algorithm to model check CTMCs against CLL formulas, i.e., the following CLL model-checking problem — Problem 1 is decidable.

In particular, we show that

In the following, we prove the above theorem from checking basic formulas — atomic propositions to the most complex one — nontrivial multiphase timed until formulas. For readability, we put the proofs of all results in Appendix 0.A.

We start with the simplest case of atomic proposition $\langle s,\mathcal{I}\rangle$. By the semantics of CLL, $\mu_{t}\models\langle s,\mathcal{I}\rangle$ if and only if $\mu_{t}=e^{Qt}\mu(s)\in\mathcal{I}$. To check this, we first observe that the execution path $e^{Qt}\mu$ of CTMCs is a system of polynomial exponential functions (PEFs).

Generally, for a PEF $f(t)$ with the range in complex numbers $\mathbb{C}$, $g(t)=f(t)+f^{*}(t)$ is a PEF with the range in real numbers $\mathbb{R}$, where $f^{*}(t)$ is the complex conjugate of $f(t)$. The factor $t$ is omitted whenever convenient, i.e., $f=f(t)$. $t$ is called a root of a function $f$ if $f(t)=0$. PEFs often appear in transcendental number theory as auxiliary functions in the proofs involving the exponential function [31].

By the above lemma, for a given $t$ in some bounded time interval $\mathcal{T}$ (to be specific in the latter discussion), $e^{Qt}\mu(s)\in\mathcal{I}$ is determined by the algebraic structure of PEF $g(t)=e^{Qt}\mu(s)$ in $\mathcal{T}$. That is all maximum intervals $\mathcal{T}_{\max}\subseteq\mathcal{T}$ such that $g(t)\in\mathcal{I}$ for all $t\in\mathcal{T}_{\max}$, where interval $\mathcal{T}_{\max}\not=\emptyset$ is called maximum for $g(t)\in\mathcal{I}$ if no sub-intervals $\mathcal{T}^{\prime}\subsetneq\mathcal{T}_{\max}$ such that the property holds, i.e., $g(t)\in\mathcal{I}$ for all $t\in\mathcal{T}^{\prime}$. Then $e^{Qt}\mu(s)\in\mathcal{I}$ if and only if $t\in\mathcal{T}_{\max}$ for some maximum interval $\mathcal{T}_{\max}$. So, we aim to compute the set $\mathscr{T}$ of all maximum intervals. By the continuity of PEF $g(t)$, this can be done by identifying a real root isolation of the following PEF $f(t)$ in $\mathcal{T}$: $f(t)=(g(t)-\inf\mathcal{I})(g(t)-\sup\mathcal{I}).$

A (real) root isolation of function $f(t)$ in interval $\mathcal{T}$ is a set of mutually disjoint intervals, denoted by $\textrm{Iso}(f)_{\mathcal{T}}=\{(a_{j},b_{j})\subseteq\mathcal{T}\}$ for $a_{j},b_{j}\in\mathbb{Q}$ such that

• •

  for any $j$, there is one and only one root of $f(t)$ in $(a_{j},b_{j})$;

• •

  for any root $t^{*}$ of $f(t)$, $t^{*}\in(a_{j},b_{j})$ for some $j$.

Furthermore, if $f$ has no any root in $\mathcal{T}$, then $\textrm{Iso}(f)_{\mathcal{T}}=\emptyset$.

Although there are infinite kinds of real root isolations of $f(t)$ in $\mathcal{T}$, the number of isolation intervals equals to the number of distinct roots of $f(t)$ in $\mathcal{T}$.

Finding real root isolations of PEFs is a long-standing problem and can be at least backtracked to Ritt’s paper [32] in 1929. Some following results were obtained since the last century (e.g. [33, 34]). This problem is essential in the reachability analysis of dynamical systems, one active field of symbolic and algebraic computation. In the case of $\mathbb{F}_{1}=\mathbb{Q}$ and $\mathbb{F}_{2}=\mathbb{N}^{+}$ in [19], an algorithm named ISOL was proposed to isolate all real roots of $f(t)$. Later, this algorithm has been extended to the case of $\mathbb{F}_{1}=\mathbb{Q}$ and $\mathbb{F}_{2}=\mathbb{R}$ [20]. A variant of the problem has also been studied in [21]. The correctness of these algorithms is based on Schanuel’s conjecture. Other works are using Schanuel’s conjecture to do the root isolation of other functions, such as exp-log functions [35] and tame elementary functions [36].

By Lemma 1, we pursue this problem in the context of CTMCs. The distinct feature of solving real root isolations of PEFs in our paper is to deal with complex numbers $\mathbb{C}$, more specifically algebraic numbers $\mathbb{A}$, i.e., $\mathbb{F}_{1}=\mathbb{F}_{2}=\mathbb{A}$. At the same time, to the best of our knowledge, all the previous works can only handle the case over $\mathbb{R}$. Here, we develop a state-of-the-art real root isolation algorithm for PEFs over algebraic numbers. Thus from now on, we always assume that PEFs are over $\mathbb{A}$, i.e., $\mathbb{F}_{1}=\mathbb{F}_{2}=\mathbb{A}$ in Eq.(6). In this case, it is worth noting that whether a PEF has a root in a given interval, $\mathcal{T}\subseteq\mathbb{R}^{+}$ is decidable subject to Schanuel’s Conjecture if $\mathcal{T}$ is bounded [37], which falls in the situation we consider in this paper.

In this paper, we extend the above checking $\textrm{Iso}(f)_{\mathcal{T}}=\emptyset$ to computing $\textrm{Iso}(f)_{\mathcal{T}}$ of PEF $f(t)$.

We can compute the set $\mathscr{T}$ of all maximum intervals with the above theorem to check atomic propositions. Furthermore, we can compare the values of any real roots of PEFs, which is important in model checking general multiphase timed until formulas at the end of this section.

For model checking general state formula $\Phi$, we can also use real root isolation of some PEF to obtain the set of all maximum intervals $\mathcal{T}_{\max}$ such that $\mu_{t}\models\Phi$ for all $t\in\mathcal{T}_{\max}$. The reason is that $\Phi$ admits conjunctive normal form consisting of atomic propositions. See the proof of the following lemma in Appendix 0.A.

At last, we characterize the multiphase timed until formulas by the reachability analysis of time intervals (instants).

By the above lemma, the problem of checking multiphase timed until formulas is reduced to verify the existence of a sequence of time intervals.

Now we can show the proof of Theorem 6.1.