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

Onderzoeksoutput: Bijdrage aan tijdschrift › Tijdschriftartikel › Academic › peer review

45 Downloads (Pure)

Samenvatting

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.

Originele taal-2	Engels
Pagina's (van-tot)	19:1-19:53
Tijdschrift	Logical Methods in Computer Science
Volume	17
Nummer van het tijdschrift	3
DOI's	https://doi.org/10.46298/LMCS-17(3:19)2021
Status	Gepubliceerd - 2021

Bibliografische nota

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.

Financiering

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.

Financiers	Financiernummer
Defense Advanced Research Projects Agency	HR001120C0107
European Union’s Horizon Europe research and innovation programme	679127
Engineering and Physical Sciences Research Council	EP/R020604/1, EP/R006865/1

Toegang tot document

10.46298/LMCS-17(3:19)2021

1807.02102Definitieve gepubliceerde versie, 673 KB

Andere bestanden en links

Link naar publicatie in Scopus

Citeer dit

@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

Samenvatting

Bibliografische nota

Financiering

Toegang tot document

Andere bestanden en links

Vingerafdruk

Citeer dit