On the verification of qualitative properties of probabilistic processes under fairness constraints

doi:10.1016/S0020-0190(98)00038-6

Information Processing Letters

Volume 66, Issue 2, 29 April 1998, Pages 71-79

https://doi.org/10.1016/S0020-0190(98)00038-6 Get rights and content

Abstract

We consider sequential and concurrent probabilistic processes and propose a general notion of fairness with respect to probabilistic choice, which allows to express various notions of fairness such as process fairness and event fairness. We show the soundness of proving the validity of qualitative properties of probabilistic processes under fairness constraints in the sense that whenever all fair executions of a probabilistic process fulfill a certain linear time property E then E holds for almost all executions (i.e., E holds with probability 1). It follows that in order to verify probabilistic processes with respect to linear time specifications, it suffices to establish that—for some instance of our general notion of fairness—all fair executions satisfy the specification. This generalizes the soundness results for extreme and α-fairness established by Pnueli in 1983 and 1993, respectively. Furthermore, we show that the α-fairness of Pnueli (1993) is the only fairness notion which is complete for validity of qualitative linear time properties.

References (32)

R. van Glabbeek et al.
Reactive, generative, and stratified models for probabilistic processes
Inform. and Comput.
(1995)
M. Kwiatkowska
Survey of fairness notions
Inform. and Software Technol.
(1989)
K. Larsen et al.
Bisimulation through probabilistic testing
Inform. and Comput.
(1991)
D. Lehmann et al.
Reasoning with time and chance
Inform. and Control
(1982)
A. Pnueli et al.
Probabilistic verification
Inform. and Comput.
(1993)
W. Yi et al.
Testing probabilistic and nondeterministic processes
R. Alur et al.
Model-checking for probabilistic real-time systems
L. de Alfaro
Formal verification of performance and reliability of real-time systems
C. Baier, M.Z. Kwiatkowska, Model checking for a probabilistic branching time logic with fairness, Distrib. Comput., to...
C. Baier et al.
Domain equations for probabilistic processes

A. Bianco et al.

Model checking of probabilistic and nondeterministic systems

L. Christoff et al.

Reasoning about safety and liveness properties for probabilistic processes

C. Courcoubetis et al.

Verifying temporal properties of finite-state probabilistic programs

N. Francez

Fairness

(1988)

A. Giacalone et al.

Algebraic reasoning for probabilistic concurrent systems

R. van Glabbeek et al.

Reactive, generative, and stratified models for probabilistic processes

Cited by (34)

When are stochastic transition systems tameable?
2018, Journal of Logical and Algebraic Methods in Programming
A decade ago, Abdulla, Ben Henda and Mayr introduced the elegant concept of decisiveness for denumerable Markov chains [1]. Roughly speaking, decisiveness allows one to lift most good properties from finite Markov chains to denumerable ones, and therefore to adapt existing verification algorithms to infinite-state models. Decisive Markov chains however do not encompass stochastic real-time systems, and general stochastic transition systems (STSs for short) are needed. In this article, we provide a framework to perform both the qualitative and the quantitative analysis of STSs. First, we define various notions of decisiveness (inherited from [1]), notions of fairness and of attractors for STSs, and make explicit the relationships between them. Then, we define a notion of abstraction, together with natural concepts of soundness and completeness, and we give general transfer properties, which will be central to several verification algorithms on STSs. We further design a generic construction which will be useful for the analysis of ω-regular properties, when a finite attractor exists, either in the system (if it is denumerable), or in a sound denumerable abstraction of the system. We next provide algorithms for qualitative model-checking, and generic approximation procedures for quantitative model-checking. Finally, we instantiate our framework with stochastic timed automata (STA), generalized semi-Markov processes (GSMPs) and stochastic time Petri nets (STPNs), three models combining dense-time and probabilities. This allows us to derive decidability and approximability results for the verification of these models. Some of these results were known from the literature, but our generic approach permits to view them in a unified framework, and to obtain them with less effort. We also derive interesting new approximability results for STA, GSMPs and STPNs.
On fairness and randomness
2009, Information and Computation
We investigate the relation between the behavior of non-deterministic systems under fairness constraints, and the behavior of probabilistic systems. To this end, first a framework based on computable stopping strategies is developed that provides a common foundation for describing both fair and probabilistic behavior. On the basis of stopping strategies it is then shown that fair behavior corresponds in a precise sense to random behavior in the sense of Martin-Löf’s definition of randomness.
We view probabilistic systems as concrete implementations of more abstract non-deterministic systems. Under this perspective the question is investigated what probabilistic properties are needed in such an implementation to guarantee (with probability one) certain required fairness properties in the behavior of the probabilistic system. Generalizing earlier concepts of $ε$ -bounded transition probabilities, we introduce the notion of divergent probabilistic systems, which enables an exact characterization of the fairness properties of a probabilistic implementation. Looking beyond pure fairness properties, we also investigate what other qualitative system properties are guaranteed by probabilistic implementations of fair non-deterministic behavior. This leads to a completeness result which generalizes a well-known theorem by Pnueli and Zuck.
Assisting the design of a groupware system
2009, Journal of Logic and Algebraic Programming
Product Data Management (PDM) systems support the product/document management of design processes such as those typically used in the manufacturing industry. They allow enterprises to capture, organise, automate and share engineering information in an efficient way. The efficient handling of queries on product information and the uploading and downloading of families of related files for modification by designers are essential aspects of such systems. The efficiency of the system as perceived by its clients depends on its correct functioning, but also for a significant part on its performance aspects. In this article, we apply both qualitative and stochastic model-checking techniques to evaluate various usability and performance aspects of the thinkteam PDM system, and of several proposed extensions, thereby assisting the design phase of an industrial groupware system.
Categorical foundations for randomly timed automata
2003, Theoretical Computer Science
The general theory of randomly timed automata is developed: starting with the practical motivation and presentation of the envisaged notion, the categorical theory of minimization, aggregation, encapsulation, interconnection and realization of such automata is worked out. All these constructions are presented universally: minimization and realization as adjunctions, aggregation as product, interconnection as cartesian lifting, and encapsulation as co-cartesian lifting. Stochastic timed automata are shown to be a particular case of randomly timed automata. The notion of stochastic timed automaton is shown to be too restrictive to establish a self contained theory of combination and realization.
Stochastic Best-Effort Strategies for Borel Goals
2023, Proceedings - Symposium on Logic in Computer Science
Beyond Strong-Cyclic: Doing Your Best in Stochastic Environments
2022, IJCAI International Joint Conference on Artificial Intelligence

View all citing articles on Scopus

^☆: Supported in part by EPSRC grant GR/K42028.

View full text

On the verification of qualitative properties of probabilistic processes under fairness constraints☆

Abstract

Inform. and Comput.

Inform. and Software Technol.

Inform. and Comput.

Inform. and Control

Inform. and Comput.

Model-checking for probabilistic real-time systems

Formal verification of performance and reliability of real-time systems

Domain equations for probabilistic processes

Model checking of probabilistic and nondeterministic systems

Reasoning about safety and liveness properties for probabilistic processes

Verifying temporal properties of finite-state probabilistic programs

Fairness

Algebraic reasoning for probabilistic concurrent systems

Reactive, generative, and stratified models for probabilistic processes