1Preorder-Constrained Simulation

3Koko Muroya £RIMS, Kyoto University, Japan

4

Takahiro Sanada £5RIMS, Kyoto University, Japan

6

Natsuki Urabe £7National Institute of Informatics, Japan

28Abstract

12

We describe our ongoing work on generalizing some quantitatively constrained notions of weaksimulation up-to that are recently introduced for deterministic systems modeling program execution.
We present and discuss a new notion dubbed preorder-constrained simulation that allows comparison
between words using a preorder, instead of equality.

132012 ACM Subject Classification Theory of computation → Verification by model checking

14Keywords and phrases simulation, weak simulation, up-to technique, language inclusion, preorder

15

Digital Object Identifier 10.4230/LIPIcs.CVIT.2016.23

16

Category Early ideas abstract

91011

17
18
19

20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44

Funding The first and second authors are supported by JST, ACT-X Grant No. JPMJAX190U,
Japan. The third author is supported by JST ERATO HASUO Metamathematics for Systems
Design Project (No. JPMJER1603).

Simulation Notions with Bounded Number of Steps In the literature of program semantics,
coinductive techniques have often been used to establish equivalence between program
behaviors. A recent approach utilizes weak simulations with quantitative constraints on
the length of terminating runs. These constraints enable comparison of execution cost for
programs, in terms of the number of execution steps it takes for a program to terminate.
One example is Accattoli et al.’s notion called improvement [1]. It was used to show thatcertain rewriting of a program before execution not only preserves the execution result, butalso improves the execution cost by requiring less execution steps. Another example was usedin the first author’s previous work [8]. It is dubbed (Q, Q1 , Q2 )-simulation, parameterized
by a triple (Q, Q1 , Q2 ) of preorders on natural numbers. This notion incorporates the socalled up-to technique, and the triple plays a crucial role to make the combination of weaksimulations and the up-to technique work. The first preorder Q is used to compare lengthsof accepted runs, generalizing the “greater-than-or-equal” preorder ≥ used by improvements.
These two notions are both designed for unlabeled deterministic transition systems,
which can model execution of deterministic programs only. We aim to pursue the idea ofconstraining terminating, or accepted, runs, in a more general setting. This abstract describes
our ongoing work on generalizing (Q, Q1 , Q2 )-simulations to nondeterministic automata. We
present a novel notion of preorder-constrained simulation that is a weak simulation up-to
constrained by preorders on words, not on natural numbers. It entails a generalized notionof language inclusion that compares words using a preorder instead of equality.
Preorder-Constrained Simulation Let Ak = (Xk , Σ, ⇝k ⊆ Xk × Σ × Xk , Fk ⊆ Xk ) (k ∈{1, 2}) be nondeterministic automata, x ∈ X1 and y ∈ X2 , and L∗A1 (x), L∗A2 (y) ⊆ Σ∗ be theset of words accepted from x and y respectively. The ordinary simulation notion [7] proves
language inclusion L∗A1 (x) ⊆ L∗A2 (y). Instead, for a preorder Q ⊆ Σ∗ × Σ∗ , we write x ⪯Q ywhen ∀w ∈ L∗A1 (x). ∃w′ ∈ L∗A2 (y). wQw′ . Our simulation notion proves this.
© Koko Muroya, Takahiro Sanada and Natsuki Urabe;licensed under Creative Commons License CC-BY 4.0
42nd Conference on Very Important Topics (CVIT 2016).
Editors: John Q. Open and Joan R. Access; Article No. 23; pp. 23:1–23:3
Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

23:2

Preorder-Constrained Simulation

45
46
47
48
49
50
51
52
53
54
55
56
57
58

59
60

61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91

Here are examples: when Q is the equality, x ⪯Q y iff L∗A1 (x) ⊆ L∗A2 (y). When Σ contains
a special letter τ , and wQw′ means that w and w′ are the same except for τ , then x ⪯Q y iff
language inclusion ignoring τ holds. When wQw′ means that w is a subword of w′ , x ⪯Q yiff for each w ∈ L∗A1 (x) there exists w′ ∈ L∗A2 (y) such that w is a subword of w′ .
▶ Def. 1. Let Q, Q1 , Q2 ⊆ Σ∗ × Σ∗ be preorders. We call R ⊆ X1 × X2 aw∗
x / x′′(Q, Q1 , Q2 )-simulation from A1 to A2 if, for any (x, y) ∈ R, the following holds.
⪯Q1w•Final: x ∈ F1 implies y ⇝∗2 y ′ for some y ′ ∈ F2 and w ∈ Σ∗ such that εQw.
RR
Step: In the following game played on X1 × Σ∗ by Challenger and Simulator,•⪯QSimulator is winning from a state (x, ε). In each round, a pebble onw′∗/ ′′ 2yy(x′ , w) ∈ X1 × Σ∗ is moved as follows.
a1. Challenger chooses a ∈ Σ and x′′ ∈ X1 such that x′ ⇝1 x′′ , and let w := wa.
2. Simulator chooses either of the following: i) choose y ′′ ∈ X2 and w′ ∈ Σ∗ such thatw′ ∗ ′′′′′′′y⇝
2 y , wQw and x ⪯Q1 R ⪯Q2 y , and end the game; or ii) skip his turn.
Simulator wins the game if (i) is chosen on his turn.
▶ Prop. 2. If the following conditions are satisfied, xRy implies x ⪯Q y: i) w1 Qw1′ andw2′ Qw2′ imply w1 w2 Qw1′ w2′ ; ii) Q1 QQ2 ⊆ Q; and iii) wQ1 w′ implies |w| ≥ |w′ |.
◀
It is known that a naïve combination of weak simulations and up-to techniques leads tounsoundness, and require special cares [9, 10]. In Prop. 2, it is dealt with by Cond.(iii).
Related Work The above notion is similar to buffered simulation [3], which was developed
to enable more relations to witness language inclusion. Buffered simulations allow Simulator
to skip his turn, to buffer Challenger’s moves and to simulate them later together, which has
a similar flavor to our simulation notion. Hence our simulation notion can be also thought ofas a generalization of buffered simulation.
Preorder-constrained simulations allow a quantitative reasoning such as comparing lengthsof accepted runs. There exist quantitative simulation notions for comparing costs of weighted
automata. Many of them are for probabilistic systems [6, 5, 4]. One simulation notion
for automata weighted with costs was introduced as a matrix over real numbers [11]. A
methodology for comparing infinite runs of weighted automata is also known [2]. In contrast
to weighted automata, which are labeled with both letters and weights, our target is automata
labeled with letters only. Quantities appear in the set of words, in our approach.
Research Directions Our simulation notion focuses on finite languages. As is the case forthe ordinary simulation notion, our notion may fail to prove inclusion of finite languages
when there is no inclusion of infinite languages. We are looking into possible solutions.
We suspect that Cond. (iii) of Prop. 2, whose analogues are also in existing notions ofweak simulation up-to, is too strong. We think Q1 violating Cond. (iii) can be allowed finitely
many times. However, at the same time, we should note that the relaxation makes thedefinition of simulations a global one, which can result in a more complicated algorithm forfinding it. We should make sure that it does not ruin efficiency gained by up-to techniques.
Our simulation notion works well with systems whose alphabet Σ carries an order. Sucha system arises in the study of linear temporal logic (LTL). An LTL formula induces a Büchi
automaton labeled with the powerset 2AP of atomic propositions [12]. The alphabet 2AP isordered by the inclusion, which induces a preorder on (2AP )∗ .
We are also interested in a categorical study of our simulation notion. One possible
strategy would be to use the category PreOrd of preordered sets as the base category. The
nondeterministic branching would be then captured by the powerset functor (or possibly amonad) P lifted to PreOrd. The categorical generalization might allow us to transfer oursimulation notion to systems with other branching types, e.g. probabilistic one.

K. Muroya, T. Sanada and N. Urabe

References

9293

19495

2969798

399
100
101

41021035104105

61061077108
1098110111

9112
113
114

10115
116

11117
118
119
120

23:3

12

Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. The machinery of interaction. InPPDP 2020, pages 4:1–4:15. ACM, 2020.
Suguman Bansal, Swarat Chaudhuri, and Moshe Y. Vardi. Comparator automata in quantitative verification. In FoSSaCS 2018, volume 10803 of Lecture Notes in Computer Science,pages 420–437. Springer, 2018.
Milka Hutagalung, Martin Lange, and Étienne Lozes. Buffered simulation games for büchiautomata. In Zoltán Ésik and Zoltán Fülöp, editors, AFL 2014, volume 151 of EPTCS, pages
286–300, 2014.
Bart Jacobs and Jesse Hughes. Simulations in coalgebra. Electronic Notes in TheoreticalComputer Science, 82(1):128–149, 2003.
Bengt Jonsson and Kim Guldstrand Larsen. Specification and refinement of probabilisticprocesses. In LICS 1991, pages 266–277. IEEE Computer Society, 1991.
Kim G. Larsen and Arne Skou. Bisimulation through probabilistic testing. Information andComputation, 94(1):1–28, 1991.
Nancy A. Lynch and Frits W. Vaandrager. Forward and backward simulations – Part I:
Untimed systems. Technical report, NLD, 1993.
Koko Muroya. Hypernet Semantics of Programming Languages. PhD thesis, University ofBirmingham, 2020.
Damien Pous. Up-to techniques for weak bisimulation. In Luís Caires, Giuseppe F. Italiano,Luís Monteiro, Catuscia Palamidessi, and Moti Yung, editors, ICALP 2005, volume 3580 ofLecture Notes in Computer Science, pages 730–741. Springer, 2005.
Damien Pous. New up-to techniques for weak bisimulation. Theoretical Computer Science,
380(1):164–180, 2007. Automata, Languages and Programming.
Natsuki Urabe and Ichiro Hasuo. Generic forward and backward simulations III: quantitative
simulations by matrices. In CONCUR 2014, volume 8704 of Lecture Notes in Computer
Science, pages 451–466. Springer, 2014.
Moshe Y. Vardi and Pierre Wolper. Reasoning about infinite computations. Information andComputation, 115(1):1–37, 1994.

CVIT 2016