Linear-Time Model Checking Branching Processes
Stefan Kiefer
University of Oxford, UK

Pavel Semukhin
University of Oxford, UK

Cas Widdershoven
University of Oxford, UK

Abstract(Multi-type) branching processes are a natural and well-studied model for generating random infinite
trees. Branching processes feature both nondeterministic and probabilistic branching, generalizing
both transition systems and Markov chains (but not generally Markov decision processes). We
study the complexity of model checking branching processes against linear-time omega-regularspecifications: is it the case almost surely that every branch of a tree randomly generated by
the branching process satisfies the omega-regular specification? The main result is that for LTL
specifications this problem is in PSPACE, subsuming classical results for transition systems andMarkov chains, respectively. The underlying general model-checking algorithm is based on theautomata-theoretic approach, using unambiguous Büchi automata.
2012 ACM Subject Classification Theory of computation → Automata over infinite objects; Theoryof computation → Verification by model checking
Keywords and phrases model checking, Markov chains, branching processes, automata, computational complexity
Digital Object Identifier 10.4230/LIPIcs.CONCUR.2021.6
Related Version Full Version: https://arxiv.org/abs/2107.01687
Funding Stefan Kiefer: supported by a Royal Society University Research Fellowship.

1

Introduction

Checking whether a (labelled) transition system satisfies a linear-time specification is a staple
in verification. The specification is often given as a formula of linear temporal logic (LTL).
While early procedures for LTL model checking work directly with the formula [25], theautomata-theoretic approach translates LTL formulas into finite automata on infinite words,
such as Büchi automata, and analyzes a product of the system and the automaton [37]. Thisapproach can lead to clean and modular model-checking algorithms.
Although LTL captures only a subset of ω-regular languages, model-checking algorithms
based on the automata-theoretic approach can be made optimal from the point of view ofcomputational complexity. In particular, model checking finite transition systems against
LTL specifications is PSPACE-complete [32], and the algorithm [37] that, loosely speaking,translates (the negation of) the LTL formula into a Büchi automaton and checks the productwith the transition system for emptiness can indeed be implemented in PSPACE.
The same approach does not directly work for probabilistic systems modelled as finite
Markov chains: intuitively, the nondeterminism in a Büchi automaton causes issues in astochastic setting where the specification should hold with probability 1, i.e., almost surely
but not necessarily surely. A possible remedy is to translate the nondeterministic Büchi
automaton further into a deterministic automaton, e.g., a deterministic Rabin automaton(deterministic Büchi automata are less expressive), with which the Markov chain can benaturally instrumented and subsequently analyzed. This determinization step causes a© Stefan Kiefer, Pavel Semukhin, and Cas Widdershoven;licensed under Creative Commons License CC-BY 4.0
32nd International Conference on Concurrency Theory (CONCUR 2021).
Editors: Serge Haddad and Daniele Varacca; Article No. 6; pp. 6:1–6:16
Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

6:2

Linear-Time Model Checking Branching Processes(second) exponential blowup and does not lead to algorithms that are optimal from acomputational-complexity point of view. However, for Markov decision processes (MDPs),
which allow for nondeterminism in the probabilistic system, this approach is adequate andleads to an optimal, double-exponential time, model-checking algorithm.
Checking whether a Markov chain satisfies an LTL specification with probability 1 is
PSPACE-complete, but membership in PSPACE was proved only in [10, 11], not using theautomata-theoretic approach but by a recursive procedure on the formula. This raised thequestion if there is also an optimal algorithm based on the automata-theoretic approach; see[36] for a survey of the state of the art at the end of the 90s.
The answer is yes and was first given in [12], using a single-exponential translationfrom LTL to separated Büchi automata. Such automata are special unambiguous Büchi
automata, which restrict nondeterministic Büchi automata by requiring that every word
have at most one accepting run. Another algorithm, using alternating Büchi automata, wasproposed in [6], exploiting reverse determinism, a property also related to unambiguousness.
A polynomial-time (even NC) model-checking algorithm for Markov chains against generalunambiguous Büchi automata was given in [2]. These works all imply optimal PSPACE
algorithms for LTL model checking of Markov chains via the automata-theoretic approach.
In this paper we exhibit an LTL model checking algorithm that has the following features:(1) it applies to (multi-type) branching processes, a well established model for random trees,
generalizing both nondeterministic transition systems and Markov chains; (2) it runs in
PSPACE, which is the optimal complexity both for nondeterministic transition systems andMarkov chains; and (3) it is based on the automata-theoretic approach (using unambiguous
Büchi automata). The fact that there exists an algorithm with the first two features
might seem surprising, as one might think that any system model that encompasses both
nondeterminism and probability will generalize MDPs, for which LTL model checking is
2EXPTIME-complete [11].
Branching processes (BPs) are a well-studied model in mathematics with applications
in numerous fields including biology, physics and natural language processing; see, e.g.,[23, 1, 22]. BPs randomly generate infinite trees, and, from a computer-science point of view,
they might be the most natural model to do so: (multi-type) BPs can be thought of as a
version of stochastic context-free grammars without terminal symbols, randomly generating
infinite derivation trees. For example, consider the following BP, taken from [8], with 3 types
I, B, D:
0.9

0.2

I ,−−→ I

1

B ,−−→ D

0.1

D ,−
→D

0.5

I ,−−→ IB

B ,−−→ B(1)

0.3

B ,−−→ BB
This BP might generate a tree with the following prefix:
I
I

B

I
I

B

B

B

B

D

The probability that the BP generates a tree with the shown prefix is the product of theprobabilities of the fired transition rules, i.e., (in breadth-first order) 0.1 · 0.9 · 0.3 · 0.1 · 0.5 · 0.2.

S. Kiefer, P. Semukhin, and C. Widdershoven

6:3

BPs generalize transition systems. Consider the following transition system:
X

Y

1

1

It is equivalent to the BP with X ,−→ Y and Y ,−→ XY , which generates with probability 1
the following unique tree:
X
Y
X

Y

Y

X

Y

The branches of this unique tree are exactly the executions of the transition system. As aconsequence, any LTL formula holds on all executions of the transition system if and only if
it holds (with probability 1) on all branches of the generated tree.
BPs also generalize Markov chains. Consider the following Markov chain:
1
X

Y

0.7

0.3
1

0.3

0.7

It is equivalent to the BP with X ,−→ Y and Y ,−−→ X and Y ,−−→ Y , which generates, withprobabilities 0.3, 0.7 · 0.3, 0.7 · 0.7, respectively, the following prefixes of (degenerated) trees:
X

X

X

Y

Y

Y

X

Y

Y

Y

X

Y

Here, each possible “tree” has only a single branch, and the possible “trees” are distributedin the same way as the possible executions of the Markov chain. As a consequence, any LTL
formula holds with probability 1 on a random execution of the Markov chain if and only if itholds with probability 1 on the (single) branch of the generated tree.
Hence, both for the transition system and for the Markov chain, the respective modelchecking question reduces to the BP model-checking problem which asks whether withprobability 1 the property holds on all branches.
For LTL specifications, we refer to this BP model-checking problem as P(LTL) = 1.
Our main result is that it is in PSPACE, generalizing the corresponding classical resultson transition systems and Markov chains. As mentioned, our model-checking algorithm isbased on the automata-theoretic approach, in particular on unambiguous Büchi automata.
Another important technical ingredient is the algorithmic analysis of certain nonnegative
matrices in terms of their spectral radius.

CONCUR 2021

6:4

Linear-Time Model Checking Branching Processes

The latter points to the fact that the numbers in the system generally matter, eventhough we only consider the qualitative problem of comparing the satisfaction probability
with 1. For example, for the BP given in (1), one can show that the probability that all
branches eventually hit a node of type D is less than 1 (in fact, it is 0). Intuitively, this0.3

is because the probability of “branching” via B ,−−→ BB is larger than the probability of
0.2“dying” via B ,−−→ D. Were the probabilities 0.3 and 0.2 swapped, the probability that all
branches eventually hit a node of type D would be 1; cf. [8, Section 1].
We also consider the problem P(LTL = 0), which asks whether the probability thatall branches satisfy a given LTL formula is 0. Even though it is trivial to negate an LTL
formula, this problem is (unlike in Markov chains) not equivalent to the complement ofP(LTL = 1), because even when the probability is less than 1 that the formula holds on all
branches, the probability may still be 0 that the negated formula holds on all branches. We
will show that P(LTL = 0) is much more computationally complex than P(LTL = 1): it is
2EXPTIME-complete.
Besides LTL, we also consider automata-based specifications. Büchi automata are relevantfrom a verification point of view, as a way of specifying desired or undesired executions of thesystem. Unambiguous Büchi automata are useful from a technical point of view, in particular,
to facilitate our main result on P(LTL = 1). See Section 2 and Table 1 for definitions of ourproblems and a map of our results.
▶ Remark 1. Readers familiar with MDPs may wonder how the problem P(LTL) = 1 canhave lower computational complexity than the problem whether all schedulers of an MDP
satisfy an LTL specification almost surely. Consider the BP1

X ,−→ Y1 Y2

0.7

Y1 ,−−→ X

0.3

0.5

Y1 ,−−→ Z

Y2 ,−−→ X

0.5

1Y2 ,−−→ Z

Z ,−
→Z,

which might be depicted graphically as follows:
Y1
0.7

0.3

0.5

0.5

X

Z

1

Y2
One might view this BP as an MDP where in an X-node the scheduler nondeterministically
picks either the Y1 - or the Y2 -successor, and in an Yi -node, the X- or the Z-successor ischosen randomly. In such an MDP, regardless of the scheduler, a random run reaches withprobability 1 a Z-node. However, in the BP above, the probability is positive that somebranch of a random tree never reaches a Z-node. Although each branch of a random tree
could be thought of as being witnessed by at least one scheduler, this is not a contradiction,
as there are uncountably many schedulers (over which one cannot take a sum). Hence, if
an MDP is interpreted as a BP in the way sketched above, then the requirement that theBP satisfy an LTL formula almost surely on all branches is stronger, and computationallyless complex to check, than the requirement that the MDP satisfy, for each scheduler, theformula almost surely.
Related work. We have already discussed related work concerning model checking transition
systems and Markov chains.

S. Kiefer, P. Semukhin, and C. Widdershoven

6:5

In addition to the mentioned applications of BPs in various fields, there has also been
work on BPs in computer science, especially in the last 10 years. This paper builds on [8],where specifications in terms of deterministic parity tree automata are considered. The
work [8] implies decidability of the problems considered in this paper and some basic uppercomplexity bounds. For example, it is not hard to derive from [8] that P(LTL = 1) is in
2EXPTIME. Lowering this to PSPACE is the main achievement of this paper.
A related strand of work considers regular tree languages; i.e., the specification is not interms of a word automaton that is run on each branch but in terms of tree automata. Even
measurability is not easy to show in this case [20], and fundamental decidability questions
around computing the measure have been answered positively only for subclasses of regulartree languages [26, 27].
Fundamental results on the complexity of algorithmically analyzing BPs have beenobtained in [18]. Indeed, in Section 3.1 we build on and improve results from [18] on
finiteness (more often called “extinction” in the literature) of BPs.
Another recent line of work considers extensions of BPs with nondeterminism, focusing
on algorithmic questions about properties such as reachability. Branching MDPs, which
are BPs where a controller chooses actions to influence the evolution of the tree, have been
investigated, e.g., in [16, 17]. Even branching games, featuring two adversarial controllers,have been studied recently [14].
The work [21] also considers BPs with “internal” nondeterminism (as opposed to the“external” nondeterminism manifested as branching in the generated tree), along with modelchecking problems against the logic GPL. This expressive, µ-calculus based modal logic
had been introduced in [9]. The system model therein, called reactive probabilistic labeledtransition systems (RPLTSs), is essentially equivalent to BPs as considered in this paper.
BPs are related to models for probabilistic programs with recursion, such as Recursive
Markov chains, for which model-checking problems have been studied in detail; see, inparticular, [19]. Very loosely speaking, a run of a (“1-exit”) Recursive Markov chain canbe viewed as a depth-first traversal of a tree generated by a BP. Indeed, for a lower boundin the present paper (Theorem 11) we adapt a proof from [19]. However, most qualitativemodel-checking problems for Recursive Markov chains are EXPTIME-complete [19], and somany of the BP problems we study turn out to have different computational complexity.
As a key technical tool we use unambiguous Büchi automata, as recently proposed forMarkov chains [2]. It is non-trivial to extend their use to random trees, as the branching
behaviour of BPs interferes with the spectral-radius based analysis from [2]. One may viewas the main technical insight of this paper that the limited nondeterminism in unambiguous
automata can be combined with the tree branching of BPs, so that, in a sense, BP model
checking reduces to comparing the spectral radius of a certain nonnegative matrix with 1(Proposition 16).

2

Preliminaries

Let N and N0 denote the set of positive and nonnegative integers, respectively. For a finite
set Γ, we write Γ∗ (resp., Γ+ ) for the set of words (resp., nonempty words) over Γ.
Branching processes. A (multi-type) branching process (BP) is a tuple B = (Γ, ,−→, Prob, X0 ),where Γ is a finite set of types, ,−→ ⊆ Γ × Γ+ is a finite set of transition rules, Prob is afunction assigning positive rational probabilities to transition rules so that for every X ∈ ΓPpwe have X ,−→ w) = 1, and X0 ∈ Γ is the start type. We write X ,−→ w to→w Prob(X ,−CONCUR 2021

6:6

Linear-Time Model Checking Branching Processes

denote that Prob(X ,−→ w) = p. Given a BP B and a type X ∈ Γ we write B[X] for the BP
obtained from B by making X the start type. For X, Y ∈ Γ we call Y a successor of X if
there is a rule X ,−→ uY v for some u, v ∈ Γ∗ .
A BP with ε-rules allowed relaxes the requirement ,−→ ⊆ Γ × Γ+ to ,−→ ⊆ Γ × Γ∗ , i.e.,there may be rules of the form X ,−→ ε, where ε denotes the empty word. In the following,
we disallow ε-rules unless specified otherwise; but the definitions generalize in a natural way.
Fix a BP B = (Γ, ,−→, Prob, X0 ) for the rest of the section.
Trees. Write JBK for the set of trees generated by B; i.e., JBK denotes the set of orderedΓ-labelled trees t such that for each X ∈ Γ and each X-labelled node v in t, there is a ruleX ,−→ X1 · · · Xk , denoted by rule(v), such that the k ordered children of v are labelled with
X1 , . . . , Xk , respectively. We say a node has type X ∈ Γ if the node is labelled with X. A
finite prefix of a tree t ∈ JBK is an ordered Γ-labelled finite tree obtained from t by designatingsome nodes as leaves, and removing all their children, grandchildren, etc. Write LBM for theset of finite prefixes of trees generated by B. For t ∈ LBM write t↓ ⊆ JBK for the (“cylinder”)
set of trees t′ ∈ JBK such that t is a finite prefix of t′ . For X ∈ Γ write JBKX ⊆ JBK and
LBMX ⊆ LBM for the subsets of trees whose root has type X; the trees in JBKX are called
X-trees. A branch of a tree t is a sequence v0 v1 · · · of nodes in t, where v0 is the root of t andvi+1 is a child of vi for all i ∈ N0 . See [8] for equivalent, more formal tree-related definitions.
Probability space. For each X ∈ Γ we define the probability space (JBKX , ΣX , PX ), whereΣX is the σ-algebra generated by {t↓ | t ∈ LBMX }, and PX is the probability measureQ
generated by PX (t↓) := v Prob(rule(v)) for all t ∈ LBMX , where the product extends over
all non-leaf nodes v in t. This is analogous to the standard definition of the probability spaceof a Markov chain. We may write PB for PX0 , omitting the subscript when B is understood.
We often talk about events (i.e., measurable sets of trees) and their probability in text form.
For example, by saying “a B-tree has with positive probability infinitely many nodes oftype X” we mean that PB (E) > 0 where E ⊆ JBKX0 is the set of X0 -trees with infinitely
many nodes of type X.
Linear-Time Properties. We are particularly interested in sets of trees all whose branches(more precisely, their associated sequences of types) satisfy an ω-regular linear-time property
L ⊆ Γω . Given L ⊆ Γω , we write PB (L) for the probability that all branches of a B-treesatisfy L. Linear temporal logic (LTL) formulas specify linear-time properties; see, e.g.,[34] for a definition of LTL. An important example for us are formulas of the form FT ,where T ⊆ Γ, which denotes the linear-time property {uXw | u ∈ Γ∗ , X ∈ T, w ∈ Γω }.
Accordingly, PB (FT ) denotes the probability that all branches of a B-tree have a node whosetype is in T (equivalently, the probability that a B-tree has a finite prefix all whose leaves
have a type in T ).
Automata. We use finite automata on infinite words over Γ, where Γ is the set of types ofa BP. We use deterministic parity automata (DPAs), deterministic Büchi automata (DBAs),
nondeterministic Büchi automata (NBAs), and unambiguous Büchi automata (UBAs). The
definitions are standard; see, e.g., [34]. In the following we fix some terms and notation.
Let A = (Q, Γ, δ, Q0 , F ) be an NBA, where Q is a finite set of states, Γ is the alphabet,δ ⊆ Q × Γ × Q is the transition relation, Q0 ⊆ Q is the set of initial states, and F ⊆ Q isX
the set of accepting states. We write q −→ r to denote that (q, X, r) ∈ δ. A finite sequence
XXX

X ···X12nn ∗q0 −−→
q1 −−→· · · −−→
qn is called a path and can be summarized as q0 −−1−−−→
qn . AnS. Kiefer, P. Semukhin, and C. Widdershoven

6:7

Table 1 Results and organization of the paper. The complexity classes indicate completenessresults, except “in NC”, which only means membership in NC.
=1
in NC
Proposition 6=0

P(finite)
Section 3.1
P(DPA)
Section 3.2

in NC
Theorem 8P(NBA)
Section 3.3

PSPACE
Theorem 10
X

P(coNBA)
Section 4=1
PSPACE
Theorem 14

P
Theorem 9P(coUBA)
Section 5

in NC
Proposition 16

EXPTIME
Theorem 11P(LTL)
Section 6

PSPACE
Theorem 18=0
EXPTIME
Theorem 15

2EXPTIME
Theorem 19

X

1
2
infinite sequence q0 −−→
q1 −−→· · · is called a run of X1 X2 · · · . We call the run accepting
if q0 ∈ Q0 and qi ∈ F holds for infinitely many qi . The NBA A accepts (resp., rejects) an
infinite word w ∈ Γω if w has (resp., does not have) an accepting run in A. The NBA A iscalled an unambiguous Büchi automaton (UBA) if every w ∈ Γω has at most one accepting
run. An automaton A defines ω-regular linear-time properties {w ∈ Γω | A accepts w}
and {w ∈ Γω | A rejects w}. In keeping with previous definitions, we write PB (A accepts)(resp., PB (A rejects)) for the probability that all branches of a B-tree (more precisely, theirassociated sequences of types) are accepted (resp., rejected) by A.

Problems. We consider the following computational problems. The problem P(finite) = 1
asks, given a BP B with ε-rules allowed, whether the probability that a B-tree is finite is 1.
The problem P(LTL) = 1 asks, given a BP B and an LTL formula φ, whether PB (φ) = 1.
The problems P(DPA) = 1 (resp., P(NBA) = 1) ask, given a BP B and a DPA (resp.,
NBA) A, whether PB (A accepts) = 1. The problems P(coNBA) = 1 (resp., P(coUBA) = 1)1
ask, given a BP B and an NBA (resp., UBA) A, whether PB (A rejects) = 1. The problems
P(LTL) = 0, P(DPA) = 0, . . . are defined similarly, where “= 1” is replaced with “= 0”. See
Table 1 for a map of our results in those terms, as well as for an overview of the rest of thepaper. As explained in the introduction, the problem P(LTL) = 1 is of particular interest
from a model-checking point of view, and the technically most challenging one.
Complexity Classes. In addition to standard complexity classes between P and 2EXPTIME,
we use the class NC, the subclass of P comprising those problems solvable in polylogarithmic
time by a parallel random-access machine using polynomially many processors; see, e.g., [28,Chapter 15]. To prove membership in PSPACE in a modular way, we will use the following
pattern:▶ Lemma 2. Let P1 , P2 be two problems, where P2 is in NC. Suppose there is a reduction
from P1 to P2 implemented by a PSPACE transducer, i.e., a Turing machine whose work
tape (but not necessarily its output tape) is PSPACE-bounded. Then P1 is in PSPACE.
Proof. Note that the output of the transducer is (at most) exponential. Problems in NC
can be decided in polylogarithmic space [4, Theorem 4]. Using standard techniques forcomposing space-bounded transducers (see, e.g., [28, Proposition 8.2]), it follows that P1 isin PSPACE.
◀
1

We do not explicitly define or use a notion of “co-Büchi automata” to avoid possible confusion about
accepting/rejecting. If one were to do so, one would define a “co-NBA” A like an NBA A, but the“co-NBA” A would accept a word w ∈ Γω if and only if A viewed as an NBA rejects w. Similarly for“co-UBAs”.

CONCUR 2021

6:8

Linear-Time Model Checking Branching Processes

Matrices. We use finite sets S to index matrices M ∈ RS×S and vectors v ∈ RS . The graphof a nonnegative matrix M ∈ [0, ∞)S×S is the directed graph (S, E) with E = {(s, t) ∈ S ×S |Ms,t > 0}. The spectral radius of a matrix is the largest absolute value of its eigenvalues.
The following lemma allows to efficiently compare the spectral radius of a nonnegative matrix
with 1.
▶ Lemma 3. Given a nonnegative rational matrix M , one can determine in NC whetherρ < 1 or ρ = 1 or ρ > 1, where ρ denotes the spectral radius of M .
Proof. Use the algorithm from [13, Proposition 2.2], but not with Gaussian elimination as suggested there, but by solving the systems of linear equations described in [13, Proposition 2.2]
in NC. The latter is possible in NC [5, Theorem 5].
◀

3

Basic Results

In this section we develop the more basic results indicated in Table 1, on finiteness (Section 3.1),
deterministic parity automata (Section 3.2), and Büchi automata (Section 3.3), on the one
hand rounding off the complexity map in Table 1, and on the other hand building thefoundation for more challenging results in the following sections. In particular, Proposition 6
is indirectly used throughout the paper.

3.1

FinitenessIn this section we consider BPs with ε-rules allowed, i.e., rules of the form X ,−→ ε. Such
BPs may generate finite trees. We are interested in the almost-sure finiteness problem, also
denoted as P(finite) = 1, i.e., the problem whether the probability that a given BP with
ε-rules allowed generates a finite tree is equal to 1. In Proposition 6 below we show that thisproblem is in NC. All upper bounds on the complexity of P(·) = 1 problems in this paperbuild directly or indirectly on this result.
While the almost-sure finiteness (or “extinction”) problem has often been studied and is
known to be in (strongly) polynomial time [18, 13], its membership in NC is, to the bestof the authors’ knowledge, new. For instance, since linear programming is P-complete, one
cannot use linear programming (as in [18]) to show membership in NC. Nor can one directly
use the strongly polynomial-time algorithm of [13], as it computes, in a sub-procedure, theset of types X for which there exists a finite X-tree. But the latter problem is P-complete.
For the rest of the section, fix a BP B = (Γ, ,−→, Prob, X0 ) with ε-rules allowed. Definea directed graph G = (Γ, E) (i.e., the types of B are the vertices of G) with an edge
(X, Y ) ∈ E if and only if Y is a successor of X (i.e., there is a rule X ,−→ uY v for someu, v ∈ Γ∗ ). Given a strongly connected component (SCC) S ⊆ Γ of G and X ∈ S, define a BP
B[S, X] = (S, ,−→S , ProbS , X) obtained from B by restricting the types to S and deleting on
all right-hand sides of the rules those types not in S. The following lemma is straightforward:▶ Lemma 4. A B-tree is infinite with positive probability if and only if there exist an SCC
S ⊆ Γ of G and X ∈ S such that X is reachable from X0 in G and a B[S, X]-tree is infinite
with positive probability.
Pp
Let M ∈ QΓ×Γ be the nonnegative Γ × Γ-matrix with MX,Y =p|w|Y , whereX ,−→w|w|Y ∈ N0 is the number of occurrences of Y in w. That is, MX,Y is the expected numberof direct Y -successors of the root of a B[X]-tree. By induction, M i , the ith power of M , issuch that (M i )X,Y is the expected number of Y -nodes that are exactly i levels under theroot of a B[X]-tree. The graph of M is exactly the previously defined graph G.

S. Kiefer, P. Semukhin, and C. Widdershoven

6:9

Let S ⊆ Γ be an SCC of G. Denote by MS ∈ QS×S the (square) principal submatrix
obtained from M by restricting it to the rows and columns indexed by elements of S. Let ρSdenote the spectral radius of MS . Call S supercritical if ρS > 1. Call S linear if for all rules
X ,−→ w with X ∈ S there is exactly one occurrence in w of a type in S. Observe that if S islinear then MS is stochastic, i.e., MS⃗1 = ⃗1 where ⃗1 is the all-1 vector, i.e., the element of{1}S . In that case, by the Perron-Frobenius theorem [3, Theorem 2.1.4 (b)], we have ρS = 1
and, thus, S is not supercritical.
The following characterization can be proved using [13, Section 3] (which builds on [18,Section 8.1]):▶ Lemma 5. A B-tree is infinite with positive probability if and only if there exist an SCC
S ⊆ Γ of G and X ∈ S such that X is reachable from X0 in G and S is supercritical or
linear.
It follows:▶ Proposition 6. The problem P(finite) = 1 is in NC.

3.2

Deterministic Parity Automata

In this section we consider deterministic parity automata (DPAs) on words. In [8, Section 3]
it was shown that the problem P(DPA) = 1 can be decided in polynomial time. We improve
this to membership in NC.
By the following lemma we can check in NC whether a B-tree almost surely has a finite
prefix all whose leaves have types in a given set T . The proof is by reduction to almost-surefiniteness.
▶ Lemma 7. Given a BP B = (Γ, ,−→, Prob, X0 ) and a set of types T ⊆ Γ, the problem
whether PX0 (FT ) = 1 is in NC.
By combining Lemma 7 with results from [8] we obtain:▶ Theorem 8. The problem P(DPA) = 1 is in NC.
The hardness result in the following theorem highlights the different complexities ofP(·) = 0 and P(·) = 1 problems in this paper.
▶ Theorem 9. The problem P(DPA) = 0 is P-complete. It is P-hard even for deterministic
Büchi automata with two states, the accepting state being a sink.

3.3

Büchi Automata▶ Theorem 10. The problem P(NBA) = 1 is PSPACE-complete.
Proof. PSPACE-hardness is immediate in two different ways. It follows from the PSPACEhardness of model checking Markov chains against NBAs [35]. It also follows from the
PSPACE-hardness of model checking transition systems against NBAs. (The latter follows
easily from the PSPACE-hardness of NBA universality [32].) Both model-checking problems
are special cases of P(NBA) = 1.
Towards membership in PSPACE, we use a translation from NBA to DPA [29]. Thistranslation causes an exponential blow-up, but an inspection of the construction [29, Section 3.2] reveals that it can be computed by a PSPACE transducer. By Theorem 8 theproblem P(DPA) = 1 is in NC. By Lemma 2 it follows that P(NBA) = 1 is in PSPACE. ◀

CONCUR 2021

6:10

Linear-Time Model Checking Branching Processes▶ Theorem 11. The problem P(NBA) = 0 is EXPTIME-complete. It is EXPTIME-hardeven for NBAs whose only accepting state is a sink.
Proof. Towards membership in EXPTIME, an NBA can be translated, in exponential time,
to a DPA of exponential size; see, e.g., [29]. Since P(DPA) = 0 is in P by Theorem 9, it
follows that P(NBA) = 0 is in EXPTIME.
Concerning EXPTIME-hardness, we adapt the proof (in the online appendix) of [19,Theorem 17] on model checking recursive Markov chains against NBAs. The details arein [24].
◀

4

Co-Büchi Automata

In this section we consider the problem P(coNBA) = 1, which asks, given a BP B and a Büchi
automaton A, whether B almost surely generates a tree whose branches are all rejected by A;i.e., whether PB (A rejects) = 1. Dually, one might ask whether the probability is positivethat a B-tree has a branch accepted by A. Intuitively, we view the Büchi automaton A as
specifying “bad” branches, and we would like the tree almost surely not to have any badbranches.
This problem is in PSPACE, which can be shown via a translation to DPAs, as in Theorem 10. However, with a view on the following sections, in particular on LTL specifications,
we pursue a different approach to the problem P(coNBA) = 1. In this section we lay thegroundwork for arbitrary Büchi automata A. By building on these results, we will show in
the next section that if A is unambiguous then the problem is in NC, which will allow us toderive our headline result, namely that P(LTL) = 1 is in PSPACE.
Let B = (Γ, ,−→, Prob, X0 ) be a BP and A = (Q, Γ, δ, Q0 , F ) a (not necessarily unambiguous) Büchi automaton.
Define a Büchi automaton, A × B, by A × B := (Q × Γ, Γ, δA×B , Q0 × {X0 }, F × Γ), where(δ(q1 , X1 ) × {X2 } if X2 is a successor of X1
δA×B ((q1 , X1 ), X2 ) =∅otherwise.
The remainder of the section is organized as follows. In Section 4.1 we show that the
problem P(coNBA) = 1 reduces to the analysis of certain SCCs within A × B. In Section 4.2
we introduce a key lemma, Lemma 13, which allows us to “forget” about the distinction
between accepting and non-accepting states: the lemma reduces P(coNBA) = 1 to a purereachability problem in an exponential-sized BP, Bdet . This leads us to prove PSPACEcompleteness of P(coNBA) = 1, but more importantly, Lemma 13 plays a key role in the restof the paper. We prove it in [24].

4.1

The Automaton A[f, Xf ]For any (f, Xf ) ∈ F × Γ on a cycle of the transition graph of A × B, define the Büchi
automaton
A[f, Xf ] := ({q̄0 } ∪ Q[f, Xf ], Γ, δ[f, Xf ], {q̄0 }, {(f, Xf )})as the Büchi automaton obtained from A × B by
1. making (f, Xf ) the only accepting state,
2. restricting the set of states, Q[f, Xf ] ⊆ Q × Γ, to those (q, X) that, in the transition
graph of A × B, are reachable from (f, Xf ) and can reach (f, Xf ), i.e., those (q, X) in
the SCC containing (f, Xf ),S. Kiefer, P. Semukhin, and C. Widdershoven

6:11

3. restricting the transition function δ[f, Xf ] accordingly, i.e.,δ[f, Xf ]((q, X), Y ) := δA×B ((q, X), Y ) ∩ Q[f, Xf ] ,4. making q̄0 the only initial state, and
5. setting δ[f, Xf ](q̄0 , Xf ) := {(f, Xf )} and δ[f, Xf ](q̄0 , X) := ∅ for all X ∈ Γ \ {Xf }.
The following lemma follows from the pigeonhole principle and basic probability arguments:▶ Lemma 12. The probability that some branch of a B-tree is accepted by A is positive if andonly if there are q0 ∈ Q0 and f ∈ F and Xf ∈ Γ such that (f, Xf ) is reachable from (q0 , X0 )in the transition graph of A × B and the probability that some branch of a B[Xf ]-tree is
accepted by A[f, Xf ] is positive.
For the rest of the section let (f, Xf ) ∈ F × Γ be on a cycle of the transition graph of
A × B.

4.2

The Determinization Adet and the BP Bdet

Let
Adet := (2{q̄0 }∪Q[f,Xf ] , Γ, δdet , {q̄0 }, 2{q̄0 }∪Q[f,Xf ] \ {∅})
be the determinization of A[f, Xf ] obtained by the standard subset construction. Whichstates are accepting will not actually be relevant. Note that every state reachable via anonempty path from {q̄0 } is of the form P × {X} with P ⊆ Q and X ∈ Γ.
Define a BP Bdet based on Adet as
Bdet := (Γ′ , ,−→′ , Prob′ , {(f, Xf )}) ,where the set of types Γ′ ⊆ 2Q[f,Xf ] is the set of those states in Adet that are reachable(in Adet ) from {q¯0 } via a nonempty path (recall that they are of the form P × {X} withP ⊆ Q and X ∈ Γ), andp

X ′ ,−→′ δdet (X ′ , X1 ) · · · δdet (X ′ , Xk )p

1

for all X ′ = P × {X} ∈ Γ′ with P ̸= ∅ and all X ,−→ X1 · · · Xk , and ∅ ,−→′ ∅. Here is the key
lemma of this section:▶ Lemma 13. The following statements are equivalent:(i) The probability that some branch of a B[Xf ]-tree is accepted by A[f, Xf ] is positive.
(ii) The probability that some branch of a Bdet -tree does not have any nodes of type ∅ ispositive.
We prove Lemma 13 in [24]. It will be used in the proof of Theorem 14 below; but more
importantly, Lemma 13 is the foundation of Section 5.
Given that Lemma 13 reflects the key insight of this section, let us comment further.
Considering that condition (ii) does not mention a notion of acceptance, one might have twoconcerns at this point:(a) Condition (ii) does not obviously imply that with positive probability there is even abranch with infinitely many nodes of types containing (f, Xf ).
(b) Even if with positive probability there is such a branch, it is not obvious that suchbranches would necessarily correspond to branches of B[Xf ] that are accepted by A[f, Xf ].

CONCUR 2021

6:12

Linear-Time Model Checking Branching Processes

Even for the special case of Markov chains (i.e., every tree has only a single branch),Lemma 13 is not at all obvious, and both concerns (a) and (b) apply. Indeed, for Markov
chains, Courcoubetis and Yannakakis prove a statement related to Lemma 13, namely [11,Proposition 4.1.4], with a proof related to ours and dealing explicitly with concern (b) above.
For the special case of transition systems (i.e., the BP generates exactly one tree), Lemma 13
is simple though: consider the branch that follows a cycle around (f, Xf ). For the generalcase, we need a result on BPs from [8], dealing with concern (a) above. The high-level
principle behind the proof of Lemma 13 is often used in the analysis of Markov chains: if it
is possible, infinitely often, to reach a state with a probability bounded away from 0, thenthis state is almost surely reached infinitely often. See [24] for a full proof of Lemma 13.
We can now derive a PSPACE procedure for the problem P(coNBA) = 1 without resortingto DPAs:▶ Theorem 14. The problem P(coNBA) = 1 is PSPACE-complete.
Theorem 11 (for NBAs) has a coNBA-analogue:▶ Theorem 15. The problem P(coNBA) = 0 is EXPTIME-complete. It is EXPTIME-hardeven for NBAs all whose states are accepting.

5

Co-Unambiguous Büchi Automata

In this section we build on the previous section, in particular on Lemma 13, to derive ourmain technical result: given a BP B and an unambiguous Büchi automaton (UBA) A, one
can decide in NC whether B almost surely generates a tree all whose branches are rejected
by A:▶ Proposition 16. The problem P(coUBA) = 1 is in NC.
The rest of the section is devoted to the proof of this theorem. Fix a BP B and a UBA A.
Since NC is closed under complement, we can focus on the problem whether the probability is
positive that a B-tree has some branch accepted by A. We use Lemma 12. Since reachability
in a graph is in NL and, hence, in NC, it suffices to decide in NC whether the probability
that some branch of a B[Xf ]-tree is accepted by A[f, Xf ] is positive. By Lemma 13 it suffices
to decide in NC whether the probability that some branch of a Bdet -tree does not have any
nodes of type ∅ is positive. The challenge is that Bdet may be exponentially larger than A,
so we need to exploit the unambiguousness of A and the regular structure it gives to Bdet .
′′Let Bdet
be the BP (with ε-rules allowed) obtained from Bdet by removing the type ∅and eliminating all occurrences of type ∅ from all right-hand sides. The probability that a′′
Bdet -tree has an infinite branch of non-∅ nodes is equal to the probability that a Bdet
-tree isinfinite. Hence, it remains to show that one can decide in NC whether the probability that a′′
Bdet-tree is infinite is positive.
Define a matrix M ∈ QQ[f,Xf ]×Q[f,Xf ] whose rows and columns are indexed with thenon-q̄0 states of A[f, Xf ]: XYp|u|Y if (q, X) −→ (r, Y ) in A[f, Xf ]pM(q,X),(r,Y ) := X ,−→u0otherwise ,where |u|Y ∈ N0 is the number of occurrences of Y in u. (Think of M(q,X),(r,Y ) as the
expected number of (r, Y )-“successors” of (q, X).) The graph of M is equal to the transition
graph of A[f, Xf ] (excluding q̄0 ), which is strongly connected.

S. Kiefer, P. Semukhin, and C. Widdershoven

6:13

Z

Z

1
2
Say that A[f, Xf ] has proper branching if there exist (q, Y ) −−→(r1 , Z1 ) and (q, Y ) −−→p(r2 , Z2 ) in A[f, Xf ] and a rule Y ,−→ u1 Z1 u2 Z2 u3 in B with u1 , u2 , u3 ∈ Γ∗ . Now we canstate the key lemma:′′-tree is infinite▶ Lemma 17. Let ρ be the spectral radius of M . The probability that a Bdet
is positive if and only if either ρ > 1 or ρ = 1 and A[f, Xf ] does not have proper branching.

Observe the similarity between Lemmas 5 and 17. In fact, the proof of Lemma 17,
given below, is based on Lemma 5. Lemma 17 shows that properties of A[f, Xf ] and M′′(which are polynomial-sized objects) determine a property of the exponential-sized BP Bdet.
Unambiguousness of A[f, Xf ] is crucial for that connection.
Given that Lemma 17 reflects the key insight of this section (if not of this paper), let
us comment further. Suppose A[f, Xf ] has two outgoing transitions in a state (q, Y ), say
Z

Z

1
2
(q, Y ) −−→(r1 , Z1 ) and (q, Y ) −−→(r2 , Z2 ). This branching could be “proper branching” asdefined before Lemma 17, or the original UBA A could be nondeterministic when reading YYY
in q and have transitions q −→ r1 and q −→ r2 . Either type of branching causes non-0 entries
in the matrix M and, intuitively, increases its spectral radius ρ. Lemma 17 tells us that′′the probability that a Bdet
-tree is infinite is governed by the combined effect on ρ of both′′types of branching: if ρ > 1 then a Bdet
-tree is infinite with positive probability; only in theborderline case, ρ = 1, the type of branching matters. Again, this characterization is only
correct if the nondeterminism in A does not cause ambiguousness.
Let us consider what Lemma 17 states for the special case of Markov chains. In that case,clearly there is no proper branching. One can show, using unambiguousness, that for Markov
chains the spectral radius ρ of the matrix M is at most 1. Hence, Lemma 17 states for′′Markov chains that the probability that a Bdet
-tree (consisting of a single branch) is infinite
is positive if and only if ρ = 1. Indeed, a related statement can be found in [2, Lemma 6].
To finish the proof of Proposition 16 it suffices to show that we can check the conditionsof Lemma 17 in NC. Indeed, for comparing the spectral radius with 1, we employ Lemma 3.
One can check for proper branching in logarithmic space, hence in NC. This completes theproof of Proposition 16.

6

LTL

With Proposition 16 from the previous section, we can now show our headline result:▶ Theorem 18. The problem P(LTL) = 1 is PSPACE-complete.
Proof. PSPACE-hardness is immediate in two different ways. It follows both from the
PSPACE-hardness of model checking Markov chains against LTL and from the PSPACEhardness of model checking transition systems against LTL [31]. Both model-checking
problems are special cases of P(LTL) = 1.
Towards membership in PSPACE, there is a classical PSPACE procedure that translates
an LTL formula into an (exponential-sized) Büchi automaton [37]. As noted by several authors(e.g., [12, 7]), this procedure can easily be adapted to ensure that the Büchi automaton be a
UBA. By applying this translation to the negation ¬φ of the input formula φ, we obtaina UBA that rejects exactly those words that satisfy φ. By Proposition 16 the problem
P(coUBA) = 1 is in NC. By Lemma 2 it follows that P(LTL) = 1 is in PSPACE.
◀
Finally we show the following result, exhibiting a big complexity gap between the problems
P(LTL) = 1 and P(LTL) = 0.

CONCUR 2021

6:14

Linear-Time Model Checking Branching Processes▶ Theorem 19. The problem P(LTL) = 0 is 2EXPTIME-complete.
Proof. For membership in 2EXPTIME, we use again the classical procedure that translates
an LTL formula into an exponential-sized Büchi automaton [37] and then invoke Theorem 11.
For 2EXPTIME-hardness we adapt the reduction from [11, Theorem 3.2.1] for MDPs.
The details are in [24].
◀

7

Conclusions

We have devised a PSPACE procedure for P(LTL) = 1, i.e., qualitative LTL model checkingof BPs. The best previously known procedure ran in 2EXPTIME [8]. Since BPs naturally
generalize both transition systems and Markov chains (for both of which LTL model checking
is PSPACE-complete), one might view our model-checking algorithm as an optimal generalprocedure. The same holds for NBA-specifications instead of LTL.
The main technical ingredients have been the automata-theoretic approach and thealgorithmic analysis of UBAs, nonnegative matrices, and finiteness of BPs. Our proofs were
inspired by the observation that the spectral radii of certain nonnegative matrices are central
to model checking Markov chains against UBAs, and also determine fundamental properties
of BPs. Very loosely speaking, when model checking Markov chains against UBAs, thespectral radius measures the amount of nondeterministic branching in the UBA, whereas
when analyzing BPs, the spectral radius measures the amount of tree branching. The “generalcase”, i.e., model checking BPs, features both kinds of branching. Serendipitously, an analysisof spectral radii still leads, as we have seen, to optimal algorithms.
We have also established the complexities of related problems, partially as a tool for thementioned LTL and NBA problems and partially to map out the landscape. We have shownthat the P(·) = 0 variants are more complex than their P(·) = 1 counterparts. An intuitive
explanation of this phenomenon is that for an instance of an P(·) = 1 problems to be negative,
tree branching and probabilistic branching “work together” to falsify the specification onsome branch. In contrast, for P(·) = 0 problems, tree branching and probabilistic branchingare “adversaries”, like in MDPs. Indeed, for lower bounds on P(·) = 0 problems we haveencoded alternation in various forms.
One might ask about the complexity of P(UBA) = 1. Indeed, in trying to solve P(LTL) = 1
efficiently, the authors set out to solve P(UBA) = 1 efficiently (perhaps in P or even NC),
with the PSPACE transduction from LTL to UBA in mind. However, the complexity of UBA
universality is an open problem [30]; only membership in PSPACE is known. So even for the
1

1

fixed transition system with a ,−→ ab and b ,−→ ab the problem P(UBA) = 1 cannot be placedin P without improving the complexity of UBA universality. A PSPACE-hardness proof ofP(UBA) = 1 might have to make use of both types of branching in BPs, as P(UBA) = 1 isin NC for Markov chains [2].
Model checking BPs quantitatively, i.e., computing the satisfaction probability, comparing
it with a threshold, or approximating it, is left for future work. Exact versions of these
problems are computationally complex, as they are at least as hard as the corresponding
P(·) = 0 problem. The paper [8] describes, for DPAs, nonlinear equation systems whose least
nonnegative solution characterizes the satisfaction probabilities. Newton’s method is efficient
for approximating the solution of such equation systems; see [33, 15].

S. Kiefer, P. Semukhin, and C. Widdershoven

6:15

References
1
2

3
4
5
6

7

8

9
10

11
12

13

14

15

16

17

18
19

K.B. Athreya and P.E. Ney. Branching Processes. Springer, 1972.
C. Baier, S. Kiefer, J. Klein, S. Klüppelholz, D. Müller, and J. Worrell. Markov chains
and unambiguous Büchi automata. In Proceedings of the 28th International Conference on
Computer Aided Verification (CAV), volume 9779 of LNCS, pages 23–42, 2016.
A. Berman and R.J. Plemmons. Nonnegative matrices in the mathematical sciences. SIAM,
1994.
A. Borodin. On relating time and space to size and depth. SIAM Journal of Computing,
6(4):733–744, 1977. doi:10.1137/0206054.
A. Borodin, J. von zur Gathen, and J.E. Hopcroft. Fast parallel matrix and GCD computations.
Information and Control, 52(3):241–256, 1982. doi:10.1016/S0019-9958(82)90766-5.
D. Bustan, S. Rubin, and M.Y. Vardi. Verifying omega-regular properties of Markov chains.
In Computer Aided Verification (CAV), volume 3114 of Lecture Notes in Computer Science,
pages 189–201. Springer, 2004.
S. Chakraborty and J.-P. Katoen. Parametric LTL on Markov chains. In 8th IFIP TC 1/WG
2.2 International Conference on Theoretical Computer Science, volume 8705 of Lecture Notes
in Computer Science, pages 207–221. Springer, 2014.
T. Chen, K. Dräger, and S. Kiefer. Model checking stochastic branching processes. In
Mathematical Foundations of Computer Science (MFCS), volume 7464 of Lecture Notes in
Computer Science, pages 271–282. Springer, 2012.
R. Cleaveland, S.P. Iyer, and M. Narasimha. Probabilistic temporal logics via the modal
mu-calculus. Theoretical Computer Science, 342(2-3):316–350, 2005.
C. Courcoubetis and M. Yannakakis. Verifying temporal properties of finite-state probabilistic
programs. In Symposium on Foundations of Computer Science (FOCS), pages 338–345. IEEE
Computer Society, 1988.
C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. Journal of
the ACM, 42(4):857–907, 1995.
J.-M. Couvreur, N. Saheb, and G. Sutre. An optimal automata approach to LTL model
checking of probabilistic systems. In International Conference on Logic for Programming
Artificial Intelligence and Reasoning (LPAR), volume 2850 of Lecture Notes in Computer
Science, pages 361–375. Springer, 2003.
J. Esparza, A. Gaiser, and S. Kiefer. A strongly polynomial algorithm for criticality of branchingprocesses and consistency of stochastic context-free grammars. Information Processing Letters,
113(10-11):381–385, 2013.
K. Etessami, E. Martinov, A. Stewart, and M. Yannakakis. Reachability for branchingconcurrent stochastic games. In International Colloquium on Automata, Languages, andProgramming (ICALP), volume 132 of LIPIcs, pages 115:1–115:14. Schloss Dagstuhl - LeibnizZentrum für Informatik, 2019.
K. Etessami, A. Stewart, and M. Yannakakis. A polynomial time algorithm for computing
extinction probabilities of multitype branching processes. SIAM Journal of Computing,46(5):1515–1553, 2017.
K. Etessami, A. Stewart, and M. Yannakakis. Greatest fixed points of probabilistic min/max
polynomial equations, and reachability for branching Markov decision processes. Information
and Computation, 261:355–382, 2018.
K. Etessami, A. Stewart, and M. Yannakakis. Polynomial time algorithms for branching Markov
decision processes and probabilistic min(max) polynomial Bellman equations. Mathematics ofOperations Research, 45(1):34–62, 2020.
K. Etessami and M. Yannakakis. Recursive Markov chains, stochastic grammars, and monotone
systems of nonlinear equations. Journal of the ACM, 56(1):1:1–1:66, 2009.
K. Etessami and M. Yannakakis. Model checking of recursive probabilistic systems. ACM
Transactions on Computational Logic, 13(2):12:1–12:40, 2012. doi:10.1145/2159531.2159534.

CONCUR 2021

6:16

Linear-Time Model Checking Branching Processes

20
21

22
23
24
25

26

27

28
29
30

31
32

33

34

35

36

37

T. Gogacz, H. Michalewski, M. Mio, and M. Skrzypczak. Measure properties of regular sets oftrees. Information and Computation, 256:108–130, 2017.
A. Gorlin and C.R. Ramakrishnan. Separable GPL: decidable model checking with more
non-determinism. In International Conference on Concurrency Theory (CONCUR), volume
118 of LIPIcs, pages 36:1–36:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.
P. Haccou, P. Jagers, and V.A. Vatutin. Branching Processes: Variation, Growth, andExtinction of Populations. Cambridge University Press, 2005.
T.E. Harris. The Theory of Branching Processes. Springer, 1963.
S. Kiefer, P. Semukhin, and C. Widdershoven. Linear-time model checking branching processes.
Technical report, arxiv.org, 2021. Available at arXiv:2107.01687.
O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy theirlinear specification. In Principles of Programming Languages (POPL), pages 97–107. ACM
Press, 1985.
H. Michalewski and M. Mio. On the problem of computing the probability of regular sets oftrees. In Foundation of Software Technology and Theoretical Computer Science (FSTTCS),
volume 45 of LIPIcs, pages 489–502. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015.
D. Niwiński, M. Przybyłko, and M. Skrzypczak. Computing measures of weak-MSO definable
sets of trees. In International Colloquium on Automata, Languages, and Programming (ICALP),
volume 168 of LIPIcs, pages 136:1–136:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2020.
C.M. Papadimitriou. Computational complexity. Addison-Wesley, 1994.
N. Piterman. From nondeterministic Büchi and Streett automata to deterministic parity
automata. Logical Methods Computer Science, 3(3), 2007. doi:10.2168/LMCS-3(3:5)2007.
A. Rabinovich. Complementation of finitely ambiguous Büchi automata. In Developments in
Language Theory (DLT), volume 11088 of Lecture Notes in Computer Science, pages 541–552.
Springer, 2018.
A.P Sistla and E.M. Clarke. The complexity of propositional linear temporal logics. Journalof the ACM, 32(3):733–749, 1985. doi:10.1145/3828.3837.
A.P. Sistla, M.Y. Vardi, and P. Wolper. The complementation problem for Büchi automata
with appplications to temporal logic. Theoretical Computer Science, 49:217–237, 1987. doi:
10.1016/0304-3975(87)90008-9.
A. Stewart, K. Etessami, and M. Yannakakis. Upper bounds for Newton’s method on monotonepolynomial systems, and P-time model checking of probabilistic one-counter automata. Journalof the ACM, 62(4):30:1–30:33, 2015.
W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of TheoreticalComputer Science (Vol. B): Formal Models and Semantics, chapter 4, pages 133–191. MIT
Press, 1990.
M.Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In
Proceedings of the 26th Annual Symposium on Foundations of Computer Science (FOCS),
pages 327–338. IEEE Computer Society, 1985. doi:10.1109/SFCS.1985.12.
M.Y. Vardi. Probabilistic linear-time model checking: An overview of the automata-theoretic
approach. In Formal Methods for Real-Time and Probabilistic Systems, pages 265–276. Springer,
1999.
M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification(preliminary report). In 1st Symposium on Logic in Computer Science (LICS), pages 332–344.
IEEE Computer Society Press, 1986.