1 Introduction

Modal and temporal logics are established tools in the specification and verification of systems. While many such logics are interpreted over relational transition systems, the semantics of quite a number of important logics goes beyond the relational setup, involving, for instance, probabilities [20, 30], concurrent games as in alternating-time logics [1, 36], monotone neighbourhoods structures as in game logic [34] and concurrent dynamic logic [37], or integer transition weights as in the multigraph semantics [5] of the graded \(\mu \)-calculus [25]. Coalgebraic logic [4] provides a uniform semantic and algorithmic framework for these logics, based on the paradigm of universal coalgebra [38]. It provides reasoning algorithms of optimal complexity at various levels of expressiveness, up to the coalgebraic \(\mu \)-calculus [3, 21,22,23]. These algorithms are parametric in the transition type of systems (weighted, probabilistic, game-based etc.) as well as in suitable choices of modalities specific to the given system type. Their instantiation to specific logics requires providing either a set of next-step modal tableau rules satisfying a suitable completeness criterion [41] or, more generally, a plug-in algorithm that determines satisfiability for an extremely simple one-step logic that describes the interaction between modalities, and consists of (conjunctions of) modal operators applied to variables only [29].

The COalgebraic Ontology Logic solver (COOL) provides reasoning support for coalgebraic logics based on these generic algorithms. The first version of the tool [15] provided reasoning support for fixpoint-free coalgebraic hybrid logic with global assumptions, using a global caching principle [13]. In the present paper, we present COOL 2, which provides reasoning support for coalgebraic fixpoint logics, specifically for both the aconjunctive fragment and the alternation-free fragment of the coalgebraic \(\mu \)-calculus. By instantiation, we obtain in particular the first implemented reasoners for the graded \(\mu \)-calculus [26] (for which a set of coalgebraic modal tableau rules has been described in the literature [41]; however, this rule set has later turned out to be incomplete, cf. Remark 2.3) and the alternating-time \(\mu \)-calculus [1]. We describe the structure of the tool including implementational details, and present evaluation results, focusing on the graded \(\mu \)-calculus and alternating-time temporal logic (ATL). Additional details on the evaluation can be found in the full version [17].

Related Work: We have already mentioned work in coalgebraic logic on which COOL is based [3, 13, 21,22,23, 41]. COOL is conceptually a successor of the Coalgebraic Logic Satisfiability Solver (CoLoSS) [2] but does not share any of its code. CoLoSS implements fixpoint-free logics, and is entirely unoptimised. The first version of COOL [15] has been evaluated on fixpoint-free next-step logics.

COOL does cover also various relational modal logics, for which there are numerous specialised reasoners, including highly optimised description logic reasoners such as FaCT++ [44], Pellet [42], RACER [18], and HermiT [12]. As these systems do not support fixpoint logics, a comparison would be of limited value. In previous work, COOL has been evaluated on various relational fixpoint logics, and has been shown to perform favourably on Computation Tree Logic [23] (in comparison to reasoners featured in a previous systematic evaluation [14]), as well as on the aconjunctive fragment of the modal \(\mu \)-calculus [22] (in comparison to MLSolver [11]). A reasoner for (next-step) graded modal logic has been evaluated against various description logic reasoners [43], using however the above-mentioned incomplete set of modal tableau rules.

For the same reasons, we refrain from evaluating COOL 2 against reasoners for coalition logic, i.e. the fixpoint-free fragment of the alternating-time \(\mu \)-calculus, such as CLProver [32]. The only implemented reasoner for any fragment of the alternating-time \(\mu \)-calculus that does include fixpoints still appears to be the tableau reasoner TATL for alternating-time temporal logic [6, 7]. TATL has been compared to COOL on random formulas in previous work [23].

2 Satisfiability in the Coalgebraic \(\mu \)-Calculus

COOL 2 is a satisfiability checker for the coalgebraic \(\mu \)-calculus [3], that is, for the extension of coalgebraic modal logic with extremal fixpoint operators. Formulas of this logic are interpreted over coalgebras, where the semantics of modal operators is defined by means of so-called predicate liftings [41]; we recapitulate examples of system types and modalities subsumed by this paradigm in Example 2.1.

Syntax: Formulas are built relative to a set \(\textsf{Var}\) of fixpoint variables and a modal similarity type \(\varLambda \), that is, a set of modal operators with assigned finite arities that is closed under duals, with \(\overline{\heartsuit }\in \varLambda \) denoting the dual of \(\heartsuit \in \varLambda \). Formulas \(\psi ,\phi ,\dots \) of the coalgebraic \(\mu \)-calculus over \(\varLambda \) are given by the grammar

$$\begin{aligned} \psi ,\phi := \bot \mid \top \mid \psi \wedge \phi \mid \psi \vee \phi \mid \heartsuit (\psi _1,\dots ,\psi _n)\mid X\mid \mu X.\,\psi \mid \nu X.\,\psi , \end{aligned}$$

where \(\heartsuit \in \varLambda \) has arity n and \(X\in \textsf{Var}\). A formula \(\chi \) is aconjunctive if for every conjunction \(\psi \wedge \phi \) that is a subformula of \(\chi \), at most one of the formulas \(\psi \) and \(\phi \) contains a free fixpoint variable X that is bound by a least fixpoint operator \(\mu X.\,\) While the logic does not contain negation as an explicit operator, full negation can be defined as usual; e.g. we have \(\lnot \heartsuit \psi =\overline{\heartsuit }\lnot \psi \) and \(\lnot \mu X.\,\psi = \nu X.\,\lnot \psi [\lnot X/X]\), using \(\lnot \lnot X=X\).

Both the theoretical satisfiability checking algorithm and its implementation in COOL 2 operate on the Fischer-Ladner closure [21, 24, 27] of the target formula. The alternation depth (e.g. [21, 29, 33]) of a formula is the maximum depth of dependent alternating nestings of least and greatest fixpoints within the formula. Formulas with alternation depth 1 are alternation-free.

Semantics: Formulas are interpreted over F-coalgebras, that is, structures

$$\begin{aligned} (C,\xi :C\rightarrow FC), \end{aligned}$$

where \(F:\textsf{Set}\rightarrow \textsf{Set}\) is a functor determining the branching type of the systems at hand; thus \(\xi (x)\in FC\) encodes the transitions from \(x\in C\), structured according to F. Modalities \(\heartsuit \in \varLambda \) of arity n are interpreted as predicate liftings, that is, families of maps \(\llbracket \heartsuit \rrbracket _U:(2^U)^n\rightarrow 2^{FU}\) (for \(U\in \textsf{Set}\)) that assign predicates on FU to n-tuples of predicates on U, subject to a naturality condition [35, 40]. On a coalgebra \((C,\xi )\), the semantics of formulas is defined inductively in the usual way for the propositional operators and fixpoints, and by \(\llbracket \heartsuit (\psi _1,\dots ,\psi _n) \rrbracket =\xi ^{-1}[\llbracket \heartsuit \rrbracket _C(\llbracket \psi _1 \rrbracket ,\dots ,\llbracket \psi _n \rrbracket )]\) for modalities.

A closed formula \(\psi \) is satisfiable if there is a coalgebra \((C,\xi )\) and a state \(x\in C\) such that \(x\in \llbracket \psi \rrbracket \). A formula \(\psi \) is valid if \(\lnot \psi \) is not satisfiable.

Example 2.1

  1. (1)

    The standard modal \(\mu \)-calculus [24] is obtained using the functor \(F=\mathcal {P}(A)\times \mathcal {P}\), where A is a fixed set of atoms, the similarity type \(\varLambda =\{\lozenge ,\square ,a,\lnot a\mid a\in A\}\), and predicate liftings

    $$\begin{aligned} \llbracket \lozenge \rrbracket _C(B)&= \{(A,Z)\in 2^A\times 2^C\mid Z\cap B\ne \emptyset \}&\llbracket a \rrbracket _C&= \{(A,Z)\in 2^A\times 2^C\mid a\in A\} \\ \llbracket \square \rrbracket _C(B)&= \{(A,Z)\in 2^A\times 2^C\mid Z\subseteq B\}&\llbracket \lnot a \rrbracket _C&= \{(A,Z)\in 2^A\times 2^C\mid a\notin A\} \end{aligned}$$

    The expressive power of the modal \(\mu \)-calculus is demonstrated by the formulas

    $$\begin{aligned}&\mu X.\,\nu Y.\, (p \wedge \lozenge Y) \vee \lozenge X{} & {} \nu X.\,\mu Y.\, (p \wedge \lozenge X) \vee \lozenge Y. \end{aligned}$$

    The former is a co-Büchi formula expressing the existence of a path on which p holds forever, from some point on; the latter formula expresses the Büchi property that there is a path on which the atom p is satisfied infinitely often.

  2. (2)

    The graded \(\mu \)-calculus [26] allows expressing quantitative properties with the help of modal operators \(\langle n \rangle \) and [n], \(n\in \mathbb {N}\); formulas \(\langle n\rangle \psi \) and \([n]\psi \) then have the intuitive meaning that ‘there are more than n successor states that satisfy \(\psi \)’, and ‘all but at most n successor states satisfy \(\psi \)’, respectively. Its coalgebraic interpretation is based on multigraphs, which are coalgebras for the multiset functor [5]. A graded variant of the above Büchi property is specified, e.g., by the formula \(\nu X.\,\mu Y.\, (p \wedge \langle n\rangle X) \vee \langle n\rangle Y\), which expresses the existence of an infinite \(n+1\)-ary tree such that the atom p is satisfied infinitely often on every path in the tree.

  3. (3)

    The alternating-time \(\mu \)-calculus (AMC) [39] extends coalition logic [36] with fixpoints and (modulo syntax) supports modalities \(\langle D\rangle \) and [D], where \(D\subseteq N\) is a coalition formed by agents from the set \(N=\{1,\ldots ,n\}\) for some fixed \(n\in \mathbb {N}\); formulas \(\langle D\rangle \psi \) and \([D]\psi \) then state that ‘coalition D has a joint strategy to enforce \(\psi \)’ and that ‘coalition D cannot prevent \(\psi \)’, respectively. For instance, the formula \(\nu X.\,\mu Y.\,\nu Z.\, (p \wedge \langle D\rangle X) \vee (q\wedge \langle D\rangle Y)\vee (\lnot q \wedge \langle D\rangle Z)\) expresses that coalition D has a joint multi-step strategy that guarantees that p is visited infinitely often whenever q is visited infinitely often.

Satisfiability Checking: We proceed to recall the satisfiability checking algorithm for the coalgebraic \(\mu \)-calculus that forms the basis of the implementation within COOL 2. This algorithm adapts the automata-based approach to satisfiability checking for the standard \(\mu \)-calculus, and generalises the treatment of modal steps by parametrizing over a solver for the one-step satisfiability problem of the logic, which concerns satisfiability of formulae with exactly one layer of next-step modalities [21]. It thus avoids the necessity of tractable sets of tableaux rules for modal operators. Under mild assumptions on the complexity of the one-step satisfiability problem of the base logic at hand (‘tractability’), the algorithm witnesses a, typically optimal, upper bound \(\textsc {ExpTime}\) for the complexity of the satisfiability problem; unlike a previous algorithm [4], the algorithm thus has optimal runtime also in cases where no tractable sets of modal tableaux rules are known, such as the graded (or, more generally, Presburger) \(\mu \)-calculus (further cases of this kind include the probabilistic \(\mu \)-calculus with polynomial inequalities [21] and the unrestricted form of the alternating-time \(\mu \)-calculus with disjunctive explicit strategies [16]).

The algorithm constructs and solves a parity game that characterises satisfiability of the input formula \(\chi \). In this game one player attempts to construct a tableau structure for \(\chi \) while the opposing player attempts to refute the existence of such a structure. Modal steps in this tableau construction are treated by using instances of the one-step satisfiability problem for the logic at hand, thereby generalising traditional modal tableau rules. The winning condition of the game is encoded by a non-deterministic parity automaton \(\textsf{A}_\chi \), reading infinite words that encode sequences of step-wise formula evaluations (so-called formula traces) within a coalgebra; such words encode branches in the constructed tableau structure. Conjunctions give rise to nondeterminism in this automaton, and the parity condition of the automaton is used to accept exactly those words that encode sequences of formula evaluations in which some least fixpoint is unfolded infinitely often. To use the language accepted by \(\textsf{A}_\chi \) as the winning condition in a parity game, we transform \(\textsf{A}_\chi \) to an equivalent deterministic parity automaton \(\textsf{B}_\chi \). This automaton then is paired with the tableau construction to yield a parity game in which the existential player aims to show the existence of a tableau structure in which all branches are rejected by \(\textsf{B}_\chi \), and that is built in such a way that modalities always are jointly one-step satisfiable. To ensure the latter property, the modal moves in the game invoke instances of the one-step satisfiability problem of the base logic. For more details on one-step satisfiability and the overall algorithm, see [17, 21].

Corollary 2.2

([21]). Suppose that the one-step satisfiability problem is tractable. Then the satisfiability problem of the corresponding instance of the coalgebraic \(\mu \)-calculus is in \(\textsc {ExpTime}\).

Remark 2.3

As mentioned above, previous algorithms for the coalgebraic \(\mu \)-calculus (also implemented in COOL 2) rely on complete sets of modal tableau rules, specifically on one-step cutfree complete sets of so-called one-step rules [41]; such rules (in their incarnation as tableau rules) have a premiss with exactly one layer of modal operators and a purely propositional conclusion. A typical example is the usual tableau rule for the modal logic K: ‘To satisfy \(\square a_1\wedge \dots \wedge \square a_n\wedge \lnot \square a_0\), satisfy \(a_1\wedge \dots \wedge a_n\wedge \lnot a_0\)’. It has been shown that the existence of a tractable one-step cutfree complete set of one-step rules implies tractability of one-step satisfiability [29], i.e. the approach via one-step satisfiability is more general.

As indicated in the introduction, a tractable one-step cutfree complete set of one-step rules for graded modal logic has been claimed in the literature [41, 43] but has since turned out to be incomplete; we give a counterexample in the full version [17]. (A similar rule for Presburger modal logic [28] has also been shown to be in fact incomplete [29].)

3 Implementation

The previous version COOL [15] only implements fixpoint-free (coalgebraic) logics, such as standard modal logic, probabilistic modal logic, or coalition logic. The main novelty of the new version COOL 2, described here, is

  • the addition of fixpoint constructs to the previously implemented logics, supporting alternation-free and aconjunctive fragments of the resulting \(\mu \)-calculi, and implementing on-the-fly solving to allow early termination

  • support for treating modal steps both by tableaux rules (when a suitable rule set exists), and by one-step satisfiability checking (in the remaining cases)

In more detail, COOL 2 is written in OCaml and implements the satisfiability checking algorithm described in Sect. 2, treating modal steps by solving instances of the one-step satisfiability problemFootnote 1. For logics where a suitable set of modal tableau rules is implemented, those are used for the treatment of modal steps, rather than relying on one-step satisfiability (unless the user explicitly chooses otherwise); in these cases, COOL 2 essentially implements the algorithm described in [29]. The current implementation supports the alternation-free and the aconjunctive fragments of the standard \(\mu \)-calculus (both serial and non-serial), the monotone \(\mu \)-calculus [19], the alternating-time \(\mu \)-calculus (i.e. coalition logic with fixpoint operators), and the graded \(\mu \)-calculus. Tractable tableaux rules are available for all cases except for the graded \(\mu \)-calculus, for which COOL 2 uses the one-step satisfiability algorithm to decide satisfiability. In particular, COOL 2 is the only existing reasoner for the graded \(\mu \)-calculus (as well as the only reasoner covering the alternating-time \(\mu \)-calculus beyond ATL).

The concrete logic used can be selected via a command-line parameter setting up the data structures in COOL 2 accordingly before parsing and checking the syntax of the given formula \(\chi \). COOL 2 then builds the determinised automaton \(\textsf{B}_\chi \), yielding the parity game described above in a step-wise manner, repeatedly adding nodes in expansion steps that explore the game. In the case of simpler alternation-free formulas, the Miyano-Hayashi method [31] is used to construct \(\textsf{B}_\chi \), resulting in asymptotically smaller games with a Büchi winning condition; for the more involved aconjunctive formulas, the implementation uses the permutation method for determinisation of limit-deterministic parity automata [9, 22]. Nodes in the constructed game are marked as either unexpanded, undecided, unsatisfiable, or satisfiable.

Optional solving steps may take place at any point during the construction of \(\textsf{B}_\chi \), depending on runtime parameters of COOL 2; these steps compute the winning regions of the partial game that has been constructed so far and accordingly mark nodes as satisfiable or unsatisfiable, if possible. The reasoner terminates as soon as the initial node is marked satisfiable or unsatisfiable. If this does not allow for early termination, the game eventually becomes fully explored, at which point a final (obligatory) solving step for the complete game is guaranteed to mark the initial node, thereby ensuring termination.

We detail the implementation of the two main procedures within COOL 2.

Implementation of Expansion Steps. The propositional expansion steps in the game construction for nodes v are performed using the propositional satisfiability solver \(\textsf{MiniSat}\) [8] to compute a word that encodes consistent propositional formula manipulations for v. Afterwards, the successor of v in \(\textsf{B}_\chi \) under this word is computed and added to the game.

When the one-step satisfiability based algorithm of COOL 2 is used, modal expansion steps for nodes v create new game nodes for each subset \(\kappa \) of the modalities that are to be jointly satisfied at v; this is done by computing the successor of v in \(\textsf{B}_\chi \) that is reached by manipulating each formula from \(\kappa \).

When the tableau-based algorithm of COOL 2 is used, the modal expansion step for a node v instead computes all applications of a modal rule matching v and inserts, for each such rule application, and each conjunctive clause \(\kappa \) in the conclusion of the rule application, the new game node that is reached from v in \(\textsf{B}_\chi \) by manipulating the modalities that constitute \(\kappa \). Intuitively, using tableau rules reduces the search space by only adding nodes found in the conclusion of some matching rule application.

Any node that is added by some expansion step is initially marked as undecided. Crucially, all expansion steps perform on-the-fly determinisation, that is, given a game node v and a word that encodes a sequence of formula manipulations, the newly added game node is computed using only the information stored in v.

Implementation of Solving Steps. A single solving step computes the winning regions in the parity game that has been constructed up to this point, and marks nodes accordingly. The game solving is done using either the parity game solver \(\textsf{PGSolver}\) [10] or a native implementation provided by COOL 2 that solves the game by fixpoint iteration.

If the one-step satisfiability-based algorithm is used, an assigned modal node v is satisfiable if its modalities are jointly one-step satisfiable in those successors of v that are satisfiable themselves. An enumerative representation of the game thus contains existential moves to all subsets \(\varPi \) of subsets of modalities of v that are sufficiently large for one-step satisfaction of the modalities of v, followed by universal moves to nodes induced by any \(\kappa \in \varPi \); the full game thus is of doubly-exponential size. This can be avoided by inlining the modal steps, thereby evading the intermediate nodes \(\varPi \). The winning region can then be computed in single-exponential time by using COOL 2’s native fixpoint iteration over a function that computes the two-tiered modal steps in one go.

Decision procedures for the one-step satisfiability problems in the relational and the graded case are implemented in COOL 2 along the lines of the algorithms described in [21, Example 6] (in the graded case, nondeterministic guessing is replaced with a recursive search procedure).

If the algorithm based on modal tableau rules is used, the treatment of modal steps follows the tableaux-based algorithm that is given in [3]. States v are satisfiable if for all rule applications that match v, the conclusion of the application contains a conjunctive clause \(\kappa \) such that the node induced by \(\kappa \) is satisfiable.

COOL 2 also allows the user to specify the desired frequency of optional game solving steps, including the options \(\textsf{once}\) and \(\textsf{adaptive}\). With the option \(\textsf{once}\), no intermediate solving takes place so that the game is fully constructed and solved just once, at the very end of the execution. With the option \(\textsf{adaptive}\), intermediate solving takes places, but the frequency of solving reduces as the size of the constructed graph increases; this option implements on-the-fly solving and allows for finishing early in cases where a small model or refutation exists.

4 Evaluation

We conduct experiments in order to evaluate the performance of the various algorithms implemented in COOL in comparison with each other, as well as in comparison with other tools (where applicable).Footnote 2 Complete definitions of all formula series used in the evaluation as well as additional experimental results can be found in the full version [17].

Experiments: In a first experiment, we compare COOL 2 with the established reasoner FaCT++, which supports the description logic \(\mathcal {SROIQ}(\mathcal {D})\) (subsuming fixpoint-free graded modal logic), using the following series of formulas from Snell et al. [43].

$$\begin{aligned} \textsf{Cardinality}(n)&:= \langle n - 1 \rangle \lnot p \wedge \langle n - 1 \rangle p \wedge [n]\lnot q \wedge [ n ] q \end{aligned}$$
(Sat)
$$\begin{aligned} \textsf{CardinalityU}(n)&:= \langle n - 1 \rangle \lnot p \wedge \langle n - 1 \rangle p \wedge [n]\lnot q \wedge [ n - 1] q \end{aligned}$$
(UnSat)

Intuitively, the satisfiable \(\textsf{Cardinality}(n)\) formulas express that there are at least 2n successors and that both q and \(\lnot q\) are satisfied in at most n successors, each; similarly the unsatisfiable \(\textsf{CardinalityU}(n)\) formulas state that there are at least 2n successors, and that q and \(\lnot q\) hold in at most n and \(n-1\) successors, respectively; the latter statements imply that there are at most \(2n-1\) successors, yielding a contradiction.

Going beyond next-step formulas, we continue by devising various complex series of graded \(\mu \)-calculus formulas that involve (nested) fixpoints and express non-trivial properties of graded trees, automata and games.

  • We obtain a series of unsatisfiable formulas by requiring the existence of an \(n+1\)-branching tree in which p holds everywhere while at the same time requiring that this tree contains some state with \(n+2\) successors that satisfy p:

    $$\begin{aligned} \textsf{TreeU}(n)&= (\nu X.\, \langle n \rangle (p\wedge X)\wedge [n+1]\lnot p) \wedge (\mu Y.\,\langle n+1\rangle p\vee \langle n\rangle (p\wedge Y)) \end{aligned}$$
    (UnSat)

  • Next we turn our attention to graded formulas involving parity conditions. We devise a series of valid formulas expressing that graded parity automata can be transformed to graded Büchi automata accepting a superlanguage of the original automaton:

    $$\begin{aligned} \textsf{ParityToBuechi}(n,k):=\textsf{Parity}(n,k)\rightarrow \textsf{Buechi}(n,k) \end{aligned}$$
    (Valid)

    Here, \(\textsf{Parity}(n,k)\) encodes parity acceptance with k priorities and grade n while \(\textsf{Buechi}(n,k)\) expresses Büchi acceptance by a nondeterministic automaton that eventually guesses the maximal priority that occurs infinitely often; the negated formula \(\lnot \textsf{ParityToBuechi}(n,k)\) is unsatisfiable.

  • Rabin conditions are given by families of pairs \(\langle i_j,f_j\rangle _{j\le k}\) of sets \(i_j,f_j\) of states, and express the constraint that there is some \(j\le k\) such that states from \(i_j\) (infinite) are visited infinitely often and states from \(f_j\) (finite) are visited only finitely often. We can express Rabin conditions with k pairs (and one-step property \(\psi \)), Büchi properties and satisfaction of single Rabin-pairs by formulas \(\textsf{Rabin}(k, \psi )\), \(\textsf{Buechi}(f,\psi )\) and \(\textsf{RabinPair}(i,f,\psi )\), respectively. Then we obtain valid formulas stating that the existence of an \(n+1\)-branching tree that satisfies the Rabin condition on each path implies that there is a path satisfying a simpler Büchi condition or a single Rabin-pair, respectively:

    $$\begin{aligned} \textsf{RabinToBuechi}(k,n)&:=\textsf{Rabin}(k,\langle n\rangle )\rightarrow \textsf{Buechi}(i_1\vee \ldots \vee i_k,\langle 0\rangle ) \end{aligned}$$
    (Valid)
    $$\begin{aligned} \textsf{RabinToRPair}(k,n)&:= \textsf{Rabin}(k,\langle n\rangle )\rightarrow \textstyle \bigvee _{1\le j\le k}\textsf{RabinPair}(i_j,f_j,\langle 0\rangle ) \end{aligned}$$
    (Valid)

  • Coming to games, we specify the winning regions in graded Büchi and Rabin games by formulas \(\textsf{BuechiG}(f,n)\) and \(\textsf{RabinG}(k,n)\), respectively; in such graded games, players are required to have at least n winning moves at their nodes in order to win. The following valid formulas then express that winning strategies in graded Rabin games with k pairs guarantee that some node from \(i_1\cup \ldots \cup i_k\) is visited infinitely often:

    $$\begin{aligned} \textsf{RabinGame}(k,n):=\textsf{RabinG}(k,n)\rightarrow \textsf{BuechiG}(i_1\vee \ldots \vee i_k,n) \end{aligned}$$
    (Valid)

In a final experiment on alternating-time formulas, we compare COOL 2 with TATL [6] on the ATL example formulas given in [6] as well as on additional formula series. For instance, we turn the formula \(\langle \!\langle 1\rangle \!\rangle G p \wedge \lnot \langle \!\langle 2\rangle \!\rangle F \langle \!\langle 1\rangle \!\rangle G p\) (written here using ATL syntax) from [6] into a series \(\textsf{Nest}(n)\) with increasing number of nested operators; formulas then alternatingly are satisfiable and unsatisfiable:

$$\begin{aligned} \chi (0)&=p&\chi (i+1)&=\lnot \langle \!\langle 2\rangle \!\rangle F \langle \!\langle 1\rangle \!\rangle G \chi (i)&\textsf{Nest}(n)&= \langle \!\langle 1\rangle \!\rangle G p \wedge \chi (n), \end{aligned}$$

Results: We conducted all experiments on a virtual machine with four \(2,3\)GHz vCPUs processors and 8GB of RAM. We compare with a 64-bit binary of FaCT++ v1.6.5 and with TATL. We compute all results with a timeout of 60 seconds and average the results over multiple executions. For the execution and measurement we use hyperfineFootnote 3. Below, ‘COOL’ and ‘COOL on-the-fly’ refer to invoking COOL 2 with solving rate \(\textsf{once}\) and \(\textsf{adaptive}\), respectively.

Fig. 1.
figure 1

Runtimes for \(\textsf{Cardinality}(n)\)

Full size image
Fig. 2.
figure 2

Runtimes for \(\textsf{CardinalityU}(n)\)

Full size image

Results for the \(\textsf{Cardinality}\) and \(\textsf{CardinalityU}\) series are shown in Fig. 1 and Fig. 2, respectively. From \(n=10\) and \(n=8\) onwards, COOL 2 outperforms FaCT++ considerably. An explanation for this could be that FaCT++ appears to treat multiplicities in a naïve way while COOL 2 employs the more efficient one-step satisfiability algorithm.

Fig. 3.
figure 3

Runtimes for \(\textsf{TreeU}(n)\)

Full size image
Fig. 4.
figure 4

Runtimes for \(\lnot \textsf{ParityToBuechi}(n,k)\)

Full size image

Results for the unsatisfiable tree property are shown in Fig. 3. As these formulas contain fixpoint operators, a comparison with FaCT++ is not possible. While COOL 2 is generally capable of handling quite large branching factors, this experiment showcases the drawbacks of on-the-fly solving in the case that a formula cannot be decided early so that repeated attempts of solving the game early lead to overhead computations.

Runtimes for COOL 2 (using on-the-fly solving) on the unsatisfiable series of parity formulas \(\lnot \textsf{ParityToBuechi}(n,k)\) are shown in Fig. 4. The results indicate that increasing the number of priorities k has a much stronger effect on the runtime than increasing multiplicities n in the modalities. This is in accordance with expectations as increasing k leads to much larger determinized automata and resulting satisfiabilty games, while increasing n only complicates the modal steps in the game while leaving the global game structure unchanged.

Results for the Rabin families of formulas are given in the table below, with \(\dagger \) indicating a timeout of 60 s. COOL 2 is able to handle reasonably large formulas describing Rabin properties of automata and games, with the series for \(n=1\) expressing properties of standard automata (solved using tableau rules), and the series with \(n=2\) properties of graded automata with multiplicity 2 (solved using one-step satisfiability).

figure a
Fig. 5.
figure 5

Runtimes for the ATL series \(\textsf{Nest}(n)\)

Full size image

In accordance with previous experiments on random ATL formulas of larger sizes in [23], COOL 2 generally outperforms TATL by a large margin, starting from formulas containing at least five modalities or involving nesting of temporal operators; this trend is confirmed by Fig. 5 which shows the stepped execution times for the series \(\textsf{Nest}\) that alternates between being satisfiable and unsatisfiable

In summary, COOL 2 shows promising performance in comparison to TATL and FaCT++, as well as for practical applicability. On graded formulas without fixpoints, COOL 2 scales much better than FaCT++ with regard to increasing multiplicities. In the presence of fixpoints, COOL 2 still scales well and can handle multiplicities that should be sufficient for practical use. The formula series \(\lnot \textsf{ParityToBuechi}\) appears to show the limits of COOL 2 with the current implementation of graded one-step satisfiability checking. Nonetheless, our results indicate that COOL 2 is capable of automatically proving or refuting involved properties of (graded) \(\omega \)-automata and games in reasonable time.

5 Conclusion

We have described and evaluated the current version COOL 2 of the COalgebraic Ontology Logic reasoner (COOL). Future development will include the implementation of additional instance logics, such as the probabilistic and graded \(\mu \)-calculus with linear inequalities, as well as support for the full coalgebraic \(\mu \)-calculus via on-the-fly determinisation of unrestricted Büchi automata, using the Safra-Piterman construction.