ATVA
2005
Springer
14 years 5 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
14 years 5 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
14 years 5 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
14 years 5 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
14 years 5 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
14 years 5 months ago
2005
Springer
ATVA
2005
Springer
14 years 5 months ago
2005
Springer