Kurzfassungen
Wir betrachten krypotographische Protokolle auf Basis der der Grundoperationen wie beim Diffie-Hellman Protokoll.
In der Vergangenheit wurde bei einigen derartigen Protokollen, die zun"achst als sicher galten, eine Schwachstelle gefunden, "uber die ein Angreifer z.B. eine falsche Authentifizierung vort"auschen kann.
Entsprechend dem Dolev-Yao Modell hat der Angreifer die M"oglichkeit alle Nachrichten abzuh"oren, abzufangen und unter falschem Absender zu verschicken. Zudem ist der Angreifer selbst ein legitimer Benutzer des Netzwerks. Andererseits wird angenommen, da"s der Angreifer z.B. nicht in der Lage ist, hinreichend gro"se Zahlen zu erraten, oder private Schl"ussel zu berechnen.
Dazu werden formale und automatische Methoden ben"otigt, mit denen entweder eine Schwachstelle aufgesp"urt oder die Sicherheit des Protokolls unter bestimmten Annahmen bewiesen werden kann. Dabei werden in "ahnlicher Weise wie bei der Verifikation von Software logische Kalk"ule verwendet.
An important aspect of counting in formal languages
is the ability to count letters in a string.
This has always been viewed as a benchmark
for language recognition formalisms.
For example, $\{a^nb^n|n>0\}$ is the ``prototype'' of a language
which is not regular.
In contrast to this, we show (published in [Rei01]) that
the language of pictures (two-dimensional words) with the same
number of $a$'s and $b$'s (and an appropriate length-width ratio)
is a recognizable picture language.
Here, we use counters similar to those used in [F\"ur82] and
combine it with the idea of a flow.
The picture languages considered here are characterized in [GRS94]
as existential monadic second order logic over two-dimensional structures.
To describe the power of logic, we consider its ability to
express representations of a counter.
This also means that counting in two-dimensional arrays is definable
in existential monadic second-order logic.
A more detailed version can be found in Chapter 4.3 in [Rei05].
Furthermore we show that the language of pictures over $\{a,b\}$,
in which all occurring $b$'s are connected, is recognizable.
This was published in [Rei98] and solves an open problem in [Mat98].
A more detailed version can be found in Chapter 4.4 in [Rei05].
The result is achieved by organizing the $b$'s in a tree while
avoiding non-connected cycles which could otherwise not be distinguished
locally.
The same problem caused by cycles arises when we consider a certain
notion of determinism which is independent from the direction in the picture.
The inclusion of the deterministic class in the nondeterministic class
is not anymore obvious here.
We can generalize the construction for avoiding cycles to show that
mono-causal deterministically recognizable
picture languages are recognizable.
Furthermore we discuss possible deterministic methods for counting at
least for the case that the picture is a square of a power of the 2 size.
References and more information can be found at\\
http://www-fs.informatik.uni-tuebingen.de/$\sim$reinhard/piclang
Pictures are a natural two-dimensional extension of words. The class of recognizable picture languages is characterized by several formalisms, among them existential monadic second-order logic and tiling systems. We show that counting and connectedness are definable properties. Different notions of determinism are discussed.
Presburger showed that first order logic over natural numbers with addition is decidable. We extend this result by additionally allowing monotone transitive closure operators in the formula. This allows us to decide the reachability problem for Petri nets in which inhibitor arcs occur only in some restricted way and the emptiness- and word problem for priority-multicounter-automata. This has consequences for semi-trace-languages and the Nonterminal Complexity of Graph-controlled Grammars, Programmed Grammars and Matrix Grammars.
Authors: Faisal N. Abu-Kzam and Henning Fernau
The notion of a "problem kernel" plays a central role in the design of
fixed-parameter algorithms. The FTP literature is rich in kernalization
algorithms that exhibit fundamentally different approaches.
We highlight these differences and discuss several generalizations
and restrictions of the standard notion.
Bilder sind eine natürliche zweidimensionale Erweiterung von
Wörtern.
Die Klasse der erkennbaren Bildsprachen wird durch verschiedene
Formalismen charakterisiert, darunter die existentielle monadische Logik zweiter Stufe.
Die Beschreibungsmächtigkeit geht weit über die im
eindimensionalen Spezialfall (reguläre Sprachen) hinaus.
Wir zeigen, dass Zählen, Zusammenhang und Azyklizität definierbare
Eigenschaften sind und diskutieren verschiedene deterministische Varianten der
erkennbaren Bildsprachen (darunter der "Sudoku-"Determinismus).
Presburger zeigte, dass Logik der ersten Stufe über den
natürliche Zahlen mit Addition entscheidbar ist.
Wir erweitern dieses Resultat auf die zusätzliche Anwendung von
monotonen Transitive-Hülle-Operatoren. Damit kann das Erreichbarkeitsproblem
in Petrinetzen, in denen Inhibitorkanten nur in eingeschränkter Anordnung vorkommen,
entschieden werden. Dies hat Konsequenzen für Halbspursprachen und die
Nichtterminalkomplexität von Graph-kontrollierten Grammatiken,
programmierten Grammatiken und Matrixgrammatiken.
We define 2 operators on relations over natural numbers such that they
generalize the operators '+' and '*' and show that the membership
and emptiness problem of relations constructed from finite relations
with these operators and $\cup$ is decidable.
This generalizes Presburger arithmetics and allows to decide
the reachability problem for
those Petri nets where inhibitor arcs occur only in some restricted way.
Especially the reachability problem is decidable for
Petri nets with only one inhibitor arc, which solves an open problem
in \cite{KLM89} .
Furthermore we describe the corresponding automaton having a
decidable emptiness problem.
Presburger zeigte, dass Logik der ersten Stufe über den
natürliche Zahlen mit Addition entscheidbar ist.
Wir erweitern dieses Resultat auf die zusätzliche Anwendung von
monotonen Transitive-Hülle-Operatoren.
Dazu definieren wir zwei Operatoren auf Relationen über den
natürlichen Zahlen, die die Operatoren '+' und '*' verallgemeinern,
und zeigen dass das Leerheitsproblem für Relationen, die mit
diesen Operatoren und $\cup$ konstruiert werden, entscheidbar ist.
Damit kann das Erreichbarkeitsproblem
in Petrinetzen, in denen Inhibitorkanten nur in eingeschränkter Anordnung
vorkommen (z.B. mit nur einer Inhibitorkante), entschieden werden.
last modified Mon Feb 26 2007 by
Klaus Reinhardt