Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/40615
Título: | Monitoring for a decidable fragment of MTL-∫ |
Autor(es): | Pedro, André Matos Pereira, David Pinho, Luís Miguel Pinto, Jorge Sousa |
Data: | Set-2015 |
Editora: | Springer Verlag |
Revista: | Lecture Notes in Computer Science |
Citação: | Pedro, A. M., Pereira, D., Pinho, L. M., & Pinto, J. S. (2015) Monitoring for a decidable fragment of mtl-∫. Vol. 9333. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 169-184). |
Resumo(s): | Temporal logics targeting real-time systems are traditionally undecidable. Based on a restricted fragment of MTL-R, 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 e↵ectively 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. |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/40615 |
ISBN: | 978-3-319-23819-7 978-3-319-23820-3 |
DOI: | 10.1007/978-3-319-23820-3_11 |
ISSN: | 0302-9743 |
Versão da editora: | http://link.springer.com/chapter/10.1007/978-3-319-23820-3_11 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: |