A Distribution Law for CCS and a New Congruence Result for the pi-calculus
我们给出了一个公理化的强双相似CCS的一个小片段，不具有总和运算符。这个公理化，然后用来推导出在有限的π演算的强双相似性的同余在没有和。据我们所知，这是唯一的非平凡的子演算的pi演算，包括完整的输出前缀和强双相似性是一个同余。
2008-05-14 cs.LO
A more general categorical framework for congruence of applicative bisimilarity
我们证明了一个一般的同余结果，在高阶语言的双相似性，概括以前的工作，以指定的语言标记的过渡系统中，程序可能会出现标签，并可能依赖于操作的其他捕获避免替代。这是PCF，$λ$ -具有分隔延续的演算，以及高阶过程演算中的早期风格的双相似性的典型情况。
2023-03-21 cs.LO math.CT
On characterising strong bisimilarity in a fragment of CCS with replication
我们提供了一个强的双相似性的CCS片段，只包含前缀，平行组成，同步和有限的复制形式的表征。这种表征不是一种公理化，而是作为一种重写系统呈现。我们讨论了我们的方法如何使我们能够得到一个新的同余结果在$π$演算：同余持有的子演算，不包括限制，也不和，并具有有限形式的复制。我们还没有正式确定后一种结果的所有细节。
2008-10-12 cs.LO
On the Axiomatisation of Branching Bisimulation Congruence over CCS
在本文中，我们调查的方程理论（限制，重新标记，和递归自由片段）CCS模扎根分支双相似性，这是一个经典的，基于bisimulation的概念等价的抽象过程中的行为从内部计算步骤。首先，我们证明了CCS不是基于模所考虑的同余。作为一个关键步骤的独立利益的证明，否定的结果，我们证明了每个CCS进程有一个独特的并行分解成不可分解的过程模分支双相似性。作为第二个主要贡献，我们表明，当一组行动是有限的，根分支双相似性有一个有限的方程基础上CCS丰富的左合并和通信合并运营商从ACP。
2022-06-28 cs.LO
Abstract Congruence Criteria for Weak Bisimilarity
我们介绍了三个一般的组合性标准操作语义，并证明，当所有三个都满足在一起，他们保证弱互模拟是一个同余。我们的工作是建立在图里和Plotkin的数学操作语义和弱互模拟的Brengos的共代数方法。我们用各种成功和失败的例子来证明每个标准，并与Bloom和van Glabbeek的简单WB酷规则格式建立正式联系。此外，我们表明，这三个标准诱导宽松的模型在这个意义上的Bonchi等人。
2021-10-13 cs.LO math.CT
Upper-Expectation Bisimilarity and Real-valued Modal Logics
概率非确定性转移系统的互模拟关系的几个概念已被认为是在文献中。我们认为一种新的基于测试的行为等价称为上期望双相似性，并开发其理论使用线性代数和功能分析的标准结果。我们表明，对于广泛的一类系统，我们的新概念与Segala的凸双相似性相吻合。我们开发的表达概率模态μ-演算和一种新的实值模态逻辑的逻辑刻画。我们证明了上期望双相似性是一个同余的过程代数指定的概率GSOS规则格式的广泛的家庭。
2013-10-02 cs.LO
Compositional Net Semantics up to Step Net Bisimilarity
步网双相似性\cite{Gor23}是有限Petri网的一个真正并发的行为等价，它是标准步网双相似性\cite{NT84}在Petri网上的光滑推广，但具有关联标记（仅相同大小）产生相同的事件偏序的性质.进程代数FNM \cite{Gor17}真实地表示所有（且仅）有限Petri网，直到同构。我们证明了步网双相似是一个同余w.r.t.这样，我们就为所有的有限Petri网类定义了一个完全尊重因果关系和系统分支结构的合成语义。
2023-01-28 cs.LO
Expected-Delay-Summing Weak Bisimilarity for Markov Automata
一个新的弱互模拟语义定义的马尔可夫自动机，除了抽象的内部行动，总结了连续的指数分布的延迟可能交织在一起的内部行动的期望值。由此产生的等价证明是一个同余相对于并行组成的马尔可夫自动机。此外，它原来是可比的弱双相似定时标记的过渡系统，从而构成了一个步骤，调和的语义随机时间和确定性时间。
2015-09-29 cs.LO
A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic
本文提出直觉主义模态逻辑$\mathcal{OM}$刻画开放互模拟，通过模态在代换下封闭实现直觉主义遗传性，并在Abella中机械化验证可靠性，同时给出生成区分公式的算法。
2021-08-09 cs.LO
Lean and Full Congruence Formats for Recursion
在本文中，我区分两个（前）同余的要求，语义等价和前序的过程中给出的封闭条件的系统描述语言与递归结构。当用等价的替换替换过程的闭子表达式时，精益同余保持等价。此外，完全全等允许子表达式的递归规范内的替换，所述子表达式可以包含绑定在这些子表达式外部的递归变量。我建立了双相似性是一个精益（前）的所有语言的递归一致的结构操作语义在ntyft/ntyxt格式。此外，它是tyft/tyxt格式的完全一致。
2017-04-11 cs.LO
A Fully Abstract Semantics for Value-passing CCS for Trees
本文提供了一个完全抽象的语义值传递CCS树（VCCTS）。的操作语义给出了一个减少语义和标记的过渡语义。带标签的转换语义是非顺序的，允许多个动作同时发生。通过引入弱倒钩同余和弱双相似性，发展了行为等价理论。特别是，我们证明了弱倒钩同余符合弱双相似的图像有限的过程。这是具有树结构的并发模型的第一个这样的结果。该系统可以很自然地对分布式系统进行建模，并给出了一些例子来说明这一点。
2016-07-01 cs.LO
Compositionality of Approximate Bisimulation for Probabilistic Systems
使用规则格式ntmuft-ntmuxt的概率转换系统规范为Segala型系统提供了结构操作语义，并保证概率双相似性是一个同余。概率双相似性在许多应用中对跃迁的精确概率过于敏感。近似互模拟提供了一个强大的语义，是稳定的概率行为的实现和测量误差。我们提供了一个通用的方法来量化多少进程组合子扩展近似互模拟距离。作为一个直接的应用程序，我们得到一个适当的规则格式，保证组合性方面的近似双相似性。此外，我们描述了如何规范格式的非标准组合性要求可能会得出。
2013-07-29 cs.LO
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
On Barbs and Labels in Reactive Systems
反应式系统（RS）表示一个元框架，旨在为那些由归约规则提供操作语义的计算形式主义导出行为一致性。RS被证明是一种灵活的规范设备，但到目前为止，大多数处理其行为语义的努力都集中在同素推出（IPO）和饱和（也称为动态）互模拟上。在本文中，我们介绍了一种新的，中间的行为等价：L-双相似性，这是能够重铸其IPO和饱和的同行。的等价性是参数的一组L的RS标签，它表明，在温和的条件下L，它确实是一个同余。此外，L-双相似性还可以改写RS的倒钩语义的概念，这是由同一作者在以前的论文中提出的。为了提供一个合适的测试床，我们实例化我们的建议，解决（异步）CCS的语义和演算的移动环境。
2010-02-15 cs.LO
Modal Reasoning = Metric Reasoning, via Lawvere
分级模态类型、系统和协同效应正在成为处理上下文相关计算的标准形式，其中代码使用起着核心作用。然而，模态语言和协同语言的程序等价理论，如果与这些语言的指称语义和操作语义相比，则相当不发达。这就提出了一个问题，即普通程序等价的理论在多大程度上可以在模态场景中给出。在这项工作中，我们表明，共归纳等价可以扩展到一个模态设置，我们这样做，通过推广阿布拉姆斯基的应用双相似coeffective行为。为了实现这一目标，我们开发了一个通用的理论，三元程序关系的基础上的新概念的comonadic宽松的扩展，在此之上，我们定义了一个模态扩展的Abramsky的应用bisimilarity（我们称之为模态应用bisimilarity）。我们证明这样的关系是一个一致性，这种方式获得一个组合技术推理模态和coeffective行为。但这并不是故事的结束：我们还建立了模态程序关系和程序距离之间的对应关系。这种对应关系表明模态应用双相似性和（适当扩展的）应用双相似性距离一致，这种方式揭示了模态程序等价性和程序距离只是同一枚硬币的两面。
2021-03-05 cs.LO
On Coinductive Equivalences for Higher-Order Probabilistic Functional Programs (Long Version)
我们研究互模拟和上下文等价的概率$λ$演算。本文的贡献有三个方面。首先，我们展示了一种证明概率应用双相似同余的技术。虽然该技术遵循豪的方法，但一些技术细节是完全不同的，依赖于实数集的非平凡“解开”属性。其次，我们表明，虽然双相似性是在一般情况下严格比上下文等价，这两个关系之间的重合达到纯$λ$ -条款。由此产生的等式是由Levy-Longo树诱导的等式，通常被认为是在懒惰制度下纯$λ$ -项上的最好的扩展等价。最后，我们推导出一个共归纳特征的上下文等价的整个概率语言，通过一个扩展，其中条款类似于分布可能会出现在redex的位置。扩展的另一个动机是它的操作语义允许我们实验不同的一致性技术，即逻辑双相似性。
2013-11-07 cs.LO cs.PL
Modeling and Reasoning About Wireless Networks: A Graph-based Calculus Approach
我们提出了一个基于图的过程演算的建模和推理无线网络与本地广播。图在语法层次上用来描述网络的拓扑结构。这种演算配备了一个减少语义和标记的过渡语义。前者用于定义弱倒钩同余。后者是用来定义一个参数化的弱互模拟强调的位置和本地广播。证明了弱双相似蕴涵弱倒钩同余。通过一些例子和两个案例研究说明了潜在的应用。
2017-06-16 cs.LO
Compositional Semantics of Finite Petri Nets
本文针对有限 Petri 网，证明保结构互模拟关于 FMN 算子为同余，并给出尊重因果性与分支结构的组合语义及可靠公理化基础。
2023-08-17 cs.LO
Reactive Bisimulation Semantics for a Process Algebra with Time-Outs
本文介绍了带有超时变迁的标号变迁系统的强双相似性的对应。它支持这一概念，通过一个模式的特点，一个标准的进程代数与递归的同余结果，和一个完整的axiomatisation。
2023-01-24 cs.LO
A Lumpability-Driven Taxonomy of Strong and Weak Stochastic Bisimilarities with Their Congruence Properties
Università di Udine（乌迪内大学）；Università di Napoli Federico II（那不勒斯费德里科二世大学）；Università di Urbino（乌尔比诺大学）；Università Ca’ Foscari, Venezia（威尼斯卡福斯卡里大学）
本文统一了PEPA中基于CTMC可聚类性的六种随机互模拟，建立包含关系分类法，并分析其同余性质。
2026-09-11 cs.LO
Divide and Congruence III: From Decomposition of Modal Formulas to Preservation of Stability and Divergence
在两个较早的文件，我们推导出同余格式关于弱语义的转换系统规范的基础上的模态公式的分解方法。其思想是，语义的一致格式必须确保该语义的模态表征中的公式总是被分解为再次处于该模态表征中的公式。到目前为止，强加在许多已知的弱语义上的稳定性和发散性要求已经超出了这种方法的范围。稳定性是指不存在$τ$ -转变。我们展示了，使用分解方法，同余格式可以放松弱语义，是稳定的尊重。例如，这种放松将优先级算子带入了尊重稳定性的分支互模拟格式的范围内。发散，这是指存在一个无限序列的$τ$ -跃迁，逃避归纳分解方法。我们绕过这个问题，证明了一个稳定的弱语义的同余格式也是一个同余格式，其分歧保持对应。
2019-08-19 cs.LO
Value-passing CCS for Trees: A Theory for Concurrent Systems
本文将树的CCS理论（CCTS）扩展到值传递CCTS（VCCTS），其中符号具有接收和发送数据值的能力，并以操作的方式提出了一种非顺序语义。在这个并发模型中，定义了弱倒钩同余和局部早期弱双相似，并证明了后者的关系足以证明前者。作为VCCTS潜在应用的一个例证，给出了一个以C/C++并发为核心的玩具多线程程序设计语言的VCCTS语义;给出了一个基于VCCTS操作语义的松弛内存模型的形式化描述，并证明了VCCTS的DRF-保证性质.
2016-04-24 cs.LO
SOS-based Modal Decomposition on Nondeterministic Probabilistic Processes
我们提出基于SOS的模态分解方法，将非确定性概率过程的公式满足问题简化为子过程验证，并引入类似SOS机制处理概率行为，从而获得概率双相似性等关系的（预）同余格式。
2018-06-22 cs.LO
RPO, Second-order Contexts, and Lambda-calculus
首先，我们扩展了Leifer-Milner RPO理论，给出了获得IPO标记的过渡系统（和双相似性）的一般条件，减少了一组过渡，并可能出现分支。此外，我们还研究了Leifer-Milner理论的弱变体，给出了弱双相似是同余的一般条件。然后，我们将这种扩展的RPO技术应用到具有懒惰和按值调用的Reduction策略的λ演算中。我们表明，相反的过程演算，可以直接处理的λ演算语法和应用Leifer-Milner技术一类的背景下，只要我们的工作框架中的弱双相似性。然而，即使在具有最小上下文的转换系统的情况下，所得到的双相似性也是无限分支的，这是因为在标准上下文范畴中，参数规则（如beta规则）只能由无限多个基本规则表示。为了克服这个问题，我们引入了二阶上下文范畴的一般概念。我们表明，通过在这种情况下进行RPO建设，懒惰的观测等价可以被捕获为一个弱的双相似等价的一个分支过渡系统。这个结果是通过考虑组合逻辑中的一种编码来实现的。
2009-08-06 cs.LO cs.PL
