基于环境演算的CTL*逻辑安全属性分析模型：环境演算和时态逻辑的模型检测

理论计算机科学电子札记99（2004）3-29www.elsevier.com/locate/entcs基于环境演算Radu Mardare1和Corrado Priami2意大利特伦托大学信息与通信学院摘要2在本文中，我们主张使用CTL* 逻辑，建立在环境演算分析安全属性。我们的逻辑是一个更具表现力的替代环境逻辑，基于一个单一的模态，但仍然足够强大，以处理移动性和动态层次的位置。此外，有一个时间逻辑来表示计算的属性，我们可以重用的算法，模型检查时间逻辑分析模型的安全问题。我们借助Ambient演算的语法树，并在语法树中增加一些标记函数，从而得到我们称之为标记语法树。标记的语法树将被用来作为可能的世界中的Kripke结构开发的命题分支时序逻辑。可达性关系是由环境演算的约简生成的，该约简被认为是语法树之间的约简。给出了计算状态间可达性关系的算法，并将其与时态逻辑的模型检测算法结合起来，开拓了环境演算模型检测的b由IST-FET项目DEGAS和MIUR-COFIN 01项目MEFISTO部分支助的工作。关键词：环境演算，时态逻辑，集合论，模型检测。1介绍Ambient Calculus [5]是构建安全问题数学模型的有用工具，因为它在表达位置及其移动性的层次结构方面很方便基于Ambient Calculus，1电子邮件地址：mardare@dit.unitn.it2电子邮件：priami@dit.unitn.it1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.0014R.马代尔角Priami /理论计算机科学电子笔记99（2004）3-29=环境逻辑[4，3]，一种可以描述移动计算属性以及位置层次结构和时间层次结构的修改的逻辑。环境逻辑的主要思想是将过程视为时空实体，因此使用了两种类型的模态-一种用于关于空间的断言，另一种用于关于时间的断言。我们将在这里证明，一个单一的模态表面描述这些实体的行为。主要的直觉是，我们只需要计算系统的每个运动对初始状态的修改，因为这些信息只需要使用基于环境演算的命题分支时间逻辑就可以重建系统的实际形状使用时态逻辑的优点与安全问题有关。考虑一个完全保密的防火墙和一个打算通过预先安排的密码k，kJ，kJJ穿越防火墙的代理之间的交互模型[5]。def防火墙在n.in，在，在。0个字符]|开kJ.开kJJ.P]=（代理defkJ[open k.kJJ[Q]]剂|防火墙（νn）（kJ [open k.kJJ [Q]]|在n.in......中，在......中。0个字符] |openkJ.open kJJ.P]）→（νn）（kJ [open k.kJJ [Q]]|在n.中，在N.中，在n.中，在n.中0个字符]|n [open kJ.open kJJ.P]）→（νn）（kJ [open k.kJJ [Q] |k [in n.] 0]] |n [open kJ.open kJJ.P]）→n（v n）（kJ [kJJ [Q]）|在n. 0个字符] |n [open kJ.open kJJ.P]）→（νn）（n [kJ [kJJ [Q]] |open kJ.open kJJ.P]）→n（v n）（n [kJJ [Q]）|打开kJJ.P]）→n（νn）n [Q|P]的范围这种计算正确地描述了所需的相互作用。我们的验证是可能的，因为公式不是太大，计算是在几个步骤中进行的，并且只有一条还原路径是可能的。在一个更复杂的情况下，其中计算路径有分支，即存在可能不止一个约简的时刻，每个可能性意味着不同的可能未来，当涉及可能完全或部分知道密码的其他代理时，我们想要检查这种情况是否总是可达的，或者如果不是，这是例外情况下系统的配置我们无法在Ambient Calculus中获得这些问题的答案。只有能够预测计算的逻辑才能给我们答案。环境逻辑可以表达这样一种可能性：R.马代尔角Priami /理论计算机科学电子笔记99（2004）3-295这个系统将出现在一个可能的未来中，用公式表示，但它不能说这个时刻是下一个时刻，还是非常遥远的未来时刻，因为它不能说这个未来是否在任何可能的时间路径中找到。在我们的例子中，我们有兴趣表达，对于所有可能的未来路径，在未来的某个时候，我们将有过程P和Q之间的相互作用。这是不可能使用环境逻辑。我们只能说，在未来的某个时候，这种交流确实是可能的，但这并不排除存在一条时间路径的可能性，在这条路径上，这种相互作用根本不可能。在其他情况下，知道一个属性在下一刻是否为真也很重要，或者，在我们希望在识别密码之前不可能进行通信的情况下，一个属性为假，直到另一个属性变为真。所有这些属性都可以用时态逻辑来表达。使用时态逻辑来建模环境演算的另一个论点是，可以重用一些已经为这些逻辑开发的软件，如SMV，NuSMV，SiMpLer，VIS，对我们的演算进行模型检查。此外，我们将丰富的语法树的环境过程的装饰功能，帮助我们解释它们作为状态的时态逻辑。装饰函数的动作将根据其性质对语法树的节点进行分组，并将与每个节点关联一些标识，这些标识将描述环境过程的分层结构2标记语法树在本节中，我们从语法树开始定义环境演算过程的标记语法树。这个概念对于进一步的构造是至关重要的，因为标记语法树的一些抽象将是我们将要构造的逻辑中的状态我们首先只考虑没有新名称操作符的进程（在下一节中处理）。一 个 进 程 的 语 法 树 S= （ S ， →S ） 是 一 个 具 有 S=P<$C<$O=（PP<$PA）<$C<$O的图，其中P是包含所有未指定的进程节点（以下称为原子进程4，并收集在子集PP中）和周围节点（收集的3 时间的可能性（Temporal Possibility）4我们用这些来表示在环境进程中发现的未指定进程;这是为环境演算开发模型检查的必要要求，因为我们必须随着时间的推移识别和区分目标进程中的未指定进程例如，P是n[in m.P]中的未指定过程。6R.马代尔角Priami /理论计算机科学电子笔记99（2004）3-29在子集PA中）;C是能力节点的集合（我们在这里包括输入节点和能力上的变量的节点）;以及O是语法运算符节点的集合（此集合包含并行运算符|和前缀运算符（·）。 我们确定子集OJ={·1∈O|·1→S|在语法树中，parallel运算符紧跟在前缀节点之后，因为它们在环境进程的空间结构中起着重要的作用。构造标记语法树背后的直觉是通过两个函数将一些标记与语法树的每个节点相关联：id，其给予每个节点标识，以及sp，其注册节点的空间位置。identity函数id关联一个标签（urelement或curl）：(i) 每个未指定的进程和每个环境;这个标签将识别节点，并帮助我们进一步区分具有相同名称(ii) 对于每种能力，该能力所处(iii) 每个语法节点空间函数sp关联：(i) 对于每个环境，将其子进程6的标识集合与之相关联，而对于未指定的进程，将ID标签与之相关联。(ii) 对于每个能力，一个自然数，用于计算该能力在属于同一过程的能力链（如果有的话）(iii) 空间函数将0关联到每个语法节点，除了OJ中的节点之外，函数sp将关联到由该点所预处理的复合过程中的主并行运算符所连接的过程的恒等式集合例如，在C的情况下。（P|，sp（·）={id（P），id（Q）}。我们在这里回顾一下集合论和图论的一些基本定义，这些定义是正式定义上面的函数id和sp所需要的。我们选择在集合论ZFC的Zermelo-Fraenkel系统中工作，5这些点运算符是将能力与由由括号连接在一起的其他过程的平行组合，下文称为复杂过程，如c。（P |Q）6.我们使用父进程和子进程这两个术语来描述进程，这意味着环境演算进程中的直接父进程和直接子进程。R.马代尔角Priami /理论计算机科学电子笔记99（2004）3-297VS基础公理（FA），作为一个肥沃的领域，提供了许多分析结构的工具，如[2]所述。这种方法使我们能够描述的空间结构的环境过程的方程在集合论，每个这样的方程被用来作为原子命题在我们的逻辑。 这样，我们就不会使用模态来描述位置的层次结构，而只是描述等级制度的演变在下文中，我们假设一类V元，集合论实体不是集合（它们没有元素），但可以是集合的元素。这些元素和空集一起将生成我们将要处理的所有集合（有时是集合的集合）。定义2.1一个集合a是传递的，如果集合b的所有元素，也是a 的元素，也属于a：如果c∈b，则c∈ a。a的传递闭包，记为TC（a），是包含a的最小传递集。 TC（a）的存在可以证明如下：TC（a）={a，a，a，... }定义2.2一个集合a的支集，记为supp（a）是TC（a）V。supp（a）的元素是以某种方式参与a的元素。def定义2.3如果则V（a）={b|b是一个集合，supp（b）<$a}。五（a）是所有集合的类，其中以某种方式涉及的唯一的元是a的元。定义2.4设SP=（Si→S）是与周围过程P相关联的语法树。我们称与P相关联的结构图为通过将语法树的边关系限制为P = OJ而获得的图，即，图TP=（P<$OJ，→T）定义为：对于n，m∈P<$OJ，我们有n→Tmi <$n→Tm和$p∈P<$OJ，使得n→βp →βmS S直观地说，一个进程的结构图是通过将其语法树的边关系限制到P来得到的。定义2.5图G=（G，→G）的装饰是内射函数e：G→V（V）<$V使得对于所有a∈G，我们有：• 若$b∈G使得a→Gb则e（a）∈V• 如果n∈G使得a→Gb，则e（a）={e（b）|对于所有的b，使得a→Gb}。现在我们引入一组辅助函数，它们是id和sp的构建块（关于这些和以下定义的应用，请参见附录）。定义2.6让下一个函数定义在 语法树（S，→）如下：8R.马代尔角Priami /理论计算机科学电子笔记99（2004）3-29VOCc• 设spP：P<$OJ→ V（V）<$V是与我们的语法树相关联的 结 构 图 的装 饰 。• 设idP：P→V是一个内射函数，使得对所有的P ∈ P考虑UPdef=idP（PP）N ，UAdef=idP（PA）• 设spO：O→V<$V（V）<$N，定义为：P（s）i∈OJspO（s）=0Jdef考虑O=spO（OJ）V（V）0i∈O\O• 令idO：O→V（V）V定义为：idO（s）=0• 设spC：C→N，使得1i| → · →c或n→ · →c，其中n∈ PspC（c）=k+1i →·1→ ·2→c和·1→cJ∈C，其中spC（cJ）=k• 设idC：C→V（V）≠V，定义为c∈C，使得·c→c，拟群P（n）i <$·c→n，其中n∈PidC（c）=idC（cJ）i·c→·J，其中·J→cJsp(·)iff·∈OJ总而言之，我们可以定义恒等函数id：P<$C<$O→V <$V（V）和空间函数sp：P<$C<$O→V<$V（V）<$N：P（s）is∈Pid（s）= idC（s）is∈CP（s）i∈Psp（s）= spC（s）is∈Cid（s）is∈OOi∈O O注意，id的范围是V<$V（V），sp的范围是V <$V（V）。 V（V）<$N（我们在这里把自然数看作基数7，这样只要N<$V<$V（V）就不会出现结构异常）。在下文中，为了演示的缘故，我们仍然会考虑自然数，而不是基数。7 非正式地说，我们把0当作，把1当作{}，把2当作{，{}}，把3当作{，{}，{，{}}，以此类推。VR.马代尔角Priami /理论计算机科学电子笔记99（2004）3-299我们确定的uelements选择的环境，uP的uelements选择的原子过程，和uelements的集合O的集合，包含所有的地址的元素在OJ。我们现在为环境进程的给定语法树定义标记语法树定义2.7设SP=（S，→）是环境进程P的语法树。我们将其标记的语法树称为三元组S1P=（S，→，φ），其中φ是在语法树的节点上定义的函数，φ（s）= φid（s），sp（s）对所有的s∈ S都是φ。注2.8函数id在上述定义中的中心位置是显而易见的。 对于一个特定的环境进程，一旦我们定义了函数id，所有的构造，直到标记的语法树，都可以在环境进程的结构上归纳完成。正因为如此，我们的标记语法树的构造是唯一的，直到元素的选择（即，P和UA）。定义2.9对于给定的标记语法树Sl=（S，→，φ），我们定义函数：• ur：POJ→UPUAOby：如果s∈P，则为n（s）ur（s）=0 sp（s）如果s∈OJ该函数将结构图的每个节点与由标记语法树定义的集合理论恒等式相关联• 设e：UP<$UA<$O→V<$V（V）为函数，定义为：e（v）=sp（ur−1（v））它将每个环境进程和复合进程关联到 它的孩子。• f：UP<$UA<$O→ Λ <$A，其中Λ是环境演算的环境名的集合，而Λ是原子过程的集合。 对于每个ν∈UP<$UA<$V，f（ν）是与ν通过id 8相关联的过程的名称，并且f（ν）=<$0，0 <$如果ν∈O。通过函数f，用作标识的每个ureElement（或ureElement集合）将接收环境或环境的名称。[8]我们可以非正式地说，在UA<$UP上，我们有f=id−1，但这并不精确，因为id是单射函数，而f不是。因为如果我们有两个名为P的进程，那么对于这两个进程，f的值都是P，但是，id-1，它们指向语法树中的不同节点。10R.马代尔角Priami /理论计算机科学电子笔记99（2004）3-29它所指向的原子进程（集合的名称为“0”，0“0”）。• F：UP<$UA<$O → C<$，对每个ν ∈ UP<$UA<$O，F（ν）=<$c1，c2，.其中ci∈C使得<$i∈N，id（ ci）= ν，sp（ ci）= i和$ck+1∈C使得id（ck+1）= ν和sp（ck+1）= k +1。在这种情况下，对于ν，我们不能找到任何这样的ci，我们定义F（ν）= ε，ε，. ε，ε是空能力。我们采用能力链上的等式关系的以下丰富化=C第九条规则：·C1，C2，C3，... cn− c1 = Cc2，c3，. cn·ε，c1，.， ck = Cc1，c2，...， ck，εk = C<$c1，.， Ct，ε，Ct+1，. ck = Cc1，c2，...， ckk，·ε，ε，..εε = Cε。函数F将它们所指向的进程前面的能力列表与这些能力中的每一个相定义2.10令S =（S，→，φ）是环境过程P的标记语法树。 我们将与P相关联的规范标记语法树称为标记语法树，由S+=（S+，→+，φ+）表示，标记语法树的限制为集合S+={n|n∈S，f（n）= 0且F（n）过程，ε是空能力。你...ε}，其中0为空此外，我们将只讨论规范标记树（通过扩展规范过程），这些树是在环境计算期间进化的树，对我们的目的来说真正重要的树也是如此3处理绑定运算符考 虑防 火墙 和代 理 之间 的相 互作 用 ，以 及 其他 两个 过程 n[R]和openn.t[S]：kJ [打开k.kJJ [Q]]|（v n）n [k][out n.in k]在n.中。0个字符]|开kJ.开kJJ.P] |n [R]|open n.t [S]这里，（νn）表示在（νn）作用域内的名字n与程序中所有其他名字不同。在这个例子中，我们希望确保out n和in n（它们是进程0之前的能力）永远不会发生作用。[1]但只有在环境中被选择为命名防火墙。反之亦然，open n，即t的能力，永远不会作用于防火墙环境，而只会作用于n[R]。直觉是，选择命名防火墙的环境名称应该是以前未使用过的名称。一个可能的解决方案可以是选择一个新的名字r∈Λ，并在（νn）的作用域中用它来替换所有出现的n这个解决方案在本地是好的，但它不会阻止名称r9这些规则是允许的语法环境演算连同规则R.马代尔角Priami /理论计算机科学电子笔记99（2004）3-2911==可以用于其他的过程，我们可以将其与我们的过程结合起来，就会出现姓名冲突。换句话说，重命名的解决方案不是一个组合的解决方案。我们通过一个类似于de Bruijn索引的技巧来保证复合性：我们接受自然数的有序对作为环境的可能名称，并使用它们来完全删除过程中的任何（νn）出现。因此，我们将一个过程中的第k个新名字（νn）替换为对k，1<$10。这种方法允许我们将我们的过程与我们已经构建了标记语法树的其他过程相结合。这样，第二个进程中的所有名称将接收名称为k，2，这意味着这是第二个进程的第k个新名称，依此类推，第l个进程的第k个新名称将接收名称k，l。这种构造是由这样的假设支持的，即在环境进程内部只能出现有限数量的新名称运算符，并且我们将只组合有限数量的进程。根据上述内容，我们的示例变为：kJ [打开k.kJJ [Q]] |1，1 0个字符]|开kJ.开kJJ.P]|开放的;开放的|open n.t [S]对我们的过程的约简的分析表明，在不使用新的名字运算符的情况下，预期的结果仍然是可能的。事实上：Firewalldef 1，1[k[out 1，1.in kJ.in 1，1. 0个字符]|开kJ.开kJJ.P]代理defkJ[open k.kJJ[Q]]剂|防火墙|n [R]|开放的;开放的kJ [打开k.kJJ [Q]] |1，1 0个字符]|开kJ.开kJJ.P] |n [R]|开放的;开放的→kJ [open k.kJJ [Q] |k [in 1，1]。0]] |1，1|n [R]|开放的;开放的→kJ [kJJ [Q]|在1991年，0个字符] |1，1|n [R]|开放的;开放的→1，1 [kJ [kJJ [Q]]|开kJ.开kJJ.P] |n [R]|开放的;开放的→100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000P]的范围n[R]开放的;开放的|||→100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000P]的范围R t [S]|||我们把它作为任何其他环境名称来处理，无论它何时出现在我们的进程中。这意味着集合Λ包含作为子集的N×N的子集。N. 这种修改并没有改变结构一致性的四个规则（（结构Res Res），（结构Res Par），（结构Res Amb）和（结构零Res），见[5]）。只有它修改了（νn）的意向性解释。这并不意味着这个名字在我们的12R.马代尔角Priami /理论计算机科学电子笔记99（2004）3-29quantifier范围内是新的，而是用一对未使用的10我们将在环境演算过程中，将所有出现在（νn）范围内的n，作为环境或能力，替换为R.马代尔角Priami /理论计算机科学电子笔记99（2004）3-2913自然数。这样，我们减少了所有的语法树的环境演算语法树没有新的名称操作符。4标号树的组成分析在本节中，我们定义了一个标记语法树代数，将Ambient Calculus的合成操作从语法树扩展到标记语法树。这意味着，从P1和P2的标记语法树开始，我们将定义P1的标记语法树。|P2，C1，C2cn.m [P] or！P.这样的构造可以简化为函数id的构造对于每种情况11.4.1并联组成假设（S1，→1，φ1）和（S2，→2，φ2）是进程P1和P2的标记语法树。根据注释2.8，我们可以假设为两棵标记树选择的元素集合是不相交的（如果不是这样，我们可以为P1选择其他元素，因为标记树在元素的选择上是唯一的）。我们可以为P1构造语法树|P2使用环境演算的规则.我们所要做的就是进一步定义新语法树的函数φ。假设α1，α2∈V是两种情况下主环境的恒等式（即，（S1，→1，φ1）是u1[P1]的树，（S2，→2，φ2）是u2[P2]的树考虑α∈V是一个新的元素（在两个标记树中未使用）。现在我们定义函数id为u [P1|P2]由：id（u）=α，id（n）=id1（n）对于每个n∈P1\ {α1}，id在α1中没有定义，id（n）=id2（n）对于每个n∈P2\ {α2}，id在α2当然，从用并行算子合成两个过程的方式来看，我们有eα=eα1<$eα2。4.2环境成分假设P1的标记语法树是（S1，→1，φ1）。我们想构造c1，c2.. ck.m [P1].考虑P1的标记语法树具有u1作为其主环境，环境具有单位元α1。 设α，β∈V是标号语法树中未使用的两个元素的P1。 让u成为c1 的主环境。c2。。ck.m[P1]. 我们可以定义，在11见备注2.814R.马代尔角Priami /理论计算机科学电子笔记99（2004）3-29标准方式，u [c1.c2.的语法树。ck.m [P1]]使用环境演算的规则。此外，我们定义它的id：id（u）=α，id（m）=β，id（n）=id1（n）对于所有n∈P1\ {u}，id在u当然，根据环境成分的定义，我们有eα={eβ}，eβ=eu。4.3标号树如果我们通过LST调用所有标记语法树的类（关于直到元素选择的恒等式），那么前面定义的两个操作可以被引入为：LST：LST×LST→LST，用于平行合成，以及C1，C2... ck.m @：LST→LST（对于环境组成）如果（S1，→1，φ1）和（S2，→2，φ2）分别是进程P1和P2的标记语法树，则P1的标记语法树|以前构造的P2是（S1，→1，φ1）<$（S2，→2，φ2）和c1，c2.. ck.m @（S1，→1，φ1）是以前对c1，c2. ck.m [P1].这些在LST上组织了一个有趣的代数结构。4.4复制假设P的标记语法树是（SP，→P，φP）。然后是P的那个|P为（SP，→P，φP）<$（SP，→P，φP）。重新考虑构造标记树的并行合成的方法，我们观察到，为了构造（SP，→P，φP）<$（SP，→P，φP），我们必须选择（SP，→P，φP）的一个副本此外，对于每个α1∈V，我们必须选择一个α2∈V作为同一个环境过程或原子过程n∈P的恒等式，但在复制的（SP，→P，φP）中。我们可以定义（S，→ ，φ）（S，→，φdef S，→ ，φ）φ2P PPP P P）=（P P P以同样的方式，我们可以定义（SP，→P，φP）k，对所有k∈N。一般来说，这种构造假设为每个环境或原子过程选择，不是一个单元作为单位，而是一个有限的k单元链。对于每个i∈1，2，. k，每个链的第i个元素满足P的元素的单位标号的要求。也就是说，如果{α，β，γ，. 如果是为（SP，→P，φP）选择的元素，那么我们将得到链：对于α：α1，α2，...， αk，对于β：β1，β2，...， βk，对于γ：γ1，γ2，.，γk.. 对于：1，2，...， 好吧对于每个i∈ 1，2，. k是元素{αi，βi，γi，.是我们的R.马代尔角Priami /理论计算机科学电子笔记99（2004）3-2915环境和P.以同样的方式，我们可以为P的过程图的每个节点选择一个可数的元素链。我们用（SP，→P，φP）φ∞表示以这种方式构造的标记语法树。更具体地说，如果主人（SP，→P，φP）的环境是α，如果我们认为αJ∈V是主环境温度（S，→ ，φ）<$∞则e∞def <${e| i ∈ 1, 2, ... k}和e∞defej，P PPαJ=αiνj=νj其中νj∈ {βj，γj，. 其中e∞是（SP，→P，φP）<$∞的函数e，ej对于标记树j的一个。作为前面构造的结果，我们可以声明标记树（SP，→P，φP）<$∞是的标记语法树！P.5逻辑本文的主要目标是构建一个基于环境演算的时态逻辑，能够描述移动计算的属性以及位置的层次结构及其随时间的修改。我们打算构造的逻辑是一个分支命题时态逻辑，CTL12。这种构造的要求[6]是组织一个结构M=（S0，S，R，L），其中S0是我们模型的初始状态，S是我们模型中所有可能状态的类，R是状态之间的可达性关系，R<$S×S，L：S−→ P（AP）是一个函数，它与每个状态S∈S是一组原子命题L（S）<$P（AP）-在状态S中为真的原子命题的集合（AP将是原子命题的类）。我们开发了标记语法树，将它们用作逻辑中的状态。初始状态的选择取决于我们分析的目的。如果我们对一个环境演算过程P本身的未来感兴趣，那么P的标记语法树将是初始状态。但是如果P将与另一个进程Q交互，或者将成为环境的子进程，或者两者都像m [P]中那样|Q]，那么，即使我们对P特别感兴趣，初始状态也将是m [ P]的标记语法树|（我们可以使用为标记树开发的计算操作来定义它，即，m和m @）。对于给定的初始状态S0=（S0，→0，φ0）（存在于给定过程P的标记语法树中）构造S的直觉是以这样的方式完成的，即包含具有与P相同的环境和原子过程的所有过程的所有语法树，具有相同的身份，但在可能的不同空间结构中。在这些状态之间，我们将消除我们选择CTL是因为它比CTL更有表达力，但CTL也是可能的。13我们在这里也包括一些环境被消费溶解的情况，16R.马代尔角Priami /理论计算机科学电子笔记99（2004）3-29我0JJ对于那些Si，OJ因为这样的空间结构对于从S014获得的状态是不可能的。这些因素促成了以下定义：定义5.1假设S0=（S0，→0，φ0）是我们的初始状态。然后defS ={（Si，→i，φi）|Pi<$P0，Oi<$O0，且对所有n∈Pi，idi（n）= id0（n）}.总之，我们可以认为，通过扩展，所有这些过程都有U0=Ui，U0=Ui且O0=Oi. 为此，我们进一步讨论A A P PUP、UA和O，无其他索引。定义5.2我们将原子命题的集合定义为：AP ={xiny x ∈ U P <$U A <$O和y ∈ U A <$O}。|在我们的逻辑中，xiny只是一个原子命题，x，y只是字母。AP的基数将是card（UP<$UA<$O）×card（UA<$O），它取决于（多项式）在环境演算过程S0中的原子过程和环境的数量。定义5.3我们定义解释函数L：S→ P（AP）为：L（S）={xiny|如果x∈UP，则x ∈ e y，或者如果x∈UA<$O，则e x ∈ey}定义5.4我们定义可达性关系R<$S×S如下：如果（S0，→0，φ0）和（S1，→1，φ1）是进程P0和P1的标记语法树，则<$（S0，→0，φ0），（S1，→1，φ1）<$∈Ri<$P0→P1(i.e.P1可以从P0在一个步骤的环境演算减少）。可达性关系可以使用一些简单的算法来描述，一个用于环境演算的每个约简规则。我们在一篇配套论文[8]中提出了这些算法。它们确定，给出一个状态S，可能的状态SJ使得（S，SJ）∈R。按照经典的方式介绍CTLwe定义：定义5.5全路径是无限序列S0，S1，. 的状态，使得（Si，Si+1）∈ R对所有i。 我们使用约定，如果x =（S0，S1，. ）表示全路径，则xi表示子路径x（Si，Si+1，Si+2，. ）的。例如，开放能力;在这种情况下，我们认为这些环境仍然存在于我们的过程中，但它们有一个14环境演算的归约规则允许通过消耗能力来破坏一些复杂的过程，但不允许构建一些复杂的过程。R.马代尔角Priami /理论计算机科学电子笔记99（2004）3-29175.1语法我们从AP开始归纳地定义了一类状态公式（状态为真或假的公式）和一类路径公式（路径为真或假）。我们接受逻辑运算符和、时间运算符X（下一次）和（直到）以及路径量化器E（对于某些未来）作为基本运算符。我们将从它们导出所有常见的命题逻辑算子，时间算子G（总是）和F（有时）以及路径量化器A（对于所有未来）。语法规则：(i) β∈AP中的每个原子命题α是一个状态公式(ii) 如果p，q是状态公式，那么p<$q，<$p也(iii) 如果p是路径公式，则Ep，Ap是状态公式1 '。每个状态公式都是一个路径公式2'. 如果p，q是路径公式，那么p<$q，<$p也3'. 如果p，q是路径公式，则Xp，p<$q也是语法约定：(i) Ap把Ep放回去。(ii) EFp取代E（真EFp）。(iii) AGp取代了<$EF <$p。(iv) AF p表示A（真βp）。(v) EGp使<$AF <$p膨胀。5.2语义我们现在定义|= inductively。我们写M，S|= p意味着状态公式p在模型M中的状态S 0处为真，并且M，x| = p意味着路径公式p对于结构M中的全路径x为真。规则是：M、S0|= Pi <$P∈L（S0），其中P∈APM，S0|= p <$q i <$M，S0|= p和M，S0|=qM、S0|=<$p i M，S0|= pM、S0|= Ep i全路径x =（S0，S1，. ）在M中，M，x|= p M，S0|= Ap i全路径x =（S0，S1，. ）在M中，M，x |= p M，x| = p i M，S0|= pM，x| = p<$q i <$M，x| = p和M，x| = qM，x|=<$p i ≠ M，x不是这样的，|= p18R.马代尔角Priami /理论计算机科学电子笔记99（2004）3-29M，x|= p <$q i <$<$i（M，xi|= q和j（j

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