Catálogo de publicaciones - libros

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 pairs. For lattices with negation, the relational structures require an additional binary relation satisfying certain conditions which derive from the properties of the negation. In each case, these conditions are sufficient to ensure that the lattice with negation is embeddable into the complex algebra of its canonical frame.

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 up a connection between hybrid systems and lazy semiring neighbours.

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 does not hold. Since in predicate-transformer models extensionality always holds, this means that the axioms of demonic refinement algebra do not characterise predicate-transformer models uniquely. The omega and the demonic refinement algebra of commands both utilise the convergence operator that is analogous to the halting predicate of modal -calculus. We show that the convergence operator can be defined explicitly in terms of infinite iteration and domain if and only if domain coinduction for infinite iteration holds.

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, the mathematical foundations for dealing with relations in such a context are not well-established, so we provide an appropriate generalisation of relational categories to semigroupoids to serve as specification for our interface.

After having established an appropriate interface for relation-algebraic programming, we also need an efficient implementation; we find this in BDD-based kernel library KURE of recent versions of the Kiel RelView system. We show how this combination enables high-level declarative and efficient relational programming in Haskell.

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 . 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 . We provide a representation theorem for these algebras and thus provide an algebraic proof of completeness of hybrid logic.

We describe , 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 simplify reasoning about distributed systems, where with purely algebraic reasoning they can reduce complicated interleaving behaviour to “separated” behaviours each of which can be analysed on its own. Until now that has not been possible for distributed systems.

Algebraic reasoning in general is very robust, and easy to check: thus an algebraic approach to probabilistic distributed systems is attractive because in that “doubly hostile” environment (probability interleaving) the opportunities for subtle error abound. Especially tricky is the interaction of probability and the demonic or “adversarial” scheduling implied by concurrency.

Our case study — based on Rabin’s — is one where just such problems have already occurred: the original presentation was later shown to have subtle flaws [15]. It motivates our interest in algebras, where assumptions relating probability and secrecy are clearly exposed and, in some cases, can be given simple characterisations in spite of their intricacy.