Author name cluster

Ralf Treinen

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

9 papers

2 author rows

I&C Journal 2017 Journal Article

Automata for unordered trees

Adrien Boiret
Vincent Hugot
Joachim Niehren
Ralf Treinen

We present a framework for defining automata for unordered data trees that is parametrised by the way in which multisets of children nodes are described. Presburger tree automata and alternating Presburger tree automata are particular instances. We establish the usual equivalence in expressiveness of tree automata and MSO for our framework. We then investigate subclasses of automata for unordered trees for which testing language equivalence is in P-time. Starting from automata in our framework that describe multisets of children by finite automata, we propose two approaches to do this deterministically. We show that confluent horizontal evaluation leads to polynomial-time emptiness and universality, but coNP-complete emptiness and intersection. Finally, efficient algorithms can be obtained by imposing an order of horizontal evaluation globally for all automata in the class. Depending on the choice of the order, we obtain different classes of automata, each of which has the same expressiveness as Counting Mso.

Details DOI

GandALF Workshop 2014 Workshop Paper

Deterministic Automata for Unordered Trees

Adrien Boiret
Vincent Hugot
Joachim Niehren
Ralf Treinen

Automata for unordered unranked trees are relevant for defining schemas and queries for data trees in Json or Xml format. While the existing notions are well-investigated concerning expressiveness, they all lack a proper notion of determinism, which makes it difficult to distinguish subclasses of automata for which problems such as inclusion, equivalence, and minimization can be solved efficiently. In this paper, we propose and investigate different notions of "horizontal determinism", starting from automata for unranked trees in which the horizontal evaluation is performed by finite state automata. We show that a restriction to confluent horizontal evaluation leads to polynomial-time emptiness and universality, but still suffers from coNP-completeness of the emptiness of binary intersections. Finally, efficient algorithms can be obtained by imposing an order of horizontal evaluation globally for all automata in the class. Depending on the choice of the order, we obtain different classes of automata, each of which has the same expressiveness as CMso.

PDF Details DOI

I&C Journal 2008 Journal Article

Symbolic protocol analysis for monoidal equational theories

Stéphanie Delaune
Pascal Lafourcade
Denis Lugiez
Ralf Treinen

We are interested in the design of automated procedures for analyzing the (in)security of cryptographic protocols in the Dolev–Yao model for a bounded number of sessions when we take into account some algebraic properties satisfied by the operators involved in the protocol. This leads to a more realistic model in comparison to what we get under the perfect cryptography assumption, but it implies that protocol analysis deals with terms modulo some equational theory instead of terms in a free algebra. The main goal of this paper is to setup a general approach that works for a whole class of monoidal theories which contains many of the specific cases that have been considered so far in an ad-hoc way (e. g. exclusive or, Abelian groups, exclusive or in combination with the homomorphism axiom). We follow a classical schema for cryptographic protocol analysis which proves first a locality result and then reduces the insecurity problem to a symbolic constraint solving problem. This approach strongly relies on the correspondence between a monoidal theory E and a semiring S E which we use to deal with the symbolic constraints. We show that the well-defined symbolic constraints that are generated by reasonable protocols can be solved provided that unification in the monoidal theory satisfies some additional properties. The resolution process boils down to solving particular quadratic Diophantine equations that are reduced to linear Diophantine equations, thanks to linear algebra results and the well-definedness of the problem. Examples of theories that do not satisfy our additional properties appear to be undecidable, which suggests that our characterization is reasonably tight.

Details DOI

I&C Journal 2007 Journal Article

Intruder deduction for the equational theory of Abelian groups with distributive encryption

Pascal Lafourcade
Denis Lugiez
Ralf Treinen

Cryptographic protocols are small programs which involve a high level of concurrency and which are difficult to analyze by hand. The most successful methods to verify such protocols are based on rewriting techniques and automated deduction in order to implement or mimic the process calculus describing the execution of a protocol. We are interested in the intruder deduction problem, that is vulnerability to passive attacks in presence of equational theories which model the protocol specification and properties of the cryptographic operators. In the present paper, we consider the case where the encryption distributes over the operator of an Abelian group or over an exclusive-or operator. We prove decidability of the intruder deduction problem in both cases. We obtain a PTIME decision procedure in a restricted case, the so-called binary case. These decision procedures are based on a careful analysis of the proof system modeling the deductive power of the intruder, taking into account the algebraic properties of the equational theories under consideration. The analysis of the deduction rules interacting with the equational theory relies on the manipulation of Z -modules in the general case, and on results from prefix rewriting in the binary case.

Details DOI

TCS Journal 2001 Journal Article

Grid structures and undecidable constraint theories

Franck Seynhaeve
Sophie Tison
Marc Tommasi
Ralf Treinen

We prove three new undecidability results for computational mechanisms over finite trees: There is a linear, ultra-shallow, noetherian and strongly confluent rewrite system R such that the ∃∗∀∗ -fragment of the first-order theory of one-step-rewriting by R is undecidable; the emptiness problem for tree automata with equality tests between cousins is undecidable; and the ∃∗∀∗ -fragment of the first-order theory of set constraints with the union operator is undecidable. The common feature of these three computational mechanisms is that they allow us to describe the set of first-order terms that represent grids. We extend our representation of grids by terms to a representation of linear two-dimensional patterns by linear terms, which allows us to transfer classical techniques on the grid to terms and thus to obtain our undecidability results.

Details DOI

I&C Journal 1998 Journal Article

How to Win a Game with Features

Rolf Backofen
Ralf Treinen

We employ the model-theoretic method of Ehrenfeucht–Fraı̈ssé games to prove the completeness of the theory CFT, which has been introduced by G. Smolka and R. Treinen (1994, J. Logic Programming 18(3), 229–258) for describing rational trees in a language of selector functions. The comparison to other techniques used in this field shows that Ehrenfeucht–Fraı̈ssé Games lead to simpler proofs.

Details DOI

TCS Journal 1998 Journal Article

The first-order theory of linear one-step rewriting is undecidable

Ralf Treinen

The theory of one-step rewriting for a given rewrite system R and signature σ is the first-order theory of the following structure: its universe consists of all σ-ground terms, and its only predicate is the relation “x rewrites to y in one step by R”. The structure contains no function symbols and no equality. We show that there is no algorithm deciding the ∃∗∀∗-fragment of this theory for an arbitrary finite, linear and non-erasing term-rewriting system. With the same technique we prove that the theory of encompassment plus one-step rewriting by the rule f(x) → g(x) and the modal theory of one-step rewriting are undecidable.

Details DOI

TCS Journal 1997 Journal Article

The first-order theory of lexicographic path orderings is undecidable

Hubert Comon
Ralf Treinen

We show, under some assumption on the signature, that the ∃∗∀∗ fragment of the theory of a lexicographic path ordering is undecidable, both in the partial and in the total precedence cases. Our result implies in particular that the simplification rule of ordered completion is undecidable.

Details DOI

MFCS Conference 1993 Conference Paper

Feature Constraints with First-Class Features

Ralf Treinen

Abstract Feature Constraint Systems have been proposed as a logical data structure for constraint (logic) programming. They provide a record-like view to trees by identifying subtrees by keyword rather than by position. Their atomic constraints are finer grained than in the constructor-based approach. The recently proposed CFT [15] in fact generalizes the rational tree system of Prolog II. We propose a new feature constraint system EF which extends CFT by considering features as first class values. As a consequence, EF contains constraints like x[ υ ]ω where υ is a variable ranging over features, while CFT restricts υ to be a fixed feature symbol. We show that the satisfiability of conjunctions of atomic EF -constraints is NP-complete. Satisfiability of quantifier-free EF -constraints is shown to be decidable, while the ∃ * ∀ * ∃ * fragment of the first order theory is undecidable.

Details