Application and Theory of Petri Nets and Concurrency: 43rd International Conference, PETRI NETS 2022, Bergen, Norway, June 19–24, 2022, Proceedings (Lecture Notes in Computer Science, 13288)

This book constitutes the proceedings of the 43rd International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2022, which was held virtually in June 2021. The 19 full papers presented in this volume were carefully reviewed and selected from 35 submissions. The papers are categorized into the following topical sub-headings: application of concurrency to system design; timed models; tools; applications; synthesis; petri nets architecture; and process mining. Preface Organization Invited Talks Assumptions in Computer Science: Mere Mathematical Hypotheses, or Representations of the Physical World? Petri Nets and Mazurkiewicz Traces Partnership When Honeymoon is Forgotten VerCors and Alpinist: Correctness of GPU Applications Throughout the Development Cycle Contents Application of Concurrency to System Design Towards the Application of Coloured Petri Nets for Design and Validation of Power Electronics Converter Systems 1 Introduction 2 Modelling Approach and Overview of the CPN Model 3 Buck Converter CPN Modelling 3.1 CPN Modelling of Inductor Current (IL) 3.2 CPN Modelling of Output Voltage (Vo) 4 Controller CPN Modelling 4.1 CPN Modelling of the XADC Conditioning 4.2 CPN Modelling of the Control Logic 5 Simulink Model of the Buck Converter 6 Model Validation and Experimental Results 6.1 Open-Loop Response Evaluation 6.2 CPN Tools and Physical Response Evaluation 7 Conclusions and Future Work References Discovering Unseen Behaviour from Event Logs 1 Introduction 2 Preliminaries 2.1 Partial Orders and Lattices 2.2 Distributive Lattices and Concurrency 2.3 Traces and Event Logs 3 Distributive Lattices of an Event Log 3.1 Reconstruction of Distributive Lattice 3.2 Containing the Amount of Behaviour Discovered During Completion 3.3 Experiments 4 Discussion and Future Work 5 Related Work 6 Conclusion References Layered Memory Automata: Recognizers for Quasi-Regular Languages with Unbounded Memory 1 Introduction 2 Layered Memory Automata 3 Regular Constructions and Closure Properties 4 A Classification of LaMA (Related Work) 5 A Quantitative Point of View on Regular Constructions 6 Conclusion A Examples of Regular Constructions (Complement to Sect.3) References Timed Models Waiting Nets 1 Introduction 2 Preliminaries 3 Waiting Nets 4 Reachability 5 Expressiveness 6 Conclusion References Computing Transience Bounds of Emergency Call Centers: A Hierarchical Timed Petri Net Approach 1 Introduction 2 Petri Net Model of a Medical Emergency Call Center 3 The Equivalence Between Semi-Markov Decision Processes and Continuous Time Petri Nets 3.1 The SMDP Model 3.2 Properties of the Dynamics Governing the Value Function 4 Deviation of the Value from the Congestion-Free Regime 4.1 Reducing to a Stochastic Shortest Path Problem 4.2 Transience Time Needed to Catch-Up the Input 5 Finite Time Convergence of the Semi-Markov SSP-value 5.1 The Different Convergence Phases 5.2 Hierarchical SSP Configurations References Tools Kong: A Tool to Squash Concurrent Places 1 Introduction 2 Commands, Basic Usage and Installation 3 Architecture of Kong 4 Concrete Example 5 Performance 6 Future Work References IOPT-Tools – From Executable Models to Automatic Code Generation for Embedded Controllers Development 1 Introduction 2 Motivation and Objectives 3 Preliminaries 4 IOPT-Tools Architecture and Availability 5 IOPT-Tools Functionality 5.1 Editing Models 5.2 Automatic Generation of Execution Code 5.3 Simulation and Testing 5.4 Create, Export, and Import Models 5.5 Property Verification 5.6 Miscellaneous 6 Conclusions and Future Works References OC: Object-Centric Process Insights 1 Introduction 2 Object-Centric Process Mining 3 Algorithmic Concept 3.1 Filtering 3.2 Process Execution Extraction 3.3 Variant Visualization 4 Usage and Functionalities 4.1 Event Log Management 4.2 Log Settings 4.3 Process Model Explorer 4.4 Variant Explorer 4.5 Implementation 5 Conclusion References Applications From Graphs to the Science Computer of a Space Telescope 1 Introduction 2 Background 2.1 Analytical and Mathematical Models 2.2 Dynamic and Functional Models 2.3 Hybrid Models 2.4 State-of-the-Art Modeling Approaches 3 The Proba-3 Mission, ASPIICS Coronagraph and Instrument Control Unit 3.1 Classic Approach to Performance Modeling 3.2 Tile-Flow Peculiarities that Need to Be Taken into Account 4 Processing Performance Modeling 4.1 Initial Processing Performance Model 4.2 Simulation of the Initial Processing Performance Model 5 Implementation 6 Correlating the Petri Net Performance Model with the Physical Model 7 Gained Insights and Conclusions References Petri Nets Semantics of Reaction Rules (RR) 1 Introduction 2 Preliminary Definitions 2.1 Boolean and Ternary Truth Valuations 2.2 Multisets 2.3 Labelled Transition Systems 2.4 Regular Petri Nets 3 Reaction Rules (RR) 3.1 Definition and Syntax 3.2 Operational Semantics 3.3 Normal and Elementary RR Systems 4 Priority Petri Nets 5 Extended Petri Nets 6 Conclusion 6.1 Related Works 6.2 Future Works References Modelling the Next Generation ALICE Grid Middleware Using Coloured Petri Nets 1 Introduction 2 Modelling JAliEn Using CPNs 2.1 User 2.2 JBox 2.3 Central Services 2.4 VOBox 2.5 Batch Queue 2.6 Worker Node 3 Simulation 3.1 State Space Insights 4 Conclusion References Synthesis Synthesis of Inhibitor-Reset Petri Nets: Algorithmic and Complexity Issues 1 Introduction 2 Preliminaries 3 Synthesis 4 Complexity 4.1 Membership in NP 4.2 Polynomial Cases 4.3 General Approach of the NP-completeness Proofs 4.4 The Synthesis Complexity of Several Plain Subclasses of SIRPN 4.5 The Synthesis Complexity of Impure SRPN and SIRPN 5 Conclusion References The Synthesis Problem for Repeatedly Communicating Petri Games 1 Introduction 2 Foundations 2.1 Graph Games 3 Reduction of Petri Games to Graph Games 3.1 Extended Petri Game Semantics 3.2 Corresponding Graph Game 3.3 From Graph Games to Petri Games and Vice Versa 4 Related Work 5 Conclusions References Petri Nets Architecture Avoiding Exponential Explosion in Petri Net Models of Control Flows 1 Introduction 2 Basic Notions 3 Equivalence Between the Problems of Modelling a Choice Between Bursts in a PN and Finding an ECC of a Complete Multipartite Graph 4 A Logarithmic Case 5 Upper Bounds for the Balanced Case 6 Upper Bounds for the Almost Balanced Case 7 Upper Bounds for the Unbalanced Case 8 A Polynomial Bisimulation-Preserving Translation from BAs to PNs 9 Conclusions References The Ins and Outs of Petri Net Composition 1 Introduction 1.1 A Few Examples of Net Composition 2 Previous Work on Composition 2.1 Net Algebras and Composition Frameworks 2.2 Composition in Tools 3 Definitions 4 A Framework for Net Composition 5 Composition Policies 5.1 Unary Conjugated Composition 5.2 N-Ary Structured Composition 6 Modelling Using the Composition Framework 6.1 Place-Based Composition 6.2 Transition-Based Composition 7 Conclusions References Process Mining Discovering Process Models with Long-Term Dependencies While Providing Guarantees and Handling Infrequent Behavior 1 Introduction and Related Work 2 Basic Notations, Event Logs, and Process Models 3 Introducing the eST-Miner 4 Place Selection 4.1 Place Classification 4.2 Selection Framework 5 Selection Strategies 6 Experimental Results and Evaluation 6.1 Experimental Setup 6.2 Results and Evaluation 7 Conclusion References Aligning Event Logs to Resource-Constrained -Petri Nets 1 Introduction 2 Preliminaries 2.1 Petri Nets 2.2 Event Logs 3 Modeling Resource-Constrained Case Handling Systems 3.1 Resource-Constrained Petri Nets 3.2 Running Example 3.3 nu-Petri Nets 3.4 Modeling Patterns 4 Alignments on Resource-Constrained Petri Nets 4.1 Traditional Case-by-Case Alignments 4.2 Unexposed Deviations; the Need for Multi-case and -resource Alignments 5 Computing Multi-case and -resource Alignments 5.1 Approach 5.2 Multi-case and -resource Alignments in Action 5.3 Relaxing the Synchronous Product Petri Net to Detect Resource-Related Deviations 6 Conclusion References From Place Nets to Local Process Models 1 Introduction 2 Related Work 3 Preliminaries 4 Approach 4.1 Place Net Adaptation and Filtering (PAF) 4.2 Building Local Process Models (B-LPMs) 4.3 Local Process Models Evaluation and Ranking (LPMs-ER) 5 Evaluation and Results 5.1 Quality Definition and Challenges 5.2 Discoverability of Constructs 5.3 Running Time vs Parameters 5.4 Comparison to Other Approaches 6 Conclusion and Outlook References Data and Process Resonance 1 Introduction 2 Preliminaries 3 Typed Petri Nets with Identifiers 4 Correctness Criteria for t-PNIDs 4.1 Correctness Criteria on System-Level 4.2 Correctness Criteria on Object-Level 5 Correctness by Construction 5.1 EC-Closed Workflow Nets 5.2 Typed Jackson Nets 5.3 Workflow Refinement 6 Related Work 7 Conclusions References Author Index