开放分布式系统的一阶多排序分支时间逻辑系统及其应用

理论计算机科学电子笔记67（2002）网址：http://www.elsevier.nl/locate/entcs/volume67.html20页一种用于开放分布式系统开发的分支时间逻辑系统卡洛斯·H C. Duarte1;2BNDES大道智利100，里约热内卢，巴西，20001-970地址：Rua do Bispo 83，Rio de Janeiro，RJ，巴西，20261-902汤姆·迈鲍姆3英国伦敦大学国王学院计算机科学系，邮编：WC2R 2LS摘要我们提出了一个新的一阶多排序分支时间逻辑系统的平等致力于支持开放分布式系统的发展。这一系列的系统，这应该是在严格的软件开发过程中对待的固有特性，在整个文件中使用，以激励我们的形式主义的具体功能。我们提出了一个解决饮酒哲学家问题的方法来说明这个新的逻辑系统的应用。关键词：时态逻辑，规范，验证，分布式系统，软件开发1引言自70年代末Amir Pnueli的开创性工作以来，时态逻辑已经在计算机科学的许多分支中取得了巨大成功，包括需求工程，软件规范和验证，逐步修正和系统测试。关于并发系统的开发，Manna和Pnueli最初展示了时态证明系统如何以自然的方式与编程语言相关联[17]。接下来，Barringer解决了一个重要的可组合性问题[5]，使得依赖并发程序的结构来证明时态属性成为可能。随后，Fiadeiro和Maibaum也通过展示并发软件系统可以基于时态理论表示以模块化方式进行指定和验证来提高其工作的抽象级别[10]。这一结果链涉及严格的软件开发过程中不同但相互关联的阶段1 部分由CNPq研究资助编号301037/00-0支持。2 电子邮件：carlos. computer.org3 电子邮件地址：tom@maibaum.org2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。184Duarte和Maibaum185采用特定软件开发方法的选择和处理特定应用领域的必要性在选择现有时态逻辑系统或开发新时态逻辑系统的决策中起着核心作用例如，Sernadas和其他人开发了一个线性时间逻辑系统，特别适合面向对象的方法[21]。Lamport和Abadi已经将动作的时间逻辑应用于许多领域[15]，特别是分布式容错系统的开发这类决策所涉及的是对手头的方法或领域的固有特性的识别，以及对每个逻辑系统的评估|在语言、模型、公理系统、推理规则和自动化支持方面|以确定这些固有特征是否以某种方式被形式主义支持，从而促进软件开发。如今，随着网络技术的出现，由于在广阔的地理区域上的计算能力，人们对软件开发方法越来越感兴趣，这种方法不仅有助于将分布识别为问题需求，而且还允许软件工程师在开发过程中将分布作为设计或实现决策。分布式系统可以被描述为松散互连的集合，不一定位于同一位置。在这个上下文中，对象是更具体的实体的抽象，例如自治代理或计算单元。顺便说一句，我们的定义承认并发系统作为一个特殊的情况。分布式对象可以以组件的形式放在一起，组件与周围环境有显式的接口。这些分布式系统或组件，保留几乎没有控制他们的环境被称为是开放的，一个重要的属性，不仅允许设计的独立性，但也强制可组合性，增量和重用的相应的软件工件。尽管开放式分布式系统目前很受欢迎，但似乎很少得到支持针对现有逻辑系统中的软件开发。这似乎主要是由于其固有特性的复杂性。分布式对象可以通过不同的模式进行交互，例如消息传递或资源共享。参与者的数量可以在每个交互模式中变化。组件的内部和外部配置可以在设计时固定，也可以动态更改。理想情况下，一个致力于开放分布式系统开发的逻辑系统应该允许对分布式系统模型中存在的所有细节进行规范和验证。在本文中，我们提出了一个新的时间逻辑系统，我们认为适当的以严格的方式开发开放的分布式系统。 我们的技术贡献分为两部分。在第二节中，我们描述了我们的逻辑系统的语义模型和证明演算。在第3节中，我们说明了这些形式结构，提出了饮酒哲学家问题的解决方案[6]。最后，我们对相关的和未来的研究提出了一些意见。2开放分布式系统的逻辑系统2.1语言和模型我们的逻辑系统是按照一个语言家族来组织的，每个语言家族都使用逻辑符号和逻辑外符号来定义。我们从一阶语言的集合出发，采用可数无穷逻辑变量族V。有可能Duarte和Maibaum186翅片翅片翅片=（S， ）是一个全域签名：S是一组排序符号，是一个S -索引的以这种方式表示由某些分布式系统的对象交换的潜在的nite数量的消息，这是Sistla [22]，Koymans [12]和其他人广泛研究的传统命题时态逻辑系统所无法达到的。我们还采用了多排序语言，因为排序符号似乎使逻辑结构更具可读性和结构化。排序和所有其他逻辑外符号都属于签名，定义如下：定义2.1（签名）签名=（，， A）是一个三元组的不相交和nite符号集，使得：函数符号族;是S - 动作符号的索引族;A是S属性符号的S-索引族。使用排序的签名符号的索引在每个语言表达式上诱导类型。一个函数结构，它采用hs1; ：;sni类的表达式，s排序的结果，即由S索引S的类型type（f）= h s ;：;si！ S.1N翅片每种签名符号都有不同的解释。排序符号表示值的非空集合。中的符号以及V中的变量都是完全的和刚性的，也就是说，它们总是具有不随时间推移而变化的意义。另一方面，[A]的元素是灵活的，这意味着它们具有依赖于时间的解释。中的动作符号表示瞬时事件的发生。它们与A中的属性符号不同，A中的属性符号是总体的、功能性的，代表着当前的状态。具有这种解释的变量、函数、动作和属性经常出现在开放分布式系统表示中。在正式确定签名符号的含义之前，我们需要澄清所采用的时间表。通常认为整个宇宙是一次产生的观点使我们认为所有的时间都是在同一瞬间开始的。请注意，分布式系统通常有一个不同的时间点，从这个时间点开始，它们开始呈现一些可观察的行为， 时间所允许的 我们很容易表现出这种特征。出于同样的原因，我们选择在这里只处理nite time ows，这也符合分布式系统中的一般情况，即从特定的时间点开始，不一定只表现出稳定的属性。关于分布式程序，这种属性的一个例子是终止，这是一个不寻常的要求，在这个领域，原来是表示使用所采用的时间OWS以及。 我们把注意力限制在离散的OWS上， 为了简单起见。时间流通常根据其线性或分支性质进行分类大多数程序的时态逻辑虽然基于线性时间流，但也依赖于附加的使能谓词来表示某些后续计算的可能性。开放的分布式系统的设计似乎也需要一种表达可能性的方式，不仅要表示可能的计算步骤，而且要与其环境建立更松散的联系，这是每个问题的固有部分。这是因为要求环境以特定方式运行可能与开放性属性相矛盾。然而，我们只知道如何用分支时间表示可能性。事实上，可能性是一种属性Duarte和Maibaum187=通过当前和/或未来的事件，但也可以考虑时间向过去的分支。 考虑到在分布式系统中，过去被认为是证明当前情况的必要事件序列，而且在初始化的时间表中，通常可以采用一组表达完整的未来时间连接词来表达任何相关属性，我们不必在这里处理过去的额外复杂性关于分支时间可以在文献中找到[7，26]。所谓的皮尔士观点主张，断言一个命题最终出现的公式在给定时刻x为真，当且仅当该命题在x的某个未来的某个时刻为真。相反，奥卡姆主义的观点认为，除非提供关于实际未来的额外信息，否则讨论公式的真值是毫无意义的。为了澄清这一区别，可以定义一个隐喻。假设一个系统和两个全知的观察者，渴望和懒惰。两人都认为，金融体系的演变几乎与前面几段所描述的一样，OW具有初始时刻，是离散的，晚上见。接受皮尔士观点的伊格尔礼貌地忽略了他所知道的一切，并密切关注系统，将所观察到的系统作为他自己的当前时刻。根据他的感知，未来会发生什么跨越了许多不确定的可能性分支懒惰，相反，采用奥卡姆主义的他只能把系统的不同行为看作是一组线性终止序列。对他来说，在系统的某个行为的某个时刻，本来可能发生的情况是根据其他可能的行为来定义的。比较这两种概念上不同的观点，我们可以得出结论，什么被视为分支时间逻辑取决于所选择的观察者。两者都是合理的观点，允许我们谈论可能性。分支时间的数学模型在文献中比比皆是。 研究时态逻辑的语义模型产生了广泛的数学结构[24]。在并发系统的领域中，事件结构和转换系统是首选[23]。在这里，我们采用第二种结构来捕捉分支时间的奥卡姆主义观点，因为我们可以通过这种方式定义基于未来时间连接词的逻辑的线性时间片段，从而依赖于一组标准的公理方案和推理规则，这是相当标准的。因此，我们将分支时间结构表示为世界的线性序列的集合，并通过这些序列中的初始区别点来定义2.2（分支结构）分支时间结构或帧是元组（，0，，），其中：和0分别是世界和初始世界的集合;：！P（）是可达性关系（幂集函数）;是一组非空的可能行为。 每个L2是一个函数，使得：(i) 多姆湖和codLdefN;(ii) 8w2domLL（w）=0$w20;(iii) 8w;w0 2domLL（w）=L（w0）！n=n0;(iv) 8 n 2鳕鱼L9w 2domL L（w）=n;以及（v）8w;w0 2domLL（w0）=L（w） + 1！第0周 2（w）.Duarte和Maibaum188UUUU=U==根据第（1）、（3）和（4）项，确定（不一定是任何计算机程序的）行为的每个世界序列与自然数一一对应。 因此，每个L2是可逆的，我们使用这个事实来定义所采用的分支时间模态的意义。基于分支时间结构，签名符号解释如下：定义2.3（解释结构）一个符号=（，A，），=（S，）的解释结构是一个元组=（ B， U， G， A），其中：B是分支时间结构;U将每个s 2 S映射到非空集合s U，并且每个f2，type（f）=hs1; ：;sni！s，到fU：s1U ： ：snU ！sU;G 映 射 ea chg2A ， type （ g ） =hs1; ： ;sni ！s ， toaG （ g ） ： s1* sn ！ ！sU;A映射ea cha2，t ype（a）=hs1; ：;sni，到A（a）：s1* sn ！ P（）。每当出现在一些符号的解释，这是连接到他们的灵活的，时间依赖的含义。 因此，属性符号表示总功能。随时间变化的事件和动作符号表示在某些时刻可能在它们之间或相对于属于封闭环境的其它事件并行发生的事件。另一方面，排序符号被解释为固定的值集合，函数符号被解释为不可变的总函数。术语代表有意义的价值。 在他们的定义中，我们假设，每个签名的分 类 。关联到一些变量排序符号in.对于符号s 2 S，我们还将s类变量的集合表示为s定义 f v 2Vj（v）= s g.由签名生成的项集定义如下：定义2.4（项）S-索引项集T（）定义如下，条件是x2s[s[A s;f2，g2A且type（f）=type（g）=hs1; ：;sni！ s;andti2T（）si，i2f1; ：;ng：t：：=xjf（ t1; ：; tn）jg（ t1; ：;tn）也就是说，项是变量、空函数或属性符号4，或者项是应用于项序列的函数或属性符号。请注意，使用排序的签名符号索引以自然的方式扩展到术语我们对术语的解释如下。因为我们有一个一阶逻辑，我们需要首先定义逻辑变量如何分配给量化域的元素：定义2.5（赋值）给定一个结构=（B，U，G，A）用于签名=（（S;）;A;），对于映射ea chs到su的赋值N，其中ea chs2S。定义2.6（术语的解释）给定签名=（（S;）; A;）的解释结构=（B，U，G，A）和，[];N：的赋值N！下面定义的是在世界w2B中s2 S类术语的解释：[[x]] ;N （w）defN（ x）if x2s;[[f（t1; ：;tn）];N （w）deffU（[[t1]];N （w）; ：;[tn];N （w））;[[g（t1; ：;tn）]];N （w）def（G（g）（[[t1]];N （w）; ：;[tn]];N （w））（w）.Duarte和Maibaum189=4 空属性符号称为 [3]中的易变常数Duarte和Maibaum190=1;N;N;N;N公式是用逻辑和非逻辑符号写成的，出现在说明书和证明中。 逻辑符号的集合由变量V的集合以及一些经典的和时间的连接词组成。 除了使用逻辑等式、泛数量词和命题连接词之外！ 和：，原子公式是“时间的开始”连接词beg和动作符号在一系列项上的应用。定义那些被认为是原子的公式集合，以及非严格\在所有交替的当前时刻”连接词A和严格\强直到”连接词V的应用。定义2.7（公式）公式集F（）由下面的产生式规则定义，给出了c2，type（c）=hs1; ：;sni;ti2T（）si，i2f1; ：;ng;x2s和qj2F（），j2f1;2g：q：：=（t1=t2）jq1！ q2j：q1j 8xq1j c（t1; ： ：;tn）j begj A（q1）j（q1）V（q2）表达式集定义如下：E（）defT（）[F（）.空连接词beg表示每个行为的开始时间。 给定公式p和q，A（p）意味着p发生在可能继承实际过去历史的任何时刻，（p）V（q）意味着p严格发生在未来（即，在当前时刻之后），并且Q从下一时刻发生，直到但不一定包括该发生时刻5。 我们更喜欢使用Kamp提出的严格强直到算子V，因为其他常见的线性未来时间联结词都可以用这种方式定义在我们的语言中包含普遍模态A，使得对偶的E成为可定义的，即可能性的模态。我们的分支时间模态被解释为使用等价关系'over be-我们的前任。我们以逐点的方式来定义这种关系，说一个框架的两个世界是等价的，当且仅当所有的属性和动作符号在两个世界中都有相同的解释。逻辑公式的满足定义如下：定义2.8（公式的满足）给定签名，在行为L的世界wi处的公式的满足（即，wi2domL）通过具有赋值N的结构=（B，U，G，A）定义如下：（;N;L;wi）j=a（t1; ：;tn）iwi2A（a）（[[t1]]（wi）; ： ：;[tn]]（wi））;（; N; L; w i）j=：p i不是（; N; L; w i）j= p;（; N; L; w i）j= p！ q i（; N; L; w i）j= p蕴含（; N; L; w i）j= q;（; N; L; w i）j= 8 x p i对于每个v 2cod N和每个赋值N v，使得如果y 6= x，则N v（y）= N（y），否则，（; N v; L; w i）j= p;（;N;L;wi）j=（t1=t2）i[[t1]（wi）=[[t2]] （wi）;（; N; L; w i）j= beg i L（w i）= 0;（; N; L; w i）j=pVqi存在wj2dom L，其中L（w i）、^、_和$的定义与往常一样。的时间连接词的以下定义也有助于说明和证明：pUq def q_（p ^qVp）（p发生直到q发生）;XpdefpV？（p发生在下一瞬间）;Fpdef>Up（p发生在现在或将来某个时候）;Gp def：F（：p）（此后p发生）;pWqdefGp_pUq（p发生直到q发生，即使q从未发生）;Ep def：A（：p）（p当前是可能的）。2.2公理系统和推理规则在这一点上，我们应该清楚，我们正在处理一个一阶多排序分支时间逻辑系统的平等。为了完成它的定义，我们将定义-ne在逻辑结果关系“之后，对于每个可接受的签名，试图创建前一节中定义的语义结果关系的证明理论近似。我们认为p是一个由非空的派生集合定义的二元关系P r（; p）从假设集合中得出结论p。Pr又由Ax（）、一组公理和一个可导关系生成。Ax（）只包含公理模式的实例，而A x （ ） 是由推理规则的应用程序生成的。导子是有向无环图，顶点用公式标记，边从假设指向结论，使得没有分支路径，并且如果p是标签，则p 2Ax（），p2或一套房产0便士0衍生自 . 为了使推导更具可读性，我们还考虑源顶点有一个传入的边缘，标记有相应的公理方案的名称或与Hyp的情况下的假设，和标准的边缘标记有相应的证明推理规则的名称。我们的公理化从逻辑的经典命题片段开始去...对于给定的分类，使用自动变量f p; q; r; sg F（）：（A1-I）p！（q！p）（弱化）;（A2-I）（p！ （q！ r））！（（p！ q）！ （p！r））（分布）;（A3-N）（：p！ ：q）！ （q！p）;（R1-MP）fp; p！qg q。Duarte和Maibaum192作为一个例子，证明在希尔伯特风格，我们验证在下面的推导推理规则HS（假设三段论）。由于我们不打算陈述和证明我们的逻辑系统的演绎定理（由于我们系统的时间特性，任何这样的定理都不会有通常的公式化），所以这个推理规则应该被广泛使用。该规则的陈述和推导如下：引理2.9（推论规则HS）对于任意p2F（），下列推论规则是可导出的：（HS）f p！q; q！ R gp！ R.校样：1. p！ qHyp2. 问！ r羟脯氨酸3. （q！ r）！ （p！ （q！（r））A1-I4. p！（q！ r）R1-MP 2，35.（p！ （q！ r））！（（p！ q）！ （p！（r））A2-I6. （p！ q）！ （p！ r）R1-MP 4，57. p！ rR1-MP 1，6现在我们转向逻辑的线性时间片段的更有趣的公理化。在下面的公理系统和推理规则中，我们采用了前一节中定义的非严格连接词的缩写：（A4-GV）G（p！ q）！ （pVr！ qVr）;（A5-GV）G（p！ q）！（rVp！ rVq）;（A6-V）pVq！pV（q^pVq）;（A7-V）（p^qVp）Vp！qVp;（A8-V）p V q ^rVs！ （p ^r）V（q ^s）_（p ^s）V（q^s）_（q ^r）V（q ^s）;（A9-V）（p_q）Vr！ pVr_qVr;（A10-GX）G（p！ Xp）！（X p！ G p）;（A11-X）X>;（A12-X be g）：X（beg）;（R2-G）f p gG p;（R3-begG）fbeg！Gp gp。这些是从公理化中得到的，公理化也考虑了强严格since连接词的存在，如[11]中所讨论的，通过删除这个过去时间连接词并包含beg来代替。方案A4、A5和A9与R2一起保证我们有一个正常的模态逻辑，它可以在关系结构上解释A6-7保证了这些关系的传递性，我们以这种方式进入时间逻辑的领域A8在其他方案Duarte和Maibaum193存在的情况下意味着时间是线性排列的。特别是，由于我们选择了初始化时间，这在任何地方都是正确的。我们还采用A10来捕获时间诱导。我们使用A11不仅是为了保证时间流没有端点，而且是为了确保总是有下一个瞬间，捕捉离散时间。方案A12说，没有瞬间在初始瞬间之前。规则R2是通常的时间推广，R3可以称为begG-消除。Duarte和Maibaum194MPMP读者可能想在推导出上述逻辑片段的替换引理之后，使用HS来验证方案A1-10加上规则R1-2是否包含[17]中Manna和Pnueli的后述关系的所有命题定理我们使用来表示这些定理的可证明性。然而，我们对他们的延伸逻辑不是保守的，因为我们更喜欢采用具有固定特性的时间的OWS，以便最小化在构成开放分布式系统规范时产生不一致的可能性。例如，如果两个组成的规范可以分别假设有端点和没有端点，本文讨论了时态逻辑在软件系统设计中的应用，由两个家族中时间属性的分离和推理原则的各自发展[2]排列。活性或进展性质，说明系统最终执行的是对验证方法的巨大挑战，并且通常使用附加的良好基础归纳规则来使用以下导出的推理规则来验证定义系统始终确保的安全属性定理2.10（推论规则IND）下列推论规则对任何p 2 F（）是可导出的：（IND）fbeg！p;G（p！X p）g p.校样：1. 求我！羟脯氨酸2. G（p！ X p）羟脯氨酸3. G（p！ Xp）！ （p！ Gp）4. p！ GpR1-MP 2，35. 求我！ G pHS1，46. pR3-begG 5重要的是要强调，使用IND表示锚定归纳是必要的，因为这条规则不能被改写为公理系统。根据Kr的评论，oger[13]，采用类似的方案会使整个逻辑变得琐碎。在[18]中，这一点如上所述被克服了，但考虑到beg在过去时间连接词方面是可定义的。在TLA中，beg没有逻辑对应物，但是期望规范规范来定义初始化条件。我们选择将分支时间模态公理化如下：（ A13-A ） A （ p！ q ）！（ A p ！ A q ） ; （ A14-A ）AP！ p;（A15-EA）E p！ AE p;（A16-EV）（E p）V q！E（pVq）;（A17-AV）A（p！X（q U p））！ （p！XA（q U p））;（A18-Ebeg）E（beg）！beg;（R4-A）f p gA p.上述公理方案定义了一个完整的分支时间模态，在这个意义上，在任何上下文中使用A都没有限制。模态概括的公理方案A13-15和规则R4-A，尽管与通常的表述略有不同，但使A成为S5模态。方案A18说，当前时刻是初始时刻的可能性迫使它成为这种情况，这意味着所有行为首先是同步的，即，他们最初世界Duarte和Maibaum195的水平是一样的。A16还要求，Duarte和Maibaum196只有当它的随后的历史直到但不包括那一点也可以通过替代行为来实现时，它才在未来时刻拥有替代图式A17意味着，我们对可能性的概念是相对不变的，在选择当前世界的可能替代品时，不会随着时间的推移而变得越来越受限制如上所述，在忠实地表示消息传递系统时需要一阶逻辑。我们假设我们的逻辑系统配备了通常的Free变量函数，将p2E（）写为p（x; y）以强调每当fx;ygFree（p）.我们还假设存在一个映射f g，具有取代关系 F G（E）E（）E（））E（）。 对于fp; q; r gE（），集合fs2E（）j（p; q;r）fg（s）g由其类属元素pfqnrg表示，表示p中r的某些q替换，这里省略了以直接的方式定义。常用的替换函数[ ]：F（）VT（）！F（）成为这个替换关系的固定点（其中所有可能的替换都已经进行）：p[x n t]=qiq2pfxnt g和qfx nt g =fq g。 我们知道r对q在p中是自由的当且仅当F ree（r）F ree（pf q n r g）. 像往常一样，我们只允许一个替换pfq nr g被引用， 如果r对p中q是自由的。有了这些定义，我们可以扩展公理化如下捕获第一级片段：（A19-8）8xp（x）！intn[n];（A20-8）8x（p！q（x））！（p！8x q（x）），条件是x62F ree（p）;（A21-EQ）t= t;（A22-EQ）t1=t2！ （aftnt1g！ aftnt2g），其中a为原子构型; qgp！8x q（x），条件是x62F ree（p）。上面的公理化是标准的。唯一的例外可能是在A22-EQ中使用替换关系来证明像x = y这样的定理！（f（x）= y！ f（y）= x），f 2，不能仅基于替换函数导出。在[21]中，采用了相同的概念。为了结束我们的公理化，我们还需要说明其他连接词是如何相互作用的等式和一阶量化器。这被定义如下，假设t对于p中的x是自由的，并且每个ti不包含属性符号：（A23-9V）（ 9x p（x））Vq！9x（p（x）Vq）;（A24-EQG）t1=t2！G（t1=t2）;（A25-NEQG）t16 =t2！G（t16=t2）;（A26-8A）8xA（p（x））！A（8x p（x））;（A27-EQA）t1=t2！ A（t1=t2）;（A28-NEQG）t16 =t2！ A（t16=t2）。A23是一个Barcan公式，说明量子结构域不随时间的推移而变化它需要更传统的8 x G p（x）！G（8× p（x））。请注意它与A16的相似性，尽管在这种情况下，反过来是无效的。A24-5的意思是，我们采用的是不包括属性符号的严格术语。由于这些方案中的边条件，我们失去了替代性质，这将允许我们在任何上下文中用逻辑等价的公式替代公式A26-8在分支时间模态方面起Duarte和Maibaum197为了结束我们的证明理论研究，我们没有证明REPL，一个替换规则，是可导出的。这一点通过基于连接词单调性的逻辑语言结构归纳得到了验证 对于A，这意味着`A（p！ q）！（A p！A q）。虽然这条规则只适用于没有灵活符号的逻辑片段，但在实践中常常是有用的：命题2.11（替换规则）给定一个签名，对于任何不包含灵活符号的fp; qg[fx;ygF（），以下推理规则是可导出的：（REPL）fx$yg p[qnx]$p[qny]。在为我们的逻辑系统的模型和证明理论提供了严格的定义之后，我们现在可以评估它的一些特征：定理2.12（强可靠性）p表示j=p。这是验证在通常的方式，根据满意的概念，通过确保每个逻辑公理是普遍有效的，每个推理规则保持有效性，这意味着有效的前提意味着有效的结论。在我们的希尔伯特式证明中，一个额外的结构归纳论证保证了每个蕴涵都保持有效性，即对于任何一组句子[f p g]，` p意味着j= p。完整的证明出现在[8]中。关于完备性，不难看出，因为可以在理论中编码皮亚诺算术，所以我们的逻辑系统是不完备的[14，19]。尽管如此，也许可以找到类似的解释结构来恢复完整性，也许沿着[3]中建议的路线。在继续研究我们的一阶框架之前，似乎有必要确定逻辑的命题片段是否是中等完全的，这意味着上述陈述的逆命题对任何nite都成立。我们已经知道这样的片段不是紧的，因此强完备性再次失败。这方面的研究正在进行中。2.3结构化概念我们采用了一个逐步的开发过程，灵感来自抽象数据类型理论的研究[16]。抽象的规范是逐渐RENE，直到产生一个具体的实现。开放分布式系统规范是根据时间理论表示来构造的，其定义如下：定义2.13（理论表示）理论表示是一个对=（，），其中是一个签名，是一组公式（表示公理）。使用理论表示来定义开放分布式系统，它们的结构和关系可以分别使用特定的签名和理论态射、分类概念来捕获，这些概念在下面介绍：定义2.14（签名态射）2=（2，A2，2），符号态射：1！2包括：代 数结构的态射：1！ 2，即对于每个s2S1，存在唯一的（s）2S2而对于eachf21因此 ，t ype（f） =hs1; ： ;sni！s有唯一的（g）22su ch是t ype（（g））=h（s1）; ：;（sn）i！（s）;Duarte和Maibaum198121集合 论 性 质 的 态 射 ： A ！ A ， 即 对 于 每 个 g2 A ， 使 得 t ype （ g ）=hs1; ：;sni！ s有唯一 的（g）2A2su ch是t ype（（g））=h（s1）; ：;（sn）i！ （s）;集合论性质：一个！2，即对于每个c21这样，类型（c）=h s1;：;sni，则存在唯一的（c）22su ch，使得ype（（c））=h（s1）;：;（sn）i。签名态射将一个签名的符号翻译成另一个签名的符号。扩展这个概念以提供用于在给定签名态射下的分类、项、公式及其集合的翻译的组合定义是直截了当的。这些在这里被省略了。定义2.15（表示态射）给定表示1=（1，1）和 表示 2=（ 2，2），表示态射：1！ 2是提升到公式的签名态射，使得2`2（p）对每个p21（保持结果）。基于逻辑结果关系，要求保留每个表示公理的结果的约束禁止当一个表示被认为是另一个表示的一部分时忘记这些结果中的一些，从而允许可组合软件工件的定义。以下结果最好地说明了这一点命题2.16（签名和表示的范畴）签名和理论表示的集合，以及相应的态射，ne余完备范畴Sig和Pres。3上一篇：哲学家的饮酒问题在本节中，我们研究了饮酒哲学家问题[6]，这是分布式系统中资源分配问题的一个推广。一群哲学家围坐在一张桌子旁，喝着几瓶饮料。每个哲学家都可能是安静的，口渴的，或喝酒的。根据他与邻居分享的瓶子和想要的饮料，哲学家可能会产生冲突，因为瓶子的使用被认为是相互排斥的。这个问题的任何解决方案都必须保证对称性，即所有哲学家都必须遵守相同的规则，并取得进展，口渴的哲学家最终喝下想要的饮料，以及其他要求不那么苛刻的要求。一个更为人所知但又受到限制的资源分配公式是用餐哲学--phers问题，其中成对的邻居共享一个单独的节点。由于这些哲学家都能获得这种共享资源，他们的行动必然是相互排斥的。就像在饮酒者的例子中一样，任何解决方案都必须保证对称和进步，但是每个哲学家的行为都在一系列不同的状态中循环，从思考到饥饿再到进食。在[10]中提出了这个问题的简化版本的模块化解决方案其中，通道用于保证筷子（实际上是叉子）的互斥使用。此外，每个哲学家最终会变得饥饿，然后举起筷子的局部进展假设被用于推导一个全局属性，确保他们在进食和思考状态之间循环。这个定理并不容易验证，因为哲学家们并不需要放下筷子，但是当他们以适当的方式放在一起形成一个系统时，这个属性就会出现。顺便说一句，为了确保在当地环境中最终降低筷子Duarte和Maibaum199对于单个哲学家，必须做出一些额外的假设，如[4]所概述的，不仅说明每个哲学家在吃饭时都愿意这样做，而且还说明一个强有力的公平假设，称为礼貌，这要求最终发生的这一行动，只要它总是最终可能的。我们使用上面概述的食客问题的完整解决方案（基于[10]和[4])作为我们的饮酒者解决方案的一部分也就是说，我们提出了一个解决方案，其中哲学家可以同时喝酒和吃饭，这最后一个活动是由于执行决策而执行的，哲学家有本地属性来记录他们在每个过程中的当前状态。正如[6]所概述的，这种策略通常被用来在解决冲突时建立哲学家之间的区别，因为考虑到吃饭的哲学家总是优先考虑喝酒的冲突。在我们的例子中，我们也使用这个策略来保证解决方案的进展。对称性是通过要求所有哲学家遵守相同的规范来保证的。饮料拟定溶液的规格、配置和验证哲学家的问题在附录中提出。其中提出的主要结果是我们的解决方案的正确性的证明，这是由以下定理的可证明性总结的，在理论介绍D-Phil的上下文中制定，其中描述了饮酒的哲学家：`thirsty （ x ） =TRUE！ F （ drinking （ x ） = TRUE ）（ 1）这个例子是非常说明性的，作为证明我们的逻辑系统的特征的一种手段句子（1）是一阶性质的，整个问题都是用这个框架来表述的，因为与用餐者问题不同，哲学家在每种情况下可以分享和喝的饮料数量是nite但先验不确定的。此外，（1）的验证只能在局部环境中通过依赖于意愿（2）和礼貌（3）的分支时间假设来进行，这是菲尔公理中的一项，描述了用餐的哲学家：吃=真的！ FE（chops #）（2）GFE（排骨#）！ F（chops #）（3）4最后发言为了支持开放分布式系统的严格开发，我们提出了一个新的一阶多排序分支时间逻辑系统。许多其他逻辑系统存在类似的功能，也许可以用于相同的目的。下文对此进行了分析在一阶形式主义，我们的系统保持了许多相似之处，[15][17][18][19][1这些系统考虑外部使能谓词（分别为Enabled和En）的存在，类似于我们的E，它们的陈述和/或证明由某些计算发生的可能性来判断（对于TLA，最近在[1]中确实提供了Enabled的句法定义）。该系统与我国的系统存在一些细微的差异，如TLA系统采用了过渡性的定义动作，该系统中没有X（next）连接词，第二个系统中也引入了X（next）连接词。然而，与我们的工作相关的最相关的区别似乎是这些系统具有线性性质的特征，而不是我们的分支时间系统。Duarte和Maibaum200我们的逻辑系统与其他命题分支时间形式有很大不同。例如，与CTL [9]相关的主要区别在于，E在这里被认为是一个完整的分支时间模态，在这个意义上，在任何上下文中使用这个连接词都没有限制，而在CTL中，它只能包含一个被线性时间连接词F或G包围的公式。另一个区别是与CTL和其他奥卡姆分支时间系统（例如[7，23]）有关，它们对E的解释受到可能的未来事件的影响。我们认为，在开发开放分布式系统时，采用E的直接解释更符合软件工程师的直觉。事实上，这种解释最初是由Zanardo [25]在具有不同语言、时间框架和逻辑外符号解释的命题逻辑系统的背景下提出的。显然，我们的系统从根本上不同于Peirce的命题时间形式主义[11]，后者以实质上不同的方式定义和公理化，没有分支时间模态。报告的工作为未来的研究提出了许多有希望的方向进来会尝试在我们的框架中引入连续时间或间隔是有趣的。此外，为我们的逻辑（至少是命题片段）提出一种替代的范畴模型理论，可能会以不同的风格，更有效的证明理论。最后，关于我们的逻辑系统在开放分布式系统规范中的应用，还有更多的实验工作要做。引用[1] Abadi，M.和S. Merz，On TLA as a logic，in：M. Broy，editor，Deductive ProgramDesign，NATO ASI Series，Springer-Verlag，1996 pp. 235{271.[2] 阿尔彭湾和F. B. Schneider，De ning liveness，Information Processing Letters21（1985），pp. 181{185.[3] Andr eka，H.例如，程序的有效时态逻辑，在：L.Bolc和A.Sza las，editors，Timeand Logic：A Computational Approach，UCL Press，1995 pp.51{129.[4] Barreiro，N.，J. Fiadeiro和T. Maibaum，客体社会中的礼貌，载：R。Wieringa和R.Feenstra，editors，Information Systems：Correctness and Reusability（1995）. 119{134.[5] 巴林杰，H.，时态逻辑在并发系统的组合规范中的应用，在：A。高尔顿，编辑，时间逻辑及其应用（1987），pp。53{90.[6] Chandy，K. M. J. Misra， The drinking philosophers problem， ACM Transactions onProgramming Languages and Systems6（1984），pp. 632{646.[7] do Carmo ， J. 和 A.Sernadas ， Branching versus linear logics yet again ， FormalAspects of Computing2（1990），pp.24{59.[8] 杜阿尔特角H. C.的方法，可扩展软件系统设计的证明理论基础英国伦敦帝国理工学院计算机系博士论文（1998年）