Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> Probabilistic Temporal Logics <s> In this paper the branching time logic pCTL* is defined. pCTL* expresses quantitative bounds on the probabilities of correct behavior; it can be interpreted over discrete Markov processes. A bisimulation relation is defined on finite Markov processes, and shown to be sound and complete with respect to pCTL*. We extend the universe of models to generalized Markov processes in order to support notions of refinement, abstraction, and parametrization. Model checking pCTL* over generalized Markov processes is shown to be elementary by a reduction to RCF. We conclude by describing practical and theoretical avenues for further work. <s> BIB001 </s> Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> Probabilistic Temporal Logics <s> The temporal logics pCTL and pCTL* have been proposed as tools for the formal specification and verification of probabilistic systems: as they can express quantitative bounds on the probability of system evolutions, they can be used to specify system properties such as reliability and performance. In this paper, we present model-checking algorithms for extensions of pCTL and pCTL* to systems in which the probabilistic behavior coexists with nondeterminism, and show that these algorithms have polynomial-time complexity in the size of the system. This provides a practical tool for reasoning on the reliability and performance of parallel systems. <s> BIB002 </s> Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> Probabilistic Temporal Logics <s> We consider concurrent probabilistic systems, based on probabilistic automata of Segala & Lynch [55], which allow non-deterministic choice between probability distributions. These systems can be decomposed into a collection of "computation trees" which arise by resolving the non-deterministic, but not probabilistic, choices. The presence of non-determinism means that certain liveness properties cannot be established unless fairness is assumed. We introduce a probabilistic branching time logic PBTL, based on the logic TPCTL of Hansson [30] and the logic PCTL of [55], resp. pCTL of [14]. The formulas of the logic express properties such as "every request is eventually granted with probability at least p". We give three interpretations for PBTL on concurrent probabilistic processes: the first is standard, while in the remaining two interpretations the branching time quantifiers are taken to range over a certain kind of fair computation trees. We then present a model checking algorithm for verifying whether a concurrent probabilistic process satisfies a PBTL formula assuming fairness constraints. We also propose adaptations of existing model checking algorithms for pCTL* [4, 14] to obtain procedures for PBTL* under fairness constraints. The techniques developed in this paper have applications in automatic verification of randomized distributed systems. <s> BIB003 </s> Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> Probabilistic Temporal Logics <s> We present a logic for stating properties such as, "after a request for service there is at least a 98\045 probability that the service will be carried out within 2 seconds". The logic extends the temporal logic CTL by Emerson, Clarke and Sistla with time and probabil- ities. Formulas are interpreted over discrete time Markov chains. We give algorithms for checking that a given Markov chain satis- fies a formula in the logic. The algorithms require a polynomial number of arithmetic operations, in size of both the formula and\003This research report is a revised and extended version of a paper that has appeared under the title "A Framework for Reasoning about Time and Reliability" in the Proceeding of the 10thIEEE Real-time Systems Symposium, Santa Monica CA, December 1989. This work was partially supported by the Swedish Board for Technical Development (STU) as part of Esprit BRA Project SPEC, and by the Swedish Telecommunication Administration.1the Markov chain. A simple example is included to illustrate the algorithms. <s> BIB004 </s> Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> Probabilistic Temporal Logics <s> We introduce a propositional logic whose formulas are built using the language of CTL*, enriched by two types of probability operators: one speaking about probabilities on branches, and one speaking about probabilities of sets of branches with the same initial state. An infinitary axiomatization for the logic, which is shown to be sound and strongly complete with respect to the corresponding class of models, is proposed. <s> BIB005 </s> Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> Probabilistic Temporal Logics <s> This paper describes a major new release of the PRISMprobabilistic model checker, adding, in particular, quantitative verification of (priced) probabilistic timed automata. These model systems exhibiting probabilistic, nondeterministic and real-time characteristics. In many application domains, all three aspects are essential; this includes, for example, embedded controllers in automotive or avionic systems, wireless communication protocols such as Bluetooth or Zigbee, and randomised security protocols. PRISM, which is open-source, also contains several new components that are of independent use. These include: an extensible toolkit for building, verifying and refining abstractions of probabilistic models; an explicit-state probabilistic model checking library; a discrete-event simulation engine for statistical model checking; support for generation of optimal adversaries/strategies; and a benchmark suite. <s> BIB006 </s> Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> Probabilistic Temporal Logics <s> The aim of the paper is to present a sound, strongly complete and decidable probabilistic temporal logic that can model reasoning about evidence. The formal system developed here is actually a solution of a problem proposed by Halpern and Pucella (J Artif Intell Res 26:1---34, 2006). <s> BIB007 </s> Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> Probabilistic Temporal Logics <s> The model-checking approach was originally formulated for verifying qualitative properties of systems, for example safety and liveness (see Chap. 2), and subsequently extended to also handle quantitative features, such as real time (see Chap. 29), continuous flows (see Chap. 30), as well as stochastic phenomena, where system evolution is governed by a given probability distribution. Probabilistic model checking aims to establish the correctness of probabilistic system models against quantitative probabilistic specifications, such as those capable of expressing, for example, the probability of an unsafe event occurring, expected time to termination, or expected power consumption in the start-up phase. In this chapter, we present the foundations of probabilistic model checking, focusing on finite-state Markov decision processes as models and quantitative properties expressed in probabilistic temporal logic. Markov decision processes can be thought of as a probabilistic variant of labelled transition systems in the following sense: transitions are labelled with actions, which can be chosen nondeterministically, and successor states for the chosen action are specified by means of discrete probabilistic distributions, thus specifying the probability of transiting to each successor state. To reason about expectations, we additionally annotate Markov decision processes with quantitative costs, which are incurred upon taking the selected action from a given state. Quantitative properties are expressed as formulas of the probabilistic computation tree logic (PCTL) or using linear temporal logic (LTL). We summarise the main model-checking algorithms for both PCTL and LTL, and illustrate their working through examples. The chapter ends with a brief overview of extensions to more expressive models and temporal logics, existing probabilistic model-checking tool support, and main application domains. <s> BIB008
In comparison with the standard non-probabilistic temporal logics CTL * , CTL, and LTL, probabilistic temporal logics can be effectively used in randomized and stochastic situations. Thus, many studies regarding probabilistic temporal logics and their applications, including probabilistic model checking, have been performed as discussed below. More information can be found in  BIB004 BIB001 BIB002 BIB003 BIB005 BIB006 BIB007  BIB008 . Probabilistic full computation tree logic (pCTL * ) and its subsystem, probabilistic computation tree logic (pCTL), have been investigated by BIB001 and BIB002 . The logics pCTL * and pCTL are obtained from CTL * and CTL, respectively, by adding the probabilistic or probability operator, P ≥x . Formulas with the form P ≥x α can be interpreted as follows: the probability that α holds in the future evolution of the system is at least x. In (Bianco and de Alfaro, 1995), pCTL * and pCTL are introduced to verify the reliability and performance of systems modeled by discrete Markov chains. These logics can appropriately express the quantitative bounds on the probability of system evolutions. The complexities of model checking algorithms with respect to the logics are clarified in BIB002 . In BIB001 , model-checking algorithms for various extensions of the previous settings of the logics are proposed to verify the probabilistic non-deterministic concurrent systems in which probabilistic behavior coexists with non-determinism. Further, these algorithms are shown to exhibit polynomial-time complexity depending on the sizes of the systems. The main difference between the pCTL * settings by Aziz et al. BIB001 and those by Bianco and de Alfaro (Bianco and de Alfaro, 1995) is the probability measure settings in the probabilistic Kripke structure of pCTL * . In BIB004 , PCTL, a probabilistic and real-time extension of CTL, is investigated based on an interpretation of discrete time Markov chains. In contrast to the probabilistic frameworks of pCTL and pCTL * , the notion of probability in PCTL is assigned to all of its temporal operators. For example, a PCTL formula with the form G ≤t ≥p α implies that α holds continuously for t time units with a probability of at least p. In  , a timed probabilistic concurrent computation tree logic (TPCTL) is introduced and investigated. In BIB003 , probabilistic branching time logics (PBTL and PBTL * ) are introduced based on the probabilistic temporal logics TPCTL, PCTL, pCTL, and pCTL * , and model-checking algorithms based on PBTL and PBTL * are proposed to automatically verify randomized distributed systems. In BIB005 , a propositional discrete probabilistic branching temporal logic (pBTL) is developed by extending CTL * . There are two types of novel probability operators in pBTL: P p ≥r and P s ≥r , where P p ≥r α implies that the probability that α holds on a randomly chosen branch is at least γ, and P s ≥r α means that the probability that α holds on a particular branch is at least γ. In BIB007 , a propositional probabilistic logic with discrete linear time is developed to handle the clinical reasoning with respect to evidence. More recent developments in probabilistic model checking based on probabilistic temporal logics are reported in BIB008 .