Denotational Testing Semantics in Coinductive Form

Abstract

Building on recent work by Rutten on coinduction and formal power series, we define a denotational semantics for the {\sc csp} calculus and prove it fully abstract for testing equivalence. The proposed methodology allows for abstract definition of operators in terms of {\em behavioural differential equations} and for coinductive reasoning on them, additionally dispensing with continuous order-theoretic structures.

@InProceedings\{boreale.gadduoci:denotational-testing-semantics-coinductive,
author = \{M. Boreale and F. Gadduoci},
title = \{Denotational Testing Semantics in Coinductive Form},
booktitle = \{Proc. of MFCS 2003},
year = \{2003},
volume = \{2747},
series = \{LNCS},
publisher = \{Springer},