In the setting of session behaviours, we study an extension of the concept of compliance when a disciplined form of backtracking and of output skipping is present. After adding checkpoints to the syntax of session behaviours, we formalise the operational semantics via an LTS, and define natural notions of checkpoint compliance and sub-behaviour, which we prove to be both decidable. Then we extend the operational semantics with skips and we show the decidability of the obtained compliance.
Reversible client/server interactions
BARBANERA, Franco;
2016-01-01
Abstract
In the setting of session behaviours, we study an extension of the concept of compliance when a disciplined form of backtracking and of output skipping is present. After adding checkpoints to the syntax of session behaviours, we formalise the operational semantics via an LTS, and define natural notions of checkpoint compliance and sub-behaviour, which we prove to be both decidable. Then we extend the operational semantics with skips and we show the decidability of the obtained compliance.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
Barbanera2016_Article_ReversibleClientServerInteract.pdf
accesso aperto
Tipologia:
Versione Editoriale (PDF)
Licenza:
Dominio pubblico
Dimensione
1.19 MB
Formato
Adobe PDF
|
1.19 MB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
