Bounded Model Checking of an MITL Fragment for Timed Automata

Preprint English OPEN
Kindermann, Roland ; Junttila, Tommi ; Niemelä, Ilkka (2013)
  • 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
Share - Bookmark