Model Checking Using Description Logic | UPT Perpustakaan UHAMKA