We characterize must testing equivalence on CSP in terms of the unique homomorphism from the Moore automaton of CSP processes to the final Moore automaton of partial formal power series over a certain semiring. The final automaton is then turned into a CSP-algebra: operators and fixpoints are defined, respectively, via behavioural differential equations and simulation relations. This structure is then shown to be preserved by the final homomorphism. As a result, we obtain a fully abstract compositional model of CSP phrased in purely set-theoretical terms.
|Autori:||Boreale M.; Gadducci F.|
|Titolo:||Processes as formal power series: A coinductive approach to denotational semantics|
|Anno del prodotto:||2006|
|Digital Object Identifier (DOI):||10.1016/j.tcs.2006.05.030|
|Appare nelle tipologie:||1.1 Articolo in rivista|