On model checking multiple hybrid views

We study consistency, satis¯ability, and validity problems for collectively model checking a set of views endowed with labelled transi- tions, hybrid constraints on states, and atomic propositions. A PTIME algorithm for deciding whether a set of views has a common re¯nement (consistency) is given. We prove that deciding whether a common re¯ne- ment satis¯es a formula of the hybrid mu-calculus (satis¯ability), and its dual (validity), are EXPTIME-complete. We determine two generically generated \summary" views that constitute informative and consistent common re¯nements and abstractions of a set of views (respectively)