On powerdomains and modality
type: Item
instance of: scholarly article
title: On powerdomains and modality
zbMATH Open document ID: 0579.68018
DOI: 10.1016/0304-3975(85)90037-4
author: Glynn Winskel
published in: Theoretical Computer Science
publication date: 1985-01-01T00:00:00Z
review text: 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)\).
Mathematics Subject Classification ID: 68Q65
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03B45
zbMATH DE Number: 3928337
zbMATH Keywords: modal logic
zbMATH Keywords: denotational semantics of non-deterministic computations
zbMATH Keywords: branching tree
reviewed by: G. E. Mints
MaRDI profile type: Publication
full work available at URL: 0304-3975(85)90037-4
OpenAlex ID: W1968606491
cites work: Q3917476
cites work: Q4133603
cites work: Algebraic semantics
cites work: Q3883467
cites work: Q3662610
cites work: Q3907039
cites work: Q4845486
cites work: Proving Liveness Properties of Concurrent Programs
cites work: A Powerdomain Construction
cites work: Q4749207
cites work: Q4195918
cites work: Q3959414
description: scientific article; zbMATH DE number 3928337