Formal Techniques for Distributed Objects, Components, and Systems: 42nd IFIP WG 6.1 International Conference, FORTE 2022 Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022 Lucca, Italy, June 13–17, 2022 Proceedings

Foreword
Preface
Organization
30+ Years of FORTE Research: A Personal Perspective (Abstract of Invited Talk)
Contents
Monitoring Hyperproperties with Circuits
	1 Introduction
	2 The Logic
	3 The Monitors
		3.1 Runtime Costs
	4 Conclusion and Future Work
	A  Appendix: Cases for the Proof of Violation Completeness
	References
Process Algebra Can Save Lives: Static Analysis of XACML Access Control Policies Using mCRL2
	1 Introduction
	2 Background on the XACML Policy Language
	3 Modeling and Analyzing XACML Policies
		3.1 Mapping XACML Policies into mCRL2
		3.2 Specifying the Properties of XACML Policies
	4 System Behavior in Presence of XACML Policies
	5 Related Work
	6 Conclusion
	References
The Reversible Temporal Process Language
	1 Introduction
	2 Informal Overview of TPL and Reversibility
	3 Reversible Temporal Process Language
	4 Properties
		4.1 Idempatience and Properties of
		4.2 Relations with TPL and Reversible CCS
	5 Reversibility in revTPL
		5.1 Revised Semantics
		5.2 Independence
		5.3 Causal Consistency
	6 Conclusions
	References
Branch-Well-Structured Transition Systems and Extensions
	1 Introduction
	2 Preliminaries
	3 Termination and Boundedness
	4 Decidability of Coverability
	5 Conclusion
	References
Offline and Online Monitoring of Scattered Uncertain Logs Using Uncertain Linear Dynamical Systems
	1 Introduction
	2 Related Works
	3 Preliminaries
	4 Monitoring Using Uncertain Linear Dynamical Systems as Bounding Model
		4.1 Offline Monitoring
		4.2 Online Monitoring
	5 Case Studies
		5.1 First Benchmark: Anesthesia
		5.2 Second Benchmark: Adaptive Cruise Control
		5.3 General Observations
	6 Conclusion
	References
Co-engineering Safety-Security Using Statistical Model Checking
	1 Context and Motivation
	2 AFMTs and Informal Semantics
	3 Conclusion
	References
Fault-Tolerant Multiparty Session Types
	1 Introduction
	2 Fault-Tolerance in Distributed Algorithms
	3 Fault-Tolerant Types and Processes
	4 A Semantics with Failure Patterns
	5 Typing Fault-Tolerant Processes
	6 The Rotating Coordinator Algorithm
	7 Conclusions
	References
Effective Reductions of Mealy Machines
	1 Introduction
	2 Definitions
	3 SAT-Based Minimization of IGMM
		3.1 General Approach
		3.2 Proposed SAT Encoding
		3.3 Adjustment of Prior Optimizations
		3.4 Algorithm
	4 Bisimulation with Output Assignment
		4.1 Reducing Machines with
		4.2 Implementing
	5 Benchmarks
	6 Conclusion
	References
Traits: Correctness-by-Construction for Free
	1 Introduction
	2 Motivating Example
	3 Object-Oriented Trait-Based Language
		3.1 Syntax
		3.2 Typing Rules
		3.3 Flattening Semantics
		3.4 Soundness of the Trait-based CbC Process
	4 Trait-Based Correctness-by-Construction in Comparison to Classical CbC
	5 Proof-of-Concept Implementation
	6 Related Work
	7 Conclusion
	References
Encodability Criteria for Quantum Based Systems
	1 Introduction
	2 Quantum Based Systems
	3 Process Calculi
		3.1 Communicating Quantum Processes
		3.2 An Algebra of Quantum Processes
	4 Encodings and Quality Criteria
	5 Encoding Quantum Based Systems
	6 Separating Quantum Based Systems
	7 Quality Criteria for Quantum Based Systems
	8 Conclusions
	References
LTL Under Reductions with Weaker Conditions Than Stutter Invariance
	1 Introduction
	2 Definitions
		2.1 A ``Shorter than'' Relation for Infinite Words
		2.2 Sensitivity of a Language to the Length of Words
		2.3 Relationship to Stutter Insensitive Logic
		2.4 When Is Visiting Shorter Words Enough?
	3 Application to Verification
		3.1 Kripke Structure
		3.2 Automata Theoretic Verification
		3.3 Detection of Language Sensitivity
		3.4 Agglomeration of Events Produces Shorter Runs
	4 Experimentation
		4.1 A Study of Properties
		4.2 A Study of Performances
	5 Related Work
	6 Conclusion
	References
Computing Race Variants in Message-Passing Concurrent Programming with Selective Receives
	1 Introduction
	2 Message Races and Selective Receives
	3 Execution Traces
	4 Computing Message Races and Race Variants
	5 Discussion and Future Work
	References
Author Index