Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
lat [2011/03/01 20:31] jobstman |
lat [2012/01/09 14:16] 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/ | ||
- | ===== SNBS Edition ===== | + | ===== ENS Lyon Course on Automata-Theoretic Model Checking ===== |
- | **Outline of the first week** (19/04 - 24/04) : | + | **Slides** |
- | - //Monday.// Introduction, First and Second Order Logics {{w1_mon.pdf}} (4h, Radu Iosif) | + | - First part: {{:mc1.pdf|mc1.pdf}} |
- | - //Tuesday.// Automata on Finite Words. Definitions of Recognizability {{w1_tue.pdf}} (4h, Radu Iosif) | + | - Second part: {{:mc2.pdf|mc2.pdf}} |
- | - //Wednesday.// Regular, Star Free and Aperiodic Languages {{w1_wed.pdf}} (4h, Radu Iosif) | + | - Related software: http://www-verimag.imag.fr/~iosif/jcat |
- | - //Thursday.// Automata on Infinite Words {{w1_thu.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) | + | |
- | **Outline of the second week** (24/05 - 29/05) : | + | ===== Ecole Doctorale Grenoble ===== |
- | - //Monday.// Automata on Finite Trees {{w2_mon.pdf}} (4h, Radu Iosif) | + | |
- | - //Tuesday.// Automata on Infinite Trees {{w2_tue.pdf}} (4h, Radu Iosif) | + | [[http://edmstii.ujf-grenoble.fr/|Ecole Doctorale Mathématiques, Sciences et Technologies de l'Information, Informatique]] |
- | - //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) | + | |
- | - //Thursday.// Obligation and weak-parity games {{:snsb_course:w2_thu_1.pdf|}}, Parity games {{:snsb_course:w2_thu_2.pdf|}} (4h, Barbara Jobstmann) | + | **Slides for lectures on game theory** (23/11/2010 and 30/11/2010) |
- | - //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) | + | - //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]] | ||
+ | |||
+ | ===== SNSB Bucharest ===== | ||
+ | |||
+ | [[http://www.imar.ro/~purice/SNS/homepage/index_eng.php3|Scoala Normala Superioara Bucharest (SNSB)]] | ||
+ | |||
+ | |||
+ | **Outline of the first week** (19/04/2010 - 24/04/2010) : | ||
+ | - //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) | ||
+ | - //Wednesday.// Regular, Star Free and Aperiodic Languages {{:w1_wed.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) | ||
+ | - //Saturday.// Linear Temporal Logic {{:w1_sat.pdf|}} (4h, Radu Iosif) | ||
+ | |||
+ | **Outline of the second week** (24/05/2010 - 29/05/2010) : | ||
+ | - //Monday.// Automata on Finite Trees {{:w2_mon.pdf|}} (4h, Radu Iosif) | ||
+ | - //Tuesday.// Automata on Infinite Trees {{:w2_tue.pdf|}} (4h, Radu Iosif) | ||
+ | - //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 {{:w2_thu_1.pdf|}}, Parity games {{:w2_thu_2.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 Edition ===== | + | ===== 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 69: | Line 89: | ||
**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 97: | Line 111: | ||
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]]. |