|
| << previous | next >> |
Journal description
All volumes of the corresponding journal
All issues of the corresponding volume
All articles of the corresponding issues
Details for article 6 of 16 found articles
| Title: |
Checking MTL Properties of Discrete Timed Automata via Bounded Model Checking |
| Author: |
Woźna-Szcześniak, Bożena Zbrzezny, Andrzej |
| Appeared in: |
Fundamenta informaticae |
| Paging: | Volume 135 (2014) nr. 4 pages 553-568 |
| Year: |
2014-11-24 |
| Contents: |
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. |
| Publisher: |
IOS Press |
| Source file: |
Elektronische Wetenschappelijke Tijdschriften |
Details for article 6 of 16 found articles
| << previous | next >> |