On kleene algebras for weighted computation

Kleene algebra with tests (KAT) was introduced as an alge- braic structure to model and reason about classic imperative programs, i.e. sequences of discrete actions guarded by Boolean tests. This paper introduces two generalisations of this structure able to ex- press programs as weighted transition...

Full description

Bibliographic Details
Main Author: Gomes, Leandro (author)
Other Authors: Madeira, Alexandre Leite Castro (author), Barbosa, L. S. (author)
Format: conferencePaper
Language:eng
Published: 2017
Subjects:
Kleene algebra
Weighted computation
Ciências Naturais::Ciências da Computação e da Informação
Science & Technology
Online Access:http://hdl.handle.net/1822/69296
Country:Portugal
Oai:oai:repositorium.sdum.uminho.pt:1822/69296
Description
Summary:Kleene algebra with tests (KAT) was introduced as an alge- braic structure to model and reason about classic imperative programs, i.e. sequences of discrete actions guarded by Boolean tests. This paper introduces two generalisations of this structure able to ex- press programs as weighted transitions and tests with outcomes in a not necessary bivalent truth space, namely graded Kleene algebra with tests (GKAT) and Heyting Kleene algebra with tests (HKAT). On these contexts, in analogy to Kozen's encoding of Propositional Hoare Logic (PHL) in KAT [10], we discuss the encoding of a graded PHL in HKAT and of its while-free fragment in GKAT.

Similar Items