Dovier-Piazza-Policriti

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:

\[a \equiv b \implies \texttt{rank}(a) = \texttt{rank}(b)\]

See also

Dovier-Piazza-Policriti’s notation

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

dovier_piazza_policriti

Compute the RSCP/maximum bisimulation of the given graph using Dovier-Piazza-Policriti's algorithm.

dovier_piazza_policriti_partition

Apply Dovier-Piazza-Policriti's algorithm to the given ranked partition.

collapse

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

build_block_counterimage

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

split_upper_ranks

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 Dovier-Piazza-Policriti’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 non-integer it is converted to an isomorphic integer graph automatically (unless is_integer_graph is True) and then re-converted 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 Dovier-Piazza-Policriti’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.

Parameters

block (_QBlock) – The block to collapse.

Return type

Tuple[_Vertex, List[_Vertex]]

Returns

A tuple whose first element is the single vertex which survived the collapse, and the second is the list of collapsed vertexes.

build_block_counterimage(block)

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

Parameters

block (_QBlock) – The block for which we intend to build the counterimage.

Return type

List[_Vertex]

split_upper_ranks(partition, block)

Split the blocks whose rank is greater than block.rank using block as splitter.

Parameters