Toward an infinitary logic of domains: abramsky logic for transition systems

Author(s):
Bonsangue, M.M. (0000-0003-3746-3618); Kok, J.N. (0000-0002-7352-1400)
Published
1999
Publication type
Article / Letter to editor

Abstract

We give a new characterization of sober spaces in terms of their completely distributive lattice of saturated sets. This characterization is used to extend Abramsky's results about a domain logic for transition systems. The Lindenbaum algebra generated by the Abramsky finitary logic is a distributive lattice dual to an SFP-domain obtained as a solution of a recursive domain equation. We prove that the Lindenbaum algebra generated by the infinitary logic is a completely distributive lattice dual to the same SFP-domain. As a consequence soundness and completeness of the infinitary logic is obtained for a class of transition systems that is computational interesting. (C) 1999 Academic Press.

Date issued
1999-11-01
Language
English
Publisher
Elsevier BV
Is part of
Information and Computation (1999), Vol. 155, no. 1-2, p. 170-201
hdl
1887/4083435
doi
10.1006/inco.1999.2827