理论计算机科学电子札记88（2004）21-37www.elsevier.com/locate/entcsA–maze–ingJoaquin Aguado和Michael Mendler1，2FakultüatfurürWirtschaftsinformatikundAngewandteIinformatik，UniversitüatBamberg，GermanyGeraldLüttgen3英国约克大学计算机科学系摘要本文表明，核心片段的Esterel对应的组合电路承认一个自然的博弈论的解释。从技术上讲，组合Esterel程序被映射到有限的新颖的保留字：同步语言，Esterel，构造语义学，因果循环，博弈论1介绍最初在描述集合论中发展起来的经典博弈论，最近已经成为程序设计语言中令人惊讶的通用数学工具[1]。博弈模型的力量在于它能够以自然和直观的方式处理组合复杂的情况，例如量化器的交替嵌套[8]。也许最近最突出的成功应用的例子是1电子邮件：joaquin. wiai.uni-bamberg.de。2电子邮件：michael. wiai.uni-bamberg.de。3 电子邮件：luettgen@cs.york.ac.uk。 由EPSRC资助的研究GR/M99637。1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2003.05.00622J. Aguado等/ Electronic Notes in Theoretical Computer Science 88（2004）21-37解决了函数式语言PCF的 这导致了新的方法，控制领域游戏是一个令人信服的隐喻，不仅在函数式编程中，而且在这是因为反应系统与其环境之间的相互作用与简单的双人迷宫游戏中玩家与其对手之间的移动有很强的相似性。然后，通过提供一个获胜策略来解决这个相互作用问题，而获胜策略又可以被理解为系统反应。在本文中，我们报告了一个新的应用，这个比喻的具体互动问题，出现在同步编程的同步假设下，即表征系统的反应在给定的环境下的存在和不存在使用Berry考虑一个密码可以有两种类型：可见的和秘密的。把代币放在任意一个房间里，开始的玩家，比如Jaakko，可以通过任意多个秘密走廊把代币从一个房间移动到下一个房间;然而，一旦Jaakko通过一个可见的走廊，他的回合就结束了。 莱昂说，控制权传给了对手，对手可能会以类似的方式继续从棋盘上代币的当前位置4如果令牌卡在地牢，即，没有走廊的房间，当前玩家输了，对手就赢了。因此，游戏的目标是将对手打入地牢。显然，游戏棋盘可以建模为有限有向图，如图1所示，其中节点是房间，实线表示可见的走廊，虚线表示秘密走廊。给定一个游戏板并为代币选择一个初始房间，这个房间现在可以根据开始玩家Jaakko是否（i）总是有可能赢（如果他玩得聪明），（ii）必须总是输（否）来无论他玩得多么聪明），或者（iii）最多能通过确保莱昂永远不能强迫他进入地牢来达到平局例如，使用图1所示的板Mex1并最初将令牌放置在房间t5，Jaakko可以通过可见的走廊将令牌移动到房间t6，从而将控制权移交给Leon。现在莱昂只能移动到地牢t0的令牌，再次通过[4]这些参与者是以逻辑学家Jaakko Hintikka和Leon Henkin的名字命名的，前者是逻辑语义游戏领域的先驱，后者是第一个引入博弈论解释的人量化器。J. Aguado等/ Electronic Notes in Theoretical Computer Science 88（2004）21-3723M1t2t1CBt3的t0一Ft6t5t4M2Gt7D的t9t8eFig. 1. 示例游戏板Mex.可见的走廊，这样控制权就回到了Jaakko身上，他立刻就输了。这意味着房间t5是一个失败的位置（对于首发球员Jaakko）。然而，如果代币最初被放置在房间t4中，则Jaakko有两种获胜策略。一方面，Jaakko可以通过可见的走廊将代币移动到房间t5，正如我们刚刚看到的那样，玩家Leon在两个回合后必然会输另一方面，在一项研究中，Jaakko可以使用秘密走廊将代币移动到房间a，并在同一回合中通过可见走廊进一步进入地牢t0据说Jaakko从t4房间有一个获胜的策略，t4被称为获胜的位置。然而，一场比赛也可能以平局结束。例如，假设令牌最初放置在房间t8中。然后Jaakko有几个选择，但其中一个让他掌握在莱昂手中。事实上，如果贾科将代币移到t6房间，莱昂就可以将代币放入地牢t0。观察到，如果代币被放置在t9中，情况类似于在房间t6中移动代币将导致输掉游戏的意义。现在，假设两个玩家都想赢，并且他们都知道将代币放在房间t6是最坏的选择，那么他们将一直通过图中的黑色阴影部分移动代币1，即，穿过由于在M2中，总是可以避开房间t6，游戏可以以这种方式无限地继续，导致平局，因此房间e，g，t8和t9被称为平局位置。24J. Aguado等/ Electronic Notes in Theoretical Computer Science 88（2004）21-37迷宫游戏和艾丝特瑞尔。本文的目的是表明，在内核片段的Esterel对应的组合电路写的程序可以很自然地直觉，即由组合程序P描述的反应瞬间信号的存在和不存在，是在系统（起始玩家）和其环境（对手）之间“协商”的。系统试图证明信号的存在和环境的不存在。因此，当且仅当与P相关联的迷宫M中的房间s是获胜（失败）位置时，信号s必须（不能）在P中发射。如果信号s的状态是未定义的，那么只有在那时，房间s才是一个平局位置。从技术上讲，M中的策略对应于P的必须一个简单的连接方法是读取每个可见（秘密）走廊as a 然后，我们得到了Esterel对必须和不能信号集的声明式计算[ 3 ]与游戏图中获胜和失败位置的归纳计算之间的确切相关性我们使用子迷宫M1来说明这种对应关系在我们图1的例子中。与M1相关联的程序P1是：（presentt3else emitt2end）（presentbthen emitt3end）（presentt6else emitt3end）当前t0else emitt6end）。我们沿着P1的声明性语义的定点计算进行推理，并从空环境开始，在空环境中没有已知的信号存在或不存在，因此必须0 =不能0 = 0。 因为没有发射是不受保护的，所以第一次迭代不会产生当前信号，即，must1= 0;但是因为b或t0没有emit语句，所以我们不能立即得到cannot1={b，t0}在游戏术语中，这对应于将M1中的房间b和t0识别为开始玩家立即输掉的位置。 事实上t6与通过可见走廊到达t0意味着开始的玩家现在具有赢得t6的策略，因为他或她可以移动到他或她的对手输的t0在计算P1的Esterel声明性语义时在 当 前 T0 中 ， 执 行 发 射 器 T6 结 束 ， 且 T6 变 为 存 在 。因 此 我 们 得 到must2={t6}，cannot2={b，t0}。 另外，我们知道presentbthen emitt3end语句在当前时刻没有执行。在游戏中，这相当于标记从t3到b的秘密走廊对于t3的任何获胜策略都是无用的。对于任何玩家来说，走到b是没有意义的，因为玩家保持他或她的回合，因此在b中输了。从t3移到t6也许还是有可能赢的。然而，根据刚刚获得的额外信息，即t6是一个获胜位置，我们得出结论，J. Aguado等/ Electronic Notes in Theoretical Computer Science 88（2004）21-3725T3实际上是一个失败位置。对于从t3到t6移动也没有帮助，因为对手会在t6获得转弯并获胜。在Esterel近似序列中，t3确实在第三次迭代步骤中进入cannot 集 ： cannot3={b ， t0 ， t3} 。 这 是 很 清 楚 的 ， 因 为 t6∈must2 和b∈cannot2，因此在P1中仅有的两个可以发出t3的语句都被切换为0。must设置不变，因此must3=must2={t6}。第四个迭代步骤将t2识别为从t3不能∈3的事实发出的。对于这种方式，执行语句presentt3elseemitt2end.用博弈的术语来说，t2房间显然是赢的位置，而t3房间是输的位置。因此，我们得到must4={t6，t2}和cannot4=cannot3={b，t0，t3}作为Esterel对P1的构造性分析的不动点综上所述，我们看到mustn+1（cannotn+1）是起始玩家在最多n步中可以赢得（必须输掉）的房间集合图1中的例子还说明了如何在博弈模型中反映我们已经看到上面的阴影Mex的区域M2仅包含绘制位置。 相关的Esterel Pro-语法P2可以写成八个陈述的平行组合如上所述，或者等效地以更紧凑的形式，P2：=presentgthen presentethen（presentgelse emiteend）presenteelse emitgend）endend，其中两个房间T8和T9不再被表示为信号，而是隐含在嵌套的present语句中。顺便说一句，我们将在下面看到，我们在博弈图中的中间状态ti是表达合取行为所必需的。对P2的必须为了证明e或g的发射是合理的，e和g都必须首先存在，以激活最外层的呈现陈述，这在因果上是不合理的。与此同时，它们必须缺席才能打开内部的emit语句，这在总体上是矛盾的。我们也不能从因果关系上证明e和g的缺失。例如，为了通过外部保护当前条件之一来停用内部发射，我们需要e和g之一不存在，这也是因果问题。缺少e和g还有第二种可能性，即内部的emit语句都被切换为0。然而，这需要两个信号都存在，这又是一个矛盾。总的来说，只有一个逻辑上连贯的解，即e和g都不存在，但这个解不是因果的。由于这是唯一逻辑上连贯的解决方案，Esterel[3]的逻辑行为语义26J. Aguado等/ Electronic Notes in Theoretical Computer Science 88（2004）21-37连贯的解决方案相当于对房间的0（输）和1（赢）标记的“推测性”分配，使得（i）如果经由可见走廊可访问的房间的后继房间之一被标记为0，或者如果经由秘密走廊连接的后继房间被标记为1，则房间被精确地标记为1;及（ii）如所有经由可见走廊连接的房间均标记为1，而所有经由秘密走廊连接的房间均标记为0，则该房间标记为0。在图1中，e=g= 0并且t8=t9= 1是M2的唯一逻辑相干标记。虽然这可能意味着e和g都在失去首发球员的位置，但很明显，这不能通过对手的任何有限策略来实现2迷宫与本节形式化了我们读者可以在[10，12]中找到一些关于经典博弈的背景材料。我们的设置与经典定义相比的唯一变化是，我们（i）允许博弈图中的两种类型的转换，即，可见和秘密过渡，以及（ii）允许绘制位置。后一个特征与自动机理论和连续集理论[ 12 ]中使用的经典游戏相反正式迷宫。迷宫本质上是有两种有向边的有限图，即可见边和秘密边。为了我们的目的，对于表示房间和迷宫项mx的变量的有限集合V，可以方便地将这些图形式化地表示为迷宫语言中的展开规则系统M：=（x<$mx）x∈V。迷宫条款的定义在一个过程代数的方式，这为我们提供了足够的结构来证明本文的主要结果。迷宫术语的语法由以下BNF给出m：：= x| 0 | μ m| τ.m| m + m。直观地说，0表示地下城，m（τ.m）表示具有通向房间m的可见（秘密）走廊的房间，并且m1+m2表示分别合并房间m1和m2的房间。在剩余部分中，我们让M代表所有迷宫项的对于任何给定迷宫M中的每个房间x，我们想确定它是否是获胜位置（对于起始玩家）。迷宫M的其中M是状态（或房间）的集合，{i，τ}是字母表，其中i编码可见动作，τ编码秘密动作，并且J. Aguado等/ Electronic Notes in Theoretical Computer Science 88（2004）21-3727−→M× {i，τ} × M是表示房间之间的有效移动（或校正）的转移关系。 过渡关系由以下规则定义，其中γ在{i，τ}上变化：−−mγmJmγmJmγmJ1−→12−→2−→x m。γγ.mγJγJγJ−→mm1+m2−→m1m1+m2−→m2x−→m本质上，这个标记的转移系统反映了SEC的博弈图。1，地下城是没有输出转换的陷阱。 在下文中，我们把m−→写成<$mJ<$γ。mγmJ. 请注意，运算符“。”, “+”, and对应于例2.1让我们指定图1中的迷宫相对于程序V={a，b，c，d，e，f，g}。 其他房间{t0，t1，.，t9}被称为未命名的房间，并隐式地表示为相应的展开规则系统M ex：=（x <$mx）x ∈V中的子项 用一个。0，b= 0，c=1。（i.a + i. （τ.b + τ. 0）），d. （τ.a+好吧0）+1。（注：0 + 1.e），e=1. （i.e + i.g + τ.g + τ. 0），f_i. （τ.a+ τ. 0），g. （i.g + i.e + τ.e + τ. 0）。观察到，对于任何x = m x，将操作规则应用于m x会导致图形从房间x开始的部分。具体地，对于f ∈ m f和mf= 1。（τ.a + τ. 0），项中的第一个i对应于连接f和未命名房间的可见走廊t4= τ.a + τ..。0.从t4开始，要么是一条秘密走廊τ可以通往a房间，要么是一条三人路径可以沿着可见的走廊到达地牢t0。玩迷宫游戏我们现在将注意力转向我们的两人迷宫游戏的博弈论语义。为了方便起见，我们将简单地将参与者命名为A和B。我们首先定义地牢、路径和转弯的概念。 第一，m室是一个地牢，如果m−→。其次，通过迷宫M的路径π是一个序列，γi（mi−→mi+1）0≤i k，其中k∈N<${ω}被称为长度|π|的π。 我们说π在k ω的情况下是有限的;否则，π是无限的。一条路π是最大的，如果它是无限的，或者如果它是有限的，而m|π|−→。我们γinπ的长度为j ∈ N的π j。最后，i−→i+10≤i j给定一个有限（a的前缀）路径π，假设参与人A总是从0开始，在游戏中，我们可以确定玩家的回合（π），它是在最后的回合。28J. Aguado等/ Electronic Notes in Theoretical Computer Science 88（2004）21-37476室m|π|如下所示，其中A：= B且B：= A：⎧转（πJ）if|π|>0和dπ=πJ·−τ→⎨turn（π）：=turn（πJ）if|π|>0且dπ=πJ·−→i⎪否则，即、|π|=0。迷宫游戏是由玩家的策略决定的一个策略是一个（偏）函数α：M~{i，τ}× M，使得对于所有的m∈ M，如果α（m）=α1（m）（α1（m），α2（m））定义为m−→α2（m）。注意参与人的策略不依赖于对手 给定策略A和B分别为α和β，策略M（α，β，m）γi在迷宫M中，从房间m开始，玩家A是最大路径π=（mi-→mi+1）0≤i k，使得m0=m，mi+1=α2（mi），γi=α1（mi），如果如果turn（πi）=B，则mi+1=β2（mi），γi=β1（mi）。迷宫M=（x<$mx）x∈V的操作语义考虑了对于每个房间x，参与者A或B是否有获胜策略，或者两者都没有。直觉上，A（B）有一个获胜的策略，如果他或她总是能够把玩家B（A）推进地牢，不管B（A）使用哪种策略，并且总是假设玩家A开始游戏。形式上，如果<$α <$β，参与人A对M中的房间x有一个获胜策略。|ω和B =|< ω and B =turn（playM（α，β，x））. 对偶地，参与人B对M中的房间x有获胜策略如果αβ≠α。|ω和A = turn（play M（α，β，x））。|< ω and A = turn (playM(α, β, x)).如果选择的起始玩家A对房间x有获胜策略，则简单地调用x一个胜利的位置。如果参与人B有一个获胜的策略，那么x是一个失败的位置。 如果两个玩家都能避免地下城，如果双方都没有赢，比赛以平局结束。因此，既不是赢的位置也不是输的位置被称为平局位置。例2.2再次考虑图1中的迷宫Mex。 假设参与者A的策略α是这样选择的，即只要有可能，A就把代币从V通过一条秘密走廊移动到一个指定的房间。 否则，他会选择一个房间ti和最小的i。参与人B的策略β是B在任何V中更喜欢i最小的ti型房间。然而，总的来说，B更喜欢秘密走廊，只要有一个。例如，α（d）=t4，α（t6）=t0，β（t4）=a，β（a）=t0，β（t7）=t6. 因此，游戏Mex（α，β，d）是路径d−→ιt −→τa−→ιt，长时间A丢失。我不知道，如果你是A0在第一轮选择t7，B会选择移动到t6，从A移动到地牢t0玩家B输了。 在这种情况wo uldbed−→ιt−→ιt−→ιt。最好的广场B可以在新的0A的策略是设置β（t7）=e，否则保持他对⎪J. Aguado等/ Electronic Notes in Theoretical Computer Science 88（2004）21-3729789秘密走廊在这种情况下，游戏相当于沿着无限长的平局路径d−→ιt−→ιe−→ιt−τ→g−→ιt−→τe−→ιt· · ·。8外延表征。迷宫在输赢位置方面的语义可以也可以从外延上来理解。指称方法依赖于两个谓词win和lose，它们将迷宫项m和增强项X作为参数。根据Esterel的符号约定，我们将环境X定义为一组有符号变量x+和x-，这意味着加标签（减标签）的变量表示已知为赢（输）场。因为一个房间不能同时是赢的和输的位置，所以对于任何x，一个环境不能同时包含x+和x-。谓词win（lose）现在对m和X成立，如果m对应于获胜（失去）位置相对于X。形式上，这些谓词被定义为遵守以下规则的最小谓词：lose（0，X）win（x，X）ifx+∈Xlose（x，X）ifx−∈Xwin（m，X） 如果lose（m，X）lose（m，X） 如果win（m，X）win（τ.m，X） 如果win（m，X）lose（τ.m，X）如果lose（m，X）win（m1+ m2，X）如果win（m1，X） 或 win（m2，X）lose（m1+ m2，X）if lose（m1，X）and lose（m2，X）.直觉告诉我们，0号地下城总是一个失败的位置。如果m1或m2中至少有一个是，则m1+m2房间是获胜位置，因为m1+m2基本上给领先的玩家自由选择是继续m1还是m2。对偶地说，如果m1和m2都是，m1+m2房间m只能由可见的走廊i到m离开，从而将控制权交给对手。 因此，m是领先玩家的赢（输）位置 如果m是对手的输（赢）位置。穿越秘密走廊不会改变玩家因此，通过适当选择房间x的可见和秘密走廊，我们可以使x的获胜（失败）谓词成为直接后继房间的否定和非否定获胜条件的任意析取（合取）组合。这对正规形式表示很有用我们现在定义一个关于环境的函数：maz e（M）（X）：=wi n（M，X）+los e（M，X）−.这里，win（M，X）表示{x∈V|win（m x，X），x<$m xin M} and lose（M，X）for {x∈V|lose（m x，X），x<$m xin M}.此外，对于变量的任何子集V<$V，V+表示集合{x+|x ∈ V}和V −的集合{x−|x ∈V}。很容易证明函数maze（M）是单调的。因此，迷宫（M）的最小不动点μmaze（M）存在，它被认为是30J. Aguado等/ Electronic Notes in Theoretical Computer Science 88（2004）21-37迷宫M 此外，因为我们的变量宇宙是有限的，我可以迭代地计算μ maze（M）=i∈Nmaze（M）（n）。例2.3让我们求出图1中迷宫Mex的获胜、失败和平局位置的集合。最初，保持的谓词是lose（0，n）和wi n（i）。0，0）。从那以后。0和b∈0，则maz e（Mex）（x）={a+，b−}。在这一点上，f∈los e（Mex，{a+，b-}）sincefi。（τ. a+.. ι。0）和wi n（τ. a+.. ι。0，{a+，b-}），后者从wi n（τ.a，{a+，b-}）。Nextwederivec∈wi n（Mex，{a+，b−}）fromci. （i. a+1.（τ. b+i. i. 0））和函数thatn （a，{a+，b-}）anddlos e （b，{a+，b-}）bothhold.Th是showsmaz e（Mex）2（M）={a+，c+，b-， f-}. 另一个迭代将其确定为最小值dpoint，即，μmaz e（Mex）={a+，c+，b−， f−}.定理2.4（重合）设M是一个迷宫，x是一个变量。• x是M中的获胜位置当且仅当x+∈ µ maze（M）。• x是M中的失败位置当且仅当x−∈ µ maze（M）。这个定理的证明可以改编自有限对称和无记忆游戏的结果唯一的一个小问题是，我们的设置允许游戏图形中的两种类型的转换，即可见和秘密。3Esterel反应和迷宫本节首先正式介绍了我们所关注的Esterel的组合片段，并回顾了Berry在[3]中定义的其构造性行为然后，我们给出了一个翻译的组合Esterel程序P到迷宫M的财产，赢得（失去）的位置在M中完全对应的信号，必须（不能）在P中发出。Esterel反应Esterel片段的语法，它指定了单个反应，并将在其余部分中使用，由以下BNF定义，其中s代表来自某个（有限）宇宙S的信号名。P：：=0无| ! s发射s| s+?（P）表示nP| s−?（P）presentselseP| PP|P||PEsterel的更一般的选择语句“present s then P1 else P2“可以被recover ere d in our s y n t a x by thet er m s +？（P-1）|s−？（临2）[6]。在本文中，J. Aguado等/ Electronic Notes in Theoretical Computer Science 88（2004）21-3731省略顺序复合和局部信号声明的组合运算符，尽管我们在第2节中讨论过。4种不同的方式包括后者。这种省略的后果是行为语义学定义完整语言所需的完成代码我们还去除输入信号i∈I ={i1，.，i n} s.这是可能的，因为P在I下的行为等价于P的行为|！i j1| ··· |！i jm，其中索引j1，.，j m∈ {1，.，n}恰好是信号i，j，k存在于I [6]中的那些。最后，我们进一步假设信号的有限集合S包括人们希望推理的组合Esterel程序的所有信号。这种限制仅仅是技术上的方便，并且可以通过为每个程序维护有限的相关信号集来取消，即，“Berry 每个信号s∈S都可以不存在，即. 具有状态S+，或不能不存在，即，具有状态s-，或具有未知状态。 对于任何集合S ∈ S，我们让S+代表{s+|s∈S}和S−for{s−|s∈S}。信号状态的一致集合ES+S −，使得/s。 s+∈ E和s−∈ E称为事件，E表示所有事件的集合。给定一个组合Esterel程序P和事件E，我们定义了必须和不能在P中发出的那些信号的集合必须（P，E）和不能（P，E），分别相对于E中的信号状态的知识[3]：jmust（P，E） ifs+∈Emust（0，E）：=must（s+？（P），E）：=必须（！s，E）：={s}必须（s−？（P），E）：=我不知道必须（P，E）如果s−∈E否则，必须（P1 |P2，E） ：= must（P1，E）=must（P2，E）cannot（0，E）：=Scannot（s+？（P），E）：=S如果s−∈E不能（！s，E）：=S\{s}cannot（s−？（P），E）：=jcannot（P，E） 我的天S如果s+∈E不能（P，E）否则不能（P1|P2，E）：= cannot（P1，E）cannot（P2，E）请注意，对于子集包含，两个函数在E中必须且不能是单调的。由于（E，E）是有限esterel（P）（E）：=must（P，E）+lancannot（P，E）−有一个最小不动点μesterel（P）=定义了P的行为语义。i∈N esterel（P）i（Ⅱ）. 这个最小固定点在[3]中，缺席信号的构造是基于不能集的补集，称为可以集。我们的等价公式引出了一个重要的结构不变式。首先，cannot（P，E）是must（P，E）的逻辑对偶，通过将替换为，将替换为S，将{s}替换为S \ {s}而得到。其次，must和cannot是互斥的：must（P，E）cannot（P，E）=，因为J32J. Aguado等/ Electronic Notes in Theoretical Computer Science 88（2004）21-37任何事件E.然而，一般来说，must（P，E）cannot（P，E）/=S，因此must和cannot不一定是补语。这类似于两人游戏中的情况must（P，E）和cannot（P，E）中的元素都不表示绘制位置。将组合Esterel程序表示为迷宫。对于每一个Esterel程序P，我们关联一个迷宫P：=（aPa）a∈S，它精确地反映了P的语义。在这里，信号扮演着代表不同房间的变量的角色，而迷宫术语“迷宫P”描述了从房间a开始可以玩的符合P的游戏。在形式上，P的结构定义如下：⟨⟨0⟩⟩a:= 0.I. 0 ifs =a你说什么？（P）a：=i. （i. s+1。（Pa）你是谁？（P）a：=i. （τ.s+1）。（Pa）你好！sa：=0否则电子邮件*|P2a：=P1a+P2a。直觉，程序0不能发出任何信号，必须对应于一个地牢，其中领先的球员失去了。在程序中强制发射信号a，而不存在信号s/=a！a导致a房间的领先玩家立即成功。0-或对手不可避免的损失-并失去了在其他任何一个房间的B-0。一个程序S+？（P）如果在房间a中，领先的玩家既赢了，在对应于P的迷宫中，s和房间a的策略。我们把这种合击编码成迷宫，首先把控制权交给对手，对手反过来又自由决定领先的玩家是必须继续他或她的s游戏还是继续他或她的P2P游戏。类似地，一个程序s-？如果在房间a中，对手有一个获胜的策略，并且领先的玩家有一个获胜的策略，那么被信号s消极保护的（P）必须发出a。最后，信号a在平行合成中的发射可以发生在任一分量中，并且因此由领先玩家的自由选择来编码。在迷宫图方面，平行构图对应于形成房间走廊的智能合并（覆盖） 作为一个例子，E圆程序Pex=！一|e+？（！（d）|a−？（！D|！f）的|a+？（b−？（！（c））|g+？（e+？（g−？（！（e）|e−？（！g）（当s不发生在Q中，以及m+0 =m，对于所有m，m=m）生成了例2.1的展开规则，从而生成了图2.1中的迷宫1.一、命题3.1设P是组合Esterel规划，E是事件。(i) must（P，E）={a ∈ S |win（P，E）}J. Aguado等/ Electronic Notes in Theoretical Computer Science 88（2004）21-3733P4SP3S均p0S(ii) cannot（P，E）={a ∈ S |lose（Pa，E）}这个命题陈述了组合Esterel程序中必须和不能分析之间的一对一关系，它的证明可以通过归纳Esterel程序的结构来进行。作为该命题的结果，函数esterel（P）和maze（m_nP_n）重合.这直接证明了本文的以下主要定理。定理3.2（博弈论特征）对于每个组合Esterel程序P，我们有μesterel（P）= μ maze（μ esterel P）。我们通过重温贝里书中的几个病理学例子来结束这一节对于每一个组合Esterel程序Pi（索引如Berry的书中所述除了P6之外，其他程序都在图2中以迷宫的形式表示.图二. “Pathological” Esterel• P4：=s+？（！（s）：根据我们的定义，我们得到M4：=P4=（sP4s）和m4，s：=P4s= i。（1.s +1. s）0）。因此，对于任何事件E∈ E：win（m4，s，E）赢输（ι.s +.. 0、E）Lose（ι.s，E）和lose（.. 0、E）赢（s，E）输（0，E）⇐⇒win(s, E)and trues+∈ E.类似地，lose（m4，s，E）s−∈E。 这意味着迷宫（M4）（M 4）=根据函数maze（M4）的定义，其中μ maze（M4）= μ。• P3：=s−？（！s）：这里我们有M3：=P3=（sP3s）和m3，s：=P3（τ.s + τ. 0）。然后，对于任何事件E∈ E，我们可以导出：win（m3，s，E）赢输（τ.s + τ. 0、E）⇐⇒lose (τ.s, E) and lose (ι.ι. 0、E）⇐⇒lose(s, E)and trues− ∈ E。此外，失去（m3，s，E）s+∈E.与M4一样，这意味着maze（M3）（m）=m，因此μ maze（M3）= m。34J. Aguado等/ Electronic Notes in Theoretical Computer Science 88（2004）21-37• P0：=s+？（！个）|s−？（！s） =P4|P3：因此， M0：=P0=（sP0s）anddm0，s：=P0s=P4s+P3s根据·s的定义。 根据P4和P3的计算，我们很容易得出结论：win（m0，s，E）赢得win（m4，s，E）或win（m3，s，E）s+∈E或 s− ∈E（m0，s，E）.很容易看出，这又产生了μ maze（M0）= μ。• P6：=s+？（！第1条）|s+？（！s0）：这是一个国际性的程序，它给了大众0 1M6：=P6=（s0P6s0，s1P6s1），对于m6，s0：=P6s0=τ。I. （i. s0+I. 0）+τ。I. （i. s1+i. i。0）和m6，s1：=τ. I. （i. s0+i. i。0）+τ。I. （i.s1+1。0）。然后可以很容易地推断，对于i∈ {1， 2}，win（m6，s，E）<$s+∈Ei1−i并失去（m6，s，E）s−∈E. 同样，这意味着μ maze（M6）= μ。i1−i在上面所有的例子中，相关的房间s，或者在M6的情况下的s0和s1，对于起始玩家来说既不是赢的位置也不是输的位置，而是平局位置。根据Thm。3.2，所有信号状态都是不确定的，我们的示例程序将被当前的Esterel编译器拒绝[4]。的因此，游戏隐喻对建构性和非建构性给出了一个自然的解释。4本地信号声明我们主要开发的最后一部分表明，游戏语义也可以支持本地信号声明，这是Esterel [3]的另一个内核操作信号声明P\s引入了仅可用于节目P内的广播的局部定义的信号s 例如，考虑程序（P\s）|Q当P：=s+？（！a）、|！s和Q：=s+？（！（b）。InQ，signals指的是与P\s内部使用的化身不同的化身，其作用域为受本地信号声明限制。因此，P\s中s的内部发射将触发P中信号a的发射，但不会触发Q中信号b的发射。从迷宫的角度解释本地信号声明的最简单方法是将slogP中的信号s重命名为新的信号名sJ，并确保sJ永远不会在slogP\slogP之外使用。虽然这种“命名分离”技术对于编译器来说是一种简单的解决方案，但还有一种代数上更令人满意的方法。直觉上，迷宫P\ s的解与求解表征迷宫P \s关于信号s的递归展开相同。如果sms是定义s的展开规则，则s的最小定点这个递归术语表示从房间s开始的博弈，然后在任何地方使用或替换s。J. Aguado等/ Electronic Notes in Theoretical Computer Science 88（2004）21-3735在所有其他房间的展开图中，均参照了P.P.P.的定义。因此，在本发明中，S被淘汰了。在我们的示例中，系统一个人。（1.s +1. s）0）+0bm。（1.s +1. 0）+0sm。（1.s +1. 0）+1。0、我们从其中得到迷宫方程，通过代入固定点µs，得到ΔP\ s的ΔP \s。（i. （1.s+1. 0）+1。0）对于其他扩展中对s的每个引用。s的展开被一个人。（i. （µs. （i. （1.s +1. 0）+1。0））+1.00。0）+ 0s0b. （i. （µs. （i. （1.s +1. 0）+1。0））+1。0）+ 0。在新的展开规则系统中，原始信号s的行为被完全封装，因此任何扩展都只能引用指定的房间a和b。留在迷宫中的信号名现在指的是一个新的信号，默认情况下没有发出，因此由地牢表示。显然，这个想法的精确技术形式化需要在我们的迷宫术语语言中添加请注意，通过固定点运算符处理局部信号声明 需 要 对 s + ？（P）ands−？（Q）thanthegiven one above.这一观点已经由Berry在[3]中提出。考虑，例如， a positi vegguardc++？（P\s），其中，取决于获胜信号c，这意味着在P\s迷宫中的任何房间都只能在c也可以赢得的额外条件下才能赢得。这适用于P\s内的所有房间，甚至适用于为了给对手一个机会，迫使首发球员在任何时候进入房间c，我们可以通过一个辅助环在P\s内部中断一个ch转换PJ\s-→IPJ\对手可以选择挑战开始的玩家进入房间C，或者一种与PJj 对于所有的，我们可以通过下式将PJ\s−→ιPJJ\sPJ\s−→ιι。c+τ。（PJJ\s），这可以通过适当地修改迷宫术语的运算规则，特别是现在陈述的规则。5结论和今后的工作本文提出了一种组合Esterel程序的博弈论语义，即，Esterel的核片段对应的组合电路。我们的方法将组合程序转换为有限的我们的研究结果补充了现有的行为，操作，特别是，他们提供了一个新颖的教学视角，让学生和工程师36J. Aguado等/ Electronic Notes in Theoretical Computer Science 88（2004）21-37通过强调更多的直觉（游戏图）和更少的数学（固定点），这种复杂的建设性语义。值得指出的是，我们的关于未来的工作，我们首先希望将我们的工作扩展到更大的Esterel片段，特别是那些涉及Esterel的暂停，等待和循环结构的片段这将允许对反应序列而不是单个反应进行推理，并且需要丰富我们的博弈图中状态所持有的信息内容。还应该研究我们的游戏语义如何与最先进的Esterel编译器中实现的操作语义相关。其次，我们希望研究我们的方法是否适合于严格的代数处理。虽然我们提出了迷宫在一个过程代数的方式都在风格的基于术语的语法和基于转换系统的语义，相关的代数理论尚未得到充分的发展。迷宫的代数语义可以基于行为等价的概念，例如互模拟。 这将为我们的游戏提供一个组合语义，并允许最小化迷宫。请注意，本文中提出的从组合Esterel程序到迷宫的转换不应用任何优化。第三，我们计划对我们的游戏语义进行逻辑解释，类似于线性逻辑中AJM作为这个计划的一部分，我们的术语语言之间的引用[1] S. 艾布拉姆斯基编程语言语义学中的游戏。第11届阿姆斯特丹学术讨论会，第1-5页。阿姆斯特丹大学，1997年。[2] P. Baillot，V. Danos，T. Ehrhard和L.雷尼尔信不信由你，AJM在LICSIEEE Comp.Soc.Press，1997.[3] G.贝瑞纯Esterel的构造性语义。CMA，Ecole des Mines，INRIA，1999年。草案版本3.0。[4] 艾丝泰尔科技 艾丝特瑞尔工作室。 www.esterel-technologies.com，2003年。[5] M. Hyland和L.昂关于PCF的完全抽象：I，II和III。告知。的Comput。，163（2）：285[6] G. LuttgenandM.
我的内容管理
展开
