Characterising Testing Preorders for Finite Probabilistic Processes

Yuxin Deng; Matthew Hennessy; Rob van Glabbeek; Carroll Morgan

doi:10.2168/LMCS-4(4:4)2008

Yuxin Deng ; Matthew Hennessy ; Rob van Glabbeek ; Carroll Morgan - Characterising Testing Preorders for Finite Probabilistic Processes

lmcs:694 - Logical Methods in Computer Science, October 28, 2008, Volume 4, Issue 4 - https://doi.org/10.2168/LMCS-4(4:4)2008

Characterising Testing Preorders for Finite Probabilistic ProcessesArticle

Authors: Yuxin Deng ; Matthew Hennessy ; Rob van Glabbeek ; Carroll Morgan

In 1992 Wang & Larsen extended the may- and must preorders of De Nicola and Hennessy to processes featuring probabilistic as well as nondeterministic choice. They concluded with two problems that have remained open throughout the years, namely to find complete axiomatisations and alternative characterisations for these preorders. This paper solves both problems for finite processes with silent moves. It characterises the may preorder in terms of simulation, and the must preorder in terms of failure simulation. It also gives a characterisation of both preorders using a modal logic. Finally it axiomatises both preorders over a probabilistic version of CSP.

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

Source: arXiv.org:0810.3708

Volume: Volume 4, Issue 4

Published on: October 28, 2008

Imported on: February 7, 2008

Keywords: Computer Science - Logic in Computer Science,F.3.2,D.3.1

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

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

48 Documents citing this article

Manuel Núñez;Robert M. Hierons;Raluca Lefticaru, 2023, Implementation relations and testing for cyclic systems: Adding probabilities, Robotics and Autonomous Systems, 165, pp. 104426, 10.1016/j.robot.2023.104426, https://doi.org/10.1016/j.robot.2023.104426.

Valentina Castiglioni;Ruggero Lanotte;Simone Tini, 2023, Back to the format: A survey on SOS for probabilistic processes, Journal of Logical and Algebraic Methods in Programming, 137, pp. 100929, 10.1016/j.jlamp.2023.100929, https://doi.org/10.1016/j.jlamp.2023.100929.

Clément Aubert;Ross Horne;Christian Johansen, 2022, Bisimulations Respecting Duration and Causality for the Non-interleaving Applied π-Calculus, arXiv (Cornell University), 368, pp. 3-22, 10.4204/eptcs.368.1.

Rob van Glabbeek, arXiv (Cornell University), Fair Must Testing for I/O Automata, pp. 559-574, 2022, 10.1007/978-3-031-15629-8_30, https://arxiv.org/abs/2212.11248.

Ruggero Lanotte;Simone Tini, 2021, A weak semantic approach to bisimulation metrics in models with nondeterminism and continuous state spaces, Theoretical Computer Science, 869, pp. 29-61, 10.1016/j.tcs.2020.12.045.

Ruggero Lanotte;Massimo Merro;Simone Tini, 2020, A probabilistic calculus of cyber-physical systems, arXiv (Cornell University), 279, pp. 104618, 10.1016/j.ic.2020.104618, https://arxiv.org/abs/1707.02279.

Valentina Castiglioni;Simone Tini, 2020, Raiders of the lost equivalence: Probabilistic branching bisimilarity, Information Processing Letters, 159-160, pp. 105947, 10.1016/j.ipl.2020.105947.

Marcus Gerhold;Arnd Hartmanns;Mariëlle Stoelinga, 2019, Model-based testing of stochastically timed systems, Innovations in Systems and Software Engineering, 15, 3-4, pp. 207-233, 10.1007/s11334-019-00349-z, https://doi.org/10.1007/s11334-019-00349-z.

Rob van Glabbeek, 2019, Ensuring liveness properties of distributed systems: Open problems, Journal of Logical and Algebraic Methods in Programming, 109, pp. 100480, 10.1016/j.jlamp.2019.100480, https://doi.org/10.1016/j.jlamp.2019.100480.

Rob van Glabbeek, arXiv (Cornell University), Reward Testing Equivalences for Processes, pp. 45-70, 2019, 10.1007/978-3-030-21485-2_5, https://arxiv.org/abs/1907.13348.

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;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.

Marcus Gerhold;Arnd Hartmanns;Mariëlle Stoelinga, Lecture notes in computer science, Model-Based Testing for General Stochastic Time, pp. 203-219, 2018, 10.1007/978-3-319-77935-5_15.

Marcus Gerhold;Mariëlle Stoelinga, 2018, Model-based testing of probabilistic systems, Formal Aspects of Computing, 30, 1, pp. 77-106, 10.1007/s00165-017-0440-4, https://doi.org/10.1007/s00165-017-0440-4.

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

Valentina Castiglioni, 2018, Trace and Testing Metrics on Nondeterministic Probabilistic Processes, arXiv (Cornell University), 276, pp. 19-36, 10.4204/eptcs.276.4.

Marcus Gerhold;Mariëlle Stoelinga, Lecture notes in computer science, Model-Based Testing of Probabilistic Systems with Stochastic Time, pp. 77-97, 2017, 10.1007/978-3-319-61467-0_5.

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

Lijun Zhang;David N. Jansen, 2016, A space-efficient simulation algorithm on probabilistic automata, Data Archiving and Networked Services (DANS), 249, pp. 138-159, 10.1016/j.ic.2016.04.002, https://hdl.handle.net/2066/159573.

Marcus Gerhold;Mariëlle Stoelinga, Proceedings of the 7th International Workshop on Automating Test Case Design, Selection, and Evaluation, Model-based testing of stochastic systems with IOCO theory, pp. 45-51, 2016, Seattle WA USA, 10.1145/2994291.2994298.

Marcus Gerhold;Mariëlle Stoelinga, Lecture notes in computer science, Model-Based Testing of Probabilistic Systems, pp. 251-268, 2016, 10.1007/978-3-662-49665-7_15.

Valentina Castiglioni;Daniel Gebler;Simone Tini, 2016, Logical Characterization of Bisimulation Metrics, arXiv (Cornell University), 227, pp. 44-62, 10.4204/eptcs.227.4.

Bart Jacobs;Alexandra Silva;Ana Sokolova, 2014, Trace semantics via determinization, 81, 5, pp. 859-879, 10.1016/j.jcss.2014.12.005, https://hal.inria.fr/hal-01539887/file/978-3-642-32784-1_7_Chapter.pdf.

Marco Bernardo;Davide Sangiorgi;Valeria Vignudelli, On the discriminating power of passivation and higher-order interaction, pp. 1-10, 2014, Vienna Austria, 10.1145/2603088.2603113, https://hal.inria.fr/hal-01089467.

Marco Bernardo;Davide Sangiorgi;Valeria Vignudelli, On the Discriminating Power of Testing Equivalences for Reactive Probabilistic Systems: Results and Open Problems, pp. 281-296, 2014, 10.1007/978-3-319-10696-0_23, https://hal.inria.fr/hal-01089484.

Marco Bernardo;Rocco De Nicola;Michele Loreti, 2014, Relating strong behavioral equivalences for processes with nondeterminism and probabilities, Theoretical Computer Science, 546, pp. 63-92, 10.1016/j.tcs.2014.03.001, https://doi.org/10.1016/j.tcs.2014.03.001.

Silvia Crafa;Francesco Ranzato, 2014, Logical Characterizations of Behavioral Relations on Transition Systems of Probability Distributions, Padua Research Archive (University of Padua), 16, 1, pp. 1-24, 10.1145/2641566, http://hdl.handle.net/11577/2961100.

Yuxin Deng, Springer eBooks, Probabilistic Bisimulation, pp. 23-69, 2014, 10.1007/978-3-662-45198-4_3.

Joost-Pieter Katoen, Lecture notes in computer science, Concurrency Meets Probability: Theory and Practice, pp. 44-45, 2013, 10.1007/978-3-642-40184-8_4.

Marco Bernardo;Rocco De Nicola;Michele Loreti, 2013, The Spectrum of Strong Behavioral Equivalences for Nondeterministic and Probabilistic Processes, arXiv (Cornell University), 117, pp. 81-96, 10.4204/eptcs.117.6.

Yuxin Deng;Rob van Glabbeek;Matthew Hennessy;Carroll Morgan, 2013, Real-reward testing for probabilistic processes, Theoretical Computer Science, 538, pp. 16-36, 10.1016/j.tcs.2013.07.016, https://doi.org/10.1016/j.tcs.2013.07.016.

Bart Jacobs;Alexandra Silva;Ana Sokolova, Lecture notes in computer science, Trace Semantics via Determinization, pp. 109-129, 2012, 10.1007/978-3-642-32784-1_7, https://doi.org/10.1007/978-3-642-32784-1_7.

Marco Bernardo;Rocco De Nicola;Michele Loreti, Lecture notes in computer science, Revisiting Trace and Testing Equivalences for Nondeterministic and Probabilistic Processes, pp. 195-209, 2012, 10.1007/978-3-642-28729-9_13, https://doi.org/10.1007/978-3-642-28729-9_13.

P. Höfner, 2012, Preface, Formal Aspects of Computing, 24, 4-6, pp. 417-422, 10.1007/s00165-012-0257-0, https://doi.org/10.1007/s00165-012-0257-0.

Riccardo Bresciani;Andrew Butterfield, University of Limerick Institutional Repository (University of Limerick), A UTP Semantics of pGCL as a Homogeneous Relation, pp. 191-205, 2012, 10.1007/978-3-642-30729-4_14, http://hdl.handle.net/10344/2607.

Robert M. Hierons;Manuel Núñez, 2012, Using schedulers to test probabilistic distributed systems, Formal Aspects of Computing, 24, 4-6, pp. 679-699, 10.1007/s00165-012-0244-5.

Sonja Georgievska;Suzana Andova, 2012, Probabilistic may/must testing: retaining probabilities by restricted schedulers, Formal Aspects of Computing, 24, 4-6, pp. 727-748, 10.1007/s00165-012-0236-5, https://doi.org/10.1007/s00165-012-0236-5.

Yuxin Deng;Alwen Tiu, 2012, Characterisations of testing preorders for a finite probabilistic π -calculus, arXiv (Cornell University), 24, 4-6, pp. 701-726, 10.1007/s00165-012-0238-3, https://arxiv.org/abs/1201.2258.

Lucia Acciai;Michele Boreale;Rocco De Nicola, Linear-Time and May-Testing in a Probabilistic Reactive Setting, pp. 29-43, 2011, 10.1007/978-3-642-21461-5_2, https://inria.hal.science/hal-01583326.

Ruggero Lanotte;Massimo Merro, Lecture notes in computer science, Semantic Analysis of Gossip Protocols for Wireless Sensor Networks, pp. 156-170, 2011, 10.1007/978-3-642-23217-6_11.

Silvia Crafa;Francesco Ranzato, Research Padua Archive (University of Padua), A Spectrum of Behavioral Relations over LTSs on Probability Distributions, pp. 124-139, 2011, 10.1007/978-3-642-23217-6_9, http://www.math.unipd.it/~ranzato/papers.html.

Wei-zhong Yang;Yu-xin Deng, 2011, On real reward testing, Journal of Shanghai Jiaotong University (Science), 16, 4, pp. 479-484, 10.1007/s12204-011-1176-6.

Yuxin Deng;Rob van Glabbeek;Matthew Hennessy;Carroll Morgan, 2011, Real-Reward Testing for Probabilistic Processes (Extended Abstract), arXiv (Cornell University), 57, pp. 61-73, 10.4204/eptcs.57.5.

Robert M. Hierons;Manuel Núñez, Lecture notes in computer science, Testing Probabilistic Distributed Systems, pp. 63-77, 2010, 10.1007/978-3-642-13464-7_6, https://doi.org/10.1007/978-3-642-13464-7_6.

Sonja Georgievska;Suzana Andova, 2010, Testing Reactive Probabilistic Processes, arXiv (Cornell University), 28, pp. 99-113, 10.4204/eptcs.28.7.

Yuxin Deng;Rob van Glabbeek, arXiv (Cornell University), Characterising Probabilistic Processes Logically, pp. 278-293, 2010, 10.1007/978-3-642-16242-8_20, https://arxiv.org/abs/1007.5188.

Michele Boreale, Lecture notes in computer science, Weighted Bisimulation in Linear Algebraic Form, pp. 163-177, 2009, 10.1007/978-3-642-04081-8_12.

Yuxin Deng;Rob van Glabbeek;Matthew Hennessy;Carroll Morgan, Lecture notes in computer science, Testing Finitary Probabilistic Processes, pp. 274-288, 2009, 10.1007/978-3-642-04081-8_19.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 1925 times.

This article's PDF has been downloaded 380 times.