ProNoBiS Final Plenary Meeting

LIX (École Polytechnique), Palaiseau, France.
Friday, December 7 2007, 10h-17h.

To come to LIX, please follow the instructions. See also the campus map.

Program:

• 09.45-10.00: Coffee Break
  
  
• 10.00-10.30: Jean and Catuscia will give a brief report.
  
  
• 10.30-11.00: Jean Goubault-Larrecq: Hemi-Metrics, and How Far Two Games Are
  
  Bisimulations are a good way of comparing two stochastic games, but only give a Boolean piece of information. Panangaden and others have defined a notion of metric between Markov Decision Processes (aka., 1 1/2 player games) that has the nice property that it gives a way of bounding the difference between payoff functions on the two MDPs, and that being at distance 0 characterizes (strong) bisimulation. I claimed in my ICALP paper this year that ludic transition systems gave a way of modeling 2 1/2 player games as easily as 1 1/2 player games. I'll illustrate this on hemi-metrics (a non-symmetric version of metrics), showing some topological properties of the Hutchinson hemi-metric. I'll show two variants of the Kantorovich-Rubinstein theorem in this setting. Eventually, I'll try to convince you that this approach specializes, in the discrete case, to an approach recently developed by de Alfaro et al. (ICALP'07 again).
  
  
• 11.00-11.30: Najla Chamseddine: Probabilistic Timed Automata with Constrained Time-outs
  
  We argue that many probabilistic protocols, in order to behave correctly, assume constraints on their time-out values. Under such constraints, the system, modelled as a timed automaton, behaves in a fully probabilistic manner: at any time, the system can only let the time pass or execute at most one action. For such models, that we called "determinate probabilistic timed automata", we are able to compute the expected time to go from one state to another with timeouts as parameters. We examplify the method on models of CSMA-CD and BRP protocols.
  
  
• 11.30-12.00: Catuscia Palamidessi: Formal approaches to Information-hiding - An overview
  
  We give an overview of various formal approaches from literature to information-hiding: The possibilistic approaches, the probabilistic approaches, the information-theoretic approaches, and the one based on statistical inference. We compare the various frameworks and point out the relations. Finally, we show how to specify information-hiding protocols and verify them (in the various approaches) using language-based techniques.
  
  
• 12.00-12.30: Vincent Danos: Stochastic Graph Rewriting
  
  
• 12.30-14.00: Lunch
  
  
• 14.00-14.30: Kostas Chatzikokolakis: A monotonicity principle for capacity
  
  The notion of capacity has be proven useful in many areas outside classical information theory, one important example being security. Even though its definition is natural, there is no analytical formula that gives the capacity in the general case and even when one is available (for example, in the case of binary channels) it is too complicated to be used even for simple tasks, like comparing the capacity of two channels. In this talk we present a monotonicity principle for capacity, based on its convexity as a function of the channel matrix. We then use this principle to show a number of results for binary channels. First we develop a new partial order for algebraic information theory with respect to which capacity is monotone. This order is much bigger than the interval inclusion order and can be characterized in three different ways: with a simple formula, geometrically and algebraically. Then we establish bounds on the capacity based on easily computable functions. We also study its behavior along lines of constant capacity leading to graphical methods for reasoning about capacity that allow us to compare channels in "most" cases.
  
  
• 14.30-15.00: Pasquale Malacaria: Measuring insecurity of Programs
  
  
• 15.00-15.30: Coffee Breack
  
  
• 15.30-16.00: Angelo Troina: A Probabilistic Applied Pi-Calculus
  
  We propose an extension of the Applied Pi-calculus by introducing nondeterministic and probabilistic choice operators. Notions of static and observational equivalence are given for the enriched calculus. In order to model the possible interaction of a process with its surrounding environment a labeled semantics is given together with a notion of weak bisimulation which is shown to coincide with the observational equivalence. We prove that results in the probabilistic framework are preserved in a purely nondeterministic setting. As an application we study the OT-1-out-of-2 protocol.
  
  
• 16.00-16.30: Peng Wu: Symbolic Bisimulations and Model Checking for Probabilistic pi-Calculus
  
  The talk will briefly introduce our recent work on probabilistic pi-calculus, a process algebra which supports modelling of concurrency, mobility and discrete probabilistic behaviour. At first, symbolic bisimulations are presented to overcome the infinite branching problem that still exists in checking ground bisimulations between probabilistic systems. Especially the definition of weak (symbolic) bisimulation does not rely on the random capability of adversaries and suggests a solution to the open problem on the axiomatization for weak bisimulation in the case of unguarded recursion. Furthermore, we present an efficient characterization of symbolic bisimulations for the calculus, which allows the "on-the-fly" instantiation of bound names and dynamic construction of equivalence relations for quantitative evaluation. This directly results in a local decision algorithm that can explore just the minimal portion of state spaces of probabilistic processes.
  Then we present an implementation of model checking for the calculus. Formal verification techniques for this calculus have clear applications in several domains, including mobile ad-hoc network protocols and random security protocols. Despite this, no implementation of automated verification exists. Building upon the (non-probabilistic) pi-calculus model checker MMC, we first show an automated procedure for constructing the Markov decision process representing a probabilistic pi-calculus process. This can then be verified using existing probabilistic model checkers such as PRISM. Secondly, we demonstrate how for a large class of systems a more efficient, compositional approach can be applied, which uses our extension of MMC on each parallel component of the system and then translates the results into a high-level model description for the PRISM tool. The feasibility of our techniques is demonstrated through three case studies from the pi-calculus literature.
  
  
• 16.30-17.00: Discussions.