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

Bonsangue, M.M.; Kok, J.N. (1999)

Article / Letter to editor

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.

• All authors: Bonsangue, M.M.; Kok, J.N.
• Date: 1999-11-01
• Journal: Information and Computation
• Volume: 155
• Issue: 1-2
• Pages: 170 - 201
• DOI: doi:10.1006/inco.1999.2827