모형 검사는 현재 가장 많이 사용되는 정형 검사 방법이다 모형 검사에서는 시스템을 기술한 모형과 시스템에서 만족되어야 할 속성을 기술한 명세언어를 SMV, SPIN 과 같은 모형 검사기에 입력하여 모형이 요구한 속성들을 만족하는지 검사한다. 시스템은 대부분 상태도와 같은 계층형 유한 상태 기계들로 기술되고 속성 명세 언어로는 CTL 혹은 PLTL 과 같은 시제 논리 를 많이 사용한다. 그런데 이러한 명세 언어는 크립키 구조와 같은 평면 구조에서 해석된다. 따라서 계층적으로 기술된 시스템 의 모형이 모형 검사기에 입력되기 위해서 는 평탄화 과정이 필요하다. 평탄화 과정에서 상태수의 증가로 인한 상태폭발이 가중 되고 본래 기술된 계층성을 온전히 지킬 수 없었다. 따라서 본 논문에서는 계층형 크립키 구조를 정의하고 계층형 구조에서 해석 되는 계층형 CTL인 HiCTL을 정의한다.