Towards an infinitary logic of domains : Abramsky logic for transition systems
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.
|Modal logic (including the logic of norms) (msc 03B45), Logic in computer science (msc 03B70), Other infinitary logic (msc 03C75), Lattices and related structures (msc 03G10), Complete distributivity (msc 06D10), Duality (msc 55M05), Semantics (msc 68Q55)|
|Software (theme 1), Logistics (theme 3), Energy (theme 4)|
|Software Engineering [SEN]|
|Organisation||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.