Using a priority preorder on requirements or specifications,
we lift established property-verification techniques of threevalued
model checking from single to multiple viewpoints.
This lift guarantees a maximal degree of autonomy and
accountability to single views, automatically synthesizes
single-analysis results for multiple-view consistency and assertion
checking, allows the re-use of single-view technology
(e.g. standard model checkers), and transforms many
meta-results (e.g. soundness of abstraction) from the singleview
to the multiple-view setting. We formulate assertionconsistency
lattices as a proper denotational universe for
this lift, show that their symmetric versions are DeMorgan
lattices, and classify both structures through (idempotent)
order-isomorphisms on (self-dual) priority preorders
in the finite case. In particular, this lift generalizes Fitting’s
multiple-valued semantics of modal logic in that our treatment
of negation generalizes Heyting negation beyond fully
specified and consistent models. We compare our approach
to existing work on multiple-valued model checking.