Indeterminacy in concurrent computation: Difference between revisions

Revision as of 18:51, 13 January 2013

Revision as of 18:54, 13 January 2013

Line 20:

:The mathematical denotation denoted by a closed system <tt>S</tt> is found by constructing increasingly better approximations from an initial behavior called <tt>⊥_S</tt> using a behavior approximating function <tt>'''progression'''_S</tt> to construct a denotation (meaning ) for <tt>S</tt> as follows :

::<tt>'''Denote'''_S ≡ ⊔<submath>i∈ω \lim_{i \to \infty}</submath> '''progression'''_Sⁱ(⊥_S)</tt>

In this way, the behavior of <tt>S</tt> can be mathematically characterized in terms of all its possible behaviors (including those involving unbounded nondeterminism).