This page contains only my publications until 1999. More recent publications can be retrieved through the web pages of my research team (S4): Recent publications (since 2000).
Published by Kluwer Academic Publishers. The editors are myself, Philippe Darondeau, Luciano Lavagno and Xiaolan Xie.
This book aims at providing a view of the current trends in the development of research on Synthesis and Control of Discrete Event Systems. Papers collected in this volume are based on a selection of talks given in June and July 2001 at two independent meetings: the Workshop on Synthesis of Concurrent Systems, held in Newcastle upon Tyne as a satellite event of ICATPN/ICACSD and organized by Ph.~Darondeau and L.~Lavagno, and the Symposium on the Supervisory Control of Discrete Event Systems (SCODES), held in Paris as a satellite event of CAV and organized by B.Caillaud and X.Xie.
Synthesis is a generic term that covers all procedures aiming to construct from specifications given as input objects matching these specifications. Theories and applications of synthesis have been studied and developped for long in connection with logics, programming, automata, discrete event systems, and hardware circuits. Logics and programming are outside the scope of this book, whose focus is on Discrete Event Systems and Supervisory Control. The stress today in this field is on a better applicability of theories and algorithms to practical systems design. Coping with decentralization or distribution and caring for an efficient realization of the synthesized systems or controllers are of the utmost importance in areas so diverse as the supervision of embedded or manufacturing systems, or the implementation of protocols in software or in hardware. This convergence might create an occasion to establish stronger links between the various areas, yet loosely related although the same basic models of concurrency, namely automata, products of automata, and Petri nets, play a central role everywhere.
This satellite workshop of the CAV'01 conference has been held in Paris on July 23rd, 2001. The organizers were myself and Xiaolan Xie.
The French joint research project "MARS" on control synthesis of discrete event systems using Petri nets has allowed researchers from several laboratories to develop original controller synthesis methods, tools and applications. The aim of the symposium is to gather a larger community of researchers interested in supervisory control of discrete event systems and outline new trends and problems in the field.
The symposium programme will consist of both contributed talks (30 minutes including questions) and invited lectures (50 minutes), covering different topics on the supervisory control of discrete event systems. Proceedings will be distributed to participants.
In "Modeling and Verification of Parallel Processes", LNCS, vol. 2067, Springer, pp. 125-152. Co-authored with P. Darondeau, L. Hélouët and G. Lesventes.
The paper presents ongoing work aiming at understanding the nature of specifications given by High Level Message Sequence Charts and the ways in which they can be put into effective use. Contrarily to some authors, we do not set finite state restrictions on HMSCs as we feel such restrictions do not fit in with the type of distributed systems encountered today in the field of telecommunications. The talk presents first a series of undecidability results about general HMSCs following from corresponding undecidability results on rational sets in product monoids. These negative results which with one exception do not appear yet in the literature on HMSCs do indicate that the sole way in which general HMSCs may be usefully handed as behavioural specifications is to interpret their linear extensions as minimal languages, to be approximated from above in any realization. The problem is then to investigate frameworks in which these incomplete specifications may be given a meaning by a closure operation. The second part of the paper presents a closure operation relative to Petri net languages. This closure operation is an effective procedure that relies on semilinear properties of HMSCs languages. We finally present some decidability results for the distribution and verification of HMSCs transformed into Petri nets.
Journal on Formal Aspects of Computing, volume 13, pages 447-470, 2002. Co-authored with E. Badouel and P. Darondeau.
The synthesis problem for Petri nets consists in deciding constructively the existence of a Petri net with sequential state graph isomorphic to a given graph. If events are attached to locations, one may set as an additional requirement that the synthesised net should be distributable; i.e. such that events at different locations have no common input place, whence distributed conflicts are avoided. Distributable nets are easily implemented by finite families of automata (one per location) communicating with each other by asynchronous message passing. We show that the general Petri net synthesis problem and its distributed version may both be solved in time polynomial in the size of the given graph. We report on some preliminary experiments of Petri net synthesis applied to the distribution of reactive automata using the tool SYNET.
Mathematical Structures in Computer Science, volume 12, pages 377--403, 2002. Co-authored with C. Jard and L. Hélouët.
This article details a partial order semantics for families of scenarios represented by High-Level Message Sequence Charts (HMSCs): Graph grammars generating event structures are being used to represent HMSCs. A decision procedure for HMSC equivalence is then described. This can be considered as a first step toward formal manipulation of scenarios.
Information and Computation, volume 163, pages 125-171, 2000. Co-authored with A. Benveniste and P. Le Guernic.
Modularity is advocated as a solution for the design of large systems, the mathematical translation of this concept is often that of compositionality. This paper is devoted to the issues of compositionality for modular code generation, in dataflow synchronous languages.
As careless reuse of object code in new or evolving system designs fails to work, we first concentrate on what are the additional features needed to abstract programs for the purpose of code generation: we show that a central notion is that of scheduling specification as resulting from a causality analysis of the given program. Using this notion, we study separate compilation for synchronous programs. An entire section is devoted to the formal study of causality and scheduling specifications.
Then we discuss the issue of distributed implementation using an asynchronous medium of communication. Our main results are that it is possible to characterize those synchronous programs which can be distributed on an asynchronous architecture without loosing semantic properties. Two new notions of endochrony and isochrony are introduced for this purpose. As a result, we derive a theory for synthesizing additional schedulers and protocols needed to guarantee the correctness of distributed code generation.
Corresponding algorithms are implemented in the framework of the DC+ common format for synchronous languages, and the V4-release of the SIGNAL language.
European Journal on Automated Systems (JESA) 31, 3, May 1997, p. 503--524.
In this article, we address the problem of automatic synthesis of distributed programs from specifications given as sequential reactive automata. We contribute to set up a theoretical model for describing and understanding a distribution process for automata, based on the distribution of actions.
Proceedings of the International Conference on Application of Concurrency to System Design, ACSD 2004, 2004. Co-authored with Dumitru Potop-Butucaru and Albert Benveniste
In this paper we introduce the notion of weak endochrony, which extends to a synchronous setting the classical theory of Mazurkiewicz traces. The notion is useful in the synthesis of correct-by-construction communication protocols for globally asynchronous, locally synchronous (GALS) systems. The independence between various computations can be exploited here to provide communication schemes that do not restrict concurrency while still guaranteeing correctness. Such communication schemes are then lighter and more flexible than existing latency-insensitive or endo/isochronous counterparts.
Applications and Theory of Petri Nets 2003, Volume 2679, Pages 140-160, June 2003. Co-authored with Marek Bednarczyk, Luca Bernardinello, Wieslaw Pawlowski and Lucia Pomello
Two, seemingly different modular techniques for concurrent system development are investigated from categorical perspective. A novel approach is presented in which they turn out to be merely special instances of {\em pullback}, a general categorical limit construction. Interestingly, the approach is based on truly concurrent semantics of systems.
Published in: CONCUR'99, Concurrency Theory, 10 International Conference, Eindhoven, The Netherlands, August 1999.
We present an in-depth discussion of the relationships between synchrony and asynchrony. Simple models of both paradigms are presented, and we state theorems which guarantee correct desynchronization, meaning that the original synchronous semantics can be reconstructed from the result of this desynchronization. Theorems are given for both the desynchronization of single synchronous programs, and for networks of synchronous programs to be implemented using asynchronous communication. Assumptions for these theorems correspond to proof obligations that can be checked on the original synchronous designs. If the corresponding conditions are not satisfied, suitable synchronous mini-programs which will ensure correct desynchronization can be composed with the original ones. This can be seen as a systematic way to generate ``correct protocols'' for the asynchronous distribution of synchronous designs. The whole approach has been implemented, in the framework of the SACRES project, within the Sildex tool marketed by TNI, as well as in the Signal compiler.
Published in : MSR'99, deuxième congrès sur la modélisation des systèmes réactifs, Cachan, France, march 1999
This paper describes a polynomial algorithm for the synthesis of distribuable bounded Petri-nets. This algorithm is the basis for a new method of distribution of reactive automata which extracts concurrency and deals with non-local choices.
Published in : ISORC'98, The 1st IEEE International Symposium on Object-oriented Real-time Distributed Computing, Kyoto, Japan, 1998.
We introduce the definition of a language of distributed reactive objects, a Behaviour Description Language (BDL), as a unified medium for specifying, verifying, compiling and validating object-oriented, distributed reactive systems. One of the novelties in BDL is its seamless integration into the Unified Modeling Language approach (UML). BDL supports a description of objects interaction which respects both the functional architecture of system designs and the declarative style of diagram descriptions. This support is implemented by means of a partial-order theoretical framework. This framework allows to specify both the causality and the control models of object interactions independently of any hypothesis on the actual configuration of the system. Given the description of such a configuration, the use of BDL offers new perspectives for a flexible verification of systems by modeling them as an asynchronous network of synchronous components. It allows an optimized code generation by using compilation techniques developed for synchronous languages. It permits an accurate validation and test of applications by supporting the manipulation of both causal and control dependencies. BDL aims at maximizing the re-usability of high-level specifications while minimizing programming effort and test-case based validation of distributed systems.
Published in Tapsoft'95
In this paper we present a concurrency measure that is especially adapted to distributed programs that are obtained by automatic parallelization of sequential code. This measure is based on the antichain lattice of the partial order that models the distributed execution under consideration. We show the conditions under which the measure is computable on an infinite execution that is the repetition of a finite pattern. There, the measure can be computed by considering only a bounded number of patterns, the bound being at most the number of processors.
Published in Parle'93.
In this paper, we prove that the data-driven parallelization technique, which compiles sequential programs into parallel programs for distributed memory parallel computers, is correct. We define a model based on labeled transition systems, and we prove, in spite of nondeterminism due to communication asynchronism, the confluence of all possible behaviours of parallel programs obtained from the compilation rules.
We also show that this model is powerful enough to prove the correctness if various optimizations of the basic compilation mechanism.
Published in Forte'91.
The superimposition is a composition a distributed programs. It is a convenient concept for the design and implementation of control and observation algorithms in distributed systems, such as snapshots, detection of termination, global time, property checking, mutual exclusion and garbage collection. The present paper deals with the implementation of the superimposition on the formal description language Estelle. It consists in a compiler in a compiler which translates a static Estelle program with superimposition into a pure static Estelle program. Guidelines for programming observers and controllers of distributed systems specified in Estelle are given. The transformation techniques used for the compilation of superimposed Estelle programs into pure Estelle are also explained.
Presented to AFADL'98
This paper details a partial order semantics for families of scenarios represented by High-Level Message Sequence Charts (HMSCs): Graph grammars generating event structures are being used to represent HMSCs. A decision procedure for HMSC equivalence is then described. This can be considered as a first step toward formal manipulation of scenarios.
In this paper we introduce the notion of weak endochrony, which extends to a synchronous setting the classical theory of Mazurkiewicz traces. The notion is useful in the synthesis of correct-by-construction communication protocols for globally asynchronous, locally synchronous (GALS) systems. The independence between various computations can be exploited here to provide communication schemes that do not restrict the concurrency while still guaranteeing correctness. Such communication schemes are then lighter and more flexible than their latency-insensitive or endo/isochronous counterparts.
Two, seemingly different modular techniques for concurrent system development are investigated from a categorical perspective. A novel approach is presented in which they turn out to be merely special instances of pullback, a general categorical limit construction. Interestingly, the approach is based on truly concurrent semantics of systems.
We present an in-depth discussion of the relationships between synchrony and asynchrony. Simple models of both paradigms are presented, and we state theorems which guarantee correct desynchronization, meaning that the original synchronous semantics can be reconstructed from the result of this desynchronization. Theorems are given for both the desynchronization of single synchronous programs, and for networks of synchronous programs to be implemented using asynchronous communication. Assumptions for these theorems correspond to proof obligations that can be checked on the original synchronous designs. If the corresponding conditions are not satisfied, suitable synchronous mini-programs which will ensure correct desynchronization can be composed with the original ones. This can be seen as a systematic way to generate ``correct protocols'' for the asychronous distribution of synchronous designs. The whole approach has been implemented, in the framework of the SACRES project, within the Sildex tool marketed by TNI, as well as in the Signal compiler.
This paper details a partial order semantics for families of scenarios represented by High-Level Message Sequence Charts (HMSCs): Graph grammars generating event structures are being used to represent HMSCs. A decision procedure for HMSC equivalence is then described. This can be considered as a first step toward formal manipulation of scenarios.
We introduce the definition of a language of distributed reactive objects, BDL, as a unified medium for specifying, verifying, compiling and validating object-oriented, distributed reactive systems. One of the novelties in BDL is its seamless integration into UML. BDL supports a description of objects interaction which respects both the functional architecture of system designs and the declarative style of diagram descriptions. This support is implemented by means of a pre-order theoretical framework which allows to specify both the causality and the control models of object interactions independently of any hypothesis on the actual configuration of the system. Given the description of such a configuration, BDL offers new perspectives for a flexible verification of systems by modeling them as an asynchronous network of synchronous components. It allows an optimized code generation by using compilation techniques developed for synchronous languages. It permits an accurate validation and test of applications by supporting the manipulation of both causal and control dependencies. BDL aims at maximizing the re-usability of high-level specifications while minimizing programming effort and test-case based validation of distributed systems.
SYNET is a tool synthesizing bounded Petri-nets from finite transition systems. The algorithms used are polynomial and consist in a computation of regions in transition systems based on linear programming methods on rationnal numbers. SYNET also implements a new algorithm for the synthesis of distribuable nets in which events are mapped on a set of distributed processes. Then, the synthesized nets can be executed on a distributed environment. Finally, an application of SYNET is reviewed: the synthesis of a connection-disconnection communication protocol from its specification of service.
In this paper, we present a concurrency measure that is especially adapted to distributed programs that exhibit regular run-time behaviours. Such programs are frequently obtained by automatic parallelization of sequential code. This measure is based on the antichain lattice of the partial order that models the distributed execution under consideration. We show under which condition the measure is computable on an infinite execution which is the repetition of a finite pattern. The measure can then be computed by considering only a bounded number of patterns, this bound being at most the number of processors.
This paper addresses the problem of distributed program synthesis. In the first part, we formalize the distribution process and prove its correctness, i.e. that the initial centralized progam's behaviour is equivalent to the corresponding distributed one. In order to achieve that, we first represent the program by a finite transition system, labeled by the program's actions. Then we derive an independence relation over the actions from the control and data dependencies. This leads to represent the program by an order-automaton, whose transitions are labeled partial orders coding for an action and its dependencies with other actions. In the second part, we show how such an order-automaton can be practically used to derive a distributed program.
In this paper, we prove that the data-driven parallelization technique, which compiles sequential programs into parallel programs for distributed memory parallel computers, is correct. We define a model based on label transition systems, and we prove, from the chosen compilation rule, the confluence of all possible behaviours of the parallel programs we obtain, in spite of the asynchronism due to the communications. We also show that this model is powerful enough to prove the correctness of various optimizations of the basic compilation mechanism.
The superimposition is a distributed program composition. It is a convenient concept for the design and implementation of control and observation algorithms is distributed systems, such as snapshots, detection of termination, global time, verification of properties, mutual exlusion, garbage collection. The present research report describes the implementation of superimposition on static Estelle. It consists in a compiler that transforms a program in static Estelle extended to the superimposition into a pure static Estelle program. The problem of the correctness and complexity of the generated is also raised.
The aim of this thesis is the behavioural study of SPMD distributed programs, which are produced by automatic distribution of sequential programs. The results detailed in this thesis can be applied to both sequential imperative and synchronous reactive programs. A formal framework for correctness proofs of distribution schemes is detailed and applied on the correctness proof of a real distribution scheme of sequential imperative programs.
Two theoretical tools are used: partially ordered set theory and semi-commutations. The set of all possible behaviors of SPMD programs is coded by structures called order automata.
Then asynchronism and communication channel behavior of a subclass of SPMD programs are characterized. Asynchronism boundness and communication channel boundness are decidable in this class of SPMD programs. Two decision criteria are given.