On incorrectness logic and Kleene algebra with top and tests

Kleene algebra with tests (KAT) is a foundational equational framework for reasoning about programs, which has found applications in program transformations, networking and compiler optimizations, among many other areas. In his seminal work, Kozen proved that KAT subsumes propositional Hoare logic, showing that one can reason about the (partial) correctness of while programs by means of the equational theory of KAT. In this work, we investigate the support that KAT provides for reasoning about incorrectness, instead, as embodied by O'Hearn's recently proposed incorrectness logic. We show that KAT cannot directly express incorrectness logic. The main reason for this limitation can be traced to the fact that KAT cannot express explicitly the notion of codomain, which is essential to express incorrectness triples. To address this issue, we study Kleene Algebra with Top and Tests (TopKAT), an extension of KAT with a top element. We show that TopKAT is powerful enough to express a codomain operation, to express incorrectness triples, and to prove all the rules of incorrectness logic sound. This shows that one can reason about the incorrectness of while-like programs by means of the equational theory of TopKAT.

An approach to Fuzzy clustering of the iris petals by using Ac-means Analysis

This paper proposes a definition of a fuzzy partition element based on the homomorphism between type-1 fuzzy sets and the three-valued Kleene algebra. A new clustering method based on the C-means algorithm, using the defined partition, is presented in this paper, which will be validated with the traditional iris clustering problem by measuring its petals.

Equivalence checking for weak bi-Kleene algebra

Pomset automata are an operational model of weak bi-Kleene algebra, which describes programs that can fork an execution into parallel threads, upon completion of which execution can join to resume as a single thread. We characterize a fragment of pomset automata that admits a decision procedure for language equivalence. Furthermore, we prove that this fragment corresponds precisely to series-rational expressions, i.e., rational expressions with an additional operator for bounded parallelism. As a consequence, we obtain a new proof that equivalence of series-rational expressions is decidable.

A Note on Congruences of Infinite Bounded Involution Lattices

We prove that an infinite (bounded) involution lattice and even pseudo-Kleene algebra can have any number of congruences between 2 and its number of elements or equalling its number of subsets, regardless of whether it has as many ideals as elements or as many ideals as subsets. Furthermore, when they have at most as many congruences as elements, these involution lattices and even pseudo-Kleene algebras can be chosen such that all their lattice congruences preserve their involutions, so that they have as many congruences as their lattice reducts. Under the Generalized Continuum Hypothesis, this means that an infinite (bounded) involution lattice and even pseudo-Kleene algebra can have any number of congruences between 2 and its number of subsets, regardless of its number of ideals. Consequently, the same holds for antiortholattices, a class of paraorthomodular Brouwer-Zadeh lattices. Regarding the shapes of the congruence lattices of the lattice{ ordered algebras in question, it turns out that, as long as the number of congruences is not strictly larger than the number of elements, they can be isomorphic to any nonsingleton well-ordered set with a largest element of any of those cardinalities, provided its largest element is strictly join-irreducible in the case of bounded lattice-ordered algebras and, in the case of antiortholattices with at least 3 distinct elements, provided that the predecessor of the largest element of that well-ordered set is strictly join{irreducible, as well; of course, various constructions can be applied to these algebras to obtain congruence lattices with different structures without changing the cardinalities in question. We point out sufficient conditions for analogous results to hold in an arbitrary variety.

The fragment of Classical Logic that respects the Variable-Sharing Principle

We examine the set of formula-to-formula valid inferences of Classical Logic, where the premise and the conclusion share at least a propositional variable in common. We review the fact, already proved in the literature, that such a system is identical to the first-degree entailment fragment of R. Epstein's Relatedness Logic, and that it is a non-transitive logic of the sort investigated by S. Frankowski and others. Furthermore, we provide a semantics and a calculus for this logic. The semantics is defined in terms of a \(p\)-matrix built on top of a 5-valued extension of the 3-element weak Kleene algebra, whereas the calculus is defined in terms of a Gentzen-style sequent system where the left and right negation rules are subject to linguistic constraints.

Models of Concurrent Kleene Algebra

Kleene Algebra and variants thereof have been successfully used in verification of se- quential programs. The leap to concurrent programs offers many challenges, both in terms of devising the right foundations to study concurrent variants of Kleene Algebra but also in finding the right models to enable effective verification of relevant programs. In this talk, we will review existing and ongoing work on concurrent Kleene Algebra with a focus on a variant called partially observable concurrent Kleene algebra (POCKA). POCKA offers an algebraic framework to reason about concurrent programs with control structures, such as conditionals and loops. We will show how a previously developed technique for com- pleteness of Kleene Algebra can be lifted to prove that POCKA is a sound and complete axiomatization of a model of partial observations. We illustrate the use of the framework in the analysis of sequential consistency, i.e., whether programs behave as if memory accesses taking place were interleaved and executed sequentially.The work described in this invited talk is based on [1, 2, 3], and it is joint with a won- derful group of people: Paul Brunet, Simon Docherty, Tobias Kapp ́e, Jurriaan Rot, Jana Wagemaker, and Fabio Zanasi.

Concurrent Kleene Algebra with Observations: From Hypotheses to Completeness

Concurrent Kleene Algebra (CKA) extends basic Kleene algebra with a parallel composition operator, which enables reasoning about concurrent programs. However, CKA fundamentally misses tests, which are needed to model standard programming constructs such as conditionals and $$\mathsf {while}$$ while -loops. It turns out that integrating tests in CKA is subtle, due to their interaction with parallelism. In this paper we provide a solution in the form of Concurrent Kleene Algebra with Observations (CKAO). Our main contribution is a completeness theorem for CKAO. Our result resorts on a more general study of CKA “with hypotheses”, of which CKAO turns out to be an instance: this analysis is of independent interest, as it can be applied to extensions of CKA other than CKAO.

Design Methodology for the Implementation of Fuzzy Inference Systems Based on Boolean Relations

This paper proposes a methodology for the design of fuzzy inference systems based on Boolean relations. The approach using Boolean sets presents limited performance due to the abrupt transitions that occur during its functioning, therefore, fuzzy sets can be used aiming the improvement of the performance. In this approach, firstly, the design of a Boolean controller is performed, which is later extended into fuzzy under design guidelines proposed in this paper. The methodology uses Kleene algebra via truth tables for the fuzzy system design, allowing the simplification of the equations that implement the fuzzy system.