The topic of this paper is the determinization problem of ω-automata under the transition-based Emerson-Lei acceptance (called TELA), which generalizes all standard acceptance conditions and is defined using positive Boolean formulas. Such automata can be determinized by first constructing an equivalent generalized Büchi automaton (GBA), which is later determinized. The problem of constructing an equivalent GBA is considered in detail, and three new approaches of solving it are proposed. Furthermore, a new determinization construction is introduced which determinizes several GBA separately and combines them using a product construction. An experimental evaluation shows that the product approach is competitive when compared with state-of-the-art determinization procedures. The second part of the paper studies limit-determinization of TELA and we show that this can be done with a single-exponential blow-up, in contrast to the known double-exponential lower-bound for determinization. Finally, one version of the limit-determinization procedure yields good-for-MDP automata which can be used for quantitative probabilistic model checking.

The classic theorems of Büchi and Kleene state the expressive equivalence of finite automata to monadic second order logic and regular expressions, respectively. These fundamental results enjoy applications in nearly every field of theoretical computer science. Around the same time as Büchi and Kleene, Rabin investigated probabilistic finite automata. This equally well established model has applications ranging from natural language processing to probabilistic model checking. Here, we give probabilistic extensions Büchi\\\'s theorem and Kleene\\\'s theorem to the probabilistic setting. We obtain a probabilistic MSO logic by adding an expected second order quantifier. In the scope of this quantifier, membership is determined by a Bernoulli process. This approach turns out to be universal and is applicable for finite and infinite words as well as for finite trees. In order to prove the expressive equivalence of this probabilistic MSO logic to probabilistic automata, we show a Nivat-theorem, which decomposes a recognisable function into a regular language, homomorphisms, and a probability measure. For regular expressions, we build upon existing work to obtain probabilistic regular expressions on finite and infinite words. We show the expressive equivalence between these expressions and probabilistic Muller-automata. To handle Muller-acceptance conditions, we give a new construction from probabilistic regular expressions to Muller-automata. Concerning finite trees, we define probabilistic regular tree expressions using a new iteration operator, called infinity-iteration. Again, we show that these expressions are expressively equivalent to probabilistic tree automata. On a second track of our research we investigate Constraint LTL over multidimensional data words with data values from the infinite tree. Such LTL formulas are evaluated over infinite words, where every position possesses several data values from the infinite tree. Within Constraint LTL on can compare these values from different positions. We show that the model checking problem for this logic is PSPACE-complete via investigating the emptiness problem of Constraint Büchi automata.

We give a necessary and sufficient condition for the existence of an increasing coupling of N (N >= 2) synchronous dynamics on S-Zd (PCA). Increasing means the coupling preserves stochastic ordering. We first present our main construction theorem in the case where S is totally ordered; applications to attractive PCAs are given. When S is only partially ordered, we show on two examples that a coupling of more than two synchronous dynamics may not exist. We also prove an extension of our main result for a particular class of partially ordered spaces.

1. Endliche Automaten 1.1. Deterministische und Nichtdeterministische Automaten 1.2. Reguläre Mengen und Reguläre Ausdrücke 1.3. Eigenschaften regulärer Sprachen und endlicher Automaten 1.4. Spezielle Automaten und Anwendungen 2. Formale Sprachen und Grammatiken 2.1. Semiotische Grundbegriffe 2.2. Regelgrammatiken und Chomsky-Klassifikation 2.3. Kontextfreie Grammatiken und Sprachen 2.4. Kontextabhängige Sprachen 3. Automaten und Sprachen 3.1. Kellerautomaten und kontextfreie Sprachen 3.2. Turing-Automaten und Regel-Sprachen 3.3. Linear-beschränkte Automaten und kontextabhängige Sprachen 3.4. Sprach- und Automatenklassen Stichwortverzeichnis

Ziel dieser Arbeit ist es, das physikalische Problem der Bestimmung der Gestalt der Flüssigkeitsoberflächer bei der Ausbreitung von Wasserwellen durch zellularen Automaten zu modellieren und anschließend die Ergebnisse durch Computerprogramme graphisch darzustellen. Für eindimensionale Wellen wird die Oberfläche durch einen einfachen zellularen Automaten modelliert. Durch Erweiterung des Automaten um eine Gedächtnisfunktion kann die Interaktion zwischen zwei Wellen einfacher Gestalt (Solitonen) bzw. zwischen einer solchen Welle und einem reflektierenden Rand modelliert werden. In Anhang werden Hinweise zur Berechnung einer speziellen zweidimensionalen Wellenform mit Mathematica gegeben. / We concider cellular automata to describe the surface of waterwaves. This description will be used in computer graphics. Simple cellular automata decribe the surface in the case of onedimensional waves. Introducing a memory effect we also obtain results about the interaction of two solitone waves and about the reflection of a solitone wave at the boundary. The Apendix contains hints about the computation of a special twodimensional wave using Mathematica.

Recently, multi-priced timed automata have received much attention for real-time systems. These automata extend priced timed automata by featuring several price parameters. This permits to compute objectives like the optimal ratio between rewards and costs. Arising from the model of timed automata, the multi-weighted setting has also attracted much notice for classical nondeterministic automata. The present thesis develops multi-weighted MSO-logics on finite, infinite and timed words which are expressively equivalent to multi-weighted automata, and studies decision problems for them. In addition, a Nivat-like theorem for weighted timed automata is proved; this theorem establishes a connection between quantitative and qualitative behaviors of timed automata. Moreover, a logical characterization of timed pushdown automata is given.

Proceedings with the revised papers of the FSMNLP (Finite-state Methods and Natural Language Processing) 2007 Workshop in Potsdam / Tagungsband mit den Beiträgen der FSMNLP (Finite-state Methods and Natural Language Processing) 2007 in Potsdam

For a general attractive Probabilistic Cellular Automata on S-Zd, we prove that the (time-) convergence towards equilibrium of this Markovian parallel dynamics, exponentially fast in the uniform norm, is equivalent to a condition (A). This condition means the exponential decay of the influence from the boundary for the invariant measures of the system restricted to finite boxes. For a class of reversible PCA dynamics on {1,+1}(Zd), wit a naturally associated Gibbsian potential rho, we prove that a (spatial-) weak mixing condition (WM) for rho implies the validity of the assumption (A); thus exponential (time-) ergodicity of these dynamics towards the unique Gibbs measure associated to rho hods. On some particular examples we state that exponential ergodicity holds as soon as there is no phase transition.

Building and mantaining large-scale ontologies is an error-prone task. It is thus not uncommon to find unwanted or unexpected consequences that follow implicitely from the restrictions in the ontology. To understand and correct these consequences, it is helpful to find the specific portions of the ontology that are responsible for them. Axiom-pinpointing is the task of finding minimal subontologies that entail a given consequence, also called MinAs. In this work we look at the task of computing all the MinAs by means of modified decision procedures. We first show that tableaux- and automata-based decision procedures can be transformed into pinpointing algorithms that output a (compact) representation of the set of all MinAs. We then explore the complexity of the problem.

In Premium-Fahrzeugen werden derzeit ca. 60-70 Steuergeräte (SG) verbaut. Steuergeräte sind „eingebettete Systeme“ und stellen die zentralen Rechen- und Steuereinheiten für die elektrischen und elektronischen Systeme im Fahrzeug dar. Mit Hilfe der Steuergeräte, die über Bus-Systeme (z.B. CAN-Bus) miteinander vernetzt sind, können komplexe Funktionen realisiert werden. Das Motor- Steuergerät ist eines der bekanntesten. Der steigende Innovationsgrad im Elektrik- / Elektronik- Umfeld zwingt die Autohersteller, in immer kürzeren Zeitabständen, neue Steuergeräte mit höherer Rechenleistung und neuen Funktionen zu entwickeln. Aufgrund der steigenden Anzahl von Steuergeräten, spielt deren Rückwärtskompatibilität eine immer wichtigere Rolle.