June 2001
Intermediate to advanced
2128 pages
82h 43m
English
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 ...
Read now
Unlock full access