拓扑（双）模拟：从拓扑角度重新定义标记的状态空间上的过渡系统，能够比较无限跃迁序列的累积状态，并得到类似结果

理论计算机科学电子笔记100（2004）49-64www.elsevier.com/locate/entcs拓扑（双）模拟P.J.L. Cuijpers1，2 硕士Reniers3荷兰埃因霍温理工大学数学与计算机科学系摘要在本文中，我们认为模拟和互模拟在混合系统的背景下是不够的，因为它们只能比较在有限数量的过渡中可达到的状态为了解决这个问题，我们扩展标记的状态空间上的拓扑结构的过渡系统。我们定义了模拟和互模拟的拓扑版本，它们也能够比较无限跃迁序列的累积状态我们表明，过渡系统的一个不离散的拓扑结构，拓扑（双）模拟和标准（双）模拟一致。对于具有离散拓扑的有限转移系统也得到了类似的结果关键词：标记跃迁系统，（双）模拟，拓扑，累积，拓扑（双）模拟。1介绍计算机科学中使用的许多技术的语义依赖于标记转换系统，包含一组表示系统物理状态的对象的结构（因此对象被称为状态），以及标记转换，表示将系统从一个状态带入另一个状态的行为自从van Glabbeek [11]的工作以来，计算机科学中普遍认为互模拟[18，16]是等价的最强概念。1我们要感谢Progress/STW（Grant EES 5173）、Philips-CFT和Assembleon对本项目的财务和物质支持。2电子邮件：P.J.L. tue.nl3电子邮件：M.A. tue.nl1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.08.01750P.J.L. Cuijpers，M.A. Reniers / Electronic Notes in Theoretical Computer Science 100（2004）49-对标记的过渡系统感兴趣。然而，例如在混合系统领域，需要比互模拟更强的等价性。在那里，Zeno行为问题（在有限时间间隔内发生的无限数量的事件[20，6，3，13]，在哲学中也称为超级任务[19，22]），产生了被认为是不同的标记转移系统，但不能使用互模拟来区分尽管在哲学上对现实中是否存在Zeno行为存在争议接下来，我们通过两个例子来解释两个这样的原因，在这两种情况下，从[13]。零行为通常来自于为了简化混合系统建模而采用的建模抽象。一个简单的例子是弹跳球。球在表面上弹性地反弹，每次反弹都会损失一部分能量。在这种弹跳球的简单模型中，人们可能希望从球在表面上弹跳的情况下的动力学中抽象出来，并简单地将其建模为离散事件。事实证明，在有限的时间内，会发生无限数量的反弹。因此，简单的弹跳球模型采用Zeno行为。由于应用某些控制策略，混合系统模型中也会出现零行为。这种现象通常被称为控制模式之间的无限快速切换。在[13]中给出了水箱系统的示例。水箱系统由两个水箱组成（见图1）。水以一定的恒定速率（v1和v2）从这些水箱中流出v2）。在每一个时刻，水都是一体的（而且是精确的一体）。在速率为w的罐中。目的是保持水箱的水量（分别为x1和x2）高于某些特定水平（分别为r1和r2）。 这是通过在适当的时间在罐之间切换输入流来实现的：每当x1≤ r1时，输入流切换到罐1，每当x2≤ r2时，输入流切换到罐2。 如果输入流大于每个输出流（w> v1和w> v2）且小于输出流之和（w 1，如图中所示，是以下非拓扑事实的证明：P.J.L. Cuijpers，M.A. Reniers / Electronic Notes in Theoretical Computer Science 100（2004）49-64 59∩图五.一个标记的转换系统。• 状态1由状态2模拟，即，1• 状态2由状态1模拟，即，2• 状态1和2是双相似的，即，1参加 2.注意，状态1和2的双相似性并不直接从模拟1“2和2“1得出，因为对于双相似性，见证模拟的关系必须彼此相反。较弱的等价“ “ -1 在 文 献 中 被 称 为 相 似 性[ 1 1 ] ， 它 不 具 有 这 种 相 似 性 。要求。注意，我们现在比较的是来自同一个标记的跃迁系统的状态。因此，对于状态起源于的标记转换系统，因此，我们从符号中省略了现在，考虑在这样的假设下的拓扑概念，即该标记转移系统的状态空间X通过离散拓扑TD（X）= 2X来构造。状态2仍由状态1：2“top 1模拟 这是由于以下意见。状态2没有累积的无限次运行因此，无限运行不必被这种从状态运行模仿1.然而，在该设置中，状态1不被状态2：1/n到p 2所模拟。状态1具有在状态1中累积的无限游程。因此，状态2也应该具有这样的游程，并且此外，它应该在相关的状态中累积。到状态1。然而，从状态2开始的运行根本不累积。同样的观察导致了这样的结论，即状态1和状态2不是拓扑双相似的：1~top 2。传统上，在计算机科学中，系统被假定为离散的，没问题。上面我们已经表明，状态空间由离散拓扑结构化的假设不足以得出拓扑和非拓扑概念一致的结论。基于这一点，读者可能倾向于相信，对于具有有限状态空间和任意拓扑的标记转移系统，非拓扑和拓扑概念是一致的。同样，情况并非如此。考虑标签60P.J.L. Cuijpers，M.A. Reniers / Electronic Notes in Theoretical Computer Science 100（2004）49-T1--∈12B一534一C6见图6。具有有限状态空间的标记转移系统。图6所示的过渡系统。这个标记的跃迁系统的状态空间是有限的：X= 1， 2，3， 4， 5， 6。考虑到非拓扑概念，我们观察到状态2和3相互模拟并且是双相似的。假设这个状态空间上的拓扑由基给出，B={{1，2}，{3，4}，{5}，{6}}。在图中，来自这个基的具有多个元素的开集被聚类。现在，由于施加在状态空间上的拓扑结构，有n个无穷erun（→x，→σ），其中h，fn在状态1中累积的N1→x（n） =2和nd→σ（n） =a。为了使状态2被状态3拓扑模拟，该方法意味着在与状态1相关的状态中积累具有h→y（0）=3的有限个元素run（→y，→σ）的这些 唯一的候选人对于这种累积，是状态3和4。但是，这两者都不能与状态1相关，因为状态1可以执行动作b，而状态3和4不能。类似的推理表明，状态3不能由状态2. 在此之前，我们有2/“到p 3和3 /“到p 2。作为一个相反的问题，也不是拓扑双相似的。然而，如果一个离散标号转移系统的状态空间是有限的，那么（双）模拟和拓扑（双）模拟的概念是一致的。定理5.3对于离散的M1和有限的M2，我们有，对于所有的x1∈X1，且x2∈ X2：M1，x1“top M2，x2当且仅当M1，x1“M2，x2.证据 拓扑模拟蕴涵普通模拟的证明由定理4.2得出。 证明了普通模拟蕴涵拓扑模拟。 假设M1，x1“M2，x2由下式证明：模拟R. 我们证明R也是一个拓扑模拟。除此之外，设t（→r， →σ）是 M1中h→r（0）=x1且t∈X 的 一 个 环 . Supposethat→ry. 设对n∈dom（→σ），σ→n：N→dom（k）= → σ（k），定义为d y σ → n（k），对所有k

下载后可阅读完整内容，剩余1页未读，立即下载