Parametric probabilistic transition systems for system design and analysis

Abstract. We develop a model of Parametric Probabilistic Transition Systems, where probabilities associated with transitions may be parameters. We show how to find instances of the parameters that satisfy a given property and instances that either maximize or minimize the probability of reaching a certain state. As an application, we model a probabilistic non–repudiation protocol with a Parametric Probabilistic Transition System. The theory we develop allows us to find instances that maximize the probability that the protocol ends in a fair state (no participant has an advantage over the others).

• Type: Journal
• Year: 2007
• Where: FAC
• Authors: Ruggero Lanotte, Andrea Maggiolo-Schettini, Angelo Troina
• Keywords: FAC 2007, Parametric Probabilistic Transition, Probabilistic Non–repudiation Protocol, Probabilistic Transition System