eprintid: 10063343 rev_number: 54 eprint_status: archive userid: 608 dir: disk0/10/06/33/43 datestamp: 2021-09-23 08:37:08 lastmod: 2022-01-31 18:52:25 status_changed: 2021-09-23 08:37:08 type: article metadata_visibility: show creators_name: Kappé, T creators_name: Brunet, P creators_name: Luttik, B creators_name: Silva, A creators_name: Zanasi, F title: Equivalence checking for weak bi-Kleene algebra ispublished: pub divisions: UCL divisions: B04 divisions: C05 divisions: F48 note: 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/ 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. date: 2021-08-13 date_type: published official_url: https://doi.org/10.46298/lmcs-17(3:19)2021 oa_status: green full_text_type: pub language: eng primo: open primo_central: open_green verified: verified_manual elements_id: 1606619 doi: 10.46298/LMCS-17(3:19)2021 lyricists_name: Brunet, Paul lyricists_name: Kappe, Tobias lyricists_name: Silva, Alexandra lyricists_name: Zanasi, Fabio lyricists_id: PBRUN86 lyricists_id: TWJKA28 lyricists_id: ASILV10 lyricists_id: FZANA74 actors_name: Kappe, Tobias actors_name: Allington-Smith, Dominic actors_id: TWJKA28 actors_id: DAALL44 actors_role: owner actors_role: impersonator full_text_status: public publication: Logical Methods in Computer Science volume: 17 number: 3 pagerange: 19:1-19:53 citation: 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 <https://doi.org/10.46298/LMCS-17%283%3A19%292021>. Green open access document_url: https://discovery.ucl.ac.uk/id/eprint/10063343/13/Kappe_1807.02102_VoR.pdf