时间π演算及其弱时间互模拟分析

• 论文 •

时间π演算及其弱时间互模拟分析

许可，刘连臣，吴澄

清华大学自动化系，北京 100084

收稿日期:2005-02-23 修回日期:2005-04-01 出版日期:2006-04-15 发布日期:2006-04-25
基金资助:
国家973计划资助项目（2002CB312202）；国家863/CIMS主题资助项目（2003AA1Z2290）。

Time π calculus and weak-timed mutual-simulation analysis

XU Ke,LIU Lian-chen,WU Cheng

Dep. of Automation, Tsinghua Univ., Beijing 100084, China

Received:2005-02-23 Revised:2005-04-01 Online:2006-04-15 Published:2006-04-25
Supported by:
Project supported by the National Key Basic Research Program,China(No.2002CB312202)and the National High-Tech.R&D Program for CIMS,China(No.2003AA1Z2290).

摘要/Abstract

摘要： 为了提高π演算对系统时间特性进行建模和分析的能力，针对可重入流生产线系统的特点，提出了一种基于持续活动和同步-等待交互方式的时间良构的时间π演算，即T-π演算。提出了一种新的弱时间互模拟关系，对模型的现有等价性判别条件进行了松弛。作为对T-π演算的有效性检验，利用T-π演算对可重入流生产线进行了形式化描述，在此基础上进行了其等价性分析，并给出了其可调度性判据。

关键词: 时间π演算, 等价性分析, 可调度性分析, 形式化描述, 可重入流生产线

Abstract: To extend the capacity of π calculus in modeling and analyzing time－related properties of a system, a well-timed π calculus with durational actions and busy-waiting interaction mechanism, namely T-π calculus, was proposed based on the characteristics of re-entrant production line system. A new weak-timed mutual-simulation relationship was also presented to relax the model equivalency conditions in existing mutual-simulation relationships. Besides, to illustrate the effectiveness of the proposed calculus, a re-entrant production line was formalized with T-π calculus. Based on the formal specification, its equivalency analysis was explored and its scheduling capacity proof was also provided.

Key words: timed π calculus, equivalency analysis, schedule ability analysis, formal specification, re-entrant production line

中图分类号:

TP301.2

许可，刘连臣，吴澄. 时间π演算及其弱时间互模拟分析[J]. .

XU Ke,LIU Lian-chen,WU Cheng. Time π calculus and weak-timed mutual-simulation analysis[J]. .

参考文献

［1］ MILNER R.Communication and concurrency［M］.Upper Saddle River,NJ,USA: Prentice Hall,1989.

[2] HOARE C.Communicating sequential processes［M］.Upper Saddle River,NJ,USA: Prentice Hall,1985.

[3] GORRIERI R,ROCCETTI M,STANCAMPIANO E.Theory of processes with durational actions［J］.Theoretical Computer Science,1995,140(1): 73-94.

[4] CORRADINI F,FERRARI G L,PISTORE M.On the semantics of durational actions［J］.Theoretical Computer Science,2001,269(1-2): 47-82.

[5] ACETO L,MURPHY D.Timing and causality in process algebra［J］.ACTA Informatics,1996,33(4): 317-350.

[6] COLIN F,JOHN Z.An expressive real-time CCS［A］.Proceedings of the Twenty-Fifth Australasian Conference on Computer Science［C］.Sydney,New South Wales,Australia:Australian Computer Society,1995.365-372.

[7] JIM D,STEVE S.A brief history of timed CSP［J］.Theoretical Computer Science,1995,138(2):243-271.

[8] MILNER R.Communicating and mobile systems: the π-calculus［M］.Cambridge，U.K.:Cambridge University Press,1999.

[9] KUMAR P R.Scheduling semiconductor manufacturing plants［J］.IEEE Control System Magazines,1994,14(6): 33-40.

[10] DEGANO P,LODDO J V,PRIAMI C.Mobile processes with local clocks［A］.Lecture Notes in Computer Science［C］.Berlin，Germany:Springer,1996,1192: 296-319.

[11] BERGER M.Towards abstractions for distributed systems［D］.London,U.K.:Imperial College,2002.

[12] BERGER M.Basic theory of reduction congruence for two timed asynchronous pi-calculi［A］.Lecture Notes in Computer Science［C］.Berlin,Germany:Springer,2004,3170.115-130.

[13] FLAVIO C.Absolute versus relative time in process algebras［J］.Information and Computation,2000,156: 122-172.

[14] GROOTE J F.Transition system specification with negative premises［J］.Theoretical Computer Science,1993,118(2):263-299.

[1]	杨潇,马军,侯金奎. 基于特征和范畴理论的体系结构模型形式化描述[J]. , 2009, 15(07): 0-0.
[2]	李慧芳，范玉顺. 时间约束工作流模型的可调度性分析算法[J]. , 2002, 8(7): 0-0.