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

p-Automata: New foundations for discrete-time probabilistic verification

PERFORMANCE EVALUATION 2012年第7-8期69卷 356-378页

作者： Huth, Michael Piterman, Nir Wagner, Daniel Univ Leicester Dept Comp Sci Leicester LE1 7RH Leics England Univ London Imperial Coll Sci Technol & Med Dept Comp London SW7 2AZ England

We introduce p-Automata, which are automata that accept languages of Markov chains, by adapting notions and techniques from alternating tree automata to the realm of Markov chains. The set of languages of p-automata is closed under Boolean operations, and for every PCTL formula it contains the language of the set of models of the formula. Furthermore, the language of every p-automaton is closed under probabilistic bisimulation. Similar to tree automata, whose acceptance is defined via two-player games, we define acceptance of Markov chains by p-automata through two-player stochastic games. We show that acceptance is solvable in EXPTIME;but for automata that arise from PCTL formulas acceptance matches that of PCTL model checking, namely, linear in the formula and polynomial in the Markov chain. We also derive a notion of simulation between p-automata that approximates language containment in EXPTIME and is complete for Markov chains. These foundations therefore enable abstraction-based probabilistic model checking for probabilistic specifications that subsume Markov chains, and LTL and CTL* like logics. (C) 2012 Elsevier B.V. All rights reserved.

关键词： Markov chains probabilistic computation tree logic Game theory Fairness conditions probabilistic evidence

来源：评论

学校读者我要写书评

暂无评论

PCTL model checking of Markov chains: Truth and falsity as winning strategies in games

引用

PERFORMANCE EVALUATION 2010年第9期67卷 858-872页

作者： Fecher, Harald Huth, Michael Piterman, Nir Wagner, Daniel Univ London Imperial Coll Sci Technol & Med Dept Comp London SW7 2AZ England Univ Freiburg Inst Informat D-79110 Freiburg Germany

probabilistic model checking is a technique for verifying whether a model such as a Markov chain satisfies a probabilistic, behavioral property - e.g. "with probability at least 0.999, a device will be elected leader". Such properties are expressible in probabilistic temporal logics, e.g. PCTL, and efficient algorithms exist for checking whether these formulae are true or false on finite-state models. Alas, these algorithms do not supply diagnostic information for why a probabilistic property does or does not hold in a given model. We provide here complete and rigorous foundations for such diagnostics in the setting of countable labeled Markov chains and PCTL. For each model and PCTL formula, we define a game between a Verifier and a Refuter that is won by Verifier if the formula holds in the model, and won by Refuter if it does not hold. Games are won by exactly one player, through monotone strategies that encode the diagnostic information for truth and falsity (respectively). These games are infinite with Buchi type acceptance conditions where simpler fairness conditions are shown to be not sufficient. Verifier can always force finite plays for certain PCTL formulae, suggesting the existence of finite-state abstractions of models that satisfy such formulae. (C) 2009 Elsevier B.V. All rights reserved.

关键词： Markov chains probabilistic computation tree logic Game theory Fairness conditions probabilistic evidence

来源：评论

学校读者我要写书评

暂无评论

A New Trust Chain Security Evaluation Model and Tool 1

引用

10th International ICST Conference on Security and Privacy in Communication Networks (SecureComm)

作者： Hu, Wei Ji, Dongyao Wang, Ting Yao, Gang Chinese Acad Sci Inst Informat Engn State Key Lab Informat Secur Beijing Peoples R China

ISBN: (数字)9783319238029

ISBN: (纸本)9783319238029;9783319238012

We've build a model of trust chain, and developed TCSE, a tool for estimating the security properties of the trust chain. The highlight of TCSE is that it can generate a probabilistic finite state automaton and verify or calculate four security properties of a trust chain following our algorithms. These properties are: credibility, usability, restorability and conformity. With these four values of a trust chain, we can estimate the security of a trusted computer (a computer with a trusted computing module). Using this tool, an ordinary user with the help of the Common Vulnerability Scoring System (CVSS) from which one can easily get the needed parameters can figure out these four properties quickly. This tool can be used in the area where the security of trusted computers are needed to be precisely quantized.

关键词： Trusted computing Trust chain Model checking probabilistic finite state automaton probabilistic computation tree logic

来源：评论

学校读者我要写书评

暂无评论

probabilistic Model Checking of Incomplete Models 7th

Probabilistic Model Checking of Incomplete Models

引用

7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)

作者： Arora, Shiraj Rao, M. V. Panduranga Indian Inst Technol Hyderabad Andhra Pradesh India

ISBN: (纸本)9783319471662;9783319471655

It is crucial for accurate model checking that the model be a complete and faithful representation of the system. Unfortunately, this is not always possible, mainly because of two reasons: (i) the model is still under development and (ii) the correctness of implementation of some modules is not established. In such circumstances, is it still possible to get correct answers for some model checking queries? This paper is a step towards answering this question. We formulate the problem for the Discrete Time Markov Chains (DTMC) modeling formalism and the probabilistic computation tree logic (PCTL) query language. We then propose a simple solution by modifying DTMC and PCTL to accommodate three valued logic. The technique builds on existing model checking algorithms and tools, obviating the need for new ones to account for three valued logic. Finally, we provide an experimental demonstration of our approach.

关键词： probabilistic models probabilistic model checking three-valued logic Discrete time markov chain probabilistic computation tree logic

来源：评论

学校读者我要写书评

暂无评论

Formal Verification of Vessel Scheduling Using probabilistic Timed Automata 1

引用

20th International Conference on Computing and Information Technology (IC2IT2)

作者： Thianpunyathanakul, Ratchanok Vatanawood, Wiwat Chulalongkorn Univ Fac Engn Dept Comp Engn Bangkok Thailand

ISBN: (数字)9783031585616

ISBN: (纸本)9783031585609;9783031585616

The effective management of time delays in vessel scheduling within the vessel transportation industry poses a complex challenge, as potential delays can lead to shifts in planned routes and increased costs. This paper addresses this issue by proposing a formal probabilistic model for vessel scheduling that considers time constraints and accommodates relevant risk factors contributing to delays. Utilizing probabilistic Timed Automata (PTAs), our model captures distributed random delays from key risk factors such asweather conditions, mechanical engine readiness, and port congestion in the target vessel scheduling. We then translate PTAs model representation of the target vessel scheduling into PRISM code. Subsequently, the PRISM model checker is employed to simulate and verify the vessel scheduling model's compliance with specified behavioral properties expressed in probabilistic computation tree logic (PCTL). This approach facilitates a comprehensive analysis of time-related aspects, aiding in both planning and mitigation of associated risk impacts.

关键词： probabilistic Timed Automata probabilistic computation tree logic Discrete-Time Markov Chain Vessel Scheduling

来源：评论

学校读者我要写书评

暂无评论

Safe Reinforcement Learning for CPSs via Formal Modeling and Verification

Safe Reinforcement Learning for CPSs via Formal Modeling and...

引用

International Joint Conference on Neural Networks (IJCNN)

作者： Yang, Chenchen Liu, Jing Sun, Haiying Sun, Junfeng Chen, Xiang Zhang, Lipeng East China Normal Univ Shanghai Key Lab Trustworthy Comp Shanghai Peoples R China CASCO Signal Ltd R&D Inst Shanghai Peoples R China

ISBN: (纸本)9780738133669

Reinforcement learning (RL) can be defined as the process of learning policies that maximize the expectation of the rewards. It has shown success in solving complex decision-making tasks. However, reinforcement learning-based controllers do not provide guarantees of safety of physical models in Cyber-physical systems (CPSs). In this paper, we propose a framework, which allows implementing RL to the safe control system by transforming formal analysis to learned policy. For satisfaction verification and quantitative analysis, we propose an uncertainty modeling language CSML to describe behaviors of the system, and transform CSML design into networks of probabilistic timed automata (NPTA). For safe learning, we present an algorithm called Safe Control with Formal Methods (SCFM). SCFM constructs a state set that obeys the constraint described by probabilistic computation tree logic (PCTL) via exploring state space before the learning process. The monitor monitors the system, determines whether the chosen action is safe and corrects unsafe decisions. We validate our method through experiments of lane-change control for autonomous cars.

关键词： Reinforcement learning CSML Networks of probabilistic timed automata probabilistic computation tree logic Safe control

来源：评论

学校读者我要写书评

暂无评论

Towards Hierarchical probabilistic CTL Model Checking: Theoretical Foundations 11

Towards Hierarchical Probabilistic CTL Model Checking: Theor...

引用

11th International Conference on Agents and Artificial Intelligence (ICAART)

作者： Kamide, Norihiro Yano, Yuki Teikyo Univ Fac Sci & Engn Dept Informat & Elect Engn Toyosatodai 1-1 Utsunomiya Tochigi 3208551 Japan

ISBN: (纸本)9789897583506

This study proposes a hierarchical probabilistic computation tree logic, HpCTL, which is an extension of the standard probabilistic computation tree logic pCTL, as a theoretical basis for hierarchical probabilistic CTL model checking. Hierarchical probabilistic model checking is a new paradigm that can appropriately verify hierarchical randomized (or stochastic) systems. Furthermore, a probability-measure-independent translation from HpCTL into pCTL is defined, and a theorem for embedding HpCTL into pCTL is proved using this translation. Finally, the relative decidability of HpCTL with respect to pCTL is proved using this embedding theorem. These embedding and relative decidability results allow us to reuse the standard pCTL-based probabilistic model checking algorithms to verify hierarchical randomized systems that can be described using HpCTL.

关键词： computation tree logic probabilistic computation tree logic Hierarchical computation tree logic Embedding Theorem Relative Decidability

来源：评论

学校读者我要写书评

暂无评论

probabilistic Model Checking applied to Autonomous Spacecraft Reconfiguration 3

Probabilistic Model Checking applied to Autonomous Spacecraf...

引用

3rd IEEE International Workshop on Metrology for Aerospace (MetroAeroSpace)

作者： Nardone, Vittoria Santone, Antonella Tipaldi, Massimo Glielmo, Luigi Univ Sannio Dept Engn Benevento Italy Compagnia Generale Spazio I-20151 Milan Italy

ISBN: (纸本)9781467382922

Formal verification techniques are necessary to demonstrate the completeness, the correctness, and the consistency in implementing spacecraft model-based autonomy requirements, where we have to explore the behavior of the system over a large input range. This paper introduces an approach based on probabilistic model checking to verify the specification of spacecraft autonomous reconfiguration functionality, modeled via Markov Decision Process. Some preliminary results show how this approach can be used to check whether the system fulfills suitably-defined properties under a given probability.

关键词： Model Checking probabilistic computation tree logic Spacecraft Autonomy Markov Decision Process

来源：评论

学校读者我要写书评

暂无评论

Mobile Robot Path Planning based on probabilistic Model Checking under Uncertainties

Mobile Robot Path Planning based on Probabilistic Model Chec...

引用

2015 3rd International Conference on Machinery,Materials and Information Technology Applications(ICMMITA 2015)

作者： Wei Lou Chunrui Xia School of Mechanical Engineering and Automation Beihang University Highly Reliable Embedded Systems Lab Capital Normal University

In this paper, a probabilistic model checking method for mobile robots path planning problem is proposed. Since surroundings always affect the behavior of mobile robots, four main environmental factors are analyzed as influencing parameters. With the map built by randomized sampling-based method, we model the uncertain motion behavior as a Markov Decision Process（MDP）. Meanwhile, the properties are described in PCTL（probabilistic computation tree logic） which can be used to describe rich mission specifications. Then the path planning problem is mapped to the problem of generating an MDP control policy that maximizes the probability of accomplishing the mission objective satisfied a PCTL formula. We apply the PRISM platform to analyze model and verify properties. Our approach is demonstrated with illustrative case studies.

关键词： Mobile robot Path planning probabilistic model checking Markov decision process probabilistic computation tree logic

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：