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 actions guarded by Boolean tests.
This paper introduces two generalisations of this structure able to express 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.
This work is financed by the 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 projects POCI-01-0145-FEDER-016692 and UID/MAT/04106/2013. The second author is also supported by the individual grant SFRH/BPD/103004/2014.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Blok, W.J., Ferreirim, I.: On the structure of hoops. Algebra Univers. 43, 233–257 (2000)
Conway, J.: Regular Algebra and Finite Machines. Dover Publications, New York (1971)
den Hartog, J., de Vink, E.P.: Verifying probabilistic programs using a Hoare like logic. Int. J. Found. Comput. Sci. 13(3), 315–340 (2002)
Guilherme, R.: A coalgebraic approach to fuzzy automata. Master’s thesis, Faculdade de Ciências e Tecnologia - Universidade Nova de Lisboa, Lisboa (2016)
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)
Kozen, D.: The Design and Analysis of Algorithms. Springer-Verlag, New York (1992)
Kozen, D.: On action algebras. In Logic and the Flow of Information, Amsterdam (1993)
Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput. 110, 366–390 (1994)
Kozen, D.: Kleene algebra with tests. ACM Trans. Program. Lang. Syst. 19(3), 427–443 (1997)
Kozen, D.: On Hoare logic and Kleene algebra with tests. ACM Trans. Comput. Logic 1(212), 1–14 (2000)
Madeira, A., Neves, R., Martins, M.A.: An exercise on the generation of many-valued dynamic logics. J. Logical Algebraic Methods Program. 1, 1–29 (2016)
McIver, A.K., Cohen, E., Morgan, C.C.: Using probabilistic Kleene algebra for protocol verification. In: Schmidt, R.A. (ed.) RelMiCS 2006. LNCS, vol. 4136, pp. 296–310. Springer, Heidelberg (2006). https://doi.org/10.1007/11828563_20
Platzer, A.: Logical Analysis of Hybrid Systems - Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010)
Pratt, V.: Action logic and pure induction. In: Eijck, J. (ed.) JELIA 1990. LNCS, vol. 478, pp. 97–120. Springer, Heidelberg (1991). https://doi.org/10.1007/BFb0018436
Qiao, R., Wu, J., Wang, Y., Gao, X.: Operational semantics of probabilistic Kleene algebra with tests. In: Proceedings of IEEE Symposium on Computers and Communications, pp. 706–713 (2008)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Gomes, L., Madeira, A., Barbosa, L.S. (2017). On Kleene Algebras for Weighted Computation. In: Cavalheiro, S., Fiadeiro, J. (eds) Formal Methods: Foundations and Applications. SBMF 2017. Lecture Notes in Computer Science(), vol 10623. Springer, Cham. https://doi.org/10.1007/978-3-319-70848-5_17
Download citation
DOI: https://doi.org/10.1007/978-3-319-70848-5_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-70847-8
Online ISBN: 978-3-319-70848-5
eBook Packages: Computer ScienceComputer Science (R0)