Completeness Theorems for Bi-Kleene Algebras and Series-Parallel Rational Pomset Languages
- Submitting institution
-
The University of Sheffield
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 2468
- Type
- E - Conference contribution
- DOI
-
10.1007/978-3-319-06251-8_5
- Title of conference / published proceedings
- Relational and Algebraic Methods in Computer Science. RAMICS 2014. Lecture Notes in Computer Science
- First page
- 65
- Volume
- 8428
- Issue
- -
- ISSN
- 0302-9743
- Open access status
- Out of scope for open access requirements
- Month of publication
- May
- Year of publication
- 2014
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
1
- Research group(s)
-
I - Verification
- Citation count
- -
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Solves an important problem in concurrency verification that was open for 5 years by introducing a new technique based on atomicity of Boolean algebras of finitely many regular languages. Has become basis for related completeness/free algebra proofs and decidability results for concurrent Kleene algebras and pomset languages, for instance by UCL's Algebra, Semantics, and Computation’s research group (e.g. https://www.sciencedirect.com/science/article/pii/S2352220817302298). Highly relevant to verification of concurrent programs and weak memory models, e.g., equivalences between specifications and implementations. Significant for structural understanding of concurrent Kleene algebra, which has attracted widespread attention. Led to two EPSRC grants on concurrency.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -