| Autor: |
Agnieszka M. Zbrzezny, Andrzej Zbrzezny |
| Jazyk: |
angličtina |
| Rok vydání: |
2022 |
| Předmět: |
|
| Zdroj: |
Sensors, Vol 22, Iss 23, p 9552 (2022) |
| Druh dokumentu: |
article |
| ISSN: |
1424-8220 |
| DOI: |
10.3390/s22239552 |
| Popis: |
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 new translation of the existential part of MTL to the existential part of linear temporal logic with a new set of atomic propositions and present the details of the new translation. We compare the new method’s advantages to the old method based on a translation of the hard reset LTL (HLTL). Our method does not need new clocks or new transitions. It uses only one path and requires a smaller number of propositional variables and clauses than the HLTL-based method. We also implemented the new method, and as a case study, we applied the technique to analyze several systems. We support the theoretical description with the experimental results demonstrating the method’s efficiency. |
| Databáze: |
Directory of Open Access Journals |
| Externí odkaz: |
|
|
Nepřihlášeným uživatelům se plný text nezobrazuje |
K zobrazení výsledku je třeba se přihlásit.
|
