Kappé, T;
Brunet, P;
Luttik, B;
Silva, A;
Zanasi, F;
(2021)
Equivalence checking for weak bi-Kleene algebra.
Logical Methods in Computer Science
, 17
(3)
19:1-19:53.
10.46298/LMCS-17(3:19)2021.
Preview |
Text
Kappe_1807.02102_VoR.pdf - Published Version Download (689kB) | Preview |
Abstract
Pomset automata are an operational model of weak bi-Kleene algebra, which describes programs that can fork an execution into parallel threads, upon completion of which execution can join to resume as a single thread. We characterize a fragment of pomset automata that admits a decision procedure for language equivalence. Furthermore, we prove that this fragment corresponds precisely to series-rational expressions, i.e., rational expressions with an additional operator for bounded parallelism. As a consequence, we obtain a new proof that equivalence of series-rational expressions is decidable.
| Type: | Article |
|---|---|
| Title: | Equivalence checking for weak bi-Kleene algebra |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.46298/LMCS-17(3:19)2021 |
| Publisher version: | https://doi.org/10.46298/lmcs-17(3:19)2021 |
| Language: | English |
| Additional information: | This work is licensed under the Creative Commons Attribution License. To view a copy of this license, visit https://creativecommons.org/licenses/by/4.0/ |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10063343 |
Loading...
Loading...Loading...Loading...Archive Staff Only
 |
View Item |
