Lattice-Theoretic Progress Measures
and Coalgebraic Model Checking
Ichiro Hasuo

Shunsuke Shimizu

Corina Cı̂rstea

arXiv:1511.00346v3 [cs.LO] 9 Jan 2016

University of Tokyo, Japan
{ichiro,shunsuke}@is.s.u-tokyo.ac.jp

University of Southampton, UK
cc2@ecs.soton.ac.uk

Abstract

(see e.g. [7, 39]) provides a clean syntax that incorporates the least
and greatest fixed-point operators (µ and ν) in a systematic manner.
Dealing with such fixed points is however a nontrivial task—
this is especially the case when µ’s and ν’s are nested and they
alternate. Many engineers find it challenging to express their intuition as a fixed-point formula; furthermore, many algorithms are
first introduced for an alternation-free fragment and then later extended to the full fragment (see e.g. [18] and [19]).
For the purpose of analyses of fixed-point logics and designing
algorithms for them, parity games have emerged as a very useful
tool in the last decade or so. A parity game is played by two players
even and odd, on a board each position x of which has a natural
number pr(x) ∈ ω called its priority. Notably its winning condition
is the parity condition: the player even wins if the largest priority
that occurs infinitely often in a given play (an infinite sequence of
positions) is an even number. This condition—that may seem adhoc at first sight—turns out to be extremely useful for modeling
nested and alternating µ’s and ν’s. It is in a sense a combinatorial
presentation of an alternation between µ’s and ν’s.
The use of parity games has been boosted further by Jurdzinski’s algorithm that efficiently determines the winner at each position of a parity game [33]. It exhibits a practical complexity that is
exponential only in so-called the alternation depth of a parity game.
It has then become a norm, in the context of fixed-point logics and
algorithmic formal verification, to take the following parity-game
workflow: it reduces a problem in question to the decision problem
of some parity game, and then solves the latter by Jurdzinski’s algorithm. A notable example is the model-checking problem for the
modal µ-calculus (see e.g. [60]).
The key ingredient of Jurdzinski’s algorithm is what is called a
progress measure (a notion originally from [35])—it can be understood as an extension of a ranking function (used e.g. for termination proofs) to a setting with nested µ’s and ν’s.

In the context of formal verification in general and model checking in particular, parity games serve as a mighty vehicle: many
problems are encoded as parity games, which are then solved by
the seminal algorithm by Jurdzinski. In this paper we identify the
essence of this workflow to be the notion of progress measure, and
formalize it in general, possibly infinitary, lattice-theoretic terms.
Our view on progress measures is that they are to nested/alternating
fixed points what invariants are to safety/greatest fixed points, and
what ranking functions are to liveness/least fixed points. That is,
progress measures are combination of the latter two notions (invariant and ranking function) that have been extensively studied in
the context of (program) verification.
We then apply our theory of progress measures to a general
model-checking framework, where systems are categorically presented as coalgebras. The framework’s theoretical robustness is
witnessed by a smooth transfer from the branching-time setting to
the linear-time one. Although the framework can be used to derive
some decision procedures for finite settings, we also expect the proposed framework to form a basis for sound proof methods for some
undecidable/infinitary problems.
Categories and Subject Descriptors D.2.4 [Software/Program
Verification]: Model checking; F.4.1 [Mathematical Logic]: Modal
logic
Keywords fixed-point logic, model checking, coalgebra

1.

Introduction

1.1

Backgrounds

Parity Games and Fixed-Point Logics For the purpose of formal
verification where one aims at establishing that a system satisfies a
certain property (called a specification), it is common to express:
a model of the system as a state-based transition system such
as an automaton or a Kripke structure; and a specification as a
formula in some modal logic. For the latter, in particular, logics
with fixed-point operators—such as LTL and CTL—serve well
thanks to their remarkable expressivity [50]. The modal µ-calculus

Coalgebras and Coalgebraic Modal Logics On the other side
of formal verification (namely system models), coalgebra has attracted attention as a categorical abstraction of state-based systems [31, 52] for more than a decade. An F -coalgebra is an arrow c : X → F X in some category C, where F : C → C is an
endofunctor. By changing C and F a coalgebra instantiates to a variety of transition systems, such as Kripke structures, LTSs, Markov
chains, tree automata, processes in the π-calculus, and so on. Abstracting away from specific choices of C and F allows us to develop a uniform theory that applies to various systems. One notable
success is a uniform definition of bisimulation that is independent
from C and F . See [31, 52].
Along with the development of the theory of coalgebras, coalgebraic modal logics have been developed as languages suited for
specifying about coalgebras (see e.g. [17]). Besides the approaches
with Moss’ cover modality [42] and Stone-like dualities [6], the one

[Copyright notice will appear here once ’preprint’ option is removed.]

1

2016/1/12

properties
safety, gfp
liveness, lfp
nested gfp’s
and lfp’s

witnessed by
invariants
ranking functions
winning strategies for parity games (if finitary),
and progress measures (in general)

widespread, in quantitative verification, program verification, and
so on—by model checking and deductive methods alike.
Progress Measure for Coalgebraic µ-Calculus Model Checking
We apply the notion of progress measure to model checking of a
coalgebraic modal µ-calculus CµΓ,Λ . Specifically, given a coalgebra c : X → F X (as a system model), a CµΓ,Λ -formula ϕ (as
a specification) and the domain Ω of truth values, we characterize the semantics JϕKc : X → Ω of ϕ over c in terms of progress
measures. Unlike the original definition of the semantics JϕKc (that
is highly nonlocal due to fixed-point operators), it can be checked
locally whether given data constitute a progress measure.
The lattice-theoretic generality of our progress measure allows:
a state space X that is infinite; a domain Ω of truth values that is
other than 2 = {tt, ff} (such as the unit interval [0, 1]); and so
on. Furthermore, for its finitary special case, we derive a modelchecking algorithm that is based on progress measures.
We expect our theoretical framework (general, possibly infinitary, in §4.1) to be a foundation on which various verification
techniques—a candidate being an extension of the simulationbased method in [56]—can be formulated and proved sound.
Besides, our generic model-checking algorithm (in §4.2, as a
finitary special case of the framework in §4.1) is a uniform algorithm that works for a variety of endofunctors F and modalities
over F (normal modal logic over Kripke models, neighborhood
frames, graded modal logic, coalition logic, and so on; see Example 3.3). Moreover, thanks to its concrete presentation with matrices, our algorithm should be easy to implement.
Currently it is not clear whether our algorithm in §4.2 competes
with tailor-developed ones for a specific modal logic. However we
believe our generic algorithm is at least worthwhile—much like a
big part of the coalgebraic attempts towards abstraction and genericity, see §1—for the following reasons: 1) among the examples
covered by our generic algorithm, not all enjoy tailor-developed algorithms; and 2) we believe our algorithm, though currently basic,
can expose further “handles” for optimization. The latter means:
in many parity game-based algorithms, the part of solving parity
games is left as a blackbox; and in principle opening up a blackbox
(like we do) should be good for optimization, possibly allowing for
“shortcut fusion”-like optimization.

Table 1. Progress measures = (invariants + ranking functions)
with predicate liftings [46] is widely adopted in the literature. The
theory has since produced many uniform results about coalgebraic
modal logics as specification languages. They are on: expressivity (i.e. that bisimilarity is captured) [36, 46]; sound and complete
axiomatizations [46, 53]; satisfiability complexity [53]; cut elimination and interpolation [47, 48]; and so on.
Fixed-point operators in coalgebraic modal logics have been
actively studied too. See e.g. [12, 13, 16, 29, 53, 54], and also [24,
59] where coalgebraic automata are studied as translations of µcalculus formulas. In particular, in [16], algorithms for the modelchecking and satisfiability problems of a coalgebraic µ-calculus are
presented. These algorithms reduce the problems to parity games—
this follows the common parity-game workflow that we already
discussed. For satisfiability they also need a tableau system devised
for this purpose.
1.2

Contributions

In this paper we scrutinize the aforementioned parity-game workflow of: reducing to a parity game, and solving by Jurdzinski’s algorithm. We identify its essence in progress measures—a key notion in Jurdzinski’s algorithm [33]—rather than in parity games
themselves. This leads us to a lattice-theoretic transfinite notion
of progress measure that works without any finiteness assumption,
a restriction that is inevitable in the combinatorial notion of parity game. We then go on to develop a generic (and not necessarily
finitary) framework for model checking, where system models and
specifications also have generic presentations in the language of
coalgebras and coalgebraic modal logics.
More specifically, our technical contributions are as follows.
Lattice-Theoretic Progress Measure Taking an arbitrary complete lattice L as a value domain (instead of a finite power 2m of
2 = {tt, ff}), we present a lattice-theoretic characterization of solutions of recursive equations with (nested and alternating) greatest
and least fixed-points. The characterization is by the notions of prioritized ordinal and progress measure—notions that are essentially
generalization of what are in Jurdzinski’s work [33]. Our general
formalization allows one to use progress measures also in infinitary settings where we deal with infinite-state systems, quantitative
verification (i.e. the set of truth values is infinite), or both.
One can also think of our progress measure as the combination
of the common proof methods by: invariants for safety/gfp properties, and ranking functions for liveness/lfp properties (Table 1).
These methods have been extensively studied especially in the field
of program verification—where problems are inherently infinitary
due to the Integer datatype—with an emphasis on automatic synthesis of invariants and ranking functions (see e.g. recent [5, 25]).
Our current results therefore open the way to combining these automated synthesis techniques, and to obtaining automated proof
methods for nested lfp/gfp properties (like the response formula
G(p → Fq) but much, much more). Once done its impact will be
significant, since currently most automation attempts in the field
focus on only safety or liveness, and not their combination.
We note that these results (in §2) are formulated solely in
(rather elementary) lattice-theoretic terms, without any category
theory. While their principal use in the current paper is in coalgebraic model checking, their application areas are expected to be

Coalgebraic µ-Calculus as a Linear-Time Logic In order to further demonstrate the theoretical robustness of our framework, we
present an adaptation of the framework to linear-time model checking. In this case a system is a coalgebra c : X → PF X (with
additional nondeterministic branching represented by the powerset
monad P); and the question is whether there is an infinitary trace
z of c starting from x such that z satisfies a CµΓ,Λ -formula ϕ.
It turns out that the combination with coalgebraic theory of
traces and simulations (developed e.g. in [27, 30, 57]) allows a
smooth transfer from the previous “branching-time” setting to the
current linear-time one. The outcome is a uniform treatment of
branching and (nondeterministic) linear-time logics—which does
not seem to be achieved before despite the obvious efforts by the
coalgebra community. This venture also needs a technical piece,
namely the “pumping”-like result (Thm. 5.7) by Zorn’s lemma.
Our technical contributions are: a progress measure-based characterization of linear-time model checking (where, again, whether
given data is a valid progress measure or not can be checked locally); and a decision procedure for linear-time model checking
(with the restriction that the state space X is finite and the truth
values are Boolean). The former solves the challenge, presented
in [14], of a local characterization of linear-time semantics (called
“step-wise semantics” in [14]) for coalgebraic fixed-point logics.

2

2016/1/12

1.3

1.4

Future Work

Notations

Throughout the paper, the domain of truth values is denoted by Ω
and is assumed to be a complete lattice, with itsF
order denoted
by
d
v, and its supremums and infimums denoted by and . Typical
examples of Ω are the set 2 = {tt, ff} of Boolean truth values,
and the unit interval [0, 1] for a quantitative notion of truth. In §2
we will use another complete lattice L; this will be instantiated by
L = ΩX —where X is the state space of the system in question—
for the use in later sections. Since Ω is a complete lattice, any
monotonic endofunction f on Ω has the greatest and least fixed
points νf, µf . The same holds for L in place of Ω.
We fix a countable set Var of (fixed-point) variables. It is
ranged by u, v, w, . . . . We let η designate fixed-point operators in
general; it is either µ or ν. Confusion with a monad unit is unlikely.
The set of natural numbers is identified with the smallest infinite
ordinal and denoted by ω.

There are a lot of further topics to study in our current venture
to coalgebraic µ-calculus. They include: implementation of our
model-checking algorithms in §4.2 and §5.4 (the one in §4.2 should
especially be easy because of the presentation by matrices); experiments, comparison with tailor-made algorithms and further optimization; satisfiability and small-model property; universal lineartime model checking (in this paper we study the existential one);
synthesis; and CµΓ,Λ as linear-time logic for systems with probabilistic branching. In particular we expect the last to be not hard,
given the lattice-theoretic generality of the current results. It should
also help that the coalgebraic theory of traces and simulations has
been recently extended to the probabilistic setting [11, 57] (using
the Giry monad over the category of measurable spaces). We can
say we understand the mathematical structures therein fairly well:
these studies suggest that the probabilistic setting is better-behaved
than the nondeterministic setting, from a coalgebraic point of view.
See [57] for further details.
Besides, our lattice-theoretic theory of nested fixed points allows progress measures (which we identify as the essence of parity
games) to be applied to infinitary settings. We believe it will be
useful for the following purposes. Working out these further applications is future work.

1.5

Organization of the Paper

In §2 we present our lattice-theoretic notion of progress measure
and prove that it characterizes the solution of a system of fixedpoint equations. In §3 we introduce our logic CµΓ,Λ —it is a
coalgebraic modal logic with both greatest and least fixed-point
operators (ν, µ); it is parametrized not only by the set Λ of predicate
liftings (i.e. modalities) for a functor F , but also by the set Γ of
propositional connectives. In §4 we adapt progress measures in §2
to the purpose of CµΓ,Λ model checking (against F -coalgebras),
derive a model-checking algorithm and analyze its complexity.
This framework is further adapted in §5 to (existential) linear-time
model checking—where a system has additional nondeterministic
branching. We present a decision procedure there.
Omitted proofs are found in Appendix B.

Establishing an Alternating Fixed-Point in Theorem Proving In
an infinitary setting (such as the state space |X| and/or the truth
domain Ω are infinite), the search space for our (infinitary) progress
measures will be infinite, and hence is not amenable to algorithmic
search. Even so, one could resort to human ingenuity to find one.
An advantage of a progress measure-based characterization of
the semantics JϕKc is, as we mentioned earlier, the validity of
a progress measure can be checked locally in a straightforward
manner. This is unlike the original definition of the semantics
JϕKc (see Def. 3.7) that involves highly nonlocal information like
V : X → Ω. We believe this advantage will be especially useful
when one works with fixed-point specifications in a proof assistant.
Due to the same advantage, our progress measure-based characterization might also form a basis of sound (but not necessarily
complete) model-checking algorithms that rely e.g. on mathematical programming. This is much like in [56] where Kleisli simulations (whose existence is checked by linear programming and
hence is PTIME) give a sound proof method for weighted language
inclusion (an undecidable property).

2.

Progress Measures for Equational Systems

2.1

Prelude: (Unnested) Fixed Points, Invariants and
Ranking Functions

In general, there are two different ways for characterizing (not
nested) least/greatest fixed points (lfp’s and gfp’s). The first is the
Knaster-Tarski one: the lfp is the least prefixed point; and the gfp
is the greatest postfixed point. The second is the Cousot-Cousot
one [20]: the lfp µf of a monotone function f : L → L over a
complete lattice L is the (possibly transfinite) supremum of the
chain ⊥ v f (⊥) v f 2 (⊥) v · · · ; similarly the gfp νf is
the infimum of > w f (>) w · · · . Sometimes these chains are
guaranteed to stabilize after ω steps, for example when f satisfies
suitable continuity conditions (the Kleene fixed-point theorem).
In this paper our principal interests will be finding lower bounds
for fixed points; see Rem. 2.9 for system verification motivations.
Among the last four characterizations (Knaster-Tarski and CousotCousot, for each of lfp and gfp), what are suited for this purpose
of ours are: the Cousot-Cousot one for lfp’s; and the KnasterTarski one for gfp’s (the other two only give us upper bounds).
We explicitly note this fact for the record:

As a Tool in a Meta-Theory In higher-order model checking
(see e.g. [37, 45, 55]), a higher-order recursion scheme (HORS)
generates an infinite tree that is then model-checked against a
modal µ-formula. The generated tree is in general irrational—
hence cannot be identified with a finite-state automaton. However
it is shown [37, 45] that the model-checking is decidable; an algorithm operates directly with the HORS that generates the tree, but
not with the tree itself. In this setting (and similar ones), we expect
our infinitary progress measure to be a useful tool on the level of
meta-theory, e.g. for showing the correctness of an algorithm.
We also envisage the use of our current results in lifting
(bi)simulation notions for Büchi and parity automata (see e.g. [22])
to the coalgebraic level of abstraction and generality. In this direction we have obtained some preliminary results that characterize
the accepted languages of Büchi/parity automata via coalgebras in
a Kleisli category—results that will hopefully enable us to extend
our coalgebraic theory of traces and simulations in [27, 30, 57] to
Büchi/parity acceptance conditions. We also intend to study the
relationship between our current work and quantitative extensions
of parity games, a topic of extensive research efforts [8, 9].

Lemma 2.1 (lower bounds for fixed points). Let L be a complete
lattice and f : L → L be a monotone function.
1. For each ordinal α we have f α (⊥) v µf . Here f α (⊥) is
defined by obvious induction: f α+1F
(⊥) = f (f α (⊥)) for a
β
successor ordinal; and f α (⊥) =
β<α f (⊥) for a limit
ordinal.
2. For any l ∈ L, l v f (l) implies l v νf .
We emphasize that this simple theoretical observation is what
underlies the difference between the common proof methods for
safety/gfp properties and for liveness/lfp properties (Table 1). For

3

2016/1/12

the former (gfp’s) one would seek for an invariant, that is, a postfixed point l such that l v f (l). For the latter (lfp’s) one would
typically synthesize a ranking function, an ω-valued function that
strictly decreases in each step. We formulate—also for the sake of
some intuitions—the general principle behind the latter, focusing
on L = 2X .

termined parameters. The interim solution of the leftmost equation
(for u1 , in terms of u2 , . . . , um ) is then used in the second equation u2 =η2 f2 (u1 , . . . , um ) to eliminate the occurrences of u1
in its right-hand side. We continue this way; then solving the last
(rightmost) equation would give us a closed (i.e. without any variables occurring in it) solution for um . Such closed solutions are
then propagated from right to left in (1), finally giving a closed solution to each variable ui .
The above intuitions can be put in the following precise terms.

Definition 2.2. Let f : 2X → 2X be a monotone function. A
ranking function for f is an ordinal- (or ♠, indicating “failure”)
valued function rk : X → Ord q {♠} such that: 1) rk(x) 6= 0 for
each x ∈ X;2) for each ordinal α, {x | rk(x) ≤ α + 1} ⊆ f {x |
rk(x) ≤ α} ; and 3) for each limit ordinal α, {x | rk(x) ≤ α} =
S
β<α {x | rk(x) ≤ β}.

Definition 2.7 (solution). The solution of an equational system (1)
is defined as follows. For each i ∈ [1, m] and j ∈ [1, i], we define
monotone functions
fi‡ : Lm−i+1 → L and

Example 2.3. Assume that X is equipped with a transition relation
R ⊆ X × X and we are interested in reachability to a subset
U ⊆ X. We would then define f by: f (X 0 ) := U ∪ {x |
∃x0 . xRx0 ∧x0 ∈ X 0 }; this yields f α (⊥) to be the set of states from
which U is reachable within α − 1 steps. A prototypical ranking
function is given by rk(x) := (the distance from x to U ) + 1.

as follows, inductively on i. For the base case i = 1:
f1‡ (l1 , . . . , lm ) := f1 (l1 , . . . , lm ),


(1)
l1 (l2 , . . . , lm ) := η1 f1‡ ( , l2 , . . . , lm ) : L → L .
In the last line we take the lfp or gfp (according to η1 ∈ {µ, ν}) of
the (monotone) function f1‡ ( , l2 , . . . , lm ) : L → L.
‡
For the step case, the function fi+1
makes use of the i-th interim
(i)
(i)
solutions l1 , . . . , li for the variables u1 , . . . , ui obtained so far:

Lemma 2.4. In Def. 2.2, a ranking function rk for f witnesses µf ,
the least fixed point of f . That is, rk(x) 6= ♠ implies x ∈ µf .
Proof. The following is easily shown by induction on an ordinal
α: for any x ∈ X such that rk(x) = α, we have x ∈ f α (⊥). The
claim then follows from Lem. 2.1.1.

‡
fi+1
(li+1 , . . . , lm ) :=

Remark 2.5. Implicit in the above is a bijective correspondence—
not unlike in Stone-like dualities—between:


(i)
(i)
fi+1 l1 (li+1 , . . . , lm ), . . . , li (li+1 , . . . , lm ), li+1 , . . . , lm .
We then let

• a ranking function rk : X → Ord q {♠}; and
• an approximating sequence U0 ⊆ U1 ⊆ · · · such that: 1)
S

U0 = ⊥ = ∅, 2) Uα+1 ⊆ f (Uα ), and 3) Uα =
for any limit ordinal α.

β<α

 ‡

(i+1)
li+1 (li+2 , . . . , lm ) := ηi+1 fi+1
( , li+2 , . . . , lm ) : L → L

Uβ

(i+1)

and use it to obtain the (i+1)-th interim solutions l1
That is, for each j ∈ [1, i],

From the former to the latter we let Uα := {x | rk(x) ≤ α};
conversely we let rk(x) := inf{α | x ∈ Uα }.
2.2

(i+1)

, . . . , li

.


(i+1)
li+1 (li+2 , . . . , lm ), li+2 , . . . , lm
(2)
sol
Finally, the solution (l1sol , . . . , lm
) ∈ Lm of the equational sys(m)
(m)
sol
tem (1) is defined by (l1sol , . . . , lm
) := (l1 , . . . , lm ), where
(m)
we identify a function lj : 1 → L with an element of L.
(i)
It is easy to see that all the functions fi‡ and lj involved here
are monotone. That the solution uniquely exists is then guaranteed
by the Knaster-Tarski theorem.
(i+1)

lj

Equational Systems

With the preparations in §2.1 for unnested fixed points, we set out
to study nested and alternating ones. As a formalism of expressing
them we prefer equational systems, to the (probably more common)
modal µ-calculus-like notations. Here we shall follow the accounts
of similar notions in [19] and [2, §1.4].
Definition 2.6 (equational system). Let L be a complete lattice. An
equational system E over L is an expression of the form
u1 =η1 f1 (u1 , . . . , um ),

(i)

lj : Lm−i → L

(i)

(li+2 , . . . , lm ) := lj

Example 2.8. As a simple example, consider an equational system
u1 =µ u2 , u2 =ν u1 . Solving the first equation yields u1 = u2
(1)
(i.e. l1 (l2 ) = l2 ); using it to eliminate u1 in the second equation,
we obtain u2 =ν u2 (i.e. f2‡ (l2 ) = l2 ). We conclude u1 = u2 = >
is the solution.
It is not hard to see that, if we change the order of the equations,
the resulting system u2 =ν u1 , u1 =µ u2 has a different solution
u1 = u2 = ⊥.

...,

um =ηm fm (u1 , . . . , um )
(1)
where: u1 , . . . , um are variables, η1 , . . . , ηm ∈ {µ, ν}, and
f1 , . . . , fm : Lm → L are monotone functions.
A variable uj is said to be a µ-variable if ηj = µ; it is a νvariable if ηj = ν.
We say ui has a bigger priority than uj if j < i.

It is not hard to give a precise correspondence between equational systems and their modal µ-calculus-like presentations. Each
equation uj =ηj fj (u1 , . . . , um ) corresponds to a fixed-point formula ηj uj . fj (u1 , . . . , um ); since an equational system like (1) is
solved from left to right, the formula that corresponds to an equation on the left occurs inside the formula for an equation on the
right. For example, if m = 2, the equational

 system (1) is presented as η2 u2 . f2 η1 u1 . f1 (u1 , u2 ) , u2 . In the light of such
a correspondence to µ-calculus-like formulas, the definition of bigger/smaller priorities in Def. 2.6 coincides with what is customary
(an outside fixed-point operator has a bigger priority). A precise
translation can be defined following [19]; see also Def. 3.5 later, in
the special case of coalgebraic fixed-point logic.

Note that, in the last definition, we have been vague about the
distinction between a function fi as a semantical object and a
syntactic symbol that denotes it.
It is straightforward to generalize the definition and allow
different variables to take values in different complete lattices
L1 , . . . , Lm , and extend accordingly our technical developments
below. We assume L1 = · · · = Lm = L for ease of presentation.
The order of equations matters in an equational system like (1).1
Intuitively, the system (1) is solved starting from the leftmost equation, where the remaining variables u2 , . . . , um are left as unde1 Here

we follow the ordering convention in [2]. In [19] the order is reversed, and the rightmost equation is solved first.

4

2016/1/12

(see Example 2.11). We define (α1 , . . . , αk ) ≺i (α10 , . . . , αk0 )
if (αa , . . . , αk ) i (αa0 , . . . , αk0 ) holds but (αa , . . . , αk ) =i
(αa0 , . . . , αk0 ) fails.

Remark 2.9 (aiming at lower bounds). Assume that an equational
system E is given. For the purpose of system verification, one is
typically not so much interested in its solution itself, as in a suitable
lower bound of it. For a simple example consider the setting of
Example 2.3, and assume that X, R and U are given as follows.
···

/ x−2

/ x−1

/ x0 o

x1 o

x2 o

Example 2.11. Let us consider the following example E0 of an
equational system:

· · ·, U := {x0 }.
u1 =µ f1 (~
u),

A common question would be if U is reachable from a specific state
of our interest, say x3 . To verify it the ranking function

u3 =µ f3 (~
u),

u4 =µ f4 (~
u),

u5 =ν f5 (~
u),

where ~
u stands for u1 , . . . , u5 . A prioritized ordinal for this E0 is
a tuple (α1 , α2 , α3 ) of ordinals, where the ordinals α1 , α2 and α3
correspond to the µ-variables u1 , u3 and u4 , respectively.
It holds that (ω, 2, 2) 1 (0, 3, 2). To see that, since u1 is with
the smallest priority, we have to check (ω, 2, 2)  (0, 3, 2). This
holds; recall that  is the lexicographic order with the latter being
the more significant. We can similarly see that:

rk(x0 ) = 1, rk(xi ) = i + 1 for each i ≥ 1,
rk(xi ) = ♠ for each i < 0
suffices. This choice of a ranking function—while it gives a lower
bound {x0 , x1 , . . . } ⊆ µf of µf —does not witness e.g. x−3 ∈
µf (that actually holds). This is not a problem because we are
interested only in x3 .
This phenomenon (of only giving a lower bound) is the case
with verification algorithms in general: they conduct “directed”
searches from the states in question. Therefore in this paper we
focus on characterizing lower bounds of the solution of an equational system. Upper bounds, in contrast, are useful in refuting that
certain states have certain properties.
2.3

u2 =ν f2 (~
u),

(ω, 2, 2) ≺2 (0, 3, 2),
(ω, 2, 2) =4 (0, 3, 2),

(ω, 2, 2) ≺3 (0, 3, 2),
and

(ω, 2, 2) =5 (0, 3, 2).

Note here that the 3-, 4- and 5-truncations of (ω, 2, 2) and (0, 3, 2)
are: (2, 2) and (3, 2); (2) and (2); and () and (), respectively.
In the following definition, the element pi (α1 , . . . , αk ) ∈ L is
understood as the “(α1 , . . . , αk )-th approximation” of the solution
for the variable ui in the equational system (1).

Progress Measures

We shall now characterize lower bounds of (nested and alternating)
fixed points specified by an equational system. We use the technical
notion of progress measure; it is a lattice-theoretic generalization of
the notion of parity progress measure in [33], and hence is seen as a
generalization of winning strategies for parity games, too. Roughly
speaking, these are how one combines invariants (for gfp’s) and
ranking functions (for lfp’s, see Table 1 and §2.1) in an intricate
way so that priorities in alternation are respected.
Following Lem. 2.1 we approximate least fixed points by transfinite sequences starting from ⊥. In general there are multiple µvariables in an equational system—we have one “counter” for each
of them, and use their tuple that we call a prioritized ordinal. In
particular, the definition of the preorder i between prioritized
ordinals—derived from the one in [33] and defined for each variable ui —lies in the technical core.

Definition 2.12 (progress measure for an equational system). Assume the same setting as in Def. 2.10, with E being the equational
system (1) and i1 < · · · < ik enumerating the indices of all the
µ-variables.
A progress measure p for E is given by a tuple


p = (α1 , . . . , αk ), pi (α1 , . . . , αk ) i,α ,...,α
1

k

that consists of:
• the maximum prioritized ordinal (α1 , . . . , αk ); and
• the approximants pi (α1 , . . . , αk ) ∈ L, defined for each i ∈

[1, m] and each prioritized ordinal (α1 , . . . , αk ) such that α1 ≤
α1 , . . . , αk ≤ αk .
The approximants pi (α1 , . . . , αk ) are subject to:

Definition 2.10 (prioritized ordinal, i ). Let E be the equational
system in (1), over a complete lattice L. Let us collect all those
indices i ∈ [1, m] for which ui is a µ-variable in the equational
system E, and arrange them so that i1 < · · · < ik . That is,

1. (Monotonicity) Let i ∈ [1, m] (hence ui is either a µ- or νvariable). Then
(α1 , . . . , αk ) i (α10 , . . . , αk0 ) implies

{i1 , . . . , ik } = {i ∈ [1, m] | ηi = µ in (1)}.

pi (α1 , . . . , αk ) v pi (α10 , . . . , αk0 ).

Then a prioritized ordinal for E is a k-tuple (α1 , . . . , αk ) of
ordinals. Note that k is the number of µ-variables in E.
For each i ∈ [1, m] we define a preorder i between prioritized
ordinals—we call i the i-th truncated lexicographic order—as
follows. Let a ∈ [1, k] be such that

2. (µ-variables, base case) Let a ∈ [1, k]. Then αa = 0 implies pia (α1 , . . . , αa , . . . , αk ) = ⊥. (Note the correspondence
between: the subscript ia of pia ; and the counter αa that is assumed to be 0.)
3. (µ-variables, step case) Let a ∈ [1, k], and let (α1 , . . . , αa +
1, . . . , αk ) be a prioritized ordinal such that its a-th counter
αa + 1 is a successor ordinal. Then, regarding the approximant
pia (α1 , . . . , αa−1 , αa + 1, αa+1 , . . . , αk ), there exist ordinals
β1 , . . . , βa−1 such that

i1 < · · · < ia−1 < i ≤ ia < · · · < ik ,
that is, uia is the µ-variable with the smallest priority that is at least
as big as that of i. Then we define
(α1 , . . . , αk ) i (α10 , . . . , αk0 )
if, between the i-truncations (αa , . . . , αk ) and (αa0 , . . . , αk0 ) of the
prioritized ordinals, we have (αa , . . . , αk )  (αa0 , . . . , αk0 ). Here
the last  denotes the lexicographic extension of the usual order ≤
between ordinals, with the latter elements being the more significant. Note here that the i-truncation (αa , . . . , αk ) of (α1 , . . . , αk )
is obtained by dropping the first elements that correspond to the
µ-variables with priorities smaller than that of ui .
In case i holds in both ways we write =i . Note that =i is
in general coarser than the equality between prioritized ordinals

pia (α1 , . . . , αa−1 , αa + 1, αa+1 , . . . , αk )


p1 (β1 , . . . , βa−1 , αa , αa+1 , . . . , αk ),
(3)

...,
v fia 
pm (β1 , . . . , βa−1 , αa , αa+1 , . . . , αk )
and β1 ≤ α1 , . . . , βa−1 ≤ αa−1 . Recall here that fia is a
function in the system (1).
Cond. (3) originates from the definition f α+1 (⊥) = f (f α (⊥))
in Lem. 2.1.1; a notable difference here is that the counters with

5

2016/1/12

smaller priorities (i.e. from the first to the (a − 1)-th) can be
modified arbitrarily.
4. (µ-variables, limit case) Let a ∈ [1, k], and let (α1 , . . . , αk )
be a prioritized ordinal such that its a-th counter αa is a limit
ordinal. Then, regarding the approximant pia (α1 , . . . , αk ), we
have
G
pia (α1 , . . . , αa , . . . , αk ) v
pia (α1 , . . . , β, . . . , αk ) .

In Appendix A, as a sanity check, we present a correspondence
between our notion of progress measure (Def. 2.12) and Jurdzinski’s parity progress measure [33]. Jurdzinski’s formalization follows that of ranking functions, while ours here is based on approximation sequences p(0) v p(1) v · · · in the lattice L = 2X . The
relationship between the two is much like in Rem. 2.5.
Example 2.16. For a simple example following the spirit of Example 2.3, let us consider a set X and a transition relation R ⊆ X ×X,
and introduce a “modal operator”  : 2X → 2X by (X 0 ) :=
{x ∈ X | ∀x0 . xRx0 ⇒ x0 ∈ X 0 }.
We now fix a subset F ⊆ X, and consider the following
equational system over L = 2X .

β<αa

(4)
5. (ν-variables) Let i ∈ [1, m] \ {i1 , . . . , ik } (i.e. ui is a νvariable in the system (1)); let a ∈ [1, k] such that
i1 < · · · < ia−1 < i < ia < · · · < ik .

u1 =µ (F ∩ u2 ) ∪ u1 ,

Let (α1 , . . . , αk ) be a prioritized ordinal. Then, regarding the
approximant pi (α1 , . . . , αk ), there exist ordinals β1 , . . . , βa−1
such that
pi (α1 , . . . , αa−1 , αa , . . . , αk )


p1 (β1 , . . . , βa−1 , αa , . . . , αk ),
(5)

...,
v fi 
pm (β1 , . . . , βa−1 , αa , . . . , αk )

(6)

The system corresponds to the µ-calculus formula νu2 .µu1 . (F ∩
u2 ) ∪ u1 , and it is not hard to see—possibly relying on the
Knaster-Tarski and Cousot-Cousot characterizations, see §2.1—
that the solution for u2 is the set of states any infinite path from
which visits F infinitely often.
For this specific system (6), a progress
(Def. 2.12) is
 measure

given by data α, p1 (α) α≤α , p2 (α) α≤α subject to suitable
conditions. Some simplifications are possible, exploiting that in (5)
(and elsewhere) counters with smaller priorities can be modified
arbitrarily. We see, after this simplification, that a progress measure
for the equational system (6) is given by

and β1 ≤ α1 , . . . , βa−1 ≤ αa−1 .
This condition is somewhat similar to Cond. 3 above: it comes
from the condition l v f (l) in Lem. 2.1.2; and much like in
Cond. 3, the counters with smaller priorities can be modified
arbitrarily.

p1 (0) ⊆ p1 (1) ⊆ · · · ⊆ p1 (α) and p2 ,

Theorem 2.13 (correctness of progress measures). Let E be the
sol
equational system in (1) over L, and (l1sol , . . . , lm
) be its solution
(Def. 2.7).

all being subsets of X, such that:S1) p1 (0) = ∅; 2) p1 (α + 1) ⊆
(F ∩ p2 ) ∪ p1 (α); 3) p1 (α) = β<α p1 (β) for a limit ordinal α;
and 4) p2 ⊆ p1 (α). This “witnesses” the solution of (6), i.e. x ∈ p2
implies that any infinite path from x visits F infinitely often.

1. (Soundness) A progress measure gives a lower bound of the
 so-
lution. That is, assume (α1 , . . . , αk ), pi (α1 , . . . , αk ) i,→
−
α
is a progress measure. Then for each i ∈ [1, m] we have
pi (α1 , . . . , αk ) v

u 2 =ν u1 .

3.

lisol .

Coalgebraic µ-Calculus CµΓ,Λ

From this section on we apply the theory developed in §2 to a coalgebraic µ-calculus CµΓ,Λ . In the current section, as a preparation,
we introduce the logic CµΓ,Λ : its syntax, semantics, and a translation to equational systems (so that the results in §2 apply).

2. (Completeness) There exists a progress measure that achieves


the optimal, that is, (α1 , . . . , αk ), pi (α1 , . . . , αk ) i,→
−
α
such that
pi (α1 , . . . , αk ) = lisol
for each i ∈ [1, m].
Moreover, such an “optimal” progress measure can be chosen so that the ordinals in its maximum prioritized ordinal
(α1 , . . . , αk ) are suitably bounded, in the following sense. Let
ascCL(L) be the ordinal defined by the supremum of the length
of any (possibly transfinite) strictly ascending chain in L. Then
αa ≤ ascCL(L) for each a ∈ [1, k].

3.1

Coalgebraic Preliminaries

We start with a minimal set of coalgebraic preliminaries. For further
backgrounds on coalgebras see e.g. [31, 52]; and see e.g. [3, 40] for
categorical preliminaries. From now to §4 we fix the base category
to be the one Sets of sets and functions.
Let F be an endofunctor on Sets. An F -coalgebra is a function
c : X → F X, where X, F and c are intuitively understood as a
state space, a behavior type and a transition structure, respectively.
Therefore an F -coalgebra is “a transition system of the behavior
type F .” Some examples are presented later in Example 3.3.
Ff
Given
two
coalgebras
/ FY
FX
O
O
(7)
c : X → F X and d : Y → F Y
c
d
f
/Y
X
for the same functor, a coalgebra homomorphism from c to d is a function f : X → Y such that
the above diagram (7) commutes. In many examples of F , the notion of homomorphism expresses a natural definition of behaviorpreserving map. Conversely, it is common in the theory of coalgebras that the notion of F -behavioral equivalence is defined using
homomorphism (namely via cospans, see [31]).
F (beh(c))
Furthermore, many func/ FZ
FX
O
O
tors F allow a “classifying
c
final ζ
(8)
coalgebra”—one that contains
/Z
X
beh(c)
every possible F -behavior without redundancy. This is categorically captured by finality of a coalgebra. Precisely, a coalgebra ζ : Z → F Z is final if, for any
coalgebra c : X → F X there exists a unique homomorphism

In the item 2, the bound ascCL(L) is generally better than the
bound by the size |L| of the complete lattice L. For example, in
case L = 2X (where 2 = {tt, ff} and X is a set), ascCL(L) = |X|
while |L| = 2|X| .
We will need the following relaxation in establishing a correspondence to Jurdzinski’s notion of parity progress measure [33].
Definition 2.14 (extended progress measure for equational systems). Assume the setting of Def. 2.12. An extended progress measure p for E is the same as a progress measure, except that Cond. 2
of Def. 2.12 is replaced by the following:
2’. Let a ∈ [1, k]. Then αa = 0 implies either pia (α1 , . . . , αk ) =
⊥, or there exists a prioritized ordinal (α10 , . . . , αk0 ) such
that (α10 , . . . , αk0 ) ≺ia (α1 , . . . , αk ) and pia (α1 , . . . , αk ) v
pia (α10 , . . . , αk0 ).
Proposition 2.15. An extended progress measure is still sound in
the sense of Thm. 2.13.1.

6

2016/1/12

beh(c) : X → Z, as shown in (8). This way we understand the
carrier Z of a final coalgebra to be the set of all F -behaviors; and
the map beh(c) induced by finality (as in (8)) as the behavior map.

k (”for all but k successors”) and ♦k (”for more than k
successors”) for k ∈ ω, with associated predicate liftings
P
Jk K : 2X → 2F X , Y 7→ {f ∈ F X | x∈Y
/ f (x) ≤ k},
P
X
FX
J♦k K : 2 → 2 , Y 7→ {f ∈ F X | x∈Y f (x) > k}.

3.2 CµΓ,Λ : Syntax
It is common in the study of coalgebraic modal logics that the set
of modalities is parametrized. In our logic CµΓ,Λ , moreover, we
parametrize propositional connectives too. This allows us to accommodate unconventional connectives that occur in quantitative
setting, like the truncated sum in the Łukasiewicz µ-calculus [41]
and the average operator in e.g. [1].

5. Our approach also covers the coalition logic [49], interpreted
over game frames—these are coalgebras of the (class-valued)
functor
Y
F X = {(S1 , . . . , SN , f ) | ∅ =
6 Si ∈ Sets, f :
Si → X}
i∈N

Definition 3.1 (Λ, Γ). A modal signature Λ over F is a ranked
alphabet Λ = (Λn )n∈ω . An element λ ∈ Λn is an n-ary modality,
and we write |λ| for its arity n.
We assume that a modal signature comes with its interpretation.
Assigned to each λ ∈ Λ is a natural transformation JλK, whose
components are functions
|λ|
JλKX : ΩX
−→ ΩF X , natural in X,

with N a set of agents, tuplesQ
(S1 , . . . , SN ) capturing agent
strategies, and functions f :
i∈N Si → X modeling the
outcomes of strategy choices for the agents. The modalities [C],
with C ⊆ N a coalition, arise from predicate liftings J[C]KX :
2X → 2F X given by J[C]KX (Y ) = {(S1 , . . . , SN , f ) ∈
FX | Q
∃σC ∈ SC .∀σC ∈ SC .f (σC , σC ) ∈ Y }, where
SC =
i∈C Si , C = N \ C, and (σC , σC ) is defined as
expected.
6. Here is an example that would yield the usual “linear-time
logic” like LTL (i.e. formulas are interpreted over infinite
words), in the setting of §5. Take F = P(AP) × ( ), Ω = 2,
Γ = {tt, ff, ∧, ∨} and Λ = AP ∪ {X}, with the predicate
liftings

JpKX : 1 → 2F X , ∗ 7→ (U, x) ∈ P(AP) × X p ∈ U ,

JXKX : 2X → 2F X , (V ⊆ X) 7→ (U, x) x ∈ V .

and a component JλKX must be monotone with respect to (pointwise extensions of) the order v of the domain Ω of truth values. Such JλK is commonly called a (monotone) predicate lifting [28, 46].
Similarly, a propositional signature is a ranked alphabet Γ
where each γ ∈ Γ is called a propositional connective. Unlike a modal signature, each γ ∈ Γ is interpreted by a function
JγK : Ω|γ| → Ω; we require that JγK be monotone.
In what follows we will often write λ and γ for JλK and JγK.

In addition to the above 2-valued logics—that are also accounted
for by other coalgebraic approaches to modal logic (see e.g. [16])—
our approach additionally covers many-valued logics. For example,
the Łukasiewicz logic of [41] can be recovered by taking F =
PD, where D : Sets → Sets is the probability
P distribution
functor defined by DX = {µ : X → [0, 1] |
x µ(x) = 1},
Ω = [0, 1], Γ = {t, ⊕} and Λ = {♦}, with interpretations
JtK, J⊕K : [0, 1] × [0, 1] → [0, 1] given by

Definition 3.2 (CµΓ,Λ ). The language of our coalgebraic modal
logic CµΓ,Λ over Γ and Λ is given by the following set of formulas.
ϕ, ϕi ::= u |

γ (ϕ1 , . . . , ϕ|γ| )

| ♥λ (ϕ1 , . . . , ϕ|λ| ) |

µu. ϕ | νu. ϕ
Here u ∈ Var is a (fixed-point) variable. The notations γ (for
γ ∈ Γ) and ♥λ (for λ ∈ Λ) are to distinguish propositional
connectives (the former) from modalities (the latter).

JtKX (p, q) = max(p, q),

Example 3.3. Examples of predicate lifting-based coalgebraic logics abound.

and predicate lifting J♦KX : [0, 1]X → [0, 1]F X given by
X
µ(x)p(x).
J♦KX (p)(f ) = max

1. Standard (normal) modal logic is obtained by taking F =
P(AP) × P( ) (with P the covariant powerset functor and
AP a set of atomic propositions), Ω = 2, Γ = {tt, ff, ∧, ∨}
with the usual interpretations, and Λ = AP ∪ {, ♦} with

JpKX : 1 → 2F X , ∗ 7→ (U, Y ) | p ∈ U (where p ∈ AP),

JKX : 2X → 2F X , (V ⊆ X) 7→ (U, Y ) Y ⊆ V ,

J♦KX : 2X → 2F X , (V ⊆ X) 7→ (U, Y ) Y ∩ V 6= ∅ .

µ∈f

J[a]KX : 2

FX

→2

x

Another many-valued logic that is covered by our framework is
logics with future discounting [1, 21, 44]. A basic fragment is given
as follows: take F = P(AP) × ( ), Ω = [0, 1], Γ = {tt, ff, ∧, ∨}
and Λ = AP ∪ {X}, with the predicate liftings
(
1 if p ∈ U
FX
JpKX : 1 → [0, 1] , JpKX (∗)(U, x) =
0 otherwise,


1
JXKX : [0, 1]X → [0, 1]F X , d 7→ (U, x) 7→ · d(x) .
2

Atomic propositions are thus identified with 0-ary modalities,
as is standard in coalgebraic modal logic (see e.g. [53]).
2. Hennessy-Milner logic is obtained by taking F = (P( ))A
(with A a set of labels), Ω and Γ as before, and Λ = {[a], hai}
with associated predicate liftings
X

J⊕KX (p, q) = min(1, p + q)

Note the factor

1
2

that discounts the value of truth in the next step.

A

, Y 7→ {f ∈ P(X) | f (a) ⊆ Y },

3.3

JhaiKX : 2X → 2F X , Y 7→ {f ∈ P(X)A | f (a) ∩ Y 6= ∅}.

Equational Presentation

3. Monotone neighborhood logic [10] is obtained by taking
F X = {Y ∈ P(P(X)) | Y is upward-closed}, Ω and Γ
as before and Λ = {}, with an associated predicate lifting

In this paper we favor working with equational presentations of µcalculus formulas. Furthermore, for simplicity, we shall present µcalculus formulas as simple equational systems, meaning that each
right-hand side is of depth at most 1.

JK : 2X → 2F X , (U ⊆ X) 7→ {Y ∈ P(P(X)) | U ∈ Y }.

Definition 3.4 (simple CµΓ,Λ -equational system). A simple
CµΓ,Λ -equational system is an expression of the form

4. Graded modal logic [23] is obtained by taking F X = (ω +
1)X , Ω and Γ as before, and Λ consisting of graded modalities

u1 =η1 ϕ1 ,
7

...,

um =ηm ϕm

(9)

2016/1/12

where: ηi ∈ {µ, ν}; u1 , . . . , um ∈ Var are fixed-point variables;
and ϕ1 , . . . , ϕm are simple CµΓ,Λ -formulas of the form
ui ,

γ (ui1 , . . . , ui|γ| )

the tradition of coalgebraic modal logic [13, 16, 24, 53] as well as
that of fixed-point logics [39].
Definition 3.7 (semantics of CµΓ,Λ formulas). Let Γ and Λ be
propositional and modal signatures in Def. 3.1, and Let c : X →
F X be a coalgebra. A formula ϕ of CµΓ,Λ —with free variables
u1 , . . . , um —is assigned its denotation over c; it is given by a
function
m
JϕKc : ΩX
−→ ΩX
~ is short for
that is defined inductively in the following way. Here V
V1 , . . . , Vm , where Vi : X → Ω.
~ )(x) := Vi (x),
Jui Kc (V

~ )(x) :=
J γ ϕ1 , . . . , ϕn Kc (V

~ )(x), . . . , Jϕn Kc (V
~ )(x) ,
γ Jϕ1 Kc (V

~ )(x) :=
J♥λ ϕ1 , . . . , ϕn Kc (V



~ ), . . . , Jϕn Kc (V
~)
λX Jϕ1 Kc (V
c(x) ,

~ )(x) := µ JϕKc (V
~ , ) : ΩX → ΩX (x),
Jµu. ϕKc (V


~ )(x) := ν JϕKc (V
~ , ) : ΩX → ΩX (x).
Jνu. ϕKc (V

or ♥λ (ui1 , . . . , ui|λ| ).

We make a further requirement that, in case ηi = µ, the corresponding equation is of the form ui =µ uj for some j ∈ [1, m].
This inessential requirement simplifies our subsequent exposition.
A simple CµΓ,Λ -equational system (9) is closed if all the variables that occur in ϕ1 , . . . , ϕm are among u1 , . . . , um .
Note that, much like in §2, the order of equations in (9)
matters—the equations are solved from left to right, i.e. priorities
increases as one goes from left to right.
Translation of µ-calculus formulas into equational systems is
standard; so is translation in the other direction.
Definition 3.5 (translation). For each CµΓ,Λ -formula ϕ, its equational presentation Eϕ is defined by the following induction. Here
uϕ ∈ Var denotes the variable on the left-hand side of the last
equation in the equational system Eϕ , E1 ; . . . ; Ek denotes the
concatenation of equational systems E1 , . . . , Ek , and the variable
v in each clause is chosen to be a fresh one.

Eu := v =ν u

E γ (ϕ1 ,...,ϕn ) := Eϕ1 ; . . . ; Eϕn ; v =ν γ (uϕ1 , . . . , uϕn )

E♥λ (ϕ1 ,...,ϕn ) := Eϕ1 ; . . . ; Eϕn ; v =ν ♥λ (uϕ1 , . . . , uϕn )

Eηu. ϕ := Eϕ ; u =η uϕ
where η ∈ {µ, ν}

Recall that γ : Ωn → Ω and λX : (ΩX )n → ΩF X are assumed
to be given (Def. 3.1). In the last two clauses it is assumed, by suitably rearranging variables, that the bound variable u is the last one
um among the free variables u1 , . . . , um of ϕ. The necessary fixed
~ , ) : ΩX → ΩX are guaranteed by
points of the function JϕKc (V
the Knaster-Tarski theorem, since Ω (and hence ΩX ) is a complete
~ , ) is easily seen to be monotone.
lattice and the function JϕKc (V

The choice of =ν in the first three clauses is arbitrary from the semantical viewpoint: changing it into =µ yields the same semantics.
It is however beneficial from the algorithmic and presentational
viewpoints—in particular the resulting system enjoys the requirement in Def. 3.4 (that a µ-equation is of the form ui =µ uj ).
It is straightforward to see that a closed formula ϕ yields a
closed equational system Eϕ .
Conversely, given a simple CµΓ,Λ -equational system E like
in (9), we define its formulaic presentation ϕE by induction on
the number m of equations. If m = 1 then an equation u1 =η1 ϕ1
becomes the formula η1 u1 . ϕ1 . For the step case, let E 0 be obtained
by dropping the first equation, that is,

E 0 = u2 =η2 ϕ2 , . . . , um =ηm ϕm .

Lemma 3.8. Let f be a coalgebra homomorphism from c : X →
F X to d : Y → F Y , as in (7). For each closed CµΓ,Λ -formula ϕ
and each x ∈ X, we have JϕKc (x) = JϕKd (f (x)).

As discussed in §3.3 we favor working with equational presentation of formulas. We shall therefore define their semantics, too.
Definition 3.9 (semantics of simple CµΓ,Λ -equational systems).
Let E be a simple CµΓ,Λ -equational system
u1 =η1 ϕ1 , . . . , um =ηm ϕm

(10)

from Def. 3.4; assume that it is closed. Let c : X → F X be an
F -coalgebra.
Then E and c together induce an equational system Ec (in the
sense of Def. 2.6) over the complete lattice L = ΩX —this is
by identifying a simple formula ϕi on a right-hand side with the
function Jϕi Kc : (ΩX )m → ΩX defined in Def. 3.7.
sol
Finally, solving Ec as in Def. 2.7 yields a solution (l1sol , . . . , lm
)
X m
sol
that is an element of (Ω ) . The last component lm is referred
to as the semantics of the simple CµΓ,Λ -equational system E over
the coalgebra c.

Then we define ϕE to be the result of replacing u1 in ϕE 0 with
η1 u1 . ϕ1 . That is,


ϕE := ϕE 0 η1 u1 .ϕ1 / u1 .
The two translations are mutually inverse—not necessarily syntactically, but the semantics is preserved. See Prop. 3.10 later.
Therefore, in what follows, we do not distinguish a CµΓ,Λ -formula
ϕ and its equational presentation Eϕ . Both will be denoted by ϕ.
Example 3.6. Let Γ = {∧, ∨} and Λ = AP ∪ {X} (from
Example 3.3). The CµΓ,Λ -formula νu. µv. ((p ∨ X v) ∧ X u) gets
translated into the simple CµΓ,Λ -equational system

The two semantics—the direct one, and the one via equational
presentation—coincide, as expected.
Proposition 3.10. Let ϕ be a closed CµΓ,Λ -formula, and c : X →
F X be a coalgebra. Consider its equational presentation Eϕ (a
simple CµΓ,Λ -equational system, Def. 3.5). Then the semantics of
Eϕ over c—in the sense of Def. 3.9, i.e. the solution of the equational system Eϕ,c over ΩX —coincides with JϕKc from Def. 3.7.

u1 =ν p, u2 =ν v, u3 =ν X u2 , u4 =ν u1 ∨ u3 ,
u5 =ν u, u6 =ν X u5 , u7 =ν u4 ∧ u6 , v =µ u7 , u =ν v,
under Def. 3.5. The translation in the other direction gives rise to a
complicated formula which, however, is easily seen to be equivalent
to the original formula under (obviously sound) simplifications like
νu1 . p into p.

Proof. Straightforward by induction.

3.4 CµΓ,Λ : Semantics

4. CµΓ,Λ Model Checking against F -Coalgebras

Formulas of CµΓ,Λ are interpreted over F -coalgebras (see §3.1).
The following inductive interpretation is a standard one; it follows

Let us turn to the model-checking problem of the modal logic
CµΓ,Λ against F -coalgebras. Later in §5 we study model checking

8

2016/1/12

form uia =µ ui0 for some i0 ∈ [1, m]. We require that there
exist ordinals β1 , . . . , βa−1 such that

against coalgebras with additional nondeterministic branching—
i.e. there the logic CµΓ,Λ is thought of as a “linear-time” logic.
In contrast, here CµΓ,Λ is a “branching-time” logic, in the sense
that there is no additional branching to be abstracted away.
Prop. 3.10, together with Thm. 2.13, already gives us a characterization of the semantics JϕKc in terms of progress measures.
In this section we shall rephrase it to yet another form, called MC
progress measure, that is easier to manipulate. Using it we present
our main technical results, namely a generic model-checking algorithm (Algorithm 1) and its complexity (Thm. 4.13).
The following correspondence for (polyadic) modalities—that
is not unlike in the Yoneda lemma—will be used in the following
developments.

pia (α1 , . . . , αa + 1, . . . , αk )
v pi0 (β1 , . . . , βa−1 , αa , . . . , αk )
and β1 ≤ α1 , . . . , βa−1 ≤ αa−1 .
4. (µ-variables, limit case) Let a ∈ [1, k], and let (α1 , . . . , αk )
be a prioritized ordinal such that its a-th counter αa is a limit
ordinal. We require
F
pia (α1 , . . . , αa , . . . , αk ) v β<αa pia (α1 , . . . , β, . . . , αk ) .
5. (ν-variables) Let i ∈ [1, m] \ {i1 , . . . , ik } (i.e. ui is a νvariable in the system (1)); let a ∈ [1, k] such that

Lemma 4.1 (λhj1 ,...,jn i , λ̃). Let λ be a natural transformation,
given by arrows λX : (ΩX )n → ΩF X that are natural in X. (This
is the setting in Def. 3.1, where λ is an n-ary modality). Let m ∈ ω
and j1 , . . . , jn ∈ [1, m]. These data induce an arrow

i1 < · · · < ia−1 < i < ia < · · · < ik .
Let (α1 , . . . , αk ) be a prioritized ordinal. We require the following on the approximant pi (α1 , . . . , αk ):
(a) (RHS is a variable) If the formula ϕi in the i-th equation
ui =ν ϕi is a variable ui0 (for some i0 ∈ [1, m]), then there
exist ordinals β1 , . . . , βa−1 such that

λhj1 ,...,jn i : F (Ωm ) → Ω
by λhj1 ,...,jn i := λΩm (πj1 , . . . , πjn ). Recall that λΩm is of type
m
m
(ΩΩ )n → ΩF (Ω ) , and πj : Ωm → Ω.
Moreover, let us define λ̃ : F (Ωn ) → Ω by λ̃ := λh1,2,...,ni =
λΩn (π1 , . . . , πn ), where π1 , . . . , πn : Ωn → Ω. Then we have
F (Ωm )
F hπj1 ,...,πjn i



F (Ωn )

4.1

pia (α1 , . . . , αa , . . . , αk )
v pi0 (β1 , . . . , βa−1 , αa , . . . , αk )

λhj1 ,...,jn i
λ̃

and β1 ≤ α1 , . . . , βa−1 ≤ αa−1 .
(b) (RHS is a propositional formula) If the
 formula ϕi is a
propositional formula γ uj1 , . . . , ujn , then there exist
ordinals β1 , . . . , βa−1 such that

/+ Ω .

MC Progress Measure

We start with customizing the lattice-theoretic notion of progress
measure (Def. 2.12) to one that is tailored to CµΓ,Λ model checking. For reuse in later sections, the definition is separated into the
transition-irrelevant part (which we call pre-progress measure), and
the full definition.

pi (α1 , . . . , αa , . . . , αk )


pj1 (β1 , . . . , βa−1 , αa , . . . , αk ),

...,
v JγK 
pjn (β1 , . . . , βa−1 , αa , . . . , αk )

Definition 4.2 (pre-progress measure, pPM). Let F : Sets →
Sets be a functor. Let ϕ be a CµΓ,Λ -formula—where Λ is a
modal signature over F —that is identified with a simple equational
system u1 =η1 ϕ1 , . . . , um =ηm ϕm as in §3.3. Let i1 < · · · < ik
enumerate the indices of all the µ-variables.
A pre-progress measure (pPM) p for ϕ is given by a tuple


p = (α1 , . . . , αk ), pi (α1 , . . . , αk ) i,α ,...,α
1

and β1 ≤ α1 , . . . , βa−1 ≤ αa−1 .
Let α be an ordinal. The collection of all pre-progress measures
for a formula ϕ, whose maximum prioritized ordinal (α1 , . . . , αk )
satisfies αi = α for each i ∈ [1, k], shall be denoted by pPMϕ,α .
Recall that Ω is the complete lattice of truth values. In the definition
of pPMϕ,α , the explicit bound by α is there so that the collection
pPMϕ,α is a (small) set.
Comparing the previous definition with Def. 2.12 of progress
measures, what are missing here are the treatment of modal formulas ♥λ (uj1 , . . . , ujn ) in Cond. 5—this is precisely the case where
the transition structure of the coalgebra in question becomes relevant. In the current setting of CµΓ,Λ as a “branching-time” logic,
this case is taken care of in the following way. MC stands for
“model checking.”

k

that consists of:
• the maximum prioritized ordinal (α1 , . . . , αk ); and
• the approximants pi (α1 , . . . , αk ) ∈ Ω, defined for each i ∈

[1, m] and each prioritized ordinal (α1 , . . . , αk ) such that α1 ≤
α1 , . . . , αk ≤ αk .
The approximants pi (α1 , . . . , αk ) are subject to:
1. (Monotonicity) Let i ∈ [1, m] (hence ui is either a µ- or
ν-variable). Then (α1 , . . . , αk ) i (α10 , . . . , αk0 ) implies
pi (α1 , . . . , αk ) v pi (α10 , . . . , αk0 ).
2. (µ-variables, base case) Let a ∈ [1, k]. Then αa = 0 implies
either: pia (α1 , . . . , αk ) = ⊥, or there exists a prioritized ordinal (α10 , . . . , αk0 ) such that (α10 , . . . , αk0 ) ≺ia (α1 , . . . , αk )
and pia (α1 , . . . , αk ) v pia (α10 , . . . , αk0 ). (Note here that this
condition mirrors Cond. 2’ of Def. 2.14, rather than Cond. 2 of
Def. 2.12. Prop. 2.15 justifies doing so.)
3. (µ-variables, step case) Let a ∈ [1, k], and let (α1 , . . . , αa +
1, . . . , αk ) be a prioritized ordinal such that its a-th counter
αa + 1 is a successor ordinal. Consider the approximant
pia (α1 , . . . , αa + 1, . . . , αk ). Since uia is a µ-variable, by
a requirement in Def. 3.4 the corresponding equation is of the

Definition 4.3 (MC progress measure). Assume the setting of
Def. 2.12, and let c : X → F X be a coalgebra in Sets. An MC
progress measure for ϕ over c is given by:
• some ordinal α, called the maximum ordinal, and
• a function Q : X → pPMϕ,α ,

that are subject to the following condition.
5(c) (ν-variables, RHS is a modal formula) Let x ∈ X and
p := Q(x) be a pre-progress measure for ϕ. Let i ∈ [1, m]
and assume the setting of Cond. 5 of Def. 4.2 (i.e. ui is a νvariable), and further that the formula ϕi is a modal formula:
ϕi = ♥λ (uj1 , . . . , ujn ).
9

2016/1/12

Now consider the approximant pi (α1 , . . . , αa , . . . , αk ) ∈ Ω of
p. We require there exist ordinals β1 , . . . , βa−1 such that

Assumption 4.5. Throughout §4.2 we focus on the Boolean setting
(i.e. Ω = 2), and restrict the state space X of the coalgebra
c : X → F X (as a system model) to be finite. This is a reasonable
assumption because we aim at a concrete algorithm. In view of
Thm. 4.4.2, in employing the theoretical machinery developed so
far, all the ordinals that occur can be restricted to finite (since
ascCL(2X ) = |X| is finite).
weVrestrict W
the propositional signature Γ to Γn :=
VFurthermore,
W
{ n , n }, where n and n are the n-ary conjunction and disjunction operators with obvious interpretations. This signature of Γ
is functionally complete in the current monotonic Boolean setting:
any other propositional connective γ : 2n → 2 can be encoded by

pi (α1 , . . . , αa , . . . , αk ) v

PT♥λ (uj1 ,...,ujn ) (β1 , . . . , βa−1 , αa , . . . , αk ) (F Q ◦ c)(x) ,
(11)
and β1 ≤ α, . . . , βa−1 ≤ α.
FQ
c
Note that (F Q ◦ c)(x) ∈ F (pPMϕ,α ) since X → F X →
0
0
F (pPMϕ,α ). For each (α1 , . . . , αk ), the function
PT♥λ (uj1 ,...,ujn ) (α10 , . . . , αk0 ) : F (pPMϕ,α ) → Ω
in (11) is defined as follows. (The name PT comes from “predicate transformer.”)
PT♥λ (uj1 ,...,ujn ) (α10 , . . . , αk0 )
h

F (pPMϕ,α )

F (ev(α01 ,...,α0k ))

−→

WV

:=

F (Ωm )

λhj1 ,...,jn i

−→

i
Ω ,

Definition 4.6 (prioritized ordinal matrix, POM). Assume the setting of Def. 4.2. A prioritized ordinal matrix is an m × k matrix


(1)
(1)
α1
· · · αk
 .
.. 
..
 .

.
 .
. ,
(m)
(m)
· · · αk
α1

(12)

where λhj1 ,...,jn i is from Lem. 4.1, and the function
ev(α10 , . . . , αk0 ) : pPMϕ,α → Ωm
is defined by “fixing a prioritized ordinal,” that is,

~0 )(p) := p1 (α
~0 ), . . . , pm (α
~0 ) ∈ Ωm .
ev(α
−
→
The composite in the definition of PT♥λ (uj1 ,...,ujn ) ( α0 ) in (12)
might seem exotic, but the definition here is in fact a straightforward adaptation of the common interpretation of modal formulas
in coalgebraic logics. Recall the interpretation of a modal formula
♥λ (ϕ1 , . . . , ϕn ) in Def. 3.7, that is also the standard one in the
literature (see e.g. [53]). Then it is not hard—by naturality of λ,
much like in the proof of Thm. 4.4—that this standard definition of
J♥λ (~
ϕ)Kc is equivalent to the following, where Jϕi Kc : X → Ω are
the interpretations of the constituent subformulas (for i ∈ [1, n]),
and λ̃ is from Lem. 4.1.

F hJϕi Kc ii
c
λ̃
J♥λ (~
ϕ)Kc = X → F X −→ F (Ωn ) −→ Ω .

(i)

where each entry αa is either
• an ordinal, or
• the symbol ♠ for “failure.”
(i)

It is required that, if any entry αa is ♠ then all entries on the same
(i)
(i)
row is ♠, that is, α1 = · · · = αk = ♠.
The set of all POMs, such that all the ordinals therein are no
bigger than α, is denoted by POMα .
A POM is therefore an m-tuple of


prioritized ordinals, where some prior3 5 2
u1
itized ordinals can be replaced by ♠.
u2  ∗ 1 0 


Its i-th row will be a prioritized ordinal
u3  ♠ ♠ ♠ 
for the i-th variable ui . In view of the
u4  ∗ ∗ 4 
monotonicity conditions (in Def. 2.12
u5
∗ ∗ ∗
and 4.2) and the definition of i (Def. 2.10), we can see that some
first elements in a row (precisely: those which correspond to µvariables with a smaller priority than ui ) do not make any difference. Such entries can safely be denoted by ∗ (“arbitrary”). An example is shown in the above: it is a POM for an equational system
with 5 variables, in which u1 , u3 , u4 are µ-variables and u2 , u5 are
ν-variables. We shall however restrict use of ∗ for providing intuitions; it does not appear in the technical developments.
In the current section (§4.2) where X is assumed to be a finite
set, it is not needed to allow any ordinal as an entry of a POM
(Def. 4.6). Natural numbers will just suffice.

This indeed resembles the right-hand side of (11), namely
c

X → FX

~0 )◦Q)
F (ev(α

−→

F (Ωm )

λhj1 ,...,jn i

−→


Ω (x).

Theorem 4.4 (correctness of MC progress measure). Assume the
setting of Def. 4.3. In particular, the formula ϕ is translated to an
equational system with m variables.
1. (Soundness) Let Q be an MC progress measure (with the maximum ordinal α), x ∈ X and p := Q(x). Then
pm (α, . . . , α) v JϕKc (x),

where JϕKc : X → Ω is from Def. 3.7.
2. (Completeness) There exists an MC progress measure Q that
achieves the optimal. That is, an MC progress measure Q such
that (Q(x))m (α, . . . , α) = JϕKc (x) for each x ∈ X. Moreover, Q can be chosen so that its maximum ordinal α is α =
ascCL(ΩX ), where ascCL(ΩX ) is the length of the longest
strictly ascending chain in ΩX (see Thm. 2.13.2).
4.2

{li1 , . . . , lik } li1 = · · · = lik = tt ⇒ γ(l1 , . . . , ln ) = tt .

Definition 4.7 (matrix progress measure, MPM). Assume the setting of Def. 4.3. A matrix progress measure (MPM) for ϕ over c,
with a maximum ordinal α, is a function R : X → POMα that
satisfies the following conditions. Let x ∈ X be arbitrary, and consider R(x) ∈ POMα .
2. (µ-variables, base case) Let a ∈ [1, k] and consider the corre(i )
sponding µ-variable uia . Assume α1 a 6= ♠. Then we must
(ia )
have (R(x))
ia (0, 0, . . . , 0). Note that the ia -th row
(R(x))(ia ) of R(x) is a prioritized ordinal, and recall ia from
Def. 2.10. Note also that the required inequality is strict.
(That is, a row in R(x) that corresponds to a µ-variable must
not be (∗, . . . , ∗, 0, . . . , 0).)
3. (µ-variables, step case) Let a ∈ [1, k] and consider the corre(i )
sponding µ-variable uia . Assume α1 a 6= ♠. Let uia =µ ui0
(where i0 ∈ [1, m]) be the corresponding equation in ϕ. If

Algorithms

Here we shall further translate the notion of MC progress measure (Def. 4.3) to a Jurdzinski-style presentation; the latter shall
be called a matrix progress measure. The correspondence is an extension of the one in Appendix A; see also Rem. 2.5. We shall then
devise a model-checking algorithm based on matrix progress measures. Thanks to the concrete presentation with matrices, we believe
its implementation is a fairly straightforward task.

10

2016/1/12

0

i0 ≤ ia , then we must have (R(x))(ia ) i (R(x))(i ) . Note
the inequality is strict.
4. (µ-variables, limit case) Let a ∈ [1, k], and consider the
(i )
corresponding µ-variable uia . Then (R(x))a a must not be a
limit ordinal. (This condition is vacuous when α is finite.)
5. (ν-variables) Let i ∈ [1, m] \ {i1 , . . . , ik } (i.e. ui is a ν(i)
variable). Assume that α1 6= ♠. Let ui =ν ϕi be the corresponding equation in ϕ.
(a) (RHS is a variable) If the formula ϕi is a variable ui0 (for
0
some i0 ∈ [1, m]). Then (R(x))(i) i (R(x))(i ) .
(b) (RHS is a propositional formula) Recall
V thatWwe have restricted propositional
and
(AssumpV connectives to
tion 4.5). If ϕi = (ui1 , . . . , uin ) then we require all of

Algorithm 1 An algorithm for CµΓ,Λ model checking, in the
setting of Def. 4.3 and Assumption 4.5. HereR(x, i) denotes the
prioritized ordinal R(x, i, 1), . . . , R(x, i, k) . Note that on lines
16, 19 and 23, ui is necessarily a ν-variable.
Input: A CµΓ,Λ -formula ϕ presented as an equational system u1 =η1
ϕ1 , . . . , um =ηm ϕm where ui1 , . . . , uik are µ-variables, and a
coalgebra c : X → F X
Output: JϕKc ∈ 2X
1: for each x ∈ X, i ∈ [1, m] and j ∈ [1, k] do
. initialization
2:
R(x, i, j) := 0
3: end for
4: for each a ∈ [1, k] do
. Cond. 2
5:
R(x, ia , a) := 1
6: end for
7: repeat
. the main loop
8:
for each x ∈ X and i ∈ [1, m] do
9:
if ui is a µ-variable, i = ia and ϕi = ui0 then
. Cond. 3
10:
R(x, i) := maxi R(x, i),
. cf. Def. 4.9

11:
R(x, i0 , 1), . . . , R(x, i0 , a) + 1, . . . , R(x, i0 , k)
12:
end if
13:
if ui is a ν-variable andϕi = ui0 then
. Cond. 5(a)
14:
R(x, i) := maxi R(x, i), R(x, i0 )
15:
end if V
V
. Cond. 5(b), the -case
16:
if ϕi = (uj1 , . . . , ujn ) then
17:
R(x, i) := maxi R(x, i), R(x, j1 ), . . . , R(x, jn )
18:
end if W
W
. Cond. 5(b), the -case
19:
if ϕi = (uj1 , . . . , ujn ) then
20:
R(x, i) := maxi R(x, i),

21:
mini R(x, j1 ), . . . , R(x, jn )
22:
end if
23:
if ϕi = ♥λ (uj1 , . . . , ujn ) then
. Cond. 5(c)

24:
R(x, i) := maxi R(x, i), PTM
(x)
.
cf. Def. 4.10
i
25:
end if
26:
27:
for each j ∈ [1, k] do
28:
if R(x, i, j) > |X| then
. ui has seen to be false at x
29:
R(x, i) := (♠, . . . , ♠)
30:
end if
31:
end for
32:
end for
33: until no change is made
34: return {x ∈ X | R(x, m, k) 6= ♠}

(R(x))(i) i (R(x))(i1 ) , . . . , (R(x))(i) i (R(x))(in )
(13)
W
to hold. If ϕi = (ui1 , . . . , uin ) then we require at least
one of (13) to hold.
(c) (RHS is a modal formula) Assume that the formula ϕi
~ =
is a modal formula ϕi = ♥λ (uj1 , . . . , ujn ). Let α
(α1 , . . . , αk ) := (R(x))(i) . Consider the following composite h : X → 2:

F (ev0 (~
α)) 
c
FR
X → F X → F (POMα ) −→
h :=
, (14)
λhj1 ,...,jn i
F (2m )
−→
2
where ev0 (~
α) : POMα → 2m is defined by


def.
(i0 )
(i)
(i0 )
= tt ⇐⇒ α
~ i0 (β1 , . . . , βk )
ev0 (~
α) (βj )i,j
i0

0

for each i ∈ [1, m]. We require that h(x) = tt.
Again, much like for Cond. 5(c) in Def. 4.3, the composite
in (14) is understood as an analogue of the usual interpretation of
modal formulas in coalgebraic logics (cf. Def. 3.7).
Theorem 4.8 (correctness of MPM). Assume the setting of Def. 4.3.
1. (Soundness) If there exists an MPM R : X → POMα such that
(m)
(R(x))k 6= ♠, then JϕKc (x) = tt.
2. (Completeness) There is an optimal MPM R0 : X → POM|X|
(m)
such that: JϕKc (x) = tt if and only if (R0 (x))k 6= ♠.

M
Definition 4.10 (PTM
i ). In Algorithm 1, the function PTi takes a
state x ∈ X and returns

We follow [33] and present an algorithm that looks for the optimal MPM. See Algorithm 1. There we use the following functions.

PTM
i (x) :=

mini α
~ ∈ |X|k

Definition 4.9 (maxi , mini ). In Algorithm 1, the function
maxi takes a set of prioritized ordinals (and possibly (♠, . . . , ♠))
and returns a prioritized ordinal such that: the first irrelevant entries
(due to priorities smaller than that of ui ) are set to 0; and the rest
is the maximum (with the lexicographic order, the latter the more
significant) among the corresponding suffixes of the prioritized ordinals given as input. In case the input set contains (♠, . . . , ♠),
then the output is (♠, . . . , ♠) too.
For example, in the setting of Example 2.11,



α) ◦ R ◦ c (x) = tt
λhj1 ,...,jn i ◦ F ev0 (~
(15)
where the composite is from (14) and R : X → POMα is given by
the current values of R(x, i, j) x,i,j in the algorithm.
The complexity of PTM
i depends greatly on the choice of a
functor F and a predicate lifting λ. A uniform and brute-force
algorithm for PTM
~ ∈
i is possible, however, by enumerating all α
|X|k from the smaller ones with respect to i , and checking for
each α
~ whether the condition in (15) is satisfied. The worst-case
complexity is O(km2 |X|k+1 + C|X|k ) with some constant C, on
the assumption that the value

λhj1 ,...,jn i ◦ F (ev0 (~
α)) ◦ F R ◦ c (x) that appear in (15)

max3 {(1, 2, 3), (3, 4, 1)} = (0, 2, 3)
where the first element of each sequence is irrelevant.
The function mini is defined similarly, by: truncating the
first irrelevant elements, choosing the smallest one in the lexicographic order, and padding the missing elements with 0. The output is (♠, . . . , ♠) in case the input set contains nothing other than
(♠, . . . , ♠).
The functions maxi and mini can be efficiently implemented: if the input is the set of N prioritized ordinals then the
time complexity is O(N k).

is computed in time O(km2 |X| + C). The last assumption is
derived as follows: the computation of ev0 (~
α) is in O(km); hence
the computation of F (ev0 (~
α)) is in O(km|X|); that of λhj1 ,...,jn i
is in O(m) (exploiting Lem. 4.1); and the other components like
c and application of F have only a constant contribution C to the
complexity.

11

2016/1/12

Remark 4.11. Most F and Λ allow much better complexity of
PTM
i . For example, the choice F = P(AP) × ( ) and λ = X
(the next-time modality) in Example 3.3.6 (that will yield a logic
like LTL in §5), the function PTM
i picks up the prioritized ordinal
R(x0 , i) of the successor x and truncates its first irrelevant elements
to 0. This can be done in time O(k). More generally, often it is
possible to “propagate backwards” by computing {t ∈ F (Ωm ) |
λhj1 ,...,jn i (t) = tt}, for which a one-step complete set of deduction
rules can be used (see e.g. [16]). Such optimizations by deduction
rules are left as future work.

A monad T on Sets is an endofunctor equipped with natural
transformations η T : id ⇒ T (unit) and µT : T ◦ T ⇒ T
(multiplication) that are subject to certain “monoid” commutative
diagrams. In our current example of the powerset monad P, its
unit η P is the singleton map and its multiplication µP is given by
union. In the class of examples of T that are relevant to us, the unit
turns an element into “a branching with a unique choice”; and the
multiplication “suppresses” two transitions into one (see [27]).
The Kleisli category K`(T ) has sets as its objects, and an arrow
p Y in K`(T ) is given by a function X → T Y . It becomes
X →
a category using the monad structure of T . For example, given
p Y and g : Y →
p Z in K`(T ),
two successive arrows f : X →
f
p Z is given by the composite X →
its composition g f : X →
µZ
Tg
T Y → T (T Z) → T Z of functions. It is also easy to see that we
have the so-called Kleisli inclusion functor J : Sets → K`(T ) by
JX = X and Jf = η T ◦ f .
p and (as opposed to → and
Note that we used the symbols →
◦) for constructs in K`(T ), for distinction. In what follows we stick
to this convention.
Note that for our example of T = P, the Kleisli category
K`(P) is nothing but the category Rel of sets and binary relations.
We will however stick to K`(P), hoping that the theory will be
transported to other monads (such as the Giry monad on Meas,
for probabilistic branching).
The following is our current notion of system model. For technical reasons, we impose certain conditions on F . These conditions
are common ones and imposed also in [27, 30, 34].

Theorem 4.12. Algorithm 1 indeed returns JϕKc .

The following complexity result is derived from an analysis of
Algorithm 1. Recall that it assumes a brute-force algorithm for
PTM
i (Def. 4.10); fixing F and Λ will allow further optimization.
See Rem. 4.11. It nevertheless achieves a complexity that is exponential only in k. This is much like the most known complexity
results for model-checking (see e.g. [19, 60])—note that k bounds
the alternation depth of a formula ϕ.
Theorem 4.13 (complexity). In the setting of Def. 4.3 and Assumption 4.5, the model-checking problem can be decided in time

O m2 (km2 |X| + C)|X|k+2 (|X| + 1)k .
A straightforward optimization is possible: each iteration of the
inner loop (lines 8–32) tests all (x, i); this is unnecessary. Algorithm 1 is presented as it is, however, since the correspondence to
Def. 4.7 is clearer. It should be possible also to improve the complexity so that it is exponential to the alternation depth, instead of
to the number k of µ-operators, of the given formula ϕ.

5.

Definition 5.1 (nondeterministic F -coalgebra). Let F : Sets →
Sets be a functor, such that the following hold.

Coalgebraic µ-Calculus CµΓ,Λ as a
Nondeterministic Linear-Time Logic

∼

=
1. A final coalgebra ζ : Z →
F Z exists in Sets.
2. The functor F comes with a distributive law ξ : F P ⇒ PF
over the powerset monad P (which, as is well-known [30],
induces a lifting F : K`(P) → K`(P) of F ).

In this section we adapt the previous results to the setting where
we think of CµΓ,Λ as a (nondeterministic) linear-time logic, that
is, where a system in question exhibits nondeterministic branching
over transitions of type F . Such a system is represented as a function c : X → PF X.
Our main results here are: 1) categorical characterization of the
truth value of a linear-time logic formula using progress measures
(Thm. 5.6); 2) a “smallness” result that cuts down the search spaces
for linear-time model checking (Thm. 5.7); and 3) a decision procedure (Thm. 5.9) that depends on the smallness result.
5.1

A nondeterministic F -coalgebra is c : X → PF X in Sets,
p F X in the Kleisli category K`(P).
that is, an arrow c : X →
Examples of such functors are polynomial functors inductively
generated by
F, Fi ::= id | A | F1 × F2 |

Coalgebraic Preliminaries

`

i∈I

Fi

where A is a constant functor that takes any set to A ∈ Sets. See
e.g. [27, 57] for further details on Cond. 1–2.
In view of §3.1, in the current setting, we can identify a state
∼
=
z of a final coalgebra ζ : Z →
F Z with a (possibly infinite,
long-term) linear-time behavior of the type F . For example, when
F = P(AP) × ( ) (Example 3.3.6), a final coalgebra is carried by
the set Z = (P(AP))ω of infinite streams of subsets of AP. Such
streams are commonly called computations in the context of model
checking.
The following result [30] allows us to characterize, in categorical terms, the set of possible (linear-time) F -behaviors of a nondeterministic F -coalgebra.3 The same holds in a probabilistic setting,
too; see e.g. [57].

In what follows we will be dealing with coalgebras of the type
c : X → PF X, where F : Sets → Sets (that is like in §3.1)
is understood as the type of linear-time behaviors, and P is the
powerset monad.
This is a common setting taken in the coalgebraic studies of
trace semantics. The use of a monad T in a coalgebra c : X →
T F X with “T -branching over F -linear time behaviors” originates
in [51], and is subsequently adopted e.g. in [11, 27, 30, 34, 57].2
The formalization in the current paper most closely follows that
in [57]. We shall again present minimal preliminaries to this Kleisli
approach to coalgebraic trace semantics. See e.g. [27, 57] for further details; for monads and Kleisli categories see [40].
2 Another

common coalgebraic formalization of linear-time semantics is
via determinization, and uses Eilenberg-Moore categories (as opposed to
Kleisli) as base categories. See e.g. [4, 32]. Adapting the current modelchecking framework to this Eilenberg-Moore approach seems hard: fixedpoint specifications are usually interpreted over infinitary traces such as infinite words; and this makes determinization, the core of the Eilenberg-Moore
approach, much more complicated (like Büchi word automata become Rabin automata, see e.g. [58]).

3 In

papers like [27] coalgebraic finite trace semantics is studied. Here
“finite” means linear-time behaviors that eventually come to halt within
finitely many steps; and the set of finite F -behaviors is identified with the
carrier of an initial F -algebra in Sets (as opposed to a final F -coalgebra).

12

2016/1/12

Proposition 5.2 (coalgebraic infinitary4 trace semantics [30]). Let
F : Sets → Sets be a functor that satisfies the conditions in
Def. 5.1; and c : X → PF X be a nondeterministic F -coalgebra.
Consider the diagram
FX
O
c_

X



Ff


f

/ FZ
O
∼
= _ Jζ
/Z

A CµΓ,Λ -formula ϕ is interpreted over elements of a final
coalgebra, i.e. computations. Overall, Def. 5.3 in this setting yields
the set of truth values that ϕ can take, ranging over all the possible
computations z ∈ tr(c)(x) that start from the given state x ∈ X.
5.3

in K`(P);

We shall follow essentially the same path as in §4.1. We shall use
precisely the same notion of pre-progress measure (Def. 4.2). The
additional compatibility condition with the dynamic structure of the
system in question is different reflecting the difference between the
p F X in K`(P)).
systems in question (X → F X in Sets, or X →
The following is a counterpart of Def. 4.3; LT is for linear-time.

(16)

then: 1) there exists at least one function f : X → PZ that makes
the diagram commute; and 2) among such f , there exists the greatest one with respect to (the pointwise extension of) the inclusion order in PZ. The greatest one shall be denoted by tr(c) : X → PZ
and called the (infinitary) trace semantics of c. Moreover, an element z ∈ tr(c)(x)—identified with a single linear-time behavior
over time—is referred to as an infinitary trace of c from x.

Definition 5.5 (LTMC progress measure). Let ϕ be a CµΓ,Λ formula, identified with a simple CµΓ,Λ -equational system u1 =η1
ϕ1 , . . . , um =ηm ϕm . Let c : X → PF X be a nondeterministic F -coalgebra (with some conditions on F ; see Def. 5.1).
An LTMC progress measure for ϕ over c is given by a tuple
q
(α, Y → F Y, r, s) of:

We note that the definition of tr(c) in Prop. 5.2 amounts to the
following: tr(c) is the greatest fixed point of the monotone function
f 7→ (Jζ)−1

Ψ : K`(P)(X, Z) → K`(P)(X, Z),

Ff

• some ordinal α,
• an F -coalgebra q : Y → F Y , and
• functions r : Y → pPMϕ,α and s : Y → X

c
(17)

where denotes composition of arrows in K`(P).
It has been observed that, for many examples of the functor
F , the greatest homomorphism tr(c) in Prop. 5.2 indeed captures
the set of all possible linear-time behaviors. See e.g. [11] and [57,
Appendix A.2].

that are subject to the following condition. Let y ∈ Y .
5(c) (ν-variables, RHS is a modal formula) In the setting of
Cond. 5 of Def. 4.2, assume further that the formula ϕi is a
modal formula: ϕi = ♥λ (uj1 , . . . , ujn ).
Consider the approximant pi (α1 , . . . , αa , . . . , αk ) ∈ Ω of
p := r(y). There must exist ordinals β1 , . . . , βa−1 such that

5.2 CµΓ,Λ as a Linear-Time Logic
We take a modal language CµΓ,Λ whose modal signature Λ is over
F . Hence a CµΓ,Λ -formula ϕ specifies a property of F -behaviors,
where the latter are identified with elements z ∈ Z of a final
∼
=
coalgebra ζ : Z →
F Z. See §3.1.

pia (α1 , . . . , αa , . . . , αk ) v

PT♥λ (uj1 ,...,ujn ) (β1 , . . . , βa−1 , αa , . . . , αk ) (F r ◦ q)(y) ,
(18)
and β1 ≤ α, . . . , βa−1 ≤ α.
6. (Compatibility with c) For each y ∈ Y we have (F s ◦
q)(y) ∈ c(x). That is diagrammatically:

Definition 5.3 (semantics of the logic CµΓ,Λ over nondeterministic F -coalgebra). Let ϕ be a closed CµΓ,Λ -formula, and c : X →
PF X be a nondeterministic F -coalgebra. The denotation of ϕ
over c is given by a function JϕKc : X → P(Ω) defined by
tr(c)

J(JϕKζ )

p Z −→
p
JϕKc := X −→
Ω

(Existential) Linear-Time Model-Checking for CµΓ,Λ

FY
O

Jq _



Y

where: tr(c) is the infinitary trace semantics of c (Prop. 5.2); JϕKζ
is the denotation of ϕ over the (proper) F -coalgebra ζ : Z → F Z
defined in Def. 3.7; and J : Sets → K`(P) is the Kleisli inclusion
functor (§5.1).



F Js
⊆



Js

/ FX
_O c
/X

in K`(P),

(19)

where Jq : Y → PF Y is given by (Jq)(y) = {q(y)} (§5.1).
Theorem 5.6 (correctness of LTMC progress measure). Assume
the setting of Def. 5.5. In particular, the formula ϕ is translated to
an equational system with m variables.

Given a nondeterministic F -coalgebra c and its state x, a typical
question is whether some (or all) of its linear-time behaviors satisfy
a formula ϕ. This problem is the existential (or universal) modelchecking problem, respectively. In the current paper we focus on
existential model checking.

q

1. (Soundness) Let (α, Y → F Y, r, s) be an LTMC progress
measure. Let y ∈ Y be an arbitrary state, x := s(y) (a state
of the coalgebra c) and p := r(y) (a pre-progress measure).
Then there exists an infinitary trace z ∈ tr(c)(x) of x such
that pm (α, . . . , α) v JϕKζ (z). Here JϕKζ : Z → Ω is from
Def. 3.7.
2. (Completeness) Let x ∈ X, and z ∈ tr(c)(x) be an infinitary
q
trace from x. There is an LTMC progress measure (α, Y →
F Y, r, s) and some y ∈ Y such that s(y) = x, beh(q)(y) = z
and pm (α, . . . , α) = JϕKζ (z) where p := r(y). Here beh(q)
is the behavior map induced by finality (8).

Example 5.4. Take the combination of F, Ω, Γ and Λ in Example 3.3.6. A Kripke structure can then be thought of as a nondeterministic F -coalgebra.5 Recall that a final coalgebra is carried by
the set (P(AP))ω of computations; in this
 case the infinitary trace
semantics tr(c) : X → P (P(AP))ω is precisely the map that
carries each state x ∈ X to the set of computations that arise from
the paths from x.
4 Note

that “infinitary” does not mean that a behavior is necessarily of an
infinite length. For example, if F = {X} + A × ( ), a final F -coalgebra
is carried by the set Z = A∗ + Aω of all words over A of finite or infinite
length. All words (finite or infinite) are deemed to be “infinitary” traces.
5 A Kripke structure is most naturally modeled by a function c0 : X →

P(AP) × PX. This gives rise to a function c : X → P P(AP) × X
in an obvious way that turns state-labels into transition-labels, namely
c(x) = {((π1 ◦ c0 )(x), x0 ) | x0 ∈ (π2 ◦ c0 )(x)}.

The completeness result in the last theorem is not totally satisfactory, especially from an algorithmic point of view. The question
is the size of an LTMC progress measure: in the proof we used
Y ⊆ X × Z, but this can be very large—Z is an uncountable set
for most common functors F . Fortunately we have the following
theorem that cuts down the set Y from X × Z to X × pPMϕ,α
(that is potentially much smaller, especially when Ω = 2).

13

2016/1/12

Theorem 5.7 (small LTMC progress measure). Assume the setting
of Def. 5.5, and let x ∈ X. For any infinitary trace z ∈ tr(c)(x),
q
there exists an LTMC progress measure (α, Y → F Y, r, s) and
some y ∈ Y such that: s(y) = x, and pm (α, . . . , α) = JϕKζ (z)
q
where p := r(y). Moreover (α, Y → F Y, r, s) can be chosen so
that: Y ⊆ X × pPMϕ,α ; and r = π2 and s = π1 .

[2] A. Arnold and D. Niwiński. Rudiments of µ-Calculus. Studies in
Logic and the Foundations of Mathematics. Elsevier, Amsterdam,
2001.
[3] S. Awodey. Category Theory. Oxford Logic Guides. Oxford Univ.
Press, 2006.
[4] F. Bartels. On generalised coinduction and probabilistic specification
formats. Distributive laws in coalgebraic modelling. PhD thesis, Free
Univ. Amsterdam, 2004.

Our proof of the last theorem comes in a pumping flavor. In it, since
the relevant set is possibly infinite, we resort to Zorn’s lemma.
5.4

[5] A. M. Ben-Amram and S. Genaim. Complexity of Bradley-MannaSipma lexicographic ranking functions. In D. Kroening and C. S.
Pasareanu, editors, Computer Aided Verification - 27th International
Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015,
Proceedings, Part II, volume 9207 of Lecture Notes in Computer
Science, pages 304–321. Springer, 2015. ISBN 978-3-319-21667-6.
. URL http://dx.doi.org/10.1007/978-3-319-21668-3_18.

Decision Procedure

We exploit the previous results and derive a decision procedure
for linear-time CµΓ,Λ -model checking. We make the following
assumption; its justification is discussed shortly.
Assumption 5.8. In what follows we assume that the satisfiability
problem of CµΓ,Λ (against F -coalgebras) is decidable.
Moreover we assume the small model property: for each satisfiable CµΓ,Λ -formula ϕ, we can compute a natural number Nϕ ∈ ω
such that there exists an F -coalgebra that satisfies ϕ the size of
whose state space is no greater than Nϕ . That is: there exists a
coalgebra ε : E → F E, its state e ∈ E and an MC progress measure Q : E → pPMϕ,α (Def. 4.3) such that Q(e)(α, . . . , α) = tt
and |E| ≤ Nϕ . It is moreover guaranteed by Thm. 4.4.2 that we
can take α := Nϕ .
Finally, we assume that F preserves finiteness, that is, F B is
finite if B is finite.

[6] M. M. Bonsangue and A. Kurz. Duality for logics of transition
systems. In V. Sassone, editor, FoSSaCS, volume 3441 of Lect. Notes
Comp. Sci., pages 455–469. Springer, 2005. ISBN 3-540-25388-2.
[7] J. Bradfield and C. Stirling. Modal mu-calculi. In P. Blackburn, J. van
Benthem, and F. Wolter, editors, Handbook of Modal Logic, volume 3
of Studies in Logic and Practical Reasoning, chapter 12. Elsevier,
2006.
[8] K. Chatterjee and L. Doyen. Energy parity games. Theor. Comput.
Sci., 458:49–60, 2012. . URL http://dx.doi.org/10.1016/j.
tcs.2012.07.038.
[9] K. Chatterjee, M. Jurdzinski, and T. A. Henzinger. Quantitative
stochastic parity games. In J. I. Munro, editor, Proceedings of the Fifteenth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA
2004, New Orleans, Louisiana, USA, January 11-14, 2004, pages 121–
130. SIAM, 2004. ISBN 0-89871-558-X. URL http://dl.acm.
org/citation.cfm?id=982792.982808.

Assumption 5.8 is a mild one. For example, [16] shows that
the assumption holds when the logic CµΓ,Λ comes with a onestep complete, contraction-closed and exponentially-tractable set of
deductive rules. These conditions hold in well-known modal logics,
including (the fixed-point extensions of) the normal modal logic K,
and monotone modal logic (Example 3.3). Of more relevance here
is the fact that the assumption holds for (coalgebras of) polynomial
functors F (with suitable finiteness requirements), which are the
ones typically used to specify linear time behavior; modalities
and deductive rules for such functors can be modularly derived
from their structure, using an approach similar to that of [15], and
proving the tractability of the set of rules is straightforward in this
case.
It also seems that the framework in §4 can be adapted to satisfiability check and hence to the small-model property. Due to lack
of space we do not do so in the current paper and just assume the
small model property.

[10] B. F. Chellas. Modal Logic. Cambridge University Press, 1980.
[11] C. Cı̂rstea. Maximal traces and path-based coalgebraic temporal
logics. Theor. Comput. Sci., 412(38):5025–5042, 2011.
[12] C. Cı̂rstea. Model checking linear coalgebraic temporal logics: An
automata-theoretic approach. In A. Corradini, B. Klin, and C. Cı̂rstea,
editors, Algebra and Coalgebra in Computer Science - 4th International Conference, CALCO 2011, Winchester, UK, August 30 - September 2, 2011. Proceedings, volume 6859 of Lecture Notes in Computer
Science, pages 130–144. Springer, 2011. ISBN 978-3-642-22943-5. .
URL http://dx.doi.org/10.1007/978-3-642-22944-2_10.
[13] C. Cı̂rstea. A coalgebraic approach to linear-time logics. In Muscholl
[43], pages 426–440. ISBN 978-3-642-54829-1. . URL http:
//dx.doi.org/10.1007/978-3-642-54830-7.
[14] C. Cı̂rstea. Canonical coalgebraic linear time logics. In Proc. 6th
International Conference on Algebra and Coalgebra in Computer
Science (CALCO 2015), 2015. To appear.

Theorem 5.9 (linear-time CµΓ,Λ -model checking is decidable).
Assume the setting of Def. 5.5. Assume further that: Ω = 2; and X
is a finite set. Then it is decidable whether there exists an infinitary
trace z ∈ tr(c)(x) such that JϕKζ (z) = tt.

[15] C. Cı̂rstea and D. Pattinson. Modular construction of complete coalgebraic logics. Theor. Comput. Sci., 388(1-3):83–108, 2007. . URL
http://dx.doi.org/10.1016/j.tcs.2007.06.002.
[16] C. Cı̂rstea, C. Kupke, and D. Pattinson. EXPTIME tableaux for the
coalgebraic µ-calculus. In E. Grädel and R. Kahle, editors, CSL,
volume 5771 of Lecture Notes in Computer Science, pages 179–193.
Springer, 2009. ISBN 978-3-642-04026-9.

Acknowledgments
We thank Kenta Cho, Tetsuri Moriya, Shota Nakagawa, Jurriaan
Rot, and Natsuki Urabe for useful discussions. I.H. and S.S. are
supported by Grants-in-Aid No. 24680001 & 15KT0012, JSPS;
C.C. was supported by a Royal Society International Exchanges
Grant (IE131642).

[17] C. Cı̂rstea, A. Kurz, D. Pattinson, L. Schröder, and Y. Venema. Modal
logics are coalgebraic. Comput. J., 54(1):31–41, 2011.
[18] R. Cleaveland and B. Steffen. A linear-time model-checking algorithm
for the alternation-free modal mu-calculus. Formal Methods in System
Design, 2(2):121–147, 1993. . URL http://dx.doi.org/10.
1007/BF01383878.

References
[1] S. Almagor, U. Boker, and O. Kupferman. Formalizing and reasoning
about quality. In F. V. Fomin, R. Freivalds, M. Z. Kwiatkowska,
and D. Peleg, editors, Automata, Languages, and Programming - 40th
International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013,
Proceedings, Part II, volume 7966 of Lecture Notes in Computer
Science, pages 15–27. Springer, 2013. ISBN 978-3-642-39211-5. .
URL http://dx.doi.org/10.1007/978-3-642-39212-2_3.

[19] R. Cleaveland, M. Klein, and B. Steffen. Faster model checking
for the modal mu-calculus. In G. von Bochmann and D. K. Probst,
editors, Computer Aided Verification, Fourth International Workshop,
CAV ’92, Montreal, Canada, June 29 - July 1, 1992, Proceedings,
volume 663 of Lecture Notes in Computer Science, pages 410–422.
Springer, 1992. ISBN 3-540-56496-9. . URL http://dx.doi.org/
10.1007/3-540-56496-9_32.

14

2016/1/12

[20] P. Cousot and R. Cousot. Constructive versions of Tarski’s fixed point
theorems. Pacific Journal of Mathematics, 82(1):43–57, 1979.

[39] D. Kozen. Results on the propositional µ-calculus. Theor. Comp. Sci.,
27(3):333–354, 1983.

[21] L. de Alfaro, T. A. Henzinger, and R. Majumdar. Discounting the
future in systems theory. In J. C. M. Baeten, J. K. Lenstra, J. Parrow,
and G. J. Woeginger, editors, Automata, Languages and Programming,
30th International Colloquium, ICALP 2003, Eindhoven, The Netherlands, June 30 - July 4, 2003. Proceedings, volume 2719 of Lect. Notes
Comp. Sci., pages 1022–1037. Springer, 2003. ISBN 3-540-40493-7.

[40] S. Mac Lane. Categories for the Working Mathematician. Springer,
Berlin, 2nd edition, 1998.
[41] M. Mio. Upper-expectation bisimilarity and Łukasiewicz µ-calculus.
In Muscholl [43], pages 335–350. ISBN 978-3-642-54829-1. . URL
http://dx.doi.org/10.1007/978-3-642-54830-7_22.
[42] L. S. Moss. Coalgebraic logic. Ann. Pure & Appl. Logic, 96(1-3):
277–317, 1999. Erratum in Ann. Pure & Appl. Logic, 99(1-3):241–
259, 1999.

[22] K. Etessami, T. Wilke, and R. A. Schuller. Fair simulation relations,
parity games, and state space reduction for büchi automata. SIAM J.
Comput., 34(5):1159–1175, 2005.

[43] A. Muscholl, editor. Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, Held
as Part of the European Joint Conferences on Theory and Practice
of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, volume 8412 of Lecture Notes in Computer Science, 2014.
Springer. ISBN 978-3-642-54829-1. . URL http://dx.doi.org/
10.1007/978-3-642-54830-7.

[23] K. Fine. In so many possible worlds. Notre Dame J. Formal Logic,
13:516–520, 1972.
[24] G. Fontaine, R. A. Leal, and Y. Venema. Automata for coalgebras:
An approach using predicate liftings. In S. Abramsky, C. Gavoille,
C. Kirchner, F. Meyer auf der Heide, and P. G. Spirakis, editors, ICALP
(2), volume 6199 of Lecture Notes in Computer Science, pages 381–
392. Springer, 2010. ISBN 978-3-642-14161-4.

[44] S. Nakagawa and I. Hasuo. Near-optimal scheduling for LTL with
future discounting. In Trustworthy Global Computing - 10th International Symposium, TGC 2015, Lecture Notes in Computer Science.
Springer, 2015. to appear.

[25] P. Garg, C. Löding, P. Madhusudan, and D. Neider. ICE: A robust framework for learning invariants. In A. Biere and R. Bloem,
editors, Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL
2014, Vienna, Austria, July 18-22, 2014. Proceedings, volume 8559
of Lecture Notes in Computer Science, pages 69–87. Springer, 2014.
ISBN 978-3-319-08866-2. . URL http://dx.doi.org/10.1007/
978-3-319-08867-9_5.

[45] C. L. Ong. On model-checking trees generated by higher-order recursion schemes. In 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings,
pages 81–90. IEEE Computer Society, 2006. ISBN 0-7695-2631-4. .
URL http://dx.doi.org/10.1109/LICS.2006.38.

[26] I. Hasuo. Generic forward and backward simulations. In C. Baier
and H. Hermanns, editors, International Conference on Concurrency
Theory (CONCUR 2006), volume 4137 of Lect. Notes Comp. Sci.,
pages 406–420. Springer, Berlin, 2006.

[46] D. Pattinson. Coalgebraic modal logic: soundness, completeness
and decidability of local consequence. Theor. Comput. Sci., 309
(1-3):177–193, 2003. . URL http://dx.doi.org/10.1016/
S0304-3975(03)00201-9.

[27] I. Hasuo, B. Jacobs, and A. Sokolova. Generic trace semantics via
coinduction. Logical Methods in Comp. Sci., 3(4:11), 2007.

[47] D. Pattinson. The logic of exact covers: Completeness and uniform
interpolation. In 28th Annual ACM/IEEE Symposium on Logic in
Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28,
2013, pages 418–427. IEEE Computer Society, 2013. ISBN 978-14799-0413-6. . URL http://dx.doi.org/10.1109/LICS.2013.
48.

[28] C. Hermida and B. Jacobs. Structural induction and coinduction in a
fibrational setting. Inf. & Comp., 145:107–152, 1998.
[29] B. Jacobs. The temporal logic of coalgebras via Galois algebras. Math.
Struct. in Comp. Sci., 12:875–903, 2002.

[48] D. Pattinson and L. Schröder. Admissibility of cut in coalgebraic
logics. Electr. Notes Theor. Comput. Sci., 203(5):221–241, 2008. .
URL http://dx.doi.org/10.1016/j.entcs.2008.05.027.

[30] B. Jacobs. Trace semantics for coalgebras. In J. Adámek and S. Milius,
editors, Coalgebraic Methods in Computer Science, volume 106 of
Elect. Notes in Theor. Comp. Sci. Elsevier, Amsterdam, 2004.

[49] M. Pauly. A modal logic for coalitional power in games. J. Logic
Comput., 12(1):149–166, 2002.

[31] B. Jacobs. Introduction to coalgebra. Towards mathematics of states
and observations. Draft of a book (ver. 2.0), available online, 2012.

[50] A. Pnueli. The temporal logic of programs. In Found. Comp. Sci.,
pages 46–57. IEEE, 1977.

[32] B. Jacobs, A. Silva, and A. Sokolova. Trace semantics via determinization. J. Comput. Syst. Sci., 81(5):859–879, 2015. . URL
http://dx.doi.org/10.1016/j.jcss.2014.12.005.

[51] J. Power and D. Turi. A coalgebraic foundation for linear time
semantics. In Category Theory and Computer Science, volume 29
of Elect. Notes in Theor. Comp. Sci. Elsevier, Amsterdam, 1999.

[33] M. Jurdzinski. Small progress measures for solving parity games.
In H. Reichel and S. Tison, editors, STACS, volume 1770 of Lecture
Notes in Computer Science, pages 290–301. Springer, 2000. ISBN
3-540-67141-2.

[52] J. J. M. M. Rutten. Universal coalgebra: a theory of systems. Theor.
Comp. Sci., 249:3–80, 2000.
[53] L. Schröder and D. Pattinson. Pspace bounds for rank-1 modal logics.
ACM Trans. Comput. Log., 10(2), 2009.

[34] H. Kerstan and B. König. Coalgebraic trace semantics for continuous probabilistic transition systems. Logical Methods in Computer Science, 9(4), 2013. . URL http://dx.doi.org/10.2168/
LMCS-9(4:16)2013.

[54] L. Schröder and Y. Venema. Flat coalgebraic fixed point logics. In
P. Gastin and F. Laroussinie, editors, CONCUR, volume 6269 of Lect.
Notes Comp. Sci., pages 524–538. Springer, 2010. ISBN 978-3-64215374-7.

[35] N. Klarlund and D. Kozen. Rabin measures and their applications
to fairness and automata theory. In Proceedings of the Sixth Annual
Symposium on Logic in Computer Science (LICS ’91), Amsterdam,
The Netherlands, July 15-18, 1991, pages 256–265. IEEE Computer
Society, 1991. ISBN 0-8186-2230-X. . URL http://dx.doi.org/
10.1109/LICS.1991.151650.

[55] T. Tsukada and C. L. Ong. Compositional higher-order model checking via ω-regular games over böhm trees. In T. A. Henzinger and
D. Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the TwentyNinth Annual ACM/IEEE Symposium on Logic in Computer Science
(LICS), CSL-LICS ’14, Vienna, Austria, July 14 - 18, 2014, pages
78:1–78:10. ACM, 2014. ISBN 978-1-4503-2886-9. . URL http:
//doi.acm.org/10.1145/2603088.2603133.

[36] B. Klin. Coalgebraic modal logic beyond Sets. In MFPS XXIII,
volume 173, pages 177–201. Elsevier, Amsterdam, 2007.
[37] N. Kobayashi and C.-H. L. Ong. A type system equivalent to the modal
mu-calculus model checking of higher-order recursion schemes. In
LICS, pages 179–188. IEEE Computer Society, 2009. ISBN 978-07695-3746-7.

[56] N. Urabe and I. Hasuo. Generic forward and backward simulations III: quantitative simulations by matrices. In P. Baldan and
D. Gorla, editors, CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy, September 25, 2014. Proceedings, volume 8704 of Lecture Notes in Computer

[38] A. Kock. Strong functors and monoidal monads. Arch. Math., XXIII:
113–120, 1972.

15

2016/1/12

Science, pages 451–466. Springer, 2014. ISBN 978-3-662-44583-9.
. URL http://dx.doi.org/10.1007/978-3-662-44584-6_31.
Best paper award.
[57] N. Urabe and I. Hasuo. Coalgebraic infinite traces and Kleisli simulations. In Proc. 6th International Conference on Algebra and Coalgebra in Computer Science (CALCO 2015), Leibniz International Proceedings in Informatics, 2015. To appear; extended version available
at http://arxiv.org/abs/1505.06819.

A.

In Case of Parity Games: Correspondence to
Jurdzinski’s Notion

[58] M. Y. Vardi. An automata-theoretic approach to linear temporal
logic. In F. Moller and G. M. Birtwistle, editors, Banff Higher Order
Workshop, volume 1043 of Lecture Notes in Computer Science, pages
238–266. Springer, 1995. ISBN 3-540-60915-6.
[59] Y. Venema. Automata and fixed point logic: A coalgebraic perspective.
Inf. Comput., 204(4):637–678, 2006.
[60] T. Wilke. Alternating tree automata, parity games, and modal µcalculus. Bull. Belg. Math. Soc. Simon Stevin, 8(2):359–391, 2001.

Definition A.1 (parity game). A parity game is a quadruple G =
(Xeven , Xodd , E, pr) of: a finite set Xeven of the player even’s positions; a finite set Xodd of the player odd’s positions; a transition
relation E ⊆ X × X where X := Xeven ∪ Xodd is the set of all
the positions; and a priority function pr : X → {1, 2, . . . , d} for
some d ∈ ω. The following are additionally assumed, mostly for
simplicity: the sets Xeven and Xodd are disjoint; X is nonempty;
each position has at least one E-successor; d is an even number.
Note, however, that whether x ∈ X is even’s position or odd’s is
independent from if pr(x) ∈ [1, d] is even or odd.
A play of G is an infinite sequence x0 x1 . . . of positions such
that (xi , xi+1 ) ∈ E for each i ∈ ω. A play x0 x1 . . . is winning for
the player even if

sup k ∈ {1, 2, . . . , d} k = pr(xi ) for infinitely many i ∈ ω

Here, as a sanity check, we shall show that our notion of progress
measure (Def. 2.12) instantiates to Jurdzinski’s parity progress
measure [33], in the special case where an equational system is
induced by a parity game.
The following definitions are all standard. See e.g. [33].

is an even number.
A strategy σ of the player even is a function σ : X ∗ × Xeven →
X, with the intuition that even chooses his move σ(~
x, x) depending
on the history ~
x of the positions already visited, and the current
position x ∈ Xeven . A play x0 x1 . . . conforms to a strategy σ of
even if, for each i ∈ ω such that xi ∈ Xeven we have xi+1 =
σ(x0 x1 . . . xi−1 , xi ). A winning strategy for the player even is a
strategy σ such that every play that conforms to σ is winning for
even. Finally, a position x ∈ X is winning for even if there exists
a winning strategy for even.
The following notion is precisely the one in [33], modulo some
minor modifications that are made for the fit to the current context.
Definition A.2 (parity progress measure). Let G be a parity game
G = (Xeven , Xodd , E, pr); let X = Xeven qXodd . A parity progress
measure for G is a function q : X → ω d/2 q {♠}, where ♠ is a
fresh symbol, such that:
• The a-th component of the tuple q(x) is never bigger than the

number
 n2a−1 of the positions of the priority 2a − 1. That is,
q(x) a ≤ n2a−1 := | pr−1 (2a − 1)| (or q(x) = ♠) for each
a ∈ [1, d/2].
• If x ∈ Xeven , then there exists a successor y of x such that:
q(x) pr(x) q(y)
q(x) pr(x) q(y)

if pr(x) is odd;
if pr(x) is even.

Here the order pr(x) is the same as in Def. 2.10, except that ♠
is assumed to be the greatest element.
• If x ∈ Xodd , then for any successor y of x we have
q(x) pr(x) q(y)
q(x) pr(x) q(y)

if pr(x) is odd;
if pr(x) is even.

A parity game gives rise to an equational system. The latter
is over (a product of) the Boolean lattice 2 = {tt, ff}—tt means
“even is winning.”
Definition A.3 (equaltional system EG from a game G). Let G =
(Xeven , Xodd , E, pr) be a parity game. For each priority i ∈ [1, d],
let ni ∈ ω be the number of positions with a priority i, that
is, ni = |{x ∈ X | pr(x) = i}|. Furthermore, let us fix an
enumeration
x1,1 , . . . , x1,n1 , x2,1 , . . . , x2,n2 , . . . , xd,1 , . . . , xd,nd
16

(20)

2016/1/12

check Cond. 3, let us first consider the case when x2a−1,j ∈ Xodd .

of all positions of G; it is arranged so that pr(xi,j ) = i.
The equational system EG induced by G is with variables
u1 , . . . , ud —we have one variable for each priority i ∈ [1, d]—
where each variable ui takes its value in the complete lattice 2ni .6
Concretely, the system EG is of the form

x2a−1,j ∈ p2a−1 (α1 , . . . , αa + 1, . . . , αd/2 )
⇐⇒ q(x2a−1,j ) 2a−1 (α1 , . . . , αa + 1, . . . , αd/2 )
=⇒ for each successor y of x2a−1,j ,
q(y) ≺2a−1 (α1 , . . . , αa + 1, . . . , αd/2 )
(by q(x2a−1,j ) 2a−1 q(y))

u)
u1 =η1 f1 (~
u) , . . . , ud =ηd fd (~
(†)

=⇒ for each successor y of x2a−1,j ,

where ηi and fi are defined as follows.

q(y) 2a−1 (α1 , . . . , αa , . . . , αd/2 )
⇐⇒ for each successor y of x2a−1,j ,
y ∈ p(α1 , . . . , αa , . . . , αd/2 ) (by def. of p)


p1 (α1 , . . . , αa , . . . , αd/2 ),
,
...,
⇐⇒ x2a−1,j ∈ f2a−1 
pd (α1 , . . . , αa , . . . , αd/2 )

• The fixed-point symbol ηi is ν if i is even; it is µ if i is odd.
• The monotone function fi : 2n1 × · · · × 2nd → 2ni is defined,

for each j ∈ [1, ni ], by:

fi (u1 , . . . , ud ) j :=
( F
π 0 (u 0 ) (xi,j , xi0 ,j 0 ) ∈ E
d j i
πj 0 (ui0 ) (xi,j , xi0 ,j 0 ) ∈ E

(21)
as required. Here (†) holds since (α1 , . . . , αa , . . . , αd/2 ) is the
greatest among those which are strictly ≺2a−1 -smaller than the
prioritized ordinal (α1 , . . . , αa + 1, . . . , αd/2 ). The case when
x2a−1,j ∈ Xeven is similar, replacing the three occurrences of
“each” by “some” in (21). There is no need of showing Cond. 4
since every αa in question is finite. Cond.
 5 is shown much like
in (21). Finally, that pi (α1 , . . . , αd/2 ) j = tt, that is, x = xi,j ∈
pi (α1 , . . . , αd/2 ), follows immediately by q(x) 6= ♠.
For the opposite direction, we first use Thm. 2.13—soundness,
and then completeness—to obtain a “small” progress measure, that
is, one such that αa ≤ ascCL(L2a−1 ) for each a ∈ [1, d/2].
(Recall that we are using an immediate generalization of Thm. 2.13
where different variables ui are allowed to take values in different
lattices Li ). Now L2a−1 = 2n2a−1 yields ascCL(L2a−1 ) =
n2a−1 : in a strictly ascending chain, each subset is at least one
element bigger than its previous step. This gives us a small progress
measure p such that αa ≤ n2a−1 .
This p is used to define a parity progress measure q : X → ω d/2
by:

q(x) := min (α1 , . . . , αd ) x ∈ p(α1 , . . . , αd ) ,

if xi,j ∈ Xeven ,
if xi,j ∈ Xodd .

F
d
Here
and
denotes a supremum and an infimum, respectively, in the complete lattice 2.
We are ready to show that our notion of progress measure
generalizes Jurdzinski’s [33]. We use the extension in Def. 2.14.
Proposition A.4. Let G be a parity game; let EG be the equational
system that arises from G (Def. A.3). Let x be an arbitrary position
of G, and assume that x = xi,j in the enumeration (20) (in
particular pr(x) = i).
Let q : X → ω d/2 be a parity progress measure for G (Def. A.2)
such that q(x) 6= ♠. Then this q gives rise to an extended progress
measure p (in the sense of Def. 2.14) such that: regarding the
maximum prioritized ordinal we have αa ≤ n2a−1 for each a ∈
[1, d/2]; and pi (α1 , . . . , αd/2 ) j = tt.
Conversely, let p be a progress measure for
 EG (in the sense
of Def. 2.12) that satisfies pi (α1 , . . . , αd/2 ) j = tt. It gives rise
to a parity progress measure q for the parity game G such that
q(x) 6= ♠.

where the minimum is taken with respect to the lexicographic order
 (the latter an element is, the more significant it is), and the
minimum of the empty set is defined to be ♠. It is easy to check
that the q is indeed what is desired.
Corollary A.5. A position x = xi,j of a parity game G is winning
for the player even if and only if the solution (Def. 2.7) of EG has
it that lisol (j) = tt.

Proof. In what follows we shall identify an element pi ∈ 2ni with
a subset pi ⊆ {xi,1 , . . . , xi,ni }, and furthermore identify a tuple
(p1 , . . . , pd ) ∈ 2n1 × · · · × 2nd with a subset p ⊆ X.
For the former direction, assume that q : X → ω d/2 is such
a parity progress measure. We define a progress measure p by:
αa := n2a−1 for each a ∈ [1, d/2], and

Proof. Immediately from Prop. A.4, Thm. 2.13 and the correctness
of parity progress measures [33, Cor. 7–8].

def.

xi,j ∈ pi (α1 , . . . , αd/2 ) ⇐⇒ q(xi,j ) i (α1 , . . . , αd/2 ),

B.

Omitted Proofs

B.1

Proof of Thm. 2.13

Proof. The item 1 (soundness). We shall prove the following
claim (∗) by induction on i. This obviously suffices, by the defisol
nition of (l1sol , . . . , lm
) (Def. 2.7).

Checking that thus defined p is indeed an (extended) progress
measure is not hard. Monotonicity (Cond. 1 of Def. 2.12) follows
from the transitivity of i . Cond. 2’ (see Def. 2.14) is easy, too. To

(∗) For each i ∈ [1, m] the following holds: for each
j ∈ [1, i], and for each prioritized ordinal (α1 , . . . , αk )
such that α1 ≤ α1 , . . . , αk ≤ αk ,


pi+1 (α1 , . . . , αk ),
(i) 
 , (22)
...,
pj (α1 , . . . , αk ) v lj
pm (α1 , . . . , αk )

6 Therefore

we shall use the extension of the theory developed in the above
that allows different variables ui to take values in different lattices Li . As
mentioned just after Def. 2.6, such extension is easy.

17

2016/1/12



(i)

where lj : Lm−i → L is the i-th interim solution in
Def. 2.7.





v fi 




In the following proof by induction on i, we distinguish cases,
according to whether ui is a µ-variable or a ν-variable. There is
no need of distinguishing the base case (i = 1) from the step case:
it is easy to take proper care of the occurrences of i − 1 in the proof
below.
Case: ui is a µ-variable. Let us choose a ∈ [1, k] so that i =
ia , that is, the variable ui currently in question has the a-th smallest
priority among all the µ-variables.
Our proof of the claim (∗) shall follow the following path. We
will first consider the special case (∗)j=i of the claim (∗) where
j is fixed to be j = i. Then we will show the inequality (22)
by (transfinite) induction. The general claim (∗) for the other j ∈
[0, i − 1] will be derived from this special case j = i.
Let us fix j = i in the claim (∗); thus we set out to prove the
following claim (∗)j=i .











for some ordinals β1 , . . . , βa−1 , by Cond. 3 of Def. 2.12



pi (β1 , . . . , βa−1 , αa0 , αa+1 , . . . , αk ),
0
 (i−1)  pi+1 (β1 , . . . , βa−1 , αa , αa+1 , . . . , αk ), 
 l1

,
...,


0
pm (β1 , . . . , βa−1 , αa , αa+1 , . . . , αk )


...,




pi (β1 , . . . , βa−1 , αa0 , αa+1 , . . . , αk ),

0
v fi 
(i−1)  pi+1 (β1 , . . . , βa−1 , αa , αa+1 , . . . , αk ), 
 li−1

,

...,


pm (β1 , . . . , βa−1 , αa0 , αa+1 , . . . , αk )

pi (β1 , . . . , βa−1 , αa0 , αa+1 , . . . , αk ),


pi+1 (β1 , . . . , βa−1 , αa0 , αa+1 , . . . , αk ),


...,

(∗)j=i
For each prioritized ordinal (α1 , . . . , αk ) such
that α1 ≤ α1 , . . . , αk ≤ αk ,


pi+1 (α1 , . . . , αk ),
(i)
 . (23)
...,
pi (α1 , . . . , αk ) v li 
pm (α1 , . . . , αk )






















pm (β1 , . . . , βa−1 , αa0 , αa+1 , . . . , αk )

by the induction hypothesis (the claim (∗) for i − 1)


 
pi (β1 , . . . , βa−1 , αa0 , αa+1 , . . . , αk ),
 (i−1) 
pi+1 (0, . . . , 0, αa+1 , . . . , αk ),
 
 l1

, 
...,




pm (0, . . . , 0, αa+1 , . . . , αk )




.
.
.
,




0


pi (β1 , . . . , βa−1 , αa , αa+1 , . . . , αk ),



p
(0,
.
.
.
,
0,
α
,
.
.
.
,
α
),
= fi 


(i−1)
i+1
a+1
k
 li−1 
,
 


.
.
.
,




pm (0, . . . , 0, αa+1 , . . . , αk )


0
pi (β1 , . . . , βa−1 , αa , αa+1 , . . . , αk ),




pi+1 (0, . . . , 0, αa+1 , . . . , αk ),




...,
pm (0, . . . , 0, αa+1 , . . . , αk )
by monotonicity (Cond. 1 of Def. 2.12), much like in (†) in (24)

= Φ pi (β1 , . . . , βa−1 , αa0 , αa+1 , . . . , αk )

(i)

We first note a fact that follows from the definition of li
(i)
(Def. 2.7) and Lem. 2.1.1: the right-hand side li (. . . ) of the
claimed inequality (23) is given a lower bound by Φα (⊥), where α
is an arbitrary ordinal and Φ : L → L is defined by


l,
 p (α , . . . , αk ), 
Φ(l) := fi‡  i+1 1

...,
pm (α1 , . . . , αk )


l,
(†) ‡  pi+1 (0, . . . , 0, αa+1 , . . . , αk ), 
= fi 

...,
pm (0, . . . , 0, αa+1 , . . . , αk )


 
l,
 (i−1)  pi+1 (0, . . . , 0, αa+1 , . . . , αk ),  
 l1

, 
...,




pm (0, . . . , 0, αa+1 , . . . , αk )




.
.
.
,


 


l,


,
p
(0,
.
.
.
,
0,
α
,
.
.
.
,
α
),
= fi 


(i−1)
i+1
a+1
k
 li−1

,




.
.
.
,




pm (0, . . . , 0, αa+1 , . . . , αk )


l,




p
(0,
.
.
.
,
0,
α
,
.
.
.
,
α
),
i+1
a+1
k




...,
pm (0, . . . , 0, αa+1 , . . . , αk )
(24)
where the second equality (†) holds due to Cond. 1 (monotonicity)
of Def. 2.12, and that (α1 , . . . , αk ) =b (0, . . . , 0, αa+1 , . . . , αk )
for each b ∈ [i + 1, m] (cf. Def. 2.10). In particular, the definition
of Φ relies on αa+1 , . . . , αk but not on αa .
We shall show, by (transfinite) induction on the ordinal αa , that
pi (α1 , . . . , αa , . . . , αk ) v Φαa (⊥)

p1 (β1 , . . . , βa−1 , αa0 , αa+1 , . . . , αk ),
...,
pi−1 (β1 , . . . , βa−1 , αa0 , αa+1 , . . . , αk ),
pi (β1 , . . . , βa−1 , αa0 , αa+1 , . . . , αk ),
pi+1 (β1 , . . . , βa−1 , αa0 , αa+1 , . . . , αk ),
...,
pm (β1 , . . . , βa−1 , αa0 , αa+1 , . . . , αk )

by def. of Φ, see (24)
= Φ pi (α1 , . . . , αa−1 , αa0 , αa+1 , . . . , αk )



by monotonicity, much like the second last equality
0

v Φαa +1 (⊥)

by the induction hypothesis (25).

Finally, if αa in (25) is a limit ordinal, then
pi (α1 , . . . , αa , αa+1 . . . , αk )
G
v
pi (α1 , . . . , β, αa+1 . . . , αk )

by Cond. 4 of Def. 2.12

β<αa

v

G

Φβ (⊥) by the induction hypothesis (25)

β<αa

= Φαa (⊥) by def. of Φαa .
This concludes the proof that the inequality (25) holds for any
ordinal αa . By the fact that Φαa (⊥) is a lower bound for the righthand side of (23) (that is argued after the inequality (23)), we have
now shown that the claim (∗)j=i holds.
Finally, the general claim (∗) for any j ∈ [1, i − 1] (other than
j = i) is shown as follows.

(25)

for each ordinal αa such that αa ≤ αa . If αa = 0, then the lefthand side of (25) is ⊥—this is Cond. 2 of Def. 2.12.
If αa is a successor ordinal αa0 + 1, then
pi (α1 , . . . , αa0 + 1, αa+1 . . . , αk )

pj (α1 , . . . , αk )

18

2016/1/12


pi (α1 , . . . , αk ),
(i−1)  pi+1 (α1 , . . . , αk ), 
v lj


...,
pm (α1 , . . . , αk )
by the induction hypothesis (the claim (∗) for i − 1)

 

pi+1 (α1 , . . . , αk ),
(i) 
, 
 li
...,


pm (α1 , . . . , αk )

(i−1) 
v lj




pi+1 (α1 , . . . , αk ),


...,
pm (α1 , . . . , αk )


where the last equality is, once again, a consequence of monotonicity (Cond. 1 of Def. 2.12) and that (β1 , . . . , βa−1 , αa . . . , αk ) =i
(α1 , . . . , αk ). This concludes the proof of Thm. 2.13.1.
The item 2 (completeness). The proof is by induction on the
number m of equations in the equational system E. For each
l ∈ L, let E (l) be the equational system obtained from E in (1) by
removing the last equation and substituting l for the last variable
um . That is,


u1 =η1 f1 (u1 , . . . , um−1 , l),
(l)
.
...,
(27)
E
:= 
um−1 =ηm−1 fm−1 (u1 , . . . , um−1 , l)

by the claim (∗)j=i (that we have already shown for the current i)


pi+1 (α1 , . . . , αk ),
(i) 

...,
= lj
pm (α1 , . . . , αk )

For the rest of the proof we distinguish cases, depending on
whether the last variable um is a µ-variable or a ν-variable.
Case: um is a µ-variable. By the induction hypothesis there
exists a progress measure that achieves the exact solution of the
system E (l) , for each l ∈ L. Such a progress measure shall be
denoted by

(i)

by the definition (2) of lj ; see Def. 2.7.
This concludes one case of our proof of the claim (∗) (by induction
on i), where ui is a µ-variable.
Case: ui is a ν-variable. Let us choose a ∈ [1, k] so that

p(l) =
(l)

(l)

(l)

(α1 , . . . , αk−1 ), pi (α1 , . . . , αk−1 )

i1 < · · · < ia−1 < i < ia < · · · < ik .
We shall prove the special case of (∗) where j = i. The claim
(∗) for general j ∈ [1, i] follows from this special case, much like
in the above for the case where ui is a µ-variable.
(i)
By the definition of li (Def. 2.7) and Lem. 2.1.2, showing the
following (i.e. pi (α1 , . . . , αk ) is a suitable postfixed point) suffices
for establishing the desired inequality (22):


pi (α1 , . . . , αk ),
 p (α , . . . , αk ), 
pi (α1 , . . . , αk ) v fi‡  i+1 1
(26)
.
...,
pm (α1 , . . . , αk )


i∈[1,m−1],α1 ,...,αk−1


.

(Note here that E (l) has k − 1 µ-variables, since E has k of such
and we assumed that um is a µ-variable.) It is easily seen to satisfy,
for each i ∈ [1, m − 1]:
(l)

pi

(l)

(l)

α1 , . . . , αk−1



(m−1)

= li

(l),

(28)

(m−1)

where li
(l) is (a component of) the (m−1)-th interim solution
of the original equational system E (Def. 2.7). Furthermore, by
(l)
induction, we assume that αa ≤ ascCL(L) for each a ∈ [1, k−1].
Using the above data, we shall construct a desired progress measure p for the system E. We define its approximants pi (α1 , . . . , αk )
by induction on the ordinal αk . For the base case:

We proceed as follows.
pi (α1 , . . . , αk )


p1 (β1 , . . . , βa−1 , αa , . . . , αk ),

...,
v fi 
pm (β1 , . . . , βa−1 , αa , . . . , αk )

pm (α1 , . . . , αk−1 , 0) := ⊥,
(pm (α1 ,...,αk−1 ,0))

pi (α1 , . . . , αk−1 , 0) := pi
=

for some ordinals β1 , . . . , βa−1 , by Cond. 5 of Def. 2.12


 
pi (β1 , . . . , βa−1 , αa . . . , αk ),
 (i−1)  pi+1 (β1 , . . . , βa−1 , αa . . . , αk ),  
 l1

, 
...,




pm (β1 , . . . , βa−1 , αa . . . , αk )




.
.
.
,






pi (β1 , . . . , βa−1 , αa . . . , αk ),

v fi 
 (i−1)  pi+1 (β1 , . . . , βa−1 , αa . . . , αk ),  
 li−1 
, 


...,


pm (β1 , . . . , βa−1 , αa . . . , αk )




pi (β1 , . . . , βa−1 , αa . . . , αk ),




...,
pm (β1 , . . . , βa−1 , αa . . . , αk )

(⊥)
pi (α1 , . . . , αk−1 )

(α1 , . . . , αk−1 )

for each i ∈ [1, m − 1].

‡
For the step case we use the function fm−1
from Def. 2.7 and define

‡
pm (α1 , . . . , αk−1 , αk + 1) := fm
pm (α1 , . . . , αk−1 , αk ) ,

pi (α1 , . . . , αk−1 , αk + 1) :=
( pm (α1 ,...,αk−1 ,αk +1) )

pi

(α1 , . . . , αk−1 ) for each i ∈ [1, m − 1].

For the limit case, similarly, we define
G
pm (α1 , . . . , αk−1 , αk ) :=
pm (α1 , . . . , αk−1 , β),
β<αk
( pm (α1 ,...,αk−1 ,αk ) )

pi (α1 , . . . , αk−1 , αk ) := pi

by the induction hypothesis (the claim (∗) for i − 1)


pi (β1 , . . . , βa−1 , αa . . . , αk ),
‡

...,
= fi
pm (β1 , . . . , βa−1 , αa . . . , αk )

(α1 , . . . , αk−1 )

for each i ∈ [1, m − 1].
(29)
In the above definitions it may happen that p(l) (α1 , . . . , αk−1 ) is
not defined because the ordinals α1 , . . . , αk−1 exceed the domain
(l)
of p(l) , that is, αi < αi for some i ∈ [1, k − 1]. In such a case
we use, in place of (α1 , . . . , αk−1 ), the greatest prioritized ordinal
that is smaller than it (with respect to the lexicographic order  in
Def. 2.10).
Regarding the maximum prioritized ordinal (α1 , . . . , αk ) of p:

by def. of fi‡ (Def. 2.7)


pi (α1 , . . . , αk ),
,
...,
= fi‡ 
pm (α1 , . . . , αk )

19

2016/1/12

• On the ordinal αk for the last µ-variable um , the approximants

other i (i.e. i ∈ [1, m − 1]):

for um form a (transfinite) ascending chain

sol
) by Def. 2.7
lisol = lim−1 (lm

pm (α1 , . . . , αk−1 , 0) v pm (α1 , . . . , αk−1 , 1) v · · · ;
(30)
‡
‡
‡
because the chain is nothing but ⊥ v fm
(⊥) v fm
(fm
(⊥)) v
· · · . This chain in the complete lattice L eventually stabilizes
(bounded by the ordinal ascCL(L), by the definition of the
latter); we let αk to be an ordinal, such that αk ≤ ascCL(L), at
which the chain (30) has stabilized.
• On the other ordinals αa for a ∈ [1, k − 1], we define
_ (pm (α1 ,...,α ,β))
k−1
αa :=
αa
;
(31)

(lsol )

= pi m

(lsol )

(lsol )

m
α1 m , . . . , αk−1



by (28)

(pm (α1 ,...,αk ))

α1

(pm (α1 ,...,αk ))

α1 , . . . , αk−1

= pi
= pi

(pm (α1 ,...,αk ))

(p

(α1 ,...,αk ))

m
, . . . , αk−1





by the convention we adopted just after (29)
= pi (α1 , . . . , αk )

by def. of pi .

This concludes the case where um is a µ-variable.
Case: um is a ν-variable. The proof in this case is similar and
simpler. We shall therefore describe only its main points; further
details can be easily filled out.
By the induction hypothesis there exists a progress measure p(l)
that achieves the exact solution of the system E (l) , for each l ∈ L:

β≤αk
(l)

it is obvious, from the induction hypothesis that αa ≤
ascCL(L) for each l ∈ L and a ∈ [1, k − 1], that αa in (31) is
no bigger than ascCL(L).

p(l) =

We have to check that the data p thus defined is indeed a
progress measure (Def. 2.12). On Cond. 1 (monotonicity): it holds
if i = m because (30) is an ascending chain; for i ∈ [1, m − 1] the
claim follows from the induction hypothesis that p(l) is a progress
measure for E (l) . Cond. 2 is easy, distinguishing cases for a = k
(obvious by definition) and a ∈ [1, k − 1] (by the induction
hypothesis).
On Cond. 3, let a = k (hence ia = m). Then

(l)

(l)

(l)

(α1 , . . . , αk ), pi (α1 , . . . , αk )


i∈[1,m−1],α1 ,...,αk


.

(Note that E (l) has k µ-variables.) We use such p(l) to define a
desired progress measure p of E. Its approximants are defined by:
sol
pm (α1 , . . . , αk ) := lm
,
( lsol
m )

pi (α1 , . . . , αk ) := pi

pm (α1 , . . . , αk−1 , αk + 1)
‡
pm (α1 , . . . , αk−1 , αk )
by definition
= fm

 (m−1)
( pm (α1 , . . . , αk−1 , αk ) ) ,
l1


...,

= fm 
 l(m−1) ( pm (α1 , . . . , αk−1 , αk ) ) , 
m−1
pm (α1 , . . . , αk−1 , αk )

 (pm (α1 ,...,αk−1 ,αk ))
(β1 , . . . , βk−1 ),
p1


...,

= fm 

 p(pm (α1 ,...,αk−1 ,αk )) (β , . . . , β
1
k−1 ),
m−1
pm (α1 , . . . , αk−1 , αk )
for some ordinals β1 , . . . , βk−1 , by (28)

 (pm (β1 ,...,βk−1 ,αk ))
(β1 , . . . , βk−1 ),
p1


(†)
...,

= fm 

 p(pm (β1 ,...,βk−1 ,αk )) (β , . . . , β
1
k−1 ),
m−1
pm (β1 , . . . , βk−1 , αk )


p1 (β1 , . . . , βk−1 , αk ),
...,


= fm 
pm−1 (β1 , . . . , βk−1 , αk ), 
pm (β1 , . . . , βk−1 , αk )

(α1 , . . . , αk ) for each i ∈ [1, m − 1].

Regarding the maximum prioritized ordinal (α1 , . . . , αk ), we de-



(lsol )

fine αa := αa m for each a ∈ [1, k]. Obviously, from the induction hypothesis, αa can be chosen so that αa ≤ ascCL(L).
In seeing that p is indeed a progress measure, checking the
conditions of Def. 2.12 is mostly straightforward by the induction
hypothesis. The only nontrivial point is Cond. 5, in case i = m. We
have to show that


p1 (β1 , . . . , βk ),
.
.
.
,


sol
lm
v fm  p
(32)

m−1 (β1 , . . . , βk ),
sol
lm
for some ordinals β1 , . . . , βk (note that all the µ-variables have
(lsol )

priorities smaller than that of um ). We set βa := αa m for each
a ∈ [1, k]. Then the right-hand side of (32) becomes:


(lsol )
(lsol )
(lsol )
p1 m (α1 m , . . . , αk m ),


...,


fm  (lsol ) (lsol )

sol
 p m (α m , . . . , α(lm ) ), 
m−1

by def. of p1 , . . . , pm−1 ,

(m−1)

= f m l1

1

sol
lm

k

(m−1)

sol
sol
sol
(lm
), . . . , lm−1 (lm
), lm



‡
sol
as required. Here the equality (†) holds since the first k − 1 argu= fm
(lm
) by Def. 2.7
ments do not matter in the definition of pm , that is, pm (α1 , . . . , αk−1 , αk ) =
sol
= lm ,
pm (β1 , . . . , βk−1 , αk ) (this is easily seen by induction on αk ). On
Cond. 3, if a ∈ [1, k − 1], the claim follows immediately by the
(m)
sol
where the last equality is because of the definition of lm
= lm as
induction hypothesis. Cond. 4 is easy, by definition for a = k and
a
greatest
fixed
point
(Def.
2.7).
This
proves
(32).
by the induction hypothesis for a ∈ [1, k − 1]. Cond. 5 is easy,
It is straightforward to show that the progress measure p indeed
too, by the induction hypothesis (we have assumed that um is a
achieves the exact solution. This completes the proof.
µ-variable).
Finally, we have to show that the progress measure p deB.2 Proof of Prop. 2.15
fined in the above indeed achieves the exact solution, that is,
sol
pi (α1 , . . . , αk ) = li for each i ∈ [1, m]. For i = m
Proof. The structure of the proof remains the same; we shall focus
sol
this is easy: lm
is characterized as the supremum of the chain
on what is changed.
‡
‡
‡
⊥ v fm
(⊥) v fm
(fm
(⊥)) v · · · (Def. 2.7 and Lem. 2.1.1); and
Let us denote the function Φ in (24) by Φαa+1 ,...,αk , so that
the last chain coincides, by definition, with the one in (30). For the
its dependence on αa+1 , . . . , αk becomes explicit. We shall prove,

20

2016/1/12

instead of (25), the following claim:

B.4

pi (α1 , . . . , αa , . . . , αk ) v (Φαa+1 ,...,αk )α (⊥) for some α
(33)
by transfinite induction on a tuple αa , αa+1 , . . . , αk (ordered lexicographically with , with the latter being the more significant).
For one base case, assume αa = 0 and pia (α1 , . . . , αk ) = ⊥.
For example this must be the case, by Def. 2.14, when αa =
αa+1 = · · · = αk = 0—this is because there is no (α10 , . . . , αk0 )
such that (α10 , . . . , αk0 ) ≺ia (α1 , . . . , αk ). In this case (33) holds
with α = 0.
For the other base case, assume that αa = 0 and there exists (α10 , . . . , αk0 ) such that (α10 , . . . , αk0 ) ≺ia (α1 , . . . , αk ) and
pia (α1 , . . . , αk ) v pia (α10 , . . . , αk0 ). The former condition means
(αa0 , . . . , αk0 ) ≺ (αa , . . . , αk ) with the lexicographic order ≺; by
the induction hypothesis, therefore, we have pi (α10 , . . . , αa0 , . . . , αk0 ) v
0
(Φα0a+1 ,...,α0k )α (⊥) for some α0 . It follows easily from Cond. 1
that Φαa+1 ,...,αk is monotonic with respect to the ordinals αa+1 , . . . , αk .
Summarizing, we have

Proof. Straightforward from the naturality of λ along the arrow
hπj1 , . . . , πjn i : Ωm → Ωn . Specifically, consider the diagram

0

v (Φα0a+1 ,...,α0k )α (⊥) v (Φαa+1 ,...,αk )α (⊥),
showing the claim.
The other cases (when αa is a successor or limit ordinal) are the
same as in the proof of Thm. 2.13. This concludes the proof.
B.3

Proof of Lem. 3.8

Proof. We prove the following (more general) statement by induction on ϕ: for any formula ϕ and for each V10 , . . . , Vm : Y → Ω,
we have
0
0 
JϕKc (f ∗ (V10 ), . . . , f ∗ (Vm
)) = f ∗ JϕKd (V10 , . . . , Vm
)
(34)
f

f

(ΩΩ )n
(Ωf )n

λΩn



m

Ωm

(ΩΩ )n

λΩm

/ ΩF (Ωn )
 ΩF f

/ ΩF (Ωm )

where f stands for hπj1 , . . . , πjn i. Starting from the element
n
hπ1 , . . . , πn i ∈ (ΩΩ )n on the top-left corner proves the claim.
B.5

Proof of Thm. 4.4

Proof. In view of Prop. 3.10 and Thm. 2.13, it suffices to show that:
• an MC progress measure (Def. 4.3) gives rise to
• a progress measure (in the sense of Def. 2.12) for the equational

system Eϕ,c over ΩX that arises from ϕ and c,

~0 ) ◦ Q is of type
for each x ∈ X. Here recall that πj ◦ ev(α
X n
FX
X → Ω, and λX : (Ω ) → Ω ; the right-hand side of (36)
~0 ) ◦ Q) (see
therefore coincides with J♥λ (uj1 , . . . , ujn )Kc (ev(α
Def. 3.7).
Now let us prove the equality (36). First notice the naturality of
~0 ) ◦ Q:
λ, where we write Q0 for ev(α

V0

where f ∗ (V 0 ) is defined by X → Y → Ω.
For the cases other than fixed-point operators the proof is as
usual in coalgebraic modal logic. For the modal formula case we
exploit the naturality of λ.
For the case of a µ-formula µu. ϕ, we shall rely on the CousotCousot characterization of least fixed points and prove the following by transfinite induction on the ordinal α:


n

ΩO n

and vice versa.
The correspondence between the two notions is straightforward
by (un)Currying. In particular, Thm. 2.13.2 gives the bound for a
maximal ordinal α by ascCL(ΩX ). We must check that Cond. 1–
5 (in each notion) are suitably transferred to each other; we shall
focus on the cases handled in Cond. 5(c) of Def. 4.3. The other
cases are straightforward.
It is not hard to see that, for this case, what needs to be shown
is the following claim that informally reads “PT♥λ (uj1 ,...,ujn )
properly imitates the semantics of ♥λ (uj1 , . . . , ujn )”:

~0 ) ◦ F Q ◦ c (x) =
PT♥λ (uj1 ,...,ujn ) (α
(36)

~0 ) ◦ Q (c(x))
~0 ) ◦ Q, . . . , πjn ◦ ev(α
λX πj1 ◦ ev(α

pia (α1 , . . . , αk ) v pia (α10 , . . . , αk0 )
0

Proof of Lem. 4.1

Ωm
O

Q0

X

−−−−→
α
JϕKc (f ∗ (V 0 ), ) (⊥X→Ω ) =
(35)

α

f ∗ JϕKd (V~ 0 , ) (⊥Y →Ω )
for each ordinal α.

m

(ΩΩ )n
0

(ΩQ )n

λΩm



X n

(Ω )

λX

/ ΩF (Ωm )
/Ω



0

ΩF Q
FX

(37)

that is used in:

~0 ) ◦ F Q ◦ c (x)
PT♥λ (uj1 ,...,ujn ) (α

~0 )) ◦ F Q ◦ c (x)
= λhj1 ,...,jn i ◦ F (ev(α
~0 )
by def. of PT♥λ (uj1 ,...,ujn ) (α

= λhj1 ,...,jn i ◦ F Q0 ◦ c (x) by Q0 = ev(~
α) ◦ Q

0
= λΩm (πj1 , . . . , πjn ) ◦ F Q ◦ c (x) by Q0 = ev(~
α) ◦ Q

= λX (πj1 ◦ Q0 , . . . , πjn ◦ Q0 ) ◦ c (x) by (37),

The base case follows from the induction hypothesis (for the proof
of (34)), since f ∗ (⊥Y →Ω ) = ⊥X→Ω . For the step case,
−−−−→
α+1
JϕKc (f ∗ (V 0 ), )
(⊥X→Ω )
−−
−−→
 ∗ 
α

∗
0
= JϕKc (f (V ), ) f
JϕKd (V~ 0 , ) (⊥Y →Ω )



by ind. hyp. (for (35))

α

= JϕKd V~ 0 , JϕKd (V~ 0 , ) (⊥Y →Ω ) by ind. hyp. (for (34))

α+1

= f ∗ JϕKd (V~ 0 , )
(⊥Y →Ω ) ,

as required. This proves (36) and hence the theorem.
B.6

Proof of Thm. 4.8

Proof. The proof, much like in Appendix A, is by showing that
MPMs and MC progress measures induce each other. We then
appeal to Thm. 4.4 to obtain the claim.
The mutual construction between an MPM R and an MC
progress measure Q is much like in Prop. A.4. The essence is:

as required. For the limit case (when α is a limit ordinal) the claim
follows from the fact that f ∗ preserves supremums.
The case of a ν-formula is symmetric to the last case. This
concludes the proof.

21

2016/1/12

= (Jζ)−1

for any prioritized ordinal (α1 , . . . , αk ),
(R(x))

(i)

i (α1 , . . . , αk ) ⇐⇒ (Q(x))i (α1 , . . . , αk ) = tt,

Combining the two items in the above, we conclude

and a row (♠, . . . , ♠) in an MPM handles an exceptional case that
(Q(x))i (α1 , . . . , αk ) = ff for every (α1 , . . . , αk ). Then Cond. 1–
5 of both notions are easily seen to be mutually transferred. Note
that, for MPMs, Cond. 1 is not needed.
B.7

tr(c)

Proof of Thm. 4.12

Proof. Let R0 : X → POM|X| be the optimal MPM guaranteed in
Thm. 4.8.2. It is easy to see that, at any time during the execution
(i)
of the algorithm, we have R(x, i, j) ≤ (R0 (x))j for any x, i, j.
Here ≤ is the usual inequality between natural numbers, where ♠
is deemed to be the greatest. Therefore we have
{x ∈ X | R(x, m, k) 6= ♠} ⊇ {x ∈ X | R0 (x, m, k) 6= ♠} = JϕKc .
(38)
It is also easy
 to see that, once the algorithm terminates, the data
R(x, i, j) x,i,j defines an MPM. By Thm. 4.8.1 (soundness) we
have the opposite inclusion ⊆ in (38). This proves the claim.
B.8

Proof of Thm. 4.13

Proof. It can be easily seen that each iteration of the main loop
(lines 7–33) strictly increases R(x, i) for at least one (x, i) with
respect to the preorder i (except for the last iteration). Since

k
each R(x, i) belongs to 0, |X| q {(♠, . . . , ♠)}, each R(x, i)
increases at most (|X| + 1)k times. There are m|X| of (x, i)’s;
therefore the main loop iterates at most m|X|(|X| + 1)k times. It
is obvious that inner loop (lines 8–32) iterates m|X| times.
The complexities of lines 9–12 and lines 13–15 are O(k), and
those of lines 16–18 and lines 19–22 are O(km), by bounding n
by m. The complexity of lines 23–25 is O(km2 |X|k+1 + C|X|k ),
as noted in Definition 4.10; it dominates the overall complexity of
the inner loop. From these we derive the claimed complexity.
B.9

Proof of Thm. 5.6

ulation, a notion from [26, 57]. Its soundness against infinitary
trace semantics—the latter being coalgebraically formalized in
Prop. 5.2—has been established in [57], under the conditions
of nonemptiness and image-finiteness. These conditions are obp X in K`(P), since it
viously satisfied by the arrow Js : Y →
is the graph relation of a function s : Y → X. From this we
conclude that the inequality

Y



by def. of µP (union) and P’s action on arrows (direct image);
(40)
hence there must be some t ∈ c(x0 ) such that (39) holds.
Now consider the following diagram:

*

⊇

p Z. We aim at tr(Jq) ⊇ J(beh(q)).
Y →
By the characterization of tr(Jq) as a greatest fixed point
(Prop. 5.2), it suffices to show that J(beh(q)) is a fixed point
of the function Ψ in (17). This is shown as follows.

X

F J beh(q)

Jq

J(F beh(q) ◦ q)

/ F P(X × Z)
O F Pι
/ F PY

ξX×Z

ξY

/ PF (X × Z)
O
PF ι
/ PF Y

/ X × PZ

hX,tr(c)i

str

/ P(X × Z)
O Pι
/ PY

which obviously follows from the definition of Y and str. The
arrow F X → PF Y that arises in (41) shall be denoted by h.
Let us now note that the following diagrams commute—we
use naturality of ξ and compatibility of ξ and str with the monad

Ψ(J beh(q))
= (Jζ)−1

F str

(41)
where str(x0 , U ) := {(x0 , z 0 ) | z 0 ∈ U } equips the monad P
with a strength [38], and ι : Y ,→ X × Z is the inclusion function.
Factorization via the dashed arrow can be seen by the restriction

tr(Jq)

holds; see [57, Thm. 4.6].

= (Jζ)

/ F (X × PZ)

F hX,tr(c)i

FX

• Next we compare two arrows tr(Jq) and J(beh(q)) of the type

−1

and equivalently beh(q)(y)
∈ tr(c)(s(y)) = tr(c)(x) because

(J beh(q))(y) = beh(q)(y) .
It remains to be shown that pm (α, . . . , α) v JϕKζ (z). It is
crucial here that r : Y → pPMϕ,α forms an MC progress measure
(Def. 4.3) for ϕ over q : Y → F Y . This fact is obvious when one
compares Cond 5(c) in Def. 4.3 and 5.5. It follows from Thm. 4.4
that pm (α, . . . , α) v JϕKq (y). Then our goal follows from the fact
that JϕKq (y) = JϕKζ (z); the latter is a consequence of Lem. 3.8.
This concludes the proof of the item 1 (soundness).
For the item 2 (completeness), let us first fix an optimal
MC progress measure Qζ : Z → pPMϕ,α , i.e. one such that

Qζ (z 0 ) m (α, . . . , α) = JϕKζ (z 0 ) for each z 0 ∈ Z. By Thm. 4.4.2
such Qζ exists. We define an LTMC progress measure as follows.
For each infinitary trace z ∈ Z, there exists an MC progress
(z)
measure p(z) such that pm (α(z) , . . . , α(z) ) = JϕKζ (z) (by completeness, Thm. 4.4). An ordinal α is chosen so that α(z) ≤ α for
each z ∈ Z; this is possible since Z is a (small) set. We define Y
by

Y := (x0 , z 0 ) ∈ X × Z z 0 ∈ tr(c)(x0 ) .

/Z
;

tr(c)

p Z,
: Y →

0
ζ(z 0 ) ∈ (µP
F Z ◦ PξZ ◦ PF tr(c) ◦ c)(x )
by def. (16) of tr(c), expanded in Sets

0
= µP
F Z ◦ P(ξZ ◦ F tr(c)) (c(x ))
S
= t∈c(x0 ) (ξZ ◦ F tr(c))(t)

• Cond. 6 of Def. 5.5 asserts that Js is a backward Kleisli sim-

Js _

Js ⊇ J beh(q)

The functions r and s are defined by r(x0 , z 0 ) := Qζ (z 0 ) and
s(x0 , z 0 ) := x0 .
The construction of the coalgebra structure q : Y → F Y is as
follows. Let y 0 = (x0 , z 0 ) ∈ Y be an arbitrary element of Y , so
that z 0 ∈ tr(c)(x0 ). We can pick t ∈ F X such that: t ∈ c(x0 ) and

F (tr(c))
ξZ
ζ(z 0 ) ∈ ξZ ◦ F (tr(c)) (t) where F X → F PZ →
PF Z.
(39)
Recall that ξ : F P ⇒ PF is a distributive law (Def. 5.1). Indeed,
z 0 ∈ tr(c)(x0 ) implies

Proof. For the item 1 (soundness), the desired infinitary trace z is
obtained by z := beh(q)(y) ∈ Z, where beh(q) is from (8). We
shall first establish that z is indeed an infinitary trace of c from x,
that is, z ∈ tr(c)(x).

XO

J(ζ ◦ beh(q)) by def. (8) of beh(q)

= J beh(q).

by F J = JF , see e.g. [57]

22

2016/1/12

= JϕKζ (z) by the choice of Qζ .

structure of P.
P
ηF
X
P
F ηX

FX
O

FX

F π1

/ F (X × PZ)

F hX,tr(c)i

F str

This concludes the proof.

/ F PX
O

ξX

/ F P(X × Z)
O F Pι
/ F PY

ξX×Z

3. F PZ
O

ξZ

/ F P(X × Z)
O F Pι
/ F PY

ξX×Z

F Pπ1

ξY


/ PF X
O

B.10

q

PF π1

/ PF (X × Z)
O
PF ι
/ PF Y
O

h
F (tr(c))
F π2

/ F (X × PZ)

F hX,tr(c)i

FX

F str

F Pπ2

ξY

Proof of Thm. 5.7

/ PF Z
O

0
Proof. Let (α, Y0 →
F Y0 , r0 , s0 ) denote, for the sake of distinction, the LTMC progress measure that we constructed in the proof
of Thm. 5.6.2. So note that Y, q, . . . in the proof of Thm. 5.6.2,
and those which are here, are different. Recall that Y0 ⊆ X × Z.
We shall define Y ⊆ X × pPMϕ,α as (an image of) a subset of Y0 .
Let Y be the family of subsets U ⊆ Y0 (hence U ⊆ X × Z)
that satisfy the following conditions.

1. (Initial state) (x, z) ∈ U (where x ∈ X and z ∈ tr(c)(x) are
both from the statement);
2. (No redundancy) In case (x0 , z10 ) ∈ U , (x0 , z20 ) ∈ U and
Qζ (z10 ) = Qζ (z20 ) hold, then z10 = z20 .

PF π2

/ PF (X × Z)
O
PF ι
/ PF Y
O
On the family Y we define an order E by: U E U 0 if
• U = U 0 , or
• U ( U 0 , and

h

(42)
We claim that the set h(t) ⊆ F Y , where t ∈ F X is the one
we chose so that (39) holds, contains an element t0 such that
(F π1 )(t0 ) = t and (F π2 )(t0 ) = ζ(z 0 ). Indeed, we have

for any (x0 , z 0 ) ∈ U , there exists t00 ∈ F U 0 such that
(F π1 )(t00 ) = (F π1 ◦ q0 )(x0 , z 0 ),
00

ζ

(PF π2 ◦ h)(t)

ζ

and

(43)

0

(F Q ◦ F π2 )(t ) = (F Q ◦ ζ)(z ).


= ξZ ◦ F (tr(c)) (t) by the second diagram in (42)

Reflexivity, antisymmetry and transitivity of E are straightforward.
We aim at applying Zorn’s lemma to obtain a maximal element of
Y with respect to E.
Note first that Y is nonempty; indeed {(x, z)}
S ∈ Y. Let
{U
}
be
a
totally
ordered
subset
of
Y.
Then
i
i∈I
i Ui —where
S
is the
S set-theoretic union—is an upper bound of {Ui }i in Y. Indeed, i Ui belongs to Y: Cond. 1 is obvious; and Cond. 2 is easy
too, because we can find i1 , i2 ∈ I such that (x0 , z10 ) ∈ Ui1 and
(x0 , z20 ) ∈ Ui2 , and Ui1 ⊆ Ui2 (without loss of generality) because
S
{Ui }i∈I is totally ordered. It remains to be shown that Ui E i Ui
for each i ∈ I. In case Ui is the maximum (with respect to E) in
{Ui }i∈I , then
S it is so with respect to the inclusion order ⊆; therefore Ui = i Ui . Assume otherwise, in which case
S there exists
j ∈ I such S
that Ui E Uj and Ui 6= Uj . Now Uj ⊆ i Ui and hence
F Uj ⊆ F ( i Ui ) (as subsets of F Y0 , since any Sets-functor preserves monos with a nonempty domain).
S It is now easy to check
the condition (43), and to see that Ui E i Ui .
What we have shown so far allows us to appeal to Zorn’s lemma
and to conclude that Y has a maximal element with respect to E.
We pick one and that is denoted by Y 0 .
On such a maximal element Y 0 we shall show that the condition (43) holds with U = U 0 = Y 0 . Assume otherwise. By the
proof of Thm. 5.6.2, there does exist an element t00 := q0 (x0 , z 0 ) ∈
F Y0 such that the two equalities in (43) hold. Hence the condition (43) holds for U = Y 0 , U 0 = Y0 . Now let us define

Yr0 := (x0 , z 0 ) ∈ Y0 ∃(x0 , z 00 ) ∈ Y 0 s.t. Qζ (z 0 ) = Qζ (z 00 ) \ Y 0 ,

3 ζ(z 0 ) by (39);
therefore there exists an element t0 of the set h(t) such that
(F π2 )(t0 ) = ζ(z 0 ). We also have (F π1 )(t0 ) = t—in fact
(F π1 )(t00 ) = t holds for any element t00 of the set h(t), since
(PF π1 ◦ h)(t) = {t} by the first diagram in (42).
Finally, we define q(y 0 ) ∈ F Y by q(y 0 ) = q(x0 , z 0 ) :=
q
0
t ∈ h(t) ⊆ F Y . It is not hard to see that the data (α, Y →
F Y, r, s) thus defined satisfies the conditions in Def. 5.5. Specifically, Cond. 5(c) follows immediately from the fact that Qζ : Z →
pPMϕ,α is an MC progress measure (Def. 4.3) over the final coalgebra ζ. In its course we use the fact that, for each y 0 = (x0 , z 0 ) ∈
Y,

(F r ◦ q)(y 0 ) = F (Qζ ◦ π2 ) (q(y 0 )) by def. of r
= (F Qζ ◦ ζ)(z 0 ) by def. of q.
Cond. 6 follows from (F π1 )(q(y 0 )) = t ∈ c(x0 ) (see (39)).
Thus we have obtained an LTMC progress measure q : Y →
F Y . Let y ∈ Y required in the statement to be y := (x, z).
Now we shall check that the data thus obtained indeed satisfies
the conditions in the statement. That s(y) = x is by definition of s
and y. For the condition that beh(q)(y) = z, we observe that
FY
O

F π2

q

Y

/ FZ
O
ζ
/Z

final
π2

Yn0 := Y0 \ (Y 0 ∪ Yr0 ).
We shall show that Yn0 6= ∅, and that the condition (43) holds
with U = Y 0 and U 0 = Y 0 ∪ Yn0 . This will yield contradiction
with the maximality of Y 0 with respect to E. Note here that Y0 =
Y 0 q Yr0 q Yn0 .
By the definition of Yr0 , we can choose a function f : Yr0 → Y 0
such that f (x0 , z 0 ) is (x0 , z 00 ) such that Qζ (z 0 ) = Qζ (z 00 ). This
means that the following diagram commutes.

commutes—recall that t0 = q(x0 , z 0 ) is chosen so that (F π2 )(t0 ) =
ζ(z 0 ) (see above). Therefore π2 in the diagram is a coalgebra homomorphism and we have
beh(q)(y) = beh(ζ)(π2 (y)) by finality
= beh(ζ)(z) = z,
as required. To see that pm (α, . . . , α) = JϕKζ (z) where p := r(y),
we have

Y 0 + Yr0 + Yn0

pm (α, . . . , α)

= Qζ (z) m (α, . . . , α) by def. of r

[Y 0 ,f ]+Yn0
0



Y + Yn0

23





/ X ×Z
/ X ×Z

X×Qζ

/ X × pPMϕ,α
4

X×Qζ

2016/1/12

= F π1 (q0 (x0 , z 0 ))

By (essentially) applying F to the diagram we obtain the following, where g denotes the arrow hF π1 , F (Qζ ◦ π2 )i. The images
g[F Y0 ] and g[F (Y 0 + Yn0 )] are characterized by epi-mono factorizations.

..

F (Y 0 + Yr0 + Yn0 )
F ([Y 0 ,f ]+Yn0 )
0



F (Y + Yn0 )





g[F Y0 ]

0

q

/ F (X × Z)
/ F (X × Z)
%

. . g[F (Y +
0

Yn0 )]

by def. of q; see (43)
∈ c(x0 ),

g

g

0
F Y0 , r0 , s0 ) is an
where the last membership is because (α, Y0 →
LTMC
progress
measure
for
c.
#
/ F X × (F pPMϕ,α ) It remains to show that the LTMC progress measure that we
@
3
have constructed indeed realizes JϕKζ (z). Let y := (x, Qζ (z)) be
the element y ∈ Y required in the statement. We have

(r(y))m (α, . . . , α)

4

= (Qζ (z))m (α, . . . , α) by definition
= JϕKζ (z) by the choice of Qζ , see the proof of Thm. 5.6.

The dashed arrow arises as a diagonal fill-in. This proves


F π1 , F (Qζ ◦ π2 ) [F Y0 ] = F π1 , F (Qζ ◦ π2 ) F (Y 0 +Yn0 ) ,
(44)
since the other direction ⊇ is straightforward from Y0 ⊇ Y 0 + Yn0 .
It is an immediate corollary of (44) that Yn0 6= ∅—otherwise we
have g[F Y0 ] = g[F Y 0 ] that contradicts with the assumption that
the condition (43) holds with U = Y 0 , U 0 = Y0 but fails with
U = U 0 = Y 0 . It follows too that the condition (43) holds with
U = Y 0 , U 0 = Y 0 + Yn0 since (44) asserts that Y0 and Y 0 + Yn0
“have the same strength” when it comes to the condition (43). It is
also obvious from the definition of Yn0 —it is defined by excluding
“redundant” elements in Yr0 —that Y 0 + Yn0 satisfies Cond. 2 of the
set Y. Summarizing, we have shown that Y 0 + Yn0 ∈ Y is such that
Y 0 E Y 0 + Yn0 , with a strict inequality. This contradicts with the
maximality of Y 0 .
Thus we have shown that the condition (43) holds with U =
U 0 = Y 0 . Now let us go back to the construction of the “small”
LTMC progress measure required in the statement. We define
 0 ζ 0 
Y :=
x , Q (z ) ∈ X × pPMϕ,α | (x0 , z 0 ) ∈ Y 0 .

This concludes the proof.
B.11

Proof of Thm. 5.9

Proof. We first check if ϕ is satisfiable by F -coalgebras. If ϕ not,
then obviously the answer to the problem in the statement is false.
Assume otherwise.
We claim that the maximum ordinal α in Theorem 5.7 can be
bounded by Nϕ from Assumption 5.8. Indeed, by the small model
property (Assumption 5.8), we can assume that there exists a coalgebra ε : E → F E, its state e ∈ E and an MC progress measure
Q0 : E → pPMϕ,α0 (Def. 4.3) such that Q0 (e)(α0 , . . . , α0 ) = tt
and |E| ≤ Nϕ . Moreover, by Thm. 4.4.1–2, we can choose the
maximum ordinal α0 of Q0 to be α0 = |E| ≤ Nϕ . It is then
straightforward to adapt the proof of Thm. 5.7 in the following way.
• The final coalgebra ζ : Z → F Z is replaced by ε : E → F E.
• The optimal MC progress measure Qζ is replaced by the MC

progress measure Q0 in the above.

Going through the adapted proof proves the statement of Thm. 5.7
with the ordinal α in it bounded by α0 , hence by Nϕ .
Since X is assumed to be finite and so is Nϕ ∈ ω, we see
that the set X × pPMϕ,Nϕ is a finite set. By the last assumption
in Assumption 5.8, the set F Y is finite for any (necessarily finite)
subset Y ∈ X × pPMϕ,Nϕ . Therefore there are only finitely many
functions q : Y → F Y . We enumerate all such, for each Y ∈
X × pPMϕ,Nϕ , and check if there is any that makes (α, q, π2 , π1 )
an LTMC progress measure. If there is, then the answer to the
problem in the statement is true (by Thm. 5.6.1). If there is none,
then the answer is false by the above arguments.

The functions r, s are defined by projections: r := π2 and s := π1 .
The coalgebraic structure q : Y → F Y is defined using the above
fact that the condition (43) holds for U = U 0 = Y 0 . Specifically,
let (x0 , p) ∈ Y ; then by Cond. 2 of Y 0 ∈ Y, there exists a unique
z 0 ∈ Z such that p = Qζ (z 0 ) and (x0 , z 0 ) ∈ Y 0 . We use the
condition (43) (for U = U 0 = Y 0 ) to find t00 ∈ F Y 0 that satisfies
the two equalities in (43). Finally we define
q(x0 , p) := F (idX × Qζ )(t00 ).
Note that the types match up: t00 ∈ F Y 0 ⊆ F (X × Z) and
F (idX × Qζ ) : F (X × Z) → F (X × pPMϕ,α ), and the latter
obviously factors through F Y ,→ F (X × pPMϕ,α ).
q
It is straightforward to check that (α, Y → F Y, r, s) thus
obtained indeed constitutes an LTMC progress measure. Let us turn
to Cond. 5(c) of Def. 5.5, and in particular (18), for example. Let
(x0 , p) ∈ Y and z 0 ∈ Z be the unique one such that p = Qζ (z 0 )
and (x0 , z 0 ) ∈ Y 0 . We have
(LHS)
= (Qζ (z 0 ))i (α1 , . . . , αa , . . . , αk )
v PT♥λ (uj1 ,...,ujn ) (β1 , . . . , βa−1 , αa , . . . , αk ) (F Qζ ◦ ζ)(z 0 )



since Qζ is an MC progress measure for ζ : Z → F Z (Def. 4.3)
= PT♥λ (uj1 ,...,ujn ) (β1 , . . . , βa−1 , αa , . . . , αk ) (F π2 )(q(x0 , p))



by def. of q; see (43)

= PT♥λ (uj1 ,...,ujn ) (β1 , . . . , βa−1 , αa , . . . , αk ) (F r ◦ q)(x0 , p) .
for suitable β1 , . . . , βa−1 , as required. For Cond. 6, let z 0 be chosen
in the same way as above. Then we have
(F s ◦ q)(x0 , p) = (F π1 )(q(x0 , p))

24

2016/1/12

