Predicate Logic Framework  for Verification of Timed
                          Distributed Systems
<P>                              A.Slissenko
                          University Paris 12
<P>
    The talk is a survey of a recent work, done mainly with D.Beauquier,
on developing  a verification framework for distributed systems
with timed constraints that may involve non-trivial arithmetic
(e. g. clock synchronization). The time we treat is continuous
(the framework works also for discrete time but with much less
efficiency). The main theoretical results concern the semantics of
timed algorithms and decidable classes of verification. The
decidable algorithms give a description of counter-models of  a
bounded  complexity. Thus, they are of interest independently of
our  decidables classes, for example as a tool of search for
attacks on security of bounded complexity.  What is surprising is
that a rather straighforward implementation of one of the
algorithms shows that it really works  for known benchmark
problems and simple protocols.