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. © 2010 Springer-Verlag.
CITATION STYLE
Malinowski, J., & Niebert, P. (2010). SAT based bounded model checking with partial order semantics for timed automata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6015 LNCS, pp. 405–419). https://doi.org/10.1007/978-3-642-12002-2_34
Mendeley helps you to discover research relevant for your work.