 |
|
|
|
| Comète-Parsifal Seminar (Abstracts 2007) |
|
Calendar
2012 2011 2010 2009 2008 2007 2006 2005 2004Abstracts
HR> Nov 20 2007, 14:00Speaker: Simon Kramer
Title: Towards Interactive Belief, Knowledge, and Provability: Possible Application to Zero-Knowledge Proofs
Abstract:
We argue that modal operators of interactive belief, knowledge, and provability are definable as natural generalisations of their non-interactive counterparts, and that zero-knowledge proofs (from cryptography) have a natural (modal) formulation in terms of interactive individual knowledge, non-interactive propositional knowledge and interactive provability.
Our work is motivated by van Benthem's investigation
into rational agency and dialogue and our attempt to
redefine modern cryptography in terms of modal logic.
Nov 15 2007, 14:00
Speaker: Antonino Salibra
Title: Algebra and topology in lambda calculus
Abstract:
In this seminar we show how algebra and topology can be fruitfully applied to the operational semantics and to the model theory of the untyped lambda calculus. It will be also analyzed one of the long-standing open problem of lambda calculus, regarding the existence of a topological model of the beta-eta lambda theory, where all Scott-continuous functions are representable.
Oct 29 2007, 14:00
Speaker: Michael Mislove
Title: Probabilistic Input/Output Automata From a Domain-theoretic Perspective
Abstract:
Probabilistic Input/Output Automata (PIOAs) are probabilistic systems that were initially devised by Roberto Segala and have been used as model in a variety of computational settings. Most recently, a variant called Task PIOAs have been used to model crypto-protocols in a way that allows for a finer analysis of lower level mechanisms that underlie modern cryptography. In particular, the approach supports allows the power of the adversary to be restricted while also supporting reasoning about probabilistic polynomial time computations and simulations that are negligible with respect to a meaningful metric. In this talk, I'll describe a domain-theoretic approach to PIOAs that allows a simple derivation of some of the key mathematical results about their structure.
This is joint work with Aaron Jaggard (DIMACS) and Catherine Meadows (NRL).
Oct 16 2007, 14:00
Speaker: Andrea Turrini
Title: Security Protocol Verification with Probabilistic Automata
Abstract:
We study simulation relations for Probabilistic Automata that require transitions to be matched up to negligible sets provided that computation lengths are polynomially bounded. These relations are meant to provide rigorous grounds to parts of correctness proofs for cryptographic protocols that are usually carried out by semi-formal arguments. We illustrate our ideas by recasting a correctness proof of Bellare and Rogaway based on the notion of matching conversation.
Paper available here
Oct 11 2007, 14:00
Speaker: Nicolas Guenot
Title: Multi-Focusing in Deep Inference
Abstract:
The calculus of structures has interesting properties of symmetry, due to its deep inference feature, which allows to work inside a formula without destroying the toplevel connectives. In this talk, we will discuss the problem of defining formally what "focusing" could be, and how this generic idea can be translated into the calculus of structures. We will then describe a focused system for MALL in CoS which naturally comes with the multi-focusing extension, where several formulas could live under a focusing arrow at the same time (under the same arrow in the sequent calculus, under several arrows in CoS). This system is quite simple, has two symmetric reaction rules unlike Andreoli's system and doesn't need a decision rule. We will finally present the open topics related to this system, such as the search for a completeness proof inside the calculus of structures, which would be more elegant than the translation from the sequent calculus used so far.
Oct 05 2007, 14:00
Speaker: Simon Kramer
Title: Animation and Knowledge Programming for the Timed Calculus of Cryptographic Communication
Abstract:
We give an overview of the Timed Calculus of Cryptographic Communication, one of the very few process calculi for security with real-time capabilities, and argue that the addition of knowledge programming capabilities to our calculus is easy. We intend to animate the calculus via logic programming.
URLs: (Thesis, Chapter 4.1 and 4.2)
Oct 02 2007, 14:00
Speaker: Simon Kramer
Title: The Intended and Actual Meaning of a Cryptographic Message and Protocol
Abstract:
We propose a denotational definition for the (actual) meaning of a cryptographic message and, based on it, an equational definition for the context-sensitivity of that meaning, both via hypothetical knowledge and provability. As a result, we obtain a formalisation of the first of Abadi and Needham's principles for prudent engineering practice for --- and a tentative denotational semantics of --- cryptographic protocols.
Building on this (published) work, we present ongoing work on the distinction between the intended and the actual meaning of a cryptographic message and protocol."
URLs: (Thesis, Chapter 4.3)
(FCS-ARSPA'07 respectively LORI'07)
Jun 19 2007, 14:00
Speaker: Cosimo Laneve
Title: The must preorder revisited -- an algebraic theory for web services contracts.
Abstract:
We define a language for Web services contracts as a parallel-free fragment of CCS and we study a natural notion of compliance between clients and services in terms of their corresponding contracts. The induced contract preorder turns out to be valuable in searching and querying registries of Web services, it shows interesting connections with the must preorder, and it exhibits good precongruence properties when choreographies of Web services are considered.
Our contract language may be used as a foundation of Web services technologies, such as WSDL and WSCL.
HTTP: cs.unibo.it/PiDuce
Jun 12 2007, 14:00
Speaker: Josef Widder
Title: Consensus in the Presence of Value Faults.
Abstract:
The problem of agreeing on a common value (consensus) encapsulates the inherent problem of building reliable, i.e., fault tolerant systems. The faults considered in this talk can be subsumed under value faults; informally, from the viewpoint of the receiver of some message, the content of the message may be different from what would have been received in the absence of faults (i.e., if every component on the path of the message has worked according to its specification).
The first part of the talk will consider a novel failure model (called
mortal Byzantine) which captures all process failures which eventually
lead to the crash of the faulty process. By considering an optimal
consensus algorithm which tolerates this failure model, we motivate a
more general formalism which should allow to investigate the
requirements of consensus regarding the communication structure in a
distributed computation. In the second part of the talk we will
introduce such a formalism (the heard-of model incorporating value
faults) which allows to separate the requirements on the communication
regarding safety and liveness of consensus while capturing dynamic and
transient link and process failures.
Jun 07 2007, 15:00
Speaker: Daniele Varacca
Title: Event structure semantics of the pi-calculus.
Abstract:
We propose the first compositional event structure semantics for a fully expressive pi-calculus, generalising Winskel's event structures for CCS. The pi-calculus we model is the pi-calculus with recursive definitions and summations. First we model the synchronous calculus, introducing a notion of dynamic renaming to the standard operators on event structures. Then we model the asynchronous calculus, for which a new additional operator, called rooting, is necessary for representing causality due to new name binding. The semantics are shown to be operationally adequate and sound with respect to bisimulation.
Jun 04 2007, 15:00
Speaker: Vladimiro Sassone
Title: A Bayesian model for event-based trust.
Abstract:
We focus on systems where trust in a computational entity is interpreted as the expectation of certain future behaviour based on behavioural patterns of the past, and concern ourselves with the foundations of such probabilistic systems. In particular, we aim at establishing formal probabilistic models for computational trust and their fundamental properties. In the paper we define a mathematical measure for quantitatively comparing the effectiveness of probabilistic computational trust systems in various environments. With this foundation in place, we formalise a general notion of information about past behaviour, based on event structures. This yields a flexible trust model where the probability of complex protocol outcomes can be assessed.
May 31 2007, 14:00
Speakers: Kaustuv Chaudhuri and Joelle Despeyroux
Title: A Hybrid Temporal Logical Framework for Systems Biology.
Abstract:
We propose a logical framework for reasoning in and about systems biology. Our framework is based on Girard's linear logic, extended with modal situated truth and a temporal interpretation of the modal worlds. The ``current world'' (or instant of time) can be referred to in the logic using the localisation operator from hybrid logic, which allows us to describe the delays in a process and hence the rates of reactions. The resulting logic gives a uniform language for both stochastic descriptions, such as those based on the Pi-calculus, and continuous ODE descriptions.
May 29 2007, 14:00
Speaker: Alexandre Miquel
Title: The experimental effectiveness of mathematical proofs.
Abstract:
The Curry-Howard correspondence interprets each mathematical proof as a program realizing some specification (deduced from the proved formula). But what happens when the proof relies on experimental assumptions - for instance laws of physics? In this talk, I propose to study the frontier between mathematical reasoning and the empirical hypotheses underlying natural sciences. For that, I will start from a problem posed by the philosopher Karl R. Popper on the use of abstract mathematical tools in an empirical framework. I will then show how modern realizability techniques can be used to solve this problem, suggesting new ways of combining mathematical reasoning with experimental protocols effectively.
May 03 2007, 14:30
Speaker: Robin Milner
Title: An Introduction to Bigraphs.
Abstract:
Bigraphs are a generic model for mobile interactive systems. They have three aims:
(1) To give a uniform treatment of behavioural equivalences and preorders in process calculi;
(2) To provide a way to models real-world mobile systems, whether natural or constructed;
(3) To provide a programming or descriptive tool that will allow real systems or specifications to be executed, or simulated.
This is the first of three talks on bigraphs in May, and I shall describe bigraph structure and dynamics slowly, with as much intuition as possible. I hope I'll get far enough to explain how to exactly recover bisimilarity for finite CCS in this general framework. This serves (1) above.
The second talk, by Arne Glenstrup on May 10, will serve (2) by explaining how bigraphs are implemented at ITU Copenhagen.
The third talk, by Jean Krivine on May 22, will serve (3) by modelling
some biology.
May 10 2007, 14:30
Speaker: Arne Glenstrup
Title: Implementing Matching of Binding Bigraphs.
Abstract:
The Bigraphical Programming Languages (BPL) Project at the IT University of Copenhagen aims to do research into how programming languages for mobile and context-aware applications can be based on the theory of bigraphs.
As a first attempt to operationalise bigraphs, we have implemented a tool for representing and manipulating binding bigraphs. The implementation stands out as being closely based on bigraph theory formally proven correct. It includes representations of normal and regular forms, as well as algorithms for normalisation and regularisation.
The keystone that enables simulation of bigraphical reactive systems is a matching algorithm which is based on an inference system that has been formally proven sound and complete [1].
This talk will report on major aspects of the ongoing implementation work.
This is joint work with Lars Birkedal, Troels Christoffer Damgaard and Espen Hojsgaard.
---------------
[1] Birkedal, L., Damgaard, T. C., Glenstrup, A. J., and Milner, R. (2006b). Matching of bigraphs. In Proceedings of Graph Transformation for Verification and Concurrency Workshop 2006, Electronic Notes in Theoretical Computer Science. Elsevier.
May 22 2007, 14:30
Speaker: Jean Krivine
Title: A platform for the Simulation and analysis of bio molecular systems in the kappa-calculus.
Abstract:
Joint work with Vincent Danos (Laboratoire Preuves Programmes et Systemes,CNRS, France), Jerome Feret (Ecole Normale Superieure, Paris), Walter Fontana (Systems Biology Department, Harvard Medical School, US).
In this talk we present a tool currently in development at Plectix Biosystems (Boston, US) allowing to analyse and simulate large bio molecular systems. The tool relies on an agent based formalism called kappa [1]. We first present the language in which states, called solutions or systems, are graphs where connections are made on sites and transitions are generated by a restricted class of graph-rewriting rules. We will see that this language can be neatly represented and extended using bigraph formalism. We will then proceed with the description of the stochastic simulation algorithm.
[1] Formal Molecular Biology (TCS 325, 2004) Vincent Danos, Cosimo Laneve
Mar 13 2007, 14:00
Speaker: Ichiro Hasuo (Joint-work with Yoshinobu Kawabe at NTT Corporation, Japan)
Title: Probabilistic Anonymity via Coalgebraic Simulations.
Abstract:
There is a growing concern on anonymity and privacy on the Internet, resulting in lots of work on formalization and verification of anonymity. Especially, importance of probabilistic aspect of anonymity is claimed recently by many authors. Among them are Bhargava and Palamidessi who present the definition of probabilistic anonymity for which, however, proof methods are not yet elaborated. In this paper we introduce a simulation-based proof method for probabilistic anonymity. It is a probabilistic adaptation of the method by Kawabe et al. for nondeterministic anonymity: anonymity of a protocol is proved by finding out a forward/backward simulation between certain automata. For the jump from non-determinism to probability we fully exploit a generic, coalgebraic theory of traces and simulations developed by Hasuo, Jacobs and Sokolova. In particular, an appropriate notion of probabilistic simulations is obtained by instantiating a generic definition with suitable parameters.
REFERENCE:
Ichiro Hasuo and Yoshinobu Kawabe.
Probabilistic Anonymity via Coalgebraic Simulations.
To appear in Proc. ESOP 2007.
Feb 14 2007, 15:00
Speaker: Daniele Gorla
Title: On the Relative Expressive Power of Calculi for Mobility.
Abstract:
In this talk, we shall comparatively analyse some mainstream calculi for mobility: the pi-calculus, the distributed pi-calculus, a distributed version of Linda and Mobile/Boxed/Safe ambients. In particular, we shall focus on their relative expressive power, i.e. we shall try to encode one in the other while respecting some reasonable properties. By means of 'good' encodings, or impossibility of such results, we set up a hierarchy of these languages. Finally, we discuss and compare several variants of ambient-like languages, including objective moves, passwords and different semantics for the mobility primitives and for parent-child communications.
Page maintainer: Carlos Olarte