Model Checking an Epistemic mu-calculus with Synchronous and Perfect Recall Semantics
我们确定了一个子问题的模型检查问题的认知μ演算是可判定的。在这个子问题的实例中，公式允许在认知模态的范围内以限制的形式存在自由变量，以避免体现任何形式的共同知识。我们的子问题包含已知的可判定片段的认知CTL/LTL，可以表示获胜策略，在两个玩家的游戏中，一个玩家有不完美的信息和不可观察的目标，并与一个合适的编码，可判定的实例的模型检查问题的ATLiR。
2013-10-23 cs.GT cs.LO
Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting
多个证明助手，如Isabelle或Coq，可以同时检查多个证明。相比之下，当今绝大多数的小型证明检查器要么根本不支持并发，要么只支持有限的并发形式，这限制了多核处理器上证明检查的效率。这项工作显示了一个小的，内存和线程安全的内核，有效地检查证明并发和非并发的设计。这种设计是在一个新的证明检查器，称为Kontroli实现的Rupda-Pi演算模重写，这是一个既定的框架，以统一表达大量的逻辑系统。在从证明助手和交互式定理证明器获得的所有五个评估数据集上，Kontroli比该演算的参考证明检查器Dedukti更快。此外，Kontroli使用八个线程将最耗时的证明检查部分的时间减少了6.6倍。
2022-03-03 cs.LO
From $μ$-Calculus to Alternating Tree Automata using Parity Games
$μ$ -无限树上的微积分和自动机是描述无限树语言的互补方式。利用$μ$ -Calculus与交替树自动机之间的对应关系，将模式$μ$ -Calculus公式编译成交替树自动机，解决了可满足性和模型检验问题.因此提倡一个自动机模型，专门为工作模式$μ$ -微积分。与Janin和Walukiewicz提出的自动机模型相比，自动机模型的优点是能够以更简单的方式处理任意分支。这两个问题（即，模型检验和可满足性）分别通过约简到交替树自动机的相应问题，即接受问题和非空问题来解决。这些问题，反过来，解决使用奇偶性游戏的语义交替树自动机被翻译成一个获胜的战略，在一个适当的奇偶性游戏。
2016-02-02 cs.FL cs.LO
A Simple Probabilistic Extension of Modal Mu-calculus
概率系统是人工智能领域的一个重要课题。作为规约语言，逻辑PCTL现在是概率属性推理的默认逻辑。在本文中，我们提出了一个自然和简洁的概率扩展μ演算，另一个突出的逻辑在并发理论。我们研究了与PCTL的关系。有趣的是，表现力与PCTL高度正交。所提出的逻辑捕获了一些有用的属性，不能在PCTL中表示。研究了模型检验和可满足性问题，证明了模型检验问题是UP和co-UP问题，可满足性检验可以归结为求解奇偶对策问题.这也与PCTL相反，PCTL的可满足性检查仍然是一个悬而未决的问题。
2015-05-08 cs.LO
Efficient Evidence Generation for Modal $μ$-Calculus Model Checking (extended version)
本文提出两步法求解带附加信息的参数化布尔方程系统，先解核心再利用信息，以高效生成模态μ演算模型检测的证据，并证明正确性及实现验证。
2025-01-27 cs.LO
Model Checking Games for the Quantitative mu-Calculus
我们研究了模态逻辑和模态μ演算的定量扩展，并研究了逻辑和游戏之间的紧密联系是否可以从定性逻辑提升到定量逻辑。事实证明，如果以适当的方式定义定量μ演算，尊重逻辑运算符之间的对偶性质，那么它的模型检验问题确实可以通过奇偶博弈的定量变体来表征。然而，这些定量游戏有相当不同的性质比他们的经典同行，特别是他们，在一般情况下，不确定的位置。逻辑和博弈之间的对应是双向的：定量转换系统上的公式的值与相关的定量博弈的值一致，相反，定量平价博弈的值在定量μ演算中是可定义的。
2008-02-20 cs.GT cs.LO
Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus
Ong证明了由n阶递归方案生成的可能无限排序树的模态μ演算模型检验问题（等价于交替奇偶树自动机（APT）接受问题）是n-EXPTIME完全的。我们认为两个子类的APT和调查各自的验收问题的复杂性。主要结果是，对于APT与一个单一的优先级，问题仍然是n-EXPTIME完全的，而对于APT与一个析取转移函数，问题是（n-1）-EXPTIME完全的。Kobayashi最近的工作表明，函数式程序的资源使用验证可以简化为递归模式的模型检验。作为一个应用，我们证明了资源使用验证问题是（n-1）-EXPTIME完全的。
2011-12-20 cs.LO cs.PL
Formula size game and model checking for modal substitution calculus
Mathematics Research Centre, Tampere University（坦佩雷大学数学研究中心）
本文通过公式大小游戏研究了MSC及其扩展的表达能力和模型检验复杂度，证明其与图灵机、mu演算等的复杂度关系，并建立了相关逻辑的复杂度分类。
2026-10-22 cs.LO
Decomposition Theorems and Model-Checking for the Modal $μ$-Calculus
我们证明了一个一般的分解定理的模式$μ$ -演算$L_μ$的精神Feferman和Vaught的定理不相交的工会。特别是，我们表明，如果一个结构（即，转换系统）由两个子结构$M_1$和$M_2$加上从$M_1$到$M_2$的边组成，则在$M$中的节点处的公式真仅取决于在相应子结构中的公式真，其意义在下面进行精确说明。因此，我们证明了$L_μ$的模型检测问题是固定参数易处理的（FPT）类结构的有界凯利宽度或有界DAG宽度。据我们所知，这些是$L_μ$的第一个FPT结果，它不遵循嵌入到一元二阶逻辑中。
2014-05-09 cs.LO math.LO
A Linear-Time Nominal $μ$-Calculus with Name Allocation
无限字母表语言的逻辑和自动机模型，如Freeze LTL和寄存器自动机，用于验证过程或带有数据的文档。它们与名义集上的形式主义密切相关，例如非确定性轨道有限自动机（NOFA），其中名称扮演数据的角色。在这种形式主义中的推理问题在计算上往往是困难的。名字绑定的名义自动机模型，如规则的非确定性名义自动机（RNAs）已被证明是计算上更容易处理。在本文中，我们介绍了一个线性时间不动点逻辑Bar-muTL有限字在一个无限的字母表，它的特点是完全否定和冻结量化通过名称绑定。我们通过对扩展的正则非确定性名义自动机的非平凡约简表明，尽管Bar-muTL允许无限制的非确定性和无限多的寄存器，但RNAs上的模型检验Bar-muTL和可满足性检验都具有基本的复杂性.例如，模型检验在2 ExpSpace中，更准确地说是在参数化的ExpSpace中，有效地将寄存器的数量作为参数。
2021-08-20 cs.FL cs.LO
On Modal μ-Calculus over Finite Graphs with Bounded Strongly Connected Components
对于每一个正整数k，我们考虑强连通分支的大小不超过k的所有有限图的类SCCk。我们表明，对于每一个k，模态μ演算不动点层次SCCk崩溃到级别Delta 2，但不是Comp（Sigma 1，Pi 1）（组成的公式级别Sigma 1和Pi 1）。这与所有图的类形成对比，其中Delta 2 =Comp（Sigma 1，Pi 1）。
2010-06-08 cs.FL cs.LO
Decidability of Type-checking in the Calculus of Algebraic Constructions with Size Annotations
自从Val Tannen的先驱工作简单类型的类演算和一阶重写的组合（LICS'88），许多作者都通过将其扩展到更丰富的类型类演算和重写范式，最终在演算像代数结构的演算。这些工作提供了理论基础的类型理论的证明助手的功能和谓词定义的定向高阶方程。这种定义包含了基于归纳的定义，更容易编写，并提供了更多的自动化。另一方面，检查用户定义的重写规则是强规范化和融合的，并且在与beta约简结合时保持类型检查的可判定性，则更加困难。大多数终止标准依赖于期限结构。在以前的工作中，我们扩展到依赖类型和高阶重写，“大小类型”的概念由几位作者在ML类语言的简单框架中研究，并证明了它保持了强规范化。本文件的主要贡献是双重的。首先，证明了在带尺寸标注的代数构造演算中，只要尺寸标注所产生的约束集是可满足的，并且允许最一般的解，则类型推断和类型检验问题是可判定的.其次，我们证明了一个大小代数足够丰富的捕获通常的归纳为基础的定义和更多的后来的属性。
2006-09-11 cs.LO cs.PL
Optimal Satisfiability Checking for Arithmetic $μ$-Calculi
共代数$μ$演算为不动点逻辑提供了一个通用的语义框架，其分支类型超出了标准的关系设置，例如概率，加权或基于博弈。以前的工作的coalgebraic $μ$ -演算包括指数时间上界的可满足性检查，但需要一个良好的表规则的下一步模态。这样的规则并不是在所有感兴趣的情况下都可用，特别是那些涉及整数权重的情况，如分级$μ$ -演算，或者实值权重与非线性算术的组合。在本文中，我们证明了相同的复杂性上限更一般的假设下，特别是关于（更简单）的可满足性问题的复杂性的基本所谓的一步逻辑，大致描述为嵌套的下一个步骤片段的逻辑。我们还提出了一个通用的全局缓存算法，是适合于实际使用，并支持对飞行可满足性检查。示例应用包括在具有Presburger算术的分级$μ$ -演算的扩展中用于可满足性检查的新指数时间上界，以及（二值）概率$μ$ -演算的扩展与多项式不等式。作为一个副结果，我们还得到了一个新的上限$\mathcal{O}(((nk)!)^2)$的最小模型大小的可满足的公式，所有的共代数$μ$ -演算，其中$n$是大小的公式和$k$的交替深度。
2019-01-15 cs.LO
Certification for mu-calculus with winning strategies
我们定义了内存高效的证书$μ$演算模型检查问题的基础上，众所周知的对应关系的$μ$演算模型检验赢得一定的奇偶校验游戏。获胜策略可以在低多项式时间内独立检验，方法是观察奇偶博弈图中不存在最大优先级为奇数的可达强连通分支。获胜策略的计算遵循$μ$ -演算的朴素语义，通过不动点迭代。我们对$μ$ -演算模型检验的通常的不动点迭代进行检测，以便它以获胜策略的形式产生证据;这些获胜策略可以在$|S|$和空间$O(|S|^2 |ϕ|^2)$中以多项式时间计算，其中$|S|$是状态空间的大小，$|ϕ|$是公式$ϕ$ \@的长度。这里主要的技术贡献是部分获胜策略的概念和代数。在技术层面上，我们的工作可以被看作是一个新的，更简单的，直接建设性的证明之间的对应关系$μ$ -演算和奇偶游戏。
2014-01-08 cs.LO
Complexity of Polyadic Boolean Modal Logics: Model Checking and Satisfiability
研究了可达性关系上的多元模态逻辑的模型检验的计算复杂性和可满足性问题。首先，我们证明了所得到的逻辑的模型检验问题的组合复杂性是PTime完全的。其次，我们证明了可及性关系上的否定扩展的多元模态逻辑的可满足性问题是ExpTime-完全的。最后，我们证明了可达性关系上的置换和布尔运算符的多元模态逻辑的可满足性问题是ExpTime-完全的，在必要的假设下，可以使用的可达性关系的数量是有界的常数。
2022-10-03 cs.LO
Model Checking and Validity in Propositional and Modal Inclusion Logics
命题包含逻辑和模态包含逻辑是属于基于团队语义的逻辑家族的形式主义。本文研究了这些逻辑的模型检验和有效性问题。我们确定这两个问题的复杂性界限，包括宽松和严格的团队语义。通过这样做，我们接近完成该计划，其最终目的是分类的中心推理问题的复杂性模态和命题依赖，独立性和包含逻辑。
2017-04-24 cs.LO
Structural Refinement for the Modal nu-Calculus
我们引入了一个新的概念，结构细化，一个健全的抽象的逻辑蕴涵，模态核演算。使用新的翻译之间的模态nu演算和析取模态转换系统，我们表明，这两个规格形式主义是结构上等价的。使用我们的翻译，我们还转移的结构操作的组成和商从析取模态转换系统的模态nu演算。这表明模态nu演算支持规格说明的组合和分解。
2014-06-10 cs.LO
Bounded game-theoretic semantics for modal mu-calculus
我们引入了一个新的博弈论语义（GTS）的模态μ演算。我们所谓的有界GTS取代奇偶游戏与替代评估游戏，只有有限的路径出现，无限的路径是不需要的，即使当考虑的过渡系统是无限的。新的游戏提供了替代方法的各种建设的框架中的μ演算。例如，它们已经成功地用作一种方法的基础，这种方法导致逻辑的自然公式大小游戏。虽然我们的主要重点是介绍新的GTS，我们也考虑一些应用程序来演示其用途。例如，我们考虑一个自然的模型转换过程，减少模型检查游戏，检查一个单一的，固定的公式在构建的模型，我们还使用GTS识别新的替代变种的μ演算与PTime模型检查。
2020-05-21 cs.LO math.LO
The Descriptive Complexity of Modal $μ$ Model-checking Games
本文回顾了模态μ演算和奇偶博弈之间的关系，表明它比以前已知的更强大。它解决了一个问题，即是否描述的复杂性模态μ模型检验游戏，以前已知的依赖于语法的复杂性的公式，实际上取决于其语义的复杂性。结果表明，直到语义co-Büchi复杂度公式，其模型检验博弈的描述复杂度与其语义复杂度完全一致。在co-Büchi之外，公式的模型检验奇偶博弈的描述复杂性被证明是其语义复杂性的上界;它是否也是一个下界仍然是一个悬而未决的问题。
2017-09-07 cs.LO
Expressiveness of the modal mu-calculus on monotone neighborhood structures
我们的特点的表达能力的模态μ演算单调的邻域结构，在风格的Janin-Walukiewicz定理的标准模态μ演算。为此，我们考虑一个一元二阶逻辑单调邻域结构。我们的主要结果表明，单调模态μ演算正好对应于这个二阶语言的片段，是不变的邻域互模拟。
2015-02-27 cs.LO
Efficient Model Checking for the Alternating-Time μ-Calculus via Effectivity Frames
本文探讨基于 effectivity frames 实现 alternating-time μ-calculus 模型检测，发现大型系统中转换开销可被后续检测收益抵消，性能优于传统方法。
2025-06-01 cs.LO
Finite Convergence of the Modal Mu-Calculus on Almost-Periodic Words
TU Munich（慕尼黑工业大学）
研究模态μ-演算在几乎周期词上的有限收敛性，证明所有几乎周期词都有有限收敛性，刻画了无限词上的有限收敛性，还重新证明了相关可判定性结果。
2026-07-10 cs.FL cs.LO
Completeness of Kozen's Axiomatization for the Modal mu-Calculus: A Simple Proof
本文提出一个更简单易懂的Kozen模态μ演算公理化系统完备性证明，基于Walukiewicz的原始证明进行改进。
2026-09-24 cs.FL cs.GT cs.LO
On the cut-elimination of the modal $μ$-calculus: Linear Logic to the rescue
本文借助线性逻辑及其指数模态构造线性化系统 \muLLmodinf{}，并通过线性翻译证明非良基模态 $μ$-演算的语形切割消除。
2025-06-11 cs.LO
Coalgebraic Satisfiability Checking for Arithmetic $μ$-Calculi
本文在更一般的假设下证明了余代数μ-演算可满足性检查的指数时间上界，通过通用全局缓存算法实现，并直接支持无保护公式，应用于带多项式不等式的分级μ-演算和概率μ-演算扩展。
2024-07-22 cs.LO
Covariant-Contravariant Refinement Modal $μ$-calculus
Nanjing University of Aeronautics and Astronautics（南京航空航天大学）；Nanjing Audit University（南京审计大学）
协变-逆变加细（简称CC-加细）概念是互模拟、模拟和加细概念的推广。介绍了由模态$μ$-演算系统K $^μ$通过添加CC-加细量词而得到的CC-加细模态$μ$ -演算（CCRML $^μ$），建立了CCRML $^μ$的公理系统，并探讨了该公理系统的重要性质：可靠性、完备性和可判定性. CCRML $^μ$的语言可以被认为是用于描述涉及反应和生成动作的系统的属性的规约语言。它可用于形式化方法领域中一些有趣的问题。
2022-08-05 cs.CL cs.FL cs.LO
Model Checking for Modal Dependence Logic: An Approach Through Post's Lattice
在本文中，我们研究了一个扩展版本的模态依赖逻辑，允许任意布尔连接词。模态依赖逻辑最近由Jouko Väänänen通过依赖原子dep（.）扩展模态逻辑而引入。本文研究了模型检验问题的计算复杂性。对于任意布尔函数的完整分类，我们使用Emil Post介绍的Lattice方法。对逻辑语言的所有片段进行这种分类，允许模态$\Diamond$和$\Box$、依赖原子和任意布尔函数的逻辑符号。
2013-03-26 cs.CC cs.LO
Bounded Game-Theoretic Semantics for Modal Mu-Calculus and Some Variants
我们引入了一个新的博弈论语义（GTS）的模态μ演算。我们所谓的有界GTS取代奇偶游戏与替代评估游戏，只有有限的路径出现，无限的路径是不需要的，即使当考虑的过渡系统是无限的。新的游戏提供了替代方法的各种建设的框架中的μ演算。例如，它们已经成功地用作一种方法的基础，这种方法导致逻辑的自然公式大小游戏。虽然我们的主要重点是介绍新的GTS，我们也考虑一些应用程序来演示其用途。例如，我们考虑一个自然的模型转换过程，减少模型检验游戏，检查一个单一的，固定的公式在构建的模型，我们还使用GTS识别新的替代变种的μ演算与PTime模型检验。
2020-09-23 cs.CC cs.LO
Reasoning about Strategic Abilities in Stochastic Multi-agent Systems
本文提出概率交替时间μ演算PAMC用于随机多智能体系统策略能力推理，证明其复杂度性质并给出模型检测与可满足性检测算法，实现为开源工具且验证了有效性。
2024-12-12 cs.FL cs.GT cs.LO
Generic Model Checking for Modal Fixpoint Logics in COOL-MC
本文提出参数化模型检测工具 COOL-MC，支持多种 μ-演算实例，并通过归约奇偶博弈或惰性局部算法进行检测和基准评估。
2023-11-03 cs.LO
A Type-Based HFL Model Checking Algorithm
高阶模态不动点逻辑（Higher-order Modal Fixpoint Logic，HFL）是模态μ演算的高阶扩展，并且比模态μ演算更严格地表达。最近的研究表明，各种程序验证问题可以自然地归结为HFL模型检验：一个给定的有限状态系统是否满足给定的HFL公式的问题。在本文中，我们提出了一种新的算法HFL模型检验：这是第一个实用的算法，它运行速度快的典型输入，尽管超指数最坏情况下的复杂性的HFL模型检验问题。我们的算法是基于小林等人。的HFL模型检验的基于类型的表征，并启发了基于饱和的算法HORS模型检验，另一个高阶扩展的模型检验。我们证明了算法的正确性，并报告的实施和实验结果。
2019-08-27 cs.LO cs.PL
A Proof System with Causal Labels (Part II): checking Counterfactual Fairness
本文扩展TNDPQ演算，通过为因果标签制定结构条件并检查评估稳健性，验证概率分类器的反事实公平性。
2025-10-25 cs.LO
First-Order Modal $ξ$-Calculus: On the Aspects of Application and Bisimulation
本文提出了一阶模态$ξ$ -演算以及系谱Kripke模型。受模态$μ$ -演算的启发，一阶模态$ξ$ -演算采取了非常相似的形式，并将其归纳表达扩展到不同的维度。我们阐述了几个生动的例子，证明了这种逻辑的深刻的效用，特别是描绘家谱的并发计算机进程。互模拟概念的逻辑也得到了彻底的检查。
2023-01-17 cs.LO math.LO
A Natural Intuitionistic Modal Logic: Axiomatization and Bi-nested Calculus
本文引入了由前向汇合 Kripke 模型刻画的自然直觉主义模态逻辑 FIK，为其提供了完备的 Hilbert 风格公理化和双嵌套演算，该演算兼具判定程序与有限反模型提取功能。
2023-09-12 cs.LO
On model checking data-independent systems with arrays without reset
一个系统对于一个数据类型X是数据独立的，当它可以对类型X的值执行的操作仅限于相等性测试。系统还可以存储、输入和输出类型X的值。我们研究的模型检验的系统是数据独立的两个不同的类型变量X和Y，并可能另外使用数组的索引从X和值从Y。我们的主要兴趣是下面的参数化模型检查问题：一个给定的程序是否满足一个给定的时间逻辑公式的所有非空的nite实例的X和Y。最初，我们考虑的抽象，而不是X和Y是无限的，其中部分功能与有限域被用来模拟阵列。使用一个翻译的数据无关的系统，没有数组，我们表明，u演算模型检查问题是可判定的这些系统。从这个结果，我们可以推出所有系统的性质与有限的情况下，X和Y。我们表明，有一个程序，上述参数化模型检查问题的通用片段的u演算，使它总是终止，但可能会给假阴性。我们还推出了参数化的模型检测问题的泛析取自由片段的u演算是可判定的。对于具有阵列的数据独立系统的模型检验的实际动机包括存储器和高速缓存系统的验证，其中X是存储器地址的类型，并且Y是可存储值的类型。作为一个例子，我们验证了一组不可靠的存储器的容错存储器接口。
2004-05-27 cs.LO
Complexity of the Model Checking problem for inquisitive propositional and modal logic
本文研究了探究命题逻辑 InqB 和探究模态逻辑 InqM 的模型检测问题复杂性，基于 Yang 的思想证明了这两个问题均为 AP-完全。
2024-03-28 cs.LO math.LO
A modal aleatoric calculus for probabilistic reasoning: extended version
我们考虑多代理系统，代理的行动和信念是任意确定的，或“掷骰子”。这个系统由为独立随机变量分配分布的可能世界和为这些可能世界分配概率的代理组成。我们提出了一个新的语法和语义这样的系统，并表明，他们推广模态逻辑。我们还给出了一个健全的和完整的演算推理的基础语义，和健全的演算充分模态语义，我们猜想是完整的。最后，我们讨论了一些应用程序的推理博弈代理。
2018-12-31 cs.LO
Minimal Proof Search for Modal Logic K Model Checking
LAMSADE（拉马萨德实验室）；Université Paris-Dauphine（巴黎第九大学）
大多数模态逻辑，如S5、LTL或ATL，都是模态逻辑K的扩展。虽然LTL和ATL的模型检验问题在过去的几十年里一直是非常活跃的研究领域，但更基本的多智能体模态逻辑K（MMLK）的模型检验问题本身作为完美信息多人游戏的正式框架具有重要的应用。我们提出了最小证明搜索（MPS），努力数为基础的算法解决的模型检验问题MMLK。我们证明了MPS的正确性之外的两个重要性质。MPS证明对于一般的代价定义是代价最小的，MPS是寻找代价最小的证明的最优算法。最优性意味着任何类似的算法要么需要探索比MPS更大或相等的状态空间，要么不能保证在每个输入上找到最小成本的证明。因此，我们的工作涉及A* 和AO* 在启发式搜索，证明数搜索和DFPN+在两个玩家的游戏，并在软件模型检验的反例最小化。
2012-07-10 cs.AI cs.LO
Łukasiewicz μ-calculus
本文探讨了ukasiewicz μ-演算的性质，或简称μ，它是ukasiewicz逻辑的一个扩展，具有标量乘法和最小和最大不动点算子（用于单调公式）。我们观察到，具有$n$变量的μ项定义了从$[0, 1]^n$到$[0, 1]$的单调分段线性函数。本文提出了两种计算有理输入下的双μ项输出的有效方法。然后我们考虑通过将盒模态和菱形模态添加到μ-演算而得到的μ-演算。或者，它可以被看作是Kozen的模态μ演算适用于概率非确定性转移系统（PNTS）的推广。我们展示了如何在著名的逻辑PCTL中表达的属性可以被编码为Mukasiewicz模态μ演算公式。我们还表明，算法计算值的ukasiewicz μ-演算条款提供自动（虽然不切实际）的方法验证ukasiewicz模态μ-演算性质的有限理性PNTS的。
2015-10-03 cs.LO
On Guarded Transformation In The Modal Mu-Calculus
保护范式要求μ演算公式中的不动点变量在模态算子的作用域下出现。文献中包含的保护变换有效地将μ演算公式转化为保护范式。我们发现，已知的守护变换可能会导致公式大小的指数爆破，与现有的多项式行为的索赔。我们还证明了对于更宽松的向量形式的μ演算公式，任何多项式保护变换都可以得到奇偶对策的多项式解算法，其存在性是一个公开问题.我们还研究了μ演算，向量形式和层次方程系统之间的转换，这是交替奇偶树自动机的另一种语法。
2013-12-20 cs.LO
Model checking Branching-Time Properties of Multi-Pushdown Systems is Hard
我们解决了多下推系统的共享内存并发程序的模型检验问题。我们认为在这里布尔程序与有限数量的线程和递归过程。众所周知，这类程序的模型检验问题是不可判定的。在本文中，我们调查的可判定性和这个问题的复杂性的假设下，有界的上下文切换定义的Qadeer和Zeroof，和相位有界的La Torre等人提出的。对时间逻辑，特别是分支时间逻辑，如模态$μ$ -演算或CTL的模型检验这样的系统很少受到关注。众所周知，与模态$μ$ -演算密切相关的奇偶博弈对于有界相位系统类是可判定的（因此对于有界上下文切换也是如此），但具有非初等复杂性（赛斯）。一个自然的问题是，这种高复杂性是否是不可避免的，有什么方法来绕过它。本文解决这些问题，不幸的是，有点令人惊讶的是，它表明，分支模型检验的MPDS本质上是一个很难的问题，没有简单的解决方案。我们证明了在相位限制下的MPDS上的奇偶博弈是非初等的。我们的主要结果表明，模型检验的$k$上下文有界MPDS对一个简单的CTL片段，由公式，其时间运营商来自集合${\EF, \EX}$，有一个非初等的下界。
2012-05-31 cs.FL cs.GT cs.LO
Complexity of Model Checking for Modal Dependence Logic
模态依赖逻辑（Modal Dependence Logic，MDL）是由Väänänen最近提出的。它通过操作符=（）增强了基本模态语言。对于命题变量p_1，.，p_n原子式=（p_1，...，p_（n-1），p_n）直观地说明p_n的值仅由p_1，.，p_（n-1）。我们证明了Kripke结构上MDL公式的模型检验是NP完全的，并进一步考虑了通过限制允许的命题和模态连接词的集合而得到的MDL片段。事实证明，几个片段，例如，没有情态动词或没有命题连接词的句子仍然是NP完全的。我们还考虑了MDL的限制，其中每个单个依赖原子的长度由整个逻辑固定的数字限制。我们表明，这个有界MDL的模型检验问题仍然是NP完全的。我们还通过允许经典析取（由Sevenster引入）来扩展MDL，除了依赖析取之外，并表明经典析取总是至少与有界元依赖原子一样糟糕，在某些情况下甚至更糟，例如，只有两个析取的片段是NP完全的。此外，我们几乎完全分类的计算复杂性的模型检验问题的所有限制的命题和模态算子的无界以及有界MDL。
2012-01-27 cs.CC cs.LO
Progress, Justness and Fairness in Modal $μ$-Calculus Formulae
针对模态$\mu$-演算中刻画带假设的活性属性难度高、易出错的问题，提出可实例化为多种活性属性的模板公式，覆盖进展、公正性等五类动作相关假设，且已证明公式正确性。
2024-07-10 cs.LO
An Improved Decision Procedure for Linear Time Mu-Calculus
本文提出了线性时间$μ$ -演算（$ν$ TL）的一种改进的现在将来形式（PF形式）.特别是，新版本的未来部分变成了公式闭包中元素的合取。我们证明了每一个封闭的$ν$ TL公式都可以转化为新的PF形式。此外，基于PF形式，给出了一种构造用于公式模型描述的现在将来形式图（PFG）的算法。在此基础上，提出了一种基于PFG的$ν$ TL公式保护片段可满足性判定方法，并在C++中实现。新的决策过程具有最好的时间复杂度比现有的，尽管指数空间的成本。最后，讨论了一种基于PFG的$ν$ TL模型检验方法，当模型违反某个性质时，可以直观地得到反例。
2015-07-20 cs.LO
Complete Bidirectional Typing for the Calculus of Inductive Constructions
本文提出了一个归纳结构演算（CIC）的双向类型系统。它引入了一种介于通常的推理和检查之间的新判断，称为约束推理，以处理类型中的计算。该系统的关键属性是其相对于通常的无向系统的完备性，这已经在Coq中作为MetaCoq项目的一部分正式证明。虽然它在一个现实的类型化算法的持续完整性证明中扮演着重要的角色，但双向性的兴趣更广泛，因为它在试图证明CIC或设计变体和扩展的属性时提供了见解和结构。特别是，我们提出了约束推理，通常的推理和检查判断之间的中间，处理类型中的计算的存在。
2021-04-19 cs.LO cs.PL
The Complexity of Model Checking Higher-Order Fixpoint Logic
高阶不动点逻辑（Higher-Order Fixpoint Logic，HFL）是简单类型λ演算和模态λ演算的混合。这使得它成为一个高度表达的时态逻辑，能够表达模态λ演算中无法表达的程序的各种有趣的正确性属性。本文给出了其模型检验问题的复杂性结果。特别是，我们认为这些片段的HFL只使用类型的有界阶k和arity m。我们建立k倍指数时间完备性的模型检验每个这样的片段。对于上界，我们使用不动点消除，以获得可达性游戏，是单指数的大小的公式和k倍指数的大小的底层过渡系统。这些博弈可以在确定性线性时间内求解。作为一个简单的结果，我们得到一个指数时间上界的表达复杂性的每个这样的片段。下界是由交替（k-1）重指数空间有界图灵机的字问题的一个简化而建立的。由于有固定的机器的类型，其字的问题已经很难相对于k倍指数时间，我们得到，作为一个推论，k倍指数时间完整性的数据复杂性的片段的HFL，提供m超过3。这也产生了表达能力的层次结构。
2007-06-29 cs.LO
First-Order Game Logic and Modal Mu-Calculus
本文研究了一阶博弈逻辑和一阶模态μ演算，它们用解释效果的一阶模态（如变量赋值）扩展了命题模态逻辑。不像在命题的情况下，这两个逻辑被证明具有相同的表达能力和他们的证明演算具有相同的演绎能力。两种结石也相互比较完整。在微分方程的存在下，推论获得了微分博弈逻辑（混合博弈的演绎验证逻辑）和微分μ演算（混合系统的模态μ演算）之间的可用和完整的翻译。微分μ-演算相对于一阶不动点逻辑是完备的，微分对策逻辑相对于它的无常微分的片段是完备的。
2022-02-11 cs.GT cs.LO math.LO
A Proof System with Names for Modal Mu-calculus
不动点是语义学、抽象解释和程序逻辑中的一个重要组成部分。它们添加到逻辑中可以增加相当大的表达能力。一个普遍的问题是如何定义这种逻辑的证明系统。在这里，我们将研究模态逻辑与不动点的证明系统。我们提出了一个Tableau证明系统，用于检查公式的有效性，它使用名称来跟踪不动点变量的展开，如Jungteerapanich所设计的。
2013-09-20 cs.LO
Filtration and canonical completeness for continuous modal mu-calculi
连续模态μ演算是模态μ演算的一个片段，其中不动点算子的应用仅限于其函数解释是斯科特连续的公式，而不仅仅是单调的。通过博弈论的手段，我们表明，这个相对表现力的片段仍然允许基本模态逻辑，这是出了名的失败的充分模态μ演算：过滤和规范模型的两个重要技术。特别是，我们证明了过滤定理的公式在语言中的连续模态μ演算。因此，我们得到了有限的模型属性在广泛的模型类。此外，我们证明了，如果一个基本模态逻辑L是标准的和类的L-框架允许过滤，那么通过添加连续不动点算子L得到的逻辑是健全的和完整的关于类的L-框架。这概括了最近的结果严格较弱的片段的模态μ演算，即PDL。
2021-09-17 cs.LO
Model-Checking of Ordered Multi-Pushdown Automata
我们解决了有序多下推自动机的验证问题：下推自动机的多栈扩展，具有对栈转换的约束，使得弹出只能在第一个非空栈上执行。首先，我们证明了有序多下推自动机的空问题是在2 ETIME。然后，我们证明了，对于一个有序的多下推自动机，一个正则配置集的所有前身的集合是一个有效的可构造正则集。我们利用这一结果来解决全球模型检验，其中包括在计算一个有序的多下推自动机，满足给定的w-正则性质（可表示在线性时间的时间逻辑或线性时间μ演算）的所有配置的集合。作为一个直接的后果，我们得到了一个2 ETIME上界的有序多下推自动机的w-正则性质的模型检验问题（匹配其下限）。
2012-09-19 cs.FL cs.LO
A Proof System with Causal Labels (Part I): checking Individual Fairness and Intersectionality
本文扩展TNDPQ演算，通过因果标签限制弱化规则，以验证概率分类器的个体公平性与交叉性，检查受保护与目标变量的条件独立性。
2025-10-25 cs.LO
Nested-sequent Calculus for Modal Logic MB
本文针对模态逻辑 MB 的完全性与可判定性未决问题，构造了其嵌套矢列演算并加以解决，同时探讨了添加新模态符号后的逻辑 MB+。
2024-12-31 cs.LO
Interpolation for the two-way modal mu-calculus
本文为双向模态 μ-演算引入非良基与循环证明演算，利用迹原子应用 Vardi 自动机证明其可靠性与完备性，并据此确立 Craig 插值与 Beth 可定义性。
2025-08-11 cs.LO math.LO
Probabilistic modal μ-calculus with independent product
概率模态μ-演算是一种不动点逻辑，用于表示概率标记变迁系统（PLTS）的性质。两个等价的语义已经研究了这个逻辑，都分配给每个状态一个值在区间[0，1]表示的概率，该公式表示的属性在状态保持。一种语义是指称的，另一种是游戏语义，指定在两个玩家的随机奇偶游戏。概率模态μ演算的一个缺点是缺乏对PLTS的其他重要时态逻辑（如概率计算树逻辑（PCTL））进行编码所需的表达能力。为了解决这个问题，我们扩展了一对新的运营商的逻辑：独立产品和余产品。由此产生的逻辑，称为概率模态μ演算与独立的产品，可以编码许多感兴趣的属性，并纳入定性片段的PCTL。本文的主要贡献是为这种扩展的概率μ演算定义了一个合适的博弈语义。这依赖于一类新的游戏的定义，它通过允许一个游戏被分成并发的子游戏，每个子游戏独立地继续它们的进化，来概括标准的两个玩家随机（奇偶）游戏。我们的主要技术结果是两个语义的等价性。证明是在ZFC集合论中进行的，在不可数基数上扩展了Martin公理。
2012-11-26 cs.LO
