Capítulo de livro Acesso aberto Revisado por pares

Concurrent Kleene Algebra: Free Model and Completeness

2018; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-319-89884-1_30

ISSN

1611-3349

Autores

Tobias Kappé, Paul Brunet, Alexandra Silva, Fabio Zanasi,

Tópico(s)

Computability, Logic, AI Algorithms

Resumo

Concurrent Kleene Algebra (CKA) was introduced by Hoare, Moeller, Struth and Wehrman in 2009 as a framework to reason about concurrent programs. We prove that the axioms for CKA with bounded parallelism are complete for the semantics proposed in the original paper; consequently, these semantics are the free model for this fragment. This result settles a conjecture of Hoare and collaborators. Moreover, the technique developed to this end allows us to establish a Kleene Theorem for CKA, extending an earlier Kleene Theorem for a fragment of CKA.

Referência(s)