Bounded Game-Theoretic Semantics for Modal Mu-Calculus and Some Variants

Lauri Hella Tampere University
Finland [email protected] University of Helsinki and Tampere University
FinlandENS Paris-Saclay
France Antti Kuusisto University of Helsinki and Tampere University
Finland [email protected] ENS Paris-Saclay
France Raine Rönnholm ENS Paris-Saclay
France [email protected]

Abstract

We introduce a new game-theoretic semantics (GTS) for the modal mu-calculus. Our so-called bounded GTS replaces parity games with alternative evaluation games where only finite paths arise; infinite paths are not needed even when the considered transition system is infinite. The novel games offer alternative approaches to various constructions in the framework of the mu-calculus. For example, they have already been successfully used as a basis for an approach leading to a natural formula size game for the logic. While our main focus is introducing the new GTS, we also consider some applications to demonstrate its uses. For example, we consider a natural model transformation procedure that reduces model checking games to checking a single, fixed formula in the constructed models, and we also use the GTS to identify new alternative variants of the mu-calculus with PTime model checking.

1 Introduction

The modal $\mu$ -calculus [18] is a well-known formalism that plays a central role in, e.g., program verification. The standard semantics of the $\mu$ -calculus is based on fixed points, but the system has also a well-known game theoretic semantics ( $\mathsf{GTS}$ ) that makes use of parity games. The related games generally involve infinite plays, and the parity condition is used for determining the winner (see, e.g., [6] for further details and a general introduction to the $\mu$ -calclus).

The agenda and contributions of this article.

In this article we present an alternative game-theoretic semantics for the modal $\mu$ -calculus. Our so-called bounded $\mathsf{GTS}$ is based on games that resemble the standard semantic games for the $\mu$ -calculus, but there is an extra feature that ensures that the plays within the novel framework always end after a finite number of rounds. Thereby only finite paths arise in related evaluation games even when investigating infinite transition systems. Thus there is no need to keep track of the parity condition, so in that sense the games we present in this article simplify the standard framework. Furthermore, they offer an alternative perspective on the $\mu$ -calculus, as we show that our semantics is equivalent to the standard one.

In the novel games, the evaluation of a fixed point formula begins by one of the players declaring an ordinal number; the verifying player declares ordinals for $\mu$ -formulae and the falsifying player for $\nu$ -formulae. The declared ordinal is then lowered as the game proceeds, and since ordinals are well-founded, the game will indeed end in finite time, i.e., after a finite number of game steps. In general, infinite ordinals are needed in the games, but finite ordinals suffice in finite models.

While the bounded $\mathsf{GTS}$ provides a new perspective on the standard modal $\mu$ -calculus, our approach also leads naturally to a range of alternative semantic systems that are not equivalent to the standard semantics. Indeed, we divide the framework of bounded semantics into subsystems dubbed $\Gamma$ -bounded semantics for different ordinals $\Gamma$ . Here $\Gamma$ provides a strict upper limit for the ordinals that can be used during the game play. For each $\Gamma$ -bounded semantics, we define also a compositional semantics and prove the game-theoretic and compositional versions equivalent.

If only finite ordinals are allowed, meaning $\Gamma=\omega$ , we obtain the finitely bounded $\mathsf{GTS}$ , which is an interesting system itself. While this semantics is equivalent to the standard case in finite models, the general expressive powers differ. Indeed, we will show that the $\mu$ -calculus under finitely bounded $\mathsf{GTS}$ does not have the finite model property. Furthermore, we observe that the set of validities of the $\mu$ -calculus under finitely bounded semantics is strictly contained in the set of standard validities.

We then introduce yet another class of variants of the bounded $\mathsf{GTS}$ consisting of the systems of $f$ -bounded semantics. In the $\Gamma$ -bounded semantics, each $\mu$ and $\nu$ -formula is associated with an ordinal of its own, while in the $f$ -bounded semantics this scheme is relaxed and only two ordinals are used, one for all $\mu$ -formulae and another one for all $\nu$ -formulae. The particular ordinals fixed in the beginning of the game depend on the particular variant of $f$ -bounded semantics. We prove PTime-completeness of the model checking problem of a range of simple yet expressive systems of $f$ -semantics. The result concerns both data and combined complexity. In addition to semantic studies, we use $\mathsf{GTS}$ to identify a canonical reduction of $\mu$ -calculus model checking instances to checking a single, uniform formula in the model obtained by the reduction.

Further motivation of the study.

While the formal results listed above are an important part of our study, the focus of our article is mainly on the conceptual development of the theory of the $\mu$ -calculus and related systems, not so much the more technical directions. While some of the technical results we obtain have straightforward and obvious implicit similarities to existing notions, such as finite approximants of fixed points, we believe the systematic, formal and conceptual study initiated in this article is justified.

Indeed, we believe the bounded $\mathsf{GTS}$ in general can be a fruitful framework for various further developments. The setting provides an alternative perspective to parity games, replacing infinite plays with games based on finitely many rounds only, thereby leading to a conceptually interesting territory to be explored further. The fragments with PTime-model checking we identify serve as an example of the various possibilities. Furthermore, it is worth noting here, e.g., that the difference between the standard and bounded $\mathsf{GTS}$ for the $\mu$ -calculus is analogous to the relationship between while-loops and for-loops; while-loops are iterated possibly infinitely long, whereas for-loops run for $k\in\mathbb{N}$ rounds, where $k$ can generally be an input to the loop. Finally, we argue that the new semantics can quite often make formulae easier to read; we will illustrate this in Examples 3.3 and 3.7.

Notes on related work.

There already exist several works where simple variants of the bounded semantics have been considered in the context of temporal logics with a significantly simpler recursion mechanisms than that of the $\mu$ -calculus. The papers [9], [12] consider a bounded semantics for the Alternating-time temporal logic $\mathsf{ATL}$ , and [11], [8] extend the related study to the extension $\mathsf{ATL}^{+}$ of $\mathsf{ATL}$ . See also [10], [13]. Part of the original motivation behind the studies in [9], [12], [11], [8] (as well as the current article) relates to work with the direct aim of understanding variants and fragments of the general, expressively Turing-complete logic presented in [20]. It is also worth mentioning that the work in the present article has already been made essential use of in constructing a canonical formula size game for the $\mu$ -calculus in [16]. The first short draft of the current submission appeared in 2017 as the arXiv manuscript [14]. It contained only the game-theoretic semantics presented below; the current article is the extended, full conference version of that short draft. The extended preprint of the current article is also available as the arXiv manuscript [15], containing full technical details.

There is a whole range of earlier but closely related logical studies that make use of notions with similar intuitions to the ones behind the bounded semantics of this paper. Indeed, for logics with time bounds, see, e.g., the paper [2] on finitary fairness and the article [19] relating to promptness in Linear temporal logic $\mathsf{LTL}$ . We also mention here the work related to bounded model checking, see, e.g., [5], [22] and [24]. The article [7] is one example of an early work that uses explicit ‘clocking’ of fixed point formulae in (a variant of) the $\mu$ -calculus, thereby involving some ideas that bear a similarity to some features used also in the present paper. However, the approach and goals of [7] are different, e.g., the paper limits to finite models only and does not discuss game-theoretic semantics at all.

2 Preliminaries

2.1 Syntax

Let $\operatorname{\Phi}$ be a set of proposition symbols and $\operatorname{\Lambda}$ a set of label symbols. Formulae of the modal $\mu$ -calculus are generated by the grammar

\displaystyle\varphi::=p\mid\neg p\mid X\mid\varphi\vee\varphi\mid\varphi\wedge\varphi\mid\Diamond\varphi\mid\Box\varphi\mid\mu X\varphi\mid\nu X\varphi,

where $p\in\operatorname{\Phi}$ and $X\in\operatorname{\Lambda}$ .

Let $\varphi$ be a formula of the $\mu$ -calculus. The set of nodes in the syntax tree of $\varphi$ is denoted by $\operatorname{Sf}(\varphi)$ . All of these nodes correspond to some subformula of $\varphi$ , but the same subformula may have several occurrences in the syntax tree of $\varphi$ , as for example in the case of $p\vee p$ . We always distinguish between different occurrences of the same subformula, and thus we always assume that the position in the syntax tree of $\varphi$ is known for any given subformula of $\varphi$ . We also use the following notation:

\operatorname{Sf}_{\_}{\mu\nu}(\varphi):=\{\theta\in\operatorname{Sf}(\varphi)\mid\theta=\mu X\psi\text{ or }\theta=\nu X\psi\text{ for some }\psi\in\operatorname{Sf}(\varphi)\text{ and }X\in\Lambda\}.

2.2 Standard Compositional Semantics

A Kripke model $\mathcal{M}$ is a tuple $(W,R,V)$ , where $W$ is a nonempty set, $R$ a binary relation over $W$ and $V:\Phi\rightarrow\mathcal{P}(W)$ a valuation for proposition symbols in $\operatorname{\Phi}$ . An assignment $s:\operatorname{\Lambda}\rightarrow\mathcal{P}(W)$ for $\mathcal{M}$ maps label symbols $X$ to subsets of $W$ .

Definition 2.1.

Let $\mathcal{M}=(W,R,V)$ be a Kripke model, $w\in W$ . Let $\varphi$ be a formula of the $\mu$ -calculus. Truth of $\varphi$ in $\mathcal{M}$ and $w$ under assignment $s$ , denoted by $\mathcal{M},w\vDash_{\_}s\varphi$ , is defined as in standard modal logic for $p$ , $\neg p$ , $\vee$ , $\wedge$ , $\Diamond$ , $\Box$ . The truth condition for label symbols is defined with respect to the assignment $s$ :

•

$\mathcal{M},w\vDash_{\_}sX$ iff $w\in s(X)$ .

To deal with $\mu$ and $\nu$ , we define an operator $\widehat{\varphi}_{\_}{X,s}:\mathcal{P}(W)\rightarrow\mathcal{P}(W)$ such that $\widehat{\varphi}_{\_}{X,s}(A)=\{w\in W\mid\mathcal{M},w\vDash_{\_}{s[A/X]}\varphi\}$ , where $s[A/X]$ is the assignment that sends $X$ to $A$ and treats other label symbols the same way as $s$ . The operators $\widehat{\varphi}_{\_}{X,s}$ are always monotone and thereby have least and greatest fixed points. The semantics for the operators $\mu X$ and $\nu X$ is as follows:

•

$\mathcal{M},w\vDash_{\_}s\mu X\psi$ iff $w$ is in the least fixed point of the operator $\widehat{\vphantom{\wedge}\smash{\psi}}_{\_}{X,s}$ .
•

$\mathcal{M},w\vDash_{\_}s\nu X\psi$ iff $w$ is in the greatest fixed point of the operator $\widehat{\vphantom{\wedge}\smash{\psi}}_{\_}{X,s}$ .

A label symbol $X$ is said to occur free in a formula $\varphi$ if it occurs in $\varphi$ but is not a subformula of any subformula of $\varphi$ of the form $\mu X\psi$ or $\nu X\psi$ . A formula $\varphi$ is called a sentence if it does not contain any free label symbols. Truth of a sentence $\varphi$ is independent of assignments $s$ , so we may simply write $\mathcal{M},w\vDash\varphi$ instead of $\mathcal{M},w\vDash_{\_}s\varphi$ .

2.3 Alternating Reachability Games

The alternating reachability game problem, which is well known to be PTime-complete (see, e.g., [17]), is defined as follows. The input to the problem is a finite pointed model $(\mathcal{M},w)$ , i.e., $\mathcal{M}$ is Kripke model and $w$ a state in it. We assume the vocabulary of $\mathcal{M}$ contains the proposition symbols $p_{\_}B$ and $q_{\_}B$ . The game is played by two players, $A$ and $B$ , starting from the state $w$ . In each round, one of the players moves (if possible) to some state that can be directly reached in one step from the current state via the accessibility relation; if $q_{\_}{B}$ holds in the current state, then $B$ moves, and otherwise $A$ moves. If the players reach a state where $p_{\_}{B}$ holds, then the game ends and $B$ wins. If a player cannot make the required move in some state (meaning the state is a dead end), then the game ends and that player loses and the other player wins. If the game does not end in a finite number of moves, then $A$ wins. The alternating reachability game problem yields the answer yes on the input $(\mathcal{M},w)$ iff $B$ has a winning strategy in the game. We let $\mathrm{AR}$ denote the class of all positive instances of the alternating reachability game problem. The following observation is well known.

Proposition 2.2.

Let $\mathcal{M}$ be a Kripke model with propositional vocabulary $\{p_{\_}\mathrm{B},q_{\_}B\}$ and let $w$ be a state in $\mathcal{M}$ . Then $(\mathcal{M},w)\in\mathrm{AR}$ if and only if $\mathcal{M},w\vDash\chi,$ where $\chi=\mu X\bigl{(}p_{\_}B\vee(q_{\_}B\wedge\Diamond X)\vee(\neg q_{\_}{B}\wedge\Box X)\bigr{)}.$

3 Bounded Game-Theoretic Semantics

The general idea of game-theoretic semantics ( $\mathsf{GTS}$ ) is that truth of a formula $\varphi$ is checked in a model $\mathcal{M}$ via playing a game where a proponent player (Eloise) attempts to show that $\varphi$ holds in $\mathcal{M}$ while an opponent player (Abelard) tries to establish the opposite—that $\varphi$ is false. In this section we define a bounded game-theoretic semantics for the $\mu$ -calculus, or bounded $\mathsf{GTS}$ . The semantics shares some features with a similar $\mathsf{GTS}$ for the Alternating-time temporal logic ( $\mathsf{ATL}$ ) defined in [9] (see also [11]).

3.1 Bounded Evaluation Games

Let $\varphi$ be a sentence of the $\mu$ -calculus and $X\in\operatorname{Sf}(\varphi)$ . The reference formula of $X$ , denoted $\operatorname{Rf}(X)$ , is the unique subformula of $\varphi$ that binds $X$ . That is, $\operatorname{Rf}(X)$ is of the form $\mu X\psi$ or $\nu X\psi$ and there is no other operator $\mu X$ or $\nu X$ in the syntax tree on the path from $\operatorname{Rf}(X)$ to $X$ . Since $\varphi$ is a sentence, every label symbol has a reference formula (and the reference formula is by definition unique for each label symbol).

Example 3.1.

Consider the sentence $\varphi^{*}:=\nu X\Box\mu Y\bigl{(}\Diamond Y\vee(p\wedge X)\bigr{)}$ . Here we have $\operatorname{Rf}(X)=\varphi^{*}$ and $\operatorname{Rf}(Y)=\mu Y(\Diamond Y\vee(p\wedge X))$ .

Definition 3.2.

Let $\mathcal{M}$ be a model, $w_{\_}0\in W$ , $\varphi_{\_}0$ a sentence and $\Gamma>0$ an ordinal. We define the $\Gamma$ -bounded evaluation game $\mathcal{G}=(\mathcal{M},w_{\_}0,\varphi_{\_}0,\Gamma)$ as follows. The game has two players, Abelard and Eloise. The positions of the game are of the form $(w,\varphi,c)$ , where $w\in W$ , $\varphi\in\operatorname{Sf}(\varphi_{\_}0)$ and

c:\operatorname{Sf}_{\_}{\mu\nu}(\varphi_{\_}0)\;\rightarrow\;\{\gamma\mid\gamma\leq\Gamma\}

is a clock mapping. We call the value $c(\theta)$ the clock value of $\theta$ (for $\theta\in\operatorname{Sf}_{\_}{\mu\nu}(\varphi_{\_}0)$ ).

The game begins from the initial position $(w_{\_}0,\varphi_{\_}0,c_{\_}0)$ , where $c_{\_}0(\theta)=\Gamma$ for every $\theta\in\operatorname{Sf}_{\_}{\mu\nu}(\varphi_{\_}0)$ . The game is then played according to the following rules:

•

In a position $(w,p,c)$ for some $p\in\operatorname{\Phi}$ , Eloise wins if $w\in V(p)$ . Otherwise Abelard wins.
•

In a position $(w,\neg p,c)$ for some $p\in\operatorname{\Phi}$ , Eloise wins if $w\notin V(p)$ . Otherwise Abelard wins.
•

In a position $(w,\psi\vee\theta,c)$ , Eloise selects whether the next position is $(w,\psi,c)$ or $(w,\theta,c)$ .
•

In a position $(w,\psi\wedge\theta,c)$ , Abelard selects whether the next position is $(w,\psi,c)$ or $(w,\theta,c)$ .
•

In a position $(w,\Diamond\psi,c)$ , Eloise selects some $v\in W$ such that $wRv$ and the next position is $(v,\psi,c)$ . If there is no such $v$ , then Abelard wins.
•

In a position $(w,\Box\psi,c)$ , Abelard selects some $v\in W$ such that $wRv$ and the next position is $(v,\psi,c)$ . If there is no such $v$ , then Eloise wins.
•

In a position $(w,\mu X\psi,c)$ , Eloise chooses an ordinal $\gamma<\Gamma$ . Then the game continues from the position $(w,\psi,c[\gamma/\mu X\psi])$ . Here $c[\gamma/\mu X\psi]$ is the clock mapping that sends $\mu X\psi$ to $\gamma$ and treats other formulae as $c$ .
•

In a position $(w,\nu X\psi,c)$ , Abelard chooses an ordinal $\gamma<\Gamma$ . Then the game continues from the position $(w,\psi,c[\gamma/\nu X\psi])$ .
•
Suppose that the game is in a position $(w,X,c)$ and let $c(\operatorname{Rf}(X))=\gamma$ .
1. 1.
  Suppose that $\operatorname{Rf}(X)=\mu X\psi$ for some $\psi$ .
  - –
    
    If $\gamma=0$ , then Abelard wins.
  - –
    
    Else, Eloise must select some $\gamma^{\prime}<\gamma$ , and then the game continues from the position $(w,\psi,c^{\prime})$ , where
    
    *
    
    $c^{\prime}(\mu X\psi)=\gamma^{\prime}$ ,
    
    *
    
    $c^{\prime}(\theta)=\Gamma$ for all $\theta\in\operatorname{Sf}_{\_}{\mu\nu}(\varphi_{\_}0)$ s.t. $\theta\in\operatorname{Sf}(\psi)$ ,
    
    *
    
    $c^{\prime}(\theta)=c(\theta)$ for all other $\theta\in\operatorname{Sf}_{\_}{\mu\nu}(\varphi_{\_}0)$ .
2. 2.
  Suppose that $\operatorname{Rf}(X)=\nu X\psi$ for some $\psi$ .
  - –
    
    If $\gamma=0$ , then Eloise wins.
  - –
    
    Else, Abelard must select some $\gamma^{\prime}<\gamma$ , and then the game continues from the position $(w,\psi,c^{\prime})$ , where
    
    *
    
    $c^{\prime}(\nu X\psi)=\gamma^{\prime}$ ,
    
    *
    
    $c^{\prime}(\theta)=\Gamma$ for all $\theta\in\operatorname{Sf}_{\_}{\mu\nu}(\varphi_{\_}0)$ s.t. $\theta\in\operatorname{Sf}(\psi)$ ,
    
    *
    
    $c^{\prime}(\theta)=c(\theta)$ for all other $\theta\in\operatorname{Sf}_{\_}{\mu\nu}(\varphi_{\_}0)$ .

The positions where one of the players wins the game are called ending positions. The execution of the rules related to a position of the game constitutes one round of the game. The number of rounds in a play of the game is called the length of the play. We call the ordinals $\gamma<\Gamma$ clock values and the ordinal $\Gamma$ the clock value bound. (We note that only rounds with formulae of type $\mu X\psi$ , $\nu X\psi$ and $X$ affect clock values.)

We observe that in evaluation games we do not need assignments $s$ . A label symbol in $X\in\Lambda$ is simply a marker that points to a node (that node being the formula $\operatorname{Rf}(X)$ ) in the syntax tree of the sentence $\varphi_{\_}0$ . Hence label symbols are conceptually quite different in $\mathsf{GTS}$ and compositional semantics. Indeed, the operators $\mu X$ (respectively $\nu X$ ) can be given a natural reading relating to self-reference. In the formula $\mu X\psi$ , the operator $\mu X$ is naming the formula $\psi$ with the name $X$ . The atoms $X$ inside $\psi$ are, in turn, claiming that $\psi$ holds, i.e., referring back to the formula $\psi$ . The difference between $\mu$ and $\nu$ is that $\mu X\psi$ relates to verifying the formula $\psi$ while $\nu X\psi$ is associated with preventing the falsification of $\psi$ , i.e., defending $\psi$ . Therefore, if $N(\psi)$ denotes a natural language reading of $\psi$ , then the natural language reading of $\mu X\psi$ states that “we can verify the claim named $X$ which asserts that $N(\psi)$ ”. An analogous reading can be given to $\nu X\psi$ . This scheme of reading recursive formulae via self-reference is from [20], [21].

Example 3.3.

Consider the Kripke model $\mathcal{M}^{*}=(W,R,V)$ , where we have $W=\{w_{\_}i\mid i\in\mathbb{N}\}$ , $R=\{(w_{\_}0,w_{\_}i)\mid i\geq 1\}\cup\{(w_{\_}{i+1},w_{\_}i)\mid i\geq 0\}$ and $V(p)=\{w_{\_}0\}$ .

Recall the sentence $\varphi^{*}=\nu X\Box\mu Y(\Diamond Y\vee(p\wedge X))$ from Example 3.1 and consider the evaluation game $\mathcal{G}^{*}=(\mathcal{M}^{*},w_{\_}0,\varphi^{*},\omega)$ . In $\mathcal{G}^{*}$ , Abelard first announces a clock value $n<\omega$ for $\operatorname{Rf}(X)$ and then makes a jump from the intial state $w_{\_}0$ (with a $\Box$ -move). Next Eloise announces some clock value $m<\omega$ for $\operatorname{Rf}(Y)$ . Then she can, by repeated $\vee$ -moves, jump in the model (making a $\Diamond$ -move) and loop back to the formula $\operatorname{Rf}(Y)$ ; each time she loops back, she needs to lower the value of $m$ . If Eloise at some point chooses the right disjunct, Abelard can either check if $p$ true in the current state or loop back to $\operatorname{Rf}(X)$ . In the latter case, the value of $n$ is lowered, but the value of $m$ is reset back to $\omega$ (allowing Eloise to choose a fresh value $m$ next time).

The game eventually ends when (1) the clock value of $\operatorname{Rf}(X)$ goes to zero, whence Abelard loses; when (2) the clock value of $\operatorname{Rf}(Y)$ goes to zero, whence Eloise loses; or when (3) Abelard chooses the left conjunct, whence Eloise wins if and only if $p$ is true at the current state. We will return to this game in Example 3.7.

Proposition 3.4.

Let $\mathcal{G}=(\mathcal{M},w,\varphi,\Gamma)$ be a bounded evaluation game. Every play of $\mathcal{G}$ ends in a finite number of rounds.

Proof.

For each positive integer $k$ , let $\prec_{\_}k$ denote the “canonical lexicographic order” of $k$ -tuples of ordinals. That is, $(\gamma_{\_}1,\dots,\gamma_{\_}k)\prec_{\_}k(\gamma_{\_}1^{\prime},\dots,\gamma_{\_}k^{\prime})$ if and only if there exists some $i\leq k$ such that $\gamma_{\_}i<\gamma_{\_}i^{\prime}$ and $\gamma_{\_}j=\gamma_{\_}j^{\prime}$ for all $j<i$ .

Consider a branch in the syntax tree of $\varphi$ . Let $\psi_{\_}1,\dots,\psi_{\_}k\in\operatorname{Sf}_{\_}{\mu\nu}(\varphi)$ be the $\mu\nu$ -formulae occurring on this branch in this order (starting from the root). In each round of the game, each such sequence $(\psi_{\_}1,\dots,\psi_{\_}k)$ is associated with the $k$ -tuple $(c(\psi_{\_}1),\dots,c(\psi_{\_}k))$ of clock values (that are ordinals less or equal to $\Gamma$ ). It is easy to see that if $c$ and $c^{\prime}$ are clock mappings such that $c^{\prime}$ occurs later than $c$ in the game, then we have $(c^{\prime}(\psi_{\_}1),\dots,c^{\prime}(\psi_{\_}k))\preceq_{\_}k(c(\psi_{\_}1),\dots,c(\psi_{\_}k))$ . Also, every time a transition from some label $X$ to the reference formula $\operatorname{Rf}(X)$ is made, there is at least one branch where the $k$ -tuple (for the relevant $k$ ) of clock values becomes strictly lowered (in relation to $\prec_{\_}k$ ). As ordinals are well-founded, it is thus clear that the game must end after finitely many rounds. ∎

Each evaluation game $\mathcal{G}$ can naturally be associated with a game tree $T(\mathcal{G})=(P_{\_}\mathcal{G},E_{\_}\mathcal{G})$ , where $P_{\_}\mathcal{G}$ is the set of positions $(v,\psi,c)$ of $\mathcal{G}$ and $E_{\_}\mathcal{G}$ is the successor position relation. $T(\mathcal{G})$ is formed by beginning from the initial position and adding transitions to all possible successor positions. This procedure is then repeated from the successor positions until an ending position is reached. In the game tree, the initial position is of course the root and ending positions are leafs. Complete branches correspond to possible plays of the game. Due to Proposition 3.4, the game tree of any bounded evaluation game is well-founded, i.e., it does not contain infinite branches. However, if the clock value bound $\Gamma$ or the model $\mathcal{M}$ is infinite, then the out-degree of some of the nodes of the game tree can be infinite.

3.2 Game-Theoretic Semantics

Definition 3.5.

Let $\mathcal{G}=(\mathcal{M},w_{\_}0,\varphi_{\_}0,\Gamma)$ be an evaluation game. A strategy $\sigma$ for Eloise in $\mathcal{G}$ is a partial mapping on the set of those positions $(w,\varphi,c)$ of the game where Eloise needs to make a move such that: $\sigma(w,\psi\vee\theta,c)\in\{\psi,\theta\}$ , $\sigma(w,\Diamond\psi,c)\in\{v\in W\mid wRv\}$ , $\sigma(w,\mu X\psi,c)\in\{\gamma\mid\gamma<\Gamma\}$ , and $\sigma(w,X,c)\in\{\gamma\mid\gamma<c(\operatorname{Rf}(X))\}$ where $\operatorname{Rf}(X)$ is of the form $\mu X\psi$ . We say that Eloise plays according to $\sigma$ if she makes all her choices according to $\sigma$ and that $\sigma$ is a winning strategy if Eloise always wins when playing according to $\sigma$ .

Definition 3.6.

Let $\mathcal{M}=(W,R,V)$ be a model, $w\in W$ , $\varphi$ a sentence and $\Gamma>0$ an ordinal. We define truth of $\varphi$ in $\mathcal{M}$ and $w$ according to $\Gamma$ -bounded game theoretic semantics, $\mathcal{M},w\Vdash^{\Gamma}\!\varphi$ , as follows:

\mathcal{M},w\Vdash^{\Gamma}\!\varphi\text{\; iff \; Eloise has a winning strategy in }(\mathcal{M},w,\varphi,\Gamma).

Example 3.7.

Recall the game $\mathcal{G}^{*}$ from Example 3.3. We define a strategy for Eloise as follows. After Abelard has made a transition to some state $w_{\_}j$ , Eloise chooses $j$ for the clock value of $\operatorname{Rf}(Y)$ and jumps in the model until reaching again $w_{\_}0$ . She then chooses the right disjunct at $w_{\_}0$ , whence she either wins (since $w_{\_}0\in V(p)$ ) or Abelard needs to lower the clock value of $\operatorname{Rf}(X)$ and the clock value of $\operatorname{Rf}(Y)$ gets reset back to $\omega$ . Clearly this is a winning strategy for Eloise and thus $\mathcal{M}^{*},w_{\_}0\Vdash^{\omega}\!\varphi^{*}$ .

From the structure of the evaluation games for $\varphi^{*}$ we find an interpretation for the meaning of $\varphi^{*}$ : “we can infinitely repeat the process where first (1) an arbitrary transition is made, and then (2) we can reach a state where $p$ is true and the process can be continued from (1)”. Hence the clock value chosen for $\operatorname{Rf}(Y)$ is intuitively a “commitment” on how many rounds at most it will take to reach a state where $p$ holds. The clock value for $\operatorname{Rf}(X)$ , on the other hand, is a “challenge” on how many times $p$ must be reached. Indeed, in models where $p$ can be reached only finitely many—say $n$ —times from the initial state, Abelard can win by choosing $n+1$ as the initial clock value for $\operatorname{Rf}(X)$ .

4 Bounded Compositional Semantics

In this section we define a compositinal semantics based on ordinal approximants of fixed point operators. Let $\mathcal{M}=(W,R,V)$ be a Kripke model, $F:\mathcal{P}(W)\rightarrow\mathcal{P}(W)$ an operator and $\gamma$ an ordinal. We define the sets $F_{\_}\mu^{\gamma}$ and $F_{\_}\nu^{\gamma}$ recursively as follows:

$\displaystyle F_{\_}\mu^{0}:=\emptyset$	and	$\displaystyle F_{\_}\nu^{0}:=W.$
$\displaystyle F_{\_}\mu^{\gamma}:=F\bigl{(}F_{\_}\mu^{\gamma-1}\bigr{)}$	and	$\displaystyle F_{\_}\nu^{\gamma}:=F\bigl{(}F_{\_}\nu^{\gamma-1}\bigr{)},\;\text{ if $\gamma$ is a successor ordinal}.$
$\displaystyle F_{\_}\mu^{\gamma}:=\bigcup_{\_}{\delta<\gamma}F_{\_}\mu^{\delta}$	and	$\displaystyle F_{\_}\nu^{\gamma}:=\bigcap_{\_}{\delta<\gamma}F_{\_}\nu^{\delta},\;\quad\text{ if $\gamma$ is a limit ordinal}.$

Definition 4.1.

Consider a model $\mathcal{M}$ with a state $w$ and a related assignment $s$ . We obtain $\Gamma$ -bounded compositional semantics for the modal $\mu$ -calculus by defining truth of $p$ , $\neg p$ , $\vee$ , $\wedge$ , $\Diamond$ , $\Box$ and $X$ recursively as in the standard compositional semantics and treating the $\mu$ and $\nu$ -operators as follows:

•

$\mathcal{M},w\vDash^{\Gamma}_{\_}s\mu X\psi$ iff $w\in(\widehat{\vphantom{\wedge}\smash{\psi}}_{\_}{X,s,\Gamma})_{\_}\mu^{\Gamma}$ ,
•

$\mathcal{M},w\vDash^{\Gamma}_{\_}s\nu X\psi$ iff $w\in(\widehat{\vphantom{\wedge}\smash{\psi}}_{\_}{X,s,\Gamma})_{\_}\nu^{\Gamma}$ ,

where the operator $\widehat{\varphi}_{\_}{X,s,\Gamma}:\mathcal{P}(W)\rightarrow\mathcal{P}(W)$ is defined such that

\displaystyle\widehat{\varphi}_{\_}{X,s,\Gamma}(A)=\{w\in W\mid\mathcal{M},w\vDash^{\Gamma}_{\_}{s[A/X]}\varphi\}.

The semantics of the $\mu$ and $\nu$ -operators can be equivalently given as follows:

•

$\mathcal{M},w\vDash^{\Gamma}_{\_}s\mu X\psi$ iff there exists some $\gamma<\Gamma$ s.t. $w\in(\widehat{\vphantom{\wedge}\smash{\psi}}_{\_}{X,s,\Gamma})_{\_}\mu^{\gamma+1}$ .
•

$\mathcal{M},w\vDash^{\Gamma}_{\_}s\nu X\psi$ iff $w\in(\widehat{\vphantom{\wedge}\smash{\psi}}_{\_}{X,s,\Gamma})_{\_}\nu^{\gamma+1}$ for every $\gamma<\Gamma$ .

If $\Gamma$ is a limit ordinal, we can replace the superscripts $\gamma+1$ above by $\gamma$ .

We say that a formula is in normal form if each label symbol in $\Lambda$ occurs in the formula at most once in the $\mu$ - $\nu$ -operators (but may occur several times on the atomic level). We let $\varphi^{\prime}$ denote a normal form variant of $\varphi$ obtained simply by renaming label symbols where appropriate. It is easy to show that $\varphi$ is equivalent to $\varphi^{\prime}$ with respect to both $\Gamma$ -bounded compositional semantics ( $\vDash^{\Gamma}$ ) and $\Gamma$ -bounded $\mathsf{GTS}$ ( $\Vdash^{\Gamma}$ ). Therefore, when proving the equivalence of these two semantics, it suffices that we consider sentences that are in normal form. Indeed, henceforth we assume that all formulae are in this normal form.

Theorem 4.2.

Let $\Gamma$ be an ordinal, $\mathcal{M}$ a Kripke model, $w_{\_}0\in W$ and $\varphi_{\_}0$ a sentence of the modal $\mu$ -calculus. Now we have

\mathcal{M},w_{\_}0\vDash^{\Gamma}\!\varphi_{\_}0\;\text{ iff }\;\mathcal{M},w_{\_}0\Vdash^{\Gamma}\!\varphi_{\_}0.

Proof.

(Sketch.) We present here a proof sketch highlighting the main ideas. For a rigorous, fully detailed proof, please see the appendix of the full arXiv preprint version [15] of the current submission.

The key in both directions of the proof is the following condition $(\star)$ which is a property satisfied/unsatisfied by positions $(w,\varphi,c)$ in the evaluation game $\mathcal{G}=(\mathcal{M},w_{\_}0,\varphi_{\_}0,\Gamma)$ :

( $\star$ )
There is an assignment $s$ such that $\mathcal{M},w\vDash_{\_}s^{\Gamma}\varphi$ , and for each $X\in\operatorname{Sf}(\varphi_{\_}0)$ :
1. 1.
  
  $s(X)=(\widehat{\vphantom{\wedge}\smash{\psi}}_{\_}{X,s,\Gamma})_{\_}\mu^{\gamma}$ if $\operatorname{Rf}(X)=\mu X\psi$ and $c(\operatorname{Rf}(X))=\gamma$ ,
2. 2.
  
  $s(X)=(\widehat{\vphantom{\wedge}\smash{\psi}}_{\_}{X,s,\Gamma})_{\_}\nu^{\gamma}$ if $\operatorname{Rf}(X)=\nu X\psi$ and $c(\operatorname{Rf}(X))=\gamma$ .

Note that this condition essentially relates the clock values $\gamma$ of bounded $\mathsf{GTS}$ to $\gamma$ -approximants in the bounded compositional semantics.

Proving the left to right implication, we first note that $(\star)$ holds in the initial position of $\mathcal{G}$ by the assumption $\mathcal{M},w_{\_}0\vDash^{\Gamma}\!\varphi_{\_}0$ . Then we show that whenever $(\star)$ holds for the current position, Eloise either wins the game in the current position or she can maintain $(\star)$ to the next position. By maintaining $(\star)$ , we obtain a winning strategy since $\mathcal{G}$ ends in a finite number of rounds.

For the other direction of the equivalence, we suppose that Eloise has a winning strategy $\sigma$ in $\mathcal{G}$ . Since the game tree of $\mathcal{G}$ is well-founded, we can use well-founded (backwards) induction on the positions in the tree to prove that: if a position $(w,\varphi,c)$ can be reached with $\sigma$ , then ( $\star$ ) holds for $(w,\varphi,c)$ . Hence, in particular, $(\star)$ holds in the initial position of $\mathcal{G}$ and thus $\mathcal{M},w_{\_}0\vDash^{\Gamma}\!\varphi_{\_}0$ . ∎

Let $\mathcal{M}$ be a model. It is well-known that over $\mathcal{M}$ , each operator related to a formula of the $\mu$ -calculus reaches a fixed point in at most $(\mathsf{card}(\mathcal{M}))^{+}$ iterations, where $(\mathsf{card}(\mathcal{M}))^{+}$ is the successor cardinal of $\mathsf{card}(\mathcal{M})$ . Thus it is easy to see that the standard compositional semantics and $(\mathsf{card}(\mathcal{M}))^{+}$ -bounded compositional semantics are equivalent in $\mathcal{M}$ . Hence we obtain the following corollary:

Corollary 4.3.

$\Gamma$ -bounded $\mathsf{GTS}$ is equivalent with the standard compositional semantics of the modal $\mu$ -calculus when $\Gamma\geq(\mathsf{card}(\mathcal{M}))^{+}$ .

Also note that, in the special case of finite models, it suffices to use finite clock values that are at most the cardinality of the model.

5 Finitely Bounded Semantics

As stated in Corollary 4.3, the bounded semantics becomes equivalent with the standard (unbounded) semantics if we set a sufficiently large clock value bound $\Gamma$ . However, using smaller values of $\Gamma$ , we obtain different semantic systems typically nonequivalent to the standard semantics. We can either set some fixed bound for $\Gamma$ or use a value that is determined by some parameters—such as the size of the given model and the given formula. In this section we consider the former case; systems relating to the latter case are examined in Section 6.

A particularly interesting case with a fixed value of $\Gamma$ is the so-called finitely bounded semantics, where we set $\Gamma=\omega$ for all evaluation games. In the corresponding $\mathsf{GTS}$ , the players can only announce finite clock values.¹¹1Note that the correspondence to for-loops is particularly natural with finitely bounded semantics: iterations can be done up to any finite bound that has to be declared in advance. Finitely bounded semantics will be denoted by $\mathsf{FBS}$ which refers to both game-theoretic and compositional semantics with $\Gamma=\omega$ . In finite models $\mathsf{FBS}$ is equivalent to the standard semantics, but this equivalence breaks over infinite models; see Example 5.1 below.

In the example and proofs that follow, we will consider the sentence

\varphi_{\_}{\mathrm{AF}p}:=\mu X(p\vee\Box X)

which intuitively means that on every path, $p$ can be reached eventually. Note that $\varphi_{\_}{\mathrm{AF}p}$ corresponds to the sentence $\mathrm{AF}p$ of Computation tree logic $\mathsf{CTL}$ .

Example 5.1.

Recall the model $\mathcal{M}^{*}$ from Example 3.3. Let $\mathcal{M}^{\dagger}$ be the model that is otherwise identical to $\mathcal{M}^{*}$ , but $V(p)=\{w_{\_}1\}$ . Since the state $w_{\_}1$ is eventually reached on every path starting from $w_{\_}0$ , it is easy to see that $\mathcal{M}^{\dagger},w_{\_}0\models\varphi_{\_}{\mathrm{AF}p}$ . However, $\mathcal{M}^{\dagger},w_{\_}0\not\models^{\omega}\varphi_{\_}{\mathrm{AF}p}$ since from $w_{\_}0$ there is no finite upper bound on how many transitions are needed to reach $w_{\_}1$ . Indeed, Abelard has a winning strategy in $(\mathcal{M}^{\dagger},w_{\_}0,\varphi_{\_}{\mathrm{AF}p},\omega)$ since he can win by choosing a transition to $w_{\_}{j+1}$ for any clock value $j<\omega$ for $\operatorname{Rf}(X)$ —chosen by Eloise.

It is worth noting that $\mathcal{M}^{\dagger},w_{\_}0\models^{\omega+1}\varphi_{\_}{\mathrm{AF}p}$ since if Eloise can choose $\omega$ as the initial clock value for $\operatorname{Rf}(X)$ and then lower it to $j-1$ after Abelard has made a transition to a state $w_{\_}j$ . Moreover, we also have $\mathcal{M}^{\dagger},w_{\_}0\models^{\omega}\Box\varphi_{\_}{\mathrm{AF}p}$ since Eloise will know how many transitions it takes to reach $w_{\_}1$ as Abelard has to make the first transition before Eloise must announce a clock value.

In the proofs that follow, we will use negations and implications of formulae of the modal $\mu$ -calculus. Such formulae are in general not included in our official syntax (in the current paper), but it is straightforward to show that they can be translated to equivalent formulae in negation normal form.

It is well known that, with standard semantics, the modal $\mu$ -calculus has the finite model property, i.e., every satisfiable sentence is satisfied in some finite model (see, e.g., [6]). However, with finitely bounded semantics, this property is lost.

Proposition 5.2.

The modal $\mu$ -calculus with $\mathsf{FBS}$ does not have the finite model property.

Proof.

It is easy to see that $\Box\varphi_{\_}{\mathrm{AF}p}\rightarrow\varphi_{\_}{\mathrm{AF}p}$ is valid with the standard semantics (this follows from the “fixpoint property” $\mathrm{AF}p\leftrightarrow p\vee\mathrm{AXAF}p$ of $\mathsf{CTL}$ ). Therefore $\Box\varphi_{\_}{\mathrm{AF}p}\wedge\neg\varphi_{\_}{\mathrm{AF}p}$ is not satisfiable with the standard semantics. As the standard semantics is equivalent to $\mathsf{FBS}$ in finite models, $\Box\varphi_{\_}{\mathrm{AF}p}\wedge\neg\varphi_{\_}{\mathrm{AF}p}$ cannot be satisfied under $\mathsf{FBS}$ in any finite model. However, $\Box\varphi_{\_}{\mathrm{AF}p}\wedge\neg\varphi_{\_}{\mathrm{AF}p}$ is satisfiable with $\mathsf{FBS}$ in an infinite model—as demonstrated by the model $\mathcal{M}^{\dagger}$ in Example 5.1. ∎

Moreover, $\mathsf{FBS}$ has the following interesting connection to the standard semantics.

Proposition 5.3.

The set of validities of the modal $\mu$ -calculus with $\mathsf{FBS}$ is strictly included in the set of validities with the standard semantics.

Proof.

To prove the inclusion, let $\varphi$ be a sentence valid under $\mathsf{FBS}$ . Then $\neg\varphi$ cannot be satisfied under $\mathsf{FBS}$ in any finite model. Since the standard semantics and $\mathsf{FBS}$ are equivalent in finite models, it follows that $\neg\varphi$ is not satisfied by the standard semantics in any finite model. Due to the finite model property of the standard semantics, $\neg\varphi$ is not satisfied by any model and thus $\varphi$ is valid. The inclusion is strict as $\Box\varphi_{\_}{\mathrm{AF}p}\rightarrow\varphi_{\_}{\mathrm{AF}p}$ is valid under standard semantics but not under $\mathsf{FBS}$ (cf. proof of Proposition 5.2). ∎

We showed in [10], [13] that the claims of Propositions 5.2, 5.3 hold also for the $\mathsf{FBS}$ defined for $\mathsf{CTL}$ and $\mathsf{ATL}$ . There we also developed a tableau method for showing that the validity problem of $\mathsf{CTL}$ and $\mathsf{ATL}$ with $\mathsf{FBS}$ is decidable and has the same complexity (ExpTime) as with the standard semantics. It remains to be investigated whether the analogous ExpTime result holds also for the $\mu$ -calculus with $\mathsf{FBS}$ .

6 Variants with PTime Model Checking

The bounded $\mathsf{GTS}$ leads naturally to semantic variants of the $\mu$ -calculus that can quite directly be shown to have PTime complete model checking. The main point is to make use of the intimate relationship between alternating Turing machines and semantic games. The novel systems of semantics we consider resemble the $\Gamma$ -bounded semantics but utilize a simplified way to control how many times $\mu$ and $\nu$ -formulae can be repeated in semantic games.

To present the alternative semantic systems in detail, let $f$ be a map that takes as input a model $\mathcal{M}$ , a point $w$ in the domain $W$ of $\mathcal{M}$ and a sentence $\varphi$ , outputting an ordinal. We assume that if $g$ is an isomorphism from $\mathcal{M}$ to $\mathcal{M}^{\prime}$ , then $f(\mathcal{M},w,\varphi)=f(\mathcal{M}^{\prime},g(w),\varphi)$ .²²2We note that $f$ is too large to be a set, but this is unproblematic to our study. The function $f$ gives rise to the simple $f$ -bounded $\mathsf{GTS}$ defined as follows.

Definition 6.1.

Let $\mathcal{M}$ be a Kripke-model, $w\in W$ and $\varphi$ a sentence of the $\mu$ -calculus. The simple $f$ -bounded evaluation game $\mathcal{G}_{\_}f=(\mathcal{M},w,\varphi)$ is played the same way as the $\Gamma$ -bounded evaluation game $\mathcal{G}_{\_}{\Gamma}=(\mathcal{M},w,\varphi,\Gamma)$ , but with the following differences on the way the number of remaining rounds is determined:

•

Eloise is controlling an ordinal $\gamma_{\_}{\exists}$ and Abelard an ordinal $\gamma_{\_}{\forall}$ . In the beginning of the game, these ordinals are set to be equal to $f(\mathcal{M},w,\varphi)$ .
•

Every time a transition is made from some label symbol $X$ to the reference formula $\mu X\psi$ , Eloise must lower the current value of $\gamma_{\_}{\exists}$ . Similarly, when a transition is made from $Y$ to the reference formula $\nu Y\psi^{\prime}$ , then Abelard must lower $\gamma_{\_}{\forall}$ . (Note that the values of $\gamma_{\_}{\exists}$ and $\gamma_{\_}{\forall}$ are never increased.)

If $\gamma_{\_}{\exists}=0$ and we enter a position where Eloise should lower $\gamma_{\_}{\exists}$ , then Eloise loses the game, and similarly, if $\gamma_{\_}{\forall}=0$ and we enter a position where Abelard should lower $\gamma_{\_}{\forall}$ , Abelard loses. In positions $(\mathcal{M},w^{\prime},p)$ and $(\mathcal{M},w^{\prime},\neg p)$ where $p$ is a proposition symbol, winning and losing is defined in the same way as in $\Gamma$ -bounded games. We define truth of $\varphi$ in $\mathcal{M}$ at $w$ according to the simple $f$ -bounded semantics such that $\mathcal{M},w\Vdash^{f}\varphi$ iff Eloise has a winning strategy in the game $\mathcal{G}_{\_}f=(\mathcal{M},w,\varphi)$ of the simple $f$ -bounded semantics.

Henceforth we mostly talk about $f$ -bounded semantics instead of simple $f$ -bounded semantics to keep the presentation simpler.

The naturalness and the general properties of $f$ -bounded semantics of course depend heavily on the choice of $f$ . One of the simpler choices is to define $f\bigl{(}\mathcal{M},w,\varphi\bigr{)}=\mathsf{card}(\mathcal{M})\cdot|\varphi|$ where $|\varphi|$ is the length of $\varphi$ , i.e., the number of symbol occurrences.³³3Each proposition symbol $p$ and label $X$ counts as one symbol despite the possible subindices: for example, $p_{\_}{1}$ is one symbol, not two symbols. This semantics has the natural property that in finite models, if the players always lower their ordinal by the minimum amount $1$ , then, if the game ends due to $\gamma_{\_}{\exists}$ or $\gamma_{\_}{\forall}$ being zero, some state-subformula pair must have been repeated. Furthermore, we can now prove the following result.

Proposition 6.2.

The $\mu$ -calculus model checking problem is PTime-complete under simple $f$ -bounded semantics with $f(\mathcal{M},w,\varphi)=\mathsf{card}(\mathcal{M})\cdot|\varphi|$ .

Proof.

To establish the upper bound, we define a Turing machine running in alternating logarithmic space that directly simulates the model checking game (i.e., the semantic evaluation game) with any input $\mathcal{M},w,\varphi$ . The game positions where Eloise makes a move correspond to existential machine states while Abelard’s positions correspond to universal states. We need some kind of a pointer indicating the current world of the Kripke structure and another pointer for the current subformula (i.e., node in the syntax tree). Furthermore, we keep binary representations of $\gamma_{\_}{\exists}$ and $\gamma_{\_}{\forall}$ in the memory. These binary strings are necessarily logarithmic in the input due to the choice of $f$ . Thus it is easy to see how the required alternating Turing machine is constructed.

We obtain the lower bound via the alternating reachability game. Recall Proposition 2.2 and the formula $\chi$ there. We will show that, as in standard semantics, $\chi$ defines the winning set of the alternating reachability game also under our $f$ -bounded semantics, i.e., $\chi$ is true in $\mathcal{M}$ at $w$ under our semantics if and only if the player $B$ has a winning strategy in the corresponding alternating reachability game. Indeed, it is easy to show that when $B$ has a winning strategy in an alternating reachability game, she can ensure a win so that no state of the game is visited more than once. Thus our choice of $f$ for the $f$ -bounded semantics guarantees that Eloise has a winning strategy in the corresponding the semantic game. And if Eloise has a winning strategy in a semantic game $\mathcal{G}_{\_}f(\mathcal{M},w,\chi)$ , then clearly $B$ wins the corresponding alternating reachability game. Thus, already with the fixed input formula $\chi$ , model checking is PTime-hard. ∎

It is worth noting here that in fact all the systems with $f(\mathcal{M},w,\varphi)=\mathsf{card}(\mathcal{M})^{k}\cdot|\varphi|$ (for different positive integers $k$ ) have PTime-complete model checking: the proof of Proposition 6.2 goes through with trivial modifications.

The $f$ -bounded semantics with $f(\mathcal{M},w,\varphi)=\mathsf{card}(\mathcal{M})\cdot|\varphi|$ is obviously very different in spirit from the standard semantics, and the $f$ -bounded semantics itself changes as we modify $f$ . Also, several further variants of the semantics immediately suggest themselves, for example the possibility of setting different limits for Eloise and Abelard, including the possibility of no limit at all. Also, letting different occurrences of $\mu$ and $\nu$ -formulae be associated with different clocks similarly to the standard semantics, but without resetting the clocks, is one of many possible interesting scenarios.

Concerning the case where we do not set clocks at all but allow the players to play indefinitely long, winning occurs only when an atomic position with a literal (e.g., $p$ or $\neg p$ ) is reached. Thus the games are not determined, i.e., it is possible that neither player has a winning strategy (consider, e.g., the formula $\mu XX$ ). This free semantics for modal logic results in a system that is essentially directly a fragment of the general, Turing-complete logic $\mathcal{L}$ of [20]. On the other hand, the different “clocking scenarios” described above (and further variants thereof) can be naturally imposed on $\mathcal{L}$ , and it would indeed make sense to study related phenomena in that framework.

7 Reducing Model Checking to Alternating Reachability

In this section we study model checking of the $\mu$ -calculus for fixed sentences.⁴⁴4The complexities of the related problems are commonly referred to as data complexity as opposed to the combined complexity of the standard problem where the sentence is not fixed. We investigate model checking separately with respect to the standard semantics and with respect to $\Gamma$ -bounded semantics. Given a sentence $\varphi$ of the $\mu$ -calculus, we use the following notation for the corresponding model checking and bounded model checking problems:

•

$\mathrm{MC}(\varphi):=\{(\mathcal{M},w)\mid\mathcal{M}\text{ is finite and }\mathcal{M},w\vDash\varphi\}$ , and
•

$\mathrm{BMC}(\varphi):=\{(\mathcal{M},w,\Gamma)\mid\mathcal{M}\text{ is finite and }\mathcal{M},w\vDash^{\Gamma}\varphi\}$ .

Recalling the relevant notations from Section 2.3, including the formula $\chi$ , we note, in particular, that the alternating reachability problem $\mathrm{AR}$ is equal to $\mathrm{MC}(\chi)$ . Our aim is to show that $\mathrm{AR}$ is a complete problem for model checking and bounded model checking:

Proposition 7.1.

For each formula $\varphi$ of the modal $\mu$ -calculus there are LogSpace-computable model transformations $J_{\_}\varphi$ and $I_{\_}\varphi$ such that for any finite Kripke model $\mathcal{M}$ , state $w$ and ordinal $\Gamma$ we have

(1)

$(\mathcal{M},w,\Gamma)\in\mathrm{BMC}(\varphi)\;\text{ iff }\;J_{\_}\varphi(\mathcal{M},w,\Gamma)\in\mathrm{AR}$ , and
(2)

$(\mathcal{M},w)\in\mathrm{MC}(\varphi)\;\text{ iff }\;I_{\_}\varphi(\mathcal{M},w)\in\mathrm{AR}$ .

Furthermore, neither $J_{\_}\varphi(\mathcal{M},w,\Gamma)$ nor $I_{\_}\varphi(\mathcal{M},w)$ contain infinite paths.

Proof.

Recall that the game tree of an evaluation game $\mathcal{G}=(\mathcal{M},w_{\_}0,\varphi,\Gamma)$ is the tree $T(\mathcal{G})=(P_{\_}\mathcal{G},E_{\_}\mathcal{G})$ , where $P_{\_}\mathcal{G}$ is the set of positions $(v,\psi,c)$ of $\mathcal{G}$ , and $E_{\_}\mathcal{G}$ is the successor position relation. We consider the following Kripke model that is obtained from $T(\mathcal{G})$ by adding proposition symbols encoding winning end positions of Eloise and positions in which it is Eloise’s turn to move: $\mathcal{T}_{\_}\mathcal{G}=(P_{\_}\mathcal{G},E_{\_}\mathcal{G},V_{\_}\mathcal{G})$ , where $V_{\_}\mathcal{G}:\{p_{\_}B,q_{\_}B\}\to\mathcal{P}(P_{\_}\mathcal{G})$ is the valuation

•

$V_{\_}\mathcal{G}(p_{\_}B)=\{(v,\psi,c)\in P_{\_}\mathcal{G}\mid\psi\text{ is a literal and }\mathcal{M},v\vDash\psi\}$ ,
•

$V_{\_}\mathcal{G}(q_{\_}B)=\{(v,\psi,c)\in P_{\_}\mathcal{G}\mid\psi\text{ is of the form }\theta\lor\eta,\,\Diamond\theta,\,\mu X\theta,\text{ or $X$ with}$ $\operatorname{Rf}(\psi)=\mu X\theta,$
a $\;\text{ or $\psi$ is a literal and }\mathcal{M},v\nvDash\psi\}$ .

Let $r_{\_}\mathcal{G}=(w_{\_}0,\varphi,c_{\_}0)$ be the initial position of $\mathcal{G}$ . Observe now that, letting Eloise play in the role of $B$ and Abelard in the role of $A$ , the alternating reachability game on the Kripke-model $\mathcal{T}_{\_}\mathcal{G}$ with starting state $r_{\_}\mathcal{G}$ is essentially identical with the game $\mathcal{G}$ : the positions and the rules for moves are the same, and the winning conditions are equivalent.⁵⁵5For example, in a position $p=(v,\psi,c)$ with $\psi$ a literal such that $\mathcal{M},v\nvDash\psi$ , $B$ loses the alternating reachability game since $p$ does not have any $E_{\_}\mathcal{G}$ -successors. Thus, defining $J_{\_}\varphi(\mathcal{M},w_{\_}0,\Gamma):=(\mathcal{T}_{\_}\mathcal{G},r_{\_}\mathcal{G})$ , and using Theorem 4.2, we obtain the first equivalence (1). Clearly $J_{\_}\varphi(\mathcal{M},w_{\_}0,\Gamma)$ can be computed from the input $(\mathcal{M},w_{\_}0,\Gamma)$ in LogSpace.

The transformation $I_{\_}\varphi$ can now be defined as follows: we let $I_{\_}\varphi(\mathcal{M},w_{\_}0):=J_{\_}\varphi(\mathcal{M},w_{\_}0,(\mathsf{card}(\mathcal{M}))^{+})$ . Denote $\Gamma^{*}:=(\mathsf{card}(\mathcal{M}))^{+}$ below. By Corollary 4.3 and (1) we have

(\mathcal{M},w_{\_}0)\in\mathrm{MC}(\varphi)\;\;\text{ iff }\;\;(\mathcal{M},w_{\_}0,\Gamma^{*})\in\mathrm{BMC}(\varphi)\;\;\text{ iff }\;\;J_{\_}\varphi(\mathcal{M},w_{\_}0,\Gamma^{*})\in\mathrm{AR},

whence (2) holds. Clearly $I_{\_}\varphi$ is LogSpace-computable.

Since game trees of bounded evaluation games are well-founded, it is clear that $J_{\_}\varphi(\mathcal{M},w,\Gamma)$ and $I_{\_}\varphi(\mathcal{M},w)$ do not contain infinite paths. ∎

Thus, checking the truth of an arbitrary sentence of the modal $\mu$ -calculus can be reduced via $I_{\_}\varphi$ to checking the truth of the simple alternation free sentence $\chi$ . A related idea was used in [4] for showing that finite parity games can be reduced to safety games by adding explicit memory $M$ to the states. The elements of $M$ are essentially the same as our clock values in the finite case, except that they are given only for one of the players. This is why the resulting game in [4] is a safety game, and this can lead to infinite plays—unlike our reachability games in $I_{\_}\varphi(\mathcal{M},w)$ .

Proposition 7.1 resembles also the “Measured Collapse Theorem” in [7], which states that checking the truth of any sentence $\varphi$ of the $\mu$ -calculus can be reduced to checking the truth of an alternation free sentence $\varphi^{\prime}$ . However, unlike in Proposition 7.1, the result of [7] is not a reduction to $\mathrm{MC}(\psi)$ for a fixed sentence $\psi$ , as $\varphi^{\prime}$ depends on $\varphi$ . Moreover, the sentence $\varphi^{\prime}$ is actually a translation of $\varphi$ to a different logic, called $\mu^{\sharp}$ -calculus, whose semantics is based on an additional domain of tuples that can be related to our clock values.

It should be noted that the existence of LogSpace-computable reductions from the model checking problems $\mathrm{BMC}$ and $\mathrm{MC}$ to $\mathrm{AR}$ follows directly from the well-known fact that alternating reachability is a PTime-complete problem. However, the main point here is that our reductions $J_{\_}\varphi$ and $I_{\_}\varphi$ arise in a natural and straightforward way from the bounded evaluation game. Moreover, except for LogSpace-computability, the proof above does not rely on any point on the assumption that the Kripke models are finite. Thus we see that the reductions $J_{\_}\varphi$ and $I_{\_}\varphi$ work on infinite Kripke models as well as on finite ones: for any Kripke model $\mathcal{M}$ , state $w$ and ordinal $\Gamma$ we have

•

$\mathcal{M},w\models^{\Gamma}\varphi\;\text{ iff }\;J_{\_}\varphi(\mathcal{M},w,\Gamma)\models\chi$ , and
•

$\mathcal{M},w\models\varphi\;\text{ iff }\;I_{\_}\varphi(\mathcal{M},w)\models\chi$ .

8 Conclusion and Future Directions

Our study has focused on conceptual developments relating to the modal $\mu$ -calculus, the main result being the new $\mathsf{GTS}$ and its variants. There are many relevant future research directions; we mention here some of them. Firstly, it would be interesting to understand new clocking patterns in general, in addition to the finitely bounded, the $f$ -bounded and the free semantics discussed above. These investigations could naturally be pushed to involve more general logics beyond modal logic, possibly containing, e.g., operators that modify the underlying models, and thereby directly linking to the research on the general logical framework of [20] and the research program of [20] and [21].

More concretely, pinpointing the complexity of the satisfiability problem of the modal $\mu$ -calculus under finitely bounded semantics remains to be done. Also, it would be interesting to investigate whether the scheme of using tuples of ordinals for defining our bounded $\mathsf{GTS}$ can be modified to work with single ordinals in a natural way. Finally, using ordinals to reduce arbitrary game arenas to well-founded trees is in general an interesting research direction.⁶⁶6The problem of finding equivalent finite duration games for infinite duration games (on finite arenas) has been studied, e.g., in [3] with an essentially different kind of method. Relating to this and the work in Section 7, it would be particularly interesting to better understand reductions of general games to (well-founded) alternating reachability games.

Acknowledgements

Antti Kuusisto was funded by the Academy of Finland project Theory of Computational Logics, grant numbers 324435 and 328987. The work of Raine Rönnholm was partially supported by Jenny and Antti Wihuri Foundation. We thank the anonymous referees for comments and additional references.

References

[1]
[2] Rajeev Alur & Thomas A. Henzinger (1998): Finitary Fairness. ACM Trans. Program. Lang. Syst. 20(6), pp. 1171–1194, 10.1145/295656.295659.
[3] Benjamin Aminof & Sasha Rubin (2017): First-cycle games. Information and Computation 254, pp. 195–216, 10.1016/j.ic.2016.10.008.
[4] Julien Bernet, David Janin & Igor Walukiewicz (2002): Permissive strategies: from parity games to safety games. RAIRO Theor. Informatics Appl. 36(3), pp. 261–275, 10.1051/ita:2002013.
[5] Armin Biere, Alessandro Cimatti, Edmund M. Clarke & Yunshan Zhu (1999): Symbolic Model Checking without BDDs. In Rance Cleaveland, editor: TACAS ’99, Proceedings, LNCS 1579, Springer, pp. 193–207, 10.1007/3-540-49059-0_14.
[6] Julian Bradfield & Colin Stirling (2007): Modal mu-calculi, pp. 721–756. Elsevier, 10.1016/s1570-2464(07)80015-2.
[7] Doron Bustan, Orna Kupferman & Moshe Y. Vardi (2004): A Measured Collapse of the Modal $\mathrm{\mu}$ -Calculus Alternation Hierarchy. In Volker Diekert & Michel Habib, editors: STACS 2004, 21st Annual Symposium on Theoretical Aspects of Computer Science, Proceedings, LNCS 2996, Springer, pp. 522–533, 10.1007/978-3-540-24749-4_46.
[8] Valentin Goranko, Antti Kuusisto & Raine Rönnholm: Game-Theoretic Semantics for ATL+ with Applications to Model Checking. To appear in Information and Computation.
[9] Valentin Goranko, Antti Kuusisto & Raine Rönnholm (2016): Game-Theoretic Semantics for Alternating-Time Temporal Logic. In: Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems, AAMAS, pp. 671–679.
[10] Valentin Goranko, Antti Kuusisto & Raine Rönnholm (2017): CTL with Finitely Bounded Semantics. In Sven Schewe, Thomas Schneider & Jef Wijsen, editors: 24th International Symposium on Temporal Representation and Reasoning, TIME, LIPIcs 90, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 14:1–14:19, 10.4230/LIPIcs.TIME.2017.14.
[11] Valentin Goranko, Antti Kuusisto & Raine Rönnholm (2017): Game-Theoretic Semantics for ATL+ with Applications to Model Checking. In: Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems, AAMAS, pp. 1277–1285.
[12] Valentin Goranko, Antti Kuusisto & Raine Rönnholm (2018): Game-Theoretic Semantics for Alternating-Time Temporal Logic. ACM Trans. Comput. Log. 19(3), pp. 17:1–17:38, 10.1145/3179998.
[13] Valentin Goranko, Antti Kuusisto & Raine Rönnholm (2019): Alternating-time temporal logic ATL with finitely bounded semantics. Theor. Comput. Sci. 797, pp. 129–155, 10.1016/j.tcs.2019.05.029.
[14] Lauri Hella, Antti Kuusisto & Raine Rönnholm (2017): Bounded game-theoretic semantics for modal mu-calculus. CoRR abs/1706.00753. Available at https://arxiv.org/pdf/1706.00753v1.pdf.
[15] Lauri Hella, Antti Kuusisto & Raine Rönnholm (2020): Bounded game-theoretic semantics for modal mu-calculus. CoRR abs/1706.00753. Available at https://arxiv.org/pdf/1706.00753v2.pdf.
[16] Lauri Hella & Miikka Vilander (2019): Formula size games for modal logic and $\mu$ -calculus. J. Log. Comput. 29(8), pp. 1311–1344, 10.1093/logcom/exz025.
[17] Neil Immerman (1999): Descriptive complexity. Graduate texts in computer science, Springer, 10.1007/978-1-4612-0539-5.
[18] Dexter Kozen (1983): Results on the Propositional mu-Calculus. Theor. Comput. Sci. 27, pp. 333–354, 10.1016/0304-3975(82)90125-6.
[19] Orna Kupferman, Nir Piterman & Moshe Y. Vardi (2007): From Liveness to Promptness. In Werner Damm & Holger Hermanns, editors: Computer Aided Verification, 19th International Conference, CAV, Proceedings, LNCS 4590, Springer, pp. 406–419, 10.1007/978-3-540-73368-3_44.
[20] Antti Kuusisto (2014): Some Turing-Complete Extensions of First-Order Logic. In Adriano Peron & Carla Piazza, editors: GandALF 2014, EPTCS 161, pp. 4–17, 10.4204/EPTCS.161.4.
[21] Antti Kuusisto (2019): On Games and Computation. CoRR abs/1910.14603.
[22] Wojciech Penczek, Bozena Wozna & Andrzej Zbrzezny (2002): Bounded Model Checking for the Universal Fragment of CTL. Fundam. Inform. 51(1-2), pp. 135–156.
[23] Robert S. Streett & E. Allen Emerson (1989): An Automata Theoretic Decision Procedure for the Propositional Mu-Calculus. Inf. Comput. 81(3), pp. 249–264, 10.1016/0890-5401(89)90031-X.
[24] Wenhui Zhang (2015): Bounded semantics. Theoretical Computer Science 564, pp. 1–29, 10.1016/j.tcs.2014.10.026.