Alur, R., Dill, D.L.: A theory of timed automata. Theoreotical Computer Science 126(2), 183-235 (1994)
Basin, D., Klaedtke, F.,Marinovic, S., Zǎlinescu, E.: Monitoring of temporal first-order properties with aggregations. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 40-58. Springer, Heidelberg (2013)
Bersani, M.M., Frigeri, A., Morzenti, A., Pradella, M., Rossi, M., San Pietro, P.: Bounded reachability for temporal logic over constraint systems. In: Proc. of TIME 2010, pp. 43-50. IEEE Computer Society (2010)
Bersani, M.M., Frigeri, A., Rossi, M., San Pietro, P.: Completeness of the bounded satisfiability problem for constraint LTL. In: Delzanno, G., Potapov, I. (eds.) RP 2011. LNCS, vol. 6945, pp. 58-71. Springer, Heidelberg (2011)
Bersani, M.M., Rossi, M., Pietro, P.S.: Deciding continuous-time metric temporal logic with counting modalities. In: Abdulla, P.A., Potapov, I. (eds.) RP 2013. LNCS, vol. 8169, pp. 70-82. Springer, Heidelberg (2013)
Bersani, M.M., Rossi, M., San Pietro, P.: On the satisfiability of metric temporal logics over the reals. In: Proc. of AVOCS 2013 (2013)
Bianculli, D., Ghezzi, C., Pautasso, C., Senti, P.: Specification patterns from research to industry: a case study in service-based applications. In: Proc. of ICSE 2012, pp. 968-976. IEEE Computer Society (2012)
Bianculli, D., Ghezzi, C., San Pietro, P.: The tale of SOLOIST: a specification language for service compositions interactions. In: Pǎsǎreanu, C.S., Salaün, G. (eds.) FACS 2012. LNCS, vol. 7684, pp. 55-72. Springer, Heidelberg (2013)
Biere, A., Heljanko, K., Junttila, T.A., Latvala, T., Schuppan, V.: Linear encodings of bounded LTL model checking. Logical Methods in Computer Science 2(15) (2006)
Burattin, A., Sperduti, A.: PLG: A framework for the generation of business process models and their execution logs. In: Muehlen, M.z., Su, J. (eds.) BPM 2010 Workshops. LNBIP, vol. 66, pp. 214-219. Springer, Heidelberg (2011)
Demri, S., D'Souza, D.: An automata-theoretic approach to constraint LTL. Inf. Comput. 205(3), 380-415 (2007)
van Dongen, B.: BPI challenge 2012 (2012), http://dx.doi.org/10.4121/ uuid:3926db30-f712-4394-aebc-75976070e91f
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: Proc. of FMSP 1998, pp. 7-15. ACM (1998)
Felder, M., Morzenti, A.: Validating real-time systems by history-checking TRIO specifications. ACM Trans. Softw. Eng. Methodol. 3(4), 308-339 (1994)
Pradella, M., Morzenti, A., San Pietro, P.: The symmetry of the past and of the future: bi-infinite time in the verification of temporal properties. In: Proc. of ESEC-FSE 2007, pp. 312-320. ACM (2007)
Pradella,M., Morzenti, A., San Pietro, P.: Bounded satisfiability checking of metric temporal logic specifications. ACM Trans. Softw. 20, 1-20 (2013)
Wozna-Szczesniak, B., Zbrzezny, A.: Checking MTL properties of discrete timed automata via bounded model checking. In: CS&P, vol. 1032, pp. 469-477. CEUR-WS.org (2013)