检索结果-内蒙古大学图书馆

Intelligent Quantitative Safety Monitoring Approach for ATP Using LSSVM and probabilistic model checking Considering Imperfect Fault Coverage

引用

IEEE TRANSACTIONS ON INTELLIGENT TRANSPORTATION SYSTEMS 2024年第5期25卷 3724-3738页

作者： Cheng, Ruijun Chen, Dewang Ma, Xiaoping Cheng, Yu Cheng, Huize North Univ China Sch Elect & Control Engn Taiyuan 030051 Peoples R China North Univ China Shanxi Prov Lab Ultrahigh Speed & Low Vacuum Pipel Taiyuan 030051 Peoples R China Fujian Univ Technol Sch Transportat Fuzhou 350118 Peoples R China Fuzhou Univ Coll Econ & Management Fuzhou 350118 Peoples R China Beijing Jiaotong Univ State Key Lab Adv Rail Autonomous Operat Beijing 100044 Peoples R China Beijing Jiaotong Univ Sch Traff & Transportat Beijing 100044 Peoples R China China Acad Railway Sci Corp Ltd Postgrad Dept Beijing 100044 Peoples R China China Acad Railway Sci Corp Ltd Inst Infrastruct Inspect Res Beijing 100081 Peoples R China Beijing Jingwei Hirain Technol Co Inc Automot Elect Engn Consulting Div Beijing 100191 Peoples R China

Online safety monitoring is the key technology to realize the safe operation of the automatic train protection (ATP) system. So, based on the probabilistic model checking and least square support vector machine (LSSVM) algorithms, an intelligent quantitative safety monitoring method is proposed to monitor the operational safety of ATP online. To begin with, the dynamic fault tree (DFT) model and continuous-time Markov Chains (CTMC) model of ATP are established based on the fault-tolerant structure of ATP. Then, the reliability and safety performance of DFT are evaluated by the hierarchical iterative evaluation method when considering the imperfect fault characteristics of the critical sub-equipment. Furthermore, continuous stochastic logic (CSL) is introduced to represent the temporal quantitative safety property. For the defined CSL property, the CTMC model will be verified by probabilistic model checking off-line, and the verification data set will be obtained. The distribution regularities of maximum reachable probability about the failure rate parameters of sub-equipment will be achieved by training the obtained verification data set with the LSSVM model. Finally, the quantitative safety boundaries (QSBs) of the corresponding quantitative safety levels are computed by the designed algorithm. The obtained QSBs can be used for monitoring the operational status of ATP online.

关键词： Safety Monitoring Computational modeling model checking probabilistic logic Control systems Rail transportation Automatic train protection (ATP) quantitative safety monitoring probabilistic model checking least square support vector machine (LSSVM) online reliability evaluation

来源：评论

学校读者我要写书评

暂无评论

Design and analysis of DNA strand displacement devices using probabilistic model checking

引用

JOURNAL OF THE ROYAL SOCIETY INTERFACE 2012年第72期9卷 1470-1485页

作者： Lakin, Matthew R. Parker, David Cardelli, Luca Kwiatkowska, Marta Phillips, Andrew Microsoft Res Cambridge CB3 0FB England Univ Oxford Dept Comp Sci Oxford OX1 3QD England Univ New Mexico Dept Comp Sci Albuquerque NM 87131 USA

Designing correct, robust DNA devices is difficult because of the many possibilities for unwanted interference between molecules in the system. DNA strand displacement has been proposed as a design paradigm for DNA devices, and the DNA strand displacement (DSD) programming language has been developed as a means of formally programming and analysing these devices to check for unwanted interference. We demonstrate, for the first time, the use of probabilistic verification techniques to analyse the correctness, reliability and performance of DNA devices during the design phase. We use the probabilistic model checker PRISM, in combination with the DSD language, to design and debug DNA strand displacement components and to investigate their kinetics. We show how our techniques can be used to identify design flaws and to evaluate the merits of contrasting design decisions, even on devices comprising relatively few inputs. We then demonstrate the use of these components to construct a DNA strand displacement device for approximate majority voting. Finally, we discuss some of the challenges and possible directions for applying these methods to more complex designs.

关键词： DNA computing formal verification probabilistic model checking DNA strand displacement

来源：评论

学校读者我要写书评

暂无评论

Prioritized Fault Recovery Strategies for Multi-Access Edge Computing Using probabilistic model checking

引用

IEEE TRANSACTIONS ON DEPENDABLE AND SECURE COMPUTING 2023年第1期20卷 797-812页

作者： Ray, Kaustabha Banerjee, Ansuman Indian Stat Inst Kolkata 700108 India

The advent of Multi-Access Edge Computing (MEC) has enabled service providers to mitigate high network latencies often encountered in accessing cloud services by deploying containerized application instances on edge servers situated near end users. MEC servers are, however, susceptible to various types of failures such as communication link failures, hardware failures and so on. A fault recovery strategy determines which MEC servers to utilize to re-deploy application containers in the event of a failure. In this work, we propose a two-fold fault recovery strategy characterized by application priority. We propose a Formal Methods driven local recovery strategy for high-priority applications. We use Stochastic Multi-Player Games as a Formal model to characterize the interactions between the different components in an MEC environment. We use objectives specified in probabilistic Alternating-Time Temporal Logic with a probabilistic model Checker to derive recovery strategies considering all possible execution scenarios of the model. For lower priority applications, we resort to a global recovery strategy by designing a greedy heuristic considering each server's failure probability. We use benchmark datasets to validate our approach. Experimental results show an average 14% reduction in latency with our approach in comparison with other state-of-the-art methods.

关键词： Servers Containers probabilistic logic Social networking (online) Games Real-time systems Multi-access edge computing fault-tolerance probabilistic model checking

来源：评论

学校读者我要写书评

暂无评论

ProFeat: feature-oriented engineering for family-based probabilistic model checking

引用

FORMAL ASPECTS OF COMPUTING 2018年第1期30卷 45-75页

作者： Chrszon, Philipp Dubslaff, Clemens Klueppelholz, Sascha Baier, Christel Tech Univ Dresden Fac Comp Sci Dresden Germany

The concept of features provides an elegant way to specify families of systems. Given a base system, features encapsulate additional functionalities that can be activated or deactivated to enhance or restrict the base system's behaviors. Features can also facilitate the analysis of families of systems by exploiting commonalities of the family members and performing an all-in-one analysis, where all systems of the family are analyzed at once on a single family model instead of one-by-one. Most prominent, the concept of features has been successfully applied to describe and analyze (software) product lines. We present the tool ProFeat that supports the feature-oriented engineering process for stochastic systems by probabilistic model checking. To describe families of stochastic systems, ProFeat extends models for the prominent probabilistic model checker Prism by feature-oriented concepts, including support for probabilistic product lines with dynamic feature switches, multi-features and feature attributes. ProFeat provides a compact symbolic representation of the analysis results for each family member obtained by Prism to support, e.g., model repair or refinement during feature-oriented development. By means of several case studies we show how ProFeat eases family-based quantitative analysis and compare one-by-one and all-in-one analysis approaches.

关键词： Feature-oriented systems probabilistic model checking Software product line analysis

来源：评论

学校读者我要写书评

暂无评论

Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Buchi automata

引用

INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER 2018年第2期20卷 179-194页

作者： Klein, Joachim Baier, Christel Chrszon, Philipp Daum, Marcus Dubslaff, Clemens Kluppelholz, Sascha Maercker, Steffen Mueller, David Tech Univ Dresden Inst Theoret Comp Sci D-01062 Dresden Germany

The popular model checker PRISM has been successfully used for the modeling and analysis of complex probabilistic systems. As one way to tackle the challenging state explosion problem, PRISM supports symbolic storage and manipulation using multi-terminal binary decision diagrams for representing the models and in the computations. However, it lacks automated heuristics for variable reordering, even though it is well known that the order of BDD variables plays a crucial role for compact representations and efficient computations. In this article, we present a collection of extensions to PRISM. First, we provide support for automatic variable reordering within the symbolic engines of PRISM and allow users to manually control the variable ordering at a fine-grained level. Second, we provide extensions in the realm of reward-bounded properties, namely symbolic computations of quantiles in Markov decision processes and, for both the explicit and symbolic engines, the approximative computation of quantiles for continuous-time Markov chains as well as support for multi-reward-bounded properties. Finally, we provide an implementation for obtaining minimal weak deterministic Buchi automata for the obligation fragment of linear temporal logic (LTL), with applications for expected accumulated reward computations with a finite horizon given by a co-safe LTL formula.

关键词： probabilistic model checking MTBDD Variable reordering Quantiles LTL Deterministic automata

来源：评论

学校读者我要写书评

暂无评论

Survivability Analysis Using probabilistic model checking: A Study on Wireless Sensor Networks

引用

IEEE SYSTEMS JOURNAL 2013年第1期7卷 4-12页

作者： Petridou, Sophia Basagiannis, Stylianos Roumeliotis, Manos Aristotle Univ Thessaloniki Dept Informat Thessaloniki 54124 Greece United Technol Res Ctr Cork Ireland Univ Macedonia Dept Technol Management Thessaloniki 54006 Greece

Survivability of a wireless sensor network (WSN) reflects the ability of the network to fulfill its mission despite the presence of abnormal events, such as failures. Given that sensor networks are receiving increasing attention due to the wide range of their applications, which include the critical areas of health, and military and security, survivability constitutes a key property for their study. This paper proposes a quantitative analysis for survivability evaluation of wireless sensors networks using probabilistic model checking. We define network survivability in line with four measures, namely, the frequency of failures, the data loss, the delay, and the compromised data due to a variety of failures. In particular, three types of failure events are considered, namely, node, link, and attack failures, which are due to power faults, communication faults, and black hole attacks, respectively. Then, we represent network's behavior with continuous-time Markov chains and randomly inject the aforementioned faults and attacks in the network to derive results that quantify the impact of them. Although the proposed study considers and provides results for a WSN architecture, it has the potential of being exploited in different networks with their own specifications.

关键词： Availability PRISM probabilistic model checking survivability wireless sensor networks (WSNs)

来源：评论

学校读者我要写书评

暂无评论

Synthesis method of strategy for multi-robot systems from local automatons under probabilistic model checking

引用

JOURNAL OF INTELLIGENT & FUZZY SYSTEMS 2022年第3期42卷 2057-2069页

作者： Huang, Yuchong Xu, Ning Wang, Nan Li, Jie Natl Univ Def Technol Coll Intelligence Sci & Technol 109 Deya Rd Changsha Hunan Peoples R China

Through innovatively introducing the receding horizon into probabilistic model checking, an online strategy synthesis method for multi-robot systems from local automatons is proposed to complete complex tasks that are assigned to each robot. Firstly, each robot is modeled as a Markov decision process which models both probabilistic and nondeterministic behavior. Secondly, the task specification of each robot is expressed as a linear temporal logic formula. For some tasks that robots cannot complete by themselves, the collaboration requirements take the form of atomic proposition into the LTL specifications. And the LTL specifications are transformed to deterministic rabin automatons over which a task progression metric is defined to determine the local goal states in the finite-horizon product systems. Thirdly, two horizons are set to determine the running steps in automatons and MDPs. By dynamically building local finite-horizon product systems, the collaboration strategies are synthesized iteratively for each robot to satisfy the task specifications with maximum probability. Finally, through simulation experiments in an indoor environment, the results show that the method can synthesize correct strategies online for multi-robot systems which has no restriction on the LTL operators and reduce the computational burden brought by the automaton-based approach.

关键词： Receding horizon linear temporal logic Markov decision process probabilistic model checking multi-robot collaboration

来源：评论

学校读者我要写书评

暂无评论

Mobile agent path planning under uncertain environment using reinforcement learning and probabilistic model checking

引用

KNOWLEDGE-BASED SYSTEMS 2023年第1期264卷

作者： Wang, Xia Liu, Jun Nugent, Chris Cleland, Ian Xu, Yang Southwest Jiaotong Univ Sch Comp & Artificial Intelligence Chengdu 610031 Peoples R China Ulster Univ Sch Comp Belfast BT15 1ED North Ireland Southwest Jiaotong Univ Sch Math Chengdu 610031 Peoples R China

The major challenge in mobile agent path planning, within an uncertain environment, is effectively determining an optimal control model to discover the target location as quickly as possible and eval-uating the control system's reliability. To address this challenge, we introduce a learning-verification integrated mobile agent path planning method to achieve both the effectiveness and the reliability. More specifically, we first propose a modified Q-learning algorithm (a popular reinforcement learning algorithm), called QEA - learning algorithm, to find the best Q-table in the environment. We then determine the location transition probability matrix, and establish a probability model using the assumption that the agent selects a location with a higher Q-value. Secondly, the learnt behaviour of the mobile agent based on QEA - learning algorithm, is formalized as a Discrete-time Markov Chain (DTMC) model. Thirdly, the required reliability requirements of the mobile agent control system are specified using probabilistic Computation Tree Logic (PCTL). In addition, the DTMC model and the specified properties are taken as the input of the probabilistic model Checker PRISM for automatic verification. This is preformed to evaluate and verify the control system's reliability. Finally, a case study of a mobile agent walking in a grids map is used to illustrate the proposed learning algorithm. Here we have a special focus on the modelling approach demonstrating how PRISM can be used to analyse and evaluate the reliability of the mobile agent control system learnt via the proposed algorithm. The results show that the path identified using the proposed integrated method yields the largest expected reward.(c) 2023 Elsevier B.V. All rights reserved.

关键词： Expected reward Mobile agent Uncertain environment probabilistic model checking Q-learning

来源：评论

学校读者我要写书评

暂无评论

Cost-aware horizontal scaling of NoSQL databases using probabilistic model checking

引用

CLUSTER COMPUTING-THE JOURNAL OF NETWORKS SOFTWARE TOOLS AND APPLICATIONS 2017年第3期20卷 2687-2701页

作者： Naskos, Athanasios Gounaris, Anastasios Katsaros, Panagiotis Aristotle Univ Thessaloniki Dept Informat Thessaloniki 54124 Greece

In this work we target horizontal scaling of NoSQL databases, which exhibit highly varying, unpredictable and difficult to model behavior coupled with transient phenomena during VM removals and/or additions. We propose a solution that is cost-aware, systematic, dependable while it accounts for performance unpredictability and volatility. To this end, we model the elasticity as a dynamically instantiated Markov decision process, which can be both solved and verified using probabilistic model checking. Further, we propose a range of complementary decision making policies, which are thoroughly evaluated in workloads from real traces. The evaluation provides strong insights into the trade-offs between performance and cost that our policies can achieve and prove that we can avoid both over- and under-provisioning.

关键词： Cloud elasticity probabilistic model checking Quantitative verification Autonomic computing PRISM NoSQL databases

来源：评论

学校读者我要写书评

暂无评论

Constraint-based debugging in probabilistic model checking

引用

COMPUTING 2023年第2期105卷 321-351页

作者： Debbi, Hichem Univ Msila Dept Comp Sci Msila Algeria

A counterexample in model checking is an error trace that represents a valuable tool for debugging. In probabilistic model checking (PMC), the counterexample generation has a quantitative aspect. A probabilistic counterexa mple is a set of diagnostic paths in which a path formula holds, and whose probability mass violates the probability threshold. Comparing to conventional model checking, debugging and analyzing counterexamples in PMC is a very complex task. In this paper, we propose a debugging method for Markov models described in the probabilistic model checker PRISM by analyzing probabilistic counterexamples. The probabilistic counterexample generated is subjected to a set of assertions, which are employed for detecting incorrect behavior of the model, and thus locating the erroneous transitions contributing to the error. Our method has been implemented and tested on many PRISM models of different case studies. The method shows promising results in terms of execution time as well as its efficiency in locating the erroneous transitions.

关键词： PRISM probabilistic model checking Markov models Debugging Constraints Counterexamples

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：