Proof Search Specifications of Bisimulation and Modal Logics for the pi-Calculus
我们指定的操作语义和互模拟关系的有限π演算内的逻辑，其中包含的nabla量词编码通用的判断和定义编码不动点。由于我们只限于有限的情况，逻辑展开不动点的能力使得这个逻辑对于操作语义的归纳性质和互模拟的共归纳性质都是完备的。nabla量词有助于解决π演算表达式中变量范围及其执行（证明）的微妙问题。我们说明了这种逻辑所允许的逻辑规范的几个优点：它们是自然的和说明性的;它们不包含关于变量名的副条件，同时保持对这些变量的完全形式化处理;后期互模拟关系和开放互模拟关系之间的差异来自于熟悉的逻辑区别;三个量词之间的相互作用（对于所有，存在，（nabla）它们的作用域可以解释早期互模拟和晚期互模拟之间的差异以及基于约束输入和输出行为的各种模态算子之间的差异;并且涉及推理规则、统一和回溯的应用的证明搜索可以为模态逻辑中的一步转换、互模拟和满足提供完整的证明系统。我们还说明了如何可以编码的π演算与复制，在一个扩展的逻辑与归纳和共归纳。
2009-02-16 cs.LO
On Bisimulation in Absence of Restriction
我们重新审视标准的互模拟等式的过程模型的限制运营商。众所周知，一般来说，弱双相似性比强双相似性更粗糙，因为它抽象了内部动作。在没有限制的情况下，这些内部行为变得有些可见，所以人们可能会怀疑弱双相似性是否仍然是“弱”的。我们表明，在两个CCScore（即，Milner的没有$τ$ -前缀、求和和重新标记的标准CCS）及其高阶变体（命名为HOCCScore），弱双相似性确实保持弱，即，即使没有限制算子，仍然严格地比强双相似性粗糙。这些结果可以推广到其他一阶或高阶过程模型。本质上，这是由于复制操作的直接或间接存在，它可以保持进程保持其状态（即，互动能力）。凭借这些意见，我们研究了一个变种的弱双相似性，称为准强双相似性。这种准强双相似性要求内部动作的匹配以强方式进行，如强双相似性，并且可见动作的匹配没有尾随的内部动作。我们表明，在CCScore没有限制算子，弱双相似性完全崩溃到这个准强双相似性，这是此外，以符合分支双相似性。这些结果表明，在没有限制操作的情况下，弱双相似性的某些成分确实变成了强的，特别是内部动作的匹配。
2022-10-19 cs.LO
Bisimulations Meet PCTL Equivalences for Probabilistic Automata
概率自动机已成功地应用于并发和随机系统的形式化验证。有效的模型检验算法已经被研究，其中最常用的用于表达属性的逻辑是基于概率计算树逻辑（PCTL）及其扩展PCTL^*。提出了各种行为等价物，作为一个强大的工具，抽象和组合最小化的PA。不幸的是，这些等价是众所周知的合理的，但就PCTL或PCTL* 所诱导的逻辑等价而言并不完整。塞加拉在1995年指出了一个既健全又完整的行为等价的愿望，但多年来一直没有定论。在本文中，我们引入了新的概念，强互模拟关系，PCTL和PCTL* 的特点。我们扩展了弱互模拟的特点PCTL和PCTL* 没有下一个运营商，分别。此外，我们还扩展了模拟前序的框架。因此，我们的论文弥合了在这种情况下逻辑和行为等价性和前序之间的差距。
2013-06-21 cs.LO
Computing Stuttering Simulations
口吃互模拟是一个著名的行为等价，它保留了CTL-X，即没有下一次操作符X的CTL。相应地，口吃模拟前序诱导了一个更粗糙的行为等价，它保留了存在片段ECTL-{X，G}，即没有下一次X和全局G算子的ECTL。虽然口吃互模拟等价可以通过著名的Groote和Vaandrager的[1990]算法计算，但据我们所知，没有计算口吃模拟前序和等价的算法。本文针对有限状态系统提出了这样一种算法。
2009-04-09 cs.LO
Pushdown Automata and Context-Free Grammars in Bisimulation Semantics
本文在反应式图灵机及互模拟语义下，通过引入带中间接受的序列算子与状态感知概念，恢复了下推自动机与上下文无关文法之间的经典对应关系。
2023-03-01 cs.FL cs.LO
On coalgebras with internal moves
在本文的第一部分中，我们回顾了处理出现在不同的基于状态的系统语义中的所谓的不可见的转换的共代数方法。我们主张这些转移总是某个单子的单位的一部分。因此，具有内部移动的余代数恰是一元型上的余代数。本文的其余部分致力于支持我们的主张，通过研究两个重要的行为等价的基于状态的系统与内部移动，即：弱互模拟和跟踪语义。我们继续研究了富序单子上余代数的弱互模拟。在本文中使用的关键概念，并提出了我们在我们以前的工作是秩序饱和单子和饱和的概念。饱和算子可以直观地理解为自反的、传递的闭包算子。有两种方法来定义具有内部移动的余代数的饱和子。在这里，我们给出了必要条件，使他们产生相同的概念弱互模拟。最后，通过一致不动点算子给出了具有静默移动的余代数的迹语义的定义。我们比较了具有内部步骤的余代数的强、弱偏化以及迹语义。
2014-02-25 cs.LO
Proving Soundness of Extensional Normal-Form Bisimilarities
本文提出一种系统方法，证明外延范式互模拟及其上下文上至技术的可靠性，并应用于三个按值调用λ-演算，结果已在Coq中形式化。
2019-03-28 cs.LO cs.PL
Bisimulation of Labelled State-to-Function Transition Systems Coalgebraically
标号状态-函数转换系统，简称FuTS，是一般半环上的状态-函数转换系统，具有丰富的高阶算子集.因此，FuTS构成了一个方便的建模工具，以处理过程语言，特别是其定量扩展。在本文中，互模拟诱导的FuTS的概念是从一个coalgebraic的角度来看。一个对应的结果是建立说明FuTS-双相似性符合行为等价的相关函子。作为一般的例子，基本的定量过程代数的主要例子的实质性片段的等价关系到特定的FuTS的双相似性。示例范围从随机过程语言PEPA到交互式马尔可夫链语言IML、（离散）定时过程语言TPC和马尔可夫自动机语言MAL。这些语言的等效性与其特定FuTS的双相似性有关。利用对应结果，得到了这些演算等价的共代数证明。语言的具体选择，除了涵盖了大量的过程交互模型和涉及数量的建模选择，使我们能够显示不同类别的FuTS，即所谓的简单FuTS，组合FuTS，嵌套FuTS，和一般FuTS。
2015-12-21 cs.LO
Games for Topological Fixpoint Logic
拓扑不动点逻辑是一个允许拓扑模型的逻辑族，其中不动点算子是关于拓扑解释定义的。在这里，我们考虑一个拓扑不动点逻辑的关系结构的基础上石空间，不动点算子解释通过闭集。我们开发了一个博弈论的语义这个逻辑。首先介绍Stone空间上单调算子闭不动点的博弈刻画。这些不动点游戏允许我们使用两个玩家的图形游戏来描述我们的拓扑不动点逻辑的语义。这是本文的主要结果。最后，我们定义了所考虑的拓扑结构的互模拟，并使用我们的游戏语义来证明我们的拓扑不动点逻辑公式的真理是互模拟不变的。
2016-09-14 cs.GT cs.LO
Resource Bisimilarity in Petri Nets is Decidable
本文针对 Petri 网中的资源互模拟关系，提出判定算法，证明其可判定性，并给出相似但不互模拟的实例，区别于不可判定的资源相似性。
2022-10-03 cs.LO
A Polynomial Translation of pi-calculus FCPs to Safe Petri Nets
我们开发了一个多项式的翻译有限控制π演算过程安全的低级别Petri网。据我们所知，这是第一个这样的翻译。这是自然的，因为有一个密切的对应关系之间的控制流，享有互模拟的结果，并适合于实际的模型检验。
2013-09-16 cs.LO
Similarity and bisimilarity notions appropriate for characterizing indistinguishability in fragments of the calculus of relations
出于数据库中的应用，本文认为各种片段的二元关系演算。这些片段是通过省略或保留一些标准算子以及一些衍生算子如集差、投影、共投影和剩余来获得的。对于每个被认为是片段，一个表征时，两个给定的二进制关系结构是无法区分的，在该片段中的表达式。的表征是基于适当适应的概念的模拟和互模拟。
2014-03-28 cs.DB cs.LO
Reducing Higher Order Pi-Calculus to Spatial Logics
在本文中，我们表明，理论的过程可以减少到理论的空间逻辑。首先，我们提出了一种高阶π演算的空间逻辑SL，并给出了SL的推理系统。证明了SL的可靠性和不完备性。进一步证明了SL公式的结构同余关系和一步转移关系可以用SL公式的逻辑关系来描述。我们还扩展了SL公式的过程的互模拟。然后，我们扩展SL的所有定义和结果，SL的弱语义版本，称为WL。最后，我们在SL中加入了mu算子。这个新逻辑被命名为muSL。我们证明了WL是muSL的一个子逻辑，并且复制算子可以用muSL表示。
2012-11-17 cs.LO
Logics of Strong Noncontingency
受Hintikka在[8]中对疑问嵌入动词的处理和非偶然算子的变化的启发，我们提出了一种以强非偶然算子$\blacktriangle$为唯一原始模态的逻辑。如果一个命题无论为真还是为假，它都必然如此，则它是强非偶然的;否则，它是弱偶然的。此逻辑不是正常的模态逻辑，因为$\blacktriangle(ϕ\toψ)\to(\blacktriangleϕ\to\blacktriangleψ)$无效。我们比较了这种逻辑与其他逻辑，如标准模态逻辑、非偶然逻辑、本质与偶然逻辑的相对表达性，并考察了它的框架可定义性。除了这些结果，我们还提出了一个合适的概念，互模拟的逻辑强noncontingency，在此基础上，我们的特点是这种逻辑内模态逻辑和一阶逻辑。我们还公理化的逻辑强noncontingency在各种框架类。我们的工作也与[10]中一致算子的处理有关。
2015-05-15 cs.LO
Impure Simplicial Complex and Term-Modal Logic with Assignment Operators
Peking University（北京大学）
本文提出一种带有赋值运算的术语模态逻辑，用于解决不纯单纯复形中死亡智能体表达式的问题，并通过双射概念证明两种语义等价，同时提供完整的公理化体系。
2025-11-27 cs.LO cs.MA
Structure Preserving Bisimilarity, Supporting an Operational Petri Net Semantics of CCSP
1987年，Ernst-Rüdiger Olderog为CCSP的一个子集提供了一个操作Petri网语义，CCSP是Milner的CCS和Hoare的CSP的结合。它为子集中的每个过程项分配一个标记的安全位置/转换网络。为了证明该方法的正确性，Olderog建立了以下协议：（1）与CCSP的标准交织语义达到强互模拟等价，（2）与CCSP算子在Petri网方面的标准指称解释达到适当的语义等价，完全尊重网的因果结构。对于后者，他采用了线性时间语义等价，即具有相同的因果网。本文加强（2），采用这种语义的一种新的分支时间版本-结构保持双相似性-而且保持必然性。我确定这是CCSP运营商的一致性。
2015-09-19 cs.LO
Out of Control: Reducing Probabilistic Models by Control-State Elimination
国家的最先进的概率模型检查器执行验证显式状态马尔可夫模型定义在一个高层次的编程形式主义，如PRISM建模语言。通常，从这种类似于程序的规范中产生的低级模型表现出许多结构，例如重复的子模式。像概率互模拟最小化等已建立的技术能够利用这些结构;然而，它们直接在显式状态模型上操作。另一方面，通过推理高级程序来减少结构化状态空间的方法还没有被研究那么多。在本文中，我们提出了一种新的，简单的，全自动的程序级技术，以减少底层马尔可夫模型。我们的方法的目的是计算程序的控制流图中相邻位置的汇总行为，从而获得一个程序较少的“控制状态”。这种减少立即反映在程序的操作语义中，从而实现更有效的模型检验。一个关键的见解是，原则上，每个（组合）程序变量与有限域可以发挥的作用，程序计数器定义的流结构。与大多数其他减少技术不同，我们的方法是属性导向的，自然支持未指定的模型参数。实验表明，我们简单的方法产生的状态空间减少高达80%的实际相关的基准。
2021-11-12 cs.LO
A Branching Time Model of CSP
我提出了一个分支时间模型的CSP，是比迄今为止提出的所有其他模型的CSP。它是通过从线性时间分支时间谱中取一个语义等价，即保持发散的耦合相似性，并证明它是CSP算子的同余而得到的。这种等价属于语义等价的互模拟家族，在这个意义上，在没有内部动作的转换系统上，它与强双相似性相一致。然而，足够的方程法CSP仍然获得一个完整的axiomatisation封闭，递归自由条款。
2017-02-25 cs.LO
Categorical Semantics for Model Comparison Games for Description Logics
一个分类的方法来研究模型比较游戏的comonads最近发起的Abramsky等人。在这项工作中，我们分析了游戏，自然出现在描述逻辑的背景下，并补充他们与合适的游戏comonads。更确切地说，我们认为表达的子逻辑ALCSelfIbO，即，逻辑扩展ALC与任何组合的逆，名，安全的布尔角色组合，和自我运营商。我们的结构扩充和修改了Abramsky和Shah的所谓模态comonad。我们采用的方法严重依赖于相对comonads的使用，我们利用它以组合的方式在互模拟游戏中封装额外的功能。
2022-11-11 cs.LO math.CT
Induction by Coinduction and Control Operators in Call-by-Name
本文研究了在带有控制算子的按名调用语言中通过共归纳来模拟归纳。由于已知具有控制算子的按名称调用程序设计语言不能具有一般的初始代数，因此归纳和控制算子的交互作用通常限于无效应函数。我们证明了一类这样的限制归纳类型可以从全共归纳类型的控制算子的权力。作为一个典型的例子，我们的结果，自然数的类型表示的类型的流。其基本思想是这样一个事实的对应，即一些共归纳类型可以用按名称调用的纯语言中的归纳类型来表达，而不会产生副作用。
2013-09-05 cs.LO cs.PL
Complete Call-by-Value Calculi of Control Operators, I
我们给出了新的控制操作符的按值调用演算，这些控制操作符对于连续传递样式的语义是完整的。各种预期的计算性质从完整性。在一系列论文的第一部分中，我们使用连续传递风格语义以及联合交叉类型规则给出了终止属性的表征。
2021-05-02 cs.LO cs.PL
Expressive Power of One-Shot Control Operators and Coroutines
本研究采用Felleisen的宏表达性，对一次性控制操作符（如效果处理器、定界续延）与非对称协程的表达能力进行严谨比较，验证了非对称协程能宏表达前者但反之不行的结论，并修正了先前非正式论证的缺陷。
2025-09-15 cs.LO cs.PL
Proving termination of evaluation for System F with control operators
我们提出了新的证明，终止评估约简语义（即，具有显式表示求值上下文的小步操作语义）。我们介绍了一个修改版本的吉拉德的证明方法的基础上reductioncandidates，reductionpredicates定义的值和评价上下文所规定的减少语义格式。我们解决这两个流产的控制操作符（callcc）和定界控制操作符（移位和复位），我们引入新的多态类型系统，我们认为调用的值和调用的名称评估策略。
2013-09-05 cs.LO cs.PL
A General Theory of Propositional Modal Bundled Modalities
Peking University（北京大学）
本文提出捆绑模态的通用理论，通过统一的双模拟定义和凸邻域语义学，为多种捆绑模态提供了表达力和公理化方法，并实例化了几种具体捆绑模态的公理化。
2026-07-01 cs.LO
Delimited control operators prove Double-negation Shift
我们提出了一个扩展的最小的直觉谓词逻辑，基于分隔的控制运算符，可以得到的谓词逻辑版本的双否定移位模式，同时保持析取和存在属性。
2011-03-11 cs.LO math.LO
