Tags:bisimulation, functional bisimulation, labeled transition system, process specification and transfer of specifications
Abstract:
We motivate basic concepts for the transfer of specifications from one system to another that we are developing in the context of the process semantics of regular expressions with respect to bisimilarity. Specifically we introduce: `bisimulating slices', which relate parts of labeled transition systems (LTSs) without regard for the context; `grounded bisimulation slices', which relate parts of a single LTS in such a way that these slices can easily be extended into bisimulations; `transfer functions', which are functional bisimulations, and as such permit to transfer specifying expressions (process specifications, programs) between LTSs; `local transfer functions', which are functional grounded bisimulation slices; and `elevations of sets of states above' an LTS, which are partial unfoldings of an LTS.
We give definitions and state basic results that link them. While purpose-built for the transfer of regular-expression specifications of processes between LTSs, these ideas might be useful in other situations as well. We are interested in finding links to similar concepts.