LTL & Auto

Notes

LTL & Automata S. Veloudis Friday 4th April, 2025 1 / 6 Interpretation (recap from Week 2) LTL formulae are interpreted (i.e. evaluated) over a discrete, linear model of time that is isomorphic to N Let Σ be a countable set of atomic propositions p, q, ... that are used to model the state of a system, and let ϕ be a formula over Σ Example (Traffic Light) Σ = {G , A, R} ϕ ≡ □(G ⇒ ♢A) An interpretation of ϕ takes the form of a function I that maps each natural number to a subset of Σ i.e., to an element of 2Σ I : N → 2Σ An interpretation I is thus an infinite sequence of sets of atomic propositions that essentially ‘assigns’ a set of atomic propositions to each time moment; each ‘assigned’ proposition is assumed to hold at t 2 / 6 Interpretation (contd.) Example (Traffic Light) In other words, an interpretation is a particular way of arranging the elements of 2Σ over the time line For each time t, the set of atomic propositions holding at t defines the state of the system at t Now, some interpretations happen to be models of ϕ, i.e. they satisfy ϕ, and some are not, i.e. they violate ϕ Notably, this is entirely analogous to, for instance, last week’s example in which some input words...