Differences between revisions 11 and 48 (spanning 37 versions)
⇤ ← Revision 11 as of 2018-04-09 12:37:40 →
Size: 3875
Editor: akschmuck
Comment:
← Revision 48 as of 2018-07-02 14:02:28 → ⇥
Size: 8420
Editor: akschmuck
Comment:
Deletions are marked like this. Additions are marked like this.
Line 1: Line 1:
#acl akschmuck:read,write,delete,revert,admin rupak:read,write,delete,revert,admin All:read
Line 5: Line 7:
 * Place: KL building G 26 room 111, videocast to SB building E1.5 room  ???
 * Intended Audience: Master or PhD students from computer science or electrical engineering, with a special interest in control/synthesis and verification.		  * Place: KL building G 26 room 113, 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.
Line 11: Line 13:
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. 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.
Line 14: Line 16:
Each week we will discuss one topic, based on a representative paper. One participant 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. 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.
Line 16: Line 18:
===== Preliminary Schedule: =====
||Date ||Topic ||Paper links ||Presenter ||
||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 ||[[https://link.springer.com/chapter/10.1007%2FBFb0028738|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? ||
||Wed 23.5., 10am ||? || || ||
||<#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? ||
||Wed 4.7., 10am ||? || || ||		 ==== Preliminary Schedule: ====
 * '''(1)''' Wed 18.4., 10am, Coordinated Supervisory Control
 [[https://dl.acm.org/citation.cfm?id=2756745|paper]]
   Some background Material on Basics for Supervisory Control Theory (SCT):
    * Course Notes by Jörg Raisch
      [[http://www.control.tu-berlin.de/wiki/images/4/40/DESnotes_v17.pdf| link]]
      (parts of the introduction and section 4 are relevant for this seminar)

    * Course Notes of W.M. Wonham (the "father" of SCT)
      [[http://www.se.wtb.tue.nl/_media/wonham/wonham_scdes2010.pdf|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:
      [[https://link.springer.com/book/10.1007%2F978-0-387-68612-7|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:
      [[https://www.ruediger-ehlers.de/papers/DissertationEhlers.pdf|link]] (part 1)
    * A nice read without too much formalization are also the lecture notes by Bernd Finkbeiner :
      [[https://www.react.uni-saarland.de/publications/F16.pdf|link]]
    * 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
      [[https://www.sciencedirect.com/science/article/pii/S0304397598000097|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:
       [[https://link.springer.com/article/10.1007%2Fs10626-015-0223-0|link]]
    * discuss a different connection w.r.t. safety specifications


 * '''(4)''' Wed 9.5., 10am, Supervisory Control vs. Reactive Synthesis (cond.)
    * We will extend the the discussed connection to omega-languages
    
    
 * '''(5)''' Wed 16.5., 10am, Comparison of Alternative Treatments of Assumptions in Reactive Synthesis
    * We will discuss the following approaches
        * Assume-Guarantee Synthesis [[https://link.springer.com/chapter/10.1007/978-3-540-71209-1_21|paper1]], and [[https://ac.els-cdn.com/S0304397506004816/1-s2.0-S0304397506004816-main.pdf?_tid=36b739de-6956-4f8d-b80a-7a94b42d9f06&acdnat=1526374156_0ceac53502225991b1db34e1af1974cd|paper2]]
        * Rational Synthesis [[https://link.springer.com/chapter/10.1007/978-3-642-12002-2_16|paper 1]], [[https://link.springer.com/chapter/10.1007/978-3-319-17130-2_15|paper 2]]
        * Assume-Admissible Synthesis [[https://link.springer.com/article/10.1007/s00236-016-0273-2|paper]]
        * Oblidging Games [[https://link.springer.com/chapter/10.1007/978-3-642-15375-4_20|paper]]
        * Cooperative Reactive Synthesis [[https://link.springer.com/chapter/10.1007/978-3-319-24953-7_29|paper]]

 * '''(6)''' Wed 23.5., '''no seminar'''


 * '''(7)''' Tue 29.5., 1pm, A/G methods for compositional safety verification '''(Damien presenting)'''
   * The notes for this session are available online here: [[https://github.com/dzufferey/presentations/blob/master/2018_05_29_ag_verification.md|notes]]
   * the mentioned related paper is this one: [[https://link.springer.com/chapter/10.1007%2FBFb0028738|link]]

 * '''(8)''' Wed 6.6., 10am, games with transferable payoffs for cooperative synthesis '''(Kaushik presenting)'''
   * The presentation will be based on the following papers:
      * Stable partitions in coalitional games [[https://arxiv.org/abs/cs/0605132|paper]]
      * Coalition formation games for dynamic multirobot tasks [[http://journals.sagepub.com/doi/pdf/10.1177/0278364915595707|paper]]
      * Coalitional game theory for communication networks [[https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=5230848&tag=1|paper]]
     
 * '''(9)''' Wed 13.6., 10am, Distributed Reactive Synthesis
    * We will discuss the classic setting for distributed reactive synthesis [[https://ieeexplore.ieee.org/abstract/document/89597/|paper]], [[https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=932514|paper]], [[https://ieeexplore.ieee.org/abstract/document/1509236/|paper]], [[http://cgi.csc.liv.ac.uk/~sven/PhD.pdf|phd thesis]]
    * We will discuss a setting based on Zielonka automata [[https://link.springer.com/chapter/10.1007/978-3-662-47666-6_2|paper]], [[https://www.sciencedirect.com/science/article/pii/S0304397515006891|paper]] [[https://pdfs.semanticscholar.org/fe68/850c47c8f6130ebbb537591bbb7f6fee7918.pdf|paper]]
    * We will try to establish a connection to decentralized/hierarchical SCT

 * '''(10)''' Wed 20.6., 10am, Adapting contracts in Reactive Synthesis '''(Marcus presenting)'''
      * We will discuss this paper [[https://arxiv.org/pdf/1611.07621.pdf|paper]]
      * and possibly these ones [[https://ieeexplore.ieee.org/abstract/document/7602549/|paper]] and [[https://link.springer.com/chapter/10.1007%2F978-3-540-85361-9_14|paper]]
      * see also [[https://link.springer.com/content/pdf/10.1007%2F978-3-319-19249-9_3.pdf|paper]] and [[https://users.ics.aalto.fi/stavros/papers/cag_acsd_2015.pdf|paper]] on circular A/G contracts

 * '''(11)''' Wed 27.6., 10am, '''no seminar'''

 * '''(12)''' Wed 4.7., 10am, Decentralized Reactive Synthesis -- a control view '''(Mahmoud presenting)'''
      * We will discuss these two papers [[https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7403184| paper]], [[https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7799148|paper]]

 * '''(13)''' Wed 11.7., 10am, Games with transferable payoff '''(Ivan presenting)'''

Seminar: Compositional Techniques for Synthesis and Verification

General Information:

  • Instructor: Anne-Kathrin Schmuck, Rupak Majumdar

  • Time: Wednesday, 10am
  • Place: KL building G 26 room 113, 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:
      • A nice read without too much formalization are also the lecture notes by Bernd Finkbeiner :
      • 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 specifications

  • (4) Wed 9.5., 10am, Supervisory Control vs. Reactive Synthesis (cond.)

    • We will extend the the discussed connection to omega-languages

  • (5) Wed 16.5., 10am, Comparison of Alternative Treatments of Assumptions in Reactive Synthesis

    • We will discuss the following approaches

  • (6) Wed 23.5., no seminar

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

    • The notes for this session are available online here: notes

    • the mentioned related paper is this one: link

  • (8) Wed 6.6., 10am, games with transferable payoffs for cooperative synthesis (Kaushik presenting)

    • The presentation will be based on the following papers:

      • Stable partitions in coalitional games paper

      • Coalition formation games for dynamic multirobot tasks paper

      • Coalitional game theory for communication networks paper

  • (9) Wed 13.6., 10am, Distributed Reactive Synthesis

    • We will discuss the classic setting for distributed reactive synthesis paper, paper, paper, phd thesis

    • We will discuss a setting based on Zielonka automata paper, paper paper

    • We will try to establish a connection to decentralized/hierarchical SCT

  • (10) Wed 20.6., 10am, Adapting contracts in Reactive Synthesis (Marcus presenting)

  • (11) Wed 27.6., 10am, no seminar

  • (12) Wed 4.7., 10am, Decentralized Reactive Synthesis -- a control view (Mahmoud presenting)

  • (13) Wed 11.7., 10am, Games with transferable payoff (Ivan presenting)

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