Bounded Model Checking for Metric Temporal Logic Properties of Timed Automata with Digital Clocks †

Metric temporal logic (MTL) is a popular real-time extension of linear temporal logic (LTL). This paper presents a new simple SAT-based bounded model-checking (SAT-BMC) method for MTL interpreted over discrete infinite timed models generated by discrete timed automata with digital clocks. We show a...

Descripción completa

Detalles Bibliográficos
Autores principales: Zbrzezny, Agnieszka M., Zbrzezny, Andrzej
Formato: Online Artículo Texto
Lenguaje:English
Publicado: MDPI 2022
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC9737090/
https://www.ncbi.nlm.nih.gov/pubmed/36502252
http://dx.doi.org/10.3390/s22239552

Internet

https://www.ncbi.nlm.nih.gov/pmc/articles/PMC9737090/
https://www.ncbi.nlm.nih.gov/pubmed/36502252
http://dx.doi.org/10.3390/s22239552

Ejemplares similares