1277.73 LTL (Linear Temporal Logic)과 유한 상태 머신