http:^^www.cs.umass.edu^~immerman^cs691^cs691.html

This data set contains WWW-pages collected from computer science departments of various universities

Date: Wednesday, 20-Nov-96 23:19:42 GMT
Server: NCSA/1.3
MIME-version: 1.0
Content-type: text/html
Last-modified: Wednesday, 13-Nov-96 20:05:42 GMT
Content-length: 6267

<title>Logic and Formal Methods</title>
<h2>Comp. Sci. 691M:<b>  Logic and Formal Methods</b>,   Fall, 1996</h2>

<b>Meeting Times:</b> MW 9:05-10:20,  LGRC: A339<p>

<b>Instructor:</b> <!WA0><a href="http://www.cs.umass.edu/~immerman">Neil Immerman</a><p>

<b> Aim of the Course:</b> We will provide introductions to propositional,
predicate, and modal logics.  These will be studied and used throughout the
course as tools for the specification and verification of properties of
programs and protocols.  <p>

<h4><b>Topics:</b>  </h4>
<ol>
<li><b>First-Order Logic:</b> propositional logic, predicate logic,
completeness and compactness theorems, semantics via quantifier games,
G&#246;del's incompleteness theorem.

<li><b>Modal logic:</b> temporal logic and logics of knowledge, axiomitization,
semantics via Kripke structures.

<li><b>Applications:</b> (These may change slightly according to the background and
interests of the students.)
<ul>

<li> Evolving Algebras: due to Gurevich et. al., this offers an operatonal
semantics for programming languages and protocols via finite logical
structures.

<li>Temporal Logic of Actions: Lamport's system of specification and
verification via temporal logic

<li> Distributed Protocols: we will use logics of knowledge to express
correctness and security of distributed protocols.

<li> Model Checking: using temporal logic to verify properties of systems

<li> Symbolic Model Checking: using ordered binary decision diagrams (OBDDs)
to symbolically represent and model-check huge Kripke structures.
</ul>
</ol>

<b> Requirements:</b> Students will be expected to participate in class.
There will be three problem sets concerning the introductory material on
first-order and modal logic.  Each student will choose a more advanced
topic to study in detail.  He or she will write a short paper and give a
lecture on this topic.<p>

<b>Texts:</b> For first-order logic, we will follow <i>Logic and
Structure,</i> Third Edition, by Dirk van Dalen, Springer-Verlag.  This is
available at the <b>Jeffery Amherst College Store</b> in downtown Amherst.
For the rest of the course, we will follow selected research papers.<p>

<b>Prerequisites:</b> Sufficient mathematical sophistication.  If you are
unsure whether you have it, try looking at van Dalen and/or come
talk with me.<p>

<h3>Notes and Handouts:</h3> <ul> 

<li> <!WA1><a href="http://www.cs.umass.edu/~immerman/cs691/notes_9_4.ps">Notes:
Sept. 4, 1996</a>

<li> <!WA2><a href="http://www.cs.umass.edu/~immerman/cs691/notes_9_9.ps">Notes:
Sept. 9, 1996</a>

<li> <!WA3><a href="http://www.cs.umass.edu/~immerman/cs691/notes_9_11.ps">Notes:
Sept. 11, 1996, plus first problem set, Due: 9/25/96</a>

<li> We have finished Propositional Logic and begun Predicate Logic.  See:
<!WA4><a href="http://www.cs.umass.edu/~immerman/cs691/notes_9_16.ps">Notes:
Sept. 16, 1996</a>

<li> On Wednesday, Oct. 2, I proved the Completeness Theorem and the
Compactness Theorem for predicate logic.  You should have read van Dalen
through page 118.  Note that in this course we are only interested in the
countable case, so you do not need to worry about larger cardinalities nor
do you have to remember Zorn's lemma.

<li> On Monday, Oct. 7, I introduced Ehrenfeucht-Fraisse games.  These are
the best and most pleasant way to figure out what can and cannot be
expressed in first-order logics.  By then you should have read the handout
<!WA5><a href="http://www.cs.umass.edu/~immerman/cs691/pebble_game.ps">pebble games</a>
from my forthcoming book, <i> Descriptive Complexity</i>.  

<li> On Wednesday, Oct. 9, I finished the introduction to Predicate Logic.  By now,
please skim the rest of Chapter 3 of van Dalen.  Topics that you should pay
particular attention to are: substructures, isomorphism, elementary
equivalence, and skolemization.

<li> <!WA6><a href="http://www.cs.umass.edu/~immerman/cs691/second_problem_set.ps">Second
Problem Set, Due: Oct. 16, 1996</a>

<li>   On Oct. 16 I introduced Evolving
Algebra.  Please read the
<!WA7><a href="http://www.eecs.umich.edu/ealgebras/tutorial/tutorial.html">Evolving
Algebra Tutorial</a>, and the paper guide.ps.  These are available as 
postscript files from anonymous FTP site, ftp.eecs.umich.edu, directory
/groups/Ealgebras, files tutorial.ps and guide.ps.

<li> On Oct. 21, I concluded my presentation of Evolving Algebras, using
the paper, "Why Use Evolving Algebras for Hardware and Software
Engineering," by Egon B&#246;rger, Proc. SOFSEM'95, Springer LNCS.  Also
available on the <!WA8><a href="http://www.eecs.umich.edu/ealgebras">Evolving
Algebra Homepage</a>.  I also talked briefly about Denotational Semantics,
using <i>Denotational Semantics</i> by Joseph Stoy, 1977, M.I.T. Press,
Chapter 9, by way of comparison.

<li> On Oct. 23, 28, and 30, I will give a three-lecture introduction to modal logics,
emphasizing temporal logic and logics of knowledge.  Please read the article by
Vardi, ``Why is Modal Logic So Robustly Decidable?'' which I handed out. I
will also use some material from the book by Fagin, Halpern, Moses, and Vardi,
<i>Reasoning about Knowledge,</i> 1995, M.I.T. press.

<li> On Monday, Nov. 4, I will talk about about an interesting paper that uses
logic of knowledge to discuss security in distributed systems: 
<!WA9><a
href="http://www.research.digital.com/SRC/personal/Martin_Abadi/Papers/src39-revised.ps">A
Logic of Authentication</a> by Burrows, Abadi, and Needham.  Please read
this paper before the class.

<li> On Wednesday, Nov. 6 through Monday, Nov. 18, I will talk about Lamport's <!WA10><a
href="http://www.research.digital.com/SRC/personal/Leslie_Lamport/tla/tla.html">
Temporal Logic of Actions</a>.

<li> You might want to look at the following webpage which has many
pointers to work going on in formal methods: <!WA11><a
href="http://lal.cs.byu.edu/other_FM.html"> Formal Methods Pointers</a>

<li> On Wednesday, Nov. 20, I will start talking about Computation Tree
Logic and Model Checking.  For a preview, take at look at the following homepage:
<!WA12><a
href="http://www.cs.cmu.edu/afs/cs/project/modck/pub/www/modck.html">Model
Checking at CMU</a>.

<li> Available slots for student lectures are: Nov. 27, Dec. 2, Dec. 4, and
Dec. 11.  I suggest that you get your reservations in early!

<li> There will be no class on Monday, Dec. 9.

</ul>