Publikationen des Jahres 1999
Bücher und Konferenzbände
Hartmut Ehrig, Wolfgang Reisig, and Herbert Weber, editors. Colloquium on Petri Net Technologies for Modelling Communication Based Systems, October 1999. Fraunhofer Gesellschaft ISST.
@Proceedings{ EhrigRW1999_pntmcbs, title = {{Colloquium on Petri Net Technologies for Modelling Communication Based Systems}}, year = 1999, editor = {Hartmut Ehrig and Wolfgang Reisig and Herbert Weber}, month = oct, publisher = {Fraunhofer Gesellschaft ISST}, url = {http://www.informatik.hu-berlin.de/PNT/Coll/index.html} }
Publikationen in Zeitschriften und Büchern
Thomas Baar and Ekkart Kindler. ILF and DAWN for verifying distributed algorithms - an idea for a tool. Fundamenta Informaticae, 37(3):201-211, February 1999.
@Article{ BaarK1999_fi373, author = {Thomas Baar and Ekkart Kindler}, title = {{ILF and DAWN for verifying distributed algorithms - an idea for a tool}}, journal = {Fundamenta Informaticae}, year = 1999, volume = 37, number = 3, pages = {201-211}, month = feb, keywords = {DAWN} }Ekkart Kindler and Sibylle Peuker. Integrating distributed algorithms into distributed systems. Fundamenta Informaticae, 37(3):291-309, February 1999.
@Article{ KindlerP1999_fi373, author = {Ekkart Kindler and Sibylle Peuker}, title = {{Integrating distributed algorithms into distributed systems}}, journal = {Fundamenta Informaticae}, year = 1999, volume = 37, number = 3, pages = {291-309}, month = feb }Karsten Schmidt. Model-Checking with Coverability Graphs. Formal Methods in System Design, 15(3):239-254, November 1999.
Abstract: We show that several formulas of a temporal logic can be verified using the coverability graph of the underlying system. Of course, the procedure is not capable of verifying all formulae, since already the reachability problem for (unbounded) Petri nets is computationally hard. Thus, the procedure returns true, false, or unknown for a query. The formulae that can be verified cover most of the well known standard properties which have been listed in the context of coverability graph analysis so far. @Article{ Schmidt1999_fmsd153, author = {Karsten Schmidt}, title = {{Model-Checking with Coverability Graphs}}, journal = {Formal Methods in System Design}, year = 1999, volume = 15, number = 3, pages = {239-254}, month = nov, publisher = {Springer-Verlag}, url = {http://www.springerlink.com/openurl.asp?genre=article&eissn=1572-8102&volume=15&issue=3&spage=239}, abstract = {We show that several formulas of a temporal logic can be verified using the coverability graph of the underlying system. Of course, the procedure is not capable of verifying all formulae, since already the reachability problem for (unbounded) Petri nets is computationally hard. Thus, the procedure returns true, false, or unknown for a query. The formulae that can be verified cover most of the well known standard properties which have been listed in the context of coverability graph analysis so far.} }
Konferenzbeiträge und Beiträge auf Workshops
Thomas Baar, Ekkart Kindler, and Hagen Völzer. Verifying Intuition - ILF Checks DAWN Proofs. In Application and Theory of Petri Nets, 20th International Conference, ICATPN '99, Proceedings, volume 1639 of Lecture Notes in Computer Science, pages 404-424, 1999. Springer-Verlag. Note: Also in: Informatik-Bericht der Humboldt-Universität zu Berlin, Nr. 119, March 1999.
Abstract: The DAWN approach allows to model and verify distributed algorithms in an intuitive way. At a first glance, a DAWN proof may appear to be informal. In this paper, we argue that DAWN proofs are formal and can be checked for correctness fully automatically by automated theorem provers. The basic technique are proof rules which generate proof obligations. For the definition of the proof rules we adopt assertions and we introduce conflict formulas for algebraic Petri nets. Experiments show that the generated proof obligations can be automatically checked by theorem provers. @InProceedings{ BaarKV1999_lncs1639, author = {Thomas Baar and Ekkart Kindler and Hagen Völzer}, title = {{Verifying Intuition - ILF Checks DAWN Proofs}}, booktitle = {{Application and Theory of Petri Nets, 20th International Conference, ICATPN '99, Proceedings}}, year = 1999, series = {Lecture Notes in Computer Science}, volume = 1639, pages = {404-424}, publisher = {Springer-Verlag}, note = {also in: Informatik-Bericht der Humboldt-Universität zu Berlin, Nr. 119, March 1999}, url = {http://link.springer.de/link/service/series/0558/bibs/1639/16390404.htm}, keywords = {DAWN}, abstract = {The DAWN approach allows to model and verify distributed algorithms in an intuitive way. At a first glance, a DAWN proof may appear to be informal. In this paper, we argue that DAWN proofs are formal and can be checked for correctness fully automatically by automated theorem provers. The basic technique are proof rules which generate proof obligations. For the definition of the proof rules we adopt assertions and we introduce conflict formulas for algebraic Petri nets. Experiments show that the generated proof obligations can be automatically checked by theorem provers.} }Ekkart Kindler. Serializability, concurrency control and replication control. In G. Saake, K. Schwarz, and C. Türker, editors, Transactions and Database Dynamics, Proceedings of the Eighth International Workshop on Foundations of Models and Languages for Data and Objects, pages 98-114, September 1999.
@InProceedings{ Kindler1999_fmldo, author = {Ekkart 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 Eighth International Workshop on Foundations of Models and Languages for Data and Objects}}, year = 1999, pages = {98-114}, month = sep }Ekkart Kindler, Tobias Vesper, and Michael Weber. Application-oriented verification scenarios. In Hartmut Ehrig, Wolfgang Reisig, and Herbert Weber, editors, Colloquium on Petri Net Technologies for Modelling Communication Based Systems, pages 279-297, October 1999. Fraunhofer Gesellschaft ISST.
@InProceedings{ KindlerVW1999_pntmcbs, author = {Ekkart Kindler and Tobias Vesper and Michael Weber}, title = {{Application-oriented verification scenarios}}, pages = {279-297}, crossref = {EhrigRW1999_pntmcbs}, year = 1999 }Ekkart Kindler and Michael Weber. Der Petrinetz-Kern: Ein Überblick. In E. Schnieder, editor, Entwicklung und Betrieb komplexer Automatisierungssysteme, 6. Fachtagung, Band II, pages 641-642, May 1999.
@InProceedings{ KindlerW1999_ebkas, author = {Ekkart Kindler and Michael Weber}, title = {{Der Petrinetz-Kern: Ein Überblick}}, editor = {E. Schnieder}, booktitle = {{Entwicklung und Betrieb komplexer Automatisierungssysteme, 6. Fachtagung, Band II}}, year = 1999, pages = {641-642}, month = may, keywords = {Petri Net Kernel} }Ekkart Kindler and Michael Weber. The Petri Net Kernel - An Infrastructure for Building Petri Net Tools. In 20th International Conference on Application and Theory of Petri Nets - Petri Net Tool Presentations, pages 10-19, June 1999. College of William and Mary, Williamsburg, Virginia, USA.
Abstract: The Petri Net Kernel is an infrastructure for building Petri net tools. It relieves the programmer of a Petri net tool from implementing standard functionality on Petri nets. In this paper, we briefly discuss the motivation, the concepts, and the realization of the Petri Net Kernel. @InProceedings{ KindlerW1999_icatpn, author = {Ekkart Kindler and Michael Weber}, title = {{The Petri Net Kernel - An Infrastructure for Building Petri Net Tools}}, booktitle = {{20th International Conference on Application and Theory of Petri Nets - Petri Net Tool Presentations}}, year = 1999, pages = {10-19}, month = jun, publisher = {College of William and Mary, Williamsburg, Virginia, USA}, ps = {http://www.informatik.hu-berlin.de/top/download/publications/KindlerW1999_icatpn.ps}, keywords = {Petri Net Kernel}, abstract = {The Petri Net Kernel is an infrastructure for building Petri net tools. It relieves the programmer of a Petri net tool from implementing standard functionality on Petri nets. In this paper, we briefly discuss the motivation, the concepts, and the realization of the Petri Net Kernel.} }Axel Martens and Ekkart Kindler. Szenarios - Lokale Kriterien für globale Korrektheit. In K. Spies and B. Schätz, editors, Formale Beschreibungstechniken für verteilte Systeme, 9. GI/ITG Fachgesprächs, June 1999. Utz Verlag, München.
@InProceedings{ MartensK1999_giitg, author = {Axel Martens and Ekkart Kindler}, title = {{Szenarios - Lokale Kriterien für globale Korrektheit}}, editor = {K. Spies and B. Schätz}, booktitle = {{Formale Beschreibungstechniken für verteilte Systeme, 9. GI/ITG Fachgesprächs}}, year = 1999, month = jun, publisher = {Utz Verlag, München}, ps = {http://www.informatik.hu-berlin.de/top/download/publications/MartensK1999_giitg.ps} }Karsten Schmidt. LoLA wird Pfadfinder. In Workshop Algorithmen und Werkzeuge für Petrinetze, Frankfurt, pages 48-53, 1999.
Abstract: LoLA ist ein erreichbarkeitsgraphbasiertes Werkzeug für Stellen/Transitions-Netze. Hier geht es um LoLAs Fähigkeit, erreichbare Zustände mit vorgegebenen Eigenschaften zu suchen und im Erfolgsfall einen solchen Zustand mit einem Weg von der Anfangsmarkierung dorthin anzugeben. Die Besonderheit besteht darin, daß während der Suche nur zwei Zustände gespeichert werden: der Anfangszustand und der aktuelle Zustand. Anstatt also den Zustandsraum systematisch zu durchmustern (und dabei meist am Speicherende zu scheitern), navigiert LoLA ohne Kenntnis der schon betretenen Zustände durch den Erreichbarkeitsgraph. Daß sie trotzdem ihre Aufgabe erfolgreich löst, liegt an ihren spezifischen Fähigkeiten: Schnelligkeit, Bescheidenheit, Zielstrebigkeit, Neugier und Ausdauer. @InProceedings{ Schmidt1999_awpn, author = {Karsten Schmidt}, title = {{LoLA wird Pfadfinder}}, booktitle = {{Workshop Algorithmen und Werkzeuge für Petrinetze}}, year = 1999, pages = {48-53}, address = {Frankfurt}, pdf = {http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-26/schmidt.pdf}, keywords = {LoLA}, abstract = {LoLA ist ein erreichbarkeitsgraphbasiertes Werkzeug für Stellen/Transitions-Netze. Hier geht es um LoLAs Fähigkeit, erreichbare Zustände mit vorgegebenen Eigenschaften zu suchen und im Erfolgsfall einen solchen Zustand mit einem Weg von der Anfangsmarkierung dorthin anzugeben. Die Besonderheit besteht darin, daß während der Suche nur zwei Zustände gespeichert werden: der Anfangszustand und der aktuelle Zustand. Anstatt also den Zustandsraum systematisch zu durchmustern (und dabei meist am Speicherende zu scheitern), navigiert LoLA ohne Kenntnis der schon betretenen Zustände durch den Erreichbarkeitsgraph. Daß sie trotzdem ihre Aufgabe erfolgreich löst, liegt an ihren spezifischen Fähigkeiten: Schnelligkeit, Bescheidenheit, Zielstrebigkeit, Neugier und Ausdauer.} }Karsten Schmidt. Stubborn Sets for Modelchecking the EF/AG-Fragment of CTL. In Workshop on Concurrency, Specification and Programming, Warsaw, pages 204-213, 1999.
@InProceedings{ Schmidt1999_csp, author = {Karsten Schmidt}, title = {{Stubborn Sets for Modelchecking the EF/AG-Fragment of CTL}}, booktitle = {{Workshop on Concurrency, Specification and Programming}}, year = 1999, pages = {204-213}, address = {Warsaw} }Karsten Schmidt. Stubborn Sets for Standard Properties. In Application and Theory of Petri Nets, 20th International Conference, ICATPN '99, Proceedings, volume 1639 of Lecture Notes in Computer Science, pages 46-65, 1999. Springer-Verlag.
Abstract: Stubborn sets are a tool for state space reduction preserving certain system properties. We present stubborn set approaches for all popular Petri net standard properties. This extends the list of properties that can be analysed successfully (including boundedness, reversibility). For other properties, our approach can lead to larger reductions (reachability) than previous ones. Furthermore, shortest and cheapest witness paths for several properties are now preserved. @InProceedings{ Schmidt1999_lncs1639, author = {Karsten Schmidt}, title = {{Stubborn Sets for Standard Properties}}, booktitle = {{Application and Theory of Petri Nets, 20th International Conference, ICATPN '99, Proceedings}}, year = 1999, series = {Lecture Notes in Computer Science}, volume = 1639, pages = {46-65}, publisher = {Springer-Verlag}, url = {http://link.springer.de/link/service/series/0558/bibs/1639/16390046.htm}, abstract = {Stubborn sets are a tool for state space reduction preserving certain system properties. We present stubborn set approaches for all popular Petri net standard properties. This extends the list of properties that can be analysed successfully (including boundedness, reversibility). For other properties, our approach can lead to larger reductions (reachability) than previous ones. Furthermore, shortest and cheapest witness paths for several properties are now preserved.} }Tobias Vesper and Michael Weber. Automatisches Verteiltes Rücksetzen. In K. Spies and B. Schätz, editors, Formale Beschreibungstechniken für verteilte Systeme, 9. GI/ITG Fachgesprächs, June 1999. Utz Verlag, München.
@InProceedings{ VesperW1999_giitg, author = {Tobias Vesper and Michael Weber}, title = {{Automatisches Verteiltes Rücksetzen}}, editor = {K. Spies and B. Schätz}, booktitle = {{Formale Beschreibungstechniken für verteilte Systeme, 9. GI/ITG Fachgesprächs}}, year = 1999, month = jun, publisher = {Utz Verlag, München} }Michael Weber. Der Petrinetz-Würfel im Petrinetz-Kern. In A. Oberweis J. Desel, editor, 6. Workshop Algorithmen und Werkzeuge für Petrinetze, pages 69-74, October 1999. J. W. Goethe-Universität Frankfurt/Main, Institut für Wirtschaftsinformatik.
@InProceedings{ Weber1999_awpn, author = {Michael Weber}, title = {{Der Petrinetz-Würfel im Petrinetz-Kern}}, editor = {J. Desel, A. Oberweis}, booktitle = {{6. Workshop Algorithmen und Werkzeuge für Petrinetze}}, year = 1999, pages = {69-74}, month = oct, publisher = {J. W. Goethe-Universität Frankfurt/Main, Institut für Wirtschaftsinformatik}, ps = {http://www.informatik.hu-berlin.de/top/download/publications/Weber1999_awpn.ps}, keywords = {Petri Net Kernel} }Michael Weber. The Tool Developer View of the 'Petri Net Baukasten'. In Hartmut Ehrig, Wolfgang Reisig, and Herbert Weber, editors, Colloquium on Petri Net Technologies for Modelling Communication Based Systems, pages 267-277, October 1999. Fraunhofer Gesellschaft ISST.
Abstract: Users and developers of Petri net tools have different requirements on an appropriate support. Both are potential users of the "Petri Net Baukasten". A user of a Petri net tool is supported by the whole "Petri Net Baukasten" depending on his need. Therefore, the Tool Developer View focuses on tool developer support. Differently skilled tool developer need different support. This paper concentrates on support for developers who are not so familiar with certain techniques. @InProceedings{ Weber1999_pntmcbs, author = {Michael Weber}, title = {{The Tool Developer View of the 'Petri Net Baukasten'}}, pages = {267-277}, ps = {http://www.informatik.hu-berlin.de/top/download/publications/Weber1999_pntmcbs.ps}, abstract = {Users and developers of Petri net tools have different requirements on an appropriate support. Both are potential users of the "Petri Net Baukasten". A user of a Petri net tool is supported by the whole "Petri Net Baukasten" depending on his need. Therefore, the Tool Developer View focuses on tool developer support. Differently skilled tool developer need different support. This paper concentrates on support for developers who are not so familiar with certain techniques. }, crossref = {EhrigRW1999_pntmcbs}, year = 1999 }
Technische Berichte
Anne Battke, Alexander Borusan, Juliane Dehnert, Hartmut Ehrig, Claudia Ermel, Maike Gajewsky, Kathrin Hoffmann, Bodo Hohberg, Gabriel Juhás, Sabine Lembke, Axel Martens, Julia Padberg, Wolfgang Reisig, Tobias Vesper, Herbert Weber, and Michael Weber. Petrinetz-Technologie: Initial Realization of the Petri Net Baukasten. Informatik-Berichte 129, Humboldt-Universität zu Berlin, October 1999.
@TechReport{ BattkeBDEEGHHJLMPRVWW1999_hub_tr129, author = {Anne Battke and Alexander Borusan and Juliane Dehnert and Hartmut Ehrig and Claudia Ermel and Maike Gajewsky and Kathrin Hoffmann and Bodo Hohberg and Gabriel Juhás and Sabine Lembke and Axel Martens and Julia Padberg and Wolfgang Reisig and Tobias Vesper and Herbert Weber and Michael Weber}, title = {{Petrinetz-Technologie: Initial Realization of the Petri Net Baukasten}}, institution = {Humboldt-Universität zu Berlin}, year = 1999, type = {Informatik-Berichte}, number = 129, month = oct, ps = {http://www.informatik.hu-berlin.de/top/download/publications/BattkeBDEEGHHJLMPRVWW1999_hub_tr129.ps} }Ekkart Kindler. A classification of consistency models. Technical Report B99-14, Freie Universität Berlin, Institut für Informatik, October 1999.
@TechReport{ Kindler1999_fub_trb9914, author = {Ekkart Kindler}, title = {{A classification of consistency models}}, institution = {Freie Universität Berlin, Institut für Informatik}, year = 1999, type = {Technical Report}, number = {B99-14}, month = oct, ps = {http://www.informatik.hu-berlin.de/top/download/publications/Kindler1999_fub_trb9914.ps} }Ekkart Kindler and Wil M. P. van der Aalst. Liveness, Fairness, and Recurrence. Technical Report UGA-CS-TR-99-02, University of Georgia, Department of Computer Science, Athens, USA, April 1999. Note: Also in: Information Processing Letters, 70(6), pp. 269-274, June 1999.
@TechReport{ KindlerA1999_uga_tr9902, author = {Ekkart Kindler and {Wil} {M.} {P.} {van} {der} Aalst}, title = {{Liveness, Fairness, and Recurrence}}, institution = {University of Georgia, Department of Computer Science, Athens, USA}, year = 1999, type = {Technical Report}, number = {UGA-CS-TR-99-02}, month = apr, note = {also in: Information Processing Letters, 70(6), pp. 269-274, June 1999} }Sibylle Peuker. Phased Decomposition of Distributed Algorithms. Informatik-Berichte 120, Humboldt-Universität zu Berlin, April 1999.
@TechReport{ Peuker1999_hub_tr120, author = {Sibylle Peuker}, title = {{Phased Decomposition of Distributed Algorithms}}, institution = {Humboldt-Universität zu Berlin}, year = 1999, type = {Informatik-Berichte}, number = 120, month = apr }Karsten Schmidt. Integrating Low Level Symmetries into Reachability Analysis. Informatik-Berichte 122, Humboldt-Universität zu Berlin, 1999.
@TechReport{ Schmidt1999_hub_tr122, author = {Karsten Schmidt}, title = {{Integrating Low Level Symmetries into Reachability Analysis}}, institution = {Humboldt-Universität zu Berlin}, year = 1999, type = {Informatik-Berichte}, number = 122 }
Dokumentationen
Ekkart Kindler and Michael Weber. The Petri Net Kernel - Documentation of the application interface. 2.0 edition, January 1999.
Abstract: This document is a combined tutorial and reference guide to the Petri Net Kernel version 2.0 (PNK 2.0 for short). It extends the English short version of the documentation of the PNK 1.1. Due to many request from outside Germany, we have decided not to carry on the German documentation but to provide a full English documentation from version 2.0 on. We hope that German users are not too unhappy about that. In the PNK 2.0, we have extended the interface and slightly improved the editor which is delivered with the PNK. In particular, we have extended the net type interface for defining extensions for any net element: places, transitions, and arcs. With PNK 2.0, we have reached a stable interface for application programmers. Of course, there are ideas for improving the PNK. These ideas, however, do not concern the application interface but will provide more flexible and user definable graphics - including a more appealing graphical user interface and editor functionality. We hope that you enjoy using the Petri Net Kernel and we are grateful for any feedback - positive or negative. @Manual{ KindlerW1999_pnkernel_apidoc, author = {Ekkart Kindler and Michael Weber}, title = {{The Petri Net Kernel - Documentation of the application interface}}, edition = {2.0}, month = jan, year = 1999, ps = {http://www.informatik.hu-berlin.de/top/download/publications/KindlerW1999_pnkernel_apidoc.ps}, keywords = {Petri Net Kernel}, abstract = {This document is a combined tutorial and reference guide to the Petri Net Kernel version 2.0 (PNK 2.0 for short). It extends the English short version of the documentation of the PNK 1.1. Due to many request from outside Germany, we have decided not to carry on the German documentation but to provide a full English documentation from version 2.0 on. We hope that German users are not too unhappy about that. In the PNK 2.0, we have extended the interface and slightly improved the editor which is delivered with the PNK. In particular, we have extended the net type interface for defining extensions for any net element: places, transitions, and arcs. With PNK 2.0, we have reached a stable interface for application programmers. Of course, there are ideas for improving the PNK. These ideas, however, do not concern the application interface but will provide more flexible and user definable graphics - including a more appealing graphical user interface and editor functionality. We hope that you enjoy using the Petri Net Kernel and we are grateful for any feedback - positive or negative.} }
Studien- und Diplomarbeiten
D. Runge. Algorithmen und Methoden für die Visualisierung molekularer Oberflächen und Grenzflächen. Diplomarbeit, Humboldt-Universität zu Berlin, June 1999.
@MastersThesis{ Runge1999_da, author = {D. Runge}, title = {{Algorithmen und Methoden für die Visualisierung molekularer Oberflächen und Grenzflächen}}, school = {Humboldt-Universität zu Berlin}, year = 1999, type = {Diplomarbeit}, month = jun }S. Unger. Automatisches Überprüfen von DAWN-Beweisen. Diplomarbeit, Humboldt-Universität zu Berlin, October 1999.
@MastersThesis{ Unger1999_da, author = {S. Unger}, title = {{Automatisches Überprüfen von DAWN-Beweisen}}, school = {Humboldt-Universität zu Berlin}, year = 1999, type = {Diplomarbeit}, month = oct, keywords = {DAWN} }
Theorie der Programmierung | | XHTML 1.0 | Wed Nov 5 08:30:01 2008

