TL;DR
This paper introduces finitary truly concurrent prebisimulations to address limitations in existing models, enabling more precise behavioral distinctions in process semantics.
Contribution
It defines new finitary truly concurrent prebisimulations, extending the behavioral form of finitary bisimulation for process semantics.
Findings
Defined truly concurrent prebisimulations.
Established finitary versions of these prebisimulations.
Enhanced behavioral distinctions in process models.
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.