Equivalence checking for weak bi-kleene algebra

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

doi:10.46298/LMCS-17(3:19)2021

Equivalence checking for weak bi-kleene algebra

Tobias Kappé (Corresponding author), Paul Brunet, Bas Luttik, Alexandra Silva, Fabio Zanasi

Research output: Contribution to journal › Article › Academic › peer-review

45 Downloads (Pure)

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.

Original language	English
Pages (from-to)	19:1-19:53
Journal	Logical Methods in Computer Science
Volume	17
Issue number	3
DOIs	https://doi.org/10.46298/LMCS-17(3:19)2021
Publication status	Published - 2021

Funding

Key words and phrases: sr-expressions, pomset automata, Kleene theorem, language equivalence. ∗ An earlier version of this paper was published at CONCUR’17 [KBL+17]. T. Kappéwas partially supported by the ERC Starting Grant 679127 (ProFoundNet) and DARPA grant HR001120C0107 (Pronto). A. Silva was partially supported by the ERC Starting Grant 679127 (ProFound-Net) and a Leverhulme Prize (PLP–2016–129). P. Brunet acknowledges support from EPSRC grant n. EP/R006865/1. F. Zanasi acknowledges support from EPSRC grant n. EP/R020604/1.

Funders	Funder number
Defense Advanced Research Projects Agency	HR001120C0107
European Union's Horizon 2020 - Research and Innovation Framework Programme	679127
Engineering and Physical Sciences Research Council	EP/R020604/1, EP/R006865/1

Keywords

Kleene theorem
Language equivalence
Pomset automata
sr-expressions

Access to Document

10.46298/LMCS-17(3:19)2021

1807.02102Final published version, 673 KB

Cite this

@article{b227d3dc14834391b727b82fd53b5fc8,

title = "Equivalence checking for weak bi-kleene algebra",

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.",

keywords = "Kleene theorem, Language equivalence, Pomset automata, sr-expressions",

author = "Tobias Kapp{\'e} and Paul Brunet and Bas Luttik and Alexandra Silva and Fabio Zanasi",

note = "Funding Information: T. Kapp? was partially supported by the ERC Starting Grant 679127 (ProFoundNet) and DARPA grant HR001120C0107 (Pronto). A. Silva was partially supported by the ERC Starting Grant 679127 (ProFound-Net) and a Leverhulme Prize (PLP?2016?129). P. Brunet acknowledges support from EPSRC grant n. EP/R006865/1. F. Zanasi acknowledges support from EPSRC grant n. EP/R020604/1. Funding Information: Key words and phrases: sr-expressions, pomset automata, Kleene theorem, language equivalence. ∗ An earlier version of this paper was published at CONCUR{\textquoteright}17 [KBL+17]. T. Kapp{\'e}was partially supported by the ERC Starting Grant 679127 (ProFoundNet) and DARPA grant HR001120C0107 (Pronto). A. Silva was partially supported by the ERC Starting Grant 679127 (ProFound-Net) and a Leverhulme Prize (PLP–2016–129). P. Brunet acknowledges support from EPSRC grant n. EP/R006865/1. F. Zanasi acknowledges support from EPSRC grant n. EP/R020604/1. Publisher Copyright: {\textcopyright} T. Kapp{\'e}, P. Brunet, B. Luttik, A. Silva, and F. Zanasi.",

year = "2021",

doi = "10.46298/LMCS-17(3:19)2021",

language = "English",

volume = "17",

pages = "19:1--19:53",

journal = "Logical Methods in Computer Science",

issn = "1860-5974",

publisher = "Technischen Universitat Braunschweig",

number = "3",

}

TY - JOUR

T1 - Equivalence checking for weak bi-kleene algebra

AU - Kappé, Tobias

AU - Brunet, Paul

AU - Luttik, Bas

AU - Silva, Alexandra

AU - Zanasi, Fabio

N1 - Funding Information: T. Kapp? was partially supported by the ERC Starting Grant 679127 (ProFoundNet) and DARPA grant HR001120C0107 (Pronto). A. Silva was partially supported by the ERC Starting Grant 679127 (ProFound-Net) and a Leverhulme Prize (PLP?2016?129). P. Brunet acknowledges support from EPSRC grant n. EP/R006865/1. F. Zanasi acknowledges support from EPSRC grant n. EP/R020604/1. Funding Information: Key words and phrases: sr-expressions, pomset automata, Kleene theorem, language equivalence. ∗ An earlier version of this paper was published at CONCUR’17 [KBL+17]. T. Kappéwas partially supported by the ERC Starting Grant 679127 (ProFoundNet) and DARPA grant HR001120C0107 (Pronto). A. Silva was partially supported by the ERC Starting Grant 679127 (ProFound-Net) and a Leverhulme Prize (PLP–2016–129). P. Brunet acknowledges support from EPSRC grant n. EP/R006865/1. F. Zanasi acknowledges support from EPSRC grant n. EP/R020604/1. Publisher Copyright: © T. Kappé, P. Brunet, B. Luttik, A. Silva, and F. Zanasi.

PY - 2021

Y1 - 2021

N2 - 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.

AB - 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.

KW - Kleene theorem

KW - Language equivalence

KW - Pomset automata

KW - sr-expressions

UR - http://www.scopus.com/inward/record.url?scp=85114885288&partnerID=8YFLogxK

U2 - 10.46298/LMCS-17(3:19)2021

DO - 10.46298/LMCS-17(3:19)2021

M3 - Article

AN - SCOPUS:85114885288

SN - 1860-5974

VL - 17

SP - 19:1-19:53

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

IS - 3

ER -

Equivalence checking for weak bi-kleene algebra

Abstract

Funding

Keywords

Access to Document

Other files and links

Fingerprint

Cite this