SACS | Generalising KAT to Verify Weighted Computations

Published in Volume XXIX, Issue 2, 2019, pages 141-184, doi: 10.7561/SACS.2019.2.141

Authors: L. Gomes, A. Madeira, L.S. Barbosa

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

Full Text (PDF)

References

[1] A. Alexandru, G. Ciobanu. Fixed Point Results for Finitely Supported Algebraic Structures. Fuzzy Sets and Systems, 2019. doi:10.1016/j.fss.2019.09.014.

[2] V. Anand, A.E. Carroll, P.G. Biondich, T.M. Dugan, S.M. Downs. Pediatric Decision Support Using Adapted Arden Syntax. Artificial Intelligence in Medicine 92, 15-23, 2018. doi:10.1016/j.artmed.2015.09.006.

[3] W.J. Blok, I. Ferreirim. On the Structure of Hoops. Algebra Universalis 43(2-3), 233-257, 2000. doi:10.1007/s000120050156.

[4] J.H. Conway. Regular Algebra and Finite Machines. Dover Publications, New York, 1971.

[5] H.-H. Dang, P. Höfner, B. Möller. Algebraic Separation Logic. The Journal of Logic and Algebraic Programming 80(6), 221-247, 2011. doi:10.1016/j.jlap.2011.04.003.

[6] J. den Hartog, E.P. de Vink. Verifying Probabilistic Programs Using a Hoare Like Logic. International Journal of Foundations of Computer Science 13(3), 315-340, 2002. doi:10.1142/S012905410200114X.

[7] J. Desharnais, B. Möller. Fuzzifying Modal Algebra. In P. Höfner, P. Jipsen, W. Kahl, M.E. Müller (Eds.) Proceedings 14th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2014), Lecture Notes in Computer Science 8428, 395-411. 2014. doi:10.1007/978-3-319-06251-8\_24.

[8] J. Desharnais, B. Möller, G. Struth. Kleene Algebra with Domain. ACM Transactions on Computational Logic 7(4), 798-833, 2006. doi:10.1145/1183278.1183285.

[9] J. Desharnais, B. Möller, G. Struth. Algebraic Notions of Termination. Logical Methods in Computer Science 7(1:1), 1-29, 2011. doi:10.2168/LMCS-7(1:1)2011.

[10] J. Desharnais, G. Struth. Modal Semirings Revisited. In P. Audebaud, C. Paulin-Mohring (Eds.) Proceedings 9th International Conference on Mathematics of Program Construction (MPC 2008), Lecture Notes in Computer Science 5133, 360-387, 2008. doi:10.1007/978-3-540-70594-9\_19.

[11] J. Desharnais, G. Struth. Internal Axioms for Domain Semirings. Science of Computer Programming 76(3), 181-203, 2011. doi:10.1016/j.scico.2010.05.007.

[12] R.W. Floyd. Assigning Meanings to Programs. In T.R. Colburn, J.H. Fetzer, T.L. Rankin (Eds.) Program Verification. Studies in Cognitive Systems 14, 65-81, 1993. doi:10.1007/978-94-011-1793-7_4.

[13] J.A. Goguen. L-fuzzy Sets. Journal of Mathematical Analysis and Applications 18(1), 145-174, 1967. doi:10.1016/0022-247X(67)90189-8.

[14] L. Gomes, A. Madeira, L.S. Barbosa. On Kleene Algebras for Weighted Computation. In S. Cavalheiro, J. Fiadeiro (Eds.) Proceedings 20th Brazilian Symposium on Formal Methods (SBMF 2017), Lecture Notes in Computer Science 10623, 271-286. 2017. doi:10.1007/978-3-319-70848-5_17.

[15] R. Guilherme. A Coalgebraic Approach to Fuzzy Automata. Master’s thesis, Faculdade de Ciências e Tecnologia – Universidade Nova de Lisboa, Lisboa, 2016.

[16] C A.R. Hoare. An Axiomatic Basis for Computer Programming. Communications of the ACM 12(10), 576-580, 1969. doi:10.1145/363235.363259.

[17] P. Höfner, B. Möller. An Algebra of Hybrid Systems. The Journal of Logic and Algebraic Programming 78(2), 74-97, 2009. doi:10.1016/j.jlap.2008.08.005.

[18] P. Jipsen, M. A. Moshier. Concurrent Kleene Algebra with Tests and Branching Automata. Journal of Logical and Algebraic Methods in Programming 85(4), 637-652, 2016. doi:10.1016/j.jlamp.2015.12.005.

[19] D. Kozen. The Design and Analysis of Algorithms. Springer-Verlag New York, 1992. doi:10.1007/978-1-4612-4400-4.

[20] D. Kozen. On Action Algebras. DAIMI Report Series 21(381), 1992. doi:10.7146/dpb.v21i381.6613.

[21] D. Kozen. A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events. Information and Computation 110(2), 366-390, 1994. doi:10.1006/inco.1994.1037.

[22] D. Kozen. Kleene Algebra with Tests. ACM Transactions on Programming Languages and Systems 19(3), 427-443, 1997. doi:10.1145/256167.256195.

[23] D. Kozen. On Hoare Logic and Kleene Algebra with Tests. ACM Transactions on Computational Logic (TOCL) 1(1), 60-76, 2000. doi:10.1145/343369.343378.

[24] A. Madeira, R. Neves, M.A. Martins. An Exercise on the Generation of Many-Valued Dynamic Logics. Journal of Logical and Algebraic Methods in Programming 85(5), 1011-1037, 2016. doi:10.1016/j.jlamp.2016.03.004.

[25] A.K. McIver, E. Cohen, C.C. Morgan. Using Probabilistic Kleene Algebra for Protocol Verification. In R.A. Schmidt (Ed.) Proceedings 9th International Conference on Relational Methods in Computer Science and 4th International Workshop on Applications of Kleene Algebra (RelMiCS/AKA 2006), Lecture Notes in Computer Science 4136, 296-310. 2006. doi:10.1007/11828563_20.

[26] V. Novák, I. Perfiljeva, J. Mockor. Mathematical Principles of Fuzzy Logic. Springer, Boston, MA, 1999. doi:10.1007/978-1-4615-5217-8.

[27] A. Platzer. Logical Analysis of Hybrid Systems – Proving Theorems for Complex Dynamics. Springer, Berlin, Heidelberg, 2010. doi:10.1007/978-3-642-14509-4.

[28] V.R. Pratt. Action Logic and Pure Induction. In J. van Eijck (Ed.) Proceedings European Workshop on Logics in Artificial Intelligence (JELIA 1990), Lecture Notes in Computer Science 478, 97-120. 1990. doi:10.1007/BFb0018436.

[29] C. Prisacariu. Synchronous Kleene Algebra. The Journal of Logic and Algebraic Programming 79(7), 608-635, 2010. doi:10.1016/j.jlap.2010.07.009.

[30] R. Qiao, Y. Wang, X. Gao, J. Wu. Operational semantics of Probabilistic Kleene Algebra with Tests. In Proceedings IEEE Symposium on Computers and Communications (ISCC 2008), 706-713, 2008. doi:10.1109/ISCC.2008.4625616.

[31] M. Samwald, K. Fehre, J. de Bruin, K. Adlassnig. The Arden Syntax Standard for Clinical Decision Support: Experiences and Directions. Journal of Biomedical Informatics 45(4), 711-718, 2012. doi:10.1016/j.jbi.2012.02.001.

[32] J.B. Starren, G. Hripcsak, D. Jordan, B. Allen, C.Weissman, P.D. Clayton. Encoding a Post-Operative Coronary Artery Bypass Surgery Care Plan in the Arden Syntax. Computers in Biology and Medicine 24(5), 411-417, 1994. doi:10.1016/0010-4825(94)90010-8.

[33] T. Vetterlein, H. Mandl, K. Adlassnig. Fuzzy Arden Syntax: A Fuzzy Programming Language for Medicine. Artificial Intelligence in Medicine 49(1), 1-10, 2010. doi:10.1016/j.artmed.2010.01.003.

[34] M. Winter. An Algebraic Formalisation of L-Fuzzy Relations. In J. Desharnais (Ed.) Participants Copies of Fifth International Seminar on Relational Methods in Computer Science (RelMiCS 2000), 233-242, 2000.

[35] M. Winter. A New Algebraic Approach to L-Fuzzy Relations Convenient to Study Crispness. Information Sciences 139(3-4), 233-252, 2001. doi:10.1016/S0020-0255(01)00167-0.

[36] M. Winter. Relation Algebraic Approaches to Fuzzy Relations – (Invited Tutorial). In H.C.M. de Swart (Ed.) Proceedings 12th International Conference on Relational and Algebraic Methods in Computer Science (RAMICS 2011), Lecture Notes in Computer Science 6663, 70-73. 2011. doi:10.1007/978-3-642-21070-9\_7.

[37] L.A. Zadeh. Fuzzy Sets. Information and Control 8(3), 338-353, 1965. doi:10.1016/S0019-9958(65)90241-X.

Bibtex

@article{sacscuza:gomes2019gkvwc,
  title={Generalising KAT to Verify Weighted Computations},
  author={L. Gomes, A. Madeira, L. S. Barbosa},
  journal={Scientific Annals of Computer Science},
  volume={29},
  number={2},
  organization={Alexandru Ioan Cuza University, Ia\c si, Rom\^ania},
  year={2019},
  pages={141–184},
  publisher={Alexandru Ioan Cuza University Press, Ia\c si},
  doi={10.7561/SACS.2019.2.141}
}