Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | https://arxiv.org/abs/2506.08437 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866909925143216128 |
|---|---|
| author | Chen, Chris McIver, Annabelle Morgan, Carroll |
| author_facet | Chen, Chris McIver, Annabelle Morgan, Carroll |
| contents | 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$_\sqcap$, 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_08437 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Forward and Backward Simulations for Partially Observable Probability Chen, Chris McIver, Annabelle Morgan, Carroll Logic in Computer Science 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$_\sqcap$, 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. |
| title | Forward and Backward Simulations for Partially Observable Probability |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2506.08437 |