Formal Modeling and Analysis of Timed Systems: 21st International Conference, FORMATS 2023, Antwerp, Belgium, September 19–21, 2023, Proceedings (Lecture Notes in Computer Science)

Preface
Organization
Encoding Planning and Games in SAT and QBF (Invited Talk)
Contents
Invited Talk
Computing the Price of Anarchy in Atomic Network Congestion Games (Invited Talk)
	1 Atomic Network Congestion Games
	2 Computing the Prices of Anarchy and Stability
		2.1 Series-Parallel Networks with Linear Latency Functions
		2.2 Dynamic Network Congestion Games
	3 Timed Network Games
	References
FORMATS 2023 Main Track
CausalReversibilityforTimedProcessCalculi with Lazy/Eager Durationless Actions and Time Additivity
	1 Introduction
	2 Reversible Timed Process Calculus: Actions Vs Delays
	3 Causal Reversibility of RTPC
	4 Conclusions
	References
Automata with Timers
	1 Introduction
	2 Preliminaries
		2.1 Timed Semantics
		2.2 Blocks and Races
	3 Reachability
	4 Race-Avoiding ATs
		4.1 Wiggling a Run
		4.2 Existence of an Unwigglable Run
		4.3 Sufficient Hypotheses
	5 Conclusion and Future Work
	References
Layered Controller Synthesis for Dynamic Multi-agent Systems
	1 Introduction
	2 Running Example: Centralized Traffic Control
		2.1 Multi-agent Traffic
		2.2 Collision Avoidance Problem
		2.3 Running Example
	3 Related Work
	4 High Level Planning
		4.1 Timed Automata, Stopwatches and Channels
		4.2 Timed Automata Representation of Our Running Example
		4.3 Computing the Optimal Strategy for Reachability
	5 Ensuring Feasibility of High-Level Plans
	6 Reinforcement Learning to Get Real-Time Policies
	7 Conclusion and Future Work
	A Markov Decision Process for the Running Example
	B Hyperparameters of the RL Algorithms
	References
On the Susceptibility of QDI Circuits to Transient Faults
	1 Introduction
	2 Related Work
	3 Model
		3.1 Example
	4 Results
		4.1 Well-Defined Executions
		4.2 A Transient-Fault Insertion Tool
		4.3 Equivalence of Transient Faults
		4.4 Automated Computation of Susceptible Regions
		4.5 Comparison of Fault-Tolerance Depending on Speed
	5 Conclusion
	References
Maximum Satisfiability of Mission-Time Linear Temporal Logic
	1 Introduction
	2 Preliminaries
	3 The Slow (recursive) Translation to Boolean Logic
	4 The Fast (iterative) Translation to Boolean Logic
		4.1 Algorithm Overview
		4.2 The Main Algorithm
	5 Benchmarks
	6 Preliminary Results of MLTL MaxSAT
	7 Conclusion and Future Work
	A Proof to Lemma 1
	References
A Local-Time Semantics for Negotiations
	1 Introduction
	2 Local-Timed Negotiations
		2.1 Some Examples
	3 Synchronization-Free Negotiations
	4 Always-Synchronizing Negotiations
	5 Reachability Is Undecidable for Local-Timed Negotiations
	6 Conclusion
	References
Timed Non-interference Under Partial Observability and Bounded Memory
	1 Introduction
	2 Definitions
		2.1 Timed Automata
		2.2 Timed Language
		2.3 Security Timed Automata
	3 State-Based Non-interference Properties
		3.1 Already Existing State-Based Non-interference Properties
		3.2 A More Realistic Property
	4 A Decidable Sub-problem
		4.1 First Approach to 2-POS-NNI
		4.2 Finite Duration Observation Automata (FDO Automata)
		4.3 Deciding K-POS-NNI for FDO Automata
	5 Discussion and Future Work
	References
Special Track on Monitoring of Cyber-Physical Systems
Usage-and Risk-Aware Falsification Testing for Cyber-Physical Systems
	1 Introduction
	2 Methodology
	3 Stochastic Hybrid Systems and Formal Specifications
	4 Falsification Testing with Randomized Accelerator
	5 Estimating Expected Severity
	6 Case Study
	7 Experiments
	8 Conclusion and Future Work
	References
Model Predictive Runtime Verification for Cyber-Physical Systems with Real-Time Deadlines
	1 Introduction
	2 Preliminaries
		2.1 Mission-Time Linear Temporal Logic (MLTL) ch10LVR19,ch10RRS14
		2.2 Abstract Syntax Tree
	3 Model Predictive Runtime Verification (MPRV)
		3.1 MPRV Algorithm
		3.2 MPRV Implementation Using R2U2
		3.3 Memory and Time Analysis of R2U2 Implementation
	4 Quadcopter Case Study
	5 Analysis of Hardware Implementation
		5.1 FPGA Implementation of Model Predictive Runtime Verification (MPRV)
	6 Conclusion and Future Work
	References
Author Index