185 research outputs found
Relations and Kleene Algebra in Computer Science - PHD Programme at RelMiCS10 / AKA5
No full textThis volume contains the tutorial materials and the contributed extended abstracts of the PhD Programme at the 10th International Conference on Relational Methods in Computer Science (RelMiCS10) and the 5th International Conference on Applications of Kleene Algebra (AKA5). The programme has been organised for the second time in association with RelMiCS/AKA. It took place in Frauenwörth on an Island in Lake Chiem in Bavaria, from April 7 to April 11, 2008, and included invited tutorials, a student session and attendance at the conference. Eight extended abstracts by students were selected for the programme by the organisers due to the relevance and quality of their submissions. They nicely reflect the diverse applications of relations and Kleene algebras in computing. The student session allowed the participants to present and discuss their own work. In addition there were three invited tutorials: Basics of Relation Algebra by Jules Desharnais (Université Laval, Quebec, Canada), Basics of Modal Kleene Algebra by Georg Struth (University of Sheffield, UK) and Basics of Preference and Fuzzy Preference Modeling by Susanne Saminger (Universität Linz, Austria). The RelMiCS/AKA conference series is the main forum for the relational calculus as a conceptual and methodological tool and for topics related to Kleene algebras. This year's proceedings, published as volume 4988 of the Springer LNCS series, contain 28 contributions by researchers from all over the world. Next to 26 regular papers there are the invited papers Formal Methods and the Theory of Social Choice by Marc Pauly (Stanford University, USA) and Relations Making Their Way from Logics to Mathematics and Applied Sciences, by Gunther Schmidt (University of the Armed Forces Munich, Germany). The papers show that relational and Kleene Algebra methods have wide-ranging impact and applicability in theory and practice
Calculating Church-Rosser proofs in Kleene algebra
No full textCalculating Church-Rosser Proofs in Kleene Algebra. - In: Relational methods in computer science : 6th International Conference, RelMiCS 2001 and 1st Workshop of COST Action 274 TARSKI, Oisterwijk, The Netherlands, October 16 - 21, 2001 ; revised papers / Harrie C. M. de Swart (ed.). - Berlin u.a. : Sprnger, 2001. - S. 276-290. - (Lecture notes in computer science ; 2561
Deriving Focused Lattice Calculi
No full textWe derive rewrite-based ordered resolution calculi for semilattices, distributive lattices and boolean lattices. Using ordered resolution as a metaprocedure, theory axioms are rst transformed into independent bases. Focused inference rules are then extracted from inference patterns in refutations. The derivation is guided by mathematical and procedural background knowledge, in particular by ordered chaining calculi for quasiorderings (forgetting the lattice structure), by ordered resolution (forgetting the clause structure) and by Knuth-Bendix completion for non-symmetric transitive relations (forgetting both structures). Conversely, all three calculi are derived and proven complete in a transparent and generic way as special cases of the lattice calculi
A calculus for set-based program development
No full textA Calculus for Set-Based Program Development. - In: Formal methods and software engineering : 5th International Conference on Formal Engineering Methods, ICFEM 2003, Singapore, November 5-7, 2003 ; proceedings / Jin Song Dong ... (eds.). - Berlin u.a. : Springer, 2003. - S. 541-559. - (Lecture notes in computer science ; 2885
On the Word Problem for Free Lattices
No full textWe prove completeness of a rewrite-based algorithm for the word problem in the variety of lattices and discuss the method of nonsymmetric completion with regard to this variety
Hoare semigroups
No full textA semigroup-based setting for developing Hoare logics and refinement calculi is introduced together with procedures for translating between verification and refinement proofs. A new Hoare logic for multirelations and two minimalist generic verification and refinement components, implemented in an interactive theorem prover, are presented as applications that benefit from this generalisation
Kleene Theorem for Higher-Dimensional Automata
No full textWe prove a Kleene theorem for higher-dimensional automata. It states that the languages they recognise are precisely the rational subsumption-closed sets of finite interval pomsets. The rational operations on these languages include a gluing composition, for which we equip pomsets with interfaces. For our proof, we introduce higher-dimensional automata with interfaces, which are modelled as presheaves over labelled precube categories, and develop tools and techniques inspired by algebraic topology, such as cylinders and (co)fibrations. Higher-dimensional automata form a general model of non-interleaving concurrency, which subsumes many other approaches. Interval orders are used as models for concurrent and distributed systems where events extend in time. Our tools and techniques may therefore yield templates for Kleene theorems in various models and applications
Parsing and Printing of and with Triples
No full textWe introduce the tool Amperspiegel, which uses triple graphs for parsing, printing and manipulating data. We show how to conveniently encode parsers, graph manipulation-rules, and printers using several relations. As such, parsers, rules and printers are all encoded as graphs themselves. This allows us to parse, manipulate and print these parsers, rules and printers within the system. A parser for a context free grammar is graph-encoded with only four relations. The graph manipulation-rules turn out to be especially helpful when parsing. The printers strongly correspond to the parsers, being described using only five relations. The combination of parsers, rules and printers allows us to extract Ampersand source code from ArchiMate XML documents. Amperspiegel was originally developed to aid in the development of Ampersand
Algebraic Investigation of Connected Components
No full textThis paper characterizes connected components of both directed and undirected graphs as atomic fixpoints. As algebraic structure for our investigations we combine complete Boolean algebras with the well-known theory of Kleene Algebra with domain. Using diamond operators as an algebraic generalization of relational image and preimage we show how connected components can be modeled as atomic fixpoints of functions operating on tests and prove some advanced theorems concerning connected components
- …
