On the Complexity of Deciding Call-by-Need
在最近的一篇论文中，我们介绍了一个新的框架，用于研究在项重写中对范式和根稳定形式的按需计算的调用。使用基本树自动机技术和地面树传感器，我们获得了简单的可判定性证明类重写系统，比以前的类定义使用复杂的顺序性概念。在本文中，我们表明，我们可以做没有地面树传感器，以达到可判定性的证明，直接树自动机结构中的措辞。这使我们能够获得更好的复杂度界限。
2011-11-28 cs.LO cs.PL
Model-checking real-time systems: revisiting the alternating automaton route
本文提出了一种基于区域方法的1-ATA空性算法，改进了MTL到1-ATA的转换，并研究了在特定条件下模型检验实时系统的方法。
2026-01-06 cs.FL cs.LO
Logical Foundations of RDF(S) with Datatypes
Vienna University of Technology（维也纳工业大学）
资源描述框架（RDF）是一种语义Web标准，它提供了一种数据语言，简称为RDF，以及一种轻量级的本体语言，称为RDF模式。我们研究了RDF在逻辑中的嵌入，并展示了如何使用标准逻辑编程和描述逻辑技术进行RDF推理。随后，我们考虑扩展的RDF与数据类型的支持，考虑D蕴涵，定义在RDF语义规范，和D* 蕴涵，语义弱化的D蕴涵，介绍了特霍斯特。我们使用的嵌入和性质的逻辑建立新的上限的复杂性决定蕴涵。随后，我们建立了两个新的下界，确定RDFS蕴涵是PTime完全的，而simple-D蕴涵是coNP困难的，当考虑任意数据类型时，无论是在蕴涵图的大小方面。结果表明，RDFS可能不像人们所期望的那样轻量级。
2014-01-16 cs.AI cs.LO
Buchi automata augmented with spatial constraints: simulating an alternating with a nondeterministic and deciding the emptiness problem for the latter
这项工作的目的是彻底调查Buchi自动机增强空间约束。这种自动机的输入树是无限k元西格玛树，节点代表时间点，西格玛除了在经典的k元西格玛树中使用外，还包括对感兴趣的n对象空间场景的快照的描述。来自RCC8类空间关系代数（RA）x的约束用于对空间场景的对象施加空间约束，最终在输入树的不同节点处。我们表明，一个布奇交替增强空间约束的自动机可以模拟与经典的布奇不确定自动机相同类型，增强空间约束。然后，我们提供了一个非确定性的双深度优先多项式空间算法的空问题，后者自动机。我们的主要动机来自另一项工作，也提交给这次会议，它定义了一个时空化的著名家庭ALC（D）的描述逻辑与一个具体的域：一起，这两个作品提供了一个有效的解决方案的可满足性问题的概念的时空化的弱循环TBox。
2020-02-22 cs.FL cs.LO
Deciding Kleene Algebras in Coq
在Coq证明助手中给出了判定Kleene代数方程理论的自反策略。这种策略依赖于有效的有限自动机算法的仔细实现，以便它即时解决休闲方程并适当地扩展到更大的表达式。证明了决策过程的正确性和完备性：正确性是建立在w.r.t.通过形式化Kozen的初始性定理的任何模型;当给定的方程不成立时返回一个反例。正确性证明是具有挑战性的：它既涉及对底层自动机算法的精确分析，又涉及大量的代数推理。特别是，我们必须正式的理论矩阵的Kleene代数。我们建立在最近增加的第一次typeclasses在Coq，以有效地工作与所涉及的代数结构。
2012-03-01 cs.LO cs.SC
Efficient Emptiness Check for Timed Büchi Automata (Extended version)
时间自动机的Büchi非空性问题是指判定一个给定的自动机是否有满足Büchi接受条件的无限非Zeno运行。这个问题的标准解决方案是添加一个辅助时钟来处理非Zenoness。在本文中，它表明，这种简单的变换有时可能导致指数爆破。提出了一种避免这种爆破的结构。它还表明，在许多情况下，非Zenoness可以确定没有额外的建设。提出了一种只在需要时使用非Zenoness构造的非空问题的动态算法。与原型实现的算法进行了实验报告。
2020-12-04 cs.LO
Model Checking Constraint LTL over Trees
约束自动机是Büchi自动机的一种改进，它处理来自某种关系结构S的数据字。这样一个自动机的每一个转换都带有S的关系的约束。只有当当前和下一个数据值满足转换的所有约束时，才能触发转换。这些自动机已被用于设置，其中S是一个线性顺序，以确定约束LTL的约束S。在本文中，S是无限分枝的无限阶树T。给出了T-约束自动机空性的PSPACE算法。这一结果暗示了T上约束LTL的可满足性和模型检验问题的PSPACE完备性。
2015-04-23 cs.LO
Finding Small Proofs for Description Logic Entailments: Theory and Practice (Extended Technical Report)
基于逻辑的人工智能方法的优势在于，它们的行为原则上可以通过为用户提供派生结果的证据来解释。然而，如果这样的证明变得非常大，那么即使各个推导步骤很容易理解，也可能很难理解结果。这激发了我们寻找描述逻辑（DL）蕴涵的小证明的兴趣。而不是集中在一个特定的DL和证明演算这个DL，我们引入了一个通用的框架，在该框架中，证明被表示为标记，有向超图，其中每个超边对应于一个单一的声音推导步骤。在理论方面，我们调查的复杂性，决定是否有一定的后果证明的大小最多$n$沿以下正交维度：（i）底层的证明系统是多项式或指数;（ii）证明可能会或可能不会重用已经派生的后果;和（iii）数$n$表示在一元或二进制。我们已经确定了这个决策问题的最坏情况下的复杂性，除了这些选项的可能组合之一。在实践方面，我们已经开发并实现了一种方法，用于基于称为遗忘的非标准推理任务生成表达性DL的证明。我们已经评估了这种方法上的一组现实的本体，并比较所获得的证明与DL推理机ELK产生的证明，发现基于遗忘的证明往往是更好的w.r.t.不同的证明复杂性的措施。
2020-04-23 cs.LO
Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic
我们介绍堆自动机，一个形式主义的符号堆碎片的分离逻辑与用户定义的归纳谓词的鲁棒性自动推理。可满足性、可达性和非循环性等鲁棒性属性对于基于分离逻辑的自动程序分析和验证中的各种推理任务都很重要。以前，这样的性质已经出现在分离逻辑文献的许多地方，但没有被系统地研究。在本文中，我们开发了一个基于堆自动机的算法框架，使我们能够以统一的方式获得广泛的鲁棒性的渐近最优决策程序。我们实现了我们的框架的原型，并取得了可喜的成果，所有上述的鲁棒性。此外，我们证明了堆自动机的适用性超出了鲁棒性。我们应用我们的算法框架的模型检验和蕴涵问题的符号堆分离逻辑。
2016-10-22 cs.LO
Deciding Regularity of the Set of Instances of a Set of Terms with Regular Constraints is EXPTIME-Complete
状态树自动机是一种研究得很好的表示术语语言的形式主义。本文研究了确定有限项的变量集的实例集的正则性的问题，其中每个变量被限制为树自动机给出的正则集的实例.这个问题最近被证明是可判定的，但复杂性未知。在这里，问题的精确复杂性是通过证明EXPTIME-完备性来确定的。主要贡献是一个新的，指数时间算法，进行各种指数变换所涉及的条款和树自动机，并决定通过分析公式不等式和高度谓词的规律性。
2009-11-18 cs.CC cs.LO cs.PL
A Unifying Approach to Decide Relations for Timed Automata and their Game Characterization
在本文中，我们提出了一个统一的方法来决定各种互模拟，模拟等价和两个时间自动机状态之间的前序。我们提出了一个区域为基础的方法来决定这些关系，我们消除了显式的产品建设的区域图或区域图在经典的方法。我们的方法也是通用的，可以用来决定几个时间关系。我们还提出了一个游戏表征这些时间的关系，并表明，游戏层次结构反映了层次结构的时间关系。人们可以得到一个无限的游戏层次，因此游戏表征进一步表明，尚未研究的定义新的时间关系的可能性。游戏的特征也帮助我们提出一个公式，它编码两个状态之间的分离，不是定时bisimilarily。这样的区别公式也可以产生许多关系以外的时间双相似性。
2013-07-29 cs.FL cs.LO
Nominals, Inverses, Counting, and Conjunctive Queries or: Why Infinity is your Friend!
Karlsruhe Institute of Technology（卡尔斯鲁厄理工学院）；Oxford University Computing Laboratory（牛津大学计算实验室）
描述逻辑是知识表示的形式主义，它提供了例如W3C OWL标准的逻辑基础。合取查询是数据库中的标准查询语言，作为查询描述逻辑知识库的一种表达形式，近年来得到了广泛的关注。几种不同的技术，决定合取查询蕴涵可用于广泛的DL。然而，OWL 1和OWL 2 DL中的名词、逆角色和数量限制的组合导致了迄今为止可用的技术无法解决的问题。我们解决这个问题，并提出了一个决定性的结果蕴涵工会的合取查询在DL ALCHOIQb，同时包含所有三个有问题的建设者。提供查询只包含简单的角色，我们的结果也显示了可判定性蕴涵（工会）合取查询的逻辑，支持OWL 1 DL，我们相信，所提出的结果将铺平道路，进一步取得进展合取查询蕴涵决策程序的描述逻辑基础的OWL标准。
2014-01-16 cs.AI cs.LO
Improved Undecidability Results for Reachability Games on Recursive Timed Automata
我们研究递归时间自动机（RTA）上的可达性游戏，推广Alur-Dill时间自动机的递归过程调用机制类似于递归状态机。对于具有两个或多个时钟的自动机，RTA上的可达性博弈中的胜者判定问题是不可判定的，而对于只有一个时钟的自动机，该问题是可判定的。Ouaknine和Worrell最近提出了一个实时验证的时间有界理论，声称对有界时间的限制恢复了与实时验证相关的几个关键决策问题的可判定性。我们重新审视了具有时间限制的递归时间自动机上的博弈，希望能恢复可判定性。然而，我们发现，这个问题仍然是不可判定的递归时间自动机与三个或更多的时钟。使用类似的证明技术，我们的特点是一个可判定性边境的推广RTA递归秒表自动机。
2014-08-26 cs.FL cs.LO
Alignment complete relational Hoare logics for some and all
本文针对关系验证中的计算步骤对齐问题，提出并证明了针对∀∀和∀∃性质的关系型霍尔逻辑的对齐完备性，同时讨论了对齐在关系推理中的局限性并提出蕴含完备性作为评估手段。
2025-11-07 cs.LO
Bisimilarity of Probabilistic Pushdown Automata
研究了概率下推自动机及其子类的双相似性问题。我们的定义pPDA允许概率和非确定性的分支，概括了下推自动机的经典概念（没有ε-转换）。我们的第一个贡献是一个一般的建设，减少检查的概率转换系统的双相似性检查的非确定性转换系统。这种构造直接产生pPDA的双相似性的可判定性，以及概率基本过程代数的子类上的双相似性问题的基本上界，即，单态pPDA。我们进一步表明，通过仔细的分析，一般的减少可以用来证明一个EXPTIME上界的概率可见下推自动机的双相似性。这里我们还提供了一个匹配的下限，建立EXPTIME-完全性。最后，我们证明了概率单计数器自动机（pPDA的另一个子类）的判定双相似性是PSPACE完全的。在这里，我们使用一个更专门的参数来获得最佳的复杂度界限。
2012-10-08 cs.FL cs.LO
Deciding the synthesis problem for hybrid games through bisimulation
本文通过交替互模拟将初始化奇异混合博弈归约为时间博弈，并利用策略翻译引理，借助时间博弈工具为混合博弈合成获胜策略。
2024-09-30 cs.FL cs.LO
Deciding the Common Fragment of CTL with Past and LTL
Università degli Studi di Napoli “Federico II”（那不勒斯费德里科二世大学）；Università degli Studi di Udine（乌迪内大学）
本文通过引入无计数器犹豫弱树自动机，证明了带过去的CTL与LTL的共同片段可判定，解决了LTL与CTL交集可判定的长期开放问题。
2026-06-29 cs.FL cs.LO
Deciding Differential Privacy of Online Algorithms with Multiple Variables
本文推广了DiP自动机模型以支持多实值变量，刻画了差分隐私DiP自动机类，证明其判定问题为PSPACE完全，并实现了相应算法验证其有效性。
2023-09-12 cs.CR cs.FL cs.LO
Star Height via Games
提出了一种新的星高判定算法。正如Kirsten所示，恒星高度问题简化为一个关于计数器自动机的问题，称为有限性。新的贡献是一个不同的算法的有限性问题，这减少了它解决一个Gale-Stewart游戏与ω-正则获胜条件。
2017-08-11 cs.FL cs.LO
Reachability and liveness in parametric timed automata
本文研究参数化时间自动机（PTAs）的可达性与活性，通过提出整数点PTAs子类推进可判定性边界，并证明L/U-PTAs中无限运行存在性为PSpace完全，而死锁存在性不可判定。
2022-02-07 cs.LO
On Delay and Regret Determinization of Max-Plus Automata
半环$(\mathbb{Z} \cup {-\infty}, \max, +)$上加权自动机的决定性问题是一个长期存在的问题。我们提出了两种方法来接近它通过限制搜索空间的确定性WA：k-延迟和r-遗憾。一个WA N是k-延迟可确定的，如果存在一个确定性自动机D，它定义了与N相同的函数，并且对于N语言中的所有词α，D在α上的接受游程总是与N在α上的最大接受游程最多相距k。也就是说，沿着相同长度的所有前缀，两个游程的权重的游程和之间的绝对差至多为k。一个WA N是r-后悔可决定的，如果对于它的语言中的所有词α，它的非决定性可以被动态地解决，以构造N的游程，使得它的值与N赋予α的值之间的绝对差至多是r。我们证明了WA是可确定的当且仅当它是k-延迟可确定的。因此，确定某个k的存在性与一般的确定性问题一样困难。当k和r被给定为输入时，k-延迟和r-后悔决定问题被证明是EXPtime-complete的.我们还表明，确定是否WA是r-后悔可确定的一些r是在EXPtime。
2017-03-03 cs.FL cs.GT cs.LO
