从因果语义到持续时间时间模型
From Causal Semantics To Duration Timed Models
摘要：
交错语义与动作细化和持续时间动作都不兼容。由于许多真正的并发语义是一致的w.r.t.行动细化，特别是因果关系和最大化的，这给我们提出了挑战，研究密集的时间行为-其中的行动是任意固定的持续时间-在因果关系语义的Da Costa。我们扩展了因果转移系统的时钟和时间约束，从而我们得到了一类时间自动机的动作不需要是原子的。我们定义了一个实时的扩展的形式化描述技术CSP，称为持续时间CSP，归因于持续时间的行动。我们给出了duration-CSP的操作时间因果语义及其在时间因果变迁系统类上的指称语义。之后，我们证明了这两个语义是等价的。最后，我们扩展的持续时间CSP语言的细化操作$ρ$ -允许替换一个动作的过程-并证明它保留了定时因果互模拟。
英文摘要：
The interleaving semantics is not compatible with both action refinement and durational actions. Since many true concurrency semantics are congruent w.r.t. action refinement, notably the causality and the maximality ones, this has challenged us to study the dense time behavior - where the actions are of arbitrary fixed duration - within the causality semantics of Da Costa. We extend the causal transition systems with the clocks and the timed constraints, and thus we obtain an over class of timed automata where the actions need not to be atomic. We define a real time extension of the formal description technique CSP, called duration-CSP, by attributing the duration to actions. We give the operational timed causal semantics of duration-CSP as well as its denotational semantics over the class of timed causal transition systems. Afterwards, we prove that the two semantics are equivalent. Finally we extend the duration-CSP language with a refinement operator $ρ$ - that allows to replace an action with a process - and prove that it preserves the timed causal bisimulation.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
