COOL - The Coalgebraic Ontology Logic Reasoner

• COOL - The Coalgebraic Ontology Logic Reasoner
  • Installation
    • Prebuilt Binaries
      • Modelchecking
    • Nix
    • Dependencies
    • Building from Source
      • Building from source in one script
  • Usage
    • Coalition Logic
  • Experimental Results
  • Literature

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); 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 (also available here) and the global caching algorithm for alternation-free fixpoint logics described in this paper; 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. This is implemented since COOL 2.0.

Installation

Prebuilt Binaries

Visit the release page to get released versions of COOL.

We provide multiple options to get your hands on an up to date COOL executables:

• Docker images on Dockerhub as cs8service/cool tagged with the branch they were published from i.e. cs8service/cool:master would give you the latest release candidate of COOL. You could e.g. use it to check coalition logic formulas echo '<{1 2}> C & [{1 2}] ~C' | docker run -i cs8service/cool:master sat CL
• A prebuilt static binary of the latest release candidate is available as cool-static. Run it e.g. coalg sat CL <<< '<{1 2}> C & [{1 2}] ~C'
• Dynamically linked executables without included dependencies are also available in the artefacts.

There are additional features yet to be merged so use at your own risk:

Modelchecking

If you want to do modelchecking you should look into the modcheck branch and the related artefacts:

• Docker images unter cs8service/cool:modcheck
• cool-static
• Dynamically linked executables.

Nix

We also provide batteries included build infrastructure using nix. See the respective documentation on how to use nix to develop or compile COOL.

You could compile and intall COOL and all it's dependencies using nix by running nix-env -f https://git8.cs.fau.de/software/cool/-/archive/master/cool-master.tar.gz -iA cool

Dependencies

Install ocaml include files, minisat include files. Place them in the include directory (e.g. /usr/include, /usr/lib/ocaml, or .).

Runtime dependencies:

• minisat (at least minisat 2)
• pgsolver
• m4
• zlib

On Debian, Ubuntu or other apt based Linux distrubutions you can use the setup script and the OCaml setup script to install the required dependencies.

Building from Source

To build the cool executables

dune build

Run it with

dune exec cool

To build everything just run

dune build @all

If you want the executables statically linked, then run the build with the flag --profile=static i.e.

dune build --profile=static

Note that static linking also requires the dependencies to be statically available which might not be included in your operating system packages.

Building from source in one script

Install the packaged dependencies (see above). Install minisat, e.g. manually via git:

git clone https://git8.cs.fau.de/software/cool
cd cool
./ci/apt-setup.sh
./ci/ocaml-setup.sh
dune build @all

Usage

To see a longer list of example formulas, just run the testsuite:

  dune exec cool-testsuite

Coalition Logic

Some formulas are

[{1}] C & [{ 2 }] ~C
[{1}] C & <{ 2 }> ~C
[{1}] C & <{ 1 2 }> ~C
<{ 1 2 }> C & <{ 1 2 3 4 5 6 7 8 9 10 }> ~C
<{ 1 2 }> C & <{ 1 2 3 4 5 6 7 8 9 }> ~C
<{ 1 2 }> C & <{ 1 2 }> ~C
<{ 1 2 }> C & [{ 1 2 }] ~C

So call for example:

./coalg sat CL  <<< '<{ 1 2 }> C & [{ 1 2 }] ~C'
# or via docker
echo '<{1 2}> C & [{1 2}] ~C' | docker run -i cs8service/cool:master sat CL

Experimental Results

Recent benchmarking results that compare MLSolver with the permutation game solving core of COOL for aconjunctive formulas can be found in this file: benchmarks.zip

We also compare the runtimes of three variants of the CTL-instantiation of the alternation-free fixpoint-reasoning core of COOL (with different frequencies of intermediate propagation -- always, never and adaptive) with TreeTab and GMUL on various series of CTL formulas; for descriptions of the benchmark formulas and the provers TreeTab and GMUL, see An Experimental Comparison of Theorem Provers for CTL, R. Goré, J. Thomson and F. Widmann, TIME 2011. More benchmarking results can be found in this file: comparison_ctl.zip

Literature

• A system description of COOL (COOL --- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions, D. Gorin, D. Pattinson, L. Schröder, F. Widmann and T. Wißmann) has been published at IJCAR 2014.
• A paper on global caching for alternation-free fixpoint logics (Global Caching for the Alternation-free µ-Calculus, D. Hausmann, L. Schröder and C. Egger) has been published at CONCUR 2016.