Zur Hauptnavigation Zum Inhaltsbereich Zur Suche Zum Seitenfuß


Projekt : Logik und Petrinetze

Deutsche Version. This page is available in German only. Cette page n'existe qu'en Allemand. Ésta página sólo existe en Alemán.


Dr. Berndt Farwer , ehemaliger Wissenschaftlicher Mitarbeiter

Laufzeit: seit 10/1994

Schlagworte: Kategorientheorie; Logik, lineare; Linear Logic Petri Net (LLPN); Nebenläufigkeit; Petrinetzstrukturen, dynamische; Logik, temporale; Multi-Regionen-Kalkül

Ziele: Untersucht werden Logiken, die zur Spezifikation und Analyse dynamischer Petrinetzstrukturen verwendet werden können. Besondere Beachtung findet in diesem Zusammenhang die Lineare Logik. Sie ermöglicht in ihrem multiplikativen Fragment eine besonders natürliche Modellierung von Petrinetzen, die zur Spezifikation von nebenläufigen Systemen geeignet ist. Bislang nicht für die Codierung von Petrinetzen betrachtete Konnektoren werden untersucht und es werden Einweg-Transitionen als eine Mögichkeit der dynamischen Veränderung der Netzstruktur eingeführt.

Es wurden Linear Logic Petri Nets (LLPN) entwickelt, die sich als Semantik für verschiedene High-Level-Netzkonzepte eignen (u.a. auch für Objektsysteme (s. 2.21 Valk) und agentenorientierte Darstellungsweisen, (s. 2.18 Moldt)). Es werden verschiedene Fragmente der Linearen Logik als Beschriftungssprache (für Token und Guards) untersucht. Insbesondere werden Möglichkeiten zur dynamischen Veränderung der Netzstrukturen untersucht und mittels LLPNs semantisch fundiert.

Als Lösungsmöglichkeit eines Problems bei der Beschreibung von dynamischen Petrinetzmodifikationen wurden Multi-Regionen-Kalküle eingeführt. Diese linearlogischen Kalküle spalten die Formeln in mehrere Regionen (z.B. für die Markierung, die Struktur, Zwischenergebnisse, etc.) auf, womit eine Anomalie, die bei linearlogischen Standardkalkülen auftritt, verhindert wird.

Zusammenhänge zwischen nichdeterministischen Transitionen und Objekt-Systemen werden untersucht. Anhand von bekannten Resultaten zur Linearen Logik werden Unentscheidbarkeitsresultate für die Erreichbarkeit bzgl. des Systemnetzprozesses von Objektsystemen erzielt und auf LLPNs übertragen.

Weiterhin werden Unterschiede zwischen Wert- und Referenzsemantiken von Petrinetzformalismen untersucht sowie unterschiedliche Objekt-Petrinetz-Formalismen diesbezüglich verglichen. Insbesondere der Formalismus der "Nested Petri Nets" von I. Lomazova wird untersucht. Er ermöglicht mehrstufige Modellierung von Systemen, wofür eine geeignete Darstellung als LLPN bzw. als linearlogische Formel gesucht wird.

Es wurden weitere Fortschritte bei der Modellierung von Petrinetzen erzielt, die ihre Sruktur dynamisch verändern können, bzw. deren Struktur durch ein auf höherer Ebene agierendes Systemnetz modifiziert wird. Weiterhin wurden Zusammenhänge zwischen Objekt-Petrinetzen und Daten-Fluss-Netze (DFN) untersucht.

Publikationen:

2004

Berndt Farwer and M. Leuschel.
Model checking object Petri nets in Maude and Prolog.
Technical Report FBI-HH-B-258/04, Fachbereich Informatik, Universität Hamburg, 2004.

Berndt Farwer and M. Leuschel.
Model checking object Petri nets in Prolog.
In Proceedings of the 6th ACM SIGPLAN international conference on Principles and practice of declarative programming, pages 20-31. ACM Press, 2004.

Berndt Farwer and Daniel Schradick.
Execution and analysis of P/T nets and object Petri nets with B.
In G. Lindemann, H.-D. Burkhard, L. Czaja, A. Skowron, H. Schlingloff, and Z. Suraj, editors, Concurrency, Specification, and Programming CS&P'2004, volume 1, Informatik-Bericht Nr. 170, pages 28-39. Humboldt Universität, Berlin, 2004.

2003

Berndt Farwer.
A logic of enablement.
In Girault and Valk (Hrsg.), Petri Nets for Systems Engineering: A Guide to Modelling, Verification, and Applications, section 16.3, pages 361-370.

2002

Berndt Farwer.
Dynamic modification of object Petri nets. an application to modelling protocols with fork-join structures.
Fundamenta Informaticae, 51(1,2):91-101, 2002.

Berndt Farwer and K. Misra.
Hierarchical object systems.
In H.-D. Burkhard, L. Czaja, G. Lindemann, A. Skowron, and P.Starke, editors, Concurrency, Specification, and Programming CS&P'2002 (Volume 1), pages 143-163 (16 pages). Humboldt-Universität zu Berlin, Informatik-Berichte 161, 2002.

Berndt Farwer.
Dynamic modification of object Petri nets. an application to modelling protocols with fork-join structures.
Fundamenta Informaticae, 51(1,2):91-101, 2002.

2001

Berndt Farwer.
Modelling protocols by object-based Petri nets.
In L. Czaja, editor, Concurrency Specification and Programming (CSP'01), Proceedings, pages 87-96. University of Warsaw, 2001.

Berndt Farwer.
Comparing concepts of object Petri net formalisms.
Fundamenta Informaticae, 47(3-4):247-258, 2001.

Berndt Farwer and I. Lomazova.
A systematic approach towards object-based Petri net formalisms.
In D. Bjorner and A. Zamulin, editors, Perspectives of System Informatics, Proceedings of the 4th International Andrei Ershov Memorial Conference, PSI 2001, Akademgorodok, Novosibirsk, volume 2244 of Lecture Notes in Computer Science, pages 255-267. Springer-Verlag, 2001.

Berndt Farwer and I. Lomazova.
A systematic approach towards object-based Petri net formalisms.
In Proceedings of Andrei Ershov Fourth International Conference Perspectives Of System Informatics, pages 141-146, July 2001.

2000

Berndt Farwer.
A multi-region linear logic based calculus for dynamic Petri net structures.
Fundamenta Informaticae, 43(1-4):61-79, 2000.

Berndt Farwer.
Relating formalisms for non-object-oriented object Petri nets.
In P. Starke L. Czaja, editor, Concurrency, Specification, and Programming (CS&P'2000). Proceedings. Volume 1, pages 53-64. Humboldt-Universität, Berlin, 2000.

Berndt Farwer.
Linear Logic Based Calculi for Object Petri Nets.
Logos Verlag, ISBN 3-89722-539-5, Berlin, Vogt-Kölln Str. 30, D-22527 Hamburg, 2000.

1999

Berndt Farwer.
Linear Logic Based Calculi for Object Petri Nets.
PhD thesis, Universität Hamburg, Fachbereich Informatik, Vogt-Kölln Str. 30, D-22527 Hamburg, 1999.

Berndt Farwer.
A linear logic view of object Petri nets.
Fundamenta Informaticae, 37(3):225-246, 1999.

Berndt Farwer.
Towards a linear logic based calculus for structural modifications of Petri nets.
In H.-D. Burkhard, L. Czaja, H.-S. Nguyen, and P. Starke, editors, Concurrency Specification and Programming (CS&P'99), Proceedings, pages 47-58. University of Warsaw, 1999.

1998

Berndt Farwer.
A linear logic view of object systems.
In H.-D. Burkhard, L. Czaja, and P. Starke, editors, Concurrency Specification and Programming (CS&P'98), Proceedings, pages 76-87. Humboldt-Universität, Berlin, 1998.

Berndt Farwer.
Towards linear logic Petri nets - From P/T-nets to object systems.
Technical report, FBI-HH-B-211/98, Fachbereich Informatik, Universität Hamburg, 1998.

Berndt Farwer.
Linear logic and Petri nets.
Lecture Notes of the MATCH summer school 1998. System Engineering: A Petri Net Based Approach to Modelling, Verification and Implementation, 1998.

Berndt Farwer.
A logic of enablement.
Lecture Notes of the MATCH summer school 1998. System Engineering: A Petri Net Based Approach to Modelling, Verification and Implementation, 1998.

Letzte Änderung: 17:40 19.05.2011
Impressum