fandreuz/bispy

BisPy - Python bisimulation library

Description

BisPy is a Python package for the computation of the maximum bisimulation of directed graphs. At the moment it supports the following algorithms:

• Paige-Tarjan
• Dovier-Piazza-Policriti
• Saha

A brief introduction to the problem can be found here.

Usage

Paige-Tarjan, Dovier-Piazza-Policriti

To compute the maximum bisimulation of a graph, first of all we import paige_tarjan and dovier_piazza_policriti from BisPy, as well as the package NetworkX, which we use to represent graphs:

>>> import networkx as nx
>>> from bispy import compute_maximum_bisimulation, Algorithms

We then create a simple graph:

>>> graph = nx.balanced_tree(2,3, create_using=nx.DiGraph)

It's important to set create_using=nx.DiGraph since BisPy works only with directed graphs. Now we can compute the maximum bisimulation using Paige-Tarjan's algorithm, which is the default for the function compute_maximum_bisimulation:

>>> compute_maximum_bisimulation(graph)
[(7, 8, 9, 10, 11, 12, 13, 14), (3, 4, 5, 6), (1, 2), (0,)]

We can use Dovier-Piazza-Policriti's algorithm as well:

>>> compute_maximum_bisimulation(graph, algorithm=Algorithms.DovierPiazzaPolicriti)
[(7, 8, 9, 10, 11, 12, 13, 14), (3, 4, 5, 6),  (1, 2), (0,)]

We may also introduce a labeling set (or initial partition):

>>> compute_maximum_bisimulation(graph, initial_partition=[(0,7,10), (1,2,3,4,5,6,8,9,11,12,13,14)])
[(7, 10), (5, 6), (8, 9, 11, 12, 13, 14), (3, 4), (2,), (1,), (0,)]

Saha

In order to use Saha's algorithm we only need to import the following function:

>>> from bispy import saha

We call that function to obtain an object of type SahaPartition, which has a method called add_edge. This method adds a new edge to the graph and recomputes the maximum bisimulation incrementally:

saha_partition = saha(graph)

(We reused the graph object which we defined in the previous paragraph). We can now use the aforementioned method add_edge (note that when you call this method the instance of graph which you passed is not modified):

>>> for edge in [(1,0), (4,0)]:
...    maximum_bisimulation = saha_partition.add_edge(edge)
...    print(maximum_bisimulation)
[(3, 4, 5, 6), (7, 8, 9, 10, 11, 12, 13, 14), (0,), (2,), (1,)]
[(3, 5, 6), (7, 8, 9, 10, 11, 12, 13, 14), (0,), (2,), (1,), (4,)]

Documentation

You can read the documentation (hosted on ReadTheDocs) at this link.

To build the HTML version of the docs locally use:

> cd docs
> make html

The generated html can be found in docs/build/html.

Dependencies and installation

BisPy requires the modules llist, networkx. The code is tested for Python 3, while compatibility with Python 2 is not guaranteed. It can be installed using pip or directly from the source code.

Installing via pip

To install the package:

> pip install bispy

To uninstall the package:

> pip uninstall bispy

Installing from source

You can clone this repository on your local machine using:

> git clone https://github.com/fAndreuzzi/BisPy

To install the package:

> cd BisPy
> python setup.py install

Testing

We are using GitHub actions for continuous intergration testing. To run tests locally (pytest is required) use the following command from the root folder of BisPy:

> pytest tests

Authors and acknowledgements

BisPy is currently developed and mantained by Francesco Andreuzzi. You can contact me at:

• andreuzzi.francesco at gmail.com
• fandreuz at sissa.it

The project has been developed under the supervision of professor Alberto Casagrande (University of Trieste), which was my advisor for my bachelor thesis.

Reporting a bug

The best way to report a bug is using the Issues section. Please, be clear, and give detailed examples on how to reproduce the bug (the best option would be the graph which triggered the error you are reporting).

How to contribute

We are more than happy to receive contributions on tests, documentation and new features. Our Issues section is always full of things to do.

Here are the guidelines to submit a patch:

1. Start by opening a new issue describing the bug you want to fix, or the feature you want to introduce. This lets us keep track of what is being done at the moment, and possibly avoid writing different solutions for the same problem.

2. Fork the project, and setup a new branch to work in (fix-issue-22, for instance). If you do not separate your work in different branches you may have a bad time when trying to push a pull request to fix a particular issue.

3. Run black before pushing your code for review.

4. Any significant changes should almost always be accompanied by tests. The project already has good test coverage, so look at some of the existing tests if you're unsure how to go about it.

5. Provide menaningful commit messages to help us keeping a good git history.

6. Finally you can submbit your pull request!

References

We consulted the following resources during the development of BisPy:

• Saha, Diptikalyan. "An incremental bisimulation algorithm." International Conference on Foundations of Software Technology and Theoretical Computer Science. Springer, Berlin, Heidelberg, 2007. DOI
• Dovier, Agostino, Carla Piazza, and Alberto Policriti. "A fast bisimulation algorithm." International Conference on Computer Aided Verification. Springer, Berlin, Heidelberg, 2001. DOI
• Gentilini, Raffaella, Carla Piazza, and Alberto Policriti. "From bisimulation to simulation: Coarsest partition problems." Journal of Automated Reasoning 31.1 (2003): 73-103. DOI
• Paige, Robert, and Robert E. Tarjan. "Three partition refinement algorithms." SIAM Journal on Computing 16.6 (1987): 973-989. DOI
• Hopcroft, John. "An n log n algorithm for minimizing states in a finite automaton." Theory of machines and computations. Academic Press, 1971. 189-196.
• Aczel, Peter. "Non-well-founded sets." (1988).
• Kanellakis, Paris C., and Scott A. Smolka. "CCS expressions, finite state processes, and three problems of equivalence." Information and computation 86.1 (1990): 43-68. DOI
• Sharir, Micha. "A strong-connectivity algorithm and its applications in data flow analysis." Computers & Mathematics with Applications 7.1 (1981): 67-72. DOI
• Cormen, Thomas H., et al. Introduction to algorithms. MIT press, 2009. (ISBN: 9780262533058)

License

See the LICENSE file for license rights and limitations (MIT).

bispy's Issues

Initial partition should be renamed to labeling set

The latter is more appropriate and describes the role better.

Improve the public interface

At the moment the interface is quite unusable, especially for Saha's algorithm. We should think about a straightforward and intuitive interface.

Wrapper for graphs whose nodes are not integer numbers

We should execute the algorithm even on graphs where nodes are not integer numbers, maybe with a wrapper which convertes the graph to an isomorphic graph whose nodes are integers numbers.

Proper implementation of propagate_nwf

In the paper An incremental bisimulation algorithm the function propagate_nwf uses an algorithm called Sharir's SCC decomposition, which I ignored while I was writing the code for Saha's algorithm. However this lack should be filled as soon as possible.

Crash with random graphs

Add iterator/generator interface for saha

Provide an alternative API for the saha algorithm as discussed on reddit.

RankedSplit: wrong implementation?

I may have misunderstood the real intuition behind the function RankedSplit in Saha's algorithm.

Use NumPy for lists that never change

Lists with constant size are the most used in the package. However, we lose some speed using Python's list, which isn't optimal when we know the size of the list in advance. numpy is preferable.

FBA is quite faster than PTA

The situation should be reversed.

Dovier-Piazza-Policriti: Paige-Tarjan Bonic

In the paper where the Dovier-Piazza-Policriti algorithm is presented the authore discuss an improvement (section 6.1) which is used also in the tests section.

is_integer_graph=False crashes

[fandreuz@fatou fandreuz]$ python3 bisi/src/timer.py
[(1, 2), (2, 4), (3, 3)]
doing n=10
Traceback (most recent call last):
  File "bisi/src/timer.py", line 45, in <module>
    fba = timeit.timeit('dovier_piazza_policriti(graph, is_integer_graph=False)', setup=setup, number=number) / number
  File "/usr/lib64/python3.6/timeit.py", line 233, in timeit
    return Timer(stmt, setup, timer, globals).timeit(number)
  File "/usr/lib64/python3.6/timeit.py", line 178, in timeit
    timing = self.inner(it, self.timer)
  File "<timeit-src>", line 14, in inner
  File "/u/f/fandreuz/.local/lib/python3.6/site-packages/bisimulation_algorithms/dovier_piazza_policriti/fba.py", line 370, in bisimulation_contraction
    return back_to_original(collapsed_graph_nodes, node_to_idx)
  File "/u/f/fandreuz/.local/lib/python3.6/site-packages/bisimulation_algorithms/utilities/graph_normalization.py", line 74, in back_to_original
    return [tuple(idx_to_node[idx] for idx in block) for block in partition]
  File "/u/f/fandreuz/.local/lib/python3.6/site-packages/bisimulation_algorithms/utilities/graph_normalization.py", line 74, in <listcomp>
    return [tuple(idx_to_node[idx] for idx in block) for block in partition]
TypeError: 'int' object is not iterable

Symbolic algorithm

Implement the symbolic algorithm from Dovier-Piazza-Policriti, Section 9.

Priority queue when we want to process in order of rank

Implement Single Edge Deletion

In the paper An incremental bisimulation algorithm there's an other algorithm for the incremental computation of maximum bisimulation, namely the one for Single Edge Deletion (page 9 of 13). It should be straightforward to implement.

Add unified and simple to use API

The current API that forces users to select a specific algorithm may be confusing to new users. Add an api with sensible defaults for those users.

Use vertexes_to_color in paige_tarjan notebook

Unique term for "initial partition"

At the moment we use the terms initial_partition, labeling set and labeling function, in documentation, comments and code. We should adotpt a unique term to avoid misunderstandings.

Support k-bisimulation

k-bisimulation is a variant of bisimulation where topological features of nodes are only considered within a local neighborhood of a certain radius. Usually bisimulation is:

• too hard to compute;
• gives an unusable partitioning

Clean tests

It would be nice to organize better the test cases. Maybe using numpy (or something similar) to store graphs(?)

Support labeled edges

Labeled edges are ubiquitous in practical applications of bisimulation (concurrency theory [1], XML indexing [2])

[1]: Kanellakis, Paris C., and Scott A. Smolka. "CCS expressions, finite state processes, and three problems of equivalence." Information and computation 86.1 (1990): 43-68.
[2]: Yi, Ke, et al. "Incremental maintenance of XML structural indexes." Proceedings of the 2004 ACM SIGMOD international conference on Management of data. 2004.