@article{cassez-jss-06,
  ABSTRACT = {In this paper, we consider Time Petri Nets (TPN)
                  where time is associated with transitions. We give a
                  formal semantics for TPNs in terms of Timed
                  Transition Systems. Then, we propose a translation
                  from TPNs to Timed Automata (TA) that preserves the
                  behavioral semantics (timed bisimilarity) of the
                  TPNs. For the theory of TPNs this result is
                  two-fold: i) reachability problems and more
                  generally TCTL model-checking are decidable for
                  bounded TPNs; ii) allowing strict time constraints
                  on transitions for TPNs preserves the results
                  described in i). The practical appli- cations of the
                  translation are: i) one can specify a system using
                  both TPNs and Timed Automata and a precise semantics
                  is given to the composition; ii) one can use
                  existing tools for analyzing timed automata (like
                  Kronos, Uppaal or Cmc) to analyze TPNs. In this
                  paper we describe the new feature of the tool Romeo
                  that implements our translation of TPNs in the
                  Uppaal input format. We also report on experiments
                  carried out on various examples and compare the
                  result of our method to state-of-the-art tool for
                  analyzing TPNs.  },
  AUTHOR = {Franck Cassez and Roux, Olivier Henri},
  JOURNAL = {Journal of Software and Systems},
  Type = {A - Journal},
  PAGES = {1456--1468},
  urlpaper = {papers/jss-06.pdf},
  TITLE = {Structural Translation from Time Petri Nets to Timed Automata},
  VOLUME = {79},
  NUMBER = {10},
  MONTH = OCT,
  PUBLISHER = {Elsevier},
  YEAR = {2006},
  keywords = {Time Petri nets, timed automata, expressiveness}
}

{"_id":"gbPHoeF3n7SyhWTwK","bibbaseid":"cassez-roux-structuraltranslationfromtimepetrinetstotimedautomata-2006","author_short":["Cassez, F.","Roux, O. H."],"bibdata":{"bibtype":"article","type":"A - Journal","abstract":"In this paper, we consider Time Petri Nets (TPN) where time is associated with transitions. We give a formal semantics for TPNs in terms of Timed Transition Systems. Then, we propose a translation from TPNs to Timed Automata (TA) that preserves the behavioral semantics (timed bisimilarity) of the TPNs. For the theory of TPNs this result is two-fold: i) reachability problems and more generally TCTL model-checking are decidable for bounded TPNs; ii) allowing strict time constraints on transitions for TPNs preserves the results described in i). The practical appli- cations of the translation are: i) one can specify a system using both TPNs and Timed Automata and a precise semantics is given to the composition; ii) one can use existing tools for analyzing timed automata (like Kronos, Uppaal or Cmc) to analyze TPNs. In this paper we describe the new feature of the tool Romeo that implements our translation of TPNs in the Uppaal input format. We also report on experiments carried out on various examples and compare the result of our method to state-of-the-art tool for analyzing TPNs. ","author":[{"firstnames":["Franck"],"propositions":[],"lastnames":["Cassez"],"suffixes":[]},{"propositions":[],"lastnames":["Roux"],"firstnames":["Olivier","Henri"],"suffixes":[]}],"journal":"Journal of Software and Systems","pages":"1456–1468","urlpaper":"papers/jss-06.pdf","title":"Structural Translation from Time Petri Nets to Timed Automata","volume":"79","number":"10","month":"October","publisher":"Elsevier","year":"2006","keywords":"Time Petri nets, timed automata, expressiveness","bibtex":"@article{cassez-jss-06,\n ABSTRACT = {In this paper, we consider Time Petri Nets (TPN)\n where time is associated with transitions. We give a\n formal semantics for TPNs in terms of Timed\n Transition Systems. Then, we propose a translation\n from TPNs to Timed Automata (TA) that preserves the\n behavioral semantics (timed bisimilarity) of the\n TPNs. For the theory of TPNs this result is\n two-fold: i) reachability problems and more\n generally TCTL model-checking are decidable for\n bounded TPNs; ii) allowing strict time constraints\n on transitions for TPNs preserves the results\n described in i). The practical appli- cations of the\n translation are: i) one can specify a system using\n both TPNs and Timed Automata and a precise semantics\n is given to the composition; ii) one can use\n existing tools for analyzing timed automata (like\n Kronos, Uppaal or Cmc) to analyze TPNs. In this\n paper we describe the new feature of the tool Romeo\n that implements our translation of TPNs in the\n Uppaal input format. We also report on experiments\n carried out on various examples and compare the\n result of our method to state-of-the-art tool for\n analyzing TPNs. },\n AUTHOR = {Franck Cassez and Roux, Olivier Henri},\n JOURNAL = {Journal of Software and Systems},\n Type = {A - Journal},\n PAGES = {1456--1468},\n urlpaper = {papers/jss-06.pdf},\n TITLE = {Structural Translation from Time Petri Nets to Timed Automata},\n VOLUME = {79},\n NUMBER = {10},\n MONTH = OCT,\n PUBLISHER = {Elsevier},\n YEAR = {2006},\n keywords = {Time Petri nets, timed automata, expressiveness}\n}\n\n\n","author_short":["Cassez, F.","Roux, O. H."],"key":"cassez-jss-06","id":"cassez-jss-06","bibbaseid":"cassez-roux-structuraltranslationfromtimepetrinetstotimedautomata-2006","role":"author","urls":{"Paper":"http://science.mq.edu.au/~fcassez/bib/papers/jss-06.pdf"},"keyword":["Time Petri nets","timed automata","expressiveness"],"metadata":{"authorlinks":{}}},"bibtype":"article","biburl":"http://science.mq.edu.au/~fcassez/bib/franck-bib.bib","dataSources":["8742EsvjQfyP2fYBW","qbqYFWskmoonRB43F","yYF8uwWqay28JyxZC"],"keywords":["time petri nets","timed automata","expressiveness"],"search_terms":["structural","translation","time","petri","nets","timed","automata","cassez","roux"],"title":"Structural Translation from Time Petri Nets to Timed Automata","year":2006}