Informationssysteme verarbeiten Daten, die logisch und physisch über Knoten verteilt sind. Datenobjekte verschiedener Knoten können dabei Bezüge zueinander haben. Beispielsweise kann ein Datenobjekt eine Referenz auf ein Datenobjekt eines anderen Knotens oder eine kritische Information enthalten. Die Semantik der Daten induziert Datenintegrität in Form von Anforderungen: Zum Beispiel sollte keine Referenz verwaist und kritische Informationen nur an einem Knoten verfügbar sein. Datenintegrität unterscheidet gültige von ungültigen Verteilungen der Daten. Ein verteiltes System verändert sich in Schritten, die nebenläufig auftreten können. Jeder Schritt manipuliert Daten. Ein verteiltes System erhält Datenintegrität, wenn alle Schritte in einer Datenverteilung resultieren, die die Anforderungen von Datenintegrität erfüllen. Die Erhaltung von Datenintegrität ist daher ein notwendiges Korrektheitskriterium eines Systems. Der Entwurf und die Analyse von Datenintegrität in verteilten Systemen sind schwierig, weil ein verteiltes System nicht global kontrolliert werden kann. In dieser Arbeit untersuchen wir formale Methoden für die Modellierung und Analyse verteilter Systeme, die mit Daten arbeiten. Wir entwickeln die Grundlagen für die Verifikation von Systemmodellen. Dazu verwenden wir algebraische Petrinetze. Wir zeigen, dass die Schritte verteilter Systeme mit endlichen vielen Transitionen eines algebraischen Petrinetzes beschrieben werden können, genau dann, wenn eine Schranke für die Bedingungen aller Schritte existiert. Wir verwenden algebraische Gleichungen und Ungleichungen, um Datenintegrität zu spezifizieren. Wir zeigen, dass die Erhaltung von Datenintegrität unentscheidbar ist, wenn alle erreichbaren Schritte betrachtet werden. Und wir zeigen, dass die Erhaltung von Datenintegrität entscheidbar ist, wenn auch unerreichbare Schritte berücksichtigt werden. Dies zeigen wir, indem wir die Berechenbarkeit eines nicht-erhaltenden Schrittes als Zeugen zeigen. / Information systems process data that is logically and physically distributed over many locations. Data entities at different locations may be in a specific relationship. For example, a data entity at one location may contain a reference to a data entity at a different location, or a data entity may contain critical information such as a password. The semantics of data entities induce data integrity in the form of requirements. For example, no references should be dangling, and critical information should be available at only one location. Data integrity discriminates between correct and incorrect data distributions. A distributed system progresses in steps, which may occur concurrently. In each step, data is manipulated. Each data manipulation is performed locally and affects a bounded number of data entities. A distributed system preserves data integrity if each step of the system yields a data distribution that satisfies the requirements of data integrity. Preservation of data integrity is a necessary condition for the correctness of a system. Analysis and design are challenging, as distributed systems lack global control, employ different technologies, and data may accumulate unboundedly. In this thesis, we study formal methods to model and analyze distributed data-aware systems. As a result, we provide a technology-independent framework for design-time analysis. To this end, we use algebraic Petri nets. We show that there exists a bound for the conditions of each step of a distributed system if and only if the steps can be described by a finite set of transitions of an algebraic Petri net. We use algebraic equations and inequalities to specify data integrity. We show that preservation of data integrity is undecidable in case we consider all reachable steps. We show that preservation of data integrity is decidable in case we also include unreachable steps. We show the latter by showing computability of a non-preserving step as a witness.

Wir betrachten offene Systeme; Systeme mit Schnittstelle und Verhalten in Form eines Protokolls. Offener Systeme interagieren durch den Austausch von Nachrichten. Die Interaktion ist korrekt, wenn die interagierende offenen Systeme terminieren können. Die korrekte Interaktion unabhängig entwickelter, offener Systeme ist nicht immer möglich. Obwohl ein offenes Systeme Funktionalität bereitstellt, die ein zweites offenes System benötigt, können Inkompatibilitäten in den Schnittstellen oder im Verhalten dazu führen, dass Nachrichten nicht korrekt ausgetauscht werden. Hier kommt die Idee eines Adapters zum Tragen, der solche Unterschiede ausgleicht. Wir führen eine Technik ein, die Inkompatibilitäten der Schnittstelle und des Verhaltens getrennt voneinander betrachtet. Mit Hilfe von Transformationsregeln geben wir an, wie Nachrichten zweier offener Systeme im Zusammenhang stehen. Wir modellieren so korrekten Datenfluss zwischen den Schnittstellen der offenen Systeme. Mit Hilfe existierender Techniken zur Controllersynthese erzeugen wir korrekten Kontrollfluss, sodass die Transformationsregeln so angewendet werden, dass Inkompatibilitäten im Verhalten überwunden werden. Wir erzeugen korrekten Kontrollfluss. Die Einheit aus Transformationsregeln und Controller bezeichnen wir als Adapter. Aufbauend auf dieser Technik betrachten wir in dieser Arbeit folgende Fragestellungen: - Welche Eigenschaften besitzt die vorgestellte Technik? Wann existiert ein Adapter? Wie lässt sich die Technik allgemein auf offene, kommunizierende Systeme anwenden? - Wie verteilen wir einen generierten Adapter auf verschiedene Komponenten? - Welche Informationen können wir bereitstellen, falls wir keinen Adapter finden? - Wie leiten wir ein formales Modell eines Adapters ab, wenn wir nur aufgezeichnetes Verhalten der offenen Systeme, aber keine formalen Modelle gegeben haben? / We consider open systems being described by an interface and behavior in form of an protocol. Interaction between open systems means exchange of messages. For the interaction to be correct, the interacting open systems must be able to terminate. The interaction of independently developed open systems is not guaranteed to be correct. Although one open system provides functionality a second open system requires, incompatiblities of the interfaces or the behavior may prevent the correct exchange of messages. The idea is to introduce an adapter to overcome the incompatiblities. We present a technique that considers incompatiblities of the interfaces and the behavior separately. With transformation rules we specify how messages of two open systems relate to each other. Using these rules we model the data flow between open systems and overcome incompatiblities of the interfaces. By using existing techniques for controller synthesis we overcome incompatiblities of the behavior. Thus we create correct control flow. We call the composition of transformation rules and controller an adapter. Based on the technique presented in this thesis, we want to answer the following reseach questions: - What are the properties of the proposed technique? When does an adapter exist? How can we apply the technique on open, communicating systems in general? - How do we distribute a generated adapter to different components? - Which information can we provide, if adapter synthesis fails? - How can we discover a formal model of an adapter, when we only have recorded behavior of open systems, but no formal models?

Um Entwurf und Verifikation komplizierter verteilter Algorithmen leichter und verständlicher zu machen, wird oft eine Verfeinerungsmethode verwendet. Dabei wird ein einfacher Algorithmus, der gewünschte Eigenschaften erfüllt, schrittweise zu einem komplizierten Algorithmus verfeinert. In jedem Schritt sollen die gewünschten Eigenschaften erhalten bleiben. Für nachrichtenbasierte verteilte Algorithmen haben wir eine neue Verfeinerungsmethmode entwickelt. Wir beginnen mit einem Anfangsalgorithmus, der Aktionen enthält, die gemeinsame Aufgaben mehrerer Agenten beschreiben. In jedem Schritt verfeinern wir eine dieser Aktionen zu einem Netz, das nur solche Aktionen enthält, die die Aufgaben einzelner Agenten beschreiben. Jeder Schritt ist also eine Verteilung einer unverteilten Aktion. Die Analyse solcher Verfeinerungsschritte wird mit Hilfe eines neuen Verfeinerungsbegriffs - der verteilenden Verfeinerung - durchgeführt. Entscheidend dabei ist das Erhaltenbleiben der Halbordnungen des zu verfeinernden Algorithmus. Dies ist durch Kausalitäten der Aktionen der Agenten im lokalen Verfeinerungsnetz zu erreichen. Die Kausalitäten im lokalen Verfeinerungsnetz lassen sich einerseits beim Entwurf direkt durch Nachrichtenaustausch realisieren. Andererseits kann man bei der Verifikation die Gültigkeit einer Kausalität im lokalen Verfeinerungsnetz direkt vom Netz ablesen. Daher ist diese Methode leicht zu verwenden. Die Anwendung der Methode wird in der Arbeit an verschiedenen nicht trivialen Beispielen demonstriert. / In order to make design and verification of complicated distributed algorithms easier and more understandable, a refinement method is often used. A simple algorithm, which fulfills desired properties, is refined stepwise to a complicated algorithm. In each step the desired properties are preserved. For messages-based distributed algorithms we have developed a new refinement method. We begin with an initial algorithm, which contains actions, which describe common tasks of several agents. In each step we refine one of these actions to a net, which contains only such actions, which describe the tasks of individual agents. Thus, each step is a distribution of an undistributed action. The analysis of such refinement steps is accomplished with the help of a new refinement notation - the distributing refinement. Preservation of the partial order of the refined algorithm is important. This can be achieved by causalities of the actions of the agents in the local refinement net. Causalities in the local refinement net can be realized on the one hand at design directly by messages passing. On the other hand, at verification one can read the validity of causality in the local refinement net directly from the net. Therefore, this method is easy to use. The application of the method is demonstrated by several nontrivial examples in this thesis.

In dieser Arbeit geht es um die schrittweise Verfeinerung verteilter Algorithmen. Dabei wird ein einfacher Algorithmus, der einige gewünschte Eigenschaften hat, Schritt für Schritt zu einem komplexen Algorithmus verfeinert, der konkrete Implementationsanforderungen erfüllt, so daß in jedem Schritt die gewünschten Eigenschaften erhalten bleiben. Wir stellen einen neuen eigenschaftserhaltenden Verfeinerungsbegriff vor, der auf der kausalen Ordnung der Aktionen eines Algorithmus basiert. Diesen Begriff definieren wir als Transitionsverfeinerung für elementare Petrinetze und diskutieren Beweiskriterien. Danach definieren und diskutieren wir die simultane Verfeinerung mehrerer Transitionen. Zur Modellierung komplexer verteilter Algorithmen sind elementare Petrinetze oft nicht adäquat. Wir benutzen deshalb algebraische Petrinetze. Wir definieren Transitionsverfeinerung für algebraische Petrinetze und stellen einen Zusammenhang zur simultanen Verfeinerung von Transitionen in elementaren Petrinetzen her. Transitionsverfeinerung ist besonders für Verfeinerungsschritte geeignet, in denen synchrone Kommunikation zwischen Agenten durch asynchronen Nachrichtenaustausch ersetzt wird. Wir zeigen dies am Beispiel eines komplexen verteilten Algorithmus, zur Berechnung des minimalen spannenden Baumes in einem gewichteten Graphen. Wir zeigen die Korrektheit dieses Algorithmus in mehreren Schritten, von denen einige Schritte Transitionsverfeinerungen sind. In anderen Schritten sind klassische Verfeinerungsbegriffe ausreichend. Wir übertragen deshalb auch einen klassischen Verfeinerungsbegriff in unser formales Modell. / The topic of this PhD thesis is the stepwise refinement of distributed algorithms. Stepwise refinement starts with a simple algorithm with certain desired properties. This algorithm is refined step by step such that the desired properties are preserved in each refinement step. The result is a complex distributed algorithm which satisfies concrete implementation requirements and which still has the desired properties. We propose a new property preserving notion of refinement which is based on the causal ordering of actions of an algorithm. We call this notion transition refinement and we define it first for elementary Petri nets. Furthermore, we discuss proof criteria. Then, we define and discuss the simultaneous refinement of several transitions. For modelling complex distributed algorithms, we use algebraic Petri nets instead of elementary Petri nets. We define transition refinement for algebraic Petri nets, and we show its relationship to simultaneous transition refinement in elementary Petri nets. Transition refinement is particularly suitable for refinement steps in which synchronous communication between agents is replaced by asynchronous message passing. We show this by means of a complex distributed algorithm for determining the minimal spanning tree of a weighted graph. We prove the correctness of this algorithm in several steps. Some of these steps are transition refinements. For other steps, well-known notions of refinement are sufficient. Therefore, we also carry over a well-known notion of refinement into our formal model.

In order to generate substantial market impact, mobile applications must be able to run on multiple platforms. Hence, software engineers face a multitude of technologies and system versions resulting in static variability. Furthermore, due to the dependence on sensors and connectivity, mobile software has to adapt its behavior accordingly at runtime resulting in dynamic variability. However, software engineers need to assure quality of a mobile application even with this large amount of variability—in our approach by the use of model-based testing (i.e., the generation of test cases from models). Recent concepts of test metamodels cannot efficiently handle dynamic variability. To overcome this problem, we propose a process for creating black-box test models based on dynamic feature Petri nets, which allow the description of configuration-dependent behavior and reconfiguration. We use feature models to define variability in the system under test. Furthermore, we illustrate our approach by introducing an example translator application.

In order to generate substantial market impact, mobile applications must be able to run on multiple platforms. Hence, software engineers face a multitude of technologies and system versions resulting in static variability. Furthermore, due to the dependence on sensors and connectivity, mobile software has to adapt its behavior accordingly at runtime resulting in dynamic variability. However, software engineers need to assure quality of a mobile application even with this large amount of variability—in our approach by the use of model-based testing (i.e., the generation of test cases from models). Recent concepts of test metamodels cannot efficiently handle dynamic variability. To overcome this problem, we propose a process for creating black-box test models based on dynamic feature Petri nets, which allow the description of configuration-dependent behavior and reconfiguration. We use feature models to define variability in the system under test. Furthermore, we illustrate our approach by introducing an example translator application.

Petrinetze werden in vielen Bereichen als Modellierungstechnik verwendet. Die verschiedenen Einsatzgebiete und Modellierungsziele erfordern dabei unterschiedliche Typen von Petrinetzen. Einen Petrinetz-Typ kennzeichnen -- neben den üblichen Stellen, Transitionen und Kanten -- eine Menge zusätzlicher, spezifischer Elemente, sowie eine spezifische Schaltregel. In der Literatur findet man zahlreiche verschiedene Petrinetz-Typen. Diese Vielfalt an Petrinetz-Typen lässt sich nicht ohne weiteres überblicken. Deshalb fehlt es auch nicht an Versuchen, allgemeine Petrinetz-Typen oder Klassifikationen -- auch einzelner Aspekte -- zu etablieren. Allerdings erfassen die bisherigen Ansätze nur einen kleinen Teil aller Petrinetz-Typen. Unser semantisch orientierter Klassifizierungsansatz des Petrinetz-Hyperwürfels umfasst deutlich mehr Petrinetz-Typen und erhebt den Anspruch, universell zu sein. Der Petrinetz-Hyperwürfel hat einen syntaktisch orientierten Klassifizierungsansatz als Grundlage. Dieser Ansatz führt einerseits zum Vorschlag der Petri Net Markup Language. Damit können Petrinetze aller Typen einheitlich beschrieben werden. Andererseits führt derselbe Ansatz zu einer Basis für Petrinetz-Werkzeuge, in der die einzelnen Teile eines Petrinetz-Typs unabhängig voneinander implementiert werden. Der Petrinetz-Kern ist eine derartige Basis mit dessen Hilfe Petrinetz-Werkzeuge gebaut werden. Er implementiert Konzepte, die allen Petrinetzen gemein sind, unabhängig von konkreten Petrinetz-Typen. Gemeinsam mit dem Petrinetz-Hyperwürfel bildet der Petrinetz-Kern ein weiteres Basiswerkzeug für einen parametrisierten Petrinetz-Typ mit einer parametrisierten Schaltregel. Die Petri Net Markup Language und der Petrinetz-Kern sind die wesentlichen Beiträge der vorliegenden Arbeit. Gemeinsam bilden sie ein mächtiges Grundgerüst für Petrinetz-Werkzeuge beliebiger Petrinetz-Typen. / Petri nets are widely used for modelling systems. The different areas and goals require different types of Petri nets. Each Petri net contains beside places, transitions, and arcs several further specific elements. Furthermore, a Petri net type defines a specific firing rule. There are many different Petri net types. It is not easy to have a general view on this bulk of Petri net types. Thus, there are attempts to establish general Petri net types or classifications of Petri net types (even of particular aspects). But, current approaches include only a few of all Petri net types. Our approach is a classification by semantics of Petri nets. We call this classification Petri Net Hypercube. It is meant to be universal for all Petri net types. A syntactical classification approach is the base of the Petri Net Hypercube. This approach leads on the one hand to the proposal of the Petri Net Markup Language. This language describes Petri nets of all types. On the other hand, the same approach leads to a base of Petri net tools. The parts of a Petri net type are implemented in this base independently of each other. The Petri Net Kernel is such a base for building Petri net tools. It implements those concepts which are general concepts of each Petri net. The Petri Net Kernel forms together with the Petri Net Hypercube a further basic Petri net tool for a parameterized Petri net type with a parameterized firing rule. The Petri Net Markup Language and the Petri Net Kernel are the main contributions of this thesis. Together, they are a powerful base for Petri net tools of each Petri net type.

Die steigende Nachfrage an immer komplexeren Systemen in verschiedensten wirtschaftlichen Bereichen, erfordert Strategien, die Wartbarkeit und Wiederverwendbarkeit unterstützen. An diesem Punkt setzen service-orientierte Architekturen (SOAn) an. Dieses Paradigma fordert die Aufspaltung von Funktionalität in Services, die komponiert werden können, um eine gewünschte, komplexe Funktionalität zu erreichen. Besonders in sicherheitskritischen Bereichen, kann eine fehlerbehaftete Komposition jedoch zu hohen finanziellen Einbußen oder sogar zu lebensbedrohlichen Situationen führen. Um die Korrektheit sicherzustellen, müssen Kompositionsmethoden im Vorfeld definierte Eigenschaften garantieren und die, durch die unabhängige Entwicklung auftretenden, Interface-Inkompatibilitäten behandeln. Existierende Ansätze zur automatisierten Service-Komposition durch Controller-Synthese beinhalten jedoch keine formale Datenbehandlung und können daher nicht mit datenabhängigem Verhalten umgehen. In der vorliegenden Arbeit, löse ich dieses Problem durch die Bereitstellung eines Ansatzes zur automatisierten Synthese datenabhängiger, korrekter Service-Controller. Dabei wird ein Controller direkt aus den spezifizierten Anforderungen und dem Verhalten der Services erzeugt. Basierend auf den Annahmen, dass die Anforderungen in RCTL, einer Untermenge der Computational Tree Logic (CTL), spezifiziert und die Services als Algebraische Petrinetze (APNe) gegeben sind, vereinigt mein neuartiger Ansatz die beiden Formalismen und unterstützt eine zuverlässige Extraktion des Controller-Verhaltens. Durch die Nutzung der APNe, erlaubt der Ansatz eine formale Datenbehandlung und somit eine Betrachtung datenabhängigen Verhaltens. Die Anwendbarkeit meines Ansatzes habe ich an drei Fallstudien aus dem medizinischen Bereich gezeigt, wo Geräte sicher miteinander kommunizieren müssen. / The continuously increasing demand for more complex systems in various economical domains requires a strategy that supports maintainability and reusability. This is addressed by the service-oriented architecture (SOA)}-paradigm that encourages the encapsulation of functionality into services. To achieve a specific functionality, services can be composed. Especially in safety-critical systems, an incorrect composition of various components can lead to high financial losses or even life threatening situations. To ensure the correctness, composition methods must particularly be able to guarantee pre-specified requirements and to overcome interface incompatibilities, which result from the independent development of the single services. However, current approaches for automated service composition via controller synthesis do not support a formal data-treatment and do not cope with data-dependent behavior. In this thesis, we overcome this problem by providing an approach for the automated synthesis of data-dependent service controllers that are correct-by-construction. The core idea is to synthesize such a controller directly from given requirements and the behavior of the services. Based on the assumptions that the requirements are specified using a subset of Computational Tree Logic (CTL), called RCTL, and that the services are given as algebraic Petri Nets (APNs), our novel synthesis process unifies the two formalisms and enables a reliable extraction of the controller behavior. Especially due to the use of APNs, our approach supports a formal data-treatment and enables a consideration of data-dependent behavior. With our synthesis process, which is based on a successive combination of requirements and services, we provide a practical applicable approach that works fully automatically. We show the applicability of our approach using three case studies in which medical devices interact with each other.

Zum Verständnis menschlichen sozialen, administrativen und wirtschaftlichen Verhaltens, das als Spiel bzw. strategische Interaktion aufgefasst werden kann, reichen die rein analytischen Methoden nicht aus. Es ist nötig, Daten menschlichen strategischen Verhaltens zu sammeln. Basierend auf Daten lässt sich solches Verhalten modellieren, simulieren bzw. vorhersagen. Der theoretische Teil der Zielsetzung wird über praxisorientierte Konzeptualisierung strategischer Interaktion realer Agenten - Menschen und Maschinen - und gegenseitige Integration der Konzepte aus Spieltheorie und Multiagentensysteme erreicht, die über die bisherigen Ansätze hinausgehen. Der praktische Teil besteht darin, ein allgemein verwendbares System zu entwerfen, das strategische Interaktionen zwischen realen Agenten mit maximalen wissenschaftlichen Nutzen durchführen kann. Die tatsächliche Implementation ist eines der Ergebnisse der Arbeit. Ähnliche vorhandene Systeme sind GDL-Server (für Maschinen) [Genesereth u.a., 2005] und z-Tree (für Menschen) [Fischbacher, 2007]. Die Arbeit ist in drei Bereiche unterteilt - (1) Entwicklung von Sprachen für die Beschreibung eines Spiels, (2) ein auf diesen Sprachen basierendes Softwaresystem und (3) eine Offline-Analyse der u.a. mit dem System bereits gesammelten Daten als Beitrag zur Möglichkeiten der Verhaltensbeschreibung. Die Innovation dieser Arbeit besteht nicht nur darin ,einzelne Bereiche mit einander zu kombinieren, sondern auch Fortschritte auf jedem Bereich für sich allein zu erreichen. Im Bereich der Spielbeschreibungssprachen, werden zwei Sprachen - PNSI und SIDL - vorgeschlagen, die beide Spiele bei imperfekter Information in diskreter Zeit definieren können. Dies ist ein Fortschritt gegenüber der bisherigen Sprachen wie Gala und GDL. Speziell die auf Petrinetzen basierende Sprache PNSI kann gleichermaßen für Gameserver und für spieltheoretische Algorithmen von z.B. GAMBIT verwendet werden. Das entwickelte System FRAMASI basiert auf JADE [Bellifemine u.a., 2001] und ist den bisherigen Client-Server-Lösungen durch Vorteile der Multiagentensysteme voraus. Mit dem entstandenen System wurde bereits ein Experiment entsprechend den Standards der experimentellen Spieltheorie durchgeführt und somit die Praxistauglichkeit nachgewiesen. Das Experiment hatte als Ziel, Daten zur menschlichen Unvorhersagbarkeit und zur Vorhersagefähigkeit anderer zu liefen. Dafür wurden Varianten von \"Knobeln\" verwendet. Die Daten dieses Experiments sowie eines Experiments einer externen Arbeitsgruppe mit ähnlicher Motivation wurden mit Hilfe von Datamining analysiert. Dabei wurden die in der Literatur berichteten Gesetzmäßigkeiten des Verhaltens nachgewiesen und weitere Gesetzmäßigkeiten entdeckt. / To understand human social, administrative and economic behavior, which can be considered as a game or strategic interaction, the purely analytical methods do not suffice. It is necessary to gather data of human strategic behavior. Based on data, one can model, simulate and predict such behavior. The theoretical part of the objective is achieved using a practice oriented conceptualization of the real agents\' - humans and machines - strategic interaction and mutual integration of the concepts from game theory and multi-agent systems, which go beyond the related work. The practical part is the design of an universally usable system that can perform the strategic interactions between real agents with maximum scientific benefit. The current implementation is one of the results of the work. Similar existing systems are GDL-server (for machines) [Genesereth et al., 2005] and z-Tree (for humans) [Fischbacher, 2007]. The work is divided in three fields - (1) development of languages for the description of a game, (2) a software system based on these languages and (3) an offline analysis of the data already gathered among other things using the system as a contribution to behavior definition facilities. The innovation of this work does not consist only in combining of the several fields to each other, but also in achieving of improvements in every field on its own. In the field of game definition languages, two languages are proposed - PNSI and SIDL, which both can define games of imperfect information in discrete time. It is an improvement comparing with hitherto languages as Gala and GDL. Especially, the Petri net based language PNSI can likewise be used for game servers and game theoretic algorithms like GAMBIT. The developed system FRAMASI is based on JADE [Bellifemine et al., 2001] and is ahead of the hitherto client-server solutions through the advantages of the multi-agent systems. Using the originated system, an experiment has been conducted according to the standards from the experimental game theory, and thus demonstrated the practicability. The experiment had the objective to provide data on the human unpredictability and the ability to predict others. Therefore, variants of Roshambo were used. The data from this experiment and from an experiment of an external workgroup with a similar motivation were analyzed using data mining. As results, the regularities of the behavior reported in literature have been demonstrated and further regularities have been discovered.

Zum Verständnis menschlichen sozialen, administrativen und wirtschaftlichen Verhaltens, das als Spiel bzw. strategische Interaktion aufgefasst werden kann, reichen die rein analytischen Methoden nicht aus. Es ist nötig, Daten menschlichen strategischen Verhaltens zu sammeln. Basierend auf Daten lässt sich solches Verhalten modellieren, simulieren bzw. vorhersagen. Der theoretische Teil der Zielsetzung wird über praxisorientierte Konzeptualisierung strategischer Interaktion realer Agenten - Menschen und Maschinen - und gegenseitige Integration der Konzepte aus Spieltheorie und Multiagentensysteme erreicht, die über die bisherigen Ansätze hinausgehen. Der praktische Teil besteht darin, ein allgemein verwendbares System zu entwerfen, das strategische Interaktionen zwischen realen Agenten mit maximalen wissenschaftlichen Nutzen durchführen kann. Die tatsächliche Implementation ist eines der Ergebnisse der Arbeit. Ähnliche vorhandene Systeme sind GDL-Server (für Maschinen) [Genesereth u.a., 2005] und z-Tree (für Menschen) [Fischbacher, 2007]. Die Arbeit ist in drei Bereiche unterteilt - (1) Entwicklung von Sprachen für die Beschreibung eines Spiels, (2) ein auf diesen Sprachen basierendes Softwaresystem und (3) eine Offline-Analyse der u.a. mit dem System bereits gesammelten Daten als Beitrag zur Möglichkeiten der Verhaltensbeschreibung. Die Innovation dieser Arbeit besteht nicht nur darin ,einzelne Bereiche mit einander zu kombinieren, sondern auch Fortschritte auf jedem Bereich für sich allein zu erreichen. Im Bereich der Spielbeschreibungssprachen, werden zwei Sprachen - PNSI und SIDL - vorgeschlagen, die beide Spiele bei imperfekter Information in diskreter Zeit definieren können. Dies ist ein Fortschritt gegenüber der bisherigen Sprachen wie Gala und GDL. Speziell die auf Petrinetzen basierende Sprache PNSI kann gleichermaßen für Gameserver und für spieltheoretische Algorithmen von z.B. GAMBIT verwendet werden. Das entwickelte System FRAMASI basiert auf JADE [Bellifemine u.a., 2001] und ist den bisherigen Client-Server-Lösungen durch Vorteile der Multiagentensysteme voraus. Mit dem entstandenen System wurde bereits ein Experiment entsprechend den Standards der experimentellen Spieltheorie durchgeführt und somit die Praxistauglichkeit nachgewiesen. Das Experiment hatte als Ziel, Daten zur menschlichen Unvorhersagbarkeit und zur Vorhersagefähigkeit anderer zu liefen. Dafür wurden Varianten von \"Knobeln\" verwendet. Die Daten dieses Experiments sowie eines Experiments einer externen Arbeitsgruppe mit ähnlicher Motivation wurden mit Hilfe von Datamining analysiert. Dabei wurden die in der Literatur berichteten Gesetzmäßigkeiten des Verhaltens nachgewiesen und weitere Gesetzmäßigkeiten entdeckt.:Einführung Grundlagen Verwandte Arbeiten Sprachen für Spielbeschreibung Implementation der Spielinfrastruktur Beschreibung Strategischen Verhaltens Resümee Ergebnisse Ausblick / To understand human social, administrative and economic behavior, which can be considered as a game or strategic interaction, the purely analytical methods do not suffice. It is necessary to gather data of human strategic behavior. Based on data, one can model, simulate and predict such behavior. The theoretical part of the objective is achieved using a practice oriented conceptualization of the real agents\' - humans and machines - strategic interaction and mutual integration of the concepts from game theory and multi-agent systems, which go beyond the related work. The practical part is the design of an universally usable system that can perform the strategic interactions between real agents with maximum scientific benefit. The current implementation is one of the results of the work. Similar existing systems are GDL-server (for machines) [Genesereth et al., 2005] and z-Tree (for humans) [Fischbacher, 2007]. The work is divided in three fields - (1) development of languages for the description of a game, (2) a software system based on these languages and (3) an offline analysis of the data already gathered among other things using the system as a contribution to behavior definition facilities. The innovation of this work does not consist only in combining of the several fields to each other, but also in achieving of improvements in every field on its own. In the field of game definition languages, two languages are proposed - PNSI and SIDL, which both can define games of imperfect information in discrete time. It is an improvement comparing with hitherto languages as Gala and GDL. Especially, the Petri net based language PNSI can likewise be used for game servers and game theoretic algorithms like GAMBIT. The developed system FRAMASI is based on JADE [Bellifemine et al., 2001] and is ahead of the hitherto client-server solutions through the advantages of the multi-agent systems. Using the originated system, an experiment has been conducted according to the standards from the experimental game theory, and thus demonstrated the practicability. The experiment had the objective to provide data on the human unpredictability and the ability to predict others. Therefore, variants of Roshambo were used. The data from this experiment and from an experiment of an external workgroup with a similar motivation were analyzed using data mining. As results, the regularities of the behavior reported in literature have been demonstrated and further regularities have been discovered.:Einführung Grundlagen Verwandte Arbeiten Sprachen für Spielbeschreibung Implementation der Spielinfrastruktur Beschreibung Strategischen Verhaltens Resümee Ergebnisse Ausblick