单调扩展的Petri网参数验证问题的可判定性研究

理论计算机科学电子札记98（2004）35-55www.elsevier.com/locate/entcs具有非阻塞弧的Petri网的分析Jean-FranpronuncoisRaskin1，2 andLaurentVanBegin3，4Universit'eLibred eBruxellesBlvd du Triomphe，1050 Bruxelles，比利时摘要本文研究了一类扩展Petri网上五个问题的可判定性。 这类扩展Petri网的研究是由多个副本的进程，可以与一个部分非阻塞的renegal-vous通信的参数验证问题的动机。这种通信发生在多线程JAVA程序的抽象中。关键词：单调扩展的Petri网，可判定性/不可判定性。1介绍在参数验证中，我们希望一次验证整个系统族。例如，一些互斥协议被设计为适用于任何数量的（相同的）进程。对特定数量的工艺的验证并不令人满意。我们想要一个证明任何数量的这些过程。这个参数验证的问题是困难的，并且通常已被证明是不可判定的[2]。为了获得部分自动方法，几个抽象已被证明是有用的。 工作1 电子邮件地址：jraskin@ulb.ac.be2提交人得到联邦难民基金会赠款2.4530.02的部分资助3 电子邮件地址：lvbegin@ulb.ac.be4本发明由Walloon Region的“F i rs t E u rop e“gran t EP H 3310 3 00 R 001 2提供。1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2003.10.00536J. - F.拉斯金湖Van Begin / Electronic Notes in Theoretical Computer Science 98（2004）35-↓在本文中直接连接到这些抽象之一的上下文，所谓的计数抽象[12]。当考虑计数抽象时，（无限）Petri网及其扩展特别重要。在这种情况下，参数系统的过程被抽象的令牌，地方被用来计数的过程，cesses在每个局部状态的参数系统和过渡的数量被用来模拟的动态过程。Sistla等人[12]已经表明，Petri网非常适合抽象参数系统，其中，实时通信用于进程之间的同步。当底层系统使用更在本文中，我们考虑了一个非常简单的扩展的Petri网，能够建模参数系统，使用“部分非阻塞”renmin-vous同步除了经典（阻塞）renmin-vous同步。部分非阻塞同步是发送方不阻塞（与通常情况相反）而接收方阻塞（与通常情况相同）的非对称同步。为了说明部分非阻塞的renewal-vous的概念，请考虑图1。这个数字代表a↑a ↓L1L2L3L4Fig. 1. 部分非阻塞肾静脉的示例。两个过程的片段。在位置l1，第一个进程可以发出一个↑，一个在符号a上的返回-vous的命题，并移动到l2，即使第二个进程不存在，通过发出一个 .如果第二进程可以同步，那么它就可以同步。另一方面，第二个进程必须与第一个进程同步，才能发出↓，并从l3移动到l4，它不能单独移动。因此，发射a↑是非阻塞的，可以在没有接收部分a↓的情况下发生，而接收是阻塞的，只能发生在排放物存在的情况下。这就是为什么我们称这样的连接为“部分非阻塞连接”。在本文中，我们将定义一个简单的扩展的基本Petri网，能够模拟这种通信之间的进程，我们称之为扩展Petri网与非阻塞弧。对Petri网的这种简单扩展的研究是由作者以前的工作激发的，这些工作是关于Petri网在多线程程序中建模通信的扩展[7]。多线程JAVA程序使用notify和notifyAll等指令进行同步。指令notify可以由部分非阻塞的renown-vous来建模，并且指令notify可以由J. - F.拉斯金湖Van Begin / Electronic Notes in Theoretical Computer Science 98（2004）35-37--我≤ ≤ ≤notifyAll可以通过广播通信来建模。虽然转移网，能够模拟广播通信，已经从理论的角度进行了研究[9，5]，这不是Petri网的扩展建模部分非阻塞renewal-vous的情况。我们在这里研究五个重要问题的可判定性的背景下，扩展的Petri网与非阻塞弧。虽然这五个问题对于Petri网来说是可判定的本文的其余部分组织如下。 在第二部分，我们回顾一些基本的概念和符号。在第三节中，我们介绍了非阻塞弧扩展的Petri网和我们研究的五个问题。在第四节中，我们表明，两个问题仍然决定的扩展模型。在第五节中，我们建立了三个不可判定性其它问题.最后，最后一节得出了一些结论。2预赛多套。一个由n个元素的集合S构成的多重集合B是一个函数B：S→N，它给S的每个元素s分配s在多重集合中出现的次数B（s 为了表示S={s1，.，s n}，我们写{（s i，B（s i））|B（s i）> 0}。 例如，设S为{s1，s2，s3}，设B为B（s1）= 3，B（s2）= 0，B（s3）= 1，则B记为（s2，3），（s3，1）.等价地，B可以表示为n维向量，表示为vec（B），其定义如下：B（s1）B（s2）vec（B）=vec我...B（sn）好的拟序，好的结构化的转移系统。集合S的元素上的“良好拟序“是一个自反且传递的关系，使得对于任何无穷序列s1s2.. 其中si∈ S（i ≥ 1），存在l1且l2→LJ。单调系统在文献[ 11 ]中为这些系统中，几个一般的可判定性结果是已知的[1，11]。我们将在第4节中使用这些结果来推导我们扩展的Petri网模型上的两个问题的可判定性一个双计数器机器C，简称2CM，是一个元组C1，C2，L，Instr，其中：•c1，c2是两个计数器，它们取N中的值• L ={11，12，.，l u}是u个位置的有限非空集合;• Instr是用具有以下三种形式之一的指令来标记每个位置L的函数·l：cj：=cj+1;gotol;，其中j∈ {1， 2}且l增量，我们定义TypeInst（l）=incj;J∈L，这被称为J· l：cj：=cj− 1;gotol;，其中j∈ {1， 2}且l递减，我们定义TypeInst（l）=decj;∈L，这被称为aJJ JJJJ· l：如果cj= 0，则转到l，否则转到l;，其中j∈{1，2}且l，l这被称为零测试，我们定义TypeInst（l）=zerotestj。∈L，这些指令具有其通常的明显语义，特别是，decre- ment只能在计数器的值严格大于零的情况下进行。一个2CMc1，c2，L，Instr的配置是一个元组loc，v1，v2，其中loc∈L是程序计数器的值，v1和v2分别是一个自然数，分别给出计数器c1和c2的值。一个2CM矩阵c1，c2，L，Instr的计算γ要么是一个有限的配置序列loc1，v1，v2，loc2，v1，v2，.，n= r，v1，v2n，或configurations configurationsloc1，v1，v2，loc2，v1，v2，. ，loc r，v1，v2，. 这样：（i）“Initialization”: 计算从l1开始1 1并且两个计数器的值为零;（ii）使得1 ≤i≤|γ|我们得到了i+1，v12一期+1这是一种配置，通过应用指令Instr（loc i）从loc i，v1，v2获取。在Finite在这种情况下，r是计算γ的长度，我们定义final（γ）=loc r，v1，v2。如果γ是一个计算，则γi表示γ的第i种配置。 A配置如果存在有限个计算γ使得final（γ）= Vlloc，v1，v2，则Vlloc，v1，v2在2CM Vlc1，c2，L，Instr中可达.2CM的可达性问题定义如下：得双曲余切值.JJ. - F.拉斯金湖Van Begin / Electronic Notes in Theoretical Computer Science 98（2004）35-39联系我们Ir， iO，ipq⟨⟩c1，c2，L，Instr n和C的一个配置“C1，v1，v2"是”c1，v1，v2"从“c1，0，0 "可达的2CM的有界性问题定义如下：众所周知，这两个问题不能完全用算法来回答。定理2.1（引自[16]）2CM的可达性和有界性问题是不可判定的。3非阻塞弧扩展的Petri网在本节中，我们正式介绍了扩展Petri网的类，我们称之为非阻塞弧。定义3.1一个具有非阻塞弧N，PN + NBA的Petri网，由一对N = P，T定义，其中P ={p1，p2，.，pn}是n个位置的有限集合，并且T ={tr1，tr2，.，tr m}是m个转换的有限集合，其中每个tr i∈ T是元组I，O，A，其中I是P中的输入位置的多集合，O是P中的输出位置的多集合，并且A是转换的非阻塞部分是空集或具有p，q ∈ P\{r|（r，i）∈或（）和1，分别称为非阻塞部分的源和目标。一个PN+NBAN=<$P，T <$N的标记是一个函数m：P →N，它给每个位置p∈ P分配一个自然数m（p）。等价地，一个标记矩阵可以看作是自然数的一维向量。在接下来的比赛中，对于一个标记m和一个位置集S，我们记为m（S），其中p∈Sm（p）。图2显示了PN+NBA的示例。 圆圈代表地点，矩形表示过渡。从地点p到过渡tr的普通边缘由p在tr的输入多集合中的出现次数来标记，并且从过渡tr到地点p的普通边缘由p在tr的输出多集合中的出现次数来标记。从（到）一个地点p到（从）一个过渡tr的边缘的缺失意味着在tr的输入（输出）多集中没有p的出现。在下文中，当一个位置在一个给定的变迁的多集合中只出现一次时，我们将只使用没有标签的边。从一个地方到一个过渡和从这个过渡到一个地方的虚线边缘对表示过渡的非阻塞部分。地方的标记以通常的方式定义标记。转移tr=I，O，A在标记向量m（I）中是可触发的请注意，在决定转换是否可在标记m中触发时，不考虑非阻塞部分。给定一个标记m，40J. - F.拉斯金湖Van Begin / Electronic Notes in Theoretical Computer Science 98（2004）35-我−}N→∈ TLLT →（m）P TL∈∈tr=<$I，O，A如果在m中是可触发的，我们说m通过触发tr导致mJ，记为m→trmJ，其中mJ定义为：• 如果A={p，q}且m（p）≥1：mJ=m-vec（I）+vec（O）-vec（{（p，1）}）+vec（{（q，1）}），即输入位置按其编号中的出现次数，输出位置增加它们在O中的出现次数，并且一个标记从非阻塞部分的源位置移动到目标位置。• 否则：mJ=mvec（I）+vec（O）。在这种情况下，要么转移没有非阻塞部分，转移的结果与通常的Petri网情况一样，要么非阻塞部分p的源没有标记而非阻塞部分没有效应。一个PN + NBAN= N，P，T的计算η是一个标记序列，它交替着过渡η= m1tr1m2tr2. tr r−1m r其中m i是任何i∈{1，2，.，r}，tr j∈ T，对于任意j∈{1，2，.，r−1}，我们有m1→tr1 m2→tr2. →trr−1m r.这种计算的概念通常被扩展到无限情况。一系列的转变σ= tr1tr2. tr r在标记m1中是可触发的，如果存在标记m1m2. m r+1使得m1tr1m2tr2. tr r m r+1是一个计算。 我们注意到mσmJ从m中激发σ导致mJ。一个标记MJ是从N i中的一个标记m可达的，则存在N的一个变迁序列σ，使得m →σ MJ。 我们注意到Reach（N，m）是从N中的m可到达的标记的集合，即Reach（N，m）={mJ| <$σ∈ T<$：m→σMJ}。标记的PN + NBA是一个元组，、哪里和是一组位置和一组过渡，：tr是一个标记函数，它用来自有限个标签集合的标签（tr）标记每个转换tr计算的概念和以前一样。对于这些计算中的每一个，η = m1tr1m2tr2. mr trr.我们将标签L（η）= L（tr1）L（tr2）. L（tr n）. 对于PN+NBAN和标记m，我们定义L（N，m）={L（η）|η是N的无限计算，初始标记为-ing. 逻辑公式在这些序列上进行评估，标签 给定一组标签，逻辑LTL的公式由以下规则定义：φ：= λ| ¬φ|φ1∨ φ2| Ⓧ φ|Qφ|Qφ|φ1U φ2其中λ为我们只给出了Q和Q运算符的语义，因为它们是本文中唯一需要的。 对于Λ使得Λ = λ1. λ i λ i+1.. . ，我们记Λ i为su_x λ i λ i+1.从这个开始，索引i和Λ（i），对于Λ中的第i个元素。 给定Λ∈ <$ω和公式φ，我们定义了满意度关系，注意到|=，如下所示：J. - F.拉斯金湖Van Begin / Electronic Notes in Theoretical Computer Science 98（2004）35-41NNNNN• 如果φ = λ，则Λ |= φ i ∈ Λ（1）= λ;• 如果φ = Q，则Λ |= φ i i ≥ 1：Λ i|= 0;• 如果φ = Q，则Λ |= φ i i ≥ 1：Λ i|= 0。对于一组无限标号序列M和一个公式φ，我们有M| = φ如果对所有的Λ∈M，我们有Λ |= φ。p4p1p 3图二. 非阻塞弧Petri网图2的PN+NBA具有两个过渡。变迁t1是一个经典的Petri网变迁，而t2有一个非阻塞部分。让我们假设标记代表进程，地点代表进程的局部状态。在这种情况下，过渡t1模拟了一个通常的renewal-vous如果一个进程处于其本地状态p 1，另一个处于其本地状态p 3，则这两个在相同的上下文中，变迁t2模拟了一个如果p4中没有进程，则p2中的进程不必等待，并且可以移动到其本地状态p1在这种情况下，p2中的进程向p4中的进程提出了一个请求。如果至少有一个进程存在于p4中，则重新启动，否则p2中的进程不必等待并可以继续。问题PN + NBA的标记可达性问题是如下定义的问题：“给定PN + NBA，具有初始标记m和标记2019 - 05 - 22 00：00：00 00： 00，m）？"。 的标记可覆盖性问题PN + NBA问 题 的定义如下：“给定PN + NBA与初始标记m和标记MJ，是否存在属于Reach（N，m）的标记MJJ，并且使得MJPN+NBAN的有界性问题定义如下：PN+NBAN的位置有界性问题是如下定义的问题：1p21 1t2t111 142J. - F.拉斯金湖Van Begin / Electronic Notes in Theoretical Computer Science 98（2004）35-初始标记m和一个位置p，是否存在c∈N使得<$MJ∈Reach（N，m）我们有MJ（p）≤c？基于动作的LTL模型检测问题是一个定义如下的问题：“给定一个标记PN + NBA N，一个初始标记m和一个基于动作的LTL公式φ，L（N，m）|= φ hold？”众所周知，这五个问题在Petri网上是可判定的[13，14，10]。定理3.2标记可达性、标记可覆盖性、有界性、库所有界性和基于动作的LTL模型检验问题在Petri网上是可判定的。在接下来的部分中，我们将研究PN+NBA的这些问题的可判定性。4可判定性结果本文给出了PN+NBA分析的两个肯定的算法结果。它们是一类扩展Petri网的严格单调性的直接结果。命题4.1类PN + NBA是严格单调的。从命题4.1和[1，11]出发，我们推出了PN+NBA的可覆盖性问题和有界性问题的可判定性.推论4.2PN + NBA类的可覆盖性问题和有界性问题是可判定的。5不可判定性结果在上一节中，我们已经看到PN+NBA的可覆盖性问题和有界性问题是可判定的。在本节中，我们将证明所有其他Petri网可判定的问题在PN+NBA中变得不可判定。为了建立这些不可判定性结果，我们将证明PN+NBA能够部分模拟2CM的计算。这个部分模拟结果将允许我们以统一的方式将2CM的不可判定问题减少到PN+NBA的问题。J. - F.拉斯金湖Van Begin / Electronic Notes in Theoretical Computer Science 98（2004）35-43Li勒LiL'LiL'LiL'不···不我我1122JJJli：cj：=cj+1;gotol'li：cj：=cj−1;gotol'li：ifci= 0then gotol'else gotol''TTTI0/0我我cjKcjKcjTcj（a）（b）（c）图三. 通过PN+NBA转换模拟2CM的操作。5.1PN+NBA对2CM小工具。对于任何2CMC=l，c2，L={l1，l2，.，l u}，Instr.，我们构造了一个具有非阻塞弧NC=N P，T N的Petri网，称为模拟小部件，定义如下。位置集合P等于{c1，c2，l1，l2，.，lu，K，T}。 位置c1和c2将用于跟踪C的两个计数器的值，l1，l2，，l u称为控制位置将用于跟踪C的程序计数器，K称为容量位置，T称为垃圾。下面将描述K和T的使用。转移集T是最小的转移集，使得对于每个li∈L：•如果Instr（li）的形式为cj：=cj+1;gotolJ，则T包含转换其中，i={（li，1），（K，1）}，0={（cj，1），（1，1）}，并且dA=0。•如果Instr（li）的形式为cj：=cj− 1;gotol，则T包含转换其中I={（li，1），（cj，1）}，0={1，K}，并且A=N;• 如果Instr（li）的形式为ifcj= 0then gotolJelse gotolJJ，则包含两个转换tr=0和tr=0，定义为：我我·tr=0= l，0，A，其中I ={（l i，1）}，0 ={（lJ，1）}，并且A={lc j，T j}。/=0JJ·tri=l，0，A，其中hI={（li，1），（cj，1）}，0={（cj，1），（1，1）}，并且dA=l。图3（a）示出了通过将一个令牌从容量位置移动到cj来模拟cj的增量的转换。图3（b）示出了通过将一个令牌从cj移动到容量位置来模拟cj的递减的转换 图3（c）示出了当c j等于零（转变t=0）和当c j大于零时对c j进行零测试的模拟转变。我们注意到m k是P ={c1，c2，l1，l2，. ，l u，K，T}定义如下：m k（l1）= 1，对于任意l∈ {l2，l3，.，lu}，mk（l）= 0，mk（c1）= 0，mk（c2）= 0，mk（K）= k，以及mk（T）= 0。小部件的属性。设C=c1，c2，L，Instr为2CM，NC=P，T为与C相关的模拟宽度，如上所定义。 设γ= γloc1，v1，v2γloc2，v2，v2γ. 被C. 我们将γ与一系列的跃迁tr1tr2.联系起来。 的不44J. - F.拉斯金湖Van Begin / Electronic Notes in Theoretical Computer Science 98（2004）35-K不L1C1LuC2K我我（一）β2p2β3（b）第（1）款β1β3（c）第（1）款β4p2（d）其他事项见图4。 使用widget进行构建。NC，使得对于所有i∈ N，使得1 ≤ i≤ |γ|，我们有tr i= α（v_i，v_1，v_2）其中，α定义为：我我α（αloc，v1，v2α）=如果loc=lk且TypeInst（loc）零测试j如果loc = 1 k且TypeInst（loc）= zerotestj且v j= 0，则tr =0。如果l〇c=l且TypeInst（l〇c）=使t和v>0归零，则t t r i =0。kkjj对应于γ的跃迁序列用α（γ）表示。模拟小部件转换的函数α−1定义为：α−1（tri）=li如果α（trli，v1，v2<$）=tri，其中v1，v2∈N。α−1应用于一系列跃迁σ = tr1.可从m k（k≥ 1）中触发的小部件的tr n，返回C γ =1 2 1 2 1 2 1 2loc0，v0，v0 |loc n，vn，vn ||使得（i）loc0= l1，v0 = 0，v0 = 0以及（ii）对于所有1≤i≤n，或者TypeInstr（li−1）/=zerotestj，并且ip1β2β1β4C2locC1L1不Kp1p3β4v1+v2β5β1p2locC23βv2C1v1L1不Kp1β2βliK不C1LiL1C2J. - F.拉斯金湖Van Begin / Electronic Notes in Theoretical Computer Science 98（2004）35-45i−1=zerotesti，v1，v2是由i−1，v12i−1applying Instr（l i−1）.或者Inst（li−1）是得双曲余切值.46J. - F.拉斯金湖Van Begin / Electronic Notes in Theoretical Computer Science 98（2004）35-⟨⟩1N→122RR我我形式如果cj= 0则转到LJ否则转到lj，并且以下情况成立。• tri=tr=0，则loci=lJ，v1=v1且v2=v2选项卡页面上创建i i−1i i −1• tri=tri=0且loci=lJ J，v1=v1，v2=v2。i i−1i i −1我们现在通过下面的引理形式化小部件的重要属性。这些引理的证明是容易的，但繁琐，所以在附录中给出。引理5.1设γ = γloc1，v1，v2γloc2，v1，v2γ. locr，v1，v22CMC=C1，C2，L，I，I，使得对于任意i∈ {1，2，.，r}，v1+v2≤k.设NC为与C相关联的模拟小部件。序列从标记mk中可以激发跃迁α（γ）转换导致如下定义的标记MJ：MJ（l）= 1，对于l =locr，MJ（lJ）=0，对于任何lJ/ =locr，MJ（c1）=v1，MJ（c2）=v2，MJ（K）=k-v1-v2，且mJ（T）=0。R r r r证据 见附录。Q这个引理形式化了这样一个事实，即计数器之和不超过k的2CM的任何计算都可以通过其关联的小部件忠实地模拟，通过使用不将令牌放入T中的计算来标记mk。引理5.2设σ = tr1tr2. tr n是与2CMC = c1，c2，L，Instr. 如果mkσMJ和MJ（T）= 0，则α−1（σ）是C的计算，其中final（α−1（σ））= loc，v1，v2使得MJ（loc）= 1，v1= MJ（c1）和v2= MJ（c2）。证据 见附录。Q这第二个引理说，任何计算的小部件从其初始标记，不把令牌在T是一个模拟的计算，其相关的2CM。引理5.3令NC是与2CMC= 2CM相C1，C2，L，仪表板 对于任意的标记m，使得m ∈ Reach（NC，mk），我们有m（{c1，c2，K，T}）= k.证据 见附录。Q最后一个引理说，在小部件的任何可达标记中，位置集合{c1，c2，K，T}中的标记之和保持不变。J. - F.拉斯金湖Van Begin / Electronic Notes in Theoretical Computer Science 98（2004）35-47C5∈→N1122RRRR1234RRS12RJRJ5.2不可判定性证明我们现在有能力建立标记可达性的不可判定性，基于动作的LTL模型检查和位置有界性问题。定理5.4 PN + NBA的盯人可达性问题是不可判定的。证据设C=C1，C2，L，Instr为2CM，s=C1，V1，V2为的构 形 .让我们证明，我们可以把C中s的可达性问题归结为PN+NBA中两个标记之间的可达性问题。我们从与C相关联的模拟部件NC=P，T开始构造PN+NBANj=PJ，TJ。在模拟小部件中，我们添加了如图4（b）所示的地点和过渡。也就是说，P = P{p1，p2}，T=T <${β1，β2，β3，β4}，新的跃迁定义如下：β1=<$I，O，A<$，使得I={（p1，1）}，O={（K，1），（p1，1）}，并且A=<$;β2=<$I，O，A<$ ，使得I={（p1，1）}，O={（l1，1）}，并且A=<$;β3=β 4 = βI，O，A，使得I ={（loc，1）}，O ={（p2，1）}且A =β;β4=βI，O，A，使得I={（K，1），（p2，1）}，O={（p2，1）}且A=β。 设初始标记m为m（p1）= 1，且对所有p∈PJ\ {p1}，m（p）= 0.此外，我们考虑从配置s定义的标记ms，如下：ms（p1）= 0，ms（p2）= 1，对于任意l L，ms（l）= 0，ms（c1）=v1，ms（ c2）=v2，ms（K）= 0，以及ms（T）= 0。现在让我们证明（i）s在C i中可达（ii）m s在N j中从m可达。(i) →㈡. 如果s在C中可达，则存在计算γ=loc1，v1，v2 ，vl，v2，其中s = vl，vl，v2，. 让我们注意到k是c1+ c2沿γ的最大值。 让我们证明我们可以激发跃迁序列σ = β k β α（γ）β β k−v1−v2，并且m→σm。 通过发射βk β，我们将k个令牌放在容量位置K中，将一个令牌放在控制位置l1中。的在引理5.1之后，widget现在准备好通过触发转换序列α（γ）来忠实地模拟γ，因为K包含足够的令牌。为仿真如果是忠实的，则位置c1包含v1个令牌，位置c2包含v2个令牌。R r我们还知道，位置T不包含记号，因此根据引理5.3，位置K包含k-v1-v2个记号。 在我们可以触发β3之后，控制令牌是从窗口小部件的控制位置LOCR移动到位置P2。因此，k−v1 −v2β4RR 导致标记MS。(ii)（一）. 假设ms在J中可达，从m到σ的一系列转变。让我们证明σ必须具有以下形式：5在可达性的情况下，我们可以通过抑制容量位置K来简化小部件的构造。然而，为了保持证明的一致性，特别是为了能够在我们所有的证明中使用引理5.1，5.2和5.3，我们决定在这个证明中保留完整版本的48J. - F.拉斯金湖Van Begin / Electronic Notes in Theoretical Computer Science 98（2004）35-⟨ ⟩ ⟨⟩J1→m122RRRR1K12其中，σ0是微隙的转变。在m中，β1和β2是1 4只有可触发的转换。一旦β2被触发，位置l1被标记，小部件的σ0要将一个token放入p2中，必须触发转换β3在触发β3之后，β4是唯一可触发的跃迁。我们还需要证明α−1（σ0）是达到s的2CMC的计算。由于ms（T）不包含记号，根据引理5.2，我们知道模拟是忠实的，因此α−1（σ）导致C中的s。Q定理5.5基于动作的LTL模型检测问题对于标记PN + NBA是不可判定的。证据设C = c1，c2，L，Instr是一个2CM，s = loc，v1，v2是C的一个构形.让我们证明我们可以将C中s的可达性问题简化为PN+NBA的基于动作的LTL模型检测问题。我们从与C相关联的模拟部件NC=P，T开始构造PN+NBANj=PJ，TJ。在模拟小部件中，我们添加了如图4（c）所示的地点和过渡也就是说，PJ=P <${p1，p2，p3}，T=T <${β1，β2，β3，β4，β5}，新的跃迁定义如下：β1=<$I，O，A<$，使得I={（p1，1）}，O={（K，1），（p1，1）}，且A=<$;β2=I，O，A使得I={（p2，1）}，O={（p3，1）}，A={c2，T};β5= I，O，A使得I={（p3，1）}，O={（l1，1），（K，v1+v2）}，且A={kc1，Tk}。标号函数L是恒等函数，也就是说，对于任何tr∈ TJ，我们有L（tr）=tr。我们考虑初始标记m使得m（p1）= 1且对所有p ∈ PJ\{p1}，m（p）=0. 此 外 ，我们考虑由配置s定义的标记ms如下： ms（p1）= 0， ms（ p2 ） = 0 ， ms （ p3 ） = 0 ， ms （ loc ） =1 ， ms （ l ） =0f 或 an nyl=/loc∈L，ms（c1）=v1，ms（c2）=v2，ms（K）= 0，且ms（T）= 0. 现在我们证明（i）s在C i中可达（ii）L（NJ，m）|=<$QQβ3。㈠→㈡。如果s在C中可达，则存在计算γ=V1，V2，V1，V2，V2，V3，V4，V5，V6，V7，V8，V9，V9，V10 ，V11，V12，V12，V13，V14，V15，V16，V17，V18，V19，V19，v1，v2，其中s =loc r，v1，v2 我们记k为c1+ c2沿γ的最大值。我们现在构建从γ计算N J的σ，使得σ |= QQβ3。我们把标记延伸mk（k≥1）到PJ使得mk（{p1，p2，p3}）= 0. 转换的顺序α（γ）使得m→βkβ2mα（γ）→β3β4β5 m。通过发射βk β，我们将k个令牌放在容量位置K中，将一个令牌放在控制位置l1中，以到达标记mk。在引理5.1之后，小部件现在准备好通过触发转换序列α（γ）来忠实地模拟导致ms的γ，因为K包含足够的令牌。在触发β3之后，控制令牌从控件的控制位置loc移动到位置p2，v1令牌被移除从C1和V2中，令牌从C2中被移除。触发β4β5将控制令牌从p2移动到l1，经过p3，并将v1+v2放入K，导致mk。KSJ. - F.拉斯金湖Van Begin / Electronic Notes in Theoretical Computer Science 98（2004）35-491N→1≥≥----≥≥我们得到无限跃迁序列σ=βk β2（α（γ）β3β4β5）ω可以从m中找到，并且满足公式QQβ3，因此L（N，m）|=<$QQβ3。㈡㈠。让我们假设有一个标签序列与从标记m计算J有关，并满足公式QQβ3。让我们证明对应于这样一个计算的无穷跃迁序列σ必须是形式β<$β2σ0β3β4β5. . σnβ3β4β5。 . . 其中每个σ i（i≥ 0）是窗口小部件的转换序列。事实上，β1和β2是从m开始的唯一可触发的跃迁。一旦β2被触发，位置l1被标记，并且必须触发窗口小部件σ0在触发β 3之后，β 4和β 5是唯一可触发的转换，然后必须触发控件σ 1的转换序列，等等。假设s是不可达的，让我们推导出一个矛盾。假设我们有m1→σ1.→β3β4β5m2i−1→σim2i→β3β4β5 m2i+1→σi+1 ... 对于每个i≥1，可能有两种情况：1. m2i−1（c1）=m2i−1（c2）= 0。我们在这里考虑两种情况。• （1a）m2i（c1）=v1和m2i（c2）=v2。当我们假设s不可达时，我们有α−1（σi）不对应于C的计算，并且通过引理5.2，我们知道至少有一个token被添加到位置T。 根据引理5.3，从位置集合{c1，c2，K}中丢失了一个标记。因此我们可以得出结论：m2i+1（{c1，c2，K}）v1 且 m2i（ c2 ）v2 或m2i （c1 ）v1 和 m2i（c2）>v2。在这种情况下，在生成序列β3β4β5之后，至少有一个to- ken从位置c1或c2添加到T，因此通过引理5.3，m2i+1（{c1，c2，K}）v1 且 m2i（ c2 ）v2 或m2i （c1 ）v1 和 m2i（c2）>v2。在这种情况下，在生成序列β3β4β5之后，至少有一个to- ken从位置c1或c2添加到T，因此通过引理3，m2i+1（{c1，c2，K}）

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