This book constitutes the proceedings of the 46th International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2025, held in Paris, France, during June 22-27, 2025.
The 21 full papers and 1 short paper included in this book were carefully reviewed and selected from 48 submissions. They deal with topics such as composition and synthesis; workflow nets; process mining; model checking; communication & concurrency; timed and stochastic Petri nets; etc. The proceedings also include one invited talk in full paper length.
.- Automated Reasoning for Data-Aware Petri Nets.
.- Petri Nets and Higher-Dimensional Automata.
.- Discovering the Influence of Exogenous Data on Decisions in Processes.
.- Synthesizing Petri Nets from Labelled Petri Nets.
.- Coverability in Well-Formed Free-Choice Nets.
.- High-Level Message Sequence Charts: Satisfiability and Realizability
Revisited.
.- Distributed Reference Net Simulation based on Event Streaming.
.- Persistent Permutations, Fairness, Asymmetric Choice Petri Nets, and
Ochmanski’s Conjecture.
.- Statistical Model Checking of Stochastic Timed-Arc Petri Nets.
.- Energy Transfer in timed cyclic networks.
.- Leveraging Petri Nets for Workflow Anomaly Detection in Microservice
Architectures.
.- Translating Workflow Nets into the Partially Ordered Workflow Language.
.- Distributed Places and Safe Net Reduction.
.- Analysing Probabilistic Hornets.
.- Enjoy the Silence, Part II: Probability-Based Queries on Stochastic
Labelled Petri Nets.
.- Decidability problems for weak Time Petri Nets with read, reset and
transfer arcs.
.- SkiNet: a User-Oriented Tool for Petri Net-based Analysis of Robotic Skills.
.- Deciding (Sub-Marking) Reachability in O(Pˆ2 + Tˆ2) for Sound
Acyclic Free-Choice Workflow Nets.
.- Complexity of Alignments on Sound Free-Choice Workflow Nets.
.- Computing Alignments for Partially-ordered Traces Through Petri Net
Unfoldings .
.- Simplifying LTL Model Checking Given Prior Knowledge.
.- Failure Resilience of strongly synchronized Processes.
.- Symbolic Model Checking in the Modular State Space using Binary
Decision Diagrams.
