Newsletter of the IEEE CSS TC on Hybrid Systems Issue 4 Conference Announcement: 6th IFAC Conference on Analysis and Design of Hybrid Systems 2018 @ Oxford University, UK, July 11-13, 2018 - Bursary/Poster deadline is May 31, 2018. ADHS 2018 takes place as a workshop of the Conference on Computer Aided Verification (CAV 2018), and within FLOC 2018. The conference happens under the auspices of IFAC and is sponsored by the IFAC Technical Committee on Discrete Event and Hybrid Systems. * Official Program: http://www.cs.ox.ac.uk/conferences/ADHS18/programme * Keynote Speakers: Raphael Jungers, Calin Belta, and Erika Abraham - http://www.cs.ox.ac.uk/conferences/ADHS18/speakers * Early Registration Deadline: June 6th, 2018 - https://www.cs.ox.ac.uk/conferences/ADHS18/registration * Accommodation: https://www.cs.ox.ac.uk/conferences/ADHS18/venue *** Bursaries are available to students and young researchers *** We intend to provide a few bursaries to support the participation of students or young researchers to ADHS18. Bursaries might be used to pay off registration costs to ADHS18. Students or young researchers wishing to get a bursary are asked to present a poster about their work (if applicable, beyond their scheduled oral presentation at ADHS18). An internal committee will select applications. Please submit a poster title and short abstract before May 31st to [email protected] For more details, go to http://www.cs.ox.ac.uk/conferences/ADHS18/ Workshop Announcement: ARCH workshop will take place on Friday, July 13, 2018 as part of and hosted by ADHS18, and within FLOC 2018 @ Oxford University — cps-vo.org/group/ARCH/ This workshop aims at bringing together researchers and practitioners, and to establish a curated set of benchmarks submitted by academia and industry. Verification of continuous and hybrid systems is increasing in importance due to new cyber-physical systems that are safety- or operation-critical. This workshop addresses verification techniques for continuous and hybrid systems with a special focus on the transfer from theory to practice. Topics include, but are not limited to Proposals for new benchmark problems (not necessarily yet solvable) Tool presentations Tool executions and evaluations based on ARCH benchmarks Experience reports including open issues for industrial success Conference Announcement: 6th IFAC Conference on Nonlinear Model Predictive Control @ Madison, Wisconsin, 19-22 August 2018 Model predictive control (MPC) is indisputably one of the advanced control techniques that has significantly affected control engineering practice with thousands of controllers implemented in various fields, spanning from process industry to automotive and robotics. This is due to its unique ability to handle constraints, take preview information about disturbances and set point changes into account and optimize performance. Furthermore, MPC allows the consideration of various types of dynamics, from linear to nonlinear, discrete to continuous, as well as on-line adaptation of models and parameters. The research community on MPC is very active, with hundreds of papers published every year. Over the past decades many theoretical, as well as implementation results have been achieved. The IFAC Conference on Nonlinear Model Predictive Control (NMPC 2018) aims at bringing together researchers interested and working in the field of MPC, from both academia and industry. This allows to reflect and establish the current state-of-the-art and focus the future development of the MPC field towards relevant directions. Major conference topics are: Uncertainty and model predictive control Stability and recursive feasibility of nonlinear model predictive control Economic model predictive control Model predictive control in the cloud IoT and model predictive control Learning and model predictive control Stochastic model predictive control Model predictive control for hybrid systems Moving horizon estimation Model predictive control for large scale systems Hierarchical and decentralized predictive control Embedded and real-time feasible predictive control Optimization and model predictive control Model predictive control of mechatronic systems Heating, ventilation, air conditioning (HVAC) control Energy systems and model predictive control Autonomous systems and model predictive control Model predictive control for autonomous driving Model predictive control for aeronautic applications Model predictive control for automotive systems Process control and model predictive control Model predictive control for medical applications Biotechnology and model predictive control Model predictive control for smart manufacturing and industry 4.0 Confirmed plenary speakers: Lorenz Biegler (Carnegie Mellon University, US) Francesco Borrelli (University of California, Berkeley, US) Stefano Di Cairano (Mitsubishi Electric Research, US) Ilya Kolmanovsky (University of Michigan, US) Jan Maciejowski (University of Cambridge, UK) Giancarlo Ferrari Trecate (École polytechnique fédérale de Lausanne, Switzerland) Stephen Wright (University of Wisconsin-Madison, US) Invited and selected keynote speakers: Alberto Bemporad (IMT School for Advanced Studies, Lucca, Italy) Jonas Buchli (Swiss Federal Institute of Technology, Switzerland) Timm Faulwasser (Karlsruhe Institute of Technology, Germany) Paul Goulart (University of Oxford, UK) Ali Mesbah (University of California, Berkley, US) Joe Qin (University of South California, US) Angela Schoellig (University of Toronto, Canada) Melanie Zeilinger (Swiss Federal Institute of Technology, Switzerland) For more details, go to: http://www.nmpc2018.org/ Call for Papers: IET Control Theory and Applications Journal SPECIAL ISSUE ON: Recent Advances in Control and Verification for Hybrid Systems The study of dynamical systems has focused, for the most part, on the two distinct areas of continuous-time and discrete-event systems. In recent years, interest has emerged in a class of systems that combine both continuous-time dynamics and discrete-event behaviors, which are referred to as hybrid systems. Typical examples of hybrid systems have been observed in various applications such as cyber-physical systems, mechanical systems, process control systems, the automotive industry, power systems, aircraft and traffic control systems, and economics and societal systems. Designing controllers and verifying specifications for hybrid systems raises severe methodological questions because they necessitate the combination of continuous variable system descriptions like differential equations with discrete-event models. Hybrid system methodologies are mostly based on the principles and results of the theories of continuous and discrete systems and, due to the greatly growing demands on control and verification for hybrid systems, extending and merging the contributions coming from different disciplines is posing a great challenge. The purpose of this special issue is to explore the latest advances in theoretical analysis, numerical simulation, data-driven methods, experimental observation, and engineering applications in hybrid systems. This special issue aims to offer a venue for researchers from various fields to make a rapid exchange of ideas and original research findings in hybrid systems. We are particularly interested in new interdisciplinary approaches in system sciences and real-world applications, or strong conceptual foundations in newly evolving topics. Potential topics of interests include, but are not limited to: Hybrid system modeling and identification Experimental methods and computational methods in hybrid systems Discrete-event driven systems, hybrid automata and Petri nets Switched, piecewise affine and stochastic jump systems Formal methods in control for hybrid systems Reach set computation and verification for hybrid systems Control and verification for data-driven hybrid systems Adaptive control for hybrid systems Optimisation and design for hybrid systems Applications to cyber-physical systems, autonomous systems, robotics systems, etc. All papers must be submitted through the journal’s Manuscript Central system: http://mc.manuscriptcentral.com/iet-cta Publication Schedule: Submission Deadline: 30 June 2018 Publication Date: June 2019 Editor-in-Chief: Professor James Lam, University of Hong Kong, Hong Kong Guest Editors: Dr. Weiming Xiang Vanderbilt University, USA E: [email protected] Prof. Guisheng Zhai Shibaura Institute of Technology, Japan E: [email protected] Prof. Taylor T. Johnson Vanderbilt University, USA E: [email protected] Prof. Simone Baldi Delft University of Technology, The Netherlands E: [email protected] Prof. Chengzhi Yuan University of Rhode Island, USA E: [email protected] PhD Position Announcement: PhD Position: Efficient synthesis of controllers using symbolic models Supervisor: Antoine Girard ([email protected] / https://sites.google.com/site/antoinesgirard/) Location: Gif-sur-Yvette (Paris area), France Laboratoire des Signaux et Systèmes - L2S (http://www.l2s.centralesupelec.fr) Institution: CNRS – CentraleSupélec – Univ. Paris-Sud – Univ. Paris-Saclay Duration: Three years, starting fall 2018 Position fully funded by European project (ERC consolidator) PROCSYS Context and Objectives Cyber-physical systems (CPS) consist of computational elements monitoring and controlling physical entities. The main objective of the PROCSYS project is to propose a general framework for the design of programmable CPS that will allow engineers to develop advanced functionalities using a high-level language for specifying the behaviors of a CPS while abstracting details of the dynamics. Controllers enforcing the specified behaviors will be generated from a high-level program using an automated model-based synthesis tool. Correctness of the controllers will be guaranteed by following the correct by construction synthesis paradigm through the use of symbolic control techniques [1,2]: the continuous physical dynamics is abstracted by a symbolic model, which is a discrete dynamical system; an interface consisting of low-level controllers is designed such that the physical system and the symbolic model behaves identically; a high-level symbolic controller is then synthesized automatically from the high-level program and the symbolic model. Work description We will develop efficient controller synthesis techniques based on incremental exploration of the dynamics of the symbolic model, which can be computed on the fly while synthesizing the controller. This has been the approach developed in our preliminary work [3], which has demonstrated significant improvements in terms of scalability for safety specifications and deterministic symbolic models. The main idea is to define priorities on the transitions of the symbolic model and explore the transitions with higher priority first. The transitions of lower priority are only explored if the control specification cannot be met with the former transitions. In the PhD thesis, we will develop efficient controller synthesis algorithms, which extend the work above in the following directions: 1. Non-deterministic symbolic models, extending the applicability of the approach to a broad class of systems 2. General specifications defined in the high-level language developed within the PROCSYS project, describing rich and complex behaviors 3. Additional synthesis objectives (timing constraints, quantitative performance criteria, robustness) Applications to case studies, e.g. in the field of autonomous driving will be considered. Background of the candidate The candidate must hold a Master in control theory, applied mathematics or computer science with a strong mathematical background. A prior experience in the area of hybrid systems is recommended. Programming skills are also needed. References [1] Belta, C., Yordanov, B., & Gol, E. A. (2017). Formal Methods for Discrete-Time Dynamical Systems (Vol. 89). Springer. [2] Tabuada, P. (2009). Verification and control of hybrid systems: a symbolic approach. Springer Science & Business Media. [3] Girard, A., Gössler, G., & Mouelhi, S. (2016). Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models. IEEE Transactions on Automatic Control, 61(6), 1537-1549. https://hal.archives-ouvertes.fr/hal-01197426v2/document PhD Position Announcement: PhD Proposal: Data Mining Dynamic Behaviors using Signal Temporal Logic Tempo group VERIMAG, University of Grenoble-Alpes France Supervisors: Oded Maler and Nicolas Basset The major goal of the project is to develop new techniques for extracting information from temporal behaviors (signals, wave-forms, sequences), and come up with succinct representation that captures their properties. These behaviors, can be a result of running simulations or measuring actual systems in various domains. In some application domains temporal data mining is handled by techniques coming from machine learning (recurrent neural networks (RNN), automaton learning), statistics and control (system identification). The project will explore the applicability of Signal Temporal Logic (STL) for inferring classifiers and for clustering of such behaviors. STL is a simple extension of temporal logic used to specify properties of real-valued signals defined over continuous time. It can express, for example constraints on the temporal distance between events such as threshold crossings of various variables. Its major use is to monitor behaviors (simulation traces, measurement from a real system during operation) and detect violations of temporal properties. Since its introduction in 2004, STL has been adopted by researchers in many application domains to specify and monitor behaviors of diverse systems such as robots, medical devices (artificial pancreas, anaesthesia machine), analog circuits, biochemical models of cellular pathways, and cyber-physical control systems, mostly within the automotive domain. An introduction to can be found in http://www-verimag.imag.fr/~maler/Papers/checking.pdf and a recent survey appears in http://www-verimag.imag.fr/~maler/Papers/monitor-RV-chapter.pdf. The starting point of the thesis will be the work on parametric identification of temporal properties which solves the following problem: given a behavior and a parametric STL (PSTL) formula, a formula where some threshold and timing constants have been replaced by parameters, find the set of parameters that makes the behavior satisfy the property. More details can be found in http://www-verimag.imag.fr/~maler/Papers/identify-tl.pdf and http://www-verimag.imag.fr/~maler/Papers/parametric-hscc18.pdf. From the point of view of machine learning, the formula can be viewed as a feature extractor that reduces the signal into a low-dimensional set in the parameter space that can be used for classification and clustering. The goal of the thesis is to develop these ideas further, theoretically and practically, to the point of being applicable to real-life case studies. The actual evolution of the thesis will depend, of course, on intermediate results but also on the qualifications and tendencies of the student. Among the topics to be investigated we find: 1) A comparison with other approaches to learn from temporal behaviors such as RNN and automata; 2) Fundamental and algorithmic studies on the quantitative semantics of STL which reflects the robustness of satisfaction in space and time; 3) An implementation of different approaches (search, quantifier elimination, backward computation) to solve the parametric identification problem, exactly or approximately; 4) Handling the fact that while observing system behaviors we have only positive examples; 5) Developing efficient algorithms for sub-problems encountered during the development of the classification and clustering algorithms, e.g., computing the Hausdorff distance between unions of poyhedra, or approximating monotone functions; 6) Applying the resulting algorithms to case-studies coming from cyber-physical systems and mostly from systems biology. 7) Integrating the results in the AMT toolbox. All in all, the thesis offers an opportunity to participate in a leading-edge research in a new and timely domain that combines clean and decent theory, real-life applicability and international collaboration. The thesis is part of the SYMER multi-disciplinary project of the Grenoble University, in collaboration with biologists working on cellular metabolism and epigenetics and the project results will be applied to models developed within the project. We are looking for motivated candidates with a Masters degree in Computer Science, Electrical Engineering, Mathematics or even Physics, and a solid background in a non-empty subset of computer science (algorithms, automata, logic), control, optimization, formal methods, machine learning, signal processing and statistical reasoning. Such candidates who are ready to learn new things and complete their background, are kindly requested to send e-mail (with "PhD-candidate" in the title) a CV and a motivation letter to [email protected] and [email protected] The Grenoble area, in addition to being surrounded skiable mountains is easily accessible: Lyon (1 hour), Geneva (1.5 hours), Torino (2 hours), Paris (3 hours by train) and Barcelona (6 hours). It features one of Europe’s largest concentrations of academic/industrial research and development with a lot of students, a cosmopolite atmosphere and work opportunities. VERIMAG, http://www-verimag.imag.fr is a leading academic lab in verification and model-based design of embedded cyber-physical systems. Its past contributions include model checking (J. Sifakis, Turing Award 2007), the data-flow language Lustre (P. Caspi, N. Halbwachs) underlying the SCADE programming environment for safety-critical systems. The Tempo group at VERIMAG has made pioneering contributions to the study of hybrid cyber-physical systems and its applications, and in particular the development of STL. Group alumni have proceeded to post-doc abroad (Berkeley, Carnegie-Mellon, Cornell, Boston University, IST Ausrtria) or integrate in industry (Mathworks, Intel, local start-ups) or R&D organization (Austrian Institute of Technology). TC Announcement: Call for contributions for Hybrid System entry @ Wikipedia.org At previous TC meetings, we have discussed the idea of updating the hybrid systems wikipedia.org entry at https://en.wikipedia.org/wiki/Hybrid_system as a coordinated TC effort. With wikipedia.org being a first stop for many research queries, it would be important that our field is well represented in that entry, and that is not currently the case. With the help of co-chair Alessandro Abate, the TC is organizing rewriting that entry and below is a tentative table of contents. 1 Overview 2 Modeling Frameworks 2.1 Hybrid Automata 2.2 Hybrid Inclusions 2.3 (and so on) 3 Analysis Tools 3.1 Viability and Forward Invariance 3.2 Temporal Logic 3.3 Lyapunov Stability 3.4 Verification 3.5 Robustness 4 Control Synthesis Tools 5 Simulation, Validation, Testing tools 6 Hybrid Systems Applications 7 Current Challenges 8 Further reading 9 References If you are interested in contributing to this effort, please email Alessandro and myself indicating the topic you would like to contribute with and we will send you instructions. The length of the entry is up to the writer, but should certainly include references to articles where more details are available. TC Announcement: Meeting at ACC 2018 -- Deadline for RSVP is June 15 We will have a TC meeting at the ACC in Milwaukee. Based on already scheduled meetings and the conference schedule, our meeting will be on Wednesday June 27, from 6:00 PM to 7:00 PM at room Wright A. Please RSVP at the link below by June 15. Appetizers will be served. https://doodle.com/poll/hbw4usqzx8k6r5qr I will send a tentative agenda a few days before the meeting. I hope to see you there.
