×
Bian, Gaoang; Abate, Alessandro

On the relationship between bisimulation and trace equivalence in an approximate probabilistic context. (English) Zbl 1486.68108

Esparza, Javier (ed.) et al., Foundations of software science and computation structures. 20th international conference, FOSSACS 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 10203, 321-337 (2017).
Summary: This work introduces a notion of approximate probabilistic trace equivalence for labelled Markov chains, and relates this new concept to the known notion of approximate probabilistic bisimulation. In particular this work shows that the latter notion induces a tight upper bound on the approximation between finite-horizon traces, as expressed by a total variation distance. As such, this work extends corresponding results for exact notions and analogous results for non-probabilistic models. This bound can be employed to relate the closeness in satisfaction probabilities over bounded linear-time properties, and allows for probabilistic model checking of concrete models via abstractions. The contribution focuses on both finite-state and uncountable-state labelled Markov chains, and claims two main applications: firstly, it allows an upper bound on the trace distance to be decided for finite state systems; secondly, it can be used to synthesise discrete approximations to continuous-state models with arbitrary precision.
For the entire collection see [Zbl 1360.68010].

Cited in 6 Documents

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
60J20 Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.)
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)

Software:

PRISM
Cite Review PDF
Full Text: DOI arXiv

References:

[1] Abate, A.: Approximation metrics based on probabilistic bisimulations for general state-space Markov processes: a survey. Electron. Notes Theor. Comput. Sci. 297, 3–25 (2013) · Zbl 1334.68128 · doi:10.1016/j.entcs.2013.12.002
[2] Abate, A., Katoen, J.P., Lygeros, J., Prandini, M.: Approximate model checking of stochastic hybrid systems. Eur. J. Control 16(6), 624–641 (2010) · Zbl 1216.93091 · doi:10.3166/ejc.16.624-641
[3] Abate, A., Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic model checking of labelled Markov processes via finite approximate bisimulations. In: Breugel, F., Kashefi, E., Palamidessi, C., Rutten, J. (eds.) Horizons of the Mind. A Tribute to Prakash Panangaden. LNCS, vol. 8464, pp. 40–58. Springer, Cham (2014). doi: 10.1007/978-3-319-06880-0_2 · Zbl 1407.68275 · doi:10.1007/978-3-319-06880-0_2
[4] Bian, G., Abate, A.: On the relationship between bisimulation and trace equivalence in an approximate probabilistic context (extended version) (2017). http://arxiv.org/abs/1701.04547 · Zbl 1486.68108
[5] Bollobás, B., Varopoulos, N.: Representation of systems of measurable sets. Math. Proc. Cambridge Philos. Soc. 78(02), 323–325 (1975) · Zbl 0304.28001 · doi:10.1017/S0305004100051756
[6] Buchholz, P.: Exact and ordinary lumpability in finite Markov chains. J. Appl. Probab. 31, 59–75 (1994) · Zbl 0796.60073 · doi:10.1017/S0021900200107338
[7] Castro, P.S., Panangaden, P., Precup, D.: Notions of state equivalence under partial observability. In: IJCAI (2009)
[8] Chen, D., Breugel, F., Worrell, J.: On the complexity of computing probabilistic bisimilarity. In: Birkedal, L. (ed.) FoSSaCS 2012. LNCS, vol. 7213, pp. 437–451. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-28729-9_29 · Zbl 1352.68096 · doi:10.1007/978-3-642-28729-9_29
[9] Chen, T., Kiefer, S.: On the total variation distance of labelled Markov chains. In: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), p. 33. ACM (2014) · Zbl 1395.68202 · doi:10.1145/2603088.2603099
[10] Comanici, G., Panangaden, P., Precup, D.: On-the-fly algorithms for bisimulation metrics. In: 2012 Ninth International Conference on Quantitative Evaluation of Systems (QEST), pp. 94–103. IEEE (2012) · doi:10.1109/QEST.2012.30
[11] Daca, P., Henzinger, T.A., Kretínský, J., Petrov, T.: Linear distances between markov chains. In: 27th International Conference on Concurrency Theory, CONCUR 2016, Québec City, Canada, 23–26 August 2016, pp. 20:1–20:15 (2016) · Zbl 1392.68293
[12] Desharnais, J., Edalat, A., Panangaden, P.: Bisimulation for labelled Markov processes. Inf. Comput. 179(2), 163–193 (2002) · Zbl 1096.68103 · doi:10.1006/inco.2001.2962
[13] Desharnais, J., Laviolette, F., Tracol, M.: Approximate analysis of probabilistic processes: logic, simulation and games. In: Fifth International Conference on Quantitative Evaluation of Systems, QEST 2008, pp. 264–273. IEEE (2008) · doi:10.1109/QEST.2008.42
[14] D’Innocenzo, A., Abate, A., Katoen, J.P.: Robust PCTL model checking. In: Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control, pp. 275–286. ACM (2012) · Zbl 1361.68140 · doi:10.1145/2185632.2185673
[15] Durrett, R.: Probability: Theory and Examples, 3rd edn. Duxbury Press, Pacific Grove (2004) · Zbl 1202.60001
[16] Esmaeil Zadeh Soudjani, S., Abate, A.: Adaptive and sequential gridding procedures for the abstraction and verification of stochastic processes. SIAM J. Appl. Dyn. Syst. 12(2), 921–956 (2013) · Zbl 1278.93243 · doi:10.1137/120871456
[17] Gebler, D., Tini, S.: Compositionality of approximate bisimulation for probabilistic systems. In: EXPRESS/SOS 2013, pp. 32–46 (2013)
[18] Gibbs, A.L., Su, F.E.: On choosing and bounding probability metrics. Int. Stat. Rev. 70(3), 419–435 (2002) · Zbl 1217.62014 · doi:10.1111/j.1751-5823.2002.tb00178.x
[19] Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-22110-1_47 · doi:10.1007/978-3-642-22110-1_47
[20] Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. In: Conference Record of the 16th ACM Symposium on Principles of Programming Languages, POPL 1989, pp. 344–352 (1989) · Zbl 0756.68035
[21] Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. Nord. J. Comput. 2(2), 250–273 (1995) · Zbl 0839.68067
[22] Spears, W.M.: A compression algorithm for probability transition matrices. SIAM J. Matrix Anal. Appl. 20(1), 60–77 (1998) · Zbl 0922.65032 · doi:10.1137/S0895479897316916
[23] Sproston, J., Donatelli, S.: Backward bisimulation in Markov chain model checking. IEEE Trans. Softw. Eng. 32(8), 531–546 (2006) · doi:10.1109/TSE.2006.74
[24] Tang, Q., van Breugel, F.: Computing probabilistic bisimilarity distances viapolicy iteration. In: 27th International Conference on Concurrency Theory, CONCUR 2016, 23-26 August 2016, Québec City, Canada, pp. 22:1–22:15 (2016) · Zbl 1392.68316
[25] Tkachev, I., Abate, A.: Formula-free finite abstractions for linear temporal verification of stochastic hybrid systems. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, pp. 283–292. ACM (2013) · Zbl 1362.68187 · doi:10.1145/2461328.2461372
[26] Wu, H., Noé, F.: Probability distance based compression of hidden Markov models. Multiscale Model. Simul. 8(5), 1838–1861 (2010) · Zbl 1210.65018 · doi:10.1137/090774161
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.