eprintid: 10130031
rev_number: 25
eprint_status: archive
userid: 608
dir: disk0/10/13/00/31
datestamp: 2021-07-21 11:55:39
lastmod: 2022-05-03 13:51:13
status_changed: 2022-05-03 13:39:40
type: proceedings_section
metadata_visibility: show
creators_name: Schmid, T
creators_name: Rot, J
creators_name: Silva, A
title: On Star Expressions and Completeness Theorems
ispublished: pub
divisions: UCL
divisions: B04
divisions: C05
divisions: F48
keywords: Regular expressions, bisimulation, program semantics, coalgebra.
note: © T. Schmid, J. Rot, & A. Silva
This work is licensed under the
Creative Commons Attribution License.
abstract: An open problem posed by Milner asks for a proof that a certain axiomatisation, which Milner showed is sound with respect to bisimilarity for regular expressions, is also complete. One of the main difficulties of the problem is the lack of a full Kleene theorem, since there are automata that can not be specified, up to bisimilarity, by an expression. Grabmayer and Fokkink (2020) characterise those automata that can be expressed by regular expressions without the constant 1, and use this characterisation to give a positive answer to Milner's question for this subset of expressions. In this paper, we analyse Grabmayer and Fokkink's proof of completeness from the perspective of universal coalgebra, and thereby give an abstract account of their proof method. We then compare this proof method to another approach to completeness proofs from coalgebraic language theory. This culminates in two abstract proof methods for completeness, what we call the local and global approaches, and a description of when one method can be used in place of the other.
date: 2021-12
official_url: http://dx.doi.org/10.4204/EPTCS.351.15
oa_status: green
full_text_type: other
language: eng
primo: open
primo_central: open_green
verified: verified_manual
elements_id: 1871901
doi: 10.4204/EPTCS.351.15
lyricists_name: Silva, Alexandra
lyricists_id: ASILV10
actors_name: Silva, Alexandra
actors_id: ASILV10
actors_role: owner
full_text_status: public
series: EPTCS
publication: arXiv.org
volume: 351
pagerange: 242-259
event_title: MFPS 2021: 37th Conference on Mathematical Foundations of Programming Semantics
book_title: Proceedings: 37th Conference on Mathematical Foundations of Programming Semantics
citation:        Schmid, T;    Rot, J;    Silva, A;      (2021)    On Star Expressions and Completeness Theorems.                     In:  Proceedings: 37th Conference on Mathematical Foundations of Programming Semantics.  (pp. pp. 242-259).         Green open access   
 
document_url: https://discovery.ucl.ac.uk/id/eprint/10130031/7/Silva_2106.08074v2.pdf