Differences between revisions 23 and 24
⇤ ← Revision 23 as of 2018-04-19 07:26:05 →
Size: 4920
Editor: akschmuck
Comment:
← Revision 24 as of 2018-04-19 08:25:53 → ⇥
Size: 5330
Editor: akschmuck
Comment:
Deletions are marked like this. Additions are marked like this.
Line 20: Line 20:
    * Course Notes from my former Supervisor, however, I never taught that particular class:     * Course Notes by Jörg Raisch
Line 34: Line 34:
    Somehow there is no standard reference for an introduction to RS. I personally like the following:
    * First part of Rüdiger Ehlers PhD Thesis:		     Somehow there is no good standard reference for an introduction to RS. Nevertheless, here are some pointers:
    * I personally like the first part of Rüdiger Ehlers PhD Thesis as an introduction to RS:
Line 37: Line 37:
    * This paper by Zielonka     * There is also a general book on "Automata, Logics, and Infinite Games", by Erich Graedel, Wolfgang Thomas, Thomas Wilke,
      [[https://link.springer.com/content/pdf/10.1007%2F3-540-36387-4.pdf|link]] (Part I covers topics relevant for this seminar)
    * This paper by Zielonka also gives a general introduction to infinite games
Line 42: Line 44:
    In this session we will recap some basics of SCT (see session (1)) and then discuss the connection between SCT and RS established here:
    * [[https://link.springer.com/article/10.1007%2Fs10626-015-0223-0|link]]		     In this session we will      * recap some basics of SCT (see session (1)),
    * discuss the connection between SCT and RS established here:
       [[https://link.springer.com/article/10.1007%2Fs10626-015-0223-0|link]]
    * discuss a different connection w.r.t. safety games.
Line 46: Line 51:
 * '''(4)''' Wed 9.5., 10am, Reduction of LTL to safety / Zielonka automata?  * '''(4)''' Wed 9.5., 10am, Compositional synthesis for safety specifications
    * We will discuss some compositional synthesis techniques for safety, e.g., this one:
     [[http://ieeexplore.ieee.org/abstract/document/7799148/|paper]]
    * We will reduce the compositional methods for SCT to safety and see if there is a connection
Line 49: Line 57:
 * '''(5)''' Wed 16.5., 10am, Compositional synthesis for safety
     [[http://ieeexplore.ieee.org/abstract/document/7799148/|paper]]

 * '''(6)''' Wed 23.5., 10am, A/G methods for safety verification (Damien)
    [[https://link.springer.com/chapter/10.1007%2FBFb0028738|paper]]

 * '''(7)''' Tue 29.5., 1pm, ? A/G methods for Synthesis in Boolean networks (Mahmoud?)
   [[http://ieeexplore.ieee.org/abstract/document/7602549/|paper]]

 * '''(8)''' Wed 6.6., 10am, Introduction to SCT over omega-languages
  

 * '''(9)''' Wed 13.6., 10am, omega-SCT vs GR(1)		  * '''(5)''' Wed 16.5., 10am, Some related topics
    * Reduction of LTL to safety
    * Zielonka automata?
Line 64: Line 62:
 * '''(10)''' Wed 20.6., 10am, Assume-Admissible Synthesis (Marcus?)  * '''(6)''' Wed 23.5., 10am, Introduction to A/G methods

 * '''(7)''' Tue 29.5., 1pm, A/G methods for compositional safety verification
    e.g. [[https://link.springer.com/chapter/10.1007%2FBFb0028738|paper]]

 * '''(8)''' Wed 6.6., 10am, A/G methods for Synthesis in Boolean networks
   e.g. [[http://ieeexplore.ieee.org/abstract/document/7602549/|paper]]

 * '''(9)''' Wed 13.6., 10am, Assume-Admissible Synthesis
Line 67: Line 73:
 * '''(11)''' Wed 27.6., 10am, A compositional setting for RS w.r.t. LTL
 [[https://link.springer.com/article/10.1007/s00236-015-0239-9|paper]] 		 * '''(10)''' Wed 20.6., 10am,
Line 70: Line 75:
 * '''(12)''' Wed 4.7., 10am, Discussion: Compositional techniques bejond safety  * '''(11)''' Wed 27.6., 10am,

 * '''(12)''' Wed 4.7., 10am,

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

    • Some background Material on Basics for Supervisory Control Theory (SCT):
      • Course Notes by Jörg Raisch

        • link (parts of the introduction and section 4 are relevant for this seminar)

      • Course Notes of W.M. Wonham (the "father" of SCT)

        • link (sec. 1 and 2 give very detailed preliminaries, section 3 is an introduction to SCT)

      • THE standard textbook on SCT by S. Lafortune and C. Cassandras:

        • link (available through the MPI-SWS library via SpringerLink) (sec. 3 is on SCT)

  • (2) Wed 25.4., 10am, Introduction to Reactive Synthesis (RS)

    • Somehow there is no good standard reference for an introduction to RS. Nevertheless, here are some pointers:
    • I personally like the first part of Rüdiger Ehlers PhD Thesis as an introduction to RS:
    • There is also a general book on "Automata, Logics, and Infinite Games", by Erich Graedel, Wolfgang Thomas, Thomas Wilke,

      • link (Part I covers topics relevant for this seminar)

    • This paper by Zielonka also gives a general introduction to infinite games

      • link (section 1--6 are sufficient)

  • (3) Wed 2.5., 10am, Supervisory Control vs. Reactive Synthesis

    • In this session we will
    • recap some basics of SCT (see session (1)),
    • discuss the connection between SCT and RS established here:
    • discuss a different connection w.r.t. safety games.

  • (4) Wed 9.5., 10am, Compositional synthesis for safety specifications

    • We will discuss some compositional synthesis techniques for safety, e.g., this one:
    • We will reduce the compositional methods for SCT to safety and see if there is a connection

  • (5) Wed 16.5., 10am, Some related topics

    • Reduction of LTL to safety
    • Zielonka automata?

  • (6) Wed 23.5., 10am, Introduction to A/G methods

  • (7) Tue 29.5., 1pm, A/G methods for compositional safety verification

  • (8) Wed 6.6., 10am, A/G methods for Synthesis in Boolean networks

  • (9) Wed 13.6., 10am, Assume-Admissible Synthesis

  • (10) Wed 20.6., 10am,

  • (11) Wed 27.6., 10am,

  • (12) Wed 4.7., 10am,

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