Publikationen zum Fachbereich Temporale Logik

Dissertationen und Habilitationen

Adrianna Alexander. Komposition Temporallogischer Spezifikationen - Spezifikation und Verifikation von Systemen mit Temporal Logic of Distributed Actions. Dissertation, Humboldt-Universit�t zu Berlin, Mathematisch-Naturwissenschaftliche Fakult�t II, September 2005.

Abstract: This thesis introduces a new temporal logic, called Temporal Logic ofDistributed Actions, TLDA for short. TLDA is designed for compositional specification and verification of distributed systems. TLDA originates syntactically from an already established temporal logic, TLA. But TLDA, contrary to TLA and other known compositional temporal logics, is based semantically on a partial order structure, called distributed run. Compared to TLA, the use of this semantical model increases the expressiveness of TLDA. Both the system and its properties are described in one formalism: They are represented by a set of distributed runs and specified in TLDA by a temporal logic formula. Hence, the verification of a system is reduced to proving that the system specification implies the property specification. We provide a set of proof rules for this. We show that the composition of systems is specified by conjunction of the specifications of its components and, usually, the specification of the interaction between the components. Hence, the specification of a composed system can be derived from specifications of its components. Component properties are preserved in the process of composition. Thus, components can be verified separately and then be integrated into the composed system. This economises the effort for verification. Attuned for distributed runs we develop a semantical criterion for TLDA-formulas, called environmental invariance. We show that environmental invariant formulas are suited for the specification of system components. We prove that such environmental invariant formulas, due to their properties, supply a modular design of systems.

Konferenzbeitr�ge und Beitr�ge auf Workshops

Dirk Fahland, Daniel L�bke, Jan Mendling, Hajo Reijers, Barbara Weber, Matthias Weidlich, and Stefan Zugal. Declarative versus Imperative Process Modeling Languages: The Issue of Understandability. In John Krogstie, Terry Halpin, and Erik Proper, editors, Proceedings of the 14th International Conference on Exploring Modeling Methods in Systems Analysis and Design (EMMSAD'09), volume 29 of Lecture Notes in Business Information Processing, Amsterdam, The Netherlands, pages 353-366, June 2009. Springer-Verlag. Note: (to appear).

Abstract: Advantages and shortcomings of different process modeling languages are heavily debated, both in academia and industry, but little evidence is presented to support judgements. With this paper we aim to contribute to a more rigorous, theoretical discussion of the topic by drawing a link to well-established research on program comprehension. In particular, we focus on imperative and declarative techniques of modeling a process. Cognitive research has demonstrated that imperative programs deliver sequential information much better while declarative programs offer clear insight into circumstantial information. In this paper we show that in principle this argument can be transferred to respective features of process modeling languages. Our contribution is a pair of propositions that are routed in the cognitive dimensions framework. In future research, we aim to challenge these propositions by an experiment.

Dirk Fahland. Modeling and Verifying Declarative Workflows. In Dagstuhl ''zehn plus eins'', Aachen, pages 135, 2007. Verlagshaus Mainz.

Dirk Fahland. Synthesizing Petri nets from LTL specifications - An engineering approach. In Stephan Philippi and Alexander Pinl, editors, Proceedings 14.Workshop Algorithmen und Werkzeuge f�r Petrinetze (AWPN), Arbeitsbericht aus dem Fach Informatik, Nr. 25/2007, Universit�t Koblenz-Landau, D, pages 69--74, September 2007.

Abstract: In this paper we present a pattern-based approach for synthesizing truly distributed Petri nets from a class of LTL specifications. The synthesis allows for the automatic, correct generation of humanly conceivable Petri nets, thus circumventing a manual construction of nets, or the use of B�uchi automata which are not distributed and often less intuitive to understand.

Dirk Fahland. Towards Analyzing Declarative Workflows. In Jana Koehler, Marco Pistore, Amit P. Sheth, Paolo Traverso, and Martin Wirsing, editors, Autonomous and Adaptive Web Services, number 07061 of Dagstuhl Seminar Proceedings, 2007. Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany.

Abstract: Enacting tasks in a workflow cannot always follow a pre-defined process model. In application domains like disaster management workflows are partially specified and circumstances of their enactment change. There exist various approaches for formal workflow models that are effective in such situations, like declarative specifications instead of operational models for formalizing flexible workflow process. These powerful models leave a gap to existing techniques in the domain of workflow modeling, workflow analysis, and workflow management. In this paper we bridge this gap with a compositional mechanism for translating declarative workflow models to operational workflow models. The mechanism is of a general nature and we reveal its principles as we provide an exemplary definition for translating DecSerFlow models based on LTL to Petri nets. We then demonstrate its use in analyzing and refining declarative models.

Adrianna Alexander. Composition of Temporal Logic Specifications. In Jordi Cortadella and Wolfgang Reisig, editors, Applications and Theory of Petri Nets 2004, 25th International Conference (ICATPN 2004), number 3099 of Lecture Notes in Computer Science, pages 98-116, 2004. Springer-Verlag.

Abstract: The Temporal Logic of Distributed Actions (TLDA) is a new temporal logic designed for the specification and verification of distributed systems. TLDA supports a modular design of systems: Subsystems can be specified and verified separately and then be integrated into one system. The properties of the subsystems will be preserved in this process. TLDA can be syntactically viewed as an extension of TLA. We propose a different semantical model based on partial order which increases the expressiveness of the logic.

Adrianna Alexander and Wolfgang Reisig. Compositional Temporal Logic Based on Partial Order. In 11th International Symposium on Temporal Representation and Reasoning (TIME'04), pages 125-132, 2004. IEEE Computer Society.

Abstract: The Temporal Logic of Distributed Actions (TLDA) is a new temporal logic designed for the specification and verification of distributed systems. The logic supports a compositional design of systems: subsystems can be specified separately and then be integrated into one system. TLDA can be syntactically viewed as an extension of TLA. We propose a different semantical model based on partial order which increases the expressiveness of the logic.

Adrianna Alexander and Wolfgang Reisig. Logic of Involved Variables - System Specification with Temporal Logic of Distributed Actions. In Proc. of the 3rd International Conference on Application of Concurrency to System Design (ACSD'03), Guimaraes, Portugal, pages 167-176, June 2003. IEEE Computer Society.

Abstract: The Temporal Logic of Distributed Actions (TLDA) is a new temporal logic designed for the specification and verification of distributed systems. TLDA can be syntactically viewed as a slight extension of TLA. We propose a different semantical model based on partial order which evidently increases the expressiveness of the logic. Local variable updates in a system are explicitly modeled and expressed by TLDA formulas. Consequently, we can distinguish between concurrency and nondeterministic choice. All valuable features of TLA (composition is conjunction, implementation is implication) are retained. In addition, we are able to describe some important phenomena and properties typical for distributed systems.

Technische Berichte

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

Studien- und Diplomarbeiten

Niels Lohmann. Formale Fundierung und effizientere Algorithmen f�r die schrittbasierte TLDA-Interleavingsemantik. Diplomarbeit, Humboldt-Universit�t zu Berlin, September 2005.

Abstract: Die Temporal Logic of Distributed Actions (TLDA) ist eine neue temporale Logik miteiner Halbordnungssemantik und eignet sich somit zur Spezifikation verteilter Systeme. Allerdings existieren f�r TLDA noch keine Werkzeuge, die die Spezifikation und Verifikation unterst�tzen. Die Verf�gbarkeit solcher Werkzeuge tr�gt jedoch entscheidend zur Verbreitung der Logik bei. In [Loh05] wurde mit der Ausarbeitung und Implementierung einer schrittbasierten Interleavingsemantik f�r TLDA die Grundlage f�r die Entwicklung eines expliziten TLDA-Modelcheckers gelegt. Der genaue Zusammenhang zwischen der Halbordnungs- und Interleavingsemantik wurde jedoch nicht bewiesen. Au�erdem handelt es sich bei der Implementierung der Interleavingsemantik um einen Brute-Force-Prototyp, der nur f�r sehr einfach Spezifikationen in der Lage ist das Transitionssystem zu konstruieren. Die formale Fundierung sowie die Ausarbeitung effizienter Algorithmen und Datenstrukturen ist Inhalt dieser Arbeit. Anhand mehrerer Fallstudien untersuchen wir die Leistungsf�higkeit des erweiterten Prototyps und illustrieren die Beziehung zwischen der Halbordnungs- und Interleavingsemantik.

Niels Lohmann. Implementierung einer schrittbasierten Interleavingsemantik f�r die Temporal Logic of Distributed Actions (TLDA). Studienarbeit, Humboldt-Universit�t zu Berlin, June 2005.

Abstract: Die Temporal Logic of Distributed Actions (TLDA) ist eine temporale Logik mit einer Halbordnungssemantik und eignet sich somit zur Spezifikation verteilter Systeme. Allerdings gibt es noch wenig Erfahrung bei der computergest�tzten Verifikation halbordnungsbasierter Formalismen. Viele bekannte effiziente Algorithmen des expliziten Modelchecking setzen ein Transitionssystem und somit eine Interleavingsemantik voraus. In dieser Arbeit wird eine Interleavingsemantik f�r TLDA vorgeschlagen und ein Prototyp entwickelt, der f�r eine bestimmte Klasse von TLDA-Spezifikationen das Transitionssystem aufbaut. Die entwickelte Semantik soll zusammen mit dem Prototypen die Grundlage f�r die weitere Arbeit an einem Modelchecker f�r TLDA sein.

Lars Kuhtz. TLDA und Petrinetze. Studienarbeit, Humboldt-Universit�t zu Berlin, April 2004.

Peter Massuthe. Verfeinerungstechniken der Temporal Logic of Distributed Actions TLDA. Diplomarbeit, Humboldt-Universit�t zu Berlin, March 2004.

Abstract: TLDA, die Temporal Logic of Distributed Actions, ist eine neue temporale Logik zur Spezifikation verteilter Systeme. Sie basiert auf halbgeordneten Abl�ufen. Diese Logik hat noch keinen formalen Verfeinerungsbegriff. Die Entwicklung von Methoden zur Unterst�tzung der Entwicklung komplexer TLDA-Spezifikationen durch schrittweise Verfeinerung ist Inhalt der vorliegenden Arbeit. Wir unterscheiden dabei zwischen Datenverfeinerung und Transitionsverfeinerung. Die Anwendbarkeit dieser Methoden wird anhand mehrerer mittelgro�er Fallstudien gezeigt. Weiterhin besch�ftigen wir uns mit der Bewahrung von Eigenschaften durch Daten- und Transitionsverfeinerungsschritte. Diese Arbeit richtet sich vor allem an die Modellierer verteilter Systeme mit formalen Spezifikationsmethoden, insbesondere temporalen Logiken.

Peter Massuthe. Parallele Komposition in TLA. Studienarbeit, Humboldt-Universit�t zu Berlin, September 2003.

Abstract: TLA ist eine temporale Logik zur Spezifikation verteilter Systeme. Aufgrund der Stotterinvarianz von TLA-Formeln erlaubt sie eine einfache parallele Komposition von Systemen. In dieser Studienarbeit werden unterschiedliche Arten der parallelen Komposition in TLA betrachtet und hier�ber ein systematischer �berblick gegeben. Es wird eine Klassifikation der parallelen Komposition in TLA entwickelt und f�r jede Klasse ein Kompositionsschema angegeben. Dies erm�glicht eine automatische Komposition und erleichtert die Analyse.

zur�ck zur �bersicht

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