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.

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,)]

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,)]

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.

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.

To install the package:

> pip install bispy

To uninstall the package:

> pip uninstall bispy

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

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

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.

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).

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!

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)

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