Saha

To implement the algorithm we followed the pseudocode and the analysis provided in the following paper:

Saha, Diptikalyan.
"An incremental bisimulation algorithm."
International Conference on Foundations of Software Technology
    and Theoretical Computer Science.
Springer, Berlin, Heidelberg, 2007.

Using Saha’s incremental algorithm we can update the RSCP/maximum bisimulation after the addition of a new edge. While we may do the same thing computing the maximum bisimulation from scratch after the modification, Saha’s algorithm may be able to take less time on average.

Warning

Saha’s algorithm works only with integer graphs. You must convert your graph to an isomorphic integer graph before creating the partition of bispy.utilities.graph_entities._QBlock.

See also

bispy.utilities.graph_normalization

The complexity of Saha’s algorithm is highly dependent on how much the maximum bisimulation changes as a consequence of the addition of the new edge:

\[\begin{split}\begin{align*} T_{\text{Saha}} = O(|E_1|\log|V_1|) &+ O(|\Delta_\texttt{wf}\log|\Delta_\texttt{wf}|) + O(|E_\texttt{nwf}| + |V_\texttt{nwf}|)\\ &+ O(|E_2||V_2|) + O(|E_2|\log|V_2|) \end{align*}\end{split}\]

Therefore without an additional hypothesis on the nature of the edges added we may encounter some cases for which the incremental algorithm takes much more than re-computing the maximum bisimulation from scratch using Paige-Tarjan or Dovier-Piazza-Policriti’s algorithm.

Summary

saha	Update the given RSCP/maximum bisimulation after the addition of the given new edge using Saha's incremental algorithm.
add_edge	Add a new edge to the graph (this is the internal BisPy representation, therefore the original graph is left untouched).
is_in_image	Check if vblock is in the image of ublock.
check_new_scc	Check if a new strongly connected component has been created after the addition of a new edge.
both_blocks_go_or_dont_go_to_block	Check if both block1 and block2 have a non-empty intersection with the set of vertexes block_counterimage.
exists_causal_splitter	Check if there is a causal splitter for blocks block1 and block2.
merge_condition	Check all the condition which may prevent the union of two blocks, returns True if the blocks can be joined.
recursive_merge	Merge block1, block2 (put the vertexes of block2 into block1), deteach block2 from the partition, and check recursively if we can also merge some couples of predecessors of block1 and block2 (namely couple of blocks \(C,D\) such that
merge_phase	We check if there is a block \(U1\) such that before the addition of the new edge \(\langle u,v \rangle\) there was a causal splitter for the couple \(([u],U1)\), and for which merge_condition() now returns True on that couple.
preprocess_initial_partition	Preprocess the given partition to split blocks which contain leafs and non-leafs.
merge_split_phase	The function MergeAndSplitPhase from the paper.
propagate_nwf	Compute the updated rank of the given SCC, and propagate the change to its counterimage in the order given by the finishing time of a visit on the graph of strongly connected components of \(G\).
propagate_wf	Recursively visit the well-founded counterimage of the given vertex and update the rank.
build_well_founded_topological_list	Build a list of all the vertexes in the graph sorted in increasing order of rank.
filter_deteached	Remove deteached blocks (blocks such that the attribute deteached is True) from the given list.

Code documentation

saha(old_rscp, vertexes, new_edge)

Update the given RSCP/maximum bisimulation after the addition of the given new edge using Saha’s incremental algorithm.

The edge must not be already in the BisPy representation of the graph (namely in the image/counterimage of the instances of bispy.utilities.graph_entities._Vertex in blocks of old_rscp).

Parameters

• old_rscp (List[_QBlock]) – The old RSCP/maximum bisimulation which we wish to update.

• vertexes (List[_Vertex]) – List of vertexes in the graph.

New_edge

The new edge to be added to the graph (as a tuple of two bispy.utilities.graph_entities._Vertex instances, or two ints which represent the indexes of the nodes which characterize the edge). The first item represents the source of the edge, the second represents the destination.

Return type

List[_QBlock]

Returns

The updated RSCP/maximum bisimulation. Also rank is updated for each vertex.

add_edge(source, destination)

Add a new edge to the graph (this is the internal BisPy representation, therefore the original graph is left untouched).

This function also sets the count attribute for the new edge, creating a new instance of bispy.utilities.graph_entities._Count if the source of the edge was a sink previously, and getting the instance from the first edge in the image otherwise.

Parameters

• source (_Vertex) – The source of the new edge.

• destination (_Vertex) – The source of the new edge.

Return type

_Edge

is_in_image(ublock, vblock)

Check if vblock is in the image of ublock. This is used before adding a new edge, because if the destination vertex is already in the image of the source vertex we do not need to change the partition to reach the maximum bisimulation.

Warning

ublock and vblock must be members of a stable partition, otherwise this function returns a wrong output.

Parameters

• ublock (_QBlock) – The block for which we check the image.

• vblock (_QBlock) – The block that we look for in the image of ublock.

Return type

bool

Returns

True if vblock belongs to the image of ublock, False otherwise.

check_new_scc(current_source, destination, finishing_time_list=None, visited_vertexes=None, root_call=True)

Check if a new strongly connected component has been created after the addition of a new edge. This is meant to be a recursive method, therefore the new edge is not always \(\langle\) current_source, destination \(\rangle\).

This method visits \(G^{-1}\) recursively (with a DFS strategy) starting from current_source until it finds the destination vertex, in which case a new SCC is recognized.

Meanwhile it also sets the flag visited for each visited vertex to prevent visiting the same node twice. At the end of the execution the root call cleans the flag visited for each vertex by exploring each vertex in the list visited_vertexes, which is passed automatically from the root call to all its children.

It also sets the flag visited for each visited bispy.utilities.graph_entities._QBlock. This information is used in other parts of the algorithm.

Parameters

• current_source (_Vertex) – The current starting point for the DFS of \(G^{-1}\).

• destination (_Vertex) – The destination vertex of the new edge.

• finishing_time_list (Optional[List[_Vertex]]) – An empty list which will be filled with the vertexes ordered by finishing time (first are those for which the exploaration of the image ended earlier). This feature is disabled if this argument is None.

• visited_vertexes (Optional[List[_Vertex]]) – An empty list which will be filled with the vertexes visited during the execution. You do not need to pass a non-None value since the root call takes care of the necessary cleanup which occurs after the execution of the function.

• root_call – True if this instance of the function is the root call. Passing any value other than True (from a user perspective) is going to end with an exception.

Return type

bool

Returns

True if a new strongly connected component has been created, False otherwise.

both_blocks_go_or_dont_go_to_block(block1, block2, block_counterimage)

Check if both block1 and block2 have a non-empty intersection with the set of vertexes block_counterimage.

Usually the parameter block_counterimage contains the counterimage of a block, therefore this method may be stated like “find if both block1 and block2 go to the third block, or if both blocks do not go to that block”.

Parameters

• block1 (_QBlock) – A block.

• block2 (_QBlock) – A block.

• block_counterimage (List[_Vertex]) – A set of vertexes.

Return type

bool

Returns

True if \(\delta(|\textit{block1} \cap \textit{block_counterimage}|)\) is equal to \(\delta(|\textit{block2} \cap \textit{block_counterimage}|)\).

exists_causal_splitter(block1, block2, check_visited)

Check if there is a causal splitter for blocks block1 and block2. A causal splitter is a block \(C\) such that

\[\textit{block1} \cap E^{-1}(C) \neq \emptyset \land \textit{block2} \cap E^{-1}(C) = \emptyset\]

or viceversa.

The existence of a causal splitter prevents two blocks from being joined.

Parameters

• block1 (_QBlock) – A block.

• block2 (_QBlock) – A block.

• check_visited – If True, we only consider vertexes in blocks which have been visited during the first DFS (namely that which was performed to search for a new SCC). If False, each block is a plausible causal splitter.

Return type

bool

Returns

True if there is a causal splitter for the two blocks, False otherwise.

merge_condition(block1, block2, check_visited=False)

Check all the condition which may prevent the union of two blocks, returns True if the blocks can be joined. Some conditions are redundant, we check first those which are almost instantaneous to verify since this method is going to be called frequently.

The conditions:

1. Same labeling set/initial partition;

2. The two blocks are not the same block;

3. Same rank;

4. One of the blocks was deteached from the partition previously (therefore

   it is most likely empty at this points);

5. There is not a causal splitter for the two blocks.

Parameters

• block1 (_QBlock) – A block.

• block2 (_QBlock) – A block.

• check_visited (bool) – See the documentation of exists_causal_splitter().

Return type

bool

recursive_merge(block1, block2)

Merge block1, block2 (put the vertexes of block2 into block1), deteach block2 from the partition, and check recursively if we can also merge some couples of predecessors of block1 and block2 (namely couple of blocks \(C,D\) such that

\[C \implies \textit{block1} \land D \implies \textit{block2}\]

where the relation “\(\implies\)” means that there is at least one vertex of the rightmost block which is a child of the leftmost block).

If such at couple exists, the method recursively merges those two blocks, for each couple for which merge_condition() is True.

Parameters

• block1 (_QBlock) – A block.

• block2 (_QBlock) – A block.

merge_phase(ublock, vblock)

We check if there is a block \(U1\) such that before the addition of the new edge \(\langle u,v \rangle\) there was a causal splitter for the couple \(([u],U1)\), and for which merge_condition() now returns True on that couple.

In that case we merge the two blocks using recursive_merge().

Parameters

• ublock (_QBlock) – The block of the partition in which resides the source of the new edge.

• vblock (_QBlock) – The block of the partition in which resides the destination of the new edge.

preprocess_initial_partition(qblocks)

Preprocess the given partition to split blocks which contain leafs and non-leafs.

Parameters

qblocks (List[_QBlock]) – A partition.

merge_split_phase(qpartition, finishing_time_list)

The function MergeAndSplitPhase from the paper.

Parameters

• qpartition (List[_QBlock]) – The current partition.

• finishing_time_list (List[_Vertex]) – List of vertexes in the graph ordered by finishing time.

Return type

List[_QBlock]

Returns

The updated partition.

propagate_nwf(scc, scc_finishing_time)

Compute the updated rank of the given SCC, and propagate the change to its counterimage in the order given by the finishing time of a visit on the graph of strongly connected components of \(G\).

Parameters

• scc (_SCC) – The SCC for which we want to update the rank.

• scc_finishing_time (List[_SCC]) – A list of SCCs ordered by finishing time of a DFS on the graph of strongly connected components of \(G\).

propagate_wf(vertex, well_founded_topological, scc_finishing_time)

Recursively visit the well-founded counterimage of the given vertex and update the rank. The visit is in increasing order of rank (this is needed in order to obtain the correct result).

Parameters

• vertex (_Vertex) – The vertex to whose counterimage we intend to propagate the change of the rank. The rank of this argument must already be updated, since it is left untouched after the execution.

• well_founded_topological (List[_Vertex]) – List of well founded vertexes of the whole graph in topological order.

build_well_founded_topological_list(partition, source, max_rank)

Build a list of all the vertexes in the graph sorted in increasing order of rank.

We ignore all the nodes which do not have rank = \(-\infty\) and have rank lower that the rank of the source vertex of the new edge.

Parameters

• partition (List[_QBlock]) – A partition of the graph from which we obtain the instances of bispy.utilities.graph_entities._Vertex. All the nodes in the same block must have the same rank.

• source (_Vertex) – The source vertex of the new edge.

• max_rank (int) – The maximum rank of a vertex in this graph, used to create a list of the appropriate size.

Return type

List[_Vertex]

filter_deteached(blocks)

Remove deteached blocks (blocks such that the attribute deteached is True) from the given list.

Parameters

blocks (List[_QBlock]) – A list of blocks.

Return type

List[_QBlock]