Systems grow in complexity, inflating model size and structural density. Place/Transition (P/T) nets are a standard formalism, but large instances strain editing, simulation, and verification. A modular perspective treats distributed P/T nets as composable units with a module interface. The research question is how to define and operationalize a concept of interface-guided modularity via Decomposition and Composition so that large P/T net models become more tractable while preserving interface compatibility. Decomposition and composition are defined over interfaces via distributed synchronous channels and realized as a proof of concept (PoC) in Renew using constructivist prototyping. Decomposition applies Karger’s randomized contraction algorithm to an undirected graph derived from the net, yielding a cut that induces subnet boundaries and interfaces. The PoC selects the minimum cut to minimize cross-partition coupling and distributed communication. Composition reconciles interfaces by aligning and merging required interface elements. Runtime is analyzed with respect to the interface-based definitions, and benchmarks are evaluated by wall-clock time, the throughput, and the runtime-to-net-size ratio. Asymptotic bounds are derived for both operations. NetSplit scales as 𝒪(n^2+n· t) , where n is the number of nodes and t the number of transitions. NetJoin is bounded by 𝒪( ∑ _i=1^n m_i· l) , where m_i is the number of net elements in the i -th net and l the number of distributed synchronous channels to be reconciled during composition. Interface-guided modularization improves operational efficiency for complex Petri net models, makes larger nets more tractable, and supports dynamic repartitioning in distributed simulation and verification.

Developing complex systems relies heavily on using models to analyze components and validate system behavior. Simulation and verification are essential for advancing those systems. Petri nets, a widely used modeling technique, excel in representing such systems. However, they face scalability and performance limitations when single computing platforms confine the simulations. This paper proposes a novel approach for the distributed simulation of Reference Nets, overcoming the constraints of single computing platforms. The proposed solution employs distributed synchronization via synchronous channels and integrates event streaming within computing clusters. A prototyping methodology grounded in constructivist principles validates the approach. The primary contribution is a distributed simulator for Reference Nets as an extension of RENEW. The simulator leverages KAFKAREGISTRY to facilitate event-driven, loosely coupled communication. This architecture enhances scalability and robustness, tackling computational challenges in modern distributed systems. The proposed solution overcomes bottlenecks of single-platform simulations. It provides a scalable simulator for Reference Nets in distributed environments, enabling efficient and high-performance system simulation.

Cycloids are particular Petri nets for modelling processes of actions and events, belonging to the fundaments of Petri's general systems theory. Defined by four parameters they provide an algebraic formalism to describe strongly synchronized sequential processes. To further investigate their structure, reduction systems of cycloids are defined in the style of rewriting systems and properties of irreducible cycloids are proved. In particular the synthesis of cycloid parameters from their Petri net structure is derived, leading to an efficient method for a decision procedure for cycloid isomorphism.

Building complex systems requires a systematic approach. One challenge of this is modeling behavior. To support this a kind of UML sequence diagram (AUML) is used in multi-agent systems. In Petri net-based, Agent- and Organization-Oriented Software Engineering (Paose), Petri nets are used to provide a formal semantics for an adapted version of AUML called Agent interaction protocol diagrams (Aips). Also using Petri nets, Fettke and Reisig address system composition based on Reisig's associative composition calculus for their HERAKLIT approach. By combining their results with Paose, systems can be built systematically based on Aips. They model web service interactions as reactions of a complex trigger of a system. Based on the Petri net semantics, they are aggregated within roles, which are then assigned to web services. With this rigorous approach, we can provide a "proof by construction" approach to model web service composition spanning distributed web services, limited to their control flow. The advantages and limitations of this type of modeling are discussed in detail.

The modeling of systems in informatics has always been a challenge and the difficulty increases with the system's scale and complexity. Since there is no direct way to turn complex systems into executable code, various modeling techniques are used to cover different perspectives of a system with models. These models must then be turned into code correctly and consistently. But how to create, structure, and compose the various models throughout the development process? As a formal basis, Reisig proposes net modules, which inherit an associative calculus for composition. Practical modeling is addressed by the work of Fettke and Reisig with the HERAKLIT approach, which adopts especially the net modules as a basis. Based on this, we combined the HERAKLIT approach with our Paose approach and its multi-agent system elements. As our main result we present HERAKLIT Interaction Diagrams which we obtain by enriching HERAKLIT modules by Agent Interaction Diagrams. We connect the concepts of reference nets and agents to HERAKLIT modules, and thereby construct Heraklit Agents.

Renew is an extensible Petri Net IDE that supports the development and execution of high-level Petri Nets and other modeling techniques. Over the past seven years, Renew has undergone significant development and refinement. To this end, Renew's code base has been reworked extensively, and its tool collection has been expanded. The reworking was necessary due to technical debt caused by environmental changes: especially Java's transition from version 9 to 17. Adapting to the latest Java versions enables the modularization of Renew's architecture through the Java Platform Module System (JPMS) which was introduced with Java 9. Additionally, some new features have been implemented, which were used to test our new architectural design. One of our main results gave Renew a cleaner code interface design and a more modern architecture. Examples of the extensions and improvements made are the new P/T-nets with synchronous channels (PTC) formalism and the Modular Model Checker (MoMoC). In addition to the aforementioned changes, the GUI has also been altered and now offers an all-in-one window.

Tools must be continuously developed further. For the Java reference nets tool Renew, the latest results of an extensive transformation process are presented. Starting from our good plugin architecture, we were able to convert the Java plugins into Java modules. Most of the architectural hindrances arose from the programming language itself. Java 9 introduced the Java Platform Module System (JPMS), and the Long-Term Support versions of Java 11 and 17 now provide modules and layers as central concepts to support better architectures. Their application is discussed using the transformation from Renew 2.5 to Renew 4.0, which applies the module concept to a medium-sized software toolset. Experiences from this extensive process are highlighted.

Synchronous channels are a powerful means to structure Petri net models. They enable large, expressive models while maintaining a coherent and well-readable structure. However, the vast number of potential bindings make Petri Nets extended with synchronous channels notoriously difficult to verify. This paper introduces synchronous channels to the basic P/T-net formalism while finding a compromise between the goals of increasing the modeling capabilities and remaining easy to verify. As part of this paper, a formal definition and an implementation of P/T-nets with synchronous channels are provided. With the provided definition, the semantics and behavior of these models are formally described and well-defined. This forms a foundation for further work based on the formalism, such as verification or formalism extensions. Additionally, transformations are provided to construct equivalent regular P/T-nets, allowing the application of traditional P/T-net techniques. Restrictions on the synchronous channels ensure that these unfolded P/T-nets retain a reasonable size. The implementation furthermore includes a mechanism to partition nets into sub-nets, providing another means to create complex, yet comprehensive models. As a result, the formalism performs a balancing act by providing multiple means to structure large models while keeping the formalism simple enough to be feasible for verification methods developed for P/T-nets.