English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Milner (1984) defined a process semantics for regular expressions. Heformulated a sound proof system for bisimilarity of process interpretations ofregular expressions, and asked whether this system is complete.  We report conceptually on a proof that shows that Milner's system iscomplete, by motivating, illustrating, and describing all of its main steps. Wesubstantially refine the completeness proof by Grabmayer and Fokkink (2020) forthe restriction of Milner's system to `1-free' regular expressions. As acrucial complication we recognize that process graphs with empty-steptransitions that satisfy the layered loop-existence/elimination property LLEEare not closed under bisimulation collapse (unlike process graphs with LLEEthat only have proper-step transitions). We circumnavigate this obstacle bydefining a LLEE-preserving `crystallization procedure' for such process graphs.By that we obtain `near-collapsed' process graphs with LLEE whose stronglyconnected components are either collapsed or of `twin-crystal' shape. Suchnear-collapsed process graphs guarantee provable solutions for bisimulationcollapses of process interpretations of regular expressions.

Milner's Proof System for Regular Expressions Modulo Bisimilarity is  Complete (Crystallization: Near-Collapsing Process Graph Interpretations of  Regular Expressions)