Compositional bisimulation metric reasoning with Probabilistic Process Calculi

Daniel Gebler; Kim G. Larsen; Simone Tini

doi:10.2168/LMCS-12(4:12)2016

Daniel Gebler ; Kim G. Larsen ; Simone Tini - Compositional bisimulation metric reasoning with Probabilistic Process Calculi

lmcs:2627 - Logical Methods in Computer Science, April 27, 2017, Volume 12, Issue 4 - https://doi.org/10.2168/LMCS-12(4:12)2016

Compositional bisimulation metric reasoning with Probabilistic Process CalculiArticle

Authors: Daniel Gebler ; Kim G. Larsen ; Simone Tini

We study which standard operators of probabilistic process calculi allow for compositional reasoning with respect to bisimulation metric semantics. We argue that uniform continuity (generalizing the earlier proposed property of non-expansiveness) captures the essential nature of compositional reasoning and allows now also to reason compositionally about recursive processes. We characterize the distance between probabilistic processes composed by standard process algebra operators. Combining these results, we demonstrate how compositional reasoning about systems specified by continuous process algebra operators allows for metric assume-guarantee like performance validation.

https://doi.org/10.2168/LMCS-12(4:12)2016

Source: arXiv.org:1610.06162

Volume: Volume 12, Issue 4

Secondary volumes: Selected Papers of the 18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2015)

Published on: April 27, 2017

Accepted on: January 2, 2017

Submitted on: December 15, 2015

Keywords: Computer Science - Logic in Computer Science

Licence: arXiv.org - Non-exclusive license to distribute

Funding:

Source : OpenAIRE Graph

Learning, Analysis, SynthesiS and Optimization of Cyber-Physical Systems; Funder: European Commission; Code: 669844

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

17 Documents citing this article

Francesco Gavazzo;Cecilia Di Florio, 2023, Elements of Quantitative Rewriting, Proceedings of the ACM on Programming Languages, 7, POPL, pp. 1832-1863, 10.1145/3571256, https://doi.org/10.1145/3571256.

Valentina Castiglioni;Michele Loreti;Simone Tini, 2023, A framework to measure the robustness of programs in the unpredictable environment, Logical Methods in Computer Science, Volume 19, Issue 3, 10.46298/lmcs-19(3:2)2023, https://doi.org/10.46298/lmcs-19(3:2)2023.

Ugo Dal Lago;Francesco Gavazzo, 2022, Effectful program distancing, Proceedings of the ACM on Programming Languages, 6, POPL, pp. 1-30, 10.1145/3498680, https://doi.org/10.1145/3498680.

Alejandro Aguirre;Gilles Barthe;Justin Hsu;Benjamin Lucien Kaminski;Joost-Pieter Katoen;Christoph Matheja, 2021, A pre-expectation calculus for probabilistic sensitivity, Proceedings of the ACM on Programming Languages, 5, POPL, pp. 1-28, 10.1145/3434333, https://doi.org/10.1145/3434333.

Matteo Mio;Ralph Sarkis;Valeria Vignudelli, 2021, Combining Nondeterminism, Probability, and Termination: Equational and Metric Reasoning, pp. 1-14, 10.1109/lics52264.2021.9470717.

Ugo Dal Lago;Francesco Gavazzo, 2021, Differential logical relations, part II increments and derivatives, 895, pp. 34-47, 10.1016/j.tcs.2021.09.027, https://inria.hal.science/hal-03520721.

Valentina Castiglioni;Michele Loreti;Simone Tini, 2021, How Adaptive and Reliable is Your Program?, pp. 60-79, 10.1007/978-3-030-78089-0_4, https://inria.hal.science/hal-03740265.

Alejandro Aguirre Galindo, 2020, Relational logics for higher-order effectful programs, 10.20868/upm.thesis.66350.

Mio, Matteo;Vignudelli, Valeria, 2020, Monads and Quantitative Equational Theories for Nondeterminism and Probability, DROPS (Schloss Dagstuhl – Leibniz Center for Informatics), 10.4230/lipics.concur.2020.28, https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.28.

Valentina Castiglioni;Michele Loreti;Simone Tini, 2019, The metric linear-time branching-time spectrum on nondeterministic probabilistic processes, Theoretical Computer Science, 813, pp. 20-69, 10.1016/j.tcs.2019.09.019, https://doi.org/10.1016/j.tcs.2019.09.019.

Valentina Castiglioni;Ruggero Lanotte;Simone Tini, 2019, Fully Syntactic Uniform Continuity Formats for Bisimulation Metrics, Lecture notes in computer science, pp. 293-312, 10.1007/978-3-030-31175-9_17.

Valentina Castiglioni;Simone Tini, 2019, Probabilistic divide & congruence: Branching bisimilarity, Theoretical Computer Science, 802, pp. 147-196, 10.1016/j.tcs.2019.09.037, https://doi.org/10.1016/j.tcs.2019.09.037.

Valentina Castiglioni;Simone Tini, 2019, Logical characterization of branching metrics for nondeterministic probabilistic transition systems, Information and Computation, 268, pp. 104432, 10.1016/j.ic.2019.06.001, https://doi.org/10.1016/j.ic.2019.06.001.

Francesco Gavazzo, 2018, Quantitative Behavioural Reasoning for Higher-order Effectful Programs, pp. 452-461, 10.1145/3209108.3209149, https://inria.hal.science/hal-01926069.

Ruggero Lanotte;Simone Tini, 2018, Weak Bisimulation Metrics in Models with Nondeterminism and Continuous State Spaces, Lecture notes in computer science, pp. 292-312, 10.1007/978-3-030-02508-3_16.

Daniel Gebler;Simone Tini, 2017, SOS specifications for uniformly continuous operators, Journal of Computer and System Sciences, 92, pp. 113-151, 10.1016/j.jcss.2017.09.011.

Ruggero Lanotte;Massimo Merro;Simone Tini, 2017, Weak Simulation Quasimetric in a Gossip Scenario, pp. 139-155, 10.1007/978-3-319-60225-7_10, https://inria.hal.science/hal-01658428.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3694 times.

This article's PDF has been downloaded 960 times.