Thursday 28 November

11.00	Arrival and accommodation
12.00	Lunch
13.00	Introduction and Presentation of Participants  Erik Jørgensen ,  Dina Research School
13.15	Lecture: Hybrid Systems A quick introduction by example to: automata, timed automata and hybrid automata Anders P. Ravn , Aalborg University
	We introduce the concept of a state machine or automaton and illustrate how it is used to model simple systems , where the dynamic behaviour consists of discrete state transitions. The model is then extended with timers or local clocks that measure the time spent in states. They can be reset at a transition, and a transition can be dependent on a clock value. Finally we generalize the concept of timers to flow variables that evolve according to a differential or differential algebraic set of equations. At the end of the lecture, we shall briefly indicate constructs for hierarchical composition of state machines: Substates and Superstates, Sequential composition, and Parallel Composition with communication.
13.50	Break
14.00	Lecture: An Application Case Study from Control Engineering An application to a trajectory following problem for an outdoor vehicle. Jan Dimon Bendtsen , Aalborg University
	This lecture discusses an application of hybrid systems design taken from nonlinear control, namely the problem of trajectory tracking for a four-wheel steered, four-wheel driven mobile robot. The purpose of the robot is to drive autonomously between waypoints, starting from rest and stopping when the next waypoint is reached. The robot is modelled as a non-holonomic dynamic system subject to pure rolling, no-slip constraints. Under normal driving conditions, a nonlinear trajectory tracking feedback control law based on dynamic feedback linearization is sufficient to stabilize the system and ensure asymptotically stable tracking. However, when the velocity of the robot becomes very small, or the wheel configurations approach certain singular points, the feedback linearization scheme tends to fail due to these singularities. It is therefore necessary to switch to other modes of control when the robot is sufficiently close to the singularities. We will show how these transitions are derived systematically from the model, and present a hybrid automaton containing the different continuous-time control laws derived above in each mode
14.30	Lecture: An Application Case Study from Biology The Immune System as a Reactive System: Modeling T-Cell Activation with Statecharts Na'aman Kam , Weizmann Institute, Israel
	The construction of reliable reactive systems is considered to be one of the most challenging goals in the fields of software and system engineering. The definition of a reactive system definitely suits biological systems at different levels, ranging from gene networks, developing embryos and the immune system of the adult. This talk will discuss the application of a tool developed for constructing computerized systems to the modeling and analysis of a biological system, the immune system. We use the language of statecharts within the framework of object-oriented modeling. The results described here indicate that this modeling strategy can contribute to the transition of biology from the phase of analysis to the phase of synthesis.
15.30	Coffee and Tea
16.00	Modelling Exercises on Computers
17.30	Discussion of Results
17.45	Dinner
19.00	Lecture: Analyzing properties of Hybrid Systems Analyzing automata: reachability, invariants, timed and hybrid extensions. Rafael Wiesniewski , Aalborg University
	In this lecture we shall continue with the notion of hybrid automaton. The focus is on a class of rectangular automata, which is a generalization of timed automata. In particular we shall analyse the following control problem. Given a set of possible control modes, together with the plant behaviour resulting from each model the control problem is to find a switching strategy between control modes that keeps the plant output out of unsafe state. The central issue is whether such a control problem can be solved algorithmically.
19.35	Modelling Exercises (continued)
21.45	Coffee, tea and Sandwiches

Friday 29 November

7.30	Breakfast
8.00	Discussion of Results from Exercises
8.35	Break
8.50	Lecture: Advanced Modelling of Biological Systems Modeling, simulation and analysis of Caenorhabditis elegans Development Na'aman Kam, Weizmann Institute, Israel
	Our understanding of biology is reaching a new phase that increasingly requires the synthesis of information from many sources to gain deeper insights into how functional organisms are assembled. To assist in the integration of this information, we have begun to model the development and function of biological systems using the languages and methodologies designed for computer modeling of highly reactive man-made systems. We are currently developing a model of the highly characterized and well-defined egg-laying system of the nematode Caenorhabditis elegans. We have begun to incorporate into our model all existing data pertaining to the coordinated development of the four tissues that enable C. elegans hermaphrodites to lay eggs. These data sets span a large spectrum of complex biological phenomena, including cell fate determination, cell cycle control, cell migration and apoptosis. Our modeling tools use various visual formalisms including statecharts and live sequence charts (LSCs) for specifying the behaviors of the system, model execution and analysis. This effort will serve to develop the tools, technology and expertise to expand this model for use by the entire C. elegans community and to allow the application of these methodologies to other biological systems.
9.30	Coffee and Tea
10.00	Lecture:  Abstraction and Refinement of  Models Anders P. Ravn, Aalborg University
	When models get too complex, we need to abstract from detail, and conversely, when the model is too superficial we have to refine some part of it.
	Abstraction and refinement are introduced as a precise notion of a simulation relation between automata. The intuition is, that whenever the refined or detailed automaton does a transition to a target state, then the corresponding abstract state makes a transition to a new abstract state corresponding with the target state. Note that the abstract automaton may stay in a state, while the detailed automaton does a number of steps, as long as the states passed, all correspond to the abstract state
10.45	Break
11.10	Discussion and Closing Erik Jørgensen, Dina Research School
12.00	Lunch and Departure

ddd