Paper Info
Title
Experiments with Deterministic omega-Automata for Formulas of Linear Temporal Logic.
Abstract
This paper addresses the problem of generating deterministic ω-automata for formulas of linear temporal logic, which can be solved by applying well-known algorithms to construct a nondeterministic Büchi automaton for the given formula on which we then apply a determinization algorithm. We study here in detail Safra's determinization algorithm, present several heuristics that attempt to decrease the size of the resulting automata and report on experimental results.
Year
DOI
Venue
2006
10.1016/j.tcs.2006.07.022
Theoretical Computer Science
Keywords
DocType
Volume
Determinization,Safra's algorithm,ω-Automata,LTL,Deterministic Rabin/Streett automata
Journal
363
Issue
ISSN
Citations 
2
0304-3975
13
PageRank 
References 
Authors
1.14
15
2
Name
Order
Citations
PageRank
Joachim Klein11189.33
Christel Baier23053185.85