并发约束程序设计及时态逻辑模型检测的在线获取与实现原型工具

可在www.sciencedirect.com在线获取理论计算机科学电子笔记312（2015）161-177www.elsevier.com/locate/entcs时间并发约束程序设计Jaime Arias1Univ. Bordeaux，LaBRI，UMR 5800，F-33400 Talence，FranceCNRS，LaBRI，UMR 5800，F-33400 Talence，FranceMichellGuzm'an2我知道，LIX，La bo ratoi redel'E cole Polyt e chnique ass o c i 'e ` a l'INRIA/CORDI-S。 Fran ceDECC，Universidad del Valle. 哥伦比亚Carlos Olarte3北里奥格兰德联邦大学巴西纳塔尔DECC哥伦比亚摘要并发约束编程（ccp）是一种并发模型，其中代理通过告知和询问约束（即，逻辑中的公式）转换为部分信息的共享存储。ntcc演算用离散时间单位的概念扩展了ccp，用于反应系统的具体化。此外，ntcc的特点是构造函数用于非确定性选择和异步行为，因此允许对于（1）在时间单元期间经由约束蕴涵的过程的同步和（2）时间间隔上的过程在本文中，我们开发的自动验证的ntcc程序的符号模型检查的基础上所需的技术我们表明，内部的过渡关系，建模过程中的时间单位（1以上）的行为，可以象征性地表示在一个合适的片段的线性时间时序逻辑的公式。此外，通过使用标准的技术作为差异决策图，我们提供了一个紧凑的表示这些约束。然后，依靠时间结构的定点表征，我们获得了可观察转变的符号模型（上面的2）。我们证明了我们的建设是正确的操作语义。 最后介绍实现我们方法的原型工具保留字：并发约束程序设计，时态逻辑，模型检测1电子邮件：ariasalmeida@gmail.com2电子邮件：michellrad@gmail.com3电子邮件：carlos. gmail.comhttp://dx.doi.org/10.1016/j.entcs.2015.04.0101571-0661/© 2015作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。162J. Arias等理论计算机科学电子笔记312（2015）1611介绍在过去的几年里，我们已经看到并发约束编程[20，21]（ccp）是如何被广泛用于指定和编程并发系统的。社区对这种强大的并发模型越来越感兴趣，这是由于它的简单性和与逻辑的紧密联系：进程在部分信息的存储中告诉和询问ccp模型的使用已经渗透到科学的不同领域（例如，生物化学系统），工程（例如，安全协议、移动和面向服务的计算以及社交网络）以及甚至现有技术（例如，多媒体交互工具）然而，尽管有许多语义和逻辑框架被设计来推理CCP过程，CCP程序的自动验证到目前为止还没有得到多少关注。本文旨在提供理论和实践工具来验证ntcc[16]演算中指定的系统，这是ccp的时间扩展，用于对反应系统进行建模。为此，我们提出了一个符号表示的过程中的行为，我们证明，这种符号模型是适合作为一个标准的模型检查技术的基础定义这种符号表示的挑战之一是ntcc的操作语义由两个不同的转换关系给出：表示时间间隔内过程步骤的内部转换和描述过程如何沿时间单位演变的可观察转换。此外，所提出的模型必须处理ntcc中的两个非基本时态结构：！P在P的有限个副本中执行（每个时间单位一个），*P通过将P延迟无限（但有限）数量的时间单位来描述异步行为。正如我们将看到的，我们可以通过定点计算来巧妙地描述这些构造的行为组织和捐款。我们开始回顾第2.1节中的ntcc二、 第3节描述了我们的方法来象征性地表示ntcc流程.我们证明了对于任何过程，符号模型都可以在有限步数中得到（定理3.6），并且我们的构造在操作语义上是正确的（定理3.9）。在第3节中，我们还提供了一些例子来说明如何计算过程的符号模型。第4节描述了我们将用来指定属性的逻辑，第5节展示了如何在标准（符号）模型检查算法中使用符号模型在第6节中，我们指出了相关的工作，并简要描述了一个实现我们方法的原型工具。2NTCC演算并发约束编程（ccp）[20，21]（参见[17]中的调查）是一种并发模型，它将进程演算的传统操作视图与基于逻辑的声明性这使得ccp能够从过程演算和逻辑的大量推理技术J. Arias等理论计算机科学电子笔记312（2015）161163ΣΣΣccp中的进程通过在部分信息的公共存储中告知和询问约束（信息片段）来相互交互。过程可能作用的约束类型不是固定的，而是约束系统（CS）中的参数。直观地，CS提供签名，根据该签名，可以从基本令牌（例如， 谓词符号）和变量，以及两 个基 本 操 作 ： 合 取 （ H ） 和 变 量 隐 藏 （ H ） 。 CS 还 定 义 了 一 个 蕴 涵 关 系（entailment relation，缩写为CRD），它指定了约束之间的相互依赖关系：CRD表示信息d可以从由C表示的信息中推导出来。这样的系统可以形式化为斯科特信息系统，如[21]，或者它们可以建立在逻辑的适当片段上，例如，如[10，16]。在这里，我们将遵循第二种方法，约束被视为直觉逻辑中的公式定义2.1（约束系统）约束系统是一个元组（C，C），其中C是从一阶签名和以下语法F：= true|一|FF|B.F.其中A是原子式。 我们将用c，cJ，d，dJ等来表示C.此外，设Δ是一组非逻辑公理，其形式为λx。[c<$cJ]其中c和c j中的所有自由变量都在x中。 我们说d包含dJ，记为d<$dJ，i <$Δ，d −→ dJ在 L J 中 是可能的。2.1工艺流程ntcc演算[16]用时间单位扩展了ccp，用于指定反应系统，即，与周围环境持续互动的系统在这种语言中，时间在概念上被划分为离散的间隔（或时间单位）。直觉上，在特定的时间间隔内，进程P接收刺激（即，约束），它以该刺激作为初始存储来执行，并且当它到达其静止点时，它以结果存储来响应环境。静止点还确定剩余过程Q，其然后在下一个时间间隔中执行定义2.2（1）过程P，Q，. . . 从底层约束系统中的约束构建，如下所示：P，Q，. * =告诉（c）|当ci做Pi时，i∈I|PQ|局部x（P）|除非c下一个P|！|! P| * P不定时的进程。进程tell（c）将约束c添加到当前存储中，从而使c在当前时间间隔内可用于其他进程。让我成为一组有限的索引。当ci非确定地做Pi时的询问过程i∈I选择一个进程Pis. t。ci是当前存储所必需的选择的替代方案，如果有的话，排除其他的。如果在当前时间单位内没有可能的选择，则所有备选方案都被排除在执行之外。因此，Ask进程定义了一种基于约束蕴涵的强大同步机制为了便于阅读，我们将省略” wheni∈I164J. Arias等理论计算机科学电子笔记312（2015）161j∈JJJ我{FP（P1），.，P = 0，P =0，P=0（j∈J，当cjdoPj）=0且FP（nextQ）=FP（unlesscnextQ）=Q时。2001年4月，i∈ J（X;tell（c），Γ;d）−→（X;Γ;c<$d）RTELL（X;n当c做P，Γ;d）−→（X;P， Γ;d）RASKx∈/X<$fv（d）<$f v（Γ）R德鲁克河（X;localx（P），Γ;d）−→（X<${x};P， Γ;d）LOC（X;unlesscnextP， Γ;d）−→（X;Γ;d）UNL（X;！P; Γ;d）−→（X;P，下一个！P; r;d）Rn≥0RREP（X;*P， Γ;d）−→（X;nextnP， Γ;d）明星（X; Γ;c）<$（XJ; ΓJ;cJ）−→（YJ; ΔJ;dJ）<$（Y; Δ;d）（x; r;c）−→x（X; rJ;d）/−→RRSTR（c，200X.d）OBSJ（X; Γ;c）→（Y; Δ;d）Γ= |图1.一、 内部（−→）和观察到的可变（=−）跃迁。 令r={P1， . ，Pn}。F（r）的未来是d中的自由变量集（分别为P）表示为fv（d）（resp. fv（P））。过程P<$Q表示P和Q的平行合成。 局部过程x（P）的行为类似于P，除了由P产生的关于x的所有信息只能由P看到，即，x是P的局部变量。定时过程。下一个进程P将P的执行延迟一个时间单位。我们将使用nextnP作为next next··nextP的缩写，其中next重复n次。过程unlesscnextP也是一个单位延迟，但只有当保护c不能从当前存储中导出时，过程P才在下一个时间单元中执行。这就是所谓的否定询问或P的抢占。过程！P表示P的无限多个拷贝，但每个时间单位一个拷贝。这是，！P可以看作是PnextPnext2P···。 这个构造足够强大，可以在ntcc中编码某些形式的递归定义，如[16]所示。最后，过程*P表示P的激活的任意长但有限的延迟。 这个过程可以看作是P+下一个P+下一个2P +. . .2.2结构操作语义学ntcc的SOS由两种约化组成：表示时间单位内过程演化的内部跃迁（−→）和表示时间单位之间过程演化的可观测跃迁（= − →）内部跃迁关系γ−→γJ满足图1中的规则。在这里，我们遵循[10]中的公式，其中程序创建的局部变量显式地更精确地说，一个配置γ是一个形式为（X; Γ;c）的三元组，其中c是表示存储的约束，Γ是一个多过程集，X是c和Γ的一组隐变量。多重集合Γ ={P1，P2，.，Pn}表示过程P1<$P2<$. [医]神经性麻痹;我们将毫无疑问地使用这两种符号来表示过程的并行合成此外，过程是通过结构一致关系“满足”来引用的。证明：（STR_1）l_ocal_x（P）_v=l_ocal_y（P[y/x]），如果y∈f_v（P）（α-不变）;（STR2）P<$Q<$=Q<$P;（STR3）P<$（Q<$R）<$=（P<$Q）<$R。我们会写J. Arias等理论计算机科学电子笔记312（2015）161165Σ===（X;r;c）n（X J;rJ;cJ）当verX=X J，rj=rJ且c≠d（即， cd和dc）。图1中的规则直接实现了上面给出的操作直觉：告诉代理tell（c）将c添加到当前存储d（规则RTELL）;如果可以包含其对应的保护ci，则当ci执行Pi时，进程执行Pii∈I从存储器（规则R ASK）;当没有变量冲突发生时，本地进程localx（P）将x添加到隐藏变量X的集合（规则R）。注意，如果前提x∈/Xfv（d）fv（r）d不成立，则规则RSTR可以用于进行alpha转换;如果当前存储需要c，则除非cnextP中的进程P不被执行（规则RUNL）;进程nextP的看似缺失的规则由规则ROBS给出，如下所述;进程！P生成P的一个副本，然后在下一个时间单元再次执行（规则R REP）;对于给定的n≥0，进程 *P执行下一个nP（规则R STAR）。现在让我们来描述可观测跃迁的规则。规则ROBS说，从P标记为（c，<$X.d）的可观察跃迁是通过对某个ΓJ执行从（X; Γ;c）到（X; ΓJ;d）的内部跃迁的终止序列而获得的。在下一个时间间隔中要执行的过程对应于rJ（即，如图1所示。请注意，未来函数F没有为过程tell（c），localx（P），！P和*P，因为所有这些过程都有一个内部的过渡。此外，X中的变量通过使用存在量化隐藏，即，关于X的信息从最终存储器d中不可见。定义2.3（可观察行为）设P是一个过程，s = c1.c2.c3···是一个无限约束序列。我们说P在输入s下输出SJ= CJ1.CJ2.CJ3···，如果PP1（c1，c′1）=P2（c2，c′2）=第3（c3，c′3）=···我们记为P（s，s′）. 我们将P的输入-输出行为定义为io（P）={（s，sJ）|P（s，s′）=}。3NTCC过程的符号模型模型检验[6]（见[19]中的一项调查）是一种成熟的系统自动验证技术。在这一节中，我们将展示如何构造一个ntcc过程行为的符号模型，然后是紧凑模型。稍后，在第5节中，我们将使用此模型作为符号模型检查算法的输入。为ntcc程序开发自动验证技术的主要困难之一是，进程的语义由两个不同的转换系统给出，即内部（−→）和可观察（= − →）转换。一方面，建立一个内部过渡的模型似乎是不必要的因为在时间单元期间过程的内部运动从外部环境是不可观察此外，从内部转换中抽象出来应该会导致系统的更紧凑的表示，从而减少搜索空间。另一方面，当考虑非确定性过程时，内部过渡决定了许多可观察的行为（例如，规则166J. Arias等理论计算机科学电子笔记312（2015）16112n112n212nmRASK和RSTAR）。然后，我们的方法是使用（时间）公式作为可达状态的紧凑表示（即，存储）的过程。正如我们将看到的，所提出的公式捕捉到了可观察到的贡献（即，约束）;此外，内部（不可观察的）转换被逻辑连接符符号化地捕获。更准确地说，我们将遵循以下步骤：- 步骤1：给出P的逻辑解释（定义3.2）。有趣的情况将是时态运算符！和*，需要定点字符化。- 步骤2：执行定点计算，找到一个公式，该公式象征性地模拟P的可达状态。- 步骤3：处理死胡同，即，没有任何过渡的国家。3.1步骤1：流程的逻辑解释我们首先介绍一些必要的符号。一个过程的行为将被指定为以下形状的公式的析取：0（c0）其中每个ci都是一个约束（定义2.1）。直观地说，上面的公式读作在线性时间逻辑中，“零”系统对应于下一个时刻[14]如下文所述。为了可读性起见，我们写c而不是c++0（c），◦（c）而非1991年（c）。更重要的是，我们认为1 1 2 2 2 m mm{{F1，F2，···，Fn1}，{F1，F2，···，Fn2}，···，{F1，F2，···，Fnm}}而不是下面的析取范式公式（F1<$F1<$··<$F1）<$（F2<$F2<$··<$F2）<$··<$（Fm<$Fm <$··<$Fm）（2）定义3.1（状态）我们将使用C来表示从约束集C和LTL运算符（next）构建的公式集。 一个状态是C个公式的合取，其形状为c1<$··<$cm。两个状态A和B是等价的，如果A<$B和B<$A。 F=A0（A1）n（An）的C_∞公式表示一个标号迁移系统（LTS），其中存在从状态sx到状态sy的迁移，记为sx~sy，如果Ai（分别为. Ai+1）在sx（resp. sy）。 我们将使用L（F）来表示这样的LTS。给定一个LTS L，我们将使用state（L）（resp. transs（L））来表示状态集合（分别为过 渡 ）。现在我们准备好用C++公式来给过程赋予逻辑意义了。定义3.2（符号表示）给定一个ntcc过程P，让S（P）如图2所示被归纳定义，其中μ（resp. v）表示最小（resp. 最大）定点算子，其中L1≤L2i =态（L1）n =态（L2）且transs（L1）n = transs（L2）。J. Arias等理论计算机科学电子笔记312（2015）161167ΣS（tell（c））=cS（当ci做Pi时，i∈I）=（<$ci）（ciS（Pi））i∈I i∈IS（P）= S（P）<$S（Q）S（local x（P））=<$x。（S（P））S（nextP）=（S（P））S（unlesscnextP）=（<$c（S（P）cS（*P）= μY。（S（P）（Y））S（！ P）= νY。（S（P）（Y））图二. NTCC过程的符号表示（定义3.2）。-c表示不存在c。让我们对前面的定义作一些直观的说明。一个过程tell（c）定义了一个c持有s的状态一个过程i∈I当ci做Pi时生成一个状态，其中没有一个警卫持有（（<$ci））和其中ci和S（Pi）成立的状态。的过程i∈IP≠Q定义了S（P）和S（Q）都成立的状态局部进程localx（P）生成一个状态，其中P成立，但关于x的信息无关紧要。一个进程，除非c下一个P，定义了一个c成立的状态（然后P不被执行）和一个c不存在的状态（即，c）和由P生成的状态保持如[16]所示，过程*P类似于LTL中的最终模态（Q）。然后，由这个过程产生的状态可以被表征为P成立的状态和P在下一个时间单位中成立的状态的析取的最小定点。同样，过程！P类似于LTL中的always（Q）模态。然后，生成的状态对应于满足P的状态和P也成立的未来状态的3.2第2步：定点计算一旦我们有了给定过程P的逻辑读数S（P），我们需要执行定点计算，以获得象征性地表示系统状态的C_∞公式。在给出这个步骤的一些例子之前，我们需要定义公式的阶（下面的符号3.3）和一个简单的程序转换，以便正确地捕获状态转换。考虑过程P=next tell（c）。 我们知道S（P）= S（c）。 那么，在第一个时间单位内，P的可观察行为应该是什么？我们知道P不给第一个时间单位增加任何信息。然后，我们需要“完成”公式f（c）来模拟P产生两个状态的事实：s 1，其中没有信息可以推导出来，以及s 2，其中c保持使得s 1 ~ s 2。我们将把这种情况象征性地表示为公式真的λ（c）。记法3.3（Empty状态和Degrees）LetF=0（c0）1（c1）···◦n（cn），我们说F的次数，记为度（F），是n。我们假设对于每一个i∈0. n在F中，则x是sci，使得mi（ci）oc在F中curs;在这种情况下，我们假设ci= true。为了可读性，我们将省略真const raint， 并且我们 将写为， 例如 ， 2 （ c）insteadoftrue2（c）。现在我们介绍一个简单的程序转换，它需要在定点计算期间正确捕获状态转换让我们解释一下168J. Arias等理论计算机科学电子笔记312（2015）161ΣΣ（2）A = B =Aj∈JwhencjdoPj，n）=j∈Jwhencj≠ndoP（Pj，n）P（PQ，n）=P（P，n）<$P（Q，n）P（localx（P），n）=localx（P（P，n））P（nextP，n）=nextP（P，n+1）P（unlesscnextP，n）=unlesscstnnextP（P，n+1）P（*P，n）=*P（P，n）P（！P，n）=！P（P，n）图三. 标签（见定义3.4）。用一个简单的例子来说明这种变换。 假设过程P和Q如下：P=tell（c）next tell（c）Q=！告诉（c）我们知道S（P）=c（c）。此外，c（c）也是方程S（Q）的解。在第一种情况下，我们想表示LTS，其中有两个不同的状态s1和s2，s1到s2（s1~s2），c在两个状态中都成立。 在第二种情况下，我们希望用单个状态s3表示LTS，其中c成立，并且在s3中有一个循环（s3~s3）。因此，我们如何区分公式S（P）和S（Q）的解？我们的想法是标记约束，以指定上面的s1和s2是不同的，并且它们之间存在时间依赖性（转换）。例如，在S（P）的情况下，我们将给出一个形状为c1（c2）的公式，以区分c在P中的两次出现。标记过程是一个简单的程序转换，如下面的定义所示定义3.4（标记）不失一般性，我们假设对于每个i∈N，sti是约束系统中的一个独特的原子约束。给定一个过程P，我们归纳地定义P（P，n），如图3所示。为了简化记法，我们将cn而不是cstn。此外，我们将c写成c，而不是c0。标记过程还需要产生形状真0的公式。◦（true1）2（c2）而不是true（true）2（c），当公式true（true）被添加到2（c）时，如符号3.3中所解释的。例如，这避免了在计算形状next nexttell（c）的过程的模型时不需要的循环true ~ true。现在我们准备好展示定点过程。其思想是计算满足方程S（P（P，0））的LTS。回想一下，每个状态都满足true，而约束false只在不一致的存储中有效。因此，作为标准，计算方程μY的解。（F）（Y）（resp.是的。（F（Y））以Y0= false（resp. Y0= true）。下面的示例为流程查找符号模型！*tell（c）需要最小和最大定点计算。例3.5设P=！*告诉（c）。我们首先计算S（*tell（c））= μX。（S（tell（c））π π（X）），如图4a所示。请注意，X3和X4都代表同一图中的跃迁系统。 那么X3是定点，我们可以用 它来计算“的意思！“，即，是的。（X3X（Y）），如图4b所示。Y2是方程S（P）的解，它代表图4b 中的LTS。读者可能想知道，在存在复制的（！P）过程。下面的定理J. Arias等理论计算机科学电子笔记312（2015）161169SX0=假X1=c（false）cX2={{c}，{（c）}}X3={{c}，{（c）}，{2（c）}}X4={{c}，{（c）}，{2（c）}，{3（c）}}(a) 符号模型的基本原理（c）。 X0= false，因为我们正在计算μX的解。（（tell（c））（X））（最小定点）。Y0=trueY1={{c}，{（c）}，{2（c）}，{（true）}}Y2={{c，n（c）}，{c，n2（c）}，{c，n3（c）}，{n（c）}，{n（c），n2（c）}，{（c），3（c）}，2（c）}，2（c），3（c）}}(b) 象征性的模型！ （c）.图四、示例3.5的标签转换系统。肯定地回答了这个问题。定理3.6设P是一个过程，S（P）= F（X1，…，Xn）是一个公式，其中变量X1，...，Xn出现在F中，前面有μ或ν。 F的定点可以通过有限步数达到。证据这个证明是从以下两点得到的直接推论：（1）[22，定理4.12]表明P的输出可以用C的有限子集（不一定是有限的）来表征;（2）[22，引理4.13]表明P可能生成的不同状态的数量也是有限的。因此，由于可能的可达状态的数量是LTSL（S（P））是有限的，定点计算必须终止。Q3.3死胡同在前一步骤中的定点计算之后，可能的情况是，所得到的LTS具有死端，即，状态没有传出转换。当进程P不是一个复制的（“！”）过程作为示例，考虑过程P=tell（c），其结果LTS具有唯一状态c而没有转换。我们还记得，在ntcc的过程应该不断地与环境的反应。然后，在tell（c）的情况下，该过程在第一个时间单位中输出c，在随后的时间单位中输出true。 请注意，此行为根据定义2.3中的操作语义：过程的输出总是约束的有限序列。因此，给定一个表示具有死端的LTS的n次C_∞公式F，C真C真170J. Arias等理论计算机科学电子笔记312（2015）161Y0=trueY1={{signal，n（on1）}，{<$（signal），n（off1）}}Y2={{信号，（开1），（信号），2（开1）}，{信号，（开1），（信号），2（关1）}，2 2{<$signal，（off1），（signal1），（on1）}，{<$signal，（off1），（<$signal），（off1）}}Y3={{信号，（信号），（1），2（1），2（信号），3（1）}，2 2 3{信号，（信号），（开1），（开1），（信号），（关1）}，2 2 3{信号，（信号），（开1），（关1），（信号），（开1）}，2 2 3{signal，（<$signal），（on1），（off1），（<$signal），（off1）}2 2 3{<$signal，（信号），（关1），（开1），（信号），（开1）}，2 2 3{<$signal，（signal），（off1），（on1），（<$signal），（off1）}，2 2 3{<$signal，（<$signal），（off1），（off1），（signal），（on1）}，2 2 3{<$signal，（<$signal），（off1），（off1），（<$signal），（off1）}}图五、例3.7中的过渡系统。状态，我们将把状态n+1（truen+1）n+2（truen+1）（结合）加到F上。因此，F的死端有一个到循环状态的转换，在循环状态下只能推导出真。例3.7（控制系统）假设一个简单的控制系统，当环境在当前时间单位报告一个给定的信号时，它必须在下一个时间单位发射信号。否则，它必须在下一个时间单元中发射信号。这可以被建模为P=！（当信号做下一个告诉（开）时，除非信号下一个告诉（关））P的符号模型由公式S（P（P，0））得出：是的。（signal（on1）<$（signal））（<$（signal）（off1）signal））（Y））定点计算得出图5中的结果。例3.8（异步行为）现在考虑一个控制系统，一旦检测到错误，它必须发出停止信号。此外，我们知道系统注定会失败（由于下面的过程 *tell（error））：P =*tell（error）！当错误做！停止（Stop）请注意，一旦检测到错误信号，ask进程就会执行该进程！tell（stop），然后，可以从该时间间隔推断出约束停止。* tell（error）的符号模型由以下公式给出：F1=error（error）2（error）其确定类似于图4a的LTS。过程的象征性模型！tell（停止）是停止状态（停止），它确定LTS，使得停止保持的状态总是被另一个状态所跟随 状 态 也停止。P的符号模型及其相应的LTS如图6所示。信号信号灯1信号信号关闭1信号关闭1月1日J. Arias等理论计算机科学电子笔记312（2015）161171222L⇒OQY2={{error，stop，（stop），（error），2（stop），2（error）}，2 2{error，stop，（stop），（error），（stop），（<$（error））}，2 2{error，stop，（stop），（<$（error）），（stop），（error）}，2 2{error，stop，（stop），（<$（error）），（stop），（<$（error））}，2 2{（error），（stop），（error），（stop），（error）}，2 2{<$（错误），<$（停止），<$（错误），<$（停止），<$（<$（错误））}，{<$（error），<$（<$（error）），<$（stop），<$（error）}，{<$（error），（<$（error）），（<$（error））}}图第六章示例3.8中的符号模型和LTS。我们通过证明我们的符号构造是正确的来结束这一节。回想一下，ci表示c不存在，<$c表示c不存在。由于这些约束是在模型构造过程中引入的（并且它们不构成原始过程的一部分），因此正确性结果可以安全地忽略这些约束。还记得所得到的LTS没有死端，即，其中的路径是状态的有限序列定理3.9（正确性）设P是一个过程，F是方程S（P（P，0））的解，L是定义3.1中的LTSL（F）。考虑一个无限约束序列π。则π是L i中的一条路，且存在一个序列πi= c1.c2.c3. ···使得（πi，πo）∈io（P），其中πo类似于π，但没有任何形状sti和<$c的约束。证据证明过程是通过对P的结构的归纳来进行的。对于该部分，假设π是LTS（F）中的一条路。 我们将证明相应的πo确实是P的输出（对于给定的输入πi）。有趣的例子是时间结构：- P=下一个Q。很容易看出，πJ，定义为没有第一个元素的π，是LTSL（S（Q））的通过归纳，存在一个πJo，它是Q. 因此，很容易看出π确实是P的输出。- P=除非c下一个Q。如果π（1）（π的第一个元素）是c成立的状态，证明是平凡的。如果c在π（1）中不成立，那么我们继续下一种情况。- P=！Q.我们知道F是方程G（X）=S（Q）X的解。 此外，通过归纳，我们知道LTSLq =L（S（Q））中的任何路径πq对应于Q的输出πo。因此，在Lq（以及L（F））中的初始状态之一中开始的任何路径对应于Q的输出。此外，由于F是G（X）的解，因此π的任何子集x也对应于Q的输出。由于π的所有子集（包括π本身）都在Q的输出中，我们得出πo是P的输出。- P=* Q。 注意F是G（X）=S（Q）X的解。 如果我们只考虑LTS中的公平路径（即，π不是一个无穷序列，其中Q状态从未被访问过），则存在π的一个子集xπJ，使得πJo对应于Q. 通过归纳，我们可以得出结论，πo对应于P的输出。证明的第二面是类似的。Q误差错误停止<$错误停止172J. Arias等理论计算机科学电子笔记312（2015）161正如我们将在第5节中看到的，证明情况*Q所需的公平条件J. Arias等理论计算机科学电子笔记312（2015）161173βi|=tr·ueβ，i|=fal·seβi|=ciβ（i）|=cβ，i|=·Fiβi|=Fβi|=Fiβ，i+1|=Fβ，i|=QFij≥iβ，j|=Fβi| = QF i j ≥is.t. β，j| = Fβi|=F1·F2iβi|=F1和β，i|=F2βi|=F1·F2iβi|=F1或β，i|=F2见图7。 CLTL公式的语义。通过考虑公平性约束的模型检查算法来保证。4属性的语言约束时序逻辑（CLTL）。由于ntcc过程操纵约束，因此认为系统属性必须以能够处理约束的逻辑来陈述是合理的。因此，我们将使用CLTL [16]，一种线性时间时间逻辑[14]，其中原子公式是约束。命题CLTL中的公式是从下面的语法构建的F：：= tr·ue|发勒瑟|C|F·F|F·F|·F|F|QF|QF其中C是约束。tr·ue、fl·se、tr·、tr·和tr·代表线性时间点。逻辑真、假、合取、析取和否定。这些符号不应与约束系统中的对应符号混淆（即，真，假，假）。符号Q、Q和Q表示LTL时间运算符next、always和finally。CLTL中公式的解释结构是约束的有限序列（如定义2.3中的可观察行为）。我们说，约束的无限序列β是公式F的模型（或它满足公式F），符号β| = F，如果β，1|= F.β的含义，i| = F在图7中给出。虽然CLTL的语义是由约束序列给出的，但LTL公式的模型是状态序列（将值分配给变量的映射）。CLTL和标准LTL [14]中的满意度之间的关系建立在[22 ， Lemma5.4] ： Afor mulaFisLTLsatisfiableiF·Q·falseisC LTLsatisfiable. 直 观地，公式false（表示不一致存储的约束）具有至少一个模型（例如，约束序列为false。假的）而fal·sed o不具有y模型（β，i）|=fal·se）。然后，“Q-false“部分去除包含（约束）false的CLTL模型。当否定具有原子作用域时，这个结果成立，即，G必须是原子（即，约束）在所有公式的形状。 在[22]中，这是一个已知的限制方程条件。174J. Arias等理论计算机科学电子笔记312（2015）161图八、 DDD结构的示例。图像和示例摘自[15]。4.1约束的表示在ntcc演算中建模的许多系统利用数值约束（参见例如，[17]）。因此，我们使用Difference Decision Diagrams （ DDD ） [15] ， 这 是 Binary Decision Diagrams（BDD）[4]的适当扩展，用于表示从以下语法构建的Difference约束表达式φ：：=假|真正|x − y

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