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)

This book constitutes selected papers from the refereed proceedings of the 14th International Workshop on Rewriting Logic and Its Applications, WRLA 2022, held in Munich, Germany, in April 2022. The 9 full papers included in this book were carefully reviewed and selected from 13 submissions. They focus on topics in rewriting logic and its applications. The book also contains 2 invited papers, 2 invited tutorials and an experience report. 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