7.2 Satisfiability Algorithms for Natural Models
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 ...
Get Handbook of Automated Reasoning now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
