Task 5: Lineartime model checking
Objectives
UNDERCONSTRUCTION
Notes
 Moshe Vardi's presentation of Task 5 in Edinburgh. [slides]
 Discussions on the above (to follow).
Background literature
[1] 
M. Y. Vardi and P. Wolper, An automatatheoretic approach to automatic program
verification, in Proc. 1st Symp. on
Logic in Computer Science, (Cambridge), pp. 332344, June 1986. [ List ]
@INPROCEEDINGS{VW86b, AUTHOR = {M. Y. Vardi and P. Wolper}, TITLE = {An AutomataTheoretic Approach to Automatic Program Verification}, BOOKTITLE = {Proc. 1st Symp. on Logic in Computer Science}, PAGES = {332344}, YEAR = {1986}, MONTH = JUN, ADDRESS = {Cambridge}, URL = {http://www.cs.rice.edu/~vardi/papers/lics86.pdf.gz} }

[2] 
M. Y. Vardi, Verification of concurrent programs  the automatatheoretic
framework, Annals of Pure and Applied
Logic, vol. 51, pp. 7998, 1991. [ List ]
@ARTICLE{Var91, AUTHOR = {M. Y. Vardi}, TITLE = {Verification of concurrent programs  the automatatheoretic framework}, JOURNAL = {Annals of Pure and Applied Logic}, VOLUME = {51}, PAGES = {7998}, YEAR = {1991}, URL = {http://www.cs.rice.edu/~vardi/papers/lics87r2.ps.gz} }

[3] 
M. Y. Vardi, Probabilistic lineartime model checking: An overview of the
automatatheoretic approach, in 5th
Int'l Workshop on Formal Methods for RealTime and Probabilistic Systems
(J. P. Katoen, ed.), Lecture Notes in Computer Science 1601, pp. 265276,
SpringerVerlag, 1999. [ List ]
@INPROCEEDINGS{Var99, AUTHOR = {M. Y. Vardi}, TITLE = {Probabilistic LinearTime Model Checking: An Overview of the AutomataTheoretic Approach}, BOOKTITLE = {5th Int'l Workshop on Formal Methods for RealTime and Probabilistic Systems}, SERIES = {Lecture Notes in Computer Science 1601}, EDITOR = {J. P. Katoen}, PUBLISHER = {SpringerVerlag}, PAGES = {265276}, YEAR = {1999}, URL = {http://www.cs.rice.edu/~vardi/papers/arts99.ps.gz} }

[4] 
C. Courcoubetis, M. Y. Vardi, P. Wolper, and M. Yannakakis, Memory efficient algorithms for the verification of temporal
properties, Formal Methods in System
Design, vol. 1, pp. 275288, 1992. [ List ]
@ARTICLE{CVWY92, AUTHOR = {C. Courcoubetis and M. Y. Vardi and P. Wolper and M. Yannakakis}, TITLE = {Memory Efficient Algorithms for the Verification of Temporal Properties}, JOURNAL = {Formal Methods in System Design}, PAGES = {275288}, VOLUME = {1}, YEAR = {1992}, URL = {http://www.cs.rice.edu/~vardi/papers/cav90rj.ps.gz} }

[5] 
M. Y. Vardi and P. Wolper, Reasoning about infinite computations,
Information and Computation, vol. 115, pp. 137, Nov. 1994. [ List ]
@ARTICLE{VW94, AUTHOR = {M. Y. Vardi and P. Wolper}, TITLE = {Reasoning about Infinite Computations}, JOURNAL = {Information and Computation}, VOLUME = {115}, NUMBER = {1}, YEAR = {1994}, MONTH = NOV, PAGES = {137}, URL = {http://www.cs.rice.edu/~vardi/papers/focs83rj.ps.gz} }

[6] 
M. Y. Vardi, An automatatheoretic approach to linear temporal
logic, in Logics for Concurrency:
Structure versus Automata (F. Moller and G. Birtwistle, eds.), vol. 1043 of
Lecture Notes in Computer Science, pp. 238266, SpringerVerlag,
Berlin, 1996. [ List ]
@INPROCEEDINGS{Var96, AUTHOR = {M. Y. Vardi}, TITLE = {An automatatheoretic approach to linear temporal logic}, EDITOR = {F. Moller and G. Birtwistle}, BOOKTITLE = {Logics for Concurrency: Structure versus Automata}, SERIES = {Lecture Notes in Computer Science}, PUBLISHER = {SpringerVerlag, Berlin}, VOLUME = {1043}, PAGES = {238266}, YEAR = {1996}, URL = {http://www.cs.rice.edu/~vardi/papers/banff94rj.ps.gz} }

[7] 
M. Y. Vardi, Alternating automata and program
verification, in Computer Science
Today Recent Trends and Developments, vol. 1000 of Lecture Notes in
Computer Science, pp. 471485, SpringerVerlag, Berlin, 1995. [ List ]
@INPROCEEDINGS{Var95d, AUTHOR = {M. Y. Vardi}, TITLE = {Alternating automata and program verification}, BOOKTITLE = {Computer Science Today Recent Trends and Developments}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {1000}, YEAR = {1995}, PUBLISHER = {SpringerVerlag, Berlin}, PAGES = {471485}, URL = {http://www.cs.rice.edu/~vardi/papers/vol1000.ps.gz} }

[8] 
R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper, Simple onthefly automatic verification of linear temporal
logic, in Protocol Specification,
Testing, and Verification (P. Dembiski and M. Sredniawa, eds.), pp. 318,
Chapman & Hall, Aug. 1995. [ List ]
@INPROCEEDINGS{GPVW95, AUTHOR = {R. Gerth and D. Peled and M. Y. Vardi and P. Wolper}, EDITOR = {P. Dembiski and M. Sredniawa}, PUBLISHER = {Chapman \& Hall}, TITLE = {Simple onthefly automatic verification of linear temporal logic}, BOOKTITLE = {Protocol Specification, Testing, and Verification}, PAGES = {318}, MONTH = AUG, YEAR = {1995}, URL = {http://www.cs.rice.edu/~vardi/papers/pstv95rj.ps.gz} }

[9] 
N. Daniele, F. Guinchiglia, and M. Y. Vardi, Improved automata generation for linear temporal
logic, in Computer Aided Verification,
Proc. 11th International Conference, vol. 1633 of Lecture Notes in
Computer Science, pp. 249260, SpringerVerlag, 1999. [ List ]
@INPROCEEDINGS{DGV99, AUTHOR = {N. Daniele and F. Guinchiglia and M. Y. Vardi}, TITLE = {Improved automata generation for linear temporal logic}, BOOKTITLE = {Computer Aided Verification, Proc. 11th International Conference}, PAGES = {249260}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {1633}, PUBLISHER = {SpringerVerlag}, YEAR = {1999}, URL = {http://www.cs.rice.edu/~vardi/papers/cav992rj.ps.gz} }

[10] 
O. Kupferman and M. Y. Vardi, Model checking of safety properties,
Formal methods in System Design, vol. 19, pp. 291314, Nov. 2001. [ List ]
@ARTICLE{KV01d, AUTHOR = {O. Kupferman and M. Y. Vardi}, TITLE = {Model checking of safety properties}, JOURNAL = {Formal methods in System Design}, VOLUME = {19}, NUMBER = {3}, MONTH = NOV, PAGES = {291314}, YEAR = {2001}, URL = {http://www.cs.rice.edu/~vardi/papers/cav991.ps.gz} }

[11] 
O. Kupferman and M. Y. Vardi, Weak alternating automata are not that
weak, ACM Trans. on Computational
Logic, vol. 2001, pp. 408429, July 2001. [ List ]
@ARTICLE{KV01c, AUTHOR = {O. Kupferman and M. Y. Vardi}, TITLE = {Weak alternating automata are not that weak}, JOURNAL = {ACM Trans. on Computational Logic}, VOLUME = {2001}, NUMBER = {2}, MONTH = JUL, YEAR = {2001}, PAGES = {408429}, URL = {http://www.cs.rice.edu/~vardi/papers/istcs97rj.ps.gz} }
