About

The School on Formal Methods for Cyber-Physical Systems addresses the foundations, techniques, and tools for analysis, verification, control, synthesis, implementation, and applications of cyber-physical systems (CPS). Applications mainly deal with engineering and natural systems, including signal circuits, robotics, automotive and avionics, large-scale infrastructure networks, as well as biochemical and physiological processes.

Topics of interest include, but are not limited to:

  • Design, synthesis, planning and control (including real-time and resource-aware control);
  • Analysis, automated verification (Boolean or quantitative), certification, validation, and testing;
  • Model building from data (via learning) and model simulation;
  • Network science and control over networks.
  • Mathematical foundations, computability and complexity;
  • Programming languages, specification formalisms;
  • Software tool engineering and experimentation.

This first edition of the school has the goal of presenting the state of the art of the current techniques in controller synthesis for hybrid systems, to enable doctoral students and young researchers to advance the field and apply the developed methodologies to concrete scenarios promoting their application in the industrial practice.

The school is supported by grants from the PhD School in Natural Sciences and Engineering and the Department of Computer Science of the University of Verona.

The school is co-located with the Forum on specification & Design Languages (FDL 2017), to be held in Verona, 18-20 September 2017 (https://ecsi.org/fdl). Special arrangements will be provided to the participants to the school who register also to FDL (TBD).





When

From 12/09/2017 to 16/09/2017
add to your calendar

Where

Dipartimento di Informatica
Strada le Grazie 15, Verona (Italy)
view accommodation info
show on Google Maps /

By plane

The airport of Verona is connected to the main European and national cities. From the airport you can reach the city by taxi or by bus. A shuttle bus connects the airport to Verona Porta Nuova train station.

By Train

The train station of Verona Porta Nuova is connected with all the main Italian cities by fast and local trains. For the train schedule, please check the Italian railway company. From the station you can reach the Department of Computer Science by bus or by taxi.

By bus

Bus line 21 (towards S. Giovanni Lupatoto) get off at the first bus stop after Borgo Roma hospital; from the bus stop, you can see the department’s buildings. You can also catch bus line 22 (towards Policlinico/San Giovanni Lupatoto) and line 93 (during the night and on Sundays), towards Cadidavid. For these last two bus lines, get off at Borgo Roma hospital, then follow the map below. You can find timetables and line maps at the ATV website.

By car
Take the A4 Milano-Venezia highway, exit Verona Sud then follow the direction "Ospedale Borgo Roma" (hospital), on the right. At the hospital, go straight, cross the small bridge on a river and take the second right. From here you can see the department buildings on your left.



The registrations are closed.


Tarsie in Santa Maria in Organo, Verona
Tarsia of Santa Maria in Organo church in Verona

Lecturers

Schedule


TimeSpeakerTitle

08:30–09:30

Angelo Montanari The Synthesis Problem: Introduction to the problem and the solution

09:30–10:30

Angelo Montanari The Synthesis Problem: From S1S to deterministic Muller automata

10:30–10:45

Coffee break

10:45–11:45

Tiziano Villa Modular Synthesis of Component-based Systems: Component-based Design by Solving Language Equations

11:45–12:45

Davide Bresolin Timed Models: Formal models of real-time systems

12:45–14:00

Lunch

14:00–15:00

Marco Faella Controller Synthesis for Linear Hybrid Systems: Models of Hybrid Systems and their Decidability

15:00–16:00

Marco Faella Controller Synthesis for Linear Hybrid Systems: Linear Hybrid Games

16:00–16:15

Coffee break

16:15–17:15

Matthias Rungger Automated synthesis for nonlinear control systems - a symbolic approach: Motivation, Systems, Specifications, Closed Loop

TimeSpeakerTitle

08:30–09:30

Marco Faella Controller Synthesis for Linear Hybrid Systems: Control with Reachability Objective

09:30–10:30

Matthias Rungger Automated synthesis for nonlinear control systems - a symbolic approach: Abstraction and Refinement, Feedback Refinement Relations, Symbolic Models

10:30–10:45

Coffee break

10:45–11:45

Matthias Rungger Automated synthesis for nonlinear control systems - a symbolic approach: Computation of Symbolic Models, Growth Bound

11:45–12:45

Angelo Montanari The Synthesis Problem: From Muller automata to Muller games

12:45–14:00

Lunch

14:00–15:00

Angelo Montanari The Synthesis Problem: From Muller games to parity games

15:00–16:00

Jan Van Schuppen Control Synthesis of Piece-wise Affine Hybrid Systems on Polytopes: Control Problems of Piecewise-affine Hybrid Systems

16:00–16:15

Coffee break

16:15–17:15

Marco Faella Controller Synthesis for Linear Hybrid Systems: Hand-on laboratory

17:15–18:15

Matthias Rungger Automated synthesis for nonlinear control systems - a symbolic approach: Hands-on laboratory

TimeSpeakerTitle

08:30–09:30

Nina Yevtushenko Timed Models: Component-based Optimization of Timed Models via Equation Solving

09:30–10:30

Salvatore La Torre Modular Synthesis of Component-based Systems: Automata-theoretic Modular Synthesis of Component-based Systems

10:30–10:45

Coffee break

10:45–11:45

Pietro Sala Interval-based synthesis

11:45–12:45

Jan Van Schuppen Control Synthesis of Piece-wise Affine Hybrid Systems on Polytopes: Control Synthesis in case of Complete Observations

12:45–14:00

Lunch

14:00–15:00

Andrea Orlandini Reliable Temporal Planning and Execution Systems: Temporal Planning and Execution with Uncertainty

15:00–16:00

Andrea Orlandini Temporal Planning and Execution with Uncertainty: Validation & Verification Issues in Planning & Scheduling

19:00–23:00

Social Dinner

TimeSpeakerTitle

08:30–09:30

Ruediger Ehlers Practical Reactive Synthesis: From the Theory to the Practice of Reactive Synthesis

09:30–10:30

Ruediger Ehlers Practical Reactive Synthesis: Bounded Synthesis

10:30–10:45

Coffee break

10:45–11:45

Andrea Orlandini Reliable Temporal Planning and Execution Systems: TGA-based Controllers for Robust Plan Execution

11:45–12:45

Andrea Orlandini Reliable Temporal Planning and Execution Systems: Hands-on laboratory

12:45–14:00

Lunch

14:00–15:00

Leonardo Mangeruca Control design and verification of cyber-physical systems: the industrial perspective

15:00–16:00

Jan Van Schuppen Control Synthesis of Piece-wise Affine Hybrid Systems on Polytopes: Control Synthesis in case of Partial Observations and Generalizations

16:00–16:15

Coffee break

16:15–17:15

Enrico Tronci Automatic Synthesis of Control Software for Discrete Time Hybrid Systems: Control Software Synthesis for Discrete Time Linear Hybrid Systems

TimeSpeakerTitle

08:30–09:30

Enrico Tronci Automatic Synthesis of Control Software for Discrete Time Hybrid Systems: Trading Closed-loop System Non-functional Requirements with Control Software Non-functional Requirements

09:30–10:30

Enrico Tronci Automatic Synthesis of Control Software for Discrete Time Hybrid Systems: Linearizing Discrete Time Hybrid Systems

10:30–10:45

Coffee break

10:45–11:45

Ruediger Ehlers Practical Reactive Synthesis: Generalized Reactivity(1) Synthesis

11:45–12:45

Ruediger Ehlers Practical Reactive Synthesis: Symbolic Game Solving

12:45–14:00

Lunch

14:00–15:00

Federico Mari Automatic Synthesis of Control Software for Discrete Time Hybrid Systems: Hands-on laboratory

15:00–16:00

Ruediger Ehlers Practical Reactive Synthesis: Hands-on laboratory

Social Events

Scientific Committee

Paolo Fiorini, Dipartimento di Informatica, Università di Verona, Italy
Angelo Montanari, Dipartimento di Informatica e Matematica, Università di Udine, Italy
Riccardo Muradore, Dipartimento di Informatica, Università di Verona, Italy
Tiziano Villa, Dipartimento di Informatica, Università di Verona, Italy

Organizers

Marta Capiluppi, Dipartimento di Informatica, Università di Verona, Italy (marta.capiluppi@univr.it)
Luca Geretti, Dipartimento di Informatica, Università di Verona, Italy (luca.geretti@univr.it)
Pietro Sala
, Dipartimento di Informatica, Università di Verona, Italy (pietro.sala@univr.it)
Tiziano Villa
, Dipartimento di Informatica, Università di Verona, Italy (tiziano.villa@univr.it)