Symbolic bisimulations. (English) Zbl 0874.68187

Hennessy, M.; Lin, H.

Theor. Comput. Sci. 138, No. 2, 353-389 (1995).

Summary: 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.

MSC:

68Q55	Semantics in the theory of computing
68Q45	Formal languages and automata

Keywords:

bisimulation equivalence; value-passing process languages

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