README.md 3.74 KB
Newer Older
1
# CoPaR, the `Co`algebraic `Pa`rtition `R`efiner
Hans-Peter Deifel's avatar
Hans-Peter Deifel committed
2

3
Copar implements a generic partition refinement algorithm with a fast run-time.
Thorsten Wißmann's avatar
Thorsten Wißmann committed
4
The genericity of copar stems from the coalgebraic approach and covers the minimization of
Hans-Peter Deifel's avatar
Hans-Peter Deifel committed
5

6 7 8 9
  - Transition Systems (under strong bisimilarity)
  - (Tree) Automata (under tree isomorphism)
  - Markov Chains, and other weighed systems (under weighed bisimilarity)
  - and *combinations* thereof (under derived bismilarity notions, e.g. backwards bisimilarity for weighted tree automata).
Hans-Peter Deifel's avatar
Hans-Peter Deifel committed
10

11
The algorithm runs in *O(m log n)* on a system with *n* states and *m*
Thorsten Wißmann's avatar
Thorsten Wißmann committed
12
transitions.
13

14
## Usage
Thorsten Wißmann's avatar
Thorsten Wißmann committed
15 16
Installation instructions can be found in the [install file](INSTALL.md).

Thorsten Wißmann's avatar
Thorsten Wißmann committed
17 18 19
Command line syntax is described in `copar --help` and the input
file syntax in `copar help`. The core partition-refinement algorithm can be
called by
Hans-Peter Deifel's avatar
Hans-Peter Deifel committed
20

21
    ./copar refine FILENAME
Hans-Peter Deifel's avatar
Hans-Peter Deifel committed
22

Hans-Peter Deifel's avatar
Hans-Peter Deifel committed
23
Examples for input files are in the directory `examples/`.
24

25 26 27
## Benchmarks

Extensive benchmarks of CoPaR on different input files can be found at
28
[git8.cs.fau.de/software/copar-benchmarks](https://git8.cs.fau.de/software/copar-benchmarks).
29 30 31

Micro-Benchmarks for internal data structures and routines are available in the
`bench/` directory and can be executed with `stack bench`.
Thorsten Wißmann's avatar
Thorsten Wißmann committed
32 33 34

## Literature

Thorsten Wißmann's avatar
Thorsten Wißmann committed
35
On coalgebraic partition refinement:
Thorsten Wißmann's avatar
Thorsten Wißmann committed
36

Thorsten Wißmann's avatar
Thorsten Wißmann committed
37 38
  - [Generic Partition Refinement and Weighted Tree Automata](https://link.springer.com/chapter/10.1007/978-3-030-30942-8_18) ([Hans-Peter Deifel](https://www8.cs.fau.de/deifel), [Stefan Milius](https://www8.cs.fau.de/milius), [Lutz Schröder](http://www8.informatik.uni-erlangen.de/schroeder/), [Thorsten Wißmann](http://www8.informatik.uni-erlangen.de/thorsten)) In: *Formal Methods – The Next 30 Years*, pp. 280–297 (Best Theory Paper Award) \[[PDF](https://link.springer.com/chapter/10.1007/978-3-030-30942-8_18)\] \[[Preprint PDF](https://arxiv.org/abs/1811.08850)\] \[[DOI: 10.1007/978-3-030-30942-8_18](https://dx.doi.org/10.1007/978-3-030-30942-8_18)\]
  - [Efficient and Modular Coalgebraic Partition Refinement](https://lmcs.episciences.org/6064) ([Thorsten Wißmann](http://www8.informatik.uni-erlangen.de/thorsten), [Ulrich Dorsch](https://www8.cs.fau.de/ulrich), [Stefan Milius](https://www8.cs.fau.de/milius), [Lutz Schröder](http://www8.informatik.uni-erlangen.de/schroeder/)) In: *Logical Methods in Computer Science*, Volume 16, Issue 1  \[[PDF](https://lmcs.episciences.org/6064)\] \[[DOI: 10.23638/LMCS-16(1:8)2020](https://dx.doi.org/10.23638/LMCS-16(1:8)2020)\]
39
  - [Hans-Peter Deifel](https://www8.cs.fau.de/deifel), [Master's Thesis](https://hpdeifel.de/master-thesis-deifel.pdf), 2019
Thorsten Wißmann's avatar
Thorsten Wißmann committed
40 41
  - Conference version of the above journal article: [Efficient Coalgebraic Partition Refinement](https://drops.dagstuhl.de/opus/volltexte/2017/7793/) ([Ulrich Dorsch](https://www8.cs.fau.de/ulrich), [Stefan Milius](https://www8.cs.fau.de/milius), [Lutz Schröder](http://www8.informatik.uni-erlangen.de/schroeder/), [Thorsten Wißmann](http://www8.informatik.uni-erlangen.de/thorsten)) In: *Proc. 28th International Conference on Concurrency Theory (CONCUR 2017)*  \[[PDF](https://drops.dagstuhl.de/opus/volltexte/2017/7793/)\] \[[Preprint PDF](https://arxiv.org/abs/1705.08362)\] \[[DOI: 10.4230/LIPIcs.CONCUR.2017.32](https://dx.doi.org/10.4230/LIPIcs.CONCUR.2017.32)\]

Thorsten Wißmann's avatar
Thorsten Wißmann committed
42

Thorsten Wißmann's avatar
Thorsten Wißmann committed
43
On reachability:
Thorsten Wißmann's avatar
Thorsten Wißmann committed
44

45
  - [A Coalgebraic View on Reachability](https://arxiv.org/abs/1901.10717) ([Thorsten Wißmann](http://www8.informatik.uni-erlangen.de/thorsten), [Stefan Milius](https://www8.cs.fau.de/milius), [Shin-ya Katsumata](http://group-mmm.org/~s-katsumata/index-e.html), [Jérémy Dubut](http://group-mmm.org/~dubut/)) In: *Commentationes Mathematicae Universitatis Carolinae*, 60, 4, pp. 605-638  [Preprint PDF](https://arxiv.org/abs/1901.10717) [DOI: 10.14712/1213-7243.2019.026](https://dx.doi.org/10.14712/1213-7243.2019.026)
Thorsten Wißmann's avatar
Thorsten Wißmann committed
46