Bounded Model Checking of an MITL Fragment for Timed Automata

Roland Kindermann, Tommi Junttila, Ilkka Niemelä

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 SA…