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

Kozen, Dexter

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

MSC:

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

Keywords:

Kleene algebra; Kleene algebra with tests; coalgebra; verification

Citations:

Zbl 0940.68085; Zbl 1270.68189; Zbl 1140.68042

References:

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