An Efficient Algorithm for Monitoring Practical TPTL Specifications
This work provides an efficient monitoring algorithm for a more expressive real-time logic, benefiting practitioners who need to verify complex timing constraints in finite traces.
The paper presents a polynomial-time dynamic programming algorithm for offline monitoring of a fragment of Timed Propositional Temporal Logic (TPTL) that is more expressive than Metric Temporal Logic, enabling the specification of complex real-time requirements. Experimental results on a prototype implementation demonstrate feasibility for practical applications.
We provide a dynamic programming algorithm for the monitoring of a fragment of Timed Propositional Temporal Logic (TPTL) specifications. This fragment of TPTL, which is more expressive than Metric Temporal Logic, is characterized by independent time variables which enable the elicitation of complex real-time requirements. For this fragment, we provide an efficient polynomial time algorithm for off-line monitoring of finite traces. Finally, we provide experimental results on a prototype implementation of our tool in order to demonstrate the feasibility of using our tool in practical applications.