TY - THES A1 - Deussen, Peter H. T1 - Analyse verteilter Systeme mit Hilfe von Prozeßautomaten N2 - Diese Arbeit behandelt einen Ansatz zur Verifikation verteilter Systeme. Zur Beschreibung des Verhaltens solcher Systeme verwenden wir die sog. Semiwörter, die eine spezielle Form von pomsets darstellen, sowie Mazurkiewiczspuren. Wir weisen nach, daß jedes nebenläufige System (d. h. ein System, für dessen Aktionen eine Unabhängigkeitsrelation angegeben werden kann) als verteiltes System aufgefaßt werden kann. Wir beschreiben eine endliche Repräsentation des Verhaltens nebenläufiger und verteilter Systeme, die auf dem Begriff des Prozeßautomaten beruht, und geben Algorithmen zur Konstruktion derartiger Prozeßautomaten an. Schließlich definieren wir die verteilte, agentenbasierte temporale Logik DCTL. Die Beschreibung eines Modelcheckers für diese Logik, der auf Prozeßautomaten operiert, schließt die Arbeit ab. N2 - This thesis addresses the verification of distributed systems. The description of the behaviour of distributed systems is done by so-called semi words. Semi words are a dedicated type of pomsets. Also, Mazurkiewicz traces are used as a behavioural description. We will prove that every concurrent system (i. e. a system for that an independence relation can be defined on system actions) can be considered as a distributed system. We describe a finite representation of the behaviour of concurrent and distributed systems based on the notion of process automata. We define algorithms for the construction of process automata. Finally, we describe the distributed, agent based temporal logic DCTL. A model checking algorithm for DCTL is given. This model checker operates on process automata. KW - Verteiltes System KW - Verifikation KW - Transitionssystem KW - Nebenläufigkeit KW - Halbordnung KW - Spurtheorie KW - Verteiltes System KW - Prozeßautomat KW - Modellchecking KW - Verifikation KW - Petri-Netz Y1 - 2001 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:co1-000000275 ER -