September 2009 - tr-announce - lists.rwth-aachen.de

2009-18: Parametrized Regular Infinite Games and Higher-Order Pushdown Strategies
by Carsten Fuhs 23 Sep '09

23 Sep '09

The following technical report is available from http://aib.informatik.rwth-aachen.de: Parametrized Regular Infinite Games and Higher-Order Pushdown Strategies Paul Hänsch, Michaela Slaats, Wolfgang Thomas AIB 2009-18 Given a set $P$ of natural numbers, we consider infinite games where the winning condition is a regular $\omega$-language parametrized by $P$. In this context, an $\omega$-word, representing a play, has letters consisting of three components: The first is a bit indicating membership of the current position in $P$, and the other two components are the letters contributed by the two players. Extending recent work of Rabinovich we study here predicates $P$ where the structure $(\mathbb{N}, +1, P)$ belongs to the pushdown hierarchy (or ``Caucal hierarchy''). For such a predicate $P$ where $(\mathbb{N}, +1, P)$ occurs in the $k$-th level of the hierarchy, we provide an effective determinacy result and show that winning strategies can be implemented by deterministic level-$k$ pushdown automata.

1 0

2009-16: Vertex Splitting and the Recognition of Trapezoid Graphs
by Carsten Fuhs 23 Sep '09

23 Sep '09

The following technical report is available from http://aib.informatik.rwth-aachen.de: Vertex Splitting and the Recognition of Trapezoid Graphs George B. Mertzios, Derek G. Corneil AIB 2009-16 Trapezoid graphs are the intersection family of trapezoids where every trapezoid has a pair of opposite sides lying on two parallel lines. These graphs have received considerable attention and lie strictly between permutation graphs (where the trapezoids are lines) and cocomparability graphs (the complement has a transitive orientation). The operation of ``vertex splitting'', introduced in~\cite{CC}, first augments a given graph $G$ and then transforms the augmented graph by replacing each of the original graph's vertices by a pair of new vertices. This ``splitted graph'' is a permutation graph with special properties if and only if $G$ is a trapezoid graph. Recently vertex splitting has been used to show that the recognition problems for both tolerance and bounded tolerance graphs is NP-complete~\cite{MSZ2}. Unfortunately, the vertex splitting trapezoid graph recognition algorithm presented in~\cite{CC} is not correct. In this paper, we present a new way of augmenting the given graph and using vertex splitting such that the resulting algorithm is simpler and faster than the one reported in~\cite{CC}.

1 0

2009-17: Learning Communicating and Nondeterministic Automata
by Carsten Fuhs 22 Sep '09

22 Sep '09

The following technical report is available from http://aib.informatik.rwth-aachen.de: Learning Communicating and Nondeterministic Automata Carsten Kern AIB 2009-17 The results of this dissertation are two-fold. On the one hand, inductive learning techniques are extended and two new inference algorithms for inferring nondeterministic, and universal, respectively, finite-state automata are presented. On the other hand, certain learning techniques are employed and enhanced to semi-automatically infer communicating automata (also called design models in the software development cycle). For both topics, theoretical results on the feasibility of the approaches, as well as an implementation are presented which, in both cases, support our theory. Concerning the first objective to derive a so-called active online learning algorithm for nondeterministic finite-state automata (NFA), we present, in analogy to Angluin's famous learning algorithm L* for deterministic finite-state automata (DFA), a version for inferring a certain subclass of NFA. The automata from this class are called residual finite-state automata (RFSA). It was shown by Denis et al. that there is an exponential gap between the size of minimal DFA and their corresponding minimal RFSA. Even if there are also cases where the canonical (i.e., minimal) RFSA is exponentially larger than a corresponding minimal NFA, we show that the new learning algorithm---called NL*---is a great improvement compared to L* as the inferred canonical RFSA has always at most the size of the corresponding minimal DFA but is usually even considerably smaller and more easy to learn. Unlike a learning procedure developed by Denis et al.---called DeLeTe2---our algorithm is capable of deriving canonical RFSA. Like L*, the new algorithm will be applicable in many fields including pattern recognition, computational linguistics and biology, speech recognition, and verification. From our point of view, NL* might especially play a major role in the area of formal verification where the size of the models that are processed is of enormous importance and nondeterminism not regarded an unpleasant property. The second objective of this thesis is to create a method for inferring distributed design models (CFMs) from a given set of requirements specified as scenarios (message sequence charts). The main idea is to extend the L* algorithm to cope with valid and invalid sets of system runs and, after some iterations, come up with an intermediate design model (a DFA) which exhibits features that make it distributable into communicating components (or processes) interacting via FIFO channels. Theoretical results on which classes of CFMs are learnable in which time-complexity bounds are presented. We also developed a tool implementation called Smyle, realizing important theoretical results evolving from this part of the thesis. Based on this learning formalism we also derive a software-engineering lifecycle model called the Smyle Modeling Approach in which we embedded our learning approach. Additionally, we launched a project for a new learning library called libalf which includes most of the learning algorithms (and their extensions) mentioned in this thesis. We hope that, due to its continuously increasing functionality, libalf will find broad acceptance among researchers, and that it will be the starting point for an extensive project of different research groups which will employ libalf, or augment the library with new algorithms.

1 0