Exogenous Probabilistic Computation Tree Logic

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}
}