Forward and backward simulations for partially observable probability

Chris Chen; Annabelle McIver; Carroll Morgan

doi:10.1007/978-3-032-11176-0_17

Forward and backward simulations for partially observable probability

Chris Chen^*, Annabelle McIver, Carroll Morgan

^*Corresponding author for this work

School of Computing

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

Abstract

Data refinement is the standard extension of a refinement relation from programs to datatypes (i.e. a behavioural subtyping relation). Forward/backward simulations provide a tractable method for establishing data refinement, and have been thoroughly studied for nondeterministic programs. However, for standard models of mixed probability and nondeterminism, ordinary assignment statements may not commute with (variable-disjoint) program fragments. This (1) invalidates a key assumption underlying the soundness of simulations, and (2) prevents modelling probabilistic datatypes with encapsulated state.

We introduce a weakest precondition semantics for Kuifje_⊓, a language for partially observable Markov decision processes, using so-called loss (function) transformers. We prove soundness of forward/backward simulations in this richer setting, modulo healthiness conditions with a remarkable duality: forward simulations cannot leak information, and backward simulations cannot exploit leaked information.

Original language	English
Title of host publication	Theoretical Aspects of Computing - ICTAC 2025
Subtitle of host publication	22nd International Colloquium, Marrakech, Morocco, November 24-28, 2025, proceedings
Editors	Zhiming Liu, Adnane Saoud, Heike Wehrheim
Place of Publication	Cham
Publisher	Springer, Springer Nature
Pages	279-297
Number of pages	19
ISBN (Electronic)	9783032111760
ISBN (Print)	9783032111753
DOIs	https://doi.org/10.1007/978-3-032-11176-0_17
Publication status	Published - 2026
Event	22nd International Colloquium on Theoretical Aspects of Computing, ICTAC 2025 - Marrakesh, Morocco Duration: 24 Nov 2025 → 28 Nov 2025

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	16237
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	22nd International Colloquium on Theoretical Aspects of Computing, ICTAC 2025
Country/Territory	Morocco
City	Marrakesh
Period	24/11/25 → 28/11/25

Keywords

Forward and backward simulations
Abstract datatypes
Data refinement
Probabilistic nondeterminism
Weakest precondition
Quantitative information flow
Probabilistic predicates

Access to Document

10.1007/978-3-032-11176-0_17

Cite this

Chen, C., McIver, A., & Morgan, C. (2026). Forward and backward simulations for partially observable probability. In Z. Liu, A. Saoud, & H. Wehrheim (Eds.), Theoretical Aspects of Computing - ICTAC 2025: 22nd International Colloquium, Marrakech, Morocco, November 24-28, 2025, proceedings (pp. 279-297). (Lecture Notes in Computer Science; Vol. 16237). Springer, Springer Nature. https://doi.org/10.1007/978-3-032-11176-0_17

Chen, Chris ; McIver, Annabelle ; Morgan, Carroll. / Forward and backward simulations for partially observable probability. Theoretical Aspects of Computing - ICTAC 2025: 22nd International Colloquium, Marrakech, Morocco, November 24-28, 2025, proceedings. editor / Zhiming Liu ; Adnane Saoud ; Heike Wehrheim. Cham : Springer, Springer Nature, 2026. pp. 279-297 (Lecture Notes in Computer Science).

@inproceedings{f058cdb4d4614b3daf5c1fe72e9f4c81,

title = "Forward and backward simulations for partially observable probability",

abstract = "Data refinement is the standard extension of a refinement relation from programs to datatypes (i.e. a behavioural subtyping relation). Forward/backward simulations provide a tractable method for establishing data refinement, and have been thoroughly studied for nondeterministic programs. However, for standard models of mixed probability and nondeterminism, ordinary assignment statements may not commute with (variable-disjoint) program fragments. This (1) invalidates a key assumption underlying the soundness of simulations, and (2) prevents modelling probabilistic datatypes with encapsulated state. We introduce a weakest precondition semantics for Kuifje⊓, a language for partially observable Markov decision processes, using so-called loss (function) transformers. We prove soundness of forward/backward simulations in this richer setting, modulo healthiness conditions with a remarkable duality: forward simulations cannot leak information, and backward simulations cannot exploit leaked information.",

keywords = "Forward and backward simulations, Abstract datatypes, Data refinement, Probabilistic nondeterminism, Weakest precondition, Quantitative information flow, Probabilistic predicates",

author = "Chris Chen and Annabelle McIver and Carroll Morgan",

year = "2026",

doi = "10.1007/978-3-032-11176-0\_17",

language = "English",

isbn = "9783032111753",

series = "Lecture Notes in Computer Science",

publisher = "Springer, Springer Nature",

pages = "279--297",

editor = "Zhiming Liu and Adnane Saoud and Heike Wehrheim",

booktitle = "Theoretical Aspects of Computing - ICTAC 2025",

address = "United States",

note = "22nd International Colloquium on Theoretical Aspects of Computing, ICTAC 2025 ; Conference date: 24-11-2025 Through 28-11-2025",

}

Chen, C , McIver, A & Morgan, C 2026, Forward and backward simulations for partially observable probability. in Z Liu, A Saoud & H Wehrheim (eds), Theoretical Aspects of Computing - ICTAC 2025: 22nd International Colloquium, Marrakech, Morocco, November 24-28, 2025, proceedings. Lecture Notes in Computer Science, vol. 16237, Springer, Springer Nature, Cham, pp. 279-297, 22nd International Colloquium on Theoretical Aspects of Computing, ICTAC 2025, Marrakesh, Morocco, 24/11/25. https://doi.org/10.1007/978-3-032-11176-0_17

Forward and backward simulations for partially observable probability. / Chen, Chris ; McIver, Annabelle; Morgan, Carroll.
Theoretical Aspects of Computing - ICTAC 2025: 22nd International Colloquium, Marrakech, Morocco, November 24-28, 2025, proceedings. ed. / Zhiming Liu; Adnane Saoud; Heike Wehrheim. Cham: Springer, Springer Nature, 2026. p. 279-297 (Lecture Notes in Computer Science; Vol. 16237).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

TY - GEN

T1 - Forward and backward simulations for partially observable probability

AU - Chen, Chris

AU - McIver, Annabelle

AU - Morgan, Carroll

PY - 2026

Y1 - 2026

N2 - Data refinement is the standard extension of a refinement relation from programs to datatypes (i.e. a behavioural subtyping relation). Forward/backward simulations provide a tractable method for establishing data refinement, and have been thoroughly studied for nondeterministic programs. However, for standard models of mixed probability and nondeterminism, ordinary assignment statements may not commute with (variable-disjoint) program fragments. This (1) invalidates a key assumption underlying the soundness of simulations, and (2) prevents modelling probabilistic datatypes with encapsulated state. We introduce a weakest precondition semantics for Kuifje⊓, a language for partially observable Markov decision processes, using so-called loss (function) transformers. We prove soundness of forward/backward simulations in this richer setting, modulo healthiness conditions with a remarkable duality: forward simulations cannot leak information, and backward simulations cannot exploit leaked information.

AB - Data refinement is the standard extension of a refinement relation from programs to datatypes (i.e. a behavioural subtyping relation). Forward/backward simulations provide a tractable method for establishing data refinement, and have been thoroughly studied for nondeterministic programs. However, for standard models of mixed probability and nondeterminism, ordinary assignment statements may not commute with (variable-disjoint) program fragments. This (1) invalidates a key assumption underlying the soundness of simulations, and (2) prevents modelling probabilistic datatypes with encapsulated state. We introduce a weakest precondition semantics for Kuifje⊓, a language for partially observable Markov decision processes, using so-called loss (function) transformers. We prove soundness of forward/backward simulations in this richer setting, modulo healthiness conditions with a remarkable duality: forward simulations cannot leak information, and backward simulations cannot exploit leaked information.

KW - Forward and backward simulations

KW - Abstract datatypes

KW - Data refinement

KW - Probabilistic nondeterminism

KW - Weakest precondition

KW - Quantitative information flow

KW - Probabilistic predicates

UR - https://www.scopus.com/pages/publications/105023502618

U2 - 10.1007/978-3-032-11176-0_17

DO - 10.1007/978-3-032-11176-0_17

M3 - Conference proceeding contribution

AN - SCOPUS:105023502618

SN - 9783032111753

T3 - Lecture Notes in Computer Science

SP - 279

EP - 297

BT - Theoretical Aspects of Computing - ICTAC 2025

A2 - Liu, Zhiming

A2 - Saoud, Adnane

A2 - Wehrheim, Heike

PB - Springer, Springer Nature

CY - Cham

T2 - 22nd International Colloquium on Theoretical Aspects of Computing, ICTAC 2025

Y2 - 24 November 2025 through 28 November 2025

ER -

Chen C , McIver A, Morgan C. Forward and backward simulations for partially observable probability. In Liu Z, Saoud A, Wehrheim H, editors, Theoretical Aspects of Computing - ICTAC 2025: 22nd International Colloquium, Marrakech, Morocco, November 24-28, 2025, proceedings. Cham: Springer, Springer Nature. 2026. p. 279-297. (Lecture Notes in Computer Science). doi: 10.1007/978-3-032-11176-0_17