A short note on Simulation and Abstraction
Chris Hankin
Institute for Security Science and Technology
Imperial College London, UK
c.hankin@imperial.ac.uk

This short note is written in celebration of David Schmidt’s sixtieth birthday. He has now been active
in the program analysis research community for over thirty years and we have enjoyed many interactions with him. His work on characterising simulations between Kripke structures using Galois
connections was particularly influential in our own work on using probabilistic abstract interpretation to study Larsen and Skou’s notion of probabilistic bisimulation. We briefly review this work and
discuss some recent applications of these ideas in a variety of different application areas.

1

Introduction

Since his earliest contributions on state transition machines for lambda calculus expressions [13], David
Schmidt has been at the forefront of research in programming language theory, particularly program
analysis.
His work on program analysis started through his collaboration with Neil Jones. No doubt partly
inspired by Patrick and Radhia Cousot’s work on abstract interpretation [2], he has made a study of
various aspects of Galois connections. An early contribution was [7]. A later example, which was
influential in our own work, was [15] where he shows how to characterise simulation relations using
Galois Connections.
The early work of our group was also inspired by the Cousots [1]. Over the last fourteen years,
we have been working on the analysis of probabilistic and quantitative programming languages and
systems [12]. This has led to a framework called probabilistic abstract interpretation (PAI). Rather than
using lattices and Galois Connections, PAI uses Hilbert Spaces and Moore-Penrose Pseudo Inverses.
Inspired by [15], we have used PAI to characterise probabilistic bisimulation [8, 10]; we demonstrated
the probabilistc analogue of Dave’s earlier results which amounted to characterising Larsen and Skou’s
probabilistic bisimulation [5] using Moore-Penrose Pseudo Inverses. A major feature of our approach is
that it becomes natural to introduce a notion of approximate bisimulation – this has proved to be very
useful in studies of language-based security [9].
The author first met David Schmidt nearly thirty years ago. He visited Imperial College whilst
developing the work in [7], his visit coincided with our own work on the ideas in [1]. We found a lot
to talk about and it was the start of many further interactions. In addition to his scientific contributions,
he has always given time to developing text books; his [14] was used to educate several generations of
Imperial students in the principles of programming language design. The author has also worked with
Dave on many programme committees; perhaps the high point was when they were co-General Chairs
of POPL in 2001. Dave has a had a long and successful career and we wish him many more years. The
author would like to add his congratulations to Dave on this important milestone.
A. Banerjee, O. Danvy, K.-G. Doh, J. Hatcliff (Eds):
David A. Schmidt’s 60th Birthday Festschrift
EPTCS 129, 2013, pp. 337–340, doi:10.4204/EPTCS.129.20

Simulation and Abstraction

338

2

Simulation and Galois Connections

In [15], Dave addresses, inter alia, the question of characterising simulation relations between Kripke
structures using Galois connections.
Recall that we define (L, α , γ , M) to be a Galois connection between the complete lattices (L, ⊑) and
(M, ⊑) if and only if

α : L → M and γ : M → L are monotone functions
that satisfy:

γ ◦ α ⊒ idL
α ◦ γ ⊑ idM

For Kripke structures C = hΣC , →C , IC i and A = hΣA , →A , IA i, a binary relation R ⊆ ΣC × ΣA is a
simulation of C by A (C ⊳R A), if for every c ∈ ΣC , a ∈ ΣA :
if c R a and c →C c′ then ∃a′ ∈ ΣA [a →A a′ and c′ R a′ ]
In the framework studied in [15], the concrete Kripke structures are often infinite state structures
representing programs and the abstract Kripke structures are some program analysis. In this setting,
we should abstract sets of states of the concrete structure to a single state in the abstract structure.
Given a Galois connection, (α : P(ΣC ) → ΣA , γ : ΣA → P(ΣC )), we can construct the relation, R(α ,γ ) ⊆
P(ΣC ) × ΣA :
S R(α ,γ ) a if and only if α (S) ⊑A a
This can be shown to be the suitable basis for a simulation relation.
Whilst [15] achieves much more than described here, it was these ideas that inspired our own work
on probabilistic bisimulation (originally introduced by Larsen and Skou [5]) for reactive systems (also
called fully probabilistic systems):
Definition 1 A probabilistic bisimulation is an equivalence relation ∼b on states of a probabilistic transition system satisfying for all actions a ∈ A:
p ∼b q and p →a π ⇔ q →a ρ and π ∼b ρ .
where π and ρ are distributions of states.
.

3

Probabilistic Bisimulation and Moore-Penrose Pseudo Inverses

In [10, 8] we introduced an approximate version of bisimulation and confinement where the approximation can be used as a measure ε for the information leakage of the system under analysis. We represented
probabilistic transition systems by linear operators, i.e. by their transition matrices M. In the case
of probabilistic programs and systems these matrices M are the usual well known stochastic matrices
which are the generators of the corresponding Markov chains (for details see [10, 8]).
We then showed that two systems M1 and M2 are bisimilar if there exist simplified, or abstracted,
versions of M1 and M2 , represented by matrices M#1 and M#2 , such that M#1 = M#2 . In the probabilistic

Chris Hankin

339

abstract interpretation setting that we use, a bounded linear operator and its Moore-Penrose Pseudo
Inverse are the analogue of the adjoined pair of monotonic functions in a Galois insertion. The abstract
systems are obtained by lumping states, i.e. by identifying each concrete state si with a class C j of states
which are all behavioural equivalent to each other.
Concretely, we compute this via n × m matrices K (where n is the number of concrete states and m
the number of abstract classes) with Kij = 1 iff si ∈ C j and 0 otherwise. We refer to such matrices which
have exactly one entry 1 in each row while all other entries are 0 as classification matrices, and denote
the set of all classification matrices by K . The abstract systems are then given by M#i = K†i Mi Ki with
Ki some classification matrix and † constructing the so called Moore-Penrose pseudo-inverse – in the
case of classification matrices K† can be constructed as the row-normalised transpose of K.
The problem of showing that two systems M1 and M2 are behaviourally equivalent, i.e. are (probabilistically) bisimilar, is now translated into finding two classification matrices Ki ∈ K such that
M#1 = K†1 M1 K1 = K†2 M2 K2 = M#2 .
In case that two systems are not bisimilar we can still define a quantity ε which describes how
(non-)bisimilar the two systems are. This ε is formally defined in terms of the norm of a linear operator
representing the partition induced by the ‘minimal’ bisimulation on the set of the states of a given system,
i.e. the one minimising the observational difference between the system’s components (see again [10]
for further details, in particular regarding labeled probabilistic transition systems):
Definition 2 Let M1 and M2 be the matrix representations of two probabilistic transition systems. We
say that M1 and M2 are ε -bisimilar, denoted by M1 ∼εb M2 , iff
inf

K1 ,K2 ∈K

kK†1 M1 K1 − K†2 M2 K2 k = ε

where k.k denotes an appropriate norm, e.g. the supremum norm k.k∞ .
In [10] we show that, when ε = 0 this gives the standard notion of probabilistic bisimulation.

4

Conclusion

This short note has sketched some early work by David which forms part of his deep study of the use
of Galois connections and relations in program analysis. Our own work on characterising probabilistic
bisimulation using probabilistic abstract interpretation has found a number of applications, including:
• the detection and removal of timing channels in probabilistic transition systems [11] – we study a
concept called probabilistic time bisimilarity and use it to detect timing channels;
• the detection of sub-communities in social media [6] – we evaluate a number of algorithms including one using the notion of stability from [3] which effectively lumps nodes together if their
mutual interactions are “stronger” than interactions outside the group; and
• the abstraction of stochastic and Bayesian games to provide decision support in cyber security [4] –
where we hope to apply probabilistic abstract interpretation directly to the underlying probabilistic
transition systems in the games, thereby developing a principled way of reducing the state spaces
to achieve tractability of game solutions.
We look forward to discussing some of this work with David in the future but, in the meantime, reiterate
our best wishes on this important anniversary.

Simulation and Abstraction

340

5

Acknowledgements

Much of the work discussed above was done in collaboration with Alessandra Di Pierro and Herbert
Wiklicky. More recently, I have enjoyed working on the application of these ideas to other areas with
Erwan Le Martelot and Pasquale Malacaria.

References
[1] Geoffrey L. Burn, Chris Hankin & Samson Abramsky (1986): Strictness Analysis for Higher-Order Functions. Sci. Comput. Program. 7(3), pp. 249–278, doi:10.1016/0167-6423(86)90010-9.
[2] Patrick Cousot & Radhia Cousot (1977): Abstract Interpretation: A Unified Lattice Model for Static
Analysis of Programs by Construction or Approximation of Fixpoints. In: POPL, ACM, pp. 238–252,
doi:10.1145/512950.512973.
[3] Jean-Charles Delvenne, Sophia Yaliraki & Mauricio Barahona (2010): Stability of graph communities across
time scales. Proc. Nat. Acad. Sci. 107(29), pp. 12755–12760, doi:10.1073/pnas.0903215107.
[4] Chris Hankin & Pasquale Malacaria (2013): Payoffs, Intensionality and Abstraction in Games. In: Computation, Logic, Games, and Quantum Foundations - The Many Facets of Samson Abramsky, Lecture Notes in
Computer Science 7860, Springer, doi:10.1007/978-3-642-38164-5-6.
[5] Kim Guldstrand Larsen & Arne Skou (1989): Bisimulation Through Probabilistic Testing. In: POPL, ACM,
pp. 344–352, doi:10.1145/75277.75307.
[6] Erwan Le Martelot & Chris Hankin (2013): Fast Multi-Scale Detection of Relevant Communities in LargeScale Networks. Computer Journal, doi:10.1093/comjnl/bxt002.
[7] Austin Melton, David A. Schmidt & George E. Strecker (1986): Galois Connections and Computer
Science Applications. In: CTCS, Lecture Notes in Computer Science 240, Springer, pp. 299–312,
doi:10.1007/3-540-17162-2-130.
[8] Alessandra Di Pierro, Chris Hankin & Herbert Wiklicky (2003): Quantitative Relations and Approximate
Process Equivalences. In: CONCUR, Lecture Notes in Computer Science 2761, Springer, pp. 498–512,
doi:10.1007/978-3-540-45187-7-33.
[9] Alessandra Di Pierro, Chris Hankin & Herbert Wiklicky (2004): Approximate Non-interference. Journal of
Computer Security 12(1), pp. 37–82.
[10] Alessandra Di Pierro, Chris Hankin & Herbert Wiklicky (2005): Measuring the confinement of probabilistic
systems. Theor. Comput. Sci. 340(1), pp. 3–56, doi:10.1016/j.tcs.2005.03.002.
[11] Alessandra Di Pierro, Chris Hankin & Herbert Wiklicky (2011): Probabilistic timing covert channels: to
close or not to close? Int. J. Inf. Sec. 10(2), pp. 83–106, doi:10.1007/s10207-010-0107-0.
[12] Alessandra Di Pierro & Herbert Wiklicky (2000): Concurrent constraint programming: towards probabilistic
abstract interpretation. In: PPDP, ACM, pp. 127–138, doi:10.1145/351268.351284.
[13] David A. Schmidt (1980): State transition machines for lambda calculus expressions. In: SemanticsDirected Compiler Generation, Lecture Notes in Computer Science 94, Springer, pp. 415–440,
doi:10.1007/3-540-10250-7-32.
[14] David A. Schmidt (1986): Denotational semantics: a methodology for language development. Allyn and
Bacon.
[15] David A. Schmidt (1999): Binary relations for abstraction and refinement. In: Workshop on Refinement and
Abstraction.

