Projekt
:
Logik und Petrinetze
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