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.

Comment: 33 pages

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

49 Documents citing this article

Hitoshi Furusawa;Walter Guttmann;Georg Struth, 2024, Modal algebra of multirelations, Journal of Logic and Computation, 35, 3, 10.1093/logcom/exae023, https://doi.org/10.1093/logcom/exae023.

Xian Xu;Wenbo Zhang, 2024, Logical Characterization of Uniformly Random Processes, SSRN Electronic Journal, 10.2139/ssrn.4874972, http://dx.doi.org/10.2139/ssrn.4874972.

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, Electronic Proceedings in Theoretical Computer Science, 368, pp. 3-22, 10.4204/eptcs.368.1, https://doi.org/10.4204/eptcs.368.1.

Rob van Glabbeek, 2022, Fair Must Testing for I/O Automata, Edinburgh Research Explorer (University of Edinburgh), pp. 559-574, 10.1007/978-3-031-15629-8_30, https://www.research.ed.ac.uk/en/publications/da8988e3-ac6e-4ed8-a6e9-424df212f89a.

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.

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, arXiv (Cornell University), 109, pp. 100480, 10.1016/j.jlamp.2019.100480, http://arxiv.org/abs/1912.05616.

Rob van Glabbeek, 2019, Reward Testing Equivalences for Processes, arXiv (Cornell University), pp. 45-70, 10.1007/978-3-030-21485-2_5, http://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.

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

Marcus Gerhold;Arnd Hartmanns;Mariëlle Stoelinga, 2018, Model-Based Testing for General Stochastic Time, Data Archiving and Networked Services (DANS), pp. 203-219, 10.1007/978-3-319-77935-5_15, https://research.utwente.nl/en/publications/29fa417e-09f5-4294-b249-c69277212c82.

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

Valentina Castiglioni, 2018, Trace and Testing Metrics on Nondeterministic Probabilistic Processes, Electronic Proceedings in Theoretical Computer Science, 276, pp. 19-36, 10.4204/eptcs.276.4, https://doi.org/10.4204/eptcs.276.4.

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

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://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, http://hdl.handle.net/2066/159573.

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

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

Valentina Castiglioni;Daniel Gebler;Simone Tini, 2016, Logical Characterization of Bisimulation Metrics, Electronic Proceedings in Theoretical Computer Science, 227, pp. 44-62, 10.4204/eptcs.227.4, https://doi.org/10.4204/eptcs.227.4.

Bart Jacobs;Alexandra Silva;Ana Sokolova, 2014, Trace semantics via determinization, Journal of Computer and System Sciences, 81, 5, pp. 859-879, 10.1016/j.jcss.2014.12.005.

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

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

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.

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, 2014, Probabilistic Bisimulation, Semantics of Probabilistic Processes, pp. 23-69, 10.1007/978-3-662-45198-4_3.

Joost-Pieter Katoen, 2013, Concurrency Meets Probability: Theory and Practice, Lecture notes in computer science, pp. 44-45, 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, Electronic Proceedings in Theoretical Computer Science, 117, pp. 81-96, 10.4204/eptcs.117.6, https://doi.org/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.

Bart Jacobs;Alexandra Silva;Ana Sokolova, 2012, Trace Semantics via Determinization, Lecture notes in computer science, pp. 109-129, 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, 2012, Revisiting Trace and Testing Equivalences for Nondeterministic and Probabilistic Processes, Lecture notes in computer science, pp. 195-209, 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, 2012, A UTP Semantics of pGCL as a Homogeneous Relation, Lecture notes in computer science, pp. 191-205, 10.1007/978-3-642-30729-4_14.

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, Formal Aspects of Computing, 24, 4-6, pp. 701-726, 10.1007/s00165-012-0238-3.

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

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

Silvia Crafa;Francesco Ranzato, 2011, A Spectrum of Behavioral Relations over LTSs on Probability Distributions, Lecture notes in computer science, pp. 124-139, 10.1007/978-3-642-23217-6_9.

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), Electronic Proceedings in Theoretical Computer Science, 57, pp. 61-73, 10.4204/eptcs.57.5, https://doi.org/10.4204/eptcs.57.5.

Robert M. Hierons;Manuel Núñez, 2010, Testing Probabilistic Distributed Systems, pp. 63-77, 10.1007/978-3-642-13464-7_6, https://inria.hal.science/hal-01055146.

Sonja Georgievska;Suzana Andova, 2010, Testing Reactive Probabilistic Processes, Electronic Proceedings in Theoretical Computer Science, 28, pp. 99-113, 10.4204/eptcs.28.7, https://doi.org/10.4204/eptcs.28.7.

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

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

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

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3342 times.

This article's PDF has been downloaded 532 times.