20.500.12556/DiRROS-29256 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 Neznano 2026-05-05 08:34:33 2026-05-05 08:34:33 2026-05-06 03:51:46 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 7DAC639C6B51BFF54BAE2F5E5956F3A4 f184dd256fff713323bc8c756aef3a7af8789909fdfa87ddc8caae46fe9eddfa ece9c81c-484c-11f1-969d-001a4af901a5 https://dirros.openscience.si/Dokument.php?lang=slv&id=43777 https://entics.episciences.org/16743 1 7b435a69-484c-11f1-969d-001a4af901a5 https://dirros.openscience.si/Dokument.php?lang=slv&id=43776 Inštitut za matematiko, fiziko in mehaniko 0 0 0