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.

翻译：为建立基于预互模拟预序的过程语言的完全抽象指称模型，其行为语义面临两个问题：（1）标准指称解释相关联的两个过程具有相同的有限观测；（2）预互模拟能依据无限观测来区分两个过程的行为差异。因此需要预互模拟的有限部分来获得完全抽象结果。关于有限互模拟存在两个主要结果：逻辑形式和行为形式。遵循后者，我们给出了真正并发预互模拟及其有限形式的定义。