Abstract
Several notions of bisimulation relations for probabilistic nondeterministic transition systems have been considered in the literature. We study a novel testing-based behavioral equivalence called upper expectation bisimilarity and, using standard results from functional analysis, we develop its coalgebraic and algebraic theory and provide a logical characterization in terms of an expressive probabilistic modal μ-calculus.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press (2008)
Bartels, F.: On Generalised Coinduction and Probabilistic Specification Formats: Distributive Laws in Coalgebraic Modelling. PhD thesis, CWI (2004)
Bernardo, M., De Nicola, R., Loreti, M.: Revisiting trace and testing equivalences for nondeterministic and probabilistic processes. In: Birkedal, L. (ed.) FOSSACS 2012. LNCS, vol. 7213, pp. 195–209. Springer, Heidelberg (2012)
Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499–513. Springer, Heidelberg (1995)
Chatzikokolakis, K., Palamidessi, C., Panangaden, P.: On the Bayes risk in information-hiding protocols. Journal of Computer Security 16(5) (2008)
Crafa, S., Ranzato, F.: A spectrum of behavioral relations over LTSs on probability distributions. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 124–139. Springer, Heidelberg (2011)
D’Argenio, P.R., Gebler, D., Lee, M.D.: Axiomatizing bisimulation equivalences and metrics from probabilistic SOS rules. In: Muscholl, A. (ed.) FOSSACS 2014. LNCS, vol. 8412, pp. 289–303. Springer, Heidelberg (2014)
de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. Journal of Computer and System Sciences 68, 374–397 (2004)
de Alfaro, L., Majumdar, R., Raman, V., Stoelinga, M.: Game refinement relations and metrics. Logical Methods in Computer Science 4 (2008)
Deng, Y., van Glabbeek, R.: Characterising probabilistic processes logically. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 278–293. Springer, Heidelberg (2010)
Deng, Y., van Glabbeek, R., Hennessy, M., Morgan, C.: Testing finitary probabilistic processes. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 274–288. Springer, Heidelberg (2009)
Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Weak bisimulation is sound and complete for PCTL. In: Brim, L., Jančar, P., Křetínský, M., Kučera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 355–370. Springer, Heidelberg (2002)
Goubault-Larrecq, J.: Prevision domains and convex powercones. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 318–333. Springer, Heidelberg (2008)
Huber, P.: Robust Statistics. Wiley (1991)
Huth, M., Kwiatkowska, M.: Quantitative analysis and model checking. In: Proc. of LICS (1997)
Kechris, A.S.: Classical Descriptive Set Theory. Springer (1994)
Kozen, D.: Results on the propositional mu-calculus. Theoretical Computer Science, 333–354 (1983)
Kurz, A.: Logics for Coalgebras and Applications to Computer Science. PhD thesis, Ludwig Maximilian University of Munich (2000)
Lax, P.: Functional Analysis. Wiley Interscience (2002)
Lynch, N., Segala, R.: Probabilistic simulations for probabilistic processes. Nordic Journal of Computing 2, 250–273 (1995)
Milner, R.: A Calculus of Communication Systems. LNCS, vol. 92. Springer, Heidelberg (1980)
Mio, M.: Game Semantics for Probabilistic μ-Calculi. PhD thesis, School of Informatics, University of Edinburgh (2012)
Mio, M.: Probabilistic Modal μ-Calculus with Independent product. Logical Methods in Computer Science 8(4) (2012)
Mio, M., Simpson, A.: Łukasiewicz mu-calculus. In: Proc. of Workshop on Fixed Points in Computer Science. EPTCS, vol. 126 (2013)
Mio, M., Simpson, A.: A proof system for compositional verification of probabilistic concurrent processes. In: Pfenning, F. (ed.) FOSSACS 2013. LNCS, vol. 7794, pp. 161–176. Springer, Heidelberg (2013)
Morgan, C., McIver, A.: A probabilistic temporal calculus based on expectations. In: Proc. of Formal Methods Pacific (1997)
Panangaden, P.: Labelled Markov processes. Imperial College Press (2009)
Sangiorgi, D., Rutten, J.: Advanced topics in bisimulation and coinduction. Cambridge University Press (2011)
Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis. MIT (1995)
Sokolova, A.: Probabilistic Systems Coalgebraically: A survey. Theoretical Computer Science 412(38) (2011)
Song, L., Zhang, L., Godskesen, J.C.: Bisimulations Meet PCTL Equivalences for Probabilistic Automata. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 108–123. Springer, Heidelberg (2011)
Tix, R., Keimel, K., Plotkin, G.D.: Semantic domains for combining probability and non-determinism. Electronic Notes in Theoretical Computer Science (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mio, M. (2014). Upper-Expectation Bisimilarity and Łukasiewicz μ-Calculus. In: Muscholl, A. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2014. Lecture Notes in Computer Science, vol 8412. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54830-7_22
Download citation
DOI: https://doi.org/10.1007/978-3-642-54830-7_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54829-1
Online ISBN: 978-3-642-54830-7
eBook Packages: Computer ScienceComputer Science (R0)