
ComèteParsifal Seminar (Abstracts 2012) 

Calendar
2012
2011
2010
2009
2008
2007
2006 2005 2004
Abstracts
Thu Dec 06, 10:30
Speaker: Tri Minh Ngo
Title: Quantitative Analysis for Multithreaded 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 informationtheoretic 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 multithreaded programs. Reasoning about the exposed information flow of multithreaded 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 informationtheoretic approaches have been also shown to be counterintuitive.
This paper proposes a novel model of quantitative analysis for multithreaded 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 multithreaded 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 fixpoint 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 NPcomplete for some restricted systems.
Nevertheless, we also introduced some techniques for overestimation of
worstcase 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 gleakage, a rich generalization of the
minentropy model of quantitative information flow. In gleakage, 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 gleakage, including bounds between
mincapacity, gcapacity, 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 nondeterminism

Thu May 10, 15:00
Speaker: Matteo Mio
Title: Probabilistic modal mucalculus 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 nondeterministic 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 PSPACEcomplete), experimental results show improvements of several orders of magnitude over the standard algorithm.

Page maintainer:
Andres Aristizabal
