The 3nd International Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR’17) will take place in Uppsala, Sweden as a satellite event of ETAPS’17. We thank the United Technologies Research Center and the Australian National University for sponsoring this event.
Hybrid systems are complex dynamical systems that combine discrete and continuous components. Reachability questions, regarding whether a system can run into a certain subset of its state space, stand at the core of verification and synthesis problems for hybrid systems.
There are several successful methods for hybrid systems reachability analysis. Some methods explicitly construct flow-pipes that over-approximate the set of reachable states over time, where efficient computation of such over-approximations requires symbolic representations such as support functions. Other methods based on satisfiability checking technologies, symbolically encode reachability properties as logical formulas, while solving such formulas requires numerically-driven decision procedures. Last but not least, also automated deduction and the usage of theorem provers led to efficient analysis approaches. The goal of this workshop is to bring together researchers working with different reachability analysis techniques and to seek for synergies between the different approaches.
The SNR workshop solicits papers broadly in the area of analysis and synthesis of continuous and hybrid systems. The scope of the workshop includes, but is not restricted to, the following topics with application to continuous and hybrid systems:
- Reachability analysis
- Flow-pipe construction; symbolic state set representations
- Logical frameworks for reasoning
- Bounded model checking
- Automated deduction
- Invariant generation
- Symbolic execution
- Trajectory generation; counterexample computation
- Abstraction techniques
- Reliable integration
- Reachability analysis for planning and synthesis
- Domain-specific approaches in biology, robotics, etc.
- Stochastic/probabilistic hybrid systems
Cyber-Physical Systems (CPS) pose new challenges to verification and validation that go beyond the proof of functional correctness based on high-level models. Particular challenges are, in particular for formal methods, heterogeneity and scalability. For numerical simulation, uncertain behavior is a challenge that motivates the use of symbolic methods. To underline this, we compare the scalability and fidelity of symbolic simulation runs with numerical multi-run simulation based approaches and show where symbolic simulation scales better than numerical approaches, and where not.
As an example for a highly scalable approach, we explain details from the SystemC AMS standard that targets highly scalable numerical simulation of mixed discrete/continuous systems and show what we can learn from it for symbolic simulation. As a concrete result, we formalize the motivated ideas and describe an implementation based on Affine Arithmetic Decision Diagrams (AADD) that allows symbolic simulation of SystemC AMS models. We describe two case studies, one of them with industrial complexity, that show the benefits and limitations of the approach.
Christoph Grimm’s research interests include in particular modeling and simulation of mixed discrete/continuous systems, both numerically and symbolically. He contributed to the standardization of VHDL-AMS and the SystemC AMS extensions where he co-authored the Language Reference Manual and the User’s Guide and served as vice-chair of the Accellera working group. He studied Electrical Engineering at TU Darmstadt and EC Lyon and holds a Dr. degree and professional habilitation in Computer Science. 2006 he became Professor for embedded systems at Vienna University of Technology, 2008 head of the Institute of Computer Technology. 2012 he accepted a call to TU Kaiserslautern.
To model and design CPS systems, we must combine models for discrete and continuous dynamics. Such combined models are fraught with subtlety. In this talk, I discuss some fundamental limits which cannot be overcome by any modeling technique. Specifically, chaos, the inability to computationally model a continuum, and the incompleteness of determinism limit the predictive power of models. I will also establish a connection between constructiveness, causality, and the incompleteness of determinism by showing that it is the existence of non-constructive models that leads to incompleteness.
Edward A. Lee is the Robert S. Pepper Distinguished Professor in the Electrical Engineering and Computer Sciences (EECS) department at U.C. Berkeley. His research interests center on design, modeling, and analysis of embedded, real-time computational systems. He is the director of the nine-university TerraSwarm Research Center (http://terraswarm.org), a director of Chess, the Berkeley Center for Hybrid and Embedded Software Systems, and the director of the Berkeley Ptolemy project. From 2005-2008, he served as chair of the EE Division and then chair of the EECS Department at UC Berkeley. He is co-author of six books and hundreds of papers. He has led the development of several influential open-source software packages, notably Ptolemy and its various spinoffs. He received the B.S. degree in Computer Science from Yale University in 1979, the S.M. degree in EECS from the Massachusetts Institute of Technology (MIT) in 1981, and the Ph.D. degree in EECS from UC Berkeley in 1986. From 1979 to 1982 he was a member of technical staff at Bell Telephone Laboratories in Holmdel, New Jersey, in the Advanced Data Communications Laboratory. He is a co-founder of BDTI, Inc., where he is currently a Senior Technical Advisor, and has consulted for a number of other companies. He is a Fellow of the IEEE, was an NSF Presidential Young Investigator, and won the 1997 Frederick Emmons Terman Award for Engineering Education.
The workshop solicits
- long research papers (not exceeding 15 pages excluding references),
- short research papers (not exceeding 6 pages excluding references) and
- work-in-progress papers (not exceeding 6 pages excluding references).
Research papers must present original unpublished work which is not submitted elsewhere. In order to foster the exchange of ideas, we also encourage work-in-progress papers, which present recent or on-going work.
The papers should be written in English and formatted according to the EPTCS guidelines.
Papers can be submitted using the EasyChair system.
All submissions will undergo a peer-reviewing process.
Accepted research papers will be presented at the workshop and published in the Electronic Proceedings in Theoretical Computer Science (EPTCS).
Accepted work-in-progress papers will be presented at the workshop but will not be included in the proceedings.
The call for papers (ASCII) can be downloaded here.
|Paper submission||EXTENDED to February 17, 2017|
|Author notification||March 10, 2017|
|Camera-ready version||March 24, 2017|
|Workshop||April 22, 2017|
Przemysław Daca (Institute of Science and Technology Austria, Austria)
Matthias Althoff (Technische Universität München, Germany)
Stanley Bak (United States Air Force Research Lab, USA)
Franck Cassez (Macquarie University, Australia)
Xin Chen (University of Colorado at Boulder, USA)
Thao Dang (CNRS/VERIMAG, France)
Martin Fränzle (University of Oldenburg, Germany)
Goran Frehse (Verimag, France)
Antoine Girard (L2S, CNRS, France)
Thomas Heinz (Robert Bosch GmbH, Germany)
Hui Kong (Institute of Science and Technology Austria, Austria)
Oleksandr Letychevskyi (Glushkov Institute of Cybernetics, Ukraine)
Nikolaj Nikitchenko (Kyiv National Taras Shevchenko University, Ukraine)
Maria Prandini (Politecnico di Milano, Italy)
Stefan Ratschan (Academy of Sciences, Czech Republic)
Rajarshi Ray (National Institute of Technology Meghalaya, India)
Stavros Tripakis (Aalto University, Finland, and UC Berkeley, USA)
Vladimir Ulyantsev (ITMO University, Russia)
Edmund Widl (Austrian Institute of Technology, Austria)
Paolo Zuliani (University of Newcastle, UK)
9:00-10:00 Session 1: Uncertainty (chair: Sergiy Bogomolov)
9:00-10:00 Invited talk
Towards Verification of Uncertain Cyber-Physical Systems
10:00-10:30 Coffee break
10:30-12:30 Session 2: Synthesis and Analysis (chair: Walid Taha)
Adrien Le Coënt, Florian De Vuyst, Ludovic Chamoin and Laurent Fribourg.
Guaranteed Control Synthesis of Nonlinear Switched Systems using Euler Method
Anna Lukina, Josef Widder and Radu Grosu.
Synthesis of Optimal Plans for Process Synchronization in the Presence of Faults
Benoît Desrochers and Luc Jaulin.
Minkowski Operation of Sets with Application to Robot Localization
On the Underapproximation of Reach Sets of Abstract Continuous-time Systems
12:30-14:00 Lunch break
14:00-15:30 Session 3: Modelling (chair: Erika Abraham)
14:00-15:00 Invited talk
Edward A. Lee.
Fundamental Limits of Cyber-Physical and Hybrid System Modeling
Yingfu Zeng, Ferenc Agoston Bartha and Walid Taha.
Compile-Time Extensions to Hybrid ODEs
15:30-16:00 Coffee break
16:00-17:30 Session 4: Tools (chair: Eugenio Moggi)
Reachability Analysis in the KeYmaera X Theorem Prover
HyPro: A C++ Library for State Set Representations for Hybrid Systems Reachability Analysis
2nd International Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR’16), affiliated with CPSWeek’16
1st International Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR’15), affiliated with CAV’15