@INPROCEEDINGS{msr-03,
  AUTHOR = {Cassez, Franck and Roux, {Olivier H.}},
  BOOKTITLE = {4$\textit{\`eme}$ Colloque Francophone sur la Mod{\'e}lisation des Syst{\`e}mes R{\'e}actifs, (MSR'03)},
  urlpaper = {papers/ri-msr-03.pdf},
  TITLE = {{From Time Petri Nets to Timed Automata}},
  YEAR = {2003},
  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 or UPPAAL or CMC) to analyse TPNs.
},
  Type = {B - International Conferences}
}

{"_id":"W78hKhjTSBZykP6Ng","bibbaseid":"cassez-roux-fromtimepetrinetstotimedautomata-2003","author_short":["Cassez, F.","Roux, O."],"bibdata":{"bibtype":"inproceedings","type":"B - International Conferences","author":[{"propositions":[],"lastnames":["Cassez"],"firstnames":["Franck"],"suffixes":[]},{"propositions":[],"lastnames":["Roux"],"firstnames":["Olivier H."],"suffixes":[]}],"booktitle":"4$<i>ème</i>}$ Colloque Francophone sur la Modélisation des Systèmes Réactifs, (MSR'03)","urlpaper":"papers/ri-msr-03.pdf","title":"From Time Petri Nets to Timed Automata","year":"2003","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 or UPPAAL or CMC) to analyse TPNs. ","bibtex":"@INPROCEEDINGS{msr-03,\n AUTHOR = {Cassez, Franck and Roux, {Olivier H.}},\n BOOKTITLE = {4$\\textit{\\`eme}$ Colloque Francophone sur la Mod{\\'e}lisation des Syst{\\`e}mes R{\\'e}actifs, (MSR'03)},\n urlpaper = {papers/ri-msr-03.pdf},\n TITLE = {{From Time Petri Nets to Timed Automata}},\n YEAR = {2003},\n ABSTRACT = {\n In this paper, we consider Time Petri Nets (TPN) where time is\n associated with transitions. We give a formal semantics for TPNs in\n terms of Timed Transition Systems. Then, we propose a translation\n from TPNs to Timed Automata (TA) that preserves the behavioural\n semantics (timed bisimilarity) of the TPNs. For the theory of TPNs\n this result is two-fold: i) reachability problems and more generally\n TCTL model-checking are decidable for bounded TPNs; ii) allowing\n strict time constraints on transitions for TPNs preserves the\n results described in i). The practical applications of the\n translation are: i) one can specify a system using both TPNs and\n Timed Automata and a precise semantics is given to the composition;\n ii) one can use existing tools for analysing timed automata (like\n KRONOS or UPPAAL or CMC) to analyse TPNs.\n},\n Type = {B - International Conferences}\n}\n\n","author_short":["Cassez, F.","Roux, O."],"key":"msr-03","id":"msr-03","bibbaseid":"cassez-roux-fromtimepetrinetstotimedautomata-2003","role":"author","urls":{"Paper":"http://science.mq.edu.au/~fcassez/bib/papers/ri-msr-03.pdf"},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"http://science.mq.edu.au/~fcassez/bib/franck-bib.bib","dataSources":["8742EsvjQfyP2fYBW","qbqYFWskmoonRB43F","yYF8uwWqay28JyxZC"],"keywords":[],"search_terms":["time","petri","nets","timed","automata","cassez","roux"],"title":"From Time Petri Nets to Timed Automata","year":2003}