Domain-Aware Session Types (Extended Version)
我们开发了一个泛化现有的Curry-Howard解释（二进制）会话类型依赖于线性逻辑的扩展与混合逻辑的功能，特别是模态世界，表明域。这些世界支配着域迁移，服从于模态逻辑的Kripke语义中熟悉的参数可访问性关系。其结果是一个富有表现力的新型流程框架，用于域感知、消息传递并发。它的逻辑基础确保良好类型的进程享有会话保真度、全局进展和终止。类型化还确保进程只与可访问域通信，因此尊重可访问性关系。值得注意的是，我们的域感知框架可以指定的情况下，域信息仅在运行时可用，灵活的可访问性关系可以干净地定义和静态执行。作为一个具体的应用，我们引入了域感知的多方会话类型，其中全局协议可以通过域迁移来表示任意嵌套的子协议。我们开发了一个精确的分析，这些多方协议减少到我们的二进制域感知框架：复杂的域感知协议可以推理在正确的抽象层次，也确保了原则性转移的关键正确性属性从二进制到多方设置。
2019-07-02 cs.LO
Reversing Single Sessions
基于会话的通信在实践中作为通过结构化交互开发安全通信系统的手段已经获得了广泛的接受。在本文中，我们研究这些结构化的相互作用是如何受到可逆性，它提供了一个计算模型，允许执行的相互作用被撤消的影响。特别是，我们提供了一个系统的研究，在两个二元和多方的单一会话的可逆性的不同概念的整合。考虑的可逆性形式是：一个是用一个向后的步骤完全反转给定的会话，另一个是用一个向后的步骤或多个步骤恢复会话的任何中间状态。我们分析了在所有这些不同的设置中逆转会话的成本。我们的研究结果表明，扩展二进制单会话多方的不影响可逆性机械及其成本。
2016-04-08 cs.LO cs.PL
Session Types for Orchestrated Interactions
在设置的π演算与二进制会话，我们的目标是放松的概念，会话类型的对偶性的概念，可伸缩的遵守合同理论。这导致使用“推测选择”的新类型操作符扩展会话类型，包括不一定由兼容伙伴提供的选择。我们解决的问题，选择成功的通信分支机构的操作语义的基础上orchestration，这已被证明是等同于合同的可伸缩语义，但显然更可行。因此，提供了一种类型系统，相对于这样的语义是合理的。
2017-11-30 cs.LO
Timeout Asynchronous Session Types: Safe Asynchronous Mixed-Choice For Timed Interactions
本文提出 TOAST，通过时间约束安全支持异步会话类型中的混合选择，并给出具备进程计时器、可建模 receive-after 超时模式的演算及主体归约证明。
2025-07-21 cs.LO
Fair Termination of Asynchronous Binary Sessions
本文提出基于线性逻辑的异步会话类型理论，利用新颖的公平异步子类型关系保证良类型进程在公平性假设下公平终止，实现无饥饿与无孤儿消息。
2025-03-14 cs.DC cs.LO cs.PL
On the Expressiveness of Mixed Choice Sessions
会话类型为结构化交互提供了灵活的编程风格，并用于保证分布式进程的安全和一致的组合。传统会话类型仅包括单向输入（外部）和输出（内部）保护选择。这阻止了会话进程探索pi演算的全部表达能力，其中混合选择被证明比（非混合）保护选择更具表达力。为了解决这个问题，最近Casal，Mordido和Vasconcelos提出了混合选择的二进制会话类型（CMV+）。本文进行了一个令人惊讶的，不幸的结果CMV+：尽管包括不受限制的渠道与混合选择，CMV+的混合选择是相当独立的，而不是混合。我们证明了这一负面结果使用两种方法（使用领导选举问题或同步模式作为显着特征），表明不存在良好的编码从π演算到CMV+，保持分布。然后，我们关闭他们的开放问题上的编码从CMV+到CMV（没有混合选择），证明其合理性，从而编码是好的耦合相似性。
2022-09-06 cs.LO
On the Expressiveness of Mixed Choice Sessions (Technical Report)
会话类型为结构化交互提供了灵活的编程风格，并用于保证分布式进程的安全和一致的组合。传统的会话类型仅包括单向输入（外部）和输出（内部）保护选择。这阻止了会话进程探索pi演算的全部表达能力，其中混合选择被证明比（非混合）保护选择更具表达力。为了解决这个问题，最近Casal，Mordido和Vasconcelos提出了混合选择的二进制会话类型（CMV+）。本文进行了一个令人惊讶的，不幸的结果CMV+：尽管包括不受限制的渠道与混合选择，CMV+的混合选择是相当独立的，而不是混合。我们证明了这一负面结果使用两种方法（使用领导选举问题或同步模式作为显着特征），表明不存在良好的编码从π演算到CMV+，保持分布。然后，我们关闭他们的开放问题上的编码从CMV+到CMV（没有混合选择），证明其合理性，从而编码是好的耦合相似性。本技术报告是EXPRESS/SOS'22研讨会上发表的一篇论文的延伸。
2022-08-15 cs.LO
Using Session Types for Reasoning About Boundedness in the Pi-Calculus
深度有界和名称有界过程的类是π演算的片段，其中一些对于完整演算不可判定的决策问题变得可判定。P是深度有界的，如果每一个减少序列P包含后继进程与最多k个积极的嵌套限制。P是k级名有界的，如果P的每个约简序列包含至多k个活动有界名的后继过程。这些进程类的成员是不可判定的。在本文中，我们使用二进制会话类型来决定两个类型系统，给出了一个健全的特性：如果一个进程是良好的类型在我们的第一个系统，它是深度有界的。如果一个进程在我们的第二个更严格的类型系统中是良好类型的，它也将是名称绑定的。
2017-09-04 cs.LO
Context-Free Session Types for Applied Pi-Calculus
我们提出了一个二进制会话类型系统，使用上下文无关的会话类型的一个版本的应用π演算的阿巴迪等。al.，其中只能发送基本项、常量和通道。会话类型类似于BPA的过程术语，我们使用互模拟等价来表征类型等价。我们提出了一个定义在类型等价类上的约束类型系统，其中类型等价被构建到类型系统中。这两种类型的系统满足一般的健全性属性，这是建立一个呼吁通用会话类型系统的PSI演算。
2018-08-27 cs.LO cs.PL
UMB: A Unified Markov Binary Format for Probabilistic Model Checking (extended version)
Brno University of Technology（布尔诺工业大学）；University of Twente（特温特大学）；Utah State University（犹他州立大学）；Radboud University（拉德堡德大学）；Lancaster University Leipzig（兰开斯特大学莱比锡分校）；University of Oxford（牛津大学）；RWTH Aachen University（亚琛工业大学）；Ruhr-University Bochum（鲁尔大学波鸿分校）
提出UMB格式，一种高效、可扩展的显式状态文件格式，用于表示多种概率系统，解决低层模型交换问题，已被主流工具采用并提供Python库支持。
2026-06-17 cs.LO
MSO+nabla is undecidable
本文是关于满二叉树上一元二阶逻辑的一个推广，它有一个量词表示“几乎必然分支π \in {0，1}^w满足一个公式<$（π <$'”.这种逻辑是由Michalewski和Mio引入的;我们按照Shelah和Lehmann的符号称之为MSO+nabla。逻辑MSO+nabla包含许多定性概率形式，包括定性概率CTL，概率LTL或具有概率接受条件的奇偶树自动机。我们表明，它是不可判定的检查，如果一个给定的句子MSO+nabla是真的，在整个二叉树。
2019-04-29 cs.LO
Weighted Positive Binary Decision Diagrams for Exact Probabilistic Inference
Radboud University Nijmegen（拉德堡德大学奈梅亨分校）
最近的工作加权模型计数已非常成功地应用于贝叶斯网络的概率推理问题。概率分布被编码成布尔范式并编译成目标语言，以便更有效地表示条件概率之间表达的局部结构。我们表明，进一步的改进是可能的，通过利用知识，在编码阶段丢失，并将其纳入编译器的启发可满足性模理论。变量之间的约束被用作背景理论，这使我们能够优化香农分解。我们提出了一种新的语言，称为加权正二进制决策图，通过使用这种分解变体，以减少尺寸的算术电路，从而降低概率推理的成本。
2016-10-18 cs.AI cs.LO
Type-checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion
我们提出了第一个会话类型系统，保证可能非终止通信进程的请求-响应活性属性。这些类型用一组所需的响应来扩充标准二进制会话类型的分支和选择类型，这表明每当选择特定标签时，最终也必须选择一组其他标签，即其响应。我们证明，这些扩展类型是严格的表达比标准的会话类型。我们提供了一个类型系统的过程演算类似于一个子集的内部（基于数据）和外部（基于事件）分支，消息传递，有界和无界循环的协作BPMN流程。我们证明了这个类型系统是合理的，即，它保证了无死锁进程的请求-响应活性。我们在一个无限状态系统的具体例子上说明了微积分和类型系统的使用。
2016-01-05 cs.LO
A Message-Passing Interpretation of Adjoint Logic
我们提出了一个系统的会话类型的基础上，伴随逻辑，推广标准的二进制会话类型。我们的系统允许我们统一捕获异步消息传递通信空间中的几个新行为，包括多播，其中一个进程向多个客户端发送单个消息，可复制服务，具有多个客户端并按需复制自己以处理来自这些客户端的请求，以及取消，其中进程丢弃通道而不沿其通信。我们为该系统提供会话保真度和无死锁结果，然后我们从中导出逻辑上合理的垃圾回收形式。
2019-04-02 cs.LO cs.PL
Correctly Communicating Software: Distributed, Asynchronous, and Beyond (extended version)
本论文以会话类型的逻辑基础为核心，研究如何在保证正确性的前提下扩展二元与多方会话类型的表达力及适用范围，以支撑分布式异步消息传递软件的可靠验证。
2024-03-01 cs.LO
Forwarders as Process Compatibility, Logically
会话类型定义进程在通信时必须遵循的协议。二元会话类型的特殊情况，即双方之间协议的类型注释，已知与线性逻辑处于命题类型对应关系中。在以前的工作中，我们已经表明，泛化到多方会话类型可以表示一致性证明或仲裁器，根据给定的协议转发消息作为中间件的过程。在本文中，按照命题作为类型的方式，我们推广到一个逻辑，我们称之为转发逻辑，一个片段的经典线性逻辑仍然满足割消。我们的主要结果总结如下：转发器推广一致性，并给出了一个优雅的证明理论的多方兼容性，并发系统的属性，保证所有发送的消息最终收到，没有死锁发生的表征。
2021-12-14 cs.LO cs.PL
Decision Questions for Probabilistic Automata on Small Alphabets
研究一元和二元概率有限自动机的空性与$\lambda$-可达性问题，根据歧义度和字母表大小刻画其复杂度，揭示了多项式与有限歧义下的NP困难性及EXPTIME可解性。
2023-12-20 cs.FL cs.LO
