On powerdomains and modality (Q1067409): Difference between revisions

Powerdomains of different kinds on the complete partial ordering (D,\(\subseteq)\) are results of certain algebraic constructions used to give denotational semantics of non-deterministic computations. The author presents a reformulation in terms of modal formulas. A (non- deterministic) D-computation is a finitely branching tree T with nodes t labelled by elements val(t) from D respecting \(\subseteq\). Branches of D are to be understood as computations beginning at its root with labels showing progress of the computation. Atomic sentences are isolated elements of D. The sentences of the language \(L_ 0\) are constructed by means of \(\square\), \(\vee\), that of \(L_ 1\) by means of \(\diamond\), and that of \(L_ 2\) by means of \(\square\), \(\diamond\), \(\vee\). The satisfaction relation \(t\vDash A\) for sentences A and nodes t of a fixed D-computation T is defined by letting \(t\vDash a\Leftrightarrow a\subseteq val(t)\) for atomic a and interpreting \(\diamond\) as ''true at this or some latter node'' and \(\square\) as ''inevitability'', i.e. \(t\vDash \square A\Leftrightarrow (t\vDash A\) or \(t'\vDash \square A\) for all t' immediately following t). Let \(\vDash A\) mean: \(t\vDash A\) for the root t of T. Define \(V_ i(T)=\{\square S\in L_ i:\) \(\vDash \square S\}\) for \(i=0,2\); \(V_ 1(T)=\{\diamond S\in L_ 1:\) \(\vDash \diamond S\}\). The 3 types of powerdomains (which the author names after Symth, Hoare and Plotkin) over given D are isomorphic respectively to the sets \(\{V_ i(T):\) T is D-computation\(\}\) ordered by inclusion. In fact it is possible to restrict \(L_ 0\) to sentences \(\square (a_ 1\vee...\vee a_ n)\) for atomic \(a_ i\), to restrict \(L_ 1\) to sentences \(\diamond a\) (or expand it to include arbitrary \(\diamond\), \(\vee)\), and to restrict \(L_ 2\) to \(\diamond a\), \(\square (a_ 0\vee...\vee a_ n)\).