Unverified Commit d49e7b8a authored by Merlin's avatar Merlin 💧
Browse files

Documentation update to include aconjunctive

parent 06f8f75a
Pipeline #11183 passed with stages
in 6 minutes and 51 seconds
......@@ -2,7 +2,7 @@
[[_TOC_]]
COOL is a generic reasoner for modal, hybrid and fixpoint logics, developed jointly at FAU Erlangen-Nürnberg and the Australian National University ([Dirk Pattinson](http://users.cecs.anu.edu.au/~dpattinson/)); it can be instantiated to any modal, hybrid or alternation-free fixpoint logic admitting an axiomatization in terms of so-called rank-1 rules or axioms. Current instantiations include multimodal K (i.e. the description logic ALC), serial monotone neighborhood logic (the next-step logic of game logic GL), and coalition logic (the next-step logic of alternating temporal logic ATL). COOL currently supports global assumptions, i.e. general TBoxes, nominals, satisfaction operators; the latter features are similar in expressivity to Boolean ABoxes. COOL implements two global caching algorithms as separate reasoner cores: the global caching algorithm described in [this paper](http://link.springer.com/chapter/10.1007/978-3-642-14203-1_5) (also available [here](https://www8.cs.fau.de/wp-content/uploads/staff/schroeder/papers/hyGlobalCaching.pdf)) and the global caching algorithm for alternation-free fixpoint logics described in [this paper](http://drops.dagstuhl.de/opus/volltexte/2016/6172/pdf/LIPIcs-CONCUR-2016-34.pdf); the latter reasoner core decides the alternation-free mu-calculi over all supported logics (including in particular CTL, ATL and the star-nesting free fragment of GL). **Recently, the fixpoint core has been extended with support for aconjunctive mu-calculi via permutation games, as described [here](https://arxiv.org/pdf/1710.08996.pdf); an archive containing according binaries, a formula generator and benchmarking scripts is available [here](https://www8.cs.fau.de/wp-content/uploads/media/research/cool/artifact.zip).**
COOL is a generic reasoner for modal, hybrid and fixpoint logics, developed jointly at FAU Erlangen-Nürnberg and the Australian National University ([Dirk Pattinson](http://users.cecs.anu.edu.au/~dpattinson/)); it can be instantiated to any modal, hybrid or alternation-free fixpoint logic admitting an axiomatization in terms of so-called rank-1 rules or axioms. Current instantiations include multimodal K (i.e. the description logic ALC), serial monotone neighborhood logic (the next-step logic of game logic GL), and coalition logic (the next-step logic of alternating temporal logic ATL). COOL currently supports global assumptions, i.e. general TBoxes, nominals, satisfaction operators; the latter features are similar in expressivity to Boolean ABoxes. COOL implements two global caching algorithms as separate reasoner cores: the global caching algorithm described in [this paper](http://link.springer.com/chapter/10.1007/978-3-642-14203-1_5) (also available [here](https://www8.cs.fau.de/wp-content/uploads/staff/schroeder/papers/hyGlobalCaching.pdf)) and the global caching algorithm for alternation-free fixpoint logics described in [this paper](http://drops.dagstuhl.de/opus/volltexte/2016/6172/pdf/LIPIcs-CONCUR-2016-34.pdf); the latter reasoner core decides the alternation-free mu-calculi over all supported logics (including in particular CTL, ATL and the star-nesting free fragment of GL). **Recently, the fixpoint core has been extended with support for aconjunctive mu-calculi via permutation games, as described [here](https://arxiv.org/pdf/1710.08996.pdf). This is implemented since COOL 2.0.**
## Installation
......@@ -20,13 +20,6 @@ We provide multiple options to get your hands on an up to date COOL executables:
There are additional features yet to be merged so use at your own risk:
#### Aconjunctive mu-Calculi
The current master can only work with **alternation free** mu-calculi so if you want to work with **aconjunctive** mu-calculi you should look into [the `pgsolver` branch](https://git8.cs.fau.de/software/cool/-/tree/pgsolver) and the related artefacts:
- Docker images unter `cs8service/cool:pgsolver`
- [`cool-static`](https://git8.cs.fau.de/software/cool/-/jobs/artifacts/pgsolver/browse/cool-static?job=nix-build)
- [Dynamically linked executables](https://git8.cs.fau.de/software/cool/-/jobs/artifacts/pgsolver/browse/dynamic?job=build).
#### Modelchecking
If you want to do modelchecking you should look into [the `modcheck` branch](https://git8.cs.fau.de/software/cool/-/tree/modcheck) and the related artefacts:
......@@ -48,6 +41,7 @@ directory (e.g. `/usr/include`, `/usr/lib/ocaml`, or `.`).
Runtime dependencies:
- readline
- minisat (at least minisat 2)
- pgsolver
- m4
- zlib
- ncurses (for the debugger and the repl-example)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment