101网址：http://www.elsevier.nl/locate/entcs/volume65.html19页持续时间演算中的迪米塔山口Guelev1;2伯明翰大学计算机科学学院、英国数学与信息学研究所、保加利亚科学院So a，保加利亚邓文雄3联合国大学国际软件技术研究所，中国摘要研究了DC的量子扩张HDC中的一个新的态投影算子和一个多矢最小不动点算子。我们给出了公理和规则，使演绎HDC的扩展新的运营商。我们的公理可用于从HDC的一个实际有效片段中的公式中消除新的算子。这需要在新算子存在下保留该片段的某些亚片段介绍人们普遍认为，DC [ZHR 91]的基本算子，如chop算子，最小定点算子和quanti ers [Pan95]，仅在理论上足以指定实时系统的行为。关于这些算子的证明规则和公理仅在理论上足以操纵所获得的规范和进行验证。在实践中，在规范中使用扩展的基本构造工具包通常是值得的，这种方式在表示具有清晰直观意义的重复模式时实现了简洁。这就是为什么提出了一些派生算子的原因1 D. Guelev在这一条上的工作部分得到了第1000号合同的保加利亚共和国教育和科学部的I-2 电子邮件地址：gelevdp@math.bas.bg3 电子邮件地址：dvh@iist.unu.educ2002年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。102不同的作者。使用这样的运营商和派生的公理和规则，他们可以变成至关重要的，以保持规范的复杂性和演绎验证DC合理低。导出算子使DC设计与规范之间的对应更简单、更直观。一组经过深入研究的此类运算符是例如可实现的[Rav95，Die00]本文研究了一个新的态上投影算子和DC在态上的量子扩张中的prex算子以及一个多矢最小不动点算子HDC [Gue00a]. 在[DVH99]中将投影到状态引入DC。它可以被视为离散时间ITL投影算子的实时变体，如从[HMM83]已知的。这个算子提供了一种方法来调和真正的同步假设，即在实时系统中计算不需要时间，而在现实中计算确实需要时间，这很难准确计算并且大小可以忽略不计，但需要保持计算步骤的因果顺序清晰。通过将不考虑计算时间的并发实时程序行为的状态要求与明确考虑计算时间的并发实时程序行为规范投影到HDC公式中。我们提请注意前x算子，因为它允许直接定义所观察行为的初始部分的属性。与对称定义的suprix算子一起，它允许指定观察到的行为是从观察延伸到未来和/或过去的某些行为的一部分的可能性。随着这两个算子的定义和应用的建议，并发实时程序的规范和验证，本文提出了以下结果：我们给出了全面的公理和规则的列表，使推导在HDC的扩展新的运营商。我们的公理可以用作减少规则，使新的运营商从公式开始，在speci- tions的建议。这意味着有一个实际上显着的HDC片段，其中前x和投影到状态的运营商可以被视为派生运营商和该片段的某些子片段的可判定性是保留在新运营商的存在1Real Time HDC在本文中，我们提出的HDC的情况下，实时的。我们允许实值状态变量[ZRH93]，其用于在我们的示例中指定DC与投影和pre x的并发交织过程的行为的规范中指定数据操作我们不提及邻域项和HDC的一些高阶量子，以保持我们的演示简洁。这就是为什么这里的HDC变体更接近于[Pan95]的DC变体，其中第一次引入DC，以及来自[ZGZ 99]的HDC。103R1.1语言一HDC词汇表由常量符号a、b、c、：、函数符号组成 f，g，：和关系符号R，：x，y，：：和布尔状态变量P，Q，：：和实状态变量p，q，* ** 在整个文件中，我们表示各种HDC符号和这里一样的字母为了简洁起见，我们依靠这些字母的用法来暗示所考虑的特定符号的种类。常量符号、函数符号和关系符号既可以是刚性的，也可以是柔性的。严格的象征因其解释上的限制而被区别开来。元0的柔性关系符号和柔性常数符号又分别称为时态命题字母和时态变量。字母X、Y、：默认表示速度- Ral proposal letters.个体变量是刚性的。状态变量灵活。每一种HDC语言都包含严格常数符号0、时态变量`、严格二元函数符号+、严格二元关系符号=和，以及单个变量、状态变量和时态命题字母的集合。给定HDC语言的词汇表，其状态项s、状态表达式S、项t和公式'由BNF定义：s ：：= cjxjpjf（s;：; s）S：：=0 jP jR（s;：;s）jS）St ：：= cjxj Sjf（t;：;t）'：：=？jR（t; ：;t）j：'j'_'j（';'）j9x' j9p'j9P' j iX ：X：';：;'在状态项和状态表达式中只允许使用刚性常数、函数和关系符号。 X1：Xm：'1; ：;'n类的F或m是良构的，仅当X 1;：; X m是不同的变量，它们的所有出现在'1; ：;'n中，并且m = n。仅使用刚性符号构建的项和公式称为刚性。1.2语义HDC语言L的抽象模型M是一对hF;Ii，其中F描述M中时间的特定结构，I描述M中L的非逻辑符号的含义，包括变量。本文中F始终是实hR;0;+;i的线性序群。 基于这个原因，我们用解释成分来识别模型。下面的辅助符号有助于简明地定义这些解释定义1.1We表示集合f[1;2]：1;22R;12g byI. Given1; 22 I，1; 2代表1[2i max 1= min 2。R 上 的函数f104V从X1;：;Xn给定任何类型的变量V，L的解释I和J被称为若f的值域为nite，且给定1; 22 R，f：f（）=c，且1<2 g是f值域内[0; 00）类整数的nite并，则f具有nite可变性.nitevariability prop ter yret e让我成为 HDC语言。定义1.2L的HDC解释I是关于L的非逻辑符号集合的函数，包括变量。各种符号的I值的类型如下：I（x）2RI（f）：IRn！ R I（P）：R！f0;1gI（c）：I！ RI（R）：IRn！ f0;1 g I（p）：R！R这里n分别代表R和f的arity。状态变量的解释应该具有nite可变性属性。刚性符号的解释不应完全依赖于它们的间隔论证这就是为什么它们经常被视为其实参数的函数，并且在0进制符号的情况下只是R的元素I（0）、I（+）、I（）、I（=）和I（`）应该是h R的相应分量;0;+;i，等于yonR和：maxmin，分别。定义1.3给定L的解释I，状态项s的值I（s）和状态表达式S在时间点的值I（S）以及项t在间隔2I的值I（t）由以下子句定义：一（c）=I（c）（[ ; ]）I（p）=I（p）（）I（x）=I（x）I（f（s1;：;sn））=I（f）（[ ;];I（s1）;：;I（sn））（0）=0I（R（s1;：;sn））=I（R）（[ ;];I（s1）;：;I（sn））I（P）=I（P）（）I（S1）S2）=maxf1I（S1）; I（S2）gI（c） =I（c）（）I（RS）=miRnmaxI（S）dI（x）= I（x）I（f（t1;：; tn））= I（f）（; I（t1）;：; I（tn））选择[;]出现在关于I（c）的子句中是任意的。在状态表达式中只允许严格的c，并且这样的c不依赖于它们的值的引用区间这同样适用于关于I（R（s 1;：; s n））的子句。V -同意，如果I（s）= J（s）对于所有非逻辑符号s 6：L。让A：我！f0;1g代表特征（membership）函数的I. 设X1;：：：;Xn是来自L的时间命题字母. 给定A1;：; AnI，我们引入L的定义为IA1;：：;An的解释，105RnF（A; ：; A）=f2I：IA1;：;An; j='g;i=1; ：;n;通过等式IA1;：;An（X）=，i=1; ：;n，和IA1;：;An（s）=I（s），X1;：;XniAiX1;：;Xns62fX1; ：;Xn g. 设jX1：Xn：'1; ：'n是L中的mula的a。则映射：2I！2Ithatwede nebytheequalities：i1nX1;：;Xni是单调的，因此方程组：Fi（A1;：; An）= Ai;i = 1;：;n有一个关于A1;：; An的最小解，相对于排序关系。我们将这个解的分量按照它们的标准顺序表示为yAI;1X1：Xn：'1;：'n; ：AI;nX1：Xn：'1;：'n。定义1.4建模关系j=L的解释I、区间2I和来自L的公式由以下条款定义：我的;j=？我的;j= R（t 1;：; t n）iI（R）（; I（t1）;：; I（tn））= 1I; j=：'i I;j='我的;j='_i或者I;j=或I;j='I;j=（';）i存在1;22我认为，为1; 2，I; 1 j='和I; 2 j='I; j=9V'i J; j='对于某个J，V-与II;j=iX1： Xn：'1; ：;'ni2AI;iX1：Xn：'1;：;'n1.3缩写我们用>，^，），8，6=<，>作为缩写，并以通常的方式用x表示。以下缩写为DC专用：10）0，dSeS=`^`6=0，3'（（>;'）;>），2'：3：'.迭代（：）和正迭代（：） +在HDC中可以通过子句'X ： '=0_（';X），'+（';'）来定义。状态变量quanter允许指定隐藏局部变量[ZGZ 99，HX 99]。这个quantier的另一个用途是表示超密集chop [ZH96，HX99].DC中的最小定点运算符使时态程序中的递归调用能够直接指定假设时态命题字母X用于表示某个递归时态过程的完整执行 然后这个过程的行为可以用一个公式来描述，它有X的出现来表示递归的自调用。最后，这种行为的规范的封闭形式可以由公式 1X ：的HDCpolyadic形式可以类似地用于指定相互递归过程的集合的行为，如图所示。106ZHHHHHH注意，上述情况取决于区间h的类型，而不仅仅是在下面的第3节中。多元数与一元数具有相同的表达能力。一个多进公式可以通过使用 Beki c原则（参见例如[AN01]）。比如说，j=HDC1X1X2：'1;'2，X1：[X2：'2=X2]'1.多元的 似乎比一元更方便对于本文的目的，嵌套出现。2投影到状态和前x上2.1投影到状态公式'到状态表达式S上的投影（'= S '）在间隔在解释I下，如果'在解释I：I（S）下在间隔：I（S）处成立。的间隔：I（S）是通过将满足S。I：I（S）是通过将I下的符号的（真值）值的对应从时间点和子区间转移到它们在I（S）中的图像来获得的。这个定义可以用几种方法来精确。下面我们给出了我们这样做的选择。让HDC公式的语法被扩展为允许这类公式（“= S”）。我们使用下面的辅助符号将关系式j=推广到这类公式。让h：R！ f0;1 g具有夜间可变性，并且R由等式，Thread（）=0h（0）d0：设h=f<$h（）：2R g. 通过定义h，将区间值f2R：h（）=1g的集合粘在一个区间h中.显然，h要么是闭区间，要么是半闭无界区间，要么是整个R，0 2h。将任意的解释从R转换到h嵌入到R中，我们需要一种新的平衡。让我们来看看：R！2R是R的多值逆，由等式定义1（0）=f2R：我们需要一个单值分支的单调扩张于R. 的延伸利用该属性，我们选择采用的可以定义如下：h（0）=0inf h+最大值≤ 1（inf h） 如果00，如果infh=0=向上h= 0：H107在0。读者应该在头脑中回想h的各种可能性，以适应它。定义2.1给定某个HDC语言L的解释I，I到h（的支集）上的投影Ih是L的HDC解释，它由等式定义：Ih（x）= I（x）对于单个变量xIh（c）（）=I（c）（[h（min）;h（max）]）对于常数c=6：`I h（s）（ ; d1;：; dn）= I（s）（[h（min）;h（max）]; d1;：;dn）对于n元函数和关系符号对于状态变量P，Ih（P）（）= I（P）（h在21中，在h上的p_（p_）h）是[p_（p_）;p_（p_）]。现在设'是一个公式，H是L中的一个状态表达式。设h =：I（H）。然后我的;j=（i = H）iIh;h j='。注意，在如上定义和使用h的情况下，Ih是通过裁剪R的o部分从I获得的，所述o部分被h仅计算为1的部分包围如果h是（半）有界的，也就是说，如果infh2R，或suph2R，或两者，f 2R上I的值：）的非终止游程的初始子区间满足。类似地，类型（：=Ri_：N）和（：=R i _： N）的投影也可以是相同的。Rj：N）可以是j2J用于将整个程序P的行为的属性指定为可观察的分别由单个组成过程Pi或组成过程的子集fPj：j2 Jg表示4投影到状态上的公理和规则在这一节中，我们将研究作为HDC算子之一的状态投影。我们将（：=：）的一些有趣的性质公式化为HDC有效公式，112RRRRRRRR rrR如果R ，也不 发生在t1，：，tn中，则R证据规则我们指定一个片段的HDC与投影到国家承认一个简单的真理保持翻译成HDC没有投影。这种翻译可以用我们的一些公理作为翻译规则来定义。翻译的存在需要关于另一个较小的片段的HDC与投影的可判定性结果。最后，我们给出了一个关于投影的一般证明规则。4.1关于状态和基本HDC算子的(1)j=HDC'，（'= H），对于来自L的刚性'。设2I，I是某个HDC语言L的解释，H是L中的状态表达式，h =：I（H）。则minh maxh意味着Ih（H）= 1。因此（二）j=HDC（` = H=H）。Max自从maxhminh =miRnI（H）d，Ih（`）=I（RH）。这个跟那个(3)j=HDC（`= x=H），H = x类似的考虑表明，（4）j= HDC（S = x=H），（S^H）= x.这意味着，在原子的情况下，只有在S出现的地方加上（S ^ H），才能用严格的符号和子项从（'= H）中消除（：= H）。如果'是原子易变公式，则可以消除（：=H）R（t1;：; tn）满足9x（H=x^（2（ H=x）R（t1; ：;tn））_2（H=x）：R（t1; ：;tn）鉴于此，j=HDC R（t1;：;tn），（R（t1;：; tn）=H）(5)j= HDC（dHe; >）^（“R（t1;：;tn）^ H = x; dHe; >））（（“R（t1;：; tn）^` = x;>）=H）其中“代表要么：要么什么都没有。简单的论证表明：（6）j=HDC（：'= H），：（'= H）（7）j=HDC（'=H），（'=H）_（=H）（8）j=HDC（（';）=H），（（'=H）;（=H））（9）j=HDC（9V'=H），9V（'=H），如果可变Vd不发生在H中（10）j=HDC（（'= S）=H），（'= S^H）(11)j=HDC'）意味着j=HDC（'= H））（=H）（12）j=HDC （H1，H2）=`意味着j=HDC（'=H1），（'= H2）（13）j=HDC（'=1），'（14）j=HDC（（i）=0），（i）=0）113J我证据 考虑 HDC公式集k;：;k，k<！， 这++k+1=k[f[1=X1; ：;n=Xn]'i：12k; ：;n2kg，j=1; ：; n让k;：;k，k<！，类似地定义，但使用1;：;n代替%1; ： ：;%n. 设（k= H）=f（=H）：2k g，j=1;n，k<！.它可以k（I;j=（=H））。后者相当于9 K<！9 2k（I;j=），4.2投射到国家和到目前为止列出的有效公式足以在HDC中处理（：=：），而无需例如，推动它走向原子公式。接下来，我们将这种方法扩展到一个包含HDC的HDC片段。命 题 4.1LetH 是 一 个状 态 表 达 式 ，“iX1 ： X n ： ”1; ： ;“n ， 并且”1; ：;“n 中的X1;：; Xn的任何一个occurrences都不在n的运算中，也不在or（：=：）的运算中。通过向内驱动投影并且最终分别用X1;：; Xn替换（X1 =H）;：;（Xn =H），j = 1;：; Xn，可以从（j = H）获得e d。 让i X 1：X n：1;：;则j=HDC（i = H），1N定义如下：0= f？Gjj1n1NJ J可以证明，（k=H）中的每个公式都有一个等价公式，k和J J反之亦然在'1; ：;' nn n尾中使用：的限制是I;j='i9 k<！92 k（I; j=）.因此，I; j=（'= H）等于9 k<！92我我是我;j= 0。2显然，这个命题最有用的推论是：（ 16 ） j=HDC （ i=H ）， （ （ i =H ） ;RH=0 ） ，j=HDC（'=H），（'=H）4.3投射到一般我们用关于（：=：）的一般证明规则来结束这一节。它适用几乎所有保守的DC扩展（：=：），仅使用内省模式。我们首先给出一些建议这一规则的意见。假设引入到de ne（：=：）的符号。由于h的持续时间永远不会超过的持续时间，所以条件Ih;h j=“可以由I 0;h0j=”中的一个等价的条件来代替，其中h0=[min;min+maxhmaxh]和I0是L的一个解释，它以Ih对h的方式对h0进行了运算。接下来，所有出现在'中的灵活符号都可以被替换为新的，从而获得了一个同构的mula'0，和I 0可以被替换为一个解释I 0 0，其 中I 00只定义在这些symbol上，并在它们上产 生 与I 0d在原始symbols上相同的值。这一切都是因为条件Ih;hj='tobereplaced byyI 0 0;h0j='0. 后者是等价的到I 00; j=9x（R H=x^（`=x^'0;>））;114^ss）（`=x;`=y^[s=s; ：;s=s]';>）i=1VI H0我0110nn0@@8x1： 8xn 8y 8zB0（R H=y;（dHe;>）^R H=z^R（x1; ： ：;xn）;（dHe;>））1C8x8y8z0y+zRH）0（RH=y;RH=z^R （P^H）=x;>）118x8y8z8t0y+zRH）0（RH=y;RH=z^R （p=t^H）=x;>）11100nH最后，对于实状态变量p和p0，pHp0是现在，假设s1; ：;sn是'的灵活系统块，并且s0; ： ;s0是所提供的x在“中没有自由发生。 现在让L0是L通过用于放置在'0中的 新鲜灵 活系统 的扩展。那么I[I 0 0]是L0的一个解释，I[I; j=（'=H），9x（R H=x^（'=x^';>））让我们通过DC来指定m ulas在的子值处的灵活系统f '上的I的值与在对应的h 0的子值处的从' 0开始的它们的对应点上的I00的值之间的期望关系。设R和R0是n-位置关系系统.We表示为（y+zR H）1，（`=y;R0（x1; ：;xn）^`=z;>）byRHR0. 设n2，f，f0为n元函数集.然后，我们表示通过将f（x1;：;xn1）=xn和f0（x1; ：;xn1）=xn分别用fHf0代替R（x1; ：;xn）和R0（x1; ：;xn）。对于可变常数c和c0，cHc0是在上述公式中的相应位置代入c = x1和c0 = x1的结果，其中n=1。RHR0中的子公式（dHe;>）是为了确定I对有足够的信息对于h0的子变量，因为可能有have（（））>，如果Hh（）= 0. 对于布尔状态变量P和P0，HP0是@@，（`=y;`=z^RP0=x;>）AA@@，（`=y;`=z^R （p0=t）=x;>）AA分别与s1;：; sn相同种类和性质的新符号，规则可以写下来如下：n（P和R）^（RHx+y;dHe;>））：（RH=x;RH=y^：（'=H）;dHe;>）5HDC的d-P-e-片段在状态上的投影是可判定的HDC的dP e片段中公式的BNF是'：：=？j'=0jdSej：'j'_' j（';'）j'j9P'已知可以从HDC dP e公式中消除9P和：是，对于每个HDC dP e-公式，一个等价的无量化和否定-AA115RR（四）j= HDC（f（x 1;：; x n）= x n+1），灵活的f可以在相同的词汇表中构建一个免费的。在本文的符号证明可以在[Gue00b]中找到。子节中的有效等效项4.1 4.2和4.2的结论是，给定这样一个公式“和一个状态表达式H，等价于（”= H）可以用只在（“= 0=H）和（dSe=H）类的然而，有效的等价物（`=0=H），`=0_d：He和（dSe=H），（dH）Se）^3dHe表明投射到状态上也可以从这些子公式中消除。因此，每个公式从dP e-片段的HDC与投影可以转化为一个等价的quantier和投影自由。如[ZHS93]所知，这些公式的有效性是可判定的。6n和su的公理和规则在HDC本节的结构是在上一节关于HDC中的（：=：）之后。6.1HDC、 SU和基本HDC算子下面的带有和su的有效HDC公式没有明确引用。它们中的大多数只处理数据库和HDC操作员之间的交互。为了得到关于su的相应等价，应该交换（：;：）的操作数。(1) j=HDCpref（“），”对于刚性“(2) j=HDC（S = x），S x(3) j=HDC（ R（x1;：：;xn）），对于灵活的R(5) j=HDCpref（c=x），适用于exiblec6=：`(6) j=HDC：pref（'）pref（：'）(7) j=HDCpref（'^））pref（'）^pref（'）(8) j=HDCpref（'_），pref（'）_pref（）（9a）j=HDCpref（（';））pref（'）_（';pref（））（9b）j=HDC （';pref（））pref（（';））（9c）j=HDC `=0^su（'））pref（）隐含j=HDCpref（'））pref（（';））（十）j=HDC pref（9x'），9xp ref（'）（十一）j=HDC pref（9P'），9Pp ref（'）（十二）j=HDC '）隐含j=HDCpref（'））pref（）（十三j=HDC （：pref（'）;>））：'116）（十四）j=HDC '）：（：;>）意味着j=HDCpref（'））（十五）j=HDC pref（p ref（'）），p ref（'）（十六）j=HDC （pref（'）=H））pref（（'=H））n和su的叠加（17）j=HDC'）2pref（su（'））(18) j=HDC'）2意味着j=HDCpref（su（'））117_0_BBlj;kW （j;k;0;ij;k;1;：;i j;k;p1HDC我(19) j=HDC3'）隐含j=HDC'）<$（su（））(20) j=HDCsu（pref（'）），pref（su（'））6.2苏，苏，就像在投影的情况下一样，上面列出的有效公式和规则的重点是在尽可能的程度上将xu和su在本小节中，我们证明这也可以用一些公式来完成。 我们得到的HDC片段是命题4.1的一部分。设H是一个状态表达式，iiX1： Xn：'1; ：;'n，i=1; ：; n，且X1; ：;Xn在'j，j=1; ：;n，b中的任何自由共现都不在否定的作用域中，也不在，（：=：）的作用域中，也不在绑定单个变量的量化器中.引理6.1每一个“j，j=1; ：;n”都等价于（1;： ;l）类公式的一个析取，其中k2fX1; ：;Xng或k没有X1;：;Xn， k = 1;：; l的自由出现。证据 等效公式可以通过应用j=HDC9P（'_），9P'_9P和j=HDC9P（';），（9P';9P）和（：;：）在析取上的分布性作为'j的子公式的约简规则，其中' j的子公式出现在X1;：; Xn上.2接下来我们假设，：'j=（j;k;0;Xij;k;1;j;k;0;： ：;j;k;lj;k;Xij;k;lj;k;j;k;lj;k）;i;j=1; ：; nk=1其中j; k;0; ： ：;j; k;lj;k不具有X1; ： ：;Xn的自由共现。因为j=HDCi，[1=X1; ：n=Xn]'iwehave0lj;k1mjW （j;k;0;ij;k;1;：;ij;k;p;pref（j;k;p））_j=pref（），_B p=0Ck=11个;j;k;p（ij;k;p））p=1在上面的等价关系中，用Y1;：; Yn代替n（1）;：;n（n）表明，j=HDCn（i），iY1：Yn：1;：;n;i= 1;：;n其中lj;kmjW （j;k;0;ij;k;1;：;ij;k;p;pref（j;k;p））_p=0ilj;kk=1@W （j;k;0;ij;k;1;：;ij;k;p1;j;k;p1;Yij;k;p）CAp=1MJ118RR这可以通过直接检查定义中的“不确定性”来确定。6.3可表示性的限制前两节中关于π和su的有效等价性意味着这些运算符可以用一种HDC，它限制了由运算符约束的时间命题字母不能出现在对个体的量化器的作用域中，也不能出现在该运算符的参数中的（：=：）的作用域中。不幸的是，没有一般的证明规则，可以制定关于苏和苏。之所以如此，是因为j=HDCpre f（（“6=0;”））等于“的满足能力。因此，只有具有相同有效性和满足性复杂度的pref的HDC片段才可能具有完备的公理系统。特别是HDC与否定，那么满足能力是不可递归的，因为著名的波斯特定理（Theorem of Post）。例如[Sho67]）。因此，这样的片段不能递归地轴对称化。备注及相关工作正如我们在引言中提到的，第一个类似于DC的逻辑被投影算子扩展是离散时间ITL [HMM 83，Mos 86，Mos 95]。另一个有趣的推广的一个IT L投影运营商在[Mos86，Mos95]中介绍，可以发现在[He 99，Gue00c]。DC中的状态投影背后的想法可以追溯到DC的早期变体，其中提出了由离散计算微时间组成的异质时域来指定控制器的内部工作，以及用于受控设备工作的密集宏时间[PD97]。在DC的这种变体中，有两个灵活的常数‘和’，分别用于测量宏观和微观时间。在我们的例子中，这些常数可以分别定义为：N和N。这些持续时间项在（：=：N ）和（：=N）的范围内相等。前x运算符的特殊情况在前面已经被用来简化符号，参见[Die96，DVH99]。运算符和su可以被认为是[Pan96]中引入DC的一对扩展模态的非确定性版本。这里给出的映射、su和投影到状态的语义，以及关于这些算子的公理和证明规则旨在实时HDC中最大可能的通用性。 相反，所提出的方法来指定并发时态程序的行为已被定制，以尽可能少地使用DC的扩展功能。特别是，非终止行为，通常需要扩展模态或无界区间来指定，已经用几乎普通的方法处理了。- 与特殊条件上[[：]]0公式举行的所有有界初始119我仅考虑非终止行为的子区间。计算时间的显式计算，通过使用状态投影来制定需求的可能性来补偿，也使得分配的指定不涉及超密集chop（参见。例如[HX99]。）HDC的一个基本特性，在示例行为规范中没有使用，但肯定需要管理一个完整的边缘编程语言，是状态变量绑定的量化器。需要指定局部变量（参见[HX99]），为了简单起见，我们的示例语言由于递归调用，局部变量可以以无限数量开始，因此不能被视为在[[P ]] i和[[P ]] 0类公式中自由出现的有限的全局作用域和范围的变量中的一些。一个适当的
我的内容管理
展开
