ATVA
2005
Springer
13 years 11 months ago
2005
Springer
We introduce a family of temporal logics to specify the behavior of systems with Zeno behaviors. We extend linear-time temporal logic LTL to authorize models admitting Zeno sequen...
ATVA
2005
Springer
13 years 11 months ago
2005
Springer
Esterel is an imperative synchronous programming language for the design of reactive systems. Esterel extends Esterel with a noninstantaneous jump instruction (compatible with conc...
ATVA
2005
Springer
13 years 11 months ago
2005
Springer
This work extends the game-based framework of µ-calculus model checking to the multi-valued setting. In multi-valued model checking a formula is interpreted over a Kripke structur...
ATVA
2005
Springer
13 years 11 months ago
2005
Springer
Partitioned BDD-based algorithms have been proposed in the literature to solve the memory explosion problem in BDD-based verification. A naive parallelization of such algorithms ...
ATVA
2005
Springer
13 years 11 months ago
2005
Springer
Abstract. Symbolic model checking provides partially effective verification procedures that can handle systems with an infinite state space. So-called “acceleration techniques...
ATVA
2005
Springer
13 years 11 months ago
2005
Springer
ATVA
2005
Springer
13 years 11 months ago
2005
Springer