We study the use of the elaboration preorder (due to Arun-Kumar and Natarajan) in the framework of up-to techniques for weak bisimulation. We show that elaboration yields a correct technique that encompasses the commonly used up to expansion technique. We also define a theory of up-to techniques for elaboration that in particular validates an elaboration up to elaboration technique, while it is known that weak bisimulation up to weak bisimilarity is unsound. In this sense, the resulting setting improves over previous works in terms of modularity. Our results are obtained using nontrivial proofs that exploit termination arguments. In particular, we need the termination of internal computations for the up-to techniques to be correct. We show how this condition can be relaxed to some extent in order to handle processes exhibiting infinite internal behaviour. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Pous, D. (2006). Weak bisimulation up to elaboration. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4137 LNCS, pp. 390–405). Springer Verlag. https://doi.org/10.1007/11817949_26
Mendeley helps you to discover research relevant for your work.