Rewriting Logic and Its Applications: 14th International Workshop, WRLA 2022, Munich, Germany, April 2–3, 2022, Revised Selected Papers (Lecture Notes in Computer Science, 13252)

Preface
Organization
Contents
Invited Papers
From Static to Dynamic Analysis and Allocation of Resources for BPMN Processes
	1 Introduction
	2 BPMN with Time and Resources
	3 Static Quantitative Analysis
		3.1 Process Description
		3.2 Execution Semantics
		3.3 Properties
		3.4 Example
	4 Dynamic Quantitative Analysis
		4.1 Instrumentation
		4.2 Computation of Properties
		4.3 Dynamic Resource Allocation
		4.4 Example
	5 Related Work
	6 Concluding Remarks
	References
Rewriting Privacy
	1 Introduction
	2 Alpha-Beta Privacy for a Fixed State
		2.1 The State Space
		2.2 Example
		2.3 Message Analysis Problems
	3 Applications in Vote Privacy
		3.1 Receipt Freeness
		3.2 Stability Under Background Knowledge
	4 Privacy as Reachability
		4.1 Example: AF2
		4.2 Semantics
	5 Conclusions and Outlook
	References
Invited Tutorials and Experience Report
Canonical Narrowing with Irreducibility and SMT Constraints as a Generic Symbolic Protocol Analysis Method
	1 Introduction
	2 Preliminaries
	3 Canonical Narrowing with Irreducibility and SMT Constraints
	4 Implementation
		4.1 Our Previous Narrowing Command
		4.2 Using Conditional Rules in Narrowing
		4.3 Extension to Handle SMT Constraints
		4.4 Variable Consistency
	5 Experiments
		5.1 Handling SMT Constraints
		5.2 Brands and Chaum with Time
		5.3 Brands and Chaum with Time and Space
	6 Conclusions and Future Work
	References
An Overview of the Maude Strategy Language and its Applications
	1 Introduction
	2 A Brief Introduction to the Maude Strategy Language
	3 Some Examples
		3.1 Deduction Procedures
		3.2 Semantics of Programming Languages
		3.3 Games
		3.4 Other Examples
	4 Related Tools and Extensions
		4.1 Model Checking
		4.2 Reflective Manipulation of Strategies
		4.3 A Probabilistic Extension
	5 Conclusions
	References
Teaching Formal Methods to Undergraduate Students Using Maude
	1 Introduction
	2 Setting and Challenges
	3 How to Teach Formal Methods?
		3.1 A Few Papers on Teaching Formal Methods.
		3.2 What to Teach?
	4 Why Teaching Formal Methods Using Maude?
	5 Course and Textbook Content
		5.1 Part I: Equational Specification in Maude and Term Rewrite Theory
		5.2 Equational Logic (1 lecture)
		5.3 Part II: Modeling and Analysis of Dynamic/Distributed Systems Using Rewriting Logic
	6 Evaluation
		6.1 Summary of Student Feedback
		6.2 Selected Student Comments
	7 Concluding Remarks
	References
Regular Papers
Business Processes Analysis with Resource-Aware Machine Learning Scheduling in Rewriting Logic
	1 Introduction
	2 The Business Process Modeling Notation (BPMN)
	3 Using Long Short-Term Memory Neural Networks
	4 Rewriting Logic Semantics with LSTM Integration
		4.1 The Specification of BPMN Processes
		4.2 Autonomous Processes
		4.3 Event-Guided Processes
		4.4 Resource Adaptation Based on LSTM Predictions
	5 Case Study
	6 Concluding Remarks
	References
Modeling, Algorithm Synthesis, and Instrumentation for Co-simulation in Maude
	1 Introduction
	2 Preliminaries
		2.1 Rewriting Logic and Maude
		2.2 Co-simulation
	3 Modeling Co-simulation Scenarios in Maude
	4 Synthesizing and Executing Co-simulation Algorithms
		4.1 Orchestration Data
		4.2 Synthesis of Co-simulation Algorithms
		4.3 Executing Co-Simulation Algorithms
		4.4 Checking Confluence of Synthesized Co-simulation Algorithms
	5 Synthesizing Instrumentations and SU Parameters
		5.1 Instrumentation of a Scenario
		5.2 Synthesizing SU Parameters
	6 Related Work
	7 Concluding Remarks
	References
An Efficient Canonical Narrowing Implementation for Protocol Analysis
	1 Introduction
	2 Preliminaries
	3 Canonical Narrowing
	4 Implementation
		4.1 Using the Meta-level
		4.2 Data Structures and the narrowing Command
		4.3 Search for Solutions
		4.4 Avoiding Variable Clashes
		4.5 Algorithm Performance Improvement
	5 Experiments
		5.1 Experiments with the Vending Machine
		5.2 Experiments with a Protocol Using the Exclusive-Or Property
		5.3 Experiments Using the Properties of an Abelian Group
		5.4 Experiments with the Vending Machine Using Idempotence
	6 Conclusions
	References
Checking Sufficient Completeness by Inductive Theorem Proving
	1 Introduction
	2 Preliminaries
	3 A Hierarchical Methodology
	4 Proving Sufficient Completeness Inductively
	5 Some Examples
	6 Related Work and Conclusions
	A  Multiset Theory
	B  Proofs
	References
On Ground Convergence and Completeness of Conditional Equational Program Hierarchies
	1 Introduction
	2 Preliminaries
	3 Proving Ground Convergence And Sufficient Completeness Hierarchically
	4 Related Work and Conclusions
	A  Proofs
	References
Automating Safety Proofs About Cyber-Physical Systems Using Rewriting Modulo SMT
	1 Introduction
	2 Motivating Example
	3 Symbolic Soft Agents Framework
		3.1 Overview
		3.2 The Structure of Soft Agent Rewriting
		3.3 Symbolic Soft Agent Rewriting
	4 Vehicle Specifications
		4.1 Basic Symbolic Sorts
		4.2 Knowledge Specifications
		4.3 Soft-Constraint Controller
		4.4 System Configurations
		4.5 Safety Properties
		4.6 Verifying Logical Scenarios
	5 Trade-Offs Between Rewriting and Constraint Solving
	6 Related Work
	7 Conclusions
	References
Executable Semantics and Type Checking for Session-Based Concurrency in Maude
	1 Introduction
	2 The Typed Process Model
	3 Rewriting Semantics for s
	4 Algorithmic Type Checking for s
		4.1 Type Syntax
		4.2 Algorithmic Type Checking
		4.3 Type Soundness
	5 Lock and Deadlock Detection in Maude
		5.1 Definitions
		5.2 Examples
	6 Closing Remarks
	References
Tool Papers
Parallel Maude-NPA for Cryptographic Protocol Analysis
	1 Introduction
	2 Preliminaries
	3 Maude-NPA
	4 Parallel Maude-NPA and Its Tool Support
	5 Experiments
	6 Related Work
	7 Conclusion
	A The Number of States Located at Each Layer
	References
Maude as a Library: An Efficient All-Purpose Programming Interface
	1 Introduction
	2 Overview of the Library
	3 How to Use the Library, Illustrated by an Example
	4 Advanced Features
		4.1 Rewrite Graphs and Model Checking
		4.2 Custom Special Operators
	5 Implementation
		5.1 Performance Considerations
	6 Some Applications
		6.1 Integration of Maude into the Robot Operating System
		6.2 The Unified Maude Model Checker
	7 Related Work
	8 Conclusions
	References
Author Index