Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems

Name: Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems | First International Joint Conference, QEST+FORMATS 2024, Calgary, AB, Canada, September 9-13, 2024, Proceedings
Brand: Springer
Price: 160.49 EUR
Availability: OnlineOnly

First International Joint Conference, QEST+FORMATS 2024, Calgary, AB, Canada, September 9-13, 2024, Proceedings

Jane Hillston Sadegh Soudjani Masaki Waga(Herausgeber*in)

Springer (Verlag)

Erschienen am 28. August 2024

XIV, 338 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-031-68416-6 (ISBN)

160,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

Intro
Preface
Organization
Compositional Verification and Run-time Monitoring for Learning-Enabled Autonomous Systems - CONFEST 2024 (ABSTRACT OF THE INVITED TALK)
Contents
Certificates and Witnesses for Multi-objective Queries in Markov Decision Processes
1 Introduction
2 Preliminaries
3 Certificates and Witnesses for ReachInv-Queries
3.1 Farkas Certificates and Witnesses for Reach-Queries
3.2 Transferring Witnesses
4 Certificates and Witnesses for Metapost-Queries
5 Experiments
6 Conclusion
References
Diagnosis of Stochastic Systems: Optimising Costs and Delays
1 Introduction
2 Preliminaries
2.1 Probabilistic Labelled Transition System
2.2 Partial Observation and Ambiguity
2.3 Fault and Diagnosis
2.4 Diagnosability Under a Given Static Mask
2.5 Cost and Latency of Diagnosis
3 Optimising Static Diagnosis
3.1 Reducing Costs
3.2 Computing the Latency of S-FF-Diagnosis
4 Dynamic Diagnosis
5 Conclusion
References
A Framework for Optimisation Based Stochastic Process Discovery
1 Introduction
1.1 Related Work
2 Preliminaries
3 Method
3.1 Computation of Trace Probability of a Stochastic WN
3.2 Measuring the Distance Between Two Stochastic Languages
3.3 Weight Optimization
3.4 Execution Time
4 Results
5 Conclusion
References
QuADTool: Attack-Defense-Tree Synthesis, Analysis and Bridge to Verification
1 Introduction
2 Attack-Defense Trees
3 Tool Overview
3.1 Model Construction
3.2 ATBEST Benchmark Collection for Attack-Defense Trees
3.3 Obtaining PAC-Quantities for Attack-Defense Trees
3.4 Analyses
4 PAC-Quantitative ADT: Fighting the Uncertainty
4.1 Quantitative ADT and PAC-Quantitative ADT
4.2 PAC-Input Extension of Bottom-Up Analyses
4.3 Analysis Example
5 Experiments
6 Conclusion and Future Work
A Quantitative Bottom-Up Analyses for Cost and Delays
B Conversion Times
References
Adaption of Stochastic Models (ASMo) - A Tool for Input Modeling -
1 Introduction
2 Tool Structure
2.1 Module Structure
2.2 Graphical User Interface
3 Data Traces
4 Distributions
4.1 Standard Distributions
4.2 Mixture Distributions
4.3 Phase-Type Distributions
5 Examples
5.1 Fitting of Mixture Distributions
5.2 Fitting of Network Traces
6 Conclusion
References
Approximation of Cumulative Distribution Functions by Bernstein Phase-Type Distributions
1 Introduction
2 Background
2.1 Bernstein Polynomials
2.2 Bernstein Exponentials
2.3 Phase-Type Distributions
3 Approximation of Cumulative Density Functions by Bernstein Phase-Type Distributions
4 Stochastically Smaller and Larger Approximation
5 Numerical Investigations
6 Conclusions
References
On Parametric DBMs and Their Applications to Time Petri Nets
1 Introduction
2 Definitions
2.1 Preliminaries
2.2 Tropical Semi-ring
2.3 Parametric Time Petri Nets
2.4 Parametric Reachability Problems
2.5 Parametric State Classes
2.6 An Efficient State Class Successor for TPNs
3 Tropical PDBM
3.1 Reachability Algorithm
3.2 Successor Operator
3.3 Inclusion
3.4 Splitting and Classical PDBMs
4 Case Studies
4.1 Fischer's Mutual-Exclusion Protocol
4.2 Level Crossing
4.3 Producerconsumer
4.4 Discussion
5 Conclusion
A Proposition 2
B Proposition 3
C Proposition 5
D Models for the Experiments
References
Dissimilarity for Linear Dynamical Systems
1 Introduction
2 Preliminaries and Notation
3 Backward Dissimilarity
4 Computation of Backward Dissimilarity
5 Related Work
6 Applications: The Thermostat Case Study
7 Experimental Comparison with LCS Bisimulation
8 Conclusion
References
MMLT/ik: Efficiently Learning Mealy Machines with Local Timers by Using Imprecise Symbol Filters
1 Introduction
2 Related Work
3 Preliminaries
3.1 Mealy Machines with Local Timers
3.2 Learning MMLTs
4 Symbol Filters for MMLTs
5 The MMLT/ik Method
5.1 Transition Output Validation
5.2 Extended Timed Counterexample Analysis
5.3 Silent-Change Search
5.4 Savings Potential
6 Practical Evaluation
7 Conclusion and Future Work
References
An Expressive Timed Modal Mu-Calculus for Timed Automata
1 Introduction
2 Timed Automata
2.1 Clocks, Clock Constraints and Clock Valuations
2.2 Syntax of Timed Automata
2.3 Semantics of Timed Automata
3 Timed Modal Mu-Calculi
3.1 Timed Modal Mu-Calculus Lrel,
3.2 Other Timed Modal Mu-Calculi
3.3 Mu-Calculus Expressiveness Results
4 Timed Computation Tree Logic (TCTL)
4.1 Syntax of TCTL
4.2 Semantics of TCTL
5 TCTL Expressiveness Results
5.1 TCTL# L,, TCTL# T
5.2 TCTLLrel,
6 Conclusion and Directions for Future Work
References
Efficiently Computable Distance-Based Robustness for a Practical Fragment of STL
1 Introduction
2 Preliminaries
2.1 Boolean Signals
2.2 Signal Temporal Logic
3 The Distance d
3.1 Algorithm to Compute d Efficiently
4 Distance-Based Temporal Robustness
4.1 Hardness of Computing
4.2 A Tractable Fragment of STL
5 Related Work
6 Conclusion
References
Rare-Event Guided Analysis of Infinite-State Chemical Reaction Networks
1 Introduction
1.1 Related Work
2 Background
2.1 Chemical Reaction Networks
2.2 Probabilistic Guarded Command Language
3 Methods
3.1 Generating K-Bounded Constraints
3.2 Probabilistic Program Conforming to K-Bounded Constraints
4 Experiments
A Appendix A
References
Transient Evaluation of Non-Markovian Models by Stochastic State Classes and Simulation
1 Introduction
2 Background
2.1 Stochastic Time Petri Nets
2.2 Transient Evaluation by the Method of Stochastic State Classes
2.3 Monte Carlo Simulation and Importance Sampling
3 Switch from Stochastic State Classes to Simulation
3.1 Approach Overview
3.2 Conditioning Stochastic State Classes on Fired Transition
3.3 Sampling Methods
4 Collecting Results and Obtaining Confidence Intervals
5 Experimental Evaluation
5.1 Four Overlapping Activities
5.2 Repairable Dynamic Fault Tree
6 Conclusion
A Stochastic Time Petri Net of Dynamic Fault Tree
B Implementation Details of Sampling Methods
References
Probabilistic Loop Synthesis from Sequences of Moments
1 Introduction
2 Related Work
3 Preliminaries
4 Synthesis Algorithm
4.1 Programming Model
4.2 Specification
4.3 Matching the Means
4.4 Matching the (Co-)variances
4.5 Matching Third Mixed Moments
4.6 Random Variable Construction
5 Case Studies
5.1 Improving Moment-Matching for Loops
5.2 Reconstructing Loops from Moments
5.3 Specification from Data
6 Discussion and Conclusion
References
IMPaCT: Interval MDP Parallel Construction for Controller Synthesis of Large-Scale STochastic Systems
1 Introduction
1.1 Original Contributions
1.2 Related Literature
1.3 Overview of IMPaCT
2 Discrete-Time Stochastic Control Systems
3 Interval Markov Decision Processes
3.1 Complexity Analysis for Serial Construction of IMDP
3.2 Temporal Logic Specifications
4 Parallel Construction of IMDP
4.1 Complexity Analysis for Parallel Construction of IMDP
4.2 Low-Cost Abstraction
5 Controller Synthesis with Interval Iteration
6 Parallel Controller Synthesis with Interval Iteration
7 Loading and Saving Files
8 Benchmarking and Case Studies
8.1 Comparisons
9 Conclusion
References
Controller Synthesis in Timed Büchi Automata: Robustness and Punctual Guards
1 Introduction
2 Partial Robustness Semantics
3 Preliminaries
4 Robustness of a Finite Path
5 Robustness of an Infinite Path
6 Slicing Regions
7 Proof of Theorem 8
8 Conclusion
References
A Floyd-Warshall Approach to Value Computation in Markov Decision Processes
1 Introduction
2 Framework and Notations
3 Floyd-Warshall Path Integrator
3.1 Weighted Automata and Path Integrals
3.2 Floyd-Warshall Recursion
3.3 Expected Discounted Reward as an Integral over Paths
4 Progressive Floyd-Warshall Integration
4.1 A Progressive Algorithm
4.2 Approximation by Early Stopping
5 Case Study
6 Conclusion
References
Multi-agent Path Finding for Timed Tasks Using Evolutionary Games
1 Introduction
2 Preliminaries
3 Reward Shaping for Timed Multi-agent Reach-Avoid Problems
4 Policy Optimization
4.1 Algorithmic Framework Using Evolutionary Game Theory
5 Experiments and Results
5.1 Results and Discussion
6 Related Work
7 Conclusion
References
What is Your Discount Factor?
1 Introduction
2 Related Work
3 Problem Definition
4 Optimal Policy Regions
5 Computing Discount Factor Ranges
5.1 Approach Using Root Isolation
6 Near-Optimal Policy Regions
7 Eliciting Discount Factor for Varying Environments
8 Conclusion
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken