Most Significant Contributions to Research

Algorithms for Controller Synthesis

I developed with my colleagues several algorithms for controller synthesis. The first algorithm constitutes an improvement of the synthesis algorithm of supervisors with partial observation proposed by Cieslak et al [IEEE Transactions on Automatic Control 40 (4)]. The second algorithm is appropriate for controller synthesis under full observation. It includes a search strategy based on an ingenious backtracking mechanism and does not need the generation of any global behavioral model of the whole system [Journal of Algorithms 25 (1)]. The third algorithm provides a better understanding of the relationship between techniques in the area of control theory and those in artificial intelligence. This work improves on methods in the control theoretic paradigm initiated by Ramadge and Wonham because it was the first to integrate the issues of controllability, safety, liveness and real time into a single framework [IEEE Transactions on Automatic Control 43 (11)].

Control of Parameterized Discrete Event Systems

The algorithms for controller synthesis proposed in the literature have major drawbacks when applied to industrial systems, particularly for parameterized systems (e.g., networks of similar processes). Two are related to scalability and computational complexity. To tackle these issues, I advocated controller synthesis methods that integrate abstraction techniques into synthesis procedures: one developed with my colleague Barbeau (now at Carleton University) and a Ph.D. student that exploits colored Petri nets and symmetry specifications [Discrete Event Dynamic Systems: Theory and Applications 9 (2)], and another that is oriented towards the calculation of attributed controllers from abstract models instead of a concrete model [Journal of Systems and Software 60 (2)]. The latter requires transformations both for reduction and merging. To be valuable, transformations must preserve soundness and correctness. My colleague Frappier and I proposed transformations that preserve correctness [LNCS 2178]. The problem of preserving soundness is more difficult and remains an open issue for the general case. Nonetheless, my colleague Desharnais from Université Laval and I, with a Ph.D. student, proposed solutions for bounded-data parameterized systems (MRS'2003) and state feedback control policies in the case of total observation [LNCS 3299] as well as in the case of partial observation [CDC-ECC'05]. Based on the latter work, we realized a deeper study on the control of parameterized discrete event systems with interconnections between processes. The result is a first complete theory on this subject [Discrete Event Dynamic Systems: Theory and Applications 19 (2)]. During the same period, we investigated heuristics-based procedures for deriving nonblocking controllers [IECON'09].

Control by delegation for behavior composition

In control of discrete event systems, the control is by disablement/enablement. There exists another type of control, the control by delegation, which is at the heart of a behavior composition framework. I formulated, with a Ph.D. student, a new team formation problem. In this problem, explicit behaviors are assigning to agents, whose tasks are equipped with multiple attributes having specific values. The goal is a desired behavior with tasks, but attribute values are expressed as preferences. The problem consists of finding a robust team of agents, in the form of compositions « agents-controller » that realize the goal with better utility values [LNAI 10413].

Systems-Theoretic View of Component-Based Software Development

Nowadays, component-based software engineering is still a fertile topic of research because software systems tend to be more complex and costly to develop. I investigated, with a Ph.D. student, the component-based software development in the perspective of systems theory, more precisely by adapting a hierarchical control theory for discrete event systems in order to synthesize observers (interfaces of components) and supervisors (controllers of components) at each level of the hierarchy. In addition, we showed how, with only three powerful atomic operators, to add control to a component and combine reusable components horizontally and vertically while maintaining invariant properties required by the theory. To the best of my knowledge, it is the first time that such a formal method is used to solve control problems in the context of component-based software engineering, including reuse. We first illustrated our approach by using an on-line system organized hierarchically from an aggregation of Web services [LNCS 6921]. Based on these results, this scalable method has been further improved to include an instantiation mechanism and an abstract dynamic in order to automatically generate code for programmable logic controllers [IEEE Transactions on Control Systems Technology]. The whole method has been used with success to create a repository of reusable components and control a modular production system available in our laboratory and similar to those encountered in the manufacturing industry. It consists of 44 components and its flat state space was estimated to 10³¹ states.

Exploring and Applying the Supervisory Control Theory Using a Satisfiability Approach

Most tools developed to support the supervisory control theory, integrate BDD-based techniques into fix-point algorithms to cope with large state space models. Another symbolic representation technique associated with SAT-solver and mainly used in bounded model checkers is less widespread. Our team formulated, in declarative manner with Alloy, abstract models for various variants of the supervisory control theory in order to demonstrate the feasibility of this technique. This work is unique because it helps people in acquiring a deep intuition of the theory, exploring the abstract models with their own instances to get solutions to practical problems, and ultimately extending the theory. Since our Alloy specifications have roughly the same size as the original mathematical formulations of these variants, prototyping and applying a theory in this way constitute a source of motivation and creativity to identify new problems and solve them. First, we defined a model of the hierarchical control architecture framework in order to obtain observers and supervisors associated with small reusable components. Among 44 components of a modular production system, 75% of those components have been successfully checked by the Alloy analyzer [LNCS 6959]. Without exploiting this hierarchical framework, it would have been impossible to achieve such a level of scalability with Alloy. Subsequently, we were the first to propose a Kodkod solution to compute supremal elements (of families of languages or predicates) [LNCS 7316]. We completely recasted the state-based control theory into an Alloy model and progressively enriched the model with respect to various extensions: partial observation, state tree structures and parameterized systems [Science of Computer Programming 94 (2)]. Finally, the Alloy model was integrated into a αRby program. The language αRby, which is a fusion of Alloy and Ruby, is a programming language for solver-aided programming. This solution yields great flexibility for sandwiching model findings between pre-and post-processing, which is a coding schema that would be extremely inefficient in Alloy/Kodkod or even impossible in pure Alloy [International Journal on Sofware Tools for Technology Transfer]. A comparison of three programming languages, including αRby, allows us to consider other programming paradigms to achieve this goal [Journal of Computer Languages].

Functional Security in Web-Based Information Systems

In a joint research project with the Laboratoire d'algorithme, logique et complexité of Université Paris-Est, we elaborated a framework for building reliable and secure Web-based information systems. First, based on the XACML standard of OASIS, we defined a metamodel for the design of access-control policy enforcement managers [LNCS 6888]. Then, we proposed solutions for a security kernel that are in line with the standard model-driven architecture defined by OMG. Security policies are expressed in EB³SEC. This language is an extension of EB³, an entity-based black-box specification method initially developed with my colleague Frappier [Software and Systems Modeling 2 (2)], or ASTD [Innovations in Systems and Software Engineering 4 (3)], a graphical notation of EB³ process expressions. The implementations of security policies are correct by construction, since ASTD formal specifications are translated into BPEL processes [International Journal of Systems and Service-Oriented Engineering 2 (2)] or interpreted by BPEL processes.

Plan Synthesis and Controller Synthesis

The experiment carried out by a Ph.D. candidate student jointly supervised by my colleague Kabanza and myself, and done in collaboration with professor Thiébaux from the Australian National Laboratory [Electronic Notes in Theoretical Computer Science 149 (2)], is based on our previous work, which provide a better understanding of the relationship between techniques in the area of control theory and those in planning. This work, carried out in collaboration with Barbeau (now at Carleton University) and my colleague Kabanza, includes a method that extends the traditional forward chaining planning approach in order to compute reactive plans, which are finite state machines involving cycles and uncontrollable events. Such plans are more appropriate for reactive agents than conventional plans [Artificial Intelligence 95 (1)]. This work, first introduced in a companion conference paper (IJCAI'1995), is still named nowadays. Other relationships between techniques in the area of control theory and those in behavior composition based on a particular form of planning have also been established [SMC 2015].