Die Dissertationsschrift stellt eine Toolkette zum abstrakten Entwurf von Mikrosystemen vor. Mikrosysteme können aus Elementen verschiedener physikalischer Domänen bestehen und zusätzlich digitale Hardware sowie Software enthalten. Die Erfassung und Formalisierung dieser heterogenen Systeme stellt den ersten Schritt im Entwurfsprozess dar, die damit verbundene neue Methodik des Designs von Mikrosystemen bildet den Kern der vorliegenden Arbeit. Zur Erfassung der analogen Spezifikationsteile enthält die Arbeit die Schilderung und Implementierung neuer Datenstrukturen, die ausgehend von einer ausführlichen Anforderungsanalyse geschaffen wurden. Das abstrakte Systemverhalten wird mit Hilfe hybrider Automaten modelliert, die sowohl mit speziellen hybriden Werkzeugen als auch mit SystemC-AMS simulierbar sind. Darüber hinaus beschäftigt sich die Arbeit mit der Erfassung von Signalverläufen und Schaltplaninformationen. Die formalisierten Anforderungen ermöglichen erste Prüfungen der Spezifikation auf Konsistenz. Zur Unterstützung niedriger Abstraktionsebenen wie der Differentialgleichungsebene steht ein Wandler von SystemC-AMS nach VHDL-AMS bereit. In die Systembeschreibung mit SystemC-AMS ist die Definition und Verknüpfung von Kostenparametern integrierbar. Das daraus entstehende globale Gütemaß hilft dem Entwerferteam, die optimale Systemrealisierung zu finden. / The PhD thesis proposes a toolflow for the design of microsystems on higher abstraction levels. Microsystems may consist of components using effects in different physical domains plus additional digital hardware and software. The collection and formalization of these heterogeneous systems is a first step in the design process, the associated design method ist the key point of this work. The system behavior is modeled using hybrid automata, which are checkable using hybrid modelcheckers and simulable using SystemC-AMS. Furthermore the work deals with signal forms and circuit parameters. To support modeling on lower abstraction levels like differential algebraic equations a syntax conversion from SystemC-AMS to VHDL-AMS was included. The integration of cost factors into SystemC-AMS allows design space exploration during system simulation.

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.

This thesis is concerned with automata over infinite trees. They are given a labeled infinite tree and accept or reject this tree based on its labels. A generalization of these automata with binary decisions are weighted automata. They do not just decide 'yes' or 'no', but rather compute an arbitrary value from a given algebraic structure, e.g., a semiring or a lattice. When passing from unweighted to weighted formalisms, many problems can be translated accordingly. The purpose of this work is to determine the feasibility of solving the inclusion problem for automata on infinite trees and its generalization to weighted automata, the infimum aggregation problem.

Die Anwendung von Methodiken und Technologien aus dem Bereich der Softwaretechnik auf den Bereich der Umweltmodellierung ist eine gemeinhin akzeptierte Vorgehensweise. Im Rahmen der "modellgetriebenen Entwicklung"(MDE, model-driven engineering) werden Technologien entwickelt, die darauf abzielen, Softwaresysteme vorwiegend auf Basis von im Vergleich zu Programmquelltexten relativ abstrakten Modellen zu entwickeln. Ein wesentlicher Bestandteil von MDE sind Techniken zur effizienten Entwicklung von "domänenspezifischen Sprachen"( DSL, domain-specific language), die auf Sprachmetamodellen beruhen. Die vorliegende Arbeit zeigt, wie modellgetriebene Entwicklung, und insbesondere die metamodellbasierte Beschreibung von DSLs, darüber hinaus Aspekte der Pragmatik unterstützen kann, deren Relevanz im erkenntnistheoretischen und kognitiven Hintergrund wissenschaftlichen Forschens begründet wird. Hierzu wird vor dem Hintergrund der Erkenntnisse des "modellbasierten Forschens"(model-based science und model-based reasoning) gezeigt, wie insbesondere durch Metamodelle beschriebene DSLs Möglichkeiten bieten, entsprechende pragmatische Aspekte besonders zu berücksichtigen, indem sie als Werkzeug zur Erkenntnisgewinnung aufgefasst werden. Dies ist v.a. im Kontext großer Unsicherheiten, wie sie für weite Teile der Umweltmodellierung charakterisierend sind, von grundsätzlicher Bedeutung. Die Formulierung eines sprachzentrierten Ansatzes (LCA, language-centered approach) für die Werkzeugunterstützung konkretisiert die genannten Aspekte und bildet die Basis für eine beispielhafte Implementierung eines Werkzeuges mit einer DSL für die Beschreibung von Zellulären Automaten (ZA) für die Umweltmodellierung. Anwendungsfälle belegen die Verwendbarkeit von ECAL und der entsprechenden metamodellbasierten Werkzeugimplementierung. / The application of methods and technologies of software engineering to environmental modeling and simulation (EMS) is common, since both areas share basic issues of software development and digital simulation. Recent developments within the context of "Model-driven Engineering" (MDE) aim at supporting the development of software systems at the base of relatively abstract models as opposed to programming language code. A basic ingredient of MDE is the development of methods that allow the efficient development of "domain-specific languages" (DSL), in particular at the base of language metamodels. This thesis shows how MDE and language metamodeling in particular, may support pragmatic aspects that reflect epistemic and cognitive aspects of scientific investigations. For this, DSLs and language metamodeling in particular are set into the context of "model-based science" and "model-based reasoning". It is shown that the specific properties of metamodel-based DSLs may be used to support those properties, in particular transparency, which are of particular relevance against the background of uncertainty, that is a characterizing property of EMS. The findings are the base for the formulation of an corresponding specific metamodel- based approach for the provision of modeling tools for EMS (Language-centered Approach, LCA), which has been implemented (modeling tool ECA-EMS), including a new DSL for CA modeling for EMS (ECAL). At the base of this implementation, the applicability of this approach is shown.

Der Elektrik/Elektronik- und der IT-Anteil steigt derzeit in den aktuellen Premium -Fahrzeugen stetig an. Durch den Verbau von immer mehr (hochvernetzten) Steuergeräten im Fahrzeug wird versucht, dem Wunsch der Kunden nach mehr Funktionalität, Sicherheit, etc. gerecht zu werden. Aufgrund der Komplexität und der großen Entwicklungssprünge sind jedoch die neuen Steuergeräte meistens nicht mehr kompatibel mit den Vorgänger-Steuergeräten. Hier ist ein großes Einsparpotenzial vorhanden und dies ist auch der Ansatzpunkt des Forschungsthemas ”CompA“ (Compatibility Analysis of Electronic Control Units), das in diesem Dokument beschrieben wird. Im Rahmen dieses Forschungsthemas wird eine Methode definiert, mit der zwei Steuergeräte auf Rückwärtskompatibilität untersucht werden können. Der Ansatz baut auf drei Schwerpunkten auf: • Definition eines Spezifikationsansatzes zur hinreichenden Beschreibung von Steuergeräten auf Basis eines XML-Schemas. Es werden hierbei sowohl die statischen als auch die dynamischen Eigenschaften abgebildet. Dieser neuartige Spezifikationsansatz bildet die Basis für den nächsten Schwerpunkt. • Definition einer Methode zur Analyse von Rückwärtskompatibilität von Steuergeräten auf Basis eines XML-Schemas. Die Rückwärtskompatibilität zweier Steuergeräte bzw. Systeme wird auf Basis der zugehörigen XML-Dokumente analysiert. Kern der Vergleichsmethode ist hierbei ein effizientes Mapping der XML-Dokumente und ein Experten-Regelwerk. • Definition einer Methode zur Kompatibilitätsanalyse von Message Sequence Charts (MSC). MSCs werden eingesetzt, um dynamisches Verhalten an der Schnittstelle von Steuergeräten zu beschreiben. In diesem Dokument wird ein Ansatz definiert, mit dem MSCs zueinander auf Rückwärtskompatibilität geprüft werden können. Der Vergleich erfolgt auf Basis deterministischer Automaten. Des Weiteren wird im vorliegenden Dokument ein Konzept für eine graphische Benutzeroberfläche (GUI) vorgestellt, die zur Spezifikation von Steuergeräten geeignet ist und sich adaptiv unterschiedlichen Schemata anpasst. Alle vorgestellten Konzepte wurden in einem Software-Tool implementiert und die Gültigkeit an mehreren Beispielen validiert.

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.

Die Dissertationsschrift stellt eine Toolkette zum abstrakten Entwurf von Mikrosystemen vor. Mikrosysteme können aus Elementen verschiedener physikalischer Domänen bestehen und zusätzlich digitale Hardware sowie Software enthalten. Die Erfassung und Formalisierung dieser heterogenen Systeme stellt den ersten Schritt im Entwurfsprozess dar, die damit verbundene neue Methodik des Designs von Mikrosystemen bildet den Kern der vorliegenden Arbeit. Zur Erfassung der analogen Spezifikationsteile enthält die Arbeit die Schilderung und Implementierung neuer Datenstrukturen, die ausgehend von einer ausführlichen Anforderungsanalyse geschaffen wurden. Das abstrakte Systemverhalten wird mit Hilfe hybrider Automaten modelliert, die sowohl mit speziellen hybriden Werkzeugen als auch mit SystemC-AMS simulierbar sind. Darüber hinaus beschäftigt sich die Arbeit mit der Erfassung von Signalverläufen und Schaltplaninformationen. Die formalisierten Anforderungen ermöglichen erste Prüfungen der Spezifikation auf Konsistenz. Zur Unterstützung niedriger Abstraktionsebenen wie der Differentialgleichungsebene steht ein Wandler von SystemC-AMS nach VHDL-AMS bereit. In die Systembeschreibung mit SystemC-AMS ist die Definition und Verknüpfung von Kostenparametern integrierbar. Das daraus entstehende globale Gütemaß hilft dem Entwerferteam, die optimale Systemrealisierung zu finden. / The PhD thesis proposes a toolflow for the design of microsystems on higher abstraction levels. Microsystems may consist of components using effects in different physical domains plus additional digital hardware and software. The collection and formalization of these heterogeneous systems is a first step in the design process, the associated design method ist the key point of this work. The system behavior is modeled using hybrid automata, which are checkable using hybrid modelcheckers and simulable using SystemC-AMS. Furthermore the work deals with signal forms and circuit parameters. To support modeling on lower abstraction levels like differential algebraic equations a syntax conversion from SystemC-AMS to VHDL-AMS was included. The integration of cost factors into SystemC-AMS allows design space exploration during system simulation.

Der Elektrik/Elektronik- und der IT-Anteil steigt derzeit in den aktuellen Premium -Fahrzeugen stetig an. Durch den Verbau von immer mehr (hochvernetzten) Steuergeräten im Fahrzeug wird versucht, dem Wunsch der Kunden nach mehr Funktionalität, Sicherheit, etc. gerecht zu werden. Aufgrund der Komplexität und der großen Entwicklungssprünge sind jedoch die neuen Steuergeräte meistens nicht mehr kompatibel mit den Vorgänger-Steuergeräten. Hier ist ein großes Einsparpotenzial vorhanden und dies ist auch der Ansatzpunkt des Forschungsthemas ”CompA“ (Compatibility Analysis of Electronic Control Units), das in diesem Dokument beschrieben wird. Im Rahmen dieses Forschungsthemas wird eine Methode definiert, mit der zwei Steuergeräte auf Rückwärtskompatibilität untersucht werden können. Der Ansatz baut auf drei Schwerpunkten auf: • Definition eines Spezifikationsansatzes zur hinreichenden Beschreibung von Steuergeräten auf Basis eines XML-Schemas. Es werden hierbei sowohl die statischen als auch die dynamischen Eigenschaften abgebildet. Dieser neuartige Spezifikationsansatz bildet die Basis für den nächsten Schwerpunkt. • Definition einer Methode zur Analyse von Rückwärtskompatibilität von Steuergeräten auf Basis eines XML-Schemas. Die Rückwärtskompatibilität zweier Steuergeräte bzw. Systeme wird auf Basis der zugehörigen XML-Dokumente analysiert. Kern der Vergleichsmethode ist hierbei ein effizientes Mapping der XML-Dokumente und ein Experten-Regelwerk. • Definition einer Methode zur Kompatibilitätsanalyse von Message Sequence Charts (MSC). MSCs werden eingesetzt, um dynamisches Verhalten an der Schnittstelle von Steuergeräten zu beschreiben. In diesem Dokument wird ein Ansatz definiert, mit dem MSCs zueinander auf Rückwärtskompatibilität geprüft werden können. Der Vergleich erfolgt auf Basis deterministischer Automaten. Des Weiteren wird im vorliegenden Dokument ein Konzept für eine graphische Benutzeroberfläche (GUI) vorgestellt, die zur Spezifikation von Steuergeräten geeignet ist und sich adaptiv unterschiedlichen Schemata anpasst. Alle vorgestellten Konzepte wurden in einem Software-Tool implementiert und die Gültigkeit an mehreren Beispielen validiert.

In this thesis, we investigate weighted tree automata with storage theoretically. This model generalises finite state automata in three dimensions: (i) from words to trees, (ii) by using an arbitrary storage type in addition to a finite-state control, and (iii) by considering languages in a quantitative setting using a weight structure.

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.