时间自动机转换新方法

理论计算机科学电子笔记130（2005）101-128www.elsevier.com/locate/entcs时间自动机转换的一种新方法Lucien Ouedraogo2部 的选举。 和比较。Eng.舍布鲁克大学SherbrookeJ1K2R1，加拿大摘要离散事件系统（DES）由它们可以执行的事件序列定义。例如，通信协议和计算机网络可以被视为DES。有限状态自动机（FSA）便于研究（即，分析、设计）DES和时间自动机（TA）是描述实时DES的方便工具。研究实时DES的一种方法是将描述实时DES的TA转化为等价的FSA，然后研究后者。本文提出了一种新的TA到FSA的转换方法。该方法适用于实时DES的一致性测试和监督控制。关键词：变换，时间自动机，集合经验自动机。1介绍离散事件系统（DES）通过执行事件与环境交互。以下是DES的一些例子：通信协议（事件：发送消息，接收消息，...）、电话系统（事件：hang on、hang up、.）、移动机器人（事件：开始移动、停止、.）.实时DES（RTDES）的正确性不仅取决于RTDES如何与环境交互，还取决于RTDES 何时与环境交互。时间自动机（TA ）[4]可以方便地描述RTDES，但TA有无限多个状态。 给出TA的状态空间的有限表示的一种方法是生成区域，1电子邮件：Ahmed. USherbrooke.ca2我是Lucien.Ouedraog o@ USh er brook e. C a1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.03.007102A.库姆西湖Ouedraogo /理论计算机科学电子笔记130（2005）101-128自动机（RA）[2]。RA的状态空间是有限的，但可以从状态爆炸中生存[2]。为了减少这种状态爆炸，已经提出了几种最小化方法来将TA转换为具有比相应RA少得多的状态的自动机[3，15，5，6，14，1]。我们提出了一种称为SetExp的新方法，用于将TA转换为有限状态自动机（FSA），称为Set-Exp-Automaton（SEA），它使用两种额外类型的事件：Set和Exp，分别模拟时钟的设置和到期。TA和相应的SEA表示指定事件的相同顺序和时序约束的两种不同方式与其他最小化方法相比，SetExp非常适合RTDES3的一致性测试和监督控制。一致性测试旨在检查实现是否符合规范[13]，监督控制旨在强制实现一致性。一个具体的定义[12]。SetExp在一致性测试中的应用监督控制）已经在[7，10]中得到证明（分别，在[11，8，9]中）。在[7，10，11，8，9]中，SetExp被用作黑盒，重点是它的应用。在本研究中，我们的目标是因此，本文是对[7，10，11，8，9]的补充。本文其余部分的结构如下。第2节介绍了TA模型。在第3节中，我们通过简单的例子来说明SetExp，并介绍了SEA模型。Sects. 图4和图5以形式化的方式解释了SetExp是如何实现的。在第6节中，我们提出了一个定理，说明了SetExp的正确性和一些性质。第7章结束了论文。2时间自动机时钟是一个实值变量，可以在发生时重置（为0）。一个事件，这样，在两次重置之间，它的衍生物（w.r.t.） 时间）等于1。设C={c1，···，cNc}是一组时钟。时钟约束是“c i k“形式的公式n ∈ {<，>，≤，≥，=}，k是非负整数.设ΦC表示依赖于C的时钟的（无限）时钟约束集。设2X表示集合X的子集的集合.3 SetExp并不旨在与验证中的其他最小化方法竞争。A.库姆西湖Ouedraogo /理论计算机科学电子笔记130（2005）101103l0Tr1TR3（; −;{c1，c2}）Tr4（{c1>1，c2<2} ; −）L1TR2（;{c13};{c1}）1，c2> 2};−）2.1TA的数量TA定义为（L，A，C，T，l0），其中：L是位置的有限集合，l0是初始位置，A是事件（字母表）的有限集合，C是时钟的有限集合，T <$L × A ×L ×2ΦC× 2C是转移关系。 因此，TA的转移定义为T=q;σ;r;G;Z，其中：q和r是起点和终点位置，σ是事件，G是ΦC的有限子集，称为T的保护，Z是C的子集，称为T的重置。图1的例子说明了这个定义。位置由节点表示，过渡Tr =q; σ; r; G; Z由连接q和r的箭头表示，并标记为（σ; G; Z）。空的G或Z用“-"表示Fig. 1. TA的例子2.2TA的语义在时间τ0= 0处，TAA =（L，A，C，T，10）在位置10处，其中C的所有时钟等于0。当q是当前位置并且保护G的所有时钟约束（如果有的话）评估为真时，启用转变Tr= Δq;σ;r;G;Z;否则，Tr被禁用。从该位置q，仅当Tr被使能时才执行事件σ;并且在执行σ之后，到达位置r并且Z中的时钟被重置。例如，图1的TA最初在位置10;它在σ出现时到达11。 从位置l1，TA到达l2，的。从位置l2开始，TA在出现φ或ρ时达到l0。 设δu，v表示事件u和v之间的延迟。我们有：δσ，μ≤3，δσ，φ2，δσ，ρ≥2，δμ，φ≥1，且δμ，ρ≥1。TAA的语义也可以由A接受的时间序列集定义。a TA的A时间序列是序列<<···<τi·· ·。 现在给一个TAA，让我们定义A对一个时间序列λ=（e1，τ1）（e2，τ2）·· ·.设n是λ的长度（n可以是无限的），λi=（ e1，τ1）···（ei，τi）是长度为i的λ的前缀，其中0≤i≤n（i是有限的）。λ被A i接受：• 或者λ是空序列λ0;104A.库姆西湖Ouedraogo /理论计算机科学电子笔记130（2005）101-128一一• 或者A具有连续转变Tr 1Tr 2···的长度为n的序列，其开始于10和s. t。i= 1，2，···，n：Tr i的事件是e i，并且在执行λ i−1之后，Tr i在时间τ i被使能。定义2.1TA的时间语言A（TL TA）是A接受的时间序列的集合。也就是说，TLTA模拟了A的行为。TA允许表达对事件之间的延迟的约束例如，为了指定两个转换Tr1和Tr2之间的延迟d使得d∈[1， 3]，我们使用时钟c1如下：Tr1的复位为{c1}，Tr2的保护为{（c1≥1），（c1≤3）}。我们将考虑的TA类遵循以下假设：假设2.1假设每个TA是确定性的，即，如果Tr1和Tr2是从相同位置执行相同事件的两个转换，并且在相同时间被使能，则它们通向相同的位置并复位相同的时钟。3SetExp，Set-Exp-Automata（SEA）本文的目的是提出一种将TA转换为有限状态自动机的方法SetExp，称为Set-Exp-Automaton（SEA），它使用两种额外类型的事件：分别模拟时钟的设置和到期的Set和ExpTA和相应的SEA表示指定事件的相同顺序和时序约束的两种不同方式在本节中，我们首先介绍事件Set和Exp，然后是一个简单的例子来说明SetExp。然后，我们提出了SEA模型，随后是与图1的TA相对应的SetExp的运行示例。1.一、3.1事件集和失效事件Set（ci;k）意味着：时钟ci被重置（到0）并且当其值等于k时将到期。而Set（ci;k1，k2，···，kp）意味着ci被重置并且将当 它 的 值 分 别 等 于 k1 ， k2 ， ··· ， kp 时 我 们 不 失 一 般 性 地 假 设k1 y}是对（x，y）s. t的集合。x > y。• 表述“A：B”意味着只要A满足，就应用B。例如：x > 3：A [x]：= 0意味着A [x]被设置为零x > 3。4.1子步骤1a：将时钟重置替换为Set事件在TA中，时钟c被重置，目的是稍后将其值与(at至少）一个常数，比如k。事件Set（c;k）非常方便，因为它重置c并编程Exp（c;k），这是c=k时的通知。子步骤1a的目的实际上是用Set（ci;k）替换ci的每次复位，如果它稍后与后续复位之前的k进行比较的话。如果对于同一个转移，我们得到几个Set（ci;k1），Set（ci;k2），···，我们用一个Set（ci;k1，k2，·· ·）代替不失一般性，我们认为k1Exp（c1，1）Exp（c2，2）TR3L0TR1（c1，3）Set（c2，2）>Exp（c1，1）>Exp（c2，2）L1集合（c1，1）<实验（c1，3）TR2L2TR4图三. 步骤1适用于图1的TA。15SetExp的第二步步 骤 2 将 AJ=StepOne （ A ） 变 换 为 SEAB =SetExp （ A ） =StepTwo（AJ）。B明确地描述了所有可能的事件序列，除了A的字母表事件之外，还包括Set和Exp事件。5.1SEA国家每一个状态的SEA是由一个位置和不等式（一个或多个）的后一个定义，我们称之为状态定义，并在本小节中给出，对于定义给定SEA的语法和语义来说是不必要的;但是在从StepOne（A）构造SetExp（A）的过程中，它对于算法的目的是有用的。一旦构造了SetExp（A），这个状态定义就可以忽略了。这里有几个必要的定义。定义5.1当至少预期c i到期时，时钟c i有效。更准确地说，当Set（c i; k1，···，k p）是最后一个发生的Set（c i; k p）时：c i是活动的，则Exp（ci; k p）没有发生。否则，c i不活动。请注意，当前活动时钟的集合取决于当前时间和自动机到当前时间的历史。定义5.2对于集合（ci;k1，···，kp），时钟条件是以下三种形式之一的表达式，其中1≤up：“<<<<<0 ci k 1“，其在Set（ci; k 1，···，k p）和Exp（ci; k 1）之间成立;“k u ci k u + 1“，其在E x p（ci; k u）和E x p（ci; k u + 1）之间成立;以及“k p ci“，其在Exp（ci; k p）之后成立。定义5.3对于一个Set（ci;k1，···，kp），ExpSeq是一个序列kuku+1···kp，其中 1≤u≤p;它指定：- 如果u>1：在Exp（ci;ku−1）之后c i将到期的剩余值;-如果u = 1：在Set（c i; k 1，k 2，···，k p）之后c i将到期的值。定义5.4一个Clock-Cond是以下四种形式之一的表达式，其中m，m1，m2是整数（它们可以是正的、负的或空的）：110A.库姆西湖Ouedraogo /理论计算机科学电子笔记130（2005）101-128“<<<→θ i−c i<$由C通过用θ i− c i替换c i得到。(v) 设θ C是一组θ Clock-Cond，θ i是一个可能在θ C中使用的时钟。通过重写其时钟条件，将θ i（如果有的话）从θ c中消除，从而从θ C中获得θ C θ i/ θ i θ c。为此，每一对电子钟都在将使用θ i的θ c彼此相加以消除θ i。为了消去θi而将两个<$C r（θ i，c j）和<$C r（θ i，c k）相加如下：1）<$C r（θ i，c j）用θ i− c j表示; 2）<$C r（θ i，c k）用c k− θ i表示; 3）将两个<$C Clock-Cond的成员相加以获得用c k− c j表示的<$C Clock-Cond; 4）如果有的话，将获得的<$C Clock-Cond与<$C r（c j，c k）组合。如果θ i被用于一个单一的时钟-条件，消除包括删除这个时钟-条件。5.3.1标记为（E）的跃迁的研究（即，类型1）设q是SEAB =StepTwo（AJ）的状态，E是一组迭代。设X是下列不等式系统（形式上描述为集合其中变量是时钟：X=<$Cq<${ci−ki0：Exp（ci;ki）∈ E}{ci−ki=cj−kj：Exp（ci;ki），Exp（cj;kj）∈ E}<${ci−ki cj−kj：Exp（ci;ki）∈EXP（q）\E，Exp（cj;kj）∈E}以下引理可用于确定在q中是否启用E。它指出E在q i中是使能的：每个Exp（ci;k）∈ E是ci的期望下一个到期日，并且X有非负解。给我5分。14（q→E）！惠（E）XP（q）和溶胶（X）/=100）。当E使dinq（注：（q→E）！），让我们正式地表示用于计算状态r的概率，不是d（q→E），在E发生之后从q4 第A.1节中的证明114A.库姆西湖Ouedraogo /理论计算机科学电子笔记130（2005）101-1281. r：=q2. Exp（c i; k）∈ E：|K r（c i）|= 0 <$C r（c i）：=（k 0Cr（ci）：=（kciKr（ci）[1]），4.|> 0 ⇒C r(c i):=(k Exp（c i; k）”或“≥ Exp（c i ;k）”，其中n k j ≥ k使得Cq（c i）=（k j c i u）或Cq（c i）=（k j c i）.以下引理可以用于确定（E，1T）（即，类型3的转换的标签）在q中被启用：引理5.36（qE，lT）！我说：(i) lT∈OUT（Lq）;(ii) （q→E）！;(iii) ”Cr：=<$Cr<$$>{Cr（cj）<$cj<$$> →cj−ci<$}9.Cr：={cj−ci=k}10.Cr（ci）：=（0

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