Bounded Model Checking of an MITL Fragment for Timed Automata

Preprint English OPEN
Kindermann, Roland; Junttila, Tommi; Niemelä, Ilkka;
  • Subject: Computer Science - Logic in Computer Science
    arxiv: Computer Science::Logic in Computer Science

Timed automata (TAs) are a common formalism for modeling timed systems. Bounded model checking (BMC) is a verification method that searches for runs violating a property using a SAT or SMT solver. MITL is a real-time extension of the linear time logic LTL. Originally, M... View more
  • References (16)
    16 references, page 1 of 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
Share - Bookmark