@TechReport{ it:2004-033,
author = {Parosh Abdulla and Johann Deneux and Pritha Mahata},
title = {Closed, Open and Robust Timed Networks},
institution = {Department of Information Technology, Uppsala University},
department = {Division of Computer Systems},
year = {2004},
number = {2004-033},
month = aug,
note = {To appear in Infinity '04},
abstract = {We consider verification of safety properties for
parameterized systems of timed processes, so called 'timed
networks'. A timed network consists of a finite state
process, called a controller, and an arbitrary set of
identical timed processes. In [AJ03] it was shown that
checking safety properties is decidable in the case where
each timed process is equipped with a single real-valued
clock. In [ADM04], we showed that this is no longer
possible if each timed process is equipped with at least
two real-valued clocks. In this paper, we study two
subclasses of timed networks: 'closed' and 'open' timed
networks. In closed timed networks, all clock constraints
are non-strict, while in open timed networks, all clock
constraints are strict (thus corresponds to syntactic
removal of equality testing). We show that the problem
becomes decidable for closed timed network, while it
remains undecidable for open timed networks. We also
consider 'robust' semantics of timed networks by
introducing timing fuzziness through semantic removal of
equality testing. We show that the problem is undecidable
both for closed and open timed networks under the robust
semantics.}
}