scholarly journals Probabilistic Model Checking and Autonomy

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.

Partially Observable Markov Decision Processes and Robotics

2022 ◽  
Vol 5 (1) ◽  
Author(s):  
Hanna Kurniawati
Keyword(s):  
Autonomous Systems ◽  
Optimal Solution ◽  
Lessons Learned ◽  
Annual Review ◽  
Publication Date ◽  
Mathematical Framework ◽  
Planning Under Uncertainty ◽  
Markov Decision ◽  
Partially Observable Markov ◽  
Partially Observable

Planning under uncertainty is critical to robotics. The partially observable Markov decision process (POMDP) is a mathematical framework for such planning problems. POMDPs are powerful because of their careful quantification of the nondeterministic effects of actions and the partial observability of the states. But for the same reason, they are notorious for their high computational complexity and have been deemed impractical for robotics. However, over the past two decades, the development of sampling-based approximate solvers has led to tremendous advances in POMDP-solving capabilities. Although these solvers do not generate the optimal solution, they can compute good POMDP solutions that significantly improve the robustness of robotics systems within reasonable computational resources, thereby making POMDPs practical for many realistic robotics problems. This article presents a review of POMDPs, emphasizing computational issues that have hindered their practicality in robotics and ideas in sampling-based solvers that have alleviated such difficulties, together with lessons learned from applying POMDPs to physical robots. 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.

scholarly journals Enhancing Probabilistic Model Checking with Ontologies

2021 ◽  
Author(s):  
Clemens Dubslaff ◽  
Patrick Koopmann ◽  
Anni-Yasmin Turhan
Keyword(s):  
Quantitative Analysis ◽  
Model Checking ◽  
Probabilistic Model ◽  
Description Logics ◽  
Probabilistic Model Checking ◽  
Established Method ◽  
Ontology Language ◽  
Markov Decision ◽  
Operational Models ◽  
Knowledge Intensive

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.

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

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>

scholarly journals ProMoca: Probabilistic Modeling and Analysis of Agents in Commitment Protocols

2016 ◽  
Vol 57 ◽  
pp. 465-508 ◽  
Author(s):  
Akın Günay ◽  
Yang Liu ◽  
Jie Zhang
Keyword(s):  
Model Checking ◽  
Multiagent Systems ◽  
Probabilistic Model ◽  
Model Uncertainty ◽  
Formal Language ◽  
Probabilistic Model Checking ◽  
Social Commitment ◽  
Modeling And Analysis ◽  
Essential Properties ◽  
Commitment Protocols

Social commitment protocols regulate interactions of agents in multiagent systems. Several methods have been developed to analyze properties of commitment protocols. However, analysis of an agent's behavior in a commitment protocol, which should take into account the agent's goals and beliefs, has received less attention. In this paper we present ProMoca framework to address this issue. Firstly, we develop an expressive formal language to model agents with respect to their commitments. Our language provides dedicated elements to define commitment protocols, and model agents in terms of their goals, behaviors, and beliefs. Furthermore, our language provides probabilistic and non-deterministic elements to model uncertainty in agents' beliefs. Secondly, we identify two essential properties of an agent with respect to a commitment protocol, namely compliance and goal satisfaction. We formalize these properties using a probabilistic variant of linear temporal logic. Thirdly, we adapt a probabilistic model checking algorithm to automatically analyze compliance and goal satisfaction properties. Finally, we present empirical results about efficiency and scalability of ProMoca.

scholarly journals Modeling and analysis of cell membrane systems with probabilistic model checking

BMC Genomics ◽  
2011 ◽  
Vol 12 (Suppl 4) ◽  
pp. S14 ◽  
Author(s):  
Mirlaine A Crepalde ◽  
Alessandra C Faria-Campos ◽  
Sérgio VA Campos
Keyword(s):  
Model Checking ◽  
Cell Membrane ◽  
Probabilistic Model ◽  
Probabilistic Model Checking ◽  
Membrane Systems ◽  
Modeling And Analysis

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

Micromachines ◽  
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.

Design and Control of Drones

2021 ◽  
Vol 5 (1) ◽  
Author(s):  
Mark W. Mueller ◽  
Seung Jae Lee ◽  
Raffaello D’Andrea
Keyword(s):  
Energy Consumption ◽  
Motion Planning ◽  
Recent Progress ◽  
Scaling Laws ◽  
Autonomous Systems ◽  
Annual Review ◽  
Publication Date ◽  
Trade Offs ◽  
Active Research ◽  
And Control

The design and control of drones remain areas of active research, and here we review recent progress in this field. In this article, we discuss the design objectives and related physical scaling laws, focusing on energy consumption, agility and speed, and survivability and robustness. We divide the control of such vehicles into low-level stabilization and higher-level planning such as motion planning, and we argue that a highly relevant problem is the integration of sensing with control and planning. Lastly, we describe some vehicle morphologies and the trade-offs that they represent. We specifically compare multicopters with winged designs and consider the effects of multivehicle teams. 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.

Secure Networked Control Systems

2021 ◽  
Vol 5 (1) ◽  
Author(s):  
Henrik Sandberg ◽  
Vijay Gupta ◽  
Karl H. Johansson
Keyword(s):  
Control Systems ◽  
Critical Infrastructure ◽  
Networked Control Systems ◽  
Denial Of Service ◽  
Autonomous Systems ◽  
Mitigation Strategies ◽  
Networked Control ◽  
Annual Review ◽  
Publication Date ◽  
Process Industries

Cyber-vulnerabilities are being exploited in a growing number of control systems. As many of these systems form the backbone of critical infrastructure and are becoming more automated and interconnected, it is of the utmost importance to develop methods that allow system designers and operators to do risk analysis and develop mitigation strategies. Over the last decade, great advances have been made in the control systems community to better understand cyber-threats and their potential impact. This article provides an overview of recent literature on secure networked control systems. Motivated by recent cyberattacks on the power grid, connected road vehicles, and process industries, a system model is introduced that covers many of the existing research studies on control system vulnerabilities. An attack space is introduced that illustrates how adversarial resources are allocated in some common attacks. The main part of the article describes three types of attacks: false data injection, replay, and denial-of-service attacks. Representative models and mathematical formulations of these attacks are given along with some proposed mitigation strategies. The focus is on linear discrete-time plant models, but various extensions are presented in the final section, which also mentions some interesting research problems for future work. 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.

Sign in / Sign up

Export Citation Format

Share Document