On Weak Bisimilarities in CCSK
Di cosa parla
In CCSK, un'estensione reversibile di CCS, si confrontano diverse nozioni di bisimilarità, cioè modi per dire se due processi mostrano lo stesso comportamento quando eseguono azioni avanti o indietro. Per il caso debole e reversibile vengono proposte due varianti, direzionale e mista, che differiscono sul fatto che le azioni interne (indicate con τ, cioè azioni non osservabili) debbano avere la stessa direzione dell’azione corrispondente. Gli autori mostrano che la bisimilarità mista è una congruenza e ignora completamente le azioni interne.
Cosa permette di osservare
Consente di esplorare come confrontare il comportamento di sistemi che possono tornare indietro: in particolare se e come le azioni non osservabili vadano coordinate con le mosse osservabili, e quali scelte mantengono l’equivalenza anche inserendo i processi in contesti più ampi.
Dalla fonte
In the context of CCSK, a reversible extension of CCS, we study different notions of bisimilarity (strong/weak, forward-only/reversible) and highlight their differences and commonalities. In particular, for the weak reversible case, not previously studied in the literature, we propose two variants, dubbed directional and mixed bisimilarity, depending on whether $\tau$ actions should be in the same direction (forward/backward) as the action being matched or not. We show, in particular, that mixed bisimilarity is a congruence and completely abstracts away from $\tau$ actions.