Checking MTL Properties of Discrete Timed Automata via Bounded Model Checking

Issue title: Concurrency Specification and Programming 2013 (CS&P'13)

Article type: Research Article

Authors: Woźna-Szcześniak, Bożena | Zbrzezny, Andrzej

Affiliations: IM&CS, Jan Długosz University, Al. Armii Krajowej 13/15, 42-200 Częstochowa, Poland. email: {b.wozna, a.zbrzezny}@ajd.czest.pl

Note: [] Address for correspondence: IM&CS, Jan Długosz University, Al. Armii Krajowej 13/15, 42-200 Częstochowa, Poland

Abstract: 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.

DOI: 10.3233/FI-2014-1140

Journal: Fundamenta Informaticae, vol. 135, no. 4, pp. 553-568, 2014