# Task 5: Linear-time model checking

## Objectives

UNDERCONSTRUCTION

## Material

- 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 automata-theoretic approach to automatic program
verification, in Proc. 1st Symp. on
Logic in Computer Science, (Cambridge), pp. 332-344, June 1986.[ BibTeX ] |

[2] |
M. Y. Vardi, Verification of concurrent programs - the automata-theoretic
framework, Annals of Pure and Applied
Logic, vol. 51, pp. 79-98, 1991.[ BibTeX ] |

[3] |
M. Y. Vardi, Probabilistic linear-time model checking: An overview of the
automata-theoretic approach, in 5th
Int'l Workshop on Formal Methods for Real-Time and Probabilistic Systems
(J. P. Katoen, ed.), Lecture Notes in Computer Science 1601, pp. 265-276,
Springer-Verlag, 1999.[ BibTeX ] |

[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. 275-288, 1992.[ BibTeX ] |

[5] |
M. Y. Vardi and P. Wolper, Reasoning about infinite computations,
Information and Computation, vol. 115, pp. 1-37, Nov. 1994.[ BibTeX ] |

[6] |
M. Y. Vardi, An automata-theoretic 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. 238-266, Springer-Verlag,
Berlin, 1996.[ BibTeX ] |

[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. 471-485, Springer-Verlag, Berlin, 1995.[ BibTeX ] |

[8] |
R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper, Simple on-the-fly automatic verification of linear temporal
logic, in Protocol Specification,
Testing, and Verification (P. Dembiski and M. Sredniawa, eds.), pp. 3-18,
Chapman & Hall, Aug. 1995.[ BibTeX ] |

[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. 249-260, Springer-Verlag, 1999.[ BibTeX ] |

[10] |
O. Kupferman and M. Y. Vardi, Model checking of safety properties,
Formal methods in System Design, vol. 19, pp. 291-314, Nov. 2001.[ BibTeX ] |

[11] |
O. Kupferman and M. Y. Vardi, Weak alternating automata are not that
weak, ACM Trans. on Computational
Logic, vol. 2001, pp. 408-429, July 2001.[ BibTeX ] |