Publikationen an der Fakultät für Informatik und Automatisierung ab 2015

Anzahl der Treffer: 1925
Erstellt: Mon, 29 Apr 2024 23:10:44 +0200 in 0.0470 sec


Jaberi, Raed;
Algorithms for computing the 2-vertex-connected components and the 2-blocks of directed graphs, 2015. - Online-Ressource (PDF-Datei: VII, 121 S., 1023 KB) Ilmenau : Techn. Univ., Diss., 2015

In dieser Dissertation beschäftigen wir uns mit mehreren Problemen in gerichteten Graphen. Zuerst betrachten wir das Problem der Berechnung der $2$-fach knotenzusammenhängenden Komponenten in gerichteten Graphen. Wir präsentieren einen neuen Algorithmus zur Lösung dieses Problems in Zeit $O(nm)$ und wir betrachten drei Anwendungen dieses Algorithmus. Sei $G=(V,E)$ ein gerichteter Graph. Ein $2$-gerichteter Block in $G$ ist eine maximale Knotenmenge $C^{2d}\subseteq V$ mit $|C^{2d}|\geq 2$, so dass für jedes Paar von verschiedenen Knoten $x,y\in C^{2d}$ zwei knoten disjunkte Wege von $x$ nach $y$ und zwei knoten disjunke Wege von $y$ nach $x$ in $G$ existieren.Wir präsentieren zwei Algorithmen zur Berechnung der $2$-gerichteten Blöcke von $G$ in Zeit $O(\min\lbrace m,(t_{sap}+t_{sb})n\rbrace n)$, wobei $t_{sap}$ die Anzahl der starken Artikulations\-punkte von $G$ und $t_{sb}$ die Anzahl der starken Brücken von $G$ ist. Wir untersuchen zwei weitere relevante Begriffe: die $2$-starken Blöcke und die $2$-Kanten-Blöcke von $G$. Wir geben zwei Algorithmen zur Berechnung der $2$-starken Blöcke von $G$in Zeit $O( \min \lbrace m,t_{sap} n\rbrace n)$ an und wir zeigen, dass die $2$-Kanten-Blöcke von $G$ in Zeit $O(\min \lbrace m, t_{sb} n \rbrace n)$ bestimmt werden können. Wir untersuchen auch einige Optimierungsprobleme, die mit starken Artikulationspunkten und $2$-Blöcken zusammenhängen. Gegeben sei ein stark zusammenhängender Graph $G=(V,E)$. Wir wollen einen minimalen stark zusammenhängenden spannenden Teilgraphen $G^{*}=(V,E^{*})$ von $G$ finden, so dass die starken Artikulationspunkte von $G$ mit den starken Artikulationspunkten von $G^{*}$ übereinstimmen. Wir zeigen, dass es einen $17/3$-Approximationsalgorithmus für dieses NP-schwere Problem gibt, der lineare Laufzeit hat. Wir betrachten auch das Problem der Berechnung eines minimalen stark zusammenhängenden spannenden Teilgraphen mit denselben $2$-Blöcken in einem stark zusammenhängenden Graphen. Wir präsentieren Approximationsalgorithmen für drei Versionen dieses Problems, die sich in der Art der $2$-Blöcke unterscheiden. Im Gegensatz zu $2$-stark-zusammenhängenden Komponenten kann Entfernung der nicht zu $2$-gerichteten Blöcken gehörenden starken Artikulations\-punkte aus $G$ diese Blöcke ändern. Wir untersuchen das Problem der Berechnung einer minimalen Teilmenge $V^{*}$ der starken Artikulationspunkte, die nicht in diesen Blöcke liegen, so dass das Entfernen von $V^{*}$ denselben Effekt hat. Außerdem untersuchen wir andere Versionen dieses Problems, die sich in der Art der $2$-Blöcke unterscheiden. Ein gerichteter Graph $G=(V,E)$ heißt einfach zusammenhängend, wenn für jedes Paar von Knoten $v,w\in V$ höchstens ein einfacher Weg von $v$ nach $w$ in $G$ existiert. Buchsbaum und Carlisle (1993) gaben einen Algorithmus an, der in Zeit $O(n^{2})$ überprüft, ob $G$ einfach zusammenhängend ist. In dieser Dissertation beschreiben wir eine verbesserte Version dieses Algorithmus, die Laufzeit $O(s\cdot t+m)$ hat, wobei $s,t$ die Anzahl der Quellen beziehungsweise Senken im reduzierten Graphen sind, den man auf folgende Weise erhält: Kontrahieren jeder stark zusammenhängenden Komponente zu einem Knoten und dann Eliminierung von Knoten mit Eingangsgrad oder Ausgangsgrad $1$ durch eine Kontrahierenoperation. Außerdem zeigen wir, dass das Problem der Berechnung einer Kantenteilmenge $C\subseteq E$ (beziehungsweise Knotenteilmenge $F\subseteq V$), deren Löschen einen einfach-zusammenhängenden Graphen übrig lässt, NP-schwer ist.



http://www.db-thueringen.de/servlets/DocumentServlet?id=26841
Mennicke, Roy;
Model checking concurrent systems using temporal logics, 2015. - Online-Ressource (PDF-Datei: X, 163 S., 1,39 MB) Ilmenau : Techn. Univ., Diss., 2015

In dieser Arbeit wird die Komplexität der automatischen Verifikation von parallelen Systemen mittels Temporallogiken untersucht. Es werden dabei zwei verschiedene Typen von Systemen betrachtet: mehrläufige Programme, die rekursive Prozeduren aufrufen, und verteilte Prozesse, die zur Kommunikation untereinander Nachrichten austauschen. Erstere werden typischerweise durch endliche Automaten mit mehreren Kellern modelliert; Letztere üblicherweise durch endliche Automaten, die über FIFO-Kanäle miteinander kommunizieren (CFMs). In beiden Fällen ist das allgemeine Verifikationsproblem selbst für sehr einfache temporale Logiken unentscheidbar. Daher richten wir das Augenmerk auf Heuristiken, die die Läufe des zu untersuchenden Systems unterapproximieren. Im Kontext der message sequence charts (MSCs), welche als Läufe von CFMs aufgefasst werden können, betrachten wir ausschließlich Verhalten, die eine Ausführung mit beschränkt großen Kanälen zulassen. Im Rahmen der Mehrkellerautomaten konzentrieren wir uns auf geschachtelte Wörter, die bezüglich der Anzahl ihrer Phasen, der Größe ihrer Bereiche bzw. ihrer Teilungsweite beschränkt sind. Dabei sind geschachtelte Wörter Zeichenketten, die für jeden Keller eine Relation aufweisen, die zusammengehörige Schreib- und Leseoperationen auf dem jeweiligen Keller explizit miteinander in Verbindung setzt. Die Art der Spezifikationssprache betreffend untersuchen wir temporale Logiken, deren Modalitäten mittels Formeln der monadischen Logik zweiter Stufe definiert werden können. Dieser Typ von Temporallogiken umfasst nahezu alle bisher in der Literatur behandelten temporalen Logiken. Für jedes von uns untersuchte beschränkte Verifikationsproblem geben wir ein Entscheidungsverfahren an, dessen Komplexität n-fach exponentiell in der jeweilig gewählten Verhaltensbeschränkung (beispielsweise in der Größe der Kanäle) ist. Dabei ist n linear in der Anzahl der monadischen Quantorenalternierungen in den Modalitätsdefinitionen. Überraschenderweise ist die Komplexität nur einfach exponentiell in den Größen der temporalen Formel und des Systemmodells. Weiterhin geben wir für jedes Problem beinahe scharfe untere Schranken an. Mit anderen Worten: Es stellt sich beinahe als ein allgemeines Naturgesetz heraus, dass die Komplexität der automatischen Verifikation im Rahmen von parallelen Systemen im Wesentlichen von der Kompliziertheit der temporalen Logik (gemessen in der Anzahl der Quantorenalternierungen in den Modalitätsdefinitionen) und der gewählten Verhaltensbeschränkung beeinflusst wird und viel weniger von den Größen der temporalen Formel und des Systemmodells. Außerdem betrachten wir im Fall der automatischen Verifikation von CFMs zwei weitere Arten von Temporallogiken. Zum einen erforschen wir konkrete Modalitäten, die üblicherweise im Zusammenhang mit parallelen Systemen Verwendung finden. Hier lässt sich zeigen, dass die Platzkomplexität des beschränkten Verifikationsproblems polynomiell in der Beschränkung und exponentiell in der Anzahl der Prozesse ist. Zum anderen zeigen wir für eine Variante der propositional dynamic logic (PDL) die Vollständigkeit des beschränkten Verifikationsproblems für polynomiellen Platz.



http://www.db-thueringen.de/servlets/DocumentServlet?id=26912
Jouffroy, Jerome; Reger, Johann
Finite-time simultaneous parameter and state estimation using modulating functions. - In: 2015 IEEE Conference on Control Applications (CCA), ISBN 978-1-4799-7787-1, (2015), S. 394-399

http://dx.doi.org/10.1109/CCA.2015.7320661
Rempel, Patrick; Mäder, Patrick
A quality model for the systematic assessment of requirements traceability. - In: 2015 IEEE 23rd International Requirements Engineering Conference (RE), ISBN 978-1-4673-6905-3, (2015), S. 176-185

http://dx.doi.org/10.1109/RE.2015.7320420
Kuang, Hongyu; Mäder, Patrick; Hu, Hao; Ghabi, Achraf; Huang, LiGuo; Lü, Jian; Egyed, Alexander
Can method data dependencies support the assessment of traceability between requirements and source code?. - In: Journal of software: evolution and process, ISSN 2047-7481, Bd. 27 (2015), 11, S. 838-866

https://doi.org/10.1002/smr.1736
Mayr, Simon; Grabmair, Gernot; Reger, Johann
Input design and parameter estimation with open source tools. - In: IFAC-PapersOnLine, ISSN 2405-8963, Bd. 48 (2015), 1, S. 286-291

http://dx.doi.org/10.1016/j.ifacol.2015.05.107
Kalwa, Jörg; Pascoal, António; Ridao, Pere; Birk, Andreas; Glotzbach, Thomas; Brignone, Lorenzo; Bibuli, Marco; Alves, João; Silva, Marina Carreiro
EU project MORPH: current status after 3 years of cooperation under and above water. - In: IFAC-PapersOnLine, ISSN 2405-8963, Bd. 48 (2015), 2, S. 119-124

http://dx.doi.org/10.1016/j.ifacol.2015.06.019
Glotzbach, Thomas; Eckstein, Sebastian; Ament, Christoph
An approach for planning a safe mission begin and end for teams of marine robots. - In: IFAC-PapersOnLine, ISSN 2405-8963, Bd. 48 (2015), 2, S. 100-106

http://dx.doi.org/10.1016/j.ifacol.2015.06.017
Barth, Alexander; Reichhartinger, Markus; Reger, Johann; Horn, Martin; Wulff, Kai
Lyapunov-design for a super-twisting sliding-mode controller using the certainty-equivalence principle. - In: IFAC-PapersOnLine, ISSN 2405-8963, Bd. 48 (2015), 11, S. 860-865

http://dx.doi.org/10.1016/j.ifacol.2015.09.298
Glotzbach, Thomas; Isma, Teuku Reza Auliandra; Ament, Christoph
An approach to combine methods for cooperative navigation and optimal sensor placement in marine robotics. - In: IFAC-PapersOnLine, ISSN 2405-8963, Bd. 48 (2015), 16, S. 107-112

http://dx.doi.org/10.1016/j.ifacol.2015.10.266