Probabilistic resource failure in real-time process algebra
Date
1998Author
Philippou, AnnaCleaveland, R.
Lee, I.
Smolka, S.
Sokolsky, O.
ISSN
0302-9743Source
9th International Conference on Concurrency Theory, CONCUR 1998Volume
1466Pages
389-404Google Scholar check
Keyword(s):
Metadata
Show full item recordAbstract
PACSR, a probabilistic extension of the real-time process algebra ACSR, is presented. The extension is built upon a novel treatment of the notion of a resource. In ACSR, resources are used to model contention in accessing physical devices. Here, resources are invested with the ability to fail and are associated with a probability of failure. The resulting formalism allows one to perform probabilistic analysis of real-time system specifications in the presence of resource failures. A probabilistic variant of Hennessy-Milner logic with until is presented. The logic features an until operator which is parameterized by both a probabilistic constraint and a regular expression over observable actions. This style of parameterization allows the application of probabilistic constraints to complex execution fragments. A model-checking algorithm for the proposed logic is also given. Finally, PACSR and the logic are illustrated with a telecommunications example. © 1998, Springer Verlag. All rights reserved.
Collections
Cite as
Related items
Showing items related by title, author, creator and subject.
-
Report
The Probabilistic Thinking of Primary School Pupils in Cyprus: The Case of Tree Diagrams
Lamprianou, Iasonas; Lamprianou, Thekla Afantiti (International Group for the Psychology of Mathematics Education, 2003)
-
Article
Optimizing the Detection Performance of Smart Camera Networks Through a Probabilistic Image-Based Model
Kyrkou, Christos; Christoforou, Eftychios G.; Timotheou, Stelios; Theocharides, Theocharis; Panayiotou, Christos; Polycarpou, Marios (2018)Networks of smart cameras, equipped with on-board processing and communication infrastructure, are increasingly being deployed in a variety of different application fields, such as security and surveillance, traffic ...
-
Conference Object
Verification of AA-Diagnosability in Probabilistic Finite Automata is PSPACE-Hard
Keroglou, Christoforos; Hadjicostis, Christoforos N. (2019)In this paper we consider the complexity of verifying the property of AA-diagnosability in probabilistic finite automata and establish that AA-diagnosability is, in general, a PSPACE-hard problem. In deterministic and ...