Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
lat [2011/03/01 20:41] jobstman |
lat [2012/01/09 15:24] (current) radu.iosif |
||
---|---|---|---|
Line 24: | Line 24: | ||
- 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 38: | Line 38: | ||
- The Gastex Package for Latex : http://www.lsv.ens-cachan.fr/~gastin/gastex/gastex.html | - The Gastex Package for Latex : http://www.lsv.ens-cachan.fr/~gastin/gastex/gastex.html | ||
- 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/ | ||
+ | |||
+ | ===== ENS Lyon Course on Automata-Theoretic Model Checking ===== | ||
+ | |||
+ | [[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 ===== | ===== 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) | **Slides for lectures on game theory** (23/11/2010 and 30/11/2010) | ||
Line 45: | Line 56: | ||
- //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 ===== | + | ===== 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) : | **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/2010 - 29/05/2010) : | **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) | ||