Exploiting interleaving semantics in symbolic state-space generation

G Ciardo, G Lüttgen, AS Miner - Formal Methods in System Design, 2007 - Springer
G Ciardo, G Lüttgen, AS Miner
Formal Methods in System Design, 2007Springer
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 …
Abstract
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 multiple lightweight next–state transformations rather than a single heavyweight one. Together, this paves the way for a novel iteration order, called saturation, which replaces the breadth–first search order of traditional algorithms. The resulting saturation algorithm is implemented in the tool SMART, and experimental studies show that it is often several orders of magnitude better in terms of time efficiency, final memory consumption, and peak memory consumption than existing symbolic algorithms.
Springer
Showing the best result for this search. See all results