We present a novel, yet well known logic of predicates with explicit substitutions. The logic is novel, since it extends the logic of predicates with explicit substitutions as a new bunch of atomic formulae. In this way the world of Platonic facts - built from predicates - is augmented with formulae capable to talk about change. The logic is well know since what it formalizes is merely a part of the usual meta-level activities. What we get is a non-monotone substructural logic. We present it in the form of a sequent calculus, and discuss its mathematical semantics. The ability to talk about `change' within the new logic opens perspectives for application in Computing Sciences. The following application areas are indicated: - imperative program verification, specification and development; - a solution to the Frame Problem (within AI area of reasoning about action) - reasoning about equivalence of symbolic transition systems (i.e., value-passing processes).

(see http://www.ipipan.gda.pl/)

We study the deductive verification of infinite-state systems modeled by extended automata. Typically, this process requires proving many invariants, and automatically discharging these proof obligations would save the user a significant amount of effort. We introduce techniques for automatically verifying that a predicate is an inductive invariant in a given context, and identify a class of systems and a logic for expressing invariants and contexts for which the problem is decidable.

(see http://www.irisa.fr/pampa/perso/rusu/csl/csl.ps)

The latest version of the test langauge TTCN testifies to the current interest in MSC-type languages in software and telecom testing; TTCN-3, which aims at a broader class of systems than its predecessors, comes equipped with an MSC-based graphical syntax known as TSC. Since we are not interested in covering such as wide spectrum as TTCN and with the aim of being more integrated in UML, we seek to define a test description language based on UML sequence diagrams. The presentation starts with a brief introduction to collaborations and interactions (abstract syntax) as well as to collaboration diagrams and sequence diagrams (concrete syntax). We attempt to clarify certain important aspects of the informal semantics for these defined in the UML documentation. We then discuss possible ways of extending these diagrams in order to cover the needs of a test description language. For pragmatic reasons, we strive to minimise any changes to the UML 1.4 definition wherever possible, particularly as regards the UML metamodel.  

TRANSPARENTS (FICHIER POSTSCRIPT)
 
 

Dans le modèle original des automates temporisés proposé par Alur et Dill, les seules affectations qui sont autorisées sont les remises à zéro. Par exemple, il n'est pas possible d'affecter à une horloge une constante non nulle, ou bien la valeur d'une autre horloge, ou bien, de manière non déterministe, une valeur quelconque plus grande ou plus petite qu'une constante voire une horloge. Dans le travail que nous avons effectué, nous avons étudié ce type d'affectations. Nous avons dégagé de larges classes d'affectations qui préservent la décidabilité du modèle et qui se trouvent juste à la frontière de l'indécidable. Un point surprenant est le fait que, contrairement aux seules remises à zéro, la décidabilité des autres affectations dépend de la forme des gardes, à savoir si elles sont diagonales ou pas. Pour toutes les classes décidables que nous avons dégagées, nous proposons une généralisation de l'automate des régions, ce qui donne un algorithme de décision PSPACE. En outre, nous avons étudié l'expressivité des classes décidables que nous avons dégagées : il s'avère que les automates temporisés avec assignations ne sont pas beaucoup plus expressifs que les automates temporisés classiques. Par contre, les assignations sont des macros compactes intéressantes pour la modélisation de certains systèmes temporisés. Enfin, nous avons étudié une possible implémentation de ces assignations avec comme structure de données les DBMs (Difference Bounded Matrices).

(voir http://www.lsv.ens-cachan.fr/~bouyer)
 

TRANSPARENTS (FICHIER POSTSCRIPT)
 
 

(Travail en collaboration avec M.-P. Béal)
Dans un premier temps, nous rappellerons la caractérisation des fonctions séquentielles due à Choffrut. Nous montrerons comment il peut être décidé en temps polynomial si un transducteur réalise une fonction séquentielle puis nous décrirons l'agorithme de déterminisation qui découle de la caractérisation.
Dans un second temps, nous montrerons comme ces résultats peuvent être étendus aux mots infinis. Nous donnerons une caractérisation des fonctions séquentielles puis nous décrirons un algorithme de déterminisation dans le cas des transducteurs sur les mots infinis.

La méthode B est une méthode formelle de programmation visant à spécifier et à produire des logiciels de manière sûre. En B, un composant logiciel - une machine abstraite - est munie d’un invariant. La preuve formelle que l'invariant est toujours satisfait est une obligation imposée au programmeur. Tant le langage utilisé pour rédiger les machines abstraites (logique, théorie des ensembles) que les obligations de preuve associées sont des outils puissants pour une meilleure maîtrise des spécifications initiales.
Pour la suite du développement, des machines abstraites peuvent être composées, une machine abstraite peut être raffinée en une autre machine et enfin une machine abstraite peut être implémentée par une autre machine. Toute action du développeur s'accompagne d'obligations de preuve qui, lorsqu'elles sont satisfaites assurent la conformité du logiciel à ses spécifications.
J-R. Abrial, The B-Book — Assigning Programs to Meanings, Cambridge University Press, 1996. J.B. Wordsworth, Software Engineering with B, Addison-Wesley, 1996
 

TRANSPARENTS (FICHIER PDF)
 
 

To keep up with the frantic pace at which devices come out, drivers need to be quickly developed, debugged and tested. We have recently introduced a new approach to improve driver robustness based on an Interface Definition Language, named Devil. Devil allows a high-level definition of the communication of a device. A compiler automatically checks the consistency of a Devil specification and generates stubs that include run-time checks. In this talk, we present and overview of Devil and an evaluation of the robustness improvement in developping drivers. To do so, we have injected programming errors using mutation analyses into Devil based Linux drivers and the original C drivers. We assess how early errors can be caught in the development process, by measuring whether errors are detected either at compile time or at run time. The results of our experiments on the IDE Linux disk driver show that nearly 3 times more errors are detected in the Devil driver than in the original C driver.

Rewriting systems on trace monoids, briefly trace rewriting systems generalize both string rewriting systems and vector replacement systems (or equivalently Petri nets). This makes trace rewriting systems interesting from a theoretical point of view. Furthermore applications for the problem of code generation and code optimization of parallel compilers are currently investigated. In the talk the decidability and complexity of several problems for trace rewriting systems is considered. These problems are termination, confluence, the word problem , and the problem of deciding the first order logic of trace rewriting.

M. Lohrey, Confluence problems for trace rewritng systems, to appear at Information and Computation
M. Lohrey, Complexity Results for Confluence Problems, Proceedings of the 24th MFCS, LNCS 1672, S. 114-124, 1999
 

TRANSPARENTS (FICHIER PDF)
 
 

Un des aspects les plus contraignants pour l'implantation d'applications temps-réel est que beaucoup de problèmes posés sont de complexité élevée (problèmes NP-durs) et ont un comportement général difficilement prévisible. Une solution est de faire un compromis entre temps de calcul et qualité du résultat, comme le permettent les algorithmes anytime. Dans cet exposé, après une partie introductive sur les algoritmes anytime, j'aborderai deux contributions de mon travail de thèse. La première concerne l'ordonnancement d'algorithmes anytime à contrat, non-interruptibles par définition, dans une situation où un événement peut interrompre le calcul. Nous traiterons de la complexité du problème résultant. La seconde contribution traite du problème de conception des algorithmes anytime et plus particulièrement de leurs profils de performance. Je montrerai en quoi la théorie de la complexité de Kolomogorov donne un point de vue éclairant sur le problème du choix des entrées.
Mots-clefs : Algorithmes Anytime, Complexité Algorithmique, Temps-réel, Ordonnancement, Complexité de Kolmogorov.
 

TRANSPARENTS (HTML)
 
 

Hierarchical Message Sequence Charts are a well-established formalism to specify telecommunication protocols. In this model, numerous undecidability results were obtained recently through algebraic approaches or relationships to Mazurkiewicz trace theory.
We show how to check whether a rational language of MSCs requires only channels of finite capacity. In that case, we also provide an upper bound for the size of the channels. This enables us to prove our main result: one can decide whether the iteration of a given regular language of MSCs is regular if, and only if, the Star Problem in trace monoids (over some restricted independence alphabets) is decidable too. This well-known question remains open and it justifies the recent proposal to restrict to locally synchronized HMSCs since they describe all regular finitely generated languages.

Let the "scope" of the accuracy property of an unreliable failure detector be the number x of processes that may not suspect a correct process. This notion gives rise to new classes of failure detectors among which S_x and <>S_x. The k-set agreement problem generalizes the consensus problem in the sense that the number of decided values is bounded by k. There exist protocols that solve this problem in asynchronous distributed systems when f=k. The talk will consider asynchronous distributed systems equipped with limited scope accuracy failure detectors. It will present conditions on n, f, k and x that allow to solve the k-set agreement problem in those systems and two protocols. The first protocol solves the problem in asynchronous distributed systems augmented with a failure detector of the class S_x. It requires f>S_x. It defines a family of protocols that allows to solve the k-set agreement problem under some condition.

Les Message Sequence Charts sont un langage graphique a priori intuitif. Cependant, les opérateurs de composition du langage permettent de définir des MSC dont l'interprétation se révèle ambiguë. Lorsque des MSC sont écrits par une première personne, puis transmis à une autre dans un but de documentation, de spécification ou d'implémentation, ces ambiguités peuvent amener des erreurs dès la phase de l'étude des exigences. Nous identifions trois types de MSC dit "pathologiques", et proposons des méthodes de détection de ces classes à risque.

Les treillis représentent une structure algébrique, mais aussi combinatoire, qui apparaît naturellement comme outil de modélisation dans un grand nombre de domaines. Un treillis est une structure algébrique possédant deux opérations particulières appelées borne supérieure et borne inférieure. C'est aussi un objet combinatoire qui se définit comme un ensemble partiellement ordonné (relation binaire réflexive, antisymmétrique et transitive) possédant des éléments particuliers appelés borne supérieures ou bornes inférieures. Notre approche est une approche combinatoire des treillis pour une étude structurelle et algorithmique. Aprés quelques définitions des treillis, et de classes de treillis intéressantes, nous présenterons dans ce séminaire deux codages d'un treillis (le premier pour des traitements locaux, le second pour des traitement sur la structure du treillis), puis nous introduirons quelques opérations classiques associant un treillis à un autre objet combinatoire (treillis des antichaînes (maximales), treillis de Galois (ou des concepts), complété de MacNeille).
 

TRANSPARENTS (FICHIER POSTSCRIPT)
 
 

Nous définissons la sémantique opérationnelle d'un calcul de processus synchrone. Ce calcul emprunte certains traits du calcul SCCS de Milner et d'autres a une variante (asynchrone) du pi-calcul due a Laneve: le calcul des solos. Nous dérivons une interprétation asynchrone du calcul à partir de sa sémantique opérationnelle synchrone en faisant abstraction de la notion de présence/absence (c.a.d. la notion de temps global). Nous montrons que les processus de ce calcul possèdent une forme normale hiérarchique. Il s'agit d'une représentation qui rend le contrôle explicite (un peu comme le C.P.S. dans le lambda-calcul). Au moyen de cette HNF, nous définissons certaines propriétés d'équivalence sémantique telles que l'endochronie et l'isochronie.

Nous avons développé depuis plusieurs années des techniques de génération automatique de test de comportements de systèmes réactifs, fondés sur une représentation des comportements par des systèmes de transitions. Le résultat est le prototype TGV. Une question actuelle est d'essayer d'étendre la méthode pour permettre la génération de tests comportant du parallélisme. Ceci est motivé par la question du test de systèmes répartis, le test pouvant être lui-même réparti. Pour cela, il faut être capable d'exploiter le parallélisme présent dans la spécification. L'idée naturelle est donc de substituer au modèle des systèmes de transitions, un modèle de vrai parallélisme (dépliage de réseaux ou encore structures d'événements). Le sujet prospectif revient à reprendre la démarche adoptée dans TGV (partir de spécifications formelles de haut-niveau et d'objectifs de test, et produire des sous comportements abstraits qui peuvent s'interpréter comme des tests). Malheureusement, l'acquis algorithmique sur ces modèles est bien moindre que dans le cas des systèmes de transitions. Cet exposé va décrire le problème et présenter quelques ébauches de solutions à partir d'illustrations.

We study a class of extended automata defined by guarded commands over Presburger arithmetic and uninterpreted functions. On the theoretical side, we show that the reachability problem is semi-decidable in this model. On the more practical side, the class is useful for modeling programs with potentially unbounded data structures. The reachability procedure can then be employed for program verification, simulation, and testing. We discuss an implementation of the procedure using the new ICS decision procedures from SRI.

A fundamental problem in software-based security is whether local security checks inserted into the code are sufficient to implement a global security property. We present a formalism based on a linear-time temporal logic for specifying global security properties pertaining to the control flow of the program, and illustrates its expressive power with a number of existing properties. We define a minimalistic, security-dedicated program model that only contains procedure call and run-time security checks and propose an automatic method for verifying that an implementation using local security checks satisfies a global security property. We then show how to instantiate the framework to the security architecture of Java 2 based on stack inspection and privileged method calls.

Les systèmes (max,+) linéaires permettent la modélisation algébrique d'une classe particulière de réseaux de Petri temporisés: les graphes d'événements. Dans cet exposé on introduira un calcul "polynomial" permettant de caractériser une classe plus générale de réseaux temporisés.

Nous examinerons certaines des logiques classiques et des logiques modales qui sont les solutions que les mathematiques et la logique ont apportees au probleme de l'analyse rationnelle de notre perception de l'espace et du temps. Nous presenterons le point de vue de la satisfaction de contraintes sous lequel le probleme de la mecanisation du raisonnement sur l'espace et sur le temps a ete aborde.

Cet exposé portera sur la fermeture des langages de HMSC dans les langages de réseaux de Petri. Cette opération de fermeture correspond à une procédure effective, reposant sur la semi-linéarité des images commutatives des langages de HMSCs. Nous présentons pour finir quelques résultats effectifs afférents à la répartition et à la vérification automatisées des réalisations de HMSCs par des réseaux de Petri.

Ce séminaire fait suite à ceux de Gilles Lesventes (30 mai 2000) et Philippe Darondeau (14 novembre 2000)

Mardi 19 septembre à 16h15 en salle Les Minquiers
Decidability of bisimilarity for infinite state systems
Exposé introductif
Colin STIRLING (Edimburgh, invité par Galion)

I survey some decidability results for bisimilarity between infinite-state systems, including decidability of equivalence between deterministic pushdown automata. All these results utilise the fact that bisimulation inequivalence is finitely approximable because the transition relations are finitely branching. It is an open question whether bisimulation equivalence is decidable for classes of infinitely branching systems. Instead of looking at bisimilarity on richer classes of infinite state systems, one can also look at the question of decidability of weak bisimulation. Little is known about weak bisimilarity because it immediately introduces the problem of infinite branching. The second half of the talk shows a new result that weak bisimilarity is decidable for a class of infinite state systems. What is particularly interesting is that weak inequivalence for these systems need not be finitely approximable.

page de Colin Stirling

---

Mardi 5 septembre 2000 à 16h15 en salle Les Minquiers
Une représentation de l'exécution non séquentielle des réseaux de Petri en logique linéaire non commutative
Exposé avancé
Christian RETORE (Paragraphe, IRISA)

Nous décrivons l'exécution d'un réseau de Petri dans la logique linéaire partiellement commutative, une logique intuitionniste introduite par Ph.~de Groote, qui contient et des connecteurs commutatifs et des connecteurs non commutatifs. Nous sommes ainsi capable de décrire fidèlement l'exécution en parallèle (step transition) d'un réseau de Petri, du moins tant que celle-ci reste un ordre série-parallèle. Ce codage s'inspire de la description des langages algébriques par les grammaires de Lambek. Bien que cela reste à préciser, ce travail suggère d'étudier un modèle plus général de réseaux de Petri dynamiques, dans lesquels un événement peut détruire ou produire d'autres événements comme c'est le cas dans les réseaux de Petri usuels pour les ressources ordinaires (ou jetons).

---

TRANSPARENTS

---

Simon Pickin (16 mai 2001)
Patricia Bouyer (15 mai 2001)
Daniel Herman (19 avril 2001)
Marcus Lorhey (16 mars 2001)
Arnaud Delhay (13 mars 2001)
Karell Bertet (20 février 2001)