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 pape...
详细信息
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.
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 learni...
详细信息
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.
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 CT...
详细信息
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.
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...
详细信息
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.
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...
详细信息
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.
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 ve...
详细信息
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.
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...
详细信息
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.
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 i...
详细信息
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.
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 le...
详细信息
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.
暂无评论