J. R. Büchi, On a Decision Method in Restricted Second Order Arithmetic, International Congress on Logic, Method and Philosophy of Science, pp.1-12, 1962.
DOI : 10.1007/978-1-4613-8928-6_23

C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis, Memory-efficient algorithms for the verification of temporal properties. Formal methods in system design, pp.275-288, 1992.

M. Daniele, F. Giunchiglia, and M. Vardi, Improved Automata Generation for Linear Temporal Logic, Computer Aided Verification (CAV'99), volume 1633 of Lecture Notes in Computer Science, pp.249-260, 1999.
DOI : 10.1007/3-540-48683-6_23

C. Fritz, Constructing B??chi Automata from Linear Temporal Logic Using Simulation Relations for Alternating B??chi Automata, 8th Intl. Conf. Implementation and Application of Automata, pp.35-48, 2003.
DOI : 10.1007/3-540-45089-0_5

C. Fritz and T. Wilke, State Space Reductions for Alternating B??chi Automata Quotienting by Simulation Equivalences, 22nd Conf. Foundations of Software Technology and Theoretical Computer Science, pp.157-168, 2002.
DOI : 10.1007/3-540-36206-1_15

P. Gastin and D. Oddoux, Fast LTL to Büchi automata translation, 13th Intl. Conf. Computer Aided Verification (CAV'01), number 2102 in Lecture Notes in Computer Science, pp.53-65, 2001.

R. Gerth, D. Peled, M. Vardi, and P. Wolper, Simple On-the-fly Automatic Verification of Linear Temporal Logic, Protocol Specification, Testing, and Verification, pp.3-18, 1995.
DOI : 10.1007/978-0-387-34892-6_1

G. Holzmann, The model checker SPIN, IEEE Transactions on Software Engineering, vol.23, issue.5, pp.279-295, 1997.
DOI : 10.1109/32.588521

O. Kupferman and M. Y. Vardi, Weak alternating automata are not so weak, 5th Israeli Symposium on Theory of Computing and Systems, pp.147-158, 1997.

C. Löding and W. Thomas, Alternating Automata and Logics over Infinite Words, IFIP Intl. Conf. Theoret. Comp. Sci, pp.521-535, 2000.
DOI : 10.1007/3-540-44929-9_36

S. Miyano and T. Hayashi, Alternating finite automata on ??-words, Theoretical Computer Science, vol.32, issue.3, pp.321-330, 1984.
DOI : 10.1016/0304-3975(84)90049-5

D. E. Muller, A. Saoudi, and P. E. Schupp, Alternating automata, the weak monadic theory of the tree, and its complexity, 13th ICALP, pp.275-283, 1986.
DOI : 10.1007/3-540-16761-7_77

D. E. Muller, A. Saoudi, and P. E. Schupp, Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time, [1988] Proceedings. Third Annual Information Symposium on Logic in Computer Science, pp.422-427, 1988.
DOI : 10.1109/LICS.1988.5139

S. Rohde, Alternating automata and the temporal logic of ordinals, 1997.

A. P. Sistla and E. M. Clarke, The complexity of propositional linear temporal logics, Journal of the ACM, vol.32, issue.3, pp.733-749, 1985.
DOI : 10.1145/3828.3837

F. Somenzi, CUDD: CU decision diagram package, release 2.3.1

F. Somenzi and R. Bloem, Efficient Büchi automata from LTL formulae, 12th Intl. Conf. Computer Aided Verification, pp.257-263, 2000.

R. E. Tarjan, Depth-First Search and Linear Graph Algorithms, SIAM Journal on Computing, vol.1, issue.2, pp.146-160, 1972.
DOI : 10.1137/0201010

M. Vardi, Verification of concurrent programs: the automata-theoretic framework*, Proceedings of the Second Symposium on Logic in Computer Science, pp.167-176, 1987.
DOI : 10.1016/0168-0072(91)90066-U

M. Y. Vardi, Alternating automata and program verification, In Computer Science Today Lecture Notes in Computer Science, vol.1000, pp.471-485, 1995.
DOI : 10.1007/BFb0015261

M. Y. Vardi and P. Wolper, Reasoning about Infinite Computations, Information and Computation, vol.115, issue.1, pp.1-37, 1994.
DOI : 10.1006/inco.1994.1092