Kleene Algebra of Weighted Programs With Domain

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F24%3A00584357" target="_blank" >RIV/67985807:_____/24:00584357 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-031-51777-8_4" target="_blank" >http://dx.doi.org/10.1007/978-3-031-51777-8_4</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-031-51777-8_4" target="_blank" >10.1007/978-3-031-51777-8_4</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Kleene Algebra of Weighted Programs With Domain

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Kleene Algebra of Weighted Programs With Domain

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA22-16111S" target="_blank" >GA22-16111S: GRADLACT: Stupňované logiky konání</a><br>

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2024

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Dynamic Logic. New Trends and Applications. Revised Selected Papers

ISBN

978-3-031-51777-8

ISSN

1611-3349

e-ISSN

1611-3349

Počet stran výsledku

16

Strana od-do

52-67

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Tbilisi

Datum konání akce

15. 9. 2023

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

001207227000004