Building on recent work by Rutten on coinduction and formal power series, we define a denotational semantics for the CSP calculus and prove it fully abstract for testing equivalence. The proposed methodology allows for abstract definition of operators in terms of behavioural differential equations and for coinductive reasoning on them, additionally dispensing with continuous order-theoretic structures.
Denotational testing semantics in coinductive form
GADDUCCI, FABIO
2003-01-01
Abstract
Building on recent work by Rutten on coinduction and formal power series, we define a denotational semantics for the CSP calculus and prove it fully abstract for testing equivalence. The proposed methodology allows for abstract definition of operators in terms of behavioural differential equations and for coinductive reasoning on them, additionally dispensing with continuous order-theoretic structures.File in questo prodotto:
File | Dimensione | Formato | |
---|---|---|---|
mfcs03.pdf
solo utenti autorizzati
Tipologia:
Versione finale editoriale
Licenza:
NON PUBBLICO - Accesso privato/ristretto
Dimensione
201.1 kB
Formato
Adobe PDF
|
201.1 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.