The branching time decision procedures described in the previous subsection construct a “most general” model for any satisfiable formula. For any sub-formula, all propositionally consistent sets are traversed. The number of propositionally consistent sets of sub-formulas is exponential in the length of the formula; therefore, with an explicit representation of sets these algorithms are limited to “small” formulas.

Natural models for linear time logics are sequences of points. Each point determines a propositionally consistent set of sub-formulas, namely the set of those sub-formulas which are valid in this point. Often, the number of different propositionally consistent sets determined by ...

Start Free Trial

No credit card required