On model checking multiple hybrid views

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 efinements and abstractions of a set of views (respectively).

• Type: Conference
• Year: 2004
• Where: ISOLA
• Authors: Michael Huth, Altaf Hussain
• Keywords: Common Refinement, ISOLA 2004, Labelled Transitions, Validity Problems