Axiomatizing bisimulation equivalences and metrics from probabilistic SOS rules
Fil: D'Argenio, Pedro Ruben. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina.
| Main Authors: | , , |
|---|---|
| Format: | publishedVersion |
| Language: | eng |
| Published: |
2023
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/11086/30135 http://dx.doi.org/10.1007/978-3-642-54830-7_19 |
| _version_ | 1801211198977343488 |
|---|---|
| author | D'Argenio, Pedro Ruben Gebler, Daniel Lee, Matías David |
| author_facet | D'Argenio, Pedro Ruben Gebler, Daniel Lee, Matías David |
| author_sort | D'Argenio, Pedro Ruben |
| collection | Repositorio Digital Universitario |
| description | Fil: D'Argenio, Pedro Ruben. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. |
| format | publishedVersion |
| id | rdu-unc.30135 |
| institution | Universidad Nacional de Cordoba |
| language | eng |
| publishDate | 2023 |
| record_format | dspace |
| spelling | rdu-unc.301352023-03-20T16:49:23Z Axiomatizing bisimulation equivalences and metrics from probabilistic SOS rules D'Argenio, Pedro Ruben Gebler, Daniel Lee, Matías David Axiomatization Bisimulation Probability Structured Operational Semantics Probabilistic Transition Systems publishedVersion Fil: D'Argenio, Pedro Ruben. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. Fil: D'Argenio, Pedro Ruben. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina. Fil: Lee, Matías David. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. Fil: Lee, Matías David. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina. Fil: Gebler, Daniel. Universidad Libre de Ámsterdam; Países Bajos. Probabilistic transition system specifications (PTSS) provide structural operational semantics for reactive probabilistic labeled transition systems. Bisimulation equivalences and bisimulation metrics are fundamental notions to describe behavioral relations and distances of states, respectively. We provide a method to generate from a PTSS a sound and ground-complete equational axiomatization for strong and convex bisimilarity. The construction is based on the method of Aceto, Bloom and Vaandrager developed for non-deterministic transition system specifications. The novelty in our approach is to employ many-sorted algebras to axiomatize separately non-deterministic choice, probabilistic choice and their interaction. Furthermore, we generalize this method to axiomatize the strong and convex metric bisimulation distance of PTSS. Supported by ANPCYT PICT 2012-1823, SeCyT-UNC 05/B497 and 05/BP02, Eramus Mundus Action 2 Lot 13A EU Mobility Programme 2010-2401/001-001-EMA2 and EU 7FP grant agreement 295261 (MEALS). publishedVersion Fil: D'Argenio, Pedro Ruben. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. Fil: D'Argenio, Pedro Ruben. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina. Fil: Lee, Matías David. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. Fil: Lee, Matías David. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina. Fil: Gebler, Daniel. Universidad Libre de Ámsterdam; Países Bajos. Ciencias de la Computación 2023-01-30T18:15:40Z 2023-01-30T18:15:40Z 2014 article http://hdl.handle.net/11086/30135 http://dx.doi.org/10.1007/978-3-642-54830-7_19 eng Attribution-NonCommercial-NoDerivatives 4.0 International http://creativecommons.org/licenses/by-nc-nd/4.0/ Impreso; Electrónico y/o Digital ISSN: 0302-9743 |
| spellingShingle | Axiomatization Bisimulation Probability Structured Operational Semantics Probabilistic Transition Systems D'Argenio, Pedro Ruben Gebler, Daniel Lee, Matías David Axiomatizing bisimulation equivalences and metrics from probabilistic SOS rules |
| title | Axiomatizing bisimulation equivalences and metrics from probabilistic SOS rules |
| title_full | Axiomatizing bisimulation equivalences and metrics from probabilistic SOS rules |
| title_fullStr | Axiomatizing bisimulation equivalences and metrics from probabilistic SOS rules |
| title_full_unstemmed | Axiomatizing bisimulation equivalences and metrics from probabilistic SOS rules |
| title_short | Axiomatizing bisimulation equivalences and metrics from probabilistic SOS rules |
| title_sort | axiomatizing bisimulation equivalences and metrics from probabilistic sos rules |
| topic | Axiomatization Bisimulation Probability Structured Operational Semantics Probabilistic Transition Systems |
| url | http://hdl.handle.net/11086/30135 http://dx.doi.org/10.1007/978-3-642-54830-7_19 |
| work_keys_str_mv | AT dargeniopedroruben axiomatizingbisimulationequivalencesandmetricsfromprobabilisticsosrules AT geblerdaniel axiomatizingbisimulationequivalencesandmetricsfromprobabilisticsosrules AT leematiasdavid axiomatizingbisimulationequivalencesandmetricsfromprobabilisticsosrules |