Monitoring for a decidable fragment of MTLD

Pedro, André; Pereira, David; Pinho, Luís Miguel; Pinto, Jorge Sousa

http://hdl.handle.net/10400.22/6913

Use this identifier to reference this record.

Name:	Description:	Size:	Format:
COM_CISTER_2015.pdf		356.9 KB	Adobe PDF	Download

Send Feedback

Authors

Abstract(s)

Temporal logics targeting real-time systems are traditionally undecidable. Based on a restricted fragment of MTLD, 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.