Published in Volume XXX, Issue 1, 2020, pages 69-104, doi: 10.7561/SACS.2020.1.69
Authors: F. Timmers, J.F. Groote
Abstract
We provide an axiomatisation for =pTr , a variant of probabilistic trace equivalence as formulated by Bernardo et al., 2014, in the setting of the alternating model of Hansson. The equivalence considers traces individually instead of trace distributions. We show that our axiomatisation is sound and also complete for recursion-free sequential processes. Due to the nature of the trace equivalence, the axiomatisation is particularly complex.
Full Text (PDF)References
[1] E. Bandini, R. Segala. Axiomatizations for Probabilistic Bisimulation. In F. Orejas, P.G. Spirakis, J. van Leeuwen (Eds.) 28th International Colloquium on Automata, Languages, and Programming (ICALP 2001), Lecture Notes in Computer Science 2076, 370-381, 2001. doi:10.1007/3-540-48224-5\_31.
[2] J.A. Bergstra, J.W. Klop. ACPτ a Universal Axiom System for Process Specification. In M. Wirsing J.A. Bergstra (Eds.) Workshop on Algebraic Methods: Theory, Tools and Applications, Lecture Notes in Computer Science 394, 445-463, 1987. doi:10.1007/BFb0015048.
[3] M. Bernardo. Coherent Resolutions of Nondeterminism. In M. Gribaudo, M. Iacono, T. Phung-Duc, R. Razumchik (Eds.) 16th European Workshop on Computer Performance Engineering (EPEW
2019), Lecture Notes in Computer Science 12039, 16-32, 2019. doi:10.1007/978-3-030-44411-2\_2.
[4] M. Bernardo, R. De Nicola, M. Loreti. Revisiting Trace and Testing Equivalences for Nondeterministic and Probabilistic Processes. Logical Methods in Computer Science (LMCS) 10(1), 2014. doi:10.2168/LMCS-10(1:16)2014.
[5] V. Castiglioni, M. Loreti, S. Tini. The Metric Linear-time Branching-time Spectrum on Nondeterministic Probabilistic Pprocesses. Theoretical Computer Science 813, 20-69, 2020. doi:10.1016/j.tcs.2019.09.019.
[6] L. Cheung, N. A. Lynch, R. Segala, F. W. Vaandrager. Switched PIOA: Parallel Composition via Distributed Scheduling. Theoretical Computer Science 365(1-2), 83-108, 2006. doi:10.1016/j.tcs.2006.07.033.
[7] L. De Alfaro, T.A. Henzinger, R. Jhala. Compositional Methods for Probabilistic Systems. In K.G. Larsen, M. Nielsen (Eds.) 12th International Conference on Concurrency Theory (CONCUR 2001), Lecture Notes in Computer Science 2154, 351-365, 2001. doi:10.1007/3-540-44685-0\_24.
[8] S. Georgievska, S. Andova. Probabilistic May/Must Testing: Retaining Probabilities by Restricted Schedulers. Formal Aspects of Computing 24(4-6), 727-748, 2012. doi:10.1007/s00165-012-0236-5.
[9] S. Giro, P.R. D’Argenio. On the Expressive Power of Schedulers in Distributed Probabilistic Systems. Electronic Notes in Theoretical Computer Science 253(3), 45-71, 2009. doi:10.1016/j.entcs.2009.10.005.
[10] R.J. van Glabbeek. Notes on the Methodology of CCS and CSP. Theoretical Computer Science 177(2), 329{349, 1997. doi:10.1016/S0304-3975(96)00251-4.
[11] R.J. van Glabbeek, S.A. Smolka, B. Steffen. Reactive, Generative, and Stratified Models of Probabilistic Processes. Information and Computation 121(1), 59-80, 1995. doi:10.1006/inco.1995.1123.
[12] J.F. Groote. Transition System Specifications with Negative Premises (Extended Abstract). In J.C. M. Baeten, J.W. Klop (Eds.) 1st International Conference on Concurrency Theory (CONCUR 1990), Lecture Notes in Computer Science 458, 332-341, 1990. doi:10.1007/BFb0039069.
[13] H.A. Hansson. Time and Probability in Formal Design of Distributed Systems. PhD Thesis, University Uppsala, Sweden, 1991.
[14] H.A. Hansson, B. Jonsson. A Calculus for Communicating Systems with Time and Probabilities. In 11th Real-Time Systems Symposium, IEEE Computer Society, 278-287, 1990. doi:10.1109/REAL.1990.128759.
[15] M. Hennessy, R. Milner. Algebraic Laws for Nondeterminism and Concurrency. Journal of the ACM 32(1), 137{161, 1985. doi:10.1145/2455.2460.
[16] K.G Larsen, A. Skou. Bisimulation Through Probabilistic Testing. Information and Computation 94(1), 1-28, 1991. doi:10.1016/0890-5401(91)90030-6.
[17] N.A. Lynch, R. Segala, F.W. Vaandrager. Compositionality for Probabilistic Automata. In R. Amadio, D. Lugiez (Eds.) 14th International Conference on Concurrency Theory (CONCUR 2003), Lecture Notes in Computer Science 2761, 204-222, 2003. doi:10.1007/978-3-540-45187-7\_14.
[18] R. Milner. Communication and Concurrency. PHI Series in computer science. Prentice Hall, 1989.
[19] A. Parma, R. Segala. Axiomatization of Trace Semantics for Stochastic Nondeterministic Processes. In First International Conference on the Quantitative Evaluation of Systems (QEST 2004), IEEE, 294-303, 2004. doi:10.1109/QEST.2004.1348043.
[20] R. Segala. A Compositional Trace-based Semantics for Probabilistic Automata. In I. Lee, S.A. Smolka (Eds.) 6th International Conference on Concurrency Theory, Lecture Notes in Computer Science 962, 234-248, 1995. doi:10.1007/3-540-60218-6_17.
[21] R. Segala. Modeling and Verification of Randomized Distributed Real-time Systems. PhD Thesis, Massachusetts Institute of Technology,1995.
[22] R. Segala, N.A. Lynch. Probabilistic Simulations for Probabilistic Processes. Nordic Journal of Computing 2(2). 250{273, 1995.
[23] R. Segala, A. Turrini. Comparative Analysis of Bisimulation Relations on Alternating and Non-alternating Probabilistic Models. In 2nd International Conference on the Quantitative Evaluation of Systems (QEST 2005), IEEE Computer Society 44-53. 2005. doi:10.1109/QEST.2005.9.
[24] A. Silva, A. Sokolova. Sound and Complete Axiomatization of Trace Semantics for Probabilistic Systems. Electronic Notes in Theoretical Computer Science 276, 291-311, 2011. doi:10.1016/j.entcs.2011.09.027.
[25] A. Sokolova, E.P. de Vink. Probabilistic Automata: System Types, Parallel Composition and Comparison. In C. Baier, B.R. Haverkort, H. Hermanns, J.P. Katoen, M. Siegle (Eds.) Validation of Stochastic Systems , Lecture Notes in Computer Science 2925, 1-43, 2004. doi:10.1007/978-3-540-24611-4_1.
[26] F. Timmers. A Sound and Complete Axiomatisation of Probabilistic Trace Equivalence. Master’s Thesis, Eindhoven University of Technology, The Netherlands, 2018.
Bibtex
@article{sacscuza:timmers20acapte,
title={A Complete Axiomatisation for Probabilistic Trace Equivalence},
author={F. Timmers, J.F. Groote},
journal={Scientific Annals of Computer Science},
volume={30},
number={1},
organization={Alexandru Ioan Cuza University, Ia\c si, Rom\^ania},
year={2020},
pages={69–104},
publisher={Alexandru Ioan Cuza University Press, Ia\c si},
doi={10.7561/SACS.2020.1.69}
}