Formal Modeling and Analysis of Timed Systems: 20th International Conference, FORMATS 2022, Warsaw, Poland, September 13–15, 2022, Proceedings (Lecture Notes in Computer Science)

This book constitutes the refereed proceedings of the 20th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2022, held in Warsaw, Poland, in September 2022. The 12 full papers together with 2 short papers that were carefully reviewed and selected from 30 submissions are presented in this volume with 3 full-length papers associated with invited/anniversary talks. The papers focus on topics such as modelling, design and analysis of timed computational systems. The conference aims in real-time issues in hardware design, performance analysis, real-time software, scheduling, semantics and verification of real-timed, hybrid and probabilistic systems. Preface Organization Abstracts A Behaviour-Based Approach to Quantitative Validation of Cyber-Physical Systems A Personal History of Formal Modeling and Analysis of Timed Systems Before There was FORMATS Contents Invited Papers Algebraic Model Checking for Discrete Linear Dynamical Systems 1 Introduction 1.1 Skolem Oracles 1.2 Main Results 2 Algebraic Model Checking 3 Conclusion References Zone-Based Verification of Timed Automata: Extrapolations, Simulations and What Next? 1 Introduction 2 Birth of Timed Automata for Verification: The Early 90's 2.1 Preliminaries 2.2 The Timed Automaton Model ch2AD90,ch2AD94 3 A Symbolic Approach to the Verification of Timed Automata 3.1 Zones and Symbolic Forward Computation 3.2 Difference Bounded Matrices (DBMs) 3.3 Efficiency of the Forward Analysis 4 Extrapolation: A First Solution 4.1 The First Extrapolation Operator 4.2 Two Refinements of This Approach 4.3 Problems with Diagonal Clock Constraints 5 Simulation: An Alternative Solution 6 Beyond Reachability 6.1 Weighted Timed Automata 6.2 Liveness Properties 7 Tools 7.1 A Tool for Verifying Timed Automata: Uppaal 7.2 The Tool TChecker 8 What Next? 8.1 BDD and SAT Based Methods 8.2 The Local-Time Semantics and Partial-Order Reduction 8.3 Domain-Specific Algorithms 8.4 Richer Models References Monitoring Timed Properties (Revisited) 1 Introduction 2 Related Work 3 Preliminaries 4 Monitoring in a Timed Setting 5 Time Divergence 6 A Symbolic Method for Monitoring 7 Time Uncertainty 8 Time Predictive Monitoring 9 Conclusion References Probabilistic and Timed Systems Bounded Delay Timed Channel Coding 1 Introduction 2 Preliminary Work 2.1 Timed Languages and Timed Automata 2.2 Entropy and Capacity 2.3 Pseudo-Distance on Timed Languages 2.4 The Factor Language 3 Bandwidth 3.1 Definitions 3.2 Examples 3.3 Existence of Limits 4 Encodings 4.1 Definition 4.2 Necessary Condition 4.3 Sufficient Condition 5 Conclusion and Further Work References Robustly Complete Finite-State Abstractions for Verification of Stochastic Systems 1 Introduction 2 Preliminaries 2.1 Canonical Sample Space 2.2 Markov Transition Systems 2.3 Weak Convergence and Prokhorov's Theorem 2.4 Discrete-Time Continuous-State Stochastic Systems 2.5 Robust Abstractions 3 Soundness of Robust IMC Abstractions 3.1 Weak Compactness of Marginal Space Mt of Probabilities 3.2 Weak Compactness of Probability Laws of I on Infinite Horizon 3.3 Soundness of IMC Abstractions 4 Robust Completeness of IMC Abstractions 5 Conclusion References Model Checking for Entanglement Swapping 1 Introduction 2 Preliminaries 2.1 Probabilistic Timed Automata 3 Modeling and Validation 3.1 The PTA Model 3.2 Validation Through Simulations 4 Experimental Setup 5 Results 6 Discussions and Outlook References Temporal Logic An STL-Based Formulation of Resilience in Cyber-Physical Systems 1 Introduction 2 Preliminaries 3 Specifying Resilience in STL 3.1 Resiliency Specification Language 3.2 Semantics of Resiliency Specifications 4 Case Study 4.1 UAV Package Delivery 4.2 Multi-agent Flocking 5 Related Work 6 Conclusion References MITL Verification Under Timing Uncertainty 1 Introduction 2 Preliminaries 2.1 Set Theory 2.2 Topology 3 Problem Formulation 3.1 Syntax and Semantics of MITL 3.2 Truth Sets and Interval Queues 4 Interval Queue Fundamentals 4.1 Construction Algorithm 4.2 Complementation Algorithm 5 Verification Procedure 5.1 Operators in the Interval Queue Domain 5.2 Constructing Under- and Over-Approximations 5.3 Conservativeness 6 Numerical Example 7 Conclusion A Proof of Theorem 1 References Classification of Driving Behaviors Using STL Formulas: A Comparative Study 1 Introduction 2 Preliminaries 3 Specifying Longitudinal Driving Behavior with STL 4 Methods 5 Experiments 6 Discussion and Conclusions References Timed Automata and Games Timed Games with Bounded Window Parity Objectives 1 Introduction 2 Preliminaries 3 Bounded Window Objectives 4 Verification of Timed Automata 5 Solving Timed Games References Non-blind Strategies in Timed Network Congestion Games 1 Introduction 2 Preliminaries 2.1 Timed Network Congestion Game 2.2 Studied Problems 3 Existence and Computation of Nash Equilibria 3.1 Transformation into an Equivalent Finite Concurrent Game 3.2 Existence of Nash Equilibria 3.3 Computation of Nash Equilibria 4 Social Optimality and Prices of Anarchy and Stability 4.1 Constrained-Social-Welfare Problem: Asymmetric Case 4.2 Constrained-Social-Welfare Problem: Symmetric Case 4.3 Social Optimum and Prices of Anarchy and Stability References Efficient Convex Zone Merging in Parametric Timed Automata 1 Introduction 2 Preliminaries 3 Efficient State Merging in Parametric Timed Automata 3.1 Merging Algorithm 3.2 Heuristics for Merging 3.3 Preservation of Properties 4 Experiments 4.1 Dataset and Experimental Environment 4.2 Description of the Experiments 5 Conclusion A Results for All Heuristics on the Full Benchmark References Neural Networks Neural Network Repair with Reachability Analysis 1 Introduction 2 Deep Neural Network Repair 2.1 Provably Safe DNNs 2.2 DNN Agent Repair for Deep Reinforcement Learning 2.3 Computation of Exact Unsafe Domain of ReLU DNNs 3 Framework for DNN Repair 3.1 Formulation of Loss Function for Problems 1 & 2 3.2 Repair for Deep Reinforcement Learning 4 Experiments and Evaluation 4.1 Repair of ACAS Xu Neural Network Controllers 4.2 Rocket Lander Benchmark 5 Conclusion and Future Work References On Neural Network Equivalence Checking Using SMT Solvers 1 Introduction 2 Preliminaries: Neural Networks 2.1 Notation 2.2 Neural Networks 3 Strict and Approximate Equivalences for Neural Networks 3.1 Strict Neural Network Equivalence 3.2 Approximate Neural Network Equivalences Based on Lp Norms 3.3 Approximate Neural Network Equivalences Based on Order of Outputs 3.4 Hybrid Lp-argsort Equivalences 3.5 The Neural Network Equivalence Checking Problem 3.6 Discussion of Application Domains for the Above Equivalence Relations 4 Neural Network Equivalence Checking Using SMT Solvers 4.1 Encoding Neural Networks as SMT Formulas 4.2 Encoding of the Equivalence Relation 4.3 Optimizing the Encoding 5 Experimental Results 5.1 Sanity Checks 5.2 Equivalence Checking 6 Related Work 7 Conclusions References Reachability Analysis of a General Class of Neural Ordinary Differential Equations 1 Introduction 2 Background and Problem Formulation 2.1 General Neural ODE 2.2 NODE: Applications 2.3 Reachability Analysis 2.4 Reachability Methods 3 Evaluation 3.1 Method and Tool Comparison 3.2 Case Study: Adaptive Cruise Control (ACC) 3.3 Classification NODEs 4 Related Work 5 Conclusion and Future Work References Reinforcement Learning Robust Event-Driven Interactions in Cooperative Multi-agent Learning 1 Introduction 1.1 Main Contribution 2 Preliminaries 2.1 Notation 2.2 MDPs and Multi-agent MDPs 2.3 Value Functions and Q-Learning in c-MMDPs 3 Information Sharing Between Collaborative Agents: Problem Formulation 4 Efficient Communication Strategies 4.1 Event-Driven Interactions 5 Robustness Surrogate and Its Computation 5.1 Learning the Robustness Surrogate with the Scenario Approach 6 Experiments 6.1 Benchmark: Collaborative Particle-Tag 6.2 Computation of Robustness Surrogates 6.3 Results 7 Discussion References Learning that Grid-Convenience Does Not Hurt Resilience in the Presence of Uncertainty 1 Introduction 2 Case Study 3 Methodology 4 Results 5 Reproducibility and Conclusions References Author Index