Monitoring for a Decidable Fragment of Mtl-∫

Pedro AM, Pereira D, Pinho LM, Pinto JS.  2015.  Monitoring for a Decidable Fragment of Mtl-∫. In Proceedings of Runtime Verification - 6Th International Conference, Rv 2015 . 9333

Date Presented:



Temporal logics targeting real-time systems are traditionally undecidable. Based on a restricted fragment of MTL-∫, we propose a new approach for the runtime verification of hard real-time systems. The novelty of our technique is that it is based on incremental evaluation, allowing us to effectively treat duration properties (which play a crucial role in real-time systems). We describe the two levels of operation of our approach: offline simplification by quantifier removal techniques; and online evaluation of a three-valued interpretation for formulas of our fragment. Our experiments show the applicability of this mechanism as well as the validity of the provided complexity results.

Citation Key:

2015_rv_15.pdf939.92 KB