Sciweavers

Share
APN
2008
Springer

MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs

8 years 4 months ago
MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs
Model checking is a powerful and widespread technique for the verification of finite distributed systems. However, the main hindrance for wider application of this technique is the well-known state explosion problem. During the last two decades, numerous techniques have been proposed to cope with the state explosion problem in order to get a manageable state space. Among them, on-the-fly modelchecking allows for generating only the "interesting" part of the model while symbolic model-checking aims at checking the property on a compact representation of the system by using Binary Decision Diagram (BDD) techniques. In this paper, we propose a technique which combines these two approaches to check LTL\X state-based properties over ystems. During the model checking process, only an abstraction of the state space of the system, namely the symbolic observation graph, ibly partially) explored. The building of such an abstraction is guided by the property to be checked and is equival...
Kais Klai, Denis Poitrenaud
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Where APN
Authors Kais Klai, Denis Poitrenaud
Comments (0)
books