Logical Languages for Specification and Verification of Reactive System's Behavior

Logical languages are playing important roles in specification and verification of reactive systems. In general, computer system specifications are created based on logical notations and proofs. In the spirit of Logical languages for reactive systems propositional Logic and Ternporal Logic are becoming the center of attention. A number of researches have verification. We believe that a pause is in order, at this point, to analyze and review the current state of the research in this area. In this area. In this paper we review a set of logical theories computational aspects of computer aided verifications of reactive systems. We discuss First order Logic, Multimodal Logic, Temporal logic modal logic , model cheching and buchi – automata Further, we compare first and second order llogic, w-automata and formal languages.

کلیدواژه ها:

Termporal Logic ، Model Checking ، Model Logic ، Multimodal Logic ، Reactive systems