Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/69188
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.author | Gomes, Leandro | por |
dc.contributor.author | Madeira, Alexandre | por |
dc.contributor.author | Barbosa, L. S. | por |
dc.date.accessioned | 2021-01-13T15:32:25Z | - |
dc.date.available | 2021-01-13T15:32:25Z | - |
dc.date.issued | 2019 | - |
dc.identifier.issn | 1843-8121 | por |
dc.identifier.uri | https://hdl.handle.net/1822/69188 | - |
dc.description.abstract | 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. | por |
dc.description.sponsorship | POCI-01-0145-FEDER-03094, NORTE-01-0145-FEDER-000037. ERDF – European Regional Development Fund through the Operational Programme for Competitiveness and Internationalisation - COMPETE 2020 Programme and by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciência e a Tecnologia, within project POCI-01-0145-FEDER-030947. This paper is also a result of the project SmartEGOV, NORTE-01-0145-FEDER-000037. The second author is supported in the scope of the framework contract foreseen in the numbers 4, 5 and 6 of the article 23, of the Decree-Law 57/2016, of August 29, changed by Portuguese Law 57/2017, of July 19, at CIDMA (Centro de Investigação e Desenvolvimento em Matemática e Aplicações) UID/MAT/04106/2019. | por |
dc.language.iso | eng | por |
dc.publisher | University Alexandru Ioan Cuza Iasi | por |
dc.relation | UID/MAT/04106/2019 | - |
dc.rights | openAccess | por |
dc.subject | Kleene algebra | por |
dc.subject | Fuzzy relations | por |
dc.subject | Hoare logic | por |
dc.subject | Graded tests | por |
dc.title | Generalising KAT to verify weighted computations | por |
dc.type | article | por |
dc.peerreviewed | yes | por |
dc.relation.publisherversion | https://www.info.uaic.ro/en/sacs_articles/generalising-kat-to-verify-weighted-computations/ | por |
oaire.citationStartPage | 141 | por |
oaire.citationEndPage | 184 | por |
oaire.citationIssue | 2 | por |
oaire.citationVolume | 29 | por |
dc.identifier.eissn | 2248-2695 | - |
dc.identifier.doi | 10.7561/SACS.2019.2.141 | por |
dc.subject.fos | Ciências Naturais::Ciências da Computação e da Informação | por |
dc.subject.wos | Science & Technology | por |
sdum.journal | Scientific Annals of Computer Science | por |
Aparece nas coleções: | HASLab - Artigos em revistas internacionais |