B.3 Semantics

The semantics of PSL formulas are defined with respect to a model. A model is a quintuple ( S, S ₀, R, P, L), where S is a finite set of states, S ₀ ? S is a set of initial states, R ? S S is the transition relation, P is a non-empty set of atomic propositions, and L is the valuation, a function L : S 2 ^P , mapping each state with a set of atomic propositions valid in that state.

A path ? is a finite (or infinite) sequence of states ? = ( ? ₀, ? ₁, ? ₂, ?, ? _n) (or ? = ( ? ₀, ? ₁, ? ₂, ?)). A computation path ? of a model M is a finite (or infinite) path ? such that for every i < n, R( ? _i, ? _{i +1}) and for no s, R( ? _n, s) (or such that for every i, R( ? _i, ? _{i +1})). Given a finite (or infinite) path ?, we define , an extension of the valuation function L from states to paths as follows: ( ?) = L( ? ₀) L(