|
| << vorige | volgende >> |
Tijdschrift beschrijving
Alle jaargangen van het bijbehorende tijdschrift
Alle afleveringen van het bijbehorende jaargang
Alle artikelen van de bijbehorende aflevering
Details van artikel 6 van 16 gevonden artikelen
| Titel: |
Checking MTL Properties of Discrete Timed Automata via Bounded Model Checking |
| Auteur: |
Woźna-Szcześniak, Bożena Zbrzezny, Andrzej |
| Verschenen in: |
Fundamenta informaticae |
| Paginering: | Jaargang 135 (2014) nr. 4 pagina's 553-568 |
| Jaar: |
2014-11-24 |
| Inhoud: |
We investigate a SAT-based bounded model checking (BMC) method for MTL (metric temporal logic) that is interpreted over linear discrete infinite time models generated by discrete timed automata. In particular, we translate the existential model checking problem for MTL to the existential model checking problem for a variant of linear temporal logic (called HLTL), and we provide a SAT-based BMC technique for HLTL. We show how to implement the BMC technique for HLTL and discrete timed automata, and as a case study we apply the technique in the analysis of GTPP, a Generic Timed Pipeline Paradigm modelled by a network of discrete timed automata. |
| Uitgever: |
IOS Press |
| Bronbestand: |
Elektronische Wetenschappelijke Tijdschriften |
Details van artikel 6 van 16 gevonden artikelen
| << vorige | volgende >> |