Real-time symbolic model checking for hard real-time systems

Citations Over Time

Abstract

We develop real-time symbolic model checking. Real-time systems can be described using timed automata. Although there exist model-checking algorithms for timed automata, the problem is intractable. In this paper, we propose a symbolic model-checking method as follows: Real-time systems can be expressed by BDDs. Symbolic computations are realized by approximations. The fixpoint computations of real-time temporal logic TCTL are realized by both forward and backward computations.

Related Papers

• → A Probabilistic Temporal Logic with Frequency Operators and Its Model Checking(2011)8 cited
• → A resolution method for CTL branching-time temporal logic(2002)18 cited
• → A Probabilistic Temporal Logic with Frequency Operators and Its Model Checking(2011)2 cited
• → A New Temporal Logic CTL[k-QDDC] and Its Verification(2008)1 cited
• Representing RCC relations in temporal logic(2015)