Pemodelan logika pemeriksaan temporal linier dengan buchi automata=Logic checking linear temporal with buchi automata

Correctness and reliability is two keywords successibilites of design both hardware and software systems. To get correct and reliability systems, it must be tight checking and testing overall components. Once of better checking method is modeling system behavioral, called Model Checking, this method possibly check system components part by part, so reliability of its overall components could be guarantee. The model checking mechanism is formulating system behavioral in logic sound and prepositional logic. Automata is an algebra model contents states, also transition between states. An automata model that accepting infinite states sequins transition or transition through final state infinitely often, is Buchi Automaton. Reactive systems characterized with its continuous reaction with environment and non-terminating. If checking does for behavioral system time to time, then the process in system considering like temporal habit, model which is satisfying this behavioral called Model Temporal Logic. If checking does for time to time as linear, then model called Model Linear Temporal Logic (MLTL) on topple M = (S, R, Label) . MLTL constructed using graph exploration and Buchi automaton then MLTL can be stated in an automata on topple Aw = (E, S, S° , F, p, Label) . This mechanism called Logic Checking Linear Temporal Modeling with Buchi Automata. Keywords: Modeling, Checking, Reactive system, Temporal Logic, Automaton