JuliaReach & JuliaIntervals Days 3

Welcome!

This event will host talks from two Julia communities: JuliaReach (reachability analysis) and JuliaIntervals (interval methods). The main goal is to bring together people interested in foundations or applications of these topics by: disseminating the current state of relevant Julia packages, organising development sprints and exchanging ideas or discussing open problems.

The event will take place from 9th to 11th December 2021, fully online. Connection details will be sent upon registration.

Registration

The event is free, but registration is required. Optionally, participants' information will be displayed in the world map of the Participants section in this webpage. Upon registration, you should receive a confirmation email. If you need to edit your form, follow the link provided in such email.

Code of Conduct

During the event, we will follow the JuliaCon code of conduct. Violations of code of conduct can be reported to mforets [at] gmail [dot] com and/or luca [dot] ferranti [at] uwasa [dot] fi.

Schedule

Thursday, 9th December 2021

All times are in UTC, convert the starting time to your timezone here.

Activity	When
Opening	13h00 -- 13h30
Talks	13h30 -- 16h00
Break	16h00 -- 17h00
Contributed Challenge Problems	17h00 -- 19h00

Friday, 10th December 2021

All times are in UTC, convert the starting time to your timezone here.

Activity	When
Talks	13h00 -- 16h00
Break	16h00 -- 17h00
JuliaIntervals Round Table	17h00 -- 19h00

Saturday, 11th December 2021

It is sprint time! During this day we will use online platforms (Discord, GitHub) to create, discuss and implement solutions for the challenge problems, or other problems that you have proposed during these Days.

Reachathon

In the spirit of a Hackathon, our Reachathon is allocated to discuss and implement exploratory solutions to programming tasks related to the workshop.

Every contribution and initiative counts, from first-time contributors seeking guidance in ways to contribute to JuliaReach and JuliaIntervals packages, to developments of more advanced research topics or tools proposed in the Challenge problems session the first day of the workshop.

Program

Thursday, 9th December 2021

All times are in UTC, convert the starting time to your timezone here.

When	Activity	Speaker(s)
13h00 -- 13h30	Opening	Marcelo Forets and Luca Ferranti
13h30 -- 14h00	Talk 1: Synthesis of hybrid automata from time-series data A time series is a sequence of data points, each associated with a point in time. A hybrid automaton is a mathematical model of continuous dynamical systems with multiple operational modes. We present recent online and offline approaches to synthesize a hybrid automaton from a set of time series based on reachability analysis.	Miriam García Soto
14h00 -- 14h30	Talk 2: Exploring synergies between proof-based and reachability-based hybrid system verification This talk presents a joint work on integrating JuliaReach and reachability analysis into a refinement and proof-based system modelling and verification framework - Event-B. In particular, the talk attempts to demonstrate how reachability analysis can help to increase the verification automation of the hybrid system development in Event-B.	Paulius Stankaitis
14h30 -- 15h00	Talk 3: The Yarkovsky effect for asteroid Apophis The leading source of uncertainty to predict the orbital motion of asteroid (99942) Apophis is a non-gravitational acceleration arising from the anisotropic thermal re-emission of absorbed radiation, known as the Yarkovsky effect. Previous attempts to obtain this parameter from astrometry for this object have only yielded marginally small values, without ruling out a pure gravitational interaction. Here we present an independent estimation of the Yarkovsky effect based on optical and radar astrometry which includes observations obtained during 2021. Our approach is based on automatic differentiation techniques in terms of high-order Taylor series expansions both with respect to time and deviations with respect to a given orbital solution. Exploiting these techniques, we implement a Newton method for orbit determination, finding a non-zero Yarkovsky parameter, A2=(-2.899 ± 0.025) × 10-14 au/d2, with induced semi-major axis drift of (-199.0 ± 1.5) m/yr for Apophis. Finally, we discuss the impact hazard assessment problem for potentially hazardous asteroids and propose a parameterized orbit determination scheme, which allows to compute the time-evolution of the orbital uncertainty region via a high-order Taylor series parameterization.	Jorge Pérez-Hernández
15h00 -- 16h00	Talk 4: Overview of JuliaReach We illustrate different aspects of the JuliaReach package ecosystem using examples from the Applied Verification for Continuous and Hybrid Systems competition (ARCH-COMP'2021). We outline possibilities for contributing to JuliaReach, including 2022 GSOC project ideas.	Marcelo Forets
16h00 -- 17h00	Break	🍕
17h00 -- 17h20	Challenge Problem 1: Verification of Flight Control Algorithms Using Reachability Analysis Aircraft manufacturers have reached a high level of expertise and experience in flight control law design. The current design and analysis techniques applied in industry enable flight control engineers to address virtually any realistic design challenge. However, the development of flight control laws from concept to validation is a very complex, multi-disciplinary task, and the many problems that have to be solved make it a costly and lengthy process. The certification or air-worthiness assessment can be seen as the final step of the flight control system design, which takes place when a mature controller design is available and is ready for flight tests. In the certification or clearance process, which includes verification and validation, it has to be proven that the flight control laws have been designed such that the aircraft is safe to fly throughout the whole flight envelope, under all parameter variability and failure conditions. The role of the certification process is to demonstrate, via exhaustive analyses, that a catalogue of selected criteria expressing stability and handling requirements is fulfilled. In this talk we will present how reachability analysis can be a viable approach for flight control certification.	Raktim Bhattacharya
17h20 -- 17h40	Challenge Problem 2: Platoon of unicycle vehicles We consider a platoon of unicycle vehicles where the i-th vehicle follows the (i-1)-th and the relative displacements between the vehicles are controlled by a state-dependent feedback. The challenge is to verify a time-dependent safety constraint on the lateral distance between the vehicles as well as a safety bound on the horizontal displacements.	Arvind Adimoolam
17h40 -- 18h00	Challenge Problem 3: Robust control problem by scenario optimization In this challenge, we wish to prescribe a robust controller design that maximizes the probability of satisfactory performance (reliability) of a two-body spring system. An optimized controller must satisfy three reliability requirements, i.e., it must guarantee system stability, fast return to equilibrium (setting time), and low energy consumption (control effort). Note that stability, setting time and control effort are competitive requirements and, thus, a controller that minimizes the failure probability for one of the requirements inevitably increases the chance of failing the others. We provide samples and a numerical model for the system and the controller. The data and model must be used for the design evaluation and to characterize the uncertainty response of the system. Note that only a few samples are available to solve this problem, further complicating the uncertainty quantification and reliability assessment tasks.	Roberto Rocchetta
18h00 -- 18h20	Challenge Problem 4: A nonlinear truss structural dynamics problem using reachability analysis In this challenge, a simple truss-structure linear/nonlinear dynamics problem will be presented, where in the nonlinear case, large displacements are considered [1]. Basic Finite Element Method and Solid Dynamics concepts will be exposed, as well as the gold-standard numerical integration techniques. The recent application of Reachability Analysis to the linear case will be recalled [2]. The numerical results for the linear case using numerical integration and reachability will be obtained. Finally the nonlinear case problem will be clearly posed allowing to discuss possible novel approaches using reachability analysis.	Jorge Pérez Zerpa
18h20 -- 18h40	Challenge Problem 5: Polynomial Zonotopes in Julia For reachability of nonlinear differential equations, the non-convex set representation known as polynomial zonotopes has proved to be very competitive with respect to other approaches. Currently, polynomial zonotopes are only available in the Matlab tool CORA. This challenge consists of implementing sparse polynomial zonotopes and set operations in the Julia library LazySets.jl. This will serve as a solid groundwork to building reachability methods in the future.	Niklas Kochdumper

Friday, 10th December 2021

All times are in UTC, convert the starting time to your timezone here.

When	Activity	Speaker(s)
13h00 -- 13h30	Talk 5: Using Intersection of Unions to Minimize Multi-directional Linearization Error in Reachability Analysis Given an initial set of a nonlinear system with uncertain parameters and inputs, the set of states that can possibly be reached is computed. The approach is based on local linearizations of the nonlinear system, while linearization errors are considered by Lagrange remainders. These errors are added as uncertain inputs, such that the reachable set of the locally linearized system encloses the one of the original system. The linearization error is controlled by splitting of reachable sets. Reachable sets are represented by zonotopes, allowing an efficient computation in relatively high-dimensional space.	Arvind Adimoolam
13h30 -- 14h00	Talk 6: Soft-constrained interval predictor models and epistemic reliability intervals: A new tool for uncertainty quantification with limited experimental data This talk presents a new identification framework for Interval Predictor Models (IPMs) and an optimization method that soften the scenario constraints and trade-off between reliability and accuracy of the predictions. IPMs give non-probabilistic (interval) characterization of random processes, are constructed directly from data, and with no assumptions on the distribution family of the uncertainty affecting data-generating mechanisms. The reliability of an IPM defines the probability of correct interval predictions for future samples, and its value is always unknown in practice (due to finite samples sizes and poor understanding of the uncertainty affecting the process). Scenario optimization theory is used in this work to prescribe epistemic bounds on the IPM's reliability. The reliability bounds hold distribution-free, non-asymptotically, and quantify the uncertainty in the predictive error of the model. We test the framework on various test examples and discuss its strengths and limitations.	Roberto Rocchetta
14h00 -- 14h30	Talk 7: Confidence-based Contractor, Propagation and Potential Cloud for Differential Equations A novel interval contractor based on the confidence assigned to a random variable is proposed. It makes it possible to consider at the same time an interval in which the quantity is guaranteed to be, and a confidence level to reduce the pessimism induced by interval approach. This contractor consists in computing a confidence region. Using different confidence levels, a particular case of potential cloud can be computed. As application, we propose to compute the reachable set of an ordinary differential equation under the form of a set of confidence regions, with respect to confidence levels on initial value.	Julien A. dit Sandretto
14h30 -- 16h00	Talk 8: Overview of JuliaIntervals This talk will give an overview of the packages inside the JuliaIntervals organisation, focusing on their current status, limitations and development. The talk will also give a general overview of interval arithmetic and the IEEE 1788-2015 standard for it. This will set grounds for discussion in the round table after the break.	Luis Benet, Luca Ferranti, Benoît Richard, David Sanders
16h00 -- 17h00	Break	🍕
17h00 -- 19h00	Round table: JuliaIntervals status and roadmap This will be an opportunity for everyone interested in the JuliaIntervals ecosystem to discuss about the current status of the organisation and brainstorm ideas for further development. Particular emphasis will be given to IntervalArithmetic.jl roadmap towards version 1.0.	everyone willing to discuss