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

We analyze a phenomenon called "image reflection" on a type ofcharacterization graphs -- LLEE charts -- of 1-free regular expressions modulobisimulation equivalence. Due to the correspondence between 1-free regularexpressions and the provable solutions of LEE/LLEE charts, this observationnaturally leads to a new proof for the completeness of the proof system\MilIfree\ for 1-free regular expressions modulo bisimulation equivalence. Thecritical part of the previous proof is to show that bisimulation collapse,which plays the role in linking the provable solutions of two LLEE charts, isstill an LLEE chart. The difference of our proof, compared to the previous one,is that we do not rely on the graph transformations from LLEE charts into theirbisimulation collapses by merging two bisimular nodes in each transformationstep. Instead, we directly show that the bisimulation collapse of an LLEE chartpossesses an LEE/LLEE structure based on its set of images mapped through thebisimulation function from the LLEE chart, and the constrained relation betweenthe images and their so-called "well-structured" looping-back charts pre-imageson the LLEE chart. Our approach provides a novel angle to look at this problemand related problems, and might introduce a different way for proving thecompleteness problem of \Mil\ for regular expressions modulo bisimulationequivalence, which had remained open until very recently.

Image Reflection on LLEE Charts -- Another Proof for the Completeness of an Axiomatization of 1-Free Regular Expressions Modulo Bisimilarity