dc.contributor.author | Philippou, Anna | en |
dc.contributor.author | Cleaveland, R. | en |
dc.contributor.author | Lee, I. | en |
dc.contributor.author | Smolka, S. | en |
dc.contributor.author | Sokolsky, O. | en |
dc.contributor.editor | Sangiorgi D. | en |
dc.contributor.editor | de Simone R. | en |
dc.creator | Philippou, Anna | en |
dc.creator | Cleaveland, R. | en |
dc.creator | Lee, I. | en |
dc.creator | Smolka, S. | en |
dc.creator | Sokolsky, O. | en |
dc.date.accessioned | 2019-11-13T10:41:59Z | |
dc.date.available | 2019-11-13T10:41:59Z | |
dc.date.issued | 1998 | |
dc.identifier.issn | 0302-9743 | |
dc.identifier.uri | http://gnosis.library.ucy.ac.cy/handle/7/54838 | |
dc.description.abstract | 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. | en |
dc.source | 9th International Conference on Concurrency Theory, CONCUR 1998 | en |
dc.source.uri | https://www.scopus.com/inward/record.uri?eid=2-s2.0-84945974249&partnerID=40&md5=12407495098617a553d7ce4155982e42 | |
dc.subject | Algebra | en |
dc.subject | Real time systems | en |
dc.subject | Specifications | en |
dc.subject | Model checking | en |
dc.subject | Interactive computer systems | en |
dc.subject | Probability of failure | en |
dc.subject | Probabilistic analysis | en |
dc.subject | Hennessy-Milner Logics | en |
dc.subject | Model checking algorithm | en |
dc.subject | Probabilistic constraints | en |
dc.subject | Probabilistic extension | en |
dc.subject | Probabilistic variant | en |
dc.subject | Real-time process algebra | en |
dc.title | Probabilistic resource failure in real-time process algebra | en |
dc.type | info:eu-repo/semantics/article | |
dc.description.volume | 1466 | |
dc.description.startingpage | 389 | |
dc.description.endingpage | 404 | |
dc.author.faculty | 002 Σχολή Θετικών και Εφαρμοσμένων Επιστημών / Faculty of Pure and Applied Sciences | |
dc.author.department | Τμήμα Πληροφορικής / Department of Computer Science | |
dc.type.uhtype | Article | en |
dc.description.notes | <p>Sponsors: | en |
dc.description.notes | Conference code: 143949 | en |
dc.description.notes | Cited By :10</p> | en |
dc.source.abbreviation | Lect. Notes Comput. Sci. | en |