Model checking is a well-established method for automatic system verification. Besides the extensively studied qualitative case, there is also an increasing interest in the quantitative analysis of system properties. Many important quantities can be formalised as the accumulated values of weight functions. These measures include resource usage such as energy consumption, or performance metrics such as the cost-utility ratio or reliability guarantees. Different kinds of accumulation like summation, averaging and ratios are necessary to cover the diverse spectrum of quantities.
This work provides a general framework for the formalisation and verification of system models and property specifications with accumulative values.
On the modelling side, we rely on weighted extensions of well-known modelling formalisms. Besides weighted transition systems, we investigate weighted probabilistic models such as Markov chains and Markov decision processes (MDPs). The weights in this sense are functions, mapping each state or transition in the model to a value, e.g., a rational vector.
For the specification side, we provide a language in the form of an extension of temporal logic with new modalities that impose restrictions on the accumulated weight along path fragments. These fragments are regular and can be characterised by finite automata, so called monitors. Specifically, we extend linear temporal logic (LTL) and (probabilistic) computation tree logic (CTL) with such constraints.
The framework allows variation to weaker formalisms, like non-negative or integral weight functions and bounded accumulation. We study the border of decidability of the model-checking problem for different combinations of these restrictions and give complexity results and algorithms for the decidable fragment.
An implementation of the model-checking algorithms on top of the popular probabilistic model checker PRISM is provided. We also investigate several optimization techniques that can be applied to a broad range of formula patterns. The practical behaviour of the implementation and its optimization methods is put to the test by a set of scaling experiments for each model type.:1. Introduction
1.1. Goal of the Thesis
1.2. Main Contributions
1.3. Related Work
1.4. Outline
1.5. Resources
2. Preliminaries
2.1. Modeling Formalisms
2.2. Finite Automata
2.3. Propositional Logic
2.4. Temporal Logics
2.4.1. Linear Temporal Logic
2.4.2. Computation Tree Logic
2.5. Model-Checking Problems
2.5.1. Markov Decision Processes
2.5.2. Markov Chains
2.5.3. Transition Systems
2.5.4. Calculate Probabilities
3. Specifications with Weight Accumulation
3.1. Weight Constraints
3.1.1. Syntax of Weight Constraints
3.1.2. Weighted Models
3.1.3. Interpretation of Weight Constraints
3.1.4. Properties of Weight Constraints
3.2. Monitor Automata
3.2.1. Automata Classes
3.2.2. Observing WMDP Paths
3.3. Variants
3.3.1. Weight Ratios
3.3.2. Other Linear Accumulation Operators
3.3.3. Other Weight Combinations
3.3.4. Filtered Semantics
4. Linear Temporal Logic with Accumulation
4.1. Syntax and Semantics of AccLTL
4.1.1. Syntax of AccLTL
4.1.2. Semantics of AccLTL
4.1.3. Past Variant
4.1.4. Transformation of Weight Functions
4.1.5. Examples for AccLTL Formulae
4.2. Decidability Results for Accumulation LTL
4.2.1. Encoding the Post Correspondence Problem
4.2.2. Reduction of the AccLTL Model-Checking Problem
4.3. Complexity Results for Bounded Accumulation LTL
4.3.1. Transformation to Unweighted MDP and LTL
4.3.2. Reduction to LTL Model-Checking Problems
4.3.3. Algorithm
4.4. Decidability Results for Conic Accumulation LTL and RMDPs
4.4.1. Transformation to Unweighted MDP and LTL
4.4.2. Simple Weight Constraints
4.4.3. 1-dimensional Weight Constraints
4.5. NP-hard and coNP-hard Formulae for WTS and WMCs
4.5.1. Formulae for WTS
4.5.2. Formulae for WMC
4.6. Efficiently Decidable Patterns
4.7. Summary
5. Computation Tree Logic with Accumulation
5.1. Syntax and Semantics
5.1.1. Syntax and Semantics of AccCTL
5.1.2. Syntax and Semantics of AccPCTL
5.2. Decidability Results for Accumulation (P)CTL
5.3. Complexity Results for Bounded Accumulation (P)CTL
5.3.1. Weighted Markov Decision Processes
5.3.2. Weighted Markov Chains
5.3.3. Weighted Transition Systems
5.4. Decidability Results for Conic Accumulation (P)CTL and RMDPs
5.5. Summary
6. Implementation and Experiments
6.1. Implementation Details
6.1.1. Formula Expression
6.1.2. Model Construction
6.2. Optimizations
6.2.1. Single Track Method
6.2.2. Rewriting Without Until
6.2.3. Monitor Filtering
6.2.4. Detection of Optimization Methods
6.3. Scaling Experiments
6.3.1. Scaling Dimensions
6.3.2. Setting
6.3.3. Model Description
6.3.4. Input Size
6.3.5. Optimization Effects
6.3.6. Filtering
7. Conclusions
7.1. Summary
7.2. Outlook and Future Work
A. Bibliography
B. Material for the experiments
B.1. Environment for the Experiments
B.1.1. Container Image
B.1.2. Model Definitions
| Identifer | oai:union.ndltd.org:DRESDEN/oai:qucosa:de:qucosa:93760 |
| Date | 23 September 2024 |
| Creators | Wunderlich, Sascha |
| Contributors | Baier, Christel, Remke, Anne, Technische Universität Dresden |
| Source Sets | Hochschulschriftenserver (HSSS) der SLUB Dresden |
| Language | English |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, doc-type:doctoralThesis, info:eu-repo/semantics/doctoralThesis, doc-type:Text |
| Rights | info:eu-repo/semantics/openAccess |
| Relation | 10.5281/zenodo.13393585, 10.5281/zenodo.13393585, 10.5281/zenodo.13389250 |
Page generated in 0.0031 seconds