On the coalgebraic theory of Kleene algebra with tests. (English) Zbl 1437.68125

Başkent, Can (ed.) et al., Rohit Parikh on logic, language and society. Cham: Springer. Outst. Contrib. Log. 11, 279-298 (2017).
Summary: We develop a coalgebraic theory of Kleene algebra with tests (KAT) along the lines of J. J. M. M. Rutten [Lect. Notes Comput. Sci. 1466, 194–218 (1998; Zbl 0940.68085)] for Kleene algebra (KA) and H. Chen and R. Pucella [Electron. Notes Theor. Comput. Sci. 82, No. 1, 94–109 (2003; Zbl 1270.68189)] for a limited version of KAT, resolving some technical issues raised by Chen and Pucella. Our treatment includes a simple definition of the Brzozowski derivative for KAT expressions and an automata-theoretic interpretation involving automata on guarded strings. We also give a complexity analysis, showing that an efficient implementation of coinductive equivalence proofs in this setting is tantamount to a standard automata-theoretic construction. It follows that coinductive equivalence proofs can be generated automatically in PSPACE. This matches the bound of J. Worthington [Lect. Notes Comput. Sci. 4988, 382–396 (2008; Zbl 1140.68042)] for the automatic generation of equational proofs in KAT.
For the entire collection see [Zbl 1381.03001].


68Q70 Algebraic theory of languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
Full Text: DOI


[1] Bonsangue, M. M., Rutten, J. J. M. M., & Silva, A. M. (2007). Regular expressions for polynomial coalgebras. Technical Report SEN-E0703, Centrum voor Wiskunde en Informatica, Amsterdam. · Zbl 1234.68272
[2] Bonsangue, M. M., Rutten, J. J. M. M., & Silva, A. M. (2009). A Kleene theorem for polynomial coalgebras. In L. de Alfaro (Ed.), Proceedings of the 12th international conference foundations of software science and computation structures (FoSSaCS 2009) (Vol. 5504, pp. 122-136)., of lecture notes in computer science New York: Springer. · Zbl 1234.68272
[3] Brzozowski, J. A. (1964). Derivatives of regular expressions. Journal of the Association for Computing Machinery, 11, 481-494. · Zbl 0225.94044
[4] Chen, H., & Pucella, R. (2003). A coalgebraic approach to Kleene algebra with tests. Electronic Notes in Theoretical Computer Science, 82(1), · Zbl 1270.68189
[5] Cohen, E., Kozen, D., & Smith, F. (1996). The complexity of Kleene algebra with tests. Technical Report TR96-1598, Computer Science Department, Cornell University.
[6] Conway, J. H. (1971). Regular algebra and finite machines. London: Chapman and Hall. · Zbl 0231.94041
[7] Kaplan, D. M. (1969). Regular expressions and the equivalence of programs. Journal of Computer and System Sciences, 3, 361-386. · Zbl 0187.13603
[8] Kleene, S. C. (1956). Representation of events in nerve nets and finite automata. In C. E. Shannon & J. McCarthy (Eds.), Automata studies (pp. 3-41). Princeton, NJ: Princeton University Press.
[9] Kozen, D. (1994). A completeness theorem for Kleene algebras and the algebra of regular events. Computing and Information, 110(2), 366-390. · Zbl 0806.68082
[10] Kozen, D. (1997). Kleene algebra with tests. Transactions on Programming Languages and Systems, 19(3), 427-443. · Zbl 0882.03064
[11] Kozen, D. (2000). On Hoare logic and Kleene algebra with tests. Transactions on Computational Logic, 1(1), 60-76. · Zbl 1365.68326
[12] Kozen, D. (2003). Automata on guarded strings and applications. Matématica Contemporânea, 24, 117-139. · Zbl 1087.68049
[13] Kozen, D. (2008). On the coalgebraic theory of Kleene algebra with tests. Technical Report.? http://hdl.handle.net/1813/10173, Computing and Information Science, Cornell University.
[14] Kozen, D., & Smith, F. (1996). Kleene algebra with tests: Completeness and decidability. In D. van Dalen & M. Bezem (Eds.), Proceedings of the 10th international workshop computer science logic (CSL’96) (Vol. 1258, pp. 244-259)., of lecture notes in computer science Utrecht: Springer. · Zbl 0882.03064
[15] Rutten, J. J. M. M. (1998). Automata and coinduction (an exercise in coalgebra). Proceedings of CONCUR’98 (Vol. 1466, pp. 193-217)., lecture notes in computer science Berlin: Springer. · Zbl 0940.68085
[16] Savitch, W. (1970). Relationship between nondeterministic and deterministic tape complexities. Journal of Computer and System Sciences, 4(2), 177-192. · Zbl 0188.33502
[17] Worthington, J.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.