D. Bianculli, P. Spoletini, A. Morzenti, M. Pradella, and P. San Pietro. Model checking temporal metric specifications with Trio2Promela. In FSEN'07, Proc. of the International Symposium on Fundamentals of Software Engineering, 2007.
A. Gargantini and A. Morzenti. Automated deductive requirements analysis of critical systems. ACM Trans. Softw. Eng. Methodol., 10(3):255-307, 2001.
P. Gastin and D. Oddoux. Fast LTL to Büchi automata translation. In CAV'01, volume 2102 of LNCS, pages 53-65, 2001.
G. J. Holzmann. The model checker SPIN. IEEE Trans. Softw. Eng., 23(5):279-295, 1997.
O. Kupferman and M. Vardi. Weak alternating automata are not that weak. In ISTCS'97, pages 147-158. IEEE Computer Society Press, 1997.
D. Mandrioli, S. Morasca, and A. Morzenti. Generating test cases for real-time systems from logic specifications. ACM Trans. Comput. Syst., 13(4):365-398, 1995.
A. Morzenti, D. Mandrioli, and C. Ghezzi. A model parametric real-time logic. ACM Trans. Program. Lang. Syst., 14(4):521-573, 1992.
A. Morzenti, M. Pradella, P. San Pietro, and P. Spoletini. Model checking TRIO specifications in Spin. In FME 2003, volume 2805 of LNCS, pages 542-561, 2003.
M. Pradella, P. San Pietro, P. Spoletini, and A. Morzenti. Practical model checking of LTL with past. In ATVA03: 1st Workshop on Automated Technology for Verification and Analysis, 2003.
F. Somenzi and R. Bloem. Efficient Büchi automata from LTL formulae. In CAV'00, volume 1855 of LNCS, pages 248-263, 2000.
