Local Model Checking for Real-Time Systems (Extended Abstract)

) ? Oleg V. Sokolsky Scott A. Smolka Department of Computer Science SUNY at Stony Brook Stony Brook, NY 11794-4400 foleg,sasg@cs.sunysb.edu Abstract. We present a local algorithm for model checking in a real-time extension of the modal mu-calculus. As such, the whole state space of the realtime system under investigation need not be explored, but rather only that portion necessary to determine the truthhood of the logical formula. To the best of our knowledge, this is the first local algorithm for the verification of real-time systems to appear in the literature. Like most algorithms dealing with real-time systems, we work with a finite quotient of the inherently infinite state space. For maximal efficiency, we obtain, on-the-fly, a quotient that is as coarse as possible in the following sense: refinements of the quotient are carried out only when necessary to satisfy clock constraints appearing in the logical formula or timed automaton used to represent the system under investigati..