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