×

SAT based bounded model checking with partial order semantics for timed automata. (English) Zbl 1284.68412

Esparza, Javier (ed.) et al., Tools and algorithms for the construction and analysis of systems. 16th international conference, TACAS 2010, held as part of the joint European conferences on theory and practice of software, ETAPS 2010, Paphos, Cyprus, March 20–28, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-12001-5/pbk). Lecture Notes in Computer Science 6015, 405-419 (2010).
Summary: We study the model checking problem of timed automata based on SAT solving. Our work investigates alternative possibilities for coding the SAT reductions that are based on parallel executions of independent transitions.
While such an optimization has been studied for discrete systems, its transposition to timed automata poses the question of what it means for timed transitions to be executed “in parallel”. The most obvious interpretation is that the transitions in parallel take place at the same time (synchronously). However, it is possible to relax this condition. On the whole, we define and analyse three different semantics of timed sequences with parallel transitions.
We prove the correctness of the proposed semantics and report experimental results with a prototype implementation.
For the entire collection see [Zbl 1185.68007].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata

Software:

POEM; PicoSAT; IF-2.0
PDF BibTeX XML Cite
Full Text: DOI