Quantitative Simulations by Matrices I
Natsuki Urabea,∗, Ichiro Hasuoa
a Department of Computer Science, Graduate School of Information Science and Technology, theUniversity of Tokyo, 7-3-1, Hongo, Bunkyo-ku, Tokyo, Japan

Abstract
We introduce notions of simulation between semiring-weighted automata as models ofquantitative systems. Our simulations are instances of the categorical/coalgebraic notions previously studied by Hasuo—hence soundness against language inclusion comesfor free—but are concretely presented as matrices that are subject to linear inequality
constraints. Pervasiveness of these formalisms allows us to exploit existing algorithms in:searching for a simulation, and hence verifying quantitative correctness that is formulated as language inclusion. Transformations of automata that aid search for simulations
are introduced, too. This verification workflow is implemented for the plus-times andmax-plus semirings. Furthermore, an extension to weighted tree automata is presented
and implemented.

1. Introduction
Quantitative aspects of various systems are more and more emphasized in recent verification scenarios. Probabilities in randomized or fuzzy systems are a classic example;
utility in economics and game theory is another. Furthermore, now that many computer systems are integrated into physical ambience—realizing so-called cyber-physicalsystems—physical quantities like energy consumption are necessarily taken into account.
1.1. Semiring-Weighted Automata
It is standard in the concurrency community to model such quantitative systems
by state-transition systems in which weights are assigned to their states and/or transitions. The semantics of such systems varies, however, depending on the interpretation ofweights. If they are probabilities, they are accumulated by × along a path and summed
across different paths; if weights are (worst-case) costs, they are summed up along a pathand we would take max across different paths.
The algebraic structure of semirings then arises as a uniform mathematical languagefor different notions of “weight,” as is widely acknowledged in the community. The
I An earlier version of this paper [38] has been presented at: Concurrency Theory—25th International
Conference (CONCUR 2014), September 2–5 2014, Rome, Italy.
∗ Corresponding author
Email addresses: urabenatsuki@is.s.u-tokyo.ac.jp (Natsuki Urabe),ichiro@is.s.u-tokyo.ac.jp (Ichiro Hasuo)
Preprint submitted to Elsevier
December 25, 2014

1

INTRODUCTION

2

subject of the current study is state-based systems with labeled transitions, in which
each transition is assigned a weight from a prescribed semiring S. We shall call themS-weighted automata; and we are more specifically interested in the (weighted, finite)language inclusion problem and a simulation-based approach to it.
1.2. Language Inclusion
Let A be an S-weighted automaton with labels from an alphabet Σ. It assigns to eachword w ∈ Σ∗ a weight taken from S—this is much like a (purely) probabilistic automaton
assigns a probability to each word. Let us denote this function by L(A) : Σ∗ → S and callit the (weighted) language of A by analogy with classic automata theory. The language
inclusion problem L(A) v L(B) asks if: L(A)(w) v L(B)(w) for each word w ∈ Σ∗ ,where v is a natural order on the semiring S.
It is not hard to see that language inclusion L(A) v L(B) has numerous applications
in verification. In a typical scenario, one of A and B is a model of a system and the otherexpresses specification; and L(A) v L(B) gives the definition of “the system meeting thespecification.” More concrete examples are as follows.
• S represents probabilities; A models a system; and B expresses the specificationthat certain bad behaviors—identified with words—occur with a certain probability.
Then L(A) v L(B) is a safety statement: each bad behavior occurs in A at mostas likely as in B.
• S represents profit, A is a specification and B is a system. Then L(A) v L(B)guarantees the minimal profit yielded by the system B.
• There are other properties reduced to language inclusion in a less trivial manner.
An example is probable innocence [35], a quantitative notion of anonymity. See [22].
1.3. Simulation
Direct check of language inclusion is simply infeasible because there are infinitely
many words w ∈ Σ∗ . One finitary proof method—well-known for nondeterministic (i.e.
possibilistic) systems—is by (forward or backward) simulations, whose systematic study
is initiated in [31]. In the nondeterministic setting, a simulation R is a relation between
states of A and B that witnesses “local language inclusion”; moreover, from the coinductive way in which it is defined, a simulation persistently witnesses local language
inclusion—ultimately yielding (global) language inclusion. This property—existence ofa simulation implies language inclusion—is called soundness.
1.4. Contribution: Weighted Forward/Backward Simulations by Matrices
In this paper we extend this simulation approach to language inclusion [31] to thequantitative setting of semiring-weighted automata. Our notions of (forward and backward) weighted simulation are not given by relations, but by matrices with entries froma semiring S.
Use of matrices in automata theory is classic—in fact our framework instantiates tothat in [31] when we take as S the Boolean semiring. This is not how we arrived here;
conversely, the current results are obtained as instances of a more general theory of coalgebraic simulations [18, 21, 19]. There various systems are identified with a categorical

1

INTRODUCTION

3

construct of coalgebras in a Kleisli category; and forward and backward simulations arecharacterized as lax/oplax morphisms between coalgebras. A generic soundness result(with respect to language/trace inclusion) is also proved in the general categorical terms.
This paper is devoted to concrete presentations of these categorical notions by matrices, and to their application to actual verification of quantitative systems. Presentation
by matrices turns out to be an advantage: a simulation is now a matrix X that satisfies
certain linear inequalities; and existence of such X—i.e. feasibility of linear inequalities—
is so common a problem in many fields that there is a large body of existing work thatis waiting to be applied. For example linear programming (LP) can be exploited forthe plus-times semiring for probabilities; and there are algorithms proposed for othersemirings such as the max-plus (tropical) one.
Our (mostly semiring-independent) workflow is as follows. A verification goal isformulated as language inclusion L(A) v L(B), which we aim to establish by finding
a forward or backward simulation from A to B. Soundness of simulations follows fromthe general result in [18]. A simulation we seek for is a matrix subject to certain linear
inequalities, existence of which is checked by various algorithms that exist for different
semirings. We implemented this workflow for the plus-times and max-plus semirings.
This simulation-based method is sound but not necessarily complete with respect
to language inclusion. Therefore we introduce transformations of weighted automata—called (forward/backward) partial execution—that potentially create matrix simulations.
Via our equivalence results between our matrix simulation and some known ones (including the one in [7]), the partial execution transformations potentially create thosesimulations, too.
Compared to the earlier version [38] of this paper, the current version additionallycontains the following materials.
• Section 7 is added, where we exploit the coalgebraic theory behind and generalize
matrix simulation from weighted (word) automata to weighted tree automata. We
describe the definition of forward partial execution in categorical terms, too, so thatit transfers to weighted tree automata. We also have a preliminary implementation.
• We now have more extensive discussions of related work, including [3, 15, 8] of
which we were not aware before.
• We conducted experiments again with a faster machine, enlarging the size of problem instances that can be handled.
• We have some examples that were absent in the previous version [38].
• Concrete description of the procedure (forward/backward) partial execution is included.
• Some proofs were omitted in [38] for space reasons; they are present here.
1.5. Organization of the paper
In Section 2 that is devoted to preliminaries, we define semiring-weighted automata,characterize them in coalgebraic terms and recap the coalgebraic theory in [18]. These
are combined to yield the notion of simulation matrix in Section 3. In Section 4 partial
execution transformations of automata are described and proved correct. The framework

2

PRELIMINARIES

4

obtained so far is applied to the plus-times and max-plus semirings, in Section 5 and Section 6, respectively. There our proof-of-concept implementations (the code is found at
the first author’s webpage) and relationship to other known simulation notions are discussed, too. In Section 7 we generalize the framework so far from words to trees: thegeneralization is straightforward—thanks to the coalgebraic backend—although linearity
of constraints, as well as backward partial execution, is lost. In Section 8 (and in earlier
sections) we discuss related work; in Section 9 we conclude.
2. Preliminaries
We review the generic theory of traces and simulations in [21, 18] that is based on(T, F )-systems, which will eventually lead to the notion of simulation matrix in Section 3.
2.1. Semiring-Weighted Automata
The notion of semiring-weighted automaton is parametrized by a semiring S. For our
purpose of applying coalgebraic theory in [18, 21], we impose the following properties.
Definition 2.1 A commutative cppo-semiring is a tuple S = (S, +S , 0S , ×S , 1S , v) thatsatisfies the following conditions.
• (S, +S , 0S , ×S , 1S ) is a semiring in which ×S , in addition to +S , is commutative.
• A relation v is a partial order on S and (S, v) is ω-complete, i.e. an increasing
chain s0 v s1 v · · · has a supremum.
• Any element s ∈ S is positive in the sense that 0S v s.
• Addition +S and multiplication ×S are monotone with respect to v.
It follows from positivity and ω-completeness that countable sum can be straightforwardly defined in a commutative cppo-semiring S. We will use this fact throughout the
paper.
Example 2.2 (semirings S+,× , Smax,+ , B) The plus-times semiring S+,×=([0, ∞], +, 0, ×, 1, ≤) is a commutative cppo-semiring, where + and × are usual
addition and multiplication of real numbers. This is the semiring that we will use formodeling probabilistic branching. Specifically, probabilities of successive transitions areaccumulated using ×, and those of different branches are combined with +.
The max-plus semiring Smax,+ = ([−∞, ∞], max, −∞, +, 0, ≤)—also sometimes called
the tropical semiring [33]—is also a commutative cppo-semiring. Here a number r ∈[−∞, ∞] can be understood as (best-case) profit: they are summed up along a path,and an optimal one (max) is chosen among different branches. Another possible understanding of r is as (worst-case) cost. The unit for the semiring addition max is givenby −∞; since it must also be a zero element of the semiring multiplication +, we define(−∞) + ∞ = −∞. In the two examples S+,× and Smax,+ we added ∞ so that they
become ω-complete.
Finally, the Boolean semiring B = ({0, 1}, ∨, 0, ∧, 1, ≤) is an example that is qualitative rather than quantitative.

2

PRELIMINARIES

5

Definition 2.3 (S-weighted automaton, weighted language) Let S = (S, +S , 0S , ×S ,1S , v) be a commutative cppo-semiring. An S-weighted automaton A = (Q, Σ, M, α, β)consists of a countable state space Q, a countable alphabet Σ, transition matrices
M (a) ∈ S Q×Q for all a ∈ Σ, the initial row vector α ∈ S Q and the final column vector
β ∈ SQ.
Let x, y ∈ Q and a ∈ Σ. We write αx and βx for the x-th entry of α and β, respectively,
and M (a)x,y for the (x, y)-entry of the matrix M (a). Note that these entries are all
elements of the semiring S.
An S-weighted automaton A = (Q, Σ, M, α, β) yields a weighted language
L(A) : Σ∗ → S. It is given by the following multiplication of matrices and vectors.
L(A)(w) := α · M (a1 ) · · · · · M (ak ) · β

for each w = a1 · · · ak ∈ Σ∗ .

(1)

We require a state space Q to be at most countably infinite. This is so that the matrix
multiplications in (1)—by addition and multiplication of S—are well-defined. Recall that
S has countable sum given by supremums of suitable ω-chains.
Our interest is in establishing language inclusion between two weighted automata.
Definition 2.4 (language inclusion) We write L(A) v L(B) if, for each w ∈ Σ∗ ,L(A)(w) v L(B)(w). The last v is the order of S.
2.2. Coalgebraic Modeling of Semiring-Weighted Automata
Here we characterize semiring-weighted automata as instances of a generic coalgebraic
model of branching systems—so-called (T, F )-systems with parameters T, F [21, 18].
Definition 2.5 ((T, F )-system) Let T be a monad and F be a functor, both on the
category Sets of sets and functions. A (T, F )-system is a triple
X =X, s : {•} → T X, c : X → T F X

of a set X (the state space), and functions s (the initial states) and c (the dynamics).
This modeling is coalgebraic [24] in the sense that c is so-called a T F -coalgebra. In
the definition we have two parameters T and F . Let us forget about their categoricalstructures (a monad or a functor ) for a moment and think of them simply as constructions
on sets. Intuitively speaking, T specifies what kind of branching the systems in question
exhibit; and F specifies a type of linear-time behaviors. Here are some examples; in theexample F = 1 + Σ × ( ) the only element of 1 is denoted by X (i.e. 1 = {X}).
T
P
D
MS

“branching”
nondeterministic
probabilistic
S-weighted

F
1+Σ×( )
(Σ + ( ))∗“linear-time behavior”a→ X or → (where a ∈ Σ)
words over terminals (a ∈ Σ)
& nonterminals, suited for CFG [20]The above examples of a monad T —the powerset monad P, the subdistribution monadD, and the S-multiset monad MS for S—are described as follows.
P
PX = {X 0 | X 0 ⊆ X}
DX = {f : X → [0, 1] | x∈X f (x) ≤ 1}
(2)
MS X = {f : X → S | supp(f ) is countable}

2

PRELIMINARIES

6

Here supp(f ) = {x ∈ X | f (x) 6= 0S }. Countable support in MS is a technical requirement so that composition of Kleisli arrows is well-defined (Definition 2.7).
It should not be hard to see that a (T, F )-system models a state-based system with T branching and F -linear-time behaviors. For example, when T = P and F = 1 + Σ × ( ),s : {•} → PX represents the set of initial states and c : X → P(1 + Σ × X) represents
one-step transitions—that X ∈ c(x) means x is accepting (x → X), and (a, x0 ) ∈ c(x)ameans there is a transition x → x0 . Overall, a (P, 1 + Σ × ( ))-system is nothing but anondeterministic automaton.
Analogously we obtain the following, by the definition of MS in (2).
Proposition 2.6 (weighted automata as (T, F )-systems) Let S be a commutative
cppo-semiring. There is a bijective correspondence
between: 1) S-weighted automata(Definition 2.3); and 2) MS , 1 + Σ × ( ) -systems whose state spaces are at mostcountably infinite.
Concretely,an S-weighted automaton A = (Q, Σ, M, α, β) gives rise to an MS , 1 +Σ × ( ) -system XA = (Q, sA , cA ) defined as follows. sA : {•} → MS Q is given bysA (•)(x) = αx ; and cA : Q → MS (1+Σ×Q) is given by cA (x)(X) = βx and cA (x)(a, y) =M (a)x,y .

2.3. Coalgebraic Theory of Traces and Simulations
We review the theory of traces and simulations in [21, 18] that is based on (T, F )systems. In presentation we restrict to T = MS and F = 1 + Σ × ( ) for simplicity.
2.3.1. Kleisli Arrows
One notable success of coalgebra was a uniform characterization, in terms of thesame categorical diagram, of bisimulations for various kinds of systems (nondeterministic,
probabilistic, etc.) [24]. This works quite well for branching-time process semantics. For
linear-time semantics—i.e. trace semantics—it is noticed in [34] that so-called a Kleisli
category, in place of the category Sets, gives a suitable base category for coalgebraic
p Y andtreatment. This idea—replacing functions X → Y with Kleisli arrows X →drawing the same diagrams—led to the development in [21, 18, 19] of an extensive theoryof traces and simulations. The notion of Kleisli arrow is parametrized by a monad T : ap T Y (or simply X →p Y ) is defined to be a function X → T Y , hence
T -Kleisli arrow X →represents a “T -branching function from X to Y .”p Y
We restrict to T = MS for simplicity of presentation. An MS -Kleisli arrow f : X →below is “an S-weighted function from X to Y .” In particular, for each x ∈ X and y ∈ Y
it assigns a weight f (x)(y) ∈ S.
Definition 2.7 (Kleisli arrow) Let X, Y be sets. An MS -Kleisli arrow (or simply a
p Y , is a function from X to MS Y .
Kleisli arrow ) from X to Y , denoted by X →We list some special Kleisli arrows: ηX , g f and Jf .
p X is given by: η(x)(x) = 1S ; and• For each set X, the unit arrow ηX : X →η(x)(x0 ) = 0S for x0 6= x. Here 0S and 1S are units in the semiring S.

2

PRELIMINARIES

7

p Y and g : Y →p Z, their composition• For consecutive Kleisli arrows f : X →p Z is given as follows:g f : X→P
(g f )(x)(z) :=y∈supp(f (x)) f (x)(y) ×S g(y)(z) .
Since supp(f (x)) is countable, the above sum in a cppo-semiring S is well-defined.
p Y is given• For a (usual) function f : X → Y , its lifting to a Kleisli arrow Jf : X →p Y with a function ηY : Y → MS Y .
by Jf = ηY ◦ f . Here we identified ηY : Y →Categorically speaking: the first two (η and ) organize Kleisli arrows as a category(the Kleisli category K`(MS )); and the third gives a functor J : Sets → K`(MS ) that is
identity on objects.
In Proposition 2.6 we characterized an S-weighted automaton A in coalgebraic terms.
Using Kleisli arrows it is presented as a triple
XA =p Q, cA : Q −→p 1+Σ×Q
Q, sA : {•} −→



.

(3)

2.3.2. Generic Trace Semantics
In [21], for monads T with a suitable order, a final coalgebra in K`(T ) is identified. It(somehow interestingly) coincides with an initial algebra in Sets. Moreover, the universality of this final coalgebra is shown to capture natural notions of (finite) trace semantics
for a variety of branching systems—i.e. for different T and F . What is important for thecurrent work is the fact that the weighted language L(A) in (1) is an instance of thisgeneric trace semantics, as we will show in Theorem 2.11.
1 + ΣO × X
_c
XO
_s
{•}

1 + Σ × (tr(c))
=



tr(c)

'

/ 1 + Σ × Σ∗O
final _ J([nil, cons]−1 )
∗
7/ Σ

(4)

tr(X )We shall state the results in [21] on coalgebraic traces, restricting again to T = MS and
F = 1 + Σ × ( ) for simplicity. In the diagram (4) above, composition of Kleisli arrows
are given byin Definition 2.7; J on the right is the lifting in Definition 2.7; and nil
and cons are the obvious constructors of words in Σ∗ . The top arrow 1 + Σ × (tr(c)) is
the functor 1 + Σ × ( ) on Sets, lifted to the Kleisli category K`(MS ), and applied to
the Kleisli arrow tr(c); its concrete description is as follows. See [21] for more details.
p Y , its lifting 1+Σ×f : 1+Σ×X →p 1+Σ×Y
Definition 2.8 For a Kleisli arrow f : X →is defined as follows:((
1S (t = ∗)f (x)(y) (t = (a, y))(1 + Σ × f )(∗)(t) =(1 + Σ × f )(a, x)(t) =0S (otherwise)
0S(otherwise)
Theorem 2.9 (final coalgebra in K`(MS )) Given any set X and any Kleisli arrow
p 1 + Σ × X, there exists a unique Kleisli arrow tr(c) that makes the top square inc: X→
the diagram (4) commute.
2

PRELIMINARIES

8

Definition 2.10 (tr(X )) Given an MS , 1 + Σ × ( ) -system X = (X, s, c) (this isp Σ∗ byon the left in the diagram (4)), its component c induces an arrow tr(c) : X →Theorem 2.9. We define tr(X ) to be the composite tr(c) s (the bottom triangle in the
diagram (4)), and call it the trace semantics of X .
Theorem 2.11 (weighted language as trace semantics) Let A be an S-weightedpautomaton. For XA = (Q, sA , cA ) induced by A in (3), its trace semantics tr(XA ) : {•}→
Σ∗ —identified with a function {•} → MS Σ∗ , hence with a function Σ∗ → S—coincides
with the weighted language L(A) : Σ∗ → S in (1).
In the last theorem we need that Σ∗ is countable; this is why we assumed that Σ ispcountable in Definition 2.3. Henceforth we do not distinguish L(A) and tr(XA ) : {•} →Σ∗ .
2.3.3. Forward and Backward Kleisli simulations
In [18], the classic results in [31] on forward and backward simulations—for (nondeterministic) labeled transition systems—are generalized to (T, F )-systems. Specifically,
forward and backward simulations are characterized as lax/oplax coalgebra homomorphisms in a Kleisli category; and soundness—their existence witnesses trace inclusion—isproved once for all in a general categorical setting.
As before, we present those notions and results in [18] restricting to T = MS and
F = 1 + Σ × ( ). If T = P and F = 1 + Σ × ( ) they instantiate to the results in [31].
Definition 2.12 (Kleisli simulation) Let X = (X, s, c) and Y = (Y, t, d) be (MS , 1 +Σ × ( ))-systems (cf. Definition 2.5, Proposition 2.6 and (3)).
p X such that
1. A forward (Kleisli) simulation from X to Y is a Kleisli arrow f : Y →s v f t and c f v (1 + Σ × f ) d. See Figure 1.
p Y such that s b v t
2. A backward simulation from X to Y is a Kleisli arrow b : X →and (1 + Σ × b) c v d b.
3. A forward-backward simulation from X to Y consists of: a (T, F )-system Z; aforward simulation f from X to Z; and a backward simulation b from Z to Y.
4. A backward-forward simulation from X to Y consists of: a (T, F )-system Z; abackward simulation b from X to Z; and a forward simulation f from Z to Y.
We write X vF Y, X vB Y, X vFB Y or X vFB Y if there exists a forward,
backward, forward-backward, or backward-forward simulation, respectively.
(Generic) soundness is proved using the maximality of tr(c) in (4) among (op)lax
coalgebra homomorphisms, arguing in the language of enriched category theory [18].
Theorem 2.13 (soundness) Let X and Y be (MS , 1 + Σ × ( ))-systems. Each of thep Σ∗ (cf. Definition 2.10).
following yields tr(X ) v tr(Y) : {•}→
1. X vF Y
2. X vB Y
3. X vFB Y
4. X vBF YTheorem 2.14 (completeness) The converse of soundness holds for backward-forward
simulations. That is: tr(X ) v tr(Y) implies X vBF Y .
3

SIMULATION MATRICES FOR SEMIRING-WEIGHTED AUTOMATA
Ff

o
FX
O
_c

v



XO o

f

{•}
fwd. sim.
o
FX
O
_c
XO o
s

F f
v



v

f

ZO
_u

v
b

/Y
O
t

{•}
bwd. sim.
F b

F OZ
_e



/ FY
O
_d

v

s

t

v
b

XO

YO

v

s

F b

FX
O
_c

FY
O
_d

9



v

{•}
fwd.-bwd. sim.

/ FY
O
_d

FX
O
_c

/Y
O

XO
t

s

F b

b

v

/ FZ o
O
_e

v

/Zo
O
_u



F f

FY
O
_d

v



f

YO

v

t

{•}
bwd.-fwd. sim.

Figure 1: Kleisli simulations (here F = 1 + Σ × ( ))3. Simulation Matrices for Semiring-Weighted Automata
In this section we fix parameters T = MS and F = 1 + Σ × ( ) in the generic theory
in Section 2.3 and rephrase the coalgebraic framework in terms of matrices (whose entries
are taken from S). Specifically: Kleisli arrows become matrices; and Kleisli simulations
become matrices subject to certain linear inequalities. Such matrix representations ease
implementation, a feature we will exploit in later sections.
p B is a function A → MS B (Definition 2.7).
Recall that a Kleisli arrow A→
p B, its maDefinition 3.1 (matrix representation Mf ) Given a Kleisli arrow f : A→trix representation Mf ∈ S A×B is given by (Mf )x,y = f (x)(y).
In what follows we shall use the notations f and Mf interchangeably.
p B and g : B →p C be Kleisli arrows.
Lemma 3.2 Let f, f 0 : A→
1. f v f 0 if and only if Mf v Mf 0 . Here the former v is between MS -Kleisli arrows,
and the latter order v is between matrices, defined entrywise.
2. Mg f = Mf Mg , computed by matrix multiplication.

f

1+Σ×f

p B to 1 + Σ × A −→p
The correspondence from A −→1 + Σ × B— used in (4) and in
Figure 1—can be described using matrices, too.
p B be a Kleisli arrow and Mf be its matrix representation.
Lemma 3.3 Let f : A →Then the matrix representation M1+Σ×f is given byI1 ⊕ (IΣ ⊗ Mf ) ∈ S (1+Σ×A)×(1+Σ×B) ,where ⊕ and ⊗ denote coproduct and the Kronecker product of matrices:

3

SIMULATION MATRICES FOR SEMIRING-WEIGHTED AUTOMATA

X⊕Y =

O

X
O

Y

!
,



· · ·



.
.
.
xi,j
.
.
.







· · ·
⊗ Y





= · · ·.
.
.
xi,j Y
.
.
.

10





· · · .
This description of MF f generalizes from F = 1 + Σ × ( ) to any polynomial functor F ,inductively on the construction of F . In this paper the generality is not needed.
Using Lemma 3.2–3.3, we can present Kleisli simulations (Definition 2.12) as matrices. Recall that a state space of a weighted automaton is assumed to be countable(Definition 2.3); hence all the matrix multiplications in the definition below make sense.
Definition 3.4 (forward/backward simulation matrix) Let A = (QA , Σ, MA , αA , βA )and B = (QB , Σ, MB , αB , βB ) be S-weighted automata.
• A matrix X ∈ S QB ×QA is a forward simulation matrix from A to B if
αA v αB X ,X · MA (a) v MB (a) · X(∀a ∈ Σ) ,and XβA v βB .

• A matrix X ∈ S QA ×QB is a backward simulation matrix from A to B if
αA X v αB ,MA (a) · X v X · MB (a)(∀a ∈ Σ) ,and βA v XβB .

The requirements on X are obtained by first translating Figure 1 into matrices, andthen breaking them up into smaller matrices using Lemma 3.3. It is notable that therequirements are given in the form of linear inequalities, a format often used in constraint
solvers. Solving them is a topic of extensive research efforts that include [1, 6]. This fact
becomes an advantage in implementing search algorithms, as we see later.
We also note that forward and backward simulation matrices have different dimensions. This difference comes from the different directions of arrows in Figure 1.
Theorem 3.5 Let A and B be S-weighted automata. There is a bijective correspondence
between: 1) forward simulation matrices from A to B; and 2) forward Kleisli simulations
from XA to XB . The same holds for the backward variants.
In what follows we write vF , vB also between S-weighted automata. Theorem 3.5 yields:
A vF B if and only if there is a forward simulation matrix.
Here is our core result; the rest of the paper is devoted to its application.
Corollary 3.6 (soundness of simulation matrices) Let A and B be S-weighted automata. Existence of a forward (or backward) simulation matrix from A to B—i.e.
A vF B or A vB B—witnesses language inclusion L(A) v L(B).
Proof. ∃ (fwd./bwd. simulation matrix from A to B)
Thm. 3.5∃ (fwd./bwd. Kleisli simulation from XA to XB )Thm. 2.13

tr(XA ) v tr(XB )⇐⇒=⇒Thm. 2.11⇐⇒

L(A) v L(B) .



It is classic to represent nondeterministic automata by Boolean matrices. This corresponds to the special case S = B (the Boolean semiring) of the current framework; anda simulation matrix becomes the same thing as a (relational) simulation in [31].

4

FORWARD AND BACKWARD PARTIAL EXECUTION

11Remark 3.7 The opposite of an S-weighted automaton A = (Q, Σ, M, α, β)—obtainedby reversing transitions and swapping initial/final states—can be naturally defined bymatrix transpose, that is, tA := (Q, Σ, tM, tβ, tα). It is easy to see that: if X is a forward
simulation matrix from A to B, then tX is a backward simulation matrix from tA to tB.
4. Forward and Backward Partial Execution
In this section we introduce for semiring-weighted automata their transformations—called forward and backward partial execution—that increase the number of forward or
backward simulation matrices. We also prove some correctness results.
4.1. Incompleteness of Matrix Simulations
We have four different notions of simulation (Definition 2.12): forward, backward,
forward-backward, and backward-forward. Our view on these is as (possibly finitary)
witnesses of language inclusion.
The combined ones (forward-backward and backward-forward) subsume the onedirection ones (forward and backward)—simply take the identity arrow as one of thetwo simulations required. Moreover, backward-forward is complete (Theorem 2.14). Despite these theoretical advantages, the combined simulations are generally harder to find:in addition to two simulations, we have to find an intermediate system too (Z in Definition 2.12). Furthermore, since language inclusion for finite S+,× -weighted automata—models of probabilistic systems—is known to be undecidable [5], existence of a backwardforward simulation is undecidable too.
Therefore in what follows we focus on the one-directional (i.e. forward or backward)
simulations as proof methods for language inclusion. They have convenient matrix presentations, too, as we saw in Section 3. However forward or backward simulations are
not necessarily complete. We can see it from the following counterexample.
Example 4.1 (vF and vB are not complete) The following S+,× -weighted automata
exhibit L(A) v L(B) (in fact L(A) = L(B)).
A
a, 21

? x1_


? x3

? x0


a, 12

a,1

a, 21

b, 12

? y1

B

1
2

/X

a,1



? y0

a,1

a, 12
b, 12

x2





y3
?

1
2

/X

a,1

y2

Indeed, for each word w ∈ Σ∗ , we have(
L(A)(w) = L(B)(w) =


1 1 n
4 2

0

(w = aaa2n or baa2n )(otherwise) .

However there is no forward or backward simulation from A to B: one can show by direct
calculation that there is no X that satisfies the requirements in Definition 3.4. Hence
this pair is a counterexample for the completeness of vF and that of vB .

4

FORWARD AND BACKWARD PARTIAL EXECUTION

12

It turns out that a simulation in the sense of Jonsson and Larsen [25] does exist from
A to B. See also Section 5.1 later, where we systematically compare our current notionsof simulation with existing ones.
The incompleteness of forward and backward simulations can be also deduced fromcomplexity arguments. See Section 5.1.
4.2. Forward and Backward Partial Execution for Semiring-weighted Automata
We shall define transformations, called FPE and BPE, that increase matrix simulations for semiring-weighted automata. We prove some of its properties, too.
Definition 4.2 (FPE, BPE) Forward partial execution (FPE) is a transformation ofa weighted automaton that “replaces some states with their one-step behaviors.” Concretely, given an S-weighted automaton A = (Q, Σ, M, α, β) and a parameter P ⊆ Q,
the resulting automaton AFPE,P = (Q0 , Σ, M 0 , α0 , β 0 ) has a state space
Q0 = X ∃x ∈ P. βx 6= 0S + (a, y) ∃x ∈ P. M (a)x,y 6= 0S + (Q \ P ) ,(5)
replacing each p ∈ P with its one-step behaviors (X or (a, q)) as new states. The otherdata M 0 , α0 , β 0 are defined as follows. For the transition matrices M 0 :M 0 (a)(a,x),X
M 0 (a)x,X= βx
= M (a)β x

M 0 (a)(a,x),(a0 ,y)M 0 (a)x,(a0 ,y)==M (a0 )x,y
M (a)M (a0 ) x,yM 0 (a)(a,x),xM 0 (a)x,y= 1S= M (a)x,y

where a, a0 ∈ Σ, x, y ∈ Q. For all the other cases we define M 0 (a)u,v = 0S , whereu, v ∈ Q0 . For the initial and final vectors α0 and β 0 , the definition is shown below.

0
0
αX
= αβ
α(a,x)= αM (a) xαx0 = αx0βX = 1Sβ(a,x) = 0S
βx0 = βx
Backward partial execution (BPE) in contrast “replaces states in a parameter P ⊆Q with their backward one-step behaviors.” For the same A as above, the resulting
automaton ABPE,P = (Q0 , Σ, M 0 , α0 , β 0 ) has a state space(6)
Q0 = • ∃x ∈ P. αx 6= 0S + (a, y) ∃x ∈ P. M (a)y,x 6= 0S + (Q \ P ) ,areplacing each p ∈ P with its backward one-step behaviors—(a, q) with q → p, and •if p is initial—as new states. The other data M 0 , α0 , β 0 are defined as follows. For thetransition matrices M 0 :M 0 (a)•,(a,y)
M 0 (a)•,y= αy= αM (a) y

M 0 (a)(a0 ,x),(a,y)
M 0 (a)(a0 ,x),y==M (a0 )x,y
(M (a0 )M (a))x,y

M 0 (a)x,(a,x)
M 0 (a)x,y

where a, a0 ∈ Σ, x, y ∈ Q. For all the other cases we define M 0 (a)u,v = 0S , whereu, v ∈ Q0 . For the initial and final vectors α0 and β 0 , the definition is shown below.
α•0
β•0

= 1S
= αβ

α(a,x)0β(a,x)= 0S= (M (a)β)x

αx0
βx0

= αx
= βx

Pictorially, the actions of FPE and BPE can be illustrated as in Figure 2. Roughly
speaking, FPE replaces a concrete state p ∈ P with an abstract state, such as (a, q) in
Q0 of (5) that is thought of as a description “a state that makes an a-transition to q.”
The idea comes from partial evaluation of a program; hence the name.

= 1S= M (a)x,y

4

FORWARD AND BACKWARD PARTIAL EXECUTION◦D◦Z
a1 ,p1◦O

a2 ,p2



•O

/ ◦Z

b,p

◦O
a1 ,1Sa,r1

a2 ,1S◦Db,p·p1◦◦“split backward”◦D Z

b1 ,q1b,p·p2

◦O

a,r2

•O

/

•O

O
r 
•O

a,1S



b2 ,q2

◦

13

◦D Z
b2 ,

b1 ,

◦ q1 ·r1◦◦ q2 ·r2“merge backward”

/

c,s

◦
◦
“eliminate dead end”

Forward Partial Execution◦Ob,pa1 ,p1◦•D Z

b,p·p1
a2 ,p2

◦D Z

/ ◦O

◦O

b,p·p2

b1 ,q1◦O
a1 ,1S◦◦“split forward”◦O
b2 ,q2•Z
a2 ,1S

•D

a,r1

◦



b1 , ◦Z
q1 ·r1/a,r2◦D b2 ,

◦O

q2 ·r2

•O 
r

◦O
a,1S

◦
◦
“merge forward”

◦
c,s

/

“eliminate dead end”

Backward Partial Execution
Figure 2: Fwd./bwd. partial execution (FPE, BPE), pictorially. Black nodes need to be in P

4.3. Correctness of FPE and BPE
The use of FPE/BPE is as follows: we aim to establish L(A) v L(B); depending onwhether we search for a forward or backward simulation matrix, we apply one of FPE
and BPE to each of A and B, according to the above table (7).
goal: L(A) v L(B)
by vF
by vB

A
B
FPE BPEBPE FPE(7)

We shall now state correctness properties of this strategy. Soundness means that
discovery of a simulation after transformation indeed witnesses the language inclusion
for the original automata. The second property—we call it adequacy—states that simulations that are already there are preserved by partial execution.
Theorem 4.3 (soundness of FPE/BPE) Let P and P 0 be arbitrary subsets of thestate spaces of A and B, respectively. Each of the following implies L(A) v L(B).
1. AFPE,P vF BBPE,P 0
2. ABPE,P vB BFPE,P 0

Theorem 4.4 (adequacy of FPE/BPE) Let P and P 0 be arbitrary subsets of thestate spaces of A and B, respectively. We have:
1. A vF B ⇒ AFPE,P vF BBPE,P 0
2. A vB B ⇒ ABPE,P vB BFPE,P 0
To prove these two theorems, we should first prove the following lemma.

4

FORWARD AND BACKWARD PARTIAL EXECUTION

Lemma 4.5 For each subset P , we have the following.
1. A vB AFPE,P
2. AFPE,P vF A
3. A vF ABPE,P

14
4. ABPE,P vB A

Proof. 1. Let A = (Q, Σ, M, α, β) and AFPE,P = (Q0 , Σ, M 0 , α0 , β 0 ). We define X ∈0
S Q×Q as follows:
Xx,X
Xx,x

= βx
= 1S

(x ∈ P ),(x ∈/ P ),

Xx,(y,a)Xu,v= M (a)x,y= 0S(x ∈ P ),(otherwise)

Then, this X is a backward simulation matrix from A to AFPE,P
The items 2., 3. and 4. are proved similarly.



Proof of Theorem 4.3. 1. From Proposition 4.5.1, A vB AFPE,P vF BBPE,P 0 vB B.
Hence from Corollary 3.6, L(A) v L(AFPE,P ) v L(BBPE,P 0 ) v L(B) holds.
The item 2. is proved similarly.

Proof of Theorem 4.4. 1. From Proposition 4.5.2, AFPE,P vF A vF B vF BBPE,P 0 .
Because vF is transitive (see the diagram below where F = 1 + Σ × ( )), this implies
AFPE,P vF BBPE,P 0 .
0
Ff

0 o
o F f
FY
FX
FX
O
O
O
_c
_
_d
0
v
v
c
 f0
 f
XO o
XO o
YO
s
t
_
0
v
v
s
{•}
The item 2. is proved similarly.

We also show that a bigger parameter P yields a greater number of simulations. In
implementation, however, a bigger P generally gives us a bigger state space which slows
down search for a simulation. Hence we are in a trade-off situation.
Proposition 4.6 (monotonicity) Assume P1 ⊆ P10 and P2 ⊆ P20 . We have:
1. AFPE,P1 vF BBPE,P2 ⇒ AFPE,P10 vF BBPE,P20 ,2. ABPE,P1 vB BFPE,P2 ⇒ ABPE,P10 vB BFPE,P20 .



For S = S+,× or Smax,+ , we can easily see that the complement problem of language
inclusion between finite S-weighted automata is semi-decidable. Since language inclusion itself is undecidable [5, 30], language inclusion is not even semidecidable. Because
existence of a simulation matrix is decidable, it can be the case that however many times
we apply FPE or BPE, simulation matrices do not exist while language inclusion holds.
A concrete example is found in the following example.
Example 4.7 (limitation of FPE) The following S+,× -weighted automata exhibit L(A) v
L(B), but a forward simulation does not exist no matter how many times FPE is applied

5

SIMULATION MATRICES FOR PROBABILISTIC SYSTEMS BY S = S+,×

to A.

XO

A

B
◦o

1
2

◦! O

a, 21

3
4

X
E Y

◦/ T

a,1
a, 14

15

3
4

a,1
/◦
◦O o
a, 14

a,1

◦E

2
3

1

1
3

It is possible to describe FPE on the coalgebraic level of abstraction. Besides providing an insight into the essence of the construction, it also allows for the applicationof FPE to quantitative tree automata. In contrast, the definition of BPE seems to relyon the fact that we can “reverse” word automata, and hence is hard to generalize e.g. totree automata. See Section 7.
5. Simulation Matrices for Probabilistic Systems by S = S+,×
In this section we focus on S+,× -weighted automata which we identify as (purely)
probabilistic automata (cf. Example 2.2). In Section 5.1 our method by simulation matrices is compared with other notions of probabilistic simulation; in Section 5.2 we discuss
our implementation.
5.1. Other Simulation Notions for Probabilistic Systems
vFB

lang. incl.
Example
4.1

×

×

[19]

vJL
vHJ

vF or vB
(i.e. by sim. matrices)

Various simulation notions have been introduced for probabilistic systems, either as abehavioral order by itself or as a proof method for language inclusion. Jonsson andLarsen’s one [25] (denoted by vJL ) is well-known; it is shown in [19] to be a special caseof Hughes and Jacobs’ coalgebraic notion of simulation [23] (vHJ ), which in turn is a
special case of forward-backward (Kleisli) simulation (vFB , Definition 2.12). Comparisonof all these notions (observed in [19]) is as depicted above; it follows from Theorem 2.13
that all these simulation notions are sound with respect to language inclusion.
We note that language inclusion between finite S+,× -weighted automata is known tobe undecidable [5] while language equivalence can be determined in polynomial time [27].
The former result can account for the fact that there does not seem to be many proof
methods for probabilistic/quantitative language inclusion. For example, probabilistic
simulation in [2] is possibilistic simulation between systems with both probabilistic andnondeterministic choice and not a quantitative notion like in the current study.
We also note that given finite-state S+,× -weighted automata A and B, if A vF B
or not is decidable: existence of a solution X of the linear constraints in Definition 3.4

5

SIMULATION MATRICES FOR PROBABILISTIC SYSTEMS BY S = S+,×16

can be reduced to linear programming (LP) problems, and the latter are known to be
decidable. The same applies to vB too.
Probabilistic systems are commonly
P modeled using the monad D (see (2))—with
an explicit normalization condition
x d(x) ≤ 1—instead of MS+,× . However there
is no need to impose normalization on simulations: sometimes only “non-normalized”
simulation matrices are found and they are still sound. Here is such an example.
Example 5.1 The following S+,× -weighted automata exhibit L(A) v L(B). Neither
forward nor backward Kleisli simulation (in the categorical sense of Definition 2.12) exists
between them as long as we represent the automata A and B as (D, 1 + Σ × ( ))-systems.
However Kleisli simulations (forward and backward) are found once we represent A and
B as (MS , 1 + Σ × ( ))-systems.
a, 83

A
X

xO 1

1
8

ui

a, 28
2
8





B
a, 48

Xo

3
8

9 y0 g

a, 58

x
E 0e
a, 81


1 1 ,
Indeed, the only matrix X that is a forward simulation(Definition
3.4)
is
X
=
 
1
and the only backward simulation matrix is X =. Neither of these satisfies the2normalization condition imposed on the subdistribution monad D.
5.2. Implementation, Experiments and Discussions
Our implementation consists of two components: +×-sim and +×-PE .
• The program +×-sim (implemented in C++) computes if a forward or backward
simulation matrix X between S+,× -weighted automata exists, and returns X if it
does exist. It first combines the constraints in Definition 3.4 into a single linear
inequality Ax ≤ b and solves it with a linear programming solver glpk [17]. We
note that the matrix A is sparse because of the way the different constraints in
Definition 3.4 are combined. It has n + anm + m rows, nm columns and at most
2nm + a(n2 m + nm2 ) nonzero entries.
• The program +×-PE (implemented in OCaml) takes an automaton A and d ∈ N as
input, and returns AFPE,P (or ABPE,P , by choice). Here P is chosen, by heuristics,ddz }| {z }| {
to be P = {x | x → · · · → X} (or P = {x | • → · · · → x}, respectively).
The two programs are alternately applied to the given automaton, for d = 1, 2, . . . , eachtime incrementing the parameter d for +×-PE . The experiments were on a MacBook
Pro laptop with a Core i5 processor (2.6 GHz, 2 cores) and 16 GB RAM.

5

SIMULATION MATRICES FOR PROBABILISTIC SYSTEMS BY S = S+,×
param.
G
S
2
8

AP
#st.
578

#tr.
1522

AS
#st.
130

#tr.
642

|Σ|
11

2

10

1102

2982

202

1202

13

2

12

1874

5162

290

2018

15

2

14

2942

8206

394

3138

17

2

16

4354

12258

514

4610

19

3

8

1923

7107

243

2163

20

3

10

3803

14323

383

4183

24

4

6

1636

7468

196

1924

23

4

8

4052

19076

356

4580

29

direction,
fwd./bwd.
APvFAS
APwBAS
APvFAS
APwBAS
APvFAS
APwBAS
APvFAS
APwBAS
APvFAS
APwBAS
APvFAS
APwBAS
APvFAS
APwBAS
APvFAS
APwBAS
APvFAS
APwBAS

time
(sec)
1.02
1.00
5.37
5.30
22.21
21.99
76.71
76.03
232.67231.3325.51
25.35
167.68166.8617.58
17.34
210.09212.58

17

space
(GB)
0.30
0.30
1.04
1.05
2.91
2.94
6.86
6.94
13.01
13.20
3.33
3.36
12.21
12.27
2.61
2.64
13.13
13.12

Table 1: Results for the grades protocol [27]5.2.1. Grades Protocol
The grades protocol is introduced in [27] and is used there as a benchmark: the protocol and its specification are expressed as probabilistic programs P and S; they are thentranslated into (purely) probabilistic automata AP and AS by a game semantics-based
tool apex [28]. By establishing L(AP ) = L(AS ), the protocol is shown to exhibit thesame behaviors as the specification—hence is verified. The protocol has two parameters
G and S.
In our experiment we proved L(AP ) = L(AS ) by establishing two-way language inclusion (v and w). The results are shown in Table. 1. For all the choices of parameters G
and S, our program +×-sim was able to establish, without applying +×-PE : AP vF AS(but not vB ) for the v direction; and AP wB AS (but not wF ) for the w direction. In
the table, #st. and #tr. denote the numbers of states and transitions, respectively, and|Σ| is the size of the alphabet. All these numbers are determined by apex.
The table indicates that space is a bigger problem for our approach than time. In [27]four algorithms for checking language equivalence between S+,× -weighted automata are
implemented and compared: two are deterministic [37, 12] and the other two are randomized [27]. These algorithms can process bigger problem instances (e.g. G = 2, S = 100
in ca. 10 sec) and, in comparison, the results in Table 1 are far from impressive. Notehowever that our algorithm is for language inclusion—an undecidable problem, unlike
language equivalence that is in P, see Section 5.1—and hence is more general.
5.2.2. Crowds Protocol
Our second experiment calls for checking language inclusion, making the algorithms
studied in [27] unapplicable. We verified some instances of the Crowds protocol [35]6SIMULATION MATRICES FOR SMAX,+ -WEIGHTED AUTOMATA
param.
n
c
5
1

9
10

AP
#st.
7

#tr.
44

AS
#st.
7

#tr.
56

|Σ|
18

pf

7

1

3
4

9

88

9

118

26

10

2

4
5

12

224

12

280

54

20

6

4
5

22

1514

22

1696

238

30

10

4
5

32

4732

32

5112

550

40

14

4
5

42

10742

42

11392

990

50

17

4
5

52

20504

52

21560

1494

direction
fwd./bwd.
APvFAS
APvBAS
APvFAS
APvBAS
APvFAS
APvBAS
APvFAS
APvBAS
APvFAS
APvBAS
APvFAS
APvBAS
APvFAS
APvBAS

time
(sec)
0.10
0.04
0.59
0.05
42.63
0.07
T/O
0.84
S/O
6.17
S/O
30.70
S/O
102.89

18
space
(GB)
0.02
0.01
0.14
0.01
3.86
0.01

d

0.20

2

1.44

2

6.07

2

13.64

2

2
2
2
2
2
2

Table 2: Results for the Crowds protocol

against a quantitative anonymity specification called probable innocence [29]. We useda general trace-based verification method in [22] for probable innocence: language inclusion L(AP ) v L(AS ), from the model AP of a protocol in question to AP ’s suitable
modification AS , guarantees probable innocence.
The Crowds protocol has parameters n, c and pf . In fact, for this specific protocol,pf
a sufficient condition for probable innocence is known [35] (namely n ≥ pf −1/2
(c + 1));
we used parameters that satisfy this condition. We implemented a small program thattakes a choice of n, c, pf and generates an automaton AP ; it is then passed to anotherprogram that generates AS .
The results are in Table. 2. For each problem instance we tried both vF and vB .
The last column shows the final value of the parameter d for +×-PE —i.e. how manytimes partial execution (Section 4) was applied.
The entry “S/O” designates that +×-PE was killed because of stack overflow causedby an oversized automaton. “T/O” means that alternate application of +×-sim and+×-PE did not terminate within a time limit (one hour).
We observe that backward simulation matrices were much faster to be found thanforward ones. This seems to result from the shapes of the automata for this specificproblem; after all it is an advantage of our forward and backward approach that we
can try two different directions and use the faster one. Space consumption seems again
serious.
6. Simulation Matrices for Smax,+ -Weighted Automata
In this section we discuss Smax,+ -weighted automata, in which weights are understoodas (best-case) profit or (worst-case) cost (see Example 2.2). Such automata are studied
in [7] (called Sum-automata there). In fact we observe that their notion of simulation—
formulated in game-theoretic terms and hence called G-simulation here—coincides with

6

SIMULATION MATRICES FOR SMAX,+ -WEIGHTED AUTOMATA

19

the notion of forward simulation matrix. This observation—that is presented in Section 6.1—follows from the game-theoretic characterization in [1] of linear inequalities in
Smax,+ . In Section 6.2 our implementation is presented.
6.1. G-Simulation by Forward Simulation Matrices
In this section we restrict to finite-state automata. In this case we can dispose of theweight ∞, and have [−∞, ∞) as the domain of weights (see Example 2.2).
What we shall call G-simulation is introduced in [7], and its soundness with respect
to weighted languages over infinite-length words Σω → [−∞, ∞) is proved there. Here
we adapt their definition to the current setting of finite-length words; the adaptation isconcerned with termination X.
Definition 6.1 (vG ) Let A = (QA , Σ, MA , αA , βA ) and B = (QB , Σ, MB , αB , βB ) be
finite-state Smax,+ -weighted automata. A finite simulation game from A to B is playedby two players called Challenger and Simulator : a strategy
 for Challenger is a pair
ρ1 : 1 → QA , τ1 : (QA ×QB )×(Σ×QA ×QB )∗ → 1+Σ×QA of functions; and a strategy
for Simulator is a pair ρ2 : QA → QB , τ2 : (QA ×QB )×(Σ×QA ×QB )∗ ×Σ×QA → QB .
A pair (p0 a1 . . . an pn , q0 a1 . . . an qn ) of runs on A and B is called the outcome ofstrategies (ρ1 , τ1 ) and (ρ2 , τ2 ) if:• ρ1 (•) = p0 and ρ2 (p0 ) = q0 where • is the unique element of the domain of ρ1 .
• τ1 (p0 , q0 )(a1 , p1 , q1 ) . . . (ai , pi , qi ) = (ai+1 , pi+1 ) for each i ∈ [0, n − 1].
• τ2 (p0 , q0 )(a1 , p1 , q1 ) . . . (ai , pi , qi ), (ai+1 , pi+1 ) = qi+1 for each i ∈ [0, n − 1].
• τ1 ((p0 , q0 )(a1 , p1 , q1 ) . . . (an , pn , qn )) = X.
A strategy (ρ1 , τ1 ) for Challenger is winning if for any strategy (ρ2 , τ2 ) for Simulator, theiroutcome (r1 , r2 ) exists and it satisfies L(A)(r1 ) > L(B)(r2 ). Here the weight L(A)(r) ofa run r is defined in the obvious way, exploiting the structure of the semiring Smax,+ .
Finally, we write A vG B if there is no winning strategy for Challenger.
Theorem 6.2 Let A and B be finite-state Smax,+ -weighted automata. Assume that A
has no trap states, that is, every state has a path to X whose weight is not −∞. Then,
A vF B if and only if A vG B.
The extra assumption can be easily enforced by eliminating trap states through backward
reachability check. This does not change the (finite) weighted language.
The proof of Theorem 6.2 is sketched as follows. We first reduce G-simulation (between the original automata A, B on finite words) to G-simulation vLimavg
between Limavg
Gautomata, the original setting in [7] with infinite words. This reduction (that is the firstequivalence below) allows us to exploit the characterization in [7] of G-simulation interms of a mean payoff game, yielding the second equivalence below.
G
A vG B ⇐⇒ ALimavg vLimavg
B Limavg ⇐⇒ Max wins in GA
Limavg ,B Limavg .
G

(8)

6

SIMULATION MATRICES FOR SMAX,+ -WEIGHTED AUTOMATA

20

Conversely, starting from A vF B, we use the fundamental result in [1] that characterizes
feasibility of inequalities in Smax,+ in terms of mean payoff games.
F
A vF B ⇐⇒ a certain linear inequality is feasible ⇐⇒ Max wins in GA,B
.

(9)

G
F
Finally, we observe that the mean payoff games GA
Limavg ,B Limavg in (8) and GA,B in (9) arein fact the same, establishing A vF B if and only if A vG B.
In what follows we introduce necessary definitions and lemmas, eventually leading to
the proof of Theorem 6.2.

Definition 6.3 (Limavg automaton) A Limavg automaton C = (Q, Σ, M, q0 ) consistsof a finite state space Q, a finite alphabet Σ, transition matrices M : Σ → [−∞, ∞)Q×Q ,and the initial state q0 ∈ Q.
For an infinite word w = a0 a1 . . . ∈ Σω , the automaton C assigns a value L(C)(w)
PN
that is calculated by L(C)(w) = supq0 q1 ...∈Q∞ liminf N →∞ N1 i=0 M (ai )qi ,qi+1 .
Lemma 6.4 Given an Smax,+ -weighted automaton C = (Q, Σ, M, α, β), we define a Limavg automaton C Limavg = (QLimavg , ΣLimavg , M Limavg , ?) by
QLimavg = Q + {?} ,ΣLimavg = Σ + {?} + {!} , andM (a)x,y (a ∈ Σ, x, y 6= ?)α(a = ?, x = ?)y
M Limavg (a)x,y = βx(a = !, y = ?)−∞(otherwise) .
Let A = (QA , Σ, MA , αA , βA ) and B = (QB , Σ, MB , αB , βB ) be Smax,+ -weighted automata; assume further that A has no trap states. Then we have
A vG B ⇐⇒ ALimavg vLimavg
B Limavg .
G

Intuitively, the automaton C Limavg is obtained from C by connecting the initial and final
states of C. More concretely, we add a new state ? that represents both the initial andfinal state in C, add transitions from ? to states in C according to the initial vector α,
and add transitions from states in C to ? according to the final vector β.
The proof of the lemma is technical and deferred to Appendix Appendix A.1. The
basic idea is as follows. A winning strategy for the (finite) game for A vG B yields thatfor the other (infinite) game, by repeating the strategy. The other direction is similar,
except that trap states call for special care.
We shall now describe the second equivalence in (8). The notion of mean payoff gameis from [13].
Definition 6.5 (mean payoff game) A weighted bipartite graph G = (QMin , QMax , qI , E, γ)
consists of a set QMin of states for Min, a set QMax of states for Max, the initial stateqI ∈ QMin , a set E = QMin × QMax + QMax × QMin of edges, and a weight function
γ : E → R.

6

SIMULATION MATRICES FOR SMAX,+ -WEIGHTED AUTOMATA

21

A mean payoff game is a game played by two players Min and Max on a weighted
bipartite graph G. A strategy for Min is a function τMin : (QMin ×QMax )∗ ×QMin → QMax
and a strategy for Max is a function τMax : (QMin × QMax )+ → QMin . An infinite run
p0 q0 p1 q1 . . . on G (here pi ∈ QMin and qi ∈ QMax ) is the outcome of strategies τMin andτMax if p0 = qI and for any i ≥ 1, τMin (p0 q0 . . . qi−1 pi ) = qi and τMin (p0 q0 . . . pi qi ) = pi+1 .
A strategy τMax for Max is winningτMax for Min, their outcome

PNif for any strategy
r0 r1 r2 r3 . . . satisfies liminf N →∞ N1 i=0 γ(ri , ri+1 ) ≥ 0.
0
Lemma 6.6 ([7]) Let E = (QE , Σ, ME , qE0 ) and F = (QF , Σ, MF , qF
) be Limavg automata. We have E vG F if and only if Max wins in the mean payoff game GE,F , where
the game GE,F = (QMin , QMax , qI , E, γ) is defined by0
QMin = QE × QF ,QMax = QE × QF × Σ ,qI = (qE0 , qF
) ,


0
0
E = ((p, q), (p , q, a)) ME (a)p,p0 6= −∞ + ((p, q, a), (p, q )) MF (a)q,q0 6= −∞0γ((p, q), (p , q, a)) = −ME (a)p,p0and0γ((p, q, a), (p, q )) = MF (a)q,q0 .

,

We turn to the equivalences in (9). The following proposition is interesting for its own
sake, characterizing vF for Smax,+ -weighted automata in terms of mean payoff games.
We crucially rely on a result in [1].
Proposition 6.7 For a pair of Smax,+ -weighted automata A and B, there exists a meanF
F.
such that: A vF B if and only if Max wins in GA,B
payoff game GA,B
Proof. Let A = (QA , Σ, MA , αA , βA ) and B = (QB , Σ, MB , αB , βB ). By Definition 3.4,
QB ×QAa forward simulation matrix from A to B is a matrix X ∈ Smax,+that satisfies
αA ≤ αB X ∧ ∀a ∈ Σ. XMA (a) ≤ MB (a)X ∧ XβA ≤ βB .

(10)The result in [1] reduces:• existence of a nontrivial (i.e. not −∞) solution of a linear inequality Ax ≤ Bx,
where A, B are matrices over Smax,+ and x is a column vector of variables, to• a mean payoff game.
We therefore need to transform (10) into the format Ax ≤ Bx. In particular, αA andβB on both ends of (10) should be taken care of.
We shall prove that: there exists a matrix X that satisfies (10), if and only if, there
QB ×QA
exist x?,? ∈ Smax,+ and X 0 ∈ Smax,+that satisfy x?,? 6= −∞ andx?,? αA ≤ αB X 0 ∧ ∀a ∈ Σ. X 0 MA (a) ≤ MB (a)X 0 ∧ X 0 βA ≤ x?,? βB .

(11)

Note here that x?,? αA denotes the vector αA multiplied by the scalar x?,? . Here “multiplication” is by the semiring multiplication of Smax,+ , that is, addition of real numbers.
Indeed, if X satisfying (10) exists, then x?,? = 0 and X 0 = X satisfy (11). Conversely,
QB ×QA
QB ×QA
if x?,? ∈ Smax,+ (where x?,? 6= −∞) and X 0 ∈ Smax,+satisfy (11), then X ∈ Smax,+0
defined by Xq,p = Xq,p − x?,? satisfies (10). Here −x?,? denotes subtraction of the real
number x?,? . It is well-defined and constitutes the inverse of (semiring-)multiplication
by x?,? , since x?,? 6= −∞.

6

SIMULATION MATRICES FOR SMAX,+ -WEIGHTED AUTOMATA

22

It is straightforward to translate (11) into the format Ax ≤ Bx. Then applying theresult [1] yields the following mean payoff game, Max’s winning in which is equivalent to
the feasibility of (11), hence to that of (10).
F
F
F
F
F
The game is played on a graph GA,B
= (QF
Min , QMax , qI , E , γ ), where
QF
Min = {x?,? } + {xq,p | q ∈ QB , p ∈ QA } ,QF
Max = QA + Σ × QB × QA + QB ,qIF = x?,?
F
FFF
E F = E1F + E2F where E1F ⊆ QF
Min × QMax , E2 ⊆ QMax × QMin andE1F = {(x?,? , p) | (αA )p 6= −∞}} + {(xq,p , (a, q, p0 )) | MA (a)p,p0 6= −∞}+ {(xq,p , q) | (βA )p 6= −∞}E2F = {(p, xq,p ) | (αB )q 6= −∞} + {((a, q, p), xq0 ,p ) | MB (a)q,q0 6= −∞}+ {(q, x?,? ) | (βB )q 6= −∞} ,γ F (x?,? , p) = −(αA )p ,γ F (xq,p , (a, q, p0 )) = −MA (a)p,p0 ,γ F (xq,p , q) = −(βA )pγ F (p, xq,p ) = (αB )q ,γ F ((a, q, p), xq0 ,p ) = MB (a)q,q0 ,γ F (q, x?,? ) = (βB )q .

This concludes the proof.

Finally, we bridge the rightmost conditions in (8–9) and prove Theorem 6.2.
Proof of Theorem 6.2. Let A = (QA , Σ, MA , αA , βA ) and B = (QB , Σ, MB , αB , βB ).
By Lemma 6.4 and Lemma 6.6, A vG B is equivalent to existence of a winning stratGGG
GGegy for Max in the mean payoff game played on a graph GA, γ G ).
Limavg ,B Limavg = (QMin , QMax , qI , E
It is defined by
QG
Min = ({?} + QA ) × ({?} + QB ) ,QG
Max = ({?} + QA ) × ({?} + QB ) × ({?} + {!} + Σ) ,qIG = (?, ?) ,GGGGE = E1G + E2G s.t. E1G ⊆ QG
Min × QMax , E2 ⊆ QMax × QMin andE1G = {((?, ?), (p, ?, ?)) | (αA )p 6= −∞}} + {((p, q), (p0 , q, a)) | MA (a)p,p0 6= −∞}+ {((p, q), (?, q, !)) | (βA )p 6= −∞}E2G = {((p, ?, ?), (p, q)) | (αB )q 6= −∞} + {((p, q, a), (p, q 0 )) | MB (a)q,q0 6= −∞}+ {((?, q, !), (?, ?)) | (βB )q 6= −∞} ,γ G ((?, ?), (p, ?, ?)) = −(αA )p , γ G ((p, q), (p0 , q, a)) = −MA (a)p,p0 , γ G ((p, q), (?, q, !)) = −(βA )pγ G ((p, ?, ?), (p, q)) = (αB )q ,γ G ((p, q, a), (p, q 0 )) = MB (a)q,q0 ,γ G ((?, q, !), (?, ?)) = (βB )q .

GF
It is not hard to see that the last graph GA
Limavg ,B Limavg is equivalent to GA,B in Proposition 6.7: the former has extra states but they are all unreachable.


Remark 6.8 (complexity) The decision problem of mean payoff games is known to
be in NP ∩ co-NP [39]; it has a pseudo polynomial-time algorithm, too [39]. By [1]6SIMULATION MATRICES FOR SMAX,+ -WEIGHTED AUTOMATA

23

this problem is equivalent to the feasibility problem of linear inequalities in Smax,+ . For
the latter problem, the algorithm proposed in [6] (for solving linear equalities) can beutilized; this algorithm is shown in [4] to be superpolynomial. These results give upperbounds for the complexity of vF and vG , by Theorem 6.2 and the subsequent lemmas.
Similarly to S+,× -weighted automata, language inclusion between Smax,+ -weighted
automata is known to be undecidable [30]. We note that, by Theorem 6.2, applying FPE
or BPE (Section 4) increases the likelihood of vG (in the sense of Theorem 4.4). We additionally note that, by exploiting symmetry of forward and backward simulation matrices(Remark 3.7), we could define “backward G-simulation” as a variation of Definition 6.1.
6.2. Implementation, Experiments and Discussions
We implemented two programs: max+-sim and max+-PE .
• We have seen that finding simulation matrices can be reduced to some problems
that have known algorithms. Since we did not find actual software available, we
implemented (in C++) the algorithm in [6] (for solving Smax,+ -linear equalities) as
part of the program max+-sim . It transforms the constraints in Definition 3.4 into
an inequality Ax ≤ Bx, which in turn is made into a linear equality A0 x0 = B 0 x0
by adding slack variables. The last equality is solved by the algorithm in [6].
• max+-PE is as in Section 5. It simply uses the whole state space as the parameter
P.
Experiments were done on a MacBook Pro laptop with a Core i5 processor (2.6 GHz,
2 cores) and 16 GB RAM. There we faced a difficulty of finding a benchmark example:
although small examples are not hard to come up with by human efforts, we could not
find a good example that has parameters (like G, S in Table 1) and allows for experimentswith problem instances of a varying size.
We therefore ran max+-sim for:• the problem if A vF A for randomly generated A, and• the problem if A vF B for randomly generated A, B,
and measured time and memory consumption. Although the answers are known byconstruction (positive for the former, and almost surely negative for the latter), actual
calculation via linear inequality constraints gives us an idea about resource consumptionof our simulation-based method when it is applied to real-world problems.
The outcome is as shown in Figure 3. The parameter p is the probability with which
an a-transition exists given a source state, a target state, and a character a ∈ Σ. Its
weight is chosen from {0, 1, . . . , 16} subject to the uniform distribution. “Same” means
checking A vF A and “difference” means checking A vF B (see above). The two problem
settings resulted in comparable performance.
We observe that space consumption is not so big a problem as in the S+,× case(Section 5.2). Somehow unexpectedly, there is no big performance gap between thesparse case (p = 0.1) and the dense case (p = 0.9); in fact the sparse case consumes
slightly more memory. Consumption of both time and space grows faster than linearly,
which poses a question about the scalability of our approach. That said, our current

7

MATRIX SIMULATION FOR POLYNOMIAL FUNCTORS
1800

45

1400

max space consumption (MB)p=0.1,same
p=0.9,same
p=0.1,different
p=0.9,different

1600
time consumption (s)

24

1200
1000
800
600
400
200
0

p=0.1,same
p=0.9,same
p=0.1,different
p=0.9,different

40
35
30
25
20
15
10
5
0

20

40

60
80
100
120
the number of states

140

160

20

40

60

80
100
120
the number of states

140

160

Figure 3: Time and max space consumption for max+-sim

implementation of the algorithm in [6] leaves a lot of room for further optimization: one
possibility is use of dynamic programming (DP). After all, it is an advantage of ourapproach that a simulation problem is reduced to linear inequality constraints, a subjectof extensive research efforts (cf. Section 5.1 and Section 6.1).
7. Matrix Simulation for Polynomial Functors
In the previous sections, we concentrated our attention on matrix simulations forweighted (word) automata. They are special cases of (T, F )-systems where T is a multiset
monad over some semiring and F = 1+Σ×( ). However, according to the general theory
developed in [21, 18], Kleisli simulation can be defined and its soundness can be proved
for more general (T, F )-systems.
In this section, we generalize the functor F from 1 + Σ × ( ) (that we have beenusing) to an arbitrary polynomial functor:aF ::= ( ) | Σ | F1 × F2 |
Fi .
(12)
i∈I

Such a generalized (T, F )-system—where T is again a multiset monad—represents asystem called a weighted tree automaton. Here, the choice of F determines the shape oftrees to which the automaton assigns a weight.
This section is organized as follows. In Section 7.1 we build on [18] and introduce thenotion of forward partial execution (FPE) on the coalgebraic level of abstraction. We
also prove its correctness (soundness and adequacy); the overall coalgebraic theory (i.e.
the one in [18] augmented with FPE) generalizes the one in Section 4 for weighted (word)
automata. The abstract theory thus obtained is applied in Section 7.2 to weighted tree
automata—i.e. (T, F )-systems with T being a multiset monad and F being a polynomial functor. Much like for word automata, Kleisli simulations for tree automata arerepresented by matrices, subject however to nonlinear inequality constraints. Finally in
Section 7.3 our proof-of-concept implementation is presented.

7

MATRIX SIMULATION FOR POLYNOMIAL FUNCTORS

25

7.1. Forward Partial Execution, CategoricallyDefinition 7.1 (FPE, categorically) Forward partial execution (FPE) for (T, F )-systems
p X, c : X →p F X) andis a transformation that takes: a (T, F )-system X = (X, s : {•}→a parameter X1 ⊆ X as input; and returns a (T, F )-system XFPE,X1 .
The outcome XFPE,X1 is defined as follows. Let c1 and c2 be the domain restrictions
p X. That is explicitly:of c to X1 and X2 , respectively, via the coprojections κi : Xi →c1 = cp FX
κ1 : X1 →p FX ,
κ2 : X2 →and c2 = c

where denotes composition of Kleisli arrows (Definition 2.7). We define X2 = X \ X1
(hence X = X1 + X2 ); the system XFPE,X1 is now given by
F (X) + X2 ,s/ F (X) + X2 ,/ X1 + X2 c1 +id.
{•}
XFPE,X1 = 



[id,c
]
F
(c
+id)
2
1


/
/
F (X) + X2
F (X1 + X2 )F F (X) + X2
Here F : K`(T ) → K`(T ) is the canonical lifting of F : Sets → Sets (see [24] for a
concrete definition).
For the last categorical generalization of FPE, we shall establish its correctness—soundness, adequacy and monotonicity—much like in Section 4.3.
Theorem 7.2 (soundness of categorical FPE) Let X1 and Y1 be arbitrary subsetsof the state spaces of X and Y, respectively. Each of the following implies tr(X ) v tr(Y).
1. XFPE,X1 vF Y
2. X vB YFPE,Y1



Theorem 7.3 (adequacy of categorical FPE) Let X1 and Y1 be arbitrary subsets ofthe state spaces of X and Y, respectively. We have:
1. X vF Y ⇒ XFPE,X1 vF Y
2. X vB Y ⇒ X vB YFPE,Y1

The last two theorems are immediate consequences of the following lemma. The lastis a categorical generalization of Lemma 4.5.
Lemma 7.4 For each subset X1 of the state space of X , we have:
1. X vB XFPE,X1
2. XFPE,X1 vF X
p F (X) + X2 by g = c1 + id. Then we have
Proof. 1. We define g : X1 + X2 →F (g)c = F (c1 + id)[c1 , c2 ]= F (c1 + id)[id, c2 ]= F (c1 + id)gs = (c1 + id)

s.

[id, c2 ](c1 + id)


g ,

7

MATRIX SIMULATION FOR POLYNOMIAL FUNCTORS

26

Note here that F (c1 + id) [id, c2 ] is the dynamics of the system XFPE,X1 . The above
equalities witness that g indeed satisfies the inequalities required in the definition of
backward Kleisli simulation, a generalization of Definition 2.12 that is found in [18].
Hence g is a backward simulation from X to XFPE .
The item 2. is proved similarly: the same g that we used in the proof of the item 1.
is shown to be a forward simulation from XFPE to X .
Finally, we present a monotonicity result. It generalizes Proposition 4.6.
Proposition 7.5 (monotonicity of categorical FPE) Assume X1 ⊆ X10 and X2 ⊆X20 . We have:
1. XFPE,X1 vF Y ⇒ XFPE,X10 vF Y
2. X vB YFPE,Y2 ⇒ X vB YFPE,Y20



Categorical formalization of BPE is still open—it seems that BPE in Section 4 exists
somewhat coincidentally, for the specific functor F = 1 + Σ × ( ) for which an opposite
automaton is canonically defined (cf. Remark 3.7).
7.2. Matrix Simulations for Weighted Tree Automata
Here we exploit the general theory we have just obtained (by augmenting [18] with
FPE). We shall apply it to a class of systems that is more general than what we have been
dealing with in the previous sections (namely weighted (word) automata). Specifically,
we use the same monads for T but allow arbitrary polynomial functors for F . Suchsystems are naturally identified with weighted tree automata, where a finite-depth tree,
instead of a finite word, gets a weight assigned.
We first define the notion of tree.
Definition 7.6 A ranked alphabet is a family Σ = (Σn )n∈N of countable sets that areindexed by natural numbers called arities.
The set Tree(Σ) of (finite-depth) trees over a ranked alphabet Σ is defined in theobvious way. Concretely, Tree(Σ) is the smallest set such that: for each a ∈ Σn ,t0 , t1 , . . . , tn−1 ∈ Tree(Σ) implies a(t0 , t1 , . . . , tn−1 ) ∈ Tree(Σ).
We introduce weighted tree automata, firstly in concrete terms.
Definition 7.7 (S-weighted tree automaton, weighted tree language) Let S =(S, +S , 0S , ×S , 1S , v) be a commutative cppo-semiring. An S-weighted tree automaton isa quadruple A = (Q, Σ, M, α) consisting of a countable state space Q, a ranked alphabetnΣ = (Σn )n∈N , transition matrices M (a) ∈ S Q×Q for each a ∈ Σn , and the initial row
vector α ∈ S Q .
An S-weighted tree automaton A = (Q, Σ, M, α) yields a weighted tree language
L(A) : Tree(Σ) → S. It is defined by L(A)(t) = α · Φ(t)—the product of a row vector α
and a column vector Φ(t)—where Φ : Tree(Σ) → S Q is defined as follows, by induction
on the depth of trees.
Φ a(t0 , t1 , . . . , tn−1 ) = M (a) Φ(t0 ) ⊗ Φ(t1 ) ⊗ · · · ⊗ Φ(tn−1 )for each a ∈ Σn .

7

MATRIX SIMULATION FOR POLYNOMIAL FUNCTORS

27

The final column vector β in Definition 2.3 do not appear here; transition matrices M (a)for a ∈ Σ0 play the corresponding role.
Language inclusion between two S-weighted tree automata is defined similarly to thecase with S-weighted automata.
Definition 7.8 (language inclusion) Let A and B be S-weighted tree automata. We
say the language of A is included in the language of B and write L(A) v L(B) if, for allt ∈ Tree(Σ), L(A)(t) v L(B)(t).
Similarly to S-weighted (word) automata (see Proposition 2.6), S-weighted tree automata are instances of (T, F )-systems.
Definition 7.9 (the functor FΣ ) It is standard that a ranked alphabet Σ gives rise toa polynomial functor. It is given as follows and is denoted by FΣ .
aFΣ =Σn × ( )n : Sets −→ Sets .
n∈N

Proposition 7.10 (weighted tree automata as (T, F )-systems) Let S be a commutative cppo-semiring. An S-weighted tree automaton A = (Q, (Σn )n∈N , M, α) gives
rise to an MS , FΣ )-system XA = (Q, sA , cA ) defined as follows. The function sA : {•} →MS Q is given by sA (•)(x) = αx ; and cA : Q → MS (FΣ Q) is given bycA (x) a, (y0 , y1 , . . . , yn−1 ) = M (a)x,(y0 ,y1 ,...,yn−1 )where a ∈ Σn .

The last identification allows us to apply the general results in [18, 21] to weighted
tree automata. One of the results characterizes coalgebraic trace semantics by a final
coalgebra in the Kleisli category K`(MS ); it is easy to see that, for weighted tree automata, coalgebraic trace semantics is nothing but the weighted tree language concretely
defined in Definition 7.7.
The notions of forward and backward Kleisli simulation is defined in [18] in categoricalterms; and a (categorical) proof of their soundness against coalgebraic trace semantics
is presented. Much like in the previous sections, we shall now characterize Kleisli simulations for weighted tree automata by matrices; their soundness then follows from theabove mentioned categorical proof.
The following lemma is a generalization of Lemma 3.3. It introduces the matrix
representation of the action of the functor FΣ on Kleisli arrows.
p B be a Kleisli arrow in K`(MS ) and Mf be its matrix
Lemma 7.11 Let f : A →representation (see Definition 3.1). Then the matrix representation MFΣ f of the arrowFΣ f is given byMIΣn ⊗ Mf⊗n
∈ S (FΣ A)×(FΣ B) .
(13)
n∈N
`
`

L
( n∈N An )×( n∈N Bn )Here, for each n ∈ N and Xn ∈ S An ×Bn ,is definedn∈N Xn ∈ S
by
(
M

(Xn )x,y (x ∈ An , y ∈ Bn )
Xn
=
x,y
0
(otherwise)n∈N

7

MATRIX SIMULATION FOR POLYNOMIAL FUNCTORS

28

that is a generalization of the binary operation ⊕. The matrix X ⊗n is defined by
X ⊗n = X ⊗ X ⊗ · · · ⊗ X .
{z
}
|



n

We note that the matrix in (13) is equivalently expressed as

L

n∈N


Mf⊗n ⊕ Mf⊗n ⊕ · · · ⊕ Mf⊗n .
|
{z
}
|Σn |

In what follows, Definition 7.12 and Theorem 7.13 are parallel to Definition 3.4 andCorollary 3.6, respectively.
Definition 7.12 (simulation matrix) Let A = (QA , Σ, MA , αA ) and B = (QB , Σ, MB , αB )be S-weighted tree automata.
• A matrix X ∈ S QB ×QA is a forward simulation matrix from A to B if
αA v αB X ,and X · MA (a) v MB (a) · (X ⊗n )for any n ∈ N and a ∈ Σn .

• A matrix X ∈ S QA ×QB is a backward simulation matrix from A to B if
αA X v αB ,and MA (a) · (X ⊗n ) v X · MB (a)for any n ∈ N and a ∈ Σn .

Similarly to the case of semiring weighted automata, we write A vF B and A vB B
if there exists a forward and backward matrix simulation from A to B, respectively.
Theorem 7.13 (soundness) Let A and B be S-weighted tree automata. Existence of aforward or backward simulation matrix from A to B—i.e. A vF B or A vB B—witnesses
language inclusion L(A) v L(B).
Proof. Simulation matrices in Definition 7.12 coincide with Kleisli simulations in thegeneral theory of [18]. The latter is sound with respect to coalgebraic trace semantics [18,21]; and the last coincides with the weighted tree language in Definition 7.7.

We note that, differently from matrix simulations for semiring weighted automata(Definition 3.4), the inequalities in Definition 7.12 are not necessarily linear. For example,

X

⊗2




= · · ·.
.
.
xi,j X
.
.
.





· · · .
This nonlinearity poses an algorithmic challenge: many known algorithms for feasibilityof inequalities are restricted to linear ones. See Section 7.3 for further discussions.
In the remainder of this section, we present a concrete definition of forward partial
execution for weighted tree automata. It is an instance of Definition 7.1. Its soundness,
adequacy and monotonicity follow from the general results in Section 7.1.

7

MATRIX SIMULATION FOR POLYNOMIAL FUNCTORS

29

Definition 7.14 (FPE for weighted tree automata) Forward partial execution (FPE)
is transformation of a weighted tree automata such that: given an S-weighted tree automaton A = (Q, Σ, M, α) where Σ = (Σn )n , and a parameter P ⊆ Q, the resulting
automaton AFPE,P = (Q0 , Σ, M 0 , α0 ) is as follows. It has a state space
Q0 = (a, (y0 , y1 , . . . , yn−1 )) a ∈ Σn , ∃x ∈ P. M (a)x,(y0 ,y1 ,...,yn−1 ) 6= 0S + (Q \ P ) ,(14)that replaces each state x ∈ P with its one-step behaviors (a, (y0 , y1 , . . . , yn−1 )) as newstates. As for the transition matrices M 0 ,M 0 (a)(a,(x0 ,...,xn−1 )),n−10)),...,(an−1 ,(y0n−1 ,...,ym))(a0 ,(y00 ,...,ym
0 −1
n−1 −1

=

n−1
Y

i
M (ai )xi ,(y0i ,...,ym
−1 )

i=0

i

M 0 (a)(a,(x0 ,x1 ,...,xn−1 )),(x0 ,x1 ,...,xn−1 ) = 1S
M 0 (a)n−1n−10,...,ymx, (a0 ,(y00 ,...,ym−1 )),...,(an−1 ,(y0n−1 −1

0



n−1
O
M (ai )= M (a) ·
i=0

))



n−1
n−1
0
,...,ymx, (y00 ,...,ym−1 ),...,(y00n−1 −1)M 0 (a)x,y = M (a)x,y
where a ∈ Σn , ai ∈ Σmi , and x, xi , yji ∈ Q. For all the other cases we define M 0 (a)u,v =0S . As for the initial vector α0 , the definition is shown below.
0α(a,(x= (αM (a))(x0 ,...,xn−1 ) ,0 ,...,xn−1 ))αx0 = αxWe do not yet have a good definition of backward partial execution for weighted tree
automata, probably for the reason that we argued at the end of Section 7.1.
7.3. Implementation, Experiments and Discussions
We implemented, in OCaml, a program +×-treesim that searches for forward andbackward simulation matrices between two given S+,× -weighted tree automata. It firstcombines the constraints in Definition 7.12 into a system of (possibly nonlinear) polynomial inequalities, and tries to solve it with the FindInstance function of Mathematica [32].
We discuss the size of the system of inequalities to be solved. Assume that our goal
is to establish A vF B. Let n be the number of states of A and m be that of B. (Incase our goal is A vB B we swap n and m.) Let d be the maximum
P arity in the ranked
alphabet Σ. Then the number of inequality constraints is at most k∈N |Σk | · m · nk ; andthe degree of each polynomial inequality constraint is at most d.
Experiments were done on a MacBook Pro laptop with a Core i5 processor (2.6 GHz,
2 cores) and 16 GB RAM. In our experiments we let the program +×-treesim try toestablish A vF A (or A vB A) for a randomly generated tree automaton A.
Our current implementation turned out to be far from scalable: for the maximum
arity d = 2, 3 and an automaton A with several states and transitions, the program
barely manages to establish the goal; it becomes hopeless for bigger problem instances.
This is in a sense as we expected: use of a general purpose algorithm like FindInstance8

RELATED WORK30

in Mathematica would never be a performance advantage; in fact, FindInstance tends
to abort after tens of seconds, consuming a few MBs of memory, for reasons that wecannot know. An obvious alternative is to use special purpose algorithms—like the ones
that are known in the field of convex optimization. This is left as future work.
8. Related Work(Bi)simulation notions and (weighted) language equivalence/inclusion for quantitative systems have been an active research topic in the field of formal verification andconcurrency. Some related work in this direction has already discussed in the earlier
sections, including [25, 7, 2, 27, 5]. Moreover, works like [23, 18, 22, 36] take a categorical/coalgebraic approach.
Use of matrices as witnesses of quantitative language equivalence/inclusion is in fact
not uncommon. The rest of this section is devoted to the discussion of such works, andtheir comparison to the current work. Overall, the current work is distinguished in thefollowing aspects.
• The categorical backend of Kleisli simulation that allows clean theoretical developments. The latter include: the duality between forward and backward simulation;a general soundness proof; and generalization to tree automata (Section 7).
• Our simulations witness language inclusion, a problem that is harder than language
equivalence (see Section 5.1).
• Forward/backward partial execution (Section 4) that enhances effectivity of theapproach by matrix simulations.
• Actual implementation of the algorithms and experiments.
In [3], a notion called conjugacy between semiring weighted (word) automata is introduced. It is an equivalence notion—it is a special case of vF in the current work,with the inequalities in Definition 3.4 replaced with equalities. The notion of conjugacy
comes with “completeness”: assuming that the weight semiring is so-called a divisionring, two automata are equivalent if and only if they are connected by some finite chainof conjugacies.
The notion of simulation in [14] is essentially the same as conjugacy in [3] (it istherefore an equivalence notion unlike the name). A simulation in [14] witnesses language
equivalence. In [14] a semiring S is called proper when: two S-weighted automata arelanguage equivalent if and only if they are connected by a finite chain of simulations.
The authors go on to study proper semirings: they present a necessary condition for asemiring to be proper, and an example that is not proper (namely Smax,+ ).
The results in [14] have been extended to weighted tree automata in [15]. Their simulation is a special case of ours (Definition 7.12) where inequalities are replaced withequalities; soundness with respect to tree language equivalence is proved; and completeness of a combined simulation (with an intermediate automaton, much like in our vBF
and vFB ) is shown, under some assumptions.
Unlike the work discussed in the above, the works [8, 9, 11] study simulations given
by matrices in the context of fuzzy automata. Here simulation is an oriented notion and9CONCLUSIONS AND FUTURE WORK

31

witnesses language inclusion (instead of language equivalence); its definition is essentiallythe same as ours (Definition 3.4). A principal difference between [8] and the current work
is in the domain of weights: in [8] it is a structure called residuated lattice.
Algorithmic aspects of the simulation notion in [8] is pursued in [9], where an algorithm for computing the greatest simulation is presented. Their algorithm works for ageneral residuated lattice, unlike ours where linear inequalities are solved in semiringspecific manners.
These results in [8, 9] are adapted in [11] to automata weighted in a semiring (insteadof a residuated lattice)—although some assumptions are imposed on a semiring and thismakes the semiring S+,× unqualified.
9. Conclusions and Future WorkWe introduced simulation matrices for weighted automata. While they are instancesof (categorical) Kleisli simulations, their concrete presentation by matrices and linear inequalities yields concrete algorithms for simulation-based quantitative verification. Generalization to weighted tree automata follows immediately from the categorical theory
behind, too, although linearity is lost in general.
There are some directions in which the current matrix-based simulation framework
can be further generalized. Our idea of S+,× -weighted automata was that they areprobabilistic systems; when we wish to accommodate uncountable state spaces (for which
discrete probabilities are hardly meaningful), we would need suitable measure theoretic
machinery. In the context of the current work of traces and simulations, this will involve
replacing Sets with Meas (the category of measurable sets and measurable functions),
and matrix multiplication with Lebesgue integration. Trace semantics for probabilistic
automata in Meas has been studied e.g. in [10, 26].
In fact, use of Meas as a base category becomes necessary if we consider infinite trace
semantics—i.e. a language of accepted infinite words—even if a state space is countable(i.e. discrete). This is simply because the set Σω of all infinite words is not countable.
We are currently working on the soundness of matrix simulations against languages of
infinite words; details will be presented in another venue.
Further generalization of the current theory will be concerned with acceptance conditions that are unique to infinite words. An example is the Büchi acceptance condition,
for which a simulation notion (for the nondeterministic setting) has been studied in [16].
Finally, further optimization of our implementation is obvious future work.
Acknowledgments
Thanks are due to Andrzej Murawski, Shota Nakagawa and the anonymous referees
for the conference version for useful discussions and comments; and to Björn Wachterfor the user support of the tool apex. The authors are supported by Grants-in-Aid forYoung Scientists (A) No. 24680001, JSPS.

APPENDIX AOMITTED PROOFS

32

Appendix A. Omitted Proofs
Appendix A.1. Proof of Lem. 6.4
Proof. We prove the contraposition of each direction.
Assume that A vG B, i.e. there exists a winning strategy (ρ1 , τ1 ) for Challenger ina finite simulation game played on A and B. Then a strategy that repeats ρ1 and τ1 isa winning strategy for Challenger in an infinite simulation game played on ALimavg and
B Limavg . Hence ALimavg vLimavg
B Limavg .
G
Conversely, assume ALimavg vLimavg
B Limavg . Then there exists a winning strategy τ1∞
G
for Challenger in an infinite simulation game played on ALimavg and B Limavg . By [13],without loss of generality, we may assume that τ1∞ is a positional strategy; i.e. the valueof τ1∞ ((p0 , q0 )(a1 , p1 , q1 ) . . . (ai , pi , qi )) only depends on pi and qi .
One might hope to use τ1∞ itself as Challenger’s winning strategy for the finite gamefor A vG B. This does not work in general, since a resulting run may not come back to ?.
Modification of τ1∞ to force to visit ? may make the strategy less advantageous. We shallshow that such modification is nevertheless feasible, by finding an upper bound r for “thedisadvantage that results from visiting ?.” In the infinite game for ALimavg vLimavg
B Limavg ,Ga winning strategy can always additionally “save” the advantage r; and it will be spent
to visit ?.
To each x ∈ QA we shall choose and assign an exit path πx . Specifically, by theassumption that A has no trap states, each state x ∈ QA has a finite path πx =xb1 u1 b2 . . . bm um in A that “reaches the final state,” that is, the path satisfies
MA (b1 )x,u1 + MA (b2 )u1 ,u2 + · · · + MA (bn )um−1 ,um + (βA )um 6= −∞ .
Within the path πx , the advantages that Simulator can make are bounded: this follows from the assumptions that no weight in B is ∞, and that B is finite state (sothat there are only finitely many choices of an initial state). Since there are only
finitely many x ∈ QA , we can take a global upper bound r ∈ R. To summarize,
the real number r is chosen so that: for each x ∈ QA , for the choice of an exit
path πx = x bx,1 ux,1 bx,2 . . . bx,m(x) ux,m(x) as described above, and for each path π =y bx,1 y1 bx,2 . . . bx,m(x) ym(x) in B on the same word bx,1 bx,2 . . . bx,m(x) , we haveMA (bx,1 )x,ux,1 + MA (bx,2 )ux,1 ,ux,2 + · · · + MA (bx,m(x) )ux,m(x)−1 ,ux,m(x) + (βA )ux,m(x) + r> MB (bx,1 )y,y1 + MB (bx,2 )y1 ,y2 + · · · + MB (bx,m(x) )ym(x)−1 ,ym(x) + (βB )ym(x) .
(A.1)
Using this r ∈ R (“an upper bound for the cost of visiting ?”), we shall construct
a strategy ρ01 : 1 → QA , τ10 : (QA × QB ) × (Σ × QA × QB )∗ → 1 + Σ × QA for
Challenger in the finite simulation game for A vG B as follows. For a pair of runsR
R = (p0 a1 . . . ai pi , q0 a1 . . . ai qi ) on A and B, we define the accumulated weights SA
and
R
SB by
R
SA
= (αA )p0 +MA (a1 )p0 ,p1 +· · ·+MA (ai )pi−1 ,pi and SBR = (αB )q0 +MB (a1 )q0 ,q1 +· · ·+MB (ai )qi−1 ,qi .
R
While SA≤ SBR + r (i.e. the saving is not enough for the cost of visiting ?), ρ01 and τ10
are defined as follows. They do essentially the same thing as τ1∞ does, except that τ10

APPENDIX AOMITTED PROOFS

33

terminates when ? is visited.
ρ01 (•) = τ1∞ ((?, ?))τ10 (p0 , q0 )(a1 , p1 , q1 ) . . . (ai , pi , qi )(X=
τ1∞ (p0 , q0 )(a1 , p1 , q1 ) . . . (ai , pi , qi )
τ1∞ (p0 , q0 )(a1 , p1 , q1 ) . . . (ai , pi , qi ) = (!, ?)(otherwise).
(A.2)
R
Assume that SA> SBR + r is satisfied at a certain stage, say at the state pn ∈ QA for
the first time. After that, τ10 is defined for each 1 ≤ j ≤ m(pn ) by:τ10 (p0 , q0 )(a1 , p1 , q1 ) . . . (an , pn , qn )(bpn ,1 , upn ,1 , y1 ) . . . (bpn ,j , upn ,j , yj )
(

(A.3)
(bpn ,j+1 , upn ,j+1 ) j < m(pn )=X
j = m(pn )where πpn = pn bpn ,1 upn ,1 bpn ,2 . . . bpn ,m(pn ) upn ,m(pn ) is the exit path for pn that we have
fixed in the above. Here τ10 is headed to the exit along πpn , no matter what Simulator’s
move yj is.
It remains to show that the strategy (ρ01 , τ10 ) of Challenger’s is winning in the finite
game for A vG B. In the case where the clause (A.3) is never invoked, we must havethat τ1∞ (p0 , q0 )(a1 , p1 , q1 ) . . . (ai , pi , qi ) = (!, ?) holds for some i. At such i Challenger
must have an accumulated weight that is strictly bigger than Simulator does: by theassumption that τ1∞ is positional, the strategy τ1∞ will just repeat what it has done, andit will not win unless it is winning so far.
Finally, in the case where the clause (A.3) is invoked, the advantage that Simulator
makes between the time n + 1 and n + m(pn ) is at most r by the definition of r. This
does not eat up the “saving” r.
Therefore we have shown that A vG B. This concludes the proof.

References[1] Akian, M., Gaubert, S., Guterman, A.E.: Tropical polyhedra are equivalent to mean payoff games.
International Journal of Algebra and Computation 22(1) (2012)[2] Baier, C., Hermanns, H., Katoen, J.P.: Probabilistic weak simulation is decidable in polynomial
time. Inf. Process. Lett. 89(3), 123–130 (2004)[3] Béal, M., Lombardy, S., Sakarovitch, J.: On the equivalence of Z-automata. In: Caires, L., Italiano,
G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) Automata, Languages and Programming, 32nd
International Colloquium, ICALP 2005, Lisbon, Portugal, July 11-15, 2005, Proceedings. Lecture
Notes in Computer Science, vol. 3580, pp. 397–409. Springer (2005)[4] Bezem, M., Nieuwenhuis, R., Rodrı́guez-Carbonell, E.: Exponential behaviour of the butkoviczimmermann algorithm for solving two-sided linear systems in max-algebra. Discrete Applied Mathematics 156(18), 3506–3509 (2008)[5] Blondel, V.D., Canterini, V.: Undecidable problems for probabilistic automata of fixed dimension.
Theory Comput. Syst. 36(3), 231–245 (2003)[6] Butkovic, P., Zimmermann, K.: A strongly polynomial algorithm for solving two-sided linear systems in max-algebra. Discrete Applied Math. 154(3), 437–446 (2006)[7] Chatterjee, K., Doyen, L., Henzinger, T.A.: Quantitative languages. ACM Trans. Comput. Log.
11(4) (2010), http://doi.acm.org/10.1145/1805950.1805953[8] Ciric, M., Ignjatovic, J., Damljanovic, N., Basic, M.: Bisimulations for fuzzy automata. Fuzzy Sets
and Systems 186(1), 100–139 (2012)

APPENDIX AOMITTED PROOFS

34[9] Ciric, M., Ignjatovic, J., Jancic, I., Damljanovic, N.: Computation of the greatest simulations and bisimulations between fuzzy automata. Fuzzy Sets and Systems 208, 22–42 (2012),
http://dx.doi.org/10.1016/j.fss.2012.05.006[10] Cı̂rstea, C.: Maximal traces and path-based coalgebraic temporal logics. Theor. Comput. Sci.
412(38), 5025–5042 (2011)[11] Damljanovic, N., Ciric, M., Ignjatovic, J.: Bisimulations for weighted automata over an additively
idempotent semiring. Theor. Comput. Sci. 534, 86–100 (2014)[12] Doyen, L., Henzinger, T.A., Raskin, J.F.: Equivalence of labeled markov chains. Int. J. Found.
Comput. Sci. 19(3), 549–563 (2008)[13] Ehrenfeucht, A., Mycielski, J.: Positional strategies for mean payoff games. International Journalof Game Theory 8(2), 109–113 (1979)[14] Ésik, Z., Maletti, A.: Simulation vs. equivalence. In: Arabnia, H.R., Gravvanis, G.A., Solo, A.M.G.
(eds.) Proceedings of the 2010 International Conference on Foundations of Computer Science, FCS
2010, July 12-15, 2010, Las Vegas, Nevada, USA. pp. 119–124. CSREA Press (2010)[15] Ésik, Z., Maletti, A.: The category of simulations for weighted tree automata. Int. J. Found.
Comput. Sci. 22(8), 1845–1859 (2011)[16] Etessami, K., Wilke, T., Schuller, R.A.: Fair simulation relations, parity games, and state space
reduction for büchi automata. SIAM J. Comput. 34(5), 1159–1175 (2005)[17] The GNU linear programming kit, http://www.gnu.org/software/glpk[18] Hasuo, I.: Generic forward and backward simulations. In: Baier, C., Hermanns, H. (eds.) CONCUR.
Lect. Notes Comp. Sci., vol. 4137, pp. 406–420. Springer (2006)[19] Hasuo, I.: Generic forward and backward simulations II: Probabilistic simulation. In: Gastin,P., Laroussinie, F. (eds.) CONCUR. Lecture Notes in Computer Science, vol. 6269, pp. 447–461.
Springer (2010)[20] Hasuo, I., Jacobs, B.: Context-free languages via coalgebraic trace semantics. In: Fiadeiro, J.L.,
Harman, N., Roggenbach, M., Rutten, J.J.M.M. (eds.) CALCO. Lecture Notes in Computer Science,
vol. 3629, pp. 213–231. Springer (2005)[21] Hasuo, I., Jacobs, B., Sokolova, A.: Generic trace semantics via coinduction. Logical Methods in
Computer Science 3(4) (2007)[22] Hasuo, I., Kawabe, Y., Sakurada, H.: Probabilistic anonymity via coalgebraic simulations. Theor.
Comput. Sci. 411(22-24), 2239–2259 (2010)[23] Hughes, J., Jacobs, B.: Simulations in coalgebra. Theor. Comput. Sci. 327(1-2), 71–108 (2004)[24] Jacobs, B.: Introduction to coalgebra. Towards mathematics of states and observations (2012),
Draft of a book (ver. 2.0), available online[25] Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS. pp.
266–277. IEEE Computer Society (1991)[26] Kerstan, H., König, B.: Coalgebraic trace semantics for continuous probabilistic transition systems.
Logical Methods in Computer Science 9(4) (2013), http://dx.doi.org/10.2168/LMCS-9(4:16)2013[27] Kiefer, S., Murawski, A.S., Ouaknine, J., Wachter, B., Worrell, J.: Language equivalence for probabilistic automata. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV. Lecture Notes in Computer
Science, vol. 6806, pp. 526–540. Springer (2011)[28] Kiefer, S., Murawski, A.S., Ouaknine, J., Wachter, B., Worrell, J.: Algorithmic probabilistic gamesemantics—playing games with automata. Formal Methods in System Design 43(2), 285–312 (2013)[29] Konstantinos, C., Catuscia, P.: Probable innocence revisited. Theoretical Computer Science 367(1),123–138 (2006)[30] Krob, D.: The equality problem for rational series with multiplicities in the tropical semiring is
undecidable. In: Kuich, W. (ed.) ICALP. Lecture Notes in Computer Science, vol. 623, pp. 101–112.
Springer (1992)[31] Lynch, N.A., Vaandrager, F.W.: Forward and backward simulations: I. Untimed systems. Inf.
Comput. 121(2), 214–233 (1995)[32] Mathematica, http://www.wolfram.com/mathematica/[33] Pin, J.E.: Tropical semirings. Idempotency (Bristol, 1994) pp. 50–69 (1998)[34] Power, J., Turi, D.: A coalgebraic foundation for linear time semantics. Electr. Notes Theor. Comput. Sci. 29, 259–274 (1999)[35] Reiter, M.K., Rubin, A.D.: Crowds: Anonymity for web transactions. ACM Trans. Inf. Syst. Secur.
1(1), 66–92 (1998)[36] Sokolova, A.: Coalgebraic Analysis of Probabilistic Systems. Ph.D. thesis, Techn. Univ. Eindhoven(2005)

APPENDIX AOMITTED PROOFS

35[37] Tzeng, W.G.: A polynomial-time algorithm for the equivalence of probabilistic automata. SIAM J.
Comput. 21(2), 216–227 (1992)[38] Urabe, N., Hasuo, I.: Generic forward and backward simulations III: quantitative simulations by matrices. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014.
Proceedings. Lecture Notes in Computer Science, vol. 8704, pp. 451–466. Springer (2014),
http://dx.doi.org/10.1007/978-3-662-44584-6 31[39] Zwick, U., Paterson, M.: The complexity of mean payoff games on graphs. Theor. Comput. Sci.
158(1&2), 343–359 (1996)