Infinite Traces, Acceptances, and CSPP

摘要

There is a long standing problem when infinite traces are included in deno-tational semantic models of CSP. Full models fail to be Complete Partial Orders under refinement. This paper introduces a novel, but entirely natural, way of representing infinite behaviour in which refinement is a Complete Partial Order when the alphabet of events is finite. Acceptance semantics also solves the problem of infinite behaviour with an infinite alphabet. That requires a different construction based on a metric space and will be described elsewhere.