Sciweavers

TACAS
2010
Springer

SAT Based Bounded Model Checking with Partial Order Semantics for Timed Automata

13 years 10 months ago
SAT Based Bounded Model Checking with Partial Order Semantics for Timed Automata
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.
Janusz Malinowski, Peter Niebert
Added 14 May 2010
Updated 14 May 2010
Type Conference
Year 2010
Where TACAS
Authors Janusz Malinowski, Peter Niebert
Comments (0)