Action Refinement for Real-Time Concurrent Processes with Urgency  

作　　者：覃广平 吴尽昭 

机构地区：[1]ChengduInstituteofComputerApplications,ChineseAcademyofSciences,Chengdu610041,P.R.China [2]ChengduInstituteofComputerApplications,ChineseAcademyofSciences,Chengdu610041,P.R.China／／FakultaetfürMathematikundInformatik,Universit[itMannheim,D7,27,68131Mannheim,Germany

出　　处：《Journal of Computer Science & Technology》2005年第4期514-525,共12页计算机科学技术学报（英文版）

基　　金：国家自然科学基金

摘　　要：Action refinement for real-time concurrent processes with urgent interactions is studied, where a partial-order setting, i.e., timed bundle event structures, is used as the system model and a real-time LOTOS-like process algebra is used as the specification language. It is shown that the proposed refinement approaches have the commonly expected properties:(1) the behaviour of the refined process can be inferred compositionally from the behaviour of the original process and from the behaviour of the processes substituted for actions; (2) the timed extensions of pomset (partially ordered multiset) trace equivalence and history preserving bisimulation equivalence are both congruences under the refinement; (3) the syntactic and semantic refinements coincide up to the aforementioned equivalence relations with respect to a cpo-based denotational semantics.

分 类 号：TP312[自动化与计算机技术—计算机软件与理论]