Kleene Algebra of Weighted Programs With Domain

0584357 - ÚI 2025 CH eng C - Konferenční příspěvek (zahraniční konf.)
Sedlár, Igor
Kleene Algebra of Weighted Programs With Domain.
Dynamic Logic. New Trends and Applications. Revised Selected Papers. Cham: Springer, 2024 - (Gierasimczuk, N.; Velázquez-Quesada, F.), s. 52-67. Lecture Notes in Computer Science, 14401. ISBN 978-3-031-51777-8. E-ISSN 1611-3349.
[DaLí 2023. International Workshop /5./. Tbilisi (GE), 15.09.2023-16.09.2023]
Grant CEP: GA ČR(CZ) GA22-16111S
Institucionální podpora: RVO:67985807
Klíčová slova: Kleene algebra with domain * Kleene algebra with tests * Program semantics * Weakest precondition calculus * Weighted programs

Weighted programs were recently introduced by Batz et al. (Proc. ACM Program. Lang. 2022) as a generalization of probabilistic programs which can also represent optimization problems and, in general, programs whose execution traces carry some sort of weight. Batzet al. show that a weighted version of Dijkstra’s weakest precondition operator can be used to reason about the competitive ratios of weighted programs. In this paper we study a propositional abstraction of weighted programs with three main contributions. First, we formulate a semantics for weighted programs with the weighted weakest precondition operator based on functions from multimonoids to quantales. Second, we show that the weighted weakest precondition operator corresponds to a generalization of the domain operator known from Kleene algebra with domain, and we study the properties of the generalized domain operator. Third, we formulate a weighted version of Kleene algebra with domain as a framework for reasoning about weighted programs with weakest precondition in an abstract setting.
Trvalý link: https://hdl.handle.net/11104/0352276