WODES 2010 Programme

Download Preliminary Programme
Post-Conference Activities

Overview

Sunday, August 29, 2010
19:00
↓↑
21:00
 Welcome Reception & Registration at Café Campus
Monday, August 30 ,2010
8:00
↓↑
9:00
 Registration
9:00
↓↑
9:15
 Welcome
9:15
↓↑
10:15
 MoP:
Supervisory Control of Differential Equations
H 0110
Speaker: Paulo Tabuada
Chair: Thomas Moor
Abstract

Research in the area of hybrid systems has always been influenced by supervisory control techniques developed for discrete-event systems. One typically envisions a finite-state controller having a quantized view of the world and issuing supervisory commands implemented by continuous feedback control laws. This deceptively simple idea has resisted a mathematical formalization upon which the systematic synthesis of finite-state controllers could be built. I shall report on recent advances on this problem based on the notion of approximate bisimulation. Along the way, I will also discuss new supervisory control problems arising when controlling differential equations with finite-state supervisors.
10:15
↓↑
10:45
 Coffee break
10:45
↓↑
12:45
 MoM1:
Petri Net-based Techniques
H 0110
Chair: Manuel Silva
Co-Chair: Janan Zaytoon
 MoM2:
Invited Session
Hybrid Systems
H 0112
Organisers: Magnus Egerstedt
Organisers: Yorai Wardi
Chair: Magnus Egerstedt
Co-Chair: Christos Cassandras
12:45
↓↑
14:30
Lunch break
Lunches will be served at TU Mensa on the campus.
TU Mensa (© TU-Pressestrelle/Böck)
14:30
↓↑
15:50
 MoA1:
Invited Session
Diagnosis and Diagnosibility of Discrete Event Systems
H 0110
Organisers: Maria Paola Cabasino
OrganiMoamar Sayed Mouchaweh
Chair: Maria Paola Cabasino
Co-Chair: Christoforos Hadjicostis
 MoA2:
Hierarchical Supervisory Control
H 0112
Chair: Klaus Schmidt
Co-Chair: Peter Caines
15:50
↓↑
16:10
 Coffee break
16:10
↓↑
17:30/ 17:50
 MoE1:
Distributed Estimation and Fault Diagnosis
H 0110
Chair: Jan van Schuppen
 MoE2:
Estimation and Control for Max-Plus and Min-Plus Systems
H 0112
Chair: Sébastien Lahaye
Co-Chair: Ton J. J. van den Boom
Tuesday, August 31, 2010
9:00
↓↑
10:00
 TuP:
Coordination of Traffic Networks
H 0110
Speaker: René Boel
Chair: Alessandro Giua
Abstract

Transportation problems provide a rich class of case studies for investigating the implementability of supervisory and distributed control ideas. This talk will abstract a few problems from this area into distributed supervisory control problems. Case studies are taken from on-ramp control for freeways, coordinated traffic light control in urban traffic, and control of autonomous vehicles executing task with a deadline while avoiding collisions.

Each of these problems can be modelled as a timed automaton or a piecewise affine model, with timed Petri nets and fluid Petri nets as concise graphical representations. Reachability analysis, safety analysis, and observer design for these models can be reduced to some standard algorithms, at least conceptually. Specifications must be satisfied by designing supervisory controller limiting the actions of the different components in the network.

The problem becomes particularly challenging when local controllers in each vehicle or in each intersection in the traffic system have only limited communication channels for coordinating their actions. It will be shown for a number of interesting cases how distributed controllers can be designed achieving good coordination of the local controllers.
10:00
↓↑
10:30
 Coffee break
10:30
↓↑
12:30
 TuM1:
Diagnosis, Estimation and Testing
H 0110
Chair: Stefan Haar
Co-Chair: Shigemasa Takai
 TuM2:
Probabilistic Discrete Event Systems
H 0112
Chair: Eric Fabre
Co-Chair: Bernd Heidergott
12:30
↓↑
14:30
Lunch break
Lunches will be served at TU Mensa on the campus.
TU Mensa (© TU-Pressestrelle/Böck)
14:30
↓↑
15:50
 TuA1:
Invited Session
Towards Application of Supervisory Control - from Modeling, through Synthesis, to Implementation (Part I)
H 0110
Organisers: Rong Su
Organisers.Walter Murray Wonham
Chair: Rong Su
Co-Chair: Knut Åkesson
 TuA2:
Modelling and Analysis of Max-Plus Systems
H 0112
Chair: Jan Komenda
Co-Chair: Jean-Jacques Lesage
15:50
↓↑
16:10
 Coffee break
16:10
↓↑
17:10
 TuE1:
Invited Session
Towards Application of Supervisory Control - from Modeling, through Synthesis, to Implementation (Part II)
H 0110
Organisers: Rong Su
Organisers.Walter Murray Wonham
Chair: Rong Su
Co-Chair: Spiridon Reveliotis
 TuE2:
Applications I
H 0112
Chair: Feng Lin
Co-Chair: Philippe Darondeau
20:30
Conference Dinner at Clärchens Ballhaus

Conference Dinner

The conference dinner will be held in the Spiegelsaal (mirror hall) at Clärchens Ballhaus on August 31st. Clärchens Ballhaus was founded in 1913 and is one of the last remaining 1920s dancehalls in Berlin. It features prominently in Alfred Döblin's famous novel Berlin Alexanderplatz. Rumours say that it was one of Bersarin's favourite places – the legendary first Soviet commanding officer in Berlin. Today, Clärchens Ballhaus is again a popular place, where Berliners and tourists alike meet to dance, relax, eat and drink.

The richly ornamented Spiegelsaal in the upper floor of Clärchens Ballhaus brings the 19th century Gründerzeit back to life. Decorated with old cracked mirrors and an opulently stuccoed ceiling, the interior of the Spiegelsaal survived nearly untouched but bears the traces of one century of turbulent history.

Spiegelsaal
Spiegelsaal at Clärchens Ballhaus (© photo: Bernd Schönberger)
Wednesday, September 1, 2010
9:00
↓↑
10:00
 WeP:
Interfaces for Control Components
H 0110
Speaker: Rajeev Alur
Chair: Stéphane Lafortune
Abstract

Modern software engineering heavily relies on clearly specified interfaces for separation of concerns among designers implementing components and programmers using those components. The need for interfaces is evident for assembling complex systems from components, but more so in control applications where the components are designed by control engineers using mathematical modeling tools and used by software executing on digital computers. However, the notion of an interface for a control component must incorporate some information about timing, and standard programming languages do not provide a way of capturing such resource requirements.

This talk will describe how finite automata over infinite words can be used to define interfaces for control components. When the resource is allocated in a time-triggered manner, the allocation from the perspective of an individual component can be described by an infinite word over a suitably chosen alphabet. The control engineer can express the interface of the component as an omega-regular language that contains all schedules that meet performance requirement. The software must ensure, then, that the runtime allocation is in this language. The main benefit of this approach is composability: conjoining specifications of two components corresponds to a simple language-theoretic operation on interfaces. We have demonstrated how to automatically compute automata for performance requirements such as exponential stability and settling time for the LQG control designs. The framework is supported by a toolkit, RTComposer, that is implemented on top of Real Time Java. The benefits of the approach will be demonstrated using applications to wireless sensor/actuator networks based on the WirelessHART protocol and to distributed control systems based on the Control Area Network (CAN) bus.
10:00
↓↑
10:30
 Coffee break
10:30
↓↑
12:10
 WeM1:
Extensions of Supervisory Control I
H 0110
Chair: Ryan Leduc
Co-Chair: Robi Malik
 WeM2:
Invited Session
Max-plus algebra and max-plus-linear systems
H 0112
Organisers: Laurent Hardouin
Organisers: Jean-Louis Boimond
Chair: Laurent Hardouin
Co-Chair: Jean-Louis Boimond
12:10
↓↑
13:40
Lunch break
Lunches will be served at TU Mensa on the campus.
TU Mensa (© TU-Pressestrelle/Böck)
13:40
↓↑
15:00/ 14:40
 WeA1:
Extensions of Supervisory Control II
H 0110
Chair: José Cury
Co-Chair: Martin Fabian
 WeA2:
Applications II
H 0112
Chair: Georg Frey
Co-Chair: Miryam Barad
15:00
↓↑
15:30
 Closing Remarks
15:30
↓↑
16:00
 Coffee break

Post-conference Activities


DISC Workshop on Distributed Discrete Event Systems

As a satellite event of WODES 2010, a Workshop on Distributed Discrete Event Systems will be held on September 2. The event, organised by A. Giua (University of Cagliari, Italy) and L. Ricker (Mt Allison University, Canada), is an initiative of the European project DISC: Distributed Supervisory Control of Large Plants (INFSO-ICT-224498). The programme is available at http://www.disc-project.eu/DISC_wodes.html.

All WODES 2010 participants are invited to attend. Participation is free, but it is necessary to register by sending an email to Maria Paola Cabasino.

Monday, August 30 ,2010

MoP:
Supervisory Control of Differential Equations
09:15 - 10:15
H 0110
Speaker: Paulo Tabuada
Chair: Thomas Moor
Abstract

Research in the area of hybrid systems has always been influenced by supervisory control techniques developed for discrete-event systems. One typically envisions a finite-state controller having a quantized view of the world and issuing supervisory commands implemented by continuous feedback control laws. This deceptively simple idea has resisted a mathematical formalization upon which the systematic synthesis of finite-state controllers could be built. I shall report on recent advances on this problem based on the notion of approximate bisimulation. Along the way, I will also discuss new supervisory control problems arising when controlling differential equations with finite-state supervisors.
MoM1:
Petri Net-based Techniques
10:45 - 12:45
H 0110
Chair: Manuel Silva
Co-Chair: Janan Zaytoon

Linear Programming Techniques for Analysis and Control of Batches Petri Nets

10:45 -11:05
Authors:
Abstract
Topics: Petri nets
In this paper we consider Generalised Batches Petri nets (GBPN) and develop new linear algebraic techniques for the analysis of this model. Two main contributions are presented. The first contribution lies in the fact that although we consider the same GBPN model that has already be presented in the literature, we associate to this model a different semantics considering that the instantaneous firing flow of continuous and batch transitions are control variables that can take an arbitrary value provided they satisfy given constraints. The second contribution consists in the analysis of the steady state behavior of GBPN. We show that under the assumption that no discrete transition fires, a steady state can be characterized by solving a linear programming problem that takes into account the net structure and the initial marking.

Timing-dependent Boundedness and Liveness in Continuous Petri Nets

11:05 - 11:25
Authors:
Abstract
Topics: Petri nets
The classical structural boundedness and repetitiveness properties for discrete and untimed models are reconsidered here for timed continuous Petri nets (TCPN), under infinite server semantics. The timing is also involved in the analysis, by taking advantage of its matricial characterization. Properties analogous to conservativeness and consistency, in which the timing is involved, are defined. It is shown that such properties are sufficient for timed boundedness and timed liveness, respectively, even if the untimed model does not exhibit such properties. The rest of the paper is devoted to the study of these timing-dependent boundedness and liveness.

An Algorithm to Compute the Minimal Siphons in S4PR Nets

11:25 - 11:45
Authors:
Abstract
Topics: Petri nets
Minimal siphons in the class of S^4PR nets have become a conceptual and practical central tool. Therefore the availability of efficient algorithms to compute the minimal siphons is very important. In this paper we try to take advantage from the particular properties of the siphons in $S^4PR$ to obtain an efficient algorithm. These properties allow to express minimal siphons as the union of pruned minimal siphons containing only one resource. The pruning operation is defined as a relation and represented in a graph. The computation of the minimal siphons is based in the maximal strongly connected components of this graph. The algorithm is very economic in memory in all intermediate steps with respect to the classical algorithms.

SimHPN: A MATLAB Toolbox for Continuous Petri Nets

11:45 - 12:05
Authors:
Abstract
Topics: Petri nets
This paper presents a MATLAB embedded package for continuous Petri nets called SimHPN. It offers a collection of tools devoted to simulation, analysis and synthesis of dynamical systems modeled by continuous Petri nets. Its embedding in the MATLAB environment provides the considerable advantage of creating powerful algebraic, statistical and graphical instruments exploiting the high quality routines available in MATLAB.

Synthesis of Behavioral Controllers for DES: Increasing Efficiency

12:05 - 12:25
Authors:
Abstract
Topics: Petri nets
In Bollue et al. (2009) (Paper for the European Control Conference 2009: "Synthesis of Behavioral Controllers for Discrete Event Systems with NCES-like Petri Net Models"), a methodology was introduced for the synthesis of behavioral controllers for discrete-event systems. The approach is based on NCES-like Petri net models of the uncontrolled plant and additional goal and safety specifications given by linear marking constraints. This paper presents different approaches to improve the synthesis process with respect to efficiency and applicability. One focus is the use of satisfiability checking of systems of integer linear inequations in the preprocessing of the model for the elimination of unnecessary complexity during the process. Further, several improvements of the synthesis algorithm itself are discussed, which increase the efficiency by applying an advanced guided search and by reusing already found partial solutions.

State-space based Analysis of a Class of Dynamic Petri Nets: A Symbolic Approach

12:25 - 12:45
Authors:
Abstract
Topics: Petri nets
The design of dynamic or adaptable discrete-event systems needs for adequate modeling techniques in order to manage possible structural changes occurring during system's lifecycle. An usual approach is that of polluting design with details not concerning the (current) system behavior, rather its evolution. That hampers analysis, reuse and maintenance in general.
A Petri net-based reflective layout based on classical Petri nets was recently proposed to support dynamic discrete-event system's design, and was applied to dynamic workflows. The basic idea is that keeping functional aspects separated from evolutionary ones, deploying evolution on the (current) system configuration when necessary, results in a clean formal model for
dynamic systems. This model preserves the ability of verifying properties typical of classical Petri nets.
As a first step toward the implementation
of a discrete-event simulator, Reflective Petri nets are provided with a (symbolic) reduced state-transition graph
MoM2:
Invited Session:
Hybrid Systems
10:45 - 12:45
H 0112
Organisers: Magnus Egerstedt
Organisers: Yorai Wardi
Chair: Magnus Egerstedt
Co-Chair: Christos Cassandras

On the Geometry of Switching Manifolds for Autonomous Hybrid Systems

10:45 - 11:05
Authors:
Abstract
Topics: Hybrid Systems
This paper provides a geometrical analysis of autonomous hybrid systems optimal
control (HSOC) by studying the properties of optimal hybrid system trajectories and the
manifolds on which they switch between controlled vector fields. First, results previously
obtained in Taringoo and Caines (2009a), Taringoo and Caines (2009c) on the parameter
optimization of switching manifolds are reviewed. Second, we analyse (i) the geometric properties
of switching manifolds and (ii) the sensitivities of optimal control trajectories and their
connections with the Hessians of the value function of hybrid optimal control problems (HOCP).
Finally, we present an optimization algorithm for the local deformation of switching manifolds
in order to reduce the overall hybrid value function. Simulation results are presented to illustrate
the main ideas of the paper.

Numerically Stable Approximations of Optimal Control Processes Associated with a Class of Switched Systems

11:05 - 11:25
Authors:
Abstract
Topics: Optimization
In this contribution, we propose a numerical approach to optimal control processes governed by some specific switched systems. Our principal computational scheme can be characterized as an extension of the conventional proximal point method to optimal control problems (OCPs) with switched dynamical models. We study proximal based constructive approximations of the initial OCPs and establish the numerical stability (numerical consistency) of the resulting algorithm. We also discuss the practical implementability of the elaborated method and point some possible generalizations of our idea in the context of hybrid control systems.

IPA for Continuous Petri Nets

11:25 - 11:45
Authors:
Abstract
Topics: Petri nets
Recently there has been a considerable interest in the application of Infinitesimal Perturbation Analysis (IPA) to continuous queues, where its sample derivatives (gradients) were shown to be unbiased for a large class of systems. This paper extends the investigation to a class of hybrid Petri nets, where the special algebraic structure of continuous transitions yields simple algorithms for the IPA derivatives. We derive such algorithms for the performance functions of throughput and average workload, and show them to be model-free and easily computable from the sample paths.

Initial Investigations of Hybrid Thermodynamic Control Systems with Phase Transitions

11:45 - 12:05
Authors:
Abstract
Topics: Hybrid Systems
A systematic approach to the modelling of thermodynamic systems with phase transitions is presented. It is shown that the dynamics of these systems can be adequately represented within the regional hybrid systems framework. This means that the discrete state changes autonomously at fixed submanifold boundaries. Furthermore, to facilitate analysis we assume that in each single phase the system's dynamics can be described in terms of equilibrium thermodynamics. This allows for the application of well developed methods from contact geometry.

The minimisation of entropy plays a central role in all processes involving energy transformation and storage. So for this class of systems, there is a natural optimal control problem, namely that where the increase of entropy is used as a criterion to be minimised.

To illustrate these ideas we present a hybrid model of a simple thermodynamic system with a liquid-vapour phase transition. We analyse the system-theoretic properties of this model and formulate a hybrid optimal control problem.

Perturbation Analysis of Stochastic Hybrid Systems and Applications to Some Non-Cooperative Games

12:05 - 12:25
Authors:
Abstract
Topics: Hybrid Systems
We establish some conditions under which Infinitesimal Perturbation Analysis (IPA) for general Stochastic Hybrid Systems (SHS) becomes particularly simple and efficient. We then apply IPA to a class of stochastic non-cooperative games
termed "resource contention games" modeled through Stochastic Flow Models (SFMs), where two or more players (users) compete for the use of a sharable
resource. Simulation examples are provided for a simple version of such games to illustrate and contrast system-centric and user-centric optimization.

Graph Process Specifications for Hybrid Networked Systems

12:25 - 12:45
Authors:
Abstract
Topics: Hybrid Systems
Research in multi-agent systems has supplied a diverse collection of decentralized controllers to accomplish specific tasks. When agents execute a sequence of these controllers, the network behaves as a hybrid system, where the dynamics in each mode evolve according to a single controller in the sequence. This paper presents a formal specification for such a system that describes the underlying graph process associated with the information flow amongst agents in each mode. Since many decentralized controllers require specific information graph topologies in order to function properly, a problem that arises is that the information graph at the termination of one mode may not be sufficient to initiate the next mode in the sequence. We propose a Graph Process Specification (GPS) framework that describes the graph process. Furthermore, if two modes cannot be executed consecutively, a GPS provides a way to determine which modes can be inserted in between them to make the resulting sequence executable. We formally define a GPS, describe its execution, and provide examples that showcase its usage in composing together multiple decentralized controllers within a multi-agent system.
MoA1:
Invited Session:
Diagnosis and Diagnosibility of Discrete Event Systems
14:30 - 15:50
H 0110
Organisers: Maria Paola Cabasino
Organisers: Moamar Sayed Mouchaweh
Chair:Maria Paola Cabasino
Co-Chair: Christoforos Hadjicostis

Diagnosability of Labeled Petri Nets via Integer Linear Programming

14:30 - 14:50
Authors:
Abstract
Topics: Petri nets
The problem of diagnosability of a fault after the firing of a finite number of observable events (i.e. K-diagnosability) is tackled in this paper. This problem corresponds to diagnosability of a fault within a finite delay in the context of discrete event systems (DESs). Two results for DESs modeled as labeled Petri nets are given: the first is a sufficient condition for K-undiagnosability of fault, while the second is a necessary and sufficient condition for K-diagnosability. The proposed results exploit the mathematical representation of Petri nets and the Integer Linear Programming standard optimization tool.

Reduced-Complexity Verification for Initial-State Opacity in Modular Discrete Event Systems

14:50 - 15:10
Authors:
Abstract
Topics: (Finite-)State Automata
In this paper, we propose and analyze reduced-complexity methodologies for verifying initial-state opacity in modular discrete event systems. Initial-state opacity requires that the membership of the system initial state to a given set of secret states S remains opaque (uncertain) to an
intruder who has complete knowledge of the system model and observes system activity through some natural projection map. In the modular setting we consider, the given system is modeled as a textit{composition} (synchronous product) of M modules {G1,G2,...,GM} where each module Gi is a non-deterministic finite automaton with Ni states with the set of secret states S is of the form S={(x1,x2,...,xM)|xi is in Si}, where Si is the set of secret states for module Gi. Assuming that the pairwise shared events are pairwise observable and that the intruder observes events that are observable in at least one module, we provide a modular algorithm for verifying initial-state opacity with O(MN^{M-1}2^{N^{2}}) state and time complexity, where N=max_{i} Ni. This is a considerable reduction compared to the O(2^{(N^{M})^{2}}) state and time complexity of the centralized verification method, which verifies initial-state opacity by considering the composed system as a monolithic system.

Robust Diagnosability of Discrete Event Systems subject to Intermittent Sensor Failures

15:10 - 15:30
Authors:
Abstract
Topics: (Finite-)State Automata
The modeling of physical systems using discrete event models assumes that a set of sensors always report the event occurrences correctly. However, bad sensor operation can result in loss of observability of the events associated with the malfunctioning sensors. If one or more sensors fail, it may be possible that either the diagnoser stands still or provide wrong information on the fault occurrence. This paper assumes that intermittent sensor failures may occur and deals with the problem of fault diagnosis in the presence of intermittent sensor failures. To this end, an automaton model for intermittent sensor failures based on a newly proposed language operation (language dilation) is presented in the paper. Necessary and sufficient conditions for robust diagnosability against intermittent sensor failure are also given in the paper. The development of a robust diagnoser that copes with intermittent sensor failures is another contribution of the paper.

Robust Diagnosis of Discrete-Event Systems subject to Permanent Sensor Failures

15:30 - 15:50
Authors:
Abstract
Topics: (Finite-)State Automata, Diagnosis and Estimation
One approach to online fault diagnosis of discrete-event system is through the use of the diagnosers. Diagnosers are deterministic automata whose states are sets formed with the states of the plant together with labels that indicate if the trace that has occurred so far possesses or not the fault event. The decision regarding fault occurrence is taken based solely on observable events, i.e., events whose occurrences can be recorded by sensors. However, if one or more sensors that provide information on event occurrences fail, the diagnoser may either come to a halt or may even provide wrong information regarding fault occurrence. In order to overcome this deficiency, this paper proposes a robust diagnoser that deploys the redundancy that may exist in a set formed of diagnosis bases (set of events that guarantee fault diagnosability) with a view to ensure the fault diagnosis even in the occurrence of permanent sensor failure.
MoA2:
Hierarchical Supervisory Control
14:30 - 15:50
H 0112
Chair: Klaus Schmidt
Co-Chair: Peter Caines

Hierarchical Multitasking Control of Discrete Event Systems: Computation of Projections and Maximal Permissiveness

14:30 - 14:50
Authors:
Abstract
Topics: (Finite-)State Automata
This paper extends previous results on the hierarchical and decentralized control of multitasking discrete event systems (MTDES). Colored observers, a generalization of the observer property, together with local control consistency, allow to derive sufficient conditions for synthesizing modular and hierarchical control that are both strongly nonblocking (SNB) and maximally permissive. A polynomial procedure to verify if a projection fulfills the above properties is proposed and in the case they fail for a given projection an algorithm is proposed to find an extension of the set of events to be projected, in order to fulfill the sufficient conditions for SNB and maximally permissive hierarchical control.

A Compositional Approach for Verifying Hierarchical Interface-Based Supervisory Control

14:50 - 15:10
Authors:
Abstract
Topics: (Finite-)State Automata
Hierarchical Interface-based Supervisory Control (HISC) decomposes a
discrete-event system into a high-level subsystem which communicates
through interfaces with several low-level subsystems. The framework
provides a set of local conditions that can be checked for each subsystem
individually to conclude global conditions such as nonblocking and
controllability. The size of HISC systems that can be verified automatically is primarily
limited by the size of the largest subsystem. To overcome this limitation,
this paper proposes the use of compositional verification. Most of the HISC
conditions can be verified efficiently using existing methods for
compositional verification, but a few are more challenging. This paper shows how these more challenging conditions can be expressed equivalently as generalized nonblocking
problems, so the compositional approach for generalized nonblocking developed by the authors in (Malik and Leduc 2009) is applicable. This makes all the HISC conditions amenable for compositional verification, considerably increasing the size of systems that can be handled using the framework.

Supremal Normal Sublanguages in Hierarchical Supervisory Control

15:10 - 15:30
Authors:
Abstract
Topics: (Finite-)State Automata
In this paper, we study hierarchical supervisory control with partial observations. In particular, we are interested in preservation of supremal normal and supremal controllable and normal sublanguages from the abstracted system (high level) in the original (low level) system. Sufficient conditions are formulated under which the supremal normal or the supremal controllable and normal sublanguage computed at the high level (for the abstracted plant) is implementable at the low level, i.e., in the original plant.

Supervisory Control based on Multi-face Modeling of Discrete Event Systems

15:30 - 15:50
Authors:
Abstract
Topics: (Finite-)State Automata
This paper reports a supervisory control design methodology based on the multi-face modeling of discrete-event systems in order to allow rapid prototyping and flexible implementation of controllers for reactive systems. Although Supervisory Control Theory assures that the closed loop system meets the prescribed requirements, it uses ordinary finite state machines as process models, which results in complicated and large-scale controllers. A new modeling methodology simplifies modeling by introducing functional models based on tasks, which allow the reduction of component models. The paper presents a multi-level supervisory control architecture for systems modeled in the framework and derives the properties of the overall control system. Implementational propositions for such supervisory architectures are also given.
MoE1:
Distributed Estimation and Fault Diagnosis
16:10 - 17:30
H 0110
Chair: Jan van Schuppen

A New Protocol for the Decentralized Diagnosis of Labeled Petri Nets

16:10 - 16:30
Authors:
Abstract
Topics: Petri nets
In this paper we deal with the problem of failure diagnosis of
discrete event systems with decentralized information. The
decentralized architecture that we use is composed by a set of sites
communicating their diagnosis information with a coordinator that is
responsible of detecting the occurrence of failures in the system.
In particular, first we present a protocol that defines the
communication rules between the sites and the coordinator. Secondly,
we prove that this protocol does not produce false alarms. Moreover,
we give sufficient conditions for diagnosability based on the notion
of failure ambiguous strings. Finally, we compare the protocol here
presented with other two protocols that we presented in a previous
work.

Distributed State Estimation for Hybrid and Discrete Event Systems Using l-Complete Approximations

16:30 -16:50
Authors:
Abstract
Topics: (Finite-)State Automata
The topic of this paper is distributed state estimation for
time-invariant systems with finite input and output spaces. We
assume that the system under investigation can be realised by a
hybrid I/S/O-machine, where some of the discrete states may also
represent failure modes. Our approach is based on previous work,
e.g., cite{MoorScl,MoorJdeds}, where $l$-complete approximations
were proposed as discrete event abstractions for hybrid dynamical
systems. In particular, it has been shown that $l$-complete
approximations can be used to provide set-valued estimates for the
unknown system state. Estimates are conservative in the sense that
the true state can be guaranteed to be contained in the set-valued
estimate. In this contribution, we show that for a class of hybrid
systems the same estimate can be obtained via a distributed, or
decentralised, approach involving several less complex
approximations, which are run in parallel. For a larger class of
systems, it can be shown that this approach provides an outer
approximation of the estimate provided by a monolithic $l$-complete
estimator. The proposed procedure implies significant computational
savings during estimator synthesis, with an only modest increase in
on-line effort. The latter is a result of "assembling" the global
estimate from the available local estimates. The resulting
computational trade-off is explicitly discussed.

An Unifying Decision-Making Framework in Discrete-Event Systems: Application to Centralized and Decentralized Control, Diagnosis and Prognosis

16:50 - 17:10
Authors:
Abstract
Topics: Supervisory Control
We develop a decision-making framework for DES, which is unifying in two ways. Firstly, it unifies the architectures: we develop a decision-making system for a generic well-formed architecture; and then, we specialize the framework for centralized and decentralized architectures. Secondly, it unifies supervisory control, diagnosis and prognosis: we develop a framework for a generic well-formed decision-maker; and then, we apply the framework to the three subjects. We hope that this unifying framework will contribute to a better understanding of the decision-making mechanism, and will promote its development.

An Optimized Algorithm for Diagnosability of Component-based Systems

17:10 - 17:30
Authors:
Abstract
Topics: (Finite-)State Automata
Diagnosability is a crucial system property that determines at design stage how accurate any diagnosis algorithm can be on a partially observable system. The existence of two indistinguishable behaviors, i.e. holding the same observations, with exactly one of them containing the fault violates the diagnosability property. A classical approach for diagnosability verification consists in constructing a finite state machine called twin plant to search for a path representing such indistinguishable behaviors, called a critical path. To avoid the unrealistic hypothesis about the monolithic model of a complex system, recent work constructs local twin plants and then incrementally synchronizes some of them until diagnosability is decided without computing the impractical global twin plant. In this paper, we optimize the distributed approach by abstracting necessary and sufficient diagnosability information from local twin plants to check the existence of critical paths. Thus diagnosability can be analyzed with as small search space as possible. Furthermore, our approach describes how to improve the diagnosis algorithm by using our diagnosability results in a formal way when the system is verified to be diagnosable. Finally, when the system is not diagnosable, the algorithm returns some useful information about its indistinguishable behaviors, which can help in upgrading system diagnosable level.
MoE2:
Estimation and Control for Max-Plus and Min-Plus Systems
16:10 - 17:50
H 0112
Chair: Sébastien Lahaye
Co-Chair: Ton J. J. van den Boom

On Proportional Controller in (Min, +) Algebra

16:10 - 16:30
Authors:
Abstract
Topics: Max-Plus Algebra
A feedback control design method for (min, +)-linear continuous systems is proposed. The controller is proportional, the resulting control law increases the tracking performance of the system while minimizing the Work In Process (WIP). As in classical system theory, the tuning of the controller is very simple. Additive disturbances acting upon the system are also considered.

Trajectory Tracking Control of a Timed Event Graph with Specifications Defined by a P-time Event Graph: On-line and Off-line Aspects.

16:30 - 16:50
Authors:
Abstract
Topics: Max-Plus Algebra
The topic of this paper is the on-line trajectory tracking control on a
sliding horizon of Timed Event Graphs with specifications defined by a P-time
Event Graph. Making the most of the specific structures of the systems, the
CPU time of the on-line procedure is drastically reduced with two techniques:
The use of specific algorithms of the graph theory instead of generic
algorithms; an off-line preparation which avoid the useless repetition of the
same calculations. As
a consequence, the approach can deal with long horizons and important
systems and the application field of the trajectory tracking control is
expanded.

Max-Plus Linear Observer: Application to Manufacturing Systems

16:50 - 17:10
Authors:
Abstract
Topics: Petri nets
This paper deals with the observer design for max-plus linear systems. The approach
is based on the residuation theory which is suitable to deal with linear mapping inversion in
idempotent semiring. An illustrative example allows to discuss about a practical implementation.

Control of Cyclically Operated High-Throughput Screening Systems

17:10 - 17:30
Authors:
Abstract
Topics: Petri nets, Max-Plus Algebra, Scheduling, Manufacturing Systems
In previous work we have shown how (max, +)-algebra can be used to model cyclically operated high-throughput screening systems. In this paper the system is modeled in a two-dimensional dioid MaxMin[[γ,δ]]. A controller is determined using residuation theory. The resulting control guarantees just-in-time operation of the plant. A small example is used to demonstrate the approach to model and control HTS systems. To apply the determined controller, it is rewritten in terms of counter-functions. A simulation of the system with and without controller is given and results are discussed.

Max-Consensus in a Max-Plus Algebraic Setting: The Case of Switching Communication Topologies

17:30 - 17:50
Authors:
Abstract
Topics: Max-Plus Algebra
Because of their use for distributed decision making, consensus algorithms have attracted a lot of interest in recent years. Coordination between entities requires that they share information over a network, and develop a consistent view regarding objectives and relevant information on the environment, i.e., reach a consensus. In practice, communication topologies may change over time, either as a consequence of disturbances or in an attempt to improve performance. Max-consensus is a specific consensus algorithm, which is particularly important in applications such as minimum time rendezvous and leader election. In this contribution, we propose an approach to analyze max-consensus algorithms in time-variant communication topologies, which is based on max-plus algebra. In this framework max-consensus algorithms become piecewise linear and may be analyzed easily. The conditions needed to achieve max-consensus and the convergence rate of the algorithm for different communication graphs are studied. This contribution is an extension of a previous work of the authors, where max-consensus was studied for time-invariant communication topologies.

Tuesday, August 31, 2010

TuP:
Coordination of Traffic Networks
09:00 - 10:00
H 0110
Speaker: René Boel
Chair: Alessandro Giua
Abstract

Transportation problems provide a rich class of case studies for investigating the implementability of supervisory and distributed control ideas. This talk will abstract a few problems from this area into distributed supervisory control problems. Case studies are taken from on-ramp control for freeways, coordinated traffic light control in urban traffic, and control of autonomous vehicles executing task with a deadline while avoiding collisions.

Each of these problems can be modelled as a timed automaton or a piecewise affine model, with timed Petri nets and fluid Petri nets as concise graphical representations. Reachability analysis, safety analysis, and observer design for these models can be reduced to some standard algorithms, at least conceptually. Specifications must be satisfied by designing supervisory controller limiting the actions of the different components in the network.

The problem becomes particularly challenging when local controllers in each vehicle or in each intersection in the traffic system have only limited communication channels for coordinating their actions. It will be shown for a number of interesting cases how distributed controllers can be designed achieving good coordination of the local controllers.
TuM1:
Diagnosis, Identification and Testing
10:30 - 12:30
H 0110
Chair: Stefan Haar
Co-Chair: Shigemasa Takai

An Identification Technique for Timed Event Systems

10:30 - 10:50
Authors:
Abstract
Topics: (Finite-)State Automata
Compared to time-driven systems, few tools are available for identification of timed event-driven systems. Here we address the identification problem for those systems that require not only proper ordering, but also correct timing, of input and output events for their complete description. First we review well-known results from computational learning theory, noting their roots in classical systems theory and interpreting their relevance to the identification problem. Next, as a prerequisite to identification, we introduce a simple formalism for modeling timed deterministic event-based system behavior that is also well-adapted to identification. Then we present the main result of the paper, an algorithm that under appropriate conditions computes an automaton whose behavior reliably imitates a given timed event system. Simulation results illustrate best-case and worst-case identification conditions.

On-line Detection and Sensor Activation for Discrete Event Systems

10:50 - 11:10
Authors:
Abstract
Topics: (Finite-)State Automata
This paper investigates on-line detection and sensor activation problem of discrete event systems. The objective is to derive minimal sensor activation policy while preserving strong detectability and strong periodic detectability. After reviewing strong detectability and strong periodic detectability, we introduce a new concept called distinguishability. Distinguishability is used for two purposes. First, it is used to characterize detectability. Secondly, it is used for on-line state estimation and sensor activation. To this end, we proposed an on-line state estimation framework which estimates the state of the system. Sensor activation is then achieved based on the state estimation. State-estimation-based sensor activation has some interesting and surprising properties that we will investigate in this paper. In particular, we introduce a new concept called coherence that plays a key role in state-estimation-based sensor activation. To obtain state-estimation-based sensor activation policy that is minimal and coherent, two algorithms are derived. One algorithm is for strong detectability. It minimizes sensor activation while preserving distinguishability, and hence strong detectability. The other algorithm deals with strong periodic detectability. For strong periodic detectability, a new property called information-preserving must be incorporated. Both algorithms are of polynomial complexity.

SIC-Testability of Sequential Logic Controllers

11:10 - 11:30
Authors:
Abstract
Topics: Reactive Systems
SIC (Single Input Change) test sequences must be privileged for conformance test of logic controllers, to prevent from erroneous test results when the test-bench and the implementation under test are not synchronized. This paper proposes first a definition of the SIC-testable part of a sequential specification model, i.e. the part of the model that can be tested by using a sequence starting from the initial state and for which only one input can change at one at the same time. Then, an algorithm to determine the SIC-testable part is given; if this part is the whole specification, the specification model is declared totally SIC-testable. Once the SIC-testable part obtained, a SIC sequence for conformance test of an implementation of this part can be generated. These contributions are exemplified on an example.

Computation of Projections for the Abstraction-based Diagnosability Verification

11:30 - 11:50
Authors:
Abstract
Topics: (Finite-)State Automata
The verification of language-diagnosability (LD) for discrete event systems (DES) generally requires the explicit evaluation of the overall system model which is infeasible for practical systems. In order to circumvent this problem, our previous work proposes the abstraction-based LD verification using natural projections that fulfill the loop-preserving observer (LPO) property. In this paper, we develop algorithms for the verification and computation of such natural projections. We first present a polynomial-time algorithm that allows to test if a given natural projection is a loop-preserving observer. Then, we show that, in case the LPO property is violated, finding a minimal extension of the projection alphabet such that the LPO condition holds is NP-hard. Finally, we adapt a polynomial-time heuristic algorithm by Feng and Wonham for the efficient computation of loop-preserving observers.

Robust Failure Diagnosis of Partially Observed Discrete Event Systems

11:50 - 12:10
Authors:
Abstract
Topics: Diagnosis and Estimation
In this paper, we study robust failure diagnosis of
partially observed discrete event systems.
Given a set of possible models,
each of which has its own nonfailure specification,
the objective is to synthesize a single diagnoser
such that, for all possible models, it detects
any occurrence of a failure within a uniformly bounded number of steps.
We call such a diagnoser a robust diagnoser.
We introduce a notion of robust diagnosability, and prove that
it serves as a necessary and sufficient condition for the existence
of a robust diagnoser.
We then present an algorithm for verifying the robust diagnosability condition.
Moreover, we show that a robust diagnoser can be synthesized
as an online diagnoser.

What Topology Tells us about Diagnosability in Partial Order Semantics

12:10 - 12:30
Authors:
Abstract
Topics: Petri nets
From a partial observation of the behaviour of a labeled Discrete Event Systems, fault Diagnosis strives to determine whether or not a given ``invisible'' fault event has occurred. The diagnosability problem can be stated as follows: does the labeling allow for an outside observer to determine the occurrence of the fault, no later than a bounded number of events after that unobservable occurrence ? In concurrent systems, partial order semantics adds to the difficulty of the problem, but also provides a richer and more complex picture of observation and diagnosis. In particular, it is crucial to clarify the intuitive notion of "time after fault occurrence". To this end, we will use a unifying metric framework for event structures, providing a general topological description of diagnosability in both sequential and nonsequential semantics for Petri nets.
TuM2:
Probabilistic Discrete Event Systems
10:30 - 12:30
H 0112
Chair: Eric Fabre
Co-Chair: Bernd Heidergott

Use of a Metric in Supervisory Control of Probabilistic Discrete Event Systems

10:30 - 10:50
Authors:
Abstract
Topics: Supervisory Control
This work represents a natural extension of our work on optimal probabilistic supervisory control of probabilistic discrete event systems (PDESs). In that work, a pseudometric on the initial states of two probabilistic generators that represent probabilistic systems is used to measure the distance between two systems. The pseudometric is given a fixed point characterization.
This paper gives a logical characterization of the same pseudometric such that the distance between two systems is measured by a formula that distinguishes between the systems the most.
A trace characterization of the pseudometric is then derived from the logical characterization. Further, the solution of the problem of approximation of a given probabilistic generator with another generator of a prespecified structure is suggested such that the new model is as close as possible to the original one in the pseudometric. The significance of the approximation is then discussed.

On Almost-Sure Properties of Probabilistic Discrete Event Systems

10:50 - 11:10
Authors:
Abstract
Topics: Petri nets
Although randomization often increases the degree of flexibility in system design, analyzing system properties in the probabilistic framework introduces additional difficulties and challenges in comparison with their nonprobabilistic counterparts. In this paper, we focus on probabilistic versions of two problems frequently encountered in discrete event systems, namely, the reachability and forbidden-state problems. Our main concern is to see whether there exists a non-blocking or fair control policy under which a given finite- or infinite-state system can be guided to reach (or avoid) a set of goal states with probability one. For finite-state systems, we devise algorithmic approaches which result in polynomial time solutions to the two problems. For infinite-state systems modelled as Petri nets, the problems are undecidable in general. For the class of persistent Petri nets, we establish a valuation approach through which the convergence behavior of a system is characterized, which in turn yields solutions to the reachability and forbidden-state problems.

On the Construction of Probabilistic Diagnosers

11:10 - 11:30
Authors:
Abstract
Topics: (Finite-)State Automata
This paper revisits the notions of observer and diagnoser, and adapts them to probabilistic automata, in a setting of weighted automata computations. In the non stochastic case, observers and diagnosers are obtained by standard elementary steps, as state augmentation, epsilon-reduction and determinization. It is shown that these steps can be adapted to probabilistic automata, and algorithms to perform them efficiently are provided. In particular, the determinization is related to a standard filtering equation that recursively computes the conditional distribution of the current state given past observations. New notions of probabilistic observers and diagnosers are provided and compared to previous constructions, and simpler derivations of the latter are proposed.

A Geometric Approach for the Homothetic Approximation of Stochastic Petri Nets

11:30 -11:50
Authors:
Abstract
Topics: Petri nets
Reliability analysis is often based on stochastic discrete event models like stochastic Petri Nets. For complex dynamical systems with numerous components, analytical expressions of the steady state are tedious to work out because of the combinatory explosion with discrete models. For this reason, fluidification is an interesting alternative to estimate the asymptotic behaviour of stochastic processes with continuous Petri nets. Unfortunately, the asymptotic mean marking of stochastic and continuous Petri nets with same structure and same initial marking are mainly often different. This paper shows that this difficulty is related to the partition in regions of the reachability state space. A geometric approach is developed to characterize the regions and to get a partial homothetic approximation of the stochastic steady state.

Gradient Estimation for Quantiles of Stationary Waiting Times

11:50 -12:10
Authors:
Abstract
Topics: Performance Evaluation
Quantiles of customer based performance characteristics have been adopted in many areas for measuring the quality of service. Recently, sensitivity analysis of quantiles has attracted quite some attention. Sensitivity analysis of quantiles is particularly challenging as quantiles cannot be expressed
as the expected value of some sample performance function, and it is therefore not evident how standard gradient estimation methods can be applied. While sensitivity analysis of quantiles of waiting times for static or fixed time horizon problems is well understood, quantile estimation for stationary waiting times remains an open question. This paper will close this gap and will provide a framework for gradient estimation for quantiles of stationary waiting times.

A Rollout Method for Finite-Stage Event-Based Decision Processes

12:10 - 12:30
Authors:
Abstract
Topics: Optimization
Event-based decision process (EDP) has provided a general framework for many event-based control, decision making, and optimization problems. Since the number of events could increase only linearly w.r.t. the system scale, EDP provides a computationally feasible way for many problems, which are time-consuming to solve in the Markov decision process (MDP) framework. Because the event sequence usually is not Markovian, policies that only depend on the current observable event usually are not optimal. In this paper, we develop a rollout method for finite-stage EDP, which uses simulation under a base policy to estimate the performances of action candidates. We show that this leads to a policy better than the base policy. This rollout method is easy to implement. The advantage is also demonstrated through a node activation policy optimization problem in wireless sensor network.
TuA1:
Invited Session:
Towards Application of Supervisory Control - from Modeling, through Synthesis, to Implementation (Part I)
14:30 - 15:50
H 0110
Organisers: Rong Su
Organisers: Walter Murray Wonham
Chair: Rong Su
Co-Chair: Knut Åkesson

Applied Supervisory Control for a Flexible Manufacturing System

14:30 - 14:50
Authors:
Abstract
Topics: (Finite-)State Automata
This paper presents a case study in the design and implementation of a discrete event system (DES) of real-world complexity. Our DES plant is a flexible manufacturing system (FMS) laboratory model that consists of 29 interacting components and is controlled via 107 digital signals. Regarding controller design, we apply a hierarchical and decentralised synthesis method from earlier work in order to achieve nonblocking and safe closed-loop behaviour. Regarding implementation, we discuss how digital signals translate to discrete events from a practical point of view, including timing issues. The paper demonstrates how both, design and implementation, are supported by the open-source software tool libFAUDES.

Supervisory Control of Software Execution for Failure Avoidance: Experience from the Gadara Project

14:50 - 15:10
Authors:
Abstract
Topics: Petri nets
We discuss our experience in the Gadara project, whose objective is to control the execution of software to avoid potential failures using discrete-event control techniques.
We summarize our accomplishments so far and discuss future challenges.
After initial work on safety of workflow scripts via supervisory control techniques,
we have focused our efforts on deadlock avoidance in multithreaded C programs that use locking primitives to control access to shared data.
We describe our efforts at automating the construction of the model, in the form of automata or Petri nets.
In the case of multithreaded C programs,
the resulting models characterize a new class of resource-allocation Petri nets called Gadara nets.
These nets enjoy structural properties that facilitate the synthesis of liveness-enforcing control policies that are maximally-permissive.
We describe our strategy for run-time implementation of these control policies by a technique known as code instrumentation.
It is hoped that the lessons learned so far in the Gadara project will be useful in other application areas and will suggest avenues for future theoretical investigations.

Optimal Deadlock Avoidance for Complex Resource Allocation Systems through Classification Theory

15:10 - 15:30
Authors:
Abstract
Topics: Supervisory Control
Most of the past research on the problem of deadlock avoidance for sequential complex resource allocation systems (RAS) has acknowledged the fact that the maximally permissive deadlock avoidance policy (DAP) possesses super-polynomial complexity for most RAS classes, and it has resorted to solutions that trade off maximal permissiveness for computational tractability. In this work, we seek the effective implementation of the maximally permissive DAP for a broad spectrum of RAS, by distinguishing between the "off-line" and the "on-line" computation that is required for the specification of this policy, and developing a representation of the derived result that will require minimal on-line computation. The particular representation that we adopt is that of a compact classifier that will effect the underlying dichotomy of the reachable state space into safe and unsafe subspaces. Through a series of reductions of the posed classification problem, we are also able to attain extensive reductions in the computational complexity of the off-line task of the construction of the sought classifier. A series of computational experiments demonstrate the efficacy of the proposed approach and establish its ability to provide tractable implementations of the maximally permissive DAP for problem instances significantly beyond the capacity of any other approach currently available in the literature.

Supervisor Computation and Representation: A Case Study

15:30 - 15:50
Authors:
Abstract
Topics: (Finite-)State Automata
When supervisory control theory is applied to industrial problems the need for a more expressive modeling formalism than plain event based automata is crucial. The models are typically built in a bottom-up structure where multiple sub-plant and sub-specifications together compose the full plant and specification, respectively. Typically, the enabling of an event in a sub-model may depend on the state of other sub-models. The standard approach is to synchronize on shared events. However, to build models of large industrial problems with complex constraints between sub-models are beyond many engineers abilities. One attempt to deal with this problem is to extend the plain automata with variables and allow guard conditions and action functions to be associated with transitions. In the paper the strengths and weaknesses of one such formulation, that is formulated to fit well together with the standard supervisory control theory, is discussed. A related problem is how to represent the result after the synthesis procedure, i.e., the supervisor. In the paper we present an approach where the supervisor may be represented as extended guard conditions on the original sub-models together. This is preferable both from a users perspective, since the result of the synthesis procedure may be more comprehensible for a human user, but also from the computers perspective, since the approach allows for efficient representation of complex supervisors. Both the modeling formalism based on extended finite automata and the way to represent the supervisor as extended guard conditions have been implemented in a supervisory control tool.
TuA2:
Modelling and Analysis of Max-Plus Systems
14:30 - 15:50
H 0112
Chair: Jan Komenda
Co-Chair: Jean-Jacques Lesage

Linear Time-Varying (Max,+) Representation of Conflicting Timed Event Graphs

14:30 - 14:50
Authors:
Abstract
Topics: Petri nets
Timed Event Graphs (TEGs) are a specific class of Petri nets that have been thoroughly studied given their useful linear state representation in (Max,+) algebra. Unfortunately, TEGs are generally not suitable for modeling systems displaying resources sharing (or conflicts). In this paper, we show that if a system with conflicts is modeled using an extended class of TEGs: Conflicting Timed Event Graphs (CTEGs), it is quite possible to obtain an equivalent (Max,+) representation. More precisely, we prove that the evolution of a CTEG satisfies linear time-varying (Max,+) equations. In case of cyclic CTEGs, which are a natural model of many repetitive systems, we provide a standard time-invariant (Max,+) representation. Finally, a practical example (a Jobshop) is used for illustration to exhibit the interest of this investigation.

Comparison of Different Classes of Service Curves in Network Calculus

14:50 - 15:10
Authors:
Abstract
Topics: Max-Plus Algebra
In envelope-based models for worst-case performance evaluation like Network Calculus
or Real-Time Calculus, several types of service curves have been introduced to
quantify some deterministic service guarantees. This paper studies the
expressiveness of those different definitions of service curves. We revisit the
hierarchy ranging from the most restrictive definition linked to "variable capacity nodes"
to the most general definition of "simple service curves". We state the conditions when
the different definitions overlap and discuss the existence of canonical descriptions
for systems specified through those definitions.

Modeling of Interval P-time Petri Nets using Dioid Algebra

15:10 - 15:30
Authors:
Abstract
Topics: Petri nets
In this paper 1-safe interval P-time Petri nets are described using
linear description in an interval like idempotent semiring.
This semiring, which is just the product of (max,+) and
(min,+) semirings, enables linear letter driven description similar to the one
known for timed Petri nets.
Examples illustrating our approach show also an application of this description
to dead token detection.

Synchronous Composition of Interval Weighted Automata

15:30 - 15:50
Authors:
Abstract
Topics: Petri nets
Interval weighted automata are introduced as automata with weights in a product dioid (idempotent semiring). They constitute an extension of (max,+) automata since they enable us to model temporal constraints (instead of exact durations) for transitions. Their synchronous composition, which coincides with the synchronous product of underlying (one clock) timed automata, results in multi-event interval weighted automata, whose behaviors are studied. Our approach is illustrated by an example.
TuE1:
Invited Session:
Towards Application of Supervisory Control - from Modeling, through Synthesis, to Implementation (Part II)
16:10 - 17:10
H 0110
Organisers: Rong Su
Organisers: Walter Murray Wonham
Chair: Rong Su
Co-Chair: Spiridon Reveliotis

Automated Controllability and Synthesis with Hierarchical Set Decision Diagrams

16:10 - 16:30
Authors:
Abstract
Topics: Reactive Systems
Computation of a maximally permissive controller in the Ramadge-Wonham framework promises a general solution to automatically design a controller for a discrete event system, when it exists. However, like for all similar model-checking approaches, the combinatorial explosion of the state space remains a practical issue.
The work presented here investigates how to exploit both hierarchical modeling and a symbolic modelchecking engine to tackle this problem. This engine is based on a powerful class of Decision Diagrams called Hierarchical Set Decision Diagrams combined with a framework called Instantiable Transition Systems, in order to describe hierarchical models. To implement the controller activity, we propose to store the set of safe states, computed offline, as a decision diagram in the controller software, allowing to take decisions on-line.
We run a prototype tool on several benchmark examples, including a problem of automated guided vehicles and a train crossing version with explicit discrete time. Results suggest good scalability, although the procedure is computationally intensive.

Coordination of Resources using Generalized State-Based Requirements

16:30 - 16:50
Authors:
Abstract
Topics: Supervisory Control
Control and coordination is an important aspect of the development of complex machines due to an ever increasing demand for better functionality, quality, and performance. We develop a coordinator for maintenance procedures for a high-tech Oce printer that eliminates undesired behavior which stems from unrestricted interaction of its distributed components. To this end, we extend and employ a model-based engineering framework for supervisory controller synthesis. We generalize standard state-based control requirements to increase modeling convenience. We model the use case with 23 generalized state-based requirements, which translate to 500+ requirements in the original form.

Application of Supervisory Control Theory to Theme Park Vehicles

16:50 - 17:10
Authors:
Abstract
Topics: Supervisory Control
Due to increasing system complexity, time-to-market and development costs reduction, new engineering processes are required. Model-based engineering processes are suitable candidates because they support system development by enabling the use of various model-based analysis techniques and tools. As a result, they are able to cope with complexity and have the potential to reduce time-to-market and development costs. Moreover,
supervisory control synthesis can be integrated in this setting, which can further contribute to the development of control systems. To evaluate the applicability of recently developed supervisor synthesis techniques and to show how they can be integrated in an engineering process, a theme park vehicle is chosen as a case study. The supervisor synthesized for the theme park vehicle has successfully been implemented and integrated in the existing resource-control platform.
TuE2:
Applications I
16:10 - 17:10
H 0112
Chair: Feng Lin
Co-Chair: Philippe Darondeau

Rotary-Wing UAV Mission Planning Aided by Supervisory Control

16:10 - 16:30
Authors:
Abstract
Topics: (Finite-)State Automata
In this paper, a method based on the supervisory control theory for hybrid systems is proposed to the mission planning of rotary-wing unmanned aerial vehicles (UAV). First, the mission is modeled by a hybrid automaton; then, by means of reachability techniques, a condition/event automaton, that represents the discrete-trace behavior of the hybrid automaton, is computed; and then the supervisory control theory is applied to obtain a discrete-trace behavior that avoids, under maximal permissiveness, the undesirable flight conditions, namely, the lack of fuel during the flight, the violation of time on target restrictions and the violation of trajectory margins. Computational tools were developed and a case-study is presented.

Augmenting Petri Nets to Model Health-Care Protocols

16:30 - 16:50
Authors:
Abstract
Topics: Petri nets
An outbreak of an infectious illness can be devastating for a population. Once confirmed, local health-care organizations will attempt to reduce the spread of the disease by adopting a protocol in response. Modelling health-care protocols requires the inclusion of both timing and probability constraints. Choice-point nets, a form of augmented Petri nets, are ideal for the task. In this data structure, time is associated with event-based transitions that may result in several possible outcomes, each of which is given a probability of occurrence. These nets may be analyzed by unravelling them into finite-state automata. By translating questions about the protocol into the mathematical language of the net, recursive algorithms may then be employed to provide health-care professionals with answers.

Fail-Safe Signalization Design for a Railway Yard: A Level Crossing Case

16:50 - 17:10
Authors:
Abstract
Topics: Petri nets
Level crossings (grade crossings or railroad crossings) are one of the most crucial parts of the railway lines as two different types of transportation intersect at these points. Human failures including ignorance of warning signs, device troubles or carelessness can easily result in accidents especially at such cross-sections. In order to decrease the possibility of accidents on level crossings, several standards have been developed. In accordance with these standards, formal methods are required to be used specially in the development of interlocking systems that control safe operation of such crossings. In this study, a railway yard with a level crossing is modeled by Automation Petri Nets in order to design a fail-safe signalization system. A SCADA testbed is also developed to test several possible failure situations. Verified design will be then establish to an unsignalled railway station known as MithatpaÅŸa to use for Turkish State Railways.

Wednesday, September 1, 2010

WeP:
Interfaces for Control Components
09:00 - 10:00
H 0110
Speaker: Rajeev Alur
Chair: Stéphane Lafortune
Abstract

Modern software engineering heavily relies on clearly specified interfaces for separation of concerns among designers implementing components and programmers using those components. The need for interfaces is evident for assembling complex systems from components, but more so in control applications where the components are designed by control engineers using mathematical modeling tools and used by software executing on digital computers. However, the notion of an interface for a control component must incorporate some information about timing, and standard programming languages do not provide a way of capturing such resource requirements.

This talk will describe how finite automata over infinite words can be used to define interfaces for control components. When the resource is allocated in a time-triggered manner, the allocation from the perspective of an individual component can be described by an infinite word over a suitably chosen alphabet. The control engineer can express the interface of the component as an omega-regular language that contains all schedules that meet performance requirement. The software must ensure, then, that the runtime allocation is in this language. The main benefit of this approach is composability: conjoining specifications of two components corresponds to a simple language-theoretic operation on interfaces. We have demonstrated how to automatically compute automata for performance requirements such as exponential stability and settling time for the LQG control designs. The framework is supported by a toolkit, RTComposer, that is implemented on top of Real Time Java. The benefits of the approach will be demonstrated using applications to wireless sensor/actuator networks based on the WirelessHART protocol and to distributed control systems based on the Control Area Network (CAN) bus.
WeM1:
Extensions of Supervisory Control I
10:30 - 12:10
H 0110
Chair: Ryan Leduc
Co-Chair: Robi Malik

Sampled-Data Supervisory Control

10:30 - 10:50
Authors:
Abstract
Topics: (Finite-)State Automata
This paper focuses on issues related to implementing timed discrete-event systems (TDES)
supervisors, and the concurrency and timing delay issues involved. In particular, we examine issues related to implementing TDES as sampled-data (SD) controllers. An SD controller is driven by a periodic clock and sees the system as a series of inputs and outputs. On each clock edge (tick event), it samples its inputs, changes states, and updates its outputs. We extend TDES controllability to a new definition, SD controllability, which captures several new properties that are useful in dealing with concurrency issues, as well as makes it easier to translate a TDES supervisor into an SD controller. We present controllability and nonblocking results for SD controllers. Finally, we apply our method to a small, flexible, manufacturing system from the literature.

Fault-Tolerant Control of Nondeterministic Input/Output Automata subject to Actuator Faults

10:50 - 11:10
Authors:
Abstract
Topics: (Finite-)State Automata
This paper presents concepts dealing with fault-tolerant control of discrete-event systems (DES) modeled by Input/Output (I/O) automata. It answers the question how to reconfigure the controller of a plant which is subject to actuator faults. The notion of the redundancy degree is addressed and formalized in an I/O automata framework. The reconfigurability condition which is essential in a reconfiguration scheme is investigated and a new method for checking the feasibility of a specification for a faulty system is introduced. A control design method, from which a deterministic baseline controller can be derived from a nondeterministic specification automaton, is presented. The diagnoser is assumed to be able to detect and identify actuator faults which occurred in the system. An example demonstrates the applicability of the concepts.

Multicriteria Optimal Reconfi guration for Fault-tolerant Real-time Tasks

11:10 - 11:30
Authors:
Abstract
Topics: (Finite-)State Automata
We propose a technique to design and optimize fault-tolerant
real-time distributed systems. It is based on discrete controller
synthesis with optimal synthesis on bounded paths. We consider that
the execution cost of each task is one criteria and we explore
different criteria combinations for multi-criteria optimization:
aggregation, hierarchization, and transformation.

Compositional Nonblocking Verification Using Annotated Automata

11:30 - 11:50
Authors:
Abstract
Topics: (Finite-)State Automata
This paper proposes to enhance compositional verification of the nonblocking property of discrete event systems by introducing annotated automata. Annotations store nondeterministic branching information, which would otherwise be stored in extra states and transitions. This more succinct representation makes it easier to simplify automata and enables new efficient means of abstraction, further reducing the size of automata to be composed and thus the size of the synchronous product state space encountered in verification. The abstractions proposed are of polynomial complexity, and they have been successfully applied for nonblocking verification of the same set of large-scale industrial examples as used in related work.

Techniques for the Parametrization of Discrete-Event System Templates

11:50 - 12:10
Authors:
Abstract
Topics: (Finite-)State Automata
Two techniques for the parametrization of templates in the template design methodology are introduced. First, the use of finite-state automata extended with variables is demonstrated. This kind of parametrization allows one to vary the occurrences of events by varying a parameter. Second, a new way of parametrizing templates is proposed, named compositional parametrization. With this technique, a template consists of the composition of a number of structurally identical components whose events are indexed differently, depending on a parameter. This kind of parametrization allows one to vary the structure and event set of the template by varying a parameter. An enhancement of compositional parametrization with the use of special selector transitions is also discussed. This extension allows one to model interactions between components which depend on the total number of components in a composition and thus cannot be modelled by simple parametrization of event indices. With the choice of a specific parameter, regular finite-state automaton models are obtainable from the templates parametrized with any of the aforementioned techniques. Thus, such parametrized templates can be easily introduced in the template design modelling environment and they integrate seamlessly with the supervisory control framework. Motivating examples to illustrate the application of template parametrization are provided.
WeM2:
Invited Session:
Max-plus algebra and max-plus-linear systems
10:30 - 12:10
H 0112
Organisers: Laurent Hardouin
Organisers: Jean-Louis Boimond
Chair: Laurent Hardouin
Co-Chair: Jean-Louis Boimond

An Approximation Approach for Model Predictive Control of Stochastic Max-Plus Linear Systems

10:30 - 10:50
Authors:
Abstract
Topics: Max-Plus Algebra
Model Predictive Control (MPC) is a model-based control method based on a receding horizon approach and online optimization. In previous work we have extended MPC to a class of discrete-event systems, namely the max-plus linear systems, i.e., models that are "linear" in the max-plus algebra. Lately, the application of MPC for stochastic max-plus-linear systems has attracted a lot of attention. At each event step, an optimization problem then has to be solved that is, in general, a highly complex and computationally hard problem. Therefore, the focus of this paper is on decreasing the computational complexity of the optimization problem. To this end, we use an approximation approach that is based on the p-th raw moments of a random variable. This method results in a much lower computational complexity and computation time while still guaranteeing a good performance.

Modeling and Control of Legged Locomotion via Switching Max-Plus Systems

10:50 - 11:10
Authors:
Abstract
Topics: Max-Plus Algebra
We present a class of gait generation and control algorithms based on the Switching Max-Plus modeling framework that allow for the synchronization of multiple legs of walking robots. Transitions between stance and swing phases of each leg are modeled as discrete events in a system described by max-plus-linear state equations. Different gaits can be systematically generated and interleaved during motion by switching between different system matrices. We show that such gait switching can be done in an optimal way, minimizing the tip leg velocity variance for all legs simultaneously touching the ground.

Asymptotic Throughput of Stochastic Max-Plus Linear Systems

11:10 - 11:30
Authors:
Abstract
Topics: Max-Plus Algebra
In a Max-plus linear system every coordinate is known to have an
asymptotic cycle time. For their stochastic counterpart, this is only
true for the backward systems.
We investigate the conditions under which this fact implies the
existence of asymptotic cycle time for the original system and show
that there are two types of obstructions.
This gives a necessary and sufficient condition for i.i.d. systems and
a bunch of sufficient conditions under weaker assumptions.

A Frequency-Domain Approach for Max-Plus Linear Systems

11:30 - 11:50
Authors:
Abstract
Topics: Max-Plus Algebra
This paper surveys recent investigations on a frequency-domain
approach to study max-plus linear systems, which can be used to
model queueing systems, communication networks, and manufacturing
systems. The challenging problem for a well-developed
frequency-domain theory of such systems is the lack of inverse
operations. This paper proposes a frequency-domain approach by
revisiting Kalman's original realization theory for max-plus linear
systems. The main advantage of Kalman's theory is that the
frequency-domain method and the state-variable method merge into a
single framework. Moreover, it introduces the concepts of poles and
zeros as semimodules instead of point poles and zeros, which cannot
be traditionally defined without inverse operations. Moreover, the
pole and zero semimodules can characterize the common Petri net
components in the solutions to the model matching problem.

Control of Uncertain (max,+)-Linear Systems in order to Decrease Uncertainty

11:50 - 12:10
Authors:
Abstract
Topics: Max-Plus Algebra
This paper deals with the control of uncertain (max,+)-linear systems, more precisely those of which parameters are not exactly known but assumed to belong to an interval. In this context, we aim at synthesizing a controller in order to reduce the uncertainty at the output of the controlled system. This study is possible thanks to the residuation theory and relies on solutions of fixed-point equations.
WeA1:
Extensions of Supervisory Control II
13:40 - 15:00
H 0110
Chair: José Cury
Co-Chair: Martin Fabian

Efficient Computation of Observer Projections using OP-Verifiers

13:40 - 14:00
Authors:
Abstract
Topics: Supervisory Control
This paper proposes a procedure to compute abstractions of Discrete Event System
(DES) models with the observer property (OP). The procedure, named OP-Search, is based on
the OP-Verifier algorithm which verifies if a given natural projection has the observer property.
In case OP fails for a projection in Sigma_r of an automaton M, OP-Search modifies M by relabelling
transitions and incorporating the new events in Sigma_r, in a way that the modified natural projection
generates OP-abstractions. Although the OP-Search does not guarantee minimal abstracted
models, it leads in general to very reasonable solutions and is shown to be of lower time complexity
when compared to previous work in the literature.

Modular Specification of Forbidden States for Supervisory Control

14:00 - 14:20
Authors:
Abstract
Topics: (Finite-)State Automata
A method for solving the forbidden state problem in the Supervisory Control Theory framework is presented. In many real-world applications both the plant and specification is given as a set of interacting automata or processes. In this work, we enable specification of forbidden states within such a modular structure. The aim with the method is to make each forbidden modular state combination uncontrollable. It is then possible to use efficient modular synthesis algorithms for calculation of a modular supervisor where the forbidden states are removed.

Supervisory Control for Modal Specifications of Services

14:20 - 14:40
Authors:
Abstract
Topics: (Finite-)State Automata
In the service oriented architecture framework, a modal specification, as defined by Larsen in~cite{Lar89}, formalises how a service should interact with its environment. More precisely, a modal specification determines the events that the server may or must allow at each stage in an interactive session. In this paper, we investigate the adaptation of the supervisory control theory of Ramadge and Wonham to enforce a modal specification (with final states marking the ends of the sessions) on a system modelled by a finite LTS. We
prove that there exists at most one most permissive solution to this control problem. We also prove that this solution is regular and we present an algorithm for the effective computation of the corresponding controller.

Synthesis of Safe Sublanguages satisfying Global Specification using Coordination Scheme for Discrete-Event Systems

14:40 - 15:00
Authors:
Abstract
Topics: (Finite-)State Automata
Decentralized control of discrete-event systems with a global specification and with only local supervisors is a difficult problem. Control synthesis has been solved by K. Rudie and W. M. Wonham in 1987. For global specifications, however, the equivalent conditions may not be met. This paper formulates and solves a control synthesis problem for a generator with a global specification and with a combination of a coordinator and local controllers. Conditional controllability is proven to be an equivalent condition for the existence of such a coordinated controller. A procedure to compute a coordinated controller is provided in this paper.
WeA2:
Applications II
13:40 - 14:40
H 0112
Chair: Georg Frey
Co-Chair: Miryam Barad

Solution of a Multi-Agent Transport Problem by Hybrid Optimization

13:40 - 14:00
Authors:
Abstract
Topics: Hybrid Systems
As reported in earlier work, methods for hybrid optimal control can be used for optimal path planning of multi-agent systems. This paper considers a multi-vehicle transport scenario in which a hybrid model is used to represent the continuous dynamics of the vehicle motion and paths and the dynamics arising from the docking-events between vehicles and a transported object. The decisions on the vehicles' heading and speed as well as on the docking sequence are strongly coupled and require a tailored numeric solution. The paper proposes a hierarchical solution strategy with three layers: on the upper layer a discrete event sequencing problem is solved, the middle determines docking positions and times, and the lower layer provides optimal vehicle paths. By a combination of graph search and embedded continuous optimal control, the efficiency of obtaining (sub-)optimal solutions is improved. The algorithm is illustrated by a scenario in which three vehicles transport one object.

Timed Petri Nets Perspective on Weaving Processes

14:00 - 14:20
Authors:
Abstract
Topics: Petri nets, Manufacturing Systems
This study deals with weaving focusing on the conceptual planning stage during which valid approximation based methods are needed. It introduces a decomposition method, directly derived from Timed Petri Nets (TPN) theories, to calculate the expected utilization of the processing equipment (the looms). The decomposed TPN model enables a quick calculation of the resources expected utilization at steady state thus providing a stick yard against which to verify its long run simulation based estimate.

Keywords:
Weaving, Timed Petri Nets, decomposition, simulation verification

Optimal Vendor-Managed Inventory Policies in Distribution Systems with Discrete-Event Processes

14:20 - 14:40
Authors:
Abstract
Topics: Optimization
The present work deals with distribution systems characterized by discrete-event processes and in which a Vendor-Managed Inventory (VMI) policy is applied. VMI is a supply chain strategy in which the vendor or supplier has the responsibility of managing the customers' inventory and, therefore, the supplier has to plan the replenishment policy taking into account his transportation costs and the customers' inventory costs. In this context, the present work refers to a distribution chain in which the system dynamics is event-driven since the demand and the deliveries are modelled as discrete-event processes. In particular, the focus of this work is on a simple network composed of one supplier and one customer. The main objective is to state an optimization problem in which, once known the asynchronous requests of the customer, the optimal deliveries are determined. Then, an optimal solution procedure is defined and explained by a numerical example.

Overview

Atop
Knut Åkesson
Dirk Abel
Erika Ábrahám
Boussad Addad
Said Amari
Sid Ahmed Attia
Vadim Azhmyakov
Btop
Robert Babuska
Naim Bajcinca
Miryam Barad
Francesco Basile
João Carlos Basilio
Beatrice Bérard
Jean-Louis Boimond
Kai Bollue
Anne Bouillard
Thomas Brunsch
Ctop
Maria Paola Cabasino
Peter E. Caines
Elia E. Cano
Lorenzo Capra
Antonio Eduardo Carrilho da Cunha
Lilian Kawakami Carvalho
Christos G. Cassandras
Arkady Cherkassky
Pasquale Chiacchio
Hyoun Kyu Cho
José Manuel Colom
Bertrand Cottenceau
José Eduardo Ribeiro Cury
Dtop
Philippe Dague
Philippe Darondeau
Max Herring de Queiroz
Bart De Schutter
Gianmaria De Tommasi
Philippe Declerck
Isabel Demongodin
Jérémy Dubreil
Emil Dumitrescu
Mustafa Seçkin Durmus
Etop
Magnus Egerstedt
Nabil El Akchioui
Ftop
Martin Fabian
Eric Fabre
Samira S. Farahani
Jean-Marc Faure
S. T. J. Forschelen
Gtop
Rosalba Galvan-Guerra
Roberto Ortiz Garrido
Stephanie Geist
Alain Girault
Alessandro Giua
José Cerdeira Gonzalez
Lenko Grigorov
Dmitry Gromov
Htop
Stefan Haar
Christoforos N. Hadjicostis
Laurent Hardouin
Bernd Heidergott
Zhiqiang Huang
Jtop
K. G. M. Jacobs
Donald E. Jarvis
Loig Jezequel
Qing-Shan Jia
Laurent Jouhet
Jorge Júlvez
Ktop
Terence P. Kelly
Leila Khalij
Ahmed Khoumsi
Jan Komenda
Fabrice Kordon
Gábor Kovács
Aysegul Kursun
Ltop
Stéphane Lafortune
Sébastien Lahaye
Mark Lawford
Euriell Le Corronc
Edouard Lecleryq
Ryan Leduc
Dimitri Lefebvre
Bengt Lennartson
Jean-Jacques Lesage
Hongwei Liao
Saulo Telles Lima
Feng Lin
Gabriel A.D. Lopes
Jan Lunze
Mtop
Patrik Magnusson
Scott Mahlke
Cristian Mahulea
Carlos Andrey Maia
Robi Malik
Herbert Mangesius
Hervé Marchand
Jasen Markovski
Patrick Martin
Tomás Masopust
James McLellan
Glenn Merlet
Sajed Miremadi
Behrang Monajemi Nejad
Thomas Moor
Marcos Vicente Moreira
Ntop
Ahmed Nazeem
Vladislav Nenchev
Eric Niel
Yannick Nke
Ptop
Vera Pantelic
Andrea Paoli
Patricia Nascimento Pena
Sebastian Perk
Laurent Piétrac
Julien Provost
Rtop
Jörg Raisch
Spyros A. Reveliotis
J. E. Rooda
Jean-Marc Roussel
Carlos A. Rovetto
Karen Rudie
Eric Rutten
Stop
Anooshiravan Saboori
Simona Sacone
Rafael Santos Mendes
Klaus Werner Schmidt
Carla Seatzu
Ying Shang
Shaolong Shu
Manuel Silva
Silvia Siri
Michaela Slaats
Marion Sobotka
L. J. A. M. Somers
Eduardo Souza de Cursi
Pavel Spacek
Olaf Stursberg
Rong Su
Mehmet Turan Söylemez
Ttop
Shigemasa Takai
Farzin Taringoo
Éric Thierry
Yann Thierry-Mieg
Wolfgang Thomas
Philip Twu
Vtop
D. A. van Beek
J. M. van de Mortel-Fronczak
Ton van den Boom
Hans van der Weide
Jan H. van Schuppen
Carlos Renato Vázquez
Felisa Vázquez-Abad
Ruben Velazquez
Warren Volk-Makarewicz
Wtop
Yin Wang
Yu Wang
Yorai Wardi
Simon Ware
Sarah-Jane Whittaker
Ytop
Chen Yao
Lina Ye
Hsu-Chun Yen
Ugur Yildirim
Ztop
Yan Zhang


Contact us

E-mail

Imprint/Impressum