0000000000052150
AUTHOR
Klaus Barthelmann
showing 6 related works from this author
Nondeterministic operations on finite relational structures
1998
Abstract This article builds on a tutorial introduction to universal algebra for language theory (Courcelle, Theoret. Comput. Sci. 163 (1996) 1–54) and extends it in two directions. First, nondeterministic operations are considered, i.e., operations which give a set of results instead of a single one. Most of their properties concerning recognizability and equational definability carry over from the ordinary case with minor modifications. Second, inductive sets of evaluations are studied in greater detail. It seems that they are handled most naturally in the framework presented here. We consider the analogues of top-down and bottom-up tree transducers. Again, most of their closure propertie…
Process specification and verification
1996
Graph grammars provide a very convenient specification tool for distributed systems of processes. This paper addresses the problem how properties of such specifications can be proven. It shows a connection between algebraic graph rewrite rules and temporal (trace) logic via the graph expressions of [2]. Statements concerning the global behavior can be checked by local reasoning.
Local Normal Forms for First-Order Logic with Applications to Games and Automata
1999
Building on work of Gaifman [Gai82] it is shown that every first-order formula is logically equivalent to a formula of the form ∃ x_1,...,x_l, \forall y, φ where φ is r-local around y, i.e. quantification in φ is restricted to elements of the universe of distance at most r from y. \par From this and related normal forms, variants of the Ehrenfeucht game for first-order and existential monadic second-order logic are developed that restrict the possible strategies for the spoiler, one of the two players. This makes proofs of the existence of a winning strategy for the duplicator, the other player, easier and can thus simplify inexpressibility proofs. \par As another application, automata mode…
Linear Types for Higher Order Processes with First Class Directed Channels
1995
Abstract We present a small programming language for distributed systems based on message passing processes. In contrast to similar languages, channels are one-to-one connections between a unique sender and a unique receiver process. Process definitions and channels are first class values and the topology of process systems can change dynamically. The operational semantics of the language is defined by means of graph rewriting rules. A static type system based on the notion of linear types ensures that channels are always used as one-to-one connections.
Graph-grammar semantics of a higher-order programming language for distributed systems
1994
We will consider a new tiny, yet powerful, programming language for distributed systems, called DHOP, which has its operational semantics given as algebraic graph rewrite rules in a certain category of labeled graphs. Our approach allows to separate actions which affect several processes from local changes such as variable bindings. We also sketch how to derive an implementation from this specification.
When can an equational simple graph be generated by hyperedge replacement?
1998
Infinite hypergraphs with sources arise as the canonical solutions of certain systems of recursive equations written with operations on hypergraphs. There are basically two different sets of such operations known from the literature, HR and VR. VR is strictly more powerful than HR on simple hypergraphs. Necessary conditions are known ensuring that a VR-equational simple hypergraph is also HR-equational. We prove that two of them, namely having finite tree-width or not containing the infinite bipartite graph, are also sufficient. This shows that equational hypergraphs behave like context-free sets of finite hypergraphs.