R. E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, vol.35, issue.8, pp.35677-691, 1986.
DOI : 10.1109/TC.1986.1676819

C. Courcoubetis, M. Y. 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. Y. Vardi, Improved Automata Generation for Linear Temporal Logic, 11th Intl. Conf. Computer Aided Verification (CAV'99), volume 1633 of Lect. Notes in Comp. Sci, pp.249-260, 1999.
DOI : 10.1007/3-540-48683-6_23

K. Etessami and G. Holzmann, Optimizing Büchi automata, Concurrency Theory: 11th International Conference, volume 1877 of Lect. Notes in Comp. Sci, pp.153-167, 2000.

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 (CIAA 2003), volume 2759 of Lect. Notes in Comp. Sci, pp.35-48, 2003.

C. Fritz and T. Wilke, State space reductions for alternating Büchi automata: Quotienting by simulation equivalences, 22nd Conf. Found. Software Tech. and Theor. Comp. Sci. (FSTTCS 2002), volume 2556 of Lect. Notes in Comp. Sci, pp.157-168, 2002.

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

J. Geldenhuys and A. Valmari, Tarjan???s Algorithm Makes On-the-Fly LTL Verification More Efficient, 10th Intl. Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp.205-219, 2004.
DOI : 10.1007/978-3-540-24730-2_18

R. Gerth, D. Peled, M. Y. 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

G. Holzmann, An analysis of bitstate hashing. Formal Methods in System Design, pp.289-307, 1998.

G. Holzmann, The model checker SPIN, IEEE Transactions on Software Engineering, vol.23, issue.5, 2003.
DOI : 10.1109/32.588521

Y. Kesten and A. Pnueli, Verifying Liveness by Augmented Abstraction, Computer Science Logic (CSL'99), volume 1683 of Lect. Notes in Comp. Sci, pp.141-156, 1999.
DOI : 10.1007/3-540-48168-0_11

C. Löding and W. Thomas, Alternating Automata and Logics over Infinite Words, IFIP Intl. Conf. Theor. Comp. Sci. (TCS 2000), volume 1872 of Lect. Notes in Comp. Sci, pp.521-535, 2000.
DOI : 10.1007/3-540-44929-9_36

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.

K. Schneider, Yet Another Look at LTL Model Checking, Conf. Correct Hardware Design and Verification Methods (CHARME'99), volume 1703 of Lect. Notes in Comp. Sci, pp.321-326, 1999.
DOI : 10.1007/3-540-48153-2_25

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

H. Tauriainen, On translating linear temporal logic into alternating and nondeterministic automata, Research Report Comp. Sci, vol.83, 2003.

H. Tauriainen, Nested emptiness search for generalized Büchi automata, 4th Intl. Conf. Application of Concurrency to System Design, pp.165-174, 2004.

W. Thomas, Languages, Automata, and Logic, Handbook of Formal Language Theory, pp.389-455, 1997.
DOI : 10.1007/978-3-642-59126-6_7

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