314
E. M. Hahn et al.
{0, 1}
{1}
∅
{0}
∅
{0, 1}
∅
{0, 1}
{0}
a, b
a , b
a, b
a , b
a
a, b
a
b
a, b
a, b
0
1
a, b
a, b
a
Fig. 2. An NBA for G F a (in the upper right corner) together with an SLDBA and a slim NBA
constructed from it. The SLDBA and the slim NBA are shown sharing their common part.
State {0, 1}, produced by the subset construction, is the initial state of the SLDBA, while state
({0, 1}, ∅)—the initial state of the breakpoint construction—is the initial state of the slim NBA.
States ({1}, ∅) and ({0}, ∅) are states of the breakpoint construction that only belong to the
SLDBA because they are not reachable from ({0, 1}, ∅). The transitions out of {0, 1}, except the
self loop, belong to Δ SB . The dashed-line transition from ({0, 1}, {0}) belongs to γ2,1
(1) may only happen after a transition from γ 2,1 has been taken, and the q l is not
among the states that is traced henceforth. (2) identifies parts of the run tree that do not
contain an accepting transition.
A node labeled with q l on level l that is not an endpoint has
δ S (q l , σ l )
children,
labeled with the different elements of δ S (q l , σ l ). It is now easy to show by induction
over i that the following holds.
1. For all q ∈ Q i , there is a node on level i labeled with q.
2. For i /
∈ I and q ∈ Q
i , there is a node labeled q on level i, a j with pred(i) ≤ j < i,
and ancestors on level j and j +1 labeled q j and q j+1 , such that (q j , σ j , q j+1 ) ∈ Γ .
(The ‘ancestor’ on level j + 1 might be the state itself.)
For i ∈ I and q ∈ Q
i , there is a node labeled q on level i, which is not an end point.
Consequently, the forest is infinite, finitely branching, and finitely rooted, and thus contains an infinite path. By construction, this path is an accepting run of B.
The resulting automata are simple in structure and enable symbolic implementation
(See Fig. 2). It cannot be expected that there are much smaller good for MDP automata,
as its explicit construction is the only non-polynomial part in model checking MDPs.
Theorem 3. Constructing a GFM B¨ uchi automaton G that recognizes the models of an
LTL formula ϕ requires time doubly exponential in ϕ, and constructing a GFM B¨ uchi
automaton G that recognizes the language of an NBA B requires time exponential in B.
Proof. As resulting automata are GFM, they can be used to model check MDPs M
against this property, with cost polynomial in product of M and G. If G could be produced faster (and if they could, consequently be smaller) than claimed, it will contradict
the 2-EXPTIME- and EXPTIME-hardness [4] of these model checking problems.
E. M. Hahn et al.
{0, 1}
{1}
∅
{0}
∅
{0, 1}
∅
{0, 1}
{0}
a, b
a , b
a, b
a , b
a
a, b
a
b
a, b
a, b
0
1
a, b
a, b
a
Fig. 2. An NBA for G F a (in the upper right corner) together with an SLDBA and a slim NBA
constructed from it. The SLDBA and the slim NBA are shown sharing their common part.
State {0, 1}, produced by the subset construction, is the initial state of the SLDBA, while state
({0, 1}, ∅)—the initial state of the breakpoint construction—is the initial state of the slim NBA.
States ({1}, ∅) and ({0}, ∅) are states of the breakpoint construction that only belong to the
SLDBA because they are not reachable from ({0, 1}, ∅). The transitions out of {0, 1}, except the
self loop, belong to Δ SB . The dashed-line transition from ({0, 1}, {0}) belongs to γ2,1
(1) may only happen after a transition from γ 2,1 has been taken, and the q l is not
among the states that is traced henceforth. (2) identifies parts of the run tree that do not
contain an accepting transition.
A node labeled with q l on level l that is not an endpoint has
δ S (q l , σ l )
children,
labeled with the different elements of δ S (q l , σ l ). It is now easy to show by induction
over i that the following holds.
1. For all q ∈ Q i , there is a node on level i labeled with q.
2. For i /
∈ I and q ∈ Q
i , there is a node labeled q on level i, a j with pred(i) ≤ j < i,
and ancestors on level j and j +1 labeled q j and q j+1 , such that (q j , σ j , q j+1 ) ∈ Γ .
(The ‘ancestor’ on level j + 1 might be the state itself.)
For i ∈ I and q ∈ Q
i , there is a node labeled q on level i, which is not an end point.
Consequently, the forest is infinite, finitely branching, and finitely rooted, and thus contains an infinite path. By construction, this path is an accepting run of B.
The resulting automata are simple in structure and enable symbolic implementation
(See Fig. 2). It cannot be expected that there are much smaller good for MDP automata,
as its explicit construction is the only non-polynomial part in model checking MDPs.
Theorem 3. Constructing a GFM B¨ uchi automaton G that recognizes the models of an
LTL formula ϕ requires time doubly exponential in ϕ, and constructing a GFM B¨ uchi
automaton G that recognizes the language of an NBA B requires time exponential in B.
Proof. As resulting automata are GFM, they can be used to model check MDPs M
against this property, with cost polynomial in product of M and G. If G could be produced faster (and if they could, consequently be smaller) than claimed, it will contradict
the 2-EXPTIME- and EXPTIME-hardness [4] of these model checking problems.