Differences between revisions 3 and 4
Revision 3 as of 2018-04-09 10:44:37
Size: 3703
Editor: akschmuck
Comment: Preliminary Schedule
Revision 4 as of 2018-04-09 11:38:44
Size: 3424
Editor: akschmuck
Comment:
Deletions are marked like this. Additions are marked like this.
Line 5: Line 5:
 * Place:  * Place: KL 111, videocast to SB ???
Line 11: Line 11:
The seminar will be organized as follows. Participants can choose to work individually or in a group. For each group/individual a particular compositional technique will be chosen. Each available topic comes with a reading list of 4-5 papers, which should be read and understood. Based on these papers (and possibly revealed related work), each group/individual should prepare a 45' presentation discussing the general mathematical problem statement and the features and limitations of the investigated compositional technique. This seminar will be registered at TU-KL, hence it will be possible for students to get credit for it. We shall organize meetings over video for Saarbruecken students. We will try to balance the work load to account for the fact that some students are seeking to get credit for this class, while other participants do not need credits. After an initial meeting in mid-April (TBA), we will have a reading phase during which every participant can contact us if he/she needs help on understanding the provided material. After that, we will have a number of meetings (depending on the number of participants) in late May/early June. In each meeting one group presents its insights and an open discussion among all participants on the transferability of those insights to other areas is encouraged. Each week we will discuss one topic, based on a representative paper. One participant is leading the discussion by giving some general introductional content for the current topic and then presenting the core priciples covered in the paper. After this, an open discussion among all participants on the current paper and on the transferability of those insights to other areas is encouraged.
Line 13: Line 13:
==== Preliminary Schedule: ==== ===== Preliminary Schedule: =====
Line 15: Line 15:
||Wed 18.4., 10am ||Supervisory Control Theory ||paper link ||Anne ||
||Wed 25.4., 10am ||Reactive Synthesis ||paper link ||Anne ||
||Wed 2.5., 10am ||Verification using Assume/Guarantee Contracts ||paper link ||Damien ||
||Wed 9.5., 10am ||Synthesis using Assume/Guarantee Contracts ||paper link ||Yunjun? ||
||Wed 16.5., 10am ||Maximal Permissiveness/ Partial Observation in Synthesis || ||Markus ||
||Wed 18.4., 10am ||Supervisory Control Theory || [[http://ieeexplore.ieee.org/abstract/document/4668520/|paper]] ||Anne ||
||Wed 25.4., 10am ||Reactive Synthesis ||[[https://link.springer.com/article/10.1007/s00236-016-0273-2|paper]] ||Anne ||
||Wed 2.5., 10am ||Verification using Assume/Guarantee Contracts ||[[|paper]] ||Damien ||
||Wed 9.5., 10am ||Synthesis using Assume/Guarantee Contracts ||[[http://ieeexplore.ieee.org/abstract/document/7602549/|paper]] ||Yunjun? ||
||Wed 16.5., 10am ||Maximal Permissiveness/ Partial Observation in Synthesis || [[https://link.springer.com/article/10.1007/s00236-015-0239-9|paper]] ||Markus ||
Line 21: Line 21:
||<#FF0000> Tue 29.5., 1pm ||Control of Continuous Time Systems || ||Anne ||
||Wed 6.6., 10am ||Control of Discrete Time Systems || ||Mahmoud ||
||Wed 13.6., 10am ||Abstraction-Based Controller Synthesis || ||Kaushik? ||
||Wed 20.6., 10am ||Compositional Symbolic Synthesis || ||? ||
||Wed 27.6., 10am ||Abstraction/Refinement Techniques? || ||Rupak? ||
||<#FF0000> Tue 29.5., 1pm ||Decentralized Control of Linear Continuous Time Systems || ||Anne ||
||Wed 6.6., 10am ||Small Gain Theorems ||[[https://www.sciencedirect.com/science/article/pii/S0947358011706008|paper]] ||Mahmoud ||
||Wed 13.6., 10am ||Abstraction-Based Controller Synthesis ||[[https://pdfs.semanticscholar.org/4369/56bce3f3dfb1082126851b8e4d3f813a9a56.pdf|paper]], [[http://ieeexplore.ieee.org/abstract/document/7857702/|paper]] ||Kaushik? ||
||Wed 20.6., 10am ||Compositional Symbolic Synthesis || [[http://ieeexplore.ieee.org/abstract/document/7403184/|paper]], [[http://ieeexplore.ieee.org/abstract/document/7799148/|paper]]|| Anne ||
||Wed 27.6., 10am ||Compositional Abstraction/Refinement Techniques? || ||Rupak? ||

Seminar: Compositional Techniques for Synthesis and Verification

General Information:

Abstract:

Large scale Cyber Physical Systems (CPS) consist of software, hardware, and physical components interacting in a non-trivial manner. Different parts of these systems are set up using very different design principles, ranging form correct-by-design controllers for physical systems modeled by continuous differential equations, to communication protocols, to code generated by compilers with various characteristics. Due to this intrinsic variability of components and the size of the overall system, synthesis or verification tools cannot be efficiently applied in a monolithic manner to ensure that CPS are safe and work as intended. As a first step towards compositional synthesis and verification techniques for CPS, this seminar investigates existing compositional techniques in relevant sub-domains of CPS analysis and design. We will discuss state-of-the art compositional techniques including for example controller synthesis for continuous-time systems, reactive synthesis over game graphs, or verification of software. We are flexible to shrink or extend the topics dependent on the interests and the number of the participants of the seminar.

Organization:

Each week we will discuss one topic, based on a representative paper. One participant is leading the discussion by giving some general introductional content for the current topic and then presenting the core priciples covered in the paper. After this, an open discussion among all participants on the current paper and on the transferability of those insights to other areas is encouraged.

Preliminary Schedule:

Date

Topic

Paper links

Presenter

Wed 18.4., 10am

Supervisory Control Theory

paper

Anne

Wed 25.4., 10am

Reactive Synthesis

paper

Anne

Wed 2.5., 10am

Verification using Assume/Guarantee Contracts

[[|paper]]

Damien

Wed 9.5., 10am

Synthesis using Assume/Guarantee Contracts

paper

Yunjun?

Wed 16.5., 10am

Maximal Permissiveness/ Partial Observation in Synthesis

paper

Markus

Wed 23.5., 10am

?

Tue 29.5., 1pm

Decentralized Control of Linear Continuous Time Systems

Anne

Wed 6.6., 10am

Small Gain Theorems

paper

Mahmoud

Wed 13.6., 10am

Abstraction-Based Controller Synthesis

paper, paper

Kaushik?

Wed 20.6., 10am

Compositional Symbolic Synthesis

paper, paper

Anne

Wed 27.6., 10am

Compositional Abstraction/Refinement Techniques?

Rupak?

Wed 4.7., 10am

?

Courses/CompositionalSynthesisVerification (last edited 2018-07-02 14:02:28 by akschmuck)