This study focuses on the development of a new, formal method for the automated checking of pedestrian circulation rules in Courthouse Design Guide. Automated building rule checking is an automated process of design evaluation against design requirements. Since the early 1970's, when the electronic representation of building design became available, automated building rule checking, a computational process, has been a focus of study, and it continues to be a popular research area because it facilitates the design evaluation process by reducing the checking time and evaluation costs and by increasing the objectivity and the reliability of the evaluation. Thanks to the emergence of BIM (Building Information Model) authoring software, BIM became available to use in real building design, and several automated building code checking systems were developed based on BIM. In practice, the use of a rule checking system in real design evaluation may be influenced by several factors. Among the factors that affect the accuracy and the reliability of automated checking such as checking algorithms and rule interpretation is the level of completeness of the BIM in the design process, which can cause limitations in the application of a rule checking algorithm to the model. Problems caused by the incompleteness of the BIM occurred in CORENET project, a project initiated by the Singapore government in 1999 for automation of building code checking, and GSA Courthouse Design Guide Automation project (GSA), initiated at Georgia Tech in 2007 also faced with the same problems caused by incompleteness of BIM in the development stage. This thesis is a continuing research of GSA-Courthouse Design Guide Automation project (Simply, GSA project). The theoretical goals of this study are to provide a logical foundation upon which one can build an automated checking module for circulation rule checking and that is capable of outlining the rule-validation process independently from its diverse implementation. The theory for circulation rule checking is devised to represent the process of the validation of a building design in the development stage. The theory deals with issues of validation caused by the lack of data in the development of a building design.