A Flexible Approach for Checking Timed Automata on Continuous Time Semantics
share
Timed Automata (TA) are used to represent systems when the interest is the analysis of their behaviour as time progresses. Even if efficient model-checkers for Timed Automata exist, they have several limitations: 1. they are not designed to easily allow adding new Timed Automata constructs, such as new synchronization mechanisms or communication procedures; 2. they rely on a precise semantics for the logic in which the property of interest is expressed which cannot be easily modified and customized; 3. they do not easily allow using different solvers that may speed up verification in different contexts. This paper presents a novel technique to perform model checking of full Metric Interval Temporal Logic (MITL) properties on TA. It relies on the translation of both the TA and the MITL formula into an intermediate Constraint LTL over clocks (CLTLoc) formula which is verified through an available decision procedure. The technique is flexible since the intermediate logic allows the encoding of new TA constructs, as well as new semantics for the logic in which the property of interest is expressed, by just adding new CLTLoc formulae. Furthermore, our technique is not bound to a specific solver as the intermediate CLTLoc formula can be verified using different procedures.
READ FULL TEXT