Quantitative Evaluation of Systems: 20th International Conference, QEST 2023, Antwerp, Belgium, September 20–22, 2023, Proceedings (Lecture Notes in Computer Science)

This book constitutes the proceedings of the 20th International Conference on Quantitative Evaluation of Systems, QEST 2023, which took place in Antwerp, Belgium, in September 2023. The 23 papers included in this book were carefully reviewed and selected from 44 submissions. They deal with current topics in quantitative evaluation and verification of computer systems and networks, focusing on data-driven and machine-learning systems, case studies, and tool papers. The book also contains the extended abstract of the invited talk from David Parker. Preface Organization Contents Multi-agent Verification and Control with Probabilistic Model Checking 1 Introduction 2 Model Checking for Stochastic Games 2.1 Turn-based Stochastic Games 2.2 Concurrent Stochastic Games 2.3 Equilibria for Stochastic Games 3 Opportunities and Challenges References Formal Controller Synthesis for Markov Jump Linear Systems with Uncertain Dynamics*-4pt 1 Introduction 2 Foundations and Problem Statement 2.1 Markov Decision Processes 2.2 Markov Jump Linear Systems 2.3 Probabilistic Computation Tree Logic 2.4 Problem Statement 3 Abstractions of Non-Hybrid Dynamical Systems 4 Abstractions of Markov Jump Linear Systems 4.1 iMDP Abstraction for Individual Modes 4.2 Abstraction Under Uncertain Markov Jumps (Assumption A) 4.3 Abstraction Under Unknown Markov Jumps (Assumption B) 5 Synthesis for General PCTL Formulae 5.1 Unsatisfied Formulae 5.2 Controller Synthesis via Policy Refinement 6 Numerical Experiments 6.1 UAV Motion Planning 6.2 Temperature Regulation in a Building 6.3 Controller Synthesis for General PCTL Formulae 7 Conclusions and Future Work References Jajapy: A Learning Library for Stochastic Models 1 Introduction 2 Jajapy in a Nutshell 3 Learning Probabilistic Models 4 Architecture and Technical Aspects 5 Experimental Evaluation and Comparison 5.1 Jajapy validation testing 5.2 Experimental Evaluation of the Scalability 5.3 Comparison with AALpy 6 Conclusions and Future Work References Introducing Asynchronicity to Probabilistic Hyperproperties 1 Introduction 2 Preliminaries 3 Asynchronous HyperPCTL 3.1 Stutter Schedulers 3.2 Syntax 3.3 Semantics 4 Applications of AHyperPCTL 5 Model Checking AHyperPCTL 6 Implementation and Evaluation 7 Conclusions References A Bounded Model Checking Technique for Discrete-Time Nonlinear Systems 1 Introduction 2 Discrete-Time Nonlinear System Model 2.1 Example: An Inverted Pendulum Model 3 Specification on Nonlinear System Models 3.1 LTLN: The Specification Logic 3.2 Example: Specification on the Inverted Pendulum Model 4 LTLN Model Checking Algorithm 4.1 DNF-based Model Checking Algorithm 4.2 Büchi Automaton-based Model Checking Algorithm 4.3 Model Checker Implementation 5 LTLN Model Checking Examples 5.1 Inverted Pendulum 5.2 Nonlinear Pharmacokinetics 6 Conclusion References An MM Algorithm to Estimate Parameters in Continuous-Time Markov Chains 1 Introduction 2 Preliminaries and Notation 3 Parametric Continuous-Time Markov Chains 4 Estimating Parameters from Partial Observations 5 Experimental Evaluation 6 Case Study: SIR Modeling of Pandemic 7 Related Work 8 Conclusion and Future Work References STAMINA in C++: Modernizing an Infinite-State Probabilistic Model Checker 1 Introduction 2 Overview of Stamina 3 Software Architecture 4 Results 5 Discussion 6 Conclusion References Skipping and Fetching: Insights on Non-conventional Product-Form Solutions 1 Introduction 2 Related Work 3 Background on Skip-Over Queuing Networks 4 Fetching Queuing Networks with Finite Capacity 5 A GSPN-Based Semantics 6 Duality Results Between CFQNWs and CSQNBs 7 Conclusion References On the Maximum Queue Length of the Hyper Scalable Load Balancing Push Strategy 1 Introduction 2 Problem Statement 3 Exponential Job Sizes 4 Vanishing Waiting Times: m=1 4.1 Hyper Exponential Job Sizes 4.2 Coxian Job Sizes 4.3 Erlang kS Job Sizes 5 Conclusions References Data-Driven Inference of Chemical Reaction Networks via Graph-Based Variational Autoencoders 1 Introduction 2 Methods 2.1 Background 2.2 Inference 3 Experiments 4 Conclusion References Modeling Uncertain Biomass Composition in Genome-Scale Metabolic Models with Flexible Nets 1 Introduction 2 Flexible Nets for GEMs 3 Modelling Uncertain Biomass Composition 4 Steady State Bounds 5 Experimental Results 6 Conclusions References On the Trade-Off Between Efficiency and Precision of Neural Abstraction 1 Introduction 2 Preliminaries 2.1 Dynamical Models and Safety Verification 2.2 Linear Hybrid Automata 2.3 Neural Networks 2.4 Neural Abstractions 2.5 Activation Functions Determine the Shape of the Abstract Neural Models 3 Formal Synthesis of Template-Dependent Neural Abstractions 3.1 Training Procedures for Neural Abstractions 3.2 Certification of the Quality of a Neural Abstraction 3.3 Refining the Precision of the Abstraction 4 Safety Verification Using Neural Abstractions 5 Experimental Results 5.1 Non-Lipschitz Models 5.2 Abstraction of Neural ODEs 6 Conclusions A Benchmarks of NonLinear Dynamical Systems B Experiments on Error Refinement Scheme References Equilibrium Analysis of Markov Regenerative Processes 1 Introduction 2 Markov Regenerative Processes 2.1 Stochastic Time Petri Nets 2.2 Markov Regenerative Processes 2.3 Analysis with Stochastic State Classes 3 Equilibrium Analysis 3.1 Steady-State Probabilities 3.2 Equilibrium PDFs 4 Experimental Evaluation 5 Conclusions A Stochastic Time Petri Nets References Max-Entropy Sampling for Deterministic Timed Automata Under Linear Duration Constraints 1 Introduction 2 Preliminaries 2.1 General Timed Languages and Their Measure 2.2 Languages Recognized by DTA and Their Measures 3 Max-Entropy Theorem Under Linear Duration Constraints 4 Max-Entropy Theorem with Prescribed Mean Duration 4.1 Computing LTV and Max-Entropy Sampling for Timed Automata 5 Experiments 6 Conclusion and Future Work References Quasi-Deterministic Burstiness Bound for Aggregate of Independent, Periodic Flows 1 Introduction 2 Assumptions and Problem Statement 3 Background and Related Works 4 Homogeneous Case 5 Heterogeneous Case 6 Numerical Evaluation 6.1 Homogeneous Case 6.2 Heterogeneous Case 7 Conclusion References Matching Distributions Under Structural Constraints 1 Introduction 2 Preliminaries 3 The Ccc Satisfiability Problem (CccSat) 4 Semi-Algorithm for Solving CccSat 4.1 Satisfying Simple Cases 4.2 Problem Decomposition 4.3 Reduction to SMT Instances 5 Empirical Evaluation 6 Conclusion References Comparing Two Approaches to Include Stochasticity in Hybrid Automata*-4pt 1 Introduction 2 Fundamentals 2.1 Hybrid Automata 2.2 Basic Stochastic Notions 3 Extending Hybrid Automata with Stochasticity 3.1 Composed Scheduling 3.2 Decomposed Scheduling 3.3 Induced Stochastic Process 3.4 Relation of Composed and Decomposed Scheduling 3.5 Extending (De-)composed Scheduling with Invariants 4 Classification of Existing Approaches 5 Conclusion References Analysis of an Epoch Commit Protocol for Distributed Processing Systems 1 Introduction 1.1 Related Literature 2 The Model 3 Solution 3.1 Performance Metrics 3.2 Determination of G(y,0) and G(y,1) 3.3 Fast Numerical Algorithm 4 Experimental Results 5 Non-exponential Work Periods 6 Conclusions References Causal Reversibility Implies Time Reversibility 1 Introduction 2 Background on Reversibility 2.1 Causal Reversibility of Concurrent Systems 2.2 Time Reversibility of Continuous-Time Markov Chains 3 Relationships Between Causal and Time Reversibilities 3.1 Extending RLTSI with Rates 3.2 From Causal Reversibility to Time Reversibility 3.3 Discussion 4 An Application to the Dining Philosophers Problem 4.1 The Problem 4.2 The RMLTSI Model 4.3 Time Reversibility and Performance Evaluation 5 Conclusions References Deductive Controller Synthesis for Probabilistic Hyperproperties 1 Introduction 2 Problem Formulation 2.1 Probabilistic Models 2.2 HyperPCTL with Structural Constraints 3 Family of Controllers 4 Deductive Exploration 4.1 Guided Abstraction Refinement Scheme 4.2 Splitting Strategy 4.3 Synthesis Algorithm (AR Loop) 5 Experiments 6 Conclusions References Model Abstraction and Conditional Sampling with Score-Based Diffusion Models 1 Introduction 2 Proposed Approach 3 Preliminary Results 4 Conclusion and Future Works References Probabilistic Counterexample Guidance for Safer Reinforcement Learning 1 Introduction 2 Background 2.1 Problem Framework 2.2 Probabilistic Model Checking and Counterexamples 3 Counterexample-Guided Reinforcement Learning 3.1 Safety-Relevant State-Space Abstraction 3.2 Online-Offline Learning with Counterexample Guidance 4 Evaluation 5 Related Work 6 Conclusion References Symbolic Semantics for Probabilistic Programs 1 Introduction 2 Probabilistic Programming 2.1 Example Program 2.2 Language 3 Symbolic Execution 3.1 Symbolic Substitutions 3.2 Path Conditions and Path Observations 3.3 Final Configurations 3.4 Symbolic Semantics 4 Correctness 5 Implementation and Experiments 6 Related Work 7 Conclusion and Future Work References Verification of Quantum Systems Using Barrier Certificates 1 Introduction 2 Background 2.1 Safety Analysis 2.2 Barrier Certificates 3 Complex-Valued Barrier Certificates 4 Generating Satisfiable Barrier Certificates for Quantum Systems 4.1 An Algorithmic Solution 5 Application to Quantum Systems 5.1 Hadamard Operation Example 5.2 Phase Operation Example 5.3 Controlled-NOT Operation Example 6 Conclusions References Author Index