Model-checking is a promising technique for the verification and validation of systems. Practical systems need complicated design descriptions because they often refer to situations concerning exceptional cases in addition to normal, regular behaviours. Since properties deal with a lot of exceptional cases, the property formulae to be verified become complicated and hard to understand. Further, as both system and property descriptions are complicated, the state space searched in the model-checking process becomes large, which affects the execution performance. This paper employs a model-checking technique based on multi-valued transition systems so that we can reduce such complexities. It discusses the advantage by applying the idea to an example case of the behavioural analysis of the EJB component framework.