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
Memory-efficient algorithms for the verification of temporal properties. Formal methods in system design, pp.275-288, 1992. ,
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
Optimizing Büchi automata, Concurrency Theory: 11th International Conference, volume 1877 of Lect. Notes in Comp. Sci, pp.153-167, 2000. ,
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. ,
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. ,
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. ,
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
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
The model checker SPIN, IEEE Transactions on Software Engineering, vol.23, issue.5, pp.279-295, 1997. ,
DOI : 10.1109/32.588521
An analysis of bitstate hashing. Formal Methods in System Design, pp.289-307, 1998. ,
The model checker SPIN, IEEE Transactions on Software Engineering, vol.23, issue.5, 2003. ,
DOI : 10.1109/32.588521
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
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
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
Alternating automata and the temporal logic of ordinals, 1997. ,
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
Efficient Büchi automata from LTL formulae, 12th Intl. Conf. Computer Aided Verification, pp.257-263, 2000. ,
Depth-First Search and Linear Graph Algorithms, SIAM Journal on Computing, vol.1, issue.2, pp.146-160, 1972. ,
DOI : 10.1137/0201010
On translating linear temporal logic into alternating and nondeterministic automata, Research Report Comp. Sci, vol.83, 2003. ,
Nested emptiness search for generalized Büchi automata, 4th Intl. Conf. Application of Concurrency to System Design, pp.165-174, 2004. ,
Languages, Automata, and Logic, Handbook of Formal Language Theory, pp.389-455, 1997. ,
DOI : 10.1007/978-3-642-59126-6_7
Alternating automata and program verification, Computer Science Today Lect. Notes in Comp. Sci, vol.1000, pp.471-485, 1995. ,
DOI : 10.1007/BFb0015261