Finitary Truly Concurrent Bisimulations
This work provides foundational definitions for finitary concurrent bisimulations, which are incremental for researchers in process algebra and concurrency theory.
The paper addresses the need for a finitary version of truly concurrent prebisimulation to achieve full abstractness in denotational models of process languages. It defines truly concurrent prebisimulations and their finitary counterparts, following the behavioural form of finitary bisimulation.
To develop a full abstract denotational model of a process language based on prebisimulation preorder, its behavioural semantics has two problems: (1) Two processes related by a standard denotational interpretation afford the same finite observations. (2) Prebisimulation can make distinctions between the behaviours of two processes based on infinite observations. So, finitary part of prebisimulation is needed to obtain full abstract results. There existed two main results on finitary bisimulation: the logical form and the behavioural form. Following the latter one, we give the definitions of truly concurrent prebisimulations and their finitary ones.