search

CinRC / IRDC-CCSK

Java implementation of distributed reversible computation verification
https://spots.augusta.edu/caubert/cinrc/
GNU General Public License v3.0
4 stars 2 forks source link

Document LTS / SOS #43

Closed aubertc closed 1 year ago

aubertc commented 1 year ago

The LTS (labelled transition system, or SOS, for structural operational semantics) of CSSK is the set of "reduction rules" describing how the system reacts / evolves. It is given, for instance, in Forward-Reverse Observational Equivalences in CCSK, page 4 (for the forward-only system):

Screenshot_20230118_113955

I believe it would benefit this project to:

std(X) -------------- TOP $\alpha.X \xrightarrow{\alpha[m]} \alpha[m].X$

(or some other formalism)

aubertc commented 1 year ago

This will be solved when https://github.com/CinRC/IRDC-CCSK/pull/53 is merged, thanks to https://github.com/CinRC/IRDC-CCSK/pull/53/commits/41508c660149f4be70207a3831c943dce64a4f77