时间I/O组件的概念及其在健康时间系统中的应用

网址：http://www.elsevier.nl/locate/entcs/volume52.html19页扩展时间自动机组合建模健康时间系统VctorBraberman1;2计算机科学系，FCEyN，布宜诺斯艾利斯大学，阿根廷Alfredo Olivero3;4阿根廷企业大学信息技术系，阿根廷布宜诺斯艾利斯摘要我们引入了时间I/O组件的概念作为时间自动机，&其中声明了一个可接受的I/O接口。我们认为，这个概念有一个关键的建模属性：在交互组件之间的“语法可检查I/O兼容性”下的非zeno保留。此外，基于静态检测组件之间行为影响的能力，可以减少组件组成[8，10，11]。另一方面，通过一些简单的额外条件，模块化假设保证风格的推理在我们的模型中是有效的。第1章介绍：非芝诺和非阻塞模型时间系统的良好定义的模型通常要求是“非zeno”的。粗略地说，非zenoness意味着任何nite run都可以扩展到nite run中的时间发散（即，没有“黑胡同”，时间总是可以进步的）。一方面，Zenoness通常是病态建模的症状，另一方面，非Zenoness需要执行一些验证过程时，语义被限制到发散运行。1 研究由UBACyT资助X156和TW722 电子邮件地址：vbraber@dc.uba.ar3 UADE资助的研究ING 6 -014 电子邮件地址：aolivero@uade.edu.arc 2002年由Elsevier Science B出版。诉在CC BY-NC-ND许可下开放访问。2不幸的是，平行组合并不能保持非天顶性非芝诺系统在连接时可能会产生时间锁。I/O定时组件（I/O TC）是为表达构建在定时自动机（TA）之上的非zeno定时行为而开发的组合模型[8]。它们强加了一种建模规则，以保证在“兼容的”I/O TC之间进行并行组合是一种自然的方式来约束单个组件的行为，而不会引入zeno行为。让我们指出I/O TC的一些有趣方面：I/O接口允许简单的语法检查，确保并行组合下的非zeno编译。通过使用I/O接口，可以以非常精确的方式计算一个组件对另一个组件行为的影响（参见[8，10，11]）。据我们所知，这是I/O接口的一个全新的目标。由于I/O TC是建立在TA的简单概念之上的，Dill-基于标签共享的通信-它们立即得到几个检查工具的支持，如Kronos[13]，Uppaal[6]等。I/O TC的定义不需要像实时I/O定时自动机[15]、反应模块[5]等那样诉诸“接受性游戏”。检查良好I/O标签划分的条件很容易自动化。我们相信它们适合于对高级非阻塞抽象进行压缩3）。通过对I/O TC的一些额外约束，可以应用“假定-保证”式规则（例如，[19])用于支票付款。就像在[19]中一样，这些约束不是基于更一般但更复杂的接受性游戏[15，5]）。这些约束不是I/O TC的基本属性（其主要受非zeno保存的启发）。我们认为，这种分离具有理论和实际意义。I/O的概念是相当独立的基本定时（或非定时5）的形式主义用于描述的动态。值得一提的是关于保持组分的“反应性和活性”的相关工作。在[7]中，提出了一个基于同步操作时间特性的代数框架（他们的目标是获得高级别的同步设施）。我们的观点是一个过渡的功能分类。在这方面的研究中，[19]的作者提出了非阻塞时间过程，以获得一个自动机家族，在那里他们可以应用as-objective/guarantee风格的推理。组件之间的通信基于信号变化而不是标签共享，适合于电路模式。5我们相信，通过改变带有公平性约束的定时发散条件，可以使该I/O模型适应于不定时框架[12，15]，这是在不定时框架中指定进度的常用方法。3tottottoteling。与我们的方法不同的是，输出变化被约束为非瞬态的，输入的更新独立于输出的更新。由于该模型专注于打破假设保证规则的循环，因此非顶点的基本概念不需要排除黑巷;相反，定义排除了在一个夜间间隔。活动和I/O接口已在通用设置中考虑，模拟证明方法\la”Lynch-Vaandrager [15]面向-Orem provers. 在这项工作中，实时I/O自动机使用了“响应性”是基于游戏定义的，游戏嵌入了几个公平I/O定时系统的建议[20，24]等。更接近的模型是[5]的反应模块。与我们的概念不同，它基于接受性游戏来定义非阻塞和I/O变量来通信模块。在下一节中，我们回顾时间自动机。在第3节中，我们正式介绍了I/O定时组件。第4节提到了一些应用。第五节讨论了获得推定担保规则的条件。最后，我们总结了结果，并提出了一些未来的工作。2时间自动机时间自动机（TA）是建模和分析时间系统的最广泛使用的形式主义之一，并得到几种工具的支持（例如，[13，6，18]等）。本文部分内容如下[26]。给定一组时钟（非线性实变量）X=fx1;x2; ：;xn g，赋值为全函数V：X！其中v（x i）是与时钟x i相关联的值。我们把V X定义为集合[X！R0]的所有函数的映射X到R 0。0 2 VX表示所有时钟均为0 给定v 2 VX和t2 R 0，v+t表示赋值给每个时钟x 2 X值v（x）+t的赋值给定一组时钟X，子集X和估值v，我们将Reset（v）定义为一个估值，该估值将零分配给时钟，并为其余时钟保持与v相同的值。给定一组时钟X，我们定义时钟约束集X根据语法：X3：：=xcjxx0c j^ j_，其中xx02x21和#IA2 >1henIA1\IA2 为使用IA的标签中的一些标签来同步（在每个状态处总是存在启用的每个输入选择的(ii) 存在游程r2R1（q），使得Lab（r）|nA=i。 输入不是强制性的，因此必须保证没有它们的非zenoness 6。M mq7！O一然后是Q7！M. 输出选择的所有标签同时0 0启用或禁用。（iv）对于任意游程r2 R A（q），如果标签o2 Out A在r中出现无限次，则必然r2R1（q）（输出的非传递性）.在附录A.1中，我们展示了如何检查I/O可接受性。定义3.2 [I/O TC] I/O定时组件（或I/O TC）是元组（A;（IA; OA）），其中A是非zeno TA，并且（IA; OA）是A的容许I/O接口。大于1的输出选择根据组件的状态来模拟组件的替代行为，将这些标签导出为输入选择（类似于类似进程代数的符号中的外部非确定性选择，参见示例3.4）。给定I/O TC C =（A;（IA; OA）），当可以从上下文推导出时，C也可以表示底层TA A。因此，在I/O TC上执行的操作应该被理解为在其底层TA上的操作。定义3.3 [兼容组件]给定两个I/O TC C1 =（A1，（IA1，OA1））和C2=（A2;（IA2;OA2）），它们是兼容组件，当且仅当：（i）标号ls（A1）\标号ls（A2）ExpA1 \ExpA2 （即，所有公共标签都由A1和A2导出），嗯嗯;（大于1的输入选择的交集必须为空）。(iii) OutA1\O utA2 =;（组件不共享输出标签）。(iv) 对于所有I2IA1[IA2 和O2OA1[OA2 然后要么I\O=;要么IO（输出选择覆盖所有输入选项）。我们把一组成对相容的组件称为相容组件集。I/O兼容性意味着底层TA不能相互阻塞，此外，我们将证明兼容组件的组合本身就是一个组件，因此是非zeno自动机。6 请注意，此属性比non-zenoness更强，因为它还需要时间发散，以避免输入标记的转换。它类似于[22]中的渐进性和[24]中的可行性。7 这一要求与之前的发散性质（定义3.1的第（ii）项）和底层TA的非顶点性一起与[24]的强I/O可行性概念密切相关。8例3.4 CSMA/CD（载波侦听，带冲突检测的多路访问）是局域网MAC子层上广泛使用的协议。它解决了在广播网络中共享单个信道（多路访问信道）的问题。当一个站有数据要发送时，它首先监听信道以检查它是空闲还是繁忙。如果总线看起来空闲，它开始发送消息，否则它等待一段随机的时间，然后重复检测操作。当发生冲突时，所有正在传输的站同时中止传输我们使用I/O定时组件（见图1）基于[21]中提出的模型对协议的定时方面进行正式建模。多个组件共享一个总线组件。我们假设总线是一个10Mbps的以太网，最坏情况下的传播延迟为26 ms。消息有一个固定的长度为1024字节，所以发送一个完整的消息的时间，包括传播延迟，是808 ms。总线是无错误的，没有传入消息的缓冲区是所有的。 注意，fSendOKi;Send Busyi g是发送器i的输出选择，并且该选择取决于在总线状态下实际使能的输入。实际上，SendBusyi在消息头已经传播时启用。 传播碰撞信号所需的时间所有的人。发送者在传输位置最多停留10秒。还请注意，发送方在自上次尝试后经过2之前不确定地进行新的发送尝试。在像定时过程[19]这样的模型中，发送器组件有必要发出代表总线状态感测的信号在软件模型中常见的两阶段建模习惯，可以在我们的建模框架中使用适当的输入和输出选择来减少。在[8]中，读者可以找到如何将文献中的几个示例建模为I/OTC。3.1 I/O组件：组合和非Zenoness让我们陈述一些有助于证明TA模型是非zeno的结果。首先，我们将看到一个可接受的接口可以推导出两个兼容的I/O TC的并行组合。这是一个相当强的结果，它意味着以下事实：给定两个兼容的I/O TCC1和C2，则结果为非zeno的组合也是I/O TC（即，A1 k A2是非zeno的，而且可以给它一个可接受的I/O接口）。简单地说，新的输入界面由原始输入选择构成，这些原始输入选择不失去定义3.1的项（i）的“选择性”。该财产对于任何输入选择，只要没有匹配的输出选择，并且它没有正确地包含在另一个输入选择中，就保留。可以做类似的事情来构建新的输出接口。由于与大小大于1的输入选择相交的输出选择9y 26>11i n1i n>1>1发送者1碰撞等sendbusy1{x1}碰撞{x1}send1ok{x1}x1=808end1x1>=1send1ok{x1}重试x1 52反式x1 =808碰撞{x1}I={{collision}}O={{send1ok，send1busy}，{end1}}x1>=1send1busy{x1}总线等send2ok{y}send1ok{y}end2y>=26y>=26send2busysend1busyend2end1end1I={{send1ok，send1busy}，{end1}，{end2}， {send2ok，send2busy}}}碰撞send1oky 26O={{collision}}y>1send2oksend1oky 26send2okend1end2Fig. 1. CSMA/CD协议可能失去同时可用性属性（定义3.1的第（iii）项），它们不是新输出选择的一部分然而，所有这些标签“丢失”输出选择可以安全地添加为大小为1的（单例通常满足定义3.1的第（iii）项）。因此，组件的所有导出标签都将在合成中导出。这个事实对于证明这个构造可以推广到n个分量的并行合成是很重要的：定理3.5给定n个I/OTC的索引edstS=f（Ai;（IAi;OAi） g1in使得它们是成对相容的，我们定义集合IA =SIA=SfI2IAi=#I>1g，OA=SOAi.（A;（IA;OA））是组分，其中：A =k1i nAiIA=fI2IA=8I 02IA：I6I 0^8O02OA：II IO0=;g和，1I n IAi，OA=fO2OA=8I 02IA：I 0\O=;g[ffog=o2O2OA^9I 02IA：I 0\O6=;g证据 见附录a 其基本思想是，从 作为一个组件，它的伙伴并不阻10止它的输出：它们只是选择它们。11（定义3.1的项目（i）和（iii）），也不需要输入，以允许时间流逝（定义（ii））。3.1）。另一方面，I/O TC的子集不能在夜间时间间隔内参与夜间活动，因为这被Def的第（iv）项排除。3.1.2在例3.4中，并行组合A = defSENDER1kBUS的结果界面为：IA=ffSend2o k;Send2Bus y g;fend2 gg，OA=ffend1g，fSend 1 okg，fSend1Busyg，fcollisiongg。注意，由于输出选择fSend1ok;Send1Busy g的同时可用性丢失，因此它们成为单吨输出选择。4I/O TC非Zeno模型的应用：兼 容 性 是 一 个语 法 条 件 ， 它 确 保 了所产生的 并 行 组 合 的 非zenoness。 如前所述，非zenoness是执行某些验证过程所需的属性。在[8，9]中，我们通过I/O TC对我们使用I/O兼容性来确保对连接器和环境进行建模的I/O TC不会阻塞系统的其余部分（任务）。正如已经解释的，I/O选择可能是在软件实体上的单个转换动作/结果中建模的有用机制。减少：安全要求通常通过虚拟组件（观察者）来建模，虚拟组件与被分析系统（SUA）并行组成（例如，[1，9]）。在[8，10，11]中，我们提出了一种技术，该技术给定SUA和观察者，构建一个较小的并行组合，相当于原始的LTS分支结构。简而言之，我们开发了一种技术，计算可能被遗忘的组件在每个观察者的位置，因为他们未来的行为不影响未来的演变SUA的观察者。在对观测器拓扑结构的一些合理假设下，这些剩余的集合（相关分量）是所有分量集合的真子集。在某些情况下，核查所需的时间大大减少。该技术的核心是一个自动机行为对另一个自动机行为的潜在“直接影响”的概念。一个简单的解决方案会说，一个自动机A潜在地影响另一个自动机B，因为它们共享一个标签。不幸的是，这将导致相当大的对称高估。然后，通过使用附加到TA的I/O接口，我们能够定义可以静态检查的行为影响的不对称条件。也就是说，我们提供了比简单的标签共享更好的潜在影响力高估。值得一提的是，[16]中提出的技术基于比本文中提出的更简单的I/O接口概念1200A B AB使用本文定义的“关联演算”的细节可以在[8，10，11]中找到。5论推定担保规则[19]的作者提出了一个简单的模块性原则，用于时间进程中的抽象假设保证规则具有明显的循环性：要证明AkB是A0kB 0的一个元素，就必须证明：（1）A是A0的一个元素，假设它的元素是B0;（2）B是B 0的一个元素，假设它的元素是A0. 为了使这个规则在我们的环境中为真，我们必须添加一些条件。首先，让我们从输出的角度来定义一个状态是不紧急定义5.1 [非紧急状态]给定I/O TC C =（A;（IA; OA）），状态q不输出紧急（表示为NU（q））i，存在游程r 2 RA（q），使得0r和Lab（r）A。定义5.2 [非阻塞附加条件]我们说一个I/O TC满足非阻塞附加条件，当且仅当：(i) 守卫和不变量是封闭谓词（即，它的二元关系只有，=或）。(ii) 输入既不禁用也不启用紧急输出： 给定状态q 2到达（A）和标签i 2在A中，如果q 7！iq 0则NU（q）iNU（q 0）8。很容易看出，这些性质通过并行组合A =kj2J Aj来保持。 首先注意，A的守卫和不变量是从组分Aj.（二）项规定。5.2，如果q 7！iq 0那么i是一个分量（即k）的不匹配输入，因此q和q 0在k的局部状态中不同。此外，NU（q）当且仅当对于所有j 2J NU（j（q））（因为组合A的内部标签的集合是分量A j的内部标签的并集）。因此，NU（q）iNU（q0），因为NU（k（q））iNU（k（q0））并且其余的分量保持相同。定理5.3（假设/保证）给定I/OTCA;B;A0;B0，满足非阻塞的额外条件，使得A和B是I/O兼容的，并且A0和B0具有A和B所代表的相同I/O接口。如果（AkB0）Exp A0和（A0kB）Exp B0意味着（AkB）E×p[E×p（A0kB0）.证据见附录二28 例如，可以使用Kronos工具的验证引擎检查此属性[13]。136结论和未来工作我们提出了I/O Timed Components，这是一个简单的组合概念，它扩展了Timed Automata\ a la”Alur-Dill以获得实时非zeno模型[8]，还提供了一些重要的方法优势，如入侵检测[10]。像[19]这样的假设保证模块化推理是通过向I/O TC添加几个约束来获得的，而不是诉诸游戏。 在我们看来，将非zeno保存条件与假设保证中破坏循环性的条件分开具有实际和理论价值。我们认为，可接受的接口的TA可以根据它提供的信息，标签的可用性。 也就是说，（I1; O1）（I2;O2）i界面（I1; O1）对TA A的容许性意味着（I2;O2）对A的容许性.我们想研究接口之间的这种关系是否可以是一种声明性的方式来定义组合的I/O接口。我们想研究如何在界面理论[14]的框架下表达和概括我们的想法。假设保证的条件可以被削弱，例如：A和B满足输入不使紧急输出有效，A0和B0满足输入不使紧急输出无效就足够了。引用[1] Alpern ， B. ， 和 F. Schneider ， 《 没 有 时 间 逻 辑 的 时 间 属 性 》 ， ACMTrans.Programming Languages and Systems ， 11 （ 1 ） （ 1989 ） ，147{ 167.[2] 巴尔河，实时系统自动验证技术斯坦福大学，1991年。[3] 巴尔河，C. Courcoubetis和D. Dill，Model-Checking for Real-Time SystemsInProceedings of Logic in Computer Science，IEEE Computer Society，LosAlamitos，CA，414-425，1990。也在信息和计算，104（1）（1993）2{34。[4] 巴尔河和D. Dill，时间自动机理论，理论计算机科学，126（1994）183{235。[5] 巴尔河，和T.陈文辉，时变与混合系统之模组化，国立成功大学电机工程研究所硕士论文，2000。[6] Bengtsson，J.，K.G. Larsen，F. Larsson，P. Pettersson，and W.李文，一种实时系统自动验证的工具包，《混合系统学报》第三卷，第1066期，1996年，第232页。[7] Bornot，S.，和J·西法基斯一个代数框架的紧迫性出现在信息和计算，学术出版社。14[8] Braberman ，V. \Modeling and Checking Real-Time System Designs ，”Ph.DThesis，Universidad de Buenos Aires，2000。【论文】[9] Braberman，V.，和M. 实时设计的验证：将调度理论与自动形式化验证相结合，第七届欧洲软件工程会议论文集。第七届ACM SIGSOFT软件工程基 础 研 讨 会 ， （ ESEC/FSE 99 ） ， LNCS 1687 ， Springer Verlag ，Sept.1999，494{510.[10] Braberman，V.，D. Garbervetski和A.利用提交给TACAS 2002的信息改进定时系统的验证。[11] Braberman，V.，D. Garbervetski和A. Olivero，\Inuence Information toImprove the Veri Cation of Timed Systems，”Tech. 报告DC-UBA2001-003。[12] Clarke ， E. ， O. Grumberg 和 D. Peled ， \Model Checking” ， MIT Press ，January（2000），330pp.[13] 道斯角，A. Olivero，S. Tripakis和S. Yovine，KRONOS工具，在混合系统III的会议记录中，LNCS 1066，Springer Verlag，1996，208{ 219.[14] de Alfaro ， L. ， 和 TA HenzingerInterface Theories for Compatient-basedDesign，载于《EMSOFT 01：嵌入式软件学报》，LNCS 2211，SpringerVerlag，148-165，2001年。[15] 加利克河，R. Segala，J. Sogaard-Andersen，N. LynchLiveness in Timed andUntimed Systems ， In Proceedings of ICALP，LNCS 820，Springer Verlag，166-177，1994.信息与计算（1998）。[16] Garbervetsky，G.“Un M etodo de Reduccion para la Composicion de SistemasTemporizados”硕士论文，布宜诺斯艾利斯大学，2000年。[17] Henzinger，T.A.，X. Nicollin，J. Sifakis，and S. Yovine，Symbolic ModelChecking for Real-Time Systems 。 信 息 与 计 算 ， 111 （ 2 ） （ 1994 ） ，193{244。[18] Larsen，K.G.，F. Laroussinie，CMC：实时系统的组合模型检查工具。FORTE-PSTV'98，439-456，Kluwer Academic Publishers，1998.[19] 库尔尚河P.，S.塔西兰河和R. K.李文，时间系统的抽象，载于《中国科学院学报》，1996年。[20] Merritt，M.，F. Modugno和M.陈文辉，时间限制自动机，国立成功大学机械工程研究所硕士论文，民国91年。[21] Nicollin，X.，J. Sifakis和S.杨文，编译实时规范为扩展自动机，IEEETrans.在软。工程师：卷18（9）（1992），794{804.15[22] Springintveld，J.，F.范德拉格，P. D 'P.，测试时间自动机，出现在理论计算机科学，254（1-2）（2001），225{257。16>1个12>1>1LL不11[23] Tripakis，S.《时间系统与实践分析》，博士。论文，约瑟夫·傅立叶大学，1998年12月[24] Vaandrager，F.，N. 林 奇 ，行动 换能器 和TimedAutomata，在Proceedings of CONCUR'92，LNCS 630，436-455，1992中。[25] 王毅，异步代理的实时行为，在CONCUR'90会议录中，LNCS 458，Springer Verlag，1990。[26] Yovine，S.，模型检测时间自动机，嵌入式系统，G. Rozemberg和F.Vaandrager编辑，LNCS 1494，Springer Verlag，1998年。附录A关于I/O定时组件引理A.1给定 两个I/O-可置换部件 C1=（ A1;（ IA1;OA1））和 C2=（ A2;（IA2;OA2）），我们定义集合IA=IA1 [IA2，IA=fI2IA=#I>1 g，OA=OA1[OA2.C =（A;（IA; OA））是组分，其中：A = A1 k A2IA=fI2IA=8I 02IA：I6I 0^8O02OA：II IO0=;g和，OA=fO2OA=8I 02IA：I 0\O=;g[ffog=o2O2OA^9I 02IA：I 0\O6=;g证据最困难的一点是证明A1 k A2确实是非zeno无论输入转换（项目（ii），定义3.1）。我们将看到，nite run可到达的任何状态都不是时间锁。此外，时间可能会流逝，从而避免输入转换。设q是A1 k A2的nite游程可达状态，则q1=A（q）且q2=A（q）分别是A1和A2的可达状态（通过nite游程）。设k2R0为常数.从分量的定义出发，必须分别从q1和q2开始运行r1和r2。时间长度等于k，则r1不包含在lnA1中与标签的任何跃迁 而r2d在In A2中不包含与La的ny跃迁（因此，它 们 在 IA 中 不包含任何标签）。现在，我们展示一个从r1和r2获得A1kA2的游程r的过程。为了得到这样的运行，我们需要合并r1和r2。如果将r1和r2的离散变迁按出现时间排序，则很容易将它们合并得到r，直到找到另一个自动机共享为了概述合并，让我们r = q1七！L1Q17！L2：：q1 ，r= q20七！10q27！2 * q2 . 现在，假设1t11t2 n20 0n01 2t1t0（另一种情况是对称的），并且l1不被A2共享（或者它是）.然后，由于并行组合交错语义，不17t11从（q1;q2+t1）w i thr1=q17使用相同的方法获得的运行！L2 *，运行r可以按以下方式构建：r=q7！L1 （q1;q2+t1）与1 1t218LL1010和r= q2 + t0七！10q27！2 * q 0 . 显然，这个过程可以重复2 1t0t10n02直到我们到达两次运行的末尾（变量是数字两个游程的转变的次数），从而获得时间长度为k的A的游程，或者直到找到共享标签。9在不失一般性的情况下，让我们假设最早的仍然非同步化的共享输出跃迁qj7！oqj+1b延伸为r1和o2O2OA1。 设I2IA2，I0是相应的匹配输入选择（即， o2I）兼容性（条款（iv），定义3.3）。通过输入选择的定义，在第j个转换发生时，在A2中启用了标记为i 0 2 I的转换。通过输出选择的定义，在qj处还必须有a离散跃迁七！我0S. 通过应用这个过程，我们可以将两个跑去拿一个从q开始的nite运行，使得它具有时间长度k，或者它以输出转换到中间状态Q0结束。因此，由于两个TA对于输出标记的转变（I/O接口容许性的项（iv））都是非瞬态的，通过从那些中间状态（即，获得新的R1、R2等），最终建立时间长度为k的游程（如果不是，则在A1或A2上的该在Nite游程的投影将示出在Nite数目的输出标记的转换，并且由于存在在Nite数目的标记，因此至少一个输出标记将经常在Nite重复，从而违反I/O接口容许性的项（iv））。I/O接口的其余项目证明如下：新的输入和输出标签是不相交的（与输出选择相交的输入选择不是新界面的一部分输入选择属性（项（i））：给定A的状态q和IA的输入选择I，我们知道I或者到IA2。 在不 失去一般性的情况下，让我们假设它属于IA1。那么，i 2 I这样，A（q）7！伊河 我们还知道，如果i 2标签（A2），则10fig2IA2（输入选择大小为1），因此存在这样的情况，A（q）7！然后是Q7！我（r; s）。20 0输出选择属性（第（iii）项）：与前一项类似最后，包含无限多个内部或输出标记转换的运行必然是时间发散的（项（iv））。实际上，由于A的任何游程都可以投影成A1的游程和A2的游程，并且这些游程中的一个必定呈现出无穷多个输出或内部转换，因此发散。2不199注意，如果其中一个游程是空的，那么它只是在另一个游程中保留了一组离散的（0时间）转换（两者最初具有相同的时间长度），因此我们可以省略sunset x，因为我们已经构建了一个时间长度为k的游程。20>1个>1个>1个定理3.5Gi表示N个I/OTC的索引集合S=f（Ai;（IAi;OAi）g1iN，使得它们是成对相容的，我们定义集合IAn =S1I n IAi，IA n=S1infI2IAi=#I>1g，OAn=S1I n 奥阿岛C =（A;（IA; OA））是组分，其中：A = k 1 iNAIIA=fI2IAN=8I 02IAN：I6I 0^8O02OAN：II IO0=;g且，OA=fO2OAN=8I 02IAN：I 0\O=;g[ffog=o2O2OAN^9I 02IAN：I 0\O6=;g证据通过归纳。基本情况由最后一个引理解决。案例n+1。通过归纳假设，我们知道，Cn =（An;（In; On））是一个分量，其中：An=k 1 inAIIn=fI2IAn=8I 02IAn：I6I 0^8O02OAn：I\O0=;g，On=fO2OAn=8I 02IA>1n：I 0\O=;g [ffog=o2O2OAn^9I 02IA>1n：I 0\O6=;g我们知道Cn+1=（An+1;（IAn+1;OAn+1）（An+ 1;（In+1;On+1））对1in与所有的Ci=（Ai;（IAi;OAi））相容. 让我们表明这是兼容的接口为n个组件，但首先让查明一些事实的接口（I n; O n）的C n。(i) Ci（1 i n）的导出标签也由Cn导出。这来自以下事实：（a）输入标签在包含它的最大输入选择中保持为输入标签，除非在输入选择与输出选择匹配的情况下（在这种情况下，I/O），以及（b）输出标签保持在接口中。(ii) In的输入选择是其组成部件中的一些的输入选择（即，如果I 2In，则存在k 2N：1 k n使得I2IAk）(iii) 如果O是On的输出选择，如果存在k 2N：1k n使得O2OAk 并且没有大于1的输入选择与它相交，或者存在O02OAk和O=fagO0，并且存在m：1mn，使得I 02IAm I0O0