Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/69188
Título: | Generalising KAT to verify weighted computations |
Autor(es): | Gomes, Leandro Madeira, Alexandre Barbosa, L. S. |
Palavras-chave: | Kleene algebra Fuzzy relations Hoare logic Graded tests |
Data: | 2019 |
Editora: | University Alexandru Ioan Cuza Iasi |
Revista: | Scientific Annals of Computer Science |
Resumo(s): | Kleene algebra with tests (KAT) was introduced as an algebraic structure to model and reason about classic imperative programs, i.e. sequences of discrete transitions guarded by Boolean tests. This paper introduces two generalisations of this structure able to express programs as weighted transitions and tests with outcomes in non necessarily bivalent truth spaces: graded Kleene algebra with tests (GKAT) and a variant where tests are also idempotent (I-GKAT). In this context, and in analogy to Kozen's encoding of Propositional Hoare Logic (PHL) in KAT we discuss the encoding of a graded PHL in I-GKAT and of its while-free fragment in GKAT. Moreover, to establish semantics for these structures four new algebras are de ned: FSET (T ), FREL(K; T ) and FLANG(K; T ) over complete residuated lattices K and T , and M(n;A) over a GKAT or I-GKAT A. As a nal exercise, the paper discusses some program equivalence proofs in a graded context. |
Tipo: | Artigo |
URI: | https://hdl.handle.net/1822/69188 |
DOI: | 10.7561/SACS.2019.2.141 |
ISSN: | 1843-8121 |
e-ISSN: | 2248-2695 |
Versão da editora: | https://www.info.uaic.ro/en/sacs_articles/generalising-kat-to-verify-weighted-computations/ |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: | HASLab - Artigos em revistas internacionais |