Scope
Hybrid systems model complex dynamical systems that combine discrete and con- tinuous components. Reachability questions, regarding whether a system can run into certain subset of its state space, stand at the core of verification and synthesis problems for hybrid systems.
Successful reachability analysis methods for hybrid systems requires the unification of techniques from at least two traditions:
- Symbolic methods that operate on exact and discrete representations of systems, in the form of various model checking and theorem proving algorithms,
- Numerical methods that operate on various forms of numerical approximations and continuous transformations of the systems, as developed in the area of continuous dynamical systems and control theory.
As concrete examples, one can observe how the two types of techniques interact in the existing approaches towards reachability analysis. Reachable set computation methods explicitly construct flow-pipes that overapproximate the reachable states over time, while efficient computation of such overapproximations requires symbolic representations such as support functions. Constraint solving methods symbolically encode reachability properties as logic formulas, while solving such formulas requires numerically-driven decision procedures. A goal of the workshop is to seek further synergies among these approaches.
Back to TopTopics
The SNR workshop solicits papers broadly in the area of verification and synthesis of continuous and hybrid systems. One of the aims is to catalyze work on the interface of symbolic and numerical methods for the reachability analysis. The scope of the workshop includes, but is not restricted to, the following topics:
- Flow-pipe construction
- Representation of symbolic regions within reachability algorithm
- Abstraction techniques for hybrid systems and numerical programs
- Trajectory generation from symbolic paths
- Decision procedures over real numbers
- Reliable integration
- Logics to reason about hybrid systems
- Reachability analysis for planning and synthesis
- Domain specific approaches in biology, robotics, etc
Program (July 19)
Session 1 (8:30-10:00)
- Ian M. Mitchell. Recent Progress on Efficient Parametric Approximations of Viability and Discriminating Kernels
- Kengo Kido, Swarat Chaudhuri and Ichiro Hasuo. Abstract Interpretation with Infinitesimals: Towards Scalability in Nonstandard Static Analysis
- Yang Gao and Martin Fränzle. Verification of Stochastic Systems by Stochastic Satisfiability Modulo Theories with Continuous Domain
- Fedor Shmarov and Paolo Zuliani. ProbReach: A Tool for Guaranteed Reachability Analysis of Stochastic Hybrid Systems
Coffee-break (10:00-10:30)
Session 2 (10:30-12:00)
- Invited talk: Sriram Sankaranarayanan (University of Colorado Boulder, USA). Symbolic-Numeric Reachability Analysis of Hybrid Systems
- Stanley Bak, Sergiy Bogomolov and Taylor T Johnson. HYST: A Source Transformation and Translation Tool for Hybrid Automaton Models
- Pavithra Prabhakar and Miriam García Soto. An Algorithmic Approach to Stability Verification of Hybrid Systems: A Summary
Important Dates
| Paper submission | |
| Author notification | May 31, 2015 |
| Camery-ready version | June 15, 2015 |
| Workshop | July 19, 2015 |
Program Committee
| Matthias Althoff (TUM, Germany) | Sergiy Bogomolov (IST Austria, Austria) - co-chair |
| Parasara Sridhar Duggirala (University of Illinois at Urbana Champaign, USA) | Martin Fränzle (University of Oldenburg, Germany) |
| Goran Frehse (Verimag, France) | Sicun Gao (Massachusetts Institute of Technology, USA) |
| Daniele Magazzeni (King’s College, UK) | Sayan Mitra (University of Illinois at Urbana Champaign, USA) |
| Erion Plaku (CUA, USA) | Stefan Ratschan (Academy of Sciences, Czech Republic) |
| Ashish Tiwari (SRI, USA) - co-chair | Stavros Tripakis (Aalto University, Finnland) |
| Paolo Zuliani (University of Newcastle, UK) |