Universität Stuttgart
Permanent URI for this communityhttps://elib.uni-stuttgart.de/handle/11682/1
Browse
4 results
Search Results
Item Open Access Automatic synthesis of distributed transition systems(2006) Stefanescu, Alin; Esparza, Javier (Prof. Dr.)This thesis investigates the synthesis problem for two classes of distributed transition systems: synchronous products and asynchronous automata. The underlying structure of these models consist of local automata synchronizing on common actions. The synthesis problem discussed is as follows: Given a global specification as a transition system TS and a distribution pattern D, find a distributed transition system over D whose global state space is equivalent' to TS. As criteria for the correctness of the (distributed) implementation vs. the specification (i.e., their equivalence') we use: transition system isomorphism, language equivalence, and bisimilarity respectively. In particular, the synthesis of asynchronous automata modulo language equivalence is a notoriously hard problem solved by Zielonka at the end of the 80s. One of the motivations behind our work was to bring this theory closer to practical applications. From the theoretical point of view, we conduct a detailed analysis of the synthesis problem for both models of distributed systems, look at effective algorithmic approaches and draw a map of computational complexity results. E.g., we provide several matching lower and upper complexity bounds for the distributed implementability problem. From the practical perspective, we provide prototype implementations for most of the synthesis algorithms discussed in the thesis. Moreover, we offer assistance when a given specification is not distributable by trying to modify this specification such that distributed synthesis can be applied. By using several heuristics to overcome the classical state space explosion, we are able to automatically generate small distributed algorithms for problems such as mutual exclusion.Item Open Access Halbordnungs- und Reduktionstechniken für die automatische Verifikation von verteilten Systemen(2006) Schröter, Claus; Esparza, Javier (Prof. Dr.)Das Hauptproblem bei der automatischen Verifikation von verteilten Systemen unter Verwendung von Model-Checking-Verfahren besteht in der Zustandsraumexplosion der Ausgangssysteme. Dieses bedeutet, daß sogar die Spezifikation eines kleinen Systems oftmals einen großen Zustandsraum aufspannt, da dieser exponentiell in der Größe des Ausgangssystems wachsen kann. In der Vergangenheit wurden verschiedene Techniken vorgeschlagen, um diese Problematik in den Griff zu bekommen. Diese können klassifiziert werden in Techniken, die auf eine implizite, kompakte Repräsentation des gesamten Zustandsraums abzielen, zum Beispiel codiert als BDD, oder die unter Verwendung von Abstraktionen oder Halbordnungsreduktionen eine reduzierte Zustandsraumrepräsentation verwenden. Eine dritte Klasse von Techniken stützt sich auf die Halbordnungssicht auf nebenläufige Berechnungen, und Systemzustände werden hier implizit durch die Verwendung azyklischer Petrinetze repräsentiert. Sehr populär darunter ist die Technik von McMillan zur Erzeugung endlicher, vollständiger Präfixe von Petrinetzentfaltungen. Das Ziel dieser Arbeit besteht darin, effiziente Halbordnungs- und Reduktionstechniken für die automatische Verifikation von verschiedenen Petrinetzklassen zu analysieren, zu erweitern, zu implementieren und experimentell zu vergleichen. Eine der Hauptfragestellungen auf dem Gebiet der automatischen Verifikation untersucht die Erreichbarkeit von Systemzuständen, da viele Sicherheitseigenschaften eines Systems auf einfache Erreichbarkeitsfragen zurückgeführt werden können. Als typisches Beispiel sei hier die Eigenschaft zum wechselseitigen Ausschluß von nebenläufigen Prozessen erwähnt. In dieser Arbeit werden vier Verfahren betrachtet, die das Erreichbarkeitsproblem für 1-sichere Petrinetze unter Verwendung von Entfaltungspräfixen exakt lösen. Es werden zwei Halbentscheidungsverfahren betrachtet, die das Erreichbarkeitsproblem für 1-sichere Petrinetze unter Verwendung von Techniken der linearen Programmierung zu lösen versuchen. Die Verfahren werden anhand von experimentellen Ergebnissen miteinander verglichen, und es wird eine Empfehlung hergeleitet, welche Verfahren für praktische Belange geeignet zu sein scheinen. Es wird gezeigt, daß das PSPACE-vollständige Erreichbarkeitsproblem für 1-sichere Petrinetze in ein (möglicherweise exponentiell größeres) NP-vollständiges Problem überführt werden kann, sofern Entfaltungstechniken eingesetzt werden. Eine weitere wichtige Fragestellung auf dem Gebiet der automatischen Verifikation beschäftigt sich mit dem Nachweis von Sicherheits- und Lebendigkeitseigenschaften, die in Form von temporalen Logiken wie beispielsweise CTL oder LTL formuliert werden. Es werden Reduktionsregeln für den Nachweis von LTL-X-Eigenschaften betrachtet, die in zwei Kategorien eingeteilt werden können: Regeln, die lineare Programmierung unter Verwendung von Invarianten oder impliziten Stellen einsetzen, und Regeln, die lokale Netzreduktionen betrachten. Es wird gezeigt, daß die Bedingungen für die Anwendbarkeit einiger lokaler Netzreduktionen abgeschwächt werden können, sofern man LTL-X-Eigenschaften mit einem Verfahren von Esparza und Heljanko nachweist. Anhand von experimentellen Ergebnissen wird gezeigt, daß die Verifikationszeit für eine LTL-X-Eigenschaft eines Systems signifikant verringert werden kann, sofern dieses mit den vorgeschlagenen Reduktionsregeln vorverarbeitet wird. Schließlich wird der von Esparza und Heljanko vorgestellte entfaltungsbasierte Ansatz zum Nachweis von LTL-X-Eigenschaften 1-sicherer Petrinetze auf eine höhere Petrinetzklasse übertragen. Anhand von experimentellen Ergebnissen wird der in dieser Arbeit vorgestellte Ansatz mit dem Ansatz von Esparza und Heljanko sowie dem Model-Checker SPIN verglichen. Die Ergebnisse zeigen, daß der in dieser Arbeit verwendete Model-Checker dem Model-Checker von Esparza und Heljanko in allen Beispielen, und SPIN gegenüber in einigen Beispielen überlegen ist.Item Open Access Logical fragments for Mazurkiewicz traces : expressive power and algebraic characterizations(2006) Kufleitner, Manfred; Diekert, Volker (Prof. Dr.)Mazurkiewicz trace are a model for concurrency. They can be seen as a generalization of words by introducing partial commutation between specific letters. Several logical and language-theoretic characterizations of the variety of monoids DA are known for words. We show which of them also hold for traces and which of them do not hold. An important tool for this task are Ehrenfeucht-Fraisse games. For several logical fragments, we introduce characterizations in terms of these games. They are used to separate logical fragments over traces that have the same expressive power over words. An essential property is, whether one can express concurrency within a fragment or not.Item Open Access Komplexitäts- und Entscheidbarkeitsresultate für inverse Monoide mit idempotenter Präsentation(2006) Ondrusch, Nicole; Diekert, Volker (Prof. Dr.)Wir haben eine Konstruktion inverser Monoide $FIM(\Gamma)/P$ und $IM(G)/P$, beruhend auf Arbeiten von Birget und Rhodes sowie Margolis und Meakin betrachtet und konnten für dies speziellen Klassen inverser Monoide mit idempotenter Präsentation die Entscheidbarkeit des Wortproblems in linearer Zeit (auf einer RAM) zeigen. Ferner ist das uniforme Wortproblem für diese inversen Monoide EXPTIME-vollständig. Wir haben ferner die relationale Struktur $\C(\IM(G)/P)$ mit Prädikat $\reach_L$ betrachtet. Hierfür konnten wir die FO-Theorie auf die MSO-Theorie des Cayeyleygraphen von $G$ reduzieren und haben damit die Entscheidbarkeit der FO-Theorie von $\C(\IM(G)/P)$ erhalten. Diese impliziert, wie wir in Kapitel \ref{rationale mengen} gesehen haben, eine Reihe weiterer Resultate, insbesondere die Entscheidbarkeit des verallgemeinerten Wortproblems für $\IM(G)/P$ sowie die Entscheidbarkeit des Leerheitsproblems für boolesche Kombinationen rationaler Mengen in $\IM(G)/P$. Es stellt sich die Frage, für welche Monoide $M$ die Struktur $\C(M)$ noch entscheidbar ist, bzw. für welche Monoide Unentscheidbarkeit gezeigt werden kann.