Annabelle McIver, Tahiry Rabehaja, Georg Struth
We provide an extension of concurrent Kleene algebras to account for probabilistic properties. The algebra yields a unified framework containing nondeterminism, concurrency and probability and is sound with respect to the set of probabilistic automata modulo probabilistic simulation. We use the resulting algebra to generalise the algebraic formulation of a variant of Jones' rely/guarantee calculus.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
We give a new true-concurrent model for probabilistic concurrent Kleene algebra. The model is based on probabilistic event structures, which combines ideas from Katoen's work on probabilistic concurrency and Varacca's probabilistic prime event structures. The event structures are compared with a true-concurrent version of Segala's probabilistic simulation. Finally, the algebraic properties of the model are summarised to the extent that they can be used to derive techniques such as probabilistic rely/guarantee inference rules.
Concurrent Kleene Algebra (CKA) extends basic Kleene algebra with a parallel composition operator, which enables reasoning about concurrent programs. However, CKA fundamentally misses tests, which are needed to model standard programming constructs such as conditionals and $\mathsf{while}$-loops. It turns out that integrating tests in CKA is subtle, due to their interaction with parallelism. In this paper we provide a solution in the form of Concurrent Kleene Algebra with Observations (CKAO). Our main contribution is a completeness theorem for CKAO. Our result resorts on a more general study o…
Concurrent Kleene Algebra (CKA) is a recently proposed algebraic structure by Hoare and collaborators that unifies the laws of concurrent programming. The unifying power of CKA rests largely on the so-called exchange law that describes how concurrent and sequential composition operators can be interchanged. Based on extensive theoretical work on true concurrency in the past, this paper extends Gischer's pomset model with least fixed point operators and formalizes the program refinement relation by Ésik's monotonic bijective morphisms to construct a partial order model of CKA. The existence of …
Concurrent Kleene Algebra is an elegant tool for equational reasoning about concurrent programs. An important feature of concurrent programs that is missing from CKA is the ability to restrict legal interleavings. To remedy this we extend the standard model of CKA, namely pomsets, with a new feature, called boxes, which can specify that part of the system is protected from outside interference. We study the algebraic properties of this new model. Another drawback of CKA is that the language used for expressing properties of programs is the same as that which is used to express programs themsel…
We reconstruct Peleg's concurrent dynamic logic in the context of modal Kleene algebras. We explore the algebraic structure of its multirelational semantics and develop an abstract axiomatisation of concurrent dynamic algebras from that basis. In this axiomatisation, sequential composition is not associative. It interacts with concurrent composition through a weak distributivity law. The modal operators of concurrent dynamic algebra are obtained from abstract axioms for domain and antidomain operators; the Kleene star is modelled as a least fixpoint. Algebraic variants of Peleg's axioms are sh…
We show how concurrent quantales and concurrent Kleene algebras arise as convolution algebras $Q^X$ of functions from structures $X$ with two ternary relations that satisfy relational interchange laws into concurrent quantales or Kleene algebras $Q$. The elements of $Q$ can be understood as weights; the case $Q=\bool$ corresponds to a powerset lifting. We develop a correspondence theory between relational properties in $X$ and algebraic properties in $Q$ and $Q^X$ in the sense of modal and substructural logics, and boolean algebras with operators. As examples, we construct the concurrent quant…
We introduce partially observable concurrent Kleene algebra (POCKA), an algebraic framework to reason about concurrent programs with control structures, such as conditionals and loops. POCKA enables reasoning about programs that can access variables and values, which we illustrate through concrete examples. We prove that POCKA is a sound and complete axiomatisation of a model of partial observations, and show the semantics passes an important check for sequential consistency.
Concurrent Kleene Algebra (CKA) is a mathematical formalism to study programs that exhibit concurrent behaviour. As with previous extensions of Kleene Algebra, characterizing the free model is crucial in order to develop the foundations of the theory and potential applications. For CKA, this has been an open question for a few years and this paper makes an important step towards an answer. We present a new automaton model and a Kleene-like theorem that relates a relaxed version of CKA to series-parallel pomset languages, which are a natural candidate for the free model. There are two substanti…
A Decision Procedure for Probabilistic Kleene Algebra with Angelic Nondeterminism
本文针对Ong、Ma和Kozen（2025）提出的带天使非确定性的概率Kleene代数，给出了其等式理论的判定过程及正确性证明。
In this paper we present a detailed proof of an important result of algebraic logic: namely that the free commutative Kleene algebra is the space of semilinear sets. The first proof of this result was proposed by Redko in 1964, and simplified and corrected by Pilling in his 1970 thesis. However, we feel that a new account of this proof is needed now. This result has acquired a particular importance in recent years, since it is a key component in the completeness proofs of several algebraic models of concurrent computations (bi-Kleene algebra, concurrent Kleene algebra...). To that effect, we p…
Kleene algebra with tests (KAT) is an algebraic framework for reasoning about the control flow of sequential programs. Generalising KAT to reason about concurrent programs is not straightforward, because axioms native to KAT in conjunction with expected axioms for concurrency lead to an anomalous equation. In this paper, we propose Kleene algebra with observations (KAO), a variant of KAT, as an alternative foundation for extending KAT to a concurrent setting. We characterise the free model of KAO, and establish a decision procedure w.r.t. its equational theory.
A Unifying Categorical View of Nondeterministic Iteration and Tests
本文从范畴论视角分离并分析Kleene迭代，提出含余积与测试的Kleene迭代范畴，证明其兼容异常、存储、并发等特性，并将自由模型刻画为非确定性有理树。
Jones' rely-guarantee calculus for shared variable concurrency is extended to include probabilistic behaviours. We use an algebraic approach which combines and adapts probabilistic Kleene algebras with concurrent Kleene algebra. Soundness of the algebra is shown relative to a general probabilistic event structure semantics. The main contribution of this paper is a collection of rely-guarantee rules built on top of that semantics. In particular, we show how to obtain bounds on probabilities by deriving rely-guarantee rules within the true-concurrent denotational semantics. The use of these rule…
Weighted programs generalize probabilistic programs and offer a framework for specifying and encoding mathematical models by means of an algorithmic representation. Kleene algebra with tests is an algebraic formalism based on regular expressions with applications in proving program equivalence. We extend the language of Kleene algebra with tests so that it is sufficient to formalize reasoning about a simplified version weighted programs. We introduce relational semantics for the extended language, and we generalize the relational semantics to an appropriate extension of Kleene algebra with tes…
Generalised Möbius Categories and Convolution Kleene Algebras
本文提出广义莫比乌斯范畴与经典星定义的结合，用于构建卷积克里勒代数，应用于程序验证和高维重写中的代数推理。
Algebraic coherent confluence and higher globular Kleene algebras
本文提出高阶球形克莱尼代数，将合流形式化扩展至相干合流证明，通过等式推理得到相干Church-Rosser定理与Newman引理，并应用于多面图建模的高阶重写系统。
The Nature of Concurrency
本研究基于真并发进程代数的最新成果，阐明交错并发与真并发的关系，给出事件结构、Petri网等真并发模型的进程代数基础。
Probabilistic game structures combine both nondeterminism and stochasticity, where players repeatedly take actions simultaneously to move to the next state of the concurrent game. Probabilistic alternating simulation is an important tool to compare the behaviour of different probabilistic game structures. In this paper, we present a sound and complete modal characterisation of this simulation relation by proposing a new logic based on probabilistic distributions. The logic enables a player to enforce a property in the next state or distribution. Its extension with fixpoints, which also charact…
Reasoning about distributive laws in a concurrent refinement algebra
本文聚焦并发细化代数，通过支持有限与无限行为实现完全正确性，提出并证明了作为等式的强分配律，用于分配 rely/guarantee 命令并处理并发程序的数据细化。
Probabilistic model checking for stochastic games enables formal verification of systems that comprise competing or collaborating entities operating in a stochastic environment. Despite good progress in the area, existing approaches focus on zero-sum goals and cannot reason about scenarios where entities are endowed with different objectives. In this paper, we propose probabilistic model checking techniques for concurrent stochastic games based on Nash equilibria. We extend the temporal logic rPATL (probabilistic alternating-time temporal logic with rewards) to allow reasoning about players wi…
Restructuring a concurrent refinement algebra
本文重构支持 rely/guarantee 推理的并发精化代数，统一其 quantale/biquantale 结构并强化交换与分配性质，且在 Isabelle/HOL 中实现。
The well-known process algebras, such as CCS, ACP and $π$-calculus, capture the interleaving concurrency based on bisimilarity semantics. We did some work on truly concurrent process algebras, such as CTC, APTC and $π_{tc}$ , capture the true concurrency based on truly concurrent bisimilarities, such as pomset bisimilarity, step bisimilarity, history-preserving (hp-) bisimilarity and hereditary history-preserving (hhp-) bisimilarity. Truly concurrent process algebras are generalizations of the corresponding traditional process algebras. In this book, we introduce probabilism into truly concurr…
Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
本文提出概率并发结果逻辑（pcOL），用于描述并发和概率程序中变量的联合分布，并通过案例分析推导精确信息，证明无界循环的几乎确定终止。
Truly concurrent process algebras are generalizations to the traditional process algebras for true concurrency, CTC to CCS, APTC to ACP, $π_{tc}$ to $π$ calculus, APPTC to probabilistic process algebra. And we also did some work on reversible process algebra and probabilistic truly concurrent process algebra. In this book, we utilize reversible truly concurrent process algebras APRTC and probabilistic process algebra APPTC to model quantum computing and unify quantum and classical computing.
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
提出Coneris，首个高阶并发分离逻辑，通过随机逻辑原子性支持并发概率程序的错误概率界模块化推理，并在Rocq和Iris中机械化验证。
Denotational Semantics for Probabilistic and Concurrent Programs
本文针对兼具概率动作与并行组合的命令式程序，提出具有良好域论性质的指称模型，并通过两个适当性定理证明其统一涵盖并发与概率非确定语义。
Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity
该研究提出可对含概率分支的未解释命令式程序推理的ProbGKAT框架，给出其操作语义、互模拟的完备Salomaa式公理化，并证明可通过通用划分求精算法在O(n³ log n)时间内判定其互模拟性。
Truly concurrent process algebras are generalizations to the traditional process algebras for true concurrency, CTC to CCS, APTC to ACP, $π_{tc}$ to $π$ calculus , APPTC to probabilistic process algebra. And we also did some work on reversible process algebra and probabilistic truly concurrent process algebra. In this book, we utilize reversible truly concurrent process algebras APRTC and APPTC to model quantum computing and unify quantum and classical computing.
Probability and Angelic Nondeterminism with Multiset Semantics
针对幂集与Giry单子间缺乏分配律的问题，提出带天使型非确定性的概率克林代数及自动机类，用多重集分布实现语义，得出克林定理、余代数理论等关键结果，解决理论障碍。
A Unifying Approach to Probabilistic Testing Equivalences
本文提出一种统一的概率测试等价性方法，通过新的分布语义和概率测试框架，研究了内部和外部测试等价性，扩展了经典公平/应等价和可能等价，并证明其为同余关系，通过pCSP模型案例展示了方法的灵活性。
We present Polaris, a concurrent separation logic with support for probabilistic reasoning. As part of our logic, we extend the idea of coupling, which underlies recent work on probabilistic relational logics, to the setting of programs with both probabilistic and non-deterministic choice. To demonstrate Polaris, we verify a variant of a randomized concurrent counter algorithm and a two-level concurrent skip list. All of our results have been mechanized in Coq.
An adequacy theorem between mixed powerdomains and probabilistic concurrency (extended version)
本文为概率GCL的并发扩展建立了基于混合幂域的充分性定理，通过拓扑化König引理证明，并应用于可半判定性，回应Escardó猜想。
An Adequacy Theorem Between Mixed Powerdomains and Probabilistic Concurrency
本文基于混合幂域构建概率GCL并发扩展的指称语义，提出借助拓扑空间开集思想表述的适配性定理，其证明依赖概率编程下Kőnig引理的拓扑推广，可推导出并发程序可观测性质的半可判定性，关联Escardo的相关猜想。
Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)
本文提出Foxtrot，首个用于证明高阶并发概率程序上下文细化的高阶分离逻辑，结合了并发推理原理与概率推理原理，展示了其在对抗性von Neumann硬币和Sodium加密库中的应用。
Concurrent stochastic games (CSGs) are an ideal formalism for modelling probabilistic systems that feature multiple players or components with distinct objectives making concurrent, rational decisions. Examples include communication or security protocols and multi-robot navigation. Verification methods for CSGs exist but are limited to scenarios where agents or players are grouped into two coalitions, with those in the same coalition sharing an identical objective. In this paper, we propose multi-coalitional verification techniques for CSGs. We use subgame-perfect social welfare (or social cos…
Continuous Algebras with Hypotheses
本文提出一个统一的框架，涵盖Kleene代数的各种变体以及正则树语言，通过考虑由完全格有序的代数，其中可以计算最小固定点，并提供一个由封闭语言组成的标准模型，证明其在所有连续模型上都是正确且完整的。此外，本文研究了准等式公理化，并展示了如何通过模块化的方式获得完整公理化，从而在每个情况下证明了交换Kleene代数、bi-KA和正则树语言在不同假设下的完备性。
Truly concurrent process algebras are generalizations to the traditional process algebras for true concurrency, CTC to CCS, APTC to ACP, $π_{tc}$ to $π$ calculus, APPTC to probabilistic process algebra. Now, it is the time to utilize truly concurrent process algebras APTC and APPTC to model quantum computing and unify quantum and classical computing. In this book, we introduce the preliminaries, the utilization of APTC to unify quantum and classical computing and its usage in verification of quantum communication protocols, the utilization of APPTC to unifying quantum and classical computing a…
We consider the problem of automatically verifying that a parameterized family of probabilistic concurrent systems terminates with probability one for all instances against adversarial schedulers. A parameterized family defines an infinite-state system: for each number n, the family consists of an instance with n finite-state processes. In contrast to safety, the parameterized verification of liveness is currently still considered extremely challenging especially in the presence of probabilities in the model. One major challenge is to provide a sufficiently powerful symbolic framework. One wel…
Verifying Equilibria in Finite-Horizon Probabilistic Concurrent Game Systems
本文研究有限视界概率多智能体并发博弈系统中给定策略配置是否为纳什均衡或子博弈完美均衡的验证问题，发现子博弈完美均衡验证属于PSPACE，而纳什均衡验证为EXPTIME完全，这一反直觉结果表明子博弈完美均衡验证可能更简单。
Truly concurrent process algebras are generalizations to the traditional process algebras for true concurrency, CTC to CCS, APTC to ACP,$π_{tc}$ to $π$ calculus, APPTC to probabilistic process algebra.In this book, we utilize truly concurrent process algebras APTC and APPTC to model quantum computing and unify quantum and classical computing.
Concurrent Strategies on Games with Algebras
针对信息不完全下并发博弈中玩家与对手移动的独立性，本文证明带代数博弈与常规博弈间存在双射，并扩展到中性事件，但良构双范畴的构建仍待解决。
The combination of nondeterminism and probability in concurrent systems lead to the development of several interpretations of process behavior. If we restrict our attention to linear properties only, we can identify three main approaches to trace and testing semantics: the trace distributions, the trace-by-trace and the extremal probabilities approaches. In this paper, we propose novel notions of behavioral metrics that are based on the three classic approaches above, and that can be used to measure the disparities in the linear behavior of processes wrt trace and testing semantics. We study t…
Automated verification techniques for stochastic games allow formal reasoning about systems that feature competitive or collaborative behaviour among rational agents in uncertain or probabilistic settings. Existing tools and techniques focus on turn-based games, where each state of the game is controlled by a single player, and on zero-sum properties, where two players or coalitions have directly opposing objectives. In this paper, we present automated verification techniques for concurrent stochastic games (CSGs), which provide a more natural model of concurrent decision making and interactio…
A Probabilistic Choreography Language for PRISM
本文提出一种基于PRISM的概率编舞语言，用于建模和分析并发系统，通过概率语义和形式编码提升系统可靠性与可验证性。
The probabilistic modal μ-calculus is a fixed-point logic designed for expressing properties of probabilistic labeled transition systems (PLTS's). Two equivalent semantics have been studied for this logic, both assigning to each state a value in the interval [0,1] representing the probability that the property expressed by the formula holds at the state. One semantics is denotational and the other is a game semantics, specified in terms of two-player stochastic parity games. A shortcoming of the probabilistic modal μ-calculus is the lack of expressiveness required to encode other important tem…
Rational verification is the problem of determining which temporal logic properties will hold in a multi-agent system, under the assumption that agents in the system act rationally, by choosing strategies that collectively form a game-theoretic equilibrium. Previous work in this area has largely focussed on deterministic systems. In this paper, we develop the theory and algorithms for rational verification in probabilistic systems. We focus on concurrent stochastic games (CSGs), which can be used to model uncertainty and randomness in complex multi-agent environments. We study the rational ver…
A Coalgebraic Model of Quantum Bisimulation
本文提出基于效应代数和分级单子的余代数模型，以定义量子并发系统的行为等价性，并推荐核互模拟以刻画对所有输入态概率行为一致的量子系统。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。