Please use this identifier to cite or link to this item: http://repositorio.inesctec.pt/handle/123456789/11234
Full metadata record
DC FieldValueLanguage
dc.contributor.authorHASLab INESC TEC,Universidade do Minho,R. da Universidade,4710-057 Braga,Portugal,en
dc.contributor.authorCIDMA,Universidade de Aveiro,Campus Universitario de Santiago,3810-193 Aveiro,Portugal,en
dc.contributor.authorLuís Soares Barbosaen
dc.contributor.authorMadeira,Aen
dc.contributor.authorLeandro Rafael Gomesen
dc.contributor.authorUniversidade do Minho,R. da Universidade,4710-057 Braga,Portugal & Quantum Software Engineering Group,INL,en
dc.contributor.other6759en
dc.contributor.other5603en
dc.date.accessioned2020-06-16T09:10:49Z-
dc.date.available2020-06-16T09:10:49Z-
dc.date.issued2019en
dc.identifier.urihttp://repositorio.inesctec.pt/handle/123456789/11234-
dc.identifier.urihttp://dx.doi.org/10.7561/sacs.2019.2.141en
dc.description.abstractKleene 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 defined: 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 final exercise, the paper discusses some program equivalence proofs in a graded context.en
dc.languageengen
dc.titleGeneralising KAT to Verify Weighted Computationsen
dc.typePublicationen
dc.typearticleen
Appears in Collections:HASLab - Indexed Articles in Journals

Files in This Item:
File Description SizeFormat 
P-00R-HF2.pdf809.12 kBAdobe PDFThumbnail
View/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.