EECI 2012: Automata Theory - Revision history

Murray at 10:13, 14 May 2012

2012-05-14T10:13:30Z

← Older revision		Revision as of 10:13, 14 May 2012
Line 6:		Line 6:
	* Lecture slides: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/L2_automata_theory-14May12.pdf Automata Theory] (presentation and notation follow that in "Principles of Model Checking" chapters 2.1, 2.2, 3.2-3.4 by Baier and Katoen.)		* Lecture slides: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/L2_automata_theory-14May12.pdf Automata Theory] (presentation and notation follow that in "Principles of Model Checking" chapters 2.1, 2.2, 3.2-3.4 by Baier and Katoen.)

	== Further Reading ~~and Additional Information~~==		== Further Reading ==
	* <p>[http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=11481 Principles of Model Checking], C. Baier and J.-P. Katoen, The MIT Press, 2008. A detailed reference on model checking. Early chapters provide an exposition to automata theory. Slides for this lecture follow this reference. </p>		* <p>[http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=11481 Principles of Model Checking], C. Baier and J.-P. Katoen, The MIT Press, 2008. A detailed reference on model checking. Early chapters provide an exposition to automata theory. Slides for this lecture follow this reference. </p>
	* <p>[http://www.amazon.com/Introduction-Theory-Computation-Michael-Sipser/dp/053494728X Introduction to the Theory of Computation], M. Sipser, PWS Publishing Company, 1997. This is a textbook on theory of computation covering preliminaries in automata theory. </p>		* <p>[http://www.amazon.com/Introduction-Theory-Computation-Michael-Sipser/dp/053494728X Introduction to the Theory of Computation], M. Sipser, PWS Publishing Company, 1997. This is a textbook on theory of computation covering preliminaries in automata theory. </p>
	* <p> [http://www.cds.caltech.edu/~utopcu/VerInCtrl/VerInCtrl.html CDS 270: Verification in Controls]: The second half of the course taught in Fall 2009 at Caltech also covered the material in this lecture. There are brief lecture notes and exercises.		* <p> [http://www.cds.caltech.edu/~utopcu/VerInCtrl/VerInCtrl.html CDS 270: Verification in Controls]: The second half of the course taught in Fall 2009 at Caltech also covered the material in this lecture. There are brief lecture notes and exercises.

Murray: /* Lecture Materials */

2012-05-14T10:12:56Z

Lecture Materials

← Older revision		Revision as of 10:12, 14 May 2012
Line 4:		Line 4:

	== Lecture Materials ==		== Lecture Materials ==
	* Lecture slides: [http:www.cds.caltech.edu/~murray/courses/eeci-sp12/L2_automata_theory-14May12.pdf Automata Theory] (presentation and notation follow that in "Principles of Model Checking" chapters 2.1, 2.2, 3.2-3.4 by Baier and Katoen.)		* Lecture slides: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/L2_automata_theory-14May12.pdf Automata Theory] (presentation and notation follow that in "Principles of Model Checking" chapters 2.1, 2.2, 3.2-3.4 by Baier and Katoen.)

	== Further Reading and Additional Information==		== Further Reading and Additional Information==

Murray at 10:12, 14 May 2012

2012-05-14T10:12:37Z

← Older revision		Revision as of 10:12, 14 May 2012
Line 2:		Line 2:

	This lecture gives an introduction to some concepts and tools in computer science that are used in the remainder of the course. We start with finite transition systems as a mathematical model to describe behavior of systems with finite, discrete states. We use linear-time properties serve as the specification language (e.g., to specify safety or liveness properties) and we discuss the preliminaries that lead to model checking, a commonly used, powerful verification tool.		This lecture gives an introduction to some concepts and tools in computer science that are used in the remainder of the course. We start with finite transition systems as a mathematical model to describe behavior of systems with finite, discrete states. We use linear-time properties serve as the specification language (e.g., to specify safety or liveness properties) and we discuss the preliminaries that lead to model checking, a commonly used, powerful verification tool.

	~~{{righttoc}}~~


	== Lecture Materials ==		== Lecture Materials ==
	* Lecture slides: [http:~~//dl~~.~~dropbox~~.~~com~~/u/~~29005314~~/~~L2_automata~~-~~theory~~-14May12.pdf Automata Theory] (presentation and notation follow that in "Principles of Model Checking" chapters 2.1, 2.2, 3.2-3.4 by Baier and Katoen.)		* Lecture slides: [http:www.cds.caltech.edu/~murray/courses/eeci-sp12/L2_automata_theory-14May12.pdf Automata Theory] (presentation and notation follow that in "Principles of Model Checking" chapters 2.1, 2.2, 3.2-3.4 by Baier and Katoen.)

	== Further Reading and Additional Information==		== Further Reading and Additional Information==

Murray at 19:17, 13 May 2012

2012-05-13T19:17:38Z

← Older revision		Revision as of 19:17, 13 May 2012
Line 1:		Line 1:
	{{~~AFRL12~~ header\|prev=Introduction \|next=Temporal Logic}}		{{eeci-sp12 header\|prev=Introduction \|next=Temporal Logic}}

	This lecture gives an introduction to some concepts and tools in computer science that are used in the remainder of the course. We start with finite transition systems as a mathematical model to describe behavior of systems with finite, discrete states. We use linear-time properties serve as the specification language (e.g., to specify safety or liveness properties) and we discuss the preliminaries that lead to model checking, a commonly used, powerful verification tool.		This lecture gives an introduction to some concepts and tools in computer science that are used in the remainder of the course. We start with finite transition systems as a mathematical model to describe behavior of systems with finite, discrete states. We use linear-time properties serve as the specification language (e.g., to specify safety or liveness properties) and we discuss the preliminaries that lead to model checking, a commonly used, powerful verification tool.

Tw68 at 03:55, 10 May 2012

2012-05-10T03:55:23Z

← Older revision		Revision as of 03:55, 10 May 2012
Line 7:		Line 7:

	== Lecture Materials ==		== Lecture Materials ==
	* Lecture slides: [http://~~www~~.~~cds~~.~~caltech.edu~~/~~~utopcu~~/~~AFRL2012~~/~~L2_Automata_Theory~~.pdf Automata Theory] (presentation and notation follow that in "Principles of Model Checking" chapters 2.1, 2.2, 3.2-3.4 by Baier and Katoen.)		* Lecture slides: [http://dl.dropbox.com/u/29005314/L2_automata-theory-14May12.pdf Automata Theory] (presentation and notation follow that in "Principles of Model Checking" chapters 2.1, 2.2, 3.2-3.4 by Baier and Katoen.)

	== Further Reading and Additional Information==		== Further Reading and Additional Information==

Tw68 at 07:57, 9 May 2012

2012-05-09T07:57:53Z

← Older revision		Revision as of 07:57, 9 May 2012
Line 7:		Line 7:

	== Lecture Materials ==		== Lecture Materials ==
	* Lecture slides: [http://www.cds.caltech.edu/~utopcu/AFRL2012/L2_Automata_Theory.pdf Automata Theory] (presentation and notation follow that in "Principles of Model Checking" chapters 2.1, 2.21, 3.2-3.~~5, and~~ 4~~.1-4.3~~ by Baier and Katoen.)		* Lecture slides: [http://www.cds.caltech.edu/~utopcu/AFRL2012/L2_Automata_Theory.pdf Automata Theory] (presentation and notation follow that in "Principles of Model Checking" chapters 2.1, 2.2, 3.2-3.4 by Baier and Katoen.)

	== Further Reading and Additional Information==		== Further Reading and Additional Information==

Utopcu at 03:08, 22 April 2012

2012-04-22T03:08:54Z

← Older revision		Revision as of 03:08, 22 April 2012
Line 7:		Line 7:

	== Lecture Materials ==		== Lecture Materials ==
	* Lecture slides: [http://www.cds.caltech.edu/~utopcu/~~eeci2011~~/L2_Automata_Theory.pdf Automata Theory] (presentation and notation follow that in "Principles of Model Checking" chapters 2.1, 2.21, 3.2-3.5, and 4.1-4.3 by Baier and Katoen.)		* Lecture slides: [http://www.cds.caltech.edu/~utopcu/AFRL2012/L2_Automata_Theory.pdf Automata Theory] (presentation and notation follow that in "Principles of Model Checking" chapters 2.1, 2.21, 3.2-3.5, and 4.1-4.3 by Baier and Katoen.)

	== Further Reading and Additional Information==		== Further Reading and Additional Information==

Utopcu at 03:06, 22 April 2012

2012-04-22T03:06:04Z

← Older revision		Revision as of 03:06, 22 April 2012
Line 1:		Line 1:
	{{~~eeci-sp11~~ header\|prev=Introduction \|next=Temporal Logic}}		{{AFRL12 header\|prev=Introduction \|next=Temporal Logic}}

	This lecture gives an introduction to some concepts and tools in computer science that are used in the remainder of the course. We start with finite transition systems as a mathematical model to describe behavior of systems with finite, discrete states. We use linear-time properties serve as the specification language (e.g., to specify safety or liveness properties) and we discuss the preliminaries that lead to model checking, a commonly used, powerful verification tool.		This lecture gives an introduction to some concepts and tools in computer science that are used in the remainder of the course. We start with finite transition systems as a mathematical model to describe behavior of systems with finite, discrete states. We use linear-time properties serve as the specification language (e.g., to specify safety or liveness properties) and we discuss the preliminaries that lead to model checking, a commonly used, powerful verification tool.

Utopcu: Created page with '{{eeci-sp11 header|prev=Introduction |next=Temporal Logic}} This lecture gives an introduction to some concepts and tools in computer science that are used in the remainder of t…'

2012-04-22T03:04:55Z

Created page with '{{eeci-sp11 header|prev=Introduction |next=Temporal Logic}} This lecture gives an introduction to some concepts and tools in computer science that are used in the remainder of t…'

New page

{{eeci-sp11 header|prev=Introduction |next=Temporal Logic}}

This lecture gives an introduction to some concepts and tools in computer science that are used in the remainder of the course. We start with finite transition systems as a mathematical model to describe behavior of systems with finite, discrete states. We use linear-time properties serve as the specification language (e.g., to specify safety or liveness properties) and we discuss the preliminaries that lead to model checking, a commonly used, powerful verification tool.

{{righttoc}}

== Lecture Materials ==
* Lecture slides: [http://www.cds.caltech.edu/~utopcu/eeci2011/L2_Automata_Theory.pdf Automata Theory] (presentation and notation follow that in "Principles of Model Checking" chapters 2.1, 2.21, 3.2-3.5, and 4.1-4.3 by Baier and Katoen.)

== Further Reading and Additional Information==
* [http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=11481 Principles of Model Checking], C. Baier and J.-P. Katoen, The MIT Press, 2008. A detailed reference on model checking. Early chapters provide an exposition to automata theory. Slides for this lecture follow this reference. 
* [http://www.amazon.com/Introduction-Theory-Computation-Michael-Sipser/dp/053494728X Introduction to the Theory of Computation], M. Sipser, PWS Publishing Company, 1997. This is a textbook on theory of computation covering preliminaries in automata theory. 
* [http://www.cds.caltech.edu/~utopcu/VerInCtrl/VerInCtrl.html CDS 270: Verification in Controls]: The second half of the course taught in Fall 2009 at Caltech also covered the material in this lecture. There are brief lecture notes and exercises.