Franco Barbanera (Dipartimento di Matematica e Informatica, University of Catania) |
Mariangiola Dezani-Ciancaglini (Dipartimento di Informatica, University of Torino) |
Ugo de' Liguoro (Dipartimento di Informatica, University of Torino) |
In the setting of session behaviours, we study an extension of the concept of compliance when a disciplined form of backtracking is present. After adding checkpoints to the syntax of session behaviours, we formalise the operational semantics via a LTS, and define a natural notion of checkpoint compliance. We then obtain a co-inductive characterisation of such compliance relation, and an axiomatic presentation that is proved to be sound and complete. As a byproduct we get a decision procedure for the new compliance, being the axiomatic system algorithmic. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.162.5 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |