EN | DE
Theoretische Informatik

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

research:software:cool [2017/11/07 17:11]
hausmann [Downloads]
research:software:cool [2018/01/17 20:49] (current)
hausmann
Line 2: Line 2:
 (See also [[https://cal8.cs.fau.de/redmine/projects/cool|the COOL project page]]) (See also [[https://cal8.cs.fau.de/redmine/projects/cool|the COOL project page]])
  
-COOL is a generic reasoner for modal, hybrid and fixpoint logics, developed jointly at FAU Erlangen-Nürnberg and the Australian National University ([[http://users.cecs.anu.edu.au/~dpattinson/|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 [[http://link.springer.com/chapter/10.1007/978-3-642-14203-1_5|this paper]] (also available [[http://www8.informatik.uni-erlangen.de/~schroeder/papers/hyGlobalCaching.pdf|here]]) and the global caching algorithm for alternation-free fixpoint logics described in [[http://drops.dagstuhl.de/opus/volltexte/2016/6172/pdf/LIPIcs-CONCUR-2016-34.pdf|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 [[https://arxiv.org/pdf/1710.08996.pdf|here]].**+COOL is a generic reasoner for modal, hybrid and fixpoint logics, developed jointly at FAU Erlangen-Nürnberg and the Australian National University ([[http://users.cecs.anu.edu.au/~dpattinson/|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 [[http://link.springer.com/chapter/10.1007/978-3-642-14203-1_5|this paper]] (also available [[http://www8.informatik.uni-erlangen.de/~schroeder/papers/hyGlobalCaching.pdf|here]]) and the global caching algorithm for alternation-free fixpoint logics described in [[http://drops.dagstuhl.de/opus/volltexte/2016/6172/pdf/LIPIcs-CONCUR-2016-34.pdf|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 [[https://arxiv.org/pdf/1710.08996.pdf|here]]; an archive containing according binaries, a formula generator and benchmarking scripts is available {{research:cool:artifact.zip|here}}.**
  
 ==== Downloads ==== ==== Downloads ====