|
Wojciech Penczek, Bo¿ena WoŸna, Andrzej Zbrzezny
SAT-Based Bounded Model Checking for the Universal Fragment of TCTL
947
Abstract
Bounded Model Checking (BMC) based on SAT methods consists in
searching for a counterexample of a particular length
and to generate a propositional formula that is satisfiable
iff such a counterexample exists.
Our paper shows how the concept of bounded model checking can be
extended to deal with \TACTL\ (the universal fragment of \TCTL )
properties of a network of concurrent Timed Automata.
Keywords :
bounded model checking, logic \TACTL\ (\TECTL),
bounded semantics, translation to SAT, Timed Automata, Region Graphs,
discretization, system verification
|
|
 |
 |
