35
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      Avoiding Shared Clocks in Networks of Timed Automata

      Preprint
      ,

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          Networks of timed automata (NTA) are widely used to model distributed real-time systems. Quite often in the literature, the automata are allowed to share clocks, i.e. transitions of one automaton may be guarded by conditions on the value of clocks reset by another automaton. This is a problem when one considers implementing such model in a distributed architecture, since reading clocks a priori requires communications which are not explicitly described in the model. We focus on the following question: given an NTA A1 || A2 where A2 reads some clocks reset by A1, does there exist an NTA A'1 || A'2 without shared clocks with the same behavior as the initial NTA? For this, we allow the automata to exchange information during synchronizations only, in particular by copying the value of their neighbor's clocks. We discuss a formalization of the problem and define an appropriate behavioural equivalence. Then we give a criterion using the notion of contextual timed transition system, which represents the behavior of A2 when in parallel with A1. Finally, we effectively build A'1 || A'2 when it exists.

          Related collections

          Most cited references11

          • Record: found
          • Abstract: not found
          • Book Chapter: not found

          A Tutorial on Uppaal

            Bookmark
            • Record: found
            • Abstract: not found
            • Article: not found

            Refinement of actions and equivalence notions for concurrent systems

              Bookmark
              • Record: found
              • Abstract: not found
              • Book Chapter: not found

              Kronos: A model-checking tool for real-time systems

                Bookmark

                Author and article information

                Journal
                18 October 2013
                2013-11-12
                Article
                10.2168/LMCS-9(4:13)2013
                1310.5558
                aafe0bfd-6c8c-4d6c-9df2-3734982db335

                http://arxiv.org/licenses/nonexclusive-distrib/1.0/

                History
                Custom metadata
                Logical Methods in Computer Science, Volume 9, Issue 4 (November 14, 2013) lmcs:933
                Article accepted to Logical Methods in Computer Science. Number: LMCS-2013-837 Special issue: 23rd International Conference on Concurrency Theory (CONCUR 2012)
                cs.FL
                LMCS

                Comments

                Comment on this article