Application and Theory of Petri Nets and Concurrency. 44th International Conference, PETRI NETS 2023 Lisbon, Portugal, June 25–30, 2023 Proceedings

Preface
Organisation
Challenges in Conformance Checking: Where Process Mining Meets Petri Net Theory (Extended Abstract)
Contents
Invited Papers
From Process-Agnostic to Process-Aware Automation, Mining, and Prediction
	1 Introduction
	2 Process-Agnostic and Process-Aware Automation
	3 Implications on Research
	References
Formal Modelling, Analysis, and Synthesis of Modular Industrial Systems Inspired by Net Condition/Event Systems
	1 Introduction
	2 Some Definitions
	3 Modelling Distributed Systems with NCES
	4 IEC 61499 Based Modular Engineering of Automation Systems
	5 Survey of Works on Modular Engineering and Modelling
		5.1 Modelling of Flexible Reconfigurable Systems
		5.2 Modelling of IEC 61499
	6 Use IEC 61499 for Condition/Event Modelling: A Comprehensive Tool Chain
	7 Summary and Open Problems
	References
Process Mining
There and Back Again
	1 Introduction
	2 Preliminaries
	3 Typed Jackson Nets to Model Interacting Processes
		3.1 Jackson Nets
		3.2 Petri Nets with Identifiers
		3.3 Typed Jackson Nets
	4 Decomposability of t-JNs
	5 A Framework for Rediscoverability
		5.1 Event Logs and Execution Traces
		5.2 Rediscoverability of Typed Jackson Nets
	6 Conclusion
	References
ILP2 Miner – Process Discovery for Partially Ordered Event Logs Using Integer Linear Programming
	Abstract
	1 Introduction
	2 Preliminaries
		2.1 ILP Miner
		2.2 Compact Tokenflow Synthesis
	3 ILP2 Miner
	4 Experimental Results
	5 Conclusion
	References
Modelling Data-Aware Stochastic Processes - Discovery and Conformance Checking*-12pt
	1 Introduction
	2 Related Work
	3 Preliminaries
	4 SLDPN
		4.1 Trace-Based Execution Semantics & XES Logs
	5 Data-Based Stochastic Discovery
		5.1 Extracting Observation Instances
		5.2 Learning Weight Functions
	6 Conformance Checking
		6.1 Conditional Probabilities in SLDPNs
		6.2 Conditional Probabilities in Logs
		6.3 A Conformance Measure
	7 Evaluation
		7.1 Implementation
		7.2 Insights
		7.3 Quantitative
	8 Conclusion
	References
Exact and Approximated Log Alignments for Processes with Inter-case Dependencies
	1 Introduction
	2 Preliminaries
		2.1 Multisets and Posets
		2.2 Petri Nets
		2.3 Event Logs
	3 Modeling, Analysis and Simulation of Case Handling Systems with Inter-case Dependencies
		3.1 Requirements Imposed by Inter-case Dependencies
		3.2 Existing Petri Net Extensions
		3.3 Resource Constrained -Petri Net with Fixed Color Types
	4 Complete Event Logs Alignments
		4.1 Foundations of Alignments
		4.2 Alignments Extended to Include Inter-case Dependencies
	5 Approximation by Composition and Local Realignments
		5.1 Composing Individual Alignments
		5.2 Resolving Violations in the Composed Alignment
		5.3 Obtaining Minimal Local Alignable Intervals
	6 Conclusion
	References
Semantics
Taking Complete Finite Prefixes to High Level, Symbolically
	1 Introduction
	2 High-Level Petri Nets and Symbolic Unfoldings
		2.1 High-Level Petri Nets
		2.2 Symbolic Branching Processes and Unfoldings
		2.3 Properties of the Symbolic Unfolding
	3 Finite and Complete Prefixes of Symbolic Unfoldings
		3.1 Generalizing Adequate Orders and Cut-Off Events
		3.2 The Generalized ERV-Algorithm
		3.3 High-Level Versus P/T Expansion
	4 Handling Infinitely Many Reachable Markings
		4.1 Symbolically Compact High-Level Petri Nets
		4.2 The Finite Prefix Algorithm for Symbolically Compact Nets
		4.3 Checking Cut-offs Symbolically
	5 Conclusions and Outlook
	References
Interval Traces with Mutex Relation
	1 Introduction
	2 Preliminaries
	3 Interval Orders
	4 Sequences and Partial Orders
	5 Mazurkiewicz Traces
	6 Interval Sequences
	7 Interval Traces
	8 Interval Traces with Mutex Relation
	9 Mutex Interval Trace Semantics of Petri Nets
	10 Concluding Remarks
	References
A Myhill-Nerode Theorem for Higher-Dimensional Automata*-12pt
	1 Introduction
	2 Pomsets with Interfaces
	3 HDAs and Their Languages
	4 Myhill-Nerode Theorem
	5 Determinism
	6 Conclusion and Further Work
	References
Tools
Hippo-CPS: A Tool for Verification and Analysis of Petri Net-Based Cyber-Physical Systems
	1 Introduction
	2 Hippo-CPS
		2.1 Architecture
		2.2 Classification of the Petri Net-Based System
		2.3 Reachability Tree Verification (Boundedness, Safeness, Liveness Analysis)
		2.4 Structural Concurrency Verification (Graph-Based Analysis)
		2.5 Concurrency Verification (Concurrency Hypergraph-Based Analysis)
		2.6 Structural Sequential Verification (Graph-Based Analysis)
		2.7 Sequentiality Verification (Sequentiality Hypergraph-Based Analysis)
		2.8 Sequentiality Verification (Linear Algebra Technique)
		2.9 Experimental Results
		2.10 A Case-Study Example
	3 Installation
	4 Comparison with Other Tools
	5 Conclusion
	References
Mochy: A Tool for the Modeling of Concurrent Hybrid Systems
	1 Introduction
	2 Mochy Description
		2.1 Architecture
		2.2 Semantics
		2.3 Simulation
		2.4 Inputs-Outputs
		2.5 User Interface
	3 Case Studies
	4 Related Work
	5 Conclusion and Future Work
	References
RENEW: Modularized Architecture and New Features
	1 Introduction
	2 Formalisms
		2.1 Reference Nets
		2.2 P/T-Nets with Synchronous Channels
	3 Objectives
		3.1 Developments after Renew 2.5
		3.2 Users
	4 Functionality
		4.1 Usability
		4.2 New Functionality
		4.3 Improvements
	5 Architecture
	6 Use Cases
		6.1 Mulan
		6.2 Settler
	7 Conclusion
	References
Explorative Process Discovery Using Activity Projections
	1 Introduction
	2 Preliminaries
	3 Approach
	4 Implementation
		4.1 Full Version Discovering Pareto Optimal Models
		4.2 Lite Version for Guided Exploration
	5 Evaluation
		5.1 General Functions
		5.2 Scalability
	6 Conclusion
	References
Verification
Computing Under-approximations of Multivalued Decision Diagrams*-12pt
	1 Introduction
	2 Preliminaries
	3 Our under-approximation Algorithm
		3.1 Incoming-edge-count
		3.2 Above-state-count
		3.3 Below-state-count
		3.4 Highest-unique-below-set
		3.5 Lowest-unique-above-set
		3.6 Dominator and Post-dominator
		3.7 Under-approximation (one Node at a Time)
	4 Speeding up the under-approximation
	5 Application
	6 Results
		6.1 Experimental Results
	7 Conclusions and Future Work
	References
Stochastic Decision Petri Nets*-12pt
	1 Introduction
	2 Preliminaries
	3 Stochastic Decision Petri Nets
	4 Stochastic Decision Petri Nets as Markov Decision Processes
	5 Complexity Analysis for Specific Classes of Petri Nets
		5.1 Complexity of Safe and Acyclic Free-Choice Decision Nets
		5.2 Complexity of Free-Choice Occurrence Decision Nets
	6 An Algorithm for SAFC Decision Nets
	7 Conclusion
	References
Token Trail Semantics – Modeling Behavior of Petri Nets with Labeled Petri Nets
	Abstract
	1 Introduction
	2 Preliminaries
	3 Token Trails
	4 Token Trails for Transition Systems and Partial Languages
	5 Token Trails for Labeled Petri Nets
	6 Conclusion
	References
On the Reversibility of Circular Conservative Petri Nets
	1 Introduction
	2 Invariant Weighted Circular Petri Nets
	3 Some Easy Algorithms
	4 Some Necessary and Sufficient Conditions
	5 Potential Reachability Checks
		5.1 The Limit Case
		5.2 The Non-limit Case
	6 Largest Dead Number of Tokens
	7 Conclusions and Perspectives
	References
Automated Polyhedral Abstraction Proving
	1 Introduction
	2 Petri Nets and Polyhedral Abstraction
	3 Parametric Reduction Rules and Equivalence
	4 Automated Proof Procedure
		4.1 Presburger Encoding of Petri Net Semantics
		4.2 Core Requirements: Parametric E-abstraction Encoding
		4.3 Global Procedure
	5 Silent Transition Relation Acceleration
	6 Generalizing Equivalence Rules
	7 Validation and Conclusion
	References
Experimenting with Stubborn Sets on Petri Nets
	1 Introduction
	2 Background
	3 Stubborn Sets for Deadlock State Detection
		3.1 Stubborn Set Theory for Deadlock Detection
		3.2 Stubborn Set Algorithms for Deadlock Detection
		3.3 Experimentation Context
		3.4 Experimental Observations
		3.5 Experimental Results Sample
	4 Stubborn Sets for Liveness Verification
		4.1 Stubborn Set Theory for Liveness Verification
		4.2 Stubborn Set Algorithms for Liveness Verification
		4.3 Experimentation Context
		4.4 Experimental Observations
		4.5 Experimental Results Sample
	5 Conclusion
	References
Timed Models
Symbolic Analysis and Parameter Synthesis for Time Petri Nets Using Maude and SMT Solving
	1 Introduction
	2 Preliminaries
	3 A Rewriting Logic Semantics for ITPNs
		3.1 Formalizing ITPNs in Maude: The Theory R0
		3.2 Some Variations of R0
		3.3 Explicit-state Analysis of ITPNs in Maude
	4 Parameters and Symbolic Executions
		4.1 The Symbolic Rewriting Logic Semantics
		4.2 A New Folding Method for Symbolic Reachability
	5 Parameter Synthesis and Symbolic Model Checking
		5.1 Parameter Synthesis
		5.2 Analyzing Temporal Properties
	6 Benchmarking
	7 Related Work
	8 Concluding Remarks
	References
A State Class Based Controller Synthesis Approach for Time Petri Nets
	1 Introduction
	2 Definitions
		2.1 Preliminaries
		2.2 Time Petri Nets
		2.3 State Classes
		2.4 Two-player Game on the State Class Graph
	3 Computing the Winning States
		3.1 Symbolic Computation for Pred()
		3.2 Predecessor Computations with DBMs
		3.3 Winning States
	4 Case Studies
		4.1 Supply Chain
		4.2 AGV
	5 Conclusion
	References
Model Transformation
Transforming Dynamic Condition Response Graphs to Safe Petri Nets
	1 Introduction
	2 Related Work
	3 Preliminaries
		3.1 Running Example
		3.2 Dynamic Condition Response Graphs
		3.3 Petri Nets with Inhibitor Arcs, Read Arcs and Pending Places
	4 Mapping DCR Graphs to Petri Nets
	5 Pruning and Reachability Analysis
		5.1 Pruning Based on the DCR Graph
		5.2 Petri Net Reachability Analysis
		5.3 Space Analysis on the Running Example
	6 Conclusion and Future Work
	References
Enriching Heraklit Modules by Agent Interaction Diagrams
	1 Introduction
	2 Paose Background
		2.1 Multi-agent System Modeling Paradigm
		2.2 The Mulan Framework
		2.3 Agent Interaction Diagrams/Protocols
	3 HERAKLIT Background
		3.1 HERAKLIT Module
		3.2 Composition
	4 Modularized Modeling Examples
		4.1 Modeling of Organizational Units
		4.2 Software Engineering: Producer/Storage/Consumer Example
		4.3 Renew\'s Plugins
	5 Heraklit Interaction Diagrams
		5.1 Extending Net Modules with Reference Nets
		5.2 Generating HERAKLIT Modules
	6 Modeling HERAKLIT Modules with Mulan Concepts
	7 Conclusion
	References
Author Index