From Timed Automata to Stochastic Hybrid Games - Model Checking, Synthesis, Refinement, Performance Analysis and Machine Learning

  • Welcome to From Timed Automata to Stochastic Hybrid Games - Model Checking, Synthesis, Refinement, Performance Analysis and Machine Learning
     Description:

    Timed automata and games, priced timed automata and energy automata have emerged as useful formalisms for modeling real-time and energy-aware systems as found in several embedded and cyber-physical systems. During the last 20 years the real-time model checker UPPAAL has been developed allowing for efficient verification of hard timing constraints of timed automata. Moreover a number of significant branches exists, e.g. UPPAAL CORA providing efficient support for optimization, and UPPAAL TIGA allowing for automatic synthesis of strategies for given safety and liveness objectives, and ECDAR supports refinement and compositional development of real-time systems. Also the branch UPPAAL SMC, provides a highly scalable new engine supporting (distributed) statistical model checking of stochastic hybrid automata, and most recently the new branch UPPAAL STRATEGO supporting safe and optimal strategies for stochastic hybrid games by combining symbolic methods with machine learning. The course will review the various branches of UPPAAL, the corresponding modeling formalisms as well as the symbolic or statistical algorithms applied. Also, examples on applications of the tools suite will be given to a range of real-time and cyber-physical examples including schedulability and performance evaluation of mixed criticality systems, modeling and analysis of biological systems, energy-aware wireless sensor networks, smart grids and smart houses and battery scheduling.

    Prerequisites: A general background in computer science or a related engineering discipline with modeling experience.

    Learning objectives: The objectives of the course is to give the participants a deep understanding of the possibilities and limitations of the UPPAAL tool suite. And to give them hands-on experience with using the tools as well as an understanding of the underlying algorithms.

    Organiser: Ulrik Nyman ulrik@cs.aau.dk

    Lecturers: Kim G Larsen, Marius Mikucionis, Ulrik Nyman

    ECTS: 2

    Time: 6 times.  All days from 8:15 to 12:00

    • Monday 27th of November
    • Tuesday 28th of November
    • Wednesday 29th of November
    • Monday 4th of December
    • Tuesday 5th of December
    • Wednesday the 6th of December

    Place: Selma Lagerlöfs Vej 300

    Zip code: 9220

    City: Aalborg

    Number of seats: 20

    Deadline: 13 November

    Important information concerning PhD courses We have over some time experienced problems with no-show for both project and general courses. It has now reached a point where we are forced to take action. Therefore, the Doctoral School has decided to introduce a no-show fee of DKK 5,000 for each course where the student does not show up. Cancellations are accepted no later than 2 weeks before start of the course. Registered illness is of course an acceptable reason for not showing up on those days. Furthermore, all courses open for registration approximately three months before start. This can hopefully also provide new students a chance to register for courses during the year. We look forward to your registration.