混合PDL的表格优化决策过程

可在www.sciencedirect.com在线获取理论计算机科学电子笔记278（2011）99-113www.elsevier.com/locate/entcs混合PDL马克·卡明斯基·格特·斯莫尔卡萨尔州大学Saarbruécken，Germany摘要我们提出了第一个基于表格的决策过程与名词的PDL。 该程序基于一个无前缀的子句表系统，该系统被设计为优雅地降低推理机的基础。子句系统将推理分解为规则推理、命题推理和模态推理。这就产生了一个模块化的决策过程，并在透明的正确性证明中付出代价。保留字：混合逻辑，动态逻辑，表系统，决策过程1引言PDL（Propositional Dynamic Logic）[6，13，9]是一种表达模态逻辑，用于程序推理。它扩展了基本的模态逻辑与表达式称为程序。程序描述了状态与状态之间的关系，并用来表示模态.程序是由熟悉正则表达式的运算符组成的。此外，它们可以使用公式来表达条件语句和while循环。Fischer和Ladner[6]使用过滤参数展示了PDL的可判定性。他们还证明了PDL的满意度问题是EXPTIME困难的。Pratt [17]表明，PDL的满足性是在EXPTIME中使用一个带字符和字符集的可扩展的方法。Go'eandWidmannn[7，8]解决了普拉特式决策程序的有效实施。我们考虑用名词扩展的PDL [14，15]，我们称之为混合PDL或HPDL的逻辑。Nominal是原子公式，对一个状态完全成立。名词使PDL具有相等性，并且是混合逻辑的特征[2]。HPDL的满意度问题在EXPTIME [15，18]中。我们感兴趣的是一个HPDL的Tableau系统，可以作为优雅地降低决策程序的基础。我们发现不可能将PDL [17，5，1，7]的现有tableau方法扩展到名词。困难在于正确性证明。对于Pratt类方法[17，7]，问题源于全局与或图表示与标称1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.10.009100M. Kaminski，G.Smolka/Electronic Notes in Theoretical Computer Science 278（2011）99我传播（参见[10]中的注释5.6以获得讨论和示例;[19]中也指出了该问题）。这些困难使我们发展出一种新的模态逻辑表法。新方法基于无前缀的从句形式。在以前的论文[10]中，我们使用该方法给出了HPDL的子逻辑的基于表的决策过程，该子逻辑将程序限制为形式a和a+，其中a是原始动作。在本文中，我们将子句方法扩展到全HPDL，并获得了第一个基于表格的HPDL决策过程。该方法将推理分解为规则推理、命题推理和模态推理。在每一级，我们实现了推理与tableau方法。名词是在情态层次上处理的。根据我们的方法，是很简单的。我们的决策过程的模块化结构支付透明的正确性证明。每个级别都需要优化。特别是常规水平，需要进一步调查。它可能受益于将正则表达式转换为确定性自动机的有效方法。与以前的方法相比，我们不依赖于Fischer-Ladner闭包。相反，我们使用可以在常规水平上获得的有限个常规DNF的概念。根据Baader [3]和De Giacomo和Massacci [5]，我们不允许坏循环，从而避免了Pratt方法[ 17 ]的后验可能性检查本文的结构如下。首先，我们定义了HPDL，并概述了子句表方法的例子。然后，我们地址，一个接一个，定期，命题和模态推理。最后，我们证明了决策过程的正确性2辆混合动力PDL我们定义了HPDL的语法和语义我们假设有三种名字给出：• nominals（元变量 x， y， z;表示状态）• 谓词（元变量p， q， r;表示状态集）• 动作（元变量a，b，c;表示状态之间的关系）。HPDL的解释是通常的转换系统，其中状态用谓词标记，边用动作标记形式上，解释I是由以下组件组成的元组：• 非空集|我|国家。• 一个状态Ix∈|我|对于每个标称x。• A set Ip|我|对于每个谓词p。• Areelation→apuzzle|我|×|我|为您提供最佳使用体验，出于技术、分析及推广目的，公式（元变量s，t，u）和程序（α，β，γ）定义如下：S ：：= X|p|s|ss|⟨α⟩sM. Kaminski，G.Smolka/Electronic Notes in Theoretical Computer Science 278（2011）99101我我α：：= a|S|1 |α+α| αα|α∗语法应该是包容性的，也就是说，每一个名词和每一个谓词都是一个公式，每一个动作和每一个公式都是一个程序。给定一个解释，公式表示状态集合，程序表示状态之间的关系我们用字母X、Y、Z表示状态。 语义关系I，X |= sndX−α→这是根据多个变量的结构确定的，项目：I，X| = x X = IxI，X|= p X∈ IpI，X| =<$s不是I，X| = sI，X| = st⇐⇒I，X| = s和I，X| = tI， X|=αs⇐⇒X−α→IYandI， Y|=sX−a→IYX→aIYX−→sIYX=Y和I，X| = sX−1→ IYX=YXα+βαβ−→ IYX−→IY或X−→IYXαβαβ−→ IYX−→ IZ和Z−→ IYα∗α∗X−→IYX −→IY−α→不确定的是−α→的可靠性xivetransiv ec lose给定一组公式A，我们写I，X| = A如果I，X| = s对于所有公式s∈A。 一个解释I满足一个公式s或一组公式A（或者是其模型），如果存在一个状态X∈|我|使得I，X| = s或分别为I、X| = A. 一个公式s（一个集合A）是可满足的，如果s（A）有一个模型。如果s=<$t，则公式s的补集s是t，否则是<$s注意如果s不是双重否定，则返回s = s。我们使用符号st：= αs。请注意，ααp=[α] p。大小|S|和|α|公式和程序的大小定义为抽象语法树的大小。比如说，|AP|为|布拉克|= 3。 注意|什特|>> |S|、|不|和|[α] s|≥ |⟨α⟩s|>> |α|、|S|。3方法概述我们的tableau方法是基于一个子句的形式，它提供了定期，命题和模态推理的分离。我们从几个定义和三个例子开始。一个基本公式是一个公式的形式p，x，或aαs。字面量是基本公式或基本公式的补项。子句（写为C，D，E）是不包含互补对的有限文字集（即， 一对形式为P，我102M. Kaminski，G.Smolka/Electronic Notes in Theoretical Computer Science 278（2011）99（p）。我们用连词来解释分句。条款的履行（即，I，X| = C）是M. Kaminski，G.Smolka/Electronic Notes in Theoretical Computer Science 278（2011）99103满足公式集的特殊情况（即，I，X（A），在第2节中定义。|例如，子句{<$a <$p，[a]（<$p<$q）}是不能满足的。一个权利要求是一对C，由一个条款C和一个菱形公式S组成。虽然我们不要求s∈C，但对于我们在下文中考虑的每一个主张Cs，都将是C支持s的情况。支持的概念后来被正式定义，使得C支持s（或A）和I，X| = C表示I，X| = s（I，X| = A）。 子句C对动作a的请求是RaC：={[α] s |[aα] s ∈C}。作为一个例子，考虑子句C={abp，bbp，[a（a+b）]<$p}。我们有RaC ={[（a + b）<$]<$p}和RbC =<$。我们的tableau方法适用于子句和链接（稍后正式定义），而不是单个公式。直觉上，链接是一对声明Cs Dt，表示为了使模型满足C中的菱形文字s，它必须满足D{t}。 给定一个子句，该方法试图将其扩展到一个tableau分支，其中每个子句C中的每个菱形文字s都通过链接CsDt实现，其中D是分支的子句之一。如果由链接所导致的关系是终止的，那么每一个这样的分支都是其所有子句的模型。如果由该方法构造的每个分支都无法实现带有链接的菱形文字，或者包含由链接形成的循环，则我们得出结论，输入是不可满足的。因此，我们得到了一个条款可满足性的判定程序。同时，该过程决定公式的可满足性，因为在HPDL中，公式s是可满足的，当且仅当子句{a}是可满足的（a的选择无关紧要）。该方法由三个推理机实现。正规推理机把程序α分解成更简单的（根据某种度量）程序β1，…，β n使得α<$β1+···+ β n.例如，一个A被分解为A和1。命题推理机为每个公式集合A确定一个支持A的子句集合，使得I，X| = A当且仅当I，X| = C为其中一个子句。例如，给定公式ap<$[b]<$p，命题推理机确定单个子句{aap，<$p，[bb]<$p}。模态推理器是我们的tableau方法的顶层推理器。对于每个可满足的子句，它构造一个有限模型，其状态是子句，并且每个状态C都满足子句C。 为此，模态推理器从初始子句开始，并推导出更多的子句，直到每个子句C中的每个菱形文字s都通过链接实现。模态推理器调用正则推理器确定后继公式t，调用命题推理器确定后继子句D。tableau方法终止，因为派生子句必须从可以从初始公式确定的有限集合中获取其文字。现在让我们举三个例子来说明我们的方法。在这一点上，它们在那里提供了一些关于方法的额外直觉，并且不必理解所有细节。要充分理解这些例子，在§8中介绍了所有正式的先决条件之后，对它们进行审查。例3.1考虑以下文字和子句：s：=a（a+b）pC：={t，<$p，u}t：=b（a+b）pD：={s，t，<$p，u}104M. Kaminski，G.Smolka/Electronic Notes in Theoretical Computer Science 278（2011）99s， t， p，ut，p，u454C2={s，p，u，v}C3={t，p，u，v}CsC s12CsC t13C4={t，p，u，v}C5={s，p，u，v}CsC t24CtC s3 5u：=[bb]（<$p t）E ：={p}我们从满足子句C开始模态推理。有一个索赔Ct要实现。我们需要一个支持公式<$（a+b）<$$>p和[b<$]（<$p<$t）的子句规则推理机和命题推理机确定Ct和Ds作为可能的后继子句和后继文字。模态推理器拒绝Ct，因为它会引入循环Ct Ct。对Ds是好的，加上子句D和连接Ct Ds。现在，索赔Ct已经实现。但是，新条款D有两个未实现的债权Ds和Dt。为了实现Ds，我们需要一个子句来支持公式（a+b）正则推理机和命题推理机产生对E1p、{s}s和{t}t。我们选择E1p并添加子句E和链接DtE 1p。 它仍然是实现D t。要做到这一点，我们需要一个支持公式<$（a + b）<$$>p和[b <$]（<$p<$t）的子句。如前所述，正则推理机和命题推理机产生Ct和Ds。两者都很好。我们选择Ct并添加链接Dt Ct。这给了我们一个初始子句C的模型。模型的图形表示如下所示：CBbD一E例3.2考虑以下文字：s：=a（a+b）pu：= [a（b+a）]pt：=<$b（a+b）<$$>p v：=[b（b+a）<$]p下面是不可满足子句{s，u}的封闭表：C1={s，u}这个表是封闭的，因为所有可能的索赔Ct和Cs的链接都引入了循环 例如，对于Ct正则推理机和命题推理机产生连接Ct Cs和Ct Ct。 请注意，子句名称Ci不充当前缀。他们4 2 4 4仅用于解释目的。例3.3由于小句形式，我们的tableau方法扩展到名词是简单的。当我们向分支添加一个新子句时，我们向pM. Kaminski，G.Smolka/Electronic Notes in Theoretical Computer Science 278（2011）99105p3ax，aap，<$p，[a]<$px，aap，pnew子句出现在分支的子句中的所有文字，这些子句与new子句具有共同的名词性。这将处理名义传播。分支上已有的子句和链接保持不变。考虑子句C={<$aa<$$>p，[a]（x<$$>p），[b]x，<$b<$[a]<$p}。初始的tableau由C组成，可以发展成如下所示的最大分支（图形表示）。数字表示各分句的引入顺序。当引入子句4时，发生从子句2的名义传播注意，我们通过将子句1、3、4和5作为状态，将三元组1a 4、1b 4、4a 5和5a 3作为转换，获得分支上所有子句的模型。12 45第四章语言理论语义学我们为程序定义了一种语言理论语义，将公式视为原子对象。这种语义是规则推理机的基础，也是命题推理机的基础。这对于模态推理机的正确性证明也是必不可少的。语义是Kleene代数的语言理论模型与测试的适应[12]。字母A、B的范围包括有限组公式。一个有保护的字符串是一个有限序列Aa1A1. a n A n，其中n≥ 0。字母σ和τ在保护字符串上的范围。每个程序都对应于一组保护字符串，这些字符串可以被视为程序的运行。例如，程序（pa ） b<$p 对应于 所有受保护 的字符串 A1aA2. aAnaAn+1bAn+2使得 n≥ 1 ，p∈A1<$··<$An，且<$p∈An+2（对An+1没有限制）.长度|σ|σ = Aa1A1... A n A n是n。我们用For表示所有公式的集合。语言是一组受保护的字符串。 对于语言L和LJ以及公式集合A，我们定义如下：LA：={B|AB}L0 ：=LL·LJ：={ωAωJ|ωA∈L，AωJ∈ LJ}L n+1：=L·LnL：=Lnn∈N其中ω，ωJ的范围是部分的，可能是空的保护串。 注意，L=L（L-L）·L。 我们给每个程序α分配一种语言Lα：La ：={AaB| A，B对}L（α+β）：= Lα- Lβaa106M. Kaminski，G.Smolka/Electronic Notes in Theoretical Computer Science 278（2011）99我我我我我Ls：=L{s} L（αβ）：=Lα· LβL 1：=L Lα：=（Lα）注意，L（s）=L 1 =L（（s+t））。给定一个解释I，我们定义关系−σ→关于σ的结构：X−A→IYX=Y 和I， X|=A我是|我|×|我|通过感应X−A→aσYI， X|=AndZ：X−a→ ZandZ−σ→Y提案4.1(i)X−α→IY<$σ∈Lα：X−σ→IY(ii) I， X|=<$α<$s<$$><$σ∈Lα<$Y：X−σ→Y和I， Y|=s(iii) I， X|=[α]sσ∈LαY：X−σ→是的，我， 是的|=s5常规DNF我们现在描述常规推理机。 常规推理依赖于语言理论语义学，而忽略了语言的命题和模态方面。如果一个程序的形式为aα，则它是基本的，如果它是1或基本的，则它是正常的。直观地说，程序α的正则DNF是α分解成正规程序β1，... ，β n使得α <$β1+···+ β n（或者更正式地，Lα = Lβ1<$···<$βn）。这种简单的直觉不能解释测试。例如，程序p不能用任何一组正常的程序来表示因此，我们正式进行如下。我们用Fα表示在α中出现的所有公式的集合作为子程序。例如，F（a<$p+b<$ap<$q）={<$p，<$ap<$q}。作为程序出现的公式称为测试。请注意，Fα不包括在α中发生的测试中发生的测试。命题5.1如果s∈ Fα，则对每个t，|S|<|s|<|阿罗克特|≤ |[α] t|。一个保护程序是一对Aα，其中A是一组公式，α是一个程序。一个保护程序Aα是正常的，如果α是正常的。保护程序的语言是L（Aα）：=LA·Lα。正则DNF是一个函数D，它映射每个程序α到正常防护程序的有限集合Dα，使得：(i) Lα=Bβ∈DαL（Bβ）(ii) 若Bβ∈ Dα，则B<$Fβ <$Fα。常规推理器计算常规DNF。Kleene我们给出了一个计算正则DNF的朴素算法由于空间原因，我们省略了正确性证明。该算法采用以下推理规则，M. Kaminski，G.Smolka/Electronic Notes in Theoretical Computer Science 278（2011）99107程序.AaAa1作为（A;s）1A（α1α2）β砷β（A;s）βA1βAααA（α1+α2）Aα1，Aα2AαβA（α1+α2）β Aα1β，Aα2βAα1α2βA1，AαAβ、Aαα <$ β符号A;s代表集合A{s}。同样，我们把不带括号的形式为α（βγ）的程序写成αβγ。给定一个保护程序集G，我们用RG表示G在规则下的闭包。我们可以证明RG描述的语言与G相同，如果G是有限的，那么RG是有限的。设G是一个保护程序集，若不存在Bα∈G使得B∈A，则称Aα∈G是G中的极小保护程序.对于Dα，我们取所有正规的保护的，在R{\displaystyle R{\displaystyleR{\displaystyle R}中最小的程序。例5.2考虑程序（a+b）。我们有：R{<$（a+b）<$}={<$（a+b）<$，<$1，<$（a+b）（a+b）<$，<$a（a+b）<$，<$b（a+b）<$} D{（a+b）<$}={<$1，<$a（a+b）<$，<$b（a+b）<$}例 5.3 考 虑 程 序 （ p+q ） n ， 其 中 p ， q 是 谓 词 。 我 们 有 D{ （ p+q ）<$}={<$1}。我们从优化中获益，只有最小的保护程序被用于DNF。否则D{（p+q）n}将包含另外三个元素：{p}1，{q}1和{p，q}1。虽然上面的朴素算法为每个程序α产生一个规则的DNF，但它在实践中的效率还有待观察。对于没有测试的程序（即，对于正则表达式），可以通过转换为确定性有限自动机来获得有效的正则DNF [4]。我们希望类似有效的规则DNF也存在于测试程序中。我们为论文的其余部分固定了一些可计算的正则DNFD提案5.4（一）I，X|=α s Bβ∈ Dα：I，X| = B; αβs（二） I，X| = [α] sBβ∈ Dα： （t∈B： I，X| =<$t）或I，X| =[β] s证据 接着是命题4.1。Q6命题DNF命题推理器依赖于从子句到公式的支持关系，该关系从语言的大多数模态方面抽象出来我们通过在s上的递归来定义支持关系C d s。108M. Kaminski，G.Smolka/Electronic Notes in Theoretical Computer Science 278（2011）99C d ss∈Cifs是文字M. Kaminski，G.Smolka/Electronic Notes in Theoretical Computer Science 278（2011）99109C d<$sC d sC dstC d s和C d t C dstC d s或C d t Cd1sC d sC d[1]sC d s如果α不正态，则C d<$α <$s <$$>Bβ∈ Dα：（<$t∈B：C d t）和C d<$β<$sC d[α]sBβ∈ Dα： （t∈B：C d<$t）或C d[β]s，如果α不正态最后两个等价的定义使用了上面固定的正则DNFD。递归终止，因为公式的大小减小了（用命题5.1验证），或者递归是在公式<$β<$s或[β]s上，其中β是正规的，s不变。如果Cd支持s，我们说C支持s。 我们记为Cd A，说C支持A，如果对每个s∈A都有Cd s.注意C dDDC（回想一下C和D表示子句）。命题6.1如果C d A和C<$D和B<$A，那么D d B。命题6.2如果I，X| = C和C d A，则I，X| = A.证据 接着是命题5.4。Q我们将命题DNF定义为这样的函数：应用于公式集A，产生A中公式合取的DNF（传统意义上），表示为一组子句。换句话说，我们要求一个命题DNFD应用于集合A满足等价性s∈As<$C∈DAt∈C t.形式上，命题DNF是一个函数D，它将公式的每个有限集合A映射到子句的有限集合，使得：(i) I，X| = AD∈ DA：I，X| = D.(ii)C d AD∈ DA：D<$C.命题DNF的性质（ii）直接意味着下面的命题。命题6.3如果C∈ DA，则C d A。在下文中，我们将经常隐式地使用命题6.3。对于模态推理机的终止，命题DNF必须有一些附加的有限性属性。我们需要一些预备性的定义。程序α的变体是基本程序β，使得对于某些B，Bβ∈Dα。一个基是一个基本公式的集合U，使得当α∈U且β是α的变体时，β∈S∈U。如果满足以下条件，则基U支持公式s：(i) U包含在S中出现的所有基本公式。(ii) 如果<$α<$t出现在s中，α不是基本的，β是α的变体，则<$β<$t∈U。一个基支持一组公式A，如果它支持每个公式s∈A。命题6.4每一个有限公式集都有一个有限基支持。110M. Kaminski，G.Smolka/Electronic Notes in Theoretical Computer Science 278（2011）99证据 从属性（ii）得出基础常规DNF。Q一个命题DNFD是无穷的，如果对于公式A的每一个有限集合和每一个支撑A的基U以及每一个子句C∈ DA，它保持U支撑C。命题6.5存在一个可计算的有限命题DNF。证据支持关系的定义可以看作是公式的表格式分解过程。 使用这个过程，可以将A展开为一个完整的场景每个开分支的文字产生一个子句。所有条款通过这种方式获得的DNF构成A。命题DNF的性质（i）的方向DNF是无穷的，这是因为除了用无穷正则DNF得到的菱形公式外，分解并没有引入新的公式。Q例6.6取§5中给出的正则DNF和命题6.5的证明中给出的命题DNF。我们有：D{bp}={{p}，{bbp}}D{bp，[b]（q<$p）}={{bbp，q，<$p，[bb]（q<$p）}}D{ap，[a]<$p}=D{（a+b）p}={{p}，{a（a+b）p}，{b（a+b）p}}在第三个例子中，注意[a]<$p是ap的补数。我们为论文的其余部分固定了一些可计算的和无限的命题DNFD。7金刚石膨胀和名义传播我们现在回到模态推理机，这是第一次解释§3。模态推理器构建一个表，其中每个分支包含子句和链接。目标在于构造一个分支，其中每个索赔都通过链接实现，并且满足一些进一步的条件。我们首先精确地说明模态推理器如何导出新的子句。权 利 要 求 Caαs 的 扩 展 是 权 利 要 求 Dβs ， 使 得 Bβ∈ Dα ，D∈ D（B;<$β<$s<$RaC），对某些B.下面的命题阐述了展开式的一个重要性质（后面不再需要这个命题命题7.1设Cs是一个要求，使得s∈C，且设I满足C。则存在Cs的展开式Dt，使得I满足D。一个链环是两个索赔的一对CsDt，使得s∈C，并且存在Cs的一个扩展Et，使得E<$D。一个拟分支是一个有限的子句和链环的集合Γ，使得{C，D}在任何时候Cs Dt∈Γ都是Γ。一个拟分支Γ实现一个主张Cs，如果Γ包含某个链CsDt。一个基支持拟分支Γ，如果它支持每个M. Kaminski，G.Smolka/Electronic Notes in Theoretical Computer Science 278（2011）99111我∗∗的条款。 一个解释I满足一个拟分支Γ（或者是Γ的一个模型），如果I满足r中的每个子句。如果一个子句包含一个名词性的，我们就称它为名词性的设Γ是一个拟分支，是一组公式。 我们用以下符号实现名义传播：AΓ ：=A{s| <$x∈A<$C∈ Γ：x∈C<$s∈C注意，AΓ是包含A和所有与A有共同名词的子句C∈Γ的公式的最小集合。故（Ar）r=Ar。此外，如果A不包含标称，则AΓ=A命题7.2如果一个解释满足Γ和C，它就满足CΓ。命题7.3设U是支撑拟分支Γ的基，Cs是一个要求，使得s∈C∈ Γ，Dt是Cs的一个扩张.则U支持DΓ。8分支和扩展规则一个实现所有要求的准分支机构不一定有一个模型。为了保证一个模型的存在，我们施加一定的条件，准分支作为模态推理机的不变量。其中一个条件是循环自由。例8.1考虑子句C ={<$aa<$$>p，p，q，[aa<$]（p<$q）}。注意C是不可满足的，{C，CpCp}是实现每个要求的准分支这个准分支的链接描述了一个循环。拟分支Γ中的路是序列C1s1. C nsn个权利要求，使得：（i）n∈[1，n]：Cr= C i.(ii)i∈[1，n−1]<$D：CisiDsi+1∈Γ且DΓ=Ci+1。拟分支中的环 r是路径C1s1. C NSN 在Γ中，使得n≥ 2和Cnsn=C1s1。分支是满足以下条件的准分支Γ• 函数性：如果C s D t∈Γ且C s E u∈Γ，则D t= E u。• 无环性：在Γ中没有环。• 名义相干性：如果C∈Γ，则CΓ∈ Γ。分支Γ的核心是C Γ：={C∈ Γ |Cr=C}。一个分支Γ是明显的，如果Γ实现C<$α<$s，对所有<$α <$s∈C∈ CΓ。我们将证明每个明显分支都有一个模型。模态推理器在分支上工作，并应用以下扩展规则：展开规则如果<$α<$s ∈C∈ CΓ且Γ不实现C<$α <$s，则将Γ展开到所有分支Γ ;DΓ;C<$α <$s（DΓ）t使得Dt是Cαs展开，DΓ是子句。112M. Kaminski，G.Smolka/Electronic Notes in Theoretical Computer Science 278（2011）99请注意，单个子句总是产生一个分支。所以模态推理器可以从任何子句开始。M. Kaminski，G.Smolka/Electronic Notes in Theoretical Computer Science 278（2011）99113我命题8.2模态推理器在每个分支上终止。证据由于分支在定义上是有限的，我们从命题6.4知道初始分支由一个有限基支持。根据命题7.3，我们知道扩展规则只添加初始基支持的子句索赔因为一个有限的基础只能支持有限多个子句。Q给定终止，模态推理器的正确性可以通过显示两个属性来建立：(i) 模型存在：每个明显分支都有一个模型。(ii) 合理性：每一个可满足的子句都可以发展成一个明显的分支。9模型存在命题9.1设Γ是一个显分支，且<$α<$s ∈C ∈ C Γ. 那么存在唯一的路径Cαs. D1sinΓ.证据路径存在，因为Γ是无环的，并且实现了CΓ中具有子句的每个索赔。 路径是唯一的，因为Γ是泛函。Q给我9分。2如果X−a→IY且I， Y|=B; Bβ∈Dα，其中I， X|=a αs。证据 接着是命题4.1和5.4。Q模型存在性的证明需要一个有点复杂的归纳，我们用下面的引理来实现。引理9.3设Γ是一个明显分支，I是一个解释，使得：• |我|= CΓ• C→aIDα，s，t，E：CaαsEt∈ΓandD=EΓforallllactionsa• C∈ Ip p∈C对所有谓词p• I x=C ⇐⇒ x∈C，对于所有出现在Γ中的名元素x让|Fα|：= max {|S||s∈ Fα}。 对于所有n∈N：(i) 对于每一条路径，D1在Γ中，使得|Fα|、|S| n<：I，C| = αs。(ii) 对于所有的C，D，σ，α，s使得|F α|、|S |δID，则在δICs>0的情况下，线性C s D t是用于非线性预测的初始值。一个qusi-brancr10.我的超次元帝国3LetIbeamododelofaquasi-brannchr。 δIAs=δIArs。引理10.4（直性）具有直模型的准分支不包含回路。证据矛盾。设I是一个拟分支Γ的直模型，C1s1. C nsn是Γ中的环。则n≥ 2且C1s1= Cnsn.对于所有i ∈ [ 1，n − 1]，都有δICisi>δICi+1si+1.Leti∈[1， n−1].对于a，α，t和D，Tensi= αaαt，C isiD si+1∈Γ，DΓ= C i+1. 因为每个σ∈L（a α）表示a的作用，其中δICi>0. Sinc e CisiDsi+1 对I而言是重要的，δICisi>δIDsi+1。 Henc e δICisi>δICi+1si+1byProposition10. 3sinceDr= Ci+1。QM. Kaminski，G.Smolka/Electronic Notes in Theoretical Computer Science 278（2011）99115我我我定理10.5（合理性）设I是分支Γ的直模型，令<$α<$s∈C∈ Γ使得Γ不实现C<$α<$s。然后存在C<$α<$s的展开式Dt，使得Γ; DΓ; C<$α<$s（DΓ）t是分支，I是Γ; DΓ; C<$α<$s（DΓ）t的直模型。证据 由于I满足C，根据命题10.2，有一些σ ∈ Lα和X，Y ∈|我|σBesuchthat|σ|=δIC（δαs）anddI， X|=CandX−→是的，我， 是|=s. Since<$α<$s是一个文字，α=aβ和σ=Aaτ，对于某些a，β，A，和τ∈ Lβ。 设Z ∈|我|besuchthatX−a→ZandZ−τ→Y. LetBγ∈Dβ，则atτ∈L（Bγ）。ThenI、Z|= B和I，Z|=由命题4.1（ii）得出的Δ γ Δ s。此外，I，Z| = RaC.因此，根据命题DNF的性质（i），存在某个D ∈ D（B;<$γ<$s<$RaC）使得I，Z| = D.显然，D<$γ<$s是C<$α<$s的展开，并且由于τ∈ L（Bγ），δID（<$γ<$s）≤|τ|为|σ|−1 <δIC （αs）. 这是由10个项目组成的。3、δIDΓ（γδ）<δIC（αδ）。 因此，I是Γ; DΓ; Cαs（DΓ）γs的一个模。 Mreover，r; Dr;Crαs（Dr）γs满足名义相干性和功能性条件。Q11最后发言本论文相对于我们以前的论文[10]的主要创新之处在于提出了无穷正则DNF的概念。这使得覆盖所有PDL程序并仍然具有透明的正确性证明成为可能。将HPDL的子句表方法直接推广到满足公式@xs。为了处理这样的公式，在[10]中提出的模态水平上增加了额外的展开规则。此外，在[10]中讨论的小句表的模态水平的优化延续到HPDL。通过简单的分析可以看出，利用§5中给出的朴素正则推理器和命题6.5中概述的基于表格的命题推理器的决策过程在NEXPTIME中运行。我们希望小句方法可以扩展到不同的模态。不太清楚的是将该方法扩展到转换模态的可能性。正如Gor'e和Widman[8]最近所述，现代化的企业可以通过Pratt式决策程序进行有效处理。然而，他们对逆向的处理似乎并不适用于我们的方法。另一方面，普拉特式程序似乎与名词不兼容（见[10，19]）。因此，为同时具有可能性、名词和逆模态的逻辑开发一个优雅的降级决策过程仍然是一个具有挑战性的开放问题。确认我们要感谢一位推荐人的宝贵意见，帮助改进了论文。116M. Kaminski，G.Smolka/Electronic Notes in Theoretical Computer Science 278（2011）99引用[1] Abate，P.，R.Gr'e和F。在以 下 情 况 下 ， 不 使 用 可 拆 卸 的 设 计 可 确 保 PDL-满足性：C. Areces和S.Demri， editors，Proc. 5th Workshop on Methods for Modalities（M4M-5） ，Electr. Notes Theor.Comput. Sci. 231（2009），pp.191-209.[2] 阿雷塞斯角和B.10 Cate，Hybrid logics，in：P.Blackburn，J.van Benthem和F.沃尔特编辑们模态逻辑手册，逻辑与实践推理研究3，爱思唯尔，2007年。821-868[3] Baader，F.，通过角色的传递闭包扩充概念语言：术语循环的替代方案，技术报告RR-90-13，DFKI（1990）。[4] Berry，G.和R.Sethi，从正则表达式到确定性自动机，Theor。Comput. Sci. 48（1986），pp. 117比126[5] De Giacomo，G.和F.Massacci，将演绎和模型检查结合到逆向PDL的表格和中，Inf.Comput。162（2000），pp. 117-137.[6] 菲舍尔，M。J.和R. E. Ladner，正则程序的命题动态逻辑，J. Comput。系统科学（1979），pp. 194-211[7] 戈雷河。 和F. 在以下情况下，为了满足PDL-要求，我们不应将可执行的所有设计都考虑在内：R. A.Schmidt，editor，CADE 2009，LNCS5663（2009），pp. 437-452[8] 戈雷河。 和F. 在我 看 来， 操 作 可以 通 过 以下 方 式 进 行： J。 给我一个机会。 Hüahn le，editors，IJCAR2010，LNCS6173（2010），pp. 225-239[9] Harel，D.，D. Kozen和J.Tiuryn，[10] Kaminski，M.和G.Smolka，具有可能性的混合逻辑的终止表，在：J。Giesl和R.Hahnle ，editors，IJCAR 2010，LNCS6173（2010），pp. 240-254[11]Kaminski，M.和G.Smolka，混合PDL的子句表，技术报告，萨尔大学（2011）。网址www.ps.uni-saarland.de/Publications/details/KaminskiSmolka:2011:HPDL.html[12] Kozen ，D.和F. Smith， Kleene代数 与测 试： 完备性 和可 判定 性， 在：D 。van Dalen和 M. Bezem，editors，CSL244-259[13] Kozen，D.和J.Tiuryn，Logics of programs，in：Handbook o