Lecture 8: Mix, match and use temporal logics

6 February 2010

Revisit example valuation of CTL formula, now corrected. Further possible logics: Hennessy-Milner, modal μ-calculus, and monadic second-order logic. Presentation of syntax, semantics, and small examples. Relative expressiveness. Mixing and matching modalities and operators for convenience, distinct from expressiveness: CTL- as an example.

Application to specific biological models, as discussed in these articles: Fages and Rizk evaluating LTL formulae over time series data; de Jong et al. on mapping textual descriptions into CTL.

Link: Slides

1 Comment | Lecture Log | Tagged: , , | Permalink
Posted by Ian Stark

Lecture 7: From LTL and CTL to CTL*

2 February 2010

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:

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.

Comments Off on Lecture 7: From LTL and CTL to CTL* | Lecture Log | Tagged: , | Permalink
Posted by Ian Stark

Lecture 5: Linear Temporal Logic

25 January 2010

The slides for this lecture review the notions of labelled transition systems, runs and traces, and give examples of the expansion of Petri net behaviour into labelled transition systems.

Boardwork then gave definitions of LTL formula, their meaning, and some small examples of application to LTS runs and Petri net behaviours.

Heiner et al. discuss how even finite reachability graphs for Petri nets may blow up very fast (§4(5)). However, they then jump straight to branching-time with CTL.

Huth and Ryan present the syntax and semantics of LTL (§3(2)) as well as some motivation on model checking.

The SPIN tool is based on LTL model checking.

Comments Off on Lecture 5: Linear Temporal Logic | Lecture Log | Tagged: , , | Permalink
Posted by Ian Stark