发表机构
Bretagne INP–ENIB; IRDL (CNRS UMR 6027); Max Planck Institute for Software Systems (MPI-SWS); University of Birmingham（布列塔尼国立高等矿业电信学校联盟-恩布理工学院; 法国国家科学研究中心第6027联合研究实验室; 马克斯·普朗克软件系统研究所; 伯明翰大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出一个用于离散事件模拟器的核心演算及证明系统，实现性能模型中几乎必然可达性和期望到达时间属性的可靠完备推理，并在Lean中实现验证。
AI 中文摘要
离散事件模拟是建模和分析计算机系统、网络及服务性能的标准技术。尽管模拟工具被广泛使用，但对它们所实现的模型的正确性和性能保证的推理在很大程度上仍然是临时性的：模拟输出被统计性地解释，但缺乏对其行为进行演绎推理的逻辑基础。我们提出了一个核心命令式演算，它捕捉了离散事件模拟器共有的基本构造：异步执行、从分布中进行连续和离散采样，以及通过全局事件队列进行基于时间的调度。在此演算之上，我们开发了一个证明系统，用于推理几乎必然可达性和期望到达时间属性。我们的主要结果是为这些属性建立了一个可靠且完备的证明规则。我们的框架将离散时间概率程序的演绎推理推广到性能模型的设置中，其中连续时间和连续概率分布是核心。我们已在嵌入Lean的工具中实现了这些证明规则。我们通过为多个案例研究推导几乎必然可达性和期望到达时间的证明来展示我们证明规则的适用性，这些案例包括超越排队论解析解的客户端-服务器示例以及网络路由协议中的收敛行为。建立我们证明规则的可靠性和完备性需要比离散时间设置复杂得多的论证。这是由于操作语义的根本不连续性以及连续时间和概率分布的测度论挑战。
英文摘要
Discrete-event simulation is a standard technique for modelling and analysing the performance of computer systems, networks, and services. Although simulation tools are widely used, reasoning about the correctness and performance guarantees of the models they implement remains largely ad hoc: simulation outputs are interpreted statistically, but there is no logical foundation for deductive reasoning about their behaviour. We present a core imperative calculus that captures the essential constructs common to discrete-event simulators: asynchronous execution, continuous and discrete sampling from distributions, and time-based event scheduling through a global event queue. On top of this calculus, we develop a proof system for reasoning about almost-sure reachability and expected reaching time properties. Our main result is a sound and complete proof rule for these properties. Our framework generalizes deductive reasoning for discrete-time probabilistic programs to the setting of performance models, in which continuous time and continuous probability distributions are central. We have implemented the proof rules in a tool embedded in Lean. We demonstrate the applicability of our proof rule by deriving proofs of almost-sure reachability and expected reaching time for a number of case studies, including client-server examples that go beyond analytic solutions from queueing theory as well as convergence behaviours in network routing protocols. Establishing the soundness and completeness of our proof rules requires significantly more complex arguments than in the discrete-time setting. This is due to the fundamentally discontinuous nature of the operational semantics and the measure-theoretic challenges of continuous time and probability distributions.
Comments38 pages
