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: 80.24 EUR
Availability: OnlineOnly

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

Jane Hillston Sadegh Soudjani Masaki Waga(Editor)

Springer (Publisher)

Published on 28. August 2024

XIV, 338 pages

E-Book

PDF with digital watermarking

System requirements

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

€80.24incl. 7% vat

System requirements

for PDF with digital watermarking

E-Book Single Licence

Available for download

Description

More details

Other editions

Content

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

System requirements

Save as PDF Copy link into clipboard

Schweitzer Fachinformationen

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

Description

More details

Other editions

Additional editions

Content

System requirements