20.500.12556/RUL-182236 Safety, relative tightness and the probabilistic frame rule Probabilistic separation logic offers an approach to reasoning about imperative probabilistic programs in which a separating conjunction is used as a mechanism for expressing independence properties. Crucial to the effectiveness of the formalism is the frame rule, which enables modular reasoning about independent probabilistic state. We explore a semantic formulation of probabilistic separation logic, in which the frame rule has the same simple formulation as in separation logic, without further side conditions. This is achieved by building a notion of safety into specifications, using which we establish a crucial property of specifications, called relative tightness, from which the soundness of the frame rule follows. probabilistic separation logic separation logic frame rule partial state operational semantics partial correctness total correctness reasoning about independence logika semantika true false true Angleški jezik Slovenski jezik Članek v reviji 2026-05-05 08:35:03 2026-05-05 08:35:08 2026-05-06 04:29:05 0000-00-00 00:00:00 2025 0 0 Str. 12-1-12-17 0000-00-00 Zaloznikova Objavljeno NiDoloceno 0000-00-00 0000-00-00 0000-00-00 510.6 2969-2431 10.46298/entics.16743 276910851 276899075 2506.01626.pdf 2506.01626.pdf 1 4FAA50E7ECC608F16B8E6B89FDE41686 6b85da8b8afe8998747d24cbad0a09103e7e71bf823ac4fb24ed8a9485918972 ac8cb0e9-484c-11f1-b0ab-0050569b8976 https://repozitorij.uni-lj.si/Dokument.php?lang=slv&id=233307 https://entics.episciences.org/16743 1 476c8b60-484c-11f1-b0ab-0050569b8976 https://repozitorij.uni-lj.si/Dokument.php?lang=slv&id=233306 Fakulteta za matematiko in fiziko Fakulteta za računalništvo in informatiko 0 0 0