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

Autor:	Janusz Malinowski, Peter Niebert
Rok vydání:	2010
Předmět:	Model checking Theoretical computer science Correctness Computer science Bounded function Timed automaton Automaton Coding (social sciences)
Zdroj:	Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783642120015 TACAS
DOI:	10.1007/978-3-642-12002-2_34
Popis:	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.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::9f23186dd7dabdea1c81100e0e786cdd https://doi.org/10.1007/978-3-642-12002-2_34 Zobrazit plný text záznamu