Abstract model repair for probabilistic systems
| Autor: | Panagiotis Katsaros, George Chatzieleftheriou |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
Soundness
Markov chain Computer science Probabilistic logic 020207 software engineering 02 engineering and technology State (functional analysis) Computer Science Applications Theoretical Computer Science Metric space Computational Theory and Mathematics Discrete time and continuous time 0202 electrical engineering electronic engineering information engineering State space 020201 artificial intelligence & image processing Temporal logic Algorithm Information Systems |
| Zdroj: | Information and Computation. 259:142-160 |
| ISSN: | 0890-5401 |
| DOI: | 10.1016/j.ic.2018.02.019 |
| Popis: | Given a Discrete Time Markov Chain M and a probabilistic temporal logic formula φ, where M violates φ, the problem of Model Repair is to obtain a new model M ′ , such that M ′ satisfies φ. Additionally, the changes made to M in order to obtain M ′ should be minimum with respect to all such M ′ . The state explosion problem makes the repair of large probabilistic systems almost infeasible. In this paper, we use the abstraction of Discrete Time Markov Chains in order to speed-up the process of model repair for temporal logic reachability properties. We present a framework based on abstraction and refinement, which reduces the state space of the probabilistic system to repair at the price of obtaining an approximate solution. A metric space is defined over the set of DTMCs, in order to measure the differences between the initial and the repaired models. For the repair, we introduce an algorithm and we discuss its important properties, such as soundness and complexity. As a proof of concept, we provide experimental results for probabilistic systems with diverse structures of state spaces, including the well-known Craps game, the IPv4 Zeroconf protocol, a message authentication protocol and the gambler's ruin model. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect