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

ver descrição completa

Detalhes bibliográficos
Autor principal: Gomes, Leandro (author)
Outros Autores: Madeira, Alexandre Leite Castro (author), Barbosa, L. S. (author)
Formato: conferencePaper
Idioma:eng
Publicado em: 2017
Assuntos:
Kleene algebra
Weighted computation
Ciências Naturais::Ciências da Computação e da Informação
Science & Technology
Texto completo:http://hdl.handle.net/1822/69296
País:Portugal
Oai:oai:repositorium.sdum.uminho.pt:1822/69296
Descrição
Resumo: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.

Registos relacionados