{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T19:04:57Z","timestamp":1770750297186,"version":"3.50.0"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032111753","type":"print"},{"value":"9783032111760","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,23]],"date-time":"2025-11-23T00:00:00Z","timestamp":1763856000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,23]],"date-time":"2025-11-23T00:00:00Z","timestamp":1763856000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-11176-0_17","type":"book-chapter","created":{"date-parts":[[2025,11,22]],"date-time":"2025-11-22T20:11:25Z","timestamp":1763842285000},"page":"279-297","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Forward and\u00a0Backward Simulations for\u00a0Partially Observable Probability"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-2628-7343","authenticated-orcid":false,"given":"Chris","family":"Chen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2405-9838","authenticated-orcid":false,"given":"Annabelle","family":"McIver","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8535-9068","authenticated-orcid":false,"given":"Carroll","family":"Morgan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,23]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. In: LICS, pp. 165\u2013175 (1988)","DOI":"10.1109\/LICS.1988.5115"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Abramsky, S., Jung, A.: Domain Theory. In: Handbook of Logic and Computer Science, pp. 1\u2013168. Oxford Science Publications (1994)","DOI":"10.1093\/oso\/9780198537625.003.0001"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Alvim, M.S., Chatzikokolakis, K., McIver, A., Morgan, C., Smith, G., Palamidessi, C.: The Science of Quantitative Information Flow. Springer (2020)","DOI":"10.1007\/978-3-319-96131-6"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Alvim, M.S., Chatzikokolakis, K., Palamidessi, C., Smith, G.: Measuring information leakage using generalized gain functions. In: Proceedings of 25th IEEE Computer Security Foundations Symposium (CSF 2012), pp. 265\u2013279 (2012)","DOI":"10.1109\/CSF.2012.26"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer (1998)","DOI":"10.1007\/978-1-4612-1674-2"},{"issue":"5","key":"17_CR6","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/s001650070008","volume":"12","author":"R-J Back","year":"2000","unstructured":"Back, R.-J., Wright, J.: Encoding, decoding and data refinement. Formal Aspects Comput. 12(5), 313\u2013349 (2000)","journal-title":"Formal Aspects Comput."},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Bolton, C., Davies, J., Woodcock, J.: On the refinement and simulation of data types and processes. In: Proceedings of iFM, pp. 273\u2013292 (1999)","DOI":"10.1007\/978-1-4471-0851-1_15"},{"key":"17_CR8","doi-asserted-by":"publisher","unstructured":"Bottenbruch, H.: Structure and use of ALGOL 60. J. ACM 9(2), 161\u2013221 (1962). https:\/\/doi.org\/10.1145\/321119.321120","DOI":"10.1145\/321119.321120"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Chen, C., McIver, A., Morgan, C.: Probabilistic datatypes. In: Proceedings of ICTAC. LNCS, pp. 3\u201316. Springer, Heidelberg (2024)","DOI":"10.1007\/978-3-031-77019-7_1"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Chen, C., McIver, A., Morgan, C.: Source-level reasoning for quantifying information leaks. In: Jansen, N., et al. (eds.) Principles of Verification: Cycling the Probabilistic Landscape. LNCS, pp. 98\u2013127. Springer, Cham (2025)","DOI":"10.1007\/978-3-031-75783-9_5"},{"key":"17_CR11","unstructured":"Dijkstra, E.: A Discipline of Programming. Prentice-Hall (1976)"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Dijkstra, E., Scholten, C.: Predicate Calculus and Program Semantics. Springer (1990)","DOI":"10.1007\/978-1-4612-3228-5"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Floyd, R.: Assigning meanings to programs. In: Schwartz, J. (ed.) Mathematical Aspects of Computer Science, pp. 19\u201332. American Mathematical Society (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"issue":"4","key":"17_CR14","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/BF01212407","volume":"5","author":"P Gardiner","year":"1993","unstructured":"Gardiner, P., Morgan, C.: A single complete rule for data refinement. Formal Aspects Comput. 5(4), 367\u201382 (1993)","journal-title":"Formal Aspects Comput."},{"key":"17_CR15","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2023.105044","volume":"293","author":"R Garner","year":"2023","unstructured":"Garner, R.: Hypernormalisation in an abstract setting. Inf. Comput. 293, 105044 (2023)","journal-title":"Inf. Comput."},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Gibbons, J., McIver, A., Morgan, C., Schrijvers, T.: Quantitative information flow with monads in haskell. In: Barthe, G., Katoen, J.-P., Silva, A. (eds.) Foundations of Probabilistic Programming. CUP (2019)","DOI":"10.1017\/9781108770750.013"},{"issue":"3","key":"17_CR17","first-page":"45","volume":"253","author":"S Giro","year":"2009","unstructured":"Giro, S., D\u2019Argenio, P.: On the expressive power of schedulers in distributed probabilistic systems. ENTCS 253(3), 45\u201371 (2009)","journal-title":"ENTCS"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1007\/11817949_27","volume-title":"CONCUR 2006 \u2013 Concurrency Theory","author":"I Hasuo","year":"2006","unstructured":"Hasuo, I.: Generic forward and backward simulations. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 406\u2013420. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817949_27"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"Hoare, C.A., Sanders, J.W.: Data refinement refined. In: ESOP 1986: European Symposium on Programming, pp. 187\u2013196 (1986)","DOI":"10.1007\/3-540-16442-1_14"},{"issue":"2","key":"17_CR20","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/0020-0190(87)90224-9","volume":"25","author":"C Hoare","year":"1987","unstructured":"Hoare, C., He, J., Sanders, J.: Prespecification in data refinement. Inf. Proc. Lett. 25(2), 71\u20136 (1987)","journal-title":"Inf. Proc. Lett."},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Jacobs, B.: Hyper normalisation and conditioning for discrete probability distributions. Log. Methods Comput. Sci. 13 (2017)","DOI":"10.23638\/LMCS-13(3:17)2017"},{"key":"17_CR22","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/j.entcs.2008.12.064","volume":"225","author":"M Johnson","year":"2009","unstructured":"Johnson, M., Naumann, D., Power, J.: Category theoretic models of data refinement. Electron. Notes Theor. Comput. Sci. 225, 21\u201338 (2009)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"17_CR23","doi-asserted-by":"crossref","unstructured":"Jones, C., Plotkin, G.: A probabilistic powerdomain of evaluations. In: LICS 1989, pp. 186\u201395. Computer Society Press, Los Alamitos (1989)","DOI":"10.1109\/LICS.1989.39173"},{"key":"17_CR24","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/S0004-3702(98)00023-X","volume":"101","author":"LP Kaebling","year":"1998","unstructured":"Kaebling, L.P., Littman, M.L., Cassandra, A.R.: Planning and acting in partially observable stochastic domains. Artif. Intell. 101, 99\u2013134 (1998)","journal-title":"Artif. Intell."},{"key":"17_CR25","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1016\/0022-0000(81)90036-2","volume":"22","author":"D Kozen","year":"1981","unstructured":"Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22, 328\u201350 (1981)","journal-title":"J. Comput. Syst. Sci."},{"key":"17_CR26","first-page":"363","volume-title":"ICALP","author":"H Langmaack","year":"1988","unstructured":"Langmaack, H., Olderog, E.-R.: Present-day Hoare-like systems for programming languages with procedures: power, limits and most likely extensions. In: De Bakker, J., van Leeuwen, J. (eds.) ICALP, pp. 363\u2013373. Springer, Heidelberg (1988)"},{"key":"17_CR27","doi-asserted-by":"crossref","unstructured":"Liskov, B.: Data abstraction and hierarchy. In: Addendum to Proceedings of OOPSLA, pp. 17\u201334 (1987)","DOI":"10.1145\/62138.62141"},{"issue":"4","key":"17_CR28","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1145\/942572.807045","volume":"9","author":"B Liskov","year":"1974","unstructured":"Liskov, B., Zilles, S.: Programming with abstract data types. ACM Sigplan Not. 9(4), 50\u201359 (1974)","journal-title":"ACM Sigplan Not."},{"issue":"2","key":"17_CR29","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1006\/inco.1995.1134","volume":"121","author":"N Lynch","year":"1995","unstructured":"Lynch, N., Vaandrager, F.: Forward and backward simulations. Inf. Comput. 121(2), 214\u2013233 (1995)","journal-title":"Inf. Comput."},{"key":"17_CR30","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Springer, New York (2005)","DOI":"10.1145\/1059816.1059824"},{"key":"17_CR31","doi-asserted-by":"crossref","unstructured":"McIver, A., Meinicke, L., Morgan, C.: A Kantorovich-monadic powerdomain for information hiding, with probability and nondeterminism. In: Proceedings of LICS 2012 (2012)","DOI":"10.1109\/LICS.2012.56"},{"key":"17_CR32","doi-asserted-by":"publisher","unstructured":"McIver, A., Meinicke, L., Morgan, C.: Hidden-Markov program algebra with iteration. Math. Struct. Comput. Sci. 24 (2014). https:\/\/doi.org\/10.1017\/S0960129513000625","DOI":"10.1017\/S0960129513000625"},{"key":"17_CR33","unstructured":"Morgan, C., McIver, A.: pGCL: formal reasoning for random algorithms. South Afr. Comput. J. 22, 14\u201327 (1999)"},{"issue":"3","key":"17_CR34","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1145\/229542.229547","volume":"18","author":"C Morgan","year":"1996","unstructured":"Morgan, C., McIver, A., Seidel, K.: Probabilistic predicate transformers. ACM Trans. Prog. Lang. Syst. 18(3), 325\u201353 (1996)","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"17_CR35","unstructured":"Perrone, P.: Categorical probability and stochastic dominance in metric spaces. Ph.D. thesis, Dissertation, Leipzig, Universit\u00e4t Leipzig (2018)"},{"key":"17_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/978-3-030-31175-9_19","volume-title":"The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy","author":"T Rabehaja","year":"2019","unstructured":"Rabehaja, T., McIver, A., Morgan, C., Struth, G.: Categorical information flow. In: Alvim, M.S., Chatzikokolakis, K., Olarte, C., Valencia, F. (eds.) The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy. LNCS, vol. 11760, pp. 329\u2013343. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31175-9_19"},{"key":"17_CR37","doi-asserted-by":"crossref","unstructured":"de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press (1998)","DOI":"10.1017\/CBO9780511663079"},{"issue":"1","key":"17_CR38","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(00)00056-6","volume":"249","author":"JJMM Rutten","year":"2000","unstructured":"Rutten, J.J.M.M.: Universal coalgebra: a theory of systems. TCS 249(1), 3\u201380 (2000)","journal-title":"TCS"},{"key":"17_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-642-00596-1_21","volume-title":"Foundations of Software Science and Computational Structures","author":"G Smith","year":"2009","unstructured":"Smith, G.: On the foundations of quantitative information flow. In: de Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 288\u2013302. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00596-1_21"},{"key":"17_CR40","doi-asserted-by":"crossref","unstructured":"Smith, G.: Quantifying information flow using min-entropy. In: Proceedings of QEST 2011, pp. 159\u2013167 (2011)","DOI":"10.1109\/QEST.2011.31"},{"key":"17_CR41","first-page":"3","volume":"222","author":"R Tix","year":"2009","unstructured":"Tix, R., Keimel, K., Plotkin, G.: Semantic domains for combining probability and non-determinism. ENTCS 222, 3\u201399 (2009)","journal-title":"ENTCS"},{"key":"17_CR42","unstructured":"Varacca, D.: Probability, nondeterminism and concurrency: two denotational models for probabilistic computation. Ph.D. thesis (2003)"},{"key":"17_CR43","doi-asserted-by":"crossref","unstructured":"Wirth, N.: Program development by stepwise refinement. Commun. ACM 14(4), 221\u2013227 (1971). http:\/\/www.acm.org\/classics\/doc96\/","DOI":"10.1145\/362575.362577"},{"key":"17_CR44","doi-asserted-by":"crossref","unstructured":"Ye, K., Foster, S., Woodcock, J.: Automated reasoning for probabilistic sequential programs with theorem proving. In: RAMiCS, pp. 465\u2013482. Springer (2021)","DOI":"10.1007\/978-3-030-88701-8_28"},{"issue":"394","key":"17_CR45","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1080\/01621459.1986.10478289","volume":"81","author":"A Zellner","year":"1986","unstructured":"Zellner, A.: Bayesian estimation and prediction using asymmetric loss functions. J. Am. Stat. Assoc. 81(394), 446\u2013451 (1986)","journal-title":"J. Am. Stat. Assoc."}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2025"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-11176-0_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T11:09:39Z","timestamp":1770721779000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-11176-0_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,23]]},"ISBN":["9783032111753","9783032111760"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-11176-0_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,23]]},"assertion":[{"value":"23 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"ICTAC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Colloquium on Theoretical Aspects of Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Marrakesh","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Morocco","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ictac2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ictac2025.digital-hub.sh\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}