Enhancing Probabilistic Model Checking with Ontologies

AbstractProbabilistic model checking (PMC) is a well-established method for the quantitative analysis of state based operational models such as Markov decision processes. Description logics (DLs) provide a well-suited formalism to describe and reason about knowledge and are used as basis for the web ontology language (OWL). We investigate how such knowledge described by DLs can be integrated into the PMC process, introducing ontology-mediated PMC. Specifically, we propose ontologized programs as a formalism that links ontologies to behaviors specified by probabilistic guarded commands, the de-facto standard input formalism for PMC tools such as Prism. Through DL reasoning, inconsistent states in the modeled system can be detected. We present three ways to resolve these inconsistencies, leading to different Markov decision process semantics. We analyze the computational complexity of checking whether an ontologized program is consistent under these semantics. Further, we present and implement a technique for the quantitative analysis of ontologized programs relying on standard DL reasoning and PMC tools. This way, we enable the application of PMC techniques to analyze knowledge-intensive systems.We evaluate our approach and implementation on amulti-server systemcase study,where different DL ontologies are used to provide specifications of different server platforms and situations the system is executed in.

Download Full-text

Quantitative Analysis of System Based on Extended UML State Diagrams and Probabilistic Model Checking

Journal of Software ◽

10.4304/jsw.5.7.793-800 ◽

2010 ◽

Vol 5 (7) ◽

Cited By ~ 3

Author(s):

Yefei Zhao ◽

Zongyuan Yang ◽

Jinkui Xie ◽

Qiang Liu

Keyword(s):

Quantitative Analysis ◽

Model Checking ◽

Probabilistic Model ◽

Probabilistic Model Checking ◽

State Diagrams

Download Full-text

Improving Graph-based methods for computing qualitative properties of markov decision processes

Indonesian Journal of Electrical Engineering and Computer Science ◽

10.11591/ijeecs.v17.i3.pp1571-1577 ◽

2020 ◽

Vol 17 (3) ◽

pp. 1571

Author(s):

Mohammadsadegh Mohagheghi ◽

Khayyam Salehi

Keyword(s):

Model Checking ◽

Markov Decision Processes ◽

Probabilistic Model ◽

Decision Processes ◽

Probabilistic Model Checking ◽

Qualitative Properties ◽

Verification Method ◽

Main Class ◽

Markov Decision ◽

Iterative Numerical Methods

<span>Probabilistic model checking is a formal verification method, which is used to guarantee the correctness of the computer systems with stochastic behaviors. Reachability probabilities are the main class of properties that are proposed in probabilistic model checking. Some graph-based pre-computation can determine those states for which the reachability probability is exactly zero or one. Iterative numerical methods are used to compute the reachability probabilities for the remaining states. In this paper, we focus on the graph-based pre-computations and propose a heuristic to improve the performance of these pre-computations. The proposed heuristic approximates the set of states that are computed in the standard pre-computation methods. The experiments show that the proposed heuristic can compute a main part of the expected states, while reduces the running time by several orders of magnitude.</span>

Download Full-text

Counterexample Generation for Probabilistic Model Checking Micro-Scale Cyber-Physical Systems

Micromachines ◽

10.3390/mi12091059 ◽

2021 ◽

Vol 12 (9) ◽

pp. 1059

Author(s):

Yang Liu ◽

Yan Ma ◽

Yongsheng Yang ◽

Tingting Zheng

Keyword(s):

Genetic Algorithm ◽

Model Checking ◽

Probabilistic Model ◽

Cyber Physical Systems ◽

Probabilistic Model Checking ◽

Dynamic Power Management ◽

Search Range ◽

Physical Systems ◽

Micro Scale ◽

Markov Decision

Micro-scale Cyber-Physical Systems (MCPSs) can be automatically and formally estimated by probabilistic model checking, on the level of system model MDPs (Markov Decision Processes) against desired requirements in PCTL (Probabilistic Computation Tree Logic). The counterexamples in probabilistic model checking are witnesses of requirements violation, which can provide the meaningful information for debugging, control, and synthesis of MCPSs. Solving the smallest counterexample for probabilistic model checking MDP has been proven to be an NPC (Non-deterministic Polynomial complete) problem. Although some heuristic methods are designed for this, it is usually difficult to fix the heuristic functions. In this paper, the Genetic algorithm optimized with heuristic, i.e., the heuristic Genetic algorithm, is firstly proposed to generate a counterexample for the probabilistic model checking MDP model of MCPSs. The diagnostic subgraph serves as a compact counterexample, and diagnostic paths of MDP constitute an AND/OR tree for constructing a diagnostic subgraph. Indirect path coding of the Genetic algorithm is used to extend the search range of the state space, and a heuristic crossover operator is used to generate more effective diagnostic paths. A prototype tool based on the probabilistic model checker PAT is developed, and some cases (dynamic power management and some communication protocols) are used to illustrate its feasibility and efficiency.

Download Full-text

Quantitative analysis of a certified e-mail protocol in mobile environments: A probabilistic model checking approach

Computers & Security ◽

10.1016/j.cose.2011.02.001 ◽

2011 ◽

Vol 30 (4) ◽

pp. 257-272 ◽

Cited By ~ 14

Author(s):

S. Basagiannis ◽

S. Petridou ◽

N. Alexiou ◽

G. Papadimitriou ◽

P. Katsaros

Keyword(s):

Quantitative Analysis ◽

Model Checking ◽

Probabilistic Model ◽

Probabilistic Model Checking ◽

Mobile Environments ◽

E Mail

Download Full-text

Probabilistic Model Checking and Autonomy

Annual Review of Control Robotics and Autonomous Systems ◽

10.1146/annurev-control-042820-010947 ◽

2021 ◽

Vol 5 (1) ◽

Author(s):

Marta Kwiatkowska ◽

Gethin Norman ◽

David Parker

Keyword(s):

Model Checking ◽

Probabilistic Model ◽

Stochastic Games ◽

Cooperative Behavior ◽

Autonomous Systems ◽

Probabilistic Model Checking ◽

Annual Review ◽

Publication Date ◽

Modeling And Analysis ◽

Markov Decision

The design and control of autonomous systems that operate in uncertain or adversarial environments can be facilitated by formal modeling and analysis. Probabilistic model checking is a technique to automatically verify, for a given temporal logic specification, that a system model satisfies the specification, as well as to synthesize an optimal strategy for its control. This method has recently been extended to multiagent systems that exhibit competitive or cooperative behavior modeled via stochastic games and synthesis of equilibria strategies. In this article, we provide an overview of probabilistic model checking, focusing on models supported by the PRISM and PRISM-games model checkers. This overview includes fully observable and partially observable Markov decision processes, as well as turn-based and concurrent stochastic games, together with associated probabilistic temporal logics. We demonstrate the applicability of the framework through illustrative examples from autonomous systems. Finally, we highlight research challenges and suggest directions for future work in this area. Expected final online publication date for the Annual Review of Control, Robotics, and Autonomous Systems, Volume 5 is May 2022. Please see http://www.annualreviews.org/page/journal/pubdates for revised estimates.

Download Full-text