DovierPiazzaPolicriti¶
To implement the algorithm we followed the pseudocode and the analysis provided in the following paper:
Dovier, Agostino, Carla Piazza, and Alberto Policriti.
"A fast bisimulation algorithm."
International Conference on Computer Aided Verification.
Springer, Berlin, Heidelberg, 2001.
The most significant improvement with respect to
bispy.paige_tarjan.paige_tarjan
is due to the usage of the notion of
rank, motivated by the following observation:
See also
Therefore we may be able to obtain the equivalence classes of the maximum bisimulation in a smaller number of steps when the relation “same rank” is a good approximation of the maximum bisimulation.
Summary¶
Compute the RSCP/maximum bisimulation of the given graph using DovierPiazzaPolicriti's algorithm. 

Apply DovierPiazzaPolicriti's algorithm to the given ranked partition. 

Collapse the given block to a single vertex chosen randomly from the vertexes of the block. 

Given a block B, construct its counterimage with respect to the binary relation \(E\) (edges of the graph). 

Split the blocks whose rank is greater than block.rank using block as splitter. 
Code documentation¶
 dovier_piazza_policriti(graph, initial_partition=None, is_integer_graph=False)¶
Compute the RSCP/maximum bisimulation of the given graph using DovierPiazzaPolicriti’s algorithm.
 Example:
>>> graph = networkx.balanced_tree(2,3) >>> dovier_piazza_policriti(graph) [(7, 8, 9, 10, 11, 12, 13, 14), (3, 4, 5, 6), (1, 2), (0,)]
This function works with integer graph (nodes are integers starting from 0 and form an interval without holes). If the given graph is noninteger it is converted to an isomorphic integer graph automatically (unless is_integer_graph is True) and then reconverted to its original form after the end of the computation. For this reason nodes of graph must be hashable objects.
Warning
Using a non integer graph and setting is_integer_graph to True will probably make the function fail with an exception, or, even worse, return a wrong output.
 Parameters
graph (
Graph
) – The input graph.initial_partition (
Optional
[List
[Tuple
[int
]]]) – The initial partition (or labeling set). Defaults to None, in which case the trivial labeling set (one block which contains all the nodes) is used.is_integer_graph (
bool
) – If True, we do not check if the given graph is integer (saves time). If is_integer_graph is True but the graph is not integer the output may be wrong. Defaults to False.
 Return type
List
[Tuple
] Returns
The RSCP/maximum bisimulation of the given labeling set as a list of tuples, each of which contains bisimilar nodes.
 dovier_piazza_policriti_partition(partition)¶
Apply DovierPiazzaPolicriti’s algorithm to the given ranked partition.
 Parameters
partition (
RankedPartition
) – A ranked partition (\(P\) in the paper). Return type
Tuple
[RankedPartition
,List
[List
[_Vertex
]]] Returns
A tuple such that the first item is the partition at the end of the algorithm (which at this point is made of blocks of size 1 containing only the vertexes which survived the collapse), and the second is a list which maps a survivor nodes to the list of nodes collapsed to that survivor node.
 collapse(block)¶
Collapse the given block to a single vertex chosen randomly from the vertexes of the block.
 build_block_counterimage(block)¶
Given a block B, construct its counterimage with respect to the binary relation \(E\) (edges of the graph).
 split_upper_ranks(partition, block)¶
Split the blocks whose rank is greater than block.rank using block as splitter.
 Parameters
partition (
RankedPartition
) – The current partition.block (
_QBlock
) – The splitter block.