The paper "A Quantitative Metric Temporal Logic for Execution-Time Constrained Verification" has been accepted for the "CyPhy'18" workshop (<link http: www.cyphy.org _self>www.cyphy.org) as part of the "ESWEEK" event on embedded systems and software (<link https: www.esweek.org _self>www.esweek.org).
Sascha Lehmann and Sibylle Schupp, in collaboration with Alexander Schlaefer and Sven-Thomas Antoni from the Institute of Medical Technology (MTEC), introduce the logic QMTL-VT to describe constraints on the time required to verify system properties (e.g. of cyber-physical real-time systems) formulated in another underlying logic.
Using QMTL-VT, it is possible to query for satisfaction of time constraints (V), the bounds of execution times (Vi), and the probability of being checkable within these bounds (Vp). Building up on that, it further allows to execute queries under temporal conditions (Vc), express their order (Vs), and provide alternatives (Va) for the case of constraint violations.