Tobias Kappé ; Paul Brunet ; Bas Luttik ; Alexandra Silva ; Fabio Zanasi - Equivalence checking for weak bi-Kleene algebra

lmcs:7502 - Logical Methods in Computer Science, August 13, 2021, Volume 17, Issue 3 - https://doi.org/10.46298/lmcs-17(3:19)2021
Equivalence checking for weak bi-Kleene algebraArticle

Authors: Tobias Kappé ORCID; Paul Brunet ORCID; Bas Luttik ; Alexandra Silva ; Fabio Zanasi ORCID

    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.


    Volume: Volume 17, Issue 3
    Published on: August 13, 2021
    Accepted on: May 24, 2021
    Submitted on: May 24, 2021
    Keywords: Computer Science - Formal Languages and Automata Theory
    Funding:
      Source : OpenAIRE Graph
    • Enhanced Formal Reasoning for Algebraic Network Theory; Funder: UK Research and Innovation; Code: EP/R020604/1
    • Incentive - LA 2 - 2013; Funder: Fundação para a Ciência e a Tecnologia, I.P.; Code: Incentivo/SAU/LA0002/2013
    • Incentive - LA 3 - 2013; Funder: Fundação para a Ciência e a Tecnologia, I.P.; Code: Incentivo/SAU/LA0003/2013
    • Interface reasoning for interacting systems (IRIS).; Funder: UK Research and Innovation; Code: EP/R006865/1
    • Incentive - LA 1 - 2013; Funder: Fundação para a Ciência e a Tecnologia, I.P.; Code: Incentivo/SAU/LA0001/2013
    • Probabilistic Foundations for Networks; Funder: European Commission; Code: 679127

    Consultation statistics

    This page has been seen 1225 times.
    This article's PDF has been downloaded 295 times.