M A S A R Y K U N I V E R S I T Y
F A C U L T Y O F I N F O R M A T I C S
Linear Temporal Logic
and o;-automata
P H D T H E S I S P R O P O S A L
František Blahoudek
B r n o , J a n u a r y 2015
Supervisor: doc. R N D r . Jan Strejček, P h . D .
Contents
1 Introduction 3
2 Preliminaries 9
2.1 Linear temporal logic (LTL) 9
2.2 omega-automata 10
3 Translations to Deterministic Automata - State of the Art . . . . 13
3.1 Determinization of Buchi automata 14
3.1.1 Implementations of Safra's determinization 17
3.1.2 Determinization of an N B A subclass 18
3.2 Direct translations of L T L to deterministic automata 19
3.2.1 Simple fragments 19
3.2.2 M o r e complex fragments 20
3.2.3 Full L T L 21
4 Achieved Results 23
4.1 Translation of LTL(Fs,Gs) 23
4.2 Comparison of L T L to deterministic automata translators. . 27
4.3 Other publications and research 28
5 Aims of the Thesis 31
5.1 Generalization of Safra's Construction 31
5.2 Extension of L T L 3 D R A to Process Full L T L 31
5.3 Expected Results and Schedule 32
Bibliography 35
Summary / Shrnuti 41
A Publications 43
1
1 Introduction
Linear temporal logic (LTL) was first introduced b y Pnueli i n 1977 [41].
Over the years it became a popular formalism for specification of infinite
behaviour of reactive systems. U s i n g L T L is convenient for t w o reasons.
First, it is relatively close to the natural language. Second, as the name
suggests, L T L allows to reason about temporal properties of single (nonbranching,
linear) runs of systems. Temporal logics w i t h branching-time
like C T L (Computational Tree Logic) a n d its extension C T L * were introduced
b y Clarke a n d Emerson i n 1981 [14]. Branching-time logics also express
various temporal properties. U n l i k e L T L , they reason about whole
computational trees of the systems.
Temporal logics have various applications. In this thesis proposal w e
focus o n L T L and its applications i n the following areas of formal methods:
• model checking, discussed i n detail i n [15, 6],
• controller synthesis for reactive systems, see [42,28].
Formal verification i n general is a task to prove that some system <S is
correct w i t h respect to its specification ip. The qualitative L T L m o d e l checking
is one approach to automated verification a n d b u g finding. It has t w o
inputs:
• m o d e l M of a system S, a n d
• specification of S given b y an L T L formula ip.
The model M. should represent the set of all relevant behaviours (runs) of S,
if expresses desired properties of runs of M.. A m o d e l checker investigates
whether all runs of M. satisfy ip, i.e. M. \= ip, or not. If some r u n a of M.
violates the specification, it is a possible b u g i n the system design a n d a is
returned as a counterexample.
Systems under consideration can also exhibit probabilistic behaviour,
such as non-deterministic failure of systems components, delays, uncertain
environment, randomized algorithms etc. We call these systems probabilistic.
Probabilistic systems can be modelled as M a r k o v chains [39] or M a r k o v
decision processes [44]. Qualitative L T L model checking of probabilistic
models answers questions like: "Is the probability that a run of M satisfies
tp at least (at most) 90%?".
Reactive systems usually w o r k i n some non-deterministic environment.
Actions of the environment are inputs of the systems. A reactive system has
3
1. I N T R O D U C T I O N
predefined a set of possible reactions (outputs) and it reacts by some of its
output to every input received. The reaction of the system is driven by its
controller. The problem of controller synthesis w i t h L T L specification [43]
is a task to produce a system controller automatically from the specification
of desired system properties given by an L T L formula ip. The controller
Cp drives the system i n a w a y that ip is always satisfied, no matter h o w
the environment behaves. The controller is correct-by-construction w i t h respect
to (p and guarantees ip. Some formulae cannot be guaranteed by any
controller. We call them not realizable.
Both model-checking and controller synthesis problems can be solved
using automata over infinite words, also called LO-automata. For simplicity,
we use the words automaton and w-automaton synonymously i n further
text. Each automaton A a n d each L T L formula ip define an w-language (a
set of infinite words), denoted as L(A) (all words accepted b y A) and L{ip)
(all words satisfying ip). The L T L formulae are convenient to write for users,
the automata are typically more suitable for algorithms. If L(A) = L{ip), w e
say that A is equivalent to ip or that A is an automaton for ip a n d w e often
denote it as A^. The construction of an equivalent automaton A^ for a form
u l a ip is called translation of ip. Automatic translation of L T L to automata
allow us to exploit advantages of both formalisms. For simplicity, instead
of translation of LTL w e use the w o r d translation alone i n further text.
The automata-theoretic approach to explicit model checking of L T L [51]
uses an automaton A-«p to recognize all behaviours (not necessarily of M)
system requirements
L T L formula ip
Does M \= ip?
model checker
automatonm o d e l M
* analysis of M x A^
+
counterexample
verified
Figure 1.1: Automata-theoretic approach to model-checking.
4
1. I N T R O D U C T I O N
system
LTL formula ip
w i n n i n g
strategy
ip not realizable
deterministic
automaton Avspecification
controller C <
LTL formula ip
w i n n i n g
strategy
ip not realizable
deterministic
automaton Avspecification
controller C <
LTL formula ip
w i n n i n g
strategy
ip not realizable
LTL formula ip
w i n n i n g
strategy
ip not realizable
two-player
game
Figure 1.2: Controller synthesis via games.
violating the specification ip, see Figure 1.1. Non-deterministic automata
are sufficient for qualitative model checking of non-probabilistic systems
(implemented for example i n Spin [22], L T S m i n [32], or D i V i n E [7]), while
quantitative model checking of probabilistic systems use deterministic au-
tomata1
(implemented for example i n P R I S M [31] or L i Q u o r [13]).
The problem of controller synthesis for reactive systems can be reduced
to a finite-state game of two players:
• the environment - generates inputs, and
• the system - reacts to inputs by performing some actions (outputs).
The game can be created from deterministic automaton Atp, as depicted
in Figure 1.2. A w i n n i n g strategy (if exists) for the player system is then
simply transformed into the controller C. If there is no w i n n i n g strategy for
system, the formula is not realizable and no correct controller exists.
Translation of L T L to automata is a part of both model checking and
controller synthesis procedures. The translation affects the amount of w o r k
performed i n the next steps of the procedures. The number of states and
transitions of the automaton used has usually a direct impact o n the size
of product M x A-«p analysed during m o d e l checking and o n the size of
the game during controller synthesis. Therefore, size of the automata after
translation have an direct impact o n the time and memory needed for
model checking and controller synthesis.
Unlike automata over finite words, w-automata may use one of various
types of accepting conditions. A n accepting condition of an automaton declares
w h e n a r u n of the automaton is accepting. The simplest and most
commonly used accepting condition is Biichi. The Biichi accepting condition
for an automaton A w i t h a set of states Q is specified by a set of states
1. In fact, unambigous automata suffice.
5
1. I N T R O D U C T I O N
F C Q called accepting states. A r u n a of A is accepting b y the Biichi condition
F if a visits states from F infinitely often.
Each L T L formula can be translated to a non-deterministic Biichi automaton
(NBA). Unfortunately deterministic Biichi automata (DBA) are
less expressive than the class of N B A a n d there is no equivalent D B A for
some L T L formulae, such as FGa. Therefore, one has to use more complex
accepting condition for translation of L T L to deterministic automata. The
traditional choice of accepting condition for deterministic automata is Rabin
or parity. Recent research started b y Esparza and Křetínský i n 2012 [26]
showed that a novel generalized Rabin condition is also applicable for the
translation to deterministic automata.
The translation of L T L to N B A underwent a n extensive research i n the
last t w o decades a n d tools such as L T L 3 B A [5] a n d S P O T [18] w h i c h are
highly optimized to produce small automata were developed. The complexity
of the translations is exponential i n the number of states w i t h respect
to the size of the translated formula.
The translation to deterministic automata is more complicated for several
reasons.
• The Biichi accepting condition is not applicable i n general and there is
variety of other possible accepting conditions one may use for the deterministic
automaton. The other accepting conditions are more complex
and cannot be specified simply as a set of states. Each type of accepting
condition has advantages and disadvantages. Automata w i t h
more complex condition can be more succinct (it may have less states
and/or transitions), but o n the other hand the algorithms that w o r k
w i t h them have usually higher complexity.
• The lower b o u n d for the number of states of a deterministic Biichi
or Rabin automaton equivalent to a n L T L formula tp is 2 2
° ( l v l )
[29].
The lower b o u n d shows a strong distinction from translation to nondeterministic
Biichi automata w i t h an upper b o u n d of \<p\ • 2^1
• Determinization of N B A is not so straightforward as i n the case of
automata over finite words. One has to use some variant of constructions
of Safra [46] or M u l l e r and Schupp [38] (discussed i n Section 3.1
i n more detail). A l l k n o w n determinization constructions are considered
complicated and difficult to implement. Indeed, they all involve
a b l o w ­ u p i n states i n order of 0(nn
).
Despite the fact that determinization of N B A is complicated a n d brings
large b l o w ­ u p i n the number of states, the traditional approach to trans­
6
1. I N T R O D U C T I O N
lation of (p to deterministic automata uses translation of (p to N B A w i t h
subsequent determinization. In 2012 Kfetinsky and Esparza introduced a
novel generalized Rabin condition and presented an elegant direct translation
to deterministic automata for a significant L T L fragment [26]. They
proved by this translation that direct translations are feasible and competitive
to the traditional approach. In the next year, Chatterjee et al. showed
that generalized Rabin condition is very suitable not only for the translation
but also for controller synthesis and qualitative model checking [12].
The new accepting condition brought a fresh air into research of L T L to deterministic
automata translators. Some new efficient algorithms for direct
translations were proposed and implemented. However, our experiments
from 2013 show that one can still produce smaller automata than those produced
by then-available translators for some formulae [10].
Better translation to deterministic automata can significantly improve
quantitative model checking of probabilistic systems and controller synthesis.
Therefore, the thesis proposal is dedicated to translations of L T L to
deterministic automata. The thesis I a m about to propose o n the following
pages should contribute there by two results.
1. Generalization of Safra's determinization procedure. Both L T L to
N B A translators mentioned above use transition-based generalized
B i i c h i 2
automata (TGBA) as an intermediate step i n the translation.
Both model checking and controller synthesis perform w e l l w i t h succinct
but complex generalized Rabin accepting condition. Therefore,
a determinization construction w h i c h takes a T G B A as input and outputs
(possibly transition-based) deterministic automaton w i t h generalized
Rabin accepting condition seems promising.
2. A n efficient translation of LTL to deterministic automata via alternating
automata. We already presented a determinization-free translation
of an L T L fragment to transition-based generalized deterministic
Rabin automata ( T G D R A ) i n 2013 [3] and implement it i n our tool
L T L 3 D R A [10]. O u r translation uses a subclass of very weak alternating
automata as an intermediate step. We plan to extend our approach
to the full L T L .
The thesis proposal is organized as follows: the next chapter introduces
the L T L and automata and fixes the notation used through the text. C h a p ter
3 is divided i n two sections. Section 3.2 presents the state of the art i n the
2. The accepting condition is specified by multiple sets of accepting transitions.
7
1. I N T R O D U C T I O N
area of direct translation L T L to deterministic automata, followed by Section
3.1 w i t h state of the art i n determinization of non-deterministic Biichi
automata. In Chapter 4 we give a brief overview of our already published
results and Chapter 5 presents the aims of the thesis and our research plan.
Finally i n A p p e n d i x A we attach to the text of this thesis proposal some of
our already published work.
8
2 Preliminaries
This chapter recalls basic definitions and notions of the linear temporal
logic (LTL) and w-automata. We use where S is a set to denote the set of
all finite sequences of elements of S.
2.1 Linear temporal logic (LTL)
The syntax of L T L is defined by
p ::= tt | a | —><p \ ipVip \ pAp \ Xp \ ipdip,
where tt stands for frue, a ranges over a countable set AP of atomic propositions,
X and U are temporal operators called nexf and until, respectively.
A n alphabet is a finite set E = 2 A P
, where AP' is a finite subset of AP.
A n co-word (or simply a word) over E is an infinite sequence of letters
u = UQU\U2 • • • € E w
. We denote the suffix UiUi+\Ui+2 . . . of tt b y itj...
We inductively define w h e n a w o r d u satisfies a formula ip, written u \=
ip, as follows.
u \= tt
u \= a iff a £ tto
u \= -up iff u Y= ip
u \= ipi V ipi iff u \= ipi or u \= ip2
u \= ipi A ip2 iff u \= pi and u \= ip2
u \= Xip iff u\.. \= p>
u \= ipi U ip2 iff 3i > 0 . (Ui.. |= ip2 and VO < j < i. Uj.. \= ipi)
G i v e n an alphabet E , a formula p defines the language £E
(<£>) = {u G
E w
| u \= p>} of words that satisfy <p. We write L{p) instead of {ip),
where AP(p) denotes the set of atomic propositions occurring i n the formula
p.
We extend L T L w i t h derived temporal operators:
• Ftp called eventually and equivalent to tt U p
• Gip called always and equivalent to -iF-np
• Fs(p called strict eventually and equivalent to XFp
• Gsp called strict always and equivalent to XGp
• ip Rip called release and equivalent to -'(-•</? U -<ip)
9
2. P R E L I M I N A R I E S
2.2 w-automata
Definition 1. A {non-deterministic) semiautomaton is a tuple T = (S, E , <5, s/),
w/zere 5 is a finite set of states, E is an alphabet, si G S is the initial state, and
5CSxT,xSisa transition relation. A triple (s,a,s') G Sis called a transition
from s to s' labelled by a.
Definition 2. A r u n of a semiautomaton T over a word u = uoui... G E w
is an infinite sequence a = (so,uo,si)(si,ui,S2) ••• G 5^ of transitions such
that so = si. By Infs(a) and Inft(a) we denote the set of recurring states and
transitions, i.e. states and transitions occurring infinitely often in a.
The semiautomaton T is deterministic if for each s £ 5 and each a G E
there is at most one state s' such that (s,a,s') G 5. For each w o r d u G E w
, a
deterministic semiautomaton has at most one r u n over u.
Definition 3. An w-automaton is a tuple A= (S,T,,5, ST, A C C ) where the tuple
(S, E, 5, si) is a semiautomaton and Acc is an accepting condition. Runs of A
are runs of the semiautomaton. The accepting condition Acc specifies when a run
of A is accepting. We say that A accepts the word u G E w
if there is at least one
run of A that is accepting. The language of A is the set L(A) of all words accepted
by the automaton. In this thesis proposal we use the following accepting conditions.
Biichi (B) condition is given by a set B C S of states. A r u n a is accepting
if the set of recurring states Infs(a) intersects B, i.e. there is a state of
B visited infinitely often by a.
Generalized Biichi (GB) condition is given by a set Q C 2s
of sets of states.
A r u n a is accepting if for all sets G G Q we have G n Infs(a) / 0, i.e.
all the sets of Q are visited infinitely often by a.
Rabin (R) condition is given by a set 1Z C 2s
x 2s
of Rabin pairs. We say
that a r u n o satisfies a Rabin pair (K, L) G 1Z if Infs(a) D K = 0 and
Infs(a) n l / I, i.e. the states from K are visited only finitely many
times and some state from L is visited infinitely often by a. A r u n is
accepting if it satisfies some Rabin pair of TZ.
Generalized Rabin (GR) condition is given by a set QTZ C 2s
x 2 2 S
of
generalized Rabin pairs. A r u n a satisfies a generalized Rabin pair
(K, {Lj}j€j) G QTl if Infs(cr) n K = 0 and Infs(cr) n L7 - / 0 holds for
each j G J, i.e. the states from K are visited only finitely many times
and all sets Lj are visited infinitely often.
10
2. P R E L I M I N A R I E S
Parity (P) condition is given b y a partition V = {PQ, ..., Pk} of the set of
states S. For s G Pi w e say s have the priority i. A r u n a is accepting
if for some even i w e have Infs(a) n Pj / 0 a n d for all j < i w e
have Infs(a) n P j = 0, i.e. the lowest priority of states that are visited
infinitely often is even.
Please note that all conditions can be used i n transition-based setting,
where the set of states S is replaced b y the transition relation 5, and Infs is
replaced b y Inft i n the definitions.
The type of the automaton is determined b y the accepting condition
and the type of transition relation (non-deterministic, deterministic). We
use acronyms from {T, e} x {G,e} x {N,D,e} x {B,R,P} x {^4} to denote
automata types. The first two symbols are optional: T declares that
the accepting condition is transition-based, G indicates generalized accepting
condition. The next symbol stands for the branching mode: N for nondeterministic
a n d D for deterministic. W h e n not present, the automaton is
non-deterministic. B, R, or P specify the accepting condition and A stands
for automaton. For example, T G D R A abbreviates transition-based generalized
deterministic Rabin automata, whereas N B A , or simply B A , is n o n deterministic
Buchi automata.
11
3 Translations of LTL to Deterministic Automata - State
of the Art
Translating an L T L formula into an equivalent deterministic automaton is
a complex task and the resulting automaton is often very large. K u p f e r m a n
and Rosenberg proved that the lower b o u n d for the number of states of
an equivalent D B A or D R A is 2 2
° ™ [29] where n is the size of the translated
f o r m u l a 1
. This doubly exponential b l o w - u p i n the number of states
cannot be avoided. Some existing translations match this asymptotic lower
bound, but recent research showed that n e w translations can bring significant
improvement and produce smaller automata i n average. This is due
the constant hiding i n the 0{) notation i n the exponent w h i c h makes the
lower b o u n d benevolent.
Translations to non-deterministic automata usually use Biichi automata.
The simplicity of checking Biichi accepting condition makes using N B A i n
algorithms convenient. U n l i k e automata over finite words, the classes of
non-deterministic Biichi and deterministic Biichi automata do not have the
same expressive power. Namely, the class of deterministic Biichi automata
is strictly less expressive than the class of their non-deterministic counterpart.
E v e n though L T L is also strictly less expressive than the class of N B A ,
there are some L T L properties not expressible by D B A 2
(formulae for w h i c h
an equivalent D B A exists are called DBA-recognizable). Therefore, i n order
to translate L T L to deterministic automata w e have to choose more complex
accepting condition, typically Rabin or parity (Streett [50] or M u l l e r [37] can
be also used). H a n d l i n g more complex conditions is a natural challenge of
the area of translations to deterministic automata and using the automata
further i n model checking and controller synthesis.
We can classify approaches to translations of L T L to automata by the
w a y the transition graph of the resulting automaton is represented. We have
two types of translations:
Symbolic. A symbolic translation produces an automaton described i n logical
language.
Explicit. A n explicit translation produces an automaton described by sets
of states and transitions.
1. However, the precise lower bound for transition-based automata and automata with
generalized accepting conditions were not studied in their work.
2. In fact, LTL and the class of D B A are incomparable in expressiveness.
13
3. T R A N S L A T I O N S T O D E T E R M I N I S T I C A U T O M A T A - S T A T E O F T H E A R T
We focus o n explicit translations i n this thesis proposal so w e comment
on symbolic methods here only briefly. Automata symbolically represented
as Binary Decision Diagrams (BDDs) are stored i n logarithmic space w i t h
respect to the number of states. In 2012 Morgenstern and Schneider showed
a symbolic translation and presented its implementation [36]. They exploit
a translation of L T L to backward-deterministic Biichi automata and present
their determinization. Symbolically represented automata have typically
m u c h (often exponentially) more states than necessary. W h i l e deterministic
symbolically encoded automata were successfully used i n controller synthesis,
model checkers of probabilistic systems deal w i t h linear arithmetic
and thus do not benefit from the symbolic representation.
The rest of this chapter is dedicated to explicit translations so from n o w
on by the w o r d translation w e always mean an explicit translation. There
are two m a i n approaches to explicit translations to deterministic automata:
Determinization of N B A . A two-step translation w h i c h first constructs an
N B A equivalent to the translated formula and then applies some uni-
versal3
determinization procedure on that N B A .
Direct. A direct translation does not use any determinization of Biichi automata.
It rather constructs the automaton straight from the formula
or other intermediate formalism (it does not necessary proceed i n one
step).
In the following sections w e mention several tools without any reference.
The references and links can be found i n Table 3.1 at the end of this
chapter.
3.1 Determinization of Biichi automata
The traditional and w i d e l y used method for obtaining deterministic automata
for specification formulae (e.g. i n P R I S M [31]) proceeds i n two steps.
1. The formula <p is translated into an equivalent N B A
2. The N B A Mv is determinized using some universal procedure for determinization
of Biichi automata w h i c h results i n deterministic Au>.
3. Universal in the sense that it is correct for all Btichi automata.
14
3 . T R A N S L A T I O N S T O D E T E R M I N I S T I C A U T O M A T A - S T A T E O F T H E A R T
There are two m a i n advantages of this approach.
• It w o r k s for the full L T L because every L T L formula can be translated
into an N B A and the determinization procedures w o r k for all N B A .
• It naturally benefits from the progress i n translations of L T L to N B A .
In most cases, the smaller is the smaller Av after determinization
is.
In the w o r l d of finite words, powerset construction is an effective procedure
that takes a non-deterministic automaton w i t h n states and constructs
a deterministic automaton w i t h at most 2 n
states accepting the same language
[45]. This method is k n o w n to be tight and is w e l l understood.
a
N B A A for w o r d s w i t h D B A V for words
only finite number w i t h infinite number
of occurrences of a. of occurences of b.
Figure 3.1: The automata A and V demonstrate that the powerset construction
is not correct for w-automata. The automaton V is the result of powerset
construction applied on A. L(A) / L(V).
Unluckily, w h e n w e shift ourselves to the w o r l d of infinite words, the
powerset construction is no longer correct as w e demonstrate by Figure 3 . 1 .
G i v e n a non-deterministic Biichi automaton A, the powerset construction
produces a deterministic Biichi automaton V that does not recognize the
same language. In particular, w e have (ab)^ G L(V), but {ab)w
£ L(A),
thus L(A) / L(V). A s w e already discussed, deterministic Biichi automata
are not expressive enough; there is no D B A that recognizes L(A). We need
different accepting condition and apparently also more sophisticated construction
for determinization of Biichi automata.
First correct determinization procedure for Biichi automata was given
by M c N a u g h t o n i n 1 9 6 6 w h e n he showed a doubly exponential construction
w h i c h for a given N B A produces an equivalent deterministic M u l l e r
automaton [34]. Twelve years later Safra presented a singly exponential determinization
construction w h i c h for a given Biichi automaton w i t h n states
1 5
3 . T R A N S L A T I O N S T O D E T E R M I N I S T I C A U T O M A T A - S T A T E O F T H E A R T
produces a deterministic Rabin automaton w i t h at most 1 2 n
n 2 n
states and
2n Rabin pairs [46]. Another determinization procedure w h i c h results to
Rabin automata was proposed by M u l l e r and Schupp i n 1 9 9 5 [38] and is of
similar complexity as the one of Safra. The asymptotic complexity of both
translations match the lower b o u n d o n determinization given b y M i c h e l
in [35]. Detailed comparison and experimental evaluation of the singly exponential
methods of Safra [46] and M u l l e r & Shupp [38] can be found
in [1]. The authors of [1] conclude that the Safra's method usually yields
smaller automata.
The Safra's construction is the most w i d e l y k n o w n determinization procedure
for N B A . Safra's m a i n idea is to follow all possible runs of the N B A
by multiple sets of states organized i n a labelled tree. The labelled trees
form the set of states of the deterministic automaton. The number of nodes
in the tree is bounded and that is h o w Safra achieved the (only) singly exponential
b l o w - u p i n the number of states.
Even though Safra's construction is asymptotically optimal, some i m provements
were proposed. In 2 0 0 6 Piterman revisited the labelling convention
and introduced compact trees where the nodes change names (labels)
dynamically [40]. We can profit from dynamic labelling of nodes i n
two ways. First, w e gain a smaller upper b o u n d o n the automaton size
w h i c h is n o w 2 n n
n ! states and only n Rabin pairs (the original construction
of Safra can yield i n at most 2n Rabin pairs). Second, we can use a parity
acceptance condition w i t h 2n priorities4
.
Three years later Schewe proposed another modification of Safra's trees
called history trees [47]. History trees do not use any node labels (names),
the nodes are identified by their position i n the history tree instead. Further,
transition-based accepting mechanism is used for the deterministic Rabin
automaton. U s i n g transition-based automata, one may separate the acceptance
principle from states (trees) to transitions and store only the states of
the N B A i n w h i c h some r u n can be, i n the history trees (states of the T D R A )
as the only information needed. Removal of n a m i n g together w i t h using
transition-based automata can lower the number of states u p to (1.65n)n
,
but increases the potential number of Rabin pairs to 2 n
. In [49] Schewe and
Varghese naturally extend this approach to determinize generalized Biichi
automata.
Figure 3.2 illustrates the difference i n the n a m i n g conventions of the
three discussed variants of Safra's determinization. There is an N B A B and
4. Using deterministic parity automaton instead of Rabin allow us to solve controller synthesis
via parity games. Solving of parity games is much easier than solving Rabin games.
1 6
3 . T R A N S L A T I O N S T O D E T E R M I N I S T I C A U T O M A T A - S T A T E O F T H E A R T
S { 1 , 2 , 3 , 4 } C { 1 , 2 , 3 , 4 } H { 1 , 2 , 3 , 4 }
{ 2 , 3 } 5 { 4 } 3
{ 2
h
{ 2 , 3 } 2 { 4 } 4 { 2 , 3 } Q
{ 2 }
oo
Figure 3.2: A Biichi automaton B and three trees that serve as states i n deterministic
automata produced b y variants of Safra's construction and sequence
caca; the Safra's tree (S) of [46], the condensed tree (C) of [40], and
the history tree {%) of [47].
three different trees i n Figure 3.2. The trees emerged as states during determinization
of B; i n particular as states reachable after reading the sequence
caca. The Safra's tree S appeared during the original Safra's construction
[46], the condensed tree C shows u p during determinization b y
Piterman [40] a n d finally % is a history tree used b y the Schewe's variant
[47]. Note that both C and % also appear for sequence ca and thus can
be reused, while the original Safra's construction uses isomorphic tree w i t h
different node names for ca.
3.1.1 Implementations of Safra's determinization
There are only a few implementations of Safra's constructions, even less are
publicly available. A prominent implementation was made b y K l e i n i n his
master thesis [23] and is called l t l 2 d s t a r . Klein's tool serves for translation
of L T L to deterministic Rabin (or alternatively Streett) automata. It
does not implement any translation of L T L to N B A and rely o n external
translators instead. For a formula <p, l t l 2 d s t a r calls some specified translator
to get the N B A A/^ and then it performs Safra's construction and some
additional optimizations, see [24]. Due to the fact that l t l 2 d s t a r implements
standard interfaces of L T L to N B A translators, it can benefit from
1 7
3. T R A N S L A T I O N S T O D E T E R M I N I S T I C A U T O M A T A - S T A T E O F T H E A R T
development i n the area of L T L to N B A translators.
In 2013 w e made extensive experiments w i t h several kinds of benchmarks
i n order to compare various L T L to D R A translators [10]. In all our
experiments w e r u n l t l 2 d s t a r i n combination w i t h several L T L to N B A
translators (see Section 4.2 for details) i n order to investigate the impact of
the first step o n the resulting automaton). The experiments revealed that
the performance of l t l 2 d s t a r can be often largely i m p r o v e d w h e n w e
use m o d e r n L T L to N B A translators like L T L 3 B A or l t l 2 t g b a instead
of L T L 2 B A w h i c h is the default choice. Unfortunately the web pages of
l t l 2 d s t a r still recommend to use the o l d L T L 2 B A .
Unfortunately to our best knowledge, no implementations of the extensions
and optimizations proposed by Piterman and Schewe are publicly
available.
3.1.2 Determinization of an N B A subclass
Safra's construction (and l t l 2 d s t a r ) w o r k s for the whole class of N B A .
This universality is a clear advantage, but o n the other h a n d the price for
the universality is high - it is a complicated procedure and the automata
produced are often unnecessarily large. In this section w e discuss a construction
that exploits special properties of WDBA -recognizable languages.
The W D B A stands for a Weak Deterministic Biichi Automaton. A D B A
w i t h a set of states S and a set of accepting states B is weak if and only if
C C B or C n B = 0 for each strongly connected component C C S. A
language L is WDBA-recognizable if there exists some W D B A A such that
L = L(A).
In 2007, Dax et al. showed that the standard powerset determinization
construction k n o w n for finite automata can be correctly used i n order to
determinize N B A for WDBA-recognizable languages [17]. The result of this
determinization is an W D B A . Moreover, i n 2001 L o d i n g showed an effective
minimization of W D B A [33]. Note that the minimization of general
D B A is an NP-complete problem [48].
Every obligation property (a boolean combination of safety and guarantee
properties) is a WDBA-recognizable language [11]. Thus combination of
the results [17],[33], and [11] mentioned above yields an effective procedure
for obtaining the m i n i m a l W D B A for all obligation properties:
1. Translate <p into an N B A Mv using an arbitrary translator.
2. Perform the W D B A - d e t e r m i n i z a t i o n [17] of Mv to obtain a W D B A
18
3. T R A N S L A T I O N S T O D E T E R M I N I S T I C A U T O M A T A - S T A T E O F T H E A R T
3. M i n i m i z e [33] Vv and obtain M.^ - the m i n i m a l W D B A for ip.
Moreover, for a D R A 1Z w e can construct an equivalent D B A B w i t h the
same number of states as 1Z for every DBA-realizable language L(7£) [27].
Therefore, every Rabin automaton for an obligation property ip has at least
the same size as the W D B A M.^ obtained by the three steps mentioned
above.
3.2 Direct translations of L T L to deterministic automata
Translation of the full L T L to deterministic automata is n o n trivial. We can
find three stages of development of the direct translations, distinguished by
fragments they w o r k o n (by fragment w e mean a subset of L T L w h i c h can
be defined by some syntactic limitation).
Simple fragments. The translations w o r k only for L T L DBA-recognizable
fragments w h i c h use F and X as the only temporal operators.
More complex fragments. The translations w o r k for more expressive fragments
w h i c h use at least temporal operators F and G and the operators
can be arbitrary nested and alternated. The Biichi accepting condition
is not expressible enough for these fragments.
The full LTL. The translations w o r k for all formulae of L T L without any
limitations.
Fragments are specified by a list of (temporal) operators. Let oplist be
a list of temporal operators. We use LTL(oplist) to denote a subset of L T L
formulae w h i c h contain only temporal operators from oplist and boolean
connectives. There is no limitation given o n boolean connectives, unless
oplist contains some. Then the formulae of the fragment cannot use other
boolean connectives then those i n oplist.
3.2.1 Simple fragments
In 2004, A l u r and L a Torre show inductive (bottom-up) translations to D B A
for several DBA-recognizable L T L fragments [2]. The fragments L T L ( F , A ) 5
and L T L ( F , X , A ) 5
are translated to automata w i t h (singly) exponentially
many states w i t h respect to the length of the translated formula. They also
5. Negations and disjunctions are allowed on the top and atomic levels in their definition
of fragments.
19
3. T R A N S L A T I O N S T O D E T E R M I N I S T I C A U T O M A T A - S T A T E O F T H E A R T
proposed doubly exponential translations for two fragments: L T L ( F , A, V )
and L T L ( F , X, A, V ) . They also give a doubly exponential lower b o u n d for
these two fragments.
3.2.2 More complex fragments
In 2012, Esparza and Kfetinsky came u p w i t h a direct translation of an L T L
fragment L T L ( F , G) [26]. The fragment is significantly more expressive then
those of [2]. M o r e specifically, it allows nesting and alternation of operators
F and G. The translation first builds a M u l l e r automaton using semantics of
subformulae, similarly to the tableaux method [16]. The M u l l e r automaton
is then converted to a generalized Rabin automaton ( G D R A ) 6
, w h i c h can
be possibly converted to standard D R A . The generalized Rabin accepting
condition was first introduced here. The tool Rabinizer is a proof-of-concept
implementation of their approach.
The w o r k of [26] w a s quickly followed b y our translation of fragment
LTL(FS ,GS ) w h i c h is strictly more expressive than LTL(F,G). O u r approach is
described i n [3] and implemented i n the tool L T L 3 D R A . The product of our
translation is a transition-based generalized Rabin automaton ( T G D R A ) ,
w h i c h is more succinct then G D R A used i n [26]. In fact, w e also showed a
straightforward extension of the translation to a larger L T L fragment called
L T L x G U X . We discuss this translation i n Chapter 4 i n more detail.
Rabinizer 2 extended the approach of [26] to w o r k w i t h a n even more
expressive fragment called L T L x G U (LTL where U is not allowed i n scope
of any G) i n 2013. Rabinizer 2 is a proof-of-concept implementation of this
translation. It is b u i l d u p o n the same methods as Rabinizer. In addition to
the translation of Rabinizer, slave automata are used to check validity of
G subformulae i n Rabinizer 2. The result of this translation is a composition
of one master automaton (basically the product of the translation from
2012 [26]) and all slave automata. The concept of slave automata allows to
handle X operators inside Gip subformulae.
We published a n experimental performance evaluation of the tools Rabinizer,
L T L 3 D R A , Rabinizer 2, and l t l 2 d s t a r (determinization of N B A )
in 2013 [10]. It showed that the tools specialized to smaller fragments (Rabinizer
and L T L 3 D R A ) outperforms the universal l t l 2 d s t a r and the less
specialized Rabinizer 2 on the less expressive fragments. See more i n C h a p ter
4.
6. Note that their definition of the generalized Rabin condition differs from that of Chapter
2. Their condition is defined as a positive boolean combination of standard Rabin pairs.
This can be easily converted to a set of generalized Rabin pairs as in our definition.
20
3 . T R A N S L A T I O N S T O D E T E R M I N I S T I C A U T O M A T A - S T A T E O F T H E A R T
3.2.3 Full LTL
The w o r k of Esparza and Kfetmsky d i d not stop by Rabinizer 2. In 2 0 1 4
they presented a translation of full L T L [19] w h i c h is implemented i n tool
Rabinizer 3. This w o r k extends their previous compositional approach [30].
The automaton for ip is a parallel composition of one master automaton and
slave automata for each G-subformula Gtp. The master automaton monitors
w h i c h parts of (p remain to be fulfilled and slave automata check whether
FGtp holds and provide information w h e n Gtp starts to hold.
Instead of classical finite automata used i n Rabinizer 2 as slaves, Rabinizer
3 uses Mojmir automata. M o j m i r automata is a novel type of deterministic
w-automata. A M o j m i r automaton is an automaton w i t h multiple
tokens. In every r u n of an usual automaton there is only one state activated
at each step. We can see that as if there is one token m o v i n g along the
automaton's states according to the transition relation. There are multiple
tokens m o v i n g along the states during the r u n of M o j m i r automaton and
positions of all of them are tracked. In every step of M o j m i r automaton M.,
a new token appears i n M.'s initial state and all older tokens are m o v e d according
to the transition relation of M.. We can imagine that as if there is a
new r u n starting at every step. A r u n of a M o j m i r automaton is accepting
if all but finitely many tokens reach accepting state (tokens that reach an
accepting state disappear from the run). The accepting condition of M o j m i r
automata naturally checks that tp eventually holds forever, i.e. FGtp.
2 1
3. T R A N S L A T I O N S T O D E T E R M I N I S T I C A U T O M A T A - S T A T E O F T H E A R T
N a m e & reference/ Last release Fragment
Availability
L T L 2 B A [21] 2007 L T L
h t t p : / / w w w . l s v . e n s - c a c h a n . f r / ~ g a s t i n / l t l 2 b a /
L T L 3 B A [5] 2012 L T L
N
h t t p : / / s o u r c e f o r g e . n e t / p r o j e c t s / l t 1 3 b a /
S P O T (ltl2tgba) [18] 2014 L T L
h t t p : / / s p o t . l i p 6 . f r /
ltl2dstar [23] 2005 L T L
h t t p : / / w w w . l t l 2 d s t a r . d e
L T L 3 D R A [10], [3] 2013 L T L x G U X
h t t p s : / / s o u r c e f o r g e . n e t / p r o j e c t s / l t 1 3 d r a /
Rabinizer [20], [26] 2012 LTL(F, G)
h t t p s : / / r a b i n i z e r . i n f o r m a t i k . t u - m u e n c h e n . d e /
Rabinizer 2 [30] 2013 L T L x G U
h t t p s : / / w w w 7 . i n . t u r n . d e / ~ k r e t i n s k / r a b i n i z e r 2 . h t m l
Rabinizer 3 [25], [19] 2014 L T L
h t t p s : / / w w w 7 . i n . t u r n . d e / ~ k r e t i n s k / r a b i n i z e r 3 . h t m l
Table 3.1: The reference list of L T L to w-automata translators. The N indicates
translators to non-deterministic automata while D stands for deter-
minstic.
22
4 Achi eved Results
Besides translations of L T L to deterministic automata, our research is focused
o n L T L and w­automata i n general. In Sections 4.1 and 4.2 w e describe
our w o r k relevant to the topic of the thesis proposed here. Then w e briefly
mention other publications i n Section 4.3.
In the field of translations to deterministic automata, w e published two
papers i n 2013.
• Tomáš Babiak, F rantišek Blahoudek, Mojmír Křetínský, and Jan Strejček.
Effective translation of L T L to deterministic Rabin automata: Bey
o n d the (F ,G)­fragment. In ATVA'13, volume 8172 of LN CS, pages
24­39. Springer, 2013 [3], discussed i n Section 4.1.
• F rantišek Blahoudek, Mojmír Křetínský, and Jan Strejček. Comparison
of L T L to deterministic Rabin automata translators. In LPAR'13,
volume 8312 of LN CS, pages 164­172. Springer, 2013 [10], discussed
i n Section 4.2.
Both publications are attached i n A p p e n d i x A . The extended version [4] of
the translation paper [3] is also publicly available. In addition to [3], this extended
version proves correspondence of M a y / M u s t alternating automata
to LTL(F S , Gs ), discusses some technical details of the translation and shows
more experimental evaluations.
4.1 Translati on of LTL(FS , Gs )
O u r translator L T L 3 D R A followed the new trend of direct translations of
non­trivial fragments that Esparza and Křetínský established w i t h their Rabinizer.
O u r approach to the translation has two sources of inspiration.
• L T L 2 B A and L T L 3 B A inspired our w o r k w i t h successful usage of very
weak alternating automata (VWAA) as an intermediate step of the
translation.
• Rabinizer inspired our w o r k by more complex (generalized Rabin)
accepting condition.
O u r translation of ip to a deterministic automaton proceeds i n two or
three steps as illustrated i n F igure 4.1. The number of steps depends on
whether the user wants a T G D R A or a D R A .
23
4. A C H I E V E D R E S U L T S
1. We first translate ip into a May/Must alternating automaton M.^. The
class of M a y / M u s t alternating automata ( M M A A ) is a subclass of
very weak co-Biichi alternating automata. We use a straightforward
translation of L T L to V W A A s h o w n by authors of L T L 2 B A [21]. This
translation naturally results i n M M A A for formulae of the fragment
LTL(FS , Gs ).
2. The M M A A My is then determinized to a T G D R A Q^. This construction
is the m a i n contribution of the paper.
3. A procedure that produces a D R A Av equivalent to Qv (and thus to
p) is then optionally performed. This procedure is called degeneralization
and is very similar of degeneralization of G D R A s h o w n by
Esparza and Kfetinsky i n [26].
L T L formula if T G D R A Q„
M M A A M, D R A Au
Figure 4.1: The w o r k f l o w of L T L 3 D R A . O u r m a i n contribution is highlighted
by red color.
May/Must Alternating Automata. The definition of V W A A and M M A A
is taken from [3].
A very weak alternating co-Biichi automaton ( V W A A ) A is a tuple A =
(S,H,5,I,F), where S is a finite set of states, subsets c C S are called configurations,
E is an alphabet, 5 C 51
x E x 2 s
is an alternating transition
relation, I C 2s
is a non-empty set of initial configurations, F C S is a set
of co-Biichi accepting states, and there exists a partial order on S such that,
for every transition (s, a, c) G 5, all the states of c are lower or equal to s.
A triple (s,a,c) G 5 is called a transition from s to c labelled by a, or an
a-transition of s. We say that s is the source state and c the target configuration
of the transition. A transition is looping if the target configuration
contains the source state, i.e. s G c. A transition is called a selfloop if its
target configuration contains the source state only, i.e. c = {s}.
A multitransition T w i t h a label a is a set of transitions w i t h the same
label and such that the source states of the transitions are pairwise different.
24
4. A C H I E V E D R E S U L T S
Figure 4.2: A V W A A (and also M M A A ) corresponding to formula GV> V Gb,
where ip = Fs a A Fs6.
A source configuration of T, denoted by dom(T), is the set of source states
of transitions i n T. A target configuration of T, denoted by range(T), is the
union of target configurations of transitions i n T. We define a multitransition
relation A C 2 5
x £ x 2s
as
A = {(dom(T), a, range(T)) | there exists a multitransition T w i t h label a}.
A run p of a V W A A A over a w o r d w = wowi... G S w
is an infinite
sequence p = TQT\ . . . of multitransitions of A such that dom(To) is an initial
configuration of A and, for each i > 0, Tj is labelled b y u>j and range(Tj) =
d o m ( T i + i ) .
A r u n p is accepting if it has no suffix where, for some co-Biichi accepting
state / € F, each multitransition contains a looping transition from /.
The language of A is L(A) = {w eT,^ \ A has an accepting r u n over w}. By
Infs(p) we denote the set of states that occur i n dom(Tj) for infinitely many
indices i.
Figure 4.2 shows a V W A A that accepts the language described by the
formula G(F5 o A Fs6) V G6. Transitions are depicted by branching edges. If
a target configuration is empty, the corresponding edge leads to an empty
space. We depict all transitions w i t h the same source state and the same
target configuration by a single edge.labelled by a propositional formula tp
over AP representing the corresponding transition labels (e.g. given S =
2^-a
'b
\ the formula tp = a V b represents labels {a}, {a, &}, {&}). Each initial
configuration is represented by a possibly branching unlabelled edge
leading from an empty space to the states of the configuration. Co-Biichi
accepting states are double circled.
25
4. A C H I E V E D R E S U L T S
May Must Loopless
selfloop selfloop i n initial,
under tt each transition n o predecessors
Figure 4.3: Illustration of state types of M a y / M u s t alternating automata.
The specific properties of the types are highlighted by distinct colours.
Definition 4. A may/must alternating automaton (MMAA) is a VWAA such
that each its statefits into one of thefollowing three categories:
1. May-states - states with a selfloop for each a eT,. A run that enters such
a state may wait in the statefor an arbitrary number of steps.
2. Must-states - every transition of a must-state is looping. A run that enters
such a state can never leave it. In other words, the run must stay there.
3. Loopless states - states that have no looping transitions and no predecessors.
They can appear only in initial configurations (or they are unreachable).
The identification of the class of M M A A is a key contribution of [3].
The class of M M A A is equivalently expressive as LTL(FS , Gs ), and w h e n using
generalized Rabin condition, M M A A can be determinized by relatively
simple construction that w e call double powerset construction (performing
de-alternation and determinization of the M M A A ) . The states of the
new automaton Av are called macrostates. A macrostate consists of several
configurations. Intuitively, it stores all configurations i n w h i c h the determinized
M M A A Aiip can be after reading the same input. U n l i k e for Safra's
construction for N B A , this is all w e need to remember for our determiniza-
tion.
We justify these statements b y following theorems. We refer the reader
to [3] for the proofs.
Theorem 1. For every formula ip ofLTL(Fs, Gs) in a positive normal form, there
exists an equivalent MMAA M.v with n states where n is the number of temporal
subformulae off.
26
4. A C H I E V E D R E S U L T S
Theorem 2. Let Mbea MMAA with n states. Then a TGDRA with at most 22
™
states exists.
Corollary 1. Every formula ip ofLTL(Fs,Gs) in a positive normal form can be
translated to an equivalent TGDRA with at most 22
™ states where n is the number
of temporal subformulae of<p (note that n < \<p\).
We further showed that the same determinization procedure can be applied
to M a y /Must in the limit Alternating Automata (HmMMAA). A very
weak alternating automaton is H m M M A A if all states that are neither maystates,
must-states, nor loopless states have n o must-state as predecessor.
We also identified the fragment L T L x G U X and showed that it is equivalently
expressive as the class of H m M M A A . The fragment L T L x G U X contain
all formulae that have no X and n o U i n scope of any G. The fragment
is strictly larger than LTL(FS , Gs ), but strictly less expressive than L T L x G U X
of Rabinizer 2.
The author of this thesis proposal performed all the experiments and
participated o n text writing.
4.2 Comparison of L T L to deterministic automata translators.
Our paper [10] published at L P A R ' 1 3 gives a n overview of then-available
methods and tools to translate L T L to explicitly represented deterministic
Rabin automata, and evaluation of their performance. We evaluated tools
that perform direct translations of L T L fragments L T L 3 D R A , Rabinizer and
Rabinizer 2, and the tool l t l 2 d s t a r w h i c h translates the full L T L b y the
two-step translation using Safra's determinization. The deterministic a u tomaton
produced by l t l 2 d s t a r depends on w h i c h L T L to N B A translator
performed the first step. We evaluated l t l 2 d s t a r together w i t h four
LTL to N B A translators. So next to comparison w i t h the direct translators
this paper can be seen as a n experimental comparison of performance of
l t l 2 d s t a r w h e n using different L T L to N B A translators, w h i c h was done
only i n 2005 before. A n d as our w o r k shows, the situation changed dramatically
since then.
We used three types of benchmarks for this paper. Real specification
formulae, r a n d o m formulae, and parametric formulae gathered from literature.
Then-available tools for direct translation w o r k for certain fragments
only. Therefore our benchmarks were d i v i d e d according to these fragments:
LTL(F, G), L T L x G U X , and the full L T L . For the full L T L w e only were able
to give results for l t l 2 d s t a r w i t h different translators of L T L to N B A .
The m a i n observations and recommendations follow.
27
4. A C H I E V E D R E S U L T S
• There was no clear winner (or w i n n i n g combination of tools) that
w o u l d produce the best result for all benchmarks.
• Tools for direct translations give i n average smaller automata then
l t l 2 d s t a r for LTL(F , G). Moreover, the generalized automata produced
by L T L 3 D R A , Rabinizer and Rabinizer 2 are often even smaller
then the D R A being compared thanks to the more complex accepting
condition.
• Outside LTL(F , G) w e recommend to use l t l 2 d s t a r combined w i t h
ltl2tgba from Spot's library [18].
• The tool l t l 2 d s t a r usually produces the smallest automaton w h e n
ltl2tgba is used for the translation of the formula to an N B A .
• The t o o l l t l 2 d s t a r should check the intermediate Biichi automaton
for determinism (it does not check it so far) and apply Safra's construction
only w h e n necessary.
• A l l tools have still space for improvement.
Rabinizer 3 d i d not exist i n 2013 and thus was not included. Unfortunately
i n both papers about Rabinizer 3 [19] and [25] only l t l 2 d s t a r
combined w i t h old­fashioned L T L 2 B A is used for benchmarks o n the full
LTL. Based on the results discussed above w e consider the comparison of
sizes of automata produced b y Rabinizer 3 and l t l 2 d s t a r combined w i t h
ltl2tgba as very interesting and as a possible future work.
The author of this proposal performed all the experiments used i n this
w o r k and participated o n the text.
4.3 Other publi cati ons and research
Outside the area of translation of L T L to deterministic automata, w e published
two papers.
• F rantišek Blahoudek, Alexandre Duret­Lutz, Mojmír Křetínský , and
Jan Strejček. Is there a best Biichi automaton for explicit model checking?
In SPIN 'U, pages 68­76. A C M , 2014 [9].
• F rantišek Blahoudek. Chasing the best Biichi automata for nested
depth­first search based model checking. In MOVEP'14, pages 89­94,
2014 [8].
28
4. A C H I E V E D R E S U L T S
The paper published at the S P I N 2014 conference [9] discusses the i m pact
of choice of N B A o n performance of the Spin model checker. The contribution
of the author of this proposal consists of all the experiments w i t h
Spin, some observations and some text writing.
In proceedings of the summer school M O V E P 2014 w e published a paper
about novel ways to estimate Spin performance w i t h different automata
used for -up [8]. The author of this thesis proposal is the only author of this
work.
29
5 Aims of the Thesis
Our future focus of research i n the area of translation of L T L to deterministic
automata can be d i v i d e d into two areas. We p l a n to contribute to both approaches
to translation of L T L to deterministic automata. We p l a n to show
a generalization of Safra's determinization procedure, w h i c h w i l l hopefully
make the two-step approach more effective and w e p l a n to extend our
translator L T L 3 D R A to process the full L T L . We comment o n both research
directions i n more detail i n the following.
5.1 Generalization of Safra's Construction
G i v e n an N B A , Safra's determinization procedure (as originally proposed
in [46]) builds an equivalent D R A . In 2012, Schewe and Varghese extended
the Safra's ideas i n a w a y that for a given non-deterministic generalized
Biichi automaton (GBA) the procedure constructs a transition-based deterministic
Rabin automaton ( T D R A ) [49]. O u r goal for the thesis is to generalize
the construction even more: w e want to b u i l d an equivalent T G D R A
for a given transition-based generalized non-deterministic Biichi automaton
(TGBA). T G D R A , as showed i n [3,25], can be m u c h more succinct than
D R A , or even T D R A . In addition, T G B A is a natural intermediate product
of many translations of L T L to N B A and the m o d e r n translators like
L T L 3 B A and ltl2tgba from Spot library can output T G B A directly.
Currently, there is no determinization of Biichi automata that w o u l d result
into ( T ) G D R A . A s s h o w n i n [12], using generalized condition can dramatically
improve performance of P R I S M . We believe that this modification
of the determinization procedure w i l l improve effectiveness of the two-step
approach to translation to deterministic automata and make it more competitive
to the direct approach. Moreover, having another source of T G D R A
for L T L formulae w i l l possibly allow us to find weaknesses of the existing
translators to T G D R A ( L T L 3 D R A , Rabinizer 3).
5.2 Extension of L T L 3 D R A to Process F u l l L T L
L T L 3 D R A is our implementation of translation to T G D R A via M a y / M u s t
automata (a subclass of very weak alternating automata) published i n [3].
L T L 3 D R A currently works only for fragment L T L x G U X . Further, P R I S M
is not able to parse the current output of L T L 3 D R A and does not support
T G D R A . This prevents us to perform interesting experiments that w o u l d
31
5. A I M S O F T H E T H E S I S
reveal properties (others than the number of states) of automata that heavily
influence the running time of verification by P R I S M .
We have the following goals regarding L T L 3 D R A .
• Extend the theory of [3] and process the full L T L .
• Implement the translation of the full L T L i n L T L 3 D R A .
• L T L 3 D R A w i l l be able to produce equivalent T G D R A and D R A for
a given formula i n H O A F 1
format. U s i n g the H O A F format should
make integration of T G D R A into P R I S M feasible i n a systematic way.
• Integration of L T L 3 D R A into P R I S M . Being able to experiment w i t h
the translation and its effect o n P R I S M we can optimize the translation
not only w i t h respect to the size of resulting automaton, but also w i t h
respect to specific needs of P R I S M .
• Prepare an experimental evaluation of performance and effectiveness
of the new L T L 3 D R A and compare it to other translators.
5.3 Expected Results and Schedule
To summarize, the expected results are the following.
• Direct L T L to T G D R A translation implemented i n L T L 3 D R A .
• A prototype tool performing generalized Safra's determinization of
T G B A into T G D R A .
• Integration of both tools w i t h P R I S M ; experiments revealing influence
of translations on the running time of P R I S M .
• Reviewed publications o n international conferences and/or i n jour­
nals.
1. A n format for aj­automata currently being developed in cooperation with Alexandre
Duret­Lutz, Joachim Klein, Jan Křetínský, and Jan Strejček.
32
5. A I M S O F T H E T H E S I S
The p l a n of m y future research and study follows here.
• Doctoral exam and defence of this thesis proposal, M a y 2015
• generalized Safra's construction, n o w - M a r c h 2015
• implementation of the generalized Safra's construction; experimental
performance evaluation; preparation af a publication,
M a r c h - A u g u s t 2015
• direct translation of the full L T L into T G D R A ,
September - December 2015
• implementation of the direct translation i n L T L 3 D R A ; integration of
T G D R A into P R I S M ; preparation af a publication,
January - A p r i l 2016
• experiments w i t h P R I S M and translations, A p r i l - A u g u s t 2016
• text of the P h . D . thesis, A u g u s t 2016 - January 2017
• the final version of the thesis. January 2017
33
5. A I M S O F T H E T H E S I S
34
Bibliography
[1] C. S. Althoff, W. Thomas, and N . Wallmeier. Observations o n determinization
of Buchi automata. In CIAA'06, pages 262­272. Springer,
2006.
[2] R. A l u r and S. L . Torre. Deterministic generators and games for L T L
fragments. ACM Trans. Comput. Log., 5(l):l­25, 2004.
[3] T. Babiak, F . Blahoudek, M . Křetínský, and J. Strejček. Effective translation
of L T L to deterministic Rabin automata: Beyond the (F ,G)fragment.
In ATVA'13, volume 8172 of LN CS, pages 24­39. Springer,
2013.
[4] T. Babiak, F . Blahoudek, M . Křetínský, and J. Strejček. Effective translation
of L T L to deterministic Rabin automata: Beyond the (F ,G)fragment.
CoRR, abs/1306.4636, 2013. Extended version of [3], publicly
available at h t t p : / / a r x i v . org/abs/1306 .4636.
[5] T. Babiak, M . Křetínský, V. Řehák, and J. Strejček. L T L to Buchi automata
translation: Fast and more deterministic. In TACAS'12, volume
7214 of LN CS, pages 95­109. Springer, 2012.
[6] C. Baier and J.­P. Katoen. Principles of model checking. M I T press,
2008.
[7] J. Barnat, L . Brim, V. H a v e l , J. Havlíček, J. Kriho, M . Lenčo, P. Ročkai,
V. Still, and J. Weiser. D i V i n E 3.0 ­ A n Explicit­State M o d e l Checker for
Multithreaded C & C++ Programs. In CAV'13, v o l u m e 8044 of LN CS,
pages 863­868. Springer, 2013.
[8] F . Blahoudek. Chasing the best Biichi automata for nested depth­first
search based model checking. In MOVEP'14, pages 89­94, 2014.
[9] F . Blahoudek, A . Duret­Lutz, M . Křetínský, and J. Strejček. Is there a
best Biichi automaton for explicit model checking? In SPIN '14, pages
68­76. A C M , 2014.
[10] F . Blahoudek, M . Křetínský, and J. Strejček. C o m p a r i s o n of L T L to
deterministic Rabin automata translators. In LPAR'13, volume 8312 of
LNCS, pages 164­172. Springer, 2013.
35
5. A I M S O F T H E T H E S I S
[11] E. Chang, Z . M a n n a , and A . Pnueli. The safety-progress classification.
In Logic and Algebra of Specification, volume 94 of NATO ASI Series,
pages 143-202. Springer, 1993.
[12] K . Chatterjee, A . Gaiser, and J. Kfetinsky. Automata w i t h generalized
Rabin pairs for probabilistic model checking and L T L synthesis. In
CAV'13, volume 8044 of LNCS, pages 559-575. Springer, 2013.
[13] F. Ciesinski and C. Baier. Liquor: A tool for qualitative and quantitative
linear time analysis of reactive systems. In QEST'06, pages 131-132,
2006.
[14] E. M . Clarke and E. A . Emerson. Design and synthesis of synchronization
skeletons using branching-time temporal logic. In Logic of
Programs, volume 131 of LNCS, pages 52-71. Springer, 1981.
[15] E. M . Clarke, O. Grumberg, and D . A . Peled. Model Checking. M I T
Press, 1999.
[16] J . - M . Couvreur. On-the-fly verification of temporal logic. In FM'99,
volume 1708 of LNCS, pages 253-271. Springer, 1999.
[17] C. Dax, J. Eisinger, and F. Klaedtke. Mechanizing the powerset construction
for restricted classes of w-automata. In ATVA'07, volume
4762 of LNCS, pages 223-236. Springer, 2007.
[18] A . Duret-Lutz. L T L translation improvements i n Spot 1.0. International
Journal on Critical Computer-Based Systems, 5(l/2):31-54, Mar.
2014.
[19] J. Esparza and J. Kfetinsky. F r o m L T L to deterministic automata: A
Safraless compositional approach. In CAV'14, volume 8559 of LNCS,
pages 192-208. Springer, 2014.
[20] A . Gaiser, J. Kfetinsky, and J. Esparza. Rabinizer: Small deterministic
automata for LTL(F,G). In ATVA'12, volume 7561 of LNCS, pages 72-
76, 2012.
[21] P. Gastin and D . O d d o u x . Fast L T L to Büchi automata translation. In
CAV'01, volume 2102 of LNCS, pages 53-65. Springer, 2001.
[22] G . H o l z m a n n . The Spin model checker: primer and reference manual.
Addison-Wesley Professional, first edition, 2003.
36
5. A I M S O F T H E T H E S I S
[23] J. Klein. Linear time logic and deterministic w­automata. Master's
thesis, University of Bonn, 2005.
[24] J. K l e i n and C. Baier. Experiments w i t h deterministic w­automata
for formulas of linear temporal logic. Theoretical Computer Science,
363(2):182­195,2006.
[25] Z . Komárkova and J. Křetínský. Rabinizer 3: Safraless translation of
L T L to small deterministic automata. In ATVA'14, volume 8837 of
LNCS, pages 235­241. Springer, 2014.
[26] J. Křetínský and J. Esparza. Deterministic automata for the (F , G)fragment
of L T L . In CAV'12, volume 7358 of LN CS, pages 7­22.
Springer, 2012.
[27] S. Krishnan, A . Puri, and R. Brayton. Deterministic w­automata vis­avis
deterministic Buchi automata. In ISAAC'94, volume 834 of LN CS,
pages 378­386. Springer, 1994.
[28] O . Kupferman. Recent challenges and ideas i n temporal synthesis. In
SOFSEM'12, pages 88­98. Springer, 2012.
[29] O . K u p f e r m a n and A . Rosenberg. The B l o w ­ u p i n Translating L T L to
Deterministic Automata. In MoChArt, volume 6572 of LN CS, pages
85­94. Springer, 2010.
[30] J. Křetínský and R. L. Garza. Rabinizer 2: Small deterministic automata
for L T L \ G U . In ATVA'13, volume 8172 of LN CS, pages 446­
450. Springer, 2013.
[31] M . K w i a t k o w s k a , G . N o r m a n , and D . Parker. P R I S M 4.0: Verification
of probabilistic real­time systems. In CAV'll, volume 6806 of LN CS,
pages 585­591. Springer, 2011.
[32] A . W. Laarman, J. C. v a n de P o l , and M . Weber. Multi­core LTSmin:
M a r r y i n g modularity and scalability. In N FM'2011, volume 6617 of
LNCS, pages 506­511. Springer, 2011.
[33] C. Loding. Efficient minimization of deterministic weak w­automata.
Information Processing Letters, 79(3): 105­109, 2001.
[34] R. M c N a u g h t o n . Testing and generating infinite sequences b y a finite
automaton. Information and control, 9(5):521­530,1966.
37
5. A I M S O F T H E T H E S I S
[35] M . Michel. Complementation is more difficult w i t h automata o n infinite
words. CNET, Paris, 15,1988.
[36] A . Morgenstern and K . Schneider. F r o m L T L to symbolically represented
deterministic automata. In VMCAF08, volume 4905 of LNCS,
pages 279-293. Springer, 2008.
[37] D . E. Muller. Infinite sequences and finite machines. In FOCS'63, pages
3-16. IEEE, 1963.
[38] D . E. M u l l e r and P. E. Schupp. Simulating alternating tree automata by
nondeterministic automata: N e w results and new proofs of the theorems
of Rabin, M c N a u g h t o n and Safra. Theoretical Computer Science,
141(1):69-107,1995.
[39] J. R. Norris. Markov chains. Cambridge university press, 1998.
[40] N . Piterman. F r o m nondeterministic Biichi and Streett automata to
deterministic parity automata. Logical Methods in Computer Science,
3(3), 2007.
[41] A . Pnueli. The temporal logic of programs. In FOCS'77, pages 46-57.
IEEE, 1977.
[42] A . Pnueli and R. Rosner. O n the synthesis of a reactive module. In
SIGPLAN-SIGACT'89, pages 179-190. A C M , 1989.
[43] A . Pnueli and R. Rosner. O n the synthesis of an asynchronous reactive
module. In ICALP'89, pages 652-671. Springer, 1989.
[44] M . L. Puterman. Markov decision processes: discrete stochastic dynamic
programming. John Wiley & Sons, 2009.
[45] M . O . Rabin and D . Scott. Finite automata and their decision problems.
IBM journal of research and development, 3(2):114-125,1959.
[46] S. Safra. O n the complexity of w-automata. In FOCS'88, pages 319-327.
IEEE, 1988.
[47] S. Schewe. Tighter bounds for the determinisation of Biichi automata.
In FOSSACS'09, volume 5504 of LNCS, pages 167-181. Springer, 2009.
[48] S. Schewe. Beyond hyper-minimisation—minimising dbas and dpas
is np-complete. In FSTTCS'10, pages 400-411. Schloss Dagstuhl Leibniz-Zentrum
fuer Informatik, 2010.
38
5. A I M S O F T H E T H E S I S
[49] S. Schewe a n d T. Varghese. Tight bounds for the determinisation a n d
complementation of generalised Biichi automata. In ATVA'12, volume
7561 of LNCS, pages 42-56. Springer, 2012.
[50] R. S. Streett. Propositional dynamic logic of looping a n d converse is
elementarily decidable. Information and control, 54(1):121-141,1982.
[51] M . Y. Vardi. A n automata-theoretic approach to linear temporal logic.
In Logics for Concurrency, volume 1043 of LNCS, pages 238-266.
Springer, 1996.
39
Summary
This proposal of m y P h . D . thesis is dedicated to a currentl y active area of
research ­ transl ation of Linear Temporal Logic (LTL) into deterministic OJautomata
(i.e. automata over infinite words). Two approaches to the translation
can be found i n the l iterature ­ direct translations and two­step translation
incl uding determinization of non­deterministic Biichi automata.
This thesis proposal describes the current state­of­the art of both approaches,
discusses the difficul ties of both, presents our w o r k al ready done
in the fiel d of direct translations, and final l y proposes further contributions
to both approaches to the transl ation. The proposed contributions are extension
of our transl ator L T L 3 D R A to process the ful l L T L (right n o w it
can handl e onl y a fragment of L T L ) , and general ization of Safra's determinization
construction to be abl e to determinize transition­based generalized
Biichi automata into transition­based general ized Rabin automata.
Shrnutí
Teze mé dizertační práce se věnují aktivní obl asti výzkumu ­ překl adu
Lineární Temporál ní Logiky (LTL) do deterministických automatů n a d nekonečnými
sl ovy (deterministických w­automatů). V l iteratuře můžeme nalézt
d v a možné přístupy k překladu: překl ad přímý a dvojkrokový překl ad,
který zahrnuje determinizaci Bůchiho automatů. Teze popisují aktuální stav
výzkumu v obou větvích, připomínají probl émy obou přístupů, prezentují
náš dosavadní publ ikovaný výzkum v této obl asti a navrhují dal ší směry
vývoje pro oba přístupy k překl adů. V obl asti přímých překl adů je to rozšíření
nástroje L T L 3 D R A na cel ou L T L (v současnosti pracuje jen s fragmentem
L T L ) , v obl asti překl adů přes nedeterministické automaty je to
zobecnění Safrovy determinizační konstrukce tak, abychom pro general izované
Bůchiho automaty s akceptující podmínkou na hranách dostal i deterministické
general izované Rabínovy automaty s akceptující podmínkou
na hranách.
41
A Publi cati ons
We attach two following papers that were published o n international conferences
to the text of this thesis:
• [3] Tomáš Babiak, F rantišek Blahoudek, Mojmír Křetínský, and Jan
Strejček. Effective translation of L T L to deterministic Rabin automata:
Beyond the (F ,G)­fragment. In ATVA'13, volume 8172 of LN CS, pages
24­39. Springer, 2013.
The author of this thesis proposal is the leading author of this paper.
• [10] F rantišek Blahoudek, Mojmír Křetínský, and Jan Strejček. C o m parison
of ltl to deterministic rabin automata translators. In LPAR'13,
volume 8312 of LN CS, pages 164­172. Springer, 2013.
The author of this thesis proposal performed all the experiments used
i n this paper and participated o n text writing.
43
Effective Translation of L T L to Deterministic
Rabin Automata: Beyond the (F ,G)­F ragment*
Tomáš Babiak, F rantišek Blahoudek, Mojmír Křetínský, and Jan Strejček
Faculty of Informatics, Masaryk University, Brno, Czech Republic
{xbabiak, xblahoud, kretinsky, strejcek}@fi.muni.cz
A b s t r a c t . Some applications of linear temporal logic (LTL) require to
translate formulae of the logic to deterministic a>­automata. There are
currently two translators producing deterministic automata: l t l 2 d s t a r
working for the whole L T L and Rabinizer applicable to LTL(F, G) which
is the L T L fragment using only modalities F and G. We present a new
translation to deterministic Rabin automata via alternating automata
and deterministic transition­based generalized Rabin automata. Our translation
applies to a fragment that is strictly larger than LTL(F, G). Experimental
results show that our algorithm can produce significantly smaller
automata compared to Rabinizer and l t l 2 d s t a r , especially for more
complex L T L formulae.
1 Introducti on
Linear temporal logic (LTL) is a popular formalism for specification of behavioral
system properties with major applications i n the area of model checking [8,5].
More precisely, L T L is typically used as a human­oriented front­end formalism as
L T L formulae are succinct and easy to write and understand. Model checking algorithms
usually work with an w­automaton representing all behaviors violating
a given specification formula rather than with the L T L formula directly. Hence,
specifications written i n the form of L T L formulae are negated and translated to
equivalent w­automata [31]. There has been a lot of attention devoted to translation
of L T L to nondeterministic Buchi automata (N BA), see for example [10,11,
29,15] and the research i n this direction still continues [12,4, 2]. However, there
are algorithms that need specifications given by deterministic w­automata, for
example, those for L T L model checking of probabilistic systems [30, 9, 5] and
those for synthesis of reactive modules for L T L specifications [7, 26], for a recent
survey see [20]. A s deterministic Buchi automata (DBA) cannot express all the
properties expressible i n L T L , one has to choose deterministic automata with
different acceptance condition.
There are basically two approaches to translation of L T L to deterministic
w­automata. The first one translates L T L to N B A and then it employs Safra's
construction [27] (or some of its variants or alternatives like [23, 28]) to transform
the N B A into a deterministic automaton. This approach is represented by the
* The authors are supported by The Czech Science Foundation, grant P202/12/G061.
tool l t l 2 d s t a r [16] which uses an improved Safra's construction [17,18] usually
in connection with L T L to N B A translator L T L 2 B A [15]. The main advantage of
this approach is its universality: as L T L 2 B A can translate any L T L formula into
an N B A and the Safra's construction can transform any N B A to a deterministic
Rabin automaton (DRA), l t l 2 d s t a r works for the whole L T L . The main disadvantage
is also connected with the universality: the determinization step does
not employ the fact that the N B A represents only an L T L definable property.
One can easily observe that l t l 2 d s t a r produces unnecessarily large automata,
especially for formulae with more fairness subformulae.
The second approach is to avoid Safra's construction. A s probabilistic modelcheckers
deal with linear arithmetic, they do not profit from symbolically represented
deterministic automata of [24,22]. A few translations of some simple
L T L fragments to D B A have been suggested, for example [1]. Recently, a translation
of a significantly larger L T L fragment to D R A has been introduced i n [19]
and subsequently implemented i n the tool Rabinizer [14]. The algorithm builds
a generalized deterministic Rabin automata (GDRA) directly from a formula.
A D R A is then produced by a degeneralization procedure. Rabinizer often produces
smaller automata than l t l 2 d s t a r . The main disadvantage is that it works
for L T L ( F , G) only, i.e. the L T L fragment containing only temporal operators
eventually (F) and always (G). Authors of the translation claim that it can be
extended to a fragment containing also the operator next (X).
In this paper, we present another Safraless translation of an L T L fragment
to D R A . The translation is influenced by the successful L T L to N B A translation
algorithm L T L 2 B A [15] and it proceeds i n the following three steps:
1. A given L T L formula ip is translated into a very weak alternating co-Biichi
automaton (VWAA) A as described i n [15]. If tp is an L T L ( F S , Gs ) formula,
i.e. any formula which makes use of F, G, and their strict variants Fs and
G s as the only temporal operators, then A satisfies an additional structural
condition. We call such automata may/must alternating automata (MMAA).
2. The M M A A A is translated into a transition-based generalized deterministic
Rabin automaton (TGDRA) Q. The construction of generalized Rabin pairs
of Q is inspired by [19].
3. Finally, Q is degeneralized into a (state-based) D R A T>.
In summary, our contributions are as follows. First, note that the fragment
LTL(FS , Gs ) is strictly more expressive than L T L ( F , G). Moreover, it can be shown
that our translation works for a fragment even larger than L T L ( F S , Gs ) but still
smaller than the whole L T L . Second, the translation has a slightly better theoretical
bound on the size of produced automata comparing to l t l 2 d s t a r , but
the same bound as Rabinizer. Experimental results show that, for small formulae,
our translation typically produces automata of a smaller or equal size as the
other two translators. However, for parametrized formulae, it often produces automata
that are significantly smaller. Third, we note that our T G D R A are much
smaller than the (state-based) G D R A of [14]. We conjecture that algorithms for
model checking of probabilistic system, e.g. those i n P R I S M [21], can be adapted
to work with T G D R A as they are adapted to work with G D R A [6].
2 Preliminaries
This section recalls the notion of linear temporal logic (LTL) [25] and describes
the w-automata used in the following.
Linear Temporal Logic (LTL) The syntax of L T L is defined by
p ::= tt | a \ -up \ <p V ip \ p A ip | Xp \ ip U ip,
where tt stands for true, a ranges over a countable set AP of atomic propositions,
X and U are temporal operators called next and until, respectively. A n alphabet
is a finite set E = 2A P
, where AP1
is a finite subset of AP. A n ui-word (or
simply a word) over E is an infinite sequence of letters u = UQU\U2 . . . £ E". B y
Ui.. we denote the suffix Ui.. = UiUi+\
We inductively define when a word u satisfies a formula p, written u \= p,
as follows.
u\= tt
u\= a iff a £ uo
u \= -up iff u p
u \= pi V ifi2 iff u \= p\ or u \= P2
u \= pi A tp2 iff u \= pi and u \= P2
u \= Xp iff ui.. \= p
u [= pi U P2 iff 3i > 0. (Ui.. \= p2 and VO < j < i. Uj.. \= pi)
Given an alphabet E, a formula tp defines the language LE
{p) = {u £ E"
u \= p}. We write L(p) instead of L2
''^(p), where AP(p) denotes the set of
atomic propositions occurring in the formula p.
We define derived unary temporal operators eventually (F), always (G), strict
eventually (Fs ), and strict always (Gs ) by the following equivalences: Ftp = tt\J p,
Gp = -iF-ic/3, Fsp = XFp, and Gsp = XGp.
L T L ( F , G) denotes the L T L fragment consisting of formulae built with temporal
operators F and G only. The fragment build with temporal operators Fs ,
Gs , F and G is denoted by L T L ( F S , Gs ) as Ftp and Gp can be seen as abbreviations
for p V Fsp and p A Gsp, respectively. Note that L T L ( F S , Gs ) is strictly
more expressive than L T L ( F , G) as formulae Fsa and Gsa cannot be equivalently
expressed in L T L ( F , G).
A n L T L formula is in positive normal form if no operator occurs in the scope
of any negation. Each L T L ( F S , Gs ) formula can be transformed to this form using
De Morgan's laws for A and V and the equivalences -^Fstp = Gs-<ip, -<Gsip = Fs-<ip,
->Fip = G-itp, and - i G ^ = F-itp. We say that a formula is temporal if its topmost
operator is neither conjunction, nor disjunction (note that a and -<a are also
temporal formulae).
Deterministic R a b i n Automata and Their Generalization A semiautomaton
is a tuple T = (S,E,5,si), where S is a finite set of states, E is an
alphabet, si £ S is the initial state, and S C S x E x S is & deterministic transition
relation, i.e. for each state s £ S and each a £ E, there is at most one state
s' such that (s, a, s') £ <5. A triple (s, a, s') £ 6 is called a transition from s to s'
labelled by a, or an a-transition of s leading to s'. In illustrations, all transitions
with the same source state and the same target state are usually depicted by
a single edge labelled by a propositional formula ip over AP representing the
corresponding transition labels (e.g. given E = 2^-a
'b
\ the formula tp = a V b
represents labels {a}, {a, b}, {&}).
A run of a semiautomaton T over a word u = UQU\ . . . £ E u
is an infinite
sequence a = (SQ, UQ, SI)(SI, U\, S2) • • • £ 5" of transitions such that So = S/. B y
Inft(a) (resp. Infs(a)) we denote the set of transitions (resp. states) occurring
infinitely often i n a. For each word u £ Eu
, a semiautomaton has at most one
run over u denoted by a(u).
A deterministic Rabin automaton ( D R A ) is a tuple V = (S, E,5, si,7Z),
where (S, E, 5, si) is a semiautomaton and 1Z C 2 s
x 2 s
is a finite set of Rabin
pairs. Runs of T> are runs of the semiautomaton. A run a satisfies a R a b i n pair
(K, L) £ K if Infs(a) (1 K = 0 and Infs(a) fl i / I. A run is accepting if it
satisfies some Rabin pair of TZ. The language of V is the set L(V) of all words
u £ E" such that o~(u) is accepting.
A transition-based generalized deterministic Rabin automaton ( T G D R A ) is
a tuple Q = (S, E, S, si, QTZ), where (S, E, S, si) is a semiautomaton and QTZ C
2s
x 22
is a finite set of generalized Rabin pairs. Runs of Q are runs of the
semiautomaton. A run a satisfies a generalized R a b i n pair (K,{Lj}jej) £ QTZ
if Inft(a) n K = 0 and, for each j £ J, Inft(a) PI Lj ^ 0. A run is accepting if it
satisfies some generalized R a b i n pair of QTZ. The language of Q is the set L(Q)
of all words u £ E" such that a(u) is accepting.
A generalization of D R A called generalized deterministic Rabin automata
( G D R A ) has been considered in [19,14]. The accepting condition of G D R A is
a boolean combination (in disjunctive normal form) of Rabin pairs. A run a is
accepting if a satisfies this condition.
Very Weak Alternating A u t o m a t a and Their Subclass A very weak alternating
co-Biichi automaton ( V W A A ) A is a tuple (S,E,S,I,F), where S is
a finite set of states, subsets c C S are called configurations, E is an alphabet,
5 C S x E x 2s
is an alternating transition relation, I C 2 s
is a non-empty set
of initial configurations, F C S is a set of co-Biichi accepting states, and there
exists a partial order on S such that, for every transition (s, a, c) £ S, all the
states of c are lower or equal to s.
A triple (s, a,c) £ S is called a transition from s to c labelled by a, or an
a-transition of s. We say that s is the source state and c the target configuration
of the transition. A transition is looping if the target configuration contains the
source state, i.e. s £ c. A transition is called a selfloop if its target configuration
contains the source state only, i.e. c = {s}.
Figure 1(a) shows a V W A A that accepts the language described by the formula
G(Fs a A Fs6) V G6. Transitions are depicted by branching edges. If a target
Fig. 1. (a) A V W A A (and also M M A A ) corresponding to formula Gip V Gb, where
ip = Fso A Fsb. (b) A n accepting run of the automaton over ({a}0{6}{a, 6})".
configuration is empty, the corresponding edge leads to an empty space. We
often depict all transitions with the same source state and the same target configuration
by a single edge (as for semiautomata). Each initial configuration is
represented by a possibly branching unlabelled edge leading from an empty space
to the states of the configuration. Co-Buchi accepting states are double circled.
A multitransition T with a label a is a set of transitions with the same
label and such that the source states of the transitions are pairwise different.
A source configuration of T, denoted by dom(T), is the set of source states of
transitions in T. A target configuration of T, denoted by range(T), is the union
of target configurations of transitions i n T. We define a multitransition relation
A C 2s
x £ x 2s
as
A = {(dom(T), a,range(T)) | there exists a multitransition T with label a}.
A run p of a V W A A A over a word w = WQWI . . . £ is an infinite sequence
p = TQT\ . . . of multitransitions of A such that dom(T0 ) is an initial configuration
of A and, for each i > 0, T; is labelled by Wi and range(Ti) = d o m ( T i + 1 ) .
A run can be represented as a directed acyclic graph ( D A G ) . For example,
the D A G of Figure 1(b) represents a run of the V W A A of Figure 1(a). The dotted
lines divide the D A G into segments corresponding to multitransitions. Each
transition of a multitransition is represented by edges leading across the corresponding
segment from the starting state to states of the target configuration.
As our alternating automata are very weak, we can order the states in a way
that all edges in any D A G go only to the same or a lower row.
A n accepting run corresponds to a D A G where each branch contains only
finitely many states from F. Formally, the run p is accepting if it has no suffix
where, for some co-Buchi accepting state / £ F, each multitransition contains
a looping transition from /. The language of A is the set L(A) = {w £
A has an accepting run of over w}. B y Infs(p) we denote the set of states that
occur i n dom(Ti ) for infinitely many indices i.
Definition 1. A may/must alternating automaton (MMAA) is a VWAA where
each state fits into one of the following three categories:
1. May-states - states with a selfloop for each a £ E. A run that enters such
a state may wait in the state for an arbitrary number of steps.
2. Must-states - every transition of a must-state is looping. A run that enters
such a state can never leave it. In other words, the run must stay there.
3. Loopless states - states that have no looping transitions and no predecessors.
They can appear only in initial configurations (or they are unreachable).
The automaton of Figure 1(a) is an M M A A with must-states Gip,Gb and
may-states Fa, Fb.
We always assume that the set F of an M M A A coincides with the set of
all may-states of the automaton. This assumption is justified by the following
observations:
— There are no looping transitions of loopless states. Hence, removing all loopless
states from F has no effect on acceptance of any run.
— A l l transitions leading from must-states are looping. Hence, if a run contains
a must-state that is in F, then the run is non-accepting. Removing all muststates
in F together with their adjacent transitions from an M M A A has no
effect on its accepting runs.
— Every may-state has selfloops for all a £ E. If such a state is not in F, we can
always apply these selfloops without violating acceptance of any run. We can
also remove these states from all the target configurations of all transitions
of an M M A A without affecting its language.
3 Translation of L T L ( F S , Gs ) to M M A A
We present the standard translation of L T L to V W A A [15] restricted to the
fragment LTL(FS , Gs ). In this section, we treat the transition relation 5 C S x
E x 2 s
of a V W A A as a function 5 : S x E —> 22
, where c £ 5(s, a) means
(s, a, c) £ S. Further, we consider Gtp and Ftp to be subformulae of Gstp and Fsip,
respectively. This is justified by equivalences Gs?/> = XGip and Fstp = XFip.
Let ip be an L T L ( F S , G S ) formula in positive normal form. A n equivalent
V W A A is constructed as Av = (Q, E, S, I, F), where
— Q is the set of temporal subformulae of ip,
- S is defined as
5(tt, a) = {0} S(a, a) = {0} if a £ a, 0 otherwise
<5(-itt, a) = 0 <5(-io, a) = {0} if a g" a, 0 otherwise
6{Gsip,a) = {{Gip}} 6{Gip,a) = { c U {G^}J c £ 6{ip,a)}
5{FsiP, a) = {{F^}} 5(Fip, a) = {{F^}} U 5{ip, a), where
S(ip, a) = 6(tjj, a) if ip is a temporal formula
S(ipi V tp2, a) = 5(ipi,a) U S(tp2, a)
S(ipi A ip2,a) = {ci U c2 | ci £ S(ipi,a) and c2 £ S(tp2, a)},
— I = ip where ip is defined as
ip = {{ip}} if ip is a temporal formula
Ipl V 1p2 = Ipl U V>2
V'l A ^ 2 = { O i U 0 2 I Ox £ iTi and G>2 £ ? M , and
— i * 1
C Q is the set of all subformulae of the form Ftp i n Q.
Using the partial order "is a subformula of" on states, one can easily prove
that Av is a V W A A . Moreover, all the states of the form Gip are must-states and
all the states of the form Ftp are may-states. States of other forms are loopless and
they are unreachable unless they appear i n I. Hence, the constructed automaton
is also an M M A A . Figure 1(a) shows an M M A A produced by the translation of
formula G(Fs a A Fsb) V G6.
In fact, M M A A and L T L ( F S , Gs ) are expressively equivalent. T h e reverse
translation can be found i n the full version of this paper [3].
4 Translation of M M A A to T G D R A
In this section we present a translation of an M M A A A = (5, E, <$4, /, F) with
multitransition relation Aj^ into an equivalent T G D R A Q. A t first we build a
semiautomaton T and then we describe the transition based generalized R a b i n
acceptance condition Q1Z of Q.
4.1 Semiautomaton T
The idea of our seminautomaton construction is straightforward: a run a(w) of
the semiautomaton T tracks all runs of A over w. More precisely, the state of T
reached after reading a finite input consists of all possible configurations i n which
A can be after reading the same input. Hence, states of the semiautomaton are
sets of configurations of A and we call them macrostates. We use /, s, s±, S2, • • •
to denote states of A (/ stands for an accepting state of F), c, c i , C2,... to denote
configurations of A, and m, m\,mi,... to denote macrostates of T . Further, we
use t, ti, t i . . . to denote the transitions of A, T, TQ, T\... to denote multitransitions
of A, and r, r±, r i . . . to denote the transitions of T , which are called
macrotransitions hereafter.
Formally, we define the semiautomaton T = ( M , E, Sf, mi) for A as follows:
— M C 2 _ S
is the set macrostates, restricted to those reachable from the initial
macrostate m/ by 6-j-,
— ( m i , a , m 2 ) £ 5r iff m2 = {Jc<EmiW I ( c
: a
: c
' ) € A A } , i-e. for each m i £
M and a £ E, there is a single macrotransition ( m i , a, m?) £ Sj-, where
m-2 consists of target configurations of all a-multitransitions leading from
configurations i n m i , and
— m/ = / is the initial macrostate.
Figure 2 depicts the semiautomaton T for the M M A A of Figure 1(a). Each
row i n a macrostate represents one configuration.
Fig. 2. The semiautomaton T for the M M A A of Figure 1(a)
4.2 Acceptance Condition Q"R. of the T G D R A Q
For any subset Z C S, must(Z) denotes the set of must-states of Z. A n M M A A
run p is bounded by Z C 5 iff Infs(p) C Z and must(Infs(p)) = must(Z). For
example, the run of Figure 1(b) is bounded by the set {G?/>, Fa, F&}.
For any fixed z7 C 5, we define the set ACz Q 2 s
of allowed configurations
of .4 and the set A T ^ C 6-j- of allowed macrotransitions of T as follows:
ACz = {c C Z | must(c) = must(Z)}
ATZ = { ( m i , a , m 2 ) £ <5r | 3 d £ A C z , c 2 £ ( m 2 n A C z ) : ( c i , a , c 2 ) £ A A } 1
Clearly, a run p of A is bounded by Z if and only if p has a suffix containing only
configurations of ACz- Let p be a run over w with such a suffix. A s the semiautomaton
T tracks all runs of A over a given input, the run a(w) of T 'covers'
also p. Hence, a(w) has a suffix where, for each macrotransition (rrii, Wi, rrii+i),
there exist configurations c\ £ PI A C ^ and c2 £ m-i+i PI A C z satisfying
(ci,Wi,c2 ) £ Aj(. In other words, a(w) has a suffix containing only macrotransitions
of A T ^ . This observation is summarized by the following lemma.
Lemma 1. If A has a run overw bounded by Z, then the run a(w) ofT contains
a suffix of macrotransitions of ATz •
In fact, the other direction can be proved as well: if a(w) contains a suffix of
macrotransitions of A T ^ , then A has a run over w bounded by Z.
For each / £ F Pi Z, we also define the set A T ^ as the set of all macrotransitions
i n ATZ such that A contains a non-looping transition of / with the same
label and with the target configuration not leaving Z:
A T | = {(mi, a, m 2 ) £ ATZ | 3(/, a, c) £ SA : f £ c, c C Z}
Using the sets A T ^ and A T | , we define one generalized Rabin pair QTZz for
each subset of states Z C S:
gnz = (5T x ATZ, {ATf
z}feFnz) (1)
Lemma 2. If there is an accepting run p of A over w then the run a(w) of T
satisfies QTZz for Z = Infs(p).
1
A definition of ATz with ci £ (mi n ACz) would be more intuitive, but less effective.
Proof. A s p is bounded by Z, Lemma 1 implies that a(w) has a suffix r i T i + i . . .
of macrotransitions of A T ^ . Thus Inft(a(w)) Pi (S-j- \ AT^) = 0.
As Z = Infs(p) and p = TQT\ . . . is accepting, for each / £ F n Z, p includes
infinitely many multitransitions 1} where / £ dom(Tj) and Tj contains
a non-looping transition (f,Wj,c) £ 8A satisfying / g" c and c C Z . Hence, the
corresponding macrotransitions r j that are also in the mentioned suffix riTi+i . . .
of a(w) are elements of A T | . Therefore, Inft(a(w)) PI A T | ^ 0 for each f e FnZ
andCT(W)satisfies (57^z. •
L e m m a 3. 7/ a ran a(w) ofT satisfies QTZz then there is an accepting run of
A over w bounded by Z.
Proof. Let a(w) = ror\... be a run of T satisfying QTZz, i-e. a(w) has a suffix
of macrotransitions of ATz and a(w) contains infinitely many macrotransitions
of A T | for each / £ F n Z. Let = (rrii, Wi, rrii+\) be the first macrotransition
of the suffix. The definition of ATz implies that there is a configuration c £
rrii+i D ACz- T h e construction of T guaranties that there exists a sequence of
multitransitions of A leading to the configuration c. More precisely, there is a
sequence TQT\ .. .Ti such that dom(To) is an initial configuration of A, Tj is
labelled by Wj for each 0 < j < i, range(Tj) = d o m ( T j + i ) for each 0 < j < i,
and range(Ti) = c. We show that this sequence is i n fact a prefix of an accepting
run of A over w bounded by Z.
We inductively define a multitransition sequence T ; + i T ; + 2 . . . completing this
run. The definition uses the suffix ri+iri+2 . . . of a(w). Let us assume that j > i
and that range(Tj_i) is a configuration of ACz- We define Tj to contain one Wjtransition
of s for each s £ range(Tj_i). Thus we get dom(Tj) = range(Tj_i). A s
Tj £ A T ^ , there exists a multitransition T" labelled by Wj such that both source
and target configurations of T' are in ACz- For each must-state s £ range(Tj_i),
Tj contains the same transition leading from s as contained i n T". For maystates
/ £ range(Tj_i), we have two cases. If Tj £ A T | , TJ contains a nonlooping
transition leading from / to some states i n Z. T h e existence of such a
transition follows from the definition of A T ^ . For the remaining may-states, Tj
uses selfloops. Formally, Tj = {tj \ s £ range(Tj_i)}, where
3
(s, Wj, cs ) contained i n T" if s £ must(Z)
{s,Wj,{s}) if S £ F A Tj;<£ A T |
^ (s, Wj, cs) where cs C Z, s £ cs if s £ F A Tj £ A T |
One can easily check that range(Tj) £ ACz and we continue by building Tj+\.
To sum up, the constructed run is bounded by Z. Moreover, Tj contains
no looping transition of / whenever Tj £ A T | . A S the run a(w) is accepting,
Tj £ A T ^ holds infinitely often for each / £ F n Z. The constructed run of A
over w is thus accepting. •
The previous two lemmata give us the following theorem.
Theorem 1. The TGDRA Q = (T, {QTlz \ Z C S}) is equivalent to A.
5 Translation of T G D R A to D R A
This section presents a variant of the standard degeneralization procedure. A t
first we illustrate the idea on a T G D R A Q' = (M, E, 6-j-, mi, {(K, {L3
}\<j<h)})
with one generalized Rabin pair. Recall that a run is accepting if it has a suffix
not using macrotransitions of K and using macrotransitions of each L3
infinitely
often.
A n equivalent D R A V consists of h + 2 copies of Q'. The copies are called
levels. We start at the level 1. Intuitively, being at a level j for 1 < j < h
means that we are waiting for a transition from L3
. Whenever a transition of K
appears, we move to the level 0. A transition r g" K gets us from a level j to
the maximal level I > j such that r £ L3
for each j < j' < I. The levels 0 and
h + 1 have the same transitions (including target levels) as the level 1. A run of
Q1
is accepting if and only if the corresponding run of V visits the level 0 only
finitely often and it visits the level h + 1 infinitely often.
In general case, we track the levels for all generalized Rabin pair simultaneously.
Given a T G D R A Q = (M,E,5r-,mi,{(Ki,{L3
i}1<j<hi)}1<i<k), we
construct an equivalent D R A as V = (Q, E, 5T>, Qi, {{K[, LQ}i<i<fc), where
- Q = M x { 0 , 1 , . . . , hi+1} x • • • x { 0 , 1 , . . . , hfc+1},
- ((TO, l\,..., Ik), a, {m1
, l[,..., l'k)) G 6-D iff r = (m, a, m') £ Sj- and for each
1 < i < k it holds
( 0 if r £ Ki
I'i = I max{ii < I < hi+1 \Vh<j<l:reL{} if r <£ Ki A 1 < h < hi
[ m a x { l < I < hi+1 | VI < j < I : r e L{} if r <£ Ki A h £ {0, hi+1},
- qt = ( m / , l , . . . , l ) ,
- K'i = {(m, h,..., lk) £ Q | h = 0}, and
- L\ = {(m, h,... ,lk) e Q | h = hi + 1}.
6 C o m p l e x i t y
This section discusses the upper bounds of the individual steps of our translation
and compares the overall complexity to complexity of the other translations.
Given a formula ip of L T L ( F S , Gs ), we produce an M M A A with at most n
states, where n is the length of p. Then we build the T G D R A Q with at most
22
states and at most 2 n
generalized Rabin pairs. To obtain the D R A V, we
multiply the state space by at most \Z\ + 2 for each generalized Rabin pair QTZzThe
value of \Z\ is bounded by n. Altogether, we can derive an upper bound on
the number of states of the resulting D R A as
\Q\ < 2 2
" • (n + 2)2
" = 2 2
" . 2 2
" ' l o
^ ( " + 2
) = 2 2
" • 2 2
" +
' ° S 2
' o g 2 <
" + 2 )
£ 2
0
( 2
" + I o g I
° g
" ) ,
which is the same bound as in [19], but lower than 2 e
' ( 2
" + l o s
" ) of l t l 2 d s t a r .
It is worth mentioning that the number of states of our T G D R A is bounded by
2 2
' v l
while the number of states of the G D R A produced by Rabinizer is bounded
by 2 2 M
.2AP
^\
7 Simplifications and Translation Improvements
A n important aspect of our translation process is simplification of all intermediate
results leading to smaller resulting D R A .
We simplify input formulae by reduction rules of L T L 3 B A , see [4] for more
details. Additionally, we rewrite the subformulae of the form G F ^ and FGtp
to equivalent formulae GFsip and FGsip respectively. This preference of strict
temporal operators often yields smaller resulting automata.
Alternating automata are simplified in the same way as in L T L 2 B A : removing
unreachable states, merging equivalent states, and removing redundant
transitions, see [15] for details.
We improve the translation of an M M A A A to a T G D R A Q i n order to
reduce the number of generalized Rabin pairs of Q. One can observe that, for
any accepting run p of A, Infs(p) contains only states reachable from some muststate.
Hence, in the construction of acceptance condition of Q we can consider
only subsets Z of states of A of this form. Further, we omit a subset Z if, for
each accepting run over w bounded by Z, there is also an accepting run over w
bounded by some Z1
C Z. The formal description of subsets Z considered i n the
construction of the T G D R A Q is described in the full version of this paper [3].
If a run T0Ti... of an M M A A satisfies range(Ti) = 0 for some i, then Tj = 0
for all j > i and the run is accepting. We use this observation to improve
the construction of the semiautomaton T of the T G D R A Q: if a macrostate m
contains the empty configuration, we remove all other configurations from m.
After we build the T G D R A , we simplify its acceptance condition i n three
ways (similar optimizations are also performed by Rabinizer).
1. We remove some generalized Rabin pairs (Ki, { L | } j e j ; ) that cannot be satisfied
by any run, i n particular when Ki = Sj- or L\ = 0 for some j £ Ji.
2. We remove L\ if there is some I £ Ji such that L ' C L j .
3. If the fact that a run p satisfies the pair QTZz implies that p satisfies also
some other pair QTZz1
, we remove QTZzFinally,
we simplify the state spaces of both T G D R A and D R A such that we
iteratively merge the equivalent states. Two states of a D R A V are equivalent
if they belong to the same sets of the acceptance condition of V and, for each
a, their a-transitions lead to the same state. Two states of a T G D R A Q are
equivalent if, for each a, their a-transitions lead to the same state and belong
to the same sets of the acceptance condition of Q. Moreover, if the initial state
of V or Q has no selfloop, we check its equivalence to another state regardless of
the acceptance condition (note that a membership in acceptance condition sets
is irrelevant for states or transitions that are passed at most once by any run).
Of course, we consider only the reachable state space at every step.
8 B e y o n d L T L ( F S , G S ) Fragment: M a y / M u s t in the L i m i t
The Section 4 shows a translation of M M A A into T G D R A . In fact, our translation
can be used for a larger class of very weak alternating automata called
may/must in the limit automata ( l i m M M A A ) . A V W A A B is a l i m M M A A if
B contains only must-states, states without looping transitions, and co-Buchi
accepting states (not exclusively may-states), and each state reachable from a
must-state is either a must- or a may-state. Note that each accepting run of a
l i m M M A A has a suffix that contains either only empty configurations, or configurations
consisting of must-states and may-states reachable from must-states.
Hence, the M M A A to T G D R A translation produces correct results also for limM
M A A under an additional condition: generalized R a b i n pairs GHz are constructed
only for sets Z that contain only must-states and may-states reachable
from them.
We can obtain l i m M M A A by the L T L to V W A A translation of [15] when it
is applied to an L T L fragment defined as
ip ::= ip | ip V ip | ip A ip | Xp | ip U ip,
where ip ranges over L T L ( F S , G S ) . Note that this fragment is strictly more expressive
than L T L ( F S , G S ) .
9 E x p e r i m e n t a l Results
We have made an experimental implementation of our translation (referred to
as LTL3DRA). The translation of L T L to alternating automata is taken from
L T L 3 B A [4]. We compare the automata produced by L T L 3 D R A to those produced
by Rabinizer and l t l 2 d s t a r . A l l the experiments are run on a Linux
laptop (2.4GHz Intel Core i7, 8 G B of R A M ) with a timeout set to 5 minutes.
Tables given below (i) compare the sizes of the D R A produced by all the
tools and (ii) show the number of states of the generalized automata produced by
L T L 3 D R A and Rabinizer. Note that L T L 3 D R A uses T G D R A whereas Rabinizer
uses (state-based) G D R A , hence the numbers of their states cannot be directly
compared. The sizes of D R A are written as s(r), where s is the number of states
and r is the number of Rabin pairs. For each formula, the size of the smallest
D R A (measured by the number of states and, in the case of equality, by the
number of Rabin pairs) is printed in bold.
Table 1 shows the results on formulae from [14] extended with another parametric
formula. For the two parametric formulae, we give all the parameter
values n for which at least one tool finished before timeout. For all formulae
in the table, our experimental implementation generates automata of the same
or smaller size as the others. Especially in the case of parametric formulae, the
automata produced by L T L 3 D R A are considerably smaller. We also note that
the T G D R A constructed for the formulae are typically very small.
Table 2 shows the results on formulae from S P E C P A T T E R N S [13] (available
online2
). We only take formulae L T L 3 D R A is able to work with, i.e. the formulae
of the L T L fragment defined in Section 8. The fragment covers 27 out of 55
formulae listed on the web page. The dash sign in Rabinizer's column means
2
http://patterns.projects.cis.ksu.edu/documentation/patterns/ltl.shtml
Formula
L T L 3 D R A Rabinizer l t l 2 d s t a r
Formula
DRA T G D R A DRA GDRA DRA
G(oVF6)
FGa V FG6 V GFc
3(2)
8(3)
2
1
4(2) 5
8(3) 8
4(1)
8(3)
F(a V b) 2(1) 2 2(1) 2 2(1)
GF(aVb) 2(1) 1 2(1) 4 2(1)
G(aVFa) 2(1) 1 2(2) 2 2(1)
G ( a V 6 V c ) 2(1) 2 2(1) 8 3(1)
G(aV F(bVc)) 3(2) 2 4(2) 9 4(1)
F a V G b 3(2) 3 3(2) 3 4(2)
G(a V F(6 Ac)) 3(2) 2 4(2) 11 4(1)
FGa V GF6 4(2) 1 4(2) 4 4(2)
GF(aV&) A G F ( b V c ) 3(1) 1 3(1) 8 7(2)
(FFa A G-io) V (GG-.0 A Fa) 1(0) 1 1(0) 1 1(0)
GFa A FG6 3(1) 1 3(1) 4 3(1)
(GFaAFGb) V (FG -10 A GF-ib) 4(2) 1 4(2) 4 5(2)
FGa A GFa 2(1) 1 2(1) 2 2(1)
G(Fa A F6) 3(1) 1 3(1) 4 5(1)
Fa A F-io 4(1) 4 4(1) 4 4(1)
(G(b V GFa) A G(c V GF-.a)) V Gb V Gc 12(3) 4 18(4) 18 13(3)
(G(b V FGa) A G(c V FG-io)) V Gb V Gc 4(2) 4 6(3) 18 14(4)
(F(b A FGa) V F(c A FG-io)) A Fb A Fc 5(2) 4 5(2) 18 7(1)
(F(b A GFa) V F(c A GF-.a)) A Fb A Fc 5(2) 4 5(2) 18 7(2)
GF(Fa V GFb V FG(a V b))
FG(Fa V GFb V FG(a V b))
FG(Fa V GFb V FG(a V 6) V FGb)
4(3)
4(3)
4(3)
1
1
1
4(3) 4
4(3) 4
4(3) 4
14(4)
145(9)
145(9)
n = l 4(2) 1 4(2) 4 4(2)
A r = i ( G F a
» -*-GFbO
n = 2
n = 3
18(4)
166(8)
1
1
20(4) 16
470(8) 64
11324(8)
timeout
n = 4 7408(16) 1 timeout timeout
n=l 4(2) 1 4(2) 4 4(2)
n = 2 10(4) 1 11(4) 8 572(7)
A r = i ( G F a
» V F G a ! + i ) n = 3 36(6) 1 52(6) 16 290046(13)
n = 4 178(9) 1 1288(9) 32 timeout
n = 5 1430(14) 1 timeout timeout
n = 6 20337(22) 1 timeout timeout
Table 1. The benchmark from [14] extended by one parametric formula.
that Rabinizer cannot handle the corresponding formula as it is not from the
L T L ( F , G) fragment. For most of the formulae i n the table, L T L 3 D R A produces
the smallest D R A . In the remaining cases, the D R A produced by our translation
is only slightly bigger than the smallest one. The table also illustrates that
L T L 3 D R A handles many (pseudo)realistic formulae not included i n L T L ( F , G).
Experimental results for another four parametric formulae are provided i n
the full version of this paper [3].
L T L 3 D R A Rabinizer l t l 2 d s t a r
DRA TGDRA DRA GDRA DRA
f2 4(2) 4 — 5(2)
<P3 4(2) 3 4(2) 5 4(1)
ip7 4(2) 3 — 4(2)
<P8 3(2) 3 3(2) 5 4(2)
<pu 6(2) 6 — 10(3)
f l 2 8(2) 8 — 9(2)
f l 3 7(3) 7 — 11(3)
<P17 4(2) 4 — 5(2)
<Pl8 4(2) 3 4(2) 5 4(1)
f21 4(2) 3 — 4(2)
f22 4(2) 4 — 5(2)
<fi23 5(3) 4 — 5(3)
<fi26 3(2) 2 4(2) 5 4(1)
Table 2. The benchmark with selected
i­th formula on the web page.
L T L 3 D R A Rabinizer Itl2dstar
DRA TGDRA DRA GDRA DRA
<fi27 4(2; 4 — 5(2)
<fi28 6(3 3 8(3) 14 5(1)
<P31 4(2; 4 — 6(2)
<fi32 5(2; 5 — 7(2)
<fi33 5(2; 5 — 7(3)
<fi36 6(3 4 — 6(2)
<fi37 6(2; 6 — 8(3)
<fi38 7(4 5 — 6(3)
<fi41 21(3; 7 — 45(3)
f42 12(2; 12 — 17(2)
<fi46 15(3) 5 — 20(2)
<fi47 7(2 7 — 6(2)
<fi48 14(3; 6 — 24(2)
<P52 7(2 7 — 6(2)
from SPEC PATTERNS. ipi denotes the
10 Conclusi on
We present another Safraless translation of an L T L fragment to deterministic
Rabin automata ( D R A ) . O u r translation employs a new class of may/must alternating
automata. We prove that the class is expressively equivalent to the
LTL(FS , Gs ) fragment. Experimental results show that our translation typically
produces D R A of a smaller or equal size as the other two translators of L T L
(i.e. Rabinizer and l t l 2 d s t a r ) and it sometimes produces automata that are
significantly smaller.
References
1. R. Alur and S. L . Torre. Deterministic generators and games for L T L fragments.
ACM Trans. Comput. Log., 5(l):l­25, 2004.
2. T. Babiak, T. Badie, A . Duret­Lutz, M . Křetínský, and J. Strejček. Compositional
approach to suspension and other improvements to L T L translation. In SPIN 2013,
volume 7976 of LNCS, pages 81­98. Springer, 2013.
3. T. Babiak, F . Blahoudek, M . Křetínský, and J. Strejček. Effective translation
of L T L to deterministic rabin automata: Beyond the (F ,G)­fragment. CoRR,
abs/1306.4636, 2013.
4. T. Babiak, M . Křetínský, V . Řehák, and J. Strejček. L T L to Biichi automata
translation: F ast and more deterministic. In TACAS 2012, volume 7214 of LN CS,
pages 95­109. Springer, 2012.
5. C. Baier and J.­P. Katoen. Principles of Model Checking. M I T Press, 2008.
6. K . Chatterjee, A . Gaiser, and J. Křetínský. Automata with generalized Rabin
pairs for probabilistic model checking and L T L synthesis. In CAV 2013, volume
8044 of LNCS, pages 559­575. Springer, 2013.
7. A . Church. Logic, arithmetic, and automata. In Proceedings of the International
Congress of Mathematicians, pages 23-35. Institut Mittag-Leffler, 1962.
8. E. M . Clarke, O. Grumberg, and D. A . Peled. Model Checking. MIT Press, 1999.
9. C. Courcoubetis and M . Yannakakis. The complexity of probabilistic verification.
J. ACM, 42(4):857-907, 1995.
10. J . - M . Couvreur. On-the-fly verification of temporal logic. In FM 1999, volume
1708 of LNCS, pages 253-271. Springer, 1999.
11. M . Daniele, F. Giunchiglia, and M . Y . Vardi. Improved automata generation for
linear temporal logic. In CAV1999, volume 1633 of LNCS, pages 249-260. Springer,
1999.
12. A . Duret-Lutz. L T L translation improvements in Spot. In VECoS 2011, Electronic
Workshops in Computing. British Computer Society, 2011.
13. M . B. Dwyer, G. S. Avrunin, and J. C. Corbett. Patterns in property specifications
for finite-state verification. In ICSE 1999, pages 411-420. IEEE, 1999.
14. A . Gaiser, J. Kfetmsky, and J. Esparza. Rabinizer: Small deterministic automata
for LTL(F,G). In ATVA 2012, volume 7561 of LNCS, pages 72-76, 2012.
15. P. Gastin and D. Oddoux. Fast L T L to Biichi Automata Translation. In CAV
2001, volume 2102 of LNCS, pages 53-65. Springer, 2001.
16. J. Klein. Itl2dstar - L T L to deterministic Streett and Rabin automata,
http://www.Itl2dstar.de.
17. J. Klein and C. Baier. Experiments with deterministic a>-automata for formulas of
linear temporal logic. Theor. Comput. Sci., 363(2):182-195, 2006.
18. J. Klein and C. Baier. On-the-fly stuttering in the construction of deterministic
u- automata. In CI A A 2007, volume 4783 of LNCS, pages 51-61. Springer, 2007.
19. J. Kfetmsky and J. Esparza. Deterministic automata for the (F, G)-fragment of
LTL. In CAV 2012, volume 7358 of LNCS, pages 7-22. Springer, 2012.
20. O. Kupferman. Recent challenges and ideas in temporal synthesis. In SOFSEM
2012, volume 7147 of LNCS, pages 88-98. Springer, 2012.
21. M . Kwiatkowska, G. Norman, and D. Parker. P R I S M 4.0: Verification of probabilistic
real-time systems. In CAV 2011, volume 6806 of LNCS, pages 585-591.
Springer, 2011.
22. A . Morgenstern and K. Schneider. From L T L to symbolically represented deterministic
automata. In VMCAI 2008, volume 4905 of LNCS, pages 279-293. Springer,
2008.
23. N . Piterman. From nondeterministic Biichi and Streett automata to deterministic
parity automata. Logical Methods in Computer Science, 3(3), 2007.
24. N . Piterman, A . Pnueli, and Y. Sa'ar. Synthesis of reactive(l) designs. In VMCAI
2006, volume 3855 of LNCS, pages 364-380. Springer, 2006.
25. A . Pnueli. The temporal logic of programs. In FOCS 1977, pages 46-57. IEEE,
1977.
26. A . Pnueli and R. Rosner. On the synthesis of an asynchronous reactive module.
In ICALP 1989, volume 372 of LNCS, pages 652-671. Springer, 1989.
27. S. Safra. On the complexity of omega-automata. In FOCS 1988, pages 319-327.
IEEE Computer Society, 1988.
28. S. Schewe. Tighter bounds for the determinisation of Biichi automata. In FOSSACS
2009, volume 5504 of LNCS, pages 167-181. Springer, 2009.
29. F. Somenzi and R. Bloem. Efficient Biichi automata from L T L formulae. In CAV
2000, volume 1855 of LNCS, pages 248-263. Springer, 2000.
30. M . Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs.
In FOCS 1985, pages 327-338. I E E E Computer Society, 1985.
M . Y . Vardi and P. Wolper. A n automata-theoretic approach to automatic prog
verification. In LICS 1986, pages 332-344. I E E E Computer Society, 1986.
Comparison of L T L to Deterministic
Rabin Automata Translators*
František Blahoudek, Mojmír Křetínský, and Jan Strejček
Faculty of Informatics, Masaryk University, Brno, Czech Republic
{xbláhoud, kretinsky, strejcek}@f i .muni. cz
Abstract. Increasing interest in control synthesis and probabilistic model
checking caused recent development of L T L to deterministic a>­automata
translation. The standard approach represented by l t l 2 d s t a r tool
employs Safra's construction to determinize a Biichi automaton produced
by some L T L to Biichi automata translator. Since 2012, three new L T L to
deterministic Rabin automata translators appeared, namely Rabinizer,
LTL3DRA, and Rabinizer 2. They all avoid Safra's construction and
work on L T L fragments only. We compare performance and automata
produced by the mentioned tools, where l t l 2 d s t a r is combined with
several L T L to Biichi automata translators: besides traditionally used
LTL2BA, we also consider LTL­>NBA, LTL3BA, and Spot.
1 Introducti on
Linear temporal logic (LTL) has proved to be an appropriate formalism for specification
of systems behavior with major applications i n the area of model checking.
Methods for L T L model checking of probabilistic systems [29, 5, 3] and for
L T L synthesis [4, 24,19] mostly need to construct, for any given L T L formula,
a deterministic w­automaton. A s deterministic Biichi automata (DBA) cannot
express all the properties expressible in L T L , one has to choose deterministic toautomata
with a more complex acceptance condition. The most common choice
is the Rabin acceptance.
There are basically two approaches to translation of L T L to deterministic
w­automata. A traditional one translates L T L to nondeterministic Biichi automata
(N BA) first and then it employs Safra's construction [26] (or some of its
variants or alternatives like [23,27]) to obtain a deterministic automaton. This
approach is represented by the tool l t l 2 d s t a r [14] which uses an improved
Safra's construction [16,17]. A s every L T L formula can be translated into an
N B A and Safra's construction can transform any N B A to a deterministic Rabin
automaton (DRA), l t l 2 d s t a r works for the whole L T L . However, the resulting
automata are sometimes unnecessarily big.
Since 2012, several translations avoiding Safra's construction have been introduced.
The first one is presented in [18] and subsequently implemented in
* Authors are supported by The Czech Science F oundation, grant no. P202/10/1469.
the tool Rabinizer [10]. The algorithm builds a generalized deterministic Rabin
automaton (GDRA) directly from a formula. A D R A is then produced by
a degeneralization procedure. Rabinizer often produces smaller automata than
ltl2dstar. The main disadvantage is that it works for L T L ( F , G) only, i.e. the
L T L fragment containing eventually (F) and always (G) as the only temporal
operators. This method has been extended to a semantically larger fragment
and reimplemented in the experimental tool Rabinizer 2 [21]. In [1] we
present a Safraless translation working with another L T L fragment subsuming
L T L ( F , G). Our translator L T L 3 D R A transforms a given formula into a very
weak alternating automaton (in the same way as L T L 2 B A [11]) and then into
a transition-based generalized deterministic Rabin automaton (TGDRA). The
construction of generalized Rabin pairs of T G D R A is inspired by [18]. A D R A
is finally obtained by a degeneralization procedure.
Here we provide a comparison of performance of the L T L to D R A translators
ltl2dstar, Rabinizer, Rabinizer 2, and L T L 3 D R A . The tool ltl2dstar is
designed to use an external L T L to N B A translator. To our best knowledge, the
last experimental comparison of performance of ltl2dstar with different L T L
to N B A translators has been done in 2005 [15]. The comparison shows that with
respect to automata sizes, L T L 2 B A and L T L - > N B A [9] "have the lead and were
the only programs without failures to calculate the D R A . " Since 2005, significant
progress has been made in L T L to N B A translation (it can already be seen in the
comparison of L T L to N B A translators [25] published in 2007). Hence, we run
ltl2dstar with L T L 2 B A , L T L - > N B A , and contemporary translators Spot [6,
7] and L T L 3 B A [2]. The experimental results obtained are briefly interpreted.
2 C o m p a r e d Tools
Here we describe settings and restrictions of the considered translators.
- Itl2dstar [14] v0.5.1, http://www.ltl2dstar.de/
We keep the default setting (all optimizations enabled). We use only the option
—ltl2nba="<intf >: <tool> [@<params>] " to specify an external <tool>
for L T L to N B A translation (<intf> specifies if ltl2dstar communicates
with the <tool> via the interface of Ibtt [28] or Spin [13], and <params> are
parameters the <tool> is called with). We use four L T L to N B A translators:
• L T L - > N B A [9], http://www.ti.informatik.uni-kiel.de/~fritz/
We call it with —ltl2nba="lbtt: /pathtoLTL->NBA/script41btt .py".
• L T L 2 B A [11] vl.l,http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/
We call it with —ltl2nba="spin:/pathtoLTL2BA/ltl2ba".
• L T L 3 B A [2] vl.0.2, http://sourceforge.net/projects/ltl3ba/
B y default, L T L 3 B A aims to produce small N B A s . W i t h the option
-M, it aims to produce potentially larger, but more deterministic automata.
We have combined both modes with other optimizations provided
by L T L 3 B A . We have selected two settings with the best results,
namely —ltl2nba="spin:/pathtoLTL3BA/ltl3ba" referenced as
L T L 3 B A and — ltl2nba="spin:/pathtoLTL3BA/ltl3ba@-M - S " referenced
as L T L 3 B A d . Option -S enables strong fair simulation reduction.
II
• Spot [6,7] vl. 1.3, http://spot.lip6.fr/wiki/
Again, Spot can be set to produce either small or more deterministic
Buchi automata. We have combined ltl2dstar with both modes of Spot.
The resulting Rabin automata produced with the first mode are usually
identical to (and sometimes slightly bigger than) the automata produced
with the latter mode. Computation times are also similar. To save some
space, we include only the results for the "more deterministic" mode
invoked by —ltl2nba="spin:/pathtoSpot/ltl2tgba@-sD".
- Rabinizer [10] v O . l l , http://crab.in.tum.de/rabinizer/
Recall that Rabinizer works for LTL(F, G) only.
- Rabinizer 2 [21],
http://www.model.in.turn.de/~kret insk/rabinizer2.html
Rabinizer 2 works with formulae of a fragment called L T L \ G U which uses
not only F and G but also next (X) and until (U) temporal operators. The
fragment consists of formulae in the negation normal form (i.e. negations are
only in front of atomic propositions) such that no U is i n the scope of any G.
- L T L 3 D R A [1] v O . l , http://sourceforge.net/projects/ltl3dra/
This tool works with formulae of a slightly less expressive fragment than
L T L \ G U . More precisely, there is one more restriction on the scope of any
G: there are no U operators, and X can appear only in front of F or G, i.e. in
subformulae of the form XFcp or XGtp. We call this fragment L T L \ G U X .
The difference is not important for specification formulae of software and
asynchronous systems as these usually contain no X operators, but it can play
some role in specification formulae of hardware and synchronous systems.
Before we run the translators, we transform input formulae to the expected
format (prefix notation for ltl2dstar and negation normal form for Rabinizer 2)
using the tool l t l f i l t [7]. Note that Rabinizer, Rabinizer 2, and L T L 3 D R A are
called with default settings.
3 Experiments: B e n c h m a r k s and Results
A l l experiments were done on a server with 8 eight-core processors Intel® Xeon®
X7560, 2.26GHz, 448 G i B R A M and a 64-bit version of G N U / L i n u x . A l l the
translators are single-threaded. The timeout limit was set to 2 hours.
We run the tools on three benchmark sets: real specification formulae, parametric
formulae, and random formulae. The benchmark sets can be downloaded
from the web pages of L T L 3 D R A .
Real specification formulae We use specification formulae from two sources:
B E E M [22] and Spec Patterns [8]. After removing duplicates (typically cases
where an atomic proposition a is consistently replaced by its negation or by
a V b), we have 67 formulae. These formulae are divided into three classes: 12
formulae of LTL(F, G), 19 formulae of L T L \ G U X not included in LTL(F, G), and
36 formulae outside L T L \ G U X . Note that all the considered formulae outside
L T L \ G U X are also outside L T L \ G U .
Ill
Unlike standard model checking algorithms, applications requiring deterministic
w-automata usually need automata equivalent to specification formulae and
not to their negations. Hence, we do not negate the formulae before translation.
Table 1 presents cummulative results of the considered tools on the three
classes of specification formulae. Table 2 provides a cross-comparison of the tools
on the same formulae classes.
Class Measure
l t l 2 d s t a r
Rabinizer Rabinizer 2 L T L 3 D R AClass Measure
L T L - > N B A L T L 2 B A L T L 3 B A L T L 3 B A d Spot
Rabinizer Rabinizer 2 L T L 3 D R A
states 55 49 47 45 52 45 59 4 3
edges 186 171 158 1 5 1 167 187 287 161
formul
LTL(F,
pairs 18 18 1 7 1 7 1 7 22 18 21
formul
LTL(F,
m i n i m a l 3 7 7 8 3 1 0 7 1 0
formul
LTL(F,
time [s] 0.70 0 . 1 2 0.14 0.13 0.72 3.08 3.05 0 . 1 2
CN ^ m e m m a x 22.53 8 . 0 2 18.66 18.69 91.06 240.75 465.09 19.02
1 — 1
0
m e m avg 19.66 7 . 1 3 18.57 18.61 86.92 160.03 173.53 18.90
<° p
»
S ü
states 180 191 184 167 1 3 2 — 160 137
<° p
»
S ü
edges 614 699 671 563 3 9 0 — 827 546
<° p
»
S ü pairs 43 11 11 44 32 — 2 8 46
a j m i n i m a l 2 2 2 3 6 — 1 1 1 1
1—i
time [s] 2.83 0.24 0.32 0.30 2.11 — 5.98 0 . 1 9
1—i
m e m m a x 33.81 8 . 7 2 18.80 18.83 92.94 — 1013.89 19.50
0
m e m avg 22.29 7 . 4 4 18.67 18.72 87.95 — 256.50 19.13
states 34 985 135 250 33 927 2 768 3 8 6 — — —
more
LTL
edges 359 494 1 726 573 416 794 31 287 1 9 3 6 — — —
more
LTL
pairs 100 111 97 83 4 9 — — —
more
LTL
m i n i m a l 9 8 9 13 3 4 — — —
£ o time [s] 26.46 102.15 16.86 1 . 0 2 1.64 — — —
CO u
m e m m a x 463.95 1 406.86 345.52 2 4 . 4 1 93.69 — — —
m e m avg 35.34 65.53 27.77 1 8 . 9 0 89.29 — — —
Table 1. For each class of considered real formulae and for each tool, the table shows
cummulative numbers of states, edges, and accepting pairs of produced automata. Further,
we show the number of minimal automata produced by the tool (minimal means
that no other considered tool produced an automaton with less states for the same
formula). We also provide cummulative computation time (in seconds) and maximal
and average memory peaks (mem max and mem avg, measured in MiB) needed for the
construction of one automaton. The best results are emphasized.
4£ Tool
12 formulae c f L T L ( F , G) 19 more of L T L \ G U X 36 more of L T L
TT
Tool
1 2 3 4 5 6 7 8 V 1 2 3 4 5 7 8 V 1 2 3 4 5 V
1 H L T L - > N B A — 0 0 0 0 1 3 1 5 - 1 1 2 0 4 3 11 — 13 9 3 0 25
2 •p L T L 2 B A 6 — 0 0 5 1 5 1 18 4 — 0 1 0 4 3 12 1 2 — 0 2 0 14
3 Tl L T L 3 B A 6 1 - 0 5 1 5 1 19 4 1 — 1 0 4 3 13 14 14 — 4 0 32
4 L T L 3 B A d 6 1 1 - 6 1 5 1 21 4 2 2 - 0 5 4 17 22 17 13 — 2 54
5 H Spot 1 1 0 0 — 1 4 1 8 12 9 9 8 — 7 6 51 27 28 27 23 — 1 0 5
6 Rabinizer 8 4 4 3 8 - 5 1 33 —
7 Rabinizer 2 6 3 3 3 6 0 — 1 22 15 15 15 14 10 — 4 7 3 —
8 L T L 3 D R A 9 4 4 3 9 2 5 3 6 14 12 12 1 1 9 8 - 66 —
Table 2. Cross-comparison of considered tools on the three classes of real specification
formulae. The number in row indexed by r and column c represents in how many cases
the tool r produced a smaller automaton (in the number of states) than the tool c.
The column V shows the sum of these "victories".
IV
Parametric formulae We consider 8 parametric formulae of [12] and formulae
6(n) of [11] and F(n) of [18]:
E{n) = A H i F p i C i ( n ) = V 7 = 1 G F f t
(7(n) = ( . . . ( ( P l U p 2 ) U p 3 ) U . . . ) U p „ C 2 ( n ) = A r = i G F P i
R{n) = A L i l G F p i V F G p i + 1 ) Q(n) = A L i ( F
P i V G p i + 1 )
U2 (n) = P l U (p2 U (... (p„_! U p „ ) . . . ) ) S(n) = V?=i Gpi
= - ( ( A r = i G F P l ) -> G(q -> Fr)) F ( n ) = A " = i ( G F
P i -> G F f t )
The results are shown i n Table 3. Note that U(n) and L^fn) are not i n the
input fragment of Rabinizer. A l l the other formulae are from L T L ( F , G).
Formula
size l t ! 2 d s t a r
Rabinizer Rabinizer 2 L T L 3 D R AFormula
m a x L T L - > N B A L T L 2 B A L T L 3 B A L T L 3 B A d Spot
Rabinizer Rabinizer 2 L T L 3 D R A
E(n)
n = 9 5 1 2 5 1 2 5 1 2 5 1 2 5 1 2 5 1 2 5 1 2 5 1 2
E(n)
m a x n 9 11 11 11 1 2 10 9 10
U(n)
n = 5 1 7 1 7 1 7 1 7 1 7 — 1 7 24
U(n)
m a x n 10 5 6 10 1 2 — 9 9
R(n)
n = 3 375 631 290 046 483 789 2 347 15 980 52 97 36
R(n)
m a x n 3 3 3 4 3 4 3 6
U2(n)
n = 14 1 5 1 5 1 5 1 5 1 5 — 1 5 1 5
U2(n)
m a x n 15 15 15 15 15 — 1 9 14
C i ( n )
n = 7 129 2 2 2 3 128 128 2
C i ( n )
m a x n 11 23 23 23 22 8 7 2 4
C2(n)
n = 6 18 17 17 11 13 7 384 7
C2(n)
m a x n 8 11 1 7 1 7 16 8 6 15
Q{n)
n = 7 1331 1 140 1 140 1 140 736 5 7 8 5 7 8 2 790
Q{n)
m a x n 7 8 8 8 9 8 7 7
S{n)
n = 9 513 513 513 513 513 5 1 2 5 1 2 5 1 2
S{n)
m a x n 1 4 1 4 1 4 1 4 11 9 9 13
9(„) n = 5 21 20 15 5 444 5 444 11 480 7
9(„)
m a x n 7 10 1 9 6 6 7 5 14
F(n)
n = 2 13181 11 324 5 650 302 4 307 20 32 1 8
F(n)
m a x n 2 2 2 2 2 3 2 4
Table 3. For each parametric formula and each tool, the table provides the size (number
of states) of the automaton for the highest n such that all the considered tools finish
the computation within the limit (upper row), and the maximal n for which the tool
finishes the computation within the limit (lower row). The best values are emphasized.
R a n d o m formulae We use L T L formulae generator r a u d i t 1 [7] to get some
more formulae of length 15-30 from various fragments. More precisely, we generate
100 formulae from the L T L ( F , G) fragment, 100 general formulae with higher
occurence of F and G operators, and 100 formulae with uniformly distributed
operators. These three sets are generated by the respective commands:
- randltl -n 100 —tree-size=15..30 —ltl-priorities="ap=l,X=0,\
implies=0,false=0,true=0,R=0,equiv=0,U=0,W=0,M=0,xor=0" a b e d
- randltl -n 100 —tree-size=15..30 —ltl-priorities="ap=l,F=2,\
G=2,false=0,true=0,X=l,R=l,U=l,W=0,M=0,xor=0" a b e d
V
- randltl -n 100 —tree-size=15..30 —ltl-priorities="ap=l,\
false=0,true=0,W=0,M=0,xor=0" a b e d
We removed 10 formulae, out of the 300 generated ones, that were elementary
equivalent to true or false. The remaining formulae are divided into four classes
corresponding to the input L T L fragments of the considered tools: we have 97
formulae of L T L ( F , G), 29 formulae of L T L \ G U X not included i n L T L ( F , G),
1 formula of L T L \ G U not included i n L T L \ G U X , and 163 formulae not i n
L T L \ G U . Unfortunately, ltl2dstar combined with L T L - > N B A produces an
error message for one formula of L T L \ G U X and two formulae outside L T L \ G U .
These formulae were removed from the set. Further, there are 19 formulae (none
of them i n L T L \ G U ) , for which at least one tool does not finish before timeout.
These formulae are not included i n the cummulative results to make them
comparable, but we show the number of timeouts i n a separate line. To sum up,
Table 4 presents cummulative results for 97 formulae of L T L ( F , G), 28 formulae
of L T L \ G U X not included i n L T L ( F , G), and 142 formulae outside L T L \ G U
(plus the numbers of timeouts for another 19 formulae outside L T L \ G U ) . We do
not show the results on the single formula of L T L \ G U not included i n L T L \ G U X
due to their low statistical significance.
Table 5 contains a cross-comparison of the tools on the same formulae sets.
In this case, the formulae previously removed because of a timeout or a tool
failure are included.
Class Measure
l t ! 2 d s t a r
Rabinizer R a b i n . 2 L T L 3 D R AClass Measure
L T L - > N B A L T L 2 B A L T L 3 B A L T L 3 B A d Spot
Rabinizer R a b i n . 2 L T L 3 D R A
states 107 620 19 470 9914 6 008 13 940 5 1 1 741 618
edges 949 094 165 856 76 827 48 440 137 977 2 2 2 2 4 987 2 666
3 U." pairs 217 201 196 190 161 198 1 4 9 198
m i n i m a l 18 36 37 11 -11 5 4 26 44
time [s] 743.66 13.47 10.15 3.42 18.09 48.81 79.92 1 . 2 1
O o
m e m m a x 6 561.89 151.16 99.75 24.86 94.03 406.66 6 712.00 2 2 . 8 9
O o
m e m avg 95.72 8 . 9 0 19.51 18.77 89.27 205.10 632.62 19.23
go
states 1 183 6 670 6 375 1 509 633 — 4 5 1 512
go
edges 6 227 39 987 38 591 8 057 3 002 — 2 4 2 2 2 810
go pairs 66 68 69 54 4 8 — 71 70
S j m i n i m a l 9 11 13 15 17 — 11 1 8
oo h time [s] 15.86 1.11 1.49 0.76 5.01 — 40.34 0 . 5 0oo h
m e m m a x 107.75 45.83 41.53 1 9 . 5 8 94.17 — 33 224.44 34.59
0 m e m avg 39.80 9 . 2 3 19.63 18.87 89.72 — 1 761.70 20.07
states 173156 640 971 157 869 143 436 1 1 7 8 0 — — —
Q edges 1513 621 5 127962 1 103410 1 031 393 8 5 4 7 6 — — —
0
S J
pairs 523 625 499 438 3 5 4 — — —
2^ m i n i m a l 54 11 57 72 1 2 6 — — —
-1- ^ time [s] 421.79 384.54 76.33 70.38 1 6 . 8 0 — — —
~ o m e m m a x 1461.08 6 019.14 1 751.94 2 357.64 9 9 . 5 0 — — —
m e m avg 92.59 96.75 37.61 3 5 . 4 5 91.13 — — —
timeouts 8 17 6 2 1 — — —
Table 4. The cummulative results on random formulae. Semantics of the table is the
same as for Table 1. Moreover, the last line shows the number of timeouts of the tools
on additional 19 formulae outside L T L \ G U .
VI
4£ Tool
97 formulae of L T L ( F , G) 29 more of L T L \ G U X 163 more of L T L
rf 1 2 3 4 5 6 7 8 V 1 2 3 4 5 7 8 V 1 2 3 4 5 V
1 H L T L - > N B A — 13 10 6 2 10 35 17 93 - 4 5 4 1 6 6 26 — 79 43 38 16 176
2
cd
+J L T L 2 B A 44 — 5 4 9 12 41 22 137 14 — 3 2 0 12 6 37 38 - 13 22 7 80
3 L T L 3 B A 44 17 — 5 11 13 43 23 156 14 3 — 1 0 11 5 34 68 80 — 30 16 194
4 L T L 3 B A d 48 24 18 — 15 15 45 28 193 15 6 6 - 2 11 8 51 87 97 73 — 24 281
5 H Spot 52 31 26 16 — 19 46 32 222 18 8 9 7 - 15 8 65 106 115 99 74 — 3 9 4
6 Rabinizer 62 44 43 36 35 — 57 37 3 1 4 —
7 Rabinizer 2 42 23 19 20 19 2 — 26 151 17 10 10 6 7 — 5 55 —
8 L T L 3 D R A 58 43 40 33 35 13 47 — 269 17 11 12 10 9 14 — 7 3 —
Table 5. Cross-comparison of the considered tools on random formulae classes. The
table has a similar semantics to Table 2: each number says in how many cases the tool
in the corresponding row produces a better result than the tool in the corresponding
column. A n automaton is better than other if it has less states. Any automaton is
better than timeout or a tool failure. Timeouts and failures are seen as equivalent
results here.
4 Observations
For each pair of tools, there are some formulae in our benchmarks, for which one
tool produces strictly smaller automata than the other (see Table 5). Hence, no
tool is fully dominated by another.
A l l the results for LTL(F, G) fragment show that the Safraless tools (especially
Rabinizer and L T L 3 D R A ) usually perform better than ltl2dstar equipped with
any of the considered L T L to N B A translators. The best results for formulae
of L T L \ G U X not included in LTL(F, G) are typically achived by ltl2dstar
combined with Spot, and the Safraless tools Rabinizer 2 and L T L 3 D R A . For
formulae outside L T L \ G U , the current Safraless tools are not applicable. For
these formulae, by far the best results are produced by ltl2dstar combined
with Spot.
The results also provide information about particular tools or relations between
them. For example, one can immediately see that Rabinizer outperforms
Rabinizer 2 on LTL(F, G) formulae. This is explained by an experimental nature
of the current version of Rabinizer 2. In particular, the tool misses some
optimizations implemented in Rabinizer [20]. Further, one can observe that Rabinizer
performs significantly better than the other tools on random formulae of
LTL(F, G), while it is just comparable on real specification and parametric formulae
of LTL(F, G). We assume that this is due to the fact that Rabinizer builds
automata state-spaces according to semantics of L T L formulae rather than their
syntax. Thus it does not distinguish between equivalent subformulae which more
often appear in random formulae than in formulae written manually.
If we focus on usage of system resources, we observe that L T L 3 D R A is often
the fastest tool. The results also show that ltl2dstar in combination with
L T L 2 B A or L T L 3 B A has usually the lowest memory consumption.
During our experimentation we found out that ltl2dstar does not check
whether an intermediate Biichi automaton is already deterministic or not: it
VII
runs Safra's construction in all cases. Running Safra's construction only on nondeterministic
B A is profitable for two reasons:
1. Computation of Safra's construction is expensive.
2. Each deterministic B A can be directly converted into a D R A with one R a bin
pair without any change in the state space, while Safra's construction
typically produces a D R A larger than the intermediate deterministic B A .
For example, given the formula G(pi —> G-1P2), both Spot and L T L 3 B A d produce
a deterministic B A with two states (and a partial transition function). A l l
considered L T L to D R A translators output D R A with four states (and total
transition functions), Rabinizer 2 even yields a D R A with five states. Hence, the
automaton produced by Spot or L T L 3 B A d is smaller even after the addition of
one state to make its transition function total.
5 Conclusi ons
We conclude that the situation with L T L to D R A translation changed substantially
since 2005. The former leading combinations of ltl2dstar with L T L ­ > N B A
or L T L 2 B A are now surpassed by Safraless tools (on relevant fragments) and
ltl2dstar with Spot. However, there is still a space for further improvements.
Acknowledgements. We would like to thank Alexandre Duret­Lutz for valuable
suggestions and comments on a draft of this paper.
References
1. T. Babiak, F . Blahoudek, M . Křetínský, and J. Strejček. Effective translation of
LTL to deterministic Rabin automata: Beyond the (F ,G)­fragment. In ATVA '13,
volume 8172 of LN CS, pages 24­39. Springer, 2013.
2. T. Babiak, M . Křetínský, V . Řehák, and J. Strejček. L T L to Biichi automata
translation: F ast and more deterministic. In TACAS'12, volume 7214 of LN CS,
pages 95­109. Springer, 2012.
3. C. Baier and J.­P. Katoen. Principles of Model Checking. M I T Press, 2008.
4. A . Church. Logic, arithmetic, and automata. In ICM'62, pages 23­35. Institut
Mittag­Leffler, 1962.
5. C. Courcoubetis and M . Yannakakis. The complexity of probabilistic verification.
J. ACM, 42(4):857­907, 1995.
6. A . Duret­Lutz. L T L translation improvements in Spot. In VECoS'll, Electronic
Workshops in Computing. British Computer Society, 2011.
7. A . Duret­Lutz. Manipulating L T L formulas using Spot 1.0. In ATVA'13, volume
8172 of LN CS, pages 451­454. Springer, 2013.
8. M . B. Dwyer, G. S. Avrunin, and J. C. Corbett. Patterns in property specifications
for finite­state verification. In ICSE'99, pages 411­420. IEEE, 1999.
9. C. F ritz. Constructing Biichi automata from linear temporal logic using simulation
relations for alternating Biichi automata. In CIAA '03, volume 2759 of LNCS, pages
35­48. Springer, 2003.
V I I I
10. A . Gaiser, J. Kfetmsky, and J. Esparza. Rabinizer: Small deterministic automata
for LTL(F,G). In ATVA '12, volume 7561 of LNCS, pages 72-76, 2012.
11. P. Gastin and D. Oddoux. Fast L T L to Biichi Automata Translation. In CAV'01,
volume 2102 of LNCS, pages 53-65. Springer, 2001.
12. J. Geldenhuys and H . Hansen. Larger automata and less work for L T L model
checking. In SPIN'06, volume 3925 of LNCS, pages 53-70. Springer, 2006.
13. G . Holzmann. The Spin model checker: primer and reference manual. AddisonWesley
Professional, first edition, 2003.
14. J. Klein. Itl2dstar - L T L to deterministic Streett and Rabin automata,
http://www.Itl2dstar.de.
15. J. Klein. Linear time logic and deterministic omega-automata. Master's thesis,
University of Bonn, 2005.
16. J. Klein and C. Baier. Experiments with deterministic a>-automata for formulas of
linear temporal logic. Theor. Comput. Sci., 363(2):182-195, 2006.
17. J. Klein and C. Baier. On-the-fly stuttering in the construction of deterministic
w-automata. In CIAA'07, volume 4783 of LNCS, pages 51-61. Springer, 2007.
18. J. Kfetmsky and J. Esparza. Deterministic automata for the (F, G)-fragment of
LTL. In CAV'12, volume 7358 of LNCS, pages 7-22. Springer, 2012.
19. O. Kupferman. Recent challenges and ideas in temporal synthesis. In SOFSEM'12,
volume 7147 of LNCS, pages 88-98. Springer, 2012.
20. J. Kfetmsky. Personal communication, 2013.
21. J. Kfetmsky and R. L. Garza. Rabinizer 2: Small deterministic automata for
L T L \ G U . In ATVA'13, volume 8172 of LNCS, pages 446-450. Springer, 2013.
22. R. Pelanek. Beem: Benchmarks for explicit model checkers. In SPIN'07, volume
4595 of LNCS, pages 263-267. Springer, 2007.
23. N . Piterman. From nondeterministic Biichi and Streett automata to deterministic
parity automata. Logical Methods in Computer Science, 3(3), 2007.
24. A . Pnueli and R. Rosner. On the synthesis of an asynchronous reactive module.
In ICALP'89, volume 372 of LNCS, pages 652-671. Springer, 1989.
25. K . Y. Rozier and M . Y. Vardi. L T L Satisfiability Checking. In SPIN'07, volume
4595 of LNCS, pages 149-167. Springer, 2007.
26. S. Safra. On the complexity of omega-automata. In FOCS'88, pages 319-327.
IEEE Computer Society, 1988.
27. S. Schewe. Tighter bounds for the determinisation of Biichi automata. In FOSSACS'09,
volume 5504 of LNCS, pages 167-181. Springer, 2009.
28. H . Tauriainen and K. Heljanko. Testing L T L formula translation into Biichi automata.
International Journal on Software Tools for Technology Transfer (STTT),
4(l):57-70, 2002.
29. M . Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs.
In FOCS'85, pages 327-338. I E E E Computer Society, 1985.
I X