Lat - Revision history

Radu iosif at 16:40, 25 February 2022

2022-02-25T16:40:01Z

Radu iosif at 16:57, 16 January 2021

2021-01-16T16:57:14Z

Radu iosif: /* Logic and Automata Theory */

2021-01-16T16:56:52Z

‎Logic and Automata Theory

Radu iosif: /* Logic and Automata Theory */

2021-01-16T16:56:13Z

‎Logic and Automata Theory

Radu iosif at 16:54, 16 January 2021

2021-01-16T16:54:46Z

Radu iosif at 14:48, 23 September 2014

2014-09-23T14:48:57Z

Radu iosif at 20:41, 28 April 2013

2013-04-28T20:41:00Z

Radu iosif at 10:37, 13 February 2013

2013-02-13T10:37:53Z

Radu iosif at 10:37, 13 February 2013

2013-02-13T10:37:34Z

Radu iosif at 10:36, 13 February 2013

2013-02-13T10:36:45Z

← Older revision		Revision as of 16:40, 25 February 2022
Line 83:		Line 83:
	* Dec 3: [http://nts.imag.fr/images/c/c3/GameTheoryMotivation.pdf Game Theory Motivation], [http://nts.imag.fr/images/5/55/GameTheoryTerminology.pdf Terminology], [http://nts.imag.fr/images/3/3b/ReachabilityBuchiGames.pdf Reachability and Buchi games]		* Dec 3: [http://nts.imag.fr/images/c/c3/GameTheoryMotivation.pdf Game Theory Motivation], [http://nts.imag.fr/images/5/55/GameTheoryTerminology.pdf Terminology], [http://nts.imag.fr/images/3/3b/ReachabilityBuchiGames.pdf Reachability and Buchi games]
	* Dec 10: [http://nts.imag.fr/images/3/36/StaigerWagnerWeakParityGames.pdf Staiger-Wagner and Weak Parity Games] [http://nts.imag.fr/images/1/1d/ParityGames.pdf Parity games] [http://nts.imag.fr/images/8/89/GamesTreeAutomata.pdf Games and Tree Automata]		* Dec 10: [http://nts.imag.fr/images/3/36/StaigerWagnerWeakParityGames.pdf Staiger-Wagner and Weak Parity Games] [http://nts.imag.fr/images/1/1d/ParityGames.pdf Parity games] [http://nts.imag.fr/images/8/89/GamesTreeAutomata.pdf Games and Tree Automata]
		+
		+	===== ED MSTII Grenoble 2021 =====
		+
		+	http://nts.imag.fr/index.php/Lat21

@@ Line 26: / Line 26: @@
 * M. Vardi and P. Wolper. [https://www.sciencedirect.com/science/article/pii/S0890540184710923 Reasoning about Infinite Computations]
 * M. Vardi. [http://www.cs.rice.edu/~vardi/papers/icla09.pdf/  From Philosophical to Industrial Logics] [http://www-verimag.imag.fr/~iosif/LAT/slides.pdf slides]
 '''Software'''

@@ Line 24: / Line 24: @@
 * [http://wcms.inf.ed.ac.uk/lfcs/Automata_On_Infinite_Trees_Slide.pdf Automata on Infinite Trees] lecture by Wolfgang Thomas
 * [http://nts.imag.fr/images/2/24/Mcnaughton.pdf Textbook proof of McNaughton's Theorem]
 * M. Vardi and P. Wolper. [https://www.sciencedirect.com/science/article/pii/S0890540184710923 Reasoning about Infinite Computations]
 * M. Vardi. [http://www.cs.rice.edu/~vardi/papers/icla09.pdf/  From Philosophical to Industrial Logics] [http://www-verimag.imag.fr/~iosif/LAT/slides.pdf slides]
@@ Line 36: / Line 34: @@
 * GAVS+: An Open Platform for the Research of Algorithmic Game Solving: http://www6.in.tum.de/~chengch/gavs/
 * [http://www-verimag.imag.fr/~iosif/jcat Java Concurrency Analysis Tool]
 ===== ENS Lyon Course on Automata-Theoretic Model Checking =====

@@ Line 20: / Line 20: @@
 * U. Zwick and M. Paterson. [http://www-verimag.imag.fr/~iosif/LAT/mean-payoff.pdf The Complexity of Mean Payoff Games]
 * Note about Karp's minimal mean-cycle algorithm. [http://webcourse.cs.technion.ac.il/236359/Spring2010/ho/WCFiles/MMC.ps ps]
 '''Software'''
@@ Line 26: / Line 35: @@
 * LTL2BA: http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/
 * 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 =====

@@ Line 1: / Line 1: @@
 === Logic and Automata Theory ===
 '''Similar or related lectures''':
@@ Line 73: / Line 63: @@
 * //Friday.// [http://www-verimag.imag.fr/~iosif/LAT/w2_fri_1.pdf Games and tree automata], [http://www-verimag.imag.fr/~iosif/LAT/quantitative-synthesis-p4.pdf Quantitative Verification and Synthesis], [http://www-verimag.imag.fr/~iosif/LAT/w2_fri_3.pdf Mean-payoff games] (4h, Barbara Jobstmann)
 * //Saturday.// [http://www-verimag.imag.fr/~iosif/LAT/presburger-slide.pdf Integer Arithmetic, Presburger Arithmetic and Semilinear Sets]. [http://www-verimag.imag.fr/~iosif/LAT/recognizable-slide.pdf Definability and Recognizability] (4h, Radu Iosif)

@@ Line 34: / Line 34: @@
 * The Mona Project : http://www.brics.dk/mona/
 * The Goal Project : http://goal.im.ntu.edu.tw/wiki/doku.php
-* The Gastex Package for Latex : http://www.lsv.ens-cachan.fr/~gastin/gastex/gastex.html
+* LTL2BA: http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/
 * GAVS+: An Open Platform for the Research of Algorithmic Game Solving: http://www6.in.tum.de/~chengch/gavs/

@@ Line 1: / Line 1: @@
 === Logic and Automata Theory ===
-'''Lecturers''': [http://www-verimag.imag.fr/~iosif/ Radu Iosif] and [http://www-verimag.imag.fr/~jobstman/ Barbara Jobstmann]
+'''Lecturers''': [[Radu_Iosif]] and [http://www-verimag.imag.fr/~jobstman/ Barbara Jobstmann]
 '''Objectives''': Many major hardware (Intel, IBM) and software (Microsoft) companies are now using the technique of Model Checking in practice. Examples of its use include the verification of VLSI circuits, communication protocols, software device drivers, real-time embedded systems, and security algorithms. The works of A. Pnueli, E. Clarke, E.A Emerson and J. Sifakis on algorithmic verification of systems using the Model Checking has been awarded the 1996 and 2007 Turing awards. The basis of this work is the relation of logic with automata theory, which was introduced by the seminal works of Buechi (1960) and Rabin (1969). This course is intended to introduce the student to these techniques, focusing on decision methods for classical non-interpreted logics and integer arithmetic theories.

@@ Line 60: / Line 60: @@
 '''Outline of the first week''' (19/04/2010 - 24/04/2010) :
 * //Monday.// [http://www-verimag.imag.fr/~iosif/LAT/w1_mon.pdf Introduction, First and Second Order Logics] (4h, Radu Iosif)
-* //Tuesday.// [http://www-verimag.imag.fr/~iosif/LAT/w1_tue.pd Automata on Finite Words. Definitions of Recognizability] (4h, Radu Iosif)
+* //Tuesday.// [http://www-verimag.imag.fr/~iosif/LAT/w1_tue.pdf Automata on Finite Words. Definitions of Recognizability] (4h, Radu Iosif)
 * //Wednesday.// [http://www-verimag.imag.fr/~iosif/LAT/w1_wed.pdf Regular, Star Free and Aperiodic Languages] (4h, Radu Iosif)
 * //Thursday.// [http://www-verimag.imag.fr/~iosif/LAT/w1_thu.pdf Automata on Infinite Words] (4h, Radu Iosif)

@@ Line 41: / Line 41: @@
 [http://www.ens-lyon.fr/DI/?p=2320 ER01 : vérification et certification du logiciel]
-* First part: {{:mc1.pdf|mc1.pdf}}
+* First part: [http://www-verimag.imag.fr/~iosif/LAT/mc1.pdf mc1.pdf]
-* Second part: {{:mc2.pdf|mc2.pdf}}
+* Second part: [http://www-verimag.imag.fr/~iosif/LAT/mc2.pdf mc2.pdf]
 * Related software: http://www-verimag.imag.fr/~iosif/jcat
@@ Line 59: / Line 59: @@
 '''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.// [http://www-verimag.imag.fr/~iosif/LAT/w1_mon.pdf Introduction, First and Second Order Logics] (4h, Radu Iosif)
-* //Tuesday.// Automata on Finite Words. Definitions of Recognizability {{:w1_tue.pdf}} (4h, Radu Iosif)
+* //Tuesday.// [http://www-verimag.imag.fr/~iosif/LAT/w1_tue.pd fAutomata on Finite Words. Definitions of Recognizability] (4h, Radu Iosif)
-* //Wednesday.// Regular, Star Free and Aperiodic Languages {{:w1_wed.pdf}} (4h, Radu Iosif)
+* //Wednesday.// [http://www-verimag.imag.fr/~iosif/LAT/w1_wed.pdf Regular, Star Free and Aperiodic Languages] (4h, Radu Iosif)
-* //Thursday.// Automata on Infinite Words {{:w1_thu.pdf}} (4h, Radu Iosif)
+* //Thursday.// [http://www-verimag.imag.fr/~iosif/LAT/w1_thu.pdf Automata on Infinite Words] (4h, Radu Iosif)
-* //Friday.// The McNaughton, Buechi and Ramsey Theorems {{:w1_fri.pdf}} (4h, Radu Iosif)
+* //Friday.// [http://www-verimag.imag.fr/~iosif/LAT/w1_fri.pdf The McNaughton, Buechi and Ramsey Theorems] (4h, Radu Iosif)
-* //Saturday.// Linear Temporal Logic {{:w1_sat.pdf}} (4h, Radu Iosif)
+* //Saturday.// [http://www-verimag.imag.fr/~iosif/LAT/w1_sat.pdf Linear Temporal Logic] (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)
+* //Monday.// [http://www-verimag.imag.fr/~iosif/LAT/w2_mon.pdf Automata on Finite Trees] (4h, Radu Iosif)
-* //Tuesday.// Automata on Infinite Trees {{:w2_tue.pdf}} (4h, Radu Iosif)
+* //Tuesday.// [http://www-verimag.imag.fr/~iosif/LAT/w2_tue.pdf Automata on Infinite Trees] (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)
+* //Wednesday.// [http://www-verimag.imag.fr/~iosif/LAT/w2_wed_1.pdf Motivation], [http://www-verimag.imag.fr/~iosif/LAT/w2_wed_2.pdf Terminology], [http://www-verimag.imag.fr/~iosif/LAT/w2_wed_3.pdf Reachability and Buchi games] (4h, Barbara Jobstmann)
-* //Thursday.// Obligation and weak-parity games {{:w2_thu_1.pdf|}}, Parity games {{:w2_thu_2.pdf|}} (4h, Barbara Jobstmann)
+* //Thursday.// [http://www-verimag.imag.fr/~iosif/LAT/w2_thu_1.pdf Obligation and weak-parity games], [http://www-verimag.imag.fr/~iosif/LAT/w2_thu_2.pdf Parity games] (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)
+* //Friday.// [http://www-verimag.imag.fr/~iosif/LAT/w2_fri_1.pdf Games and tree automata], [http://www-verimag.imag.fr/~iosif/LAT/quantitative-synthesis-p4.pdf Quantitative Verification and Synthesis], [http://www-verimag.imag.fr/~iosif/LAT/w2_fri_3.pdf Mean-payoff games] (4h, Barbara Jobstmann)
-* //Saturday.// Integer Arithmetic, Presburger Arithmetic and Semilinear Sets {{presburger-slide.pdf}}. Definability and Recognizability {{recognizable-slide.pdf}} (4h, Radu Iosif)
+* //Saturday.// [http://www-verimag.imag.fr/~iosif/LAT/presburger-slide.pdf Integer Arithmetic, Presburger Arithmetic and Semilinear Sets]. [http://www-verimag.imag.fr/~iosif/LAT/recognizable-slide.pdf Definability and Recognizability] (4h, Radu Iosif)