### 12 juin 2017

*TBA*

**Yuri Gurevich**

Skip to content
# Séminaires 2016-17

Contact : seminar@lacl.fr
# Les lundis, à partir de 14h - UPEC CMC - Salle P2-131

### 12 juin 2017

*TBA*

**Yuri Gurevich**
(Microsoft Research)

### 22 mai 2017

*On the chemistry of typestate-oriented actors*

**Silvia Crafa**
(Université de Padoue)

### 15 mai 2017

*TBA*

**Thomas Fernique**
(LIPN)

### 24 avril 2017

*Computational modeling using P systems*

**Agustín Riscos Núñez**
(Universidad de Sevilla)

### 3 avril 2017

*Non-commutative lower bounds*

**Guillaume Lagarde**
(IRIF)

### 27 mars 2017

*TBA*

**Catalin Dima**
(LACL)

### 20 mars 2017

*Parameterised Verification of Epistemic Properties in Security Protocols*

**Ioana boureanu**
(University of Surrey)

### 20 mars 2017

*Parameterised Verification of Epistemic Properties in Security Protocols*

**Ioana boureanu**
(University of Surrey)

Abstract: Verifying certain security requirements is not even always decidable. Furthermore, properties like privacy preservation, which are not expressible as trace properties, can be verified only via few methodologies. In this talk, we will see some of these challenges and how they can be tackled, in part, by parameterised verification of temporal-epistemic logics in specialised multi-agent system semantics.

### 6 mars 2017

*Abstractions in humanoid motion*

**Nicolas Perrin**
(UPMC)

### 27 février 2017

*Probabilistic Disclosure: Maximisation vs. Minimisation*

**Serge Haddad**
(LSV)

Typestate-oriented programming is an extension of the OO paradigm in which objects are modeled not just in terms of interfaces but also in terms of their usage protocols, describing legal sequences of method calls, possibly depending on the object’s internal state. We argue that the Actor Model allows typestate-OOP in an inherently distributed setting, whereby objects/actors can be accessed concurrently by several processes, and local entities cooperate to carry out a communication protocol. We illustrate the approach by means of a number of examples written in Scala Akka.

TBA

The talk will try to provide a general overview of modeling frameworks for systems biology and population dynamics based on membrane computing.

We will overview some recent achievements which show that this unconventional and bio-inspired computing paradigm can be an alternative to classical modeling frameworks (e.g. those based on differential equations).

We will also refer to the associated simulation software tools which are necessary to enable virtual experimentation, as well as for the process of model validation.

No knowledge in arithmetic complexity will be assumed.

We still don’t know an explicit polynomial that requires non-commutative circuits of size at least superpolynomial.

However, the context of non commutativity seems to be convenient to get such lower bound because the rigidity of the non-commutativity implies a lot of constraints about the ways to compute.

It is in this context that Nisan, in 1991, provides an exponential lower bound against the non commutative Algebraic Branching Programs computing the permanent, the very first one in arithmetic complexity. We show that this result can be naturally seen as a particular case of a theorem about circuits with ***unique parse tree***, and show some extensions to get closer to lower bounds for general NC circuits.

Two joint works: with Guillaume Malod and Sylvain Perifel; with Nutan Limaye and Srikanth Srinivasan.

TBA

Abstract: Verifying certain security requirements is not even always decidable. Furthermore, properties like privacy preservation, which are not expressible as trace properties, can be verified only via few methodologies. In this talk, we will see some of these challenges and how they can be tackled, in part, by parameterised verification of temporal-epistemic logics in specialised multi-agent system semantics.

Humans typically do not realize how much intelligence is required to perform usual motions.

One of the reasons why we are so good at motion control seems to be that we can abstract continuous inputs and outputs and their relationships with great flexibility, and perhaps reason almost symbolically on these abstractions. This observation leads to the temptation to tackle humanoid robot motion problems with discrete abstractions and formal methods.

We consider opacity questions where an observation function provides

to an external attacker a view of the states along executions and

secret executions are those visiting some secret state from a fixed

subset. Disclosure occurs when the observer can deduce from a finite

observation that the execution is secret. In a probabilistic and non

deterministic setting, where an internal agent can choose between

actions, there are two points of view, depending on the status of

this agent: the successive choices can either help the attacker

trying to disclose the secret, if the system has been corrupted, or

they can prevent disclosure as much as possible if these choices are

part of the system design. In the former situation, corresponding to

a worst case, the disclosure value is the supremum over the

strategies of the probability to disclose the secret (maximisation),

whereas in the latter case, the disclosure is the infimum

(minimisation). We address quantitative problems (relation between

the optimal value and a threshold) and qualitative ones (when the

threshold is zero or one) related to both forms of disclosure for a

fixed or finite horizon. For all problems, we characterise their

decidability status and their complexity. Surprisingly, while in

maximisation problems optimal strategies may be chosen among

deterministic ones, it is not the case for minimisation problems,

but more minimisation problems than maximisation ones are decidable.