Closed, Open and Robust Timed Networks

• 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.

Ämnesord

NATURVETENSKAP  -- Data- och informationsvetenskap (hsv//swe)

NATURAL SCIENCES  -- Computer and Information Sciences (hsv//eng)

Publikations- och innehållstyp

vet (ämneskategori)

rap (ämneskategori)