|
Size: 3401
Comment:
|
Size: 3524
Comment:
|
| Deletions are marked like this. | Additions are marked like this. |
| Line 17: | Line 17: |
| * Wed 18.4., 10am, Coordinated Supervisory Control | * '''(1)''' Wed 18.4., 10am, Coordinated Supervisory Control |
| Line 20: | Line 20: |
| * Wed 25.4., 10am, Introduction to Reactive Synthesis | * '''(2)''' Wed 25.4., 10am, Introduction to Reactive Synthesis |
| Line 23: | Line 23: |
| * Wed 2.5., 10am, Supervisory Control vs. Reactive Synthesis | * '''(3)''' Wed 2.5., 10am, Supervisory Control vs. Reactive Synthesis |
| Line 26: | Line 26: |
| * Wed 9.5., 10am, Reduction of LTL to safety / Zielonka automata? | * '''(4)''' Wed 9.5., 10am, Reduction of LTL to safety / Zielonka automata? |
| Line 29: | Line 29: |
| * Wed 16.5., 10am, Compositional synthesis for safety | * '''(5)''' Wed 16.5., 10am, Compositional synthesis for safety |
| Line 32: | Line 32: |
| * Wed 23.5., 10am, A/G methods for safety verification (Damien) | * '''(6)''' Wed 23.5., 10am, A/G methods for safety verification (Damien) |
| Line 35: | Line 35: |
| * Tue 29.5., 1pm, ? A/G methods for Synthesis in Boolean networks (Mahmoud?) | * '''(7)''' Tue 29.5., 1pm, ? A/G methods for Synthesis in Boolean networks (Mahmoud?) |
| Line 38: | Line 38: |
| * Wed 6.6., 10am, Introduction to SCT over omega-languages | * '''(8)''' Wed 6.6., 10am, Introduction to SCT over omega-languages |
| Line 41: | Line 41: |
| * Wed 13.6., 10am, omega-SCT vs GR(1) | * '''(9)''' Wed 13.6., 10am, omega-SCT vs GR(1) |
| Line 44: | Line 44: |
| * Wed 20.6., 10am, Assume-Admissible Synthesis (Marcus?) | * '''(10)''' Wed 20.6., 10am, Assume-Admissible Synthesis (Marcus?) |
| Line 47: | Line 47: |
| * Wed 27.6., 10am, A compositional setting for RS w.r.t. LTL | * '''(11)''' Wed 27.6., 10am, A compositional setting for RS w.r.t. LTL |
| Line 50: | Line 50: |
| * Wed 4.7., 10am, Discussion: Compositional techniques bejond safety | * '''(12)''' Wed 4.7., 10am, Discussion: Compositional techniques bejond safety |
Seminar: Compositional Techniques for Synthesis and Verification
General Information:
Instructor: Anne-Kathrin Schmuck, Rupak Majumdar
- Time: Wednesday, 10am
- Place: KL building G 26 room 111, videocast to SB building E1.5 room 105
- Intended Audience: Master or PhD students from computer science or electrical engineering with a special interest in control/synthesis and verification.
- Grading: The final grade will be based on the paper presentation and participation in class.
- Paper Assignment: Please talk to the instructors for a paper assignment based on your interests.
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.
Organization:
Each week we will discuss one topic, based on a representative paper. One participant or the instructor is leading the discussion by giving some general instructional content for the current topic and then presenting the core principles 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:
(1) Wed 18.4., 10am, Coordinated Supervisory Control
(2) Wed 25.4., 10am, Introduction to Reactive Synthesis
(3) Wed 2.5., 10am, Supervisory Control vs. Reactive Synthesis
(4) Wed 9.5., 10am, Reduction of LTL to safety / Zielonka automata?
(5) Wed 16.5., 10am, Compositional synthesis for safety
(6) Wed 23.5., 10am, A/G methods for safety verification (Damien)
(7) Tue 29.5., 1pm, ? A/G methods for Synthesis in Boolean networks (Mahmoud?)
(8) Wed 6.6., 10am, Introduction to SCT over omega-languages
(9) Wed 13.6., 10am, omega-SCT vs GR(1)
(10) Wed 20.6., 10am, Assume-Admissible Synthesis (Marcus?)
(11) Wed 27.6., 10am, A compositional setting for RS w.r.t. LTL
(12) Wed 4.7., 10am, Discussion: Compositional techniques bejond safety