~~NOCACHE~~
/* DO NOT EDIT THIS FILE */
[[en:seminaires:acs:index|Analysis and conception of systems]]\\
Thursday December 1, 2016, 10:30AM, Salle 1007\\
**Julien Lange** (Imperial College) //Building Graphical Choreographies From Communicating Machines: Principles and Applications//
\\
Graphical choreographies, or global graphs, are general multiparty session specifications featuring expressive constructs such as forking, merging, and joining for representing application-level protocols. Global graphs can be directly translated into modelling notations such as BPMN and UML. In the first part of the talk, I will first present an algorithm whereby a global graph can be constructed from asynchronous interactions represented by communicating finite-state machines (CFSMs); and a sound characterisation of a subset of safe CFSMs from which global graphs can be constructed. In the second part, I will outline a few recent applications of this work to communicating timed automata and the Go programming language.
Organisation jointe avec le séminaire de l'équipe PPS
[[en:seminaires:acs:index|Analysis and conception of systems]]\\
Thursday June 23, 2016, 2:30PM, Salle 1007\\
**Elisabeth Remy** (Institut de Mathématiques de Luminy) //Analyse qualitative des réseaux de régulation génétiques//
\\
Les modèles d’interactions Booléens ont été introduits dans le contexte des réseaux de gènes par S. Kauffman dans la fin des années 60. On considère ici une variante, les modèles logiques, qui reposent sur un formalisme qualitatif avec mise à jour asynchrone des systèmes dynamiques discrets associés (R. Thomas, 1973).
L’expression d'un gène y est représentée par une variable discrète et l’évolution du réseau est contrôlée par un système d'équations logiques. A partir de ce système peut être extrait un graphe de régulation : il s’agit d’un graphe orienté signé, dont les noeuds représentent les gènes, et les arcs les régulations entre gènes. On y distingue deux types de régulations : les activations (interactions positives) et les inhibitions (interactions négatives).
Ces modèles génèrent des dynamiques de taille exponentielle, et nous faisons face à des problèmes d’explosion combinatoire.
Ainsi, nous cherchons à caractériser des propriétés de la dynamique (attracteurs, atteignabilité,...) sans avoir à générer le graphe de transition d’états, qui représente l’ensemble des trajectoires possibles.
Une méthode consiste à réduire le graphe, et étudier la dynamique réduite. L’opération de réduction crée des modifications potentiellement importantes dans la dynamique, il est donc nécessaire de bien caractériser ses propriétés de (non-)conservation. Nous verrons aussi comment identifier les attracteurs et quantifier leurs bassins d’attraction à l’aide de méthodes de Monte-Carlo adaptées.
Enfin, nous mettrons en valeur ces méthodes d'analyse à travers l’étude d’un modèle concernant la tumorigénèse du cancer de vessie.
[[en:seminaires:acs:index|Analysis and conception of systems]]\\
Thursday May 26, 2016, 2:30PM, Salle 1008\\
**Ralf Treinen** (IRIF) //Towards the verification of file tree transformations - the Colis project//
\\
This talk describes a recently started ANR project named Colis
(http://colis.irif.univ-paris-diderot.fr/), which has the goal of
developing techniques and tools for the formal verification of shell
scripts. More specifically, our goal is to verify the transformation
of a file system tree described by so-called debian maintainer
scripts. These scripts, often written in the Posix shell language, are
part of the software packages in the Debian GNU/Linux distribution.
A possible example of a program specification is absence of execution
error under certain initial conditions. Automatic program verification
even for this kind of specification is a challenging task. In case of
Debian maintainer scripts we are faced with even more challenging
properties like idempotency of scripts (required by policy), or
commutation of scripts.
The project is still in the beginning, so there are no results yet to
present. However, I will explain why I think that the case of Debian
maintainer scripts is very interesting for program verification : some
aspects of scripts (POSIX shell, manipulation of a complex data
structure) make the problem very difficult, while other aspects of the
Debian case are likely to make the problem easier than the task of
verifying any arbitary shell script.
[[en:seminaires:acs:index|Analysis and conception of systems]]\\
Thursday April 7, 2016, 2:30PM, Salle UFR\\
**Tobias Heindel** (University of Copehagen) //Computing means and moments of occurrence counts: rule-based modeling meets adaptive uniformization and finite state projection//
\\
The talk presents recent results on how to solve the general problem of computing the time evolution of means and moments of ``occurence counts'' in rule-based models; computability is in the sense of Weihrauch. Roughly, established techniques, namely adaptive uniformization and finite state projection, can be reused -- provided that occurrence counts (and their powers) are bounded by a polynomial in the ``size'' of the rule-based system and the ``size'' of the system does not explode. The most interesting results can be obtained for context-free systems, which can be thought of as branching processes equipped with structure; for these systems we have PTIME computability.
All results will be exemplified for the case of string rewriting, aiming for a widest possible audience of computer scientists, assuming only basic knowledge of continous time Markov chains with countable state space. Computing the time evolution of mean word counts in stochastic string rewriting is already highly non-trivial, even if it is the most basic example. The GEM OF THE TALK is the computation of mean word counts for context-free grammars!