Title: Formal description of properties of concurrency system by temporal logic
Abstract: The temporal logic is a formal method for describing sequences of transition between states in a reactive (concurrent) system. It is common to use the temporal logic to specify the properties that the design must satisfy. The temporal logic is the basic of model checking. This paper states the syntax and semantics of CTL~* and its sub-logics: CTL and LTL, and analyzes how to state the properties of concurrent system, and finally the application example is given.
Publication Year: 2004
Publication Date: 2004-01-01
Language: en
Type: article
Access and Citation
Cited By Count: 3
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot