M. Abadi, L. Lamport, and P. Wolper, Realizable and unrealizable specifications of reactive systems, Proc. ICALP, pp.1-17, 1989.
DOI : 10.1007/BFb0035748

T. Aoshima, K. Sakuma, and N. Yonezaki, An efficient verification procedure supporting evolution of reactive system specifications, Proceedings of the 4th international workshop on Principles of software evolution , IWPSE '01, pp.182-185, 2001.
DOI : 10.1145/602461.602505

A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu, Symbolic Model Checking without BDDs, Proc. TACAS, pp.193-207, 1999.
DOI : 10.1007/3-540-49059-0_14
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.42.8033

A. Cimatti, E. M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore et al., NuSMV 2: An OpenSource Tool for Symbolic Model Checking, Proc. CAV, pp.359-364, 2002.
DOI : 10.1007/3-540-45657-0_29
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.107.8023

N. Eén and N. Sörensson, An extensible sat-solver, Proc. SAT, pp.502-518, 2003.

S. Hagihara and N. Yonezaki, Completeness of verification methods for approaching to realizable reactive specifications, Proc. Asian Working Conference on Verified Software, pp.242-257, 2006.

K. Heljanko, T. A. Junttila, M. Keinänen, M. Lange, and T. Latvala, Bounded model checking for weak alternating Büchi automata, Proc. CAV, pp.95-108, 2006.
DOI : 10.1007/11817963_12
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.71.7759

D. Jackson, Software Abstractions: Logic, Language, and Analysis, 2006.

B. Jobstmann and R. Bloem, Optimizations for LTL Synthesis, 2006 Formal Methods in Computer Aided Design, pp.117-124, 2006.
DOI : 10.1109/FMCAD.2006.22
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.150.425

R. Mori and N. Yonezaki, Several realizability concepts in reactive objects, Proc. Information Modeling and Knowledge Bases IV: Concepts, Methods and Systems, pp.407-424, 1993.

R. Mori and N. Yonezaki, Derivation of the input conditional formula from a reactive system specification in temporal logic, Proc. Formal Techniques in Real-Time and Fault-Tolerant Systems, pp.567-582, 1994.
DOI : 10.1007/3-540-58468-4_184

A. Pnueli and R. Rosner, On the synthesis of a reactive module, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '89, pp.179-190, 1989.
DOI : 10.1145/75277.75293

S. Schewe and B. Finkbeiner, Bounded Synthesis, Proc. ATVA, pp.474-488, 2007.
DOI : 10.1007/978-3-540-75596-8_33

M. Sheeran, S. Singh, and G. Stålmarck, Checking Safety Properties Using Induction and a SAT-Solver, Proc. FMCAD, pp.108-125, 2000.
DOI : 10.1007/3-540-40922-X_8

D. Sheridan, Bounded Model Checking with SNF, Alternating Automata, and B??chi Automata, Electronic Notes in Theoretical Computer Science, vol.119, issue.2, pp.83-101, 2005.
DOI : 10.1016/j.entcs.2004.12.024
URL : http://doi.org/10.1016/j.entcs.2004.12.024

M. Shimakawa, S. Hagihara, and N. Yonezaki, Complexity of Checking Strong Satisfiability of Reactive System Specifications, Proc. International Conference on Advances in Information Technology and Communication, pp.42-51, 2012.
DOI : 10.1007/978-3-540-37621-7_8