Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
lat [2011/03/01 20:34]
jobstman
lat [2012/01/09 15:24] (current)
radu.iosif
Line 19: Line 19:
  
 **Bibliography** **Bibliography**
-      - M. Vardi. [[http://​www.cs.rice.edu/​~vardi/​papers/​icla09.pdf/​|From Philosophical to Industrial Logics]] {{slides.pdf}}+      - M. Vardi. [[http://​www.cs.rice.edu/​~vardi/​papers/​icla09.pdf/​|From Philosophical to Industrial Logics]] {{:slides.pdf|}}
       - W. Thomas. Handbook of Theoretical Computer Science, Volume B, Chapter 4. Automata on Infinite Objects       - W. Thomas. Handbook of Theoretical Computer Science, Volume B, Chapter 4. Automata on Infinite Objects
       - B. Khoussainov and A. Nerode. Automata Theory and its Applications. ISBN 0-8176-4207-2       - B. Khoussainov and A. Nerode. Automata Theory and its Applications. ISBN 0-8176-4207-2
       - D. Perrin and J.E. Pin. Infinite Words. ISBN 0-12-532111-2       - D. Perrin and J.E. Pin. Infinite Words. ISBN 0-12-532111-2
       - [[http://​tata.gforge.inria.fr/​|Tree Automata Techniques and Applications]] Collective Online Book       - [[http://​tata.gforge.inria.fr/​|Tree Automata Techniques and Applications]] Collective Online Book
-      - M. Vardi. The Buchi Complementation Saga. {{stacs07.pdf}}+      - M. Vardi. The Buchi Complementation Saga. {{:stacs07.pdf|}}
       - S. Schewe. Büchi complementation made tight. [[http://​arxiv.org/​PS_cache/​arxiv/​pdf/​0902/​0902.2152v1.pdf|STACS 2009]]       - S. Schewe. Büchi complementation made tight. [[http://​arxiv.org/​PS_cache/​arxiv/​pdf/​0902/​0902.2152v1.pdf|STACS 2009]]
       - A genealogy of LTL to Buechi automata translations [[http://​spot.lip6.fr/​wiki/​LtlTranslationAlgorithms]]       - A genealogy of LTL to Buechi automata translations [[http://​spot.lip6.fr/​wiki/​LtlTranslationAlgorithms]]
Line 30: Line 30:
       - V. Bruyere, G. Hansel, C. Michaux and R. Villemairez. Logic and p-Recognizable Sets of Integers. {{BRU.pdf}}       - V. Bruyere, G. Hansel, C. Michaux and R. Villemairez. Logic and p-Recognizable Sets of Integers. {{BRU.pdf}}
       - M. Jurdzinski, J. Voege. A Discrete Stratety Improvement Algorithm for Solving Parity Games. [[http://​www.brics.dk/​RS/​00/​48/​BRICS-RS-00-48.pdf|pdf]]       - M. Jurdzinski, J. Voege. A Discrete Stratety Improvement Algorithm for Solving Parity Games. [[http://​www.brics.dk/​RS/​00/​48/​BRICS-RS-00-48.pdf|pdf]]
-      - U. Zwick and M. Paterson. The Complexity of Mean Payoff Games. {{:​snsb_course:​mean-payoff.pdf|}}+      - U. Zwick and M. Paterson. The Complexity of Mean Payoff Games. {{:​mean-payoff.pdf|}}
       - Note about Karp's minimal mean-cycle algorithm. [[http://​webcourse.cs.technion.ac.il/​236359/​Spring2010/​ho/​WCFiles/​MMC.ps|ps]]       - Note about Karp's minimal mean-cycle algorithm. [[http://​webcourse.cs.technion.ac.il/​236359/​Spring2010/​ho/​WCFiles/​MMC.ps|ps]]
  
Line 39: Line 39:
       - GAVS+: An Open Platform for the Research of Algorithmic Game Solving: http://​www6.in.tum.de/​~chengch/​gavs/​       - GAVS+: An Open Platform for the Research of Algorithmic Game Solving: http://​www6.in.tum.de/​~chengch/​gavs/​
  
-===== Ecole Doctorale Grenoble (2010) ​=====+===== ENS Lyon Course on Automata-Theoretic Model Checking ​=====
  
-**Slides for lectures on game theory** (23/11 and 30/11)+[[http://​www.ens-lyon.fr/​DI/?​p=2320|ER01 : vérification et certification du logiciel]] 
 + 
 +**Slides** 
 +     - First part: {{:​mc1.pdf|mc1.pdf}} 
 +     - Second part: {{:​mc2.pdf|mc2.pdf}} 
 +     - Related software: http://​www-verimag.imag.fr/​~iosif/​jcat 
 + 
 +===== Ecole Doctorale Grenoble ===== 
 + 
 +[[http://​edmstii.ujf-grenoble.fr/​|Ecole Doctorale Mathématiques,​ Sciences et Technologies de l'​Information,​ Informatique]] 
 + 
 +**Slides for lectures on game theory** (23/11/2010 and 30/11/2010)
   - //​Tuesday//,​ 23/11/2010, [[http://​www-verimag.imag.fr/​~jobstman/​teaching/​LAT2011/​1_motivation.pdf|Motivation]],​ [[http://​www-verimag.imag.fr/​~jobstman/​teaching/​LAT2011/​2_terminology.pdf|Terminology]],​ [[http://​www-verimag.imag.fr/​~jobstman/​teaching/​LAT2011/​3_safety_buchi.pdf|Safety and Buchi Games]]   - //​Tuesday//,​ 23/11/2010, [[http://​www-verimag.imag.fr/​~jobstman/​teaching/​LAT2011/​1_motivation.pdf|Motivation]],​ [[http://​www-verimag.imag.fr/​~jobstman/​teaching/​LAT2011/​2_terminology.pdf|Terminology]],​ [[http://​www-verimag.imag.fr/​~jobstman/​teaching/​LAT2011/​3_safety_buchi.pdf|Safety and Buchi Games]]
   - //​Tuesday//,​ 30/11/2010, [[http://​www-verimag.imag.fr/​~jobstman/​teaching/​LAT2011/​4_parity.pdf|Parity Games]], [[http://​www-verimag.imag.fr/​~jobstman/​teaching/​LAT2011/​5_games_and_trees.pdf|Relationship between Games and Tree Automata]]   - //​Tuesday//,​ 30/11/2010, [[http://​www-verimag.imag.fr/​~jobstman/​teaching/​LAT2011/​4_parity.pdf|Parity Games]], [[http://​www-verimag.imag.fr/​~jobstman/​teaching/​LAT2011/​5_games_and_trees.pdf|Relationship between Games and Tree Automata]]
  
-===== SNBS (2010) ​=====+===== SNSB Bucharest ​===== 
 + 
 +[[http://​www.imar.ro/​~purice/​SNS/​homepage/​index_eng.php3|Scoala Normala Superioara Bucharest (SNSB)]] 
  
-**Outline of the first week** (19/04 - 24/04) : +**Outline of the first week** (19/04/2010 - 24/04/2010) : 
-  - //Monday.// Introduction,​ First and Second Order Logics {{w1_mon.pdf}} (4h, Radu Iosif) +  - //Monday.// Introduction,​ First and Second Order Logics {{:w1_mon.pdf|}} (4h, Radu Iosif) 
-  - //​Tuesday.//​ Automata on Finite Words. Definitions of Recognizability {{w1_tue.pdf}} (4h, Radu Iosif) +  - //​Tuesday.//​ Automata on Finite Words. Definitions of Recognizability {{:w1_tue.pdf|}} (4h, Radu Iosif) 
-  - //​Wednesday.//​ Regular, Star Free and Aperiodic Languages {{w1_wed.pdf}} (4h, Radu Iosif) +  - //​Wednesday.//​ Regular, Star Free and Aperiodic Languages {{:w1_wed.pdf|}} (4h, Radu Iosif) 
-  - //​Thursday.//​ Automata on Infinite Words {{w1_thu.pdf}} (4h, Radu Iosif) +  - //​Thursday.//​ Automata on Infinite Words {{:w1_thu.pdf|}} (4h, Radu Iosif) 
-  - //Friday.// The McNaughton, Buechi and Ramsey Theorems {{w1_fri.pdf}} (4h, Radu Iosif) +  - //Friday.// The McNaughton, Buechi and Ramsey Theorems {{:w1_fri.pdf|}} (4h, Radu Iosif) 
-  - //​Saturday.//​ Linear Temporal Logic {{w1_sat.pdf}} (4h, Radu Iosif)+  - //​Saturday.//​ Linear Temporal Logic {{:w1_sat.pdf|}} (4h, Radu Iosif)
  
-**Outline of the second week** (24/05 - 29/05) : +**Outline of the second week** (24/05/2010 - 29/05/2010) : 
-  - //Monday.// Automata on Finite Trees {{w2_mon.pdf}} (4h, Radu Iosif) +  - //Monday.// Automata on Finite Trees {{:w2_mon.pdf|}} (4h, Radu Iosif) 
-  - //​Tuesday.//​ Automata on Infinite Trees {{w2_tue.pdf}} (4h, Radu Iosif) +  - //​Tuesday.//​ Automata on Infinite Trees {{:w2_tue.pdf|}} (4h, Radu Iosif) 
-  - //​Wednesday.//​ Motivation {{:​snsb_course:​w2_wed_1.pdf|}},​ Terminology {{:​snsb_course:​w2_wed_2.pdf|}},​ Reachability and Buchi games {{:​snsb_course:​w2_wed_3.pdf|}} (4h, Barbara Jobstmann) +  - //​Wednesday.//​ Motivation {{:​w2_wed_1.pdf|}},​ Terminology {{:​w2_wed_2.pdf|}},​ Reachability and Buchi games {{:​w2_wed_3.pdf|}} (4h, Barbara Jobstmann) 
-  - //​Thursday.//​ Obligation and weak-parity games {{:​snsb_course:​w2_thu_1.pdf|}},​ Parity games {{:​snsb_course:​w2_thu_2.pdf|}} (4h, Barbara Jobstmann) +  - //​Thursday.//​ Obligation and weak-parity games {{:​w2_thu_1.pdf|}},​ Parity games {{:​w2_thu_2.pdf|}} (4h, Barbara Jobstmann) 
-  - //Friday.// Games and tree automata {{:​snsb_course:​w2_fri_1.pdf|}},​ Quantitative Verification and Synthesis {{:​snsb_course:​quantitative-synthesis-p4.pdf|}},​ Mean-payoff games {{:​snsb_course:​w2_fri_3.pdf|}} (4h, Barbara Jobstmann)+  - //Friday.// Games and tree automata {{:​w2_fri_1.pdf|}},​ Quantitative Verification and Synthesis {{:​quantitative-synthesis-p4.pdf|}},​ Mean-payoff games {{:​w2_fri_3.pdf|}} (4h, Barbara Jobstmann)
   - //​Saturday.//​ Integer Arithmetic, Presburger Arithmetic and Semilinear Sets {{presburger-slide.pdf}}. Definability and Recognizability {{recognizable-slide.pdf}} (4h, Radu Iosif)   - //​Saturday.//​ Integer Arithmetic, Presburger Arithmetic and Semilinear Sets {{presburger-slide.pdf}}. Definability and Recognizability {{recognizable-slide.pdf}} (4h, Radu Iosif)
  
-===== EPFL (2009) ​=====+===== EPFL =====
  
 A course in the [[http://​phd.epfl.ch/​edic|EPFL Doctoral Program in Computer and Communication Sciences]] A course in the [[http://​phd.epfl.ch/​edic|EPFL Doctoral Program in Computer and Communication Sciences]]
   * [[http://​infowww.epfl.ch/​imoniteur_ISAP/​!itffichecours.htm?​ww_i_matiere=280335500&​ww_x_anneeAcad=2009-2010&​ww_i_section=2139068&​ww_c_langue=en|Official Course Book Page]]   * [[http://​infowww.epfl.ch/​imoniteur_ISAP/​!itffichecours.htm?​ww_i_matiere=280335500&​ww_x_anneeAcad=2009-2010&​ww_i_section=2139068&​ww_c_langue=en|Official Course Book Page]]
   * the course carries 4 credits   * the course carries 4 credits
 +
 +**Organized by:** [[http://​lara.epfl.ch/​~kuncak|Viktor Kuncak]]
  
 **Schedule**:​ (lectures and exercises): Fridays 13:15-16:00 **Schedule**:​ (lectures and exercises): Fridays 13:15-16:00
Line 75: Line 91:
  
 **Location**:​ [[http://​map.epfl.ch/?​room=BC355|BC 355]] **Location**:​ [[http://​map.epfl.ch/?​room=BC355|BC 355]]
- 
-**Instructors:​** 
-  * [[http://​www-verimag.imag.fr/​~iosif/​|Radu Iosif]] 
-  * [[http://​mtc.epfl.ch/​~jobstman/​|Barbara Jobstmann]] 
- 
-**Organized by:** [[http://​lara.epfl.ch/​~kuncak|Viktor Kuncak]] 
  
 **Preliminary Outline:** **Preliminary Outline:**
Line 103: Line 113:
 Please find the homework [[LAT:​homework|here.]] ​ Please find the homework [[LAT:​homework|here.]] ​
  
- 
-More details will follow. The course will be similar to [[http://​www-verimag.imag.fr/​~iosif/​LogicAutomata07/​|the following course]].