Invited Talks at PAuL 2007

Antonin Kucera
Masaryk University, Czech Republic

Title:        "PCTL formulae as a winning objective in stochastic games"
Abstract:  The talk presents an overview of recent results about finite-state stochastic games where the winning objectives are specified by formulae of branching-time 
                logics such as PCTL (the goal of Player1/Player2 to is to satisfy/falsify a given formula). The properties of these games are quite different from the properties
                of stochastic games with linear-time winning objectives (Buchi, Rabin, Street, etc.). In particular, these games are not determined, winning strategies may
                require infinite memory, and the existence of a winning strategy for a general PCTL formula is highly undecidable even for Markov decision processes (i.e.,
                for the subclass of stochastic games where Player 2 does not control any nodes). All results will be explained as informally as possible and illustrated on


Catuscia Palamidessi
LIX, Ecole Polytechnique, France

Title:       "Information-hiding protocols as opaque channels"
Abstract:  I will make a brief introduction to the problem of information-hiding, and present some (randomized) protocols designed to provide this property.
               Then I will introduce an information-theoretic framework in which these protocols are interpreted as channels, and I will discuss various quantitative
               definitions of their degree of opacity, showing the relation with probabilistic definitions of information-hiding in literature. Further, I will show how
               the channel matrix associated to such a protocol can be used by an adversary to try to infer the secret information from the observables, using Bayesian
               inference, and I will discuss how the probability of error (Bayesian risk) depends on the matrix. Finally, I will show some examples of protocol specifications
               using a probabilistic process calculus, and discuss how to compute the matrix associated to the protocol using model checking techniques. This talk is based
               on joint work with Kostas Chatzikokolakis and Prakash Panangaden.