MITL Model Checking via Generalized Timed Automata and a New Liveness Algorithm

S. Akshay, Paul Gastin, R. Govind +1

The translation of Metric Interval Temporal Logic (MITL) to timed automata is a topic that has been extensively studied. A key challenge here is the conversion of future modalities…