by Pedro Baltazar, Paulo Mateus, Rajagopal Nagarajan, Nikolaos Papanikolaou

Abstract:

We define a logic EpCTL for reasoning about the evolution of probabilistic systems. System states correspond to probability distributions over classical states and the system evolution is modelled by probabilistic Kripke structures that capture both stochastic and non-deterministic transitions. The proposed logic is a temporal enrichment of Exogenous Probabilistic Propositional Logic (EPPL). The model-checking problem for EpCTL is analysed and the logic is compared with PCTL; the semantics of the former is defined in terms of probability distributions over sets of propositional symbols, whereas the latter is designed for reasoning about distributions over paths of possible behaviour. The intended application of the logic is as a specification formalism for properties of communication protocols, and security protocols in particular; to demonstrate this, we specify relevant security properties for a classical contract signing protocol and for the so-called quantum one-time pad.

Reference:

Exogenous Probabilistic Computation Tree Logic (Pedro Baltazar, Paulo Mateus, Rajagopal Nagarajan, Nikolaos Papanikolaou), In Proceedings of the Fifth Workshop on Quantitative Aspects of Programming Languages (QAPL ’07), 2007.

Bibtex Entry:

@INPROCEEDINGS{Baltazar2007, author = {Pedro Baltazar and Paulo Mateus and Rajagopal Nagarajan and Nikolaos Papanikolaou}, title = {Exogenous Probabilistic Computation Tree Logic}, booktitle = {Proceedings of the Fifth Workshop on Quantitative Aspects of Programming Languages (QAPL '07)}, year = {2007}, address = {Braga, Portugal}, month = mar, abstract = {We define a logic EpCTL for reasoning about the evolution of probabilistic systems. System states correspond to probability distributions over classical states and the system evolution is modelled by probabilistic Kripke structures that capture both stochastic and non-deterministic transitions. The proposed logic is a temporal enrichment of Exogenous Probabilistic Propositional Logic (EPPL). The model-checking problem for EpCTL is analysed and the logic is compared with PCTL; the semantics of the former is defined in terms of probability distributions over sets of propositional symbols, whereas the latter is designed for reasoning about distributions over paths of possible behaviour. The intended application of the logic is as a specification formalism for properties of communication protocols, and security protocols in particular; to demonstrate this, we specify relevant security properties for a classical contract signing protocol and for the so-called quantum one-time pad.}, owner = {Nick}, timestamp = {2010.06.20}, url = {../files/qapl2007.pdf} }