https://murray.cds.caltech.edu/index.php?action=history&feed=atom&title=EECI_2012%3A_Temporal_Logic 2026-09-05T16:36:45Z Revision history for this page on the wiki MediaWiki 1.44.2 https://murray.cds.caltech.edu/index.php?title=EECI_2012:_Temporal_Logic&diff=14021&oldid=prev 2012-05-14T09:20:56Z

<p><span class="autocomment">Additional Information</span></p> <table style="background-color: #fff; color: #202122;" data-mw="interface"> <col class="diff-marker" /> <col class="diff-content" /> <col class="diff-marker" /> <col class="diff-content" /> <tr class="diff-title" lang="en"> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">← Older revision</td> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Revision as of 09:20, 14 May 2012</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l12">Line 12:</td> <td colspan="2" class="diff-lineno">Line 12:</td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>==  Additional Information ==</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>==  Additional Information ==</div></td></tr> <tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">* [http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/ LTL2BA] - a web page (and program) for converting LTL formulas to Buchi automata.</ins></div></td></tr> <!-- diff cache key acs_math_mw_144-murraycds_:diff:1.41:old-14020:rev-14021:php=table --> </table>

Murray https://murray.cds.caltech.edu/index.php?title=EECI_2012:_Temporal_Logic&diff=14020&oldid=prev 2012-05-14T09:20:40Z

<p><span class="autocomment">Additional Information</span></p> <table style="background-color: #fff; color: #202122;" data-mw="interface"> <col class="diff-marker" /> <col class="diff-content" /> <col class="diff-marker" /> <col class="diff-content" /> <tr class="diff-title" lang="en"> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">← Older revision</td> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Revision as of 09:20, 14 May 2012</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l12">Line 12:</td> <td colspan="2" class="diff-lineno">Line 12:</td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>==  Additional Information ==</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>==  Additional Information ==</div></td></tr> <tr><td class="diff-marker" data-marker="−"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div><del style="font-weight: bold; text-decoration: none;">* [http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/ LTL2BA] - a web page (and program) for converting LTL formulas to Buchi automata.</del></div></td><td colspan="2" class="diff-side-added"></td></tr> <!-- diff cache key acs_math_mw_144-murraycds_:diff:1.41:old-14019:rev-14020:php=table --> </table>

Murray https://murray.cds.caltech.edu/index.php?title=EECI_2012:_Temporal_Logic&diff=14019&oldid=prev 2012-05-14T09:18:41Z

<p><span class="autocomment">Lecture Materials</span></p> <table style="background-color: #fff; color: #202122;" data-mw="interface"> <col class="diff-marker" /> <col class="diff-content" /> <col class="diff-marker" /> <col class="diff-content" /> <tr class="diff-title" lang="en"> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">← Older revision</td> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Revision as of 09:18, 14 May 2012</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l5">Line 5:</td> <td colspan="2" class="diff-lineno">Line 5:</td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>==  Lecture Materials ==</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>==  Lecture Materials ==</div></td></tr> <tr><td class="diff-marker" data-marker="−"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>* Lecture slides: [http://www.cds.caltech.edu/~<del style="font-weight: bold; text-decoration: none;">utopcu</del>/<del style="font-weight: bold; text-decoration: none;">EECI2012</del>/<del style="font-weight: bold; text-decoration: none;">L2_ltl_14May12</del>.pdf Linear Temporal Logic] (Presentation and notation follow that in "Principles of Model Checking" chapter 5.1 by Baier and Katoen.)</div></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>* Lecture slides: [http://www.cds.caltech.edu/~<ins style="font-weight: bold; text-decoration: none;">murray</ins>/<ins style="font-weight: bold; text-decoration: none;">courses</ins>/<ins style="font-weight: bold; text-decoration: none;">eeci-sp12/L3_ltl-14May12</ins>.pdf Linear Temporal Logic] (Presentation and notation follow that in "Principles of Model Checking" chapter 5.1 by Baier and Katoen.)</div></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== Further Reading ==</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== Further Reading ==</div></td></tr> <!-- diff cache key acs_math_mw_144-murraycds_:diff:1.41:old-14015:rev-14019:php=table --> </table>

Murray https://murray.cds.caltech.edu/index.php?title=EECI_2012:_Temporal_Logic&diff=14015&oldid=prev 2012-05-13T19:17:57Z

<p></p> <table style="background-color: #fff; color: #202122;" data-mw="interface"> <col class="diff-marker" /> <col class="diff-content" /> <col class="diff-marker" /> <col class="diff-content" /> <tr class="diff-title" lang="en"> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">← Older revision</td> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Revision as of 19:17, 13 May 2012</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l1">Line 1:</td> <td colspan="2" class="diff-lineno">Line 1:</td></tr> <tr><td class="diff-marker" data-marker="−"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>{{<del style="font-weight: bold; text-decoration: none;">AFRL12 </del>header|prev=Automata Theory|next=Model Checking}}</div></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>{{<ins style="font-weight: bold; text-decoration: none;">eeci-sp12 </ins>header|prev=Automata Theory|next=Model Checking}}</div></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>{{righttoc}}</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>{{righttoc}}</div></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td></tr> <!-- diff cache key acs_math_mw_144-murraycds_:diff:1.41:old-14007:rev-14015:php=table --> </table>

Murray https://murray.cds.caltech.edu/index.php?title=EECI_2012:_Temporal_Logic&diff=14007&oldid=prev 2012-05-13T15:38:38Z

<p></p> <table style="background-color: #fff; color: #202122;" data-mw="interface"> <col class="diff-marker" /> <col class="diff-content" /> <col class="diff-marker" /> <col class="diff-content" /> <tr class="diff-title" lang="en"> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">← Older revision</td> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Revision as of 15:38, 13 May 2012</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l5">Line 5:</td> <td colspan="2" class="diff-lineno">Line 5:</td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>==  Lecture Materials ==</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>==  Lecture Materials ==</div></td></tr> <tr><td class="diff-marker" data-marker="−"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>* Lecture slides: [http://www.cds.caltech.edu/~<del style="font-weight: bold; text-decoration: none;">murray</del>/<del style="font-weight: bold; text-decoration: none;">courses</del>/<del style="font-weight: bold; text-decoration: none;">afrl-sp12/L3_ltl-24Apr12</del>.pdf Linear Temporal Logic] (Presentation and notation follow that in "Principles of Model Checking" chapter 5.1 by Baier and Katoen.)</div></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>* Lecture slides: [http://www.cds.caltech.edu/~<ins style="font-weight: bold; text-decoration: none;">utopcu</ins>/<ins style="font-weight: bold; text-decoration: none;">EECI2012</ins>/<ins style="font-weight: bold; text-decoration: none;">L2_ltl_14May12</ins>.pdf Linear Temporal Logic] (Presentation and notation follow that in "Principles of Model Checking" chapter 5.1 by Baier and Katoen.)</div></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== Further Reading ==</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== Further Reading ==</div></td></tr> <!-- diff cache key acs_math_mw_144-murraycds_:diff:1.41:old-13925:rev-14007:php=table --> </table>

Utopcu https://murray.cds.caltech.edu/index.php?title=EECI_2012:_Temporal_Logic&diff=13925&oldid=prev 2012-04-22T16:17:00Z

<p><span class="autocomment">Additional Information</span></p> <table style="background-color: #fff; color: #202122;" data-mw="interface"> <col class="diff-marker" /> <col class="diff-content" /> <col class="diff-marker" /> <col class="diff-content" /> <tr class="diff-title" lang="en"> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">← Older revision</td> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Revision as of 16:17, 22 April 2012</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l12">Line 12:</td> <td colspan="2" class="diff-lineno">Line 12:</td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>==  Additional Information ==</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>==  Additional Information ==</div></td></tr> <tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">* [http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/ LTL2BA] - a web page (and program) for converting LTL formulas to Buchi automata.</ins></div></td></tr> <!-- diff cache key acs_math_mw_144-murraycds_:diff:1.41:old-13924:rev-13925:php=table --> </table>

Murray https://murray.cds.caltech.edu/index.php?title=EECI_2012:_Temporal_Logic&diff=13924&oldid=prev 2012-04-22T16:16:09Z

<p></p> <table style="background-color: #fff; color: #202122;" data-mw="interface"> <col class="diff-marker" /> <col class="diff-content" /> <col class="diff-marker" /> <col class="diff-content" /> <tr class="diff-title" lang="en"> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">← Older revision</td> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Revision as of 16:16, 22 April 2012</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l1">Line 1:</td> <td colspan="2" class="diff-lineno">Line 1:</td></tr> <tr><td class="diff-marker" data-marker="−"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>{{<del style="font-weight: bold; text-decoration: none;">eeci-sp11 </del>header|prev=Automata Theory|next=Model Checking}}</div></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>{{<ins style="font-weight: bold; text-decoration: none;">AFRL12 </ins>header|prev=Automata Theory|next=Model Checking}}</div></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>{{righttoc}}</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>{{righttoc}}</div></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td></tr> <!-- diff cache key acs_math_mw_144-murraycds_:diff:1.41:old-13923:rev-13924:php=table --> </table>

Murray https://murray.cds.caltech.edu/index.php?title=EECI_2012:_Temporal_Logic&diff=13923&oldid=prev 2012-04-22T16:15:53Z

<p>Created page with &#039;{{eeci-sp11 header|prev=Automata Theory|next=Model Checking}} {{righttoc}} In this lecture we introduce &#039;&#039;linear temporal logic&#039;&#039; (LTL), a mathematical language for describing l…&#039;</p> <p><b>New page</b></p><div>{{eeci-sp11 header|prev=Automata Theory|next=Model Checking}}<br /> {{righttoc}}<br /> <br /> In this lecture we introduce &#039;&#039;linear temporal logic&#039;&#039; (LTL), a mathematical language for describing linear time properties of transition systems. After a short introduction to the concept of temporal logics, we introduce the syntax and semantics of LTL, including examples. Examples of LTL specifications for control protocols are drawn from the applications given in the introductory lecture. If time permits, we will also briefly introduce other temporal logics and describe some of the differences between various formulations.<br /> <br /> == Lecture Materials ==<br /> * Lecture slides: [http://www.cds.caltech.edu/~murray/courses/afrl-sp12/L3_ltl-24Apr12.pdf Linear Temporal Logic] (Presentation and notation follow that in &quot;Principles of Model Checking&quot; chapter 5.1 by Baier and Katoen.)<br /> <br /> == Further Reading ==<br /> * &lt;p&gt;[http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&amp;tid=11481 Principles of Model Checking], C. Baier and J.-P. Katoen, The MIT Press, 2008. A detailed reference on model checking. Slides for this lecture follow Chapter 6 of this reference. &lt;/p&gt;<br /> * &lt;p&gt;[http://research.microsoft.com/en-us/um/people/lamport/tla/book.html &#039;&#039;Specifying Systems&#039;&#039;], L. Lamport.. Addison-Wesley, 2002. This is a very readable text on specification using temporal logic of actions (LTA).&lt;/p&gt;<br /> <br /> == Additional Information ==</div>

Murray