Checking EMTLK Properties of Timed Interpreted Systems via Bounded Model Checking

We investigate a SAT-based bounded model checking (BMC) method for EMTLK (the existential fragment of the metric temporal logic with knowledge) that is interpreted over timed models generated by timed interpreted systems. In particular, we translate the existential model checking problem for EMTLK to the existential model checking problem for a linear temporal logic (called HLTLK), and we provide a SAT-based BMC technique for HLTLK.