Kleene Algebra of Weighted Programs With Domain

Result code in 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>

Result on the web

<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>

Result language

angličtina

Original language name

Kleene Algebra of Weighted Programs With Domain

Original language description

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.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

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

Project

<a href="/en/project/GA22-16111S" target="_blank" >GA22-16111S: GRADLACT: Graded Logics of Action</a><br>

Continuities

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Publication year

2024

Confidentiality

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

Article name in the collection

Dynamic Logic. New Trends and Applications. Revised Selected Papers

ISBN

978-3-031-51777-8

ISSN

1611-3349

e-ISSN

1611-3349

Number of pages

16

Pages from-to

52-67

Publisher name

Springer

Place of publication

Cham

Event location

Tbilisi

Event date

Sep 15, 2023

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

001207227000004