Toward an Infinitary Logic of Domains: Abramsky Logic for Transition Systems |
| |
Authors: | Marcello M Bonsangue Joost N Kok |
| |
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. |
| |
Keywords: | |
本文献已被 ScienceDirect 等数据库收录! |