Parity Automata for Quantitative Linear Time
LogicsCorina Cîrstea1 , Shunsuke Shimizu2 , and Ichiro Hasuo2
1
2

University of Southampton, UK
cc2@ecs.soton.ac.uk
National Institute of Informatics, Tokyo, Japanshunsuke,hasuo@nii.ac.jp

Abstract
We initiate a study of automata-based model checking for previously proposed quantitative linear
time logics interpreted over coalgebras. Our results include: (i) an automata-theoretic characterisation of the semantics of these logics, based on a notion of extent of a quantitative parity
automaton, (ii) a study of the expressive power of Büchi variants of such automata, with implications on the expressiveness of fragments of the logics considered, and (iii) a naïve algorithm forcomputing extents, under additional assumptions on the domain of truth values.
Keywords and phrases coalgebra, quantitative logic, linear time logic, parity automaton
Digital Object Identifier 10.4230/LIPIcs.CALCO.2017.7

1

Introduction

Linear time logics such as LTL or the linear time µ-calculus (see e.g. [9]), originally interpreted
over non-deterministic transition systems, have been adapted and used successfully in model
checking various types of non-deterministic and probabilistic systems [3]. These logics sharethe same notion of linear time behaviour, but depending on the branching present in themodels, have either a qualitative or a quantitative interpretation (with {0, 1}, resp. theunit interval as domains of truth values). Despite commonalities between the logics andtheir automata-based verification techniques, a uniform account of the connection between(quantitative) linear-time logics and (quantitative) automata over infinite structures is still
missing. This would allow existing verification techniques to be transferred to new models,
including weighted ones (for which linear time logics have already been studied [15]).
This paper initiates a general study of the connection between quantitative linear time
logics and quantitative automata on infinite structures, grounded in coalgebraic modelling, bybuilding on recent work on maximal traces [6], quantitative linear time logics for systems with
branching [4, 5], and coalgebraic trace semantics for Büchi and parity automata [17]. (Here,a maximal trace is either a finite, completed trace or an infinite trace.) The work in [6, 4, 5]
models systems with branching as coalgebras of type T◦F , with F : Set → Set an endofunctor
used to specify linear behaviour (the structure of individual transitions) and T : Set → Set a
monad used to specify branching structure (which typically associates quantities to individualtransitions). Examples include non-deterministic/probabilistic/weighted labelled transition
systems, with or without explicit termination, but also models with a more general “linear”
behaviour, including tree-like behaviour; for example, taking F : Set → Set to be A × Id × Id
with Id : Set → Set the identity functor captures linear behaviours given by infinite labelledbinary trees. In this setting, a canonical definition of linear time behaviour of states in a
coalgebra with branching associates, to each state and each possible maximal trace (elementof the final F -coalgebra), a quantity measuring the extent of the given state exhibiting
licensed under Creative Commons License CC-BY
7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017).
Editors: Filippo Bonchi and Barbara König; Article No. 7; pp. 7:1–7:26
Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

7:2

Parity Automata for Quantitative Linear Time Logics

that trace, accumulated across all branches [6]. This recovers known concepts of infinite
trace semantics, including the possibility (for the finite powerset monad), likelihood (for the
sub-probability distribution monad) or minimal cost (for a weighted monad with weights
modelling costs) of exhibiting a particular trace.
Coalgebraic linear time logics, interpreted over the same types of models, were studied
in [4, 5], with formulas specifying properties of linear behaviour, and with their semantics
measuring the extent with which such properties hold in states of coalgebras with branching.
The monad T uniformly determines both the domain of truth values for the logics and the
choice of propositional operators (e.g. finite disjunctions for non-deterministic systems, subconvex combinations for probabilistic systems and linear combinations for weighted systems).
The modal operators employed arise from the functor F , but their interpretation is based
both on a choice of associated predicate liftings for F and on a canonical predicate lifting for
T, with the latter being used to accumulate the quantities associated to different branches.
As with the notion of linear time behaviour, exactly how this accumulation works depends
on the type of branching. For non-deterministic systems, one recovers the aconjunctive
linear-time µ-calculus. For probabilistic systems, the resulting logics differ from probabilistic
variants of LTL or the linear time µ-calculus in their absence of boolean operators. Thisdifference is beneficial, as it results in an expensive automata determinisation step required
for model checking such probabilistic variants (see [3, Section 10.3]) being avoided with our
logics, without a real loss in expressiveness (see Remark 6). For weighted systems, the logics
are similar to previously proposed ones [15] in their absence of conjunction operators. Our
choice of propositional operators is further supported by results in [5] on the equivalence ofthe original, step-wise semantics of the logics with an alternative path-based semantics akinto that of LTL, and by the close connection to quantitative automata described in this paper.
We now turn to the contributions of this paper. A definition of the extent with which
two states in coalgebras with branching exhibit similar linear behaviour was given in[6]. Here we take this further by providing alternative characterisations of notions ofmaximal and finite trace similarity between two branching coalgebras. These instantiate
to the existence/likelihood/minimal joint cost of a common trace, in the case of nondeterministic/probabilistic/weighted branching. When one of the coalgebras models thesystem of interest and the other captures (un)desirable behaviours, these notions provide
the right concepts for automata-theoretic model checking. Our alternative characterisations
involve a product construction, and a novel notion of extent of a coalgebra with branching.
We then extend these ideas to provide an automata-theoretic characterisation of thesemantics of the logics in [4, 5]. For this, we use a generalisation of standard parity automata
over words/trees, inspired by recent work on coalgebraic trace semantics for Büchi andparity automata [17]. Our automata are parameterised by (i) a partial semiring monad,
specifying a type of branching, and (ii) a polynomial endofunctor F , specifying a type of
linear behaviour. Key to our approach is the notion of extent of a parity automaton, which
provides a quantitative notion of acceptance, not of a single maximal trace, but across all
maximal traces that conform to the automaton. This instantiates to the existence/likelihood/minimal cost of an accepting trace (maximal trace satisfying the parity condition), for
non-deterministic/probabilistic/weighted branching (with weights modelling costs), respectively (see Example 17). A key advantage of the extent-based characterisation of the semantics
is a localised view of the satisfaction relation of the logics – fixpoints are computed locally on
the reachable part of the product between model and formula automata, rather than globallyas predicates on the model state space, as stipulated in the original semantics. Our generictranslation from formulas to automata resembles known translations for non-deterministic

Corina Cîrstea, Shunsuke Shimizu, and Ichiro Hasuo

7:3

systems (see e.g. [19]), while additionally exploiting the choices made in the semantics of ourlogics to simplify the construction. A translation from automata to formulas is also sketched.
For non-deterministic branching, Büchi automata over words are as expressive as parity
ones [11], while over trees this fails to hold [16]. Here we generalise this result to a quantitative
setting, under the additional assumption that the branching semiring is total. Given ourtranslations from logics to automata and back, this also yields an important result about
our logics, namely that for word-like linear behaviour (i.e. F isomorphic to a coproductof constant and identity fnctors), the alternation degree 1 fragment of the logics is fully
expressive. We stress that our translation from parity to Büchi automata preserves thequantitative language. To our knowledge, the only related result in a quantitative setting is atranslation from probabilistic Rabin to probabilistic Büchi automata [2], which only preserves
the qualitative language. Unlike the standard translation from parity to Büchi via Rabin
automata [11], which uses the idempotence of disjunction, our translation does not require
idempotence of the semiring addition. For partial semirings which arise as sub-semiringsof total semirings satisfying our assumptions (as is the case for probabilistic branching), a
similar translation is obtained by moving to the larger semiring; this time, the resulting
Büchi automaton has branching as specified by the larger semiring, but can nonetheless beused in the same way, given the preservation of the quantitative language (see Remark 32).
Our final contribution is a naïve algorithm for computing extents of parity automata.
This requires an additional assumption on the underlying semiring, satisfied by both nondeterministic branching and a bounded variant of weighted branching, to ensure that thecomputation of individual fixpoints terminates. To summarise, our contributions are:1. automata-theoretic characterisations of finite and maximal trace similarity between statesof coalgebras with branching (Theorem 14),
2. a notion of extent of a parity automaton, parameterised by a choice of branching monadand linear time behaviour (Definition 16),
3. translations from linear time formulas to automata and back, providing an automatatheoretic characterisation of the quantitative semantics of the logics in [4, 5] (Theorem 24),
4. a translation from quantitative parity to quantitative Büchi automata over words (Theorem 31), rendering the alternation degree 1 fragment of the logics fully expressive,
5. an algorithm for computing extents, similar in complexity to known algorithms for
emptiness checking in the non-deterministic case [14].
We assume familiarity with the coalgebraic approach to modelling systems. Section 2 recalls
the results of [6, 4, 5], while each subsequent section contains one of the above contributions.

Acknowledgments
S.S. and I.H. are supported by ERATO HASUO Metamathematics for Systems Design
Project (No. JPMJER1603), JST, and Grants-in-Aid No. 15KT0012 & 15K11984, JSPS.
Part of this work was carried out during a visit of the second author to the University ofSouthampton, supported by an EPSRC Institutional Sponsorship Award EP/P511407/1.
The authors thank the anonymous reviewers for their insightful comments.

2

Preliminaries

2.1

From Partial Commutative Semirings to Commutative Monads

I Definition 1. A partial commutative semiring is a tuple S := (S, +, 0, •, 1) with (S, +, 0)a partial commutative monoid and (S, •, 1) a commutative monoid, with • distributing over

CALCO 2017

7:4

Parity Automata for Quantitative Linear Time Logics+; that is, for all s, t, u ∈ S, s • 0 = 0, and whenever t + u is defined, then so is s • t + s • uand moreover s • (t + u) = s • t + s • u.
The addition operation of any partial commutative semiring induces a pre-order relation v
on S, given by x v y iff there exists z ∈ S with x + z = y, and having 0 as its least element.
I Example 2. Here we consider the boolean semiring ({0, 1}, ∨, 0, ∧, 1), the (partial) probabilistic semiring ([0, 1], +, 0, ∗, 1), the tropical semiring N = (N∞ , min,(∞, +, 0) and its boundedm + n, if m + n ≤ Bvariants SB = ([0, B]∞ , min, ∞, +B , 0) with B ∈ N, where m+B n =.
∞, otherwise
The associated pre-orders are ≤ on {0, 1} and [0, 1], and ≥ on N∞ and [0, B]∞ .
We further assume that v has a top element and is an ω-chain complete as well as ω op -chain
complete partial order. This holds in all our examples.
A partial commutative semiring S induces a semiring monad (TS , η, µ) withP
TS (X) = { ϕ : X → S | supp(ϕ) is finite ,ϕ(x) is defined }x∈supp(ϕ)(ηX (x)(y) =1

if y = x0otherwise,µX (Φ)(x) =P

Φ(ϕ) • ϕ(x)ϕ∈supp(Φ)

where supp(ϕ) = {x ∈ X | ϕ(x) 6= 0} is the support of ϕ. Moreover, the monad TS above isstrong and commutative, with strength stX,Y : X × TS Y → TS (X × Y ) and double strength
dstX,Y : TS X × TS Y → TS (X × Y ) given by(
ψ(y) if z = x
stX,Y (x, ψ)(z, y) =,dstX,Y (ϕ, ψ)(z, y) = ϕ(z) • ψ(y)0otherwise
We note that TS 1 = S, with 1 a final object in Set, and therefore S carries a TS -algebra
structure given by µ1 : T2S 1 → TS 1. The relationship between monads and partial semirings
was studied in [8, 6]. We use semiring monads to model branching, with the semirings in
Example 2 modelling non-deterministic, probabilistic and weighted branching. In the latter
case, we think of the weights as costs associated to individual system steps.

2.2

Finite and Maximal Traces

A coalgebraic approach to defining maximal traces of coalgebras of type TS ◦ F , with F
a polynomial 1 endofunctor and TS : Set → Set a semiring monad, is described in [6]. The
monad TS is used to specify branching structure, whereas the functor F is used to specify
linear behaviour, with the elements of the final F -coalgebra defining individual traces. Since
any polynomial endofunctor on Set can be written as a coproduct of finite products of identity` ar(λ)functors, we readily assume this shape: F X =Xwith Λ a set of operators withλ∈Λ

finite arities. The elements of the final F -coalgebra (initial F -algebra) are potentially infinite(resp. finite) trees with nodes labelled by some λ and having as many outgoing edges as ar(λ).
The definition of maximal traces resembles the alternative partition-refinement definitionof bisimilarity, but differs from it in two key ways: (i) what is defined is a trace relation
between states of a TS ◦ F -coalgebra and elements of the final F -coalgebra, and (ii) trace
relations are S-valued relations that measure, for each state in a coalgebra with branching1

An endofunctor F : Set → Set is polynomial if it is constructed from constant and identity functors
using finite products and arbitrary coproducts.

Corina Cîrstea, Shunsuke Shimizu, and Ichiro Hasuo

7:5

and each linear behaviour, the extent (e.g. ability, likelihood or minimal cost) of that state
exhibiting the given linear behaviour. Concretely, for a TS ◦ F -coalgebra γ : C → TS F C,
its maximal traces are given by the greatest fixpoint of the following operator on S-valued
relations between C and the carrier of the final F -coalgebra (Z, ζ):
RelC,Z

Rel(F )

/ RelF C,F Z

LS∗/ RelT F C,F Z (γ×ζ) / RelC,ZS(1)Here, RelX,Y is the category of S-valued relations on X ×Y , and Rel(F ) : RelX,Y → RelF X,F Y“lifts” S-valued relations on X×Y to S-valued relations on F X×F Y , with the help of the semiring multiplication: for R : X × Y → S, Rel(F )(R) maps (ιλ (x1 , . . . , xar(λ) ), ιλ0 (y1 , . . . , yar(λ0 ) ))to 0 if λ 6= λ0 , and (ιλ (x1 , . . . , xar(λ) ), ιλ (y1 , . . . , yar(λ) )) to R(x1 , y1 ) • . . . • R(xar(λ) , yar(λ) ).
Also, LS : RelX,Y → RelTS X,Y , called extension lifting, takes a relation R : X × Y → S to
the relation µ1 ◦ TS R ◦ st0X,Y : TS X × Y → S, with st0X,Y : TS X × Y → TS (X × Y ) theswapped strength map of TS . This choice for LS is canonical, in the sense that LS (R)(_, y)is the unique extension of R(_, y) to a TS -algebra homomorphism, for y ∈ Y (see [6] forPP
details). Concretely, LS (R)( i ci xi , y) = µ1 ( i ci R(xi , y)) for xi ∈ X and y ∈ Y . The
effect of using LS above is that the quantity ultimately associated to each pair (c, z) ∈ C × Z
is accumulated across all branches from c, in a step-wise fashion.
A similar treatment of finite traces is obtained by replacing the final F -coalgebra (Z, ζ)' /with the initial F -algebra (I, ι), with ι : F I
I , and taking the least fixpoint of thefollowing operator on S-valued relations:
RelC,I

Rel(F )

/ RelF C,F I

LS

−1 ∗

/ RelT F C,F I (γ×ιS)

/ RelC,I

I Example 3. When S = ({0, 1}, ∨, 0, ∧, 1) (and thus TS is isomorphic to the finite powerset
monad), the (greatest, resp. least) fixpoints of the previous operators relate a state in a
non-deterministic coalgebra with a (maximal, resp. finite) trace iff that state can exhibit
the given trace. When S = ([0, 1], +, 0, ∗, 1) or S = (N∞ , min, ∞, +, 0), the (greatest,
resp. least) fixpoints give, for each state and each (maximal, resp. finite) trace, the likelihood,resp. minimal cost of that state exhibiting the given trace. The precise shape of a trace
is determined by the choice of F ; taking F = 1 + A × Id captures words over A, whereas
F = 1 + A × Id × Id captures binary trees with non-leaf nodes labelled by A.

2.3

Quantitative Linear Time Logics for Coalgebras

We now recall (a variant of) the logics studied in [4, 5]. They are interpreted over TS ◦ F coalgebras, with TS and F as before, and have syntax given byPµLVΛ 3 ϕ ::= x | [λ](ϕ1 , . . . , ϕar(λ) ) |i∈I ci • ϕi | µx.ϕ | νx.ϕPwith x ∈ V, λ ∈ Λ and ci ∈ S such that i∈I ci is defined. Here, V is a set of variables and I
is a finite set. Writing ιλ : X ar(λ) → F X with λ ∈ Λ for the coproduct injections, we define,__F_
for each modal operator λ ∈ Λ, an S-valued predicate lifting JλK : S × . . . × S ⇒ S
by:(p1 (x1 ) • . . . • par(λ) (xar(λ) ), if λ = λ0
JλK(p1 , . . . , par(λ) )(ιλ0 (x1 , . . . , xar(λ0 ) )) =(2)0, otherwise
I Definition 4. For a TS ◦ F -coalgebra (C, γ) and a valuation V : V → S C , the denotation
JϕKVγ ∈ S C of a formula ϕ ∈ µLV
Λ is defined inductively on the structure of ϕ byV
JxKγ = V (x),PP
J ci • ϕi KVγ = µ1 ( ci Jϕi KVγ ),
i∈I

i∈I

CALCO 2017

7:6

Parity Automata for Quantitative Linear Time Logics

J[λ](ϕ1 , . . . , ϕar(λ) )KVγ = γ ∗ (extF C (JλKC (Jϕ1 KVγ , . . . , Jϕar(λ) KVγ ))), where the extension pre_T _dicate lifting ext : S ⇒ S S takes an S-valued predicate p : C → S to the S-valued
predicate µ1 ◦ TS p : TS C → S, while γ ∗ : S TS F C → S C is pre-composition with γ.
V \{x}
V \{x}
Jµx.ϕKγ(Jνx.ϕKγ) is the least (resp. greatest) fixpoint of the operator on S C
V [p/x]taking p : C → S to JϕKγ
, where the valuation V [p/x] : V → S C takes x to p andy ∈ V \ {x} to V (y).
(In the second clause, both the formal sum notation and the action of µ1 have been extended
pointwisely to functions on C.) We write µLΛ for the set of closed formulas (V = ∅).
For the operator in the last clause of Definition 4 to be order-preserving, monotonicity of both
ext and JλK, with λ ∈ Λ, is required, and proved in [5]. The existence of lfps, respectively gfps
then follows by [10, Theorem 8.22], which assumes an order-preserving operator on a cpo. The
use of extension lifting in the third clause of Definition 4 results in J[λ](ϕ1 , . . . , ϕar(λ) )KVγ (c)Paccumulating the values JλKC (Jϕ1 KVγ , . . . , Jϕar(λ) KVγ )(fi ), with γ(c) = i ci fi , by taking into
account the weights ci :XJ[λ](ϕ1 , . . . , ϕar(λ) )KVγ (c) = µ1 (ci JλKC (Jϕ1 KVγ , . . . , Jϕar(λ) KVγ )(fi ))i

The presence of weighted sums in the logics is supported by results in [5] showing that theinclusion of such sums preserves the equivalence of the above step-wise semantics with analternative, path-based semantics, akin to that of LTL. Finite conjunctions are missing fromthe logics, and our step-wise semantics prevents their inclusion. It is worth noting, however,that fixpoint logics for weighted systems are similar in their absence of conjunctions [15]. For
total semirings S, finite disjunctions are present as finite weighted sums with the weights
Pequal to 1. Their interpretation is as expected: the formula i 1 • ϕi (written more simplyPi ϕi ) measures the extent of conforming to one of the ϕi s.
`
I Example 5. Taking F = 1 + A × Id ' 1 + a∈A Id yields a logic with a nullary modality ∗(for termination), and unary modalities [a] with a ∈ A, with the usual interpretation. Taking`
F = A × Id × Id ' a∈A (Id × Id) yields a logic with binary modalities [a] with a ∈ A, with(p1 (x) • p2 (y), if a0 = a
associated predicate liftings given by JaKX (p1 , p2 )(ιa0 (x, y)) =,0, otherwise
for p1 , p2 ∈ S X and x, y ∈ X. Irrespective of the choice of F , when S = ({0, 1}, ∨, 0, ∧, 1),
a formula ϕ holds in a state of a TS ◦ F -coalgebra iff that state admits a maximal tracesatisfying ϕ. For S = ([0, 1], +, 0, ∗, 1) or S = (N∞ , min, ∞, +, 0), JϕKγ : C → S measuresthe likelihood, resp. minimal cost of states of TS ◦ F -coalgebras conforming to ϕ (suitably
scaled according to the weighted sums present in ϕ).
I Remark 6. Taking S = ([0, 1], +, 0, ∗, 1) and F = 1 + A × Id yields a linear time logic forprobabilistic transition systems. The absence of pure disjunctions makes this logic different
from probabilistic LTL. A variant of our logics which incorporates disjunctions that can be
resolved in one step (e.g. [a]ϕ ∨ [b]ψ with a 6= b) as new modalities turns out to be more
expressive than probabilistic LTL (see [5, Example 4.3]). In this case, deterministic parity
automata (known to be more expressive than LTL) can be directly encoded in the logic.
I Remark 7. By casting our logics into a dual adjunction framework, as done in [5], it follows
immediately that TS ◦ F -behavioural equivalence implies logical equivalence. This, however,is not very interesting, given the linear time nature of our logics. A detailed study of a
weaker, trace-based notion of equivalence for which our logics are both sound and expressiveis left as future work.

Corina Cîrstea, Shunsuke Shimizu, and Ichiro Hasuo

2.4

7:7

Equational Systems

The use of nested fixpoints in the semantics of fixpoint logics can elegantly be rephrased interms of solutions of equational systems [1].
I Definition 8. An equational system over posets L1 , . . . , Ln is a sequence of equations
u1 =η1 f1 (u1 , . . . , un ) , . . . , un =ηn fn (u1 , . . . , un ) , where u1 , . . . , un are variables, ηi ∈{µ, ν} and fi : L1 × . . . × Ln → Li is a monotone function. A variable uj is a µ-variable(ν-variable) if ηj = µ (resp. ηj = ν).
A precise definition of the solution of an equational system can be found in [1, Section 1.4.4].
Intuitively, assuming that the Li s have enough suprema and infima, the solution of an
equational system is defined as follows:
1. the first equation is solved (by taking either the least or the greatest solution, depending(1)
on η1 ), to obtain an interim solution u1 = l1 (u2 , . . . , un );2. this is substituted for u1 in the second equation, yielding a new equation u2 =η2f2‡ (u2 , . . . , un );(2)
3. the second equation is solved to obtain an interim solution u2 = l2 (u3 , . . . , un );4. continuing this way from left to right eventually eliminates all the variables and leads to(n)a closed solution un = ln ∈ Ln ; and5. closed solutions are propagated back from right to left to yield closed solutions for all of
u1 , . . . , un .
Instead of µ- and ν-annotations, some of the equational systems appearing later in the paper
use natural numbers, with odd (even) values indicating µ- (resp. ν-) variables, and with theorder of equations being determined by the natural order on N. We also use a generalised
form for equational systems, which allows several equations indexed by the same value, all ofwhich are to be solved simultaneously.

3

An Automata-Based Approach to Trace Similarity

As already sketched in [6], notions of maximal and resp. finite trace similarity between statesof TS ◦F -coalgebras can be defined by using a double extension lifting in place of the extension
lifting LS of (1). This section paves the way towards an automata-based characterisationof the semantics of the logic µLΛ , by providing a similar (and simpler) characterisation of
maximal and resp. finite trace similarity.
The double extension lifting L0S : RelX,Y → RelTS X,TS Y takes an S-valued relation
R : X × Y → S to the S-valued relation µ1 ◦ TS R ◦ dstX,Y : TS X × TS Y → S. Comparedto LS , L0S uses the double strength map of TS in place of the swapped strength map to yielda relation on TS X × TS Y . As with LS , this choice for L0S is canonical (see [6]), and satisfiesPP
P P
L0S (R)( i ci xi , j dj yj ) = µ1 ( i j (ci • dj )R(xi , yj )).
I Definition 9. The maximal (resp. finite) trace similarity relation between two TS ◦ F coalgebras (C, γ) and (D, δ) is the greatest (resp. least) fixpoint of the following operator on
S-valued relations between C and D:
RelC,D

Rel(F )

/ RelF C,F D

L0S∗/ RelT F C,T F D (γ×ζ) / RelC,DS

S

We write 'νγ,δ : C × D → S and 'µγ,δ : C × D → S for these relations.
I Example 10. For S = ({0, 1}, ∨, 0, ∧, 1), maximal (finite) trace similarity relates precisely
those states which admit a common maximal (resp. finite) trace. For S = ([0, 1], +, 0, ∗, 1) or

CALCO 2017

7:8

Parity Automata for Quantitative Linear Time Logics

S = (N∞ , min, ∞, +, 0), maximal (finite) trace similarity measures the likelihood, resp. minimal joint cost of two states exhibiting a common maximal (resp. finite) trace.
We now introduce notions of ν- and µ-extent of a TS ◦ F -coalgebra, and rephrase thedefinitions of 'νγ,δ and 'µγ,δ using these notions. The idea is to measure the weight withwhich a state in a coalgebra with branching can exhibit any maximal (resp. finite) trace.
This weight is cumulative across all the branches.
I Definition 11. The ν-extent (µ-extent) of a TS ◦ F -coalgebra (A, α) is the gfp (resp. lfp)
of the operator on S A taking p : A → S to the compositionAα/ TS F A

TS F p/ TS F S

TS (•F )/ TS S = T2 1

µ1

S/ TS 1 = S

where •F : F S → S is given by •F (ιλ (s1 , . . . , sar(λ) )) = s1 • . . . • sar(λ) for λ ∈ λ.
The above operator uses a one-step unfolding of the coalgebra structure to compute a finer
approximation of the extent on a state based on the extent on its immediate successors. As
the generality of F allows for immediate successors which are tuples of states, the semiring
multiplication may also need to be used (in •F ). The monad multiplication is used toaccumulate the values from different branches. The composition in Definition 11 takes a ∈ APPwith α(a) = i ci (a1i , . . . , aji i ) to µ1 ( i ci (p(a1i ) • . . . • p(aji i ))). That is, the extent associatedto a particular state accumulates the extents associated to its immediate successors, scaledby the weights of the corresponding branches.
I Example 12. For the TS ◦F -coalgebras below, with F = 1+A×Id and S = ([0, 1], +, 0, ∗, 1)(resp. S = (N∞ , min, ∞, +, 0)), the ν-extent maps x to 0.4, y to 0.6 and z to 0.2 (resp. x andy to 1 and z to 0), whereas the µ-extent again maps x to 0.4, y to 0.6 and z to 0.2 (resp. x
and z to 4 and y to 2). Intuitively, the reason for the µ- and ν-extents being the same in theprobabilistic case is that the likelihood of never reaching y from either x or z is 0.
1
2 ,a

o

1
2 ,∗

y



1
2 ,b

Ax]
1
4 ,c

1
4 ,c

 q
z

Ax]

2,a

1
2 ,c

o

2,∗

y



0,c

1,b

0,c

 q
z

0,c

The notions of ν- and µ-extent turn out to be particularly useful when applied to the
product of two TS ◦ F -coalgebras; this collects their common F -behaviour, suitably quantified
with the help of the monad structure of TS .
I Definition 13. The product of TS ◦ F -coalgebras (C, γ) and (D, δ) is the TS ◦ F -coalgebrawith carrier C × D and transition function γ ⊗ δ given by
C ×D

γ×δ

/ TS F C × TS F D

dstF C,F D∗/ TS (F C × F D) hF π1 ,F π2 i / TS F (C × D)

where hF π1 , F π2 i∗ is pre-composition with hF π1 , F π2 i : F (C × D) → F C × F D.
The effect of pre-composing with hF π1 , F π2 i is that pairs of non-matching one-step behaviours
are discarded from the resulting coalgebra.
Our first result relates the ν- and µ-extents of the product of two coalgebras with the
maximal and respectively finite trace similarity relation between them.
I Theorem 14. Let (C, γ) and (D, δ) be two TS ◦ F -coalgebra. The ν-extent (µ-extent) of
the product coalgebra (C × D, γ ⊗ δ) coincides with the maximal trace similarity relation 'νγ,δ
(resp. the finite trace similarity relation 'µγ,δ ).
Proof (sketch). The proof involves showing that the operators used in the definition of 'νγ,δ
and 'µγ,δ on the one hand, and of the ν-/µ-extent of the product automaton on the other,coincide.
JCorina Cîrstea, Shunsuke Shimizu, and Ichiro Hasuo

7:9

Parity (S, F )-Automata and their Extent

4

We now consider parity (S, F )-automata, as extensions of TS ◦F -coalgebras with a parity map,and define their extent. Parity maps are a natural way to formulate acceptance conditions forautomata on infinite words/trees: the states of the automaton are assigned natural number
parities, and a run of the automaton is accepting iff the largest parity occurring infinitely
often along the run is even (see e.g. [11]). We use parity maps in a similar way, but this timein a quantitative setting where the emphasis moves away from individual runs.
I Definition 15. A parity (S, F )-automaton is given by a TS ◦ F -coalgebra (A, α) together
with a function Ω : A → {1, 2, . . .} with finite range, called parity map.
A similar notion called (T, F )-system was considered in [17], albeit under different assumptions
on the monad T, which rule out semiring monads as considered here. A trace semantics fora (T, F )-system was defined in loc. cit. as a Kleisli map obtained by taking least and greatest
fixpoints, and this was proved to instantiate to the standard notions of acceptance by anon-deterministic, resp. probabilistic parity automaton. As in [17], our assignment of parities
to all states of the automaton allows for a smooth relationship to equational systems.
The extent of a parity automaton generalises the ν- and µ-extents of a coalgebra by taking
into account the different parities associated to the automaton states. The only difference isthat now the extent involves a collection of nested fixpoints, one for each parity.
I Definition 16. Let (A, α, Ω) be a parity (S, F )-automaton with ran(Ω) ⊆ {1, . . . , n}, let
Ak = {a ∈ A | Ω(a) = k}, and let αk = α ◦ ιk : Ak → TS F A denote the restriction of α to
Ak . The extent e = [e1 , . . . , en ] : A → S of (A, α, Ω) is the solution of the equational system
u1 =µ µ1 ◦ TS (•F ) ◦ TS F [u1 , . . . , un ] ◦ α1


..
(3)


.
un

=η

µ1 ◦ TS (•F ) ◦ TS F [u1 , . . . , un ] ◦ αnwith η = µ (η = ν) if n is odd (resp. even), with variables uk ranging over the poset (S Ak , v)
(and therefore [u1 , . . . , un ] : A → S), and with the rhss of the equations pictured below:
Akαk/ TS F A

TS F [u1 ,...,un ]/ TS F S

TS (•F )/ TS S = T2 1

µ1

S/ TS 1 = S

I Example 17. For non-deterministic/probabilistic/weighted systems, the extent captures
the existence/likelihood/minimal cost of an accepting run. For the coalgebras in Example 12,
assigning parities 1 to the states x and y and 2 to the state z yields automata with extents
mapping x to 0.4, y to 0.6 and z to 0.2, and resp. x to 1, y to 1 and z to 0. The reason for theextent being similar to the µ- and ν-extents of the underlying coalgebra in the probabilistic
case is that, although runs which visit z infinitely often contribute to the extent, under
the current assignment of probabilities to transitions, the contributed quantity is 0. The
situation would be different if the transition from z to x was removed and the one from z to5itself had probability 1, in which case the extent would map x to 12
14 , y to 7 and z to 1.
I Remark 18. A trace semantics for parity (S, F )-automata similar to that of [17] can also
be defined, using an equational system whose variables uk range over S Ak ×Z . In this case,the rhs of the kth equation is given by:
Ak × Zα×(ηF Z ◦ζ)/ TS F A × TS F Z

dst /TS (F A × F Z)

hF π1 ,F π2 i∗/ TS F (A × Z)
TS F [u1 ,...,un ]Soµ1

TS S oTS (•F )
TS F SCALCO 2017

7:10

Parity Automata for Quantitative Linear Time Logics

5

From Linear Time Logics to Parity (S, F )-Automata

We now show how to assign, to each clean and guarded formula of µLΛ (Definition 19),a parity (S, F )-automaton. We then give an automata-theoretic characterisation of thesemantics of a µLΛ -formula, using the extent of a product automaton (between a model anda formula automaton). The next definition is standard for fixpoint logics (see e.g. [18]).
I Definition 19. For a set V of variables, a formula ϕ ∈ µLV
Λ is clean if no variable appears
both free and bound, or is bound more than once, in ϕ, and guarded if each occurrence of abound variable inside its defining fixpoint formula lies within the scope of a modal operator.
For a clean formula ϕ ∈ µLV
Λ , we write BVar(ϕ) for its set of bound variables. Also, forx, y ∈ BVar(ϕ), we write ϕx = ηx.ψx for the unique sub-formula of ϕ which binds x, andy ≤ x iff ϕy is a sub-formula of ϕx . Our technical development will require first transforming
a guarded formula to a strictly guarded one, as defined below.
I Definition 20. A formula ϕ ∈ µLV
Λ is (i) strongly guarded if every occurrence of a fixpoint
variable x inside the defining formula ψy of a variable y (with y ≤ x) appears within thescope of a modal operator, and (ii) strictly guarded if every occurrence of a fixpoint variable
x inside ψx is immediately preceded by a modal operator.
Guardedness requires that, in the formula syntax tree, one cannot pass from a fixpoint
quantification ηy.ψy to an occurrence of y without encountering a modal operator. Strong
guardedness additionally requires that this is the case when passing from ηy.ψy to any fixpoint
variable x occurring inside ψy . It is easy to see that every guarded formula is equivalent toa strongly guarded one. To see this, assume for simplicity that S = ({0, 1}, ∨, 0, ∧, 1) andtherefore the logic only contains non-weighted sums (i.e. disjunctions) which we denote by +.
Then, a non-strongly guarded occurrence of variable x, necessarily of the form ηx.ϕ[η 0 y.(x+ψ)]with ϕ a formula with a guarded hole, is equivalent to ηx.ϕ[x + η 0 y 0 .ψ[(x + y 0 )/y]], where x is
now guarded in ψ[(x + y 0 )/y] as y was initially guarded in ψ. (This argument generalises toPweighted sums, where now x+ψ is replaced by i ci ψi with ψi = x for some i. However, when
S is a partial semiring, an additional unfolding of the formula η 0 y 0 .ψ[(x + y 0 )/y] is required,as the counterpart of the sum x + η 0 y 0 .ψ[(x + y 0 )/y] may not be defined.) Strict guardedness
additionally requires that occurrences of x inside ψy are immediately preceded by modal
operators. Given the distributivity of modal operators over weighted sums (an immediate
consequence of the definition of JλK), one can translate a strongly guarded formula into an
equivalent, strictly guarded one by pushing weighted sums outside the modal operators.
The next definition can be traced back to the notion of Fischer-Ladner closure [12].
I Definition 21. A set C ⊆ µLV
Λ of formulas is closed if
ψ[ηx.ψ/x] ∈ C whenever ηx.ψ ∈ C, for η ∈ {µ, ν},P
ϕi ∈ C for i ∈ {1, . . . , n}, wheneverci • ϕi ∈ C,i∈{1,...,n}ϕ1 , . . . , ϕar(λ) ∈ C whenever [λ](ϕ1 , . . . , ϕar(λ) ) ∈ C.
The closure Cl(ϕ) of a µLV
Λ -formula ϕ is the smallest closed set containing ϕ.
We note that Cl(ϕ) is always finite: the second and third clauses above can only be applied
finitely many times before the first clause applies; and applications of the first clause only
lead to the inclusion of a new formula in Cl(ϕ) once for each fixpoint sub-formula of ϕ.
We now exploit the close relationship between the logic µLΛ on the one hand and thesemiring S and endofunctor F on the other to associate, to each clean and strictly guarded
formula ϕ ∈ µLΛ , a parity (S, F )-automaton with carrier Cl(ϕ). To this end, we assign

Corina Cîrstea, Shunsuke Shimizu, and Ichiro Hasuo

7:11

natural numbers nx to variables x ∈ BVar(ϕ) in a way which is consistent with the order
BVar(ϕ), that is, nx ≤ ny whenever x ≤ y, and which differentiates between least andgreatest fixpoints, that is, nx is odd (even) if ϕx = µx.ψ (resp. ϕx = νx.ψ). The numberof parities can be optimised to equal the alternation depth of ϕ, given by the number ofalternations between least and greatest fixpoints [1]. Hereafter we assume that ϕ is a fixpoint
formula (otherwise the formula νx.ϕ with x a fresh variable can be considered instead).
I Definition 22. The parity (S, F )-automaton (Cl(ϕ), β, Ω) associated to a clean and strictly
guarded formula ϕ ∈ µLΛ with ϕ = ϕz = ηz.ψz has β : Cl(ϕ) → TS F Cl(ϕ) and Ω : Cl(ϕ) →{1, 2, . . .} defined by induction on the structure of Cl(ϕ):Ω(ηx.ψx ) = nx (and hence Ω(ϕ) = nz ),β(ηx.ψx ) = β(ψ[ηx.ψx /x]); Ω(ψ[ηx.ψ/x]) = nx , unless ψ[ηx.ψ/x] is a fixpoint formula
itself, in which caseapplies, the previous clausePPP
ci • ϕi = µF Cl(ϕ)β
ci β(ϕi ) ; Ω(ϕi ) = Ω(ci • ϕi ) for i ∈i∈{1,...,n}i∈{1,...,n}i∈{1,...,n}{1, . . . , n}, unless ϕi is a fixpoint formula, in which case the first clause applies,β([λ](ϕ1 , . . . , ϕar(λ) )) = ηF Cl(ϕ) (ιλ (ϕ1 , . . . , ϕar(λ) )); Ω(ϕi ) = Ω([λ](ϕ1 , . . . , ϕar(λ) )) fori ∈ {1, . . . , ar(λ)}, unless ϕi is a fixpoint formula, in which case the first clause applies,
with η : Id ⇒ TS and µ : T2S ⇒ TS the unit and resp. multiplication of TS . (Note thePdifference in denotations between the first and the second occurrences of thesymbol in thethird clause: the first is part of a propositional symbol of µLΛ , whereas the second describes
an element of TS TS F Cl(ϕ) as a formal sum.)Thus, formulas in Cl(ϕ) are assigned parities starting from the outermost formula, and with aformula receiving the same parity as the smallest formula which contains it – unless the given
formula is a fixpoint one ηx .ψx , in which case its parity is nx . This is standard (see e.g. [7]),and gives Ω(ψ 0 ) ≤ Ω(ψ) whenever ψ 0 is a sub-formula of ψ different from a fixpoint formula.
However, if a formula ψ ∈ Cl(ϕ) occurs several times within ϕ, Ω(ψ) is defined more thanonce according to the above definition. In this case, a copy of ψ should be made within Cl(ϕ)
for each occurrence of ψ, with different copies assigned possibly different parities. To avoid
complicating the definition of the parity automaton associated to ϕ, and our subsequent
exposition, we assume (for the above definition) that ϕ does not contain several occurrences ofany sub-formula. Our technical development does not, however, depend on this assumption.
The recursive definition of β, with base case [λ](ϕ1 , . . . , ϕar(λ) ), deviates from the more
standard approach to translating fixpoint formulas to automata (see e.g. [18]), which applies
more generally to unguarded formulas and involves an intermediate automaton with silent
steps. Here, silent steps are automatically absorbed into the next non-silent transition, withno unwanted consequences. This is possible due to our strict guardedness assumption:
1. Guardedness ensures well-definedness of β, as only a finite number of applications of thesecond and third clauses of Definition 19 are possible before the last clause applies.
2. Strict guardedness ensures that the implicit elimination of silent steps is such that every
path from ϕy to x in the formula syntax tree corresponds to a “path” from ϕy [ϕx /x] to
ϕx in the resulting automaton. Thus, states (such as ϕx ) with parities greater than theparity associated to ϕy are not sidestepped during the implicit elimination of silent steps.
The first formula of Example 23 illustrates why strict guardedness is needed.
I Example 23. Assume F = 1 + A × Id. Thus, the associated logic contains a single nullarymodality ∗ and unary modalities [a] with a ∈ A.
1. The strongly guarded formula ξx := νx.ξy with ξy := µy.[a](x + y), with associatedautomaton shown below on the left, is not strictly guarded. This automaton does not

CALCO 2017

7:12

Parity Automata for Quantitative Linear Time Logics

faithfully represent ξx , as it does not accept aω (since Ω(ξx + ξy [ξx /x]) = Ω(ξy ) = 1). On
the other hand, the automaton associated to the equivalent, strictly guarded formulaξx0 := νx.ξy0 with ξy0 := µy.([a]x + [a]y), shown below on the right, correctly accepts aω(as Ω(ξx0 ) = 2). The problem with ξx is that the path from ξy to x in the formula syntax
tree does not correspond to a path from ξx + ξy [ξx /x] to ξx in the resulting automaton(and similarly for the path from ξx to x).
a
a

ξx

a


/ ξx + ξy [ξx /x] o a ξy [ξx /x]

a


ξx0 k

-

a


ξy0 [ξx0 /x]a

2. The automata associated to the strictly guarded formulas ϕx := νx.(ϕy + [b]x) with
ϕy := µy.(∗ + [a]y), and ψx := νx.ψy with ψy := µy.[c]([a]x + [b]y), are:
b

o

∗



a

ϕx

a

/ ϕy

∗

/

ψx

x

a

b

[a]ψx + [b]ψy0
5
i
c

&

ψy0

c

with ψy0 := ψy [ψx /x], Ω(ϕx ) = Ω(ψx ) = 2 and Ω(ϕy ) = Ω(ψy0 ) = Ω([a]ψx + [b]ψy0 ) = 1.
Given a TS ◦F -coalgebra (C, γ) and ϕ ∈ µLΛ with associated automaton (Cl(ϕ), β, Ω), one
can endow the product of (C, γ) and (Cl(ϕ), β) with a parity map by setting Ω(c, ψ) = Ω(ψ)
for (c, ψ) ∈ C × Cl(ϕ). The next result provides a characterisation of JϕKγ using the extent
of the resulting parity automaton.
I Theorem 24. If (Cl(ϕ), β, Ω) with ran(Ω) ⊆ {1, . . . , n} is the parity automaton for a cleanand strictly guarded formula ϕ ∈ µLΛ , (C, γ) is a TS ◦ F -coalgebra and e = [(en )n∈ran(Ω) ] :A → S is the extent of the product parity automaton (A, α, Ω) of (C, γ) and (Cl(ϕ), β, Ω),then JϕKγ (c) = e(c, ϕ) for c ∈ C.
The proof of Theorem 24 involves defining an equational system Eϕ in generalised form (seeSection 2.4), whose solution is known to provide an alternative characterisation of JϕKγ , andproving that this solution can alternatively be characterised using the extent of the productautomaton (A, α, Ω). This intermediary result makes use of solution-preserving substitutionsof rhss of equations in Eϕ for the respective variables, to transform Eϕ into an equational
system equivalent to the one used to define the extent of the product automaton.
The equational system Eϕ employs a variable uψ ranging over S C for each formulaψ ∈ Cl(ϕ). In order to specify the rhss of Eϕ , we define, for each ψ ∈ Cl(ϕ), a termdψ : (S C )Cl(ϕ) → S C over these variables:d[λ](ϕ1 ,...,ϕar(λ) ) = γ ∗ (extF C (JλK(uϕ1 , . . . , uϕar(λ) ))),XdP
ci uϕi ),ci •ϕi = µ1 (i∈{1,...,n}(4)i∈{1,...,n}dηx.ψ = uηx.ψ .
I Definition 25. For ϕ ∈ µLΛ clean and strictly guarded, the system Eϕ collects (i) all
equations uηx.ψ =Ω(ηx.ψ) dψ[ηx.ψ/x] with ηx.ψ ∈ Cl(ϕ), and (ii) all equations uξ =Ω(ξ) dξ
with ξ ∈ Cl(ϕ), ξ 6= ηx.ψ, where the uψ s range over S C for ψ ∈ Cl(ϕ).
The following result is folklore (see e.g. [7] for a similar result).
I Proposition 26. For ϕ ∈ µLΛ clean and guarded, and (C, γ) a TS ◦ F -coalgebra, let(vψ )ψ∈Cl(ϕ) denote the solution of the equational system Eϕ . Then, for ψ ∈ Cl(ϕ), JψKγ :C → S coincides with dψ [(vξ /uξ )ξ∈Cl(ϕ) ].

Corina Cîrstea, Shunsuke Shimizu, and Ichiro Hasuo

7:13

I Example 27. The systems of equations associated to ξx and resp. ϕx of Example 23 are


uϕx
=2
µ1 (uϕy + u[b]ϕx ) u[b]ϕx =2 γ ∗ (extF C (JbKuϕx )) uξx=2uξy [ξx /x]∗ uξ [ξ /x]=1µ1 (u∗ + u[a]ϕy ) =1 γ (extF C (JaKuξx +ξy [ξx /x] )) 
y x

 uϕy
 u∗
=1
γ ∗ (extF C (J∗K)) uξx +ξy [ξx /x] =1µ1 (uξx + uξy [ξx /x])u[a]ϕy =1 γ ∗ (extF C (JaKuϕy ))The definitions of both Eϕ and β are driven by the structure of Cl(ϕ), and use the same
strategy to associate parities to formulas. However, the definition of β sidesteps certain
formulas during the implicit elimination of silent steps from the resulting automaton. The
proof of Theorem 24, not included here for space reasons, shows that, under the assumptionthat ϕ is strictly guarded, carrying out a suitable choice of substitutions (those implicitly
performed in the definition of β) on Eϕ results in an equational system equivalent to bothEϕ and the system of equations defining the extent of the product automaton.
For the modal µ-calculus, a converse translation, from parity automata to fixpoint
formulas, also exists. This is defined by induction on the number of parities and uses vectorialsyntax as an intermediary step. Vectorial syntax [1] generalises standard fixpoint calculus
syntax by replacing fixpoint variables with arrays of such variables, all with the same parity,with the corresponding fixpoints being computed simultaneously. A similar translation fromparity (S, F )-automata to µLΛ -formulas can be defined here. A translation from a parity(S, F )-automaton to vectorial syntax is straightforward: each automaton state yields a newvariable, with parity given by the automaton, and whose defining formula is taken from thecoalgebra map of the automaton. A translation from vectorial to standard syntax is thencarried out by appealing to the Bekič principle – this allows reducing a simultaneous fixpoint
to a sequence of individual fixpoints (see e.g. [1, Lemma 1.4.2]). The formula associated tothe original automaton can now be read directly from the resulting equational system.
I Theorem 28. For a parity (S, F )-automaton (A, α, Ω) with Amax(ran(Ω)) = {a}, there exists
ϕa ∈ µLΛ such that, for every TS ◦ F -coalgebra (C, γ), if e : [(en )n∈ran(Ω) ] is the extent of
the product parity automaton between (C, γ) and (A, α, Ω) then Jϕa Kγ (c) = e(c, a) for c ∈ C.
Proof (sketch). The proof closely follows that of [19, Theorem 34].

J

I Remark. The results of this section can easily be extended to the variant of µLΛ describedin Remark 6: while formula and model automata now have slightly different types, theirproduct, itself a parity (S, F )-automaton, can be constructed in a similar way.

6

From Parity to Büchi Automata

We now present a direct reduction from parity word automata to Büchi ones. Parity word
automata are parity (S, FΣ,∆ )-automata, with FΣ,∆ = Σ × Id + ∆ for alphabets Σ and ∆.
Büchi automata have ran(Ω) = {1, 2}. Here we additionally assume the semiring S to be total.
Our reduction involves manipulating “linear” equational systems; their rhss use operations
that resemble matrix-vector multiplication and vector addition, as defined below.
I Definition 29. Let X and Y be sets, and let M : X × Y → S and v : Y → S be a relation
and a predicate respectively. Assume M and v to have finite support. M • v : X → S isP
defined by (M • v)(x) =y∈Y M (x, y) • v(y) . For predicates v1 , v2 : Y → S, v1 + v2 isdefined by pointwisely extending + on S.
By the finite support property, M • v is well-defined even for X or Y infinite. The next
lemma concerning linear equational systems is key to our reduction.

CALCO 2017

7:14

Parity Automata for Quantitative Linear Time Logics
Figure 1 A step of the reduction from a parity automaton to a Büchi automaton. The number
on each node denotes its parity. This step does not change the accepted language ((b c∗ b)∗ (aa)∗)ω |((b c∗ b)∗ (aa)∗)∗ b cω | ((b c∗ b)∗ (aa)∗)∗ b c∗ c(ddd)∗ .
a

a

6

5
a

3

b

2

c

4
d

c

7−−−→

3

b

3

c

3
d

b

b

d

d

1

3
a

b

d

d

4

c
3

3

c

4
d

d

d

2

c
1

X

X

I Lemma 30. Let a set X = X1 +. . .+Xn , a number k ∈ [1, n] and a relation M : X ×X → S
be fixed. Let X≤k = X1 + . . . + Xk and X>k = Xk+1 + . . . + Xn . For a predicate v : X≤k → S,
the equational systems Ekη (v) and Ekµ (v), whose solutions belong to S X1 × . . . × S Xk ∼= S X≤k ,η
are defined as follows. Polarities η1 , . . . , ηk ∈ {µ, ν} of Ek (v) can be chosen arbitrarily.
u1 =η1 M1 • [u1 , . . . , uk ] + v1
u1 =µ M1 • [u1 , . . . , uk ] + v1




..
..
µ
Ekη (v) = 
 , Ek (v) = 

.
.
uk

=η k

Mk • [u1 , . . . , uk ] + vkuk=µMk • [u1 , . . . , uk ] + vk

Here each sub-relation Mi : Xi × X≤k → S and each sub-predicate vi : Xi → S are given bydomain restriction. Then for any v η , v µ : X≤k → S, the solution of Ekη (v η + v µ ) is obtainedby summing the solutions of Ekη (v η ) and Ekµ (v µ ).
The reduction proceeds in a step-wise manner, decrementing the largest parity, assumed
without loss of generality to be even, by 2 at each step. An example is given in Figure 1.
One reduction step is as follows:
1. Create a copy of states with parity lower than n − 1. Incoming (only!) edges to thosestates are also copied. (This is only possible if the semiring is total.)
2. For the old copy of states with parity lower than n − 1, let the new parity be n − 3 anddrop explicit terminations (i.e. transitions with a nullary letter).
3. Decrement the priorities of the other states by 2.
The intuition is that, from old copies of states, a state with parity higher than n − 2 must be
visited again for acceptance; whereas from new copies, such a state must not be visited. The
correctness of this translation is proved using Lemma 30. This also explains why the shapeof F must be restricted to FΣ,∆ – this makes extents be given by linear equational systems.
By repeatedly applying the reduction step, any parity (S, FΣ,∆ )-automaton A can be
reduced to a Büchi (S, FΣ,∆ )-automaton AB . Since the reduction is such that an accepting
path of A corresponds to exactly one accepting path of AB , idempotence of + is not required.
I Theorem 31. Let A = (A, α, Ω) be a parity (S, FΣ,∆ )-automaton with ran(Ω) = [1, n].
Assume without loss of generality that n is even. The Büchi (S, FΣ,∆ )-automaton AB =(AB , αB , ΩB ) is given by`
AB = k∈[1,n] Ak × {i | i ∈ [k, n], i is even}(α(a)(ισ (a0 )) if i = j, or dΩ(a)e = i and i > jB0
α (a, i)(ισ (a , j)) =0otherwise(α(a)(ιδ )if dΩ(a)e = i
αB (a, i)(ιδ ) =0otherwise

Corina Cîrstea, Shunsuke Shimizu, and Ichiro Hasuo(ΩB (a, i) =2

if dΩ(a)e = i and i is even1otherwise

Here dΩ(a)e = min{k | k ≥ Ω(a) and k is even}. The automaton AB satisfies
PB
ext(A × M)(a, m) =(a,i)∈AB ext(A × M)((a, i), m)

7:15

(5)

for any TS ◦ FΣ,∆ -coalgebra M and each (a, m) ∈ A × M .
I Remark 32. The definition of AB does not generalise to partial semirings S, due to the
duplication of states involved. However, if S can be extended to a total semiring S 0 satisfying
our assumptions, then carrying out the reduction for A as an (S 0 , FΣ,∆ )-automaton yields
the desired result, namely a Büchi (S 0 , FΣ,∆ )-automaton AB that satisfies condition (5). In
particular, this means that one can treat the probabilistic case (S = ([0, 1], +, 0, ∗, 1)) bymoving to the total semiring S 0 = (R∞ , +, 0, ∗, 1). Specifically, one can model check formulasin our probabilistic linear time µ-calculus by (i) taking the product of the given model andformula automata, (ii) reducing the resulting automaton, viewed as an (S 0 , FΣ,∆ )-automaton,
to a Büchi one, and (iii) computing the extent of the (S 0 , FΣ,∆ )-automaton thus obtained.
Theorem 31 together with the existence of semantics preserving translations from µLΛ formulas to parity (S, F )-automata and back (Theorems 24 and 28) now give us the following:
I Corollary 33. For F = FΣ,∆ , the alternation degree 1 fragment of µLΛ is fully expressive.

7

An Algorithm for Computing Extents

We now describe an algorithm for computing the extent of a parity (S, F )-automaton, under
the additional assumption that the length of any strictly ascending/descending chain in (S, v)
is bounded. Both the boolean semiring and the bounded version of the tropical semiring (seeExample 2) satisfy this assumption.
We fix a parity (S, F )-automaton (A, α, Ω). Thus, for a ∈ A, α(a) is a finite weighted
sum of tuples ιλ (a1 , . . . , ak ) with λ ∈ Λ, k = ar(λ) and ai ∈ A. The algorithm is describedin Figure 2, and employs a recursive procedure Extent(n ∈ ω).
To see that the algorithm terminates, note that each call of Extent(n) either increases ordecreases all the values in An . The assumed bound on the length of strictly ascending/descending chains guarantees termination of each call: each iteration of the repeat . . . untilchanges at least one of the values e(a) with a ∈ An . Several improvements to the algorithm
are possible, e.g. only remembering certain extent values (those with parity n) in the variable
old; and deferring the recursive call until the approximation on the current parity saturates.
Next, we discuss complexity. If |ran(Ω)| = 1, and assuming for simplicity that S is finite,
the algorithm has a time complexity which is quadratic in the size of the automaton – thelength of a strictly increasing/decreasing chain in B Ai is at most |Ai ||B|, each iteration (lines
8-10 in the algorithm) increases/decreases at least one of the values e(a), and takes time linear
in |A|. If |ran(Ω)| = m > 1, then since each recursive call of Extent only updates values e(a)Qwith a ∈ Ai , for some i ∈ ran(Ω), the time complexity is O(|A||ran(Ω)| |B||ran(Ω)| i∈ran(Ω) |Ai |).
We conclude by noting that, for Büchi (S, F )-automata, the algorithm can be generalised
to semirings S where only strictly ascending chains in (S, v) are required to have bounded
length. This extends applicability e.g. to the tropical semiring. Instead of the exact extent of a
Büchi automaton, the generalised algorithm computes increasingly finer over-approximationsof the extent. The boundedness assumption guarantees that inner calls to Extent terminate.

CALCO 2017

7:16

Parity Automata for Quantitative Linear Time Logics
Figure 2 Algorithm for computing the extent e : A → S of (A, α, Ω)Input: parity automaton (A, α, Ω)Output: extent e : A → S of (A, α, Ω)
1. let e := [a 7→ 0S ]2. Extent(max(ran(Ω)))
Procedure Extent(n ∈ N)
1. if n = 0 then return endif
2. for a ∈ A(
n do
0S , if n is even
3. e(a) ←1S , otherwise
4. endfor
5. repeat
6. let old := e
7. e ← Extent(n − 1)
8. for a ∈ APn do
9.
e(a) ← i∈I vi • old(a1 ) • . . . • old(aji )P
where α(a) = i∈I vi ιλ (a1 , . . . , aji )10. endfor
11. until e = old8Lines 8-10 of the Extent procedurecompute a better approximation of theextent for automaton states with thecurrent parity n, based on a one-step
unfolding of the automaton transition
structure.
Line 7 computes the extent of stateswith immediately lower parity, relative
to the current values for states withparity n, through a recursive call toExtent (which may involve further recursive calls).
Recursive calls to Extent update thesame copy of e, and only make an additional copy to remember values fromthe previous step.

Related Work and Concluding Remarks

A study of fixpoint calculi over an arbitrary signature Σ, including a translation from suchcalculi to Σ-automata, is carried out at an abstract level in [1, Section 7]. However, thefixpoint calculi of loc. cit. are intrinsically boolean (their semantics is given in terms of parity
games), and therefore they do not subsume the quantitative logics described here. Our logics
share many features with concrete µ-calculi, and our translations from formulas to automata
and back resemble existing ones (see e.g. [19, Section 5.3]). Yet, our logics differ in theirquantitative semantics, which, in particular, means that an equivalent semantics based onparity games is not available anymore. Moreover, our (quantitative semantics preserving)translation from formulas to automata is presented in a way which exposes and exploits thecoalgebraic structures present in both models and formulas.
Theorems 24 and 28 are similar to results in [18], which also provide a coalgebraic
perspective on the connection between fixpoint logics and automata. Differently from[18], our construction of the automaton for a formula avoids the use of silent transitions(by exploiting specific properties of our logics) and, more importantly, applies also toquantitative logics. Thus, our results go beyond existing ones, both in the case of probabilistic
systems (given our choice of logics) and in the case of weighted systems (where we are notaware of similar translations). In particular, for probabilistic systems, our logics are subtly
different from existing ones (they contain sub-convex combinations of formulas but no puredisjunctions/conjunctions), yet are at least as expressive (see Remark 6).
Our parity-Büchi translation (Theorem 31) is novel in two ways: (i) unlike existingtranslations (e.g. from probabilistic Rabin to probabilistic Büchi automata [2]) which preserve
only the qualitative language, our translation preserves the quantitative language, and (ii) ourresult comes with a proof which is not a generalisation of any proof we are aware of in thequalitative case. Thus, the jump from a qualitative to a quantitative setting is non-trivial.
Our (admittedly trivial) model checking algorithm has complexity similar to that ofknown algorithms for the qualitative case [14], while also being applicable in quantitative

Corina Cîrstea, Shunsuke Shimizu, and Ichiro Hasuo

7:17

settings. Currently this only includes semirings with finite strictly ascending/descending
chains. Such semirings can e.g. be used to model resource usage with bounded resources.
The study of more generally applicable algorithms is left as future work. For this, our recent
lattice-based generalisation of the notion of progress measure [13], so far mainly studied inconnection with branching time logics, is expected to prove useful.
References
1
2
3
4

5
6
7
8

9

10
11
12
13

14

15
16
17

18
19

A. Arnold and D. Niwiński. Rudiments of µ-Calculus. Studies in Logic and the Foundationsof Mathematics. North-Holland, 2001.
C. Baier, M. Größer, and N. Bertrand. Probabilistic ω-automata. J. ACM, 59(1):1, 2012.
C. Baier and J.-P. Katoen. Principles of model checking. MIT Press, 2008.
C. Cîrstea. A coalgebraic approach to linear-time logics. In A. Muscholl, editor, Foundationsof Software Science and Computation Structures, 17th International Conference, pages 426–
440. Springer, 2014.
C. Cîrstea.
A coalgebraic approach to quantitative linear time logics.
CoRR,
abs/1612.07844, 2016. URL: http://arxiv.org/abs/1612.07844.
C. Cîrstea. From branching to linear time, coalgebraically. Fundamenta Informaticae,
150:1–28, 2017.
R. Cleaveland, M. Klein, and B. Steffen. Faster model checking for the modal µ-calculus. In
Computer Aided Verification, 4th International Workshop, pages 410–422. Springer, 1993.
D. Coumans and B. Jacobs. Scalars, monads, and categories. In Quantum Physics and
Linguistics. A Compositional, Diagrammatic Discourse, pages 184–216. Oxford Univ. Press,2013.
M. Dam. Fixed points of Büchi automata. In R. Shyamasundar, editor, Foundationsof Software Technology and Theoretical Computer Science, 12th Conference, pages 39–50.
Springer, 1992.
B. A. Davey and H. A. Priestley. Introduction to Lattices and Order (2. ed.). Cambridge
University Press, 2002.
B. Farwer. ω-Automata. In E. Grädel, W. Thomas, and T. Wilke, editors, Automata,
Logics, and Infinite Games: A Guide to Current Research, pages 3–20. Springer, 2002.
M. J. Fischer and R. E. Ladner. Propositional dynamic logic of regular programs. Journalof Computer and System Sciences, 18(2):194 – 211, 1979.
I. Hasuo, S. Shimizu, and C. Cîrstea. Lattice-theoretic progress measures and coalgebraic
model checking. In 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles ofProgramming Languages, pages 718–732, 2016.
D. Kirsten. Alternating tree automata and parity games. In E. Grädel, W. Thomas, and
T. Wilke, editors, Automata Logics, and Infinite Games: A Guide to Current Research,
pages 153–167. Springer, 2002.
I. Meinecke. A weighted µ-calculus on words. In 13th International Conference on Developments in Language Theory, pages 384–395. Springer, 2009.
M. O. Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society, 141:1–35, 1969.
N. Urabe, S. Shimizu, and I. Hasuo. Coalgebraic Trace Semantics for Büchi and Parity
Automata. In J. Desharnais and R. Jagadeesan, editors, 27th International Conference on
Concurrency Theory, volume 59 of LIPICS, pages 24:1–24:15, 2016.
Y. Venema. Lectures on the modal µ-calculus. Lecture notes, Institute for Logic, Language
and Computation, University of Amsterdam, 2012.
I. Walukiewicz.
Automata and logic, 2001.
Notes available fromhttp://www.labri.fr/perso/igw/Papers/igw-eefss01.ps.

CALCO 2017

7:18

Parity Automata for Quantitative Linear Time Logics

A

Omitted Proofs

Proof of Theorem 14
We show that the operators used in the definition 'νγ,δ and 'µγ,δ on the one hand, and ofthe ν/µ-extent of the product automaton on the other, coincide. For maximal/finite trace
similarity, the operator takes r : C × D → S to L0S (Rel(F )(r)) ◦ (γ × δ), whereas for theν/µ-extent of (C × D, γ ⊗ δ), the operator takes r : C × D → S to µ1 ◦ TS (•F ) ◦ TS F r ◦hF π1 , F π2 i∗ ◦ dstF C,F D ◦ (γ × δ). Based on the definition of L0S (Rel(F )(r)), it suffices toshow:
TS (Rel(F )(r)) = TS (•F ) ◦ TS F r ◦ hF π1 , F π2 i∗(6)This follows from the commutativity of the diagram below:
TS (F X × F A)OTS (Rel(F )(r))

TS hF π1 ,F π2 i

/ TS SO(7)

T•F

TS F (X × A)

TS F r/ TS F S

together withTS (Rel(F )(r)) ◦ TS hF π1 , F π2 i ◦ hF π1 , F π2 i∗ =TS (Rel(F )(r))(8)

by the following argument:
TS (Rel(F )(r)) =∗TS (Rel(F )(r)) ◦ TS hF π1 , F π2 i ◦ hF π1 , F π2 i =(by (8))(by (7))∗

TS (•F ) ◦ TS F r ◦ hF π1 , F π2 i

In turn, (7) follows directly from the definitions of Rel(F ) and •F , whereas (8) follows fromthe definition of Rel(F )(r) using that Rel(F )(r)(f, g) = 0 for (f, g) 6∈ Im(hF π1 , F π2 i).

Proof of Theorem 24
We begin by recalling that the extent e = [(en )n∈ran(Ω) ] : A → S (Definition 16) of the productautomaton (A, α, Ω) between (C, γ) and (Cl(ϕ), β, Ω) is the solution of the equational systemwith variables un ranging over S C×Cl(ϕ)n , with the defining term of un (which from now on
we denote by tn ) given by the composition:
C × Cl(ϕ)n/ TS F C × TS F Cl(ϕ)

γ×βn

dst /

TS (F C × F Cl(ϕ))

hF π1 ,F π2 i∗/ TS F (C × Cl(ϕ))

TS F [(un )n∈ran(Ω) ]Soµ1

TS S oTS (•F )
TS F SOn the other hand, the equational system Eϕ of Definition 25 has one variable uψ withpriority Ω(ψ) for each formula ψ ∈ Cl(ϕ), with the defining term of uψ (which from now on
we denote by tψ ) having one of three forms, depending on the shape of ψ:
1. For ψ = [λ](ψ1 , . . . , ψi ):Cγ/ TS F C

where i = ar(λ).

(ιλ )∗/ TS C ar(λ)

TS (×l∈{1,...,i} uψi )/ TS S i

TS •/ TS S µ1 / S(9)Corina Cîrstea, Shunsuke Shimizu, and Ichiro Hasuo

2. For ψ =

P

7:19

ci • ψi :i∈{1,...,n}

P

µ1

C

huψ1 ,...,uψn i/ Sni∈{1,...,n}

ci _


/S

3. For ψ = ηx.ψ 0 :C

dψ0 [ηx.ψ0 /x]/S

where dψ0 [ηx.ψ0 /x] is as in (4).
In general, a series of substitutions is required to transform Eϕ into an equational systemthat matches β. Similarly, a series of substitutions is required to transform Eϕ into a standard
equational system, with the equations for the latter being in one-to-one correspondence withthe fixpoint sub-formulas of ϕ. To define such a series of substitutions, we will use the notionof a tree of substitutions.
For any o : S C×Cl(ϕ) → S C and ψ ∈ Cl(ϕ) (with associated tψ : S C×Cl(ϕ) → S C ), leto[tψ /uψ ] : S C×Cl(ϕ) → S C be defined by o[tψ /uψ ](r) = o(r[tψ (r)(c)/(c, ψ)]). Intuitivelyo[tψ /uψ ] is obtained by substituting tψ for uψ within o. We will use this to replace occurrencesof the variable uψ in the right hand side of an equation by tψ . This is safe as long as theparity of uψ is less than or equal to the parity of the given equation [1, Proposition 1.4.14].
I Definition 34. Let ξ ∈ Cl(ϕ). The tree of substitutions for uξ is the finite tree each ofwhose nodes is labelled by some tψ with ψ ∈ Cl(ϕ), such that:the root of the tree is labelled by tξ ,a node labelled by [λ](uψ1 , . . . , uψn ) with λ ∈ Λ is a leaf,Pthe child nodes of a node labelled by i∈{1,...,n} ci • uψi are trees of substitutions for thevariables uψ1 , . . . , uψn ,the only child node of a node labelled by uψ is a tree of substitutions for uψ .
Thus, the tree of substitutions for ξ matches the structure of tξ , up to the places where
modalities are present in the formula syntax tree. Moreover, any sub-tree of a tree ofsubstitutions is itself a tree of substitutions (for a different variable). The guardedness
assumption ensures that any tree of substitutions is finite.
I Definition 35. Given o : S C×Cl(ϕ) → S C and a variable uξ with ξ ∈ Cl(ϕ), with associatedtree of substitutions T , we let o[T ] : S C×Cl(ϕ) → S C be defined recursively as follows:
if T is a leaf node tψ , then o[T ] is the same as o[tψ /uψ ],P
if T is a node labelled by i∈{1,...,n} ci • uψi and child nodes Ti for i ∈ {1, . . . , n}, thenPo[T ] is given by o[ i∈{1,...,n} (ci • uψi [Ti ])/uP
ci •ψi ],i∈{1,...,n}if T is a node labelled by uψ with the only child node T 0 , then o[T ] is given by o[uψ [T 0 ]/uψ ].
We can now associate another equational system Eϕ0 to each formula ϕ ∈ µLΛ .
I Definition 36. For ϕ ∈ µLΛ clean and strictly guarded, the system Eϕ0 collects all equationsuψ =Ω(ψ) uψ [T ], with T the tree of substitutions for uψ , for ψ ∈ Cl(ϕ).
I Remark. The strict guardedness assumption ensures that, in the system of equations Eϕ0 ,only variables of the form ux with x ∈ BVar(ϕ) or u[λ]ψ with [λ]ψ ∈ Cl(ϕ) are used in therhss.

CALCO 2017

7:20

Parity Automata for Quantitative Linear Time Logics

I Example 37. Let ϕx and ϕy be as in Example 23. The tree of substitutions T for uϕx is
given below:
tϕx = uϕy + u[b]ϕxtϕy = u∗ + u[a]ϕy(t[b]ϕx = [b]uϕxt∗ = ∗(
t[a]ϕy = [a]uϕy

The result of uϕx [T ] is the formula (∗ + [a]ϕy ) + [b]ϕx . On the other hand, the equational
system Eϕ0 x is as follows:
uϕx=2 µ1 (µ1 (γ ∗ (extF C (J∗K)) + γ ∗ (extF C (JaKuϕy ))) + γ ∗ (extF C (JbKuϕx )))
 uϕy

=1
µ1 (γ ∗ (extF C (J∗K)) + γ ∗ (extF C (JaKuϕy )))


∗
 u∗

=
γ
(ext
(J∗K))
1
FC


u

=1
γ ∗ (extF C (JbKuϕ ))[b]ϕx

u[a]ϕyx=1γ ∗ (extF C (JaKuϕy ))The equational system Eϕ0 is obtained from Eϕ by performing trees of substitutions driven
by the rhss of the equations in Eϕ . Such substitutions are only guaranteed to preserve thesolution of the equational system if the parity associated to uψ is at most that of the equation
substituting into (see [1, Proposition 1.4.14]). The next lemma shows that this is indeed thecase. The strict guardedness of ϕ is crucial here.
I Lemma 38. For ϕ ∈ µLΛ strictly guarded and ψ ∈ Cl(ϕ), the tree of substitutions for uψ
is such that, for any node of T , labelled by tψ , with children Ti whose roots are labelled bytψi for i ∈ {1. . . . , n}, Ω(ψ) ≥ Ω(ψi ).
Proof. Induction on T . The base case is trivial. For the inductive step, there are twocases: (i) T is labelled by uξ . In this case, both ψ and ξ are fixpoint formulas, with
ψ := ηx.ψ 0 and ξ = ψ 0 [ψ/x]. The definition of Ω now gives Ω(ξ) < Ω(ψ). (ii) T is labelledPby i∈{1,...,n} ci • ψi . Then, by strict guardedness, none of the ψi s can be a fixpoint formula.
Hence, by the definition of Ω, Ω(ψi ) = Ω(ψ) for i ∈ {1, . . . , n}.
J
By Lemma 38, the (trees of) substitutions used to obtain Eϕ0 from Eϕ are solutionpreserving. This now gives:
I Lemma 39. The solution of Eϕ0 coincides with that of Eϕ .
Proof. Fix a formula uψ and let T be the tree of substitutions for uψ . The conclusion follows
by induction on the structure of T . The base case is immediate, since a leaf node T will beof the form tψ = [λ]ψ and therefore the resulting equation of Eϕ0 is the same as the original
one in Eϕ , namely uψ =Ω(ψ) tψ (no substitution is performed). For the inductive step, thefollowing two cases need to be distinguished:P
If the root of T is labelled by i∈{1,...,n} ci • uψi , assuming that all substitutions uψi [Ti ]Pare safe, then since by definition Ω( i∈{1,...,n} ci • uψi ) = Ω(uψi ) for i ∈ {1, . . . , n}, itfollows that the substitution uψ [T ] is also safe.
If the root of T is labelled by uξ and with only child node T 0 , this necessarily means that
ξ is a fixpoint (strict) sub-formula of ψ, with ψ a fixpoint formula itself. In this case,substituting uψ [T ] = uξ [T 0 ] into the rhs (uξ ) of the defining equation of uψ is clearly safe,
given that the assignment of priorities respects the nesting of fixpoint formulas.

Corina Cîrstea, Shunsuke Shimizu, and Ichiro Hasuo

7:21

J
As illustrated by the formula ϕx of Example 37, the equational system Eϕ0 matches
the definition of (Cl(ϕ), β, Ω) very closely. The next result makes this relationship formal,
showing that the equational system Eϕ0 is equivalent to the equational system used to define
the extent of the product automaton (A, α, Ω).
I Lemma 40. For ψ ∈ Cl(ϕ), the tree of substitutions T for uψ satisfiestΩ(ψ) (r)(c, ψ) = uψ [T ](r)(c)for any r : C × Cl(ϕ) → S and c ∈ C. Note that tΩ(ψ) : S C×Cl(ϕ)n → S C and uψ [T ] :(S C )Cl(ϕ) → S C can be applied to r, respectively, because of the isomorphisms r ∼= (rn : C ×
Cl(ϕ)n → S)n∈ran(Ω) and r ∼= (rψ : C → S)ψ∈Cl(ϕ) .
Proof. We prove this claim by structural induction on T .
1. Assume T a leaf node labelled by [λ](uψ1 , . . . , uψi ), and therefore ψ = [λ](ψ). Fixr : C × Cl(ϕ) → S. The term tΩ(ψ) (r) acts (c, [λ](ψ)) with ψ = (ψ1 , . . . , ψi ) as follows:(c, [λ](ψ))

  dst P
hf π1 ,f π2 i∗ γ×β / P d f , η//
dj (fj , ιλ (ψ)) j j f Cl(ψ) (ιλ (ψ))
j∈JP
fj =ιλ (cj1 ,...,cji )j∈J

dj ιλ ((cj1 , ψ1 ), . . . , (cji , ψi )) 

TS F r/dj ιλ (r(cj1 , ψ1 ), . . . , r(cji , ψi )) 

TS (•f )P
fj =ιλ (cj1 ,...,cji )P
fj =ιλ (cj1 ,...,cji )P
fj =ιλ (cj1 ,...,cji )dj (r(cj1 , ψ1 ) • . . . • r(cji , ψi ))



/

/

µ1

dj • r(cj1 , ψ1 ) • . . . • r(cji , ψi )Thus, tΩ([λ]ψ) (r)(c, [λ]ψ) =P
fj =ιλ (cj1 ,...,cji )dj • r(cj1 , ψ1 ) • . . . • r(cji , ψi ).

The rhs for u[λ](ψ) in the equational system Eϕ0 (Definition 36) is tψ = [λ](uψ1 , . . . , uψi ).
Thus, u[λ](ψ) [T ] is itself given by u[λ](ψ) [T ], and therefore u[λ](ψ) [T ](r) acts on c ∈ C as
follows:∗
P TS F r / (ιλ ) /
 γ / P
dj fj ∈ TS f c
dj (cj1 , . . . , cji ) ∈ TS cicj∈JPfj =ιλ (cj1 ,...,cji )P
fj =ιλ (cj1 ,...,cji )P
fj =ιλ (cj1 ,...,cji )fj =ιλ (cj1 ,...,cji )dj (rψ1 (cj1 ), . . . , rψi (cji )) ∈ TS S i 
dj (rψ1 (cj1 ) • . . . • rψi (cji )) ∈ TS S
dj • rψ1 (cj1 ) • . . . • rψi (cji ) =

TS •s



µ1

/
/

P
fj =ιλ (cj1 ,...,cji )dj • r(cj1 , ψ1 ) • . . . • r(cji , ψi )It now follows that tΩ([λ]ψ) (r)(c, [λ]ψ) = u[λ](ψ) [T ](r)(c).

CALCO 2017

7:22

Parity Automata for Quantitative Linear Time Logics

P

2. Assume T is a substitution tree withci • uψi as the root and substitution treesPci • ψi . Fix r : C × Cl(ϕ) → S. By thei∈{1,...,n}Ti for uψi as direct sub-trees. Hence, ψ =i∈{1,...,n}definition of β, the action of tΩ(

ci •ψi ) , as the defining term for uΩ(Pi∈{1,...,n}is given by:Ptci •ψi ) (r) c,Ω(i∈{1,...,n}On the other hand, ui∈{1,...,n}ci •ψi ) ,i∈{1,...,n}
ci • ψi = µ1

P

P

P

ci tΩ(ψi ) (r)(c, ψi )



(10)

i∈{1,...,n}ci •ψi [T ] is given byPi∈{1,...,n}uci •ψi [T ](r)(c)

P

X

= µ1


(ci • uψi [Ti ])(r)(c)i∈{1,...,n}i∈{1,...,n}

X

= µ1

(ci uψi [Ti ](r)(c))



(11)

i∈{1,...,n}

By the induction hypothesis, we haveuψi [Ti ](r)(c) = tΩ(ψi ) (r)(c, ψi )(12)

The following equalities now hold by (11) and (12)Xu P ci •ψi [T ](r)(c) = µ1
ci uψi [Ti ](r)(c)i∈{1,...,n}i∈{1,...,n}

X

= µ1


ci tΩ(ψi ) (r)(c, ψi )(13)

i∈{1,...,n}and finally the statement follows by (10) and (13).
3. Assume T is a substitution tree with root labelled by uξ and T 0 as the only sub-tree.
Hence, ψ = ηx.ψ 0 and ξ = ψ 0 [ψ/x]. Fix r : C × Cl(ϕ) → S. The following are immediate
consequences of the respective definitions:tΩ(ηx.ψ0 ) (r)(c, ηx.ψ 0 ) = tΩ(ψ0 [ηx.ψ0 /x]) (r)(c, ψ 0 [ηx.ψ 0 /x])

(14)

0

(15)

u

ηx.ψ 0[T ](r)(c) = uξ [T ](r)(c)Moreover, by the induction hypothesis, we havetΩ(ξ) (r)(c, ξ) = uξ [T 0 ](r)(c)(16)

Substituting ψ 0 [ηx.ψ 0 /x] for ξ in (16) and combining the result with (15) yields
uηx.ψ0 [T ](r)(c) = tΩ(ψ0 [ηx.ψ0 /x]) (r)(c, ψ 0 [ηx.ψ 0 /x])

(17)

The conclusion now follows from (14) and (17).
J
We can now formally state the relationship between the solution of the equational system
Eϕ and the extent of the product of (C, γ) with the parity automaton (Cl(ϕ), β, Ω).
I Lemma 41. For ϕ ∈ µLΛ clean and strictly guarded, and (C, γ) a TS ◦ F -coalgebra, let(vψ )ψ∈Cl(ϕ) denote the solution of the equational system Eϕ , let (Cl(ϕ), β, Ω) denote the parity
automaton associated to ϕ, and let e = [(en )n∈ran(Ω) ] : A → S denote the extent of the productparity automaton (A, α, Ω) of (C, γ) and (Cl(ϕ), β, Ω). Then tψ [(vξ /uξ )ξ∈Cl(ϕ) ](c) = e(c, ψ)for all c ∈ C and ψ ∈ Cl(ϕ).

Corina Cîrstea, Shunsuke Shimizu, and Ichiro Hasuo

Proof. Immediate from Lemmas 39 and 40.

7:23

J

A final lemma relates the solution of Eϕ with the semantics of formulas in Cl(ϕ).
I Lemma 42. For ϕ ∈ µLΛ clean and strictly guarded, and (C, γ) a TS ◦ F -coalgebra, let(vψ )ψ∈Cl(ϕ) denote the solution of the equational system Eϕ0 over S C . Then, for ψ ∈ Cl(ϕ),
JψKγ : C → S coincides with tψ [(vξ /uξ )ξ∈Cl(ϕ) ].
Proof. As a result of strict guardedness, the only variables used in the rhss of Eϕ0 are of theform uψ , with ψ either a fixpoint formula or a formula of the form [λ]ψ. By successively
substituting all the rhss of the equations for u[λ]ψ into the remaining rhss of equations
in Eϕ0 (and noting that since Ω([λ]ψ) = min{ nx | x ∈ BVar(ϕ) }, such substitutions are
solution-preserving), it is not difficult to see that one now obtains the standard equational
system induced by the formula ϕ, whose solution, equal to (vψ )ψ∈Cl(ϕ) , is known to satisfy
the property in the statement of the lemma. This concludes the proof.
J
Theorem 24 now follows from Lemma 41 and Proposition 26.

Proof of Lemma 30
I Definition 43. When a partition X = X1 + · · · + Xn is given, for each k ∈ [1, n] we denote`
iQk Xi by XQk .
For X = X1 + · · · + Xm , Y = Y1 + · · · Yn and a relation M : X × Y → S, the sub-relation
MQj,Qk : XQj × YQk → S is defined by restricting the domain of M to XQj × YQk . For any
predicate v : Y → S, in the similar manner, sub-predicates vk : Yk → S and vQ : YQk → S is
defined.
I Definition 44. For an equational system E with n equations, which solution is given by
v1 , . . . , vn , let JEK = hv1 , . . . , vn i and JEKi = vi for each i ∈ {1, . . . , n}, where hv1 , . . . , vn i isthe product of v1 , . . . , vn .
Proof. The claim is shown by induction on k. Assuming the claim holds up to k, we show
the claim for k + 1. Fix predicates v η , v µ : X>k+1 → S. It suffices to show that
η
η
µ
JEk+1
(v η + v µ )Kk+1 = JEk+1(v η )Kk+1 + JEk+1(v µ )Kk+1 ,

(18)

η
η
µ
since the equation JEk+1(v η + v µ )Kj = JEk+1(v η )Kj + JEk+1(v µ )Kj for each j ∈ [1, k] immedi-

ately follows from (18).
Let us define three functions oηµ , oη , oµ : S Xk+1 → S Xk+1 byqη
µ yoηµ (w) = Mk+1,≤k • Ekη M≤k,k+1 • w + v≤k
+ v≤k
+

η
µ
Mk+1,k+1 • w + vk+1
+ vk+1qyηηoη (w) = Mk+1,≤k • Ekη M≤k,k+1 • w + v≤k+ Mk+1,k+1 • w + vk+1qµ yµoµ (w) = Mk+1,≤k • Ekµ M≤k,k+1 • w + v≤k+ Mk+1,k+1 • w + vk+1.

By the definition of solutions, (18) is equivalent to the following.

lfp[oηµ ] = lfp[oη ] + lfp[oµ ]if ηk = µgfp[oηµ ] = gfp[oη ] + lfp[oµ ]if ηk = ν

(19)

(20)

For any ∗ : Xk+1 → S, we show for each i < ω that(oηµ )i (∗) = (oη )i (∗) + (oµ )i (⊥) .

(21)

CALCO 2017

7:24

Parity Automata for Quantitative Linear Time Logics

Intuitively this can be shown by i-steps unfolding of the inner fixpoints. It is proven by
induction on i; that is, assuming (21) holds up to i, we have(oηµ )i+1 (∗)
qηµ y= Mk+1,≤k • Ekη M≤k,k+1 • (oηµ )i (∗) + v≤k
+ v≤k
+
η
µ
Mk+1,k+1 • (oηµ )i (∗) + vk+1
+ vk+1by def. (19)
q η
η
µ y
η i
µ i
= Mk+1,≤k • Ek M≤k,k+1 • (o ) (∗) + M≤k,k+1 • (o ) (⊥) + v≤k + v≤k +ηµMk+1,k+1 • (oη )i (∗) + Mk+1,k+1 • (oµ )i (⊥) + vk+1
+ vk+1by ind. on i
q η
y
η
η
η i
η i
= Mk+1,≤k • Ek M≤k,k+1 • (o ) (∗) + v≤k + Mk+1,k+1 • (o ) (∗) + vk+1 +qµ yµMk+1,≤k • Ekµ M≤k,k+1 • (oµ )i (⊥) + v≤k+ Mk+1,k+1 • (oµ )i (⊥) + vk+1

by ind. on k
η i+1

= (o )µ i+1(∗) + (o )(⊥)

by def. (19).

Assume the case ηk = µ. By substituting lfp[oη ] to ∗ in (21), we have(oηµ )i (lfp[oη ]) = lfp[oη ] + (oµ )i (⊥)
for each i < ω. Then (20) can be proven by taking its limit, because lfp[oη ] ≤ lfp[oηµ ] and S
is assumed to be ω-continuous. The case ηk = ν is similar. In this case gfp[oηµ ] is substituted
to ∗.
J

Lemma 45 and its proof
I Lemma 45. Let A = (A, α, Ω) be a parity (S, FΣ,∆ )-automaton with ran(Ω) = [1, n].
Assume n > 2 and n is even. The parity (S, FΣ,∆ )-automaton flat(A) = (A[ , α[ , Ω[ ) isdefined as follows.
A[ = A≤n−2 × {0, 1} + A>n−2 × {2}(α(a)(F π0 (τ [ )) if τ [ = ισ (a0 , 0) or τ [ = ιδ[[α (a, 0)(τ ) =0
if τ [ = ισ (a0 , 1) or τ [ = ισ (a0 , 2)(0
if τ [ = ισ (a0 , 0) or τ [ = ιδα[ (a, 1)(τ [ ) =[α(a)(F π0 (τ )) if τ [ = ισ (a0 , 1) or τ [ = ισ (a0 , 2)
α[ (a, 2)(τ [ ) = α(a)(F π0 (τ [ ))Ω[ (a, 0) = Ω(a),Ω[ (a, 1) = n − 3,Ω[ (a, 2) = Ω(a) − 2

Here F π0 : FΣ,∆ A[ → FΣ,∆ A[ is defined by F π0 (ισ (a, i)) = ισ (a) and F π0 (ιδ ) = ιδ . Thistransformation flat satisfies:i) ext(A)(a) =P(a,i)∈A[ ext(flat(A))(a, i) for any a ∈ A; andii) flat(A) × M = flat(A × M) for any (TS , F )-coalgebra M.

Corina Cîrstea, Shunsuke Shimizu, and Ichiro Hasuo

7:25

Proof. i) For any v 0 : A≤n−2 → S, we define the two equational systems
u1 =µ M1,≤n−2 • hu1 , . . . , un−2 i + v1 + v10
u2 =ν M2,≤n−2 • hu1 , . . . , un−2 i + v2 + v20

p 0
E (v ) = 

..


.
0
un−2 =ν M1,≤n−2 • hu1 , . . . , un−2 i + vn−2 + vn−2
u1 =µ M1,≤n−2 • hu1 , . . . , un−2 i + v10
u1 =µ M2,≤n−2 • hu1 , . . . , un−2 i + v20
E µ (v 0 ) = 

..


.
un−2

=µ

0
M1,≤n−2 • hu1 , . . . , un−2 i + vn−2

where the relation M : A × A → S and the predicate v : A → S is given byXX
M (a, a0 ) =α(a)(ισ (a0 )) and v(a) =α(a)(ιδ ) .
δ∈∆(σ,a)∈Σ×A

By Lemma 30, we have
JE p (v 0 )K = JE p (⊥)K + JE µ (v 0 )K .
p

µ

(22)

0

β

0

A≤n−2 ×{0,1}We can coalesce E (⊥) and E (v ) into one system E (v ) over S, which isdefined as follows.

u1 =µ M1,≤n−2
O • hu1 , . . . , un−2 i + v1




u2 =ν
M2,≤n−2O • hu1 , . . . , un−2 i + v2




..




.




β 0
E (v ) =  un−4 =ν

•
hu
,
.
.
.
,
u
i
+
v
M
O
1
n−2
n−4
n−4,≤n−2






Mn−3,≤n−2O u0 • hu1 , . . . , un−2 i + vn−3 + v  n−3 =µOM≤n−2,≤n−2
un−2 =ν
Mn−2,≤n−2
O • hu1 , . . . , un−2 i + vn−2
Here un−3 runs over S An−3 ×{0}+A≤n−2 ×{1} , whereas ui runs over S Ai ×{0} for i ∈ {1, . . . , n −4, n − 2}. By definition, it is easy to show that
JE β (v 0 )K(a, 0) + JE β (v 0 )K(a, 1) = JE p (⊥)K(a) + JE µ (v 0 )K(a)(23)

for any a ∈ A≤n−2 .

Let us define the equational systems E and E [ as follows:
un−1 =µ JE p (hun−1 , un i)K + Mn−1,>n−2 • hun−1 , un i + vn−1
E =un =ν JE p (hun−1 , un i)K + Mn,>n−2 • hun−1 , un i + vn

un−1 =µ JE β (hun−1 , un i)K† + Mn−1,>n−2 • hun−1 , un i + vn−1
E[ =un =ν JE β (hun−1 , un i)K† + Mn,>n−2 • hun−1 , un i + vn

where JE β (v 0 )K† : A≤n−2 → S is defined by JE β (v 0 )K† (a) = JE β (v 0 )K(a, 0) + JE β (v 0 )K(a, 1).
By definition of extents, we haveX
ext(A)(a) = JEK(a) andext(flat(A))(a, i) = JE [ K(a)(24)(a,i)∈A[for each a ∈ A. Since for any predicate v 0
(22)

(23)

JE p (v 0 )K = JE p (⊥)K + JE µ (v 0 )K = JE [ (v 0 )K†

holds, we also have JEK = JE [ K. This and (24) conclude the proof.

ii) Both of the automata flat(A) × M and flat(A × M) have the same state space

CALCO 2017

7:26

Parity Automata for Quantitative Linear Time Logics

A≤n−2 × M × {0, 1} + A>n−2 × M × {2}. It is easy to see that the priorities and thetransitions are also the same.
J