Abstract
Concurrent Kleene algebras were introduced by Hoare, Möller, Struth and Wehrman in [HMSW09, HMSW09a, HMSW11] as idempotent bisemirings that satisfy a concurrency inequation and have a Kleene-star for both sequential and concurrent composition. Kleene algebra with tests (KAT) were defined earlier by Kozen and Smith [KS97]. Concurrent Kleene algebras with tests (CKAT) combine these concepts and give a relatively simple algebraic model for reasoning about operational semantics of concurrent programs. We generalize guarded strings to guarded series-parallel strings, or gsp-strings, to provide a concrete language model for CKAT. Combining nondeterministic guarded automata [Koz03] with branching automata of Lodaya and Weil [LW00] one obtains a model for processing gsp-strings in parallel, and hence an operational interpretation for CKAT. For gsp-strings that are simply guarded strings, the model works like an ordinary nondeterministic guarded automaton. If the test algebra is assumed to be {0,1} the language model reduces to the regular sets of bounded-width sp-strings of Lodaya and Weil.
Since the concurrent composition operator distributes over join, it can also be added to relation algebras with transitive closure to obtain the variety CRAT. We provide semantics for these algebras in the form of coalgebraic arrow frames expanded with concurrency.
Keywords
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Andréka, H., Mikulás, S., Németi, I.: The equational theory of Kleene lattices. Theoret. Comput. Sci. 412(52), 7099–7108 (2011)
Gisher, L.: The equational theory of pomsets. Theoretical Computer Science 62, 224–299 (1988)
Hoare, C.A.R., Möller, B., Struth, G., Wehrman, I.: Concurrent Kleene algebra and its foundations. J. Log. Algebr. Program. 80(6), 266–296 (2011)
Hoare, C.A.R., Möller, B., Struth, G., Wehrman, I.: Foundations of concurrent Kleene algebra. In: Berghammer, R., Jaoua, A.M., Möller, B. (eds.) RelMiCS/AKA 2009. LNCS, vol. 5827, pp. 166–186. Springer, Heidelberg (2009)
Hoare, C.A.R., Möller, B., Struth, G., Wehrman, I.: Concurrent Kleene algebra. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 399–414. Springer, Heidelberg (2009)
Kurucz, Á., Németi, I., Sain, I., Simon, A.: Undecidable varieties of semilattice-ordered semigroups, of Boolean algebras with operators, and logics extending Lambek calculus. Logic Journal of IGPL 1(1), 91–98 (1993)
Kozen, D.: Automata on guarded strings and applications. In: 8th Workshop on Logic, Language, Informations and Computation WoLLIC 2001 (Braslia). Mat. Contemp., vol. 24, pp. 117–139 (2003)
Kozen, D.: On the representation of Kleene algebras with tests. In: Královič, R., Urzyczyn, P. (eds.) MFCS 2006. LNCS, vol. 4162, pp. 73–83. Springer, Heidelberg (2006)
Kozen, D., Smith, F.: Kleene algebra with tests: Completeness and decidability. In: van Dalen, D., Bezem, M. (eds.) CSL 1996. LNCS, vol. 1258, pp. 244–259. Springer, Heidelberg (1997)
Kozen, D., Tiuryn, J.: Substructural logic and partial correctness. ACM Trans. Computational Logic 4(3), 355–378 (2003)
Lodaya, K., Weil, P.: Series-parallel languages and the bounded-width property. Theoret. Comput. Sci. 237(1-2), 347–380 (2000)
Ng, K.C.: Relation Algebras with Transitive Closure. PhD thesis, University of California, Berkeley (1984)
Ng, K.C., Tarski, A.: Relation algebras with transitive closure, Abstract 742-02-09. Notices Amer. Math. Soc. 24, A29–A30 (1977)
Pratt, V.: Modelling concurrency with partial orders. Internat. J. Parallel Prog. 15(1), 33–71 (1986)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Jipsen, P. (2014). Concurrent Kleene Algebra with Tests. In: Höfner, P., Jipsen, P., Kahl, W., Müller, M.E. (eds) Relational and Algebraic Methods in Computer Science. RAMICS 2014. Lecture Notes in Computer Science, vol 8428. Springer, Cham. https://doi.org/10.1007/978-3-319-06251-8_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-06251-8_3
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-06250-1
Online ISBN: 978-3-319-06251-8
eBook Packages: Computer ScienceComputer Science (R0)