In this paper we propose an ecient symbolic algorithm for the problem of determining the maximum bisimulation on a nite structure. The starting point is an algorithm, on explicit representation of graphs, which saves both time and space exploiting the notion of rank. This notion provides a layering of the input model and allows to proceed bottom-up in the bisimulation computation. In this paper we give a procedure that allows to compute the rank of a graph working on its symbolic representation and requiring a linear number of symbolic steps. Then we embed it in a fully symbolic, rank-driven, bisimulation algorithm. Moreover, we show how the notion of rank can be employed to optimize the CTL Model Checking procedures. Key words: Bisimulation, Ordered Binary Decision Diagrams, Symbolic Algorithms, Model Checking.
Rank-Based Symbolic Bisimulation (and Model Checking)
GENTILINI, Raffaella;
2002
Abstract
In this paper we propose an ecient symbolic algorithm for the problem of determining the maximum bisimulation on a nite structure. The starting point is an algorithm, on explicit representation of graphs, which saves both time and space exploiting the notion of rank. This notion provides a layering of the input model and allows to proceed bottom-up in the bisimulation computation. In this paper we give a procedure that allows to compute the rank of a graph working on its symbolic representation and requiring a linear number of symbolic steps. Then we embed it in a fully symbolic, rank-driven, bisimulation algorithm. Moreover, we show how the notion of rank can be employed to optimize the CTL Model Checking procedures. Key words: Bisimulation, Ordered Binary Decision Diagrams, Symbolic Algorithms, Model Checking.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
