Review and comparison of the syntax and semantics of temporal logics LTL and CTL. Distinction between the direct observability of individual runs, and the assessment of alternative possibilities in branching-time logics like CTL. Valuation of CTL formulae on specific transition systems. Distinct expressiveness of LTL and CTL: example to show **AF AG** is not **AFG**.

*Link:* Slides (with CTL valuation table corrected)

### Reading

Two items to read for Thursday:

- H. de Jong. Qualitative modeling and simulation of bacterial regulatory networks. In
*Computational Methods in Systems Biology: Proceedings of the 6th International Conference CMSB 2008*, Lecture Notes in Bioinformatics 5307, p. 1. Springer-Verlag, 2008. - P. T. Monteiro, D. Ropers, R. Mateescu, A. T. Freitas, and H. de Jong. Temporal logic patterns for querying dynamic models of cellular interaction networks.
*Bioinformatics*, 24(16):227–233, 2008.

The first of these is an invited conference talk, giving an overview of some work on applying model-checking to problems in systems biology. The second is a more detailed article on the material.