• Karsten Wolf
• Kathrin Kaschner
• Niels Lohmann
• Olivia Oanea
• Daniela Weinberg
• Harro Wimmel

• 2010
• 2009
• 2008
• 2007
• 2006
• 2005
• 2004
• 2003
• 2002
• 2001
• 2000
• 1999
• 1998
• 1997
• 1996
• 1995
• 1994
• 1993
• 1991

2010

Zeitschriftenartikel / Journal Articles

Wil M. P. van der Aalst, Niels Lohmann, Peter Massuthe, Christian Stahl, and Karsten Wolf. Multiparty Contracts: Agreeing and Implementing Interorganizational Processes. Comput. J., 53(1):90-106, January 2010. [PDF] [DOI]

Abstract. To implement an interorganizational process between different enterprizes, one needs to agree on the ``rules of engagement''. These can be specified in terms of a contract that describes the overall intended process and the duties of all parties involved. We propose to use such a process-oriented contract which can be seen as the composition of the public views of all participating parties. Based on this contract each party may locally implement its part of the contract such that the implementation (the private view) agrees on the contract. In this paper, we propose a formal notion for such process-oriented contracts and give a criterion for accordance between a private view and its public view. The public view of a party can be substituted by a private view if and only if the private view accords with the public view. Using the notion of accordance the overall implemented process is guaranteed to be deadlock-free and it is always possible to terminate properly. In addition, we present a technique for automatically checking our accordance criterion. A case study illustrates how our proposed approach can be used in practice.

@article{AalstLMSW_2010_compj,
Abstract = {To implement an interorganizational process between different enterprizes, one needs to agree on the ``rules of engagement''. These can be specified in terms of a contract that describes the overall intended process and the duties of all parties involved. We propose to use such a process-oriented contract which can be seen as the composition of the public views of all participating parties. Based on this contract each party may locally implement its part of the contract such that the implementation (the private view) agrees on the contract. In this paper, we propose a formal notion for such process-oriented contracts and give a criterion for accordance between a private view and its public view. The public view of a party can be substituted by a private view if and only if the private view accords with the public view. Using the notion of accordance the overall implemented process is guaranteed to be deadlock-free and it is always possible to terminate properly. In addition, we present a technique for automatically checking our accordance criterion. A case study illustrates how our proposed approach can be used in practice.},
Author = {{Wil} {M.} {P.} {van} {der} Aalst and Niels Lohmann and Peter Massuthe and Christian Stahl and Karsten Wolf},
Journal = {Comput. J.},
Month = jan,
Number = {1},
Pages = {90-106},
Title = {Multiparty Contracts: Agreeing and Implementing Interorganizational Processes},
Volume = {53},
Year = {2010},
}

Niels Lohmann and Karsten Wolf. Compact Representations and Efficient Algorithms for Operating Guidelines. Fundam. Inform., 2010. (Accepted for publication in January 2010).

@article{LohmannW_2010_fi,
Author = {Niels Lohmann and Karsten Wolf},
Journal = {Fundam. Inform.},
Note = {(Accepted for publication in January 2010)},
Title = {Compact Representations and Efficient Algorithms for Operating Guidelines},
Year = {2010},
}

Konferenzbeiträge / Conference Papers

Niels Lohmann. Communication Models for Services. In Christian Gierds and Jan Sürmeli, editors, Proceedings of the 2nd Central-European Workshop on Services and their Composition, ZEUS 2010, Berlin, Germany, February 26-27, 2010, volume 563 of CEUR Workshop Proceedings, March 2010. CEUR-WS.org.

@inproceedings{Lohmann_2010_zeus,
Author = {Niels Lohmann},
Booktitle = {Proceedings of the 2nd Central-European Workshop on Services and their Composition, ZEUS 2010, Berlin, Germany, February 26-27, 2010},
Editor = {Christian Gierds and Jan S{\"u}rmeli},
Month = mar,
Publisher = {CEUR-WS.org},
Series = {CEUR Workshop Proceedings},
Title = {Communication Models for Services},
Volume = {563},
Year = {2010}
}

Niels Lohmann and Daniela Weinberg. Wendy: A tool to synthesize partners for services. In Johan Lilius and Wojciech Penczek, editors, 31st International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, PETRI NETS 2010, Braga, Portugal, June 21-25, 2010, Proceedings, Lecture Notes in Computer Science, June 2010. Springer-Verlag.

@inproceedings{LohmannW_2010_atpn,
Author = {Niels Lohmann and Daniela Weinberg},
Booktitle = {31st International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, PETRI NETS 2010, Braga, Portugal, June 21-25, 2010, Proceedings},
Editor = {Johan Lilius and Wojciech Penczek},
Month = jun,
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Wendy: A tool to synthesize partners for services},
Year = {2010}
}

Olivia Oanea, Harro Wimmel, and Karsten Wolf. New Algorithms for Deciding the Siphon-Trap Property. In Johan Lilius and Wojciech Penczek, editors, 31st International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, PETRI NETS 2010, Braga, Portugal, June 21-25, 2010, Proceedings, Lecture Notes in Computer Science, June 2010. Springer-Verlag.

@inproceedings{OaneaWW_2010_atpn,
Author = {Olivia Oanea and Harro Wimmel and Karsten Wolf},
Booktitle = {31st International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, PETRI NETS 2010, Braga, Portugal, June 21-25, 2010, Proceedings},
Editor = {Johan Lilius and Wojciech Penczek},
Month = jun,
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {New Algorithms for Deciding the Siphon-Trap Property},
Year = {2010}
}

Technische Berichte / Technical Reports

Wil M. P. van der Aalst, Niels Lohmann, Marcello La Rosa, and Jingxin Xu. Correctness Ensuring Process Configuration: An Approach Based on Partner Synthesis (extended version). BPM Center Report BPM-10-02, BPMcenter.org, March 2010. [PDF]

Abstract. A configurable process model describes a family of similar process models in a given domain. Such a model can be configured to obtain a specific process model that is subsequently used to handle individual cases, for instance, to process customer orders. Process configuration is notoriously difficult as there may be all kinds of interdependencies between configuration decisions. In fact, an incorrect configuration may lead to behavioral issues such as deadlocks and livelocks. To address this problem, we present a new verification approach inspired by the "operating guidelines" used for partner synthesis. We view the configuration process as an external service, and compute a characterization of all such services which meet particular requirements via the notion of configuration guideline. As a result, we can characterize all feasible configurations (i. e., configurations without behavioral problems) at design time, instead of repeatedly checking each individual configuration while configuring a process model.

@techreport{AalstLLX_2010_tr,
Abstract = {A configurable process model describes a family of similar process models in a given domain. Such a model can be configured to obtain a specific process model that is subsequently used to handle individual cases, for instance, to process customer orders. Process configuration is notoriously difficult as there may be all kinds of interdependencies between configuration decisions. In fact, an incorrect configuration may lead to behavioral issues such as deadlocks and livelocks. To address this problem, we present a new verification approach inspired by the "operating guidelines" used for partner synthesis. We view the configuration process as an external service, and compute a characterization of all such services which meet particular requirements via the notion of configuration guideline. As a result, we can characterize all feasible configurations (i. e., configurations without behavioral problems) at design time, instead of repeatedly checking each individual configuration while configuring a process model.},
Author = {{Wil} {M.} {P.} {van} {der} {Aalst} and Niels Lohmann and Marcello {La Rosa} and Jingxin Xu},
Institution = {BPMcenter.org},
Month = mar,
Number = {BPM-10-02},
Title = {Correctness Ensuring Process Configuration: An Approach Based on Partner Synthesis (extended version)},
Type = {BPM Center Report},
Year = {2010}
}

2009

Bücher und Tagungsbände / Books and Proceedings

Roberto Bruni and Karsten Wolf, editors. Web Services and Formal Methods, 5th International Workshop, WS-FM 2008, Milan, Italy, September 4-5, 2008, Revised Selected Papers, volume 5387 of Lecture Notes in Computer Science, April 2009. Springer-Verlag. [DOI]

@proceedings{BruniW_2008_wsfm,
Editor = {Roberto Bruni and Karsten Wolf},
Month = apr,
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Web Services and Formal Methods, 5th International Workshop, WS-FM 2008, Milan, Italy, September 4-5, 2008, Revised Selected Papers},
Volume = {5387},
Year = {2009},
}

Giuliana Franceschinis and Karsten Wolf, editors. Applications and Theory of Petri Nets, 30th International Conference, PETRI NETS 2009, Paris, France, June 22-26, 2009. Proceedings, volume 5606 of Lecture Notes in Computer Science, June 2009. Springer-Verlag. [DOI]

@proceedings{FranceschinisW_2009_icatpn,
Editor = {Giuliana Franceschinis and Karsten Wolf},
Month = jun,
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Applications and Theory of Petri Nets, 30th International Conference, PETRI NETS 2009, Paris, France, June 22-26, 2009. Proceedings},
Volume = {5606},
Year = {2009},
}

Oliver Kopp and Niels Lohmann, editors. Proceedings of the 1st Central-European Workshop on Services and their Composition, ZEUS 2009, Stuttgart, Germany, March 2-3, 2009, volume 438 of CEUR Workshop Proceedings, March 2009. CEUR-WS.org. [WWW] [PDF]

@proceedings{KoppL_2009_zeus,
Booktitle = {Services und ihre Komposition},
Editor = {Oliver Kopp and Niels Lohmann},
Month = mar,
Publisher = {CEUR-WS.org},
Series = {CEUR Workshop Proceedings},
Title = {Proceedings of the 1st Central-European Workshop on Services and their Composition, ZEUS 2009, Stuttgart, Germany, March 2-3, 2009},
Volume = {438},
Year = {2009},
}

Zeitschriftenartikel / Journal Articles

Niels Lohmann, H.M.W. Verbeek, and Remco Dijkman. Petri Net Transformations for Business Processes - A Survey. LNCS ToPNoC, II(5460):46-63, March 2009. Special Issue on Concurrency in Process-Aware Information Systems. [PDF] [DOI]

Abstract. In Process-Aware Information Systems, business processes are often modeled in an explicit way. Roughly spoken, the available business process modeling languages can be divided into two groups. Languages from the first group are preferred by academic people but shunned by business people, and include Petri nets and process algebras. These academic languages have a proper formal semantics, which allows the corresponding academic models to be verified in a formal way. Languages from the second group are preferred by business people but disliked by academic people, and include BPEL, BPMN, and EPCs. These business languages often lack any proper semantics, which often leads to debates on how to interpret certain business models. Nevertheless, business models are used in practice, whereas academic models are hardly used. To be able to use, for example, the abundance of Petri net verification techniques on business models, we need to be able to transform these models to Petri nets. In this paper, we investigate a number of Petri net transformations that already exist. For every transformation, we investigate the transformation itself, the constructs in the business models that are problematic for the transformation and the main applications for the transformation.

@article{LohmannVD_2008_topnoc,
Abstract = {In Process-Aware Information Systems, business processes are often modeled in an explicit way. Roughly spoken, the available business process modeling languages can be divided into two groups. Languages from the first group are preferred by academic people but shunned by business people, and include Petri nets and process algebras. These academic languages have a proper formal semantics, which allows the corresponding academic models to be verified in a formal way. Languages from the second group are preferred by business people but disliked by academic people, and include BPEL, BPMN, and EPCs. These business languages often lack any proper semantics, which often leads to debates on how to interpret certain business models. Nevertheless, business models are used in practice, whereas academic models are hardly used. To be able to use, for example, the abundance of Petri net verification techniques on business models, we need to be able to transform these models to Petri nets. In this paper, we investigate a number of Petri net transformations that already exist. For every transformation, we investigate the transformation itself, the constructs in the business models that are problematic for the transformation and the main applications for the transformation.},
Author = {Niels Lohmann and H.M.W. Verbeek and Remco Dijkman},
Journal = {LNCS ToPNoC},
Month = mar,
Note = {Special Issue on Concurrency in Process-Aware Information Systems},
Number = {5460},
Pages = {46-63},
Title = {{Petri} Net Transformations for Business Processes - A Survey},
Volume = {II},
Year = {2009},
}

Niels Lohmann, H.M.W. Verbeek, Chun Ouyang, and Christian Stahl. Comparing and Evaluating Petri Net Semantics for BPEL. Int. J. Business Process Integration and Management, 4(1):60-73, 2009. [PDF] [DOI]

Abstract. We compare two Petri net semantics for the Web Services Business Process Execution Language (BPEL). The comparison reveals different modelling decisions. These decisions together with their consequences are discussed. We also give an overview of the different properties that can be verified on the resulting models. A case study helps to evaluate the corresponding compilers which transform a BPEL process into a Petri net model.

@article{LohmannVOSA_2009_ijbpim,
Abstract = {We compare two Petri net semantics for the Web Services Business Process Execution Language (BPEL). The comparison reveals different modelling decisions. These decisions together with their consequences are discussed. We also give an overview of the different properties that can be verified on the resulting models. A case study helps to evaluate the corresponding compilers which transform a BPEL process into a Petri net model.},
Author = {Niels Lohmann and H.M.W. Verbeek and Chun Ouyang and Christian Stahl},
Journal = {Int. J. Business Process Integration and Management},
Number = {1},
Pages = {60-73},
Title = {Comparing and Evaluating {Petri} Net Semantics for {BPEL}},
Volume = {4},
Year = {2009},
}

Christian Stahl and Karsten Wolf. Deciding Service Composition and Substitutability Using Extended Operating Guidelines. Data Knowl. Eng., 68(9):819-833, September 2009. [PDF] [DOI]

Abstract. We study the correct interaction between services using the following notion for correctness: there is no deadlock in the interaction of the services, and a given set of activities is covered, that is, such an activity can be executed in at least one scenario. The second condition has not been studied before. An operating guideline of a service P is an operational characterization of all deadlock-free interacting partners of P. In this paper, we present an extension of the concept of an operating guideline to characterize all correctly interacting partners of a service P. This extension can be used for answering at least the following two questions. First, given a service R, does R interact correctly with P? Second, given a service P', can P be substituted by P', that is, is every correctly interacting partner of P a correctly interacting partner of P', too?

@article{StahlW_2008_dke,
Abstract = {We study the correct interaction between services using the following notion for correctness: there is no deadlock in the interaction of the services, and a given set of activities is covered, that is, such an activity can be executed in at least one scenario. The second condition has not been studied before. An operating guideline of a service P is an operational characterization of all deadlock-free interacting partners of P. In this paper, we present an extension of the concept of an operating guideline to characterize all correctly interacting partners of a service P. This extension can be used for answering at least the following two questions. First, given a service R, does R interact correctly with P? Second, given a service P', can P be substituted by P', that is, is every correctly interacting partner of P a correctly interacting partner of P', too?},
Author = {Christian Stahl and Karsten Wolf},
Journal = {Data Knowl. Eng.},
Month = sep,
Number = {9},
Pages = {819-833},
Title = {Deciding Service Composition and Substitutability Using Extended Operating Guidelines},
Volume = {68},
Year = 2009,
}

Karsten Wolf. Does my service have partners?. LNCS ToPNoC, 5460(II):152-171, March 2009. Special Issue on Concurrency in Process-Aware Information Systems. [PDF] [DOI]

Abstract. Controllability for service models is a similar criterion as soundness for workflow models: it establishes a necessary condition for correct behavior of a given service model. Technically, controllability is the problem to decide, for a given service, whether it can interact correctly with at least one other service. Parameters to the problem are the established correctness criterion (e.g. deadlock freedom, livelock freedom, quasi-liveness), the shape of partners (centralized partners versus independently acting partners), or the shape of communication (asynchronous versus synchronous). In this article, we survey and partly extend various recent results concern- ing the verification of controllability for Petri net based service models. Significant extensions include the study of livelock freedom as correctness criterion as well as the new results on autonomous multi-port controllability.

@article{Wolf_2008_topnoc,
Abstract = {Controllability for service models is a similar criterion as soundness for workflow models: it establishes a necessary condition for correct behavior of a given service model. Technically, controllability is the problem to decide, for a given service, whether it can interact correctly with at least one other service. Parameters to the problem are the established correctness criterion (e.g. deadlock freedom, livelock freedom, quasi-liveness), the shape of partners (centralized partners versus independently acting partners), or the shape of communication (asynchronous versus synchronous). 

In this article, we survey and partly extend various recent results concern- ing the verification of controllability for Petri net based service models. Significant extensions include the study of livelock freedom as correctness criterion as well as the new results on autonomous multi-port controllability.},
Author = {Karsten Wolf},
Journal = {LNCS ToPNoC},
Month = mar,
Note = {Special Issue on Concurrency in Process-Aware Information Systems},
Number = {II},
Pages = {152-171},
Title = {Does my service have partners?},
Volume = {5460},
Year = {2009},
}

Konferenzbeiträge / Conference Papers

Wil M. P. van der Aalst, Arjan J. Mooij, Christian Stahl, and Karsten Wolf. Service Interaction: Patterns, Formalization, and Analysis. In Marco Bernardo, Luca Padovani, and Gianluigi Zavattaro, editors, Formal Methods for Web Services, 9th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2009, Bertinoro, Italy, June 1-6, 2009, Advanced Lectures, volume 5569 of Lecture Notes in Computer Science, pages 42-88, April 2009. Springer-Verlag. [PDF] [DOI]

Abstract. As systems become more service oriented and processes increasingly cross organizational boundaries, interaction becomes more important. New technologies support the development of such systems. However, the paradigm shift towards service orientation, requires a fundamentally different way of looking at processes. This survey aims to provide some foundational notions related to service interaction. A set of service interaction patterns is given to illustrate the challenges in this domain. Moreover, key results are given for three of these challenges: (1) How to expose a service?, (2) How to replace and refine services?, and (3) How to generate service adapters? These challenges will be addressed in a Petri net setting. However, the results extend to other languages used in this domain.

@inproceedings{AalstMSW_2009_sfm,
Abstract = {As systems become more service oriented and processes increasingly cross organizational boundaries, interaction becomes more important. New technologies support the development of such systems. However, the paradigm shift towards service orientation, requires a fundamentally different way of looking at processes. This survey aims to provide some foundational notions related to service interaction. A set of service interaction patterns is given to illustrate the challenges in this domain. Moreover, key results are given for three of these challenges: (1) How to expose a service?, (2) How to replace and refine services?, and (3) How to generate service adapters? These challenges will be addressed in a Petri net setting. However, the results extend to other languages used in this domain.},
Author = {{Wil} {M.} {P.} {van} {der} Aalst and Arjan J. Mooij and Christian Stahl and Karsten Wolf},
Booktitle = {Formal Methods for Web Services, 9th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2009, Bertinoro, Italy, June 1-6, 2009, Advanced Lectures},
Editor = {Marco Bernardo and Luca Padovani and Gianluigi Zavattaro},
Month = apr,
Pages = {42-88},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Service Interaction: Patterns, Formalization, and Analysis},
Volume = {5569},
Year = 2009,
}

Ahmed Awad, Gero Decker, and Niels Lohmann. Diagnosing and Repairing Data Anomalies in Process Models. In Hajo Reijers, Selma Limam Mansar, and Michael Rosemann, editors, Business Process Design (BPD 2009), 5th International Workshop, Proceedings, Lecture Notes in Business Information Processing, September 2009. Springer-Verlag. [PDF]

Abstract. When using process models for automation, correctness of the models is a key requirement. While many approaches concentrate on control flow verification only, correct data flow modeling is of similar importance. This paper introduces an approach for detecting and repairing modeling errors that only occur in the interplay between control flow and data flow. The approach is based on Petri nets and detects anomalies in BPMN models. In addition to the diagnosis of the modeling errors, a subset of errors can also be repaired automatically.

@inproceedings{AwadDL_2009_bpd,
Abstract = {When using process models for automation, correctness of the models is a key requirement. While many approaches concentrate on control flow verification only, correct data flow modeling is of similar importance. This paper introduces an approach for detecting and repairing modeling errors that only occur in the interplay between control flow and data flow. The approach is based on Petri nets and detects anomalies in BPMN models. In addition to the diagnosis of the modeling errors, a subset of errors can also be repaired automatically.},
Author = {Ahmed Awad and Gero Decker and Niels Lohmann},
Booktitle = {Business Process Design (BPD 2009), 5th International Workshop, Proceedings},
Editor = {Hajo Reijers and Selma Limam Mansar and Michael Rosemann},
Month = sep,
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Business Information Processing},
Title = {Diagnosing and Repairing Data Anomalies in Process Models},
Year = {2009}
}

Dirk Fahland, Cédric Favre, Barbara Jobstmann, Jana Koehler, Niels Lohmann, Hagen Völzer, and Karsten Wolf. Instantaneous Soundness Checking of Industrial Business Process Models. In Umeshwar Dayal, Johann Eder, Jana Koehler, and Hajo A. Reijers, editors, Business Process Management, 7th International Conference, BPM 2009, Ulm, Germany, September 8-10, 2009, Proceedings, volume 5701 of Lecture Notes in Computer Science, pages 278-293, September 2009. Springer-Verlag. [PDF] [DOI]

Abstract. We report on a case study on control-flow analysis of business process models. We checked 735 industrial business process models from financial services, telecommunications and other domains. We checked these models for soundness (absence of deadlock and lack of synchronization) using three different approaches: the business process verification tool Woflan, the Petri net model checker LoLA and a recently developed technique based on SESE decomposition. We evaluate the various techniques utilized by these approaches with respect to their ability of accelerating the check. Our results show that an average industrial business process model can be checked in a few milliseconds, which enables tight integration of modeling with control-flow analysis. We also briefly compare the diagnostic information delivered by the different approaches.

@inproceedings{FahlandWJKLVW_2009_bpm,
Abstract = {We report on a case study on control-flow analysis of business process models. We checked 735 industrial business process models from financial services, telecommunications and other domains. We checked these models for soundness (absence of deadlock and lack of synchronization) using three different approaches: the business process verification tool Woflan, the Petri net model checker LoLA and a recently developed technique based on SESE decomposition. We evaluate the various techniques utilized by these approaches with respect to their ability of accelerating the check. Our results show that an average industrial business process model can be checked in a few milliseconds, which enables tight integration of modeling with control-flow analysis. We also briefly compare the diagnostic information delivered by the different approaches.},
Author = {Dirk Fahland and C{\'e}dric Favre and Barbara Jobstmann and Jana Koehler and Niels Lohmann and Hagen V{\"o}lzer and Karsten Wolf},
Booktitle = {Business Process Management, 7th International Conference, BPM 2009, Ulm, Germany, September 8-10, 2009, Proceedings},
Editor = {Umeshwar Dayal and Johann Eder and Jana Koehler and Hajo A. Reijers},
Month = sep,
Pages = {278-293},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Instantaneous Soundness Checking of Industrial Business Process Models},
Volume = {5701},
Year = {2009},
}

Kathrin Kaschner and Niels Lohmann. Automatic Test Case Generation for Interacting Services. In George Feuerlicht and Winfried Lamersdorf, editors, Service-Oriented Computing - ICSOC 2008 Workshops, ICSOC 2008 International Workshops, Sydney, Australia, December 1st, 2008, Revised Selected Papers, volume 5472 of Lecture Notes in Computer Science, pages 66-78, April 2009. Springer-Verlag. [PDF] [DOI]

Abstract. Service-oriented architectures propose loosely coupled interacting services as building blocks for distributed applications. Since distributed services differ from traditional monolithic software systems, novel testing methods are required. Based on the specification of a service, we introduce an approach to automatically generate test cases for black-box testing to check for conformance between the specification and the implementation of a service whose internal behavior might be confidential. Due to the interacting nature of services this is a nontrivial task.

@inproceedings{KaschnerL_2008_wesoa,
Abstract = {Service-oriented architectures propose loosely coupled interacting services as building blocks for distributed applications. Since distributed services differ from traditional monolithic software systems, novel testing methods are required. Based on the specification of a service, we introduce an approach to automatically generate test cases for black-box testing to check for conformance between the specification and the implementation of a service whose internal behavior might be confidential. Due to the interacting nature of services this is a nontrivial task.},
Author = {Kathrin Kaschner and Niels Lohmann},
Booktitle = {Service-Oriented Computing - ICSOC 2008 Workshops, ICSOC 2008 International Workshops, Sydney, Australia, December 1st, 2008, Revised Selected Papers},
Editor = {George Feuerlicht and Winfried Lamersdorf},
Month = apr,
Pages = {66-78},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Automatic Test Case Generation for Interacting Services},
Volume = {5472},
Year = {2009},
}

Kathrin Kaschner and Niels Lohmann. Does my service have unspecified behavior?. In Oliver Kopp and Niels Lohmann, editors, Proceedings of the 1st Central-European Workshop on Services and their Composition, ZEUS 2009, Stuttgart, Germany, March 2-3, 2009, volume 438 of CEUR Workshop Proceedings, pages 22-28, March 2009. CEUR-WS.org. [PDF]

Abstract. Services are loosely coupled interacting software components. Since a service is not executed in isolation, but in composition with other services, its implemented behavior must not differ from its specification. In this paper, we propose an approach to generate test cases which can be used to detect unspecified behavior in an implemented service. Due to the interacting nature of services this is a nontrivial task.

@inproceedings{KaschnerL_2009_zeus,
Abstract = {Services are loosely coupled interacting software components. Since a service is not executed in isolation, but in composition with other services, its implemented behavior must not differ from its specification. In this paper, we propose an approach to generate test cases which can be used to detect unspecified behavior in an implemented service. Due to the interacting nature of services this is a nontrivial task.},
Author = {Kathrin Kaschner and Niels Lohmann},
Booktitle = {Proceedings of the 1st Central-European Workshop on Services and their Composition, ZEUS 2009, Stuttgart, Germany, March 2-3, 2009},
Editor = {Oliver Kopp and Niels Lohmann},
Month = mar,
Pages = {22-28},
Publisher = {CEUR-WS.org},
Series = {CEUR Workshop Proceedings},
Title = {Does my service have unspecified behavior?},
Volume = {438},
Year = {2009}
}

Kathrin Kaschner and Karsten Wolf. Set Algebra for Service Behavior: Applications and Constructions. In Umeshwar Dayal, Johann Eder, Jana Koehler, and Hajo Reijers, editors, Business Process Management, 7th International Conference, BPM 2009, Ulm, Germany, September 8-10, 2009, Proceedings, volume 5701 of Lecture Notes in Computer Science, pages 193-210, September 2009. Springer-Verlag. [PDF] [DOI]

Abstract. Compatibility of behavior, i.e. the correct ordering of messages, is one of the core aspects for the interaction between services as parts of an inter-organizational business process. In previous work, we proposed formal representations for service behavior (including Petri nets and service automata) and finite representations of sets thereof (operating guidelines). In this article, we show how the basic set operations union, intersection, and complement, as well as membership and emptiness tests, can be implemented on finite representations of (typically infinite) sets of services. We motivate the operations by three examples of applications -- service substitution, selection of behavior, and navigation in a behavioral registry.

@inproceedings{KaschnerW_2009_bpm,
Abstract = {Compatibility of behavior, i.e. the correct ordering of messages, is one of the core aspects for the interaction between services as parts of an inter-organizational business process. In previous work, we proposed formal representations for service behavior (including Petri nets and service automata) and finite representations of sets thereof (operating guidelines). 

In this article, we show how the basic set operations union, intersection, and complement, as well as membership and emptiness tests, can be implemented on finite representations of (typically infinite) sets of services. We motivate the operations by three examples of applications -- service substitution, selection of behavior, and navigation in a behavioral registry.},
Author = {Kathrin Kaschner and Karsten Wolf},
Booktitle = {Business Process Management, 7th International Conference, BPM 2009, Ulm, Germany, September 8-10, 2009, Proceedings},
Editor = {Umeshwar Dayal and Johann Eder and Jana Koehler and Hajo Reijers},
Month = sep,
Pages = {193-210},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Set Algebra for Service Behavior: Applications and Constructions},
Volume = {5701},
Year = {2009},
}

Nannette Liske, Niels Lohmann, Christian Stahl, and Karsten Wolf. Another Approach to Service Instance Migration. In Luciano Baresi, Chi-Hung Chi, and Jun Suzuki, editors, Service-Oriented Computing - ICSOC 2009, 7th International Conference, Stockholm, Sweden, November 24-27, 2009. Proceedings, volume 5900 of Lecture Notes in Computer Science, pages 607-621, November 2009. Springer-Verlag. [PDF] [DOI]

Abstract. Services change over time, be it for internal improvements, be it for external requirements such as new legal regulations. For long running services, it may even be necessary to change a service while instances are actually running and interacting with other services. This problem is referred to as instance migration. We present a novel approach to the behavioral (service protocol) aspects of instance migration. We apply techniques for finitely characterizing the set of all correctly interacting partners to a given service. The approach assures that migration does not introduce behavioral problems with any running partner of the original service. Our technique scales up to services with thousands of states, including models of real WS-BPEL processes.

@inproceedings{LiskeLSW_2009_icsoc,
Abstract = {Services change over time, be it for internal improvements, be it for external requirements such as new legal regulations. For long running services, it may even be necessary to change a service while instances are actually running and interacting with other services. This problem is referred to as instance migration. We present a novel approach to the behavioral (service protocol) aspects of instance migration. We apply techniques for finitely characterizing the set of all correctly interacting partners to a given service. The approach assures that migration does not introduce behavioral problems with any running partner of the original service. Our technique scales up to services with thousands of states, including models of real WS-BPEL processes. },
Author = {Nannette Liske and Niels Lohmann and Christian Stahl and Karsten Wolf},
Booktitle = {Service-Oriented Computing - ICSOC 2009, 7th International Conference, Stockholm, Sweden, November 24-27, 2009. Proceedings},
Editor = {Luciano Baresi and Chi-Hung Chi and Jun Suzuki},
Month = nov,
Pages = {607-621},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Another Approach to Service Instance Migration},
Volume = {5900},
Year = {2009},
}

Niels Lohmann. Why does my service have no partners?. In Roberto Bruni and Karsten Wolf, editors, Web Services and Formal Methods, 5th International Workshop, WS-FM 2008, Milan, Italy, September 4-5, 2008, Revised Selected Papers, volume 5387 of Lecture Notes in Computer Science, pages 191-206, April 2009. Springer-Verlag. [PDF] [DOI]

Abstract. Controllability is a fundamental correctness criterion for interacting service models. A service model is controllable if there exists a partner service such that their composition is free of deadlocks and livelocks. Whereas controllability can be automatically decided, the existing decision algorithm gives no information about the reasons of why a service model is uncontrollable. This paper introduces a diagnosis framework to find these reasons which can help to fix uncontrollable service models.

@inproceedings{Lohmann_2008_wsfm,
Abstract = {Controllability is a fundamental correctness criterion for interacting service models. A service model is controllable if there exists a partner service such that their composition is free of deadlocks and livelocks. Whereas controllability can be automatically decided, the existing decision algorithm gives no information about the reasons of why a service model is uncontrollable. This paper introduces a diagnosis framework to find these reasons which can help to fix uncontrollable service models.},
Author = {Niels Lohmann},
Booktitle = {Web Services and Formal Methods, 5th International Workshop, WS-FM 2008, Milan, Italy, September 4-5, 2008, Revised Selected Papers},
Editor = {Roberto Bruni and Karsten Wolf},
Month = apr,
Pages = {191-206},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Why does my service have no partners?},
Volume = {5387},
Year = {2009},
}

Niels Lohmann and Karsten Wolf. Petrifying Operating Guidelines for Services. In Ninth International Conference on Application of Concurrency to System Design (ACSD 2009), 1-3 July 2009, Augsburg, Germany, pages 80-88, June 2009. IEEE Computer Society. [PDF] [DOI]

Abstract. Operating guidelines characterize correct interaction (e.g. deadlock freedom) with a service. They can be stored in a service registry. So far, they have been represented as an annotated transition system. For the sake of saving space in the registry, we want to translate operating guidelines into Petri nets. To make this possible, we carefully investigate regularities in the annotations.

@inproceedings{LohmannW_2009_acsd,
Abstract = {Operating guidelines characterize correct interaction (e.g. deadlock freedom) with a service. They can be stored in a service registry. So far, they have been represented as an annotated transition system. 

For the sake of saving space in the registry, we want to translate operating guidelines into Petri nets. To make this possible, we carefully investigate regularities in the annotations.},
Author = {Niels Lohmann and Karsten Wolf},
Booktitle = {Ninth International Conference on Application of Concurrency to System Design (ACSD 2009), 1-3 July 2009, Augsburg, Germany},
Month = jun,
Pages = {80-88},
Publisher = {IEEE Computer Society},
Title = {Petrifying Operating Guidelines for Services},
Year = {2009},
}

Niels Lohmann and Karsten Wolf. Realizability is Controllability. In Cosimo Laneve and Jianwen Su, editors, Web Services and Formal Methods, 6th International Workshop, WS-FM 2009, Bologna, Italy, September 4-5, 2009, Revised Selected Papers, Lecture Notes in Computer Science, September 2009. Springer-Verlag. (in press). [PDF]

Abstract. A choreography describes the interaction between services. It may be used for specification purposes, for instance serving as a contract in the design of an inter-organizational business process. Typically, not all describable interactions make sense which motivates the study of the realizability problem for a given choreography. In this paper, we show that realizability can be traced back to the problem of controllability which asks whether a service has compatible partner processes. This way of thinking makes algorithms for controllability available for reasoning about realizability. In addition, it suggests alternative definitions for realizability. We discuss several proposals for defining realizability which differ in the degree of coverage of the specified interaction.

@inproceedings{LohmannW_2009_wsfm,
Abstract = {A choreography describes the interaction between services. It may be used for specification purposes, for instance serving as a contract in the design of an inter-organizational business process. Typically, not all describable interactions make sense which motivates the study of the realizability problem for a given choreography. 

In this paper, we show that realizability can be traced back to the problem of controllability which asks whether a service has compatible partner processes. This way of thinking makes algorithms for controllability available for reasoning about realizability. In addition, it suggests alternative definitions for realizability. We discuss several proposals for defining realizability which differ in the degree of coverage of the specified interaction.},
Author = {Niels Lohmann and Karsten Wolf},
Booktitle = {Web Services and Formal Methods, 6th International Workshop, WS-FM 2009, Bologna, Italy, September 4-5, 2009, Revised Selected Papers},
Editor = {Cosimo Laneve and Jianwen Su},
Month = sep,
Note = {(in press)},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Realizability is Controllability},
Year = {2009},
}

Niels Lohmann and Karsten Wolf. Realizability is Controllability. In Oliver Kopp and Niels Lohmann, editors, Proceedings of the 1st Central-European Workshop on Services and their Composition, ZEUS 2009, Stuttgart, Germany, March 2-3, 2009, volume 438 of CEUR Workshop Proceedings, pages 61-67, March 2009. CEUR-WS.org. [PDF]

Abstract. A choreography describes the interaction between services. It may be used for specification purposes, e.g. serving as a contract in the design of an interorganizational business process. Typically, not all describable interactions make sense which motivates the study of the realizability problem for a given choreography. In this paper, we show that realizability can be traced back to the problem of controllability which asks whether a service has compatible partner processes. This way of thinking makes algorithms for controllability available for reasoning about realizability. In addition, it suggests alternative definitions for realizability. We discuss several proposals for defining realizability which differ in the degree of coverage of the specified interaction.

@inproceedings{LohmannW_2009_zeus,
Abstract = {A choreography describes the interaction between services. It may be used for specification purposes, e.g. serving as a contract in the design of an interorganizational business process. Typically, not all describable interactions make sense which motivates the study of the realizability problem for a given choreography. 

In this paper, we show that realizability can be traced back to the problem of controllability which asks whether a service has compatible partner processes. This way of thinking makes algorithms for controllability available for reasoning about realizability. In addition, it suggests alternative definitions for realizability. We discuss several proposals for defining realizability which differ in the degree of coverage of the specified interaction.},
Author = {Niels Lohmann and Karsten Wolf},
Booktitle = {Proceedings of the 1st Central-European Workshop on Services and their Composition, ZEUS 2009, Stuttgart, Germany, March 2-3, 2009},
Editor = {Oliver Kopp and Niels Lohmann},
Month = mar,
Pages = {61-67},
Publisher = {CEUR-WS.org},
Series = {CEUR Workshop Proceedings},
Title = {Realizability is Controllability},
Volume = {438},
Year = {2009}
}

Stephan Mennicke, Olivia Oanea, and Karsten Wolf. Decomposition into open nets. In Thomas Freytag and Andreas Eckleder, editors, 16th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2009, Karlsruhe, Germany, September 25, 2009, Proceedings, volume 501 of CEUR Workshop Proceedings, pages 29-34, September 2009. CEUR-WS.org. [PDF]

Abstract. We study the decomposition of an arbitrary Petri net into open nets. This means that shared places can be seen as message channels between components. We show that there exists a unique decomposition into atomic components which can be efficiently computed. We further show that every composition of components yields a component and that every component can be built from atomic components. Finally, we briefly discuss potential applications.

@inproceedings{MennickeOW_2009_awpn,
Abstract = {We study the decomposition of an arbitrary Petri net into open nets. This means that shared places can be seen as message channels between components. We show that there exists a unique decomposition into atomic components which can be efficiently computed. We further show that every composition of components yields a component and that every component can be built from atomic components. Finally, we briefly discuss potential applications.},
Author = {Stephan Mennicke and Olivia Oanea and Karsten Wolf},
Booktitle = {16th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2009, Karlsruhe, Germany, September 25, 2009, Proceedings},
Editor = {Thomas Freytag and Andreas Eckleder},
Month = sep,
Pages = {29-34},
Publisher = {CEUR-WS.org},
Series = {CEUR Workshop Proceedings},
Title = {Decomposition into open nets},
Volume = {501},
Year = {2009}
}

Olivia Oanea and Karsten Wolf. An efficient necessary condition for compatibility. In Oliver Kopp and Niels Lohmann, editors, Proceedings of the 1st Central-European Workshop on Services and their Composition, ZEUS 2009, Stuttgart, Germany, March 2-3, 2009, volume 438 of CEUR Workshop Proceedings, pages 81-87, March 2009. CEUR-WS.org. [PDF]

Abstract. Composing services makes sense only if they are compatible, i.e. composition does not lead to problems such as livelocks or deadlocks. In general, compatibility can be checked using state space explorations on any kind of formal models of services. Petri nets, one of the formal model in use, offer a rich theory for reasoning without exploring a state space. Among the techniques is the so-called state equation which forms a linear algebraic necessary condition for reachability of states. In this article, we show how the state equation can be applied for a necessary condition for compatibility. This way, the number of expensive state space based compatibility checks can be drastically reduced. The condition can be applied even if compatibility is achieved through the construction of a behavioral adapter (mediator).

@inproceedings{OaneaW_2009_zeus,
Abstract = {Composing services makes sense only if they are compatible, i.e. composition does not lead to problems such as livelocks or deadlocks. In general, compatibility can be checked using state space explorations on any kind of formal models of services. 

Petri nets, one of the formal model in use, offer a rich theory for reasoning without exploring a state space. Among the techniques is the so-called state equation which forms a linear algebraic necessary condition for reachability of states. 

In this article, we show how the state equation can be applied for a necessary condition for compatibility. This way, the number of expensive state space based compatibility checks can be drastically reduced. The condition can be applied even if compatibility is achieved through the construction of a behavioral adapter (mediator).},
Author = {Olivia Oanea and Karsten Wolf},
Booktitle = {Proceedings of the 1st Central-European Workshop on Services and their Composition, ZEUS 2009, Stuttgart, Germany, March 2-3, 2009},
Editor = {Oliver Kopp and Niels Lohmann},
Month = mar,
Pages = {81-87},
Publisher = {CEUR-WS.org},
Series = {CEUR Workshop Proceedings},
Title = {An efficient necessary condition for compatibility},
Volume = {438},
Year = {2009}
}

Jarungjit Parnjai, Christian Stahl, and Karsten Wolf. A Finite Representation of all Substitutable Services and its Applications. In Oliver Kopp and Niels Lohmann, editors, Proceedings of the 1st Central-European Workshop on Services and their Composition, ZEUS 2009, Stuttgart, Germany, March 2-3, 2009, volume 438 of CEUR Workshop Proceedings, pages 29-34, March 2009. CEUR-WS.org. [PDF]

Abstract. We present a finite representation of all substitutable services P' of a given service P. We show that our approach can be used for at least two applications: (1) given a finite set of services P = {P1, ..., Pn}, we provide a representation of all services P' that can substitute every Pi in P, and (2) given a service P'' that cannot substitute a service P, we find the most similar service P* to P'' that can substitute P.

@inproceedings{ParnjaiSW_2009_zeus,
Abstract = {We present a finite representation of all substitutable services P' of a given service P. We show that our approach can be used for at least two applications: (1) given a finite set of services P = {P1, ..., Pn}, we provide a representation of all services P' that can substitute every Pi in P, and (2) given a service P'' that cannot substitute a service P, we find the most similar service P* to P'' that can substitute P. },
Author = {Jarungjit Parnjai and Christian Stahl and Karsten Wolf},
Booktitle = {Proceedings of the 1st Central-European Workshop on Services and their Composition, ZEUS 2009, Stuttgart, Germany, March 2-3, 2009},
Editor = {Oliver Kopp and Niels Lohmann},
Month = mar,
Pages = {29-34},
Publisher = {CEUR-WS.org},
Series = {CEUR Workshop Proceedings},
Title = {A Finite Representation of all Substitutable Services and its Applications},
Volume = {438},
Year = {2009},
}

Karsten Wolf. A Theory of Service Behavior. In Oliver Kopp and Niels Lohmann, editors, Proceedings of the 1st Central-European Workshop on Services and their Composition, ZEUS 2009, Stuttgart, Germany, March 2-3, 2009, volume 438 of CEUR Workshop Proceedings, pages 1-7, March 2009. CEUR-WS.org. [PDF]

Abstract. We outline a fundamental approach to behavioral aspects of services. In the center of this approach, we see behavioral models of services, interactions, and finite representations of sets thereof. Several operations and relations can be defined and their implementation on our representations can be studied. Finally, a number of interesting problems can be traced back to our models and operations. On the boundary of our theory, we place interfaces to other aspects of services.

@inproceedings{Wolf_2009_zeus,
Abstract = {We outline a fundamental approach to behavioral aspects of services. In the center of this approach, we see behavioral models of services, interactions, and finite representations of sets thereof. Several operations and relations can be defined and their implementation on our representations can be studied. Finally, a number of interesting problems can be traced back to our models and operations. On the boundary of our theory, we place interfaces to other aspects of services.},
Author = {Karsten Wolf},
Booktitle = {Proceedings of the 1st Central-European Workshop on Services and their Composition, ZEUS 2009, Stuttgart, Germany, March 2-3, 2009},
Editor = {Oliver Kopp and Niels Lohmann},
Month = mar,
Pages = {1-7},
Publisher = {CEUR-WS.org},
Series = {CEUR Workshop Proceedings},
Title = {A Theory of Service Behavior},
Volume = {438},
Year = {2009}
}

Karsten Wolf, Christian Stahl, Janine Ott, and Robert Danitz. Verifying Livelock Freedom in an SOA Scenario. In Ninth International Conference on Application of Concurrency to System Design (ACSD 2009), 1-3 July 2009, Augsburg, Germany, pages 168-177, June 2009. IEEE Computer Society. [PDF] [DOI]

Abstract. In a service-oriented architecture (SOA), we want to enable a service registry to match a request with a published service where their composition is livelock-free. To this end, we model check the composed system. We pre-compute and pre-reduce parts of the composed system thus shifting run time from the critical request phase to the less critical publish phase of the SOA approach.

@inproceedings{WolfSOD_2009_acsd,
Abstract = {In a service-oriented architecture (SOA), we want to enable a service registry to match a request with a published service where their composition is livelock-free. To this end, we model check the composed system. 

We pre-compute and pre-reduce parts of the composed system thus shifting run time from the critical request phase to the less critical publish phase of the SOA approach. },
Author = {Karsten Wolf and Christian Stahl and Janine Ott and Robert Danitz},
Booktitle = {Ninth International Conference on Application of Concurrency to System Design (ACSD 2009), 1-3 July 2009, Augsburg, Germany},
Month = jun,
Pages = {168-177},
Publisher = {IEEE Computer Society},
Title = {Verifying Livelock Freedom in an {SOA} Scenario},
Year = {2009},
}

Technische Berichte / Technical Reports

Ahmed Awad, Gero Decker, and Niels Lohmann. Diagnosing and Repairing Data Anomalies in Process Models. BPT Technical Report 03-2009, Hasso-Plattner-Institute, Potsdam, Germany, March 2009. [PDF]

Abstract. When using process models for automation, correctness of the models is a key requirement. While many approaches concentrate on control flow verification only, correct data flow modeling is of similar importance. This paper introduces an approach for detecting and repairing modeling errors that only occur in the interplay between control flow and data flow. The approach is based on place/transition nets and detects anomalies in BPMN models. In addition to the diagnosis of the modeling errors, a subset of errors can also be repaired automatically.

@techreport{AwadDL_2009_tr,
Abstract = {When using process models for automation, correctness of the models is a key requirement. While many approaches concentrate on control flow verification only, correct data flow modeling is of similar importance. This paper introduces an approach for detecting and repairing modeling errors that only occur in the interplay between control flow and data flow. The approach is based on place/transition nets and detects anomalies in BPMN models. In addition to the diagnosis of the modeling errors, a subset of errors can also be repaired automatically.},
Address = {Potsdam, Germany},
Author = {Ahmed Awad and Gero Decker and Niels Lohmann},
Institution = {Hasso-Plattner-Institute},
Month = mar,
Number = {03-2009},
Title = {Diagnosing and Repairing Data Anomalies in Process Models},
Type = {BPT Technical Report},
Year = {2009}
}

2008

Bücher und Tagungsbände / Books and Proceedings

Harro Wimmel. Entscheidbarkeit bei Petri Netzen - Überblick und Kompendium. Springer-Verlag, 2008. [DOI]

@book{Wimmel_2008_book,
Author = {Harro Wimmel},
Publisher = {Springer-Verlag},
Title = {{Entscheidbarkeit bei Petri Netzen - {\"U}berblick und Kompendium}},
Year = {2008},
}

Niels Lohmann and Karsten Wolf, editors. Proceedings of the 15th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2008, Rostock, Germany, September 26-27, 2008, volume 380 of CEUR Workshop Proceedings, September 2008. CEUR-WS.org. [WWW] [PDF]

@proceedings{LohmannW_2008_awpn,
Booktitle = {Algorithmen und Werkzeuge f\"ur Petrinetze},
Editor = {Niels Lohmann and Karsten Wolf},
Month = sep,
Publisher = {CEUR-WS.org},
Series = {CEUR Workshop Proceedings},
Title = {Proceedings of the 15th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2008, Rostock, Germany, September 26-27, 2008},
Volume = {380},
Year = {2008},
}

Zeitschriftenartikel / Journal Articles

Kees van Hee, Olivia Oanea, Alexander Serebrenik, Natalia Sidorova, and Marc Voorhoeve. History-Based Joins: Semantics, Soundness and Implementation. Data Knowl. Eng., 64(1):24-37, January 2008. [DOI]

Abstract. In this paper we study the use of case history for control structures in workflow processes. History-dependent control offers much more modeling power than classical control structures and it solves several semantical problems of industrial modeling frameworks. In particular, we introduce a history-dependent join. We study the modeling power by means of workflow patterns. Since proper completion (i.e. the ability of any configuration reachable from the initial one to reach the final one) is always an important ``sanity check'' of process modeling, we introduce a modeling method that guarantees this property holds. Finally we consider an implementation of the proposed control structures on top of an existing workflow engine.

@article{HeeOSSV_2008_dke,
Abstract = {In this paper we study the use of case history for control structures in workflow processes. History-dependent control offers much more modeling power than classical control structures and it solves several semantical problems of industrial modeling frameworks. In particular, we introduce a history-dependent join. We study the modeling power by means of workflow patterns. Since proper completion (i.e. the ability of any configuration reachable from the initial one to reach the final one) is always an important ``sanity check'' of process modeling, we introduce a modeling method that guarantees this property holds. Finally we consider an implementation of the proposed control structures on top of an existing workflow engine.},
Author = {{Kees} {van} Hee and Olivia Oanea and Alexander Serebrenik and Natalia Sidorova and Marc Voorhoeve},
Journal = {Data Knowl. Eng.},
Month = jan,
Number = {1},
Pages = {24-37},
Title = {History-Based Joins: Semantics, Soundness and Implementation},
Volume = {64},
Year = {2008},
}

Niels Lohmann, Peter Massuthe, Christian Stahl, and Daniela Weinberg. Analyzing Interacting WS-BPEL Processes Using Flexible Model Generation. Data Knowl. Eng., 64(1):38-54, January 2008. [PDF] [DOI]

Abstract. We address the problem of analyzing the interaction between WS-BPEL processes. We present a technology chain that starts out with a WS-BPEL process and translates it into a Petri net model. On the model we decide controllability of the process (the existence of a partner process, such that both can interact properly) and compute its operating guideline (a characterization of all properly interacting partner processes). To manage processes of realistic size, we present a concept of a flexible model generation which allows the generation of compact Petri net models. A case study demonstrates the value of this technology chain.

@article{LohmannMSW_2008_dke,
Abstract = {We address the problem of analyzing the interaction between WS-BPEL processes. We present a technology chain that starts out with a WS-BPEL process and translates it into a Petri net model. On the model we decide controllability of the process (the existence of a partner process, such that both can interact properly) and compute its operating guideline (a characterization of all properly interacting partner processes). To manage processes of realistic size, we present a concept of a flexible model generation which allows the generation of compact Petri net models. A case study demonstrates the value of this technology chain.},
Author = {Niels Lohmann and Peter Massuthe and Christian Stahl and Daniela Weinberg},
Journal = {Data Knowl. Eng.},
Month = jan,
Number = {1},
Pages = {38-54},
Title = {Analyzing Interacting {WS-BPEL} Processes Using Flexible Model Generation},
Volume = {64},
Year = 2008,
}

Peter Massuthe, Alexander Serebrenik, Natalia Sidorova, and Karsten Wolf. Can I find a Partner? Undecidablity of Partner Existence for Open Nets. Inf. Process. Lett., 108(6):374-378, November 2008. [DOI]

Abstract. We study open nets as Petri net models of web services, with a link to the practically relevant language WS-BPEL. For those nets, we investigate the problem of serviceableness which we consider as fundamental as the successful notion of soundness for workflow nets, i.e. Petri net models of business processes and workflows. While we could give algorithmic solutions to the serviceableness problem for subclasses of open nets in earlier work, this article shows that the problem is in general undecidable.

@article{MassutheSSW_2008_ipl,
Abstract = {We study open nets as Petri net models of web services, with a link to the practically relevant language WS-BPEL. For those nets, we investigate the problem of serviceableness which we consider as fundamental as the successful notion of soundness for workflow nets, i.e. Petri net models of business processes and workflows. While we could give algorithmic solutions to the serviceableness problem for subclasses of open nets in earlier work, this article shows that the problem is in general undecidable.},
Author = {Peter Massuthe and Alexander Serebrenik and Natalia Sidorova and Karsten Wolf},
Journal = {Inf. Process. Lett.},
Month = nov,
Number = {6},
Pages = {374-378},
Title = {Can {I} find a Partner? {Undecidablity} of Partner Existence for Open Nets},
Volume = {108},
Year = {2008},
}

Konferenzbeiträge / Conference Papers

Wil M. P. van der Aalst, Niels Lohmann, Peter Massuthe, Christian Stahl, and Karsten Wolf. From Public Views to Private Views -- Correctness-by-Design for Services. In Marlon Dumas and Reiko Heckel, editors, Web Services and Formal Methods, Forth International Workshop, WS-FM 2007, Brisbane, Australia, September 28-29, 2007, Proceedings, volume 4937 of Lecture Notes in Computer Science, pages 139-153, April 2008. Springer-Verlag. [PDF] [DOI]

Abstract. Service orientation is a means for integrating across diverse systems. Each resource, whether an application, system, or trading partner, can be accessed as a service. The resulting architecture, often referred to as SOA, has been an important enabler for interorganizational processes. Apart from technological issues that need to be addressed, it is important that all parties involved in such processes agree on the "rules of engagement". Therefore, we propose to use a contract that specifies the composition of the public views of all participating parties. Each party may then implement its part of the contract such that the implementation (i.e., the private view) accords with the contract. In this paper, we define a suitable notion of accordance inspired by the asynchronous nature of services. Moreover, we present several transformation rules for incrementally building a private view such that accordance with the contract is guaranteed by construction. These rules include adding internal tasks as well as the reordering of messages and are therefore much more powerful than existing correctness-preserving construction rules.

@inproceedings{AalstLMSW_2007_wsfm,
Abstract = {Service orientation is a means for integrating across diverse systems. Each resource, whether an application, system, or trading partner, can be accessed as a service. The resulting architecture, often referred to as SOA, has been an important enabler for interorganizational processes. Apart from technological issues that need to be addressed, it is important that all parties involved in such processes agree on the "rules of engagement". Therefore, we propose to use a contract that specifies the composition of the public views of all participating parties. Each party may then implement its part of the contract such that the implementation (i.e., the private view) accords with the contract. In this paper, we define a suitable notion of accordance inspired by the asynchronous nature of services. Moreover, we present several transformation rules for incrementally building a private view such that accordance with the contract is guaranteed by construction. These rules include adding internal tasks as well as the reordering of messages and are therefore much more powerful than existing correctness-preserving construction rules.},
Author = {{Wil} {M.} {P.} {van} {der} Aalst and Niels Lohmann and Peter Massuthe and Christian Stahl and Karsten Wolf},
Booktitle = {Web Services and Formal Methods, Forth International Workshop, WS-FM 2007, Brisbane, Australia, September 28-29, 2007, Proceedings},
Editor = {Marlon Dumas and Reiko Heckel},
Month = apr,
Pages = {139-153},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {From Public Views to Private Views -- Correctness-by-Design for Services},
Volume = {4937},
Year = {2008},
}

Gero Decker, Alistair Barros, Frank Michael Kraft, and Niels Lohmann. Non-desynchronizable Service Choreographies. In Athman Bouguettaya, Ingolf Krüger, and Tiziana Margaria, editors, Service-Oriented Computing - ICSOC 2008, 6th International Conference, Sydney, Australia, December 1-5, 2008. Proceedings, volume 5364 of Lecture Notes in Computer Science, pages 331-346, December 2008. Springer-Verlag. [PDF] [DOI]

Abstract. A precise definition of interaction behavior between services is a prerequisite for successful business-to-business integration. Service choreographies provide a view on message exchanges and their ordering constraints from a global perspective. Assuming message sending and receiving as one atomic step allows to reduce the modelers' effort. As downside, problematic race conditions resulting in deadlocks might appear when realizing the choreography using services that exchange messages asynchronously. This paper presents typical issues when desynchronizing service choreographies. Solutions from practice are discussed and a formal approach based on Petri nets is introduced for identifying desynchronizable choreographies.

@inproceedings{DeckerBKL_2008_icsoc,
Abstract = {A precise definition of interaction behavior between services is a prerequisite for successful business-to-business integration. Service choreographies provide a view on message exchanges and their ordering constraints from a global perspective. Assuming message sending and receiving as one atomic step allows to reduce the modelers' effort. As downside, problematic race conditions resulting in deadlocks might appear when realizing the choreography using services that exchange messages asynchronously. This paper presents typical issues when desynchronizing service choreographies. Solutions from practice are discussed and a formal approach based on Petri nets is introduced for identifying desynchronizable choreographies.},
Author = {Gero Decker and Alistair Barros and Frank Michael Kraft and Niels Lohmann},
Booktitle = {Service-Oriented Computing - ICSOC 2008, 6th International Conference, Sydney, Australia, December 1-5, 2008. Proceedings},
Editor = {Athman Bouguettaya and Ingolf Kr{\"u}ger and Tiziana Margaria},
Month = dec,
Pages = {331-346},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Non-desynchronizable Service Choreographies},
Volume = {5364},
Year = {2008},
}

Kathrin Kaschner and Niels Lohmann. Automatic Test Case Generation for Services. In Monika Solanki, Barry Norton, and Stephan Reiff-Marganiec, editors, 3rd Young Researchers Workshop on Service Oriented Computing, YR-SOC 2008, London, UK, 12-13 June 2008, Proceedings, London, UK, pages 21-26, June 2008. Imperial College. [PDF]

Abstract. Service-oriented computing (SOC) proposes loosely coupled interacting services as building blocks for distributed applications. This distributed nature makes the guarantee of correctness a challenging task. Based on the specification of a service (the public view), we introduce an approach to automatically generate test cases for black-box testing to check for compliance between the specification and the implementation of a service whose internal behavior might be secret.

@inproceedings{KaschnerL_2008_yrsoc,
Abstract = {Service-oriented computing (SOC) proposes loosely coupled interacting services as building blocks for distributed applications. This distributed nature makes the guarantee of correctness a challenging task. Based on the specification of a service (the public view), we introduce an approach to automatically generate test cases for black-box testing to check for compliance between the specification and the implementation of a service whose internal behavior might be secret.},
Address = {London, UK},
Author = {Kathrin Kaschner and Niels Lohmann},
Booktitle = {3rd Young Researchers Workshop on Service Oriented Computing, YR-SOC 2008, London, UK, 12-13 June 2008, Proceedings},
Editor = {Monika Solanki and Barry Norton and Stephan Reiff-Marganiec},
Month = jun,
Pages = {21-26},
Publisher = {Imperial College},
Title = {Automatic Test Case Generation for Services},
Year = {2008}
}

Dieter König, Niels Lohmann, Simon Moser, Christian Stahl, and Karsten Wolf. Extending the Compatibility Notion for Abstract WS-BPEL Processes. In Wei-Ying Ma, Andrew Tomkins, and Xiaodong Zhang, editors, Proceedings of the 17th International Conference on World Wide Web, WWW 2008, Beijing, China, April 21-25, 2008, pages 785-794, April 2008. ACM. [PDF] [DOI]

Abstract. WS-BPEL defines a standard for executable processes. Executable processes are business processes which can be automated through an IT infrastructure. The WS-BPEL specification also introduces the concept of abstract processes: In contrast to their executable siblings, abstract processes are not executable and can have parts where business logic is disguised. Nevertheless, the WS-BPEL specification introduces a notion of compatibility between such an under-specified abstract process and a fully specified executable one. Basically, this compatibility notion defines a set of syntactical rules that can be augmented or restricted by profiles. So far, there exist two of such profiles: the Abstract Process Profile for Observable Behavior and the Abstract Process Profile for Templates. None of these profiles defines a concept of behavioral equivalence. Therefore, both profiles are too strict with respect to the rules they impose when deciding whether an executable process is compatible to an abstract one. In this paper, we propose a novel profile that extends the existing Abstract Process Profile for Observable Behavior by defining a behavioral relationship. We also show that our novel profile allows for more flexibility when deciding whether an executable and an abstract process are compatible.

@inproceedings{KoenigLMSW_2008_www,
Abstract = {WS-BPEL defines a standard for executable processes. Executable processes are business processes which can be automated through an IT infrastructure. The WS-BPEL specification also introduces the concept of abstract processes: In contrast to their executable siblings, abstract processes are not executable and can have parts where business logic is disguised. Nevertheless, the WS-BPEL specification introduces a notion of compatibility between such an under-specified abstract process and a fully specified executable one. Basically, this compatibility notion defines a set of syntactical rules that can be augmented or restricted by profiles. So far, there exist two of such profiles: the Abstract Process Profile for Observable Behavior and the Abstract Process Profile for Templates. None of these profiles defines a concept of behavioral equivalence. Therefore, both profiles are too strict with respect to the rules they impose when deciding whether an executable process is compatible to an abstract one. In this paper, we propose a novel profile that extends the existing Abstract Process Profile for Observable Behavior by defining a behavioral relationship. We also show that our novel profile allows for more flexibility when deciding whether an executable and an abstract process are compatible.},
Author = {Dieter K{\"o}nig and Niels Lohmann and Simon Moser and Christian Stahl and Karsten Wolf},
Booktitle = {Proceedings of the 17th International Conference on World Wide Web, WWW 2008, Beijing, China, April 21-25, 2008},
Editor = {Wei-Ying Ma and Andrew Tomkins and Xiaodong Zhang},
Month = apr,
Organization = {ACM},
Pages = {785-794},
Slides = {foo},
Title = {Extending the Compatibility Notion for Abstract {WS-BPEL} Processes},
Year = {2008},
}

Niels Lohmann. A Feature-Complete Petri Net Semantics for WS-BPEL 2.0. In Marlon Dumas and Reiko Heckel, editors, Web Services and Formal Methods, Forth International Workshop, WS-FM 2007, Brisbane, Australia, September 28-29, 2007, Proceedings, volume 4937 of Lecture Notes in Computer Science, pages 77-91, April 2008. Springer-Verlag. [PDF] [DOI]

Abstract. We present an extension of a Petri net semantics for the Web Service Business Execution Language (WS-BPEL). This extension covers the novel activities and constructs introduced by the recent WS-BPEL 2.0 specification. Furthermore, we simplify several aspects of the Petri net semantics to allow for more compact models suited for computer-aided verification.

@inproceedings{Lohmann_2007_wsfm,
Abstract = {We present an extension of a Petri net semantics for the Web Service Business Execution Language (WS-BPEL). This extension covers the novel activities and constructs introduced by the recent WS-BPEL 2.0 specification. Furthermore, we simplify several aspects of the Petri net semantics to allow for more compact models suited for computer-aided verification.},
Author = {Niels Lohmann},
Booktitle = {Web Services and Formal Methods, Forth International Workshop, WS-FM 2007, Brisbane, Australia, September 28-29, 2007, Proceedings},
Editor = {Marlon Dumas and Reiko Heckel},
Month = apr,
Pages = {77-91},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {A Feature-Complete {Petri} Net Semantics for {WS-BPEL} 2.0},
Volume = {4937},
Year = {2008},
}

Niels Lohmann. Correcting Deadlocking Service Choreographies Using a Simulation-Based Graph Edit Distance. In Marlon Dumas, Manfred Reichert, and Ming-Chien Shan, editors, Business Process Management, 6th International Conference, BPM 2008, Milan, Italy, September 1-4, 2008, Proceedings, volume 5240 of Lecture Notes in Computer Science, pages 132-147, September 2008. Springer-Verlag. [PDF] [DOI]

Abstract. Many work has been conducted to analyze service choreographies to assert manyfold correctness criteria. While errors can be detected automatically, the correction of defective services is usually done manually. This paper introduces a graph-based approach to calculate the minimal edit distance between a given defective service and synthesized correct services. This edit distance helps to automatically fix found errors while keeping the rest of the service untouched. A prototypic implementation shows that the approach is applicable to real-life services.

@inproceedings{Lohmann_2008_bpm,
Abstract = {Many work has been conducted to analyze service choreographies to assert manyfold correctness criteria. While errors can be detected automatically, the correction of defective services is usually done manually. This paper introduces a graph-based approach to calculate the minimal edit distance between a given defective service and synthesized correct services. This edit distance helps to automatically fix found errors while keeping the rest of the service untouched. A prototypic implementation shows that the approach is applicable to real-life services.},
Author = {Niels Lohmann},
Booktitle = {Business Process Management, 6th International Conference, BPM 2008, Milan, Italy, September 1-4, 2008, Proceedings},
Editor = {Marlon Dumas and Manfred Reichert and Ming-Chien Shan},
Month = sep,
Pages = {132-147},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Correcting Deadlocking Service Choreographies Using a Simulation-Based Graph Edit Distance},
Volume = {5240},
Year = {2008},
}

Niels Lohmann. Decompositional Calculation of Operating Guidelines Using Free Choice Conflicts. In Niels Lohmann and Karsten Wolf, editors, 15th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2008, Rostock, Germany, September 26-27, 2008, Proceedings, volume 380 of CEUR Workshop Proceedings, pages 63-68, September 2008. CEUR-WS.org. [PDF]

Abstract. An operating guideline (OG) for a service S finitely characterizes the (possibly infinite) set of all services that can interact with S without deadlocks. This paper presents a decompositional approach to calculate an OG for a service whose underlying structure is acyclic and contains free-choice conflicts. This divide-and-conquer approach promises to be more efficient than the classical OG computation algorithm.

@inproceedings{Lohmann_2008_awpn,
Abstract = {An operating guideline (OG) for a service S finitely characterizes the (possibly infinite) set of all services that can interact with S without deadlocks. This paper presents a decompositional approach to calculate an OG for a service whose underlying structure is acyclic and contains free-choice conflicts. This divide-and-conquer approach promises to be more efficient than the classical OG computation algorithm.},
Author = {Niels Lohmann},
Booktitle = {15th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2008, Rostock, Germany, September 26-27, 2008, Proceedings},
Editor = {Niels Lohmann and Karsten Wolf},
Month = sep,
Pages = {63-68},
Publisher = {CEUR-WS.org},
Series = {CEUR Workshop Proceedings},
Title = {Decompositional Calculation of Operating Guidelines Using Free Choice Conflicts},
Volume = {380},
Year = {2008}
}

Niels Lohmann. Fixing Deadlocking Service Choreographies Using a Simulation-based Graph Edit Distance. In Monika Solanki, Barry Norton, and Stephan Reiff-Marganiec, editors, 3rd Young Researchers Workshop on Service Oriented Computing, YR-SOC 2008, London, UK, 12-13 June 2008, Proceedings, pages 13-20, June 2008. [PDF]

Abstract. Many work has been conducted to analyze services and service choreographies to assert manyfold correctness criteria. While errors can be detected automatically, the correction of defective services is usually done manually. This paper introduces a graph-based approach to calculate the minimal edit distance between a given defective service and synthesized correct services. This edit distance helps to automatically fix found errors while keeping the rest of the service untouched.

@inproceedings{Lohmann_2008_yrsoc,
Abstract = {Many work has been conducted to analyze services and service choreographies to assert manyfold correctness criteria. While errors can be detected automatically, the correction of defective services is usually done manually. This paper introduces a graph-based approach to calculate the minimal edit distance between a given defective service and synthesized correct services. This edit distance helps to automatically fix found errors while keeping the rest of the service untouched.},
Author = {Niels Lohmann},
Booktitle = {3rd Young Researchers Workshop on Service Oriented Computing, YR-SOC 2008, London, UK, 12-13 June 2008, Proceedings},
Editor = {Monika Solanki and Barry Norton and Stephan Reiff-Marganiec},
Month = jun,
Pages = {13-20},
Title = {Fixing Deadlocking Service Choreographies Using a Simulation-based Graph Edit Distance},
Year = {2008}
}

Niels Lohmann and Jens Kleine. Fully-automatic Translation of Open Workflow Net Models into Simple Abstract BPEL Processes. In Thomas Kühne, Wolfgang Reisig, and Friedrich Steimann, editors, Modellierung 2008, 12.-14. März 2008, Berlin, Proceedings, volume P-127 of Lecture Notes in Informatics (LNI), pages 57-72, March 2008. GI. [PDF]

Abstract. On the one hand, Petri net models have a successful history in the modeling, simulation, and verification of workflows and business processes. On the other hand, BPEL is the de facto standard for describing executable Web service-based business processes. With abstract BPEL processes, BPEL can also be used as modeling language. However, being a complicated language with many syntactic constraints, abstract BPEL processes impede a straightforward modeling. In this paper, we introduce a fully-automatic translation of Petri net models into abstract BPEL processes which can be refined to executable BPEL processes. This approach combines strengths of Petri nets in modeling and verification with the ability to execute BPEL processes. Furthermore, it completes the Tools4BPEL framework to synthesize BPEL processes which are correct by design.

@inproceedings{LohmannK_2008_mod,
Abstract = {On the one hand, Petri net models have a successful history in the modeling, simulation, and verification of workflows and business processes. On the other hand, BPEL is the de facto standard for describing executable Web service-based business processes. With abstract BPEL processes, BPEL can also be used as modeling language. However, being a complicated language with many syntactic constraints, abstract BPEL processes impede a straightforward modeling. 

In this paper, we introduce a fully-automatic translation of Petri net models into abstract BPEL processes which can be refined to executable BPEL processes. This approach combines strengths of Petri nets in modeling and verification with the ability to execute BPEL processes. Furthermore, it completes the Tools4BPEL framework to synthesize BPEL processes which are correct by design.},
Author = {Niels Lohmann and Jens Kleine},
Booktitle = {Modellierung 2008, 12.-14. M{\"a}rz 2008, Berlin, Proceedings},
Editor = {Thomas K{\"u}hne and Wolfgang Reisig and Friedrich Steimann},
Month = mar,
Pages = {57-72},
Publisher = {GI},
Series = {Lecture Notes in Informatics (LNI)},
Title = {Fully-automatic Translation of Open Workflow Net Models into Simple Abstract {BPEL} Processes},
Volume = {P-127},
Year = {2008}
}

Niels Lohmann and Oliver Kopp. Tools4BPEL4Chor. In Monika Solanki, Barry Norton, and Stephan Reiff-Marganiec, editors, 3rd Young Researchers Workshop on Service Oriented Computing, YR-SOC 2008, London, UK, 12-13 June 2008, Proceedings, pages 74-75, June 2008. [PDF]

@inproceedings{LohmannK_2008_yrsoc,
Author = {Niels Lohmann and Oliver Kopp},
Booktitle = {3rd Young Researchers Workshop on Service Oriented Computing, YR-SOC 2008, London, UK, 12-13 June 2008, Proceedings},
Editor = {Monika Solanki and Barry Norton and Stephan Reiff-Marganiec},
Month = jun,
Pages = {74-75},
Title = {{Tools4BPEL4Chor}},
Year = {2008}
}

Niels Lohmann, Oliver Kopp, Frank Leymann, and Wolfgang Reisig. Analyzing BPEL4Chor: Verification and Participant Synthesis. In Marlon Dumas and Reiko Heckel, editors, Web Services and Formal Methods, Forth International Workshop, WS-FM 2007, Brisbane, Australia, September 28-29, 2007, Proceedings, volume 4937 of Lecture Notes in Computer Science, pages 46-60, April 2008. Springer-Verlag. [PDF] [DOI]

Abstract. Choreographies offer means to capture global interactions between business processes of different partners. BPEL4Chor has been introduced to describe these interactions using BPEL. Currently, there are no formal methods available to verify BPEL4Chor choreographies. In this paper, we present how BPEL4Chor choreographies can be completely verified using Petri nets. A case study undermines that our verification techniques scale. Additionally, we show how the verification techniques can be used to generate a stub process for a partner taking part in a choreography. This is especially useful when the behavior of one participant is intended to follow the corresponding requirements of the other participants. Thus, the missing participant behavior can be generated and the error-prone design of that participant can be skipped.

@inproceedings{LohmannKLR_2007_wsfm,
Abstract = {Choreographies offer means to capture global interactions between business processes of different partners. BPEL4Chor has been introduced to describe these interactions using BPEL. Currently, there are no formal methods available to verify BPEL4Chor choreographies. In this paper, we present how BPEL4Chor choreographies can be completely verified using Petri nets. A case study undermines that our verification techniques scale. Additionally, we show how the verification techniques can be used to generate a stub process for a partner taking part in a choreography. This is especially useful when the behavior of one participant is intended to follow the corresponding requirements of the other participants. Thus, the missing participant behavior can be generated and the error-prone design of that participant can be skipped.},
Author = {Niels Lohmann and Oliver Kopp and Frank Leymann and Wolfgang Reisig},
Booktitle = {Web Services and Formal Methods, Forth International Workshop, WS-FM 2007, Brisbane, Australia, September 28-29, 2007, Proceedings},
Editor = {Marlon Dumas and Reiko Heckel},
Month = apr,
Pages = {46-60},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Analyzing {BPEL4Chor}: Verification and Participant Synthesis},
Volume = {4937},
Year = {2008},
}

Olivia Oanea. Soundness and related concepts for nested workflow nets. In Proc. of the International Workshop on Petri Nets and Distributed Systems (PNDS'2008), June 2008.

@inproceedings{Oanea_2008_pnds,
Author = {Olivia Oanea},
Booktitle = {Proc. of the International Workshop on Petri Nets and Distributed Systems (PNDS'2008)},
Month = jun,
Title = {Soundness and related concepts for nested workflow nets},
Year = {2008}
}

Christian Stahl and Karsten Wolf. An Approach to Tackle Livelock-Freedom in SOA. In Niels Lohmann and Karsten Wolf, editors, 15th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2008, Rostock, Germany, September 26-27, 2008, Proceedings, volume 380 of CEUR Workshop Proceedings, pages 69-74, September 2008. CEUR-WS.org. [PDF]

Abstract. We calculate a fixed finite set of state space fragments for a service P, where each fragment carries a part of the whole behavior of P. By composing these fragments according to the behavior of a service R we build the state space of their composition P+R which can be checked for deadlocks and livelocks. We show that this approach is applicable to realize a ``find'' request by a service R with a provided service P in SOA.

@inproceedings{StahlW_2008_awpn,
Abstract = {We calculate a fixed finite set of state space fragments for a service P, where each fragment carries a part of the whole behavior of P. By composing these fragments according to the behavior of a service R we build the state space of their composition P+R which can be checked for deadlocks and livelocks. We show that this approach is applicable to realize a ``find'' request by a service R with a provided service P in SOA. },
Author = {Christian Stahl and Karsten Wolf},
Booktitle = {15th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2008, Rostock, Germany, September 26-27, 2008, Proceedings},
Editor = {Niels Lohmann and Karsten Wolf},
Month = sep,
Pages = {69-74},
Publisher = {CEUR-WS.org},
Series = {CEUR Workshop Proceedings},
Title = {An Approach to Tackle Livelock-Freedom in {SOA}},
Volume = {380},
Year = {2008}
}

Christian Stahl and Karsten Wolf. Covering Places and Transitions in Open Nets. In Marlon Dumas, Manfred Reichert, and Ming-Chien Shan, editors, Business Process Management, 6th International Conference, BPM 2008, Milan, Italy, September 1-4, 2008, Proceedings, volume 5240 of Lecture Notes in Computer Science, pages 116-131, September 2008. Springer-Verlag. [PDF] [DOI]

Abstract. We present a finite representation of all services M where the composition with a given service N is deadlock-free, and a given set of activities of N can be covered (i.e. is not dead). Our representation is an extension of the existing notion of an operating guideline which only cared about deadlock freedom. We further present an algorithm to decide whether a service M matches with the extended operating guideline of N.

@inproceedings{StahlW_2008_bpm,
Abstract = {We present a finite representation of all services M where the composition with a given service N is deadlock-free, and a given set of activities of N can be covered (i.e. is not dead). Our representation is an extension of the existing notion of an operating guideline which only cared about deadlock freedom. We further present an algorithm to decide whether a service M matches with the extended operating guideline of N.},
Author = {Christian Stahl and Karsten Wolf},
Booktitle = {Business Process Management, 6th International Conference, BPM 2008, Milan, Italy, September 1-4, 2008, Proceedings},
Editor = {Marlon Dumas and Manfred Reichert and Ming-Chien Shan},
Month = sep,
Pages = {116-131},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Covering Places and Transitions in Open Nets},
Volume = {5240},
Year = {2008},
}

Karsten Wolf. On Synthesizing Behavior that Is Aware of Semantical Constraints. In Niels Lohmann and Karsten Wolf, editors, 15th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2008, Rostock, Germany, September 26-27, 2008, Proceedings, volume 380 of CEUR Workshop Proceedings, pages 49-54, September 2008. CEUR-WS.org. [PDF]

Abstract. Without taking care of the semantics of messages, every message is an isolated entity that can be created and sent at will. This leads to anomalies like a synthesized service that sends a filled form before having received the empty form. In this paper we pick up ideas from adapter synthesis for taking care of semantical constraints and develop them into two directions. First, we show that the approach taken for adapter synthesis can be applied to synthesis of services in general. Second, we argue that the taken approach is in a certain sense complete.

@inproceedings{Wolf_2008_awpn,
Abstract = {Without taking care of the semantics of messages, every message is an isolated entity that can be created and sent at will. This leads to anomalies like a synthesized service that sends a filled form before having received the empty form. In this paper we pick up ideas from adapter synthesis for taking care of semantical constraints and develop them into two directions. First, we show that the approach taken for adapter synthesis can be applied to synthesis of services in general. Second, we argue that the taken approach is in a certain sense complete. },
Author = {Karsten Wolf},
Booktitle = {15th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2008, Rostock, Germany, September 26-27, 2008, Proceedings},
Editor = {Niels Lohmann and Karsten Wolf},
Month = sep,
Pages = {49-54},
Publisher = {CEUR-WS.org},
Series = {CEUR Workshop Proceedings},
Title = {On Synthesizing Behavior that Is Aware of Semantical Constraints},
Volume = {380},
Year = {2008}
}

Technische Berichte / Technical Reports

Christian Gierds, Arjan J. Mooij, and Karsten Wolf. Specifying and generating behavioral service adapter based on transformation rules. Preprint CS-02-08, Universität Rostock, Rostock, Germany, August 2008. [PDF]

Abstract. Behavioral adapters are a way to establish proper interaction between services that have been developed independently. We present a novel approach for specifying such adapters, based on domain-specific transformation rules that reflect the elementary operations that adapters can perform. We show how complex adapters that adhere to these rules can be generated using existing controller generation algorithms. We discuss some example applications, including real-world business processes.

@techreport{GierdsMW_2008_tr_cs0208,
Abstract = {Behavioral adapters are a way to establish proper interaction between services that have been developed independently. We present a novel approach for specifying such adapters, based on domain-specific transformation rules that reflect the elementary operations that adapters can perform. We show how complex adapters that adhere to these rules can be generated using existing controller generation algorithms. We discuss some example applications, including real-world business processes.},
Address = {Rostock, Germany},
Author = {Christian Gierds and Arjan J. Mooij and Karsten Wolf},
Institution = {Universit{\"a}t Rostock},
Month = aug,
Number = {CS-02-08},
Title = {Specifying and generating behavioral service adapter based on transformation rules},
Type = {Preprint},
Year = {2008}
}

Peter Massuthe, Alexander Serebrenik, Natalia Sidorova, and Karsten Wolf. Can I find a Partner?. Preprint CS-01-08, Universität Rostock, Rostock, Germany, March 2008. [PDF]

Abstract. We study open nets as Petri net models of web services, with a link to the practically relevant language WS-BPEL. For those nets, we investigate the problem of serviceableness which we consider as fundamental as the successful notion of soundness for workflow nets, i.e. Petri net models of business processes and workflows. While we could give algorithmic solutions to the serviceableness problem for subclasses of open nets in earlier work, this article shows that the problem is in general undecidable.

@techreport{MassutheSSW_2008_tr_cs0108,
Abstract = {We study open nets as Petri net models of web services, with a link to the practically relevant language WS-BPEL. For those nets, we investigate the problem of serviceableness which we consider as fundamental as the successful notion of soundness for workflow nets, i.e. Petri net models of business processes and workflows. While we could give algorithmic solutions to the serviceableness problem for subclasses of open nets in earlier work, this article shows that the problem is in general undecidable.},
Address = {Rostock, Germany},
Author = {Peter Massuthe and Alexander Serebrenik and Natalia Sidorova and Karsten Wolf},
Institution = {Universit{\"a}t Rostock},
Month = mar,
Number = {CS-01-08},
Title = {Can {I} find a Partner?},
Type = {Preprint},
Year = {2008}
}

2007

Zeitschriftenartikel / Journal Articles

Eike Best, Philippe Darondeau, and Harro Wimmel. Making Petri Nets Safe and Free of Internal Transitions. Fundam. Inform., 80(1-3):75-90, 2007. [WWW]

Abstract. This paper discusses the following results: that bounded Petri nets can be transformed into pomset-equivalent safe nets; that boundedmarked graphs can be transformed into step-language-equivalent safe marked graphs; that safe labelled marked graphs can be transformed into tau-free safe labelled marked graphs; and that marked graphs can be separated. The paper also lists some open problems that have arisen in this context.

@article{BestDW_2007_fi,
Abstract = {This paper discusses the following results: that bounded Petri nets can be transformed into pomset-equivalent safe nets; that boundedmarked graphs can be transformed into step-language-equivalent safe marked graphs; that safe labelled marked graphs can be transformed into tau-free safe labelled marked graphs; and that marked graphs can be separated. The paper also lists some open problems that have arisen in this context.},
Author = {Eike Best and Philippe Darondeau and Harro Wimmel},
Journal = {Fundam. Inform.},
Number = {1-3},
Pages = {75-90},
Title = {Making {Petri} Nets Safe and Free of Internal Transitions},
Volume = {80},
Year = {2007},
}

Kees van Hee, Olivia Oanea, Alexander Serebrenik, Natalia Sidorova, and Marc Voorhoeve. LogLogics: A logic for history-dependent business processes. Sci. Comput. Program., 65(1):30-40, March 2007. [DOI]

Abstract. Choices in business processes are often based on the process history saved as a log-file listing events and their time stamps. In this paper we introduce LogLogics, a finite-path variant of the Timed Propositional Temporal Logic with Past, which can be in particular used for specifying guards in business process models. The novelty is due to the presence of boundary points corresponding to the starting and current observation points, which gives rise to a three-valued logic allowing us to distinguish between temporal formulas that hold for any log extended with some possible past and future (true), those that do not hold for any extended log (false) and those that hold for some but not all extended logs (unknown). We reduce the check of the truth value of a LogLogics formula to a check on a finite abstraction and present an evaluation algorithm. We also define LogLogics patterns for commonly occurring properties.

@article{HeeOSSV_2006_scp,
Abstract = {Choices in business processes are often based on the process history saved as a log-file listing events and their time stamps. In this paper we introduce LogLogics, a finite-path variant of the Timed Propositional Temporal Logic with Past, which can be in particular used for specifying guards in business process models. The novelty is due to the presence of boundary points corresponding to the starting and current observation points, which gives rise to a three-valued logic allowing us to distinguish between temporal formulas that hold for any log extended with some possible past and future (true), those that do not hold for any extended log (false) and those that hold for some but not all extended logs (unknown). We reduce the check of the truth value of a LogLogics formula to a check on a finite abstraction and present an evaluation algorithm. We also define LogLogics patterns for commonly occurring properties.},
Author = {{Kees} {van} Hee and Olivia Oanea and Alexander Serebrenik and Natalia Sidorova and Marc Voorhoeve},
Journal = {Sci. Comput. Program.},
Month = mar,
Number = {1},
Pages = {30-40},
Title = {{LogLogics}: A logic for history-dependent business processes},
Volume = {65},
Year = {2007},
}

Kees van Hee, Olivia Oanea, Alexander Serebrenik, Natalia Sidorova, Marc Voorhoeve, and Irina A. Lomazova. Checking Properties of Adaptive Workflow Nets. Fundam. Inform., 79(3-4):347-362, August 2007. [WWW]

Abstract. In this paper we consider adaptive workflow nets, a class of nested nets that allows more comfort and expressive power for modeling adaptability and exception handling in workflow nets. We define two important behavioural properties of adaptive workflow nets: soundness and circumspectness. Soundness means that a proper final marking (state) can be reached from any marking which is reachable from the initial marking, and no garbage will be left. Circumspectness means that the upper layer is always ready to handle any exception that can happen in a lower layer. We define a finite state abstraction for adaptive workflow nets and show that soundness and circumspectness can be verified on this abstraction.

@article{HeeOSSVL_2007_fi,
Abstract = {In this paper we consider adaptive workflow nets, a class of nested nets that allows more comfort and expressive power for modeling adaptability and exception handling in workflow nets. We define two important behavioural properties of adaptive workflow nets: soundness and circumspectness. Soundness means that a proper final marking (state) can be reached from any marking which is reachable from the initial marking, and no garbage will be left. Circumspectness means that the upper layer is always ready to handle any exception that can happen in a lower layer. We define a finite state abstraction for adaptive workflow nets and show that soundness and circumspectness can be verified on this abstraction.},
Author = {{Kees} {van} Hee and Olivia Oanea and Alexander Serebrenik and Natalia Sidorova and Marc Voorhoeve and Irina A. Lomazova},
Journal = {Fundam. Inform.},
Month = aug,
Number = {3-4},
Pages = {347-362},
Title = {Checking Properties of Adaptive Workflow Nets},
Volume = {79},
Year = {2007},
}

Kathrin Kaschner, Peter Massuthe, and Karsten Wolf. Symbolic Representation of Operating Guidelines for Services. Petri Net Newsletter, 72:21-28, April 2007. [PDF]

@article{KaschnerMW_2007_pnn,
Author = {Kathrin Kaschner and Peter Massuthe and Karsten Wolf},
Journal = {Petri Net Newsletter},
Month = apr,
Pages = {21-28},
Title = {Symbolic Representation of Operating Guidelines for Services},
Volume = 72,
Year = 2007
}

Peter Massuthe and Karsten Wolf. An Algorithm for Matching Nondeterministic Services with Operating Guidelines. Int. J. Business Process Integration and Management, 2(2):81-90, 2007. [DOI]

Abstract. Interorganisational cooperation is more and more organised by the paradigm of services. Service-Oriented Architectures (SOA) provide a general framework for service interaction. SOA describe three roles of services, the service provider, the service requester and the service broker, together with the three operations publish, find and bind. We provide a formal method based on non-deterministic automata to model services and their interaction. In this paper, we restrict ourselves to finite and acyclic automata. We suggest operating guidelines as a convenient and intuitive artefact to realise the publish operation. In our approach, the find operation reduces to a matching problem between the requester's service and the published operating guidelines. If matching services are actually bound together, our approach guarantees deadlock-free interaction. In this paper, matching of deterministic as well as non-deterministic automata with operating guidelines is presented.

@article{MassutheW_2007_ijbpim,
Abstract = {Interorganisational cooperation is more and more organised by the paradigm of services. Service-Oriented Architectures (SOA) provide a general framework for service interaction. SOA describe three roles of services, the service provider, the service requester and the service broker, together with the three operations publish, find and bind. We provide a formal method based on non-deterministic automata to model services and their interaction. In this paper, we restrict ourselves to finite and acyclic automata. We suggest operating guidelines as a convenient and intuitive artefact to realise the publish operation. In our approach, the find operation reduces to a matching problem between the requester's service and the published operating guidelines. If matching services are actually bound together, our approach guarantees deadlock-free interaction. In this paper, matching of deterministic as well as non-deterministic automata with operating guidelines is presented.},
Author = {Peter Massuthe and Karsten Wolf},
Journal = {Int. J. Business Process Integration and Management},
Number = {2},
Pages = {81-90},
Title = {An Algorithm for Matching Nondeterministic Services with Operating Guidelines},
Volume = {2},
Year = {2007},
}

Wolfgang Reisig, Karsten Wolf, Jan Bretschneider, Kathrin Kaschner, Niels Lohmann, Peter Massuthe, and Christian Stahl. Challenges in a Service-Oriented World. ERCIM News, 70:28-29, July 2007. [WWW]

Abstract. Interacting services raise a number of new software engineering challenges. To meet these challenges, the behaviour of the involved services must be considered. We present results regarding the behaviour of services in isolation, the interaction of services in choreographies, the exchangeability of a service, and the synthesis of desired partner services.

@article{ReisigWBKLMS_2007_ercim,
Abstract = {Interacting services raise a number of new software engineering challenges. To meet these challenges, the behaviour of the involved services must be considered. We present results regarding the behaviour of services in isolation, the interaction of services in choreographies, the exchangeability of a service, and the synthesis of desired partner services.},
Author = {Wolfgang Reisig and Karsten Wolf and Jan Bretschneider and Kathrin Kaschner and Niels Lohmann and Peter Massuthe and Christian Stahl},
Journal = {ERCIM News},
Month = jul,
Pages = {28-29},
Title = {Challenges in a Service-Oriented World},
Volume = {70},
Year = {2007},
}

Konferenzbeiträge / Conference Papers

Kees van Hee, Olivia Oanea, Natalia Sidorova, and Marc Voorhoeve. Verifying Generalized Soundness for Workflow Nets. In Irina Virbitskaite and Andrei Voronkov, editors, Perspectives of Systems Informatics, 6th International Andrei Ershov Memorial Conference, PSI 2006, Novosibirsk, Russia, June 27-30, 2006. Revised Papers, volume 4378 of Lecture Notes in Computer Science, pages 235-247, June 2007. Springer-Verlag. [DOI]

Abstract. We improve the decision procedure from [10] for the problem of generalized soundness of workflow nets. A workflow net is generalized sound iff every marking reachable from an initial marking with k tokens on the initial place terminates properly, i.e. it can reach a marking with k tokens on the final place, for an arbitrary natural number k. Our new decision procedure not only reports whether the net is sound or not, but also returns a counterexample in case the workflow net is not generalized sound. We report on experimental results obtained with the prototype we made and explain how the procedure can be used for the compositional verification of large workflows.

@inproceedings{HeeOSV_2006_psi,
Abstract = {We improve the decision procedure from [10] for the problem of generalized soundness of workflow nets. A workflow net is generalized sound iff every marking reachable from an initial marking with k tokens on the initial place terminates properly, i.e. it can reach a marking with k tokens on the final place, for an arbitrary natural number k. Our new decision procedure not only reports whether the net is sound or not, but also returns a counterexample in case the workflow net is not generalized sound. We report on experimental results obtained with the prototype we made and explain how the procedure can be used for the compositional verification of large workflows.},
Author = {{Kees} {van} Hee and Olivia Oanea and Natalia Sidorova and Marc Voorhoeve},
Booktitle = {Perspectives of Systems Informatics, 6th International Andrei Ershov Memorial Conference, PSI 2006, Novosibirsk, Russia, June 27-30, 2006. Revised Papers},
Editor = {Irina Virbitskaite and Andrei Voronkov},
Month = jun,
Pages = {235-247},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Verifying Generalized Soundness for Workflow Nets},
Volume = {4378},
Year = {2007},
}

Niels Lohmann. A Feature-Complete Petri Net Semantics for WS-BPEL 2.0. In Kees van Hee, Wolfgang Reisig, and Karsten Wolf, editors, Proceedings of the Workshop on Formal Approaches to Business Processes and Web Services (FABPWS'07), Siedlce, Poland, pages 21-35, June 2007. University of Podlasie. [PDF]

Abstract. We present an extension of a Petri net semantics for the Web Service Business Execution Language (WS-BPEL). This extension covers the novel activities and constructs introduced by the recent WS-BPEL 2.0 specification. Furthermore, we simplify several aspects of the Petri net semantics to allow for more compact models suited for computer-aided verification.

@inproceedings{Lohmann_2007_fabpws,
Abstract = {We present an extension of a Petri net semantics for the Web Service Business Execution Language (WS-BPEL). This extension covers the novel activities and constructs introduced by the recent WS-BPEL 2.0 specification. Furthermore, we simplify several aspects of the Petri net semantics to allow for more compact models suited for computer-aided verification.},
Address = {Siedlce, Poland},
Author = {Niels Lohmann},
Booktitle = {Proceedings of the Workshop on Formal Approaches to Business Processes and Web Services (FABPWS'07)},
Editor = {{Kees} {van} Hee and Wolfgang Reisig and Karsten Wolf},
Month = jun,
Pages = {21-35},
Publisher = {University of Podlasie},
Title = {A Feature-Complete {Petri} Net Semantics for {WS-BPEL 2.0}},
Year = 2007
}

Niels Lohmann, Peter Massuthe, and Karsten Wolf. Behavioral Constraints for Services. In Gustavo Alonso, Peter Dadam, and Michael Rosemann, editors, Business Process Management, 5th International Conference, BPM 2007, Brisbane, Australia, September 24-28, 2007, Proceedings, volume 4714 of Lecture Notes in Computer Science, pages 271-287, September 2007. Springer-Verlag. [PDF] [DOI]

Abstract. Recently, we introduced the concept of an operating guideline of a service as a structure that characterizes all its properly interacting partner services. The hitherto considered correctness criterion is deadlock freedom of the composition of both services. In practice, there are intended and unintended deadlock-freely interacting partners of a service. In this paper, we provide a formal approach to express intended and unintended behavior as behavioral constraints. With such a constraint, unintended partners can be "filtered" yielding a customized operating guideline. Customized operating guidelines can be applied to validate a service and for service discovery.

@inproceedings{LohmannMW_2007_bpm,
Abstract = {Recently, we introduced the concept of an operating guideline of a service as a structure that characterizes all its properly interacting partner services. The hitherto considered correctness criterion is deadlock freedom of the composition of both services. In practice, there are intended and unintended deadlock-freely interacting partners of a service. In this paper, we provide a formal approach to express intended and unintended behavior as behavioral constraints. With such a constraint, unintended partners can be "filtered" yielding a customized operating guideline. Customized operating guidelines can be applied to validate a service and for service discovery.},
Author = {Niels Lohmann and Peter Massuthe and Karsten Wolf},
Booktitle = {Business Process Management, 5th International Conference, BPM 2007, Brisbane, Australia, September 24-28, 2007, Proceedings},
Editor = {Gustavo Alonso and Peter Dadam and Michael Rosemann},
Month = sep,
Pages = {271-287},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Behavioral Constraints for Services},
Volume = {4714},
Year = {2007},
}

Niels Lohmann, Peter Massuthe, and Karsten Wolf. Operating Guidelines for Finite-State Services. In Jetty Kleijn and Alex Yakovlev, editors, 28th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, ICATPN 2007, Siedlce, Poland, June 25-29, 2007, Proceedings, volume 4546 of Lecture Notes in Computer Science, pages 321-341, June 2007. Springer-Verlag. [PDF] [DOI]

Abstract. We study services modeled as open workflow nets (oWFN) and describe their behavior as service automata. Based on service automata, we introduce the concept of an operating guideline, extending the work of [1, 2] which was restricted to acyclic services. An operating guideline gives complete information about how to properly interact (in this paper: deadlock-freely and with limited communication) with an oWFN N. It can be executed thus forming a properly interacting partner of N, or it can be used to support service discovery. An operating guideline for N is a particular service automaton S that is enriched with Boolean annotations. S interacts properly with the service automaton Prov, representing the behavior of N , and is able to simulate every other service that interacts properly with Prov . The attached annotations give complete information about whether or not a simulated service interacts properly with Prov, too.

@inproceedings{LohmannMW_2007_atpn,
Abstract = {We study services modeled as open workflow nets (oWFN) and describe their behavior as service automata. Based on service automata, we introduce the concept of an operating guideline, extending the work of [1, 2] which was restricted to acyclic services. An operating guideline gives complete information about how to properly interact (in this paper: deadlock-freely and with limited communication) with an oWFN N. It can be executed thus forming a properly interacting partner of N, or it can be used to support service discovery. An operating guideline for N is a particular service automaton S that is enriched with Boolean annotations. S interacts properly with the service automaton Prov, representing the behavior of N , and is able to simulate every other service that interacts properly with Prov . The attached annotations give complete information about whether or not a simulated service interacts properly with Prov, too.},
Author = {Niels Lohmann and Peter Massuthe and Karsten Wolf},
Booktitle = {28th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, ICATPN 2007, Siedlce, Poland, June 25-29, 2007, Proceedings},
Editor = {Jetty Kleijn and Alex Yakovlev},
Month = jun,
Pages = {321-341},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Operating Guidelines for Finite-State Services},
Volume = {4546},
Year = {2007},
}

Wolfgang Reisig, Jan Bretschneider, Dirk Fahland, Niels Lohmann, Peter Massuthe, and Christian Stahl. Services as a Paradigm of Computation. In Cliff B. Jones, Zhiming Liu, and Jim Woodcock, editors, Formal Methods and Hybrid Real-Time Systems, Essays in Honor of Dines Bjorner and Chaochen Zhou on the Occasion of Their 70th Birthdays, Papers presented at a Symposium held in Macao, China, September 24-25, 2007, volume 4700 of Lecture Notes in Computer Science, pages 521-538, September 2007. Springer-Verlag. [PDF] [DOI]

Abstract. The recent success of service-oriented architectures gives rise to some fundamental questions: To what extent do services constitute a new paradigm of computation? What are the elementary ingredients of this paradigm? What are adequate notions of semantics, composition, equivalence? How can services be modeled and analyzed? This paper addresses and answers those questions, thus preparing the ground for forthcoming software design techniques.

@inproceedings{ReisigBFLMS_2007_festschrift,
Abstract = {The recent success of service-oriented architectures gives rise to some fundamental questions: To what extent do services constitute a new paradigm of computation? What are the elementary ingredients of this paradigm? What are adequate notions of semantics, composition, equivalence? How can services be modeled and analyzed? This paper addresses and answers those questions, thus preparing the ground for forthcoming software design techniques.},
Author = {Wolfgang Reisig and Jan Bretschneider and Dirk Fahland and Niels Lohmann and Peter Massuthe and Christian Stahl},
Booktitle = {Formal Methods and Hybrid Real-Time Systems, Essays in Honor of Dines Bj{\o}rner and Chaochen Zhou on the Occasion of Their 70th Birthdays, Papers presented at a Symposium held in Macao, China, September 24-25, 2007},
Editor = {Cliff B. Jones and Zhiming Liu and Jim Woodcock},
Month = sep,
Pages = {521-538},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Services as a Paradigm of Computation},
Volume = {4700},
Year = {2007},
}

Karsten Wolf. Generating Petri Net State Spaces. In Jetty Kleijn and Alex Yakovlev, editors, 28th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, ICATPN 2007, Siedlce, Poland, June 25-29, 2007, Proceedings, volume 4546 of Lecture Notes in Computer Science, pages 29-42, June 2007. Springer-Verlag. Invited lecture. [PDF] [DOI]

Abstract. Most specific characteristics of (Place/Transition) Petri nets can be traced back to a few basic features including the monotonicity of the enabling condition, the linearity of the firing rule, and the locality of both. These features enable ``Petri net'' analysis techniques such as the invariant calculus, the coverability graph technique, approaches based on unfolding, or structural (such as siphon/trap based) analysis. In addition, most verification techniques developed outside the realm of Petri nets can be applied to Petri nets as well. In this paper, we want to demonstrate that the basic features of Petri nets do not only lead to additional analysis techniques, but as well to improved implementations of formalism-independent techniques. As an example, we discuss the explicit generation of a state space. We underline our arguments with some experience from the implementation and use of the Petri net based state space tool LoLA.

@inproceedings{Wolf_2007_atpn,
Abstract = {Most specific characteristics of (Place/Transition) Petri nets can be traced back to a few basic features including the monotonicity of the enabling condition, the linearity of the firing rule, and the locality of both. These features enable ``Petri net'' analysis techniques such as the invariant calculus, the coverability graph technique, approaches based on unfolding, or structural (such as siphon/trap based) analysis. In addition, most verification techniques developed outside the realm of Petri nets can be applied to Petri nets as well. 

In this paper, we want to demonstrate that the basic features of Petri nets do not only lead to additional analysis techniques, but as well to improved implementations of formalism-independent techniques. As an example, we discuss the explicit generation of a state space. We underline our arguments with some experience from the implementation and use of the Petri net based state space tool LoLA. },
Author = {Karsten Wolf},
Booktitle = {28th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, ICATPN 2007, Siedlce, Poland, June 25-29, 2007, Proceedings},
Editor = {Jetty Kleijn and Alex Yakovlev},
Month = jun,
Note = {Invited lecture},
Pages = {29-42},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Generating {Petri} Net State Spaces},
Volume = {4546},
Year = {2007},
}

Technische Berichte / Technical Reports

Wil M. P. van der Aalst, Peter Massuthe, Christian Stahl, and Karsten Wolf. Multiparty Contracts: Agreeing and Implementing Interorganizational Processes. Informatik-Berichte 213, Humboldt-Universität zu Berlin, Berlin, Germany, June 2007. [PDF]

Abstract. A contract specifies an interorganizational process together with a distribution of responsibilities for the activities among the parties involved. In this paper, we formally show how a party can implement its part of the contract such that the implementation accords with the contract. We propose a formal notion of a contract and give a criterion for accordance between a local implementation and a contract such that, if all local implementations accord with the contract, the overall process is deadlock-free and it is always possible to terminate properly. Then, we sketch a technique for automatically checking the proposed accordance criterion. Finally, we present accordance-preserving transformation rules. These rules can be used to implement a part of the contract while preserving the accordance criterion.

@techreport{AalstMSW_2007_hub_tr213,
Abstract = {A contract specifies an interorganizational process together with a distribution of responsibilities for the activities among the parties involved. In this paper, we formally show how a party can implement its part of the contract such that the implementation accords with the contract. We propose a formal notion of a contract and give a criterion for accordance between a local implementation and a contract such that, if all local implementations accord with the contract, the overall process is deadlock-free and it is always possible to terminate properly. Then, we sketch a technique for automatically checking the proposed accordance criterion. Finally, we present accordance-preserving transformation rules. These rules can be used to implement a part of the contract while preserving the accordance criterion.},
Address = {Berlin, Germany},
Author = {{Wil} {M.} {P.} {van} {der} {Aalst} and Peter Massuthe and Christian Stahl and Karsten Wolf},
Institution = {Humboldt-Universit{\"a}t zu Berlin},
Month = jun,
Number = {213},
Title = {Multiparty Contracts: Agreeing and Implementing Interorganizational Processes},
Type = {Informatik-Berichte},
Year = {2007}
}

Dieter König, Niels Lohmann, Simon Moser, Christian Stahl, and Karsten Wolf. Extending the Compatibility Notion for Abstract WS-BPEL Processes. Preprint CS-02-07, Universität Rostock, Rostock, Germany, November 2007. [PDF]

Abstract. WS-BPEL defines a standard for executable business processes. Executable processes are business processes which can be automated through an IT infrastructure. The WS-BPEL specification also introduces the concept of abstract processes: In contrast to their executable siblings, abstract processes are not executable and can have parts where business logic is disguised. Nevertheless, the WS-BPEL specification introduces a notion of compatibility between such an under-specified abstract process and a fully specified executable one. Basically, this compatibility notion defines a set of syntactical rules that can be augmented or restricted by profiles. So far, there exists two of such profiles: the Abstract Process Profile for Observable Behavior and the Abstract Process Profile for Templates. None of these profiles defines a concept of behavioral equivalence. Therefore, both profiles are too strict with respect to the rules they impose when deciding whether an executable process is compatible to an abstract one. In this paper, we propose a novel profile that extends the existing Abstract Process Profile for Observable Behavior by defining a behavioral relationship. We also show that our novel profile allows for more flexibility when deciding whether an executable and an abstract process are compatible.

@techreport{KoenigLMSW_2007_tr_cs0207,
Abstract = {WS-BPEL defines a standard for executable business processes. Executable processes are business processes which can be automated through an IT infrastructure. The WS-BPEL specification also introduces the concept of abstract processes: In contrast to their executable siblings, abstract processes are not executable and can have parts where business logic is disguised. Nevertheless, the WS-BPEL specification introduces a notion of compatibility between such an under-specified abstract process and a fully specified executable one. Basically, this compatibility notion defines a set of syntactical rules that can be augmented or restricted by profiles. So far, there exists two of such profiles: the Abstract Process Profile for Observable Behavior and the Abstract Process Profile for Templates. None of these profiles defines a concept of behavioral equivalence. Therefore, both profiles are too strict with respect to the rules they impose when deciding whether an executable process is compatible to an abstract one. In this paper, we propose a novel profile that extends the existing Abstract Process Profile for Observable Behavior by defining a behavioral relationship. We also show that our novel profile allows for more flexibility when deciding whether an executable and an abstract process are compatible.},
Address = {Rostock, Germany},
Author = {Dieter K{\"o}nig and Niels Lohmann and Simon Moser and Christian Stahl and Karsten Wolf},
Institution = {Universit{\"a}t Rostock},
Month = nov,
Number = {CS-02-07},
Title = {Extending the Compatibility Notion for Abstract {WS-BPEL} Processes},
Type = {Preprint},
Year = {2007}
}

Niels Lohmann. A Feature-Complete Petri Net Semantics for WS-BPEL 2.0 and its Compiler BPEL2oWFN. Informatik-Berichte 212, Humboldt-Universität zu Berlin, Berlin, Germany, August 2007. [PDF]

Abstract. We present an extension of a Petri net semantics for the Web Service Business Execution Language (WS-BPEL). This extension covers the novel activities and constructs introduced by the recent WS-BPEL 2.0 specification. Furthermore, we simplify several aspects of the Petri net semantics to allow for more compact models suited for computer-aided verification. This technical report is the extended version of the papers [1, 2] and can be seen as the sequel of [3].

@techreport{Lohmann_2007_hubtr212,
Abstract = {We present an extension of a Petri net semantics for the Web Service Business Execution Language (WS-BPEL). This extension covers the novel activities and constructs introduced by the recent WS-BPEL 2.0 specification. Furthermore, we simplify several aspects of the Petri net semantics to allow for more compact models suited for computer-aided verification. This technical report is the extended version of the papers [1, 2] and can be seen as the sequel of [3].},
Address = {Berlin, Germany},
Author = {Niels Lohmann},
Institution = {Humboldt-Universit{\"a}t zu Berlin},
Month = aug,
Number = 212,
Title = {A Feature-Complete {Petri} Net Semantics for {WS-BPEL} 2.0 and its Compiler {BPEL2oWFN}},
Type = {Informatik-Berichte},
Year = 2007
}

Niels Lohmann, Peter Massuthe, and Karsten Wolf. Behavioral Constraints for Services. Informatik-Berichte 214, Humboldt-Universität zu Berlin, Berlin, Germany, May 2007. [PDF]

Abstract. Recently, we introduced the concept of an operating guideline of a service as a structure that characterizes all its properly interacting partner services. The hitherto considered correctness criterion is deadlock freedom of the composition of both services. In practice, there are intended and unintended deadlock-freely interacting partners of a service. In this paper, we provide a formal approach to express intended and unintended behavior as behavioral constraints. With such a constraint, unintended partners can be ``filtered'' yielding a customized operating guideline. Customized operating guidelines can be applied to validate a service and for service discovery.

@techreport{LohmannMW2007_hub_tr214,
Abstract = {Recently, we introduced the concept of an operating guideline of a service as a structure that characterizes all its properly interacting partner services. The hitherto considered correctness criterion is deadlock freedom of the composition of both services. In practice, there are intended and unintended deadlock-freely interacting partners of a service. In this paper, we provide a formal approach to express intended and unintended behavior as behavioral constraints. With such a constraint, unintended partners can be ``filtered'' yielding a customized operating guideline. Customized operating guidelines can be applied to validate a service and for service discovery.},
Address = {Berlin, Germany},
Author = {Niels Lohmann and Peter Massuthe and Karsten Wolf},
Institution = {Humboldt-Universit{\"a}t zu Berlin},
Month = may,
Number = 214,
Title = {Behavioral Constraints for Services},
Type = {Informatik-Berichte},
Year = 2007
}

Niels Lohmann, H.M.W. Verbeek, Chun Ouyang, Christian Stahl, and Wil M. P. van der Aalst. Comparing and Evaluating Petri Net Semantics for BPEL. Computer Science Report 07/23, Eindhoven University of Technology, Eindhoven, The Netherlands, August 2007. [PDF]

Abstract. We compare two Petri net semantics for the Web Services Business Process Execution Language (BPEL). The comparison reveals different modeling decisions. These decisions together with their consequences are discussed.We also give an overview of the different properties that can be verified on the resulting models. A case study helps to evaluate the corresponding compilers which transform a BPEL process into a Petri net model.

@techreport{LohmannVOSA_2007_tue_0723,
Abstract = {We compare two Petri net semantics for the Web Services Business Process Execution Language (BPEL). The comparison reveals different modeling decisions. These decisions together with their consequences are discussed.We also give an overview of the different properties that can be verified on the resulting models. A case study helps to evaluate the corresponding compilers which transform a BPEL process into a Petri net model.},
Address = {Eindhoven, The Netherlands},
Author = {Niels Lohmann and H.M.W. Verbeek and Chun Ouyang and Christian Stahl and {Wil} {M.} {P.} {van} {der} {Aalst}},
Institution = {Eindhoven University of Technology},
Month = aug,
Number = {07/23},
Title = {Comparing and Evaluating {Petri} Net Semantics for {BPEL}},
Type = {Computer Science Report},
Year = {2007}
}

Abschlüsse / Theses

Olivia Oanea. Verification of soundness and other properties of business processes. PhD thesis, Department of Mathematics and Computer Science, Eindhoven University of Technology, Eindhoven, The Netherlands, December 2007. [PDF]

@phdthesis{Oanea_2007_phd,
Address = {Eindhoven, The Netherlands},
Author = {Olivia Oanea},
Month = dec,
School = {Department of Mathematics and Computer Science, Eindhoven University of Technology},
Title = {Verification of soundness and other properties of business processes},
Year = {2007}
}

2006

Zeitschriftenartikel / Journal Articles

Lars Michael Kristensen, Karsten Schmidt, and Antii Valmari. Question-Guided Stubborn Set Methods for State Properties. Formal Methods in System Design, 29(3):215-251, November 2006. [DOI]

Abstract. This paper presents two stubborn set methods for alleviating the state explosion problem when reasoning about state properties. The first method makes it possible to determine whether a state of the system is reachable in which a given state predicate holds. The second method makes it possible to determine if from all reachable states it is possible to reach a state where a given state predicate holds. The novelty of the two methods is that they rely on so-called up sets and down sets rather than the notion of visible transitions which causes earlier methods to give only limited reduction of the state space, especially when considering state predicates referring to many of the state variables of the system. The suggested stubborn set methods have been implemented in the LoLA tool, and we report on some experimental results obtained with this computer tool together with some general guidance for applying the two question-guided stubborn set methods and their different implementations in verification. The two methods are presented in the context of Petri Nets, but are applicable also to other state and action oriented modelling formalisms for which the basic stubborn set theory is applicable.

@article{KristensenSV_2006_fmsd,
Abstract = {This paper presents two stubborn set methods for alleviating the state explosion problem when reasoning about state properties. The first method makes it possible to determine whether a state of the system is reachable in which a given state predicate holds. The second method makes it possible to determine if from all reachable states it is possible to reach a state where a given state predicate holds. The novelty of the two methods is that they rely on so-called up sets and down sets rather than the notion of visible transitions which causes earlier methods to give only limited reduction of the state space, especially when considering state predicates referring to many of the state variables of the system. The suggested stubborn set methods have been implemented in the LoLA tool, and we report on some experimental results obtained with this computer tool together with some general guidance for applying the two question-guided stubborn set methods and their different implementations in verification. The two methods are presented in the context of Petri Nets, but are applicable also to other state and action oriented modelling formalisms for which the basic stubborn set theory is applicable.},
Author = {Lars Michael Kristensen and Karsten Schmidt and Antii Valmari},
Journal = {Formal Methods in System Design},
Month = nov,
Number = {3},
Pages = {215-251},
Title = {Question-Guided Stubborn Set Methods for State Properties},
Volume = {29},
Year = 2006,
}

Karsten Wolf. Automated Generation of a Progress Measure for the Sweep-Line Method. STTT, 8(3):195-203, June 2006. [DOI]

Abstract. In the context of Petri nets, we propose an automated construction of a progress measure which is an important pre-requisite for a state space reduction technique called the sweep-line method. Our construction is based on linear-algebraic techniques concerning the transition vectors of the Petri net under consideration. We further discuss the possible combination of the sweep-line method with other state space reduction techniques (partial order reduction, the symmetry method).

@article{Wolf_2007_sttt,
Abstract = {In the context of Petri nets, we propose an automated construction of a progress measure which is an important pre-requisite for a state space reduction technique called the sweep-line method. Our construction is based on linear-algebraic techniques concerning the transition vectors of the Petri net under consideration. We further discuss the possible combination of the sweep-line method with other state space reduction techniques (partial order reduction, the symmetry method).},
Author = {Karsten Wolf},
Journal = {STTT},
Month = jun,
Number = {3},
Pages = {195-203},
Title = {Automated Generation of a Progress Measure for the Sweep-Line Method},
Volume = {8},
Year = {2006},
}

Konferenzbeiträge / Conference Papers

Eike Best, Javier Esparza, Harro Wimmel, and Karsten Wolf. Seperability of Confict-Free Petri Nets. In Irina Virbitskaite and Andrei Voronkov, editors, Perspectives of Systems Informatics, 6th International Andrei Ershov Memorial Conference, PSI 2006, Novosibirsk, Russia, June 27-30, 2006. Revised Papers, volume 4378 of Lecture Notes in Computer Science, pages 1-18, June 2006. Springer-Verlag. [DOI]

Abstract. We study whether transition sequences that transform markings with multiples of a number k on each place can be separated into k sequences, each transforming one k-th of the original marking. We prove that such a separation is possible for marked graph Petri nets, and present an inseparable sequence for a free-choice net.

@inproceedings{BestEWW_2007_psi,
Abstract = {We study whether transition sequences that transform markings with multiples of a number k on each place can be separated into k sequences, each transforming one k-th of the original marking. We prove that such a separation is possible for marked graph Petri nets, and present an inseparable sequence for a free-choice net.},
Author = {Eike Best and Javier Esparza and Harro Wimmel and Karsten Wolf},
Booktitle = {Perspectives of Systems Informatics, 6th International Andrei Ershov Memorial Conference, PSI 2006, Novosibirsk, Russia, June 27-30, 2006. Revised Papers},
Editor = {Irina Virbitskaite and Andrei Voronkov},
Month = jun,
Pages = {1-18},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Seperability of Confict-Free {Petri} Nets},
Volume = {4378},
Year = {2006},
}

Kees van Hee, Irina A. Lomazova, Olivia Oanea, Alexander Serebrenik, Natalia Sidorova, and Marc Voorhoeve. Nested Nets for Adaptive Systems. In Susanna Donatelli and P. S. Thiagarajan, editors, Petri Nets and Other Models of Concurrency - ICATPN 2006, 27th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, Turku, Finland, June 26-30, 2006, Proceedings, volume 4024 of Lecture Notes in Computer Science, pages 241-260, June 2006. Springer-Verlag. [DOI]

Abstract. We consider nested nets, i.e. Petri nets in which tokens can be Petri nets themselves. We study the value semantics of nested nets rather than the reference semantics, and apply nested nets to model adaptive workflow, i.e. flexible workflow that can be modified during the execution. A typical domain with a great need for this kind of workflow is health care, from which domain we choose the running example. To achieve the desired flexibility we allow transitions that create new nets out of the existing ones. Therefore, nets with completely new structure can be created at the run time. We show that by careful selection of basic operations on the nets we can obtain a powerful modeling formalism that enforces correctness of models. Moreover, the formalism can be implemented based on existing workflow engines.

@inproceedings{HeeLOSSV_2006_atpn,
Abstract = {We consider nested nets, i.e. Petri nets in which tokens can be Petri nets themselves. We study the value semantics of nested nets rather than the reference semantics, and apply nested nets to model adaptive workflow, i.e. flexible workflow that can be modified during the execution. A typical domain with a great need for this kind of workflow is health care, from which domain we choose the running example. To achieve the desired flexibility we allow transitions that create new nets out of the existing ones. Therefore, nets with completely new structure can be created at the run time. We show that by careful selection of basic operations on the nets we can obtain a powerful modeling formalism that enforces correctness of models. Moreover, the formalism can be implemented based on existing workflow engines.},
Author = {{Kees} {van} Hee and Irina A. Lomazova and Olivia Oanea and Alexander Serebrenik and Natalia Sidorova and Marc Voorhoeve},
Booktitle = {Petri Nets and Other Models of Concurrency - ICATPN 2006, 27th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, Turku, Finland, June 26-30, 2006, Proceedings},
Editor = {Susanna Donatelli and P. S. Thiagarajan},
Month = jun,
Pages = {241-260},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Nested Nets for Adaptive Systems},
Volume = {4024},
Year = {2006},
}

Kees van Hee, Olivia Oanea, Reinier Post, Lou J. Somers, and Jan Martijn E. M. van der Werf. Yasper: a tool for workflow modeling and analysis. In Sixth International Conference on Application of Concurrency to System Design (ACSD 2006), 28-30 June 2006, Turku, Finland, pages 279-282, June 2006. IEEE Computer Society. [DOI]

Abstract. This paper presents Yasper, a tool for modeling, analyzing and simulating workflow systems, based on Petri nets. Yasper puts Petri net modeling in the hands of business analysts and software architecture designers. They can specify systems in familiar terms (XOR choice, workflow, cases, roles, processing time and cost), and can directly run manual and automatic simulations on the resulting models to analyze correctness and performance. Yasper was designed to cooperate with other tools, such as Petri net analyzers, and off-the-shelf software for data (color) handling and forms handling.

@inproceedings{HeeOPSW_2006_acsd,
Abstract = {This paper presents Yasper, a tool for modeling, analyzing and simulating workflow systems, based on Petri nets. Yasper puts Petri net modeling in the hands of business analysts and software architecture designers. They can specify systems in familiar terms (XOR choice, workflow, cases, roles, processing time and cost), and can directly run manual and automatic simulations on the resulting models to analyze correctness and performance. Yasper was designed to cooperate with other tools, such as Petri net analyzers, and off-the-shelf software for data (color) handling and forms handling.},
Author = {{Kees} {van} Hee and Olivia Oanea and Reinier Post and Lou J. Somers and Jan Martijn E. M. {van} {der} {Werf}},
Booktitle = {Sixth International Conference on Application of Concurrency to System Design (ACSD 2006), 28-30 June 2006, Turku, Finland},
Month = jun,
Pages = {279-282},
Publisher = {IEEE Computer Society},
Title = {Yasper: a tool for workflow modeling and analysis},
Year = {2006},
}

Kees van Hee, Olivia Oanea, Alexander Serebrenik, Natalia Sidorova, and Marc Voorhoeve. History-Based Joins: Semantics, Soundness and Implementation. In Schahram Dustdar, José Luiz Fiadeiro, and Amit P. Sheth, editors, Business Process Management, 4th International Conference, BPM 2006, Vienna, Austria, September 5-7, 2006, Proceedings, volume 4102 of Lecture Notes in Computer Science, pages 225-240, September 2006. Springer-Verlag. [DOI]

Abstract. In this paper we study the use of case history for control structures in workflow processes. In particular we introduce a history-dependent join. History dependent control offers much more modeling power than classical control structures and it solves several semantical problems of industrial modeling frameworks. We study the modeling power by means of workflow patterns. Since proper completion (i.e. the ability of any configuration reachable from the initial one to reach the final one) is always an important ''sanity check'' of process modeling, we introduce a modeling method that guarantees this property for the new control structures. Finally we consider an implementation of the proposed control structures on top of an existing workflow engine.

@inproceedings{HeeOSSV_2006_bpm,
Abstract = {In this paper we study the use of case history for control structures in workflow processes. In particular we introduce a history-dependent join. History dependent control offers much more modeling power than classical control structures and it solves several semantical problems of industrial modeling frameworks. We study the modeling power by means of workflow patterns. Since proper completion (i.e. the ability of any configuration reachable from the initial one to reach the final one) is always an important ''sanity check'' of process modeling, we introduce a modeling method that guarantees this property for the new control structures. Finally we consider an implementation of the proposed control structures on top of an existing workflow engine.},
Author = {{Kees} {van} Hee and Olivia Oanea and Alexander Serebrenik and Natalia Sidorova and Marc Voorhoeve},
Booktitle = {Business Process Management, 4th International Conference, BPM 2006, Vienna, Austria, September 5-7, 2006, Proceedings},
Editor = {Schahram Dustdar and Jos{\'e} Luiz Fiadeiro and Amit P. Sheth},
Month = sep,
Pages = {225-240},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {History-Based Joins: Semantics, Soundness and Implementation},
Volume = {4102},
Year = {2006},
}

Kees van Hee, Olivia Oanea, Alexander Serebrenik, Natalia Sidorova, and Marc Voorhoeve. Modelling History-Dependent Business Processes. In Joseph Barjis, Ulrich Ultes-Nitsche, and Juan Carlos Augusto, editors, Modelling, Simulation, Verification and Validation of Enterprise Information Systems, Proceedings of the 4th International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems, MSVVEIS 2006, In conjunction with ICEIS 2006, Paphos, Cyprus, May 2006, pages 76-85, May 2006. INSTICC Press. [PDF]

Abstract. Choices in business processes are often based on the process history saved as a log-file listing events and their time stamps. In this paper we introduce a finite-path variant of the timed propositional logics with past for specifying guards in business process models. The novelty is due to the introduction of boundary points start and now corresponding to the starting and current observation points. Reasoning in presence of boundary points requires three-valued logics as one needs to distinguish between temporal formulas that hold, those that do not hold and ``unknown'' ones corresponding to ``open cases''. Finally, we extend a sub-language of the logics to take uncertainty into account.

@inproceedings{HeeOSSV_2006_msvveis,
Abstract = {Choices in business processes are often based on the process history saved as a log-file listing events and their time stamps. In this paper we introduce a finite-path variant of the timed propositional logics with past for specifying guards in business process models. The novelty is due to the introduction of boundary points start and now corresponding to the starting and current observation points. Reasoning in presence of boundary points requires three-valued logics as one needs to distinguish between temporal formulas that hold, those that do not hold and ``unknown'' ones corresponding to ``open cases''. Finally, we extend a sub-language of the logics to take uncertainty into account.},
Author = {{Kees} {van} Hee and Olivia Oanea and Alexander Serebrenik and Natalia Sidorova and Marc Voorhoeve},
Booktitle = {Modelling, Simulation, Verification and Validation of Enterprise Information Systems, Proceedings of the 4th International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems, MSVVEIS 2006, In conjunction with ICEIS 2006, Paphos, Cyprus, May 2006},
Editor = {Joseph Barjis and Ulrich Ultes-Nitsche and Juan Carlos Augusto},
Month = may,
Pages = {76-85},
Publisher = {INSTICC Press},
Title = {Modelling History-Dependent Business Processes},
Year = {2006}
}

Kees van Hee, Olivia Oanea, Alexander Serebrenik, Natalia Sidorova, Marc Voorhoeve, and Irina A. Lomazova. Checking Properties of Adaptive Workflow Nets. In Proceedings Concurrency Specification and Programming (CS&P'2006, Wandlitz, Germany, September 27-29, 2006), pages 92-103, September 2006. [PDF]

Abstract. In this paper we consider adaptive workflow nets, a subclass of nested nets that allows more comfort and expressive power for modelling adaptation and exception handling in workflow nets. We define two important behavioral properties of adaptive workflow nets: soundness and circumspectness. Soundness means that a proper final marking (state) can be reached from any marking which is reachable from the initial marking, and no garbage will be left. Circumspectness means that the upper layer is always ready to handle any exception that can happen in a lower layer. Since adaptive workflow nets can have an infinite state space, we use an abstraction to reduce the problem of verifying soundness and circumspectness to a finite one.

@inproceedings{HeeOSSVL_2006_csp,
Abstract = {In this paper we consider adaptive workflow nets, a subclass of nested nets that allows more comfort and expressive power for modelling adaptation and exception handling in workflow nets. We define two important behavioral properties of adaptive workflow nets: soundness and circumspectness. Soundness means that a proper final marking (state) can be reached from any marking which is reachable from the initial marking, and no garbage will be left. Circumspectness means that the upper layer is always ready to handle any exception that can happen in a lower layer. Since adaptive workflow nets can have an infinite state space, we use an abstraction to reduce the problem of verifying soundness and circumspectness to a finite one.},
Author = {{Kees} {van} Hee and Olivia Oanea and Alexander Serebrenik and Natalia Sidorova and Marc Voorhoeve and Irina A. Lomazova},
Booktitle = {Proceedings Concurrency Specification and Programming (CS\&P'2006, Wandlitz, Germany, September 27-29, 2006)},
Month = sep,
Pages = {92-103},
Title = {Checking Properties of Adaptive Workflow Nets},
Year = {2006}
}

Kathrin Kaschner, Peter Massuthe, and Karsten Wolf. Symbolische Repräsentation von Bedienungsanleitungen für Services. In Daniel Moldt, editor, Tagungsband des 13. Workshops Algorithmen und Werkzeuge für Petri-Netze, AWPN'06, pages 54-61, September 2006. Universität Hamburg. Appeared as Bericht FBI-HH-B-267. [PDF]

@inproceedings{KaschnerMW_2006_awpn,
Author = {Kathrin Kaschner and Peter Massuthe and Karsten Wolf},
Booktitle = {Tagungsband des 13. Workshops Algorithmen und Werkzeuge f{\"u}r Petri-Netze, AWPN'06},
Editor = {Daniel Moldt},
Month = sep,
Note = {Appeared as Bericht FBI-HH-B-267},
Pages = {54-61},
Publisher = {Universit{\"a}t Hamburg},
Title = {{Symbolische Repr{\"a}sentation von Bedienungsanleitungen f{\"u}r Services}},
Year = 2006
}

Oliver Kopp, Carsten Frenkler, and Niels Lohmann. Korrektheit und Zuverlässigkeit zusammengesetzter Web Services am Beispiel der Geschäftsprozess-Modellierungssprache BPEL. In Forschungsoffensive ``Software Engineering 2006'', Statuskonferenz, 26.-28. Juni 2006, July 2006. Bundesministerium für Bildung und Forschung (BMBF). [PDF]

Abstract. Unternehmens{\"u}bergreifende Gesch{\"a}ftsprozesse werden zunehmend nach dem Paradigma der Services organisiert. Dabei stellen sich Fragen nach der Komponierbarkeit, Bedienbarkeit, Austauschbarkeit sowie der R{\"u}cksetzbarkeit (Kompensation) im Fehlerfall. In diesem Vorhaben werden Methoden und Werkzeuge zum Umgang mit solchen Fragen entwickelt, am Beispiel der Gesch{\"a}ftsprozess-Modellierungssprache BPEL erprobt und in ein Entwurfswerkzeug der Firma Gedilan Technologies integriert.

@inproceedings{KoppFL_2006_bmbf,
Abstract = {Unternehmens{\"u}bergreifende Gesch{\"a}ftsprozesse werden zunehmend nach dem Paradigma der Services organisiert. Dabei stellen sich Fragen nach der Komponierbarkeit, Bedienbarkeit, Austauschbarkeit sowie der R{\"u}cksetzbarkeit (Kompensation) im Fehlerfall. In diesem Vorhaben werden Methoden und Werkzeuge zum Umgang mit solchen Fragen entwickelt, am Beispiel der Gesch{\"a}ftsprozess-Modellierungssprache BPEL erprobt und in ein Entwurfswerkzeug der Firma Gedilan Technologies integriert.},
Author = {Oliver Kopp and Carsten Frenkler and Niels Lohmann},
Booktitle = {Forschungsoffensive ``Software Engineering 2006'', Statuskonferenz, 26.-28. Juni 2006},
Month = jul,
Publisher = {Bundesministerium f{\"u}r Bildung und Forschung (BMBF)},
Title = {{Korrektheit und Zuverl{\"a}ssigkeit zusammengesetzter Web Services am Beispiel der Gesch{\"a}ftsprozess-Modellierungssprache BPEL}},
Year = {2006}
}

Niels Lohmann. A Local Cut-off Criterion for Unfoldings of Safe Petri Nets. In Jörg Desel, editor, Proceedings of the Doctoral Consortium ACSD & Petri Nets 2006, Turku, Finland, June 2006. Åbo Academy. [PDF]

Abstract. Finite prefixes of branching processes are a compact way to represent the state space of finite safe systems. McMillan in [1] formulated a cut-off criterion stating under which conditions the (usually infinite) maximal branching process can be truncated without loosing reachable markings. However, this criterion depends on the reachable markings itself and thus suffers the state explosion problem. In this work, we propose local cut-off criteria that base on partial markings.

@inproceedings{Lohmann_2006_atpndc,
Abstract = {Finite prefixes of branching processes are a compact way to represent the state space of finite safe systems. McMillan in [1] formulated a cut-off criterion stating under which conditions the (usually infinite) maximal branching process can be truncated without loosing reachable markings. However, this criterion depends on the reachable markings itself and thus suffers the state explosion problem. In this work, we propose local cut-off criteria that base on partial markings.},
Address = {Turku, Finland},
Author = {Niels Lohmann},
Booktitle = {Proceedings of the Doctoral Consortium ACSD {\&} Petri Nets 2006},
Editor = {J{\"o}rg Desel},
Month = jun,
Publisher = {{\AA}bo Academy},
Title = {A Local Cut-off Criterion for Unfoldings of Safe {Petri} Nets},
Year = 2006
}

Niels Lohmann, Peter Massuthe, Christian Stahl, and Daniela Weinberg. Analyzing Interacting BPEL Processes. In Schahram Dustdar, José Luiz Fiadeiro, and Amit P. Sheth, editors, Business Process Management, 4th International Conference, BPM 2006, Vienna, Austria, September 5-7, 2006, Proceedings, volume 4102 of Lecture Notes in Computer Science, pages 17-32, September 2006. Springer-Verlag. [PDF] [DOI]

Abstract. This paper addresses the problem of analyzing theinteraction between BPEL processes. We present a technology chain that starts out with a BPEL process and transforms it into a Petri net model. On the model we decide controllability of the process (the existence of a partner process, such that both can interact properly) and compute its operating guideline (a characterization of all properly interacting partner processes). A case study demonstrates the value of this technology chain.

@inproceedings{LohmannMSW_2006_bpm,
Abstract = {This paper addresses the problem of analyzing theinteraction between BPEL processes. We present a technology chain that starts out with a BPEL process and transforms it into a Petri net model. On the model we decide controllability of the process (the existence of a partner process, such that both can interact properly) and compute its operating guideline (a characterization of all properly interacting partner processes). A case study demonstrates the value of this technology chain.},
Author = {Niels Lohmann and Peter Massuthe and Christian Stahl and Daniela Weinberg},
Booktitle = {Business Process Management, 4th International Conference, BPM 2006, Vienna, Austria, September 5-7, 2006, Proceedings},
Editor = {Schahram Dustdar and Jos{\'e} Luiz Fiadeiro and Amit P. Sheth},
Month = sep,
Pages = {17-32},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Analyzing Interacting {BPEL} Processes},
Volume = 4102,
Year = 2006,
}

Mirjam Minor and Karsten Schmidt. Automatic Transformation and Enlargement of Similarity Models for Case-Based Reasoning. In Heinrich C. Mayr and Ruth Breu, editors, Modellierung 2006, 22.-24. März 2006, Innsbruck, Tirol, Austria, Proceedings, volume P-82 of Lecture Notes in Informatics (LNI), pages 293-296, March 2006. GI. [PDF]

@inproceedings{MinorS_2006_mod,
Author = {Mirjam Minor and Karsten Schmidt},
Booktitle = {Modellierung 2006, 22.-24. M{\"a}rz 2006, Innsbruck, Tirol, Austria, Proceedings},
Editor = {Heinrich C. Mayr and Ruth Breu},
Month = mar,
Pages = {293-296},
Publisher = {GI},
Series = {Lecture Notes in Informatics (LNI)},
Title = {Automatic Transformation and Enlargement of Similarity Models for Case-Based Reasoning},
Volume = {P-82},
Year = {2006}
}

Wolfgang Reisig, Dirk Fahland, Niels Lohmann, Peter Massuthe, Christian Stahl, Daniela Weinberg, Karsten Wolf, and Kathrin Kaschner. Analysis Techniques for Service Models. In Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, 2006 (ISoLA 2006), 15-19 November 2006, Paphos, Cyprus, pages 11-17, November 2006. IEEE Computer Society. [PDF] [DOI]

Abstract. The paradigm of Service-Oriented Computing (SOC) provides a framework for interorganizational business processes and for the emerging programming-in-the-large. The basic idea of SOC, the interaction of services, rises a lot of issues such as proper termination of interacting services or substitution of a service by another one. Such issues can be addressed by means of models of services. We show how services can intelligibly be modeled, and we present algorithms and tools to analyze properties of service models. To make sure that our models properly reflect real world issues of services, we model and investigate services represented in established languages such as WS-BPEL.

@inproceedings{ReisigFLMSWWK_2006_isola,
Abstract = {The paradigm of Service-Oriented Computing (SOC) provides a framework for interorganizational business processes and for the emerging programming-in-the-large. The basic idea of SOC, the interaction of services, rises a lot of issues such as proper termination of interacting services or substitution of a service by another one. Such issues can be addressed by means of models of services. We show how services can intelligibly be modeled, and we present algorithms and tools to analyze properties of service models. To make sure that our models properly reflect real world issues of services, we model and investigate services represented in established languages such as WS-BPEL.},
Author = {Wolfgang Reisig and Dirk Fahland and Niels Lohmann and Peter Massuthe and Christian Stahl and Daniela Weinberg and Karsten Wolf and Kathrin Kaschner},
Booktitle = {Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, 2006 (ISoLA 2006), 15-19 November 2006, Paphos, Cyprus},
Month = nov,
Pages = {11-17},
Publisher = {IEEE Computer Society},
Title = {Analysis Techniques for Service Models},
Year = 2006,
}

Stephan Roch and Karsten Schmidt. On the Step Explosion Problem. In Susanna Donatelli and P. S. Thiagarajan, editors, Petri Nets and Other Models of Concurrency -- ICATPN 2006, 27th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, Turku, Finland, June 26--30, 2006, Proceedings, volume 4024 of Lecture Notes in Computer Science, pages 342-361, June 2006. Springer-Verlag. [DOI]

Abstract. In many well-known extensions of place-transition nets, including read arcs, inhibitory arcs, reset arcs, priorities and signal arcs, it is sometimes possible to reach a marking through firing a step of transitions which cannot be reached through firing a sequence of single transitions. For state space analysis, it is thus recommendable to consider, in each state, all steps of transitions for firing. Since the number of activated steps may be exponential in the number of transitions, we have, in addition to the well-known state explosion problem, another explosion which we call step explosion. In this paper, we present an approach for alleviating step explosion. We furthermore discuss the joint application of our method with partial order reduction and in the context of CTL model checking.

@inproceedings{RochS_2006_icatpn,
Abstract = {In many well-known extensions of place-transition nets, including read arcs, inhibitory arcs, reset arcs, priorities and signal arcs, it is sometimes possible to reach a marking through firing a step of transitions which cannot be reached through firing a sequence of single transitions. For state space analysis, it is thus recommendable to consider, in each state, all steps of transitions for firing. Since the number of activated steps may be exponential in the number of transitions, we have, in addition to the well-known state explosion problem, another explosion which we call step explosion. In this paper, we present an approach for alleviating step explosion. We furthermore discuss the joint application of our method with partial order reduction and in the context of CTL model checking.},
Author = {Stephan Roch and Karsten Schmidt},
Booktitle = {Petri Nets and Other Models of Concurrency -- ICATPN 2006, 27th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, Turku, Finland, June 26--30, 2006, Proceedings},
Editor = {Susanna Donatelli and P. S. Thiagarajan},
Month = jun,
Pages = {342-361},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {On the Step Explosion Problem},
Volume = 4024,
Year = 2006,
}

Technische Berichte / Technical Reports

Kees van Hee, Irina A. Lomazova, Olivia Oanea, Alexander Serebrenik, Natalia Sidorova, and Marc Voorhoeve. Nested Nets for Adaptive Systems. Computer Science Report 06/02, Eindhoven University of Technology, Eindhoven, The Netherlands, 2006. [PDF]

Abstract. We improve the decision procedure from [7] for the problem of generalized soundness for workflow nets: \Every marking reachable from an initial marking with k tokens on the initial place terminates properly, i.e. it can reach a marking with k tokens on the final place, for an arbitrary natural number k". Moreover, our new decision procedure returns a counterexample in case the workflow net is not generalized sound. We also report on experimental results obtained with the prototype we made and explain how the procedure can be used for the compositional verification of large workflows.

@techreport{HeeLOSSV_2006_tr0602,
}

Kees van Hee, Olivia Oanea, Natalia Sidorova, and Marc Voorhoeve. Verifying Generalized Soundness for Workflow Nets. Computer Science Report 06/08, Eindhoven University of Technology, Eindhoven, The Netherlands, 2006. [PDF]

Abstract. We consider nested nets, i.e. Petri nets in which tokens can be Petri nets themselves. We study value semantics of nested nets rather than reference semantics, and apply nested nets to model adaptive workflow, i.e. flexible workflow that can be modified during the execution. A typical domain with a great need for this kind of workflow is health care from which domain we choose the running example. To achieve the desired flexibility we allow transitions that create new nets out of the existing ones. Therefore, nets with completely new structure can be created at the run time. We show that by careful selection of basic operations on the nets we can obtain a powerful modeling formalism that enforces correctness of models. Moreover, the formalism can be implemented based on existing workflow engines.

@techreport{HeeOSV_2006_tr0608,
Abstract = {We consider nested nets, i.e. Petri nets in which tokens can be Petri nets themselves. We study value semantics of nested nets rather than reference semantics, and apply nested nets to model adaptive workflow, i.e. flexible workflow that can be modified during the execution. A typical domain with a great need for this kind of workflow is health care from which domain we choose the running example. To achieve the desired flexibility we allow transitions that create new nets out of the existing ones. Therefore, nets with completely new structure can be created at the run time. We show that by careful selection of basic operations on the nets we can obtain a powerful modeling formalism that enforces correctness of models. Moreover, the formalism can be implemented based on existing workflow engines.},
Address = {Eindhoven, The Netherlands},
Author = {{Kees} {van} Hee and Olivia Oanea and Natalia Sidorova and Marc Voorhoeve},
Institution = {Eindhoven University of Technology},
Number = {06/08},
Title = {Verifying Generalized Soundness for Workflow Nets},
Type = {Computer Science Report},
Year = {2006}
}

Niels Lohmann, Peter Massuthe, and Karsten Wolf. Operating Guidelines for Finite-State Services. Informatik-Berichte 210, Humboldt-Universität zu Berlin, Berlin, Germany, December 2006. [PDF]

Abstract. We introduce the concept of an operating guideline for an arbitrary finite-state service P, extending the work of [1, 2] which was restricted to acyclic services. An operating guideline gives complete information about how to correctly (in this paper: deadlock-free) communicate with P. It can further be executed or used for service discovery. An operating guideline for P is a particular service S that is enriched with annotations. S communicates deadlock-free with P and is able to simulate every other service that communicates deadlock-free with P. The attached annotations give complete information about whether or not a simulated service is deadlock-free, too.

@techreport{LohmannMW2006_hub_tr210,
Abstract = {We introduce the concept of an operating guideline for an arbitrary finite-state service P, extending the work of [1, 2] which was restricted to acyclic services. 

An operating guideline gives complete information about how to correctly (in this paper: deadlock-free) communicate with P. It can further be executed or used for service discovery. 

An operating guideline for P is a particular service S that is enriched with annotations. S communicates deadlock-free with P and is able to simulate every other service that communicates deadlock-free with P. The attached annotations give complete information about whether or not a simulated service is deadlock-free, too.},
Address = {Berlin, Germany},
Author = {Niels Lohmann and Peter Massuthe and Karsten Wolf},
Institution = {Humboldt-Universit{\"a}t zu Berlin},
Month = dec,
Number = 210,
Title = {Operating Guidelines for Finite-State Services},
Type = {Informatik-Berichte},
Year = 2006
}

Abschlüsse / Theses

Kathrin Kaschner. BDD-basiertes Matching von Services. Diplomarbeit, Humboldt-Universität zu Berlin, Institut für Informatik, Berlin, Germany, March 2006. [PDF]

Abstract. Moderne Software-Systeme werden zunehmend nach dem Paradigma der Serviceorientierten Architektur (SOA) aus unabh{\"a}ngigen Services zusammengesetzt, die definierte Funktionen zur Verf{\"u}gung stellen und Nachrichten miteinander austauschen. Eine M{\"o}glichkeit zur Gew{\"a}hrleistung der reibungslosen Kommunikation besteht in der Bereitstellung einer Bedienungsanleitung durch den Service Provider, mit der der Service Broker anhand eines Pr{\"u}fverfahrens - dem Matching -- entscheiden kann, ob der Service eines Service Requesters zu dem angebotenen Service passt. F{\"u}r die praktische Anwendung m{\"u}ssen Bedienungsanleitungen in geeigneter Weise kodiert werden. In der vorliegenden Arbeit werden dazu Bin{\"a}re Entscheidungsdiagramme (BDDs) genutzt. F{\"u}r das Matching wird der Service des Service Requesters durch einen Serviceautomaten modelliert, der seinerseits ebenfalls in eine BDD-Darstellung {\"u}berf{\"u}hrt wird. Darauf aufbauend wird schlie{\ss}lich ein Matching-Algorithmus entwickelt und seine Korrektheit bewiesen. Die Effizienz der Kodierung durch BDDs und die Funktionsweise des BDD-basierten Matching-Algorithmus wird an Beispielen gezeigt.

@mastersthesis{Kaschner_2006_da,
Abstract = {Moderne Software-Systeme werden zunehmend nach dem Paradigma der Serviceorientierten Architektur (SOA) aus unabh{\"a}ngigen Services zusammengesetzt, die definierte Funktionen zur Verf{\"u}gung stellen und Nachrichten miteinander austauschen. Eine M{\"o}glichkeit zur Gew{\"a}hrleistung der reibungslosen Kommunikation besteht in der Bereitstellung einer Bedienungsanleitung durch den Service Provider, mit der der Service Broker anhand eines Pr{\"u}fverfahrens - dem Matching -- entscheiden kann, ob der Service eines Service Requesters zu dem angebotenen Service passt. F{\"u}r die praktische Anwendung m{\"u}ssen Bedienungsanleitungen in geeigneter Weise kodiert werden. In der vorliegenden Arbeit werden dazu Bin{\"a}re Entscheidungsdiagramme (BDDs) genutzt. F{\"u}r das Matching wird der Service des Service Requesters durch einen Serviceautomaten modelliert, der seinerseits ebenfalls in eine BDD-Darstellung {\"u}berf{\"u}hrt wird. Darauf aufbauend wird schlie{\ss}lich ein Matching-Algorithmus entwickelt und seine Korrektheit bewiesen. Die Effizienz der Kodierung durch BDDs und die Funktionsweise des BDD-basierten Matching-Algorithmus wird an Beispielen gezeigt.},
Address = {Berlin, Germany},
Author = {Kathrin Kaschner},
Month = mar,
School = {Humboldt-Universit{\"a}t zu Berlin, Institut f{\"u}r Informatik},
Title = {{BDD-basiertes Matching von Services}},
Type = {Diplomarbeit},
Year = 2006
}

Kathrin Kaschner. Repräsentation von Bedienungsanleitungen durch BDDs. Studienarbeit, Humboldt-Universität zu Berlin, Institut für Informatik, Berlin, Germany, January 2006. [PDF]

@mastersthesis{Kaschner_2006_sa,
Address = {Berlin, Germany},
Author = {Kathrin Kaschner},
Month = jan,
School = {Humboldt-Universit{\"a}t zu Berlin, Institut f{\"u}r Informatik},
Title = {{Repr{\"a}sentation von Bedienungsanleitungen durch BDDs}},
Type = {Studienarbeit},
Year = 2006
}

2005

Zeitschriftenartikel / Journal Articles

Peter Massuthe, Wolfgang Reisig, and Karsten Schmidt. An Operating Guideline Approach to the SOA. AMCT, 1(3):35-43, 2005. [PDF]

Abstract. Interorganizational cooperation is more andmore organized by the paradigm of services. The serviceorientedarchitecture (SOA) provides a general frameworkfor service interaction. It describes three roles, serviceprovider, service requester, and service broker, togetherwith the three operations publish, find, and bind.We provide a formal method based on Petri nets tomodel services and their cooperation. We characterizewell-behaving pairs of requester's and provider's servicesand suggest operating guidelines as a convenient andintuitive artifact to realize publish. In our approach, thefind operation reduces to a matching problem between therequester's service and the operating guideline. Binding ofa requester's and a provider's service is therefore guaranteedto result in a well-behaving cooperating service. Atthis time, the approach is limited to acyclic Petri nets.

@article{MassutheRS_2005_amct,
Abstract = {Interorganizational cooperation is more andmore organized by the paradigm of services. The serviceorientedarchitecture (SOA) provides a general frameworkfor service interaction. It describes three roles, serviceprovider, service requester, and service broker, togetherwith the three operations publish, find, and bind.We provide a formal method based on Petri nets tomodel services and their cooperation. We characterizewell-behaving pairs of requester's and provider's servicesand suggest operating guidelines as a convenient andintuitive artifact to realize publish. In our approach, thefind operation reduces to a matching problem between therequester's service and the operating guideline. Binding ofa requester's and a provider's service is therefore guaranteedto result in a well-behaving cooperating service. Atthis time, the approach is limited to acyclic Petri nets.},
Author = {Peter Massuthe and Wolfgang Reisig and Karsten Schmidt},
Journal = {AMCT},
Number = 3,
Pages = {35-43},
Title = {An Operating Guideline Approach to the {SOA}},
Volume = 1,
Year = 2005
}

Wolfgang Reisig, Karsten Schmidt, and Christian Stahl. Kommunizierende Workflow-Services modellieren und analysieren. Inform., Forsch. Entwickl., 20(1-2):90-101, October 2005. [DOI]

Abstract. Zur ad{\"a}quaten Nutzung von Workflow-Implementierungen kommunizierender Gesch{\"a}ftsprozesse werden Konzepte vorgeschlagen, die von konkreten Implementierungen abstrahieren. Auf der Basis von Petrinetzen werden unterschiedliche Varianten der Bedienbarkeit von Workflows charakterisiert und daf{\"u}r Entscheidungsalgorithmen vorgestellt. Die Angemessenheit des Ansatzes wird am Beispiel der Semantik von Komponenten der Gesch{\"a}ftsprozess-Modellierungssprache BPEL demonstriert.

@article{ReisigSS_2005_ife,
Abstract = {Zur ad{\"a}quaten Nutzung von Workflow-Implementierungen kommunizierender Gesch{\"a}ftsprozesse werden Konzepte vorgeschlagen, die von konkreten Implementierungen abstrahieren. Auf der Basis von Petrinetzen werden unterschiedliche Varianten der Bedienbarkeit von Workflows charakterisiert und daf{\"u}r Entscheidungsalgorithmen vorgestellt. Die Angemessenheit des Ansatzes wird am Beispiel der Semantik von Komponenten der Gesch{\"a}ftsprozess-Modellierungssprache BPEL demonstriert.},
Author = {Wolfgang Reisig and Karsten Schmidt and Christian Stahl},
Journal = {Inform., Forsch. Entwickl.},
Month = oct,
Number = {1-2},
Pages = {90-101},
Title = {{Kommunizierende Workflow-Services modellieren und analysieren}},
Volume = {20},
Year = 2005,
}

Bernd-Holger Schlingloff, Axel Martens, and Karsten Schmidt. Modeling and Model Checking Web Services. Electr. Notes Theor. Comput. Sci., 126:3-26, March 2005. [DOI]

Abstract. We give an overview on web services and the web service technology stack. We then show how to build Petri net models of web services formulated in the specification language BPEL4WS. We define an abstract correctness criterion for these models and study the automated verification according to this criterion. Finally, we relate correctness of web service models to the model checking problem for alternating temporal logics.

@article{SchlingloffMS_2005_entcs,
Abstract = {We give an overview on web services and the web service technology stack. We then show how to build Petri net models of web services formulated in the specification language BPEL4WS. We define an abstract correctness criterion for these models and study the automated verification according to this criterion. Finally, we relate correctness of web service models to the model checking problem for alternating temporal logics.},
Author = {Bernd-Holger Schlingloff and Axel Martens and Karsten Schmidt},
Journal = {Electr. Notes Theor. Comput. Sci.},
Month = mar,
Pages = {3-26},
Title = {Modeling and Model Checking {Web} Services},
Volume = 126,
Year = 2005,
}

Konferenzbeiträge / Conference Papers

Carsten Frenkler and Karsten Schmidt. Modellierung und Analyse transaktionaler Geschäftsprozesse. In Karsten Schmidt and Christian Stahl, editors, 12. Workshop ``Algorithmen und Werkzeuge für Petrinetze'' (AWPN 2005), Proceedings, pages 72-77, September 2005. Humboldt-Universität zu Berlin. Appeared as Informatik-Berichte Nr. 192. [PDF]

Abstract. Wie erweitern in dieser Arbeit Workflow-Module um ein Konzept, mit dem derEinflu{\ss} eines Datenbanksystems auf die Bedienbarkeit eines Gesch{\"a}ftsprozesses untersucht werden kann. Wir integrieren transaktionale Eigenschaften als internes Verhalten in Workflow-Module und k{\"o}nnen damit Bedienbarkeit und Einhaltung transaktionaler Eigenschaften durch Analyse entscheiden.

@inproceedings{FrenklerS_2005_awpn,
Abstract = {Wie erweitern in dieser Arbeit Workflow-Module um ein Konzept, mit dem derEinflu{\ss} eines Datenbanksystems auf die Bedienbarkeit eines Gesch{\"a}ftsprozesses untersucht werden kann. Wir integrieren transaktionale Eigenschaften als internes Verhalten in Workflow-Module und k{\"o}nnen damit Bedienbarkeit und Einhaltung transaktionaler Eigenschaften durch Analyse entscheiden.},
Author = {Carsten Frenkler and Karsten Schmidt},
Booktitle = {12. Workshop ``Algorithmen und Werkzeuge f{\"u}r Petrinetze'' (AWPN 2005), Proceedings},
Editor = {Karsten Schmidt and Christian Stahl},
Month = sep,
Note = {Appeared as Informatik-Berichte Nr. 192},
Pages = {72-77},
Publisher = {Humboldt-Universit{\"a}t zu Berlin},
Title = {{Modellierung und Analyse transaktionaler Gesch{\"a}ftsprozesse}},
Year = 2005
}

Kees van Hee, Olivia Oanea, and Natalia Sidorova. Colored Petri Nets to Verify Extended Event-Driven Process Chains. In Robert Meersman, Zahir Tari, Mohand-Said Hacid, John Mylopoulos, Barbara Pernici, Özalp Babaoglu, Hans-Arno Jacobsen, Joseph P. Loyall, Michael Kifer, and Stefano Spaccapietra, editors, On the Move to Meaningful Internet Systems 2005: CoopIS, DOA, and ODBASE, OTM Confederated International Conferences CoopIS, DOA, and ODBASE 2005, Agia Napa, Cyprus, October 31 - November 4, 2005, Proceedings, Part I, volume 3760 of Lecture Notes in Computer Science, pages 183-201, October 2005. Springer-Verlag. [PDF] [DOI]

Abstract. Business processes are becoming more and more complex and at the same time their correctness is becoming a critical issue: The costs of errors in business information systems are growing due to the growing scale of their application and the growing degree of automation. In this paper we consider Extended Event-driven Process Chains (eEPCs), a language which is widely used for modeling business processes, documenting industrial reference models and designing workflows. We describe how to translate eEPCs into timed colored Petri nets in order to verify processes given by eEPCs with the CPN Tools.

@inproceedings{HeeOS_2005_otm,
Abstract = {Business processes are becoming more and more complex and at the same time their correctness is becoming a critical issue: The costs of errors in business information systems are growing due to the growing scale of their application and the growing degree of automation. In this paper we consider Extended Event-driven Process Chains (eEPCs), a language which is widely used for modeling business processes, documenting industrial reference models and designing workflows. We describe how to translate eEPCs into timed colored Petri nets in order to verify processes given by eEPCs with the CPN Tools.},
Author = {{Kees} {van} Hee and Olivia Oanea and Natalia Sidorova},
Booktitle = {On the Move to Meaningful Internet Systems 2005: CoopIS, DOA, and ODBASE, OTM Confederated International Conferences CoopIS, DOA, and ODBASE 2005, Agia Napa, Cyprus, October 31 - November 4, 2005, Proceedings, Part I},
Editor = {Robert Meersman and Zahir Tari and Mohand-Said Hacid and John Mylopoulos and Barbara Pernici and {\"O}zalp Babaoglu and Hans-Arno Jacobsen and Joseph P. Loyall and Michael Kifer and Stefano Spaccapietra},
Month = oct,
Pages = {183-201},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Colored {Petri} Nets to Verify Extended Event-Driven Process Chains},
Volume = {3760},
Year = {2005},
}

Sebastian Hinz, Karsten Schmidt, and Christian Stahl. Transforming BPEL to Petri Nets. In Wil M. P. van der Aalst, B. Benatallah, F. Casati, and F. Curbera, editors, Proceedings of the Third International Conference on Business Process Management (BPM 2005), volume 3649 of Lecture Notes in Computer Science, pages 220-235, September 2005. Springer-Verlag. [PDF] [DOI]

Abstract. We present a Petri net semantics for the Business Process Execution Language for Web Services (BPEL). Our semantics covers the standard behaviour of BPEL as well as the exceptional behaviour (e.g. faults, events, compensation). The semantics is implemented as a parser that translates BPEL specifications into the input language of the Petri net model checking tool LoLA. We demonstrate that the semantics is well suited for computer aided verification purposes.

@inproceedings{HinzSS_2005_bpm,
Abstract = {We present a Petri net semantics for the Business Process Execution Language for Web Services (BPEL). Our semantics covers the standard behaviour of BPEL as well as the exceptional behaviour (e.g. faults, events, compensation). The semantics is implemented as a parser that translates BPEL specifications into the input language of the Petri net model checking tool LoLA. We demonstrate that the semantics is well suited for computer aided verification purposes.},
Author = {Sebastian Hinz and Karsten Schmidt and Christian Stahl},
Booktitle = {Proceedings of the Third International Conference on Business Process Management (BPM 2005)},
Editor = {{Wil} {M.} {P.} {van} {der} Aalst and B. Benatallah and F. Casati and F. Curbera},
Month = sep,
Pages = {220-235},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Transforming {BPEL} to {Petri} Nets},
Volume = 3649,
Year = 2005,
}

Peter Massuthe, Wolfgang Reisig, and Karsten Schmidt. An Operating Guideline Approach to the SOA. In 2nd South-East European Workshop on Formal Methods 2005 (SEEFM05), 18-19 November 2005, Ohrid, Republic of Macedonia, 2005. SEERC. [PDF]

@inproceedings{MassutheRS_2005_seefm,
Author = {Peter Massuthe and Wolfgang Reisig and Karsten Schmidt},
Booktitle = {2nd South-East European Workshop on Formal Methods 2005 (SEEFM05), 18-19 November 2005, Ohrid, Republic of Macedonia},
Publisher = {SEERC},
Title = {An Operating Guideline Approach to the {SOA}},
Year = {2005}
}

Peter Massuthe and Karsten Schmidt. Operating Guidelines -- an Automata-Theoretic Foundation for the Service-Oriented Architecture. In Kai-Yuan Cai, Atsushi Ohnishi, and M.F. Lau, editors, Fifth International Conference on Quality Software (QSIC 2005), 19-20 September 2005, Melbourne, Australia, pages 452-457, September 2005. IEEE Computer Society. [PDF] [DOI]

Abstract. In the service-oriented architecture (SOA), we distinguish three roles of service owners: service providers, service requesters, and service brokers. Each service provider publishes information to the broker about how requesters can interact with its service. Thus, the broker can assign a fitting service provider to a querying requester. We propose the information published to the broker to be operating guidelines. Operating guidelines are essentially communication instructions for the service requester. We present an automata-theoretic approach that is centered around operating guidelines and is capable of implementing all tasks arising in the SOA.

@inproceedings{MassutheS_2005_qsic,
Abstract = {In the service-oriented architecture (SOA), we distinguish three roles of service owners: service providers, service requesters, and service brokers. Each service provider publishes information to the broker about how requesters can interact with its service. Thus, the broker can assign a fitting service provider to a querying requester. We propose the information published to the broker to be operating guidelines. Operating guidelines are essentially communication instructions for the service requester. We present an automata-theoretic approach that is centered around operating guidelines and is capable of implementing all tasks arising in the SOA.},
Author = {Peter Massuthe and Karsten Schmidt},
Booktitle = {Fifth International Conference on Quality Software (QSIC 2005), 19-20 September 2005, Melbourne, Australia},
Editor = {Kai-Yuan Cai and Atsushi Ohnishi and M.F. Lau},
Month = sep,
Pages = {452-457},
Publisher = {IEEE Computer Society},
Title = {Operating Guidelines -- an Automata-Theoretic Foundation for the Service-Oriented Architecture},
Year = 2005,
}

Peter Massuthe and Karsten Schmidt. Operating Guidelines for Services. In Karsten Schmidt and Christian Stahl, editors, 12. Workshop ``Algorithmen und Werkzeuge für Petrinetze'' (AWPN 2005), Proceedings, pages 78-83, September 2005. Humboldt-Universität zu Berlin. Appeared as Informatik-Berichte Nr. 192. [PDF]

Abstract. In the service-oriented architecture (SOA), we distinguish three roles of service owners:service providers, service requesters, and service brokers, and the three standard operations publish, find, and bind. We provide a formal method based on Petri nets to model services. We suggest operating guidelines as a convenient and intuitive artifact to realize publish. Then, the find operation reduces to a matching problem between the requester?s service and the operating guideline.

@inproceedings{MassutheS_2005_awpn,
Abstract = {In the service-oriented architecture (SOA), we distinguish three roles of service owners:service providers, service requesters, and service brokers, and the three standard operations publish, find, and bind. We provide a formal method based on Petri nets to model services. We suggest operating guidelines as a convenient and intuitive artifact to realize publish. Then, the find operation reduces to a matching problem between the requester?s service and the operating guideline.},
Author = {Peter Massuthe and Karsten Schmidt},
Booktitle = {12. Workshop ``Algorithmen und Werkzeuge f{\"u}r Petrinetze'' (AWPN 2005), Proceedings},
Editor = {Karsten Schmidt and Christian Stahl},
Month = sep,
Note = {Appeared as Informatik-Berichte Nr. 192},
Pages = {78-83},
Publisher = {Humboldt-Universit{\"a}t zu Berlin},
Title = {Operating Guidelines for Services},
Year = 2005
}

Karsten Schmidt. Controllability of Open Workflow Nets. In Jörg Desel and Ulrich Frank, editors, Enterprise Modelling and Information Systems Architectures, Proceedings of the Workshop in Klagenfurt, October 24-25, 2005, volume P-75 of Lecture Notes in Informatics (LNI), pages 236-249, 2005. GI. [PDF]

Abstract. An open workflow net is basically a workflow net extended with a message passing interface. Open workflow nets are adequate models for services or parts of inter-organizational business processes. We investigate the problem of control lability, a natural counterpart of soundness in classical workflow nets (as studied by van der Aalst). We distinguish centralized, distributed, and local controllability and provide solutions to all problems.

@inproceedings{Schmidt_2005_emisa,
Abstract = {An open workflow net is basically a workflow net extended with a message passing interface. Open workflow nets are adequate models for services or parts of inter-organizational business processes. We investigate the problem of control lability, a natural counterpart of soundness in classical workflow nets (as studied by van der Aalst). We distinguish centralized, distributed, and local controllability and provide solutions to all problems. },
Author = {Karsten Schmidt},
Booktitle = {Enterprise Modelling and Information Systems Architectures, Proceedings of the Workshop in Klagenfurt, October 24-25, 2005},
Editor = {J{\"o}rg Desel and Ulrich Frank},
Pages = {236-249},
Publisher = {GI},
Series = {Lecture Notes in Informatics (LNI)},
Title = {Controllability of Open Workflow Nets},
Volume = {P-75},
Year = 2005
}

Daniela Weinberg and Karsten Schmidt. Reduction Rules for Interaction Graphs. In Karsten Schmidt and Christian Stahl, editors, 12. Workshop ``Algorithmen und Werkzeuge für Petrinetze'' (AWPN 2005), Proceedings, pages 60-65, September 2005. Humboldt-Universität zu Berlin. Appeared as Informatik-Berichte Nr. 192. [PDF]

Abstract. The internet today has grown to be more than just being a basisfor exchanging information. It steadily becomes a platform for processing business processes. Many companies distribute their service with the help of web services or integrate other web services into their own workflow. However, before a web service gets published it should be examined well. We will introduce a way of examining the controllability of a web service. We propose the interaction graph of a web service, that is modelled by an open workflow net. To verify whether such a net is controllable or not it is sufficient to construct a reduced interaction graph. We will define reduction rules that minimize the size of the graph greatly. The analysis using the interaction graph as well as the reduction rules are implemented and have been integrated into an analysis tool kit for web services.

@inproceedings{WeinbergS_2005_awpn,
Abstract = {The internet today has grown to be more than just being a basisfor exchanging information. It steadily becomes a platform for processing business processes. Many companies distribute their service with the help of web services or integrate other web services into their own workflow. However, before a web service gets published it should be examined well. We will introduce a way of examining the controllability of a web service. We propose the interaction graph of a web service, that is modelled by an open workflow net. To verify whether such a net is controllable or not it is sufficient to construct a reduced interaction graph. We will define reduction rules that minimize the size of the graph greatly. The analysis using the interaction graph as well as the reduction rules are implemented and have been integrated into an analysis tool kit for web services.},
Author = {Daniela Weinberg and Karsten Schmidt},
Booktitle = {12. Workshop ``Algorithmen und Werkzeuge f{\"u}r Petrinetze'' (AWPN 2005), Proceedings},
Editor = {Karsten Schmidt and Christian Stahl},
Month = sep,
Note = {Appeared as Informatik-Berichte Nr. 192},
Pages = {60-65},
Publisher = {Humboldt-Universit{\"a}t zu Berlin},
Title = {Reduction Rules for Interaction Graphs},
Year = 2005
}

Technische Berichte / Technical Reports

Peter Massuthe, Wolfgang Reisig, and Karsten Schmidt. An Operating Guideline Approach to the SOA. Informatik-Berichte 191, Humboldt-Universität zu Berlin, Berlin, Germany, 2005. [PDF]

Abstract. Interorganizational cooperation is more and more organized by the paradigm of services. The service-oriented architecture (SOA) provides a general framework for service interaction. It describes three roles, service provider, service requester, and service broker, together with the three operations publish, find, and bind. We provide a formal method based on Petri nets to model services and their cooperation. We characterize well-behaving pairs of requester?s and provider?s services and suggest operating guidelines as a convenient and intuitive artifact to realize publish. Then, the find operation reduces to a matching problem between the requester?s service and the operating guideline. Binding of a requester?s and a provider?s service is therefore guaranteed to result in a well-behaving cooperating service.

@techreport{MassutheRS_2005_hub_tr191,
Abstract = {Interorganizational cooperation is more and more organized by the paradigm of services. The service-oriented architecture (SOA) provides a general framework for service interaction. It describes three roles, service provider, service requester, and service broker, together with the three operations publish, find, and bind. We provide a formal method based on Petri nets to model services and their cooperation. We characterize well-behaving pairs of requester?s and provider?s services and suggest operating guidelines as a convenient and intuitive artifact to realize publish. Then, the find operation reduces to a matching problem between the requester?s service and the operating guideline. Binding of a requester?s and a provider?s service is therefore guaranteed to result in a well-behaving cooperating service.},
Address = {Berlin, Germany},
Author = {Peter Massuthe and Wolfgang Reisig and Karsten Schmidt},
Institution = {Humboldt-Universit{\"a}t zu Berlin},
Number = 191,
Title = {An Operating Guideline Approach to the {SOA}},
Type = {Informatik-Berichte},
Year = 2005
}

Peter Massuthe and Karsten Schmidt. Matching Nondeterministic Services with Operating Guidelines. Informatik-Berichte 193, Humboldt-Universität zu Berlin, Berlin, Germany, June 2005. [PDF]

Abstract. Abstract Interorganizational cooperation is more and more organizedby the paradigm of services. The service-oriented architecture (SOA) provides a general framework for service interaction. It describes three roles, service provider, service requester, and service broker, together with the operations publish, find, and bind. We provide a formal method based on nondeterministic automata to model services and their interaction. We suggest operating guidelines as a convenient and intuitive artifact to realize publish. In our approach, the find operation reduces to a matching problem between the requester?s service and operating guidelines. In this paper, matching of deterministic as well as nondeterministic automata with operating guidelines is presented.

@techreport{MassutheS_2005_hub_tr193,
Abstract = {Abstract Interorganizational cooperation is more and more organizedby the paradigm of services. The service-oriented architecture (SOA) provides a general framework for service interaction. It describes three roles, service provider, service requester, and service broker, together with the operations publish, find, and bind. We provide a formal method based on nondeterministic automata to model services and their interaction. We suggest operating guidelines as a convenient and intuitive artifact to realize publish. In our approach, the find operation reduces to a matching problem between the requester?s service and operating guidelines. In this paper, matching of deterministic as well as nondeterministic automata with operating guidelines is presented.},
Address = {Berlin, Germany},
Author = {Peter Massuthe and Karsten Schmidt},
Institution = {Humboldt-Universit{\"a}t zu Berlin},
Month = jun,
Number = 193,
Title = {Matching Nondeterministic Services with Operating Guidelines},
Type = {Informatik-Berichte},
Year = 2005
}

Peter Massuthe and Karsten Schmidt. Operating Guidelines -- an Alternative to Public View. Informatik-Berichte 189, Humboldt-Universität zu Berlin, Berlin, Germany, 2005. [PDF]

Abstract. We propose operating guidelines as artifacts for publishing information about how to communicate with a business process that is intended to be provided as a service. We present an approach to compute operating guidelines fully automatically. We compare operating guidelines with the concept of public view.

@techreport{MassutheS_2005_hub_tr189,
Abstract = {We propose operating guidelines as artifacts for publishing information about how to communicate with a business process that is intended to be provided as a service. We present an approach to compute operating guidelines fully automatically. We compare operating guidelines with the concept of public view.},
Address = {Berlin, Germany},
Author = {Peter Massuthe and Karsten Schmidt},
Institution = {Humboldt-Universit{\"a}t zu Berlin},
Number = 189,
Title = {Operating Guidelines -- an Alternative to Public View},
Type = {Informatik-Berichte},
Year = 2005
}

Wolfgang Reisig, Karsten Schmidt, and Christian Stahl. Verteilte Geschäftsprozesse modellieren und analysieren. Informatik-Berichte 182, Humboldt-Universität zu Berlin, Berlin, Germany, February 2005. [PDF]

Abstract. Verteilte Gesch{\"a}ftsprozesse nutzen das Internet, um auf heterogenen Rechnerstrukturen Dienste auszubieten. Modellierungstechniken und Implementierungssprachen f{\"u}r solche Dienste werfen im Vergleich mit herk{\"o}mmlichen Rechnern grundlegend neue Fragestellungen auf. Wir diskutieren einige davon und zeigen, wie Petrinetze ihre Beantwortung erm{\"o}glichen.

@techreport{ReisigSS_2005_hub_tr182,
Abstract = {Verteilte Gesch{\"a}ftsprozesse nutzen das Internet, um auf heterogenen Rechnerstrukturen Dienste auszubieten. Modellierungstechniken und Implementierungssprachen f{\"u}r solche Dienste werfen im Vergleich mit herk{\"o}mmlichen Rechnern grundlegend neue Fragestellungen auf. Wir diskutieren einige davon und zeigen, wie Petrinetze ihre Beantwortung erm{\"o}glichen.},
Address = {Berlin, Germany},
Author = {Wolfgang Reisig and Karsten Schmidt and Christian Stahl},
Institution = {Humboldt-Universit{\"a}t zu Berlin},
Month = feb,
Number = 182,
Title = {{Verteilte Gesch{\"a}ftsprozesse modellieren und analysieren}},
Type = {Informatik-Berichte},
Year = 2005
}

Karsten Schmidt. Controllability of Distributed Business Processes. Informatik-Berichte 180, Humboldt-Universität zu Berlin, Berlin, Germany, 2005.

@techreport{Schmidt_2005_hub_tr180,
Address = {Berlin, Germany},
Author = {Karsten Schmidt},
Institution = {Humboldt-Universit{\"a}t zu Berlin},
Number = 180,
Title = {Controllability of Distributed Business Processes},
Type = {Informatik-Berichte},
Year = 2005
}

Karsten Schmidt and Christian Stahl. 12. Workshop Algorithmen und Werkzeuge für Petrinetze (AWPN 2005), Proceedings. Informatik-Berichte 192, Humboldt-Universität zu Berlin, Berlin, Germany, September 2005. [PDF]

@techreport{SchmidtS_2005_hub_tr192,
Address = {Berlin, Germany},
Author = {Karsten Schmidt and Christian Stahl},
Institution = {Humboldt-Universit{\"a}t zu Berlin},
Month = sep,
Number = 192,
Title = {{12. Workshop Algorithmen und Werkzeuge f{\"u}r Petrinetze (AWPN 2005), Proceedings}},
Type = {Informatik-Berichte},
Year = 2005
}

Abschlüsse / Theses

Niels Lohmann. Formale Fundierung und effizientere Algorithmen für die schrittbasierte TLDA-Interleavingsemantik. Diplomarbeit, Humboldt-Universität zu Berlin, Institut für Informatik, Berlin, Germany, September 2005. [PDF]

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{\"u}r TLDA noch keine Werkzeuge, die die Spezifikation und Verifikation unterst{\"u}tzen. Die Verf{\"u}gbarkeit solcher Werkzeuge tr{\"a}gt jedoch entscheidend zur Verbreitung der Logik bei. In [Loh05] wurde mit der Ausarbeitung und Implementierung einer schrittbasierten Interleavingsemantik f{\"u}r TLDA die Grundlage f{\"u}r die Entwicklung eines expliziten TLDA-Modelcheckers gelegt. Der genaue Zusammenhang zwischen der Halbordnungs- und Interleavingsemantik wurde jedoch nicht bewiesen. Au{\ss}erdem handelt es sich bei der Implementierung der Interleavingsemantik um einen Brute-Force-Prototyp, der nur f{\"u}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{\"a}higkeit des erweiterten Prototyps und illustrieren die Beziehung zwischen der Halbordnungs- und Interleavingsemantik.

@mastersthesis{Lohmann_2005_da,
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{\"u}r TLDA noch keine Werkzeuge, die die Spezifikation und Verifikation unterst{\"u}tzen. Die Verf{\"u}gbarkeit solcher Werkzeuge tr{\"a}gt jedoch entscheidend zur Verbreitung der Logik bei. In [Loh05] wurde mit der Ausarbeitung und Implementierung einer schrittbasierten Interleavingsemantik f{\"u}r TLDA die Grundlage f{\"u}r die Entwicklung eines expliziten TLDA-Modelcheckers gelegt. Der genaue Zusammenhang zwischen der Halbordnungs- und Interleavingsemantik wurde jedoch nicht bewiesen. Au{\ss}erdem handelt es sich bei der Implementierung der Interleavingsemantik um einen Brute-Force-Prototyp, der nur f{\"u}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{\"a}higkeit des erweiterten Prototyps und illustrieren die Beziehung zwischen der Halbordnungs- und Interleavingsemantik.},
Address = {Berlin, Germany},
Author = {Niels Lohmann},
Month = sep,
School = {Humboldt-Universit{\"a}t zu Berlin, Institut f{\"u}r Informatik},
Title = {{Formale Fundierung und effizientere Algorithmen f{\"u}r die schrittbasierte TLDA-Interleavingsemantik}},
Type = {Diplomarbeit},
Year = 2005
}

Niels Lohmann. Implementierung einer schrittbasierten Interleavingsemantik für die Temporal Logic of Distributed Actions (TLDA). Studienarbeit, Humboldt-Universität zu Berlin, Institut für Informatik, Berlin, Germany, June 2005. [PDF]

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{\"u}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{\"u}r TLDA vorgeschlagen und ein Prototyp entwickelt, der f{\"u}r eine bestimmte Klasse von TLDA-Spezifikationen das Transitionssystem aufbaut. Die entwickelte Semantik soll zusammen mit dem Prototypen die Grundlage f{\"u}r die weitere Arbeit an einem Modelchecker f{\"u}r TLDA sein.

@mastersthesis{Lohmann_2005_sa,
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{\"u}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{\"u}r TLDA vorgeschlagen und ein Prototyp entwickelt, der f{\"u}r eine bestimmte Klasse von TLDA-Spezifikationen das Transitionssystem aufbaut. Die entwickelte Semantik soll zusammen mit dem Prototypen die Grundlage f{\"u}r die weitere Arbeit an einem Modelchecker f{\"u}r TLDA sein.},
Address = {Berlin, Germany},
Author = {Niels Lohmann},
Month = jun,
School = {Humboldt-Universit{\"a}t zu Berlin, Institut f{\"u}r Informatik},
Title = {{Implementierung einer schrittbasierten Interleavingsemantik f{\"u}r die Temporal Logic of Distributed Actions (TLDA)}},
Type = {Studienarbeit},
Year = 2005
}

2004

Zeitschriftenartikel / Journal Articles

Farn Wang, Karsten Schmidt, Fang Yu, Geng-Dian Huang, and Bow-Yaw Wang. BDD-Based Safety-Analysis of Concurrent Software with Pointer Data Structures Using Graph Automorphism Symmetry Reduction. IEEE Trans. Software Eng., 30(6):403-417, June 2004. [PDF] [DOI]

@article{WangSYHW_2004_tse,
Author = {Farn Wang and Karsten Schmidt and Fang Yu and Geng-Dian Huang and Bow-Yaw Wang},
Journal = {IEEE Trans. Software Eng.},
Month = jun,
Number = 6,
Pages = {403-417},
Title = {{BDD}-Based Safety-Analysis of Concurrent Software with Pointer Data Structures Using Graph Automorphism Symmetry Reduction},
Volume = 30,
Year = 2004,
}

Konferenzbeiträge / Conference Papers

Karsten Schmidt. Automated Generation of a Progress Measure for the Sweep-Line Method. In Kurt Jensen and Andreas Podelski, editors, Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29-April 2, 2004, Proceedings., volume 2988 of Lecture Notes in Computer Science, pages 192-204, 2004. Springer-Verlag. [DOI]

Abstract. In the context of Petri nets, we propose an automated construction of a progress measure which is an important pre-requisite for a state space reduction technique called the sweep-line method. Our construction is based on linear-algebraic considerations concerning the transition vectors of the Petri net under consideration.

@inproceedings{Schmidt_2004_tacas,
Abstract = {In the context of Petri nets, we propose an automated construction of a progress measure which is an important pre-requisite for a state space reduction technique called the sweep-line method. Our construction is based on linear-algebraic considerations concerning the transition vectors of the Petri net under consideration.},
Author = {Karsten Schmidt},
Booktitle = {Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29-April 2, 2004, Proceedings.},
Editor = {Kurt Jensen and Andreas Podelski},
Pages = {192-204},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Automated Generation of a Progress Measure for the Sweep-Line Method},
Volume = 2988,
Year = 2004,
}

Karsten Schmidt. Distributed Usability of Web Services. In Ekkart Kindler, editor, Proceedings of the 11th Workshop on Algorithms and Tools for Petri Nets (AWPN 04), pages 19-24, September 2004. Universität Paderborn. Appeared as Bericht tr-ri-04-251. [PDF]

Abstract. We estabilish a theory of distributed usability. To do so, it is however neccessary to modify the already existing theory of central usability.

@inproceedings{Schmidt_2004_awpn,
Abstract = {We estabilish a theory of distributed usability. To do so, it is however neccessary to modify the already existing theory of central usability.},
Author = {Karsten Schmidt},
Booktitle = {Proceedings of the 11th Workshop on Algorithms and Tools for Petri Nets (AWPN 04)},
Editor = {Ekkart Kindler},
Month = sep,
Note = {Appeared as Bericht tr-ri-04-251},
Pages = {19-24},
Publisher = {Universit{\"a}t Paderborn},
Title = {Distributed Usability of {Web} Services},
Year = {2004}
}

Karsten Schmidt and Christian Stahl. A Petri Net Semantic for BPEL4WS -- Validation and Application. In Ekkart Kindler, editor, Proceedings of the 11th Workshop on Algorithms and Tools for Petri Nets (AWPN'04), pages 1-6, September 2004. Universität Paderborn. Appeared as Bericht tr-ri-04-251. [PDF]

Abstract. We translated a small business process into a recently defined Petri net semantic. Then we used the tool LoLA for validating the semantic as well as for proving relevant properties of the particular process.

@inproceedings{SchmidtS_2004_awpn,
Abstract = {We translated a small business process into a recently defined Petri net semantic. Then we used the tool LoLA for validating the semantic as well as for proving relevant properties of the particular process.},
Author = {Karsten Schmidt and Christian Stahl},
Booktitle = {Proceedings of the 11th Workshop on Algorithms and Tools for Petri Nets (AWPN'04)},
Editor = {Ekkart Kindler},
Month = sep,
Note = {Appeared as Bericht tr-ri-04-251},
Pages = {1-6},
Publisher = {Universit{\"a}t Paderborn},
Title = {A {Petri} Net Semantic for {BPEL4WS} -- Validation and Application},
Year = 2004
}

Harro Wimmel. Eliminating Internal Behaviour in Petri Nets. In Jordi Cortadella and Wolfgang Reisig, editors, Applications and Theory of Petri Nets 2004, 25th International Conference, ICATPN 2004, Bologna, Italy, June 21-25, 2004, Proceedings, volume 3099 of Lecture Notes in Computer Science, pages 411-425, June 2004. Springer-Verlag. [DOI]

Abstract. A safe labelled marked graph (Petri Net) with internal transitions can be transformed into a pomset-equivalent safe labelled marked graph without internal transitions.

@inproceedings{Wimmel_2004_icatpnb,
Abstract = {A safe labelled marked graph (Petri Net) with internal transitions can be transformed into a pomset-equivalent safe labelled marked graph without internal transitions.},
Author = {Harro Wimmel},
Booktitle = {Applications and Theory of Petri Nets 2004, 25th International Conference, ICATPN 2004, Bologna, Italy, June 21-25, 2004, Proceedings},
Editor = {Jordi Cortadella and Wolfgang Reisig},
Month = jun,
Pages = {411-425},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Eliminating Internal Behaviour in {Petri} Nets},
Volume = {3099},
Year = {2004},
}

Harro Wimmel. Infinity of Intermediate States Is Decidable for Petri Nets. In Jordi Cortadella and Wolfgang Reisig, editors, Applications and Theory of Petri Nets 2004, 25th International Conference, ICATPN 2004, Bologna, Italy, June 21-25, 2004, Proceedings, volume 3099 of Lecture Notes in Computer Science, pages 426-434, June 2004. Springer-Verlag. [DOI]

Abstract. Based on the algorithms to decide reachability for Petri nets, we show how to decide whether the number of markings reachable on paths between two given markings is finite or infinite.

@inproceedings{Wimmel_2004_icatpna,
Abstract = {Based on the algorithms to decide reachability for Petri nets, we show how to decide whether the number of markings reachable on paths between two given markings is finite or infinite.},
Author = {Harro Wimmel},
Booktitle = {Applications and Theory of Petri Nets 2004, 25th International Conference, ICATPN 2004, Bologna, Italy, June 21-25, 2004, Proceedings},
Editor = {Jordi Cortadella and Wolfgang Reisig},
Month = jun,
Pages = {426-434},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Infinity of Intermediate States Is Decidable for {Petri} Nets},
Volume = {3099},
Year = {2004},
}

2003

Zeitschriftenartikel / Journal Articles

Karsten Schmidt. Distributed Verification with LoLA. Fundam. Inform., 54(2-3):253-262, 2003. [WWW]

Abstract. We report work in progress on a distributed version of explicit state space generation in the Petri net verification tool LoLA. We propose a data structure where all available memory of all involved workstations can be fully exploited, and load balancing actions are possible at any time while the verification is running. It is even possible to extend the set of involved workstations while a verification is running.

@article{Schmidt_2003_fi,
Abstract = {We report work in progress on a distributed version of explicit state space generation in the Petri net verification tool LoLA. We propose a data structure where all available memory of all involved workstations can be fully exploited, and load balancing actions are possible at any time while the verification is running. It is even possible to extend the set of involved workstations while a verification is running.},
Author = {Karsten Schmidt},
Journal = {Fundam. Inform.},
Number = {2-3},
Pages = {253-262},
Title = {Distributed Verification with {LoLA}},
Volume = 54,
Year = 2003,
}

Ferucio Laurentiu Tiplea and Olivia Oanea. Model Checking for Linear Time $\mu$-calculus and Extended Petri Nets. An. Univ. Timis., Ser. Mat.-Inform., XLI:229-245, 2003. [PDF]

@article{TipleaO_2003_smi,
Author = {Ferucio Laurentiu Tiplea and Olivia Oanea},
Journal = {An. Univ. Timis., Ser. Mat.-Inform.},
Pages = {229-245},
Title = {Model Checking for Linear Time $\mu$-calculus and Extended {Petri} Nets},
Volume = {XLI},
Year = {2003}
}

Konferenzbeiträge / Conference Papers

Karsten Schmidt. Using Petri Net Invariants in State Space Construction. In Hubert Garavel and John Hatcliff, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2003), 9th International Conference, Part of ETAPS 2003, Warsaw, Poland, volume 2619 of Lecture Notes in Computer Science, pages 473-488, April 2003. Springer-Verlag. [DOI]

Abstract. The linear algebraic invariant calculus is a powerful technique for the verification of Petri nets. Traditionally it is used for structural verification, i.e. for avoiding the explicit construction of a state space. In this paper, we study the use of Petri net invariants for reducing the memory resources required during state space construction. While place invariants help to reduce the amount of memory needed for each single state (without reducing the number of states as such), transition invariants can be used to reduce the number of states to be stored. Interestingly, our approach does not require computing invariants in full, let alone storing them permanently. All information we need can be deduced from an upper triangular form of the Petri net's incidence matrix. Experiments prove that the place invariant technique leads to improvements in both memory and run time costs while transition invariants lead to a space/time tradeoff that can be controlled heuristically.

@inproceedings{Schmidt_2003_tacas,
Abstract = {The linear algebraic invariant calculus is a powerful technique for the verification of Petri nets. Traditionally it is used for structural verification, i.e. for avoiding the explicit construction of a state space. In this paper, we study the use of Petri net invariants for reducing the memory resources required during state space construction. While place invariants help to reduce the amount of memory needed for each single state (without reducing the number of states as such), transition invariants can be used to reduce the number of states to be stored. Interestingly, our approach does not require computing invariants in full, let alone storing them permanently. All information we need can be deduced from an upper triangular form of the Petri net's incidence matrix. Experiments prove that the place invariant technique leads to improvements in both memory and run time costs while transition invariants lead to a space/time tradeoff that can be controlled heuristically.},
Author = {Karsten Schmidt},
Booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2003), 9th International Conference, Part of ETAPS 2003, Warsaw, Poland},
Editor = {Hubert Garavel and John Hatcliff},
Month = apr,
Pages = {473-488},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Using {Petri} Net Invariants in State Space Construction},
Volume = 2619,
Year = 2003,
}

Ferucio Laurentiu Tiplea and Olivia Oanea. Model Checking Linear for Time $\mu$-Calculus for Extended Petri Nets. In Tudor Jebelean and Viorel Negru, editors, 5th International Workshop Symbolic and Numeric Algorithms for Scientific Computing SYNASC 2003, Timisoara (Romania), Oct 1-4, 2003, pages 297-310, October 2003.

@inproceedings{LaurentiuO_2003_synasc,
Author = {Ferucio Laurentiu Tiplea and Olivia Oanea},
Booktitle = {5th International Workshop "Symbolic and Numeric Algorithms for Scientific Computing" SYNASC 2003, Timisoara (Romania), Oct 1-4, 2003},
Editor = {Tudor Jebelean and Viorel Negru},
Month = oct,
Pages = {297-310},
Title = {Model Checking Linear for Time $\mu$-Calculus for Extended {Petri} Nets},
Year = {2003}
}

Technische Berichte / Technical Reports

Philippe Darondeau and Harro Wimmel. From bounded T-systems to 1-safe T-systems up to language equivalence. Technical Report INRIA-RR-4708, INRIA, Rennes, France, January 2003. [WWW]

Abstract. We show that every finite and bounded marked graph or T-system has a 1-safe labelled version with an identical language.

@techreport{DarondeauW_2003_tr,
Abstract = {We show that every finite and bounded marked graph or T-system has a 1-safe labelled version with an identical language.},
Address = {Rennes, France},
Author = {Philippe Darondeau and Harro Wimmel},
Institution = {INRIA},
Month = jan,
Number = {INRIA-RR-4708},
Title = {From bounded {T}-systems to 1-safe {T}-systems up to language equivalence},
Type = {Technical Report},
Year = {2003},
}

Abschlüsse / Theses

Olivia Oanea. Model Checking Petri Nets. Master thesis, University ``A.I.Cuza'' of Ia\csi, Faculty of Computer Science, Ia\csi, Romania, June 2003.

@mastersthesis{Oanea_2003_mt,
Address = {Ia\c{s}i, Romania},
Author = {Olivia Oanea},
Month = jun,
School = {University ``A.I.Cuza'' of Ia\c{s}i, Faculty of Computer Science},
Title = {Model Checking {Petri} Nets},
Type = {Master thesis},
Year = {2003}
}

2002

Bücher und Tagungsbände / Books and Proceedings

Lutz Priese and Harro Wimmel. Theoretische Informatik: Petri-Netze. Springer-Verlag, 2002. [DOI]

@book{PrieseW_2002_book,
Author = {Lutz Priese and Harro Wimmel},
Publisher = {Springer-Verlag},
Title = {{Theoretische Informatik: Petri-Netze}},
Year = {2002},
}

Zeitschriftenartikel / Journal Articles

Roxana Melinte, Olivia Oanea, Ioana Olga, and Ferucio Laurentiu Tiplea. The Home Marking Problem and Some Related Concepts. Acta Cybern., 15(3):467-478, 2002.

Abstract. In this paper we study the home marking problem for Petri nets, and some related concepts to it like confluence, noetherianity, and state space inclusion. We show that the home marking problem for inhibitor Petri nets is undecidable. We relate then the existence of home markings to confluence and noetherianity and prove that confluent and noetherian Petri nets have an unique home marking. Finally, we define some versions of the state space inclusion problem related to the home marking and sub-marking problems, and discuss their decidability status.

@article{MelinteOOT_2002_ac,
Abstract = {In this paper we study the home marking problem for Petri nets, and some related concepts to it like confluence, noetherianity, and state space inclusion. We show that the home marking problem for inhibitor Petri nets is undecidable. We relate then the existence of home markings to confluence and noetherianity and prove that confluent and noetherian Petri nets have an unique home marking. Finally, we define some versions of the state space inclusion problem related to the home marking and sub-marking problems, and discuss their decidability status.},
Author = {Roxana Melinte and Olivia Oanea and Ioana Olga and Ferucio Laurentiu Tiplea},
Journal = {Acta Cybern.},
Number = {3},
Pages = {467-478},
Title = {The Home Marking Problem and Some Related Concepts},
Volume = {15},
Year = {2002}
}

Konferenzbeiträge / Conference Papers

Roxana Melinte, Olivia Oanea, Ioana Olga, and Ferucio Laurentiu Tiplea. The Home Marking Problem and Some Related Concepts. In Jörg Desel and Mathias Weske, editors, Prozessorientierte Methoden und Werkzeuge für die Entwicklung von Informationssystemen - Promise 2002, 9.-11. Oktober 2002, Potsdam, volume P-21 of Lecture Notes in Informatics (LNI), pages 104-115, October 2002. GI. [PDF]

@inproceedings{MelinteOOT_2002_promise,
Author = {Roxana Melinte and Olivia Oanea and Ioana Olga and Ferucio Laurentiu Tiplea},
Booktitle = {Prozessorientierte Methoden und Werkzeuge f{\"u}r die Entwicklung von Informationssystemen - Promise 2002, 9.-11. Oktober 2002, Potsdam},
Editor = {J{\"o}rg Desel and Mathias Weske},
Month = oct,
Pages = {104-115},
Publisher = {GI},
Series = {Lecture Notes in Informatics (LNI)},
Title = {The Home Marking Problem and Some Related Concepts},
Volume = {P-21},
Year = {2002}
}

Karsten Schmidt. Distributed Verification with LoLA. In Hans-Dieter Burkhard, L. Czaja, G. Lindemann, A. Skowdron, and Peter H. Starke, editors, Workshop Concurrency, Specification and Programming CS&P 2002, Berlin; Oct. 7-9, Vol. 2, pages 317-326, October 2002. Humbolt-Universität zu Berlin. Appeared as Informatik-Berichte Nr. 161.

Abstract. We report work in progress on a distributed version of explicit state space generation in the Petri net verification tool LoLA. We propose a data structure where all available memory of all involved workstations can be fully exploited, and load balancing actions are possible at any time while the verification is running. I t is even possible to extend the set of involved workstations which a verification is running.

@inproceedings{Schmidt_2002_csp,
Abstract = {We report work in progress on a distributed version of explicit state space generation in the Petri net verification tool LoLA. We propose a data structure where all available memory of all involved workstations can be fully exploited, and load balancing actions are possible at any time while the verification is running. I t is even possible to extend the set of involved workstations which a verification is running.},
Author = {Karsten Schmidt},
Booktitle = {Workshop Concurrency, Specification and Programming CS\&P 2002, Berlin; Oct. 7-9, Vol. 2},
Editor = {Hans-Dieter Burkhard and L. Czaja and G. Lindemann and A. Skowdron and Peter H. Starke},
Month = oct,
Note = {Appeared as Informatik-Berichte Nr. 161},
Pages = {317-326},
Publisher = {Humbolt-Universit{\"a}t zu Berlin},
Title = {Distributed Verification with {LoLA}},
Year = {2002}
}

Karsten Schmidt. Distributed Verification with LoLA. In Jörg Desel and Mathias Weske, editors, Prozessorientierte Methoden und Werkzeuge für die Entwicklung von Informationssystemen - Promise 2002, 9.-11. Oktober 2002, Potsdam, volume P-21 of Lecture Notes in Informatics (LNI), pages 94-103, October 2002. GI.

@inproceedings{Schmidt_2002_promise,
Author = {Karsten Schmidt},
Booktitle = {Prozessorientierte Methoden und Werkzeuge f{\"u}r die Entwicklung von Informationssystemen - Promise 2002, 9.-11. Oktober 2002, Potsdam},
Editor = {J{\"o}rg Desel and Mathias Weske},
Month = oct,
Pages = {94-103},
Publisher = {GI},
Series = {Lecture Notes in Informatics (LNI)},
Title = {Distributed Verification with {LoLA}},
Volume = {P-21},
Year = {2002}
}

Farn Wang and Karsten Schmidt. Symmetric Symbolic Safety-Analysis of Concurrent Software with Pointer Data Structures. In Doron Peled and Moshe Y. Vardi, editors, Formal Techniques for Networked and Distributed Sytems -- FORTE 2002 : 22nd IFIP WG 6.1 International Conference, Houston, Texas, USA, November 11--14, 2002. Proceedings, volume 2529 of Lecture Notes in Computer Science, pages 50-64, November 2002. Springer-Verlag. [DOI]

Abstract. We formally define the model of software with pointer data structures. We developed symbolic algorithms for the manipulation of conditions and assignments with indirect operands for verification with BDD-like data-structures. We rely on two techniques, including inactive variable elimination and process-symmetry reduction in the data-structure configuration, to contain the time and memory complexity. We use binary permutation for efficiency but also identify the possibility of anomaly of image false reachability. We implemented the techniques in tool red and compare performance with Mur and SMC against several other benchmarks.

@inproceedings{WangS_2002_forte,
Abstract = {We formally define the model of software with pointer data structures. We developed symbolic algorithms for the manipulation of conditions and assignments with indirect operands for verification with BDD-like data-structures. We rely on two techniques, including inactive variable elimination and process-symmetry reduction in the data-structure configuration, to contain the time and memory complexity. We use binary permutation for efficiency but also identify the possibility of anomaly of image false reachability. We implemented the techniques in tool red and compare performance with Mur and SMC against several other benchmarks.},
Author = {Farn Wang and Karsten Schmidt},
Booktitle = {Formal Techniques for Networked and Distributed Sytems -- FORTE 2002 : 22nd IFIP WG 6.1 International Conference, Houston, Texas, USA, November 11--14, 2002. Proceedings},
Editor = {Doron Peled and Moshe Y. Vardi},
Month = nov,
Pages = {50-64},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Symmetric Symbolic Safety-Analysis of Concurrent Software with Pointer Data Structures},
Volume = 2529,
Year = 2002,
}

Technische Berichte / Technical Reports

Roxana Melinte, Olivia Oanea, Ioana Olga, and Ferucio Laurentiu Tiplea. The Home Marking Problem and Some Related Concepts. Technical report TR 02-02, University ``A.I.Cuza'' of Ia\csi, Faculty of Computer Science, Ia\csi, Romania, February 2002. [POSTSCRIPT]

Abstract. In this paper we study the home marking problem for Petri nets, and some related concepts to it like confluence, noetherianity, and state space inclusion. We show that the home marking problem for inhibitor Petri nets is undecidable. We relate then the existence of home markings to confluence and noetherianity and prove that confluent and noetherian Petri nets have an unique home marking. Finally, we define some versions of the state space inclusion problem related to the home marking and sub-marking problems, and discuss their decidability status.

@techreport{MelinteOOT_2002_tr0202,
Abstract = {In this paper we study the home marking problem for Petri nets, and some related concepts to it like confluence, noetherianity, and state space inclusion. We show that the home marking problem for inhibitor Petri nets is undecidable. We relate then the existence of home markings to confluence and noetherianity and prove that confluent and noetherian Petri nets have an unique home marking. Finally, we define some versions of the state space inclusion problem related to the home marking and sub-marking problems, and discuss their decidability status.},
Address = {Ia\c{s}i, Romania},
Author = {Roxana Melinte and Olivia Oanea and Ioana Olga and Ferucio Laurentiu Tiplea},
Institution = {University ``A.I.Cuza'' of Ia\c{s}i, Faculty of Computer Science},
Month = feb,
Number = {TR 02-02},
Title = {The Home Marking Problem and Some Related Concepts},
Year = {2002}
}

Olivia Oanea. Decidability and Complexity of Petri Net Problems. Technical report TR 02-04, University ``A.I.Cuza'' of Ia\csi, Faculty of Computer Science, Ia\csi, Romania, September 2002. [POSTSCRIPT]

Abstract. Petri net theory plays a very important role in modeling and analysing parallel and distributed systems. It provides a simple mathematical structure, and basic properties can be cleanly analysed. The aim of this paper is to give an overview on the basic decision problems in the theory of Petri nets. We discuss both decidability and complexity aspects. We have also a contribution in the area of home markings. We prove that the home marking problem for inhibitor Petri nets is undecidable.

@techreport{Oanea_2002_tr0204,
Abstract = {Petri net theory plays a very important role in modeling and analysing parallel and distributed systems. It provides a simple mathematical structure, and basic properties can be cleanly analysed. The aim of this paper is to give an overview on the basic decision problems in the theory of Petri nets. We discuss both decidability and complexity aspects. We have also a contribution in the area of home markings. We prove that the home marking problem for inhibitor Petri nets is undecidable.},
Address = {Ia\c{s}i, Romania},
Author = {Olivia Oanea},
Institution = {University ``A.I.Cuza'' of Ia\c{s}i, Faculty of Computer Science},
Month = sep,
Number = {TR 02-04},
Title = {Decidability and Complexity of {Petri} Net Problems},
Year = {2002}
}

Abschlüsse / Theses

Karsten Schmidt. Explicit State Space Verification. Habilitationsschrift, Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II, Berlin, Germany, December 2002. [WWW] [PDF]

Abstract. Verification is the task of determining whether a (model of a) system holds a given behavioral property. State space verification comprises a class of computer aided verification techniques where the property is verified through exhaustive exploration of the reachable states of the system. Brute force implementations of state space verification are intractable, due to the well known state explosion problem. Explicit state space verification techniques explore the state space one state at a time, and rely usually on data structures where the size of the data structure increases monotonously with an increasing number of explored states. They alleviate state explosion by constructing a reduced state space that, by a mathematically founded construction, behaves like the original system with respect to the specified properties. Thereby, decrease of the number of states in the reduced system is the core issue of a reduction technique thus reducing the amount of memory required. An explicit state space verification technique comprises of - a theory that establishes whether, and how, certain properties can be preserved through a construction of a reduced state space; - a set of procedures to execute the actual construction efficiently. In this thesis, we contribute to several existing explicit state space verification techniques in either of these two respects. We extend the class of stubborn set methods (an instance of partial order reduction) by constructions that preserve previously unsupported classes of properties. Many existing constructions rely on the existence of "invisible" actions, i.e. actions whose effect does not immediately influence the verified property. We propose efficient constructions that can be applied without having such invisible actions, and prove that they preserve reachability properties as well as certain classes of more complex behavioral system properties. This way, so called "global" properties can now be approached with better stubborn set methods. We pick up a graph automorphism based approach to symmetry reduction and propose a set of construction algorithms that make this approach feasible. In difference to established symmetry techniques that rely on special "symmetry creating" data types, a broader range of symmetries can be handled with our approach thus obtaining smaller reduced state spaces. Coverability graph construction leads to a finite representation of an infinite state space of a Petri net by condensing diverging sequences of states to their limit. We prove rules to determine temporal logic properties of the original system from its coverability graph, far beyond the few properties known to be preserved so far. We employ the Petri net concept of linear algebraic invariants for compressing states as well as for leaving states out of explicit storage. Compression uses place invariants for replacing states by smaller fingerprints that still uniquely identify a state (unlike many hash compression techniques). For reducing the number of explicitly stored states, we rely on the capability of Petri net transition invariants to characterize cycles in the state space. For termination of an exhaustive exploration of a finite state space, it is sufficient to cover all cycles with explicitly stored states. Both techniques are easy consequences of well known facts about invariants. As a novel contribution, we observe that both techniques can be applied without computing an explicit representation of (a generating set for) the respective invariants. This speeds up the constructions considerably and saves a significant amount of memory. For all presented techniques, we illustrate their capabilities to reduce the complexity of state space reduction using a few academic benchmark examples. We address compatibility issues, i.e. the possibility to apply techniques in combination, or in connection with different strategies for exploring the reduced state space. We propose a scheme to distribute state space exploration on a cluster of workstations and discuss consequences for using this scheme for state space reduction. We collect observations concerning the impact of the choice of system description formalisms, and property specification languages, on the availability of explicit state space verification techniques.

@phdthesis{Schmidt_2002_habil,
Abstract = {Verification is the task of determining whether a (model of a) system holds a given behavioral property. State space verification comprises a class of computer aided verification techniques where the property is verified through exhaustive exploration of the reachable states of the system. Brute force implementations of state space verification are intractable, due to the well known state explosion problem. Explicit state space verification techniques explore the state space one state at a time, and rely usually on data structures where the size of the data structure increases monotonously with an increasing number of explored states. They alleviate state explosion by constructing a reduced state space that, by a mathematically founded construction, behaves like the original system with respect to the specified properties. Thereby, decrease of the number of states in the reduced system is the core issue of a reduction technique thus reducing the amount of memory required. An explicit state space verification technique comprises of - a theory that establishes whether, and how, certain properties can be preserved through a construction of a reduced state space; - a set of procedures to execute the actual construction efficiently. In this thesis, we contribute to several existing explicit state space verification techniques in either of these two respects. We extend the class of stubborn set methods (an instance of partial order reduction) by constructions that preserve previously unsupported classes of properties. Many existing constructions rely on the existence of "invisible" actions, i.e. actions whose effect does not immediately influence the verified property. We propose efficient constructions that can be applied without having such invisible actions, and prove that they preserve reachability properties as well as certain classes of more complex behavioral system properties. This way, so called "global" properties can now be approached with better stubborn set methods. We pick up a graph automorphism based approach to symmetry reduction and propose a set of construction algorithms that make this approach feasible. In difference to established symmetry techniques that rely on special "symmetry creating" data types, a broader range of symmetries can be handled with our approach thus obtaining smaller reduced state spaces. Coverability graph construction leads to a finite representation of an infinite state space of a Petri net by condensing diverging sequences of states to their limit. We prove rules to determine temporal logic properties of the original system from its coverability graph, far beyond the few properties known to be preserved so far. We employ the Petri net concept of linear algebraic invariants for compressing states as well as for leaving states out of explicit storage. Compression uses place invariants for replacing states by smaller fingerprints that still uniquely identify a state (unlike many hash compression techniques). For reducing the number of explicitly stored states, we rely on the capability of Petri net transition invariants to characterize cycles in the state space. For termination of an exhaustive exploration of a finite state space, it is sufficient to cover all cycles with explicitly stored states. Both techniques are easy consequences of well known facts about invariants. As a novel contribution, we observe that both techniques can be applied without computing an explicit representation of (a generating set for) the respective invariants. This speeds up the constructions considerably and saves a significant amount of memory. For all presented techniques, we illustrate their capabilities to reduce the complexity of state space reduction using a few academic benchmark examples. We address compatibility issues, i.e. the possibility to apply techniques in combination, or in connection with different strategies for exploring the reduced state space. We propose a scheme to distribute state space exploration on a cluster of workstations and discuss consequences for using this scheme for state space reduction. We collect observations concerning the impact of the choice of system description formalisms, and property specification languages, on the availability of explicit state space verification techniques.},
Address = {Berlin, Germany},
Author = {Karsten Schmidt},
Month = dec,
School = {Humboldt-Universit{\"a}t zu Berlin, Mathematisch-Naturwissenschaftliche Fakult{\"a}t II},
Title = {Explicit State Space Verification},
Type = {Habilitationsschrift},
Year = 2002,
}

Olivia Oanea. Decidability and Complexity of Petri Net Problems. Diploma thesis, University ``A.I.Cuza'' of Ia\csi, Faculty of Computer Science, Ia\csi, Romania, September 2002.

@mastersthesis{Oanea_2002_da,
Address = {Ia\c{s}i, Romania},
Author = {Olivia Oanea},
Month = sep,
School = {University ``A.I.Cuza'' of Ia\c{s}i, Faculty of Computer Science},
Title = {Decidability and Complexity of {Petri} Net Problems},
Type = {Diploma thesis},
Year = {2002}
}

2001

Zeitschriftenartikel / Journal Articles

Karsten Schmidt. Narrowing Petri Net State Spaces Using the State Equation. Fundam. Inform., 47(3-4):325-335, October 2001. [WWW]

Abstract. Given a (possibly partially defined) state, all count vectors of transition sequences reaching that state are solutions to a corresponding Petri net state equation. We propose a search strategy where sequences corresponding to a minimal solution of the state equation are explored first. Then step by step the search space is relaxed to arbitrary count vectors. This heuristics relies on the observation that in many (though provably not in all) cases, minimal solutions of the state equation can be realized as a firing sequence. If no target state is reachable, either the state equation does not have solutions, or our search method would yield the full state space. We study the impact of the state equation on reachability, present an algorithm that exploits information from the state equation and discuss its application in stateless search as well as its combination with stubborn set reduction.

@article{Schmidt_2001_fi,
Abstract = {Given a (possibly partially defined) state, all count vectors of transition sequences reaching that state are solutions to a corresponding Petri net state equation. We propose a search strategy where sequences corresponding to a minimal solution of the state equation are explored first. Then step by step the search space is relaxed to arbitrary count vectors. This heuristics relies on the observation that in many (though provably not in all) cases, minimal solutions of the state equation can be realized as a firing sequence. If no target state is reachable, either the state equation does not have solutions, or our search method would yield the full state space. We study the impact of the state equation on reachability, present an algorithm that exploits information from the state equation and discuss its application in stateless search as well as its combination with stubborn set reduction.},
Author = {Karsten Schmidt},
Journal = {Fundam. Inform.},
Month = oct,
Number = {3-4},
Pages = {325-335},
Title = {Narrowing {Petri} Net State Spaces Using the State Equation},
Volume = 47,
Year = 2001,
}

Konferenzbeiträge / Conference Papers

Karsten Schmidt. Using Invariants for State Space Reduction. In Workshop on Concurrency, Specification and Programming (CS&P 2001), Proceedings, Warsaw, Poland, 2001.

@inproceedings{Schmidt_2001_wcsp,
Address = {Warsaw, Poland},
Author = {Karsten Schmidt},
Booktitle = {Workshop on Concurrency, Specification and Programming (CS\&P 2001), Proceedings},
Title = {Using Invariants for State Space Reduction},
Year = 2001
}

2000

Zeitschriftenartikel / Journal Articles

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

@article{Schmidt_2000_pnn,
Author = {Karsten Schmidt},
Journal = {Petri Net Newsletter},
Pages = {30-44},
Title = {Flexible net Inscriptions with {LoLA}},
Volume = 59,
Year = 2000
}

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

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{Schmidt_2000_ai,
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.},
Author = {Karsten Schmidt},
Journal = {Acta Inf.},
Number = 7,
Pages = {545-590},
Title = {How to Calculate Symmetries of {Petri} Nets},
Volume = 36,
Year = 2000,
}

Karsten Schmidt. Stubborn Sets for Model Checking the EF/AG Fragment of CTL. Fundam. Inform., 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{Schmidt_2000_fi,
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.},
Author = {Karsten Schmidt},
Journal = {Fundam. Inform.},
Month = aug,
Number = {1-4},
Pages = {331-341},
Title = {Stubborn Sets for Model Checking the {EF/AG} Fragment of {CTL}},
Volume = 43,
Year = 2000
}

Konferenzbeiträge / Conference Papers

Eike Best and Harro Wimmel. Reducing k-Safe Petri Nets to Pomset-Equivalent 1-Safe Petri Nets. In Mogens Nielsen and Dan Simpson, editors, Application and Theory of Petri Nets 2000: 21st International Conference, ICATPN 2000, Aarhus, Denmark, June 2000. Proceedings, volume 1825 of Lecture Notes in Computer Science, pages 63-82, June 2000. Springer-Verlag. [DOI]

Abstract. It is a well-known fact that for every k-safe Petri net, i.e. a Petri net in which no place contains more than k in N tokens under any reachable marking, there is a 1-safe Petri net with the same interleaving behaviour. Indeed these types of Petri nets generate regular languages. In this paper, we show that this equivalence of k-safe and 1-safe Petri nets holds also for their pomset languages, a true-concurrency semantics.

@inproceedings{BestW_2000_icatpn,
Abstract = {It is a well-known fact that for every k-safe Petri net, i.e. a Petri net in which no place contains more than k in N tokens under any reachable marking, there is a 1-safe Petri net with the same interleaving behaviour. Indeed these types of Petri nets generate regular languages. In this paper, we show that this equivalence of k-safe and 1-safe Petri nets holds also for their pomset languages, a true-concurrency semantics.},
Author = {Eike Best and Harro Wimmel},
Booktitle = {Application and Theory of Petri Nets 2000: 21st International Conference, ICATPN 2000, Aarhus, Denmark, June 2000. Proceedings},
Editor = {Mogens Nielsen and Dan Simpson},
Month = jun,
Pages = {63-82},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Reducing k-Safe {Petri} Nets to Pomset-Equivalent 1-Safe {Petri} Nets},
Volume = {1825},
Year = {2000},
}

Karsten Schmidt. Integrating Low Level Symmetries into Reachability Analysis. In Susanne Graf and Michael I. Schwartzbach, editors, Tools and Algorithms for the Construction and Analysis of Systems: 6th International Conference, TACAS 2000, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March/April 2000. Proceedings, volume 1785 of Lecture Notes in Computer Science, pages 315-330, March 2000. Springer-Verlag. [DOI]

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. Keywords: symmetries, automorphisms, reachability analysis.

@inproceedings{Schmidt_2000_tacas,
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. Keywords: symmetries, automorphisms, reachability analysis.},
Author = {Karsten Schmidt},
Booktitle = {Tools and Algorithms for the Construction and Analysis of Systems: 6th International Conference, TACAS 2000, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March/April 2000. Proceedings},
Editor = {Susanne Graf and Michael I. Schwartzbach},
Month = mar,
Pages = {315-330},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Integrating Low Level Symmetries into Reachability Analysis},
Volume = 1785,
Year = 2000,
}

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

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{Schmidt_2000_icatpn,
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.},
Author = {Karsten Schmidt},
Booktitle = {Application and Theory of Petri Nets 2000: 21st International Conference, ICATPN 2000, Aarhus, Denmark, June 2000. Proceedings},
Editor = {Mogens Nielsen and Dan Simpson},
Month = jun,
Pages = {465-474},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {{LoLA}: A Low Level Analyser},
Volume = 1825,
Year = 2000,
}

Karsten Schmidt. Narrowing the State Space of Petri Nets Using the State Equation. In Hans-Dieter Burkhard, L. Czaja, A. Skowdron, and Peter H. Starke, editors, Proceedings of the workhop on Concurrency, Specification and Programming, Oct 9-11, 2000, Berlin, pages 243-253, 2000. Humbolt-Universität zu Berlin.

Abstract. Given a (possibly partially defined) state, all firing count vectors that correspond to sequences reaching that state are solutions to a corresponding Petri net state equation. We propose a search strategy that first explores sequences corresponding to a minimal solution of the state equation and then step by step relaxes the search space to other solutions of the equation. This heuristics relies on the observation that in many cases a shortest sequence reaching a state corresponds to a minimal solution of the state equation. Should the target state be non-reachable, our algorithm usually does not reduce the state space at all. We study the impact of the state equation on reachability, present an algorithm that exploits information from the state equation and discuss its application in stateless search as well as its combination with stubborn set reduction.

@inproceedings{Schmidt_2000_csp,
Abstract = {Given a (possibly partially defined) state, all firing count vectors that correspond to sequences reaching that state are solutions to a corresponding Petri net state equation. We propose a search strategy that first explores sequences corresponding to a minimal solution of the state equation and then step by step relaxes the search space to other solutions of the equation. This heuristics relies on the observation that in many cases a shortest sequence reaching a state corresponds to a minimal solution of the state equation. Should the target state be non-reachable, our algorithm usually does not reduce the state space at all. We study the impact of the state equation on reachability, present an algorithm that exploits information from the state equation and discuss its application in stateless search as well as its combination with stubborn set reduction.},
Author = {Karsten Schmidt},
Booktitle = {Proceedings of the workhop on Concurrency, Specification and Programming, Oct 9-11, 2000, Berlin},
Editor = {Hans-Dieter Burkhard and L. Czaja and A. Skowdron and Peter H. Starke},
Organization = {Humbolt-Universit{\"a}t zu Berlin},
Pages = {243-253},
Title = {Narrowing the State Space of {Petri} Nets Using the State Equation},
Year = 2000
}

Abschlüsse / Theses

Harro Wimmel. Algebraische Semantiken für Petri-Netze. PhD thesis, Universität Koblenz-Landau, 2000.

Abstract. Diese Arbeit besch{\"a}ftigt sich mit der Semantik von (P/T) Petri-Netzen. Es werden dabei drei verschiedene Varianten f{\"u}r die Semantik betrachtet: Erstens die Sprache eines Petri-Netzes, bestehend aus Feuersequenzen (Worten) von Transitionen bzw. deren Labelings, zweitens die Stepsprache, bestehend aus Stepworten, in denen Buchstaben, d.h. Feuerungen von Transitionen, nebenl{\"a}ufig sein k{\"o}nnen, und drittens die Pomsetsprache, in deren Pomsets Informationen zur Kausalit{\"a}t enthalten sind. F{\"u}r verschiedene Klassen von Petri-Netzen, so etwa die sicheren und beschr{\"a}nkten Netze, S-Systeme (markierte Graphen) und die Klasse der allgemeinen Petri-Netze (ohne Restriktionen) geben wir algebraische Charakterisierungen {\"u}ber Abschlusseigenschaften f{\"u}r die verschiedenen zugeh{\"o}rigen Sprachklassen an, die jeweils f{\"u}r alle drei Typen von Sprachen uniform sind. Wir unterscheiden weiter zwischen Klassen von Petri-Netzen mit und ohne (unsichtbare) T-Transitionen und mit oder ohne Finalmarkierungen, soweit dies sinnvoll scheint. F{\"u}r die Charakterisierungen {\"u}ber Abschlusseigenschaften geben wir kompositionale Semantiken an, aus deren atomaren (Pomset-, Step-) Sprachen sich die Sprachen von beliebigen Petri-Netzen mittels einiger Operationen (gegen die die jeweilige Sprachklasse abgeschlossen ist) gewinnen lassen. Die notwendigen Abschlusseigenschaften weisen wir z.T. mittels einer neuen Normalform f{\"u}r Petri-Netze nach, die speziell f{\"u}r den Pomsetfall konstruiert wurde. Wir zeigen ferner, dass die Pomsetsprache eines beschr{\"a}nkten Netzes stets auch Pomsetsprache eines sicheren Netzes ist, und dass zu jedem Petri-Netz ein Free-Choice-Netz mit derselben Pomsetsprache existiert. Diese Ergebnisse, wie auch einige der Charakterisierungen, waren bisher nur f{\"u}r den Fall von Sprachen (aus normalen Worten) von Petri-Netzen bekannt.

@phdthesis{Wimmel_2000_phd,
Abstract = {Diese Arbeit besch{\"a}ftigt sich mit der Semantik von (P/T) Petri-Netzen. Es werden dabei drei verschiedene Varianten f{\"u}r die Semantik betrachtet: Erstens die Sprache eines Petri-Netzes, bestehend aus Feuersequenzen (Worten) von Transitionen bzw. deren Labelings, zweitens die Stepsprache, bestehend aus Stepworten, in denen Buchstaben, d.h. Feuerungen von Transitionen, nebenl{\"a}ufig sein k{\"o}nnen, und drittens die Pomsetsprache, in deren Pomsets Informationen zur Kausalit{\"a}t enthalten sind. F{\"u}r verschiedene Klassen von Petri-Netzen, so etwa die sicheren und beschr{\"a}nkten Netze, S-Systeme (markierte Graphen) und die Klasse der allgemeinen Petri-Netze (ohne Restriktionen) geben wir algebraische Charakterisierungen {\"u}ber Abschlusseigenschaften f{\"u}r die verschiedenen zugeh{\"o}rigen Sprachklassen an, die jeweils f{\"u}r alle drei Typen von Sprachen uniform sind. Wir unterscheiden weiter zwischen Klassen von Petri-Netzen mit und ohne (unsichtbare) T-Transitionen und mit oder ohne Finalmarkierungen, soweit dies sinnvoll scheint. F{\"u}r die Charakterisierungen {\"u}ber Abschlusseigenschaften geben wir kompositionale Semantiken an, aus deren atomaren (Pomset-, Step-) Sprachen sich die Sprachen von beliebigen Petri-Netzen mittels einiger Operationen (gegen die die jeweilige Sprachklasse abgeschlossen ist) gewinnen lassen. Die notwendigen Abschlusseigenschaften weisen wir z.T. mittels einer neuen Normalform f{\"u}r Petri-Netze nach, die speziell f{\"u}r den Pomsetfall konstruiert wurde. Wir zeigen ferner, dass die Pomsetsprache eines beschr{\"a}nkten Netzes stets auch Pomsetsprache eines sicheren Netzes ist, und dass zu jedem Petri-Netz ein Free-Choice-Netz mit derselben Pomsetsprache existiert. Diese Ergebnisse, wie auch einige der Charakterisierungen, waren bisher nur f{\"u}r den Fall von Sprachen (aus normalen Worten) von Petri-Netzen bekannt. },
Author = {Harro Wimmel},
School = {Universit{\"a}t Koblenz-Landau},
Title = {{Algebraische Semantiken f{\"u}r Petri-Netze}},
Year = {2000}
}

1999

Zeitschriftenartikel / Journal Articles

Karsten Schmidt. Model-Checking with Coverability Graphs. Formal Methods in System Design, 15(3):239-254, November 1999. [DOI]

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{Schmidt_1999_fmsd,
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.},
Author = {Karsten Schmidt},
Journal = {Formal Methods in System Design},
Month = nov,
Number = 3,
Pages = {239-254},
Publisher = {Springer-Verlag},
Title = {Model-Checking with Coverability Graphs},
Volume = 15,
Year = 1999,
}

Konferenzbeiträge / Conference Papers

Karsten Schmidt. LoLA wird Pfadfinder. In 6. Workshop Algorithmen und Werkzeuge für Petrinetze (AWPN'99), Frankfurt, Germany, October 11.-12., 1999, volume 26 of CEUR Workshop Proceedings, pages 48-53, October 1999. CEUR-WS.org. [PDF]

@inproceedings{Schmidt_1999_awpn,
Author = {Karsten Schmidt},
Booktitle = {6. Workshop Algorithmen und Werkzeuge f{\"u}r Petrinetze (AWPN'99), Frankfurt, Germany, October 11.-12., 1999},
Month = oct,
Pages = {48-53},
Publisher = {CEUR-WS.org},
Series = {CEUR Workshop Proceedings},
Title = {{LoLA wird Pfadfinder}},
Volume = {26},
Year = 1999
}

Karsten Schmidt. Stubborn Sets for Modelchecking the EF/AG-Fragment of CTL. In Workshop on Concurrency, Specification and Programming (CS&P'99), Proceedings, Warsaw, pages 204-213, 1999.

@inproceedings{Schmidt_1999_csp,
Address = {Warsaw},
Author = {Karsten Schmidt},
Booktitle = {Workshop on Concurrency, Specification and Programming (CS\&P'99), Proceedings},
Pages = {204-213},
Title = {Stubborn Sets for Modelchecking the {EF/AG}-Fragment of {CTL}},
Year = 1999
}

Karsten Schmidt. Stubborn Sets for Standard Properties. In Applications and Theory of Petri Nets 1999: 20th International Conference, ICATPN'99, Williamsburg, Virginia, USA, June 1999. Proceedings, volume 1639 of Lecture Notes in Computer Science, pages 46-65, June 1999. Springer-Verlag. [DOI]

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{Schmidt_1999_icatpn,
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.},
Author = {Karsten Schmidt},
Booktitle = {Applications and Theory of Petri Nets 1999: 20th International Conference, ICATPN'99, Williamsburg, Virginia, USA, June 1999. Proceedings},
Month = jun,
Pages = {46-65},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Stubborn Sets for Standard Properties},
Volume = 1639,
Year = 1999,
}

Technische Berichte / Technical Reports

Karsten Schmidt. Integrating Low Level Symmetries into Reachability Analysis. Informatik-Berichte 122, Humboldt-Universität zu Berlin, Berlin, Germany, 1999. [PDF]

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

@techreport{Schmidt_1999_hub_tr122,
Abstract = {We present three methods for the integration of symmetries into reachability analysis. Two of them lead to perfect reduction but their runtime depends on the symmetry structure. The third one works always fast but does not always yield perfect reduction.},
Address = {Berlin, Germany},
Author = {Karsten Schmidt},
Institution = {Humboldt-Universit{\"a}t zu Berlin},
Number = 122,
Title = {Integrating Low Level Symmetries into Reachability Analysis},
Type = {Informatik-Berichte},
Year = 1999
}

Karsten Schmidt. Stubborn Sets for Model Checking the EF/AG Fragment of CTL. Informatik-Berichte 123, Humboldt-Universität zu Berlin, Berlin, Germany, 1999. [PDF]

Abstract. The general stubborn set approach to CTL model checking 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.

@techreport{Schmidt_1999_hub_tr123,
Abstract = {The general stubborn set approach to CTL model checking 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.},
Address = {Berlin, Germany},
Author = {Karsten Schmidt},
Institution = {Humboldt-Universit{\"a}t zu Berlin},
Number = 123,
Title = {Stubborn Sets for Model Checking the {EF/AG} Fragment of {CTL}},
Type = {Informatik-Berichte},
Year = 1999
}

software

Karsten Schmidt. LoLA: A Low Level Analyser. Petrinetzbasiertes Werkzeug zur Verifikation diverser temporallogischer Spezifikationen. Integriert in die Werkzeuge CPN-AMI (Univ. Paris VI), Model Checking Kit (Univ. Stuttgart) und Helena (CNAM Paris). Ca. 30.000 Zeilen Quelltext., 1999. [WWW]

@misc{LoLA,
Author = {Karsten Schmidt},
Howpublished = {Petrinetzbasiertes Werkzeug zur Verifikation diverser temporallogischer Spezifikationen. Integriert in die Werkzeuge CPN-AMI (Univ. Paris VI), Model Checking Kit (Univ. Stuttgart) und Helena (CNAM Paris). Ca. 30.000 Zeilen Quelltext.},
Title = {{LoLA}: A Low Level Analyser},
Year = {1999},
}

1998

Zeitschriftenartikel / Journal Articles

Lutz Priese and Harro Wimmel. A Uniform Approach to True-Concurrency and Interleaving Semantics for Petri Nets. Theor. Comput. Sci., 206(1-2):219-256, October 1998. [DOI]

Abstract. This paper continues a research on universal contexts and semantics for Petri nets started by Nielsen, Priese and Sassone (1995). We consider generalized, labelled Petri nets N where some transitions and places are distinguished as public. They form the interface of N that may communicate with a Petri net context. An elementary calculus, E, is introduced in which one can construct any Petri net with an interface from trivial constants (single places, single transitions) by drawing arcs, adding tokens, and hiding public places and transitions. We prove the existence of a universal context U such that two Petri nets behave the same in any context if their behaviour is equal in the universal context. Let B(U[N]) be the behaviour of N embedded in its universal context, where B may be the interleaving language, step-language, or true-concurrent pomset-language. In any of these cases, B(U[N]) (in contrast to B(N)) turns out to be a compositional semantics of N with respect to the algebra E. In addition, the interleavingand step-semantics are just special cases of the true-concurrency pomset-semantics.

@article{PrieseW_1998_tcs,
Abstract = {This paper continues a research on universal contexts and semantics for Petri nets started by Nielsen, Priese and Sassone (1995). We consider generalized, labelled Petri nets N where some transitions and places are distinguished as public. They form the interface of N that may communicate with a Petri net context. An elementary calculus, E, is introduced in which one can construct any Petri net with an interface from trivial constants (single places, single transitions) by drawing arcs, adding tokens, and hiding public places and transitions. We prove the existence of a universal context U such that two Petri nets behave the same in any context if their behaviour is equal in the universal context. Let B(U[N]) be the behaviour of N embedded in its universal context, where B may be the interleaving language, step-language, or true-concurrent pomset-language. In any of these cases, B(U[N]) (in contrast to B(N)) turns out to be a compositional semantics of N with respect to the algebra E. In addition, the interleavingand step-semantics are just special cases of the true-concurrency pomset-semantics.},
Author = {Lutz Priese and Harro Wimmel},
Journal = {Theor. Comput. Sci.},
Month = oct,
Number = {1-2},
Pages = {219-256},
Title = {A Uniform Approach to True-Concurrency and Interleaving Semantics for {Petri} Nets},
Volume = {206},
Year = {1998},
}

Karsten Schmidt. On the New Low Level Symmetry Tool in INA. Petri Net Newsletter, 54:22-30, 1998. [PDF]

Abstract. In INA 2.1, the whole symmetry approach has been revised. We calculate and store only a generating set of the symmetries. This yields a signicant save of time and space. For every iteration of the symmetries during the generation of reduced reachability or coverability graphs, we compose the symmetries systematically without storing more symmetries permanently than the generating set. The time for composing the symmetries, instead of jumping from pointer to pointer in the old version, is compensated by the ability to exclude whole blocks of symmetries from the iteration.

@article{Schmidt_1998_pnn,
Abstract = {In INA 2.1, the whole symmetry approach has been revised. We calculate and store only a generating set of the symmetries. This yields a signicant save of time and space. For every iteration of the symmetries during the generation of reduced reachability or coverability graphs, we compose the symmetries systematically without storing more symmetries permanently than the generating set. The time for composing the symmetries, instead of jumping from pointer to pointer in the old version, is compensated by the ability to exclude whole blocks of symmetries from the iteration.},
Author = {Karsten Schmidt},
Journal = {Petri Net Newsletter},
Pages = {22-30},
Title = {On the New Low Level Symmetry Tool in {INA}},
Volume = {54},
Year = {1998}
}

Konferenzbeiträge / Conference Papers

Klaus-Peter Neuendorf, Karsten Schmidt, Dimitris Kiritsis, and Paul Xirouchakis. Workflow Modelling and Analysis with Chameleon Nets. In Hans-Dieter Burkhard, L. Czaja, and Peter H. Starke, editors, Workshop Concurrency, Specification and Programming, 28-30 September 1998, pages 156-161, September 1998. Humbolt-Universität zu Berlin. Appeared as Informatik-Berichte Nr. 110.

@inproceedings{NeuendorfSKX_1998_csp,
Author = {Klaus-Peter Neuendorf and Karsten Schmidt and Dimitris Kiritsis and Paul Xirouchakis},
Booktitle = {Workshop Concurrency, Specification and Programming, 28-30 September 1998},
Editor = {Hans-Dieter Burkhard and L. Czaja and Peter H. Starke},
Month = sep,
Note = {Appeared as Informatik-Berichte Nr. 110},
Organization = {Humbolt-Universit{\"a}t zu Berlin},
Pages = {156-161},
Title = {Workflow Modelling and Analysis with Chameleon Nets},
Year = 1998
}

Karsten Schmidt. Goal Oriented Stubborn Sets. In Hans-Dieter Burkhard, L. Czaja, and Peter H. Starke, editors, Workshop Concurrency, Specification and Programming, 28-30 September 1998, pages 204-213, September 1998. Humboldt-Universität zu Berlin. Appeared as Informatik-Berichte Nr. 110.

@inproceedings{Schmidt_1998_csp,
Author = {Karsten Schmidt},
Booktitle = {Workshop Concurrency, Specification and Programming, 28-30 September 1998},
Editor = {Hans-Dieter Burkhard and L. Czaja and Peter H. Starke},
Month = sep,
Note = {Appeared as Informatik-Berichte Nr. 110},
Organization = {Humboldt-Universit{\"a}t zu Berlin},
Pages = {204-213},
Title = {Goal Oriented Stubborn Sets},
Year = 1998
}

Karsten Schmidt. Symmetrien in der Erreichbarkeitsanalyse. In Jörg Desel, P. Kemper, Ekkart Kindler, and Andreas Oberweis, editors, 5. Workshop Algorithmen und Werkzeuge für Petrinetze (AWPN 1998), pages 101-106, 1998. Universität Dortmund.

Abstract. Various approaches to incorporate known symmetries of ordinary Petri nets into the reachability analysis are sketched and evaluated.

@inproceedings{Schmidt_1998_awpn,
Abstract = {Various approaches to incorporate known symmetries of ordinary Petri nets into the reachability analysis are sketched and evaluated.},
Author = {Karsten Schmidt},
Booktitle = {5. Workshop Algorithmen und Werkzeuge f{\"u}r Petrinetze (AWPN 1998)},
Editor = {J{\"o}rg Desel and P. Kemper and Ekkart Kindler and Andreas Oberweis},
Organization = {Universit{\"a}t Dortmund},
Pages = {101-106},
Title = {{Symmetrien in der Erreichbarkeitsanalyse}},
Year = 1998
}

1997

Konferenzbeiträge / Conference Papers

Karsten Schmidt. Modelchecking on Symbolic Reachability Graphs of Petri nets. In Jörg Desel, Ekkart Kindler, and Andreas Oberweis, editors, 4. Workshop Algorithmen und Werkzeuge für Petrinetze (AWPN 1997), pages 43-48, September 1997. Humbolt-Universität zu Berlin.

@inproceedings{Schmidt_1997_awpn,
Author = {Karsten Schmidt},
Booktitle = {4. Workshop Algorithmen und Werkzeuge f{\"u}r Petrinetze (AWPN 1997)},
Editor = {J{\"o}rg Desel and Ekkart Kindler and Andreas Oberweis},
Month = sep,
Organization = {Humbolt-Universit{\"a}t zu Berlin},
Pages = {43-48},
Title = {Modelchecking on Symbolic Reachability Graphs of {Petri} nets},
Year = 1997
}

Karsten Schmidt. Modelchecking with Coverability Graphs. In Workshop on Concurrency, Specification and Programming (CS&P'97), Proceedings, Warsaw, Poland, pages 112-123, 1997.

@inproceedings{Schmidt_1997_csp,
Address = {Warsaw, Poland},
Author = {Karsten Schmidt},
Booktitle = {Workshop on Concurrency, Specification and Programming (CS\&P'97), Proceedings},
Pages = {112-123},
Title = {Modelchecking with Coverability Graphs},
Year = 1997
}

Karsten Schmidt. Siphons, Traps, and High-Level Nets with Infinite Color Domains. In Pierre Azéma and Gianfranco Balbo, editors, Application and Theory of Petri Nets 1997, 18th International Conference, ICATPN '97, Toulouse, France, June 23-27, 1997, Proceedings, volume 1248 of Lecture Notes in Computer Science, pages 271-289, June 1997. Springer-Verlag. [DOI]

Abstract. Commoner's Theorem establishes a relation between siphons, traps and liveness in free choice systems. Most proofs of this theorem do explicitly involve the finiteness of the net. Therefore we cannot apply the theorem directly to high level nets with infinite color domains. We prove generalisations of both the `if' and the `only if' direction to the infinite case which unfortunately cannot be combined to an `iff' statement. We present examples which show that there are both live and non-live nets in the grey zone left by our generalisations. Our approach enlarges the application area of Commoner's theorem to infinite Petri nets, compared with an earlier generalisation to a class of free choice predicate event system, but does not cover the other approach completely.

@inproceedings{Schmidt_1997_icatpn1,
Abstract = {Commoner's Theorem establishes a relation between siphons, traps and liveness in free choice systems. Most proofs of this theorem do explicitly involve the finiteness of the net. Therefore we cannot apply the theorem directly to high level nets with infinite color domains. We prove generalisations of both the `if' and the `only if' direction to the infinite case which unfortunately cannot be combined to an `iff' statement. We present examples which show that there are both live and non-live nets in the grey zone left by our generalisations. Our approach enlarges the application area of Commoner's theorem to infinite Petri nets, compared with an earlier generalisation to a class of free choice predicate event system, but does not cover the other approach completely.},
Author = {Karsten Schmidt},
Booktitle = {Application and Theory of Petri Nets 1997, 18th International Conference, ICATPN '97, Toulouse, France, June 23-27, 1997, Proceedings},
Editor = {Pierre Az{\'e}ma and Gianfranco Balbo},
Month = jun,
Pages = {271-289},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Siphons, Traps, and High-Level Nets with Infinite Color Domains},
Volume = 1248,
Year = 1997,
}

Karsten Schmidt. Verification of Siphons and Traps for Algebraic Petri nets. In Pierre Azéma and Gianfranco Balbo, editors, Application and Theory of Petri Nets 1997, 18th International Conference, ICATPN '97, Toulouse, France, June 23-27, 1997, Proceedings, volume 1248 of Lecture Notes in Computer Science, pages 427-446, June 1997. Springer-Verlag. [DOI]

Abstract. Siphons and traps are structures which allow for some implications on the net's behaviour and can be used in manual correctness proofs for concurrent systems. We introduce symbolic representations of siphons and traps which work quite well even in infinite cases and are still intuitively readable. The verification of symbolic siphons and traps is traced back to unification and structural induction on the terms. This approach is motivated by some additional considerations. For unification and other proposed structural reasoning mechanisms tool support is given by completeness proof tools studied in the theorem-proving community.

@inproceedings{Schmidt_1997_icatpn2,
Abstract = {Siphons and traps are structures which allow for some implications on the net's behaviour and can be used in manual correctness proofs for concurrent systems. We introduce symbolic representations of siphons and traps which work quite well even in infinite cases and are still intuitively readable. The verification of symbolic siphons and traps is traced back to unification and structural induction on the terms. This approach is motivated by some additional considerations. For unification and other proposed structural reasoning mechanisms tool support is given by completeness proof tools studied in the theorem-proving community.},
Author = {Karsten Schmidt},
Booktitle = {Application and Theory of Petri Nets 1997, 18th International Conference, ICATPN '97, Toulouse, France, June 23-27, 1997, Proceedings},
Editor = {Pierre Az{\'e}ma and Gianfranco Balbo},
Month = jun,
Pages = {427-446},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Verification of Siphons and Traps for Algebraic {Petri} nets},
Volume = 1248,
Year = 1997,
}

Harro Wimmel and Lutz Priese. Algebraic Characterization of Petri Net Pomset Semantics. In Antoni W. Mazurkiewicz and Józef Winkowski, editors, CONCUR '97: Concurrency Theory, 8th International Conference, Warsaw, Poland, July 1-4, 1997, Proceedings, volume 1243 of Lecture Notes in Computer Science, pages 406-420, July 1997. Springer-Verlag. [DOI]

Abstract. Sets of pomsets are frequently used as a true-concurrency, linear-time semantics of Petri nets. For a Petri net N, let P(N), a set of pomsets, denote the pomset behaviour of N, and let P:=P(N)|N is a Petri net denote the class of pomset behaviours of Petri nets, a generalization of L, the class of all Petri net languages. We present here an algebraic characterization for P, similar to the known algebraic characterizations for L.

@inproceedings{WimmelP_1997_concur,
Abstract = {Sets of pomsets are frequently used as a true-concurrency, linear-time semantics of Petri nets. For a Petri net N, let P(N), a set of pomsets, denote the pomset behaviour of N, and let P:=P(N)|N is a Petri net denote the class of pomset behaviours of Petri nets, a generalization of L, the class of all Petri net languages. We present here an algebraic characterization for P, similar to the known algebraic characterizations for L.},
Author = {Harro Wimmel and Lutz Priese},
Booktitle = {CONCUR '97: Concurrency Theory, 8th International Conference, Warsaw, Poland, July 1-4, 1997, Proceedings},
Editor = {Antoni W. Mazurkiewicz and J{\'o}zef Winkowski},
Month = jul,
Pages = {406-420},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Algebraic Characterization of {Petri} Net Pomset Semantics},
Volume = {1243},
Year = {1997},
}

Technische Berichte / Technical Reports

Karsten Schmidt. Applying Reduction Rules to Algebraic Petri nets. Technical Report A44, Helsinki University of Technology, Helsinki, Finland, 1997.

@techreport{Schmidt_1997_hut_tra44,
Address = {Helsinki, Finland},
Author = {Karsten Schmidt},
Institution = {Helsinki University of Technology},
Number = {A44},
Title = {Applying Reduction Rules to Algebraic {Petri} nets},
Type = {Technical Report},
Year = 1997
}

Karsten Schmidt. How to Calculate Symmetries of Petri Nets. Technical Report MATH-AL-8-1997, Dresden University of Technology, Dresden, Germany, 1997. [PDF]

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 difffierent 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.

@techreport{Schmidt_1997_tud_al8,
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 difffierent 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.},
Address = {Dresden, Germany},
Author = {Karsten Schmidt},
Institution = {Dresden University of Technology},
Number = {MATH-AL-8-1997},
Title = {How to Calculate Symmetries of {Petri} Nets},
Type = {Technical Report},
Year = {1997}
}

Karsten Schmidt. Model Checking on Symbolic Reachability Graphs of Petri nets. Technical Report MATH-AL-10-1997, Dresden University of Technology, Dresden, Germany, 1997.

@techreport{Schmidt_1997_tud_al10,
Address = {Dresden, Germany},
Author = {Karsten Schmidt},
Institution = {Dresden University of Technology},
Number = {MATH-AL-10-1997},
Title = {Model Checking on Symbolic Reachability Graphs of {Petri} nets},
Type = {Technical Report},
Year = 1997
}

Karsten Schmidt. Model-Checking with Coverability Graphs. Technical Report MATH-AL-9-1997, Dresden University of Technology, Dresden, Germany, 1997. [PDF]

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 difffierent 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.

@techreport{Schmidt_1997_tud_al9,
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 difffierent 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.},
Address = {Dresden, Germany},
Author = {Karsten Schmidt},
Institution = {Dresden University of Technology},
Number = {MATH-AL-9-1997},
Title = {Model-Checking with Coverability Graphs},
Type = {Technical Report},
Year = {1997}
}

1996

Konferenzbeiträge / Conference Papers

Karsten Schmidt. Ein Verfahren zur Verifikation von `Immer möglich' und `Möglich, dass immer'-Eigenschaften. In Jörg Desel, Ekkart Kindler, and Andreas Oberweis, editors, 3. Workshop Algorithmen und Werkzeuge für Petrinetze (AWPN 1996), October 1996. Universität Karlsruhe, Universität Karlsruhe. [PDF]

Abstract. Zur Verifikation der im Titel genannten Klasse von Formeln einer {\"u}ber der Interleaving-Semantik eines Platz-Transitions-Netzes interpretierten Branching-Time-Logik werden nur die terminalen stark zusammenh{\"a}ngenden Komponenten des Erreichbarkeitsgraphen ben{\"o}tigt. Das vorgeschlagene Verfahren kombiniert die Methode sturer Mengen zum m{\"o}glichst schnellen und sparsamen Erreichen der terminalen Komponenten eines Graphen mit der symbolischen Berechnung von Erreichbarkeitsmengen mit Entscheidungsgraphen zur vollst{\"a}ndigen, aber kompakten Repr{\"a}sentation der terminalen Komponenten.

@inproceedings{Schmidt_1996_awpn,
Abstract = {Zur Verifikation der im Titel genannten Klasse von Formeln einer {\"u}ber der Interleaving-Semantik eines Platz-Transitions-Netzes interpretierten Branching-Time-Logik werden nur die terminalen stark zusammenh{\"a}ngenden Komponenten des Erreichbarkeitsgraphen ben{\"o}tigt. Das vorgeschlagene Verfahren kombiniert die Methode sturer Mengen zum m{\"o}glichst schnellen und sparsamen Erreichen der terminalen Komponenten eines Graphen mit der symbolischen Berechnung von Erreichbarkeitsmengen mit Entscheidungsgraphen zur vollst{\"a}ndigen, aber kompakten Repr{\"a}sentation der terminalen Komponenten.},
Author = {Karsten Schmidt},
Booktitle = {3. Workshop Algorithmen und Werkzeuge f{\"u}r Petrinetze (AWPN 1996)},
Editor = {J{\"o}rg Desel and Ekkart Kindler and Andreas Oberweis},
Month = oct,
Organization = {Universit{\"a}t Karlsruhe},
Publisher = {Universit{\"a}t Karlsruhe},
Title = {{Ein Verfahren zur Verifikation von `Immer m{\"o}glich' und `M{\"o}glich, da{\ss} immer'-Eigenschaften}},
Year = 1996
}

Karsten Schmidt. Siphons and Traps for Algebraic Petri nets. In Workshop on Concurrency, Specification and Programming (CS&P'96), Berlin, Proceedings, pages 157-168, October 1996. [PDF]

Abstract. We overview recent results concerning the symbolic verification and calculation of siphons and traps for algebraic Petri nets and their relation to the net behavior
.

@inproceedings{Schmidt_1996_csp,
Abstract = {We overview recent results concerning the symbolic verification and calculation of siphons and traps for algebraic Petri nets and their relation to the net behavior
.},
Author = {Karsten Schmidt},
Booktitle = {Workshop on Concurrency, Specification and Programming (CS\&P'96), Berlin, Proceedings},
Month = oct,
Pages = {157-168},
Title = {Siphons and Traps for Algebraic {Petri} nets},
Year = 1996
}

Technische Berichte / Technical Reports

Karsten Schmidt. How to Calculate Symbolically Siphons and Traps of Algebraic Petri Nets. Technical Report A39, Helsinki University of Technology, Helsinki, Finland, August 1996. [PDF]

Abstract. We present a symbolic approach to the calculation of siphons and traps for algebraic Petri nets where the color domains are specied without equations and with at most unary operation symbols.

@techreport{Schmidt_1996_hut_tra39,
Abstract = {We present a symbolic approach to the calculation of siphons and traps for algebraic Petri nets where the color domains are specied without equations and with at most unary operation symbols.},
Address = {Helsinki, Finland},
Author = {Karsten Schmidt},
Institution = {Helsinki University of Technology},
Month = aug,
Number = {A39},
Title = {How to Calculate Symbolically Siphons and Traps of Algebraic {Petri} Nets},
Type = {Technical Report},
Year = 1996
}

Abschlüsse / Theses

Karsten Schmidt. Symbolische Analysemethoden für algebraische Petri-Netze. Dissertation, Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II, Berlin, Germany, 1996. Erschienen im Dieter Bertz Verlag. 246 Seiten, ISBN 3-929470-54-3.

Abstract. The text of this book is a dissertation, submitted to Humboldt-University in Berlin. It deals with symbolic analysis methods for algebraic Petri nets. For this kind of high--level nets algebraic specifications are used to describe the individuality of tokens. Though it is possible to specify infinite data types and therefore many standard properties are undecidable for this net class there should be a computer aid for the analysis of algebraic nets. The formalism of algebraic specifications provides a syntactic framework for symbolic calculations, in particular rewriting techniques for deciding equivalence of descriptions and solving equations. We study how these techniques can be involved in well known Petri net analysis methods, namely invariant calculus and reachability graph construction. Chapter I introduces the main concepts used in the remaining chapters. It contains a short introduction of algebraic specifications, the definition of algebraic Petri nets and their interpretation. In chapter II we compare invariant definitions for place transition nets, coloured nets and algebraic nets. Then we investigate the structure of place invariants and transition invariants for algebraic nets and end up in the characterization of small generator sets. We develop an algorithm to enumerate such a generator set. Thereby the calculations are traced back to unification problems. We prove that an algorithm which computes a generator set for all transition invariants cannot always terminate since it is undecidable whether an algebraic net has non-trivial transition invariants or not. We propose simplifications of the analysis problems which allow to circumvent the major computational problems. In chapter III we take up the idea of parameterized reachability graphs which have been introduced for predicate/transition nets. We translate this method to the formalism of algebraic nets. Thereby we apply several improvements which allow stronger implications between the graph and the behavior of the underlying nets. We present ideas how the stubborn set method can be used to reduce the size of a parametrized reachability graph. Chapter IV contains examples where we demonstrate our methods and general conclusions.

@phdthesis{Schmidt_1996_diss,
Abstract = {The text of this book is a dissertation, submitted to Humboldt-University in Berlin. It deals with symbolic analysis methods for algebraic Petri nets. For this kind of high--level nets algebraic specifications are used to describe the individuality of tokens. Though it is possible to specify infinite data types and therefore many standard properties are undecidable for this net class there should be a computer aid for the analysis of algebraic nets. 

The formalism of algebraic specifications provides a syntactic framework for symbolic calculations, in particular rewriting techniques for deciding equivalence of descriptions and solving equations. We study how these techniques can be involved in well known Petri net analysis methods, namely invariant calculus and reachability graph construction. 

Chapter I introduces the main concepts used in the remaining chapters. It contains a short introduction of algebraic specifications, the definition of algebraic Petri nets and their interpretation. 

In chapter II we compare invariant definitions for place transition nets, coloured nets and algebraic nets. Then we investigate the structure of place invariants and transition invariants for algebraic nets and end up in the characterization of small generator sets. We develop an algorithm to enumerate such a generator set. Thereby the calculations are traced back to unification problems. We prove that an algorithm which computes a generator set for all transition invariants cannot always terminate since it is undecidable whether an algebraic net has non-trivial transition invariants or not. We propose simplifications of the analysis problems which allow to circumvent the major computational problems. 

In chapter III we take up the idea of parameterized reachability graphs which have been introduced for predicate/transition nets. We translate this method to the formalism of algebraic nets. Thereby we apply several improvements which allow stronger implications between the graph and the behavior of the underlying nets. We present ideas how the stubborn set method can be used to reduce the size of a parametrized reachability graph. 

Chapter IV contains examples where we demonstrate our methods and general conclusions. },
Address = {Berlin, Germany},
Author = {Karsten Schmidt},
Note = {Erschienen im Dieter Bertz Verlag. 246 Seiten, ISBN 3-929470-54-3},
School = {Humboldt-Universit{\"a}t zu Berlin, Mathematisch-Naturwissenschaftliche Fakult{\"a}t II},
Title = {{Symbolische Analysemethoden f{\"u}r algebraische Petri-Netze}},
Type = {Dissertation},
Year = 1996
}

1995

Konferenzbeiträge / Conference Papers

Karsten Schmidt. On the Computation of Place Invariants for Algebraic Petri Nets. In Jörg Desel, editor, Structures in Concurrency Theory, Proceedings of the International Workshop on Structures in Concurrency Theory (STRICT), Berlin, 11-13 May 1995, pages 310-325, May 1995. [PDF]

@inproceedings{Schmidt_1995_strict,
Author = {Karsten Schmidt},
Booktitle = {Structures in Concurrency Theory, Proceedings of the International Workshop on Structures in Concurrency Theory (STRICT), Berlin, 11-13 May 1995},
Editor = {J{\"o}rg Desel},
Month = may,
Pages = {310-325},
Title = {On the Computation of Place Invariants for Algebraic {Petri} Nets},
Year = {1995}
}

Karsten Schmidt. Parameterized Reachability Trees for Algebraic Petri Nets. In Giorgio De Michelis and Michel Diaz, editors, Application and Theory of Petri Nets 1995, 16th International Conference, Turin, Italy, June 26-30, 1995, Proceedings, volume 935 of Lecture Notes in Computer Science, pages 392-411, 1995. Springer-Verlag. [DOI]

Abstract. Parameterized reachability trees have been proposed by M. Lindquist for predicate/transition nets. We discuss the application of this concept to algebraic nets. For this purpose a modification of several definitions is necessary due to the different net descriptions, transition rules and theoretical backgrounds. That's why we present the concept from the bottom for algebraic nets. Furthermore we discuss the combination of parameterized reachability analysis with the well known stubborn set method.

@inproceedings{Schmidt_1995_atpn,
Abstract = {Parameterized reachability trees have been proposed by M. Lindquist for predicate/transition nets. We discuss the application of this concept to algebraic nets. For this purpose a modification of several definitions is necessary due to the different net descriptions, transition rules and theoretical backgrounds. That's why we present the concept from the bottom for algebraic nets. Furthermore we discuss the combination of parameterized reachability analysis with the well known stubborn set method.},
Author = {Karsten Schmidt},
Booktitle = {Application and Theory of Petri Nets 1995, 16th International Conference, Turin, Italy, June 26-30, 1995, Proceedings},
Editor = {Giorgio De Michelis and Michel Diaz},
Pages = {392-411},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science},
Title = {Parameterized Reachability Trees for Algebraic {Petri} Nets},
Volume = {935},
Year = {1995},
}

Karsten Schmidt. Symmetrieberechnung. In Jörg Desel, H. Fleischhack, Andreas Oberweis, and M. Sonnenschein, editors, Workshop Algorithmen und Werkzeuge für Petrinetze, Oldenburg, October 10-11, 1995, pages 1-3, October 1995. Universität Oldenburg. [PDF]

@inproceedings{Schmidt_1995_awpn,
Author = {Karsten Schmidt},
Booktitle = {Workshop Algorithmen und Werkzeuge f{\"u}r Petrinetze, Oldenburg, October 10-11, 1995},
Editor = {J{\"o}rg Desel and H. Fleischhack and Andreas Oberweis and M. Sonnenschein},
Month = oct,
Organization = {Universit{\"a}t Oldenburg},
Pages = {1-3},
Title = {Symmetrieberechnung},
Year = {1995}
}

Karsten Schmidt. Symmetry Calculation. In Proc. Workshop CS&P, Warsaw, Poland, pages 147-162, October 1995. [PDF]

Abstract. We consider several applications of net symmetries for various Petri net classes. We show, that almost all computations of symmetry groups for different net classes and almost all decision problems which appear when applying symmetric reductions can be traced back to a single algorithm. This is a very pleasing result for a multi purpose analysis tool like INA (see for instance [Fel92]). For the two exceptions from this general result - the computation of symmetry groups for self-modifying nets ([Val77]) and the decision of the coverability problem for place/transition nets we present extensions of the basic algorithm.

@inproceedings{Schmidt_1995_csp,
Abstract = {We consider several applications of net symmetries for various Petri net classes. We show, that almost all computations of symmetry groups for different net classes and almost all decision problems which appear when applying symmetric reductions can be traced back to a single algorithm. This is a very pleasing result for a multi purpose analysis tool like INA (see for instance [Fel92]). For the two exceptions from this general result - the computation of symmetry groups for self-modifying nets ([Val77]) and the decision of the coverability problem for place/transition nets we present extensions of the basic algorithm.},
Author = {Karsten Schmidt},
Booktitle = {Proc. Workshop CS\&P, Warsaw, Poland},
Month = oct,
Pages = {147-162},
Title = {Symmetry Calculation},
Year = {1995}
}

1994

Konferenzbeiträge / Conference Papers

Karsten Schmidt. Parameterized Reachability Trees for Algebraic Petri Nets. In Workshop CS&P Berlin 1994, 1994. [PDF]

@inproceedings{Schmidt_1994_csp,
Author = {Karsten Schmidt},
Booktitle = {Workshop CS\&P Berlin 1994},
Title = {Parameterized Reachability Trees for Algebraic {Petri} Nets},
Year = {1994}
}

Karsten Schmidt. Symbolische Analysemethoden für algebraische Petrinetze. In Algorithmen und Werkzeuge für Petrinetze, Workshop der GI-Fachrgruppe 0.0.1 ``Petrinetze und verwandte Systemmodelle'', Berlin, pages 55-60, October 1994. [PDF]

@inproceedings{Schmidt_1994_awpn,
Author = {Karsten Schmidt},
Booktitle = {Algorithmen und Werkzeuge f{\"u}r Petrinetze, Workshop der GI-Fachrgruppe 0.0.1 ``Petrinetze und verwandte Systemmodelle'', Berlin},
Month = oct,
Pages = {55-60},
Title = {{Symbolische Analysemethoden f{\"u}r algebraische Petrinetze}},
Year = {1994}
}

Technische Berichte / Technical Reports

Karsten Schmidt. Symmetries of Petri Nets. Informatik-Berichte 33, Humboldt-Universität zu Berlin, Berlin, Germany, October 1994. [PDF]

Abstract. A definition of Petri net symmetries is given and an algorithm is introduced, which computes these symmetries. Then three examples are given how algorithms from different fields of Petri net analysis can be improved using symmetries, namely computation of reachability graphs, semipositive place invariants and structural deadlocks, respectively.

@techreport{Schmidt_1994_hub_tr33,
Abstract = {A definition of Petri net symmetries is given and an algorithm is introduced, which computes these symmetries. Then three examples are given how algorithms from different fields of Petri net analysis can be improved using symmetries, namely computation of reachability graphs, semipositive place invariants and structural deadlocks, respectively.},
Address = {Berlin, Germany},
Author = {Karsten Schmidt},
Institution = {Humboldt-Universit{\"a}t zu Berlin},
Month = oct,
Number = {33},
Title = {Symmetries of {Petri} Nets},
Type = {Informatik-Berichte},
Year = {1994}
}

Karsten Schmidt. T-Invariants of Algebraic Petri Nets. Informatik-Berichte 31, Humboldt-Universität zu Berlin, Berlin, Germany, September 1994. [PDF]

Abstract. A detailed observation of the structure of T-invariants leads to the definition of a subset of invariants, which generates the whole set of invariants by linear combination and instantiation and the elements of which have a simple structure by means of computation. Then an algorithmically insoluble problem concerning T-invariants is presented to justify the non-termination of the algorithm which computes this subset of invariants. The algorithm consists mainly of a clever application of term unification.

@techreport{Schmidt_1994_hub_tr31,
Abstract = {A detailed observation of the structure of T-invariants leads to the definition of a subset of invariants, which generates the whole set of invariants by linear combination and instantiation and the elements of which have a simple structure by means of computation. Then an algorithmically insoluble problem concerning T-invariants is presented to justify the non-termination of the algorithm which computes this subset of invariants. The algorithm consists mainly of a clever application of term unification.},
Address = {Berlin, Germany},
Author = {Karsten Schmidt},
Institution = {Humboldt-Universit{\"a}t zu Berlin},
Month = sep,
Number = {31},
Title = {T-Invariants of Algebraic {Petri} Nets},
Type = {Informatik-Berichte},
Year = {1994}
}

1993

Zeitschriftenartikel / Journal Articles

Karsten Schmidt. Symmetries of Petri Nets. Petri Net Newsletter, 43:9-25, 1993.

@article{Schmidt_1993_pnn,
Author = {Karsten Schmidt},
Journal = {Petri Net Newsletter},
Pages = {9-25},
Title = {Symmetries of {Petri} Nets},
Volume = {43},
Year = {1993}
}

Konferenzbeiträge / Conference Papers

Karsten Schmidt. Computation of Invariants for Algebraic Petri Nets. In Workshop on Concurrency, Specification and Programming (CS&P'93), Warsaw, Poland, Proceedings, pages 196-218, 1993. [PDF]

@inproceedings{Schmidt_1993_csp,
Author = {Karsten Schmidt},
Booktitle = {Workshop on Concurrency, Specification and Programming (CS\&P'93), Warsaw, Poland, Proceedings},
Pages = {196-218},
Title = {Computation of Invariants for Algebraic {Petri} Nets},
Year = {1993}
}

Abschlüsse / Theses

Karsten Schmidt. Implementation der Umgebung eines Programms zur Prüfung und Berechnung von Invarianten algebraischer Petrinetze. Diplomarbeit, Humboldt-Universität zu Berlin, Fachbereich Informatik, Berlin, Germany, November 1993. [PDF]

Abstract. Nach der Definition des Begriff
s algebraischer Petrinetze und der Diskussion der dazugehorenden Invariantenbegri
e werden die wesentlichen Entwurfsentscheidungen zur Implementation der Umgebung des Programms IVAN Invariant Verification of Algebraic Nets besprochen Dieses Programm soll gegebene Invarianten auf Korrektheit {\"u}berprufen und Hilfswerkzeuge zur Unterstutzung der Suche nach Invarianten anbieten Zur Umgebung von IVAN gehoren ein Kommandointerpreter zur interaktiven Anwendung der Werkzeuge und zur Bearbeitung von algebraischen Netzen und Invarianten sowie ein Parser zum Einlesen externer Netz und Invariantenbeschreibungen.

@mastersthesis{Schmidt_1993_da,
Abstract = {Nach der Definition des Begriff
s algebraischer Petrinetze und der Diskussion der dazugehorenden Invariantenbegri
e werden die wesentlichen Entwurfsentscheidungen zur Implementation der Umgebung des Programms IVAN Invariant Verification of Algebraic Nets besprochen Dieses Programm soll gegebene Invarianten auf Korrektheit {\"u}berprufen und Hilfswerkzeuge zur Unterstutzung der Suche nach Invarianten anbieten Zur Umgebung von IVAN gehoren ein Kommandointerpreter zur interaktiven Anwendung der Werkzeuge und zur Bearbeitung von algebraischen Netzen und Invarianten sowie ein Parser zum Einlesen externer Netz und Invariantenbeschreibungen.},
Address = {Berlin, Germany},
Author = {Karsten Schmidt},
Month = nov,
School = {Humboldt-Universit{\"a}t zu Berlin, Fachbereich Informatik},
Title = {{Implementation der Umgebung eines Programms zur Pr{\"u}fung und Berechnung von Invarianten algebraischer Petrinetze}},
Type = {Diplomarbeit},
Year = {1993}
}

1991

Zeitschriftenartikel / Journal Articles

Karsten Schmidt and Peter H. Starke. An Algorithm to Compute the Symmetries of Petri Nets. Petri Net Newsletter, 40:25-30, December 1991.

@article{SchmidtS_1991_pnn,
Author = {Karsten Schmidt and Peter H. Starke},
Journal = {Petri Net Newsletter},
Month = dec,
Pages = {25-30},
Title = {An Algorithm to Compute the Symmetries of {Petri} Nets},
Volume = {40},
Year = {1991}
}