Transformace výrazů CCS do GCCS

Opačný směr korespondence GCCS a CCS není náplní této práce, nicméně tu uvedeme pár postřehů. Motivací pro transformaci výrazů CCS na systémy GCCS může být hned několik. Snad nejvýraznější z nich jsou tyto:

• Grafické zobrazení systémů specifikovaných pomocí CCS.
• Grafické znázornění výsledků verifikačních algoritmů vyjádřených v CCS.
• Možnost specifikovat systém kombinovaně (textově i graficky) pomocí CCS i GCCS.

Při návrhu algoritmu pro překlad systémů definic CCS do GCCS je nutné si zejména uvědomit odlišné chápání pojmu procesu v CCS a GCCS a dvouvrstvou architekturu syntaxe GCCS. V principu lze překládat přímo systémy definic CCS, v nichž je tato dvouvrstvá architektura dodržena. To klade následující požadavky na strukturu výrazů CCS v těchto systémech:

• Systém CCS je nutné rozdělit na dvě disjunktní množiny definic.
• První množina definic obsahuje ve výrazech na pravé straně pouze operátory prefix a sumace, přičemž žádný z podtermů neobsahuje jméno procesu definovaného definicí ze druhé množiny. V podstatě se jedná o definice procesů ve smyslu GCCS.
• Druhá množina obsahuje definice sestávající na pravé straně pouze z operátorů paralelní kompozice, restrikce a přejmenování. Na podtermy v tomto případě není třeba klást v principu žádné omezující předpoklady. V podstatě se jedná o definice sítí ve smyslu GCCS.

Dále je nutné si uvědomit, že procesy GCCS, s nimiž jsme pracovali, jsou konečně stavové. Zejména není tedy prakticky možné transformovat procesy s nekonečnou sumací. Tento směr transformace tedy bude směřovat k určitému vhodnému omezování syntaxe vstupních CCS výrazů (příp. systémů definic).

Další problém, který je třeba řešit, je jak přehledně graficky zobrazit získané termy GCCS, tj. aby zejména nedocházelo ke křížení hran. Zde bude nutné najít vhodné geometrické algoritmy, které by tento problém alespoň parciálně řešily.

Celkem je vidět, že problém opačného směru transformace spočívá především v nalezení vhodného přehledného grafického vyjádření obecně komplikovaných výrazů algebry procesů CCS.