## Bounded Model Checking of an MITL Fragment for Timed Automata

*Kindermann, Roland*;

*Junttila, Tommi*;

*Niemelä, Ilkka*;

- Subject: Computer Science - Logic in Computer Sciencearxiv: Computer Science::Logic in Computer Science

- References (16) 16 references, page 1 of 2
- 1
- 2

[1] R. Alur and D. L. Dill, “A theory of timed automata,” Theoretical Computer Science, vol. 126, no. 2, pp. 183-235, 1994.

[2] G. Behrmann, A. David, and K. G. Larsen, “A tutorial on UPPAAL,” in Proc. FM-RT 2004, ser. LNCS, vol. 3185. Springer, September 2004, pp. 200-236.

[3] R. Alur, T. Feder, and T. A. Henzinger, “The benefits of relaxing punctuality,” Journal of the ACM, vol. 43, no. 1, pp. 116-146, 1996.

[4] O. Maler, D. Nickovic, and A. Pnueli, “From MITL to timed automata,” in FORMATS, ser. LNCS, vol. 4202. Springer, 2006, pp. 274-289.

[5] R. Alur, “Timed automata,” in Proc. CAV 1999, ser. LNCS, vol. 1633. Springer, 1999, pp. 8-22.

[6] J. Bengtsson and W. Yi, “Timed automata: Semantics, algorithms and tools,” in Lectures on Concurrency and Petri Nets, ser. LNCS, vol. 3098. Springer, 2004, pp. 87-124.

[7] M. Sorea, “Bounded model checking for timed automata,” Elect. Notes Theor. Comp. Sci., vol. 68, no. 5, pp. 116-134, 2002.

[8] G. Audemard, A. Cimatti, A. Kornilowicz, and R. Sebastiani, “Bounded model checking for timed systems,” in Proc. FORTE 2002, ser. LNCS, vol. 2529. Springer, 2002, pp. 243-259.

[9] R. Kindermann, T. Junttila, and I. Niemela¨, “Modeling for symbolic analysis of safety instrumented systems with clocks,” in Proc. ACSD 2011. IEEE, 2011, pp. 185-194.

[10] C. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli, “Satisfiability modulo theories,” in Handbook of Satisfiability. IOS Press, 2009, pp. 825-885.

- Metrics No metrics available

- Download from

- Funded by

- Cite this publication