@article{DBLP:journals/entcs/CassezR05,
  author    = {Franck Cassez and
               Olivier H. Roux},
  title     = {Structural Translation from Time Petri Nets to Timed Automata},
  journal   = {Electr. Notes Theor. Comput. Sci. (Proceedings of AVOCS 2004)},
  volume    = {128},
          Type = {B - International Conferences},
  number    = {6},
  pages     = {145--160},
  year      = {2005},
  url       = {http://dx.doi.org/10.1016/j.entcs.2005.04.009},
  doi       = {10.1016/j.entcs.2005.04.009},
  urlslides = {papers/slides-avocs-04.pdf},

  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 behavioural 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 applications 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 analysing timed automata (like Kronos, Uppaal or Cmc) to analyse TPNs.},
  keywords = {Petri nets, timed, automata},
}

{"_id":"oCFzTyDQdBuiLTMXS","bibbaseid":"cassez-roux-structuraltranslationfromtimepetrinetstotimedautomata-2005","author_short":["Cassez, F.","Roux, O. H."],"bibdata":{"bibtype":"article","type":"B - International Conferences","author":[{"firstnames":["Franck"],"propositions":[],"lastnames":["Cassez"],"suffixes":[]},{"firstnames":["Olivier","H."],"propositions":[],"lastnames":["Roux"],"suffixes":[]}],"title":"Structural Translation from Time Petri Nets to Timed Automata","journal":"Electr. Notes Theor. Comput. Sci. (Proceedings of AVOCS 2004)","volume":"128","number":"6","pages":"145–160","year":"2005","url":"http://dx.doi.org/10.1016/j.entcs.2005.04.009","doi":"10.1016/j.entcs.2005.04.009","urlslides":"papers/slides-avocs-04.pdf","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 behavioural 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 applications 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 analysing timed automata (like Kronos, Uppaal or Cmc) to analyse TPNs.","keywords":"Petri nets, timed, automata","bibtex":"@article{DBLP:journals/entcs/CassezR05,\n author = {Franck Cassez and\n Olivier H. Roux},\n title = {Structural Translation from Time Petri Nets to Timed Automata},\n journal = {Electr. Notes Theor. Comput. Sci. (Proceedings of AVOCS 2004)},\n volume = {128},\n Type = {B - International Conferences},\n number = {6},\n pages = {145--160},\n year = {2005},\n url = {http://dx.doi.org/10.1016/j.entcs.2005.04.009},\n doi = {10.1016/j.entcs.2005.04.009},\n urlslides = {papers/slides-avocs-04.pdf},\n\n 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 behavioural 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 applications 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 analysing timed automata (like Kronos, Uppaal or Cmc) to analyse TPNs.},\n keywords = {Petri nets, timed, automata},\n}\n\n","author_short":["Cassez, F.","Roux, O. H."],"key":"DBLP:journals/entcs/CassezR05","id":"DBLP:journals/entcs/CassezR05","bibbaseid":"cassez-roux-structuraltranslationfromtimepetrinetstotimedautomata-2005","role":"author","urls":{"Paper":"http://dx.doi.org/10.1016/j.entcs.2005.04.009","Slides":"http://science.mq.edu.au/~fcassez/bib/papers/slides-avocs-04.pdf"},"keyword":["Petri nets","timed","automata"],"metadata":{"authorlinks":{}}},"bibtype":"article","biburl":"http://science.mq.edu.au/~fcassez/bib/franck-bib.bib","dataSources":["8742EsvjQfyP2fYBW","qbqYFWskmoonRB43F"],"keywords":["petri nets","timed","automata"],"search_terms":["structural","translation","time","petri","nets","timed","automata","cassez","roux"],"title":"Structural Translation from Time Petri Nets to Timed Automata","year":2005}