Publikationen des Jahres 2000

Dissertationen und Habilitationen

Tobias Vesper. Petrinetze zum Entwurf selbststabilisierender Algorithmen. Dissertation, Humboldt-Universit�t zu Berlin, Mathematisch-Naturwissenschaftliche Fakult�t II, December 2000.

Abstract: Edsger W. Dijkstra pr�gte im Jahr 1974 den Begriff Selbststabilisierung (self-stabilization) in der Informatik. Ein System ist selbststabilisierend, wenn es von jedem denkbaren Zustand aus nach einer endlichen Anzahl von Aktionen ein stabiles Verhalten erreicht. Im Mittelpunkt dieser Arbeit steht der Entwurf selbststabilisierender Algorithmen. Wir stellen eine Petrinetz-basierte Methode zum Entwurf selbststabilisierender Algorithmen vor. Wir validieren unsere Methode an mehreren Fallstudien: Ausgehend von algorithmischen Ideen existierender Algorithmen beschreiben wir jeweils die die schrittweise Entwicklung eines neuen Algorithmus. Dazu geh�rt ein neuer randomisierter selbststabilisierender Algorithmus zur Leader Election in einem Ring von Prozessoren. Dieser Algorithmus ist abgeleitet aus einem publizierten Algorithmus, von dem wir hier erstmals zeigen, da� er fehlerhaft arbeitet. Wir weisen die Speicherminimalit�t unseres Algorithmus nach. Ein weiteres Ergebnis ist der erste Algorithmus, der ohne Time-Out-Aktionen selbststabilisierenden Tokenaustausch in asynchronen Systemen realisiert. Petrinetze bilden einen einheitlichen formalen Rahmen f�r die Modellierung und Verifikation dieser Algorithmen.

@PhDThesis{ Vesper2000_diss,
author = {Tobias Vesper},
title = {{Petrinetze zum Entwurf selbststabilisierender Algorithmen}},
school = {Humboldt-Universit�t zu Berlin, Mathematisch-Naturwissenschaftliche Fakult�t II},
year = 2000,
type = {Dissertation},
month = dec,
pdf = {http://edoc.hu-berlin.de/dissertationen/vesper-tobias-2000-12-08/PDF/Vesper.pdf},
ps = {http://edoc.hu-berlin.de/dissertationen/vesper-tobias-2000-12-08/PS/Vesper.ps},
url = {http://dochost.rz.hu-berlin.de/dissertationen/vesper-tobias-2000-12-08},
abstract = {Edsger W. Dijkstra pr�gte im Jahr 1974 den Begriff Selbststabilisierung (self-stabilization) in der Informatik. Ein System ist selbststabilisierend, wenn es von jedem denkbaren Zustand aus nach einer endlichen Anzahl von Aktionen ein stabiles Verhalten erreicht. Im Mittelpunkt dieser Arbeit steht der Entwurf selbststabilisierender Algorithmen. Wir stellen eine Petrinetz-basierte Methode zum Entwurf selbststabilisierender Algorithmen vor. Wir validieren unsere Methode an mehreren Fallstudien: Ausgehend von algorithmischen Ideen existierender Algorithmen beschreiben wir jeweils die die schrittweise Entwicklung eines neuen Algorithmus. Dazu geh�rt ein neuer randomisierter selbststabilisierender Algorithmus zur Leader Election in einem Ring von Prozessoren. Dieser Algorithmus ist abgeleitet aus einem publizierten Algorithmus, von dem wir hier erstmals zeigen, da� er fehlerhaft arbeitet. Wir weisen die Speicherminimalit�t unseres Algorithmus nach. Ein weiteres Ergebnis ist der erste Algorithmus, der ohne Time-Out-Aktionen selbststabilisierenden Tokenaustausch in asynchronen Systemen realisiert. Petrinetze bilden einen einheitlichen formalen Rahmen f�r die Modellierung und Verifikation dieser Algorithmen.} 
}

Hagen V�lzer. Fairne�, Randomisierung und Konspiration in verteilten Algorithmen. Dissertation, Humboldt-Universit�t zu Berlin, Mathematisch-Naturwissenschaftliche Fakult�t II, December 2000.

Abstract: Fairne� (d.h. faire Konfliktl�sung), Randomisierung (d.h. M�nzw�rfe) und partielle Synchronie sind verschiedene Konzepte, die h�ufig zur L�sung zentraler Synchronisations- und Koordinationsprobleme in verteilten Systemen verwendet werden. Beispiele f�r solche Probleme sind das Problem des wechselseitigen Ausschlusses (kurz: Mutex-Problem) sowie das Konsens-Problem. F�r einige solcher Probleme wurde bewiesen, da� ohne die oben genannten Konzepte keine L�sung f�r das betrachtete Problem existiert. Unm�glichkeitsresultate dieser Art verbessern unser Verst�ndnis der Wirkungsweise verteilter Algorithmen sowie das Verst�ndnis des Trade-offs zwischen einem leicht analysierbaren und einem ausdrucksstarken Modell f�r verteiltes Rechnen. In dieser Arbeit stellen wir zwei neue Unm�glichkeitsresultate vor. Dar�berhinaus beleuchten wir ihre Hintergr�nde. Wir betrachten dabei Modelle, die Randomisierung einbeziehen, da bisher wenig �ber die Grenzen der Ausdrucksst�rke von Randomisierung bekannt ist. Mit einer L�sung eines Problems durch Randomisierung meinen wir, da� das betrachtete Problem mit Wahrscheinlichkeit 1 gel�st wird. Im ersten Teil der Arbeit untersuchen wir die Beziehung von Fairne� und Randomisierung. Einerseits ist bekannt, da� einige Probleme (z.B. das Konsens- Problem) durch Randomisierung nicht aber durch Fairne� l�sbar sind. Wir zeigen nun, da� es andererseits auch Probleme gibt (n�mlich das Mutex-Problem), die durch Fairne�, nicht aber durch Randomisierung l�sbar sind. Daraus folgt, da� Fairne� nicht durch Randomisierung implementiert werden kann. Im zweiten Teil der Arbeit verwenden wir ein Modell, das Fairne� und Randomisierung vereint. Ein solches Modell ist relativ ausdrucksstark: Es erlaubt L�sungen f�r das Mutex-Problem, das Konsens-Problem, sowie eine L�sung f�r das allgemeine Mutex-Problem. Beim allgemeinen Mutex-Problem (auch bekannt als Problem der speisenden Philosophen) ist eine Nachbarschaftsrelation auf den Agenten gegeben und ein Algorithmus gesucht, der das Mutex-Problem f�r jedes Paar von Nachbarn simultan l�st. Schlie�lich betrachten wir das ausfalltolerante allgemeine Mutex-Problem -- eine Variante des allgemeinen Mutex-Problems, bei der Agenten ausfallen k�nnen. Wir zeigen, da� sogar die Verbindung von Fairne� und Randomisierung nicht gen�gt, um eine L�sung f�r das ausfalltolerante allgemeine Mutex-Problem zu konstruieren. Ein Hintergrund f�r dieses Unm�glichkeitsresultat ist ein unerw�nschtes Ph�nomen, f�r das in der Literatur der Begriff Konspiration gepr�gt wurde. Konspiration wurde bisher nicht ad�quat charakterisiert. Wir charakterisieren Konspiration auf der Grundlage nicht-sequentieller Abl�ufe. Desweiteren zeigen wir, da� Konspiration f�r eine gro�e Klasse von Systemen durch die zus�tzliche Annahme von partieller Synchronie verhindert werden kann, d.h. ein konspirationsbehaftetes System kann zu einem randomisierten System verfeinert werden, das unter Fairne� und partieller Synchronie mit Wahrscheinlichkeit 1 konspirationsfrei ist. Partielle Synchronie fordert, da� alle relativen Geschwindigkeiten im System durch eine Konstante beschr�nkt sind, die jedoch den Agenten nicht bekannt ist. Die Darstellung der Unm�glichkeitsresultate und die Charakterisierung von Konspiration wird erst durch die Verwendung nicht-sequentieller Abl�ufe m�glich. Ein nicht-sequentieller Ablauf repr�sentiert im Gegensatz zu einem sequentiellen Ablauf kausale Ordnung und nicht zeitliche Ordnung von Ereignissen. Wir entwickeln in dieser Arbeit eine nicht-sequentielle Semantik f�r randomisierte verteilte Algorithmen, da es bisher keine in der Literatur gibt. In dieser Semantik wird kausale Unabh�ngigkeit durch stochastische Unabh�ngigkeit widergespiegelt.

@PhDThesis{ Voelzer2000_diss,
author = {Hagen V�lzer},
title = {{Fairne�, Randomisierung und Konspiration in verteilten Algorithmen}},
school = {Humboldt-Universit�t zu Berlin, Mathematisch-Naturwissenschaftliche Fakult�t II},
year = 2000,
type = {Dissertation},
month = dec,
pdf = {http://edoc.hu-berlin.de/dissertationen/voelzer-hagen-2000-12-08/PDF/Voelzer.pdf},
ps = {http://edoc.hu-berlin.de/dissertationen/voelzer-hagen-2000-12-08/PS/Voelzer.ps},
url = {http://dochost.rz.hu-berlin.de/dissertationen/voelzer-hagen-2000-12-08},
abstract = {Fairne� (d.h. faire Konfliktl�sung), Randomisierung (d.h. M�nzw�rfe) und partielle Synchronie sind verschiedene Konzepte, die h�ufig zur L�sung zentraler Synchronisations- und Koordinationsprobleme in verteilten Systemen verwendet werden. Beispiele f�r solche Probleme sind das Problem des wechselseitigen Ausschlusses (kurz: Mutex-Problem) sowie das Konsens-Problem. F�r einige solcher Probleme wurde bewiesen, da� ohne die oben genannten Konzepte keine L�sung f�r das betrachtete Problem existiert. Unm�glichkeitsresultate dieser Art verbessern unser Verst�ndnis der Wirkungsweise verteilter Algorithmen sowie das Verst�ndnis des Trade-offs zwischen einem leicht analysierbaren und einem ausdrucksstarken Modell f�r verteiltes Rechnen. In dieser Arbeit stellen wir zwei neue Unm�glichkeitsresultate vor. Dar�berhinaus beleuchten wir ihre Hintergr�nde. Wir betrachten dabei Modelle, die Randomisierung einbeziehen, da bisher wenig �ber die Grenzen der Ausdrucksst�rke von Randomisierung bekannt ist. Mit einer L�sung eines Problems durch Randomisierung meinen wir, da� das betrachtete Problem mit Wahrscheinlichkeit 1 gel�st wird. Im ersten Teil der Arbeit untersuchen wir die Beziehung von Fairne� und Randomisierung. Einerseits ist bekannt, da� einige Probleme (z.B. das Konsens- Problem) durch Randomisierung nicht aber durch Fairne� l�sbar sind. Wir zeigen nun, da� es andererseits auch Probleme gibt (n�mlich das Mutex-Problem), die durch Fairne�, nicht aber durch Randomisierung l�sbar sind. Daraus folgt, da� Fairne� nicht durch Randomisierung implementiert werden kann. Im zweiten Teil der Arbeit verwenden wir ein Modell, das Fairne� und Randomisierung vereint. Ein solches Modell ist relativ ausdrucksstark: Es erlaubt L�sungen f�r das Mutex-Problem, das Konsens-Problem, sowie eine L�sung f�r das allgemeine Mutex-Problem. Beim allgemeinen Mutex-Problem (auch bekannt als Problem der speisenden Philosophen) ist eine Nachbarschaftsrelation auf den Agenten gegeben und ein Algorithmus gesucht, der das Mutex-Problem f�r jedes Paar von Nachbarn simultan l�st. Schlie�lich betrachten wir das ausfalltolerante allgemeine Mutex-Problem -- eine Variante des allgemeinen Mutex-Problems, bei der Agenten ausfallen k�nnen. Wir zeigen, da� sogar die Verbindung von Fairne� und Randomisierung nicht gen�gt, um eine L�sung f�r das ausfalltolerante allgemeine Mutex-Problem zu konstruieren. Ein Hintergrund f�r dieses Unm�glichkeitsresultat ist ein unerw�nschtes Ph�nomen, f�r das in der Literatur der Begriff Konspiration gepr�gt wurde. Konspiration wurde bisher nicht ad�quat charakterisiert. Wir charakterisieren Konspiration auf der Grundlage nicht-sequentieller Abl�ufe. Desweiteren zeigen wir, da� Konspiration f�r eine gro�e Klasse von Systemen durch die zus�tzliche Annahme von partieller Synchronie verhindert werden kann, d.h. ein konspirationsbehaftetes System kann zu einem randomisierten System verfeinert werden, das unter Fairne� und partieller Synchronie mit Wahrscheinlichkeit 1 konspirationsfrei ist. Partielle Synchronie fordert, da� alle relativen Geschwindigkeiten im System durch eine Konstante beschr�nkt sind, die jedoch den Agenten nicht bekannt ist. Die Darstellung der Unm�glichkeitsresultate und die Charakterisierung von Konspiration wird erst durch die Verwendung nicht-sequentieller Abl�ufe m�glich. Ein nicht-sequentieller Ablauf repr�sentiert im Gegensatz zu einem sequentiellen Ablauf kausale Ordnung und nicht zeitliche Ordnung von Ereignissen. Wir entwickeln in dieser Arbeit eine nicht-sequentielle Semantik f�r randomisierte verteilte Algorithmen, da es bisher keine in der Literatur gibt. In dieser Semantik wird kausale Unabh�ngigkeit durch stochastische Unabh�ngigkeit widergespiegelt.}
}

Publikationen in Zeitschriften und B�chern

Adrianna Foremniak and Peter H. Starke. Structural Analysis of Signal-Event Systems. Fundamenta Informaticae, 43(1-4): 81-104, August 2000.

@Article{ ForemniakS2000_fi43,
author = {Adrianna Foremniak and Peter H. Starke},
title = {{Structural Analysis of Signal-Event Systems}},
journal = {Fundamenta Informaticae},
year = 2000,
volume = 43,
number = {1-4},
pages = {81-104},
month = aug 
}

Ekkard Kindler and Axel Martens. Cross-talk revisited - What's the problem?. Petri Net Newsletter, 58: 4-10, 2000. Note: Cover Picture Story.

@Article{ KindlerM2000_pnn58,
author = {Ekkard Kindler and Axel Martens},
title = {{Cross-talk revisited - What's the problem?}},
journal = {Petri Net Newsletter},
year = 2000,
volume = 58,
pages = {4-10},
note = {Cover Picture Story},
ps = {http://www.informatik.hu-berlin.de/top/download/publications/KindlerM2000_pnn58.ps} 


}

Ekkard Kindler and Hagen V�lzer. Algebraic Nets with Flexible Arcs. Theoretical Computer Science, 2000.

@Article{ KindlerV2000_tcs,
author = {Ekkard Kindler and Hagen V�lzer},
title = {{Algebraic Nets with Flexible Arcs}},
journal = {Theoretical Computer Science},
year = 2000 
}

Karsten Schmidt. Flexible net Inscriptions with LoLA. Petri Net Newsletter, 59: 30-44, 2000.

@Article{ Schmidt2000_pnn59,
author = {Karsten Schmidt},
title = {{Flexible net Inscriptions with LoLA}},
journal = {Petri Net Newsletter},
year = 2000,
volume = 59,
pages = {30-44},
keywords = {LoLA} 
}

Karsten Schmidt. How to Calculate Symmetries of Petri Nets. Acta Informatica, 36(7): 545-590, 2000.

Abstract: Symmetric net structure yields symmetric net behaviour. Thus, knowing the symmetries of a net, redundant calculations can be skipped. We present a framework for the calculation of symmetries for several net classes including place/transition nets, timed nets, stochastic nets, self-modifying nets, nets with inhibitor arcs, and many others. Our approach allows the specification of different symmetry groups. Additionally it provides facilities either to calculate symmetries on demand while running the actual analysis algorithm, or to calculate them in advance. For the latter case we define and calculate a ground set of symmetries. Such a set has polynomial size and is sufficient for an efficient implementation of the for all symmetries loop and the partition of net elements into equivalence classes. These two constructions are the usual way to integrate symmetries into an analysis algorithm.

@Article{ Schmidt2000_ai367,
author = {Karsten Schmidt},
title = {{How to Calculate Symmetries of Petri Nets}},
journal = {Acta Informatica},
year = 2000,
volume = 36,
number = 7,
pages = {545-590},
url = {http://www.springerlink.com/openurl.asp?genre=article&eissn=1432-0525&volume=36&issue=7&spage=545},
abstract = {Symmetric net structure yields symmetric net behaviour. Thus, knowing the symmetries of a net, redundant calculations can be skipped. We present a framework for the calculation of symmetries for several net classes including place/transition nets, timed nets, stochastic nets, self-modifying nets, nets with inhibitor arcs, and many others. Our approach allows the specification of different symmetry groups. Additionally it provides facilities either to calculate symmetries on demand while running the actual analysis algorithm, or to calculate them in advance. For the latter case we define and calculate a ground set of symmetries. Such a set has polynomial size and is sufficient for an efficient implementation of the for all symmetries loop and the partition of net elements into equivalence classes. These two constructions are the usual way to integrate symmetries into an analysis algorithm.} 
}

Karsten Schmidt. Stubborn Sets for Model Checking the EF/AG Fragment of CTL. Fundamenta Informaticae, 43(1-4): 331-341, August 2000.

Abstract: The general stubborn set approach to CTL model checking [2] has the drawback that one either finds a stubborn set with only one enabled transition or one has to expand all enabled transitions. This restriction does not apply in our approach to a fragment of CTL. Furthermore, our reduction does not depend on the invisibility of transitions in a stubborn set.

@Article{ Schmidt2000_fi43,
author = {Karsten Schmidt},
title = {{Stubborn Sets for Model Checking the EF/AG Fragment of CTL}},
journal = {Fundamenta Informaticae},
year = 2000,
volume = 43,
number = {1-4},
pages = {331-341},
month = aug,
ps = {http://www.informatik.hu-berlin.de/~kschmidt/efag.ps},
abstract = {The general stubborn set approach to CTL model checking [2] has the drawback that one either finds a stubborn set with only one enabled transition or one has to expand all enabled transitions. This restriction does not apply in our approach to a fragment of CTL. Furthermore, our reduction does not depend on the invisibility of transitions in a stubborn set.} 
}

Konferenzbeitr�ge und Beitr�ge auf Workshops

Matthias J�ngel, Ekkard Kindler, and Michael Weber. The Petri Net Markup Language. In S. Philippi, editor, 7. Workshop Algorithmen und Werkzeuge f�r Petrinetze, Fachberichte Informatik 7/2000, pages 47-52, June 2000. Universit�t Koblenz-Landau. Note: Also in: Petri Net Newsletter 59, pages 24-29, October 2000.

@InProceedings{ JuengelKW2000_awpn,
author = {Matthias J�ngel and Ekkard Kindler and Michael Weber},
title = {{The Petri Net Markup Language}},
editor = {S. Philippi},
booktitle = {{7. Workshop Algorithmen und Werkzeuge f�r Petrinetze, Fachberichte Informatik 7/2000}},
year = 2000,
pages = {47-52},
month = jun,
publisher = {Universit�t Koblenz-Landau},
note = {also in: Petri Net Newsletter 59, pages 24-29, October 2000},
ps = {http://www.informatik.hu-berlin.de/top/download/publications/JuengelKW2000_awpn.ps} 


}

Matthias J�ngel, Ekkard Kindler, and Michael Weber. Towards a Generic Interchange Format for Petri Nets. In Remi Bastide, Jonathan Billington, Ekkard Kindler, Fabrice Kordon, and Kjeld H. Mortensen, editors, Meeting on XML/SGML based Interchange Formats for Petri Nets, 21. ICATPN, �rhus, D�nemark, pages 1-5, June 2000.

@InProceedings{ JuengelKW2000_icatpn,
author = {Matthias J�ngel and Ekkard Kindler and Michael Weber},
title = {{Towards a Generic Interchange Format for Petri Nets}},
editor = {Remi Bastide and Jonathan Billington and Ekkard Kindler and Fabrice Kordon and Kjeld H. Mortensen},
booktitle = {{Meeting on XML/SGML based Interchange Formats for Petri Nets, 21. ICATPN}},
year = 2000,
pages = {1-5},
address = {�rhus, D�nemark},
month = jun,
ps = {http://www.informatik.hu-berlin.de/top/download/publications/JuengelKW2000_icatpn.ps} 


}

Ekkard Kindler. Consistency, Causality, Petri Nets, and Automata. In Hans-Dieter Burkhard, Ludwik Czaja, Andrzej Skowron, and Peter H. Starke, editors, Workshop Concurrency, Specification & Programming (CS&P 2000), pages 93-104, October 2000.

@InProceedings{ Kindler2000_csp,
author = {Ekkard Kindler},
title = {{Consistency, Causality, Petri Nets, and Automata}},
editor = {Hans-Dieter Burkhard and Ludwik Czaja and Andrzej Skowron and Peter H. Starke},
booktitle = {{Workshop Concurrency, Specification \& Programming (CS\&P 2000)}},
year = 2000,
pages = {93-104},
month = oct,
ps = {http://www.informatik.hu-berlin.de/top/download/publications/Kindler2000_csp.ps} 


}

Ekkard Kindler. Serializability, concurrency control and replication control. In G. Saake, K. Schwarz, and C. T�rker, editors, Transactions and Database Dynamics, Proceedings of the 8th International Workshop on Foundations of Models and Languages for Data and Objects, Selected Papers, volume 1773 of Lecture Notes in Computer Science, pages 26-44, 2000. Springer-Verlag.

@InProceedings{ Kindler2000_lncs1773,
author = {Ekkard Kindler},
title = {{Serializability, concurrency control and replication control}},
editor = {G. Saake and K. Schwarz and C. T�rker},
booktitle = {{Transactions and Database Dynamics, Proceedings of the 8th International Workshop on Foundations of Models and Languages for Data and Objects, Selected Papers}},
year = 2000,
series = {Lecture Notes in Computer Science},
volume = 1773,
pages = {26-44},
publisher = {Springer-Verlag} 
}

Ekkard Kindler, Axel Martens, and Wolfgang Reisig. Inter-operability of Workshop Applications - Local Criteria for Global Soundness. In Wil M. P. van der Aalst, J�rg Desel, and Andreas Oberweis, editors, Business Process Management, volume 1806 of Lecture Notes in Computer Science, pages 235-253, 2000. Springer-Verlag.

@InProceedings{ KindlerMR2000_lncs1806,
author = {Ekkard Kindler and Axel Martens and Wolfgang Reisig},
title = {{Inter-operability of Workshop Applications - Local Criteria for Global Soundness}},
editor = {{Wil} {M.} {P.} {van} {der} Aalst and J�rg Desel and Andreas Oberweis},
booktitle = {{Business Process Management}},
year = 2000,
series = {Lecture Notes in Computer Science},
volume = 1806,
pages = {235-253},
publisher = {Springer-Verlag},
ps = {http://www.informatik.hu-berlin.de/top/download/publications/KindlerMR2000_lncs1806.ps} 


}

Ekkard Kindler and Michael Weber. The Petri Net Kernel. In Kjeld H�yer Mortensen, editor, Tool Demonstrations, 21. ICATPN, �rhus, Denmark, pages 71-75, June 2000.

@InProceedings{ KindlerW2000_icatpn,
author = {Ekkard Kindler and Michael Weber},
title = {{The Petri Net Kernel}},
editor = {Kjeld H�yer Mortensen},
booktitle = {{Tool Demonstrations, 21. ICATPN}},
year = 2000,
pages = {71-75},
address = {�rhus, Denmark},
month = jun,
ps = {http://www.informatik.hu-berlin.de/top/download/publications/KindlerW2000_icatpn.ps},
keywords = {Petri Net Kernel} 
}

Wolfgang Reisig. The Linear Theory of Multiset Based Dynamic Systems. In Cristian Calude, Gheorghe Paun, Grzegorz Rozenberg, and Arto Salomaa, editors, Workshop on Multiset Processing (WMP 2000), volume 2235 of Lecture Notes in Computer Science, pages 287-298, 2000. Springer-Verlag.

@InProceedings{ Reisig2000_wmp,
author = {Wolfgang Reisig},
title = {{The Linear Theory of Multiset Based Dynamic Systems}},
editor = {Cristian Calude and Gheorghe Paun and Grzegorz Rozenberg and Arto Salomaa},
booktitle = {{Workshop on Multiset Processing (WMP 2000)}},
year = 2000,
series = {Lecture Notes in Computer Science},
volume = 2235,
pages = {287-298},
publisher = {Springer-Verlag},
url = {http://link.springer.de/link/service/series/0558/bibs/2235/22350287.htm} 


}

Wolfgang Reisig. Towards an ASM Thesis for Unconventional Algorithms. In Yuri Gurevich, Philipp W. Kutter, Martin Odersky, and Lothar Thiele, editors, Abstract State Machines, volume 1912 of Lecture Notes in Computer Science, pages 112-130, 2000. Springer-Verlag.

Abstract: All descriptions of algorithms, be they formal or informal, employ data structures, operations on them, and some policy to cause operations be applied to data. Gurevich calls a formal description technique for algorithms algorithm universal if it allows for each informally described algorithm a formal representation that would essentially make precise the notions used in the informal description, not employing additional data, operations or steps. Gurevich's ASM thesis claims Abstract State Machines be algorithm universal for conventional, sequential algorithms. Here we are behind properties of formal presentations that are algorithm universal for unconventional, distributed algorithms.

@InProceedings{ Reisig2000_lncs1912,
author = {Wolfgang Reisig},
title = {{Towards an ASM Thesis for Unconventional Algorithms}},
editor = {Yuri Gurevich and Philipp W. Kutter and Martin Odersky and Lothar Thiele},
booktitle = {{Abstract State Machines}},
year = 2000,
series = {Lecture Notes in Computer Science},
volume = 1912,
pages = {112-130},
publisher = {Springer-Verlag},
url = {http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=1912&spage=112},
keywords = {ASM},
abstract = {All descriptions of algorithms, be they formal or informal, employ data structures, operations on them, and some policy to cause operations be applied to data. Gurevich calls a formal description technique for algorithms algorithm universal if it allows for each informally described algorithm a formal representation that would essentially make precise the notions used in the informal description, not employing additional data, operations or steps. Gurevich's ASM thesis claims Abstract State Machines be algorithm universal for conventional, sequential algorithms. Here we are behind properties of formal presentations that are algorithm universal for unconventional, distributed algorithms.} 
}

Karsten Schmidt. Integrating Low Level Symmetries into Reachability Analysis. In Susanne Graf and Michael I. Schwartzbach, editors, Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference, TACAS 2000, volume 1785 of Lecture Notes in Computer Science, pages 315-330, 2000. Springer-Verlag.

Abstract: We present three methods for the integration of symmetries into reachability analysis. Two of them lead to maximal reduction but their runtime depends on the symmetry structure. The third one works always fast but does not always yield maximal reduction.

@InProceedings{ Schmidt2000_lncs1785,
author = {Karsten Schmidt},
title = {{Integrating Low Level Symmetries into Reachability Analysis}},
editor = {Susanne Graf and Michael I. Schwartzbach},
booktitle = {{Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference, TACAS 2000}},
year = 2000,
series = {Lecture Notes in Computer Science},
volume = 1785,
pages = {315-330},
publisher = {Springer-Verlag},
pdf = {http://citeseer.ist.psu.edu/rd/30200811%2C343848%2C1%2C0.25%2CDownload/http://citeseer.ist.psu.edu/cache/papers/cs/12935/http:zSzzSzwww.informatik.hu-berlin.dezSz%7EkschmidtzSzsymmreach.pdf/schmidt99integrating.pdf},
ps = {http://www.informatik.hu-berlin.de/~kschmidt/symmreach.ps},
url = {http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=1785&spage=315},
abstract = {We present three methods for the integration of symmetries into reachability analysis. Two of them lead to maximal reduction but their runtime depends on the symmetry structure. The third one works always fast but does not always yield maximal reduction.} 
}

Karsten Schmidt. LoLA: A Low Level Analyser. In Mogens Nielsen and Dan Simpson, editors, Application and Theory of Petri Nets, 21st International Conference (ICATPN 2000), volume 1825 of Lecture Notes in Computer Science, pages 465-474, June 2000. Springer-Verlag.

Abstract: With LoLA, we put recently developed state space oriented algorithms to other tool developers disposal. Providing a simple interface was a major design goal such that it is as easy as possible to integrate LoLA into tools of different application domains. LoLA supports place/transition nets. Implemented verification techniques cover standard properties (liveness, reversibility, boundedness, reachability, dead transitions, deadlocks, home states) as well as satisfiability of state predicates and CTL model checking. For satisfiability, both exhaustive search and heuristically goal oriented system execution are supported. For state space reduction, LoLA features symmetries, stubborn sets, and coverability graphs.

@InProceedings{ Schmidt2000_lncs1825,
author = {Karsten Schmidt},
title = {{LoLA: A Low Level Analyser}},
editor = {Mogens Nielsen and Dan Simpson},
booktitle = {{Application and Theory of Petri Nets, 21st International Conference (ICATPN 2000)}},
year = 2000,
series = {Lecture Notes in Computer Science},
volume = 1825,
pages = {465-474},
month = jun,
publisher = {Springer-Verlag},
url = {http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=1825&spage=465},
keywords = {LoLA},
abstract = {With LoLA, we put recently developed state space oriented algorithms to other tool developers disposal. Providing a simple interface was a major design goal such that it is as easy as possible to integrate LoLA into tools of different application domains. LoLA supports place/transition nets. Implemented verification techniques cover standard properties (liveness, reversibility, boundedness, reachability, dead transitions, deadlocks, home states) as well as satisfiability of state predicates and CTL model checking. For satisfiability, both exhaustive search and heuristically goal oriented system execution are supported. For state space reduction, LoLA features symmetries, stubborn sets, and coverability graphs.} 
}

Karsten Schmidt. Narrowing the state space of Petri nets using the state equation. In Workshop on Concurrency, Specification and Programming, Berlin, 2000.

@InProceedings{ Schmidt2000_csp,
author = {Karsten Schmidt},
title = {{Narrowing the state space of Petri nets using the state equation}},
booktitle = {{Workshop on Concurrency, Specification and Programming}},
year = 2000,
address = {Berlin} 
}

Technische Berichte

Adrianna Foremniak and Wolfgang Reisig. A Temporal Logic of Distributed Actions (TLDA). Informatik-Berichte 140, Humboldt-Universit�t zu Berlin, 2000.

@TechReport{ ForemniakR2000_hub_tr140,
author = {Adrianna Foremniak and Wolfgang Reisig},
title = {{A Temporal Logic of Distributed Actions (TLDA)}},
institution = {Humboldt-Universit�t zu Berlin},
year = 2000,
type = {Informatik-Berichte},
number = 140,
keywords = {TLDA, Temporale Logik} 
}

Felix C. G�rtner and Hagen V�lzer. Redundancy in Space in Fault-Tolerant Systems. Technical Report TUD-BS-2000-06, Department of Computer Science, Darmstadt University of Technology, July 2000.

@TechReport{ GaertnerV2000_tud_tr200006,
author = {Felix C. G�rtner and Hagen V�lzer},
title = {{Redundancy in Space in Fault-Tolerant Systems}},
institution = {Department of Computer Science, Darmstadt University of Technology},
year = 2000,
type = {Technical Report},
number = {TUD-BS-2000-06},
month = jul,
url = {http://sherry.ifi.unizh.ch/artner00redundancy.html} 
}

Ekkard Kindler and Dennis Shasha. Verifying a Design Pattern for the Fault-Tolerant Execution of Parallel Programs. Technical Report TR2000-803, New York University, Courant Institute of Mathematical Sciences, Computer Science Department, June 2000.

@TechReport{ KindlerS2000_nyu_tr803,
author = {Ekkard Kindler and Dennis Shasha},
title = {{Verifying a Design Pattern for the Fault-Tolerant Execution of Parallel Programs}},
institution = {New York University, Courant Institute of Mathematical Sciences, Computer Science Department},
year = 2000,
type = {Technical Report},
number = {TR2000-803},
month = jun,
pdf = {http://www.informatik.hu-berlin.de/top/download/publications/KindlerS2000_nyu_tr803.pdf} 


}

Sibylle Peuker. Property Preserving Transition Refinement with Concurrent Runs. Informatik-Berichte 139, Humboldt-Universit�t zu Berlin, July 2000.

@TechReport{ Peuker2000_hub_tr139,
author = {Sibylle Peuker},
title = {{Property Preserving Transition Refinement with Concurrent Runs}},
institution = {Humboldt-Universit�t zu Berlin},
year = 2000,
type = {Informatik-Berichte},
number = 139,
month = jul 
}

Tobias Vesper. Randomized Self-Stabilizing Leader Election (Extended Abstract). Informatik-Berichte 133, Humboldt-Universit�t zu Berlin, January 2000.

@TechReport{ Vesper2000_hub_tr133,
author = {Tobias Vesper},
title = {{Randomized Self-Stabilizing Leader Election (Extended Abstract)}},
institution = {Humboldt-Universit�t zu Berlin},
year = 2000,
type = {Informatik-Berichte},
number = 133,
month = jan,
ps = {http://www.informatik.hu-berlin.de/top/download/publications/Vesper2000_hub_tr133.ps} 


}

Michael Weber. An XML-based Approach towards an Interchange Format for Petri Nets (Extended Abstract). Informatik-Berichte 140, Humboldt-Universit�t zu Berlin, October 2000.

@TechReport{ Weber2000_hub_tr140,
author = {Michael Weber},
title = {{An XML-based Approach towards an Interchange Format for Petri Nets (Extended Abstract)}},
institution = {Humboldt-Universit�t zu Berlin},
year = 2000,
type = {Informatik-Berichte},
number = 140,
month = oct,
pages = {351-353} 
}

Studien- und Diplomarbeiten

Abdourahaman. DAWN-ILF Tool. Modelchecking Anwendung. Diplomarbeit, Humboldt-Universit�t zu Berlin, September 2000.

@MastersThesis{ Abdourahaman2000_da,
author = {Abdourahaman},
title = {{DAWN-ILF Tool. Modelchecking Anwendung}},
school = {Humboldt-Universit�t zu Berlin},
year = 2000,
type = {Diplomarbeit},
month = sep,
keywords = {DAWN} 
}

zur�ck zur �bersicht

Theorie der Programmierung | Kontakt | XHTML 1.0 | Fri Sep 11 16:30:32 2009