This week's talk will be by Shant Harutunian. Model-Checking in Dense Real Time -------------------------------------- The talk will begin with a review of the propositional temporal logic CTL (computation tree logic) and transition systems. We will demonstrate, with an example, how to decide whether a transition system satisfies a sample CTL formula. We will then introduce the timed graph and discuss its semantics. We will discuss the runs over the timed graph, which has infinitely many states. We will show that these runs are equivalent to runs of a region graph, which is finite state. We will then discuss the syntax and semantics of TCTL (Timed CTL). The semantics of TCTL shall be in terms of paths, which are functions that map nonnegative reals to the states of the timed graph. We will proceed to show how to model-check a timed graph by checking that paths, based on runs of its region graph, satisfy a given TCTL formula. We will note how this algorithm depends on tracking of the duration of time along each path. We will then show an alternative model checking method whereby we extend the region graph to an augmented region graph. We will discuss a model checking algorithm for a timed graph by checking that paths, based on runs of its augmented region graph, satisfy a given TCTL formula, without requiring the tracking of duration along a path. The background assumed for this talk is familiarity with CTL and transition systems. Familiarity with the Mu-Calculus and the Tarski-Knaster theorem is beneficial so as to understand the basis of the model-checking algorithm, but is not necessary. The talk will be based on a paper by Rajeev Alur, et al. The URL for this paper is http://www.cis.upenn.edu/~alur/Lics90D.ps.gz. An overview of CTL and model checking is found at http://www.cs.utexas.edu/users/emerson/pubs/fmt96q.ps Regards, Shant