Towards an Infinitary Logic of Domains: Abramsky Logic for Transition Systems.211 Software Engineering

摘要

The authors give a new characterization of sober spaces in terms of their211u001ecompletely distributive lattice of saturated sets. This characterization is used 211u001eto extend Abramsky's results about a domain logic for transition systems. The 211u001eLindenbaum algebra generated by the Abramsky finitary logic is a distributive 211u001elattice dual to an SFP-domain obtained as a solution of a recursive domain 211u001eequation. We prove that the Lindenbaum algebra generated by the infinitary logic 211u001eis a completely distributive lattice dual to the same SFP-domain. As a 211u001econsequence soundness and completeness of the infinitary logic is obtained for a 211u001eclass of transition systems that is computational interesting.