# Categorical Büchi and Parity Conditions via Alternating Fixed Points of Functors

Natsuki Urabe, Ichiro Hasuo

► To cite this version:

Natsuki Urabe, Ichiro Hasuo. Categorical Büchi and Parity Conditions via Alternating Fixed Points of Functors. 14th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2018, Thessaloniki, Greece. pp.214-234, 10.1007/978-3-030-00389-0_12. hal-02044648

HAL Id: hal-02044648

https://inria.hal.science/hal-02044648

Submitted on 21 Feb 2019

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Categorical Büchi and Parity Conditions via Alternating Fixed Points of Functors

Natsuki Urabe<fnref n="1" />(✉) and Ichiro Hasuo<fnref n="2" />

**Abstract.** Categorical studies of recursive data structures and their associated reasoning principles have mostly focused on two extremes: initial algebras and induction, and final coalgebras and coinduction. In this paper we study their in-betweens. We formalize notions of alternating fixed points of functors using constructions that are similar to that of free monads. We find their use in categorical modeling of accepting run trees under the Büchi and parity acceptance condition. This modeling abstracts away from states of an automaton; it can thus be thought of as the “behaviors” of systems with the Büchi or parity conditions, in a way that follows the tradition of coalgebraic modeling of system behaviors.

## 1 Introduction

**Büchi Automata** The Büchi condition is a common acceptance condition for automata for infinite words. Let $x_i \in X$ be a state of an automaton $\mathcal{A}$ and $a_i \in A$ be a character, for each $i \in \omega$. An infinite run $x_0 \xrightarrow{a_0} x_1 \xrightarrow{a_1} \dots$ satisfies the Büchi condition if $x_i$ is an accepting state (usually denoted by $\emptyset$) for infinitely many $i$. An example of a Büchi automaton is shown on the right. The word $(ba)^\omega$ is accepted, while $ba^\omega$ is not. A function that assigns each $x \in X$ the set of accepted words from $x$ is called the *trace semantics* of the Büchi automaton.

**Categorical Modeling** The main goal of this paper is to give a categorical characterization of such runs under the Büchi condition. This $d^\uparrow \xrightarrow{\zeta^\uparrow} Y \rightarrow Z$ is in the line of the established field of categorical studies of finite and infinite datatypes: it is well-known that finite trees form an initial algebra, and infinite trees form a final coalgebra; and finite/infinite words constitute a special case. These categorical characterizations offer powerful reasoning principles of (co)induction for both definition and proof. While the principles are categorically simple ones corresponding to universality of initial/final objects, they have proved powerful and useful in many different branches of computer science, such as functional programming and process theory. See the diagram on the right above illustrating coinduction: given a functor $F$, its final coalgebra $\zeta: Z \rightsquigarrow FZ$

<footnote n="1">¹ The University of Tokyo, Japan,
urabenatsuki@is.s.u-tokyo.ac.jp</footnote>

<footnote n="2">² National Institute of Informatics, Tokyo, Japan</footnote>
has a unique homomorphism to it from an arbitrary $F$-coalgebra $d: Y \to FY$. In many examples, a final coalgebra is described as a set of "infinite $F$-trees."

Extension of such (co)algebraic characterizations of data structures to the Büchi condition is not straightforward, however. A major reason is the non-local character of the Büchi condition: its satisfaction cannot be reduced to a local, one-step property of the run. For example, one possible attempt of capturing the Büchi condition is as a suitable subobject of the set $Run(X) = (A \times X)^\omega$ of all runs (including nonaccepting ones). The latter set admits clean categorical characterization as a final coalgebra $Run(X) \cong F(\text{Run}(X))$ for the functor $F = (A \times X) \times_\_$. Specifying its subset according to the Büchi condition seems hard if we insist on the coalgebraic language which is centered around the local notion of transition represented by a coalgebra structure morphism $c: X \to FX$.

There have been some research efforts in this direction, namely the categorical characterization of the Büchi condition. In [5] the authors insisted on finality and characterize languages of *Muller automata* (a generalization of Büchi automata) by a final coalgebra in *Sets*². Their characterization however relies on the lasso characterization of the Büchi condition that works only in the setting of finite state spaces. In [21] we presented an alternative characterization that covers infinite state spaces and automata with probabilistic branching. The key idea was the departure from coinduction, that is, reasoning that relies on the universal property of greatest fixed points. Note that a final coalgebra $\zeta: Z \cong FZ$ is a "categorical greatest fixed point" for a functor $F$.

Our framework in [21] was built on top of the so-called *Kleisli approach* to trace semantics of coalgebras [16, 12, 10, 11]. There a system is a coalgebra in a Kleisli category $\mathcal{K}\ell(T)$, where $T$ represents the kind of branching the system exhibits (nondeterminism, probability, etc.). A crucial fact in this approach is that homsets of the category $\mathcal{K}\ell(T)$ come with a natural order structure. Specifically, in [21], we characterized trace semantics under the Büchi condition as in the diagrams (1) below<fnref n="3" />, where i) $X_1$ (resp. $X_2$) is the set of nonaccepting (resp. accepting) states of the Büchi automaton (i.e. $X = X_1 + X_2$), and ii) the two diagrams form a *hierarchical equation system* (HES), that is roughly a planar representation of nested and alternating fixed points. In the HES, we first calculate the least fixed point for the left diagram, and then calculate the greatest fixed point for the right diagram with $u_1$ replaced by the obtained least fixed point. Note that the order of calculating fixed points matters.

$$ \begin{array}{ccc} \begin{array}{ccc} \multicolumn{3}{c}{\bar{F}[u_1, u_2]} \\ FX \quad \begin{array}{c} \xrightarrow{\phantom{=} \bar{F}[u_1, u_2]} \\ \xleftarrow[c_1 \uparrow]{\phantom{=} \bar{F}[u_1, u_2]} \end{array} & \longrightarrow & FZ \\ X_1 \quad \begin{array}{c} \xrightarrow{\phantom{=} \bar{F}[u_1, u_2]} \\ \xleftarrow[c_2 \uparrow]{\substack{=\mu \\ u_1}} \end{array} & \longrightarrow & Z \end{array} \quad (1) $$

**Contributions: Decorated Trace Semantics by Categorical Datatypes**

In this paper we introduce an alternative categorical characterization to the one

<footnote n="3">³ We write $f: X \to Y$ for a Kleisli arrow $f \in \mathcal{K}\ell(T)(X, Y)$ and $\bar{F}: \mathcal{K}\ell(T) \to \mathcal{K}\ell(T)$ for a lifting of the functor $F$ over $\mathcal{K}\ell(T)$, for distinction.</footnote>
in [21] for the Büchi conditions, where we do not need alternating fixed points in homsets. This is made possible by suitably refining the value domain, from a final coalgebra to a novel categorical datatypes $F^{+\oplus 0}$ and $F^{+}(F^{+\oplus 0})$ that have the Büchi condition built in them. Diagrammatically the characterization looks as in (2) below. Note that we ask for the greatest fixed point in both squares.

$$ \begin{array}{ccc} \begin{array}{rcl} \overline{F(v_1 + v_2)} & \dashrightarrow & F(F^+(F^{+\oplus 0}) + F^{+\oplus 0}) \\ \begin{array}{c} c_1 \\ \uparrow \end{array} & \quad & \begin{array}{c} =\nu \\ J(\beta_1)_0 \uparrow \end{array} \\ X_1 & \dashrightarrow & \begin{array}{c} v_1 \\ \uparrow \end{array} \end{array} \quad \begin{array}{rcl} \overline{F(v_1 + v_2)} & \dashrightarrow & F(F^+(F^{+\oplus 0}) + F^{+\oplus 0}) \\ \begin{array}{c} c_2 \\ \uparrow \end{array} & \quad & \begin{array}{c} =\nu \\ J(\beta_2)_0 \uparrow \end{array} \\ X_2 & \dashrightarrow & \begin{array}{c} v_2 \\ \uparrow \end{array} \end{array} \end{array} \quad (2) $$

The functors $F^+$ and $F^{+\oplus}$ used in the datatypes are obtained by applying two operations ($\_\)_+$ and ($\_\)_\oplus$) to a functor $F$. For an endofunctor $G$ on a category $\mathcal{C}$ with enough initial algebras, $G^+X$ is given by the carrier object of a (choice of) an initial $G(\_ + X)$-algebra for each $X \in \mathcal{C}$. The universality of initial algebras allows one to define $G^+f : G^+X \to G^+Y$ for each $f : X \to Y$ and extend $G^+$ to a functor $G^+ : \mathcal{C} \to \mathcal{C}$. This definition is much similar to that of a free monad $G^*$, where $G^*X$ is the carrier object of an initial $G(\_)$ + $X$-algebra for $X \in \mathcal{C}$. The operation ($\_\)_\oplus$) is defined similarly: for $G : \mathcal{C} \to \mathcal{C}$ and $X \in \mathcal{C}$, $G^\oplus X$ is given by the carrier object of a final $G(\_ + X)$-coalgebra. This construction resembles to that of free completely iterative algebras [14].

The constructions of $F^+(F^{+\oplus 0})$ and $F^{+\oplus 0}$ has a clear intuitive meaning. For the specific example of A-labeled nondeterministic Büchi automata, $T = \mathcal{P}$, $F = A \times (\_)$, $F^+(F^{+\oplus 0}) \cong F^{+\oplus 0} \cong (A^+)^\omega$. Hence an element in $F^+(F^{+\oplus 0})$ or $F^{+\oplus 0}$ is identified with an infinite sequence of finite words. We understand it as an infinite word “decorated” with information about how accepting states are visited, by considering that an accepting state is visited at each splitting between finite words. For example, we regard $(a_0a_1)(a_2a_3a_4)(a_5a_6)(a_7) \dots \in (A^+)^\omega \cong F^{+\oplus 0}$ as an infinite word decorated as follows.
$$ (3) $$

$$ \circled{0} \rightarrow \circled{1} \rightarrow \circled{2} \rightarrow \circled{3} \rightarrow \circled{4} \rightarrow \circled{5} \rightarrow \circled{6} \rightarrow \circled{7} \rightarrow \circled{8} \rightarrow \dots $$

An element in $F^+(F^{+\oplus 0})$ is similarly understood, except that the initial state is regarded as a nonaccepting state. We note that by its definition, the resulting “decorated” word always satisfies the Büchi condition.

Thus the arrows $v_1 : X_1 \to F^+(F^{+\oplus 0})$ and $v_2 : X_2 \to F^{+\oplus 0}$ in (2) are regarded as a kind of trace semantics that assigns each state $x \in X$ the set of infinite words accepted from $x$ “decorated” with information about the corresponding accepting run. Hence we shall call $v_1$ and $v_2$ a decorated trace semantics for the coalgebra $c$. The generality of the category theory allows us to define decorated trace semantics for systems with other transition or branching types, e.g. *Büchi tree automata* or *probabilistic Büchi automata*.

In this paper, we also show the relationship between decorated trace semantics and (ordinary) trace semantics for Büchi automata. For the concrete case of Büchi automata sketched above, there exists a canonical function $(A^+)^\omega \to A^\omega$ that flattens a sequence and hence removes the “decorations”. It is easy to see
that if we thus remove decorations of a decorated trace semantics then we obtain
an ordinary trace semantics. We shall prove its categorical counterpart.

In fact, the framework in [21] also covered the *parity* condition, which generalizes the Büchi condition. A *parity automaton* is equipped with a function $\Omega : X \to [1, 2n]$ that assigns a natural number called a *priority* to each state $x \in X$. Our new framework developed in the current paper also covers parity automata. In order to obtain the value domain for parity automata, we repeatedly apply $(\_)+$ and $(\_)^{\oplus}$ to $F$ like $F^{+\oplus \cdots + \oplus 0}$.

Compared to the existing characterization shown in (1), one of the characteristics of our new characterization as shown in (2) is that information about accepting states is more explicitly captured in decorated trace semantics, as in (3). This characteristics would be useful in categorically characterizing notions about Büchi or parity automata. For example, we could use it for categorically characterizing (bi)simulation notions for Büchi automata, e.g. *delayed simulation* [8], a simulation notion known to be appropriate for state space reduction.

To summarize, our contributions in this paper are as follows:

- We introduce a new categorical data type $F^{+\oplus 0}$, an alternating fixed point of a functor, for characterizing the Büchi acceptance condition.

- Using the data type, we introduce a categorical decorated trace semantics, simply as a greatest fixed point.

- We show the categorical relationship with ordinary trace semantics in [21].

- We instantiate the framework to several types of concrete systems.

- We extend the framework to the parity condition (in the appendix).

**Related Work** As we have mentioned, a categorical characterization of Büchi and parity conditions is also found in [5], but adaptation to infinite-state or probabilistic systems seems to be difficult in their framework. There also exist notions which are fairly captured by their characterization but seem difficult to capture in the frameworks in [21] and this paper, such as bisimilarity.

The notion of alternating fixed point of functors is also used in [9, 2]. In [9] the authors characterize the set of continuous functions from $A^\omega$ to $B^\omega$ as an alternating fixed point $\nu X \cdot \mu Y \cdot (B \times X) + Y^A$ of a functor. Although the data type and the one used in the current paper are different and incomparable, the intuition behind them is very similar, because the former comes with a Büchi-like flavor: if $f(a_0 a_1 \dots) = b_0 b_1 \dots$ then each $b_i$ should be determined by a *finite* prefix of $a_0 a_1 \dots$, and therefore $f$ is regarded as an *infinite* sequence of such assignments. In [2, §7] a sufficient condition for the existence of such an alternating fixed point is discussed.

**Organization** §2 gives preliminaries. In §3 we introduce a categorical data type for decorated trace semantics as an alternating fixed point of functors. In §4 we define a categorical decorated trace semantics, and show a relationship with ordinary categorical trace semantics in [21]. In §5 we apply the framework to nondeterministic Büchi tree automata. In §6, we briefly discuss systems with other branching types. In §7, we conclude and give future work.
All the discussions in this paper also apply to the parity condition. However, for the sake of simplicity and limited space, we mainly focus on the Büchi condition throughout the paper, and defer discussions about the parity condition to the appendix, that is found in the extended version [20] of this paper. We omit a proof if an analogous statement is proved for the parity condition in the appendix. Some other proofs and discussions are also deferred to the appendix.

# 2 Preliminaries

## 2.1 Notations

For $m, n \in \mathbb{N}$, $[m, n]$ denotes the set $\{i \in \mathbb{N} \mid m \le i \le n\}$. We write $\pi_i : \prod_i X_i \to X_i$ and $\kappa_i : X_i \to \prod_i X_i$ for the canonical projection and injection respectively. For a set $A$, $A^*$ (resp. $A^\omega$) denotes the set of finite (resp. infinite) sequences over $A$, $A^\infty$ denotes $A^* \cup A^\omega$, and $A^+$ denotes $A^* \setminus \{\langle\rangle\}$. We write $\langle\rangle$ for the empty sequence. For a monotone function $f : (X, \sqsubseteq) \to (X, \sqsubseteq)$, $\mu f$ (resp. $\nu f$) denotes its least (resp. greatest) fixed point (if it exists). We write **Sets** for the category of sets and functions, and **Meas** for the category of measurable sets and measurable functions. For $f : X \to Y$ and $A \subseteq Y$, $f^{-1}(A)$ denotes $\{x \in X \mid f(x) \in A\}$.

## 2.2 Fixed Point and Hierarchical Equation System

In this section we review the notion of hierarchical equation system (HES) [6, 3]. It is a kind of a representation of an alternating fixed point.

**Definition 2.1 (HES)** A hierarchical equation system (HES for short) is a system of equations of the following form.

$$E = \begin{cases} u_1 = \eta_1 & f_1(u_1, \dots, u_m) \in (L_1, \sqsubseteq_1) \\ u_2 = \eta_2 & f_2(u_1, \dots, u_m) \in (L_2, \sqsubseteq_2) \\ \vdots \\ u_m = \eta_m & f_m(u_1, \dots, u_m) \in (L_m, \sqsubseteq_m) \end{cases}$$

Here for each $i \in [1, m]$, $(L_i, \leq_i)$ is a complete lattice, $u_i$ is a variable that ranges over $L_i$, $\eta_i \in \{\mu, \nu\}$ and $f_i : L_1 \times \dots \times L_m \to L_i$ is a monotone function.

**Definition 2.2 (solution)** Let $E$ be an HES as in Def. 2.1. For each $i \in [1, m]$ and $j \in [1, i]$ we inductively define $f_i^\ddagger : L_i \times \dots \times L_m \to L_i$ and $l_j^{(i)} : L_{i+1} \times \dots \times L_m \to L_j$ as follows (no need to distinguish the base case from the step case):

$$-f_i^\ddagger(u_i, \dots, u_m) := f_i(l_1^{(i-1)}(u_i, \dots, u_m), \dots, l_{i-1}^{(i-1)}(u_i, \dots, u_m), u_i, \dots, u_m); \text{ and}$$

$$-l_i^{(i)}(u_{i+1}, \dots, u_m) := \eta f_i^\ddagger(\_, u_{i+1}, \dots, u_m) \text{ where } \eta = \mu \text{ if } i \text{ is odd and } \eta = \nu \\ \text{if } i \text{ is even. For } j < i, l_j^{(i)}(u_{i+1}, \dots, u_m) := l_j^{(i-1)}(l_i^{(i)}(u_{i+1}, \dots, u_m), u_{i+1}, \dots, u_m). \\ \text{If such a least or greatest fixed point does not exist, then it is undefined.}$$

We call $(l_1^{(i)}, \dots, l_i^{(i)})$ the $i$-th intermediate solution. The solution of the HES $E$ is a family $(u_1^{\text{sol}}, \dots, u_m^{\text{sol}}) \in L_1 \times \dots \times L_m$ defined by $u_i^{\text{sol}} := l_i^{(m)}(*)$ for each $i$.
## 2.3 Categorical Finite and Infinitary Trace Semantics

We review [16, 11, 12, 18] and see how finite and infinitary traces of transition systems are characterized categorically. We assume that the readers are familiar with basic theories of categories and coalgebras. See e.g. [4, 13] for details.

We model a system as a (T, F)-system, a coalgebra $c : X \to TFX$ where T is a monad representing the branching type and F is an endofunctor representing the transition type of the system. Here are some examples of T and F:

**Definition 2.3 (P, D, L and G)** The powerset monad is a monad $P = (P, \eta^P, \mu^P)$ on **Sets** where $PX := \{A \subseteq X\}$, $Pf(A) := \{f(x) \mid x \in A\}$, $\eta_X^P(x) := \{x\}$ and $\mu_X^P(\Gamma) := \bigcup_{A \in \Gamma} A$. The subdistribution monad is a monad $D = (D, \eta^D, \mu^D)$ on **Sets** where $DX := \{\delta : X \to [0,1] \mid |\{x \mid \delta(x) > 0\}| \text{ is countable, and } \sum_x \delta(x) \le 1\}$, $Df(\delta)(y) := \sum_{x \in f^{-1}(\{y\})} \delta(x)$, $\eta_X^D(x)(x')$ is 1 if $x = x'$ and 0 otherwise, and $\mu_X^D(\Phi)(x) := \sum_{\delta \in DX} \Phi(\delta) \cdot \delta(x)$. The lift monad is a monad $\mathcal{L} = (\mathcal{L}, \eta^\mathcal{L}, \mu^\mathcal{L})$ on **Sets** where $\mathcal{L}X := \{\perp\} + X$, $\mathcal{L}f(a)$ is $f(a)$ if $a \in X$ and $\perp$ if $a = \perp$, $\eta_X^\mathcal{L}(x) := x$ and $\mu_X^\mathcal{L}(a) := a$ if $a \in X$ and $\perp$ if $a = \perp$. The sub-Giry monad is a monad $\mathcal{G} = (\mathcal{G}, \eta^\mathcal{G}, \mu^\mathcal{G})$ on **Meas** where $\mathcal{G}(X, \mathfrak{F}_X)$ is carried by the set of probability measures over $(X, \mathfrak{F}_X)$, $\mathcal{G}f(\varphi)(A) := \varphi(f^{-1}(A))$, $\eta_X^\mathcal{G}(x)(A)$ is 1 if $x \in A$ and 0 otherwise, and $\mu_X^\mathcal{G}(\Xi)(A) := \int_{\delta \in \mathcal{G}X} \delta(A)d\Xi$.

**Definition 2.4 (polynomial functors)** A polynomial functor $F$ on **Sets** is defined by the following BNF notation: $F ::= \text{id} \mid A \mid F \times F \mid \coprod_{i \in I} F$ where $A \in \text{Sets}$ and $I$ is countable. A (standard Borel) polynomial functor $F$ on **Meas** is defined by the following BNF notation: $F ::= \text{id} \mid A \mid F \times F \mid \coprod_{i \in I} F$ where $A \in \text{Meas}$, $I$ is countable, and the $\sigma$-algebras over products and coproducts are given in the standard manner (see e.g. [18, Def. 2.2]).

A carrier of an initial $F$-algebra models a domain of finite traces [11] while that of a final $F$-coalgebra models a domain of infinitary traces [12]. For example, as we have seen in §1, for $F = \{\check{\vee}\} + A \times (\_)$ on **Sets**, the carrier set of the final $F$-coalgebra is $A^\infty$ while that of the initial $F$-algebra is $A^*$. The situation is similar for a polynomial functor $F = (\{\check{\vee}\}, \mathcal{P}\{\check{\vee}\}) + (A, \mathcal{P}A) \times (\_)$ on **Meas**. The carrier of an initial algebra is $(A^*, \mathcal{P}A^*)$, and that of a final coalgebra is $(A^\infty, \mathfrak{F}_{A^\infty})$ where $\mathfrak{F}_{A^\infty}$ is the standard $\sigma$-algebra generated by the cylinder set.

In general, for a certain class of functors, an initial algebra and a final coalgebra are obtained by the following well-known construction.

**Theorem 2.5 ([1])** 1. Let $(A, (\pi_i : F^i 0 \to A)_{i \in \omega})$ be a colimit of an $\omega$-chain $0 \xrightarrow{\cdot} F0 \xrightarrow{F^1} F^2 0 \xrightarrow{F^2 \cdot} \dots$. If $F$ preserves the colimit, then the unique mediating arrow $\iota : FA \to A$ from the colimit $(FA, (F\pi_i : F^{i+1} 0 \to FA)_{i \in \omega})$ to a cocone $(A, (\pi'_i : F^i 0 \to A)_{i \in \omega})$ where $\pi'_i = \pi_{i+1}$ is an initial $F$-algebra.

2. Let $(Z, (\pi_i : A \to F^i 1)_{i \in \omega})$ be a limit of an $\omega^{\text{op}}$-chain $1 \stackrel{!}{\leftarrow} F1 \stackrel{F^1}{\leftarrow} F^{21} \stackrel{F^{21}!}{\leftarrow} \dots$. If $F$ preserves the limit, then the unique mediating arrow $\zeta : Z \to FZ$ from a cone $(Z, (\pi'_i : A \to F^i 1)_{i \in \omega})$ where $\pi'_i = \pi_{i+1}$ to the limit $(FZ, (F\pi_i : FZ \to F^{i+1} 1)_{i \in \omega})$ is a final $F$-coalgebra. $\square$
We next quickly review notions about the Kleisli category $\mathcal{K}\ell(T)$.

**Definition 2.6** (*$\mathcal{K}\ell(T)$, $J$, $U$ and $\overline{F}$*) Let $T = (T, \eta, \mu)$ be a monad on $\mathbb{C}$. The Kleisli category $\mathcal{K}\ell(T)$ is given by $|\mathcal{K}\ell(T)| = |\mathbb{C}|$ and $\mathcal{K}\ell(T)(X, Y) = \mathbb{C}(X, TY)$ for $X, Y \in |\mathcal{K}\ell(T)|$. An arrow $f \in \mathcal{K}\ell(T)(X, Y)$ is called a Kleisli arrow, and we write $f : X \to Y$ for distinction. Composition of arrows $f : X \to Y$ and $g : Y \to Z$ is defined by $\mu_Z \circ Tg \circ f$, and denoted by $g \odot f$ for distinction. The lifting functor $J : \mathbb{C} \to \mathcal{K}\ell(T)$ is defined by: $JX := X$ and $J(f) := \eta_Y \circ f$ for $f : X \to Y$. The forgetful functor $U : \mathcal{K}\ell(T) \to \mathbb{C}$ is defined by: $UX := TX$ and $U(g) := \mu_Y \circ Tg$ for $g : X \to Y$. A functor $\overline{F} : \mathcal{K}\ell(T) \to \mathcal{K}\ell(T)$ is called a lifting of $F : \mathbb{C} \to \mathbb{C}$ if $\overline{FJ} = JF$.

**Example 2.7** Let $T = \mathcal{P}$ and $F = \sum_{n=0}^{\infty} \Sigma_n \times (\_)^n : \mathbf{Sets} \to \mathbf{Sets}$. A lifting $\overline{F}$ over $\mathcal{K}\ell(T)$ is given by $\overline{FX} = FX$ for $X \in \mathbf{Sets}$ and $\overline{Ff}(\sigma, x_0, \dots, x_{n-1}) = \{(\sigma, y_0, \dots, y_{n-1}) \mid \forall i. y_i \in f(x_i)\}$ for $f : X \to Y$, $\sigma \in \Sigma_n$ and $x_0, \dots, x_{n-1} \in X$. (see e.g. [11]).

It is well-known that there is a bijective correspondence between a lifting $\overline{F}$ and a distributive law, a natural transformation $\lambda : FT \Rightarrow TF$ satisfying some axioms [15]. See §D of the extended version [20] for the details.

In the rest of this section, let $F$ be an endofunctor and $T$ be a monad on a category $\mathbb{C}$, and assume that a lifting $\overline{F} : \mathcal{K}\ell(T) \to \mathcal{K}\ell(T)$ is given.

In [11], a finite trace semantics of a transition system was characterized as the unique homomorphism to the final $\overline{F}$-coalgebra in $\mathcal{K}\ell(T)$, which is obtained by reversing and lifting the initial $F$-algebra in $\mathbb{C}$.

**Definition 2.8** (*$\text{tr}(c)$*) We say $F$ and $T$ constitute a finite trace situation with respect to $\overline{F}$ if the following conditions are satisfied:

- An initial $F$-algebra $\iota^F : FA \to A$ exists.

- $J(\iota^F)^{-1} : A \to \overline{FA}$ is a final $\overline{F}$-coalgebra.

For $c : X \to \overline{FX}$, the unique homomorphism from $c$ to $J(\iota^F)^{-1}$ is called the (coalgebraic) finite trace semantics of $c$ and denoted by $\text{tr}(c) : X \to A$.

In [11], a sufficient condition for constituting a finite trace situation is given.

**Theorem 2.9** ([11]) Assume each homset of $\mathcal{K}\ell(T)$ carries a partial order $\sqsubseteq$. If the following conditions are satisfied, $F$ and $T$ constitute a finite trace situation.

- The functor $F$ preserves $\omega$-colimits in $\mathbb{C}$.

- Each homset of $\mathcal{K}\ell(T)$ constitutes an $\omega$-cpo with a bottom element $\bot$.

- Kleisli composition $\odot$ is monotone, and the lifting $\overline{F}$ is locally monotone, i.e. $f \sqsubseteq g$ implies $\overline{Ff} \sqsubseteq \overline{Fg}$.

- Kleisli composition $\odot$ preserves $\omega$-suprema and the bottom element $\bot$.
Their coalgebraic trace semantics is given by a solution of an HES.

**Definition 2.13 (tr<sup>B</sup><sub>i</sub>(c))** Assume that each homset of Kℓ(T) carries a partial order ⊑. We say that F and T constitute a *Büchi trace situation* with respect to F and ⊑ if they satisfy the following conditions:

- A final F-coalgebra ζ : Z → FZ exists.

- For an arbitrary Büchi (T, F)-system X = (c, (X₁, X₂)), the following HES has a solution.

$$E_c = \begin{cases} u_1 = \mu & J\zeta^{-1} \odot \bar{F}[u_1, u_2] \odot c_1 \in (K\ell(T)(X_1, Z), \sqsubseteq_{X_1, Z}) \\ u_2 = \nu & J\zeta^{-1} \odot \bar{F}[u_1, u_2] \odot c_2 \in (K\ell(T)(X_2, Z), \sqsubseteq_{X_2, Z}) \end{cases}$$

The solution ($u_1^{\text{sol}} : X_1 \to Z, u_2^{\text{sol}} : X_2 \to Z$) of $E_c$ is called the (coalgebraic) Büchi trace semantics of X. We write tr<sup>B</sup><sub>i</sub>(c) for $u_i^{\text{sol}}$ for each i (see also Eq. (1)).

**Example 2.14** Let $T = \mathcal{P}$ and $F = A \times (\_)$.

Then a Büchi (T, F)-system (c : X → FX, (X₁, X₂)) is identified with an A-labeled Büchi automaton. Following Def. 2.2 we shall sketch how the solution of the HES $E_c$ in Def. 2.13 is calculated.

Note that $Z \cong A^\omega$.

- We first calculate an intermediate solution $l_1^{(1)}(u_2) : X_1 \to A^\omega$ as the least fixed point of $u_1 \mapsto J\zeta^{-1} \odot \bar{F}[u_1, u_2] \odot c_1$.

- We next define $f_2^\ddagger : K\ell(T)(X_2, Z) \to K\ell(T)(X_2, Z)$ by $f_2^\ddagger(u_2) := J\zeta^{-1} \odot \bar{F}[l_1^{(1)}(u_2), u_2] \odot c_2$.

- We calculate $l_2^{(2)}(*) : X_2 \to A^\omega$ as the greatest fixed point of $f_2^\ddagger$.

- We let $l_1^{(2)}(*) := l_1^{(1)}(l_2^{(2)}) : X_1 \to A^\omega$.

Then for each i, the solution tr<sup>B</sup><sub>i</sub>(c) = $l_i^{(2)}(*)$ is given as follows [21]:

$$\text{tr}_{i}^{\mathcal{B}}(c)(x) := \left\{ a_1 a_2 \dots \in A^{\omega} \mid \begin{array}{l} \exists x_0, x_1, \dots \in X. \forall i \in \omega. (a_{i+1}, x_{i+1}) \in c(x_i) \text{ and} \\ x_i \in X_2 \text{ for infinitely many } i \end{array} \right\}.$$

# 3 Alternating Fixed Points of Functors

## 3.1 Categorical Datatypes for Büchi Systems

We first introduce the categorical datatypes $F^+X$ and $F^\oplus X$, which are understood as least and greatest fixed points of a functor F.

**Definition 3.1 (F<sup>+</sup>, F<sup>\oplus</sup>)** For $F: \mathbb{C} \to \mathbb{C}$, we define functors $F^+, F^{\oplus}: \mathbb{C} \to \mathbb{C}$ as follows. Given $X \in \mathbb{C}$, the object $F^+X$ is the carrier of (a choice of) an initial algebra $\iota_X^F : F(F^+X + X) \cong F^+X$ for the functor $F(\_, X)$. Similarly, the object $F^{\oplus}X$ is the carrier of a final coalgebra $\zeta_X^F : F^{\oplus}X \cong F(F^{\oplus}X + X)$. For
$f: X \to Y$, $F^+f: F^+X \to F^+Y$ is given as the unique homomorphism from $\iota_X^F$ to $\iota_Y^F \circ F(\mathrm{id}_{F^+X} + f)$. We define $F^\oplus f: F^\oplus X \to F^\oplus Y$ similarly.

$$ \begin{array}{ccc} F(F^+X + X) & \xrightarrow{F(F^+f+\mathrm{id})} & F(F^\oplus X + Y) \\ \multicolumn{3}{c}{\xleftarrow{\mathrm{F}(\mathrm{id}+f)} \mathrm{F}(\mathrm{id}+f)\uparrow} \\ \multicolumn{3}{c}{\begin{array}{c} \cong \\ \iota_X^F \end{array} \quad = \quad \begin{array}{c} \mathrm{F}(F^+Y + Y) \\ \iota_Y^F \end{array}} \\ \multicolumn{3}{c}{\begin{array}{c} \xrightarrow{F^+f} \\ \mathrm{F}^+X \end{array} \quad \xrightarrow{\mathrm{F}^\oplus f} \quad \begin{array}{c} \cong \\ \iota_X^F \end{array} \end{array} \quad \begin{array}{ccc} F(F^\oplus X + Y) & \xrightarrow{F(F^\oplus f+\mathrm{id})} & F(F^\oplus Y + Y) \\ \multicolumn{3}{c}{\xleftarrow{\mathrm{F}(\mathrm{id}+f)} \mathrm{F}(\mathrm{id}+f)\uparrow} \\ \multicolumn{3}{c}{\begin{array}{c} \cong \\ \iota_Y^F \end{array} \quad = \quad \begin{array}{c} \mathrm{F}^\oplus X + X \\ \iota_X^F \end{array}} \\ \multicolumn{3}{c}{\begin{array}{c} \xrightarrow{F^\oplus f} \\ \mathrm{F}^\oplus X \end{array} \quad \xrightarrow{\mathrm{F}^\oplus f} \quad \begin{array}{c} \cong \\ \iota_Y^F \end{array} \end{array} \end{array} $$

**Remark 3.2** The construction $F^+$ resembles the free monad $F^*$ over $F$. The latter is defined as follows: given $X \in \mathbb{C}$, the object $F^*X$ is the carrier of an initial algebra $F(F^*X) + X \cong F^*X$ for the functor $F(\cdot) + X$. The notations generalize the usual distinction between $\otimes$ and $+$. Indeed, for $\mathbb{C} = \mathbf{Sets}$ and $F = \Sigma_0 \times \cdot$ (where $\Sigma_0$ is an alphabet), we have $F^+1 = \Sigma_0^+$ (the set of finite words of length $\ge 1$) and $F^*1 = \Sigma_0^*$ (the set of all finite words). Similarly, $F^\oplus$ resembles the free completely iterative monad [14].

**Example 3.3** For $F = \mathbf{A} \times (\cdot)$, by the construction in Thm. 2.5, $F^+X \cong \mathbf{A}^+X$, $F^\oplus X \cong \mathbf{A}^+X + \mathbf{A}^\omega$ and $F^{+\oplus}X \cong (\mathbf{A}^+)^+X + (\mathbf{A}^+)^\omega$. Especially, if we let $X = 0$ then $F^{+\oplus 0} \cong (\mathbf{A}^+)^\omega$. We identify $(a_{00}a_{01} \dots a_{0n_0})(a_{10}a_{11} \dots a_{1n_1}) \dots \in F^{+\oplus 0} \cong (\mathbf{A}^+)^\omega$ with the following “decorated” sequence:

$$ (a_{00}, \odot)(a_{01}, \odot) \dots (a_{0n_0}, \odot)(a_{10}, \odot)(a_{11}, \odot) \dots (a_{1n_1}, \odot) \dots \in (\mathbf{A} \times \{\odot, \odot\})^\omega. $$

The second component of each element (i.e. *decoration*) represents a break of a word: it is 2 if and only if it is the beginning of a word. It is remarkable that in the sequence above, $\odot$ always appears infinitely many times. Hence $w \in (\mathbf{A}^+)^\omega$ is understood as an infinite word decorated so that the Büchi condition is satisfied.

We next define Kleisli arrows $\beta_1 X$ and $\beta_2 X$ that are used to define decorated trace semantics (see the diagrams in (2)).

**Definition 3.4** We define natural transformations $\beta_1: F^+(F^{+\oplus}+\mathrm{id}) \Rightarrow F(F^+F^{+\oplus}+F^{+\oplus}+\mathrm{id})$ and $\beta_2: F^{+\oplus} \Rightarrow F(F^+F^{+\oplus} + F^{+\oplus} + \mathrm{id})$ as follows.

$$ \beta_1 X := \left( \begin{array}{c} F^+(F^{+\oplus}X + X) \\ \multicolumn{2}{c}{\xrightarrow{\iota_{F^{+\oplus}X}^F} \iota_{F^{+\oplus}X}^F} \end{array} \right) \xrightarrow{\iota_{F^{+\oplus}X}^F} F(F^+F^{+\oplus}X + F^{+\oplus}X + X) $$

$$ \beta_2 X := \left( F^{+\oplus}X \xrightarrow{\iota_X^{F^+}} F^+(F^{+\oplus}X + X) \xrightarrow{\iota_{F^{+\oplus}X}^F} F(F^+F^{+\oplus}X + F^{+\oplus}X + X) \right) $$

**Remark 3.5** As a final coalgebra $\iota_X^{F^+}$ is an isomorphism, we can see from Def. 3.4 that $F^+(F^{+\oplus}X + X) \cong F^{+\oplus}X$. For $F = \mathbf{A} \times (\cdot)$, if we regard $F^{+\oplus}X$ as $(\mathbf{A}^+)^\omega$ as in Ex. 3.3, $F^+(F^{+\oplus}X + X)$ would be understood as $\mathbf{A}^+(\mathbf{A}^+)^\omega$, which is indeed isomorphic to $(\mathbf{A}^+)^\omega$. However, in this paper, mainly for the sake of simplicity of notations, we explicitly distinguish them and later write types of a decorated trace semantics of a Büchi $(T, F)$-system as $\mathrm{dtr}_1(c) : X_1 \to F^+(F^{+\oplus}0)$ and $\mathrm{dtr}_2(c) : X_2 \to F^{+\oplus}0$. Because of this choice, while an element in $F^{+\oplus}0 \cong (\mathbf{A}^+)^\omega$
### 3.3 Liftings $\overline{F}^+$ and $\overline{F}^{\oplus}$ over $\mathcal{K}\ell(T)$

Let $\overline{F} : \mathcal{K}\ell(T) \to \mathcal{K}\ell(T)$ be a lifting of a functor $F$. We show that under certain conditions, it induces liftings $\overline{F}^+ : \mathcal{K}\ell(T) \to \mathcal{K}\ell(T)$ of $F^+$ and $\overline{F}^{\oplus} : \mathcal{K}\ell(T) \to \mathcal{K}\ell(T)$ of $F^{\oplus}$. Note that a lifting $\overline{F}$ induces a lifting $\overline{F}(-+A) : \mathcal{K}\ell(T) \to \mathcal{K}\ell(T)$ of $F(-+A)$ which is defined by $\overline{F}(-+A)f := \overline{F}(f+\mathrm{id}_A) = \overline{F}([T\kappa_1, T\kappa_2]\circ(f+\eta_A))$ using the coproduct in $\mathcal{K}\ell(T)$.

**Definition 3.10** 1. Assume $T$ and $F$ constitute a finite trace situation. For $X \in \mathbb{C}$, we let $\overline{F}^+X := F^+X$. For $f : X \to Y$, we define $\overline{F}^+f : F^+X \to F^+Y$ as the unique homomorphism from $\overline{F}(\mathrm{id}_{F^+X} + f) \odot J(\iota_X^F)^{-1}$ to $J(\iota_Y^F)^{-1}$.

2. Assume $T$ and $F$ constitute an infinitary trace situation. For $X \in \mathbb{C}$, we let $\overline{F}^{\oplus}X := F^{\oplus}X$. For $f : X \to Y$, we define $\overline{F}^{\oplus}f : F^{\oplus}X \to F^{\oplus}Y$ as the greatest homomorphism from $\overline{F}(\mathrm{id}_{F^{\oplus}X} + f) \odot J\zeta_X^F$ to $J\zeta_Y^F$.

$$ \begin{array}{ccc} \overline{F}(F^+X + Y)_- \xrightarrow{\overline{F}(\overline{F}^+f+\mathrm{id}_{F^+X})} \overline{F}(F^+Y + Y) & & \overline{F}(F^\oplus X + Y)_- \xrightarrow{\overline{F}(\overline{F}^\oplus f+\mathrm{id}_{F^\oplus X})} \overline{F}(F^\oplus Y + Y) \\ \overline{F}(\mathrm{id}_F)\hat{\oplus} & & \overline{F}(\mathrm{id}_F)\hat{\oplus} \\ \overline{F}(F^+X + X) & \stackrel{J(\iota_X^F)^{-1}\cong}{=} & \overline{F}(F^\oplus X + X) \stackrel{\nu}{=} \overline{J\zeta_Y^F}\cong \\ \overline{J(\iota_X^F)^{-1}\hat{\oplus}\cong} & & \overline{F^+X} \stackrel{\overline{F^\oplus f}\cong}{\xrightarrow{\overline{F^\oplus X}}} \overline{F^\oplus Y} \end{array} $$

$$ \begin{array}{ccc} \overline{F}(F^\oplus X + Y)_- \xrightarrow{\overline{F}(F^\oplus f+\mathrm{id}_{F^\oplus X})} \overline{F}(F^\oplus Y + Y) & & \overline{F}(\mathrm{id}_F)\hat{\oplus} \\ \overline{F}(\mathrm{id}_F)\hat{\oplus} & & \overline{F}(\mathrm{id}_F)\hat{\oplus} \\ \overline{F}(F^\oplus X + X) & \stackrel{\nu}{=} & \overline{F^\oplus f} \\ \overline{J\zeta_X^F}\hat{\oplus}\cong & & \overline{F^\oplus f} \\ \overline{F^\oplus X} & \xrightarrow{\overline{F^\oplus f}} & \overline{F^\oplus Y} \end{array} $$

In the rest of this section, we check under which conditions $\overline{F}^+$ and $\overline{F}^{\oplus}$ are functors and form liftings of $F^+$ and $F^{\oplus}$. Factoriality of $\overline{F}^+$ holds if and only if for each $f : X \to Y$ and $g : Y \to W$, $F^+g \odot F^+f$ is the unique homomorphism from $\overline{F}(\mathrm{id} + g) \odot \overline{F}(\mathrm{id} + f) \odot J(\iota_X^F)^{-1}$ to $J(\iota_W^F)^{-1}$. Similarly, factoriality of $\overline{F}^{\oplus}$ holds if and only if $F^\oplus g \odot F^\oplus f$ is the greatest homomorphism from $\overline{F}(\mathrm{id} + g) \odot \overline{F}(\mathrm{id} + f) \odot J\zeta_X^F$ to $J\zeta_W^F$.

The former always holds by the finality. In contrast, the latter doesn't necessarily hold: a counterexample is $T = \mathcal{D}$ and $F = \{o\} \times (-)^2$ (see Ex. C.1 for details). Hence we need an extra assumption to make $\overline{F}^{\oplus}$ a functor. We hereby assume a stronger condition than is needed for the sake of discussions in §4.

**Definition 3.11** $(\Phi_{c,\sigma})$ Let $c : X \to \overline{F}X$ and $\sigma : \overline{F}Y \to Y$. We define a function $\Phi_{c,\sigma} : \mathcal{K}\ell(T)(X, Y) \to \mathcal{K}\ell(T)(X, Y)$ by $\Phi_{c,\sigma}(f) := \sigma \odot \overline{F}f \odot c$.

**Definition 3.12** Assume that $T$ and $F$ constitute an infinitary trace situation. Let $\zeta^F : Z \to FZ$ be a final $F$-coalgebra. We say that $T$ and $F$ satisfy the *gfp-preserving condition* with respect to an $\overline{F}$-algebra $\sigma : FY \to Y$ if for each $X \in \mathbb{C}$ and $c : X \to FX$, if $l : X \to Z$ is the greatest homomorphism from $c$ to $J\zeta^F$ and the function $\Phi_{J\zeta^F,\sigma}$ has the greatest fixed point $m : Z \to Y$, then $m \odot l : X \to Y$ is the greatest fixed point of $\Phi_{c,\sigma}$.

$$ \begin{array}{ccc} FX & \xrightarrow{\overline{F}l} & FZ \xrightarrow{\overline{F}m} FY \\ c\uparrow & \stackrel{\nu}{=} & \stackrel{\nu J\zeta^F\cong}{=} \\ X & \xrightarrow{l} & Z \xrightarrow{m} Y \end{array} $$

We next check if $\overline{F}^+$ and $\overline{F}^{\oplus}$ are liftings of $F^+$ and $F^{\oplus}$. By definition, we have $\overline{F}^+JX = JF^+X$ and $\overline{F}^{\oplus}JX = JF^{\oplus}X$ for each $X \in \mathbb{C}$. Let $f : X \to Y$. By definition, $\overline{F}^+Jf = JF^+f$ holds if and only if $JF^+f$ is a unique homomorphism
from $\overline{F}(\mathrm{id} + Jf) \odot J(\iota_X^F)^{-1}$ to $J(\zeta_Y^F)^{-1}$. Similarly, $\overline{F}^+Jf = JF^+f$ holds if and only if $JF^+f$ is the greatest homomorphism from $\overline{F}(\mathrm{id} + Jf) \odot J\zeta_X^F$ to $J\zeta_Y^F$.

The former is easily proved by the finality of $J(\iota_Y^F)^{-1}$, while the latter requires an assumption again.

**Definition 3.13** Assume $T$ and $F$ constitute an infinitary trace situation. Let $\zeta^F: Z \to FZ$ be a final $F$-coalgebra. We say that $T$ and $F$ satisfy the deterministic-greatest condition if for $c: X \to FX$ in $\mathbb{C}$, if $u: X \to Z$ is the unique homomorphism from $c$ to $\zeta^F$ then $Ju$ is the greatest homomorphism from $Jc$ to $J\zeta^F$.

Concluding the discussions so far, we obtain the following proposition.

**Proposition 3.14** 1. If $T$ and $F(\mathrm{id} + A)$ constitute a finite trace situation for each $A \in \mathbb{C}$, the operation $\overline{F}^+$ is a functor and is a lifting of $F^+$.

2. If $T$ and $F(\mathrm{id} + A)$ constitute an infinitary trace situation and satisfy the gfp-preserving condition with respect to an arbitrary algebra and the deterministic-greatest condition for each $A \in \mathbb{C}$, $\overline{F}^{\oplus}$ is a functor and is a lifting of $F^{\oplus}$. $\square$

Hence under appropriate conditions, a lifting $\overline{F}: K\ell(T) \to K\ell(T)$ of $F$ gives rise to liftings of $F^+$ and $F^{\oplus}$. By repeating this, we can define $\overline{F}_j^{(i)}$ for each $i$ and $j$.

See §D of the extended version [20] for the distributive laws corresponding to the liftings defined above.

**Example 3.15** Let $F = A \times (\mathrm{id})$ and $T = \mathcal{P}$. As we have seen in Ex. 3.3, $F^{+\oplus}X \cong (A^+)^+X + (A^+)^\omega$. Let $\overline{F}$ be a lifting that is given as in Ex. 2.7. We can construct a lifting $\overline{F}^{+\oplus}$ using Prop. 3.14, and for $f: X \to Y$ in $K\ell(\mathcal{P})$, $\overline{F}^{+\oplus}f: (A^+)^+X + (A^+)^\omega \to (A^+)^+Y + (A^+)^\omega$ is given by $\overline{F}^{+\oplus}f(w) = \{w'y \mid y \in f(x)\}$ if $w = w'x$ where $w' \in (A^+)^+$ and $x \in X$, and $\{w\}$ if $w \in (A^+)^\omega$.

# 4 Decorated Trace Semantics of Büchi ($T, F$)-systems

## 4.1 Definition

**Assumption 4.1** Throughout this section, let $T$ be a monad and $F$ be an endofunctor on $\mathbb{C}$, and assume that each homset of $K\ell(T)$ carries a partial order $\sqsubseteq$. We further assume the following conditions for each $A \in \mathbb{C}$.

1. $F^+, F^{+\oplus}: \mathbb{C} \to \mathbb{C}$ are well-defined and liftings $\overline{F}, \overline{F}^+, \overline{F}^{+\oplus}: K\ell(T) \to K\ell(T)$ are given.

2. $T$ and $F(\mathrm{id} + A)$ satisfy the conditions in Thm. 2.9 with respect to $\overline{F}(\mathrm{id} + A)$ and $\sqsubseteq$, and hence constitute a finite trace situation.

3. $T$ and $F^+(\mathrm{id} + A)$ constitute an infinitary trace situation with respect to $\overline{F}^+(\mathrm{id} + A)$ and $\sqsubseteq$.

4. $T$ and $F^+(\mathrm{id} + A)$ satisfy the gfp-preserving condition wrt. an arbitrary $\sigma$.

5. $T$ and $F^+(\mathrm{id} + A)$ satisfy the deterministic-greatest condition.

6. The liftings $\overline{F}^+$ and $\overline{F}^{+\oplus}$ are obtained from $\overline{F}$ and $\overline{F}^+$ using the procedure in Def. 3.10 respectively.
7. $\overline{F^+}(\underline{+}A)$ and $\overline{F^+\oplus}(\underline{+}A)$ are locally monotone.

8. T and F constitute a Büchi trace situation with respect to $\sqsubseteq$ and $\overline{F}$.

Using the categorical data type defined in §3, we now introduce a decorated Büchi trace semantics $dtr_1(c) : X_1 \to F^+(F^{+\oplus}0)$ and $dtr_2(c) : X_2 \to F^{+\oplus}0$.

**Definition 4.2** ($dtr_i(c)$) For a Büchi $(T, F)$-system $(c, (X_1, X_2))$, the decorated Büchi trace semantics is a solution ($dtr_1(c) : X_1 \to F^+(F^{+\oplus}0)$, $dtr_2(c) : X_2 \to F^{+\oplus}0$) of the following HES (see also Eq. (2)).

$$ \begin{cases} v_1 =_\nu J(\beta_1 0)^{-1} \odot \overline{F}(v_1 + v_2) \odot c_1 \in (K\ell(T)(X_1, F^+(F^{+\oplus}0)), \sqsubseteq) \\ v_2 =_\nu J(\beta_2 0)^{-1} \odot \overline{F}(v_1 + v_2) \odot c_2 \in (K\ell(T)(X_2, F^{+\oplus}0), \sqsubseteq) \end{cases} $$

Existence of a solution will be proved in the next section.

## 4.2 Trace Semantics vs. Decorated Trace Semantics

This section is devoted to sketching the proof of the following theorem, which relates decorated trace semantics $dtr_i(c)$ and Büchi trace semantics $\text{tr}_i^B(c)$ in [21] via the natural transformation in Def. 3.8.

**Theorem 4.3** For each $i \in \{1, 2\}$, $\text{tr}_i^B(c) = p_{i0}^{(2)} \circ dtr_i(c)$. $\square$

To prove this, we introduce Kleisli arrows $c_2^\ddagger$, $\tilde{l}_1^{(1)}$, $\tilde{l}_1^{(2)}$ and $\tilde{l}_2^{(2)}$. They are categorical counterparts to $f_2^\ddagger$, $l_1^{(1)}$, $l_1^{(2)}$ and $l_2^{(2)}$ (see Def. 2.2) for the HES defining $\text{tr}_i^B(c)$ (see Def. 2.13), and bridge the gap between $dtr_i(c)$ and $\text{tr}_i^B(c)$.

**Definition 4.4** ($c_2^\ddagger$, $\tilde{l}_1^{(1)}$, $\tilde{l}_1^{(2)}$, $\tilde{l}_2^{(2)}$) We define Kleisli arrows $\tilde{l}_1^{(1)} : X_1 \to F^+X_2$, $c_2^\ddagger : X_2 \to F^+X_2$, $\tilde{l}_2^{(2)} : X_2 \to F^{+\oplus}0$ and $\tilde{l}_1^{(2)} : X_1 \to F^{+\oplus}0$ as follows:

- We define $\tilde{l}_1^{(1)} : X_1 \to F^+X_2$ as the unique homomorphism from an $F(\underline{+}X_2)$-coalgebra $c_1$ to $J(\ell_{X_2}^F)^{-1}$ (see the left diagram in Eq. (4) below).

- We define $c_2^\ddagger : X_2 \to F^+X_2$ by:

$$ c_2^\ddagger := \left( X_2 \xrightarrow{c_2} F(X_1 + X_2) \xrightarrow{\overline{F(\tilde{l}_1^{(1)} + \text{id})}} F(F^+X_2 + X_2) \xrightarrow{J\ell_{X_2}^F} F^+X_2 \right). $$

- We define $\tilde{l}_2^{(2)} : X_2 \to F^{+\oplus}0$ as the greatest homomorphism from $c_2^\ddagger$ to $J\zeta_0^F$ (see the right diagram below).

$$ \begin{array}{ccc} F(X_1 + X_2) & \xrightarrow{\overline{F(\tilde{l}_1^{(1)} + \text{id})}} & F(F^+X_2 + X_2) \\ \xrightarrow{\oplus c_1} & \xrightarrow{\oplus \tilde{l}_1^{(1)}} & \xrightarrow{\oplus J(\ell_{X_2}^F)^{-1}} \\ X_1 & \xrightarrow{\oplus} & \xrightarrow{\oplus} F^+X_2 \end{array} \qquad \begin{array}{ccc} F^+(X_2) & \xrightarrow{\overline{F^+(\tilde{l}_2^{(2)})}} & F^+(F^{+\oplus}0) \\ \xrightarrow{\oplus c_2^\ddagger} & \xrightarrow{\oplus \tilde{l}_2^{(2)}} & \xrightarrow{\oplus} J\zeta_0^F \end{array} \qquad (4) $$

- We define $\tilde{l}_1^{(2)} : X_1 \to F^+(F^{+\oplus}0)$ as follows:

$$ \tilde{l}_1^{(2)} := \left( X_1 \xrightarrow{\tilde{l}_1^{(1)}} F^+X_2 \xrightarrow{\overline{F^+\tilde{l}_2^{(2)}}} F^+(F^{+\oplus}0) \right). $$
We explain an intuition why Kleisli arrows defined above bridge the gap between $\mathrm{tr}_i^B(c)$ and $\mathrm{dtr}_i(c)$. One of the main differences between them is that $\mathrm{tr}_1^B(c)$ is calculated from $l_1^{(1)}(u_2)$ which is the least fixed point of a certain function, while $\mathrm{dtr}_1(c)$ is defined as the greatest homomorphism. The arrow $\tilde{\ell}_1^{(1)}$ fills the gap because it is defined as the unique fixed point, which is obviously both the least and the greatest fixed point.

We shall prove Thm. 4.3 following the intuition above. The lemma below, which is easily proved by the finality of $a$, shows that not only $\tilde{\ell}_1^{(1)}$ but also $\tilde{\ell}_1^{(2)}$ is characterized as the unique homomorphism.

**Lemma 4.5** The Kleisli arrow $\tilde{\ell}_1^{(2)}: X_1 \to F^+(F^{+\oplus 0})$ is the unique homomorphism from $\bar{F}(\mathrm{id}+\tilde{\ell}_2^{(2)}) \odot c_1$ to $J(t_{F^{+\oplus 0}}^{-1})$. $\square$

$$ \begin{array}{c} F(X_1 + F^{+\oplus 0}) - \xrightarrow{\bar{F}(\mathrm{id}+\tilde{\ell}_2^{(2)})\oplus \bar{F}(\tilde{\ell}_1^{(2)+\mathrm{id}})} F(X_1 + X_2) \\ \xrightarrow{\tilde{\ell}_1^{(2)}} X_1 - \xrightarrow{\mathrm{id}} F^+(F^{+\oplus 0}) \end{array} \xrightarrow{\mathrm{J}(\mathrm{id}F^{+\oplus 0})^{-1}} \cong $$

Together with the definition of $\tilde{\ell}_2^{(2)}$, we have the following proposition.

**Proposition 4.6** For each $i \in \{1, 2\}$, $\tilde{\ell}_i^{(2)} = \mathrm{dtr}_i(c)$. $\square$

<figure><img src="image_2.png" /></figure>

This proposition implies the existence of a solution of the HES in Def. 4.2.

It remains to show the relationship between the $\tilde{\ell}_j^{(i)}$ and $\mathrm{tr}_i^P(c)$. By using that $\tilde{\ell}_1^{(1)}$ is the unique fixed point (and hence the least fixed point), we can prove the following equality for an arbitrary $u_2: X_2 \to F^{\oplus 0}$.

$$ l_1^{(1)}(u_2) = \left( X_1 \xrightarrow{\tilde{\ell}_1^{(1)}} F^+ X_2 \xrightarrow{\overline{F^+ u_2}} F^+ F^{\oplus 0} \xrightarrow{Jp_1^{(1)}} F^{\oplus} F^{\oplus 0} \xrightarrow{\mu_0^{F^{\oplus}}} F^{\oplus 0} \right) $$

The following equalities are similarly proved using the equality above.

$$ l_1^{(2)}(*) = \left( X_1 \xrightarrow{\tilde{\ell}_1^{(2)}} F^+ F^{\oplus 0} \xrightarrow{\overline{F^+ F^{\oplus 0}}} F^{+\oplus 0} \xrightarrow{Jp_1^{(2)}} F^{\oplus 0} \xrightarrow{\mu_0^{\oplus}} F^{\oplus 0} \right) $$

$$ l_2^{(2)}(*) = \left( X_2 \xrightarrow{\tilde{\ell}_2^{(2)}} F^{\oplus 0} \xrightarrow{\overline{F^{\oplus 0}}} F^{\oplus 0} \xrightarrow{Jp_2^{(2)}} F^{\oplus 0} \xrightarrow{\mu_0^{\oplus}} F^{\oplus 0} \right) $$

By the definition of $\mathrm{tr}_i^B(c)$, these equalities imply the following proposition.

**Proposition 4.7** For each $i \in \{1, 2\}$, $\mathrm{tr}_i^B(c) = p_i^{(2)} \circ \tilde{\ell}_i^{(2)}$. $\square$

<figure><img src="image_3.png" /></figure>

Prop. 4.6 and Prop. 4.7 immediately imply Thm. 4.3.

# 5 Decorated Trace Semantics for Nondeterministic Büchi Tree Automata

We apply the framework developed in §3–4 to *nondeterministic Büchi tree automata* (NBTA), systems that nondeterministically accept trees with respect to the Büchi condition (see e.g. [17]). We show what datatypes $F^+(F^{+\oplus 0})$ and $F^{+\oplus 0}$, and $\mathrm{dtr}_i(c)$ characterize for an NBTA. We first review some basic notions.
## 5.1 Preliminaries on Büchi Tree Automaton

**Definition 5.1 (ranked alphabet)** A *ranked alphabet* is a set $\Sigma$ equipped with an *arity function* $|\cdot|: \Sigma \to \mathbb{N}$. We write $\Sigma_n$ for $\{a \in \Sigma \mid |a| = n\}$. For a set $X$, we regard $\Sigma + X$ as a ranked alphabet by letting $|x| = 0$. We also regard $\Sigma \times X$ as a ranked alphabet by letting $|(a, x)| = |a|$.

**Definition 5.2 (Σ-labeled tree, [7])** A *tree domain* is a set $D \subseteq \mathbb{N}^*$ s.t.: i) $\langle\rangle \in D$, ii) for $w, w' \in \mathbb{N}^*$, $ww' \in D$ implies $w \in D$ (i.e. it is prefix-closed), and iii) for $w \in D$ and $i, j \in \mathbb{N}$, $wi \in D$ and $j \le i$ imply $wj \in D$ (i.e. it is downward-closed). A *Σ-labeled (infinitary) tree* is a pair $t = (D, l)$ of a tree domain $D$ and a *labeling function* $l: D \to \bigcup_{n \in \mathbb{N}} \Sigma_n$ s.t. for $w \in D$, $|l(w)| = n$ implies $\{i \in \mathbb{N} | wi \in D\} = [0, n-1]$. A *Σ-labeled tree* $t = (D, l)$ is *finite* if $D$ is a finite set. We write $\mathbf{Tree}_\infty(\Sigma)$ (resp. $\mathbf{Tree}_{\mathrm{fin}}(\Sigma)$) for the set of Σ-labeled infinitary (resp. finite) trees. For $w \in D$, the $w$-th subtree $t_w$ of $t$ is defined by $t_w := (D_w, l_w)$ where $D_w := \{w' \in \mathbb{N}^* | ww' \in D\}$ and $l_w(w') := l(ww')$. A *branch* of $t$ is a possibly infinite sequence $i_1i_2\dots \in \mathbb{N}^\infty$ s.t. $i_1i_2\dots i_k \in D$ for each $k \in \mathbb{N}$, and if it is a finite sequence $i_1i_2\dots i_k$ then $|l(i_0i_1\dots i_k)| = 0$. We sometimes identify a branch $i_0i_1\dots \in \mathbb{N}^\infty$ with a sequence $l(\langle\rangle)l(i_1)l(i_1i_2)\dots \in \Sigma^\infty$.

**Remark 5.3** For the sake of notational simplicity, we identify a $\Sigma$-labeled tree with a $\Sigma$-term in a natural manner. For example, a $\{a, b\}$-term $(a, (b, b))$ denotes an $\{a, b\}$-labeled finite tree $t = (\{\langle\rangle, 0, 1\}, [\langle\rangle \mapsto a, 0 \mapsto b, 1 \mapsto b])$. Moreover, for $\{a, b, c\}$-labeled trees $t_0 = (D_0, l_0)$ and $t_1 = (D_1, l_1)$, we write $(c, t_0, t_1)$ for a tree $t = (\{\langle\rangle \cup \{0w \mid w \in D_0\} \cup \{1w \mid w \in D_1\}, [\langle\rangle \mapsto c, 0w \mapsto l_0(w), 1w \mapsto l_1(w)]\})$.

**Definition 5.4 (NBTA)** A *nondeterministic Büchi tree automaton (NBTA)* is a tuple $\mathcal{A} = (X, \Sigma, \delta, \mathrm{Acc})$ of a state space $X$, a ranked alphabet $\Sigma$, a transition function $\delta: X \to \mathcal{P}(\bigcap_{n \in \mathbb{N}} \Sigma_n \times X^n)$ and a set $\mathrm{Acc} \subseteq X$ of accepting states.

**Definition 5.5 ($L_\mathcal{A}^\Sigma$)** Let $\mathcal{A} = (X, \Sigma, \delta, \mathrm{Acc})$ be an NBTA. A *run tree* over $\mathcal{A}$ is a $(\Sigma \times X)$-labeled tree $\rho$ such that for each subtree $((a, x), ((a_0, x_0), t_{00}, \dots, t_{0n_0}), \dots, ((a_n, x_n), t_{n0}, \dots, t_{nn_n}))$, $(a, x_0, \dots, x_n) \in \delta(x)$ holds. A run tree is *accepting* if for each branch $(a_0, x_0)(a_1, x_1) \dots \in (\Sigma \times X)^\omega$, $x_i \in \mathrm{Acc}$ for infinitely many $i$. We write $\mathrm{Run}_\mathcal{A}(x)$ (resp. $\mathrm{AccRun}_\mathcal{A}(x)$) for the set of run trees (resp. accepting run trees) whose root node is labeled by $x \in X$. For $\mathcal{A} \subseteq X$, $\mathrm{Run}_\mathcal{A}(\mathcal{A})$ denotes $\cup_{x \in \mathcal{A}} \mathrm{Run}(x)$. We define $\mathrm{AccRun}_\mathcal{A}(\mathcal{A})$ similarly. If no confusion is likely, we omit the subscript $\mathcal{A}$. We define $\mathrm{DelSt}: \mathrm{Run}(X) \to \mathbf{Tree}_\infty(\Sigma)$ by $\mathrm{DelSt}(D, l) := (D, l')$ where $l'(w) := \pi_1(l(w))$. The language $L_\mathcal{A}^\Sigma: X \to \mathcal{P}\mathbf{Tree}_\infty(\Sigma)$ of $\mathcal{A}$ is defined by $L_\mathcal{A}^\Sigma(x) = \mathrm{DelSt}(\mathrm{AccRun}_\mathcal{A}(x))$.

## 5.2 Decorated Trace Semantics of NPTA

A ranked alphabet $\Sigma$ induces a functor $F_\Sigma = \coprod_{n \in \mathbb{N}} \Sigma_n \times (\cdot)^n : \mathbf{Sets} \to \mathbf{Sets}$.
In [21], an NBTA $\mathcal{A}$ was modeled as a Büchi $(\mathcal{P}, F_\Sigma)$-system, and it was shown
that $L_\mathcal{A}^\Sigma$ is characterized by a coalgebraic Büchi trace semantics $\mathrm{tr}_i^\Sigma(c)$.
**Proposition 5.6 ([21])** For $X, Y \in \text{Sets}$, we define an order $\sqsubseteq$ on $K\ell(\mathcal{P})(X, Y)$ by $f \sqsubseteq g \overset{\text{def.}}{\iff} \forall x \in X. f(x) \subseteq g(x)$. We define $\overline{F_\Sigma} : K\ell(\mathcal{P}) \to K\ell(\mathcal{P})$ by $\overline{F_\Sigma}X := X$ for $X \in K\ell(\mathcal{P})$ and $\overline{F_\Sigma}f(a, x_1, \dots, x_n) := \{(a, y_1, \dots, y_n) \mid y_i \in f(x_i)\}$ for $f : X \to Y$. It is easy to see that $\overline{F_\Sigma}$ is a lifting of $F_\Sigma$. Then we have:

1. $\mathcal{P}$ and $F_\Sigma$ constitute a Büchi trace situation (Def. 2.13) with respect to $\sqsubseteq$ and $\overline{F_\Sigma}$.

2. The carrier set of the final $F_\Sigma$-coalgebra is isomorphic to $\text{Tree}_\infty(\Sigma)$.

3. For an NBTA $\mathcal{A} = (X, \Sigma, \delta, \text{Acc})$, we define a Büchi $(\mathcal{P}, F_\Sigma)$-system $(c : X \to \overline{F_\Sigma}X, (X_1, X_2))$ by $c := \delta, X_1 := X \setminus \text{Acc}$ and $X_2 := \text{Acc}$. Then we have: $[\text{tr}_1^\mathcal{B}(c), \text{tr}_2^\mathcal{B}(c)] = L_\mathcal{A}^\mathcal{B} : X \to \mathcal{P}\text{Tree}_\infty(\Sigma)$. $\square$

In the rest of this section, for an NBTA $\mathcal{A} = (X, \Sigma, \delta, \text{Acc})$ modeled as a $(\mathcal{P}, F_\Sigma)$-system $(c : X \to \mathcal{P}F_\Sigma X, (X_1, X_2))$, we describe $\text{dtr}_i(c)$ and show the relationship with $\text{tr}_i^\mathcal{B}(c)$ using Thm. 4.3.

We first describe datatypes $F_\Sigma^+(F_\Sigma^{\oplus 0})$ and $F_\Sigma^{\oplus 0}$ referring to the construction of a final coalgebra in Thm. 2.5. We can easily see that $F_\Sigma^+ A \cong \text{Tree}_\text{fin}^+(\Sigma, A) := \text{Tree}_\text{fin}(\Sigma+A) \setminus \{(x) \mid x \in A\}$. Hence for each $i \in \omega$, by a similar characterization to Ex. 3.3, we have:

$$ (F_{\Sigma}^{+}(- + 0))^i \cong \underbrace{\text{Tree}_{\text{fin}}^{+}(\Sigma, \text{Tree}_{\text{fin}}^{+}(\Sigma, \dots, \text{Tree}_{\text{fin}}^{+}(\Sigma, \{*\}) \dots))}_{i} \cong \left\{ \xi \in \text{Tree}_{\text{fin}}(\Sigma \times \{\bigcirc, \bigcirc\} \mid \begin{array}{l} \text{the root node is labeled by } \bigcirc, \text{ and for each branch} \\ \text{whose last component is } *, \text{ } \bigcirc \text{ appears exactly } i\text{-times} \end{array} \right\}. $$

Therefore $F_\Sigma^{+\oplus 0}$, a limit of the above sequence by Thm. 2.5, and $F_\Sigma^+(F_\Sigma^{\oplus 0})$ are characterized as follows:

**Proposition 5.7** We define $\text{AccTree}_i(\Sigma) \subseteq \text{Tree}_\infty(\Sigma \times \{\bigcirc, \bigcirc\})$ by:

$$ \text{AccTree}_i(\Sigma) := \left\{ \xi \in \text{Tree}_\infty(\Sigma \times \{\bigcirc, \bigcirc\} \mid \begin{array}{l} \text{the root node is labeled by } \bullet, \text{ and for each} \\ \text{infinite branch } \bigcirc \text{ appears infinitely often} \end{array} \right\}. $$

where $i \in \{1, 2\}$ and $\bullet$ is $\bigcirc$ if $i=1$ and $\bigcirc$ if $i=2$. Then $\text{AccTree}_1(\Sigma) \cong F_\Sigma^+(F_\Sigma^{\oplus 0})$ and $\text{AccTree}_2(\Sigma, A) \cong F_\Sigma^{\oplus 0}$. $\square$

We now show what $\text{dtr}_i(c)$ characterizes for an NBTA with respect to the characterization in Prop. 5.7. Firstly, Asm. 4.1 in the previous section is satisfied.

**Proposition 5.8** Asm. 4.1 is satisfied by $(T, F) = (\mathcal{P}, F_\Sigma)$. $\square$

By Prop. 5.7, for $i \in \{1, 2\}$, $\beta_{i0}$ (see Def. 3.4) has a type

$$ \beta_{i0} : \text{AccTree}_i(\Sigma) \to \coprod_{n \in \omega} \Sigma_n \times (\text{AccTree}_1(\Sigma) + \text{AccTree}_2(\Sigma)), $$

and is given by $\beta_i A(\xi) = (a, \xi_0, \dots, \xi_{n-1})$ if the root of $\xi$ is labeled by $(a, \bullet) \in \Sigma_n \times \{\bigcirc, \bigcirc\}$. Using this, we can show the following characterization of $\text{dtr}_i(c)$.
**Proposition 5.9** Let $\mathcal{A} = (X, \Sigma, \delta, \text{Acc})$ be an NBTA. We define $\Omega: \text{Run}(X) \to \text{Tree}_{\infty}(\Sigma \times \{\emptyset, \emptyset\})$ by $\Omega(D, l) := (D, l')$ where for $w \in D$ s.t. $l(w) = (a, x)$, $l'(w) := (a, \emptyset)$ if $x \notin \text{Acc}$ and $(a, \emptyset)$ if $x \in \text{Acc}$. We define a Büchi $(\mathcal{P}, F_{\Sigma})$-system $(c: X \to \overline{F}_{\Sigma}X, (X_1, X_2))$ as in Prop. 5.6.3. Then for $i \in [1, 2n]$ and $x \in X_i$,

$$ \mathrm{dtr}_i(c)(x) = \{\Omega(\rho) \in \mathrm{AccTree}_i(\Sigma) \mid \rho \in \mathrm{AccRun}_A(x)\}. \quad \square $$

We conclude this section by instantiating $p_{iA}^{(2)}$ (Def. 3.8) for NBTAs.

**Proposition 5.10** We overload DelSt and define DelSt: $\text{AccTree}_1(\Sigma) + \text{AccTree}_2(\Sigma) \to \text{Tree}_{\infty}(\Sigma)$ by $\text{DelSt}(D, l) := (D, l')$ where $l'(w) := \pi_1(l(w))$. Then with respect to the isomorphism in Prop. 5.7, $\text{DelSt}(\xi) = p_{iA}^{(2)}(\xi)$ for each $i \in \{1, 2\}$ and $\xi \in \text{AccTree}_i(\Sigma)$. $\square$

Hence Thm. 4.3 results in the following (obvious) equation for NBTAs:

$$ \{\text{DelSt}(\Omega(\rho)) \mid \rho \in \text{AccRun}_{\mathcal{A}}(x)\} = L_{\mathcal{A}}^{\text{B}}(x). $$

# 6 Systems with Other Branching Types

In this section we briefly discuss other monads than $T = \mathcal{P}$. As we have discussed in §3.3, the framework does not apply to $T = \mathcal{D}$.

Let $T = \mathcal{L}$ and $F = F_{\Sigma}$. A Büchi $(\mathcal{L}, F_{\Sigma})$-system $(c: X \to \overline{F}_{\Sigma}X, (X_1, \dots, X_{2n}))$ is understood as a $\Sigma$-labeled deterministic Büchi tree automaton with an exception. In a similar manner to $T = \mathcal{P}$ we can prove that they satisfy Asm. 4.1. The resulting decorated trace semantics has a type $\mathrm{dtr}_i(c): X_i \to \{\perp\} + \text{AccTree}_i(\Sigma)$. Note that once $x \in X$ is fixed, either of the following occurs: a decorated tree is determined according to $c$; or $\perp$ is reached at some point. The function $\mathrm{dtr}_i(c)$ assigns $\perp$ to $x \in X_i$ if and only if $\perp$ is encountered from $x$ or the resulting decorated tree does not satisfy the Büchi condition: otherwise, the generated tree is assigned to $x$. See §E.1 of the extended version [20] for detailed discussions, which includes the case of parity automata.

We next let $T = \mathcal{G}$. A Büchi $(\mathcal{G}, F_{\Sigma})$-system is understood as a probabilistic Büchi tree automaton. In fact, it is open if $T = \mathcal{G}$ and $F = F_{\Sigma}$ satisfy Asm. 4.1. The challenging part is the gfp-preserving condition (Asm. 4.1.4). However, by carefully checking the proofs of the lemmas and the propositions where the gfp-preserving condition is used (i.e. Prop. 3.14, Lem. 4.5 and Prop. 4.7), we can show that Asm. 4.1.4 can be relaxed to the following weaker but more complicated conditions:

4'-1. $T$ and $F^+(\_ + A)$ satisfy the gfp-preserving condition with respect to $\overline{F^+}(F^{+\oplus}B_+ + A) \xrightarrow{\overline{F_i^+}(\mathrm{id}+f)} \overline{F^+}(F^{+\oplus}B + B) \xrightarrow{J(\zeta_B^{F^+})^{-1}} F^{+\oplus}B$ for each $f: A \to B$;

4'-2. $T$ and $F^+(\_ + A)$ satisfy the gfp-preserving condition with respect to an algebra $F^+(F^{+\oplus}A + A) \xrightarrow{J_{\tau}} F^+(F^{+\oplus}A + A) \xrightarrow{J(\zeta_A^{F^{+\oplus}})^{-1}} F^{+\oplus}A$ where $\tau$ is the unique homomorphism from $(\iota_{F^{+\oplus}A+A})^{-1}$ to $\zeta_{F^{+\oplus}A+A}^F$; and
4'-3. $T$ and $F(_ + A)$ satisfy the gfp-preserving condition with respect to an algebra $F(F^{\oplus}A + F^{\oplus}A + A) \xrightarrow[+]{JF([id,id]+id)} F(F^{\oplus}A + A) \xrightarrow[\downarrow]{J(\zeta_A^F)^{-1}} F^{\oplus}A$.

In fact, only the first condition is sufficient to prove Prop. 3.14 and Lem. 4.5.

We can show that $T = \mathcal{G}$ and $F = F_\Sigma$ on **Meas** satisfy the above weakened gfp-preserving condition, and hence we can consider a decorated trace semantics $dtr_i(c)$ for a Büchi ($\mathcal{G}, F_\Sigma$)-system ($c: X \to \overline{F_\Sigma}X, (X_1, X_2)$) and use Thm. 4.3.

Assume $X$ is a countable set equipped with a discrete $\sigma$-algebra for simplicity. Then the resulting decorated trace semantics $dtr_i(c)$ has a type $X_i \to \mathcal{G}(\mathrm{AccTree}_i(\Sigma), \mathcal{F}_{\mathrm{AccTree}_i(\Sigma)})$ where $\mathcal{F}_{\mathrm{AccTree}_i(\Sigma)}$ is the standard $\sigma$-algebra generated by cylinders. The probability measure assigned to $x \in X_i$ by $dtr_i(c)$ is defined in a similar manner to the probability measure over the set of run trees generated by a probabilistic Büchi tree automaton (see e.g. [18]).

The situation is similar for parity $(\mathcal{G}, F_\Sigma)$-systems. See [20, §E.2] for details.

# 7 Conclusions and Future Work

We have introduced a categorical data type for capturing behavior of systems with Büchi acceptance conditions. The data type was defined as an alternating fixed point of a functor, which is understood as the set of traces decorated with priorities. We then defined a notion of coalgebraic decorated trace semantics, and compared it with the coalgebraic trace semantics in [21]. We have applied our framework for nondeterministic Büchi tree automata, and showed that decorated trace semantics is concretized to a function that assigns a set of trees decorated with priorities so that the Büchi condition is satisfied in every branch. We have focused on the Büchi acceptance condition for simplicity, but all the results can be extended to the parity acceptance condition (see §A of [20] for the details).

**Future Work** There are some directions for future work. In this paper we focused on systems with a simple branching type like nondeterministic or probabilistic. Extending this so that we can deal with systems with more complicated branching type like *two-player games* (systems with two kinds of nondeterministic branching) or *Markov decision processes* (systems with both nondeterministic and probabilistic branching) is a possible direction of future work.

Another direction would be to use the framework developed here to categorically generalize a verification method. For example, using the framework of coalgebraic trace semantics in [21], a simulation notion for Büchi automata is generalized in [19]. Searching for an existing verification method that we can successfully generalize in our framework would be interesting.

Finally, it was left open in §6 if Asm. 4.1.4 is satisfied by $T = \mathcal{G}$ and $F = F_\Sigma$. Investigating this is clearly a future work.

**Acknowledgments** We thank Kenta Cho, Shin'ya Katsumata and the anonymous referees for useful comments. The authors are supported by JST ERATO
HASUO Metamathematics for Systems Design Project (No. JPMJER1603), and
JSPS KAKENHI Grant Numbers 15KT0012 & 15K11984. Natsuki Urabe is sup-
ported by JSPS KAKENHI Grant Number 16J08157.

References

1. Adámek, J., Koubek, V.: Least fixed point of a functor. J. Comput. Syst. Sci. 19(2), 163–178 (1979), http://dx.doi.org/10.1016/0022-0000(79)90026-6

2. Adámek, J., Milius, S., Moss, L.S.: Fixed points of functors. Journal of Logical and Algebraic Methods in Programming 95, 41 – 81 (2018)

3. Arnold, A., Niwiński, D.: Rudiments of µ-Calculus. Studies in Logic and the Foundations of Mathematics, Elsevier, Amsterdam (2001)

4. Borceux, F.: Handbook of Categorical Algebra, Encyclopedia of Mathematics and its Applications, vol. 1. Cambridge University Press (1994)

5. Ciancia, V., Venema, Y.: Stream automata are coalgebras. In: Proc. CMCS 2012. Lecture Notes in Computer Science, vol. 7399, pp. 90–108. Springer (2012)

6. Cleaveland, R., Klein, M., Steffen, B.: Faster model checking for the modal mu-calculus. In: Proc. CAV '92. LNCS, vol. 663, pp. 410–422. Springer (1992)

7. Courcelle, B.: Fundamental properties of infinite trees. Theor. Comput. Sci. 25, 95–169 (1983), https://doi.org/10.1016/0304-3975(83)90059-2

8. Etessami, K., Wilke, T., Schuller, R.A.: Fair simulation relations, parity games, and state space reduction for Büchi automata. SICOMP 34(5), 1159–1175 (2005)

9. Ghani, N., Hancock, P., Pattinson, D.: Representations of stream processors using nested fixed points. Logical Methods in Computer Science 5(3) (2009)

10. Hasuo, I., Jacobs, B.: Context-free languages via coalgebraic trace semantics. In: Proc. CALCO 2005. LNCS, vol. 3629, pp. 213–231. Springer (2005)

11. Hasuo, I., Jacobs, B., Sokolova, A.: Generic trace semantics via coinduction. Logical Methods in Computer Science 3(4) (2007)

12. Jacobs, B.: Trace semantics for coalgebras. Electr. Notes Theor. Comput. Sci. 106, 167–184 (2004), http://dx.doi.org/10.1016/j.entcs.2004.02.031

13. Jacobs, B.: Introduction to Coalgebra: Towards Mathematics of States and Observation. Cambridge Tracts in Theoret. Comp. Sci., Cambridge Univ. Press (2016)

14. Milius, S.: Completely iterative algebras and completely iterative monads. Information and Computation 196(1), 1 – 41 (2005)

15. Mulry, P.S.: Lifting theorems for Kleisli categories. In: Proc. MFPS IX. Lecture Notes in Computer Science, vol. 802, pp. 304–319. Springer (1993)

16. Power, J., Turi, D.: A coalgebraic foundation for linear time semantics. Electr. Notes Theor. Comput. Sci. 29, 259–274 (1999)

17. Thomas, W.: Languages, Automata, and Logic, pp. 389–455. Springer Berlin Heidelberg, Berlin, Heidelberg (1997)

18. Urabe, N., Hasuo, I.: Coalgebraic infinite traces and Kleisli simulations. CoRR abs/1505.06819 (2015), http://arxiv.org/abs/1505.06819

19. Urabe, N., Hasuo, I.: Fair Simulation for Nondeterministic and Probabilistic Buechi Automata: a Coalgebraic Perspective. LMCS vol. 13, iss. 3 (2017)

20. Urabe, N., Hasuo, I.: Categorical Büchi and parity conditions via alternating fixed points of functors. arXiv preprint (2018)

21. Urabe, N., Shimizu, S., Hasuo, I.: Coalgebraic trace semantics for Büchi and parity automata. In: Proc. CONCUR 2016. LIPIcs, vol. 59, pp. 24:1–24:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)