Symbolic bisimulations.

*(English)*Zbl 0874.68187Summary: We re-examine bisimulation equivalence for value-passing process languages in which actions have associated with them values from a possibly infinite value set. Using symbolic actions we generalise the standard notion of labelled transition graph to that of symbolic transition graph. The advantage of the latter is that the operational semantics of many value-passing processes may be expressed in terms of finite symbolic transition graphs although the underlying (standard) labelled transitions graph is infinite. A collection of symbolic bisimulations parameterised on boolean expressions, \(\simeq ^{b}\), are then defined over symbolic transition graphs. These are related to standard bisimulations by proving that \(t\simeq ^{b}u\) if and only if in every interpretation which satisfies \(b,t\) is bisimulation equivalent to \(u\) in the standard sense. We then give an algorithm for checking the relation \(t\simeq ^{b}u\) which can be applied to arbitrary finite symbolic trees. The results apply to both early and late bisimulation equivalence, which are the two natural generalisations of the standard bisimulation equivalence to value-passing languages.

PDF
BibTeX
XML
Cite

\textit{M. Hennessy} and \textit{H. Lin}, Theor. Comput. Sci. 138, No. 2, 353--389 (1995; Zbl 0874.68187)

Full Text:
DOI

##### References:

[1] | Alur, R; Dill, D, The theory of timed automata, () · Zbl 0803.68071 |

[2] | Bradfield, J; Stirling, C, Local model checking for infinite state spaces, () · Zbl 0747.68036 |

[3] | Burns, G, A language for value-passing ccs, () |

[4] | Cleaveland, R; Parrow, J; Steffen, B, The concurrency workbench: A semantics based verification tool for finite state systems, () |

[5] | De Simone, R; Vergamimi, D, () |

[6] | Godskesen, J; Larsen, K; Zeeberg, M, () |

[7] | Holmer, U; Larsen, K.G; Wang, Y, Deciding properties of regular timed processes, () |

[8] | Jonsson, B; Parrow, J, Deciding bisimulation equivalences for a class of non-finite-state programs, Inform. comput., 107, 272-302, (1993) · Zbl 0799.68133 |

[9] | Larsen, K.G, Contex-dependent bisimulation between processes, () |

[10] | Milner, R, Communication and concurrency, (1989), Prentice-Hall Englewood Cliffs, NJ · Zbl 0683.68008 |

[11] | Milner, R; Parrow, J; Walker, D, Mobile logics for mobile processes, Theoret. comput. sci., 114, 149-171, (1993) · Zbl 0778.68033 |

[12] | Schreiber, M.Z, Value-passing process calculi as a formal method, () |

[13] | Walker, D, Automated analysis of mutual exclusion algorithms using CCS, Formal aspects of computing, 1, 273-292, (1989) · Zbl 0696.68039 |

[14] | Wolper, P, Expressing interesting properties of programs in propositional temporal logic (extended abstract), (), 184-193 |

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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.