Local model checking for real-time systems

We present a local algorithm for model checking in a real-time extension of the modal mu-caculus. 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 bat 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 reel-time systems, we work with it 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 rep resent the system under investigation. In this sense, oar data structures are optima with respect to the given formula and automaton.