Transactions on Petri Nets and Other Models of Concurrency IX

Name: Transactions on Petri Nets and Other Models of Concurrency IX
ISBN: 978-3-662-45729-0

Erstes Kapitel lesen

Buchreihe: Lecture Notes in Computer Science

Herausgeber: Maciej Koutny, Serge Haddad, Alex Yakovlev

Verlag: Springer Berlin Heidelberg

Print ISBN: 978-3-662-45729-0

Electronic ISBN: 978-3-662-45730-6

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Zugang erhalten Inhaltsverzeichnis

Über dieses Buch

These Transactions publish archival papers in the broad area of Petri nets and other models of concurrency, ranging from theoretical work to tool support and industrial applications. ToPNoC issues are published as LNCS volumes, and hence are widely distributed and indexed. This Journal has its own Editorial Board which selects papers based on a rigorous two-stage refereeing process. ToPNoC contains: - Revised versions of a selection of the best papers from workshops and tutorials at the annual Petri net conferences - Special sections/issues within particular subareas (similar to those published in the Advances in Petri Nets series) - Other papers invited for publication in ToPNoC - Papers submitted directly to ToPNoC by their authors The 9th volume of ToPNoC contains revised and extended versions of a selection of the best workshop papers presented at the 34th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2013) and the 13th International Conference on Application of Concurrency to System Design (ACSD 2013). It also contains one paper submitted directly to ToPNoC. The 8 papers cover a diverse range of topics including model checking and system verification, refinement and synthesis, foundational work on specific classes of Petri nets, and innovative applications of Petri nets and other models of concurrency. Application areas covered in this volume are: biological systems, communication protocols, business processes, distributed systems, and multi-agent systems. Thus, this volume gives a good view of ongoing concurrent systems and Petri nets research.

Inhaltsverzeichnis

Frontmatter

Decidability of $$k$$ -Soundness for Workflow Nets with an Unbounded Resource

Abstract

A resource workflow net (RWF-net) is a workflow net, supplied with an additional set of initially marked resource places. Resources can be consumed and/or produced by transitions. Neither the intermediate nor final resource markings are constrained, hence a net can have an infinite number of different reachable states.

An RWF-net with $k$ tokens in the initial place and a certain number of resource tokens in resource places is called $k$-sound if it properly terminates with $k$ tokens in the final place and, moreover, adding any extra initial resource does not violate its proper termination. An unmarked RWF-net is $k$-sound if it is $k$-sound for some initial resource. In this paper we prove the decidability of both marked and unmarked $k$-soundness for a restricted class of RWF-nets with a single unbounded resource place (1-dim RWF-nets). We present an algorithm for computing the minimal $k$-sound resource for a given sound 1-dim RWF-net.

Vladimir A. Bashkin, Irina A. Lomazova

Modeling Distributed Private Key Generation by Composing Petri Nets

Abstract

We present a Petri net model of a protocol for the distributed generation of id-based private keys. Those keys can then be used for secure communications. The components of the system are built as refinements of a common interface, by applying a formal operation based on a class of morphisms between Elementary Net Systems. It is then shown that we can derive behavioural properties of the composed system without building it explicitly, by exploiting properties of the given morphisms.

Luca Bernardinello, Görkem Kılınç, Elisabetta Mangioni, Lucia Pomello

Software Engineering with Petri Nets: A Web Service and Agent Perspective

Abstract

The context of this paper is given through a software engineering approach that uses Petri nets as executable code. We apply the particular understanding that Petri nets are not only used to model systems for design purposes but also to implement system components. Following this approach, we develop complex Petri net-based software applications according to the multi-agent paradigm. Agent-internal as well as agent-spanning processes are implemented directly as (high-level) Petri nets. These nets are essential parts of the resulting software application – alongside other parts (operational and declarative ones), which are implemented using traditional ways of programming.

One of our goals is to open our Petri net-based agent framework Mulan/Capa so that multi-agent applications can communicate and interact with other systems – especially with Web-based applications. With this intention, we present a gateway solution to enable Petri net-based applications to access Web services as well as to offer Web services to other applications: the WebGateway. In addition to describing the WebGateway extension itself, we use its presentation to demonstrate the practicability of the Petri net-based software engineering approach in general. We emphasize the benefit of having Petri net models serve as conceptual models that progressively refine the constructed system from simple models to well-defined specifications of the systems. This improves the understanding of the systems.

Tobias Betz, Lawrence Cabac, Michael Duvigneau, Thomas Wagner, Matthias Wester-Ebbinghaus

Modeling Organizational Structures and Agent Knowledge for Mulan Applications

Abstract

In software engineering the initial setup of a system, as well as the self-adaptation processes within a system are challenging tasks. We address these challenges by providing explications of organizational structures through modeling. In this paper we present a service-oriented perspective on the organizational structure of MAS and we present modeling techniques and tools for supporting this perspective. We pursue a model-driven approach and a tight integration between various models on the one hand and between the models and the generated code on the other hand. In particular, we use ontologies to define a meta-model for organizational structures in a way that we can easily generate the initial content of agent knowledge bases in the form of FIPA semantic language (SL) fragments, depending on the positions the agents occupy in the context of the organizational structure. This allows the agents to reason and to communicate about their organizational embedding, which is a prerequisite for self-adaptation in multi-agent systems.

Lawrence Cabac, David Mosteller, Matthias Wester-Ebbinghaus

A Canonical Contraction for Safe Petri Nets

Abstract

Under maximal semantics, the occurrence of an event $a$ in a concurrent run of an occurrence net may imply the occurrence of other events, not causally related to $a$, in the same run. In recent works, we have formalized this phenomenon as the reveals relation, and used it to obtain a contraction of sets of events called facets in the context of occurrence nets. Here, we extend this idea to propose a canonical contraction of general safe Petri nets into pieces of partial-order behaviour which can be seen as “macro-transitions” since all their events must occur together in maximal semantics. On occurrence nets, our construction coincides with the facets abstraction.Our contraction preserves the maximal semantics in the sense that the maximal processes of the contracted net are in bijection with those of the original net.

Thomas Chatain, Stefan Haar

Symbolic Termination and Confluence Checking for ECA Rules

Abstract

Event-condition-action (ECA) rules can specify decision processes and are widely used in reactive systems and active database systems. Applying formal verification techniques to guarantee properties of the designed ECA rules is essential to help the error-prone procedure of collecting and translating expert knowledge. However, while the nondeterministic and concurrent semantics of ECA rule execution enhances expressiveness, it also makes analysis and verification more difficult. We propose an approach to analyze the dynamic behavior of a set of ECA rules, by first translating them into an extended Petri net, then studying two fundamental correctness properties: termination and confluence. Our experimental results show that the symbolic algorithms we present greatly improve scalability.

Xiaoqing Jin, Yousra Lembachar, Gianfranco Ciardo

Tissue Systems and Petri Net Synthesis

Abstract

Tissue systems are a computational abstraction of the chemical reactions and transport of molecules in a tissue. We consider the problem of synthesising tissue systems from specifications of observed or desired behaviour given in the form of transition systems. We demonstrate how a Petri net solution to this problem, based on the notion of regions, yields a method for automated synthesis of tissue systems from transition systems. We first assume that the input of the algorithm contains information about the topology of the system to be constructed, and then discuss the case when such a topology is not known in advance and has yet to be determined.

Jetty Kleijn, Maciej Koutny, Marta Pietkiewicz-Koutny

A Coloured Petri Net Approach to the Functional and Performance Analysis of SIP Non-INVITE Transaction

Abstract

With the increasing popularity of Voice over IP, the Session Initiation Protocol (SIP), a protocol for session creation and management, has become more and more important. This paper is focused on SIP non-INVITE transaction (NIT) and analyzes its functional correctness and performance. We firstly propose an extension to a Coloured Petri Net (CPN) based protocol verification methodology with a performance analysis component. Following the extended methodology, CPN models for NIT are created, verified and simulated. Functional verification shows that NIT contains no livelock and dead code, but it is not free of deadlock. Simulation analysis indicates that channel loss has a signifcant impact on bandwidth consumption by NIT, and when channel loss rate is less than 20 %, the delay by the server generating its final response has great influence on NIT performance. The outcome of this research also demonstrates the effectiveness of CPN for both functional and performance analysis of network protocols.

Junxian Liu, Lin Liu

Backmatter

Titel: Transactions on Petri Nets and Other Models of Concurrency IX
Verlag: Springer Berlin Heidelberg
Print ISBN: 978-3-662-45729-0
Electronic ISBN: 978-3-662-45730-6
DOI: https://doi.org/10.1007/978-3-662-45730-6
Herausgeber:: Maciej Koutny
Serge Haddad
Alex Yakovlev

Premium Partner

Bildnachweise