# Verification of Continuous-time Markov Chains

Ji Guan State Key Laboratory of Computer Science, Institute of Software,
Chinese Academy of Sciences, Beijing, China. Email address:
<EMAIL_ADDRESS> Nengkun Yu Centre for Quantum Software and Information,
University of Technology Sydney, Australia. Email address:
<EMAIL_ADDRESS>
###### Abstract

In this paper, we fill the long-standing gap in the field of the verification
of continuous-time systems by proposing a linear-time temporal logic, named
continuous linear logic (CLL) and the corresponding model checking algorithm
for continuous-time Markov chains. The correctness of our model checking
algorithm depends on Schanuel’s conjecture, a central open question in
transcendental number theory.

##  1 Introduction

_Model checking_ is a method for checking whether a finite-state model of a
system meets a given specification, which is usually expressed by a temporal
logic formula. Since the 1970s, the area of checking program has been promoted
significantly through the discovery and development of the algorithmic methods
for verifying discrete-time temporal logic properties of finite-state systems
[Pnu77, CES86, LP85, QS82, VW86]. Regarding the nature of time, two dominant
logic emerged. _Linear-time temporal logics (LTL)_ was first proposed by Amir
Pnueli in 1977 [Pnu77]. After that, in 1981, Clarke and Emerson introduced
_computational tree logic (CTL)_ , a branching-time logic [CE81]. Not
surprisingly, LTL and CTL are expressively incomparable [EH86, CD88, Lam80].
CTL and LTL are used to specify qualitative properties for non-probabilistic
model checking, for example, _safety_ (nothing bad happens) and _liveness_
(something good eventually happens). When considering probabilistic transition
systems, in practice, discrete-time Markov chains with finite states are the
most successful model for probabilistic dynamical systems. By allowing for
probabilistic quantification on transition paths, Hansson and Jonsson
introduced _probabilistic computational tree logic (PCTL)_ in 1994 [HJ94]. The
verification of the linear-time property of discrete-time Markov chains was
achieved by Agrawal, Akshay, Genest, and Thiagarajan in [AAGT15]. They
introduced _probabilistic linear-time logic (PLTL)_ to reason the dynamics of
discrete-time Markov chains by adding probabilistic quantifiers on the state
space. The first three model-checking algorithms can be found in [BK08] and
the last one is given in [AAGT15]. Recently, Yu provided _quantum temporal
logic (QTL)_ , a quantum generalization of LTL, mainly targeting on the
verification of quantum programs in [Yu19].

Model checking continuous-time (real-time) systems is even nastier. For
specifying the temporal properties of (non)deterministic systems, LTL and CTL
both have been generalized from discrete-time domain to continuous-time domain
in the 1990s, named _metric temporal logic (MTL)_[Koy90] and _timed
computational temporal logic (TCTL)_ [AH94], respectively. The syntaxes of the
two continuous-time logics both use time-constrained temporal operators to
replace the corresponding versions in LTL and CTL. The semantics are _dense_ ,
i.e., the path is defined on infinitely countable time instants rather than
the non-negative real numbers. Model checking for TCTL is decidable, while
model checking for MTL is undecidable. However, model checking for _Metric
Interval Temporal Logic (MITL)_ , a fragment of MTL, is decidable. MITL was
proposed by Alur et al. in [AFH96].

After that, temporal logics are also brought in the field of the verification
of probabilistic continuous-time systems. _Continuous-time Markov chains
(CTMCs)_ form a fundamental class of probabilistic dynamical systems that have
been widely studied theoretically and practically since Kolmogorov [Kol31].
Due to a broad range of applications, continuous-time model checking is
invented for the verification of continuous-time Markov chains. Lots of
efforts have been devoted in this field to constitute the underlying
semantical model of a plethora of modeling formalisms for continuous-time
probabilistic systems, in the last two decades, cf. the recent survey [Kat16].
In a majority of the verification related studies, the continuous-time Markov
chain is viewed as a probabilistic interval transition system. The time is
measured in discrete intervals, so at each time interval the system is in a
particular state and the state will transfer to another state with an
appropriate probability after the time interval. The paths of this transition
system are viewed as computations and the goal is to use the branching-time
probabilistic temporal logic, named _continuous stochastic logic (CSL)_ , to
reason about these computations [BHHK03]. Thus the semantic of CSL is also
dense. Reusing the name presented in [ASSB00], CSL generalizes PCTL to fit for
specifying properties of continuous-time Markov chains. Thanks to this time
discretization method, efficient techniques for analyzing discrete-time Markov
chains have been developed for model checking continuous-time Markov chains.
Furthermore, model-checking algorithms developed in [BHHK03] has been
implemented in model checkers PRISM [KNP02] and MRMC [KZH+11]. As the
semantics of all three continuous-time logics MITL, TCTL and CSL are dense,
all model-checking algorithms for them are in general approximate. Table 1
overviews the current status of temporal logics.

| Linear-time | Branching-time
---|---|---
discrete-time (non)deterministic systems | LTL [Pnu77] | CTL [CE81]
continuous-time (non)deterministic systems | MTL [Koy90] | TCTL [AH94]
discrete-time probabilistic systems | PLTL [AAGT15] | PCTL [HJ94]
continuous-time probabilistic systems | ? | CSL [ASSB00]
Table 1: Overview of Temporal Logics

There is an obvious gap in the above table.

###### Problem 1

Developing a linear-time temporal logic and the corresponding model-checking
algorithm for continuous-time probabilistic systems?

This is formulated as a challenging open problem mentioned in [CHKM11a]. We
remark that linear-time temporal logics and branching-time temporal logics are
naturally incomparable from many perspectives including the expressiveness.
The techniques and results of branching-time temporal logic can not be used to
solve the above problem.

###  1.1 Conceptual Contribution

In this paper, we introduce _continuous linear logics (CLL)_ filling the
mentioned gap in temporal logics.

We adopt an alternative approach to viewing the state space of the continuous-
time Markov chain to be the set of probability distributions over the states
of the chain, which was used in analyzing discrete-time Markov chains
[AAGT15]. Thus the continuous-time Markov chain transforms initial probability
distribution continuously. CLL studies the properties of the trajectory at all
times generated from a given initial distribution. Many interesting dynamical
properties can be formulated in this setting regarding the behaviors of the
chain. For instance, in some time interval, no time will it be the case that
the probability of being in the state $s_{i}$ and the probability of being in
the state $s_{j}$ are both low, or starting from some time the system is most
likely to be in state $s_{i}$ or state $s_{j}$. To our best knowledge, such
temporal properties have not been discussed in previous literature on the
verification of continuous-time Markov chains.

We apply the method of symbolic dynamics on the distributions of continuous-
time Markov chains. To be specified in our setting, we symbolize the
probability value space $[0,1]$ into a finite set of intervals
$\mathcal{I}=\\{\mathcal{I}_{k}\\}_{k=1}^{m}$. A probability distribution
$\mu$ over its set of states $S=\\{s_{1},s_{2},...,s_{n}\\}$ is then
represented symbolically as a set of symbols $Sym=\\{s:=(j,\mathcal{I}_{k})\in
S\times\mathcal{I}:\mu_{j}\in\mathcal{I}_{k}\\}$ which asserting that the
$j$-th element of $\mu$ falls in interval $\mathcal{I}_{k}$. For example, a
special case of symbolization of distributions has been considered in
[AAGT15]: choosing a disjoint cover of $[0,1]$:
$\mathcal{I}=\\{[0,p_{1}),[p_{1},p_{2}),...,[p_{n},1]\\}$. $Sym$ is regarded
as the set of atomic propositions. It is direct to define if a probability
distribution satisfies $s\in Sym$. A crucial fact is that the set of symbols
$Sym$ is finite. Consequently, the path over real numbers generated by an
initial probability distribution $\mu$ will induce a sequence over the finite
alphabet $Sym$. Hence, given an initial distribution, the symbolic dynamics of
continuous-time Markov chains can be studied in terms of a language over the
alphabet $Sym$. Our focus here is on continuous behaviors over real numbers.

Our main motivation for studying continuous-time Markov chains in this fashion
is that in many practical applications such as biochemical networks and
queuing systems, obtaining exact estimations of the probability distributions
(including the initial distribution) may be neither feasible nor necessary.
Actually, interesting properties are stated in terms of probability ranges,
such as “low, medium, or high” or “above the threshold 0.9” rather than exact
probabilities.

We formulate the CLL in which an atomic proposition will assert that “the
current probability of the state $s_{k}$ lies in some interval”. Different
from temporal logic in the discrete-time domain, CLL has two types of
formulas: states and paths. The state type formulas are constructed under
propositional connectives. The path type formulas are obtained under
propositional connectives and the temporal model timed until in the usual way.
The timed until is bounded. The usual next-step temporal operator is not
meaningful in our logic. This is not surprised as in continuous-time, the
steps of time can not be defined because the time domain (real numbers) is
uncountable. On the other hand, keeping the time continuous instead of
discretizing time, our logic’s expressive power is incomparable with logics
such as CSL interpreted over the states transitions of the continuous-time
Markov chain.

###  1.2 Technical contribution

Based on Schanuel’s conjecture, we develop an algorithm to model checking
continuous-time Markov chains against CLL formulas.

We reduce the model checking problem to the real root isolation problem of
real polynomial-exponential functions (PEFs) over the field of the algebraic
number, a widely studied problem in recent symbolic and algebraic computation
community [GCL+17, AMW08, LHXL16]. We resolve the latter problem under the
assumption of the validity of Schanuel’s conjecture, a central open question
in transcendental number theory [Lan66].

###  1.3 Comparison with Related Work

Symbolic dynamics is a classical topic in the theory of dynamical systems
[MH38] with data storage, transmission and coding being the major application
areas [LMDB95]. The basic idea is to partition the “smooth” state space into a
finite set of blocks and represent a trajectory as a sequence of such blocks.
The symbolic dynamics of discrete-time Markov chains was verified in [AAGT15].
This idea regards distributions as the state space instead of the states of
discrete-time Markov chains and partitioning the probability value space
$[0,1]$ into finite disjoint covers (intervals). Therefore, for a given
initial distribution, there is only one single path, which PLTL can be
introduced to reason the behavior of the dynamics of distributions. In our
setting, we follow this view and symbolizing the probability value space
$[0,1]$ into finite intervals, not needed to be a partition. This
generalization endows CLL’s stronger power of expressiveness.

The verification of continuous-time Markov chains was studied in [ASSB00]
using CSL, a branching-time logic, i.e., asserting the exact temporal
properties with time continuous. The essential feature of CSL is that the path
formula is the form of nesting of bounded timed until operators only reasoning
the absolutely temporal properties (all time instants basing on one starting
time). In our CLL logic, the nesting of bounded timed until operator can also
specify relatively temporal properties. This setting significantly enriches
the expressiveness of temporal properties.

CSL was extended by adding next-step operator in [BHHK03]. For introducing the
operator, they make time discretization such that the time is measured in
discrete intervals. So at each time interval, the system is in a particular
state. Each state is associated with a set of atomic propositions and the
evolution of the system is described by an infinite sequence of symbols, which
is represented as strings. The distinct feature in our CLL setting is that the
discretization is applied on the distributions over states and we leave the
time continuous. The set of all distributions is inherently not discrete. We
fix finite intervals of $[0,1]$ representing a distribution by satisfying
these intervals, to get a coarse-grained description of the system. This
method ensures the time is real continuous such that we can exactly model
checking continuous-time Markov chains instead of approximate verification by
CSL. For more comparison, please see Table 2.

CLL | CSL
---|---
Linear-time | Branching-time
Distributions Discretization | Time Discretization
Labeling Distributions | Labeling States
Continuous Semantics | Dense Semantics
Table 2: CLL v.s. CSL

Linear-time model checking for continuous-time Markov chains has also been
studied through time discretization in [CHKM11a]. The specification is given
by deterministic timed automaton (DTA) with finite and Muller acceptance
criteria. The central question they addressed is: what is the probability of
the set of paths of continuous-time Markov chains that are accepted by a DTA.
The model checker was also developed in [BCH+11]. Furthermore, the
verification of the continuous-time Markov decision process (CTMDP) against
DTA has been studied in [CHKM11b]. A DTA can only express a property. The
logic system CLL provides the opportunity of covering many more properties we
are interested in.

###  1.4 Organization of this paper

In the next section, we give the mathematical preliminaries used in this
paper. In Section 3, we introduce the symbolic dynamics of continuous-time
Markov chains by symbolizing distributions of them. In the subsequent section,
we present our continuous-time temporal logic CLL and illustrate the model
checking problem. In Section 5, with the help of the real root isolation of
polynomial exponential functions, we develop an algorithm to solve the model
checking problem. In Section 6, we illustrate the real root isolation of
polynomial exponential functions over algebraic numbers and prove the
correctness basing on Schanuel’s conjecture. In the concluding section, we
summarize our results and point to future research directions.

##  2 Preliminaries

We use the set $\mathbb{R}^{+}$ of the nonnegative real numbers (including
$0$) to denote the time domain. A bounded (time) _interval_ $\mathcal{T}$ is a
subset of $\mathbb{R}^{+}$. Intervals may be open, half-open, or closed. Each
interval has one of the following forms:

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

where $t_{2}\geq t_{1}\geq 0$. For an interval of the above forms, $t_{1}$ is
the left endpoint of $\mathcal{T}$, and $t_{2}$ is the right endpoint of
$\mathcal{T}$. The left and right endpoints of $\mathcal{T}$ are denoted by
$\inf\mathcal{T}$ and $\sup\mathcal{T}$, respectively.

The expression $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 intervals $\\{-t+t^{\prime}:t^{\prime}\in\mathcal{T}\\}$. 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$.

Throughout this paper, we write $\mathbb{C},\mathbb{R},\mathbb{Q}$ and
$\mathbb{A}$ for the fields of complex, real, rational and algebraic numbers,
respectively.

###### Definition 1

An _algebraic number_ is any complex number that is a root of a non-zero
polynomial in one variable with rational coefficients (or equivalently with
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 $P$ of
$\alpha$ is the polynomial with the lowest degree in $\mathbb{Q}[t]$ such that
$\alpha$ is a root of the polynomial.

Furthermore, for any field
$\mathbb{F}\in\\{\mathbb{R},\mathbb{Q},\mathbb{A}\\}$, we use $\mathbb{F}^{+}$
to denote the set of positive elements (including 0) of $\mathbb{F}$ and
$\mathbb{F}[t]$ to denote the set of polynomials in $t$ with coefficients in
$\mathbb{F}$; let $\mathbb{F}^{n\times m}$ be $n$-by-$m$ matrix with every
entry on the filed of $\mathbb{F}$. For any complex number $z=a+bi$ where
$a,b\in\mathbb{R}$ and $i$ is the imaginary unit, we denote the real part and
the imaginary part of $z$ by $R(z)=a$ and $I(z)=b$, respectively. It is well
known that a root of $f(t)\in\mathbb{A}[t]$ is also 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 is the
equality checking [Coh13].

###### Definition 2

$t^{*}$ is called a _root_ of a function $f(t)$ if $f(t^{*})=0$. Furthermore,
the multiplicity of $t^{*}$ is the maximum number $m$ such that
$(t-t^{*})^{m}$ is a factor of $f(t)$, i.e., there exists a function $g(t)$
such that $f(t)=g(t)(t-t^{*})^{m}$. Furthermore, if $m=1$, then we call that
$t^{*}$ is a _single root_ ; otherwise $t^{*}$ is a _multiple root_.

###  2.1 The Real Root Isolation of Polynomial Exponential Functions

###### Definition 3

A function $f:\mathbb{R}\to\mathbb{R}$ is a _polynomial-exponential function
(PEF)_ if $f$ has the following form:

$f(t)=\sum_{k=0}^{K}f_{k}(t)e^{\lambda_{k}t}$ (1)

where for all $0\leq k\leq K<\infty$, $f_{k}(t)\in\mathbb{F}_{1}[t]$,
$\lambda_{k}\in\mathbb{F}_{2}$ and $\mathbb{F}_{1},\mathbb{F}_{2}$ are fields.
Furthermore, $\textrm{Power}(f)$ denotes the set of _power factors_ of $f(t)$,
i.e., $\textrm{Power}(f)=\\{\lambda_{k}\\}_{k=0}^{K}$.

We define the degree of $f(t)$ be the maximum degree of $f_{k}(t)$s.

We usually write this PEF as
$f(t,e^{\lambda_{0}t},e^{\lambda_{2}t},\dots,e^{\lambda_{K}t})$.

Generally, if the range of $f(t)$ is in complex numbers $\mathbb{C}$, then let
$f^{\prime}(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)$.

PEFs often appear in transcendental number theory as auxiliary functions in
proofs involving the exponential function [Bak90].

###### Definition 4

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 at least and only one root of $f(t)$ in $(a_{j},b_{j})$;

  * •

for any root $\lambda$ of $f(t)$, $\lambda\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 a real root isolation of PEFs is a long-standing problem and can at
least backtrack to Ritt’s paper [Rit29] in 1929. After that, some following
results were obtained since the last century (e.g. [AH80, Tij71]). This
problem plays an essential role 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 [AMW08],
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}$ [GCL+17]. A
variant of the problem has also been studied in [LHXL16]. The correctness of
all these algorithms is based on very famous Schanuel’s conjecture from
transcendental number theory.

We will also pursue this problem in the context of continuous-time Markov
chains. The distinct feature of solving the problem 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}$, while all the
previous works can only handle the case over $\mathbb{R}$. Up to our best
knowledge, finding a real root isolation of PEFs over $\mathbb{A}$ has not
been solved. From now on, we always assume that PEFs are over $\mathbb{A}$,
i.e., $\mathbb{F}_{1}=\mathbb{F}_{2}=\mathbb{A}$.

We remark that the algorithms for finding real root isolations of PEFs over
$\mathbb{R}$ can not be directly generalized to the case over $\mathbb{C}$.
The main reason is that there are only finitely many real roots of PEF $f(t)$
over $\mathbb{R}$ in any interval $\mathcal{T}$ [GCL+17], while there are
infinitely many real roots over $\mathbb{C}$ or $\mathbb{A}$, for example

$f(t)=e^{i\theta t}+e^{-i\theta t}=2\cos(\theta t)\
\forall\theta\in\mathbb{R}\textrm{ and }\theta\not=0$

the real roots of $f(t)$ is
$\\{t=\frac{2k\pi+\pi}{2\theta}\\}_{k\in\mathbb{N}}$, i.e., infinitely many.

###  2.2 Existence Checking of Real Roots

Usually, finding a (real) root isolation of a function $f$ bases on the
decision problem: checking whether or not there is a root of $f$ in some given
interval $\mathcal{T}$. This can be done by the following proposition in
[COW15].

######  Proposition 1 ([COW15])

Let $f:[a,b]\rightarrow\mathbb{R}$ be a function defined on a closed interval
of reals with endpoints $a,b\in\mathbb{Q}$. There is a procedure to decide the
existence of the roots of $f$ if $f$ satisfies the following conditions:

  * 1

there exists $M>0$ such that $f$ is $M$-Lipschitz, i.e., $|f(s)-f(t)|\leq
M|s-t|$ for all $s,t\in[a,b]$;

  * 2

given $t\in[a,b]\cap\mathbb{Q}$ and positive error bound
$0<\varepsilon\in\mathbb{Q}$, we can compute $q\in\mathbb{Q}$ such that
$|f(t)-q|<\varepsilon$;

  * 3

$f(a)\not=0\textrm{ and }f(b)\not=0$;

  * 4

for any $t\in(a,b)$ such that $f(t)=0$, $f^{\prime}(t)$ exists and is non-
zero, i.e., $f$ has no tangential zeros.

For our use in the latter discuss, we formate the procedure presented in
[COW15] as Algorithm 1—$Exist()$.

Algorithm 1 $Exist(f,[a,b],\delta)$

0: A $f(t)$ satisfying all conditions in Proposition 1, a closed interval
$[a,b]$ and a positive number $\delta>0$

0: true and false indicate whether or not there is a root of $f(t)$ in closed
interval $[a,b]$

1: $M\leftarrow$ the Lipschitz constant

2: $N\leftarrow\lceil\frac{4(b-a)M}{\delta}\rceil$

3: Let $s_{j}=a+\frac{(b-a)j}{N}$ for $j=0,\ldots,N$.

4: For each sample point $s_{j}$ compute $q_{j}\in\mathbb{Q}$ such that
$|q_{j}-f(s_{j})|<\delta/4.$

5: Let $f^{-}(s_{j})=q_{j}-\delta/2$ and $f^{+}(s_{j})=q_{j}+\delta/2$, and
extend $f^{-}$ and $f^{+}$ linearly between sample points.

6: if $f^{+}(t)<0$ for all $t\in[a,b]$ or $f^{-}(t)>0$ for all $t\in[a,b]$
then

7: return false

8: else if $f^{+}(s)<0$ and $f^{-}(t)>0$ for some $s,t\in[a,b]$ then

9: return true

10: else

11: return $Exist(f,[a,b],\delta/2)$

12: end if

###  2.3 Jordan Decomposition

To reduce our continuous-time model checking problem to the real root
isolation of PEFs, we need to use the _Jordan decomposition_.

###### Definition 5

A _Jordan block_ is a square matrix of the following form

$\left[\begin{matrix}\lambda&1&0&\cdots&0\\\ 0&\lambda&1&\cdots&0\\\
&&\ddots&\ddots&\\\ &&&\ddots&1\\\ 0&0&0&\cdots&\lambda\end{matrix}\right].$

A square matrix $J$ is in Jordan norm form if

$J=\left[\begin{matrix}J_{1}&&&&\\\ &J_{2}&&&\\\ &&&\ddots&\\\
&&&&J_{n}\end{matrix}\right],$

where $J_{k}$ is a Jordan blocks for each $1\leq k\leq n$.

Because $\mathbb{A}$ is algebraic closed, we know that

###### Proposition 2

Any matrix $A\in\mathbb{Q}^{n\times n}$ is algebraically similar to a matrix
in Jordan normal form over algebraic number field $\mathbb{A}$. Namely, there
exists some invertible $P\in\mathbb{A}^{n\times n}$ and
$J\in\mathbb{A}^{n\times n}$ in Jordan form such that $A=P^{-1}JP$, where
$\mathbb{A}^{n\times n}$ is the set of all $n$-by-$n$ matrices with every
entry being algebraic number.

###  2.4 Transcendental Number Theory

In the latter discussion, we will see that transcendental number theory can be
applied to compare time instants when the values are _transcendental numbers_.
A transcendental number is a complex number that is not an algebraic number,
such as $\pi,e^{\pi}$.

In general, it is extremely difficult to verify relationships between two
transcendental numbers [Ric97]. But for some transcendental numbers
represented by PEFs can be compared with the help of Lindemann-Weierstrass
theorem.

######  Theorem 1 (Lindemann-Weierstrass theorem)

Let $\eta_{1},\cdots,\eta_{n}$ be pairwise distinct algebraic complex numbers.
Then there exists no equation $\sum_{k}\lambda_{k}e^{\eta_{k}}=0$ in which
$\lambda_{1},\cdots,\lambda_{n}$ are algebraic numbers and are not all zero.

The following fact was observed in [ASSB00] by Lindemann-Weierstrass theorem.

###### Observation 1

Given a real number $r\in\mathbb{R}$ of the form $\sum_{k}\mu_{k}e^{\eta_{k}}$
where ${\mu_{k}}^{\prime}s$ and ${\eta_{k}}^{\prime}s$ are algebraic complex
numbers, and the ${\eta_{k}}^{\prime}s$ are pairwise distinct, there is an
effective procedure to compare the values of $r$ and $c$ for any
$c\in\mathbb{Q}$.

First by Lindemann-Weierstrass theorem, we know that $r=c$ if and only if
$r=c=0$ or $c=-\lambda_{k}$ for some $k$ with $\eta_{k}=0$. Then the main idea
of the above observation is for each $k$, $e^{\eta_{k}}$ can be approximated
with an error of less than $\varepsilon$ (when $\varepsilon<1$) by taking the
first $\lceil 3|\eta_{k}|^{2}/\varepsilon\rceil+1$ terms of the Maclaurin
expansion for $e^{\eta_{k}}$. This can be extended to obtain an upper bound on
the number of terms needed to approximate $r$ to within $\varepsilon$. Since
the individual terms in the Maclaurin expansion are algebraic functions of the
$\eta_{k}$’s, it follows that the approximations are algebraic. Then we can
check if $r>c$ by the comparision between the approximations and $c$.

For finding a real root isolation of PEFs, we also need the famous open
problem Schanuel’s conjecture to factoring a PEF into finite _irreducible_
PEFs. Before introducing the conjecture, we need more concepts.

######  Definition 6 (Algebraic independence)

A set of complex numbers $S=\\{a_{1},\cdots,a_{n}\\}$ is algebraically
independent over $\mathbb{Q}$ if the elements of $S$ do not satisfy any
nontrivial (non-constant) polynomial equation with coefficients in
$\mathbb{Q}$.

By the above definition, for any transcendental number $u$, $\\{u\\}$ is
algebraically independent over $\mathbb{Q}$, $\\{a\\}$ for any algebraic
number $a\in\mathbb{A}$ is not. Thus, a number in an algebraically independent
set over $\mathbb{Q}$ must be a transcendental number. Excluding singlet sets,
$\\{\pi,e^{\pi\sqrt{n}}\\}$ is also algebraically independent over
$\mathbb{Q}$ for any positive integer $n$ [Nes96]. Checking the algebraic
independence is a challenging problem, and there are many open problems. It is
still not known whether $\\{e,\pi\\}$ is algebraically independent over
$\mathbb{Q}$.

######  Definition 7 (Transcendence degree)

Let $L$ be a field extension of $\mathbb{Q}$, the transcendence degree of $L$
over $\mathbb{Q}$ is defined as the largest cardinality of an algebraically
independent subset of $L$ over $\mathbb{Q}$.

For instance, let $\mathbb{Q}(e)=\\{a+be\mid a,b\in\mathbb{Q}\\}$ and
$\mathbb{Q}(\sqrt{2})=\\{a+b\sqrt{2}\mid a,b\in\mathbb{Q}\\}$ be two field
extensions 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 a algebraic number.

######  Conjecture 2 (Schanuel’s conjecture)

Given any complex numbers $z_{1},\cdots,z_{n}$ that are linearly independent
over $\mathbb{Q}$, the extension field
$\mathbb{Q}(z_{1},...,z_{n},e^{z_{1}},...,e^{z_{n}})$ has transcendence degree
of at least $n$ over $\mathbb{Q}$.

This conjecture was proposed by Stephen Schanuel during a course given by
Serge Lang at Columbia in the 1960s [Lan66]. Schanuel’s conjecture concerning
the transcendence degree of certain field extensions of the rational numbers.
The conjecture, if proven, would generalize the most known results in
transcendental number theory [Ter08, MW96]. For example, $\\{e,\pi\\}$ is
algebraically independent simply by setting $z_{1}=1$ and $z_{2}=\pi i$, and
using _Euler’s identity_ $e^{\pi i}+1=0$.

###### Corollary 1

[GCL+17, Corollary 3] Let $a_{1},\ldots,a_{n}$ be algebraic numbers that are
linearly independent over $\mathbb{Q}$. Based on Schanuel’s conjecture, the
transcendence degree of the field extension
$\mathbb{Q}(t,e^{a_{1}t},\ldots,e^{a_{n}t})$ is at least $n$ if $t\not=0$.

###  2.5 Factoring Multivariate Polynomials over Algebraic Number Fields

Recall that PEF $f(t)$ in Eq.(1) over algebraic number field has the form:

$f(t)=\sum_{k=0}^{K}f_{k}(t)e^{\lambda_{k}t}$ (2)

where $f_{k}(t)\in\mathbb{A}[t]$ and $\lambda_{k}\in\mathbb{A}$ for all $0\leq
k\leq K$.

$f(t)$ is called _exponential_ if there exists some $a,\eta\in\mathbb{C}$ such
that

$f(t)\equiv a\cdot e^{\eta t}.$

$f(t,e^{a_{1}t},\ldots,e^{a_{n}t})$ is called _irreducible_ in $\mathbb{A}$ if
it has only trivial factoring as follows

$f(t,e^{a_{1}t},\ldots,e^{a_{n}t})=e^{\mu t}\cdot
g(t,e^{b_{1}t},\ldots,e^{b_{n}t}),$

for some $\mu,b_{i}\in\mathbb{A}$ and a PEF $g(t)$.

We are interested in factoring a non exponential PEF into product of PEFs,
i.e.,

$f(t,e^{a_{1}t},\ldots,e^{a_{n}t})=e^{\mu t}\cdot
f_{1}^{m_{1}}(t,e^{b_{1,1}t},\ldots,e^{b_{1,n_{1}}t})\cdots
f_{s}^{m_{s}}(t,e^{b_{s,1}t},\ldots,e^{b_{s,n_{s}}t}),$

for some $\mu,b_{i,j}\in\mathbb{C}$, and non-exponential
$f_{i}(t,e^{b_{1,1}t},\ldots,e^{b_{1,n_{1}}t})$.

###### Definition 8

A PEF $f(t)$ is square free if

$f(t)\not\equiv f_{1}^{2}(t)\cdots f_{s}(t)$

where $f_{i}(t)$s are PEFs and $f_{1}(t)$ is not exponential.

There is an efficient algorithm to factor multivariate polynomials over
$\mathbb{A}$ with polynomial-time complexity in the degrees of the polynomial
to be factored [Len87]. The main idea is that the multivariate polynomial
$f(x_{1},\ldots,x_{n})$ is first reduced to a polynomial in just one variable
by substituting properly selected integers
$(e.g.,x_{2}=b_{1},\ldots,x_{n}=b_{n})$ for all but one variable $x_{1}$. The
resulting univariate polynomial $f(x_{1},b_{1},\ldots,b_{n})$ is then factored
over $\mathbb{A}$. Then the well-known algorithm for factoring univariate
polynomial over rational numbers [LLL+82] can be generalized to factor
$f(x_{1},b_{1},\ldots,b_{n})$.

We can employ this algorithm for factoring multivariate polynomials into the
factoring of PEFs, an important step to get real root isolation of PEF $f(t)$
over algebraic number field $\mathbb{A}$.

If $f(t)$ is exponential, the factoring is trivial. Assume $f(t)$ is not
exponential, and we have the following factoring,

$f(t)=\sum_{k=0}^{K}f_{k}(t)e^{\lambda_{k}t}=f_{1}^{m_{1}}(t,e^{b_{1,1}t},\ldots,e^{b_{1,n_{1}}t})\cdots
f_{s}^{m_{s}}(t,e^{b_{s,1}t},\ldots,e^{b_{s,n_{s}}t}),$

where $f_{i}(t)$s are not exponential.

We know that $\lambda_{k}$ can be written as some natural number combinations
of $b_{i,j}$’s and this is sufficient requirement for $b_{i,j}$’s by expanding
this equation observing that $\sum_{k=0}^{K}f_{k}(t)e^{\lambda_{k}t}\equiv 0$
if and only if $f_{k}(t)\equiv 0$ for all $k$.

We first compute an integral basis of $\lambda_{0},\ldots,\lambda_{K}$, says
$a_{1},\ldots,a_{n}$. Then $a_{1},\ldots,a_{n}$ are linearly independent over
$\mathbb{Q}$, and $f(t)$ is a _multivariate polynomial_ of
$t,e^{a_{1}t},\ldots,e^{a_{n}t},e^{-a_{1}t},\ldots,e^{-a_{n}t}$, denoted by
$P(t,e^{a_{1}t},\ldots,e^{a_{n}t},e^{-a_{1}t},\ldots,e^{-a_{n}t})$. We can
always choose $b_{i,j}$ to be some natural number combination of
$a_{1},\ldots,a_{n},-a_{1},\ldots,-a_{n}$, thus, $f_{i}(t)$ are all
_multivariate polynomials_ of
$t,e^{a_{1}t},\ldots,e^{a_{n}t},e^{-a_{1}t},\ldots,e^{-a_{n}t}$, denoted by
$P_{i}(t,e^{a_{1}t},\ldots,e^{a_{n}t},e^{-a_{1}t},\ldots,e^{-a_{n}t})$.
Therefore,

$\displaystyle
P(t,e^{a_{1}t},\ldots,e^{a_{n}t},e^{-a_{1}t},\ldots,e^{-a_{n}t})=\Pi_{i=1}^{s}P_{i}^{m_{i}}(t,e^{a_{1}t},\ldots,e^{a_{n}t},e^{-a_{1}t},\ldots,e^{-a_{n}t})$

Comparing the polyomial degrees of both sides. The degree of the left hand
side is the maximum degree of $f_{k}(t)$s, says $d$. The right hand side is at
least $\sum_{i=1}^{s}m_{s}$ because the degree of PEFs is additive and each
non-exponential PEF has degree at least 1.

Therefore,

$\sum_{i=1}^{s}m_{s}\leq d.$

There exists a positive integer $r$ such that

$\displaystyle
P(t,e^{a_{1}t},\ldots,e^{a_{n}t},e^{-a_{1}t},\ldots,e^{-a_{n}t})\cdot
e^{\sum_{i=1}^{n}rda_{i}t}=Q(t,e^{a_{1}t},\ldots,e^{a_{n}t})$ $\displaystyle
P_{i}(t,e^{a_{1}t},\ldots,e^{a_{n}t},e^{-a_{1}t},\ldots,e^{-a_{n}t})\cdot
e^{\sum_{i=1}^{n}rm_{i}a_{i}t}=Q_{i}(t,e^{a_{1}t},\ldots,e^{a_{n}t})$

for some multivariate polynomials $Q$ and $Q_{i}$s.

Now we have

$\displaystyle
Q(t,e^{a_{1}t},\ldots,e^{a_{n}t})=\Pi_{i=1}^{s}Q_{i}(t,e^{a_{1}t},\ldots,e^{a_{n}t})\cdot
e^{\sum_{i=1}^{n}ha_{i}t},$

for some integer $h$.

One can use the factoring algorithm for multivariate polynomials by regarding
$h$ and $h_{i}$’s as multivariate polynomial on
$t,e^{a_{1}t},\ldots,e^{a_{n}t}$.

In Section 6, we will prove that assuming Schanuel’s conjecture, $f(t)$ has
only single roots excepting $0$ if $f(t)$ is square free. Thus the algorithm
of factoring multivariate polynomials over $\mathbb{A}$ can be used to getting
$f^{\prime}(t)$ from PEF $f(t)$ such that $f^{\prime}(t)$ inherits all roots
of $f(t)$ and each root is single excepting 0. As we will see latter, this
simplification plays essential role in finding a root isolation of $f(t)$.

##  3 Symbolic Dynamics of Continuous-time Markov Chains

We begin with _continuous-time Markov chains_. A continuous-time Markov chain
is a Markovian (i.e. memoryless) stochastic process that takes values on a
finite state set $S$ ($|S|=d<\infty$) and evolves in continuous-time
$t\in\mathbb{R}^{+}$. More formally:

###### Definition 9

A _stochastic process_ $\\{X(t):t\in\mathbb{R}^{+}\\}$ with finite state set
$S$ is a continuous-time Markov chain if it satisfies the Markov property,
i.e. for any $k\in\mathbb{R}^{+}$:

$p(X_{t+k}=j|X_{t}=i,\\{X_{h}:0\leq h<t\\})=p(X_{t+k}=j|X_{t}=i),$

where $i,j\in S$ and $p(\,\mathord{\cdot}\,|\,\mathord{\cdot}\,)$ is the
conditional probability of events. The number of states $d=|S|$ is the
dimension of the chain.

It turns out that a continuous-time Markov chain is fully characterized by a
_transition rate matrix_ $Q$ [GS07]. $Q$ is $d$-by-$d$ matrix and the 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_{i\not=j}Q_{i,j}$ for all $1\leq j\leq d$. Consequently, the row
summations of $Q$ are all zero. The dynamic of a continuous-time Markov chain
is fully described by a master equation, which is a system of coupled ordinary
differential equations that describe how the probability distribution changes
over time for each of the states of the system. Specifically, the master
equation is:

$dP(t)=P(t)Qdt,$

where $P(t)$ is the $d$-by-$d$ transition probability matrix at time $t$; the
quantity $P_{i,j}(t)=p(X_{t}=j|X_{0}=i)$ denotes the probability from state
$i$ at time $0$ to state $j$ at time $t\in\mathbb{R}^{+}$. The master equation
is solved subject to initial conditions $P(0)=I$, the identity matrix:

$P(t)=e^{Qt}.$

Thus, given an initial distribution $\mu_{0}$, the distribution at time
$t\in\mathbb{R}^{+}$ is:

$\mu_{t}=P(t)\mu_{0}=e^{Qt}\mu_{0}.$

Therefore, we have the brief definition of continuous-time Markov chains:

###### Definition 10

A continuous-time Markov chain is a pair $\mathcal{M}=(S,Q)$, where $S$
($|S|=d$) is a finite state set, $Q$ a $d$-by-$d$ transition rate matrix.

W.l.o.g, we always denote $S=\\{s_{1},s_{2},\ldots,s_{d}\\}$ in this paper.

###### Example 1

Consider continuous-time Markov chain $\mathcal{M}=(S,Q)$, where $|S|=3$,

$Q=\left(\begin{matrix}-0.025&0.02&0.005\\\ 0.3&-0.5&0.2\\\
0.02&0.4&-0.42\end{matrix}\right)$

Given continuous-time Markov chain $\mathcal{M}=(S,Q)$, we denote
$\mathcal{D(S)}$ the set of all distributions over $S$, which is called the
_state space_ of continuous-time Markov chains, while in previous work
(e.g.[ASSB00, CHKM11a, BHHK03]), $S$ is regarded as the state apace of the
chain. The path of $\mathcal{M}$ is a continuous function indexed by an
initial distribution $\mu\in\mathcal{D(S)}$:

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

We remark that defining path $\sigma_{\mu}$ over distributions transitions is
different to the usual way over the transitions of states set $S$, i.e.,
functions $\omega_{s}:\mathbb{R}^{+}\rightarrow S$ with the starting state
$s$. Furthermore, $\omega_{s}$ must have _finite variability_ , i.e., its set
of discontinuities has no accumulation points (in other words, on any finite
interval the value of $\omega_{s}$ can only change a finite number of times).
This restriction is for applying analyzing methods of discrete-time Markov
chains on the continuous-time counterpart as the domain $\omega_{s}$ is
actually $\mathbb{N}^{+}$ rather than $\mathbb{R}^{+}$. However, we do not put
the constrain on the path $\sigma_{\mu}$ such that we track all time instants
not a part domain of continuous-time Markov chains. Thus in any time interval,
the number of $\sigma_{\mu}$ changing may be infinite.

We move to the _symbolic dynamic (path)_ of continuous-time Markov chains. The
_symbolization of distributions_ is a generalization of the discretization of
distributions in [AAGT15]. First, we fix a finite set of intervals
$\mathscr{I}=\\{\mathcal{I}_{k}\subseteq[0,1]\\}_{k\in K}$. With the states
$S=\\{s_{j}\\}_{j=1}^{d}$, 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
j,\mathcal{I}_{k}\rangle:\mu(j)\in\mathcal{I}_{k}\\}.$ (4)

where $\times$ denotes the Cartesian product, and $2^{S\times\mathscr{I}}$ is
the set of all subsets of $S\times\mathscr{I}$.

$\langle j,\mathcal{I}_{k}\rangle\in\mathbb{S}(\mu)$ asserts that the $j$-th
element of $\mu$ is in the interval $\mathcal{I}_{k}$. Specially, in [AAGT15],
$\mathscr{I}$ must be fixed as a partition of $[0,1]$, i.e.,
$\mathcal{I}_{k}\cap\mathcal{I}_{m}=\emptyset$ for all $k\not=m$. Thus for any
$\mu\in\mathcal{D(S)}$, we can label it by finite symbols from
$S\times\mathscr{I}$.

###### Example 2

Considering distributions

$\mu_{0}=\left(\begin{matrix}0.3\\\ 0.3\\\
0.4\end{matrix}\right),\mu_{1}=\left(\begin{matrix}0\\\ 0.7\\\
0.3\end{matrix}\right)$

suppose

$\mathscr{I}=\\{[0,0.2),[0.4,0.4],(0.5,0.7],(0.3,1]\\}.$

Then, $\mathbb{S}(\mu_{0})=\\{\langle 3,[0.4,0.4]\rangle,\langle
3,(0.3,1]\rangle\\}$, $\mathbb{S}(\mu_{1})=\\{\langle 1,[0,0.2)\rangle,\langle
2,(0.5,0.7]\rangle,\langle 2,(0.3,1]\rangle\\}$.

The benefits of the symbolization are that in practice, we do not care the
exact probability of some state but the range of the probability, which can be
represented by intervals. In the next section, we will further explain this
with our temporal logic CLL.

With the symbolization, we have

###### Definition 11

A _symbolized_ continuous-time Markov chain is a tuple
$\mathcal{SM}=(S,Q,\mathscr{I})$, where $(S,Q)$ is a continuous-time Markov
chain and $\mathscr{I}$ is a finite set of intervals in $[0,1]$.

Throughout this paper, we always assume that $\mathcal{SM}$ is rational, i.e.,
all elements of $Q$, and for all $\mathcal{I}\in\mathscr{I}$ is a rational
interval, i.e., the endpoints must be rational numbers. Thus $(a,b)$, $(a,b]$,
$[a,b)$ and $[a,b]$ are all valid rational intervals for all
$a,b\in\mathbb{Q}$. Furthermore, the elements of all the distributions are
also rational.

Next, we extend this symbolization to the path $\sigma_{\mu}$:

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

###### Definition 12

Given a symbolized continuous-time Markov chain $\mathcal{SM}$,
$\mathbb{S}\circ\sigma_{\mu}$ is a _symbolic dynamic (path)_ of $\mathcal{M}$.

In the end of this section, we prove that the path (continuous function)
$\sigma_{\mu}=e^{Qt}\mu$ is a system of PEFs over algebraic number
$\mathbb{A}$.

###### Lemma 1

Given a continuous-time Markov chain $\mathcal{M}=(S,Q)$ with an initial
distribution $\mu$, for any $1\leq i\leq d\ (|S|=d)$ , $e^{Qt}\mu(i)$, the
$i$-th element of $e^{Qt}\mu$, can be expressed as a PEF
$f:\mathbb{R}^{+}\rightarrow[0,1]$ of
$f(t)=\sum_{k=0}^{K}f_{k}(t)e^{\lambda_{k}t}$ over $\mathbb{A}$.

Proof. As the elements of $\mu$ are rational, we only need to prove that any
entry of $e^{Qt}$ can be expressed as a finite sum of
$\sum_{k}f_{k}(t)e^{\eta_{k}t}$ for $\eta_{k}\in\mathbb{A}$ and
$f_{k}(t)\in\mathbb{A}[t]$.

By Proposition 2, we have that there is a $P\in\mathbb{A}^{n\times n}$ such
that $Q=P^{-1}(\oplus_{k}J_{k})P$ such that

$J_{k}=\left[\begin{matrix}\lambda_{k}&1&0&\cdots&0\\\
0&\lambda_{k}&1&\cdots&0\\\ &&&\ddots&\\\
0&0&0&\cdots&\lambda_{k}\par\end{matrix}\right]$

Note that $\lambda_{k}$ is an eigenvalue of $Q$ and $Q\in\mathbb{Q}^{d\times
d}$, so $\lambda_{k}$ is algebraic. Furthermore,
$J_{k}\in\mathbb{A}^{n_{k}\times n_{k}}$, where $n_{k}$ is the dimension of
$J_{k}$.

Therefore, $e^{Qt}=P^{-1}e^{\oplus_{k}J_{k}t}P=P^{-1}(\oplus_{k}e^{J_{k}t})P$.
So we complete the proof by proving that for each $k$, any entry of
$e^{J_{k}t}$ can be expressed as a finite sum of
$\sum_{k}f_{k}(t)e^{\eta_{k}t}$ for $\eta_{k}\in\mathbb{A}$ and
$f_{k}(t)\in\mathbb{A}[t]$. Computing $e^{J_{k}t}$, we obtain that

$e^{J_{k}t}=\left[\begin{matrix}e^{\lambda_{k}t}&te^{\lambda_{k}t}&t^{2}e^{\lambda_{k}t}/{2!}&\cdots&t^{n}_{k}e^{\lambda_{k}t}/{n_{k}!}\\\
0&e^{\lambda_{k}t}&te^{\lambda_{k}t}&\cdots&t^{n_{k}-1}e^{\lambda_{k}t}/{(n_{k}-1)!}\\\
&&&\ddots&\\\ 0&0&0&\cdots&e^{\lambda_{k}t}\par\end{matrix}\right].$

$\hfill\Box$

By the above lemma, analyzing dynamics $\sigma_{\mu}$ of continuous-time
Markov chains is equivalent to studying corresponding PEFs.

##  4 Continuous Linear Logic

In this section, we introduce _continuous linear logic (CLL)_ to specify the
temporal properties of symbolized continuous-time Markov chain
$\mathcal{SM}=(S,Q,\mathscr{I})$. In summary, CLL is a linear-time temporal
logic. Unlike LTL, CLL has the path and state formulas expressing temporal
properties of $\mathcal{SM}$. However, the path formulas in CLL are simpler
because the only applied temporal operator is a timed version of until
operator. Furthermore, the nesting of until temporal operator is allowed,
which does not appear in the previous work [BHHK03]. More importantly, CLL
formulas can express not only absolutely temporal properties (all-time
instants basing on one starting time) but also relative versions. Up to our
best knowledge, this is the first logic with this distinctive feature in the
context of the verification of continuous-time Markov chains.

Remark: The next-step operator is important in the expressiveness of LTL and
CSL with time-domain non-negative positive numbers $\mathbb{N}^{+}$. However,
the time domain of CLL is non-negative real numbers $\mathbb{R}^{+}$, so
“next-step” is not meaningful.

###### Definition 13

CLL _path formulas_ are formed according to the following grammar:

$\varphi:=\mathbf{true}\mid\Phi_{0}U^{\mathcal{T}_{1}}\Phi_{1}U^{\mathcal{T}_{2}}\Phi_{2}\ldots
U^{\mathcal{T}_{n}}\Phi_{n}\mid\neg\varphi\mid\varphi_{1}\land\varphi_{2}$

where $n\in\mathbb{N}^{+}$ is a positive integer, for all $0\leq k\leq n$,
$\Phi_{k}$ is a state formula, and $\mathcal{T}_{k}$’s are arbitrary _rational
time intervals_ (with rational endpoints) in $\mathbb{R}^{+}$, i.e.,
$\mathcal{T}_{k}$ is one of the forms:

$(a,b),[a,b],(a,b],[a,b)\qquad\forall a,b\in\mathbb{Q}^{+}.$

The syntax of CLL _state formulas_ is described by the following grammar:

$\Phi:=\mathbf{true}\mid a\in AP\mid\neg\Phi\mid\Phi_{1}\land\Phi_{2}$

where $AP$ denotes the set of atomic propositions.

For $n=1$, the until operator $\Phi_{0}U^{\mathcal{T}_{1}}\Phi_{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 holds $\Phi_{0}$. This can be extended to arbitrary $n$ by
noting 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})$. One
important point of CLL is that we consider the relative time, i.e.,
$\mathcal{T}_{1}$ and $\mathcal{T}_{2}$ do not have to be disjoint, and the
starting time point $0$ of $\mathcal{T}_{2}$ is based on some time event in
$\mathcal{T}_{1}$. For instance $\Phi_{0}U^{[3,9]}\Phi_{1}U^{(2,7)}\Phi_{2}$
is a valid path formula, which is different to CLL path formula
$\Phi_{0}U^{[3,9]}\Phi_{1}\land\Phi_{1}U^{(2,7)}\Phi_{2}$. This picture will
be more clear by the following semantics of CLL.

Given a symbolized continuous-time Markov chain
$\mathcal{SM}=(S,Q,\mathscr{I})$, the semantics of CLL path formulas is
defined on paths $\\{\sigma_{\mu}\\}_{\mu\in\mathcal{D(S)}}$.

  * •

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

  * •

$\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 $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[0,t)\cap\mathcal{T}_{1}$, ${\mu_{t^{\prime}}}\models\Phi_{0}$,
where $\sigma_{\mu}\models\Phi$ iff $\mu\models\Phi$, $\mu_{t}=e^{Qt}\mu\
\forall t\in\mathbb{R}^{+}$;

  * •

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

  * •

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

As we see, the CLL path formula
$\sigma_{\mu}\models\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$. This
makes time instants relative. This can be further explained by comparing
$\Phi_{0}U^{\mathcal{T}_{1}}\Phi_{1}U^{\mathcal{T}_{2}}\Phi_{2}$ and
$\Phi_{0}U^{\mathcal{T}_{1}}\Phi_{1}\land\Phi_{1}U^{\mathcal{T}_{2}}\Phi_{2}$.

  * •

$\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 picture.

  * •

$\underbrace{\hskip 56.9055pt}_{\Phi_{0}}$$\underbrace{\hskip
28.45274pt}_{\Phi_{1}}$$\overbrace{\hskip
71.13188pt}^{=\inf\mathcal{T}_{2}}$$\downarrow{\Phi_{2}}$$\overbrace{\hskip
71.13188pt}^{=\inf\mathcal{T}_{1}}$$\uparrow$ time 0$\uparrow t_{1}$
$\uparrow(t_{1}+t_{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}^{+}$.

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

  * •

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

  * •

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

  * •

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

  * •

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

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 formulas
$\varphi$ follows the same way.

Temporal operators like $\Diamond$ (“eventually”), its timed variant
$\Diamond^{\mathcal{T}}$ is derived as follows:

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

For $\Box$ (“always”), its timed variant $\Box^{\mathcal{T}}$, we have:

$\Box^{\mathcal{T}}\Phi=\neg\Diamond^{\mathcal{T}}\neg\Phi.$

In this paper, we aim to solve the decidability of model checking continuous-
time Markov chains against CLL formulas.

######  Problem 2 (CLL Model-checking Problem)

Given a symbolized continuous-time Markov chain
$\mathcal{SM}=(S,Q,\mathscr{I})$ with an initial distribution $\mu$ and a CLL
path formula $\varphi$ on $AP=S\times\mathscr{I}$, the goal is to decide
whether $\sigma_{\mu}\models\varphi$.

Before proceeding to solve this model-checking problem, we shall first
consider what can be specified in our logic CLL.

Given a continuous-time Markov chain $(S,Q)$ with initial distribution $\mu$,
the liveness property $\Diamond^{[0,1000]}\langle k,[1,1]\rangle$ expresses
state $s_{k}\in S$ is eventually reached with probability one before time
instants $1000$. The safety property $\Box^{[100,1000]}\langle k,[0,0]\rangle$
expresses that state $s_{k}\in S$ is always not reached (with probability
zero) in time interval $[100,1000]$. Furthermore, setting the intervals non-
trivial (not $[0,0]$ or $[1,1]$), liveness and safety can be asserted with
probabilities, such as $\Diamond^{[0,1000]}\langle k,[0.5,1]\rangle$ and
$\Box^{[100,1000]}\langle k,[0,0.5]\rangle$. Further,

$\langle k,[0.7,1]\rangle U^{[2,3]}\langle k,[0.7,1]\rangle\ldots
U^{[2,3]}\langle k,[0.7,1]\rangle,$

where the number of $U^{[2,3]}$ is 100, asserts that the probability of
$s_{k}$ 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.2],(0.2,0.8),[0.8,1]\\}$, we can declare the first interval as “low”
and the last interval as “high”. In this case $\Box^{[10,1000)}(\langle
i,[0,0.2]\rangle\rightarrow\langle j,[0.8,1]\rangle)$ will say that whenever
the probability of $s_{i}$ is low, the probability of $s_{j}$ will be high in
time interval $[10,1000)$.

##  5 CLL Model Checking

In this section, we establish that there is an algorithm to model checking
continuous-time Markov chains against CLL formulas, i.e., the model-checking
problem in Problem 2 is decidable. This result mainly depends on the following
theorem about the root isolation of PEFs. Thus the correctness of our model
checking algorithm is based on Schanuel’s conjecture.

###### Theorem 3

Based on Schanuel’s conjecture, given a PEF $f(t)$ and a bounded time interval
$\mathcal{T}$ , there is an algorithm (Algorithm 2) to find a real root
isolation $\textrm{Iso}(f)_{\mathcal{T}}$ of $f(t)$. Furthermore, the number
of real roots is finite, i.e., $|\textrm{Iso}(f)|<\infty$.

For the readability, the proof of the above theorem will be postponed in the
next section.

###### Theorem 4

Based on Schanuel’s conjecture, the CLL model checking problem in Problem 2 is
decidable.

$\it Proof.$ The nontrivial step is to model check formulas of the forms

$\Phi_{0}U^{\mathcal{T}_{1}}\Phi_{1}U^{\mathcal{T}_{2}}\Phi_{2}\cdots
U^{\mathcal{T}_{n}}\Phi_{n},$

where $\\{\mathcal{T}_{j}\\}_{j=1}^{n}$ is a set of bounded rational intervals
in $\mathbb{R}^{+}$, and for $0\leq k\leq n+1$, $\Phi_{k}$ is a state formula
by the following grammar:

$\Phi:=\mathbf{true}\mid a\in AP\mid\neg\Phi\mid\Phi_{1}\land\Phi_{2}.$

Thus $\Phi_{k}$ is actually the same to the formula of propositional logics.
So $\Phi$ admits _conjunctive normal form (CNF)_ , i.e.,

$\Phi_{k}=\land_{j\in J_{k}}\lor_{l\in L_{k}}lit_{j,l},$

where $lit_{j,l}$ is a _literal_ of $a\in AP$ or $\neg a$, and $J_{k}$ and
$L_{k}$ are finite sets. Furthermore, we observe that $\neg a$ can be
represented by the disjunction of (at most) two extra atomic propositions. For
example, if $a=\langle k,[0.1,0.9]\rangle$, then $\neg a=a_{1}\lor a_{2}$,
where $a_{1}=\langle k,[0,0.1)\rangle$ and $a_{2}=\langle k,(0.9,1]\rangle$.
Therefore, the left problem is to model check

$\sigma_{\mu}\models\Phi_{0}U^{\mathcal{T}_{1}}\Phi_{1}U^{\mathcal{T}_{2}}\Phi_{2}\cdots
U^{\mathcal{T}_{n}}\Phi_{n},$ (6)

where $\Phi_{k}=\land_{j\in J_{k}}\lor_{l\in L_{k}}a_{j,l}$ and $a_{j,l}\in
AP$ for all $j,l$.

In the following, we always assume that each $a\in AP$ contains closed
interval, i.e., $a=\langle k,[a,b]\rangle$ for $a,b\in\mathbb{Q}$, and
$\forall 1\leq j\leq n$, $\mathcal{T}_{j}$ is left closed, i.e.
$\mathcal{T}_{j}=[t_{j},t_{j}^{\prime})$ for
$t_{j},t_{j}^{\prime}\in\mathbb{Q}^{+}$. Other situations can also be handled
in the similar way. First of all, we claim that the relative time relationship
can be rewritten as absolute versions.

###### Lemma 2

$\sigma_{\mu}\models\Phi_{0}U^{\mathcal{T}_{1}}\Phi_{1}U^{\mathcal{T}_{2}}\Phi_{2}\cdots
U^{\mathcal{T}_{n}}\Phi_{n}$ if and only if there exists time intervals
$\\{\mathcal{I}_{k}\subseteq\mathbb{R}^{+}\\}_{k=0}^{n}$ with
$\mathcal{I}_{0}=[0,0]$ such that

  * •

_The satisfaction of intervals_ : for all $1\leq k\leq n$,
${\mu_{t}}\models\Phi_{k-1}$ for all $t\in\mathcal{I}_{k}$, and
${\mu_{t^{*}}}\models\Phi_{n}$, where $t^{*}=\sup\mathcal{I}_{n}$ and
$\mu_{t}=e^{Qt}\mu\ \forall t\in\mathbb{R}^{+}$;

  * •

_The order of intervals_ : for all $1\leq k\leq n$,
$\mathcal{I}_{k}\subseteq\sup\mathcal{I}_{k-1}+\mathcal{T}_{k}$ and
$\inf\mathcal{I}_{k}=\sup\mathcal{I}_{k-1}+\inf\mathcal{T}_{k}$.

Proof. We first prove the sufficient direction. Let
$\varphi_{1}=\Phi_{1}U^{\mathcal{T}_{2}}\Phi_{2}\cdots
U^{\mathcal{T}_{n}}\Phi_{n}$. Then the above formula is
$\Phi_{0}U^{\mathcal{T}_{1}}\varphi_{1}$. By the semantic of CLL, we have that
there is a time $t_{1}\in\mathcal{T}_{1}$ such that
$\sigma_{\mu_{t_{1}}}\models\varphi_{1}$, and for any
$t_{1}^{\prime}\in[0,t)\cap\mathcal{T}_{1}$,
${\mu_{t_{1}^{\prime}}}\models\Phi_{0}$. Then let
$\varphi_{2}=\Phi_{2}U^{\mathcal{T}_{3}}\Phi_{3}\cdots
U^{\mathcal{T}_{n}}\Phi_{n}$ and we get
$\varphi_{1}=\Phi_{1}U^{\mathcal{T}_{2}}\varphi_{2}$. In the similar way, we
have that there is a time $t_{2}\in\mathcal{T}_{2}$ such that
$\sigma_{\mu_{t_{1}+t_{2}}}\models\varphi_{2}$, and for any
$t_{2}^{\prime}\in[0,t_{2})\cap\mathcal{T}_{2}$,
${\mu_{t_{1}+t_{2}^{\prime}}}\models\Phi_{1}$. Iteratively, we get a set of
time instants $\\{t_{k}\\}_{k=0}^{n}$ with $t_{0}=0$. Let
$\mathcal{I}_{k}=\sum_{j=0}^{k-1}t_{j}+[0,t_{k})\cap\mathcal{T}_{k}$ for all
$1\leq k\leq n$. Then it is easy to check that
$\\{\mathcal{I}_{k}\in\mathbb{R}^{+}\\}_{k=0}$ with $\mathcal{I}_{0}=[0,0]$
are the desired intervals satisfying the above two conditions.

Considering the necessary direction, by the above proof, we only need to
identify $\\{t_{k}\\}_{k=1}^{n}$ throughout intervals
$\\{\mathcal{I}_{k}\\}_{k=0}^{n}$. Let
$t_{k}=\sup\mathcal{I}_{k}-\sup\mathcal{I}_{k-1}$ for all $1\leq k\leq n$.
$\Box$

Thus from the above lemma, for model checking the formula in Eq.(6), we only
need to check the existence of time intervals
$\\{\mathcal{I}_{k}\\}_{k=0}^{n}$. The following procedure can construct such
set of intervals if it exists:

  * •

(1) Let $\mathscr{I}_{0}=\\{\mathcal{I}_{0}=[0,0]\\}$ ;

  * •

(2) For each $1\leq k\leq n$, compute the set $\mathscr{I}_{k}$ in
$[0,\sum_{j=1}^{k}\sup\mathcal{T}_{j}]$ of all maximum intervals such that
$\mu_{t}\models\Phi_{k-1}$ for all $t\in\mathcal{I}$ of
$\mathcal{I}\in\mathscr{I}$, where $\mu_{t}=e^{Qt}\mu$, and an interval
$\mathcal{I}$ satisfying some property is maximum if there is no sub-interval
$\mathcal{I}^{\prime}\subseteq\mathcal{I}$ satisfying the same property;
Noting that $\mathscr{I}_{k}$ can be the empty set, i.e.,
$\mathscr{I}_{k}=\emptyset$;

  * •

(3) Let $k$ from $1$ to $n+1$. Updating $\mathscr{I}_{k}$ by

$\\{\mathcal{I}\cap(\sup\mathcal{I}^{\prime}+\mathcal{T}_{k}):\inf\mathcal{I}\leq\sup\mathcal{I}^{\prime}+\inf\mathcal{T}_{k},\mathcal{I}\in\mathscr{I}_{k}\text{
and }\mathcal{I}^{\prime}\in\mathscr{I}_{k-1}\\}.$

Deleting the element of $\emptyset$ in $\mathscr{I}_{k}$ if there exists one
in $\mathscr{I}_{k}$ . If $\mathscr{I}_{k}=\emptyset$, then the formula is not
satisfied;

  * •

(4) For each $\mathcal{I}\in\mathscr{I}_{n}$ Updating $\mathscr{I}_{n}$ by

$\\{\mathcal{I}:\mu_{\sup\mathcal{I}}\models\Phi_{n},\mathcal{I}\in\mathscr{I}_{k}\\},$

where $\mu_{\sup\mathcal{I}}=e^{Q\sup\mathcal{I}}\mu.$ If
$\mathscr{I}_{n}=\emptyset$, then the formula is not satisfied.

Thus after the above procedure, we have non-empty sets
$\\{\mathscr{I}_{k}\\}_{k=0}^{n}$ with the following properties.

  * •

for each $1\leq k\leq n$, $\mu_{t}\models\Phi_{k-1}$ for all
$t\in\mathcal{I}_{k}$ and $\mathcal{I}_{k}\in\mathscr{I}_{k}$, and
$\mu_{t^{*}}\models\Phi_{n}$, where $t^{*}=\sup\mathcal{I}_{n}$;

  * •

for each $1\leq k\leq n$, $\mathcal{I}\in\mathscr{I}_{k}$, there exists at
least one $\mathcal{I}^{\prime}\in\mathscr{I}_{k-1}$ such that
$\mathcal{I}\subseteq\sup\mathcal{I}^{\prime}+\mathcal{T}_{k}$ and
$\inf\mathcal{I}=\sup\mathcal{I}^{\prime}+\inf\mathcal{T}_{k}$.

Therefore, we can get a set of intervals $\\{\mathcal{I}_{k}\\}_{k=0}^{n}$
satisfying the two conditions in Lemma 2 if it exists. On the other hand, it
is easy to check that all such $\\{\mathcal{I}_{k}\\}_{k=0}^{n}$ must be in
$\\{\mathscr{I}_{k}\\}_{k=0}^{n}$, i.e., for each $k$,
$\mathcal{I}_{k}\subseteq\mathcal{I}$ for some
$\mathcal{I}\in\mathscr{I}_{k}$. This ensures the correctness of the above
procedure.

Finally, we are going to give the specific steps to implement the above
procedure by transcendental number theory and real root isolation of PEFs.

###### Lemma 3

Based on Schanuel’s conjecture, given a bounded rational time interval
$\mathcal{T}$, the set $\mathscr{I}$ of all maximum intervals satisfying
$\mu_{t}\models\Phi$ can be computed, where $\Phi=\land_{j\in J}\lor_{l\in
L_{j}}a_{j,l}$ and $a_{j,l}\in AP$ for all $j,l$. Furthermore,

  * •

The number of all intervals in $\mathscr{I}$ is finite;

  * •

The left and right endpoints of each interval in $\mathscr{I}$ are roots of
PEFs.

Proof. From $\mu_{t}\models\land_{j\in J}\lor_{l\in L_{j}}a_{j,l}$, by the
semantic of CLL, we have that for all $j\in J$, $\mu_{t}\models a_{j,l}$ for
some $l\in L_{j}$. As $J$ and all $L_{j}$ are finite sets, we can one-by-one
check whether or not $\mu_{t}\models a_{j,l}$. Let $\mathscr{I}_{j,l}$ be the
set of all the maximum intervals such that for each
$\mathcal{I}\in\mathscr{I}_{j,l}$, $\mu_{t}\models a_{j,l}$ for all
$t\in\mathcal{I}$. Then $\mathscr{I}=\cap_{j\in J}\mathscr{I}_{L_{j}}$, where

$\mathscr{I}_{L_{j}}=\\{\mathcal{I}_{1}\cup\mathcal{I}_{2}:\mathcal{I}_{1}\in\mathscr{I}_{l_{1}}\textrm{
and }\mathcal{I}_{2}\in\mathscr{I}_{l_{2}}\textrm{ for all distinct
}l_{1},l_{2}\in L_{j}\\}\textrm{ for all }j\in J,$

and

$\mathscr{I}_{L_{i}}\cap\mathscr{I}_{L_{j}}=\\{\mathcal{I}_{1}\cap\mathcal{I}_{2}:\mathcal{I}_{1}\in\mathscr{I}_{L_{i}}\textrm{
and }\mathcal{I}_{2}\in\mathscr{I}_{L_{j}}\\}.$

Next, we first show how to compute $\mathscr{I}_{j,l}$ and then deal with
$\mathcal{I}_{1}\cap\mathcal{I}_{2}$ and $\mathcal{I}_{1}\cup\mathcal{I}_{2}$.

###### Lemma 4

Given a bounded time interval $\mathcal{T}$, a symbolized continuous-time
Markov chain $(S,Q,\mathscr{I})$ with initial distribution $\mu$ and $\langle
k,[a,b]\rangle\in AP$, Let $\mathcal{I}\subseteq\mathcal{T}$ be an maximum
interval in $\mathcal{T}$ such that $\mu_{t}\models\langle k,[a,b]\rangle$ for
all $t\in\mathcal{I}$, where $\mu_{t}=e^{Qt}\mu$ for all $t\in\mathbb{R}^{+}$.
Then the left and right endpoints of $\mathcal{I}$ must be
$\inf\mathcal{T},\sup\mathcal{T}$ or a root of $f(t)=a$ or $f(t)=b$, where
$f(t)=e^{Qt}\mu(k)$.

Proof. Let $\mathscr{I}$ be the set of intervals in $\mathcal{T}$ such that
$\mu_{t}\models\langle k,[a,b]\rangle$ for all $t\in\mathcal{I}$, where
$\mu_{t}=e^{Qt}\mu$ for all $t\in\mathbb{R}^{+}$. W.l.o.g., we assume that
$\mathcal{I}$ is the first one, i.e.
$\inf\mathcal{I}<\inf\mathcal{I}^{\prime}$ for any
$\mathcal{I}^{\prime}\in\mathscr{I}$ and
$\mathcal{I}^{\prime}\not=\mathcal{I}$. By the semantics of CLL,
$\mu_{t}\models a$ means $f(t)=e^{Qt}\mu(k)\in\mathcal{I}$.

We first consider the left endpoint of $\mathcal{I}$, denoted by
$t^{*}=\inf\mathcal{I}$, and the right endpoint follows the same way.

Let $t_{1}=\inf\mathcal{T}$. We analyze the roots of two PEFs $f(t)-a$ and
$f(t)-b$ case by case.

  * •

If $\textrm{Iso}(f(t)-a)=\textrm{Iso}(f(t)-b)=\emptyset$, then by the
continuity of $f(t)$, we have that

$\begin{cases}t^{*}\textrm{ does not exist
}(\mathcal{I}=\emptyset)&f(t_{1})<a\textrm{ or }f(t_{1})>b;\\\
t^{*}=t_{1}&\textrm{others}\end{cases}$

.

  * •

If $\textrm{Iso}(f(t)-a)\not=\emptyset$ and $\textrm{Iso}(f(t)-b)=\emptyset$,
then, by the continuity of $f(t)$ again,

$t^{*}=\begin{cases}t_{1}&f(t_{1})\geq a;\\\
\min_{f(t)=a}t\in\mathcal{T}&\textrm{others}\end{cases}$

.

  * •

If $\textrm{Iso}(f(t)-a)=\emptyset$ and $\textrm{Iso}(f(t)-b)\not=\emptyset$,
then, by the continuity of $f(t)$ again,

$t^{*}=\begin{cases}t_{1}&f(t_{1})\leq b;\\\
\min_{f(t)=b}t\in\mathcal{T}&\textrm{others}\end{cases}$

.

  * •

If $\textrm{Iso}(f(t)-a)\not=\emptyset$ and
$\textrm{Iso}(f(t)-b)\not=\emptyset$, then, by the continuity of $f(t)$ again,

$t^{*}=\begin{cases}\min_{f(t)=a}t\in\mathcal{T}&f(t_{1})<a;\\\
\min_{f(t)=b}t\in\mathcal{T}&f(t_{1})>b;\\\ t_{1}&\textrm{others}.\end{cases}$

where $\min_{f(t)=a}t\in\mathcal{T}$ is the minimum $t\in\mathcal{T}$ with $t$
being a root of $f(t)-a$. Theorem 3 ensures the existence checking of PEFs.

$\Box$

By the above lemma, the left and right endpoints of
$\mathcal{I}\in\mathscr{I}$ must be a root of a PEF $f(t)$ by noting that
$\inf\mathcal{T}$ is a rational number, and can be a root of PEF
$f(t)=t-\inf\mathcal{T}$. By Theorem 3, the number of roots of $f(t)$ in
$\mathcal{T}$ is finite. Therefore, the number of all intervals in
$\mathscr{I}$ is finite.

The left problem is to handle $\mathcal{I}_{1}\cap\mathcal{I}_{2}$ and
$\mathcal{I}_{1}\cup\mathcal{I}_{2}$, where the left and right endpoints of
$\mathcal{I}_{1}$ and $\mathcal{I}_{2}$ are the roots of PEFs. It is
equivalent to compare the values of two real roots of two (different) PEFs.

###### Lemma 5

Let $f_{1}(t)$ and $f_{2}(t)$ two PEFs in $\mathcal{T}_{1}$ and
$\mathcal{T}_{2}$, respectively. For any roots $t_{1}\in\mathcal{T}_{1}$ and
$t_{2}\in\mathcal{T}_{2}$ of $f_{1}(t)$ and $f_{2}(t)$, respectively, based on
Schanuel’s conjecture, there is an efficient way to check whether or not
$t_{1}-t_{2}<g$ for any given rational number $g\in\mathbb{Q}$.

Proof. First, by Theorem!3, isolating the real roots of $f_{1}(t)$ and
$f_{2}(t)$, we have $t_{1}\in(a_{1},b_{1})$ and $t_{2}\in(a_{2},b_{2})$ for
$a_{1},a_{2},b_{1},b_{2}\in\mathbb{Q}$. Then we first check if
$t_{1}-t_{2}=g$. Note that $t_{1}-t_{2}=g$ if and only if
$f_{1}^{2}(t)+f_{2}^{2}(t+g)=0$ has a root in
$(a_{1},b_{1})\cup(a_{2},b_{2})$. $f_{1}^{2}(t)+f_{2}^{2}(t+g)$ is still a
PEF, then we can check whether or not there is a root of it in
$(a_{1},b_{1})\cup(a_{2},b_{2})$ by Algorithm 1.

If $t_{1}-t_{2}\not=g$, we answer whether or not $t_{1}-(t_{2}-g)<0$ by
narrowing $(a_{1},b_{1})$ and $(a_{2},b_{2})$ and maintaining the roots of
$f_{1}(t)$ and $f_{2}(t)$ in the intervals. As we can arbitrarily narrowing
the intervals and there is a gap between $t_{1}$ and $t_{2}-g$, we can compare
them by comparing $a_{1}$ and $b_{2}$ ($a_{2}$ and $b_{1}$).

$\Box$

$\Box$

By the above lemma, back to the procedure Item (3), we can compute
$\mathcal{I}\cap(\sup\mathcal{I}^{\prime}+\mathcal{T}_{k})$ and check whether
or not $\inf\mathcal{I}\leq\sup\mathcal{I}^{\prime}+\inf\mathcal{T}_{k}$. The
reason is that $\mathcal{T}_{k}$ is a rational interval.

Finally, for Item (4) in the procedure, $\mu_{\sup\mathcal{I}}\models\Phi_{n}$
can be checked by Lemma 3.

$\Box$

##  6  Real Root Isolation of PEFs

In this section, we give an algorithm to find a real root isolation of PEFs
and finish the proof of Theorem 3.

From Rolle’s theorem, we know there must exist at last one real root of
$f^{\prime}(t)$ between every two distinct real roots of $f(t)$, if $f(t)$ is
continuous differentiable. In order to isolating the real roots of $f(t)$, we
can try to get an real root isolation of $f^{\prime}(t)$ first. Likewise, in
order to obtain the real roots of $f^{\prime}(t)$, we can try to get the real
roots of $f^{\prime\prime}(t)$ first. We can repeat the above procedure until
the real solutions of the $i$-th derivative of $f(t)$ for some $i$ can be
achieved. Then, we lift the real solutions of the respective derivative in the
inverse order until $f(t)$ itself. Following the basic idea, we have

###### Lemma 6

Let $f(t)$ be a PEF, $f^{\prime}(t)$ the derivative of $f(t)$ w.r.t. $t$, and
$\textrm{Iso}(f^{\prime})_{\mathcal{T}}=\\{\mathcal{T}_{j}=(a_{j},b_{j})\\}_{j=1}^{J}$,
in which $\mathcal{T}=[a,b]$ and
$a=b_{0}<a_{1}<b_{1}<\ldots<a_{J}<b_{J}<a_{J+1}=b$. Furthermore, $f(t)$ has no
real roots in any closed interval $[a_{j},b_{j}]$, $1\leq j\leq J$. Then,
$\textrm{Iso}(f)_{\mathcal{T}}=\\{(b_{j},a_{j+1})|f(b_{j})f(a_{j+1})<0,0\leq
j\leq J\\}$.

Proof: Since $f(t)$ has no real roots in any closed interval $[a_{j},b_{j}]$,
$1\leq j\leq J$, all real roots of $f(t)$ are in
$\cup_{j=0}^{J}(b_{j},a_{j+1})$ and $f(b_{j})f(a_{j+1})\not=0$. Moreover,
$f(t)$ has at most one real root in each $(b_{j},a_{j+1})$, otherwise, there
must be at least one real root of $f^{\prime}(t)=0$ on it by Rolle’s theorem,
which is a contradiction with
$\textrm{Iso}(f^{\prime})_{\mathcal{T}}=\\{\mathcal{T}_{j}=(a_{j},b_{j}\\}_{j=1}^{J}$.
So, if $f(b_{j})f(a_{j+1})<0$, then there exists only one real root of $f(t)$
in $(b_{j},a_{j+1})$, otherwise no real root of $f(t)$ in $(b_{j},a_{j+1})$.
$\hfill\Box$

From the above lemma, if $f(t)$ has only single roots, then such
$\textrm{Iso}(f^{\prime})=\\{\mathcal{T}_{j}=(a_{j},b_{j})\\}_{j=1}^{J}$
always exists because there is always a gap between the roots of $f(t)$ and
$f^{\prime}(t)$. Thus $\textrm{Iso}(f^{\prime})$ can be used to reason about
$\textrm{Iso}(f)$. Otherwise, $f(t)$ has one multiple root, then the root will
be hidden by the root of $f^{\prime}(t)$, leading that such
$\textrm{Iso}(f^{\prime})=\\{\mathcal{T}_{j}=(a_{j},b_{j})\\}_{j=1}^{J}$ does
not exists. Therefore, we need ensure that the roots of $f(t)$ are all single.
This can be done by factoring $f(t)$ and replace $f(t)$ by its square free
part $\hat{f}(t)$. Then the following result guarantees that $\hat{f}(t)$ is
single.

###### Lemma 7

Let $f(t)=\sum_{k=0}^{K}f_{k}(t)e^{\lambda_{k}t}$ be a square free PEF. Based
on Schanuel’s conjecture, $f(t)$ has no multiple real root except $0$.

Proof. The proof is similar to [GCL+17, Corollary 4] (PEFs over real numbers).
For the completeness, we present the proof as follows.

Let $\\{a_{j}\\}_{j=1}^{n}$ be an integral basis of
$\textrm{Power}(f)=\\{\lambda_{k}\\}_{k=0}^{K}$. Since $f(t)$ is square free,
we may write

$f(t,e^{a_{1}t},\ldots,e^{a_{n}t})=f_{1}(t,e^{a_{1}t},\ldots,e^{a_{n}t})\cdots
f_{n}(t,e^{a_{1}t},\ldots,e^{a_{n}t})$

where for any $1\leq i,j\leq n$, $i\not=j$,
$f_{i}(t,e^{a_{1}t},\ldots,e^{a_{n}t})$ is irreducible and
$f_{i}(t,e^{a_{1}t},\ldots,e^{a_{n}t})$ and
$f_{j}(t,e^{a_{1}t},\ldots,e^{a_{n}t})$ are coprime, i.e., they are not a
factor of each other.

We first prove, by contradiction, that $f_{i}(t,e^{a_{1}t},\ldots,e^{a_{n}t})$
and $f_{j}(t,e^{a_{1}t},\ldots,e^{a_{n}t})$ have no nonzero common real root
w.r.t. $t$. Suppose $t_{0}\not=0$ is a common real root of
$f_{i}(t,e^{a_{1}t},\ldots,e^{a_{n}t})$ and
$f_{j}(t,e^{a_{1}t},\ldots,e^{a_{n}t})$. By Corollary 1, we have that the
transcendence degree of
$\mathbb{Q}(t_{0},e^{a_{1}t_{0}},\ldots,e^{a_{n}t_{0}})$ is at least $n$.
Then, there must exist $n$ elements in
$\\{t_{0},e^{a_{1}t_{0}},\ldots,e^{a_{n}t_{0}}\\}$ that are algebraically
independent. Without loss of generality, let
$\\{t_{0},e^{a_{1}t_{0}},\ldots,e^{a_{n-1}t_{0}}\\}$ be the $n$ elements that
are algebraically independent. Besides, let
$g(t,e^{a_{1}t},\ldots,e^{a_{n-1}t})$ be the resultant of
$f_{i}(t,e^{a_{1}t},\ldots,e^{a_{n}t})$ and
$f_{j}(t,e^{a_{1}t},\ldots,e^{a_{n}t})$ w.r.t. $e^{a_{n}t}$, then
$(t_{0},e^{a_{1}t_{0}},\ldots,e^{a_{n-1}t_{0}})$ is a real root of
$g(t,y_{1},\ldots,y_{n-1})$. Further since
$f_{i}(t,e^{a_{1}t},\ldots,e^{a_{n}t})$ and
$f_{j}(t,e^{a_{1}t},\ldots,e^{a_{n}t})$ are coprime,
$g(t,y_{1},\ldots,y_{n-1})$ is nontrivial polynomial, indicating that
$(t_{0},e^{a_{1}t_{0}},\ldots,e^{a_{n}t_{0}})$ is a real root of some
nontrivial polynomial. This contradicts that
$\\{t_{0},e^{a_{1}t_{0}},\ldots,e^{a_{n}t_{0}}\\}$ are algebraically
independent.

Next, we prove that $f_{i}(t,e^{a_{1}t},\ldots,e^{a_{n}t})$ has no multiple
real root. Suppose

$f_{i}(t,e^{a_{1}t},\ldots,e^{a_{n}t})=h_{0}(t)+\sum_{k=1}^{s}h_{k}(t)(e^{a_{1}t})^{b_{k1}}\cdots(e^{a_{n}t})^{b_{kn}}$

where $h_{0}(t),\ldots,h_{n}(t)$ are nontrivial polynomials and
$b_{jk}\in\mathbb{N}$ for $1\leq j\leq s$ and $1\leq k\leq n$. Then we have

$f_{i}^{{}^{\prime}}(t,e^{a_{1}t},\ldots,e^{a_{n}t})=h_{0}^{\prime}(t)+\sum_{k=1}^{s}[h_{k}^{{}^{\prime}}(t)+h_{k}^{{}^{\prime}}(t)(a_{1}b_{k1}+\cdots+a_{n}b_{kn})](e^{a_{1}t})^{b_{k1}}\cdots(e^{a_{n}t})^{b_{kn}}$

Moreover

$f_{i}(t,y_{1},\ldots,y_{n})=h_{0}(t)+\sum_{k=1}^{s}h_{k}(t)(y_{1})^{b_{k1}}\cdots(y_{n})^{b_{kn}}$
$f_{i}^{{}^{\prime}}(t,y_{1},\ldots,y_{n})=h_{0}^{\prime}(t)+\sum_{k=1}^{s}[h_{k}^{{}^{\prime}}(t)+h_{k}^{{}^{\prime}}(t)(a_{1}b_{k1}+\cdots+a_{n}b_{kn})](y_{1})^{b_{k1}}\cdots(y_{n})^{b_{kn}}$

Consider the degree and $h_{0}(t)$ to be nontrivial, it is evident to see that
$f_{i}(t,y_{1},\ldots,y_{n})$ is not a factor of
$f_{i}^{{}^{\prime}}(t,y_{1},\ldots,y_{n})$. Then,
$f_{i}(t,y_{1},\ldots,y_{n})$ and $f_{i}^{{}^{\prime}}(t,y_{1},\ldots,y_{n})$
are coprime, since $f_{i}(t,y_{1},\ldots,y_{n})$ is irreducible. For the same
reason as above $f_{i}(t,e^{a_{1}t},\ldots,e^{a_{n}t})$ and
$f_{i}^{{}^{\prime}}(t,e^{a_{1}t},\ldots,e^{a_{n}t})$ have no common real
roots. Therefore, $f_{i}(t,e^{a_{1}t},\ldots,e^{a_{n}t})$ has no multiple real
root. $\Box$

Algorithm 2 IsolatePEF($f$)

0: A PEF $f(t)$ with bounded time interval $(B,C)$

0: $\textrm{Iso}(f)$ a real root isolation of $f(t)$ in $\mathbb{R}^{+}$

1: $r=0$

2: while $|\textrm{Power}(f)|!=1$ do

3: $f(t)=\hat{f}(t),$ the square part of $f(t)$

4: $S_{r}(t)=f(t)$

5: $r=r+1$

6: while $0\in\textrm{Power}(f)$ do

7: $f(t)=f^{\prime}(t)$

8: $f(t)=\hat{f}(t),$ the square part of $f(t)$

9: $S_{r}(t)=f(t)$

10: $r=r+1$

11: end while

12: $\lambda\leftarrow$ the first element of $\textrm{Power}(f)$

13: $f(t)=f(t)e^{-\lambda t}$

14: end while

15: $S_{r+1}(t)=f(t)$

16: $\textrm{Iso}(S_{r+1})\leftarrow$ a real root isolation of polynomial
$S_{r}(t)$ on $(B,C)$;

17: if $\textrm{Iso}(S_{r+1})=\emptyset$ then

18: $\textrm{Iso}(S_{r+1})=\\{(B,C)\\}$

19: end if

20: for each $k=r;k\geq 0;k--$ do

21: for each $(u,l)\in\textrm{Iso}(S_{k+1})$ do

22: while $S_{k}(u)=0$ or $S_{k}(l)=0$ or
$Exist(S_{k},[u,l],0.5)=\textbf{true}{}$ do

23: if $S_{k+1}(u)S_{k+1}(\frac{l+u}{2})<0$ then

24: $l=\frac{l+u}{2}$

25: else if $S_{k+1}(\frac{l+u}{2})=0$ then

26: $l=u=\frac{l+u}{2}$

27: else

28: $u=\frac{l+u}{2}$

29: end if

30: end while

31: $\textrm{Iso}(S_{k})=\emptyset$.

32: Let $\textrm{Iso}(S_{r})=\\{(a_{k},b_{k})\\}_{k=1}^{m}$ with
$a_{1}<b_{1}<a_{2}<b_{2}<\cdots<a_{m}<b_{m}$

33: Let $b_{0}=B$ and $a_{m+1}=C$

34: for each $j=0;j<m+1;j++$ do

35: if $S_{k}(b_{j})S_{k}(a_{j+1})<0$ then

36:
$\textrm{Iso}(S_{k})\leftarrow\textrm{Iso}(S_{k})\cup\\{(b_{j},a_{j+1})\\}$

37: end if

38: end for

39: end for

40: end for

41: return $\textrm{Iso}(S_{0})$

Now we can present our algorithm to find a real root isolation of a given PEF
$f(t)$ in interval $(B,C)$. This procedure is implemented in Algorithm 2,
whose main steps can be understood as follows:

  * •

Step 1: From line 1 to 15, construct a sequence PEFs
$S_{0}(t),S_{1}(t),S_{2}(t),...,S_{r+1}(t)$, where $S_{0}(t)$ is the square
free part of $f(t)$, for $1\leq k\leq r$, $S_{k}(t)$ is square free which has
the same real roots as the derivative of $S_{k-1}$ and
$S_{r+1}(t)\in\mathbb{A}[t]$, a polynomial in t.

  * •

Step 2: In line 16 to 19, finding a all real roots of $S_{r}(t)$ on $(B,C)$.
If $\textrm{Iso}{S_{r}(t)}=\emptyset$, then let
$\textrm{Iso}{S_{r}(t)}=(B,C)$. Note that the problem of isolating real roots
of a univariate polynomial is well studied [CA76, Joh98].

  * •

Step 3: In the rest part, for $k=r$ down to $0$, for each
$(u,l)\in\textrm{Iso}(S_{k})$, adjusting $u$ and $v$ such that $(u,l)$ is
still in one of sets of real root isolations of $S_{k+1}$ and $S_{k}$ has no
any root in $[u,l]$ by calling $Exist()$ to satisfy the requirements of Lemma
6. Then by Lemma 6, finding a real root isolation of $S_{k}$.

From the above procedure, as we can always get a polynomial $S_{t}(t)$ and the
number of roots of $S_{t}(t)$ in $(B,C)$ is finite, we can claim that the
number of roots of $f(t)$ in $(B,C)$ is finite. If not, we can use
$\textrm{Iso}(S_{t}(t))$ to reason $\textrm{Iso}(f)$, contradicting the fact
in Lemma 6.

######  Theorem 5 (Correctness of IsolatePEF))

Based on Schanuel’s conjecture, Algorithm 2 IsolatePEF always terminates and
returns a real root isolation for a given PEF $f(t)$.

Proof. Termination is immediately obtained from the correctness of Algorithm
1. The correctness of procedures are obtained by Lemmas 6 and 7. $\Box$

##  7 Conclusion

In this paper, we have initiated here the study of the symbolic dynamics of
finite-state continuous-time Markov chains obtained by symbolizing the
probability value space $[0,1]$ into a finite set of intervals in every
dimension of the distributions. Then a new continuous-time logic, named
continuous linear logic, was proposed to specify the properties of the
symbolic dynamics of continuous-time Markov chains. The logic is an extension
of linear-time temporal logic in the discrete-time domain. We have considered
the model checking problem in this setting. Our main result is that based on
Schanuel’s conjecture, the problem is decidable for the full class of
continuous-time Markov chains.

As mentioned in the introduction, our main goal has been to prove decidability
in as simple a fashion as possible without paying much attention to complexity
issues. We are however confident that number theory and linear algebraic
techniques can considerably lower the complexity of many of our constructions.
This could lead to a significant improvement of our algorithm from a practical
stand-point.

## Acknowledgments

We would like to thank Professor Joost-Pieter Katoen for discussions related
to this paper, including pointing out the references [CHKM11a, CHKM11b].

This work is supported by the National Key R$\&$D Program of China (Grant No:
2018YFA0306701), the National Natural Science Foundation of China (Grant No:
61832015), and DE180100156.

## References

  * [AAGT15] Manindra Agrawal, Sundararaman Akshay, Blaise Genest, and PS Thiagarajan.  Approximate verification of the symbolic dynamics of markov chains.  Journal of the ACM (JACM), 62(1):2, 2015.
  * [AFH96] Rajeev Alur, Tomás Feder, and Thomas A Henzinger.  The benefits of relaxing punctuality.  Journal of the ACM (JACM), 43(1):116–146, 1996.
  * [AH80] Cerino E Avellar and Jack K Hale.  On the zeros of exponential polynomials.  Journal of Mathematical Analysis and Applications, 73(2):434–452, 1980.
  * [AH94] Rajeev Alur and Thomas A Henzinger.  A really temporal logic.  Journal of the ACM (JACM), 41(1):181–203, 1994.
  * [AMW08] Melanie Achatz, Scott McCallum, and Volker Weispfenning.  Deciding polynomial-exponential problems.  In Proceedings of the twenty-first international symposium on Symbolic and algebraic computation, pages 215–222. ACM, 2008.
  * [ASSB00] Adnan Aziz, Kumud Sanwal, Vigyan Singhal, and Robert Brayton.  Model-checking continuous-time markov chains.  ACM Transactions on Computational Logic, 1(1):162–170, 2000.
  * [Bak90] Alan Baker.  Transcendental number theory.  Cambridge university press, 1990.
  * [BCH+11] Beno$\hat{i}$t Barbot, Taolue Chen, Tingting Han, Joost-Pieter Katoen, and Alexandru Mereacre.  Efficient ctmc model checking of linear real-time objectives.  In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 128–142. Springer, 2011.
  * [BHHK03] Christel Baier, Boudewijn Haverkort, Holger Hermanns, and J-P Katoen.  Model-checking algorithms for continuous-time markov chains.  IEEE Transactions on software engineering, 29(6):524–541, 2003\.
  * [BK08] Christel Baier and Joost-Pieter Katoen.  Principles of model checking.  MIT press, 2008.
  * [CA76] George E Collins and Alkiviadis G Akritas.  Polynomial real root isolation using descarte’s rule of signs.  In Proceedings of the third ACM symposium on Symbolic and algebraic computation, pages 272–275, 1976.
  * [CD88] Edmund M Clarke and I Anca Draghicescu.  Expressibility results for linear-time and branching-time logics.  In Workshop/School/Symposium of the REX Project (Research and Education in Concurrent Systems), pages 428–437. Springer, 1988.
  * [CE81] Edmund M Clarke and E Allen Emerson.  Design and synthesis of synchronization skeletons using branching time temporal logic.  In Workshop on Logic of Programs, pages 52–71. Springer, 1981.
  * [CES86] Edmund M. Clarke, E Allen Emerson, and A Prasad Sistla.  Automatic verification of finite-state concurrent systems using temporal logic specifications.  ACM Transactions on Programming Languages and Systems (TOPLAS), 8(2):244–263, 1986.
  * [CHKM11a] Taolue Chen, Tingting Han, Joost-Pieter Katoen, and Alexandru Mereacre.  Model checking of continuous-time markov chains against timed automata specifications.  arXiv preprint arXiv:1101.3694, 2011.
  * [CHKM11b] Taolue Chen, Tingting Han, Joost-Pieter Katoen, and Alexandru Mereacre.  Observing continuous-time mdps by 1-clock timed automata.  In International Workshop on Reachability Problems, pages 2–25. Springer, 2011.
  * [Coh13] Henri Cohen.  A course in computational algebraic number theory, volume 138.  Springer Science & Business Media, 2013.
  * [COW15] Ventsislav Chonev, Joël Ouaknine, and James Worrell.  On the skolem problem for continuous linear dynamical systems.  arXiv preprint arXiv:1506.00695, 2015.
  * [EH86] E Allen Emerson and Joseph Y Halpern.  “sometimes” and “not never” revisited: on branching versus linear time temporal logic.  Journal of the ACM (JACM), 33(1):151–178, 1986.
  * [GCL+17] Ting Gan, Mingshuai Chen, Yangjia Li, Bican Xia, and Naijun Zhan.  Reachability analysis for solvable dynamical systems.  IEEE Transactions on Automatic Control, 63(7):2003–2018, 2017.
  * [GS07] Charles Miller Grinstead and James Laurie Snell.  Introduction to Probability.  Swarthmore College, pages 1–520, 2007.
  * [HJ94] Hans Hansson and Bengt Jonsson.  A logic for reasoning about time and reliability.  Formal aspects of computing, 6(5):512–535, 1994.
  * [Joh98] Jeremy R Johnson.  Algorithms for polynomial real root isolation.  In Quantifier elimination and cylindrical algebraic decomposition, pages 269–299. Springer, 1998.
  * [Kat16] Joost-Pieter Katoen.  The probabilistic model checking landscape.  In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, pages 31–45. ACM, 2016.
  * [KNP02] Marta Kwiatkowska, Gethin Norman, and David Parker.  Prism: Probabilistic symbolic model checker.  In International Conference on Modelling Techniques and Tools for Computer Performance Evaluation, pages 200–204. Springer, 2002.
  * [Kol31] Andrei Kolmogoroff.  Über die analytischen methoden in der wahrscheinlichkeitsrechnung.  Mathematische Annalen, 104(1):415–458, 1931.
  * [Koy90] Ron Koymans.  Specifying real-time properties with metric temporal logic.  Real-time systems, 2(4):255–299, 1990.
  * [KZH+11] Joost-Pieter Katoen, Ivan S Zapreev, Ernst Moritz Hahn, Holger Hermanns, and David N Jansen.  The ins and outs of the probabilistic model checker mrmc.  Performance evaluation, 68(2):90–104, 2011.
  * [Lam80] Leslie Lamport.  Sometime is sometimes not never: On the temporal logic of programs.  In Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 174–185. ACM, 1980.
  * [Lan66] Serge Lang.  Introduction to transcendental numbers.  Addison-Wesley Pub. Co., 1966.
  * [Len87] Arjen K Lenstra.  Factoring multivariate polynomials over algebraic number fields.  SIAM Journal on Computing, 16(3):591–598, 1987.
  * [LHXL16] Jing-Cao Li, Cheng-Chao Huang, Ming Xu, and Zhi-Bin Li.  Positive root isolation for poly-powers.  In Proceedings of the ACM on International Symposium on Symbolic and Algebraic Computation, pages 325–332. ACM, 2016.
  * [LLL+82] Hendrik Willem Lenstra, Arjen K Lenstra, L Lovfiasz, et al.  Factoring polynomials with rational coeficients.  Math.Ann., 261:515–534, 1982.
  * [LMDB95] Douglas Lind, Brian Marcus, Lind Douglas, and Marcus Brian.  An introduction to symbolic dynamics and coding.  Cambridge university press, 1995.
  * [LP85] Orna Lichtenstein and Amir Pnueli.  Checking that finite state concurrent programs satisfy their linear specification.  In Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 97–107. ACM, 1985.
  * [MH38] Marston Morse and Gustav A Hedlund.  Symbolic dynamics.  American Journal of Mathematics, 60(4):815–866, 1938.
  * [MW96] Angus Macintyre and Alex J Wilkie.  On the decidability of the real exponential field.  1996\.
  * [Nes96] Yu Nesterenko.  Modular functions and transcendence problems.  Comptes rendus de l’Académie des sciences. Série 1, Mathématique, 322(10):909–914, 1996.
  * [Pnu77] A. Pnueli.  The temporal logic of programs.  In 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pages 46–57, Oct 1977.
  * [QS82] Jean-Pierre Queille and Joseph Sifakis.  Specification and verification of concurrent systems in cesar.  In International Symposium on programming, pages 337–351. Springer, 1982.
  * [Ric97] Daniel Richardson.  How to recognize zero.  Journal of Symbolic Computation, 24(6):627–645, 1997.
  * [Rit29] Joseph Fels Ritt.  On the zeros of exponential polynomials.  Transactions of the American Mathematical Society, 31(4):680–686, 1929.
  * [Ter08] Giuseppina Terzo.  Some consequences of schanuel’s conjecture in exponential rings.  Communications in Algebra®, 36(3):1171–1189, 2008\.
  * [Tij71] Robert Tijdeman.  On the number of zeros of general exponential polynomials.  In Indagationes Mathematicae (Proceedings), volume 74, pages 1–7. North-Holland, 1971.
  * [VW86] Moshe Y Vardi and Pierre Wolper.  An automata-theoretic approach to automatic program verification.  In Proceedings of the First Symposium on Logic in Computer Science, pages 322–331. IEEE Computer Society, 1986.
  * [Yu19] Nengkun Yu.  Quantum temporal logic: from birkhoff and von neumann to pnueli.  arXiv preprint arXiv:1908.00158, 2019.