On Model Checking Multiple Hybrid Views

Abstract. We study consistency, satisfiability, and validity problems for collectively model checking a set of views endowed with labelled transitions, hybrid constraints on states, and atomic propositions. A PTIME algorithm for deciding whether a set of views has a common refinement (consistency) is given. We prove that deciding whether a common refinement satisfies a formula of the hybrid mu-calculus (satisfiability), and its dual (validity), are EXPTIME-complete. We determine two generically generated “summary ” views that constitute informative and consistent common refinements and abstractions of a set of views (respectively).