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.

, , , , , ,
, ,
Software Engineering [SEN]
Intelligent and autonomous systems

Bonsangue, M.M, & Kok, J.N. (1999). Towards an infinitary logic of domains : Abramsky logic for transition systems. Software Engineering [SEN]. CWI.