Petri-PDL：随机Petri网的动态逻辑及其应用

DS可在www.sciencedirect.com在线获取理论计算机科学电子笔记305（2014）67-83www.elsevier.com/locate/entcsPetri网的扩展命题动态逻辑1Bruno Lopesa，2 Mario Benevidesb，3Edward Hermann Haeuslera，4aDepartamentodeInform'aticaPontif'ıciaUniversidadeCat'olicadoRiodeJaneirobProgramadeEngenhariadeSistemaseComputaBundesaoUniversidade Federal do Rio de Janeiro摘要命题动态逻辑（Propositional Dynamic Logic，PDL）是一种多模态逻辑，用于序列程序的描述和推理。Petri网是一种被广泛使用的形式化描述和分析并发程序的非常直观的图形表示。Petri-PDL是PDL的扩展，其程序是Petri网，它结合了两种形式主义的优点，使用组合和结构方法来处理Petri网在这项工作中，我们提出了一个扩展的Petri-PDL处理随机Petri网，3逻辑。该系统是一种替代模型的性能评估的组成和结构的方法。我们讨论了它的可靠性，可判定性和完备性，并给出了它的SAT问题的EXPTime完备性的证明给出了一个使用实例关键词：动态逻辑，Petri网，随机Petri网，程序验证1引言随机现象在我们的日常经验中无处不在。天气变化和设备故障，大多是不可预测的，是任何人都熟悉的。实时和容错计算机系统必须考虑这些随机现象，并应设计考虑到一些环境参数。旧的多用户备份系统的设计者考虑了硬盘的逻辑（磁道和扇区）和物理（写头）部件的故障概率，建立了一个容错驱动程序，能够根据1这项工作得到巴西研究机构CNPq和CAPES的支助。审稿人提供了有用的建议，导致第一份手稿的改进版本2电子邮件：bvieira@inf.puc-rio.br3电子邮件：mario@cos.ufrj.br4电子邮件：hermann@inf.puc-rio.brhttp://dx.doi.org/10.1016/j.entcs.2014.06.0061571-0661/© 2014 Elsevier B. V.保留所有权利。68B. Lopes等人/理论计算机科学电子笔记305（2014）67要求.当然，这可能是建模和性能评估领域中最简单的例子之一。本文介绍了我们的建议，加入一个逻辑形式主义（动态模态逻辑）和数学建模工具描述随机现象（随机Petri网），允许，一个带标记的随机Petri网π和一个性质α描述了一个要求<$π<$α，这意味着π的至少一个预期行为满足α，或者，[π]α意味着π的每个行为都满足α。 这些性质的验证可以被看作是在设计阶段对π我们用DS3表示这里提出的逻辑，其中普通的Petri网程序被随机Petri网程序所取代我们讨论了DS3的可靠性，可判定性和完备性问题，我们的语义和我们提出了一个多项式减少的两人走廊瓷砖游戏DS3SAT，从而显示其EXPTime完备性。在第2节中，我们提出了理论和概念背景，激励我们的建议和简要比较它与其他方法。 第3节介绍技术Petri网的背景下，第4节介绍了DS3逻辑，并讨论其可靠性，可判定性和完整性方面，我们的语义和第5节介绍了两个人的走廊瓷砖游戏减少。第6节给出了一个使用示例，第7节给出了结论和进一步的工作。2理论背景随机过程是一种数学建模工具，主要用于描述作为强制性参数的时间函数的概率性质的现象。之三[22]。随机过程{Y（t）：t∈[0，∞）}是定义在同一概率空间上并在同一状态空间中取值的随机变量族。因此，随机过程可以被理解为提高样本路径的时间函数族，即，状态空间中的轨迹一般的随机过程可能相当复杂。其中，那些没有记忆的轨迹，以达到目前的状态6，也被称为马尔可夫过程，已被广泛认为是建模计算过程。具有离散状态空间的马尔可夫过程如果时间是连续的，则通常使用术语连续时间马尔可夫链（CTMC）。 CTMC是在随机性（内部或外部）环境中考虑的计算系统的自然模型。CMTCs作为建模和绩效评估的工具与嵌入式网络竞争。然而，后者并没有提供清晰的机制来描述同步、阻塞和分叉（即消费者拆分）。另一方面，Petri网在描述系统的这些最后提到的方面方面是相当不错的。随机Petri网（SPN）的提出带来了一种均衡计算机科学的一个分支，研究和开发工具和方法，以帮助模拟和评估计算机系统，并将随机现象考虑在内。[6] 数学上需要Pr（Y（t）≤ y：Y（tn）= yn... Y（t0）= y0）= Pr（Y（t）≤ y：Y（tn）= yn），其中t> tn···> t1> t0.B. Lopes等人/理论计算机科学电子笔记305（2014）6769在系统设计的建模和性能评估阶段在[24]中，提出了SPN，以避免将建模阶段定义的嵌入网络转换为评估阶段的复杂CTMC。在第3节中，SPN的定义要求根据指数概率分布（实际上是负指数分布）启用转换。为了确保从SPN自然导出的随机过程是CTMC，该要求是必不可少的[27]。动态逻辑[9，13]通常用于处理程序推理，命题动态逻辑（PDL）[9]是其最知名的变体之一。在PDL中，每个节目P对应于模态[P]。公式[P] α意味着，在P的每一个可能的运行之后，α保持不变，考虑到P停止。因此，<$P<$α，<$[P]<$α）的缩写形式，表明该性质在P的某些可能的运行之后保持不变。动态逻辑提供了大量的系统和工具，在模型检验中使用[5，11，17]。Petri网不仅是一种被广泛使用的处理并发程序的形式主义利用这一点，Petri-PDL [1，18]用标记Petri网程序代替了传统的PDL程序因此，如果π是一个带有标记s的程序，那么公式πs，π意味着在运行由其初始标记为s的Petri网设计的程序之后，π π最终将为真（也可能是一个类似Q的模态，用括号替换标记）。正如我们已经讨论过的，普通的Petri网不能表达运行-dom现象以精确的方式。例如，一个共享内存的两处理器系统这种情况可以被视为一个实时问题，或者是一个生产力问题。后者被证明是一个概率问题，可以通过CTMC或SPN以更优雅的方式进行建模。因此，使用概率附加到Petri网中的转移是获得SPN的一种方法。本文提出了基于扩展Petri网的动态逻辑。因此，随机Petri网是通过将指数分布的随机变量与每个普通Petri网变迁相关联而获得的[12，26]。这个随机变量将控制其跃迁的发射速率。转换仅在使能且计时为零时才会触发。这种形式主义已被用来处理非线性时间建模[3，14，21]。还有一些其他众所周知的随机方法PDL，但我们认为，事实上，概率特征存在于这些形式主义的每一个被添加在一个非结构化的方式。我们说，概率形式主义比其他形式主义更有结构性，只要第一种形式主义比其他形式主义具有更清晰的马尔可夫结构。在这个意义上，系统P-Pr（DL）[6，7]没有有限公理化，不允许命题变量的布尔组合，并且只为常规程序定义，结构性较差。Pr（DL）[8]与P-Pr（DL）具有相同的限制，并且是不可判定的。系统PPDL [16]计算一个命题在某些状态下为真的概率，但程序被一个可测量的函数所取代，也就是说，它的随机分量不是合成的。最后，PPDL> r [32]只能描述以下情况：70B. Lopes等人/理论计算机科学电子笔记305（2014）67∈某些概率大于常数r∈且PPDL> 0 [31]，这只能描述某些概率大于零的情况，显示了建模参数如何在查询中施加限制，完全恢复了模型在正式验证中的作用3背景在本节中，我们介绍了在整个工作中使用的Petri网系统，并简要回顾了随机Petri网。3.1Petri网规约系统Petri-PDL使用de Almeida和Haeusler [4]定义的Petri网模型。在这个模型中，只有三种类型的转换，由于其组成，定义了所有有效的Petri网。这些基本的Petri网如图1所示。XX Y(a) 类型1：t1Y(b) 类型2：t2Z(c) 类型3：t3Fig. 1. 基本Petri网为了从这三种基本类型的组成中组成更复杂的Petri网，使用了胶合过程[4]。 以图2（a）的Petri网为例。它是图2（b），2（c）和2（d）的基本Petri网的组合，其中相同的地名表明当粘合时它们将崩溃。3.2随机Petri网随机Petri网（SPN）[12，20，23，26]是一个5元组P=ΛP，T，L，M0，Λ N，其中P是一个有限的位置集，T是一个有限的转移集，P=T，PT和L是一个函数，它定义了地方之间的有向边，转移并分配一个w∈，一个用于转移的乘法权重，作为L：（P×T）<$（T×P）→（在这项工作中，我们假设对于所有边w = 1），M0是初始标记，并且Λ = λ1，λ2，.，λn是每个跃迁的发射率。在SPN中，点火由加价和点火率决定。对于每个转移ti∈T，都与具有参数λi∈Λ的指数分布的唯一随机变量相关联。在初始标记（M0）中，每个转换通过与之相关的随机变量 每个触发延迟都依赖于标记，标记M j处的过渡tiT触发速率定义为λi（Mj），其平均触发delayy为[λi（Mj）]−1。在击发后，eachp通常不启用标记ZXYB. Lopes等人/理论计算机科学电子笔记305（2014）6771Mj（x）−1<$x∈·t\t·BC c(a) 组合Petri网(b) 基本Petri网类型1a BC c(c) 基本Petri网类型2(d) 基本Petri网类型3图二、Petri网与其基本Petri网的组合示例transition通过对其关联的随机变量进行采样来获得新的触发延迟。保持标记启用的先前标记启用的转变使其触发延迟以恒定速度减小。当转换触发延迟达到零时，此转换触发。我们定义t∈T的预设，记为·t，作为所有sk∈S的集合，该集合起源于t的边。t的后集，记为t·，定义为所有sl∈S的集合，t起源于一条边我们说，当且仅当在每个位置p∈·t中至少有一个标记时，转移t是有效的。给定Petri网的标记Mj，转移ti在Mj上成立当且仅当<$x∈·ti，Mj（x）≥ 1且λi（Mj）= min（λ1（Mj），λ2（Mj），.，λn（Mj）），其中·ti是t i的预设。通过设置启用的转换生成的新标记它的定义方式与标记Petri网相同，即Mj+1（x）=Mj（x）+1 <$x∈t·t.（一）Mj（x）其他情况标记Mj的转换ti的新触发延迟定义为：(i) 如果t触发，则与之相关联的随机变量的新出现是新的触发延迟;(ii) 如果ti被禁用并且刚刚被启用，则与它相关联的随机变量的新出现是新的触发延迟;(iii) 在其他情况下，ti的点火延迟的值必须减小。一B一B72B. Lopes等人/理论计算机科学电子笔记305（2014）67⎪⎨⎪⎩⎤Kk：<$l∈·tk，Mj（l）>0J那就是：⎧⎪⎪其中，Mj（x）≥1λi（Mj）≤min（λ1（Mj）， . ，λn（Mj））λ（M）λi=newe（λi）if（二）i j+1⎪M（x）1I j⎪⎪其中，Mj∈·ti，Mj+1（x）≥1<λi（Mj） 其他情况其中newe（λ）表示随机变量的一个新出现，参数λ与ti有关。两个随机变量的最小值分别为λ1和λ2，是一个参数λ1+λ2服从指数分布的随机变量，在一个标记Mj上的逗留时间是一个均值服从指数分布的随机变量⎣⎡Σ−1λi（Mj）.（三）i：m∈·ti，Mj（k）>0由于所有随机变量都具有指数分布，因此可以计算使能转换ti具有最小触发延迟的概率（即，t立即点火的概率）在标记Mj处：λi（Mj）Pr（ti|Mj）=λ（M）。（四）为了说明随机Petri网的使用，我们可以对共享资源的两个进程系统进行建模。进程1是I/O绑定的，进程2是CPU绑定的，如图3（a）所示。输入请求量的巨大差异可以通过设置Λ值（即λ1> λ3）来建模。图3（b）展示了一个在SPN中建模的简单并行系统，其中令牌表示进程。Λ值决定了它在某些方面是否会更快。过程从q 1到q2而不是q 4的概率可以根据等式（4）计算。4DS3逻辑DS3的语言与Petri-PDL的语言相同。差异普通的Petri网程序将被随机Petri网程序所取代（关于如何在框架定义4.4中处理其行为的更多细节）;它包括命题符号：p，q。. .，其中Φ是所有命题符号地名：例如：a b c d . .B. Lopes等人/理论计算机科学电子笔记305（2014）677313⎩2⎩四季及五季年q1第二季第三季(a)一个双进程系统（b）一个简单的并行系统图3.第三章。随机Petri网实例过渡类型：T1：at1b，T2：abt2c和T3：at3bc，每个过渡名称都有唯一的类型Petri网组成符号：名称序列：S ={S，s1，s2，. }，其中n是空序列。我们用符号ssJ来表示所有出现在s中的名字也出现在sJ中。定义4.1程序：我们用π来表示随机Petri网程序，s是一个名称序列（π的标记）。基本程序：πb：：= at1b|公元前2年|abt3c其中ti属于类型Ti，i = 1，2，3随机Petri网程序：π：：= s，πb|π Ⓢ π定义4.2公式DS3公式定义为：|不|¬ϕ|ϕ∧ϕ|好吧，π。我们使用标准的缩写词<$<$T，<$φ <$$>（<$$><$φ），→φφ）和[s，π]s，π，和π是一个带有标记s的随机Petri网程序。DS3中跃迁的激发是根据定义4.3中的激发函数定义的。定义4.3我们定义函数f：S×πb→S如下• f（s，atb）=f=s1bs2，ifs=s1as2·f（s，atbc）=ffs1s2bc，ifs=s1as2如果a/s，• f（s，abtc）=0，s1cs2s3，ifs=s1as2bs3如果a/s，• f（n，η）=n，对所有Petri网程序η.如果a、b/s，则为定义4.4DS3帧用于DS3的帧是5元组F3=R3W，Rπ，M，M， Λ，δπ，其中• W是一个非空的状态p1p4p3T1T3p2p5T2T4问674B. Lopes等人/理论计算机科学电子笔记305（2014）67• M：W→S• Petri网是一个有限的随机Petri网，使得对于模态中使用的任何程序π，π∈Π（即π是Π的子网）• Λ（π）=Λλ1，λ2，.，λn<$是+值序列，表示π1<$π2<$· ·<$πn=π∈ <$的每个跃迁的发射率。• δ（w，π）= δd1，d2，.，dn<$是程序π∈ <$在世界w ∈ W中的触发延迟序列，分别对于每个程序π1<$π2<$··<$πn= π，满足以下条件（设s = M（w）和r = M（v））· 若wRπbv，f（r，πb）=π，则δ（w，πb）=δ（v，πb）· 如果f（s，πb）=π，f（r，πb）= π，且wRπbv，δ（v，πb）是一个随机参数为Λ（πb）的指数分布变量;通过反演，定理，δ（v，πb）=ln（1−u）其中u是一致随机变量的出现−Λ（πb）· 若f（s，πb）/=π，f（r，πb）/=π且wRπbv，δ（v，πb）<δ（w，πb）• Rα是W上的一个二元关系，对于每个基本程序α∈πb，满足下列条件（设s=M（w））· 若f（s，α）<$且δ（w，α）= min（δ（w，α）），wRαvi <$f（s，α）<$M（v）· 若f（s，α）=π或δ（w，α）= min（δ（w，Π）），则wRαvi πw =v• 我们归纳地为每个Petri网程序定义一个二元关系Rη，η=η1<$η2<$··<$ηn，Rη={（w，v）|使得si<$M（u）和wRηi u和δ（w，ηi）= min（δ（w，η i））和uRηv}其中si=f（s，ηi），对于所有1≤i≤n。引理4.5空出现对任意Petri网程序π，f（π，π）=π，Rπ，π是自反的.证据 从定义4.3和4.4中可以直接证明。Q定义4.6DS3模型DS3的一个模型是一对M=<$F3，V<$，其中F3是DS3框架，V是赋值函数V：Φ→ 2W。定义4.7DS3的语义概念设M3为DS3的模型.M3中一个公式的满足性在状态w，用M3表示，wD3归纳定义如下。•M3，wDpi<$w∈V（p）• M3，WDT总是• M3，wDi M3，wK• M3，wD12iM3，wD1和 M3，wD2•M3，wD|其中ηb是η的某个基本程序（即，在从世界w开始运行η之后，如果存在一B. Lopes等人/理论计算机科学电子笔记305（2014）6775个由Rη从w可访问的世界v，如定义4.4所示，76B. Lopes等人/理论计算机科学电子笔记305（2014）67B其中η停止且η保持）如果在M3的所有状态下都满足，则在M3中，则在M3中，引理4.8模态的真值概率M3，wD <$s，πb<$s的概率为（设s=M（w））δ（w，πb）Pr（M3，wD εs，πbεs|δ（w，ω））=δ（w，π）。πb∈φ：f（s，πb）/= φ证据 从关系式（4）和定义4.4可以直接证明这个问题。Q4.1公理系统我 们 考 虑 下 面 的 公 理 和 规 则 集 ， 其 中 p 和 q 是 命 题 符 号 ， η 和 η 是 公 式 ，η=η1<$η2<$· ·<$ηn是Petri网程序，π是标记Petri网程序。（PL）足够的命题逻辑重言式（K）[s，π]（p→q）→（[s，π]p→[s，π]q）（Du）[s，π]p参与者s，πp（PC3）s，η Participants，η1s1，ηs，η2s2，η···s，ηnsn，η，其中si=f（s，ηi），对所有1≤i≤n.（R3c）ns，ηnn参与，若f（s，η）=n（Sub）如果D<$，则D<$σ，其中σ一致地用任意公式替换命题符号。（MP）若D且D→，则D。如果D是，则D[s，π]是。4.2健全性公理（PL）、（K）和（Du）以及规则（Sub）、（MP）和（Gen）在模态逻辑文献中是标准的引理4.9DS3公理的有效性(i) DPC3(ii) D R3证明。(i) DPC3：假设存在一个来自模型M3=<$WJ，Rη，M，ε， Λ，δ，Vε的世界w其中PC3为假。对于PC3在w中为假，有两种情况：(a) 设M3，wD s，ηs（1），M3，w s，η1s1，η2s2，η2 s···s，ηn sn，η2 s（2）.B. Lopes等人/理论计算机科学电子笔记305（2014）6777(1) 存在一个世界v使得wRηv和Pr（M3，v D ≤s，ηb≤ s）|δ（v，v））>0（3）。根据定义4.4 Rη={（w，v）|ηi，δ（w，ηi）= min（δ（w，η i））和uRηv}，由（3）M3，uDsi，ηs和M3，wD si，ηsi，ηs，这意味着Pr（M3，wDs，η1s1，η 2 s2，η2 s2···s，ηnsn，η2sn|δ（w，ω））> 0（4）。由（4）M3，wDs，η1s1，η2s2，ηnsn，ηnsn，与（2）相矛盾。(b)设M3，wD s，η1s1，η2s2，ηns···s，ηn sn，ηns（2），i，对某个i（1≤i≤n），M，wD s，ηisi，ηni存在一个u使得wRηiu，Pr（M3，wDs，η1s1，η2 s2，η 2s2，···s，ηnsn，η|δ（w，ω））> 0（3）存在一个v使得uRηv和M3，vD<$（4）.根据定义4.4，（3）和（4），我们有wRηv，Pr（M3，wD s，η1s1，η s 1）s，η2 |δ（w，ω））> 0和M3，vD> 0. 因此，在本发明中，M3，wD s，ηs.所以PC3是有效的。(ii) DR2003：假设存在一个来自模型M3=<$WJ，Rη，M，ε， Λ，δ，Vε的世界w其中R是假的。对于R3在w中为假，有两种情况：(a) 设M3，wD，η（1），M3，西海岸（2）(1) 存在一个v，使得wR∈，η和Pr（M3，wD ∈，η∈|δ（w，ω））> 0。当f（n，η）=n时，由引理4.5，w=v，wRηw和M3，wDη，这与（2）相反.(b) 设M3，w∈N，η∈N（1），M3，wD（2）. (1)i = Pr（M3，wD =Pr，η=Pr|δ（w，ω））= 0.当f（n，η）=n时，根据引理4.5，wRηw，根据定义4.4，M3，wK，这与（2）相矛盾。因此，R3是有效的。Q4.3完整性正如A. Mazurkiewicz [28，29]，处理Petri网的逻辑通常是不完整的，因为一个地方总是增加其令牌数量的可能性（直到有限可数）。为了能够得到可判定性和完整性的结果，我们将限制自己的一个子集的Petri网，我们称之为规范化Petri网。基本上，规范化的Petri网是一个如3.1节所述的Petri网，它不会积累无限数量的令牌。从现在开始，我们将只考虑规范化的Petri网。DS3的完备性证明是以与Blackburn et.al. [2]，Harel et.al. [13]和Goldblatt[10]。定理4.10DS3逻辑对于标准化SPN程序是完备的78B. Lopes等人/理论计算机科学电子笔记305（2014）67ηη∫0证据（素描）第一步是定义Fischer-Ladner闭包（FL），其中FL（F）表示包含子公式下封闭的最小集合然后，给定一个DS3公式K3和一个DS3模型K3= KW，Rη，M，λ，δ，Vη，我们定义了一个新的模型K=W，R，M，，Λ，δ，V，K通过3η 3F L（），如下所示。K3世界上的关系定义为：u∈v参与φ∈F L（k），Pr（K3，uDφ|δ（u，v））= Pr（K3，vDφ|δ（v，ε）），关系Rε定义为[u]R<$[v]Participate（<$uJ∈[u]<$$>vJ∈[v]<$uJRηvJ）.(a)[u] ={v|vu}(b) W={[u]|u∈W}(c) [u]∈V<$（p）i <$u∈V（p）(d) M（[u]）=s1，s2，. 其中对所有j≥1，vj∈ [u] i <$M（vj）=sj(e) Πϕ= Π(f) Λϕ= Λ（g）δπ（[u]，π）=δd1，d2， . 其中π=π1<$π2<$··<$πn和di=ih（δ（u，u））du其中h是根据稳定性过程减少点火延迟的函数[12]。我们证明了在一个过滤模型中世界（状态）的数量是有限的，因此DS3是可判定的。对于语言L，取DS3的典范模型（一种模型，其中词的集合是所有最大相容集的集合），C3L=<$WL，RπL， ML，<$L，ΛL，δL，VL<$，我们证明了[s，π]<$∈ui <$在所有v中满足uRπLv，<$∈v.然后证明了对任意w∈WL，wD∈w.因此，我们可以证明，如果D，则。完整的证明可以在www.example.com上找到http://www.tecmf.inf。puc-rio.br/BrunoLopes/Proofs。Q推论4.11Petri-PDL完备性由于在所有转移具有相同触发速率的情况下，Petri-PDL被DS 3逻辑包含，因此Petri-PDL对于规范化Petri网也是完整的。5DS3可满足性复杂度在本节中，我们将一个著名的EXPTime完全问题多项式约简为DS3满意度（SAT）问题：两人走廊铺砖游戏。DS3SAT问题涉及确定是否存在满足DS3公式的解释。引理5.1 DS 3的可满足性是EXPTime-hard的。B. Lopes等人/理论计算机科学电子笔记305（2014）6779n证据 证明是通过将两人走廊铺砖问题简化为DS3SAT问题，遵循布莱克本等人的方法[2]的文件。在双人走廊瓷砖游戏中，两名玩家（Eloise和Abelard）必须将正方形瓷砖放置在网格中，以便颜色匹配（每个瓷砖侧面可能有不同的颜色）。玩家从有限数量的瓷砖（颜色随机定义）开始，网格的开始有一个特殊的颜色（比如白色），并且有一个特殊的瓷砖给Eloise，如果放在第1列，那么Eloise就赢了。当游戏开始时，Eloise应该在第0列放置一个瓷砖;轮到他时，Abelard必须在网格上的以下位置放置一个瓷砖。在行结束后（对于游戏的实例n，游戏有n列），玩家必须在下一行，列放置一个瓷砖0. 如果没有玩家能够做出有效的移动或没有瓷砖，那么Abelard获胜。给定实例T =（n，{T0，...，Ts+1}），其中n是走廊的宽度，Ti是瓷砖类型，我们将构造一个公式πτ使得(i) 如果Eloise有一个获胜的策略，那么在T的某个博弈树的根上，τ τ是满意的（被看作是一个常规的DS3模型，对于一个大小为n的公式， 模型的大小将是a，其中a > 1）。(ii) 如果τ是满意的，那么Eloise在博弈T中有一个获胜策略。(iii) 可以在n和s的时间多项式中计算公式ττ。公式πτ描述了游戏，并陈述了Eloise获胜的必要和充分为了构造πτ，我们将使用以下命题字母：t 0，...，t s+1表示图块，其中t0为白色;p1，...， p n表示当前回合中必须放置的牌的位置;c i（t），0≤i≤n +1，n∈ {t 0，.，ts+1}以指示列i中先前放置的瓦片的类型t;w表示当前位置是Eloise的获胜位置对博弈进行建模的Petri网（η）的一般模式如图4所示，其中对于每一行r都有一个类似于R的转移，使得10δ（w，π）BBKIDIBBLXOBR误差F好图五.有故障其中s是由K个重复的“BB”和“OK”组成的名称序列，而“OK”是在此SPN运行后保持的某个属性。验证这个公式是否在模型M的世界w中成立（即某些过渡可能发生火灾），等价于计算某些基本程序发生火灾的概率大于零，这简化为引理4.8中的等式。为了验证是否可以并行处理两个资源，我们可以看到，在其中一些资源开始处理之后（即，如果一个token在B）的位置，Id将不在名称序列中，因此其他资源不能开始它们的进程，除非将token重新声明为Id的转换被触发。验证是否从世界w∈W中有可能某个资源开始其处理等价于计算如果Pr（M，wD r ， IB ， Idt2BB T|δ （ w ， Kt1IBIB ， Idt2BB ， OKt2llt3OK ， xxt3Id ，OBOBt1BBOKt1Error Errort1Ok））其中r=M（w）。使用引理4.8，它等价于验证，如果δ（Idt2B<$B）Bπb∈Π： f（ r，πb） π式中，k =Kt1IBkIB，Idt2BkIB，Okt2lklt3OK，xkxt3Id，OBkOBt1BBkOKt1误差误差t1Ok和πb是的一个基本跃迁7结论和进一步的工作这项工作扩展了Petri-PDL，一个动态逻辑的推理标记Petri网，一个新的动态逻辑定制的推理标记随机Petri网，不仅增加了它的表现力，但也提出了一个模块化和组合的方法概率模态逻辑。该系统的目的是成为一种替代模型性能评估。本文提出了一种程序为标记随机Petri网的PDL与以往的方法，将Petri网转化为动态逻辑，在我们我们提出了一种公理化逻辑，并证明了它的可靠性和完备性。最后，我们建立了它的SAT问题的可判定性、有限模型性质和EXPTime-完全性，并给出了我们方法的应用实例B. Lopes等人/理论计算机科学电子笔记305（2014）6783使用DS3，可以利用从UML图自动生成SPN的系统[19]，用于软件规范，以验证适当性。系统的行为也可以转化为CTMC。进一步的工作包括寻找有意义的案例研究，应用在具体的情况下，提出了一个自然演绎和解决系统的DS3和调查模型检查和自动定理证明DS3。引用[1] Mario Benevides，Edward Haeusler，and Bruno Lopes.Petri网的命题动态逻辑在Annals of the 6th Workshop on Logical and Semantic Frameworks，with Applications，2011.[2] P. Blackburn，M. de Rijke和Y.维尼玛模态逻辑计算机科学中的理论理论。剑桥大学出版社，2001年。[3] J. L. Coleman，W.亨德森和P.G. Taylor.随机Petri网的乘积型平衡分布和卷积算法。性能评价，26（3）：159[4] E. S. de Almeida和E. H.豪斯勒用LoRes逻辑语言证明普通Petri网的性质。Petri Net Newsletter，57：23[5] Giuseppe De Giacomo和Fabio Massacci。将演绎和模型检查结合到逆向PDL的表格和算法中。信息与计算，160：2000，1998。[6] 伊 沙 伊 河 费 尔 德 曼 一 个 可 判 定 的 命 题 概 率 动 态 逻 辑 。 在 Proceedings of the fifteenth annual ACMsymposium on Theory of computing，STOCACM，1983年。[7] 伊沙伊河费尔德曼一个具有显式概率的可判定命题动态逻辑。Information and Control，63（1-2）：11[8] 伊沙伊河费尔德曼和大卫·哈雷尔。一种概率动态逻辑Journal of Computer and System Sciences，28（2）：193[9] Michael J. Fischer和Richard E.拉德纳 常规程序的命题动态逻辑。 杂志计算机和系统科学，18：194 -211，1979。[10] R.戈德布拉特并行动作：具有独立模态的并发动态逻辑。Studia Logica，51：551[11] StefanGüoler和 MarkusLohre y.PropositionalDynamicLogics 的 无 限 状 态 模 型在 Zolt'anE'sik ， 编 辑 ，ComputerScien ceLogic，第4207卷，计算机科学笔记，第349-364页。Springer Berlin Heidelberg，2006.[12] P. J. 哈斯随机Petri网：建模，稳定性，模拟。Springer，2002年。[13] 大卫·哈雷尔，德克斯特·科曾，和杰西·蒂伦。动态逻辑计算机基础系列。麻省理工学院出版社，2000