[Prev][Next][Index]
FWD: European workshop on hybrid systems - program
[Larchers: Note the abstract of the last talk. -- Jim H.]
------- Forwarded Message
From: gandalf@Csli.Stanford.EDU (Juergen Wagner)
Date: 4 Apr 1995 02:39:44 -0700
Subject: European workshop on hybrid systems - program
Newsgroups: news.announce.conferences
Sender: Oded.Maler@imag.fr (Oded Maler)
This announcement is also available through the conferences announcement index:
<URL:http://www.iao.fhg.de/Library/conferences>.
---------------------------------------------------------------------------
SECOND EUROPEAN WORKSHOP
ON REAL-TIME and HYBRID SYSTEMS
May 31, June 1-2, 1995
Grenoble (France)
Organised by
VERIMAG Laboratory, Grenoble
with support from
the ESPRIT-NSF project HYBRID EC-US-043
**************************
* WORKSHOP PROGRAM *
**************************
Wednesday, 31 May
=================
9:00-9:30 J. Sifakis, O. Maler, A. Bouajjani (Grenoble)
Wellcome, administration, introduction, and motivation.
9:30-10:30 Anil Nerode (Cornell):
Hybrid Systems and Control Theory (invited talk).
10:30-11:00 Coffee break
11:00-11:30 B.H. Widjaja (Jakarta), C. Zongji (Beijing),
H. Weidong, Z. Chaochen (Macau):
A cooperative design for hybrid systems.
11:30-12:00 M. Andersson (Lund):
Representation and simulation of hybrid systems in OmSim.
12:00-12:30 C. Zanne, J-F. Aubry, C. Iung (Nancy):
Electromechanical processes: an example of hybrid systems.
12:30-14:00 Lunch.
14:00-14:50 F. Vaandrager (Amsterdam):
Linear Hybrid Systems (invited talk).
14:50-15:20 S. Yovine (Grenoble):
Symbolic verification of linear hybrid automata with KRONOS.
15:20-15:50 T.I. Seidman (Baltimore),
Stochastic Versions of Hybrid Systems (invited talk).
15:50-16:20 Coffee break.
16:20-16:50 H.R. Andersen, J.L. Petersen (Lyngby),
Specification of a real-time pulse detector.
16:50-17:15 L. Urbina, G. Riedewald (Rostock),
Simulation and verification in constraint logic programming.
17:15-17:40 R. de Lemos, A. Saeed (Newcastle), J. Hall (York):
ERTL: an extension to RTL for requirements analysis for
hybrid systems.
17:40-18:05 C. Weise (Aachen):
Verifying real-time systems using parametrized timed modal
specifications.
18:05-18:30 J.J. Vereijken (Eindhoven),
A process algebra for hybrid systems.
===========================================================================
Thursday, 1 June
=================
8:45-9:00 Daily weather report, program update, stand-up comedy and more.
9:00-10:00 A. Pnueli (Weizmann):
Developments in Hybrid Systems Synthesis and
Verification (invited talk).
10:00-10:30 J. Raisch (Stuttgart):
Analysis and synthesis of symbolic output feedback structures
for continuous plants.
10:30-11:00 Coffee break.
11:00-11:30 R.L. Grossman (Chicago), A. Nerode, M. Sweedler (Cornell):
A Hilbert space approach to hybrid systems using formal
dynamical systems.
11:30-12:30 M. Fliess (Gif-sur-Yvette):
Flat Systems: Towards a New Paradigm in Nonlinear
Control (invited talk).
12:30-14:00 Lunch.
14:00-15:00 B. Mishra (New-york):
Hybrid Systems and their Controllers with Applications
to Robotics (invited talk).
15:00-15:30 A. Deshpande, P. Varaiya (Berkeley):
Design and evaluation of automated highway systems.
15:30-16:00 N. Lynch, H.B. Weinberg (MIT):
Proving correctness of vehicle maneuver: deceleration.
16:00-16:30 Coffee break.
16:30-17:00 J. Vitt (Kiel), J. Hooman (Eindhoven):
Specification and verification of a real-time steam
boiler system.
17:00-17:30 Y. Lakhnech (Kiel), A. Bouajjani, R. Robbana (Grenoble):
From duration calculus to linear hybrid automata.
17:30-18:00 D. Simon, K. Kapellos (Sophia-Antipolis), B. Espiau,
M. Jourdan (Grenoble):
Formal verification of robotic missions and tasks.
18:00-18:30 S. Nadjm-Teherani, J.-E. Stromberg (Linkoping):
JAS-95 lite: proving dynamic properties of a landing
gear system.
*********************************************************
20:00 Conference dinner at Chateau de Sassenage.
*********************************************************
=================================================================
Friday, 2 June
==============
8:45-9:00 Recent developments since yesterday, dinner evaluations
and hangover suggestions.
9:00-10:00 Z. Artstein (Weizmann):
Hybrid Feedback Stabilization (invited talk).
10:00-10:30 A. Benveniste (Rennes):
A compositional and uniform model for general
hybrid systems.
10:30-11:00 Coffee break.
11:00-11:30 N. Halbwachs, F. Maraninchi, Y.-E. Proy (Grenoble):
Hybrid Argos + Polka, description and analysis
of linear hybrid systems.
11:30-12:00 S. Engell, S. Kowalewski, K. Woellhaf (Dortmund):
Steps towards model-based verification of controllers
for chemical batch processes.
12:00-12:30 F. Favret (Gaz de France):
Real-time like hybrid simulation performed at your time?
12:30-14:00 Lunch.
14:00-14:40 E. Asarin (Moscow):
Ergodic Theory and Hybrid Systems (invited talk).
14:40-15:10 Th. Wilke (Kiel):
Monadic second-order logic and timed automata.
15:10-15:35 M. Romdhani, A.A. Jerraya (Grenoble), R.P. Hautbois, A. Jeffroy,
P. de Chazelles (Aerospatialle), A.E.K. Sahraoui (Toulouse):
Towards a multi-language specification based-on approach in
the development of avionics.
15:35-15:55 Coffee break.
15:55-16:20 O. Roux, V. Rusu (Nantes):
Decidable hybrid systems to model and verify
real-time applications.
16:20-16:45 S. Pettersson, B. Lennartson (Goteborg):
Hybrid modelling focused on hybrid petri nets.
16:45-17:10 V. Friessen (Berlin),
An excercise in hybrid systems specification using an
extension of Z.
17:10-17:30 Conclusion.
============================================================================
************************************
* Abstracts of invited talks *
************************************
------------------------------------------------------------------------
Ergodic Theory and Hybrid Systems
=================================
Eugene Asarin
=============
Inst. for Problems of Information Transmission,
Russian Academy of Science,
Moscow, Russia.
The following topics will be considered (not covered) by this talk:
- Some basic notions of ergodic theory (short tutorial);
- Entropy and complexity;
- Chaos and undecidability;
- Hybrid dynamical systems and their ergodic properties - some examples.
----------------------------------------------------------------------
Hybrid Feedback Stabilization
=============================
Zvi Artstein
============
Faculty of Mathematical Sciences
The Weizmann Institute
Rehovot, Israel.
Continuous feedback stabilization is sometimes impossible, even
for systems with a seemingly simple structure. At times the
stabilization is possible, but natural heuristics lead to ill
posed problems. Modifications to the continuous feedback
paradigm, that overcome some of the complications, are offered
in the control literature. Among these one finds the dynamic
stabilization, chattering, sliding modes, etc. In the talk the
hybrid feedback will be offered as a stabilization paradigm. On
one hand it serves as a mathematical tool to overcome some of
the deficiencies of continuous feedback stabilization. On the
other hand it is a model for realistic stabilization when
continuous and discrete machines interact.
The talk plan is to display a hybrid stabilization notion, to
list some of the problematics of continuous stabilization, to
comment on the available solutions and to demonstrate how hybrid
feedback handles them.
--------------------------------------------------------------
Flat systems: Towards a new paradigm in nonlinear control
=========================================================
Michel Fliess
=============
Laboratory of Signals and Systems,
Gif-sur-Yvette, France.
Flat systems, which are equivalent to linear ones via a special
type of dynamic feedback, were introduced in 1992 by J. Levine,
P. Martin, P. Rouchon and the speaker. Their physical properties
are subsumed by a linearizing, or flat, output and they might be
regarded as providing another nonlinear extension of Kalman's
controllability. Many realistic classes of examples are flat and
we will detail some popular ones, like the crane and the motion
planning of the car with several trailers. We will show that
many important control problems, like discretization or
stabilization, become quite easy in this setting. The connection
with classic linear theory will also be examined.
-----------------------------------------------------------------
Hybrid Systems and their Controllers with Applications to Robotics
==================================================================
Bud Mishra
==========
Robotics Research Laboratory,
Courant Institute,
New York University, USA.
In this talk, I shall describe our experience with a prototype
system capable of synthesizing Supervisor Controller Programs
based largely on the theory of discrete event systems (DES)
first proposed by Ramadge and Wonham. We augment the theory by
also allowing continuous time trajectories modeling transitions
between events. We illustrate our approach by an example, "the
discrete control of a walking machine", which poses some
challenges on extending the traditional approaches to a hybrid
systems.
I shall survey various approaches posed by other researchers and
why they do not adequately address the issues raised in the
context of these robotic hybrid system applications and suggest
some of the major open problems.
-----------------------------------------------------------
Hybrid Systems and Control Theory
=================================
Anil Nerode,
MSI, Cornell University,
Ithaca, NY, USA
Hybrid Systems is an amalgam of control theory and computer
science. Its purpose is to analyze and design ``hybrid systems'' in
which digital programs or automata and continuous physical plants
interact with each other and the external environment in networks.
The first fundamental problem of hybrid systems is the problem of how
to extract digital control programs for continuous plants. That is, to
find algorithms which, given continuous plant differential equations
and plant performance specifications, extract digital control programs
(mode switching) that force the state trajectories of the system to
obey their performance specifications.
The second fundamental problem is how to implement such controls in
real time systems, especially cooperating distributed systems of
plants.
----------------------------------------------------------------
Developments in Hybrid Systems Synthesis and Verification
=========================================================
Amir Pnueli
===========
Department of Computer Science,
Weizmann Institute,
Rehovot, Israel.
In this talk I will survey various results concerning the analysis
and synthesis of hybrid systems which have accumulated since the
introduction of these systems into the verification literature
around 4 years ago. These results range from axiomatic frameworks
for proving properties of such systems to algorithmic methods.
Special emphasis will be given to recent control synthesis results
for real-time and linear hybrid systems.
----------------------------------------------------------------
Stochastic Versions of Hybrid Systems
=====================================
Thomas I. Seidman
=================
Department of Mathematics and Statistics,
University of Maryland BC,
Baltimore, USA.
To the extent that hybrid systems may be viewed as the
interaction of discrete event systems in the computer control of
parts of the real-world, one must be prepared to model the
relevant classes of real-world dynamics. For many realistic
problems, this includes, for example, stochastic elements in the
form of random exogenous excitations. We will attempt to present
the issues involved, indicating both the technical feasibility
of such an approach and some ways in which this may be relevant.
-------------------------------------------------------------------
Linear Hybrid Systems
=====================
Frits Vaandrager
================
CWI and University of Amsterdam,
Holland
In this presentation, I will discuss the model of linear hybrid
automata introduced into the verification literature by various
authors. This model has become quite popular recently because
it allows for fully automatic model checking.
The semantics of linear hybrid automata will be defined via a
translation to the timed I/O automata of Lynch and Vaandrager.
To illustrate the model of linear hybrid automata, I will
present a simple version of a protocol developed by Philips for
the physical layer of an interface bus that connects the various
devices of some stereo equipment (tuner, CD player,...).
I will discuss the original verification in the I/O automata
model by Bosscher, Polak and Vaandrager, the mechanical checking
of the proof using the Larch Prover by Griffioen, and the fully
automatic verification of an instance of this protocol using the
HyTech tool by Wong Toi and Ho.
===============================================================================
******************************
* WORKSHOP INFORMATION *
******************************
LOCATION
========
The workshop will be held at :
Institut National Polytechnique de Grenoble
Amphi Barbillon
46, avenue Filix Viallet
F-38000 Grenoble, France.
The Buildings of the Institut National Polytechnique de Grenoble are
situated in the center of Grenoble, near the railway station.
Grenoble is the Alpes' capital and is surrounded by a beautiful
landscape. It is also an important center of computer science and
industry.
TRANSPORTATION
==============
Grenoble Airport (Saint Geoirs) can be reached from Paris.
Lyon Airport (Satolas) or Geneva Airport (Cointrin) are served by most
major airlines and can be reached from all parts of the world.
* From Saint-Geoirs you can take a bus to Grenoble (35 mn),
* from Satolas you can take a train or a bus to Grenoble (70 mn),
* from Cointrin you can take a train to Grenoble (2 hours).
Grenoble can also be reached by train (TGV) from Paris (3 hours).
WORKSHOP OFFICE
===============
Please address the registration form and inquiries to:
Chantal Costes,
Verimag, Miniparc Zirst,
Rue Lavoisier,
F-38330 Montbonnot St Martin - France.
E-mail : Chantal.Costes@imag.fr
Phone : (+33) 76 90 96 40
Fax : (+33) 76 41 36 20
REGISTRATION DEADLINE
=====================
Registration forms should be sent (possibly by e-mail or by fax)
NO LATER THAN April 30.
REGISTRATION FEES
=================
Registration fees are 1000 FF.
They include coffee breaks, three lunches, a conference dinner, and
the proceedings.
PAYMENT
=======
- By cheque to: Agent Comptable INPG
- By bank transfer to:
Tresor Public de Grenoble, Tresorerie Generale
account Number 3000141,
bank code 10071,
guichet code 38000,
RIB 43,
Verimag M 020 R1
In case of transfer, make sure that all fees are charged to YOUR account.
ACCOMMODATION
=============
We propose to arrange reservations in the two following hotels:
1- GRAND HOTEL (***),
in Grenoble's center, at ten minutes walk distance from the buildings
of the Institut National Polytechnique. All the rooms are
sound-proofed, with bathroom, toilet, direct telephone, and
television.
Single room 283 FF, Double room 326 FF
Breakfast 40 FF
2- SAVOIE Hotel (**),
in front of the buildings of
the Institut National Polytechnique.
All the rooms are sound-proofed with shower/wc, TV, radio, and telephone.
Single room with breakfast 255 FF
Double room with breakfast 289 FF
REGISTRATION FORM
=================
The registration form must be sent by *** April 30 ***.
[It can be sent by e-mail or by fax]
------------------------------------------------------------------------------
THE SECOND
EUROPEAN WORKSHOP
ON REAL-TIME and HYBRID SYSTEMS
May 31, June 1-2, 1995,
Grenoble (France).
----- REGISTRATION FORM -----
Name (s)
...........................................................................
...........................................................
Surname.....................................................................
..................................................................
Affiliation :
...........................................................................
.........................................................
Mailing address :
............................................................................
............................................................................
............................................................................
............................................................................
Phone number : .................................................
E-mail: ........................................................
Fax number : ...................................................
Arrival Date : .............................First meal : ..................
Departure Date : ........................... Last meal : ...................
Please make the following reservations :
Grand Hotel (3*) Savoie Hotel (2*)
Single room Double room
Payment of the Registration Fees (1000FF):
- by cheque Agent Comptable INPG
- by bank transfer to Tresor Public de Grenoble,
Tresorerie Generale,
account Number 3000141, bank code 10071, guichet code 38000,
RIB 43, Verimag M 020 R1
Signature :
------------------------------------------------------------------------------
------- End of Forwarded Message