This paper presents a verification technique for dense-time MTL based on discretization. The technique reduces the validity problem of MTL formulas from dense to discrete time, through the notion of sampling invariance, introduced in previous work [13]. Since the reduction is from an undecidable problem to a decidable one, the technique is necessarily incomplete, so it fails to provide conclusive answers for some formulas. The paper discusses this shortcoming and hints at how it can be mitigated in practice. The verification technique has been implemented on top of the ℤot tool [19] for discrete-time bounded validity checking; the paper also reports on in-the-small experiments with the tool, which show some results that are promising in terms of performance. © 2008 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Furia, C. A., Pradella, M., & Rossi, M. (2008). Automated verification of dense-time MTL specifications via discrete-time approximation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5014 LNCS, pp. 132–147). https://doi.org/10.1007/978-3-540-68237-0_11
Mendeley helps you to discover research relevant for your work.