Generic Forward and Backward Simulations III:
Quantitative Simulations by Matrices
Natsuki Urabe and Ichiro Hasuo
University of Tokyo, Japan

Abstract. We introduce notions of simulation between semiring-weighted automata as models of quantitative systems. Our simulations are instances of thecategorical/coalgebraic notions previously studied by Hasuo—hence soundness
wrt. language inclusion comes for free—but are concretely presented as matricesthat 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 and max-plus semirings.

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-physical systems—physical quantities like energy consumption are necessarily taken into account.
Semiring-weighted automata It is standard in the concurrency community to modelsuch quantitative systems by state-transition systems in which weights are assigned totheir states and/or transitions. The semantics of such systems varies, however, depending on the interpretation of weights. 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 path and 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
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.
Language inclusion Let A be an S-weighted automaton with labels from an alphabet
Σ. It assigns to each word w ∈ Σ ∗ a weight taken from S—this is much like a (purely)
probabilistic automaton assigns a probability to each word. Let us denote this functionby L(A) : Σ ∗ → S and call it 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.

2

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 andthe other expresses specification; and L(A) v L(B) gives the definition of “the systemmeeting the specification.” 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 most as
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 [26], a quantitative notion of anonymity. See [15].
Simulation Direct check of language inclusion is simply infeasible because there areinfinitely 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 [23]. In the nondeterministic setting, a simulation R is arelation 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 of a simulation implies language inclusion—is called soundness.
Contribution: weighted forward/backward simulations by matrices In this paper
we extend this simulation approach to language inclusion [23] to the quantitative setting of semiring-weighted automata. Our notions of (forward and backward) weighted
simulation are not given by relations, but by matrices with entries from a semiring S.
Use of matrices in automata theory is classic—in fact our framework instantiates
to that in [23] 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 theoryof coalgebraic simulations [11, 12, 14]. There various systems are identified with acategorical construct of coalgebras in a Kleisli category; and fwd./bwd. 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 thatsatisfies 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 that is waiting to be applied. For example linear programming (LP) canbe exploited for the plus-times semiring for probabilities; and there are algorithms proposed for other semirings 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 findinga fwd. or bwd. simulation from A to B. Soundness of simulations follows from thegeneral result in [11]. A simulation we seek for is a matrix subject to certain linear

3

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 tolanguage 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.
Organization of the paper In §2 we define semiring-weighted automata, characterizethem in coalgebraic terms and recap the coalgebraic theory in [11]. These are combined
to yield the notion of simulation matrix in §3. In §4 partial execution transformationsof automata are described and proved correct. The framework obtained so far is applied to the plus-times and max-plus semirings, in §5 and §6, respectively. There ourproof-of-concept implementations (the code is found at the first author’s webpage) andrelationship to other known simulation notions are discussed, too. In §7 we conclude.

2

Preliminaries

We review the generic theory of traces and simulations in [11, 14] that is based on(T, F )-systems, which will eventually lead to the notion of simulation matrix in §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 [11, 14], we impose the following properties.
Definition 2.1 A commutative cppo-semiring is a tuple S = (S, +S , 0S , ×S , 1S , v)that satisfies 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 comm. 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 comm. cppo-semiring, where + and × are usual addition
and multiplication of real numbers. This is the semiring that we will use for modeling 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 [24]—is also a comm. cppo-semiring. Here a number r ∈[−∞, ∞] can be understood as (best-case) profit: they are summed up along a path,4

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 given by−∞; 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.
Definition 2.3 (S-weighted automaton, weighted language) Let S = (S, +S , 0S , ×S ,1S , v) be a comm. 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 ∈ Σ, an initial row vector α ∈ S Q and a final column vector β ∈ S Q .
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 [11, 14].
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 [17] in the sense that c is so-called a T F -coalgebra. In thedefinition we have two parameters T and F . Let us forget about their categorical structures (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”
non-deterministic
probabilistic
S-weighted

F
1+Σ×( )
(Σ + ( ))∗“linear-time behavior”a→ X or → (where a ∈ Σ)
words over terminals (a ∈ Σ)
& nonterminals, suited for CFG [13]5

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}
Here supp(f ) = {x ∈ X | f (x) 6= 0S }. Countable support in MS is a technicalrequirement so that composition of Kleisli arrows is well-defined (Def. 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), anda(a, x0 ) ∈ c(x) means there is a transition x → x0 . Overall, a (P, 1 + Σ × ( ))-system
is nothing but a nondeterministic 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 comm. cppo-semiring.
There is a bijective correspondence
between: 1) S-weighted automata (Def. 2.3); and2) MS , 1 + Σ × ( ) -systems whose state spaces are at most countably 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
by sA (•)(x) = αx ; and cA : Q → MS (1 + Σ × Q) is given by cA (x)(X) = βx andcA (x)(a, y) = M (a)x,y .
tu
2.3

Coalgebraic Theory of Traces and Simulations

We review the theory of traces and simulations in [11, 14] that is based on (T, F )systems. In presentation we restrict to T = MS and F = 1 + Σ × ( ) for simplicity.
Kleisli Arrows One notable success of coalgebra was a uniform characterization, in
terms of the same categorical diagram, of bisimulations for various kinds of systems(nondeterministic, probabilistic, etc.) [17]. This works quite well for branching-timeprocess semantics. For linear-time semantics—i.e. trace semantics—it is noticed in [25]that so-called a Kleisli category, in place of the category Sets, gives a suitable basecategory for coalgebraic treatment. This idea—replacing functions X → Y with Kleislip Y and drawing the same diagrams—led to the development in [11, 12,arrows X →14] of an extensive theory of traces and simulations. The notion of Kleisli arrow is
p T Y (or simply X →p Y ) is definedparametrized by a monad T : a T -Kleisli arrow X →to be a function X → T Y , hence represents a “T -branching function from X to Y .”We restrict to T = MS for simplicity of presentation. An MS -Kleisli arrow
p Y below is “an S-weighted function from X to Y .” In particular, for each
f: X →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.

6

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 Prop. 2.6 we characterized an S-weighted automaton A in coalgebraic terms.
Using Kleisli arrows it is presented as a triplep Q, cA : Q −→p 1+Σ×Q .
XA = Q, sA : {•} −→(3)
Generic Trace Semantics In [14], for monads T with a suitable order, a final coalgebrain 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 the current work is the fact that the weighted language
L(A) in (1) is an instance of this generic trace semantics, as we will show in Thm. 2.10.
We shall state the results in [14] on coalge1+Σ×(tr(c))
/ 1 + Σ × Σ∗
braic traces, restricting again to T = MS and 1 + ΣO × X
O_c=final _ J([nil,cons]−1 )F = 1 + Σ × ( ) for simplicity. In the di
/ Σ∗
XO
9
agram (4) on the right, composition of Kleisli
tr(c)
_s
(4)
( tr(X )arrows are given byin Def. 2.7; J on the{•}right is the lifting in Def. 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 found in Def. A.4.
Theorem 2.8 (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 squarec: X→
in the diagram (4) commute.
tu
Definition 2.9 (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 →Thm. 2.8. 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.10 (weighted language as trace semantics) Let A be an S-weighted aup
tomaton. 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).
tu
In the last theorem we need that Σ ∗ is countable; this is why we assumed that Σ isp Σ∗.
countable in Def. 2.3. Henceforth we do not distinguish L(A) and tr(XA ) : {•}→

7

Forward and Backward Kleisli simulations In [11], the classic results in [23] on forward and backward simulations—for (nondeterministic) labeled transition systems—
are generalized to (T, F )-systems. Specifically, fwd./bwd. simulations are characterized
as lax/oplax coalgebra homomorphisms in a Kleisli category; and soundness—their existence witnesses trace inclusion—is proved once for all in a general categorical setting.
As before, we present those notions and results in [11] restricting to T = MS and
F = 1 + Σ × ( ). If T = P and F = 1 + Σ × ( ) they instantiate to the results in [23].
Definition 2.11 (Kleisli simulation) Let X = (X, s, c) and Y = (Y, t, d) be (MS , 1+
Σ × ( ))-systems (cf. Def. 2.5, Prop. 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 Fig. 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; afwd. simulation f from X to Z; and a bwd. simulation b from Z to Y.
4. A backward-forward simulation from X to Y consists of: a (T, F )-system Z; abwd. simulation b from X to Z; and a fwd. simulation f from Z to Y.


o
FX
O

Ff
v

FY
O

s

v

t

_c
XO o

 f

{•}
fwd. sim.

_d
YO

F b
/ F Y F X o F  f F Z F b / F Y F X F b / F Z o F f F Y_c v_O d _O c v _O e v _O d _O c v _O e v _O d
 f Z b  /Y /Zo  f Y
/
XO b
YO
XO o
XO b
O
O
_O
_O

FX
O
s

v

{•}
bwd. sim.

t

s

v

u

v

{•}
fwd.-bwd. sim.

t

s

v

u

v

t

{•}
bwd.-fwd. sim.

Fig. 1. Kleisli simulations (here F = 1 + Σ × ( ))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 [11].
Theorem 2.12 (soundness) Let X and Y be (MS , 1 + Σ × ( ))-systems. Each of thep Σ ∗ (cf. Def. 2.9).
following yields tr(X ) v tr(Y) : {•}→
1. X vF Y
2. X vB Y
3. X vFB Y
4. X vBF Ytu
Theorem 2.13 (completeness) The converse of soundness holds for backward-forward
simulations. That is: tr(X ) v tr(Y) implies X vBF Y .
tu

3Simulation Matrices for Semiring-Weighted Automata

In this section we fix parameters T = MS and F = 1 + Σ × ( ) in the generic theoryin §2.3 and rephrase the coalgebraic framework in terms of matrices (whose entries aretaken 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 (Def. 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).

8

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.
t
u
f

1+Σ×f

p B to 1 + Σ × A −→p
The correspondence from A −→1 + Σ × B—used in (4) andin Fig. 1—can be described using matrices, too. Details are in Appendix A.2.
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:

X⊕Y =

X
O

O
Y

!
,

.
.
.







· · · xi,j · · · ⊗ Y




.
.
.

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





· · · .
tuThis 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 Lem. 3.2–3.3, we can present Kleisli simulations (Def. 2.11) as matrices.
Recall that a state space of a weighted automaton is assumed to be countable (Def. 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 Fig. 1 into matrices, and thenbreaking them up into smaller matrices using Lem. 3.3. It is notable that the requirements 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 [2, 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 Fig. 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.
tu
In what follows we write vF , vB also between S-weighted automata. Thm. 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.

9

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.12

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

L(A) v L(B) .

tu

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 [23].
Remark 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 fwd.
simulation matrix from A to B, then tX is a bwd. simulation matrix from tA to tB.

4

Forward and Backward Partial Execution

We have four different notions of simulation (Def. 2.11): fwd., bwd., fwd.-bwd., andbwd.-fwd. Our view on these is as (possibly finitary) witnesses of language inclusion.
The combined ones (fwd.-bwd. and bwd.-fwd.) subsume the one-direction ones
(fwd. and bwd.)—simply take the identity arrow as one of the two simulations required.
Moreover, bwd.-fwd. is complete (Thm. 2.13). 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 Def. 2.11). Furthermore, since language inclusion for finite S+,× -weighted automata—models of probabilistic systems—
is known to be undecidable [5], existence of a bwd.-fwd. simulation is undecidable too.
Therefore in what follows we focus on the one-directional (i.e. fwd. or bwd.) simulations as proof methods for language inclusion. They have convenient matrix presentations, too, as we saw in §3. However fwd. or bwd. simulations are not necessarily
complete, by a counterexample (Example A.1) or by complexity arguments (§5.1).
In this section we introduce for semiring-weighted automata their transformations—called forward and backward partial execution—that increase the number of fwd./bwd.
simulation matrices. We also prove some correctness results.
Definition 4.1 (FPE, BPE) Forward partial execution (FPE) is a transformation of aweighted automaton that “replaces some states with their forward one-step behaviors.”
Concretely, given an S-weighted automaton A = (Q, Σ, M, α, β) and a parameterP ⊆ 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 x ∈ P with its forward one-step behaviors—X or (a, y)—as new states.
The other data M 0 , α0 , β 0 are suitably defined following the above intuition; see Appendix A.3. Possible patterns of transformations are illustrated in Fig. 2.
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
Q0 = • ∃x ∈ P. αx 6= 0S + (a, y) ∃x ∈ P. M (a)y,x 6= 0S + (Q \ P ) ,10areplacing each p ∈ P with its backward one-step behaviors—(a, y) with y → x, and •if x is initial—as new states. M 0 , α0 , β 0 are defined in Appendix A.3. See also Fig. 2.
◦_
◦?
◦O
◦O
◦? _ a,r2◦OO
a,r1
a1 ,p1
a2 ,p2a,1S
a2 ,p2r 
a1 ,p1


/
/
/
•O
◦_
◦?
•O
•O
◦? _
•O
b,p

◦

b,p

◦

b1 ,q1b,p

b2 ,q2◦◦“split backward”◦Ob,p
a1 ,p1

◦

•? _

b,p


a2 ,p2

◦

/ ◦O
◦

◦

◦

b2 ,
q2 ·r2“merge backward”◦? _a1 ,p1“split forward”

b1 ,
q1 ·r1b,p◦O◦

a2 ,p2•_a,r1

b2 ,q2◦•?

 q1 ·r1 /a,r2“merge forward”◦“eliminate dead end”

Forward Partial Execution◦O◦O
b1 , ◦_
b1 ,q1

c,s

◦

◦?
◦O
a,1S

◦

◦O

b2 ,
q2 ·r2

◦


•O

c,s

/

r
“eliminate dead end”

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

Roughly speaking, FPE replaces a concrete state p ∈ P with an abstract state, suchas (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.
The use of FPE/BPE is as follows: we aim to goal: L(A) v L(B) A B
establish L(A) v L(B); depending on whether weby vF
FPE BPEsearch for a forward or backward simulation matrix,
by vB
BPE FPE
we apply one of FPE and BPE to each of A and B, according to the above table.
We shall now state correctness properties of this strategy; proofs are in Appendix A.4.
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.2 (soundness of FPE/BPE) Let P, P 0 be arbitrary subsets. Each of the following implies L(A) v L(B).
1. AFPE,P vF BBPE,P 0
2. ABPE,P vB BFPE,P 0tu
Theorem 4.3 (adequacy of FPE/BPE) Let P, P 0 be arbitrary subsets. We have:
1. A vF B ⇒ AFPE,P vF BBPE,P 0
2. A vB B ⇒ ABPE,P vB BFPE,P 0 .
tu
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 whichslows down search for a simulation, resulting in a trade-off situation.
Proposition 4.4 (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 .

tu

In fact we have a coalgebraic characterization of FPE, too, as a partial applicationof the functor 1 + Σ × ( ). This characterization generalizes to a large class of (T, F )systems, and the above correctness results can be proved generally by categorical arguments. See Appendix A.5 for details. Capturing BPE categorically is still open—it
seems that BPE exists somewhat coincidentally, for the specific functor F = 1+Σ×( )for which an opposite automaton is canonically defined (cf. Rem. 3.7).

11

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, 22], language inclusion is not semidecidable either.
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 Example A.2.

5

Simulation Matrices for Probabilistic Systems by S = S+,×In §5 we focus on S+,× -weighted automata which we identify as (purely) probabilistic
automata (cf. Example 2.2). In §5.1 our method by simulation matrices is comparedwith other notions of probabilistic simulation; in §5.2 we discuss our implementation.
5.1

Other Simulation Notions for Probabilistic Systems
lang. incl.

vFB

Various simulation notions have been
Example
×
×
[12]
A.1
introduced for probabilistic systems, eiv
JLther as a behavioral order by itself or asvF or vB
vHJ
a proof method for language inclusion.
(i.e. by sim. matrices)
Jonsson and Larsen’s one [18] (denoted by vJL ) is well-known; it is shown in [12] tobe a special case of Hughes and Jacobs’ coalgebraic notion of simulation [16] (vHJ ),which in turn is a special case of fwd.-bwd. (Kleisli) simulation (vFB , Def. 2.11).
Comparison of all these notions (observed in [12]) is as depicted above; it follows fromThm. 2.12 that all these simulation notions are sound with respect to language inclusion.
We note that language inclusion between finite S+,× -weighted automata is undecidable [5] while language equivalence can be determined in polynomial time [19]. The
former result can account for the fact that there seem to be not many proof methods
for probabilistic/quantitative language inclusion. For example, probabilistic simulationin [3] is possibilistic simulation between systems with both probabilistic and nondeterministic 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 Def. 3.4 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 (Example A.3) and they are still sound.
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 Def. 3.4 into a single linear inequality
Ax ≤ b and solves it with a linear programming solver glpk [1]. We note thatthe matrix A is sparse, having n + anm + m rows, nm columns and at most
2nm + a(n2 m + nm2 ) non-zero entries.

12– The program +×-PE (implemented in OCaml) takes an automaton A and d ∈ N as
input, and returns AFPE,P (or ABPE,P , by choice) where 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 given automata, for d = 1, 2, . . . , each timeincrementing the parameter d for +×-PE . The experiments were on an Ubuntu Linux
laptop with a Core i5 2.53 GHz processor (4 cores) and 4 GB RAM.
Grades Protocol The grades protocol is introduced in [19] and is used there as abenchmark: the protocol and its specification are expressed as probabilistic programs
P and S; they are then translated into (purely) probabilistic automata AP and AS by agame semantics-based tool APEX [20]. By establishing L(AP ) = L(AS ), the protocol is shown to exhibit the same behaviors as the specification—hence is verified. The
protocol has two parameters G and S.
In our experiment we proved L(AP ) = param. AP
ASdirection, time space
L(AS ) by establishing two-way language G S #st. #tr. #st. #tr. |Σ| fwd./bwd. (sec) (GB)APvFAS 1.77 1.21
inclusion (v and w). The results are shown 2 8 578 1522 130 642 11 A
PwBAS 1.72 1.22
in Table. 1. For all the choices of param- 2 10 1102 2982 202 1202 13 APvFAS 9.42 4.05
PwBAS 9.25 4.09
eters G and S, our program +×-sim was 2 12 1874 5162 290 2018 15 A
APvFAS 38.60 11.51
able to establish, without applying +×APwBAS 38.34 11.63
PE : AP vF AS (but not vB ) for the v 3 8 1923 7107 243 2163 20 APvFAS 44.43 12.26
APwBAS 44.11 12.64
direction; and AP wB AS (but not wF ) 4 6 1636 7468 196 1924 23 APvFAS 30.28 10.39
APwBAS 29.94 10.49
for the w direction. In the table, #st. and#tr. denote the numbers of states and tranTable 1. Results for the grades protocol [19]sitions, respectively, and |Σ| is the size ofthe alphabet. All these numbers are determined by APEX .
The table indicates that space is a bigger problem for our approach than time.
In [19] four algorithms for checking language equivalence between S+,× -weighted
automata are implemented and compared: two are deterministic [9, 27] and the othertwo are randomized [19]. 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. Note however that our algorithm is for language inclusion—an undecidable
problem, unlike language equivalence that is in P, see §5.1—and hence is more general.
Crowds Protocol Our second exper- param. AP
ASdirection time space diment calls for checking language in- n c pf #st. #tr. #st. #tr. |Σ| fwd./bwd. (sec) (GB)9APvFAS 52.48 0.01 2
clusion, making the algorithms studied 5 1 10 7 44 7 56 18 A
0.01 0.01 2
PvBAS
in [19] unapplicable. We verified some 7 1 34 9 88 9 118 26 APvFAS 0.15 0.03 2
APvBAS 0.02 0.01 2
instances of the Crowds protocol [26]
10 2 45 12 224 12 280 54 APvFAS 802.47 0.35 2
against a quantitative anonymity speciAPvBAS 0.05 0.03 2
2
fication called probable innocence [21]. 20 6 45 22 1514 22 1696 238 APvFAS T/O
A v A
1.32 0.78 2
We used a general trace-based verifi- 30 6 4 32 4732 32 5112 550 APPvBFASS S/F
5
APvBAS 11.84 5.99 2
cation method in [15] for probable innocence: language inclusion L(AP ) v
Table 2. Results for the Crowds protocol
L(AS ), from the model AP of a protocol in question to AP ’s suitable modification AS , guarantees probable innocence.

13

The Crowds protocol has parameters n, c and pf . In fact, for this specific protocol, apf
sufficient condition for probable innocence is known [26] (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 (§4) was applied.
The entry “S/F” designates that +×-PE was killed because of segmentation fault
caused by 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 fwd./bwd. 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 §6 we discuss Smax,+ -weighted automata, in which weights are understood as (bestcase) 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 fwd. simulation matrix. This observation is in §6.1; in §6.2 our implementation is presented.
6.1 G-Simulation by Forward Simulation Matrices
In this section we restrict to finite-state automata, in which case we can also disposeof the weight ∞. What we shall call G-simulation is introduced in [7], and its soundness with respect to weighted languages over infinite-length words Σ ω → [−∞, ∞) isproved there. Here we adapt their definition to the current setting of finite-length words.
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 isplayed by two players called Challenger and Simulator: a strategy for Challenger is apair (ρ1 : 1 → QA , τ1 : (QA × QB )+ → 1 + Σ × QA ) of functions; a strategy for
Simulator is a pair (ρ2 : QA → QB , τ2 : (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 , ρ2 (p0 ) =q0 and τ1 ((p0 , q0 ) . . . (pn , qn )) = X.
– τ1 (p0 , q0 ) . . . (pi , qi ) = (ai+1 , pi+1 ) and τ2 (p0 , q0 ) . . . (pi , qi ), (ai+1 , pi+1 ) =qi+1 , for each i ∈ [0, n − 1].
A strategy (ρ1 , τ1 ) for Challenger is winning if for any strategy (ρ2 , τ2 ) for Simulator,
their outcome (r1 , r2 ) satisfies L(A)(r1 ) > L(B)(r2 ). Here the weight L(A)(r) of arun r is defined in the obvious way.
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.
t
u

14

The extra assumption can be easily enforced by eliminating trap states through backward reachability check. This does not change the (finite) weighted language.
Now the situation is as shown on the right. It folks Thm. 6.2 +3 A vF B
lows from [7] that the question if A vG B holds or A vG B
By def. 
not is reduced to a mean payoff game [10], whose de [7]payoff ks [2] +3 linear inequalities
cision problem is in NP ∩ co-NP and has a pseudo mean
gameover Smax,+polynomial-time algorithm [28]. Moreover it is known
that the decision problem of mean payoff games is equivalent to the feasibility problemof linear inequalities over Smax,+ [2]. For the latter an algorithm is proposed in [6] thatis shown in [4] to be superpolynomial.
Similarly to S+,× -weighted automata, language inclusion between Smax,+ -weighted
automata is known to be undecidable [22]. We note that, by Thm. 6.2, applying FPE or
BPE (§4) increases the likelihood of vG in the sense of Thm. 4.3. We additionally note
that, by exploiting symmetry of fwd. and bwd. simulation matrices (Rem. 3.7), we candefine “backward G-simulation” as a variation of Def. 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 thathave known algorithms. Since we did not find actual software available, we implemented (in C++) the algorithm in [6] as the program max+-sim . It transforms theconstraints in Def. 3.4 into an inequality Ax ≤ Bx, which in turn is made into alinear equality A0 x0 = B 0 x0 by adding slack variables. The last equality is solvedby the algorithm in [6].
– max+-PE is as in §5. It simply uses the whole state space as the parameter P .
Experiments were done on an Ubuntu Linux laptop with a Core 2 duo processor(1.40 GHz, 2 cores) and 2 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 forexperiments with 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 Fig. 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 ischosen 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(§5.2). Somehow unexpectedly, there is no big performance gap between the sparse case(p = 0.1) and the dense case (p = 0.9); in fact the sparse case consumes slightly more

15

memory. Consumption of both time and space grows faster than linearly, which posesa question about the scalability of our approach. That said, our current implementationof 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 our approach thata simulation problem is reduced to linear inequality constraints, a subject of extensive
research efforts (cf. §5.1 and §6.1).
time consumption (s)

4000
3500
3000

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

2500
2000
1500
1000
500
0
30 40 50 60 70 80 90 100 110 120 130
the number of states

max space consumption (MB)

4500

20

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

15
10
5
0
30 40 50 60 70 80 90 100 110 120 130
the number of states

Fig. 3. Time and max space consumption for max+-sim

7

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.
There are some directions in which the current matrix-based simulation framework
can be further generalized. Generalizing F from 1 + Σ × ( ) to any polynomial functor
is mostly straightforward, as we noted after Lem. 3.3. We have not done that mainly forthe space reason. Generalizing T from MS (for semiring-weighted branching) to others
seems more challenging. For example, in [7] weights can be given from an algebraic
structure S in which an additive unit 0S does not satisfy 0S ×S x = 0S . In this case
operations like matrix multiplication becomes hard to define.
Another direction is to incorporate infinite traces, which is done in [7]. In fact ourcurrent coalgebraic backend [11] fails to do so; the work [8] will be useful here. Finally,further optimization of our implementation is obvious future work.
Acknowledgments Thanks are due to Shota Nakagawa and the anonymous referees
for useful discussions and comments. The authors are supported by Grants-in-Aid forYoung Scientists (A) No. 24680001, JSPS.

References
1. The GNU linear programming kit, http://www.gnu.org/software/glpk
2. Akian, M., Gaubert, S., Guterman, A.E.: Tropical polyhedra are equivalent to mean payoff
games. International Journal of Algebra and Computation 22(1) (2012)
3. Baier, C., Hermanns, H., Katoen, J.P.: Probabilistic weak simulation is decidable in polynomial time. Inf. Process. Lett. 89(3), 123–130 (2004)
4. Bezem, M., Nieuwenhuis, R., Rodrı́guez-Carbonell, E.: Exponential behaviour of the
butkovic-zimmermann algorithm for solving two-sided linear systems in max-algebra. Discrete Applied Mathematics 156(18), 3506–3509 (2008)

16
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.: Expressiveness and closure properties for quantitative languages. Logical Methods in Computer Science 6(3) (2010)
8. Cı̂rstea, C.: Maximal traces and path-based coalgebraic temporal logics. Theor. Comput. Sci.
412(38), 5025–5042 (2011)
9. Doyen, L., Henzinger, T.A., Raskin, J.F.: Equivalence of labeled markov chains. Int. J.
Found. Comput. Sci. 19(3), 549–563 (2008)
10. Ehrenfeucht, A., Mycielski, J.: Positional strategies for mean payoff games. International
Journal of Game Theory 8(2), 109–113 (1979)
11. 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)
12. Hasuo, I.: Generic forward and backward simulations II: Probabilistic simulation. In: Gastin,P., Laroussinie, F. (eds.) CONCUR. LNCS, vol. 6269, pp. 447–461. Springer (2010)
13. 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)
14. Hasuo, I., Jacobs, B., Sokolova, A.: Generic trace semantics via coinduction. Logical Methods in Computer Science 3(4) (2007)
15. Hasuo, I., Kawabe, Y., Sakurada, H.: Probabilistic anonymity via coalgebraic simulations.
Theor. Comput. Sci. 411(22-24), 2239–2259 (2010)
16. Hughes, J., Jacobs, B.: Simulations in coalgebra. Theor. Comput. Sci. 327(1-2), 71–108(2004)
17. Jacobs, B.: Introduction to coalgebra. Towards mathematics of states and observations(2012), Draft of a book (ver. 2.0), available online
18. Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS.
pp. 266–277. IEEE Computer Society (1991)
19. 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)
20. Kiefer, S., Murawski, A.S., Ouaknine, J., Wachter, B., Worrell, J.: Algorithmic probabilistic
game semantics—playing games with automata. Formal Methods in System Design 43(2),285–312 (2013)
21. Konstantinos, C., Catuscia, P.: Probable innocence revisited. Theoretical Computer Science367(1), 123–138 (2006)
22. 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)
23. Lynch, N.A., Vaandrager, F.W.: Forward and backward simulations: I. Untimed systems. Inf.
Comput. 121(2), 214–233 (1995)
24. Pin, J.E.: Tropical semirings. Idempotency (Bristol, 1994) pp. 50–69 (1998)
25. Power, J., Turi, D.: A coalgebraic foundation for linear time semantics. Electr. Notes Theor.
Comput. Sci. 29, 259–274 (1999)
26. Reiter, M.K., Rubin, A.D.: Crowds: Anonymity for web transactions. ACM Trans. Inf. Syst.
Secur. 1(1), 66–92 (1998)
27. Tzeng, W.G.: A polynomial-time algorithm for the equivalence of probabilistic automata.
SIAM J. Comput. 21(2), 216–227 (1992)
28. Zwick, U., Paterson, M.: The complexity of mean payoff games on graphs. Theor. Comput.
Sci. 158(1&2), 343–359 (1996)

17

A

Appendix

A.1

Examples and Counterexamples

Example A.1 The following S+,× -weighted automata exhibit L(A) v L(B), but there
is no forward or backward simulation from A to B—as is shown by the fact that there
is no X that satisfies the requirements in Def. 3.4. Hence this pair is a counterexample
for the completeness of vF and that of vB . In contrast, there exists a simulation by
Jonsson and Larsen [18] between them.
A
a, 12

? x1_

? x0


a, 12


x
? 3

a, 12

b, 12

? y1

B
a,1
1
2

/X

a,1



? y0

a,1

a, 12
b, 12



x2


y2

y3
?

1
2

/X

a,1

Language inclusion (in fact language equivalence) is shown as follows. For eachword w ∈ Σ ∗ ,
(

1 1 n
(w = aaa2n or baa2n )4
2
L(A)(w) = L(B)(w) =0(otherwise) .
Example A.2 The following S+,× -weighted automata exhibit L(A) v L(B), but aforward simulation does not exist no matter how many times FPE is applied to A.
XO

A

B
◦o

1
2

◦! O

a, 12

a,1
a, 14

E Y
X

3
4

3
4

◦/ T

a,1
◦O o
◦/
a, 14

a,1

◦E

2
3

1

◦

◦

1
3

Example A.3 The following S+,× -weighted automata exhibit L(A) v L(B). Neither
forward nor backward Kleisli simulation exists between them if we represent them as(D, 1+Σ×( ))-systems while both can be found if we represent as (MS , 1+Σ×( ))systems.
a, 38

A
X

ui

xO 1

1
8

a, 28
2
8





B
a, 48

x
E 0e
a, 18

Xo

3
8

9 y0 g

a, 58

18


The only X satisfying the inequalities in Def.
3.4.1 is X = 1 1 , and the only X 1satisfying the inequalities in Def. 3.4.2 is X =.
2
A.2

Action of 1 + Σ × ( ) on Kleisli arrows

We have used an operation 1 + Σ × ( ) acting on Kleisli arrows. It is defined as thefunctor 1+Σ ×( ) on Sets lifted to the Kleisli category K`(MS ); see [14] for details.
Here we describe it in concrete terms.
p Y , its lifting 1 + Σ × f : 1 + Σ × X →pDefinition A.4 For a Kleisli arrow f : X →1 + Σ × Y is defined as follows:((
1S (t = ∗)f (x)(y) (t = (a, y))(1+Σ×f )(∗)(t) =(1+Σ×f )(a, x)(t) =0S (otherwise)
0S(otherwise)
Lem. 3.3 follows immediately from this concrete description.
A.3

Formal Definitions of Forward/Backward Partial Execution

We formally describe Def. 4.1.
Definition A.5 (FPE, BPE) Forward partial execution (FPE) is a transformation of aweighted automaton that “replaces some states with their one-step behaviors.” Precisely,
given an S-weighted automaton A = (Q, Σ, M, α, β) and a parameter P ⊆ Q, theresulting 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 ) ,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.
00
M 0 (a)(a,x),X = βx
M 0 (a)(a,x),x = 1S
 M (a)0 (a,x),(a0 ,y) = M (a )x,y 00
M (a)x,X = M (a)β x
M (a)x,(a0 ,y) = (M (a)M (a ))x,y
M 0 (a)x,y = M (a)x,y
M (a)u,v = 0S (otherwise)
0
αX
= αβ
0
βX
= 1S

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

αx0 = αxβ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
Q0 =




• ∃x ∈ P. αx 6= 0S + (a, y) ∃x ∈ P. M (a)y,x 6= 0S + (Q \ P ) ,19areplacing each p ∈ P with its backward one-step behaviors—(a, q) with q → p, and •if p is initial—as new states. The definitions of M 0 , α0 , β 0 are as follows.
00
M 0 (a)•,(a,y) = βyM 0 (a)x,(a,x) = 1S
 M (a)0 (a0 ,x),(a,y) = M (a )0 x,y0
M (a)(a0 ,x),y = (M (a )M (a))x,y
M (a)•,y = αM (a) y0
M (a)x,y = M (a)x,y
M (a)u,v = 0S (otherwise)α•0 = 1Sβ•0 = αβA.4

α(a,x) = 0S

αx0 = αx

0β(a,x)= (M (a)β)xβx0 = βx

Correctness of Forward/Backward Partial Execution

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

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 = βx (x ∈ P ),Xx,x = 1S (x ∈/ P ),

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

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

tuProof of Thm. 4.2 1. From Prop. A.6.1, A vB AFPE,P vF BBPE,P 0 vB B. Hencefrom Cor. 3.6, L(A) v L(AFPE,P ) v L(BBPE,P 0 ) v L(B) holds.
The item 2. can be proved similarly.
tu0
Proof of Thm. 4.3 1. From Prop. A.6.2, AFPE,P vF A vF
o F f F X 0 o F f F Y
OB vF BBPE,P 0 . Because vF satisfies transitivity rule (see the F_X_O c0 v_O dcv
diagram on the right where F = 1 + Σ × ( )), this implies X o  f 0 X o  f YOtOs Ov s0 _
v
AFPE,P vF BBPE,P 0 .
{•}The item 2 can be proved similarly.
t
u

A.5

Categorical Forward Partial Execution

Here we describe FPE in §4 in categorical terms of (T, F )-systems, and prove its correctness results (namely soundness and adequacy) in this general setting.
Definition A.7 Forward partial execution (FPE) for (T, F )-systems is a transformationthat takes a (T, F )-system X = (X, s, c) and a parameter X1 ⊆ X as inputs andreturns a (T, F )-system XFPE,X1 = (F (X) + X2 , (c1 + id) s, F (c1 + id) [id, c2 ]).
(X = X1 + X2 , c1 = c κ1 , and c2 = c κ2 where κ1 and κ2 are injections.
Moreover, F : K`(T ) → K`(T ) is a lifted functor of F : Sets → Sets (see [17] forconcrete definition) ).
Lem A.8, Thm. A.9, Thm. A.10, and Prop. A.11 are categorical analogies of Lem. A.6,
Thm. 4.2, Thm. 4.3, and Prop. 4.4 respectively.

20

Proposition A.8 For each subset X1 , we have the following.
1. X vB XFPE,X1 .
2. XFPE,X1 vF X .
p F (X) + X2 as g = c1 + id. Then,
Proof. 1. We define g : X1 + X2 →
F (g)

g

c = F (c1 + id)[c1 , c2 ]= F (c1 + id)[id, c2 ]= (F (c1 + id)[id, c2 ])s = (c1 + id)

X1
+
F
X
M P 2

! c 1id(c1 + id)
g

c1 \

b c2

s.
X1
+
X2

c 1

!
/F (X)
O
+
F
/XO 2
c1 _
!
X1 id _+FF R X2id N/F (X) f c2
+
id
/X2

Hence g is a backward simulation from X to XFPE .
The item 2. can be proved similarly (g in the proof of the item 1. is also a forward
simulation from XFPE to X ).
tu
Theorem A.9 (soundness of FPE, categorically) Let X1 , Y1 be arbitrary subsets. Eachof the following implies tr(X ) v tr(Y).
1. AFPE,X1 vF Y
2. A vB BFPE,Y1tu
Theorem A.10 (adequacy of FPE, categorically) Let X1 , Y1 be arbitrary subsets. We
have:
1. X vF Y ⇒ XFPE,X1 vF Y
2. X vB Y ⇒ X vB BFPE,Y1 .
tu
Proposition A.11 (monotonicity, categorically) 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 . tu
A.6

Proof of Thm. 6.2

Before proving Thm.6.2, we review the notions of Limavg automaton [7] and mean
payoff game [10], which is used in the proof of Thm. 6.2.
Definition A.12 A Limavg automaton ALimavg = (Q, Σ, M, q0 ) consists of a finite
state space Q, a finite alphabet Σ, transition matrices M : Σ → [−∞, ∞)Q×Q , and theωLimavginitial state q0 ∈ Q. For an infinite word w = a0 aP
assigns a value
1 ··· ∈ Σ , A
N
1LimavgL(A)(w) := supq1 q2 ···∈Q∞ liminf N →∞ N i=0 M (ai )qi ,qi+1
G-simulation for Limavg automaton can be defined similarly as Def. 6.1.
Definition A.13 A mean payoff game is a game played by two players Min and Max
on a parity graph G = (QMin , QMax , qI , E, γ) consisting of states of Min QMin , statesof Max QMax , the initial state qI ∈ QMin , edges E = QMin × QMax + QMax × QMin ,and a weight function γ : E → R. A strategy for Min and Max are functions τMin :(QMin × QMax )∗ × QMin → QMax and τMax : (QMin × QMax )+ → QMin respectively. An infinite run p0 q0 p1 q1 . . . on G is the outcome of τMin and τMax if p0 = qI ,p0 , p1 , · · · ∈ QMin , q0 , q1 , · · · ∈ QMax , and for any i ≥ 1, τMin (p0 q0 . . . qi−1 pi ) = qiand τMin (p0 q0 . . . pi qi ) = pi+1 . A strategy τMax for Max is winning if for any strategy

PN
τMin for Min, their outcome r0 r1 r2 r3 . . . satisfies liminf N →∞ N1 i=0 γ(ri , ri+1 ) ≥0.

21Using these notions, Thm. 6.2 is derived as follows.
1. There exists a linear inequality Ax ≤ Bx in Smax,+ such that forward Kleisli
simulation from A to B exists if and only if Ax ≤ Bx has a non-trivial (i.e.
x 6= −∞) solution.
2. ([2]) There exists a mean payoff game MP such that existence of a non-trivial
solution in Ax ≤ Bx is equivalent to the existence of winning strategy for Max inMP.
3. There exists a Limavg automaton ALimavg and B Limavg such that G-simulation from
A to B exists if and only if G-simulation from ALimavg to B Limavg exits.
4. ([7]) G-simulation from ALimavg to B Limavg exists if and only if there exists a winning strategy for Max in MP.
Proof of Thm. 6.2 Let A = (QA , Σ, MA , αA , βA ) and B = (QB , Σ, MB , αB , βB ).
1 : By definition, forward simulation matrix is a matrix X that satisfies below:
αA ≤ αB X ∧ ∀a ∈ Σ. XMA (a) ≤ MB (a)X ∧ XβA ≤ βB .

(6)Adding a new variable x?,? , such X exists iff there exist non-trivial X 0 and z satisfying
αA + x?,? ≤ αB X 0 ∧ ∀a ∈ Σ. X 0 MA (a) ≤ MB (a)X 0 ∧ X 0 βA ≤ βB + x?,? . (7)(Only if part is easy. Assume non-trivial X 0 and z satisfying (7) exist. If x?,? 6= −∞,then X = X 0 − x?,? satisfies (6). If x?,? = −∞, by the assumption that A has no trap
state, all entries of X 0 are −∞, hence X 0 and x?,? are trivial solution. This contradicts.)
2 : From [2] and that x?,? 6= −∞ if (7) has a non-trivial solution, a non-trivial solutionof (7) exists if and only if there is a winning strategy for player Max in a mean payoff
game played on a graph G = (QMin , QMax , qI , E, γ) such that
QMin = {x?,? } + {xj,i | j ∈ QB , i ∈ QA } ,QMax = QA + Σ × QB × QA + QB ,qI = x?,?
E = E1 + E2 s.t. E1 ⊆ QMin × QMax , E2 ⊆ QMax × QMin andE1 = {(x?,? , i) | (αA )i 6= −∞}} + {(xj,i , (a, j, i0 )) | MA (a)i,i0 6= −∞}+ {(xj,i , j) | (βA )i 6= −∞}E2 = {(i, xj,i ) | (αB )j 6= −∞} + {((a, j, i), xj 0 ,i ) | MB (a)j,j 0 6= −∞}+ {(j, x?,? ) | (βB )j 6= −∞} ,γ(x?,? , i) = −(αA )i ,γ(xj,i , (a, j, i0 )) = −MA (a)i,i0 ,γ(xj,i , j) = −(βA )iγ(i, xj,i ) = (αB )j ,γ((a, j, i), xj 0 ,i ) = MB (a)j,j 0 ,γ(j, x?,? ) = (βB )j .

22

where i ∈ QA , j ∈ QB . This game is equal to a mean payoff game MP played on agraph G 0 = (Q0Min , Q0Max , qI0 , E 0 , γ 0 ) such that
Q0Min = ({?} + QA ) × ({?} + QB ) ,Q0Max = ({?} + QA ) × ({?} + QB ) × ({?} + {!} + Σ) ,qI0 = (?, ?) ,E 0 = E1 + E2 s.t. E1 ⊆ QMin × QMax , E2 ⊆ QMax × QMin andE1 = {((?, ?), (i, ?, ?)) | (αA )i 6= −∞}} + {((i, j), (i0 , j, a)) | MA (a)i,i0 6= −∞}+ {((i, j), (?, j, !)) | (βA )i 6= −∞}E2 = {((i, ?, ?), (i, j)) | (αB )j 6= −∞} + {((i, j, a), (i, j 0 )) | MB (a)j,j 0 6= −∞}+ {((?, j, !), (?, ?)) | (βB )j 6= −∞} ,γ((?, ?), (i, ?, ?)) = −(αA )i , γ((i, j), (i0 , j, a)) = −MA (a)i,i0 , γ((i, j), (?, j, !)) = −(βA )iγ((i, ?, ?), (i, j)) = (αB )j ,γ((i, j, a), (i, j 0 )) = MB (a)j,j 0 , γ((?, j, !), (?, ?)) = (βB )j .

3 : Let ALimavg and B Limavg be Limavg automata such that ALimavg = ({?}+QA , {?}+
00(a)x,y =, ?) and B Limavg = ({?} + QB , {?} + {!} + Σ, MB0 , ?). (Here MA{!} + Σ, MA000(a))x,y =MA (a)x,y (a ∈ Σ, x, y 6= ?), MA (?)?,y = (αA )y , MA (!)x,? = (βA )x and (MA0−∞ otherwise. MB is defined similarly.) We prove that a winning strategy for Challenger exists in a game played on A and B if and only if it exists in a game playedon ALimavg and B Limavg . Only if part is easy: by repeating winning strategy on A and
B,challenger can also win the game on ALimavg and B Limavg . Assume that there exists a winning strategy τ for Challenger in the game played on ALimavg and B Limavg .
From [10], we can assume that τ is positional (i.e. τ ((p0 , q0 ) . . . (pi , qi )) only dependson (pi , qi )). Because A has no trap state and A and B are finite, there exists r ∈ Rsuch that for each q ∈ QA , there is a path πq to the final state in A such that for
all path π from an arbitrary state to the final state in B on the same word, difference
between the summation of weights on πq and π is less than r. Using this r, we define strategy (ρ1 , τ1 ) for Challenger. Because τ is a winning strategy, p0 such that
τ (?, ?) = (?, p0 ) exists. We define ρ1 (•) as p0 . Furthermore, we define τ1 as follows: τ1 ((p0 , q0 ) . . . (pi , qi )) = τ ((?, ?)(p0 , q0 ) . . . (pi , qi )) until difference between
the summation of weights on p0 . . . pi and q0 . . . qi exceeds r, and after that, go πq
according to the state q where Challenger is at that time. Strategy τ constructed in asuch manner is a winning strategy for Challenger in the game played on ALimavg and
B Limavg ), and taking a path πi according to the state i where Challenger is at that time.
4 : From [7], G-simulation from ALimavg to B Limavg exists if and only if there exists a
winning strategy for Max in a mean payoff game MP.
tu