 |
|
|
|
| Comète-Parsifal Seminar (Abstracts 2012) |
|
Calendar
2012 2011 2010 2009 2008 2007 2006 2005 2004| 2012 | ||
Thu Dec 06, 10:30 | Tri Minh Ngo | Quantitative Analysis for Multi-threaded Programs |
| Fri Oct 19, 14:30 | Fabio Gadducci | A Quantified Modal Logic for Systems with Dynamic Structure |
| Thu Jul 12, 15:00 | Sergio Giro | Verification of distributed probabilistic systems under partial information |
| Thu Jun 21, 15:00 | Kostas Chatzikokolakis | Measuring Information Leakage using Generalized Gain Functions |
| Thu Jun 07, 15:00 | Andrei Dorman | Interaction solos |
| Thu May 10, 15:00 | Matteo Mio | Probabilistic modal mu-calculus with independent product |
| Tue Jan 17, 14:30 | Filippo Bonchi | Checking NFA equivalence with bisimulations up to congruence |
Abstracts
Thu Dec 06, 10:30 Speaker: Tri Minh Ngo Title: Quantitative Analysis for Multi-threaded Programs Abstract: Quantitative theories of information flow gives us an approach to relax the absolute confidentiality properties that are difficult to satisfy for many practical applications. The classical information-theoretic approaches for sequential programs, where the program is modeled as a communication channel with only input and output, and the measure of leakage is based on the notions of initial and remaining uncertainty, are not suitable to multi-threaded programs. Reasoning about the exposed information flow of multi-threaded programs is more complicated, because the outcome of such programs depends on the scheduler policy, and the leakages in intermediate states also contribute to the overall leakage of the program. Besides, the information-theoretic approaches have been also shown to be counter-intuitive. This paper proposes a novel model of quantitative analysis for multi-threaded programs that also takes into account the effect of observables of intermediate states along the trace. We define the notion of the leakage of a program trace. Given the fact that the execution of a multi-threaded programs typically is described by a set of traces, the leakage of a program under a specific scheduler is computed as the expected value of the leakages of all possible traces. This model is also applicable to sequential programs. Examples are given to compare our approach with the existing approaches. |
Fri Oct 19, 14:30 Speaker: Fabio Gadducci Title: A Quantified Modal Logic for Systems with Dynamic Structure Abstract: Quantified μ-calculi combine the fix-point and modal operators of temporal logics with (existential and universal) quantifiers, and they allow for reasoning about the possible behavior of individual components within a software system. In this talk a novel approach to the semantics of such calculi is proposed, namely, labeled transition systems whose states are algebras and transitions are partial homomorphisms. Most importantly, formulae are interpreted over sets of state assignments (families of partial substitutions, associating formula variables to state components). Our proposal allows us to model and reason about the creation and deletion of components, as well as the merging of components, and it avoids the limitations of existing approaches, usually enforcing restrictions of the transition relation. The talk is rounded up with some considerations about model checking and approximation techniques. |
Thu Jul 12, 15:00 Speaker: Sergio Giro Title: Verification of distributed probabilistic systems under partial information Abstract: In the verification of systems that involve probabilities, it is crucial to study qualitative properties concerning the probability of certain events as, for instance, 'the probability that a failure occurs is less that 0.01'. In case the system under consideration is distributed, each of the components of the system might have a partial view of the information available to other components. The analysis of these systems is carried out by considering 'distributed adversaries' with restricted observations. In this talk I will summarise six years of research on automatic verification of distributed probabilistic systems. On the negative side, we proved the verification problem to be undecidable in general and NP-complete for some restricted systems. Nevertheless, we also introduced some techniques for overestimation of worst-case probabilities, and showed that the concept of distributed adversaries can be used to improve existing techniques such as partial order reduction. |
Thu Jun 21, 15:00 Speaker: Kostas Chatzikokolakis Title: Measuring Information Leakage using Generalized Gain Functions Abstract: This talk introduces g-leakage, a rich generalization of the min-entropy model of quantitative information flow. In g-leakage, the benefit that an adversary derives from a certain guess about a secret is specified using a gain function g. Gain functions allow a wide variety of operational scenarios to be modeled, including those where the adversary benefits from guessing a value close to the secret, guessing a part of the secret, guessing a property of the secret, or guessing the secret within some number of tries. I will discuss important properties of g-leakage, including bounds between min-capacity, g-capacity, and Shannon capacity. Moreover I will discuss a connection between a strong leakage ordering on two channels, C1 and C2, and the possibility of factoring C1 into C_2C_3, for some C3. Based on this connection, I will propose a generalization of the Lattice of Information from deterministic to probabilistic channels |
Thu Jun 07, 15:00 Speaker: Andrei Dorman Title: Interaction solos Abstract: We build a language of processes corresponding exactly to the most general Interaction Nets in which cells 'are' solos. We then introduce several styles of subcalculi we call designs, out of which, a rather unusual one and show it is as expressive as the whole system: names are shared by at most two processes. In other words, channels only connects two processes (a bit like a physical wire can only connect two machines). Conversely, translating such a system into the other designs, when possible, introduces divergence.
This first results leads us to a possible classification of complexity of non-determinism
|
Thu May 10, 15:00 Speaker: Matteo Mio Title: Probabilistic modal mu-calculus with independent product Abstract: The modal µ-calculus (Lµ) is the logic obtained by extending standard propositional modal logic with least and greatest fixed points operators. This logic was intensively studied in the last 20 years, as it allows the expression of many interesting properties of labeled transition systems.
The probabilistic modal µ-calculus (pLµ) is a generalization of Lµ,
designed for expressing properties of probabilistic labeled transition
systems. In this talk I will discuss an extension of pLµ, called probabilistic
modal µ-calculus with independent product, which can express more
complex properties of practical interest. We provide two semantics for
this extended logic: one denotational and one based on a new kind of
games which we call Tree games. The main result is the equivalence of
the two semantics. The proof is carried out in ZFC set theory extended
with Martin’s Axiom at the first uncountable cardinal.
|
Tue Jan 17, 14:30 Speaker: Filippo Bonchi Title: Checking NFA equivalence with bisimulations up to congruence Abstract: We introduce bisimulation up to congruence as a technique for proving language equivalence of non-deterministic finite automata. Exploiting this technique we devise an optimization of the classical algorithm by Hopcroft and Karp that, instead of computing the whole determinized automata, explores only a small portion of it. Although the optimized algorithm remains exponential in worst case (the problem is PSPACE-complete), experimental results show improvements of several orders of magnitude over the standard algorithm. |
Page maintainer: Andres Aristizabal