A. E. Salem, A. Duret-lutz, and F. Kordon, Generalized Büchi automata versus testing automata for model checking, Proc. of SUMo'11, pp.65-79

A. E. Salem, A. Duret-lutz, and F. Kordon, Model Checking using Generalized Testing Automata. Transactions on Petri Nets and Other Models of Concurrency, ToPNoC VI), vol.7400, pp.94-122, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00855991

J. Couvreur, On-the-fly verification of temporal logic, Proc. of FM'99, pp.253-271

A. Duret-lutz and D. Poitrenaud, SPOT: an extensible model checking library using transition-based generalized buchi automata, The IEEE Computer Society's 12th Annual International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems, 2004. (MASCOTS 2004). Proceedings., pp.76-83
DOI : 10.1109/MASCOT.2004.1348184
URL : https://hal.archives-ouvertes.fr/hal-01496158

K. Etessami, Stutter-Invariant Languages, ??-Automata, and Temporal Logic, Proc. of CAV'99, pp.236-248
DOI : 10.1007/3-540-48683-6_22

J. Geldenhuys and H. Hansen, Larger Automata and Less Work for LTL Model Checking, Proc. of SPIN'06, pp.53-70
DOI : 10.1007/3-540-56922-7_33
URL : http://www.cs.tut.fi/~hansen/thesis/GH2006.pdf

D. Giannakopoulou and F. Lerda, From States to Transitions: Improving Translation of LTL Formulae to B??chi Automata, Proc. of FORTE'02, pp.308-326
DOI : 10.1007/3-540-36135-9_20

H. Hansen, W. Penczek, and A. Valmari, Stuttering-Insensitive Automata for On-the-fly Detection of Livelock Properties, Proc. of FMICS'02
DOI : 10.1016/S1571-0661(04)80411-0

M. Heiner, D. Gilbert, and R. Donaldson, Petri Nets for Systems and Synthetic Biology, Proc. of SFM'08, pp.215-264
DOI : 10.1007/978-3-540-68894-5_7
URL : http://www.brc.dcs.gla.ac.uk/~drg/publications/tutorials/bertinoro.pdf

J. Hugues, Y. Thierry-mieg, F. Kordon, L. Pautet, S. Barrir et al., On the Formal Verification of Middleware Behavioral Properties, Proc. of FMICS'04, pp.139-157
DOI : 10.1016/j.entcs.2004.08.062
URL : https://hal.archives-ouvertes.fr/hal-01520379

/. Move and . Lrde, The Spot home page: http://spot, 2014.

D. Peled and T. Wilke, Stutter-invariant temporal properties are expressible without the next-time operator, Information Processing Letters, vol.63, issue.5, pp.243-246, 1995.
DOI : 10.1016/S0020-0190(97)00133-6
URL : http://www.dcs.warwick.ac.uk/~doron/ps/stutter.ps

R. Sebastiani and S. Tonetta, more deterministic" vs. "smaller" Büchi automata for efficient LTL model checking, Proc. of CHARME'03, pp.126-140

H. Tauriainen, Automata and Linear Temporal Logic: Translation with Transition-based Acceptance, 2006.

M. Y. Vardi, Automata-theoretic model checking revisited, Proc. of VMCAI'07
DOI : 10.1007/978-3-642-01702-5_2
URL : https://link.springer.com/content/pdf/10.1007%2F978-3-642-01702-5_2.pdf