Sciweavers

FMSD
2007

Exploiting interleaving semantics in symbolic state-space generation

13 years 10 months ago
Exploiting interleaving semantics in symbolic state-space generation
Symbolic techniques based on Binary Decision Diagrams (BDDs) are widely employed for reasoning about temporal properties of hardware circuits and synchronous controllers. However, they often perform poorly when dealing with the huge state spaces underlying systems based on interleaving semantics, such as communications protocols and distributed software, which are composed of independently acting subsystems that communicate via shared events. This article shows that the efficiency of state–space exploration techniques using decision diagrams can be drastically improved by exploiting the interleaving semantics underlying many event–based and component–based system models. A new algorithm for symbolically generating state spaces is presented that (i) encodes a model’s state vectors with Multi–valued Decision Diagrams (MDDs) rather than flattening them into BDDs and (ii) partitions the model’s Kronecker–consistent next–state function by event and subsystem, thus enabling...
Gianfranco Ciardo, Gerald Lüttgen, Andrew S.
Added 14 Dec 2010
Updated 14 Dec 2010
Type Journal
Year 2007
Where FMSD
Authors Gianfranco Ciardo, Gerald Lüttgen, Andrew S. Miner
Comments (0)