دانلود کتاب 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