A modal aleatoric calculus for probabilistic reasoning: extended version
我们考虑多代理系统，代理的行动和信念是任意确定的，或“掷骰子”。这个系统由为独立随机变量分配分布的可能世界和为这些可能世界分配概率的代理组成。我们提出了一个新的语法和语义这样的系统，并表明，他们推广模态逻辑。我们还给出了一个健全的和完整的演算推理的基础语义，和健全的演算充分模态语义，我们猜想是完整的。最后，我们讨论了一些应用程序的推理博弈代理。
2018-12-31 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
On Refinements of Boolean and Parametric Modal Transition Systems
我们考虑扩展的模态转换系统（MTS），即布尔MTS和参数MTS，我们调查这两个类的细化问题。首先，我们减少了这两个类的模态细化的问题，一个问题可解决的QBF求解器，并提供实验结果表明我们的技术规模以及。其次，我们扩展的算法，彻底完善MTS提供更好的复杂性，然后通过减少以前研究的问题。最后，我们研究了两类模型的模态精化和完全精化之间的关系，并展示了模态精化如何近似完全精化。
2013-04-18 cs.LO
Refinement Calculus of Reactive Systems
精化演算是一个强大的和表达的工具，推理顺序程序的组合方式。在本文中，我们提出了一个反应系统的精化演算的扩展。精化演算是基于单调谓词Transformers，它将后状态集转换为前状态集。为了对反应系统进行建模，我们引入了单调属性Transformers，它将输出轨迹集变换为输入轨迹集。我们将展示如何在这种语义细化，顺序组合，恶魔的选择，以及其他语义反应系统上的操作模型。我们主要使用高阶逻辑来表达我们的结果，但我们也展示了如何使用其他形式主义更适合自动化，如线性时序逻辑（适用于规范）和符号转换系统（适用于实现）的属性Transformers器可以定义。最后，我们展示了这个框架如何推广以前的工作关系接口，以便能够表达系统的无限行为和活性属性。
2014-06-23 cs.LO cs.SE
Progress, Justness and Fairness in Modal $μ$-Calculus Formulae
针对模态$\mu$-演算中刻画带假设的活性属性难度高、易出错的问题，提出可实例化为多种活性属性的模板公式，覆盖进展、公正性等五类动作相关假设，且已证明公式正确性。
2024-07-10 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
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
A Saturation Method for the Modal Mu-Calculus with Backwards Modalities over Pushdown Systems
我们提出了一个扩展的算法，用于直接计算的μ演算公式X上的下推系统的配置图，以允许向后的方式表示。我们的方法给出了第一个扩展的饱和技术，以充分的μ演算向后模态。
2010-06-30 cs.FL cs.LO
A Syntactic Approach to Computing Complete and Sound Abstraction in the Situation Calculus
针对现有缺乏计算可靠完备抽象的句法方法的问题，本文提出线性整数情境演算，迁移相关抽象框架，定义受护动作约束低层程序并限制精化映射，最终设计出可计算可靠完备抽象的句法方法。
2025-01-13 cs.LO
Nested-sequent Calculus for Modal Logic MB
本文针对模态逻辑 MB 的完全性与可判定性未决问题，构造了其嵌套矢列演算并加以解决，同时探讨了添加新模态符号后的逻辑 MB+。
2024-12-31 cs.LO
First-Order Modal $ξ$-Calculus: On the Aspects of Application and Bisimulation
本文提出了一阶模态$ξ$ -演算以及系谱Kripke模型。受模态$μ$ -演算的启发，一阶模态$ξ$ -演算采取了非常相似的形式，并将其归纳表达扩展到不同的维度。我们阐述了几个生动的例子，证明了这种逻辑的深刻的效用，特别是描绘家谱的并发计算机进程。互模拟概念的逻辑也得到了彻底的检查。
2023-01-17 cs.LO math.LO
Probabilistic modal μ-calculus with independent product
概率模态μ-演算是一种不动点逻辑，用于表示概率标记变迁系统（PLTS）的性质。两个等价的语义已经研究了这个逻辑，都分配给每个状态一个值在区间[0，1]表示的概率，该公式表示的属性在状态保持。一种语义是指称的，另一种是游戏语义，指定在两个玩家的随机奇偶游戏。概率模态μ演算的一个缺点是缺乏对PLTS的其他重要时态逻辑（如概率计算树逻辑（PCTL））进行编码所需的表达能力。为了解决这个问题，我们扩展了一对新的运营商的逻辑：独立产品和余产品。由此产生的逻辑，称为概率模态μ演算与独立的产品，可以编码许多感兴趣的属性，并纳入定性片段的PCTL。本文的主要贡献是为这种扩展的概率μ演算定义了一个合适的博弈语义。这依赖于一类新的游戏的定义，它通过允许一个游戏被分成并发的子游戏，每个子游戏独立地继续它们的进化，来概括标准的两个玩家随机（奇偶）游戏。我们的主要技术结果是两个语义的等价性。证明是在ZFC集合论中进行的，在不可数基数上扩展了Martin公理。
2012-11-26 cs.LO
Proof Systems for the Modal $μ$-Calculus Obtained by Determinizing Automata
本文提出一种二叉树构造以确定化非确定性奇偶流自动机，并据此得到公式由二进制字符串元组标注的循环证明系统 $\mathsf{BT}$，其可靠性与完备性由确定化正确性直接导出。
2023-07-14 cs.LO
Formula size games for modal logic and $μ$-calculus
我们提出了一个新版本的公式大小游戏模态逻辑。该游戏的特点是等价的指向Kripke模型的公式给定数量的模态算子和二元连接。我们的游戏类似于著名的Adler-Immerman游戏。然而，由于博弈位置定义的关键区别，它的获胜条件更简单，第二个参与者没有平凡的最优策略。因此，与Adler-Immerman博弈不同，我们的博弈是一个真正的两人博弈。我们说明了使用的游戏，通过证明互模拟不变的一阶逻辑$\mathrm{FO}$和（基本）模态逻辑$\mathrm{ML}$之间的非小学简洁的差距。我们还提出了一个版本的游戏模式$μ$演算$\mathrm{L}_μ$，并表明$\mathrm{FO}$也是非elementarily更简洁比$\mathrm{L}_μ$。
2019-12-17 cs.LO
Refinement calculus of quantum programs with projective assertions
本文提出一种专为量子程序定制的精化演算，通过正交投影子作为断言并基于对偶语义引入精化规则，为量子程序增量开发提供系统方法，并推出交互式原型工具 Quire 提供支持。
2023-11-23 cs.LO quant-ph
Formula size game and model checking for modal substitution calculus
Mathematics Research Centre, Tampere University（坦佩雷大学数学研究中心）
本文通过公式大小游戏研究了MSC及其扩展的表达能力和模型检验复杂度，证明其与图灵机、mu演算等的复杂度关系，并建立了相关逻辑的复杂度分类。
2026-10-22 cs.LO
A Simple Probabilistic Extension of Modal Mu-calculus
概率系统是人工智能领域的一个重要课题。作为规约语言，逻辑PCTL现在是概率属性推理的默认逻辑。在本文中，我们提出了一个自然和简洁的概率扩展μ演算，另一个突出的逻辑在并发理论。我们研究了与PCTL的关系。有趣的是，表现力与PCTL高度正交。所提出的逻辑捕获了一些有用的属性，不能在PCTL中表示。研究了模型检验和可满足性问题，证明了模型检验问题是UP和co-UP问题，可满足性检验可以归结为求解奇偶对策问题.这也与PCTL相反，PCTL的可满足性检查仍然是一个悬而未决的问题。
2015-05-08 cs.LO
Proof Search Specifications of Bisimulation and Modal Logics for the pi-Calculus
我们指定的操作语义和互模拟关系的有限π演算内的逻辑，其中包含的nabla量词编码通用的判断和定义编码不动点。由于我们只限于有限的情况，逻辑展开不动点的能力使得这个逻辑对于操作语义的归纳性质和互模拟的共归纳性质都是完备的。nabla量词有助于解决π演算表达式中变量范围及其执行（证明）的微妙问题。我们说明了这种逻辑所允许的逻辑规范的几个优点：它们是自然的和说明性的;它们不包含关于变量名的副条件，同时保持对这些变量的完全形式化处理;后期互模拟关系和开放互模拟关系之间的差异来自于熟悉的逻辑区别;三个量词之间的相互作用（对于所有，存在，（nabla）它们的作用域可以解释早期互模拟和晚期互模拟之间的差异以及基于约束输入和输出行为的各种模态算子之间的差异;并且涉及推理规则、统一和回溯的应用的证明搜索可以为模态逻辑中的一步转换、互模拟和满足提供完整的证明系统。我们还说明了如何可以编码的π演算与复制，在一个扩展的逻辑与归纳和共归纳。
2009-02-16 cs.LO
Modal Calculus of Illocutionary Logic
言外逻辑的目的是解释语境如何影响某些特殊类型的施为话语的意义。回想一下，施为性话语被理解为：说话者用施为力（分别是：断言、推测、许诺），由适当的施为动词命名，以表示自己正在实施该行为。在这篇论文中，我提出了将言外之力理解为模态算子的多值解释。因此，我建立了一个非阿基米德价值逻辑形式化的言外行为。第一次提出了一种正式的多值以言行事逻辑方法。
2011-02-22 cs.LO
The Refined Calculus of Inductive Construction: Parametricity and Abstraction
我们提出了一个改进的演算归纳结构，其中可以很容易地定义一个概念的关系参数。它提供了一种新的方式来自动化证明的交互式定理证明器，如Coq。
2012-11-27 cs.LO
The Modal Logic of Abstraction Refinement
Technische Universität Dresden（德累斯顿工业大学）
本文研究了抽象细化中CTL属性真值变化的模态逻辑，并为三种情形提供了上界和下界，同时开发了新的控制语句技术来证明结果。
2026-01-13 cs.LO
Calculating modules in contextual logic program refinement
逻辑程序的精化演算是从规范导出逻辑程序的框架。它基于一种可以表达规范和代码的广谱语言，以及一种对正确实现的概念进行建模的细化关系。在本文中，我们扩展和概括上下文细化的早期工作。上下文精化通过抽象地捕获程序的子组件的上下文来简化精化过程，该上下文通常包括关于自由变量的值的信息。本文还推广和推广了模加细。模块是对公共数据类型进行操作的过程的集合;规范模块A和实现模块C之间的模块细化允许对A的过程的调用被系统地替换为对C的相应过程的调用。基于模块细化的条件，我们提出了一种从规范模块计算实现模块的方法。上下文和模块细化内的细化演算已经从早期的工作和结果中概括了一个统一的框架。
2006-08-29 cs.LO
The mu-calculus' Alternation Hierarchy is Strict over Non-Trivial Fusion Logics
本文研究了模态 mu-演算的交替层级在非平凡融合逻辑上的严格性问题，证明了多模态 mu-演算的交替层级在模态逻辑的非平凡融合上是严格的，并讨论了其退化为模态逻辑的示例。
2025-11-04 cs.LO
Complexity results for modal logic with recursion via translations and tableaux
本文通过逻辑间翻译迁移复杂性结果，为带递归的多智能体模态逻辑构建表列系统并将其可满足性归约为μ-演算可满足性，得到通用2EXP上界。
2024-08-06 cs.LO
Labelled Sequents for Inquisitive First-Order Modal Logic
University of Padua（帕多瓦大学）
针对探究性一阶模态逻辑，提出一个完整的标记矢列演算，扩展了Litak和Sano的演算，证明了强完备性及规则可逆性和切割可容许性。
2026-07-01 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
First-Order Game Logic and Modal Mu-Calculus
本文研究了一阶博弈逻辑和一阶模态μ演算，它们用解释效果的一阶模态（如变量赋值）扩展了命题模态逻辑。不像在命题的情况下，这两个逻辑被证明具有相同的表达能力和他们的证明演算具有相同的演绎能力。两种结石也相互比较完整。在微分方程的存在下，推论获得了微分博弈逻辑（混合博弈的演绎验证逻辑）和微分μ演算（混合系统的模态μ演算）之间的可用和完整的翻译。微分μ-演算相对于一阶不动点逻辑是完备的，微分对策逻辑相对于它的无常微分的片段是完备的。
2022-02-11 cs.GT cs.LO math.LO
Size matters in the modal $μ$-calculus
我们讨论和比较复杂性措施的模态$μ$演算，专注于大小和交替深度。作为一个尺度，我们采取威尔克的交替树自动机，我们将呼吁奇偶公式在文本中。在Bruse，Friedmann和Lange的工作基础上，我们比较了$μ$ -演算公式的两种大小度量：子公式大小，即给定公式的子公式的数量，和闭包大小。这些概念对应于公式的表示，即分别基于其子公式dag和闭包图的奇偶公式。我们的方法的区别在于，我们明确了α等价的作用，因为天真地重命名绑定变量可能导致指数爆破。此外，我们匹配公式的交替深度与奇偶公式的索引。我们从一个没有阿尔法等价的环境开始。定义了子公式大小和闭包大小，并指出$μ$ -演算公式可以转化为大小线性的奇偶公式，给出了将$μ$ -演算公式转化为等价的奇偶公式的构造.相反，有一个标准的转换产生一个指数子公式的$μ$ -演算公式-但根据原始奇偶公式的大小，闭包大小是线性的。我们确定所谓的无扭奇偶公式的子公式的大小存在的变换线性。然后，我们引入大小的概念是完全不变的阿尔法等价。我们转移Bruse等人的结果，表明在我们的设置中，闭包大小也可以指数小于子公式大小。我们还展示了如何重命名绑定变量，使阿尔法等价成为语法上的封闭集的身份。最后，我们回顾了保护变换的复杂性。
2020-10-27 cs.LO
A Natural Deduction style proof system for propositional $μ$-calculus and its formalization in inductive type theories
在本文中，我们提出了一个形式化的Kozen的命题模态$μ$ -演算，在演算的归纳结构。我们解决了几个有问题的问题，如使用高阶抽象语法在归纳集合中存在的递归构造器，编码的模态（“证明”）规则和上下文敏感的语法。该编码可用于\Coq系统中，为$μ$ -演算中的无错证明的交互式开发提供了一个实验性的计算机辅助证明环境。我们采用的技术可以很容易地移植到其他语言和证明系统具有类似的问题。
1998-09-29 cs.LO
Canonicity of Proofs in Constructive Modal Logic
本文针对构造性模态逻辑中lambda演算与获胜策略间的证明等价性差距，通过扩充归约规则定义了新lambda演算，证明其规范化与合流性，并利用聚焦证明系统风格的类型系统建立了范式项与获胜策略间的一一对应关系。
2023-07-30 cs.LO
Modal Logic for Simulation, Refinement, and Mutual Ignorance
University of Toulouse CNRS, IRIT（图卢兹大学）；University of Western Australia（西澳大学）；University of Bergen（卑尔根大学）；Liverpool University（利物浦大学）
本文提出了一种基于多模态逻辑的模态逻辑，用于模拟、细化和相互无知，通过模块化的方式构建了多种逻辑体系，探讨了细化与模拟之间的关系。
2025-11-27 cs.LO
The Finite Model Property of Quasi-transitive Modal Logic
建立了准传递模态逻辑$\mathsf{K}_2^3=\mathsf{K}\oplus \Box\Box p\rightarrow \Box\Box\Box p$的有限模型性质。这种模态逻辑被保守地扩展到时态逻辑$\mathsf{Kt}_2^3$。本文提出了一个求解$\mathsf{Kt}_2^3$的Gentzen微积分$\mathsf{G}$。该演算$\mathsf{G}$通过有限的句法结构而具有有限代数性质。因此，$\mathsf{Kt}_2^3$和$\mathsf{K}_2^3$具有有限模型性质。
2019-02-22 cs.LO
Input-based Three-valued Abstraction Refinement
提出基于输入分裂的三值抽象精化（TVAR）算法框架，简化状态空间形式主义，在开源工具machine-check中实现并验证AVR架构机器码系统性质，首次将TVAR实际用于机器码验证且能处理朴素模型检查或CEGAR无法验证的场景。
2025-11-12 cs.LO
Interpolation for the two-way modal mu-calculus
本文为双向模态 μ-演算引入非良基与循环证明演算，利用迹原子应用 Vardi 自动机证明其可靠性与完备性，并据此确立 Craig 插值与 Beth 可定义性。
2025-08-11 cs.LO math.LO
Model-Checking the Higher-Dimensional Modal mu-Calculus
高维模态μ演算是μ演算的扩展，其中公式被解释为标记转换系统的状态元组。在这种逻辑中可以表达的每个属性都可以在多项式时间内进行检查，相反，每个具有互模拟不变编码到标记转换系统中的多项式时间可判定问题也可以在高维模态μ演算中定义。我们通过给出几个决策问题的例子来证明后一种联系，这些决策问题归结为对某些固定公式的高维模态μ演算的模型检验。通过这种方式，用于逻辑的通用模型检验算法然后可以经由部分评估来使用，以便获得用于这些问题的算法，这些算法可以受益于在程序验证领域中良好建立的改进，即运行中（on-the-fly）和符号技术。这项工作的目的是将这种技术扩展到其他领域，以及，在这里示例性地做了过程等价，自动机理论，解析，字符串问题，和游戏。
2012-02-16 cs.FL cs.LO
Sequent Calculi for Data-Aware Modal Logics
本文为数据感知模态逻辑HXPathD提出Gentzen式矢列演算，并给出可靠性、完备性、可逆性及切消的完整证明，作为形式结果的参考。
2025-05-22 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
Cut elimination for the alternation-free modal mu-calculus
University of Gothenburg（哥德堡大学）；University of Amsterdam（阿姆斯特丹大学）
本文为模态μ-演算的无交替片段提出一种基于循环证明系统的语法切消去过程，利用多切和良拟序理论直接将带切证明转换为无切证明并保证终止。
2026-10-23 cs.LO math.LO
Complexity through Translations for Modal Logic with Recursion
本文研究了经典模态逻辑的复杂性及其扩展与不动点算子，使用翻译转移结果跨越逻辑。特别是，我们通过翻译和从μ演算和模态逻辑，这使我们能够转移已知的上限和下限的多智能体逻辑的复杂性结果。我们还使用这些翻译介绍一个终止表系统的逻辑，我们研究的基础上，Kozen的表的μ演算，和一个拟合和Massacci模态逻辑。
2022-09-21 cs.LO
Bounded game-theoretic semantics for modal mu-calculus
我们引入了一个新的博弈论语义（GTS）的模态μ演算。我们所谓的有界GTS取代奇偶游戏与替代评估游戏，只有有限的路径出现，无限的路径是不需要的，即使当考虑的过渡系统是无限的。新的游戏提供了替代方法的各种建设的框架中的μ演算。例如，它们已经成功地用作一种方法的基础，这种方法导致逻辑的自然公式大小游戏。虽然我们的主要重点是介绍新的GTS，我们也考虑一些应用程序来演示其用途。例如，我们考虑一个自然的模型转换过程，减少模型检查游戏，检查一个单一的，固定的公式在构建的模型，我们还使用GTS识别新的替代变种的μ演算与PTime模型检查。
2020-05-21 cs.LO math.LO
Efficient Evidence Generation for Modal $μ$-Calculus Model Checking (extended version)
本文提出两步法求解带附加信息的参数化布尔方程系统，先解核心再利用信息，以高效生成模态μ演算模型检测的证据，并证明正确性及实现验证。
2025-01-27 cs.LO
Proof Theory of Riesz Spaces and Modal Riesz Spaces
本文为Riesz空间和模态Riesz空间设计超序列演算证明系统，证明可靠性、完备性和切割消去，并首次证明模态Riesz空间理论的可判定性，应用于概率程序逻辑。
2022-02-16 cs.LO
Cut-elimination for the mu-calculus with one variable
我们建立了一个变量片段的模态μ演算的语法切割消除。我们的方法是基于最近的削减消除技术的薄荷糖，利用布赫霍尔茨的欧米茄规则。
2012-02-16 cs.LO
Calculi for Intuitionistic Normal Modal Logic
本文给出了一个按名称调用和一个按值调用的项演算，它们都与直觉模态逻辑IK的盒片段有Curry-Howard对应关系。显示了结石的强归一化性和汇合性。此外，我们还定义了一个从按值调用演算到按名称调用演算的CPS转换，并证明了它的可靠性和完备性。
2016-06-10 cs.LO cs.PL
The Refinement Calculus of Reactive Systems
Refinement Calculus of Reactive Systems（RCRS）是一个用于反应式系统建模和推理的组合形式化框架。RCRS提供了一种语言，它允许描述原子组件作为符号转换系统或QTL公式，和复合组件形成使用三个原始的组合运算符：串行，并行和反馈。的语言的语义给出的单调属性Transformers器，单调谓词Transformers器，已被用来组合语义顺序程序的反应系统的扩展。RCRS允许指定安全性和活性属性。它还允许对既不确定又不接受输入的输入-输出系统进行建模（即，其可以在某些时间点拒绝某些输入），并且因此可以被视为行为类型系统。RCRS提供了一套符号计算机辅助推理的技术，包括组合静态分析和验证。RCRS带有一个公开的实现，其中包括在Isabelle证明助手中对RCRS理论的完整形式化。
2018-02-08 cs.LO cs.PL cs.SE
Denotation of syntax and metaprogramming in contextual modal type theory (CMTT)
模态逻辑S4可以通过Curry-Howard风格的对应关系来使用，以获得一个模态演算。模态（盒装）类型被直观地解释为“演算的封闭语法”。这种模式演算被称为模态类型论--这是更一般的上下文模态类型论或CMTT的基本情况。CMTT从来没有被赋予一个指称语义，其中模态类型被赋予作为封闭语法的指称。我们展示了如何确实可以做到这一点，与扭曲。我们还利用这个表示证明了系统的一些性质。
2012-02-04 cs.LO math.LO
Grammar Logics in Nested Sequent Calculus: Proof Theory and Decision Procedures
语法逻辑是指多模态逻辑K的扩展，其中模态公理从形式语法生成。我们考虑一个证明理论，在嵌套微积分，与逆，即，语法逻辑，每个模态算子[a]都有一个逆。扩展以前的作品嵌套的tense逻辑系统，我们表明所有的语法逻辑（有或没有逆）可以在嵌套的tense演算，其中的公理是内在的演算作为结构规则的形式化。这些结石的语法切割消除证明使用类似的程序显示逻辑。如果文法是上下文无关的，那么可以摆脱所有的结构规则，支持深度推理和额外的传播规则。我们给出了一个新的半决策过程的上下文无关文法逻辑，使用嵌套的深度推理演算，并表明，在给定的上下文无关文法是正规的情况下，这个过程终止。与文献中所有其他现有的决策程序的规则文法逻辑，我们的程序不假设一个有限状态自动机编码的公理。
2012-04-11 cs.LO
Formal Small-step Verification of a Call-by-value Lambda Calculus Machine
我们正式验证一个抽象的机器调用的值的alcuda演算与de Bruijn条款，简单的替代，和小步语义。我们遵循逐步改进的方法，从一个带有替换的朴素堆栈机器开始。然后，我们细化到一个具有闭包的机器，最后是一个具有为闭包提供结构共享的堆的机器。我们证明了三个细化步骤的正确性与组成小步自下而上的模拟。有一个附带的Coq开发验证所有结果。
2019-01-02 cs.LO cs.PL
Automating the Verification of Realtime Observers using Probes and the Modal mu-calculus
一个经典的方法模型检查的时间属性，如那些表示使用时间扩展的时间逻辑是依赖于使用观察员。在这种情况下，一个主要的问题是证明观察者的正确性。从本质上讲，这归结为证明：（1）每一个与属性相矛盾的轨迹都可以被观察者检测到;而且（2）观察者是无害的，这意味着它不能干扰被观察的系统。在本文中，我们描述了一种自动测试实时观测器的正确性的方法。这种方法是通过自动化通常被称为视觉验证的方法来获得的，在该方法中，通过检查其状态空间的图形表示来执行系统的正确性。我们的方法已经实现的工具蒂娜，时间Petri网的模型检查工具箱。
2015-09-22 cs.LO
The Constructive $μ$-calculus: Game Semantics and Non-Wellfounded Proof Systems
Institute of Sciece Tokyo, Japan（东京科学研究所）
本文研究基于构造模态逻辑CK的μ-演算变种，定义了游戏语义并证明其等价于双关系李普克内语义，进而利用游戏语义证明了完全标记的非良基证明系统的正确性与完备性，并探讨如何将其扩展到其他非经典模态逻辑的μ-演算。
2026-04-25 cs.LO math.LO
Some model theory for the modal $μ$-calculus: syntactic characterisations of semantic properties
本文针对模态 $\mu$-演算的若干语义性质（如连续性、完全可加性等）给出对应的语法片段刻画，证明每个性质可判定，并基于自动机理论方法实现有效转换。
2018-02-05 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
