Separability in Domain Semirings
Dexter C. Kozen · OPUS (Augsburg University) · 2004
Abstract. First, we show with two examples that in test semirings with an incomplete test algebra a domain operation may or may not exist. Second, we show that two notions of separability in test semirings coincide, respectively, with locality of composition and with extensionality of the diamond operators in domain semirings. We conclude with a brief comparison of dynamic algebras and modal Kleene algebras. 1 Basic Definitions A test semiring [6] is a two-sorted structure (K, test(K)), where K is an idempotent semiring and test(K) ⊆ K is a Boolean algebra embedded into K such that the operations of test(K) coincide with the restricted operations of K. In particular, p ≤ 1 for all p ∈ test(K). In general, test(K) may be a proper subset of all elements below 1. A domain semiring [1] is a structure (K, �), where K is an idempotent semiring such that the domain operation �: K → test(K) satisfies, for all a, b ∈ K and p ∈ test(K), a ≤ �a a, (D1) �(pa) ≤ p. (D2) The conjunction of (D1) and (D2) is equivalent to each of �a ≤ p ⇔ a = pa, (LLP) �a ≤ p ⇔ ¬pa = 0, (GLA) which constitute elimination laws for domain. (LLP) says that �a is the least left preserver of a. (GLA) says that ¬�a is the greatest left annihilator of a. Both properties obviously characterize domain in set-theoretic relations. An important consequence of the axioms is strictness of the domain operation: a = 0 ⇔ �a = 0. (1) Moreover, we have the following useful proof principle.