Séminaire
Les lundis, à partir de 15h - UPEC CMC - Salle P1-009
Séminaires 2012-13
2013-06-17
Francesco Belardinelli (Laboratoire IBISC, Université d'Evry) P1-05
Verification of Artifact-Centric Multi-Agent Systems via Finite Abstraction: Some Decidability Results
Artifact systems have recently received considerable attention in the business process community. These can be described in terms of interacting modules, or artifacts, consisting of a data model and a lifecycle, which account respectively for the relational structure of data and their evolutions over time. However, by considering data and processes as equally relevant tenets, the typical questions concerning the verification of these services become inherently more difficult and can no longer be solved by current methodologies. Specifically, the presence of data means that the number of states in artifact systems is infinite in general.
In this talk I will present agent-based abstraction techniques that can be deployed to make the model checking problem amenable, thus obtaining decidability results for specific classes of artifact systems. These results enable the verification of basic temporal-epistemic properties in a first-order setting.
The research presented in this talk is joint work with Prof A. Lomuscio and Dr F. Patrizi and it has received funding within the EU STREP Project ACSI.
2013-06-10
Daniel Leivant (Indiana University Bloomington) 15h30, salle des theses
Notions de completude pour les logiques de programmes
Les logiques de programmes ne peuvent etre completes dans le sense ou le sont les logiques purs. La completude relative, inventee par Cook, etait le substitut de choix. Et pourtant cette notion a des importantes lacunes.
Commencant par un expose sommaire des logiques en question, nous considererons une approche alternative a la question de completude, inspiree celle-ci par la theorie de la demonstration.
2013-05-27
Arnaud Sangnier (LIAFA) salle des thèses
Reachability analysis of reconfigurable broadcast networks
We study decision problems for parameterized verification of a formal model of Ad Hoc Networks with broadcast and spontaneous movement. The communication topology of a network is represented as a graph. Nodes represent states of individual processes. Adjacent nodes represent single-hop neighbors. Processes are finite state automata that communicate via selective broadcast messages. Reception of a broadcast is restricted to single-hop neighbors. We study parameterized reachability of an error state for this model and show that this problem can be solved in polynomial time. We then move to richer reachability queries with cardinality constraints and show how the complexity changes when considering different restrictions on the syntax of the queries.
This is a joint work with Giorgio Delzanno (University of Genova, Italy), Riccardo Traverso (University of Genova, Italy) and Gianluigi Zavattaro (University of Bologna, Italy).
2013-03-18
Yurii Rogozhin (Institute of Mathematics and Computer Science, Academy of Sciences of Moldova) salle des thèses
Small universal computing devices inspired by molecular biology
Alan Turing discovered that there are universal computing devices, which in principal are very simple. Claude Shannon suggested to find universal Turing machine of smallest size (he considered a descriptional complexity of universal programs). In this talk we apply the Shannon's task to other computing models, especially to modern computing models inspired by molecular biology, namely for Membrane computing, DNA computing and some others computing models. Thus, several very small universal computing devices inspired by molecular biology are presented.
2013-02-18
Pierre-Etienne Meunier (LAMA - Université de Savoie) salle des thèses
Complexité de communication et intrinsèque universalité des automates cellulaires
Je parlerai d'une méthode générique pour fabriquer des conditions nécessaires d'intrinsèque universalité pour les automates cellulaires. Cette notion d'universalité est plus forte que l'universalité Turing, et préserve une grande quantité d'invariants topologiques. L'idée de mon travail est de définir un problème de décision sur la dynamique d'un automate cellulaire, puis de prouver que la complexité de communication de ce problème est croissante avec une notion de simulation. Enfin, de montrer l'existence d'un automate cellulaire de complexité de communication Ω(n). La construction d'un protocole de communication simple résolvant le problème pour un automate cellulaire F montre alors que F n'est pas intrinsèquement universel.
2013-02-11
Thomas Polacsek (Onera) salle des thèses
Vers une aide à la spécification d’une politique d’échange d’information dans un SI
Aujourd'hui, face à la massification des échanges, il devient crucial de disposer au sein des Systèmes d'Information de règles qui régissent la diffusion de l'information entre les différents partenaires, c'est-à-dire d'une politique d'échange d'informations. Le but de cette approche est de fournir, dès les phases de conception, un outil qui aide l'utilisateur à définir la politique. Nous proposons donc d'utiliser des solveurs de contraintes pour analyser les propriétés génériques d'une spécification d'une politique d'échange et vérifier si la formalisation de cette politique est conforme aux intuitions. En effet, les erreurs de conception qui ne sont pas détectées avant la phase d'implémentation ne font qu'accroître les coûts de développement et les risques liés à la diffusion non maîtrisée de l'information.
2013-02-04
Vitor Rodrigues (Université d'Orléans) salle des thèses
Semantics-based Program Verification: an Abstract Interpretation Approach
Modern real-time systems demand safe determination of bounds on the execution times of programs. To this purpose, program execution for all possible combinations of input values is impracticable. In alternative, static analysis methods provide sound and efficient mechanisms for determining execution time bounds, regardless of knowledge on input data. We present a calculational and compositional development of a functional static analyzer using the theory of abstract interpretation. A particular instantiation of our data flow framework was created for the static analysis of the “worst-case execution time” (WCET) of a program running on multicore systems. The entire system is implemented in Haskell, with the objective to take advantages of the declarative features of the language for a simpler and more robust specification of the underlying concepts.
2013-01-28
Youssouf Oualhadj (LIF, Marseille)
Computing Optimal Strategies for Markov Decision Processes with Parity and Positive-Average Conditions
We study Markov decision processes (one-player stochastic games) equipped with parity and positive-average conditions. In these games, the goal of the player is to maximize the probability that both the parity and the positive-average conditions are fulfilled. We show that the values of these games are computable in polynomial time. We also show that optimal strategies exist, require only finite memory and can be effectively computed.
2013-01-14
Julien Tesson (LACL) P1-009
Développement et preuve de correction de programmes parallèles fonctionnels avec Coq
Concevoir et implanter des programmes parallèles est une tâche complexe, sujette aux erreurs. La vérification des programmes parallèles est également plus difficile que celle des programmes séquentiels.
Pour permettre le développement et la preuve de correction de programmes parallèles, nous proposons de combiner le langage parallèle fonctionnel quasi-synchrone BSML, les squelettes algorithmiques - qui sont des fonctions d’ordre supérieur sur des structures de données réparties offrant une abstraction du parallélisme - et l’assistant de preuve Coq, dont le langage de spécification est suffisamment riche pour écrire des programmes fonctionnels purs et leurs propriétés. Nous proposons un plongement superficiel des primitives BSML dans la logique de Coq sous une forme modulaire adaptée à l’extraction de programmes. Ainsi, nous pouvons écrire dans Coq des programmes BSML, raisonner dessus, puis les extraire et les exécuter en parallèle. Pour faciliter le raisonnement sur ceux-ci, nous formalisons le lien entre programmes parallèles, manipulant des structures de données distribuées, et les spécifications, manipulant des structures séquentielles.
Nous prouvons ainsi la correction d’une implantation du squelette algorithmique BH, un squelette adapté au traitement de listes réparties dans le modèle de parallélisme quasi synchrone. Pour un ensemble d’applications partant d’une spécification d’un problème sous forme d’un programme séquentiel simple, nous dérivons une instance de nos squelettes, puis nous extrayons un programme BSML avant de l’exécuter sur des machines parallèles.
2012-12-10
Amélie Gheerbrant (Laboratory for Foundations of Computer Science, University of Edinburgh) salle des thèses
Pattern-based XML queries
We present results of our study of pattern-based XML query languages. A variety of analogs of conjunctive queries over XML documents have been studied in the literature. We focus on languages based on tree patterns, which follow the structure of tree documents. They arise naturally in many problems related to integrating and exchanging data and to handling incomplete information. In this talk, we concentrate on the problems of finding certain answers to queries, and on static analysis, in particular, query containment.
The problem of computing certain answers arises when one queries incompletely specified databases, i.e., databases with missing information. As often happens, the complexity of the problem jumps when one moves from relations to XML. Nonetheless, we identified large relevant classes of queries for which efficient algorithms can be developed. Curiously, for some of these classes, no analogous results existed in the relational world. In fact, we uncovered a well-behaved class of relational queries which had been overlooked so far. Testing for query containment is a fondamental task in query optimization. In the relational case, classical homomorphism based tools lead to reasonable complexity algorithms. In XML such techniques can be applied only for very simple queries. Beyond thoses classes of queries, they can either be adapted by using more sophisticated data structures, or – provably – they cannot be adapted at all. In addition, we look at the containment problem in the presence of extra features (such as schemas for documents).
The talk will be based on papers from ICDT’12 and ICDT’13.
2012-11-26
Pablo Arrighi (IMAG) salle des thèses
Causal Graph Dynamics
We extend the theory of Cellular Automata to arbitrary, time-varying graphs. In other words we formalize, and prove theorems about, the intuitive idea of a labelled graph which evolves in time — but under the natural constraint that information can only ever be transmitted at a bounded speed, with respect to the distance given by the graph. The notion of translation-invariance is also generalized. The definition we provide for these causal graph dynamics' is simple and axiomatic. The theorems we provide also show that it is robust. For instance, causal graph dynamics are stable under composition and under restriction to radius one. In the finite case some fundamental facts of Cellular Automata theory carry through: causal graph dynamics admit a characterization as continuous functions, and they are stable under inversion. The provided examples suggest a wide range of applications of this mathematical object, from complex systems science to theoretical physics.
2012-11-19
Luidnel MAIGNAN (LACL) salle des thèses
Algorithmics on Cellular Automata: Some Geometric Examples
In this presentation, we study the programming of cellular automata and consider three problems of geometrical nature: moving “computation particles” on the grid in order to uniformize their density, constructing their convex hull, and constructing a connected proximity graph between them. With a focus on the algorithmic methodology, we show how to solve these problems using the same building blocks: computation of distances fields and motions/detections based on distance patterns. The obtained solutions use constant memory per cell and generalize over arbitrary regular grid. This shows that the algorithmic notion of modularity, but not only, can be retrieved in the context of cellular automata programming.
2012-11-12
Emmanuel Polonowski (LACL) salle des thèses
Génération automatique d'infrastructure pour les indices de De Bruijn en Coq
La formalisation à l'aide d'assistants de preuve des théories en sémantique des langages de programmation suppose de choisir une façon de représenter les lieurs de la syntaxe étudiée. Trois approches sont traditionnellement envisagées : une représentation par des variables nommées, une représentation par des indices de De Bruijn, une représentation par une syntaxe d'ordre supérieure. Chacune de ces approches possède un certain nombre d'avantages et d'inconvénients, et toutes ne peuvent être utilisées dans les différents assistants de preuve.
Nous présenterons dans cet exposé un outil permettant la génération automatique de fonctions et de propriétés nécessaires à la représentation sous forme d'indices de De Bruijn, qui évite au chercheur un développement souvent fastidieux et sans intérêt et lui laisse ainsi davantage de temps pour se concentrer sur les propriétés majeures de son travail. Nous verrons les points forts et les limites de cet outil, ainsi que plusieurs exemples d'utilisation et des informations sur sa conception.
2012-11-05
Emmanuel Filiot (LACL) salle des thèses
Exploiting Structure in LTL Synthesis
The aim of program synthesis is to automatically generate a program that satisfies a given specification, in contrast to program verification, for which both the specification and the program are given as input. The underlying goal is to improve program reliability and optimize design constraints, like time and human errors, and to get rid of the low-level programming tasks, by replacing them with the design of high-level specifications. The old dream of automatic synthesis, which among others was shared by Church, is difficult to realize for general-purpose programming languages. However in recent years, there has been a renewed interest in feasible methods for the synthesis of application specific programs, which have been, for instance, applied to reactive systems, distributed systems, programs manipulating arithmetic or concurrent data-structures.
Reactive systems are non-terminating programs that continuously interact with their environment. They arise both as hardware and software, and are usually part of safety-critical systems, for example microprocessors, air traffic controllers, programs to monitor medical devices, or nuclear plants. It is therefore crucial to guarantee their correctness. The temporal logic LTL is a very important abstract formalism to describe properties of reactive systems. As shown by Pnueli and Rosner in 89, the synthesis of reactive systems from LTL specifications is a 2-Exptime complete problem.
In this talk, I will present recent progresses in LTL synthesis based on a bounded synthesis approach inspired by bounded model-checking, and show that the high worst-case time complexity of LTL synthesis does not handicap its practical feasibility. This is achieved by exploiting the structure underlying the automata constructions used to solve the synthesis problem.
2012-10-22
Membres du LACL () 22 - 23 octobre 2012
Séminaire du labo
Résumé à venir
2012-10-11
Michael Guedj (LACL) 14h, salle des thèses
BSP Algorithms for LTL & CTL* Model Checking of Security Protocols
It has long been a challenge to determine conclusively whether a given protocol is secure or not. The development of formal techniques that can check various security properties is an important tool to meet this challenge. This document contributes to the development of such techniques by model security protocols using an algebra of coloured Petri net call ABCD and reduce time to checked the protocols using parallel computations. We exploit the well-structured nature of security protocols and match it to a model of parallel computation called BSP. The structure of the protocols is exploited to partition the state space and reduce cross transitions while increasing computation locality. At the same time, the BSP model allows to simplify the detection of the algorithm termination and to load balance the computations. We consider the problem of checking a LTL and CTL* formulas over labelled transition systems (LTS) that model security protocols. A prototype implementation has been developed, allowing to run benchmarks.
|
Adresse :
LACL, Département d'Informatique |
Secrétariat :
Flore Tsila |
Direction :
Régine Laleau |