The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
9th International Conference on Relational Methods in Computer Science and 4th International Workshop on Applications of Kleene Algebra, RelMiCS/AKA 2006, Manchester, UK, August 29–September 2, 2006. Proceedings
The Kleene algebra axioms are too strong for some program models of interest (e.g. models that mix demonic choice with angelic or probabilistic choice). This has led to proposals that weaken the right distributivity axiom to monotonicity, and possibly weaken or eliminate the right induction and left annihilation axioms (e.g. lazy Kleene algebra, probabilistic Kleene algebra, monodic tree Kleene algebra,...
The class of finite symmetric integral relation algebras with no 3-cycles is a particularly interesting and easily analyzable class of finite relation algebras. For example, it contains algebras that are not representable, algebras that are representable only on finite sets, algebras that are representable only on infinite sets, algebras that are representable on both finite and infinite sets, and...
We explore the view of a computation as a relational section of a (trivial) fibre bundle: initial states lie in the base of the bundle and final states lie in the fibres located at their initial states. This leads us to represent a computation in ‘fibre-form’ as the angelic choice of its behaviours from each initial state. That view is shown to have the advantage also of permitting final states to...
The formal analysis of programs with arrays is a notoriously difficult problem due largely to aliasing considerations. In this paper we augment the rules of Kleene algebra with tests (KAT) with rules for the equational manipulation of arrays in the style of schematic KAT. These rules capture and make explicit the essence of subscript aliasing, where two array accesses can be to the same element. We...
Most previous work on the semantics of programs with local state involves complex storage modeling with pointers and memory cells, complicated categorical constructions, or reasoning in the presence of context. In this paper, we explore the extent to which relational semantics and axiomatic reasoning in the style of Kleene algebra can be used to avoid these complications. We provide (i) a fully compositional...
We model groups as relational systems and develop relation-algebraic specifications for direct products of groups, quotient groups, and the enumeration of all subgroups and normal subgroups. The latter two specifications immediately lead to specifications of the lattices of subgroups and normal subgroups, respectively. All specifications are algorithmic and can directly be translated into the language...
Pratt [22] defines action algebras as Kleene algebras with residuals. In [9] it is shown that the equational theory of *-continuous action algebras (lattices) is Π –complete. Here we show that the equational theory of relational action algebras (lattices) is Π –hard, and some its fragments are Π –complete. We also show that the equational theory of action algebras...
We first recall the concept of Kleene algebra with domain (KAD). Then we explain how to use the operators of KAD to define a demonic refinement ordering and demonic operators (many of these definitions come from the literature). Then, taking the properties of the KAD-based demonic operators as a guideline, we axiomatise an algebra that we call Demonic algebra with domain (DAD). The laws of DAD not...
The theory of Boolean contact algebras has been used to represent a region based theory of space. Some of the primitives of Boolean algebras are not well motivated in that context. One possible generalization is to drop the notion of complement, thereby weakening the algebraic structure from Boolean algebra to distributive lattice. The main goal of this paper is to investigate the representation theory...
We give a brief overview of the axiomatic development of betweenness relations, and investigate the connections between these and comparability graphs. Furthermore, we characterize betweenness relations induced by reflexive and antisymmetric binary relations, thus generalizing earlier results on partial orders. We conclude with a sketch of the algorithmic aspects of recognizing induced betweenness...
Relational representation theorems are presented for general (i.e., non-distributive) lattices with the following types of negations: De Morgan, ortho, Heyting and pseudo-complement. The representation is built on Urquhart’s representation for lattices where the associated relational structures are doubly ordered sets and the canonical frame of a lattice consists of its maximal disjoint filter-ideal...
We introduce a strategy for the verification of relational specifications based on the analysis of monotonicity of variables within formulas. By comparing with the Alloy Analyzer, we show that for a relevant class of problems this technique outperforms analysis of the same problems using SAT-solvers, while consuming a fraction of the memory SAT-solvers require.
Max-plus analogues of linear spaces, convex sets, and polyhedra have appeared in several works. We survey their main geometrical properties, including max-plus versions of the separation theorem, existence of linear and non-linear projectors, max-plus analogues of the Minkowski-Weyl theorem, and the characterization of the analogues of “simplicial” cones in terms of distributive lattices.
We extend an earlier algebraic approach to Neighbourhood Logic (NL) from domain semirings to lazy semi-rings yielding lazy semiring neighbours. Furthermore we show three important applications for these. The first one extends NL to intervals with infinite length. The second one applies lazy semiring neighbours in an algebraic semantics of the branching time temporal logic CTL *. The third one sets...
Weak omega algebra and demonic refinement algebra are two ways of describing systems with finite and infinite iteration. We show that these independently introduced kinds of algebras can actually be defined in terms of each other. By defining modal operators on the underlying weak semiring, that result directly gives a demonic refinement algebra of commands. This yields models in which extensionality...
We present a Haskell interface for manipulating finite binary relations as data in a point-free relation-algebraic programming style that integrates naturally with the current Haskell collection types. This approach enables seamless integration of relation-algebraic formulations to provide elegant solutions of problems that, with different data organisation, are awkward to tackle. Perhaps surprisingly,...
This paper will discuss and characterise the cardinality of boolean (crisp) and fuzzy relations. The main result is a Dedekind inequality for the cardinality, which enables us to manipulate the cardinality of the composites of relations. As applications a few relational proofs for the basic theorems on graph matchings, and fundamentals about network flows will be given.
We model a set of search points as a relation and use relational algebra to evaluate all elements of the set in one step in order to select search points with certain properties. Therefore we transform relations into vectors and prove a formula to translate properties of relations into properties of the corresponding vectors. This approach is applied to timetable problems.
This paper introduces an algebraic semantics for hybrid logic with binders ${\mathcal{H}(\downarrow,@)}$ . It is known that this formalism is a modal counterpart of the bounded fragment of the first-order logic, studied by Feferman in the 1960’s. The algebraization process leads to an interesting class of boolean algebras with operators, called substitution-satisfaction algebras. We provide a...
We describe pKA, a probabilistic Kleene-style algebra, based on a well known model of probabilistic/demonic computation [3,16,10]. Our technical aim is to express probabilistic versions of Cohen’s separation theorems. Separation theorems simplify reasoning about distributed systems, where with purely algebraic reasoning they can reduce complicated interleaving behaviour to “separated” behaviours...
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.