2012
Conference article
Open Access
Bisimulation of Labeled State-to-Function Transition Systems of Stochastic Process Languages
Latella D., Massink M., De Vink E.
Structured Operational Semantics Category Theory FOS: Computer and information sciences Stochastic Process Calculi Computer Science - Logic in Computer Science Continuous Time Markov Chains Logic in Computer Science (cs.LO) Coalgebras F.3.2
Labeled state-to-function transition systems, FuTS for short, admit multiple transition schemes from states to functions of finite support over general semirings. As such they constitute a convenient modeling instrument to deal with stochastic process languages. In this paper, the notion of bisimulation induced by a FuTS is proposed and a correspondence result is proven stating that FuTS-bisimulation coincides with the behavioral equivalence of the associated functor. As generic examples, the concrete existing equivalences for the core of the process algebras ACP, PEPA and IMC are related to the bisimulation of specific FuTS, providing via the correspondence result coalgebraic justification of the equivalences of these calculi
Source: Seventh ACCAT Workshop on Applied and Computational Category Theory (ACCAT 2012), pp. 23–43, Tallin, Estonia, 4 april 2012
[1] C. Baier, B.R. Haverkort, H. Hermanns, J.-P. Katoen & M. Siegle, editors (2004): Validation of Stochastic Systems - A Guide to Current Research. LNCS 2925, doi:10.1007/b98484.
[2] J.W. de Bakker & E.P. de Vink (1996): Control Flow Semantics. The MIT Press.
[3] M. Bernardo (2007): A Survey of Markovian Behavioral Equivalences. In M. Bernardo & J. Hillston, editors: SFM 2007 Advanced Lectures, LNCS 4486, pp. 180-219, doi:10.1007/978-3-540-72522-0 5.
[4] M. Bernardo & R. Gorrieri (1998): A tutorial on EMPA: a theory of concurrent processes with nondeterminism, priorities, probabilities and time. Theoretical Computer Science 202(1-2), pp. 1-54, doi:10.1016/S0304-3975(97)00127-8.
[5] F. Bonchi, M. Bonsangue, M. Boreale, J. Rutten & A. Silva (2011): A coalgebraic perspective on linear weighted automata. Technical Report SEN-1104, CWI. 31pp.
[6] M. Boreale (2009): Weighted Bisimulation in Linear Algebraic Form. In M. Bravetti & G. Zavattaro, editors: Proc. CONCUR 2009, LNCS 5710, pp. 163-177, doi:10.1007/978-3-642-04081-8 12.
[7] R. De Nicola, D. Latella, M. Loreti & M. Massink (2009): Rate-based Transition Systems for Stochastic Process Calculi. In S. Albers et al., editor: Proc. ICALP 2009, Part II, LNCS 5556, pp. 435-446, doi:10.1007/978-3-642-02930-1 36.
[8] R. De Nicola, D. Latella, M. Loreti & M. Massink (2011): State to function labelled transition systems: a uniform framework for defining stochastic process calculi. Technical Report ISTI-2011-TR-012, CNR/ISTI.
[9] R. De Nicola, D. Latella & M. Massink (2005): Formal modeling and quantitative analysis of Klaim-based mobile systems. In H. Haddad et al., editor: Proc. SAC 2005, ACM, pp. 428-435, doi:10.1145/1066677.1066777.
[10] C. Eisentraut, H. Hermanns & L. Zhang (2010): Concurrency and Composition in a Stochastic World. In P. Gastin & F. Laroussinie, editors: Proc. CONCUR 2010, LNCS 6269, pp. 21-39, doi:10.1007/978-3-642- 15375-4 3.
[11] H.P. Gumm & T. Schro¨der (2001): Products of coalgebras. Algebra Universalis 46, pp. 163-185.
[12] H.P. Gumm & T. Schro¨der (2002): Coalgebras of bounded type. Mathematical Structures in Computer Science 12, pp. 565-578, doi:10.1017/S0960129501003590.
[13] H. Hermanns (2002): Interactive Markov Chains. LNCS 2428, doi:10.1007/3-540-45804-2.
[14] H. Hermanns, U. Herzog & J.-P. Katoen (2002): Process algebra for performance evaluation. Theoretical Computer Science 274(1-2), pp. 43-87, doi:10.1016/S0304-3975(00)00305-4.
[15] H. Hermanns, U. Herzog & V. Mertsiotakis (1998): Stochastic process algebras - between LOTOS and Markov chains. Computer Networks and ISDN Systems 30, pp. 901-924, doi:10.1016/S0169- 7552(97)00133-5.
[16] H. Hermanns & J.-P. Katoen (2010): The How and Why of Interactive Markov Chains. In F.S. de Boer, M.M. Bonsangue, S. Hallerstede & M. Leuschel, editors: Proc. FMCO 2009, LNCS 6286, pp. 311-337, doi:10.1007/978-3-642-17071-3 16.
[17] J. Hillston (1996): A Compositional Approach to Performance Modelling. Distinguished Dissertations in Computer Science 12, Cambridge University Press.
[18] J. Hillston (2005): Process Algebras for Quantitative Analysis. In: Proc. LICS, Chicago, IEEE, pp. 239-248, doi:10.1109/LICS.2005.35.
[19] B. Klin & V. Sassone (2008): Structural Operational Semantics for Stochastic Process Calculi. In R.M. Amadio, editor: Proc. FoSSaCS 2008, LNCS 4962, pp. 428-442, doi:10.1007/978-3-540-78499-9 30.
[20] A. Kurz (2000): Logics for coalgebras and applications to computer science. Ph.D. thesis, LMU Mu¨nchen.
[21] R. Milner (1980): A Calculus of Communicating Systems. LNCS 92, doi:10.1007/3-540-10235-3.
[22] D. Park (1981): Concurrency and Automata on Infinite Sequences. In: Proc. GI-Conference 1981, Karlsruhe, LNCS 104, pp. 167-183.
[25] A. Silva, F. Bonchi, M. Bonsangue & J. Rutten (2011): Quantitative Kleene coalgebras. Information and Computation 209(5), pp. 822-846, doi:10.1016/j.ic.2010.09.007.
[26] A. Sokolova (2011): Probabilistic systems coalgebraically: a survey. Theoretical Computer Science 412(38), pp. 5095-5110, doi:10.1016/j.tcs.2011.05.008.
[27] D. Turi & G.D. Plotkin (1997): Towards a Mathematical Operational Semantics. In: Proc. LICS 1997, Warsaw, IEEE, pp. 280-291, doi:10.1109/LICS.1999.782615.
[28] E.P. de Vink & J.J.M.M. Rutten (1999): Bisimulation for probabilistic transition systems: a coalgebraic approach. Theoretical Computer Science 221, pp. 271-293, doi:10.1016/S0304-3975(99)00035-3.
The other cases are standard or similar and easier. (b) Guarded induction. We treat the cases for :P and P1 kA P2. Case :P. Assume P 2 P.
Suppose P = :P0. Then it holds that P admits a single d -transition, viz. P d P0. Thus we have P fj j P d P0 jg = = [ P0 7! ](P0) = P(P0). Suppose P = :P00 for some P00 , P. Then we have P fj j P d P0 jg = 0 = [ P00 7! ](P0) = P(P0). Case P1 kA P2. Assume P1 2 P1, P2 2 P2 and P1 kA P2 P. It holds that P = (P1 kA XP2) + (XP1 kA P2). We calculate P fj j P1 kA P2 d P0 jg = P fj j P1 d P01; P0 = P01 kA P2 jg + P fj j P2 d P02; P0 = P1 kA P02 jg (by analysis of d) = ( if P0 = P01 kA P2 then P fj j P1 d P01 jg else 0 end ) + ( if P0 = P1 kA P02 then P fj j P2 d P02 jg else 0 end ) = ( if P0 = P01 kA P2 then P1(P01) else 0 end ) + ( if P0 = P1 kA P02 then P2(P02) else 0 end ) (by induction hypothesis for P1 and P2) = ( P1 kA XP2 )(P0) + ( XP1 kA P2 )(P0) (by definition of kA, XP1,XP2 and + on FS(PIML; R>0 )) = P(P0)
[2] J.W. de Bakker & E.P. de Vink (1996): Control Flow Semantics. The MIT Press.
[3] M. Bernardo (2007): A Survey of Markovian Behavioral Equivalences. In M. Bernardo & J. Hillston, editors: SFM 2007 Advanced Lectures, LNCS 4486, pp. 180-219, doi:10.1007/978-3-540-72522-0 5.
[4] M. Bernardo & R. Gorrieri (1998): A tutorial on EMPA: a theory of concurrent processes with nondeterminism, priorities, probabilities and time. Theoretical Computer Science 202(1-2), pp. 1-54, doi:10.1016/S0304-3975(97)00127-8.
[5] F. Bonchi, M. Bonsangue, M. Boreale, J. Rutten & A. Silva (2011): A coalgebraic perspective on linear weighted automata. Technical Report SEN-1104, CWI. 31pp.
[6] M. Boreale (2009): Weighted Bisimulation in Linear Algebraic Form. In M. Bravetti & G. Zavattaro, editors: Proc. CONCUR 2009, LNCS 5710, pp. 163-177, doi:10.1007/978-3-642-04081-8 12.
[7] R. De Nicola, D. Latella, M. Loreti & M. Massink (2009): Rate-based Transition Systems for Stochastic Process Calculi. In S. Albers et al., editor: Proc. ICALP 2009, Part II, LNCS 5556, pp. 435-446, doi:10.1007/978-3-642-02930-1 36.
[8] R. De Nicola, D. Latella, M. Loreti & M. Massink (2011): State to function labelled transition systems: a uniform framework for defining stochastic process calculi. Technical Report ISTI-2011-TR-012, CNR/ISTI.
[9] R. De Nicola, D. Latella & M. Massink (2005): Formal modeling and quantitative analysis of Klaim-based mobile systems. In H. Haddad et al., editor: Proc. SAC 2005, ACM, pp. 428-435, doi:10.1145/1066677.1066777.
[10] C. Eisentraut, H. Hermanns & L. Zhang (2010): Concurrency and Composition in a Stochastic World. In P. Gastin & F. Laroussinie, editors: Proc. CONCUR 2010, LNCS 6269, pp. 21-39, doi:10.1007/978-3-642- 15375-4 3.
[11] H.P. Gumm & T. Schro¨der (2001): Products of coalgebras. Algebra Universalis 46, pp. 163-185.
[12] H.P. Gumm & T. Schro¨der (2002): Coalgebras of bounded type. Mathematical Structures in Computer Science 12, pp. 565-578, doi:10.1017/S0960129501003590.
[13] H. Hermanns (2002): Interactive Markov Chains. LNCS 2428, doi:10.1007/3-540-45804-2.
[14] H. Hermanns, U. Herzog & J.-P. Katoen (2002): Process algebra for performance evaluation. Theoretical Computer Science 274(1-2), pp. 43-87, doi:10.1016/S0304-3975(00)00305-4.
[15] H. Hermanns, U. Herzog & V. Mertsiotakis (1998): Stochastic process algebras - between LOTOS and Markov chains. Computer Networks and ISDN Systems 30, pp. 901-924, doi:10.1016/S0169- 7552(97)00133-5.
[16] H. Hermanns & J.-P. Katoen (2010): The How and Why of Interactive Markov Chains. In F.S. de Boer, M.M. Bonsangue, S. Hallerstede & M. Leuschel, editors: Proc. FMCO 2009, LNCS 6286, pp. 311-337, doi:10.1007/978-3-642-17071-3 16.
[17] J. Hillston (1996): A Compositional Approach to Performance Modelling. Distinguished Dissertations in Computer Science 12, Cambridge University Press.
[18] J. Hillston (2005): Process Algebras for Quantitative Analysis. In: Proc. LICS, Chicago, IEEE, pp. 239-248, doi:10.1109/LICS.2005.35.
[19] B. Klin & V. Sassone (2008): Structural Operational Semantics for Stochastic Process Calculi. In R.M. Amadio, editor: Proc. FoSSaCS 2008, LNCS 4962, pp. 428-442, doi:10.1007/978-3-540-78499-9 30.
[20] A. Kurz (2000): Logics for coalgebras and applications to computer science. Ph.D. thesis, LMU Mu¨nchen.
[21] R. Milner (1980): A Calculus of Communicating Systems. LNCS 92, doi:10.1007/3-540-10235-3.
[22] D. Park (1981): Concurrency and Automata on Infinite Sequences. In: Proc. GI-Conference 1981, Karlsruhe, LNCS 104, pp. 167-183.
[25] A. Silva, F. Bonchi, M. Bonsangue & J. Rutten (2011): Quantitative Kleene coalgebras. Information and Computation 209(5), pp. 822-846, doi:10.1016/j.ic.2010.09.007.
[26] A. Sokolova (2011): Probabilistic systems coalgebraically: a survey. Theoretical Computer Science 412(38), pp. 5095-5110, doi:10.1016/j.tcs.2011.05.008.
[27] D. Turi & G.D. Plotkin (1997): Towards a Mathematical Operational Semantics. In: Proc. LICS 1997, Warsaw, IEEE, pp. 280-291, doi:10.1109/LICS.1999.782615.
[28] E.P. de Vink & J.J.M.M. Rutten (1999): Bisimulation for probabilistic transition systems: a coalgebraic approach. Theoretical Computer Science 221, pp. 271-293, doi:10.1016/S0304-3975(99)00035-3.
The other cases are standard or similar and easier. (b) Guarded induction. We treat the cases for :P and P1 kA P2. Case :P. Assume P 2 P.
Suppose P = :P0. Then it holds that P admits a single d -transition, viz. P d P0. Thus we have P fj j P d P0 jg = = [ P0 7! ](P0) = P(P0). Suppose P = :P00 for some P00 , P. Then we have P fj j P d P0 jg = 0 = [ P00 7! ](P0) = P(P0). Case P1 kA P2. Assume P1 2 P1, P2 2 P2 and P1 kA P2 P. It holds that P = (P1 kA XP2) + (XP1 kA P2). We calculate P fj j P1 kA P2 d P0 jg = P fj j P1 d P01; P0 = P01 kA P2 jg + P fj j P2 d P02; P0 = P1 kA P02 jg (by analysis of d) = ( if P0 = P01 kA P2 then P fj j P1 d P01 jg else 0 end ) + ( if P0 = P1 kA P02 then P fj j P2 d P02 jg else 0 end ) = ( if P0 = P01 kA P2 then P1(P01) else 0 end ) + ( if P0 = P1 kA P02 then P2(P02) else 0 end ) (by induction hypothesis for P1 and P2) = ( P1 kA XP2 )(P0) + ( XP1 kA P2 )(P0) (by definition of kA, XP1,XP2 and + on FS(PIML; R>0 )) = P(P0)
Metrics
Back to previous page
BibTeX entry
@inproceedings{oai:it.cnr:prodotti:190160,
title = {Bisimulation of Labeled State-to-Function Transition Systems of Stochastic Process Languages},
author = {Latella D. and Massink M. and De Vink E.},
doi = {10.4204/eptcs.93.2 and 10.48550/arxiv.1209.1432},
booktitle = {Seventh ACCAT Workshop on Applied and Computational Category Theory (ACCAT 2012), pp. 23–43, Tallin, Estonia, 4 april 2012},
year = {2012}
}
0000-0002-3257-9059
