@inproceedings{GCH-atpn86,
  address = {Oxford, UK},
  year = 1987,
  volume = 266,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  editor = {Rozenberg, Grzegorz},
  acronym = {{APN}'86},
  booktitle = {{A}dvances in {P}etri {N}ets~1987, 
	       {S}elected {P}apers from the 7th
               {I}nternational {C}onference on
               {A}pplications and {T}heory of {P}etri {N}ets
               ({APN}'86)},
  author = {Girault, Claude and Chatelain, {\relax Ch}ristian and Haddad, Serge},
  title = {Specification and Properties of a Cache Coherence Protocol
                  Model},
  pages = {1-20}
}
@inproceedings{HG-atpn86,
  address = {Oxford, UK},
  year = 1987,
  volume = 266,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  editor = {Rozenberg, Grzegorz},
  acronym = {{APN}'86},
  booktitle = {{A}dvances in {P}etri {N}ets~1987, 
	       {S}elected {P}apers from the 7th
               {I}nternational {C}onference on
               {A}pplications and {T}heory of {P}etri {N}ets
               ({APN}'86)},
  author = {Haddad, Serge and Girault, Claude},
  title = {Algebraic Structure of Flows of a Regular Coloured Net},
  pages = {73-88}
}
@inproceedings{DH-pnpm89,
  address = {Kyoto, Japan},
  month = dec,
  year = 1989,
  publisher = {{IEEE} Computer Society Press},
  noeditor = {},
  acronym = {{PNPM}'89},
  booktitle = {{P}roceedings of the 3rd {I}nternational {W}orkshop on {P}etri
                  {N}ets and {P}erformance {M}odels ({PNPM}'89)},
  author = {Dutheillet, Claude and Haddad, Serge},
  title = {Aggregation of States in Colored Stochastic {P}etri Nets:
                  Application to a Multiprocessor Architecture},
  pages = {40-49}
}
@inproceedings{BMBH-atpn88,
  address = {Venice, Italy},
  month = jun,
  year = 1988,
  noeditor = {},
  acronym = {{APN}'88},
  booktitle = {{P}roceedings of the 9th
               {I}nternational {C}onference on
               {A}pplications and {T}heory of {P}etri {N}ets
               ({APN}'88)},
  author = {Bernard, Jean-Marc and Mounier, Jean-Luc and 
		  Beldiceanu, Nicolas and Haddad, Serge},
  title = {{AMI}: An Extensible {P}etri Nets Interactive Workshop},
  nopages = {}
}
@inproceedings{CH-atpn88,
  address = {Venice, Italy},
  month = jun,
  year = 1988,
  noeditor = {},
  acronym = {{APN}'88},
  booktitle = {{P}roceedings of the 9th
               {I}nternational {C}onference on
               {A}pplications and {T}heory of {P}etri {N}ets
               ({APN}'88)},
  author = {Couvreur, Jean-Michel and Haddad, Serge},
  title = {Towards a General and Powerful Computation of Flows for
                  Parameterized Coloured Nets},
  nopages = {}
}
@inproceedings{HC-pp88,
  address = {Pisa, Italy},
  month = apr,
  year = 1988,
  publisher = {North-Holland},
  editor = {Cosnard, Michel and Barton, Michael H. and Vanneschi, Marco},
  acronym = {{PP}'88},
  booktitle = {{P}roceedings of the {IFIP} {WG10.3} {W}orking {C}onference on 
		{P}arallel {P}rocessing ({PP}'88)},
  author = {Haddad, Serge and Couvreur, Jean-Michel},
  title = {Validation of Parallel Systems with Coloured {P}etri Nets},
  pages = {377-390}
}
@inproceedings{CHP-atpn91,
  address = {Gjern, Denmark},
  year = 1993,
  volume = 674,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  editor = {Rozenberg, Grzegorz},
  acronym = {{APN}'91},
  booktitle = {{P}apers from the 12th
               {I}nternational {C}onference on
               {A}pplications and {T}heory of {P}etri {N}ets
               ({APN}'91)},
  author = {Couvreur, Jean-Michel and Haddad, Serge and Peyre,
                  Jean-Fran{\c{c}}ois},
  title = {Generative Families of Positive Invariants in Coloured Nets
                  Sub-Classes},
  pages = {51-70}
}
@inproceedings{Had-atpn88,
  address = {Venice, Italy},
  year = 1990,
  volume = 424,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  editor = {Rozenberg, Grzegorz},
  acronym = {{APN}'88},
  booktitle = {{A}dvances in {P}etri {N}ets~1989, 
	       {P}apers from the 9th
               {I}nternational {C}onference on
               {A}pplications and {T}heory of {P}etri {N}ets
               ({APN}'88)},
  author = {Haddad, Serge},
  title = {A Reduction Theory for Coloured {P}etri Nets},
  pages = {209-235}
}
@inproceedings{DH-atpn89,
  address = {Bonn, Germany},
  year = 1991,
  volume = 483,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  editor = {Rozenberg, Grzegorz},
  acronym = {{APN}'89},
  booktitle = {{A}dvances in {P}etri {N}ets~1990, 
	       {P}apers from the 10th
               {I}nternational {C}onference on
               {A}pplications and {T}heory of {P}etri {N}ets
               ({APN}'89)},
  author = {Dutheillet, Claude and Haddad, Serge},
  title = {Regular Stochastic {P}etri Nets},
  pages = {186-209}
}
@incollection{CDFH-hlpn91,
  author = {Chiola, Giovanni and Dutheillet, Claude and Franceschinis,
                  Giuliana and Haddad, Serge},
  title = {Stochastic Well-Formed Coloured Nets and
                  Multiprocessor Modelling Applications},
  booktitle = {High-Level {P}etri Nets~-- Theory and Application},
  editor = {Jensen, Kurt and Rozenberg, Grzegorz},
  publisher = {Springer},
  year = 1991,
  pages = {504-530},
  isbn = {3-540-54125-x}
}
@incollection{CDFH2-hlpn91,
  author = {Chiola, Giovanni and Dutheillet, Claude and Franceschinis,
                  Giuliana and Haddad, Serge},
  title = {On Well-Formed Coloured Nets and their Symbolic Reachability Graph},
  booktitle = {High-Level {P}etri Nets~-- Theory and Application},
  editor = {Jensen, Kurt and Rozenberg, Grzegorz},
  publisher = {Springer},
  year = 1991,
  pages = {373-396},
  isbn = {3-540-54125-x}
}
@inproceedings{THS-pdces91,
  address = {Corfu, Greece},
  month = jun,
  year = 1991,
  publisher = {North-Holland},
  editor = {Tzafestas, Spyros G. and Borne, Pierre and Grandinetti, Lucio },
  acronym = {{PDCES}'91},
  booktitle = {{P}roceedings of the {IMACS-IFAC} {I}nternational {S}ymposium on
	   {P}arallel and {D}istributed {C}omputing in {E}ngineering {S}ystems
	   ({PDCES}'91)},
  author = {Taghelit, Mohamed and Haddad, Serge and Sens, Pierre},
  title = {An Algorithm Providing Fault-Tolerance for Layered
                  Distributed Systems},
  nopages = {}
}
@inproceedings{DH-iscis92,
  address = {Antalya, Turkey},
  month = nov,
  year = 1992,
  publisher = {},
  noeditor = {},
  acronym = {{ISCIS}'92},
  booktitle = {{P}roceedings of the 7th {I}nternational {S}ymposium
           on {C}omputer and {I}nformation {S}cience ({ISCIS}'92)},
  author = {Dutheillet, Claude and Haddad, Serge},
  title = {An Efficient Computation of Structural Relations in Unary
                  Regular Nets},
  pages = {73-79}
}
@article{CDFH-toc93,
  publisher = {{IEEE} Computer Society Press},
  journal = {IEEE Transactions on Computers},
  author = {Chiola, Giovanni and Dutheillet, Claude and Franceschinis,
                  Giuliana and Haddad, Serge},
  title = {Stochastic Well-Formed Colored Nets and Symmetric Modeling Applications},
  volume = 42,
  number = 11,
  pages = {1343-1360},
  month = nov,
  year = 1993,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CDFH-toc93.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CDFH-toc93.ps}
}
@inproceedings{DH-pnpm93,
  address = {Toulouse, France},
  month = oct,
  year = 1993,
  publisher = {{IEEE} Computer Society Press},
  noeditor = {},
  acronym = {{PNPM}'93},
  booktitle = {{P}roceedings of the 5th {I}nternational {W}orkshop on {P}etri
                  {N}ets and {P}erformance {M}odels ({PNPM}'93)},
  author = {Dutheillet, Claude and Haddad, Serge},
  title = {Conflict Sets in Coloured {P}etri Nets},
  pages = {76-87},
  doi = {10.1109/PNPM.1993.393433}
}
@inproceedings{EH-dds93,
  address = {Palma de Mallorca, Spain},
  month = sep,
  year = 1993,
  volume = {A-39},
  series = {IFIP Transactions},
  publisher = {North-Holland},
  editor = {Cosnard, Michel and Puigjaner, Ram{\'o}n},
  acronym = {{DDS}'93},
  booktitle = {{P}roceedings of the {IFIP} {WG10.3} {I}nternational {C}onference
                  on {D}ecentralized and {D}istributed {S}ystems ({DDS}'93)},
  author = {Ezpeleta, Joaquin and Haddad, Serge},
  title = {A Distributed Algorithm for Resource Management},
  pages = {61-72}
}
@inproceedings{ZHT-dds93,
  address = {Palma de Mallorca, Spain},
  month = sep,
  year = 1993,
  volume = {A-39},
  series = {IFIP Transactions},
  publisher = {North-Holland},
  editor = {Cosnard, Michel and Puigjaner, Ram{\'o}n},
  acronym = {{DDS}'93},
  booktitle = {{P}roceedings of the {IFIP} {WG10.3} {I}nternational {C}onference
                  on {D}ecentralized and {D}istributed {S}ystems ({DDS}'93)},
  author = {Zouari, Belhassen and Haddad, Serge and Taghelit, Mohamed},
  title = {A Protocol Specification Language with a High-Level {P}etri Net Semantics},
  pages = {225-241}
}
@inproceedings{BDH-atpn93,
  address = {Chicago, Illinois, USA},
  month = jun,
  year = 1993,
  volume = 691,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  editor = {Marsan, Marco Ajmone},
  acronym = {{APN}'92},
  booktitle = {{P}roceedings of the 13th
               {I}nternational {C}onference on
               {A}pplications and {T}heory of {P}etri {N}ets
               ({APN}'92)},
  author = {Barkaoui, Kamel and Dutheillet, Claude and Haddad, Serge},
  title = {An Efficient Algorithm for Finding Structural Deadlocks in
                  Colored {P}etri Nets},
  pages = {69-88}
}
@inproceedings{HTZ-pstv93,
  address = {Li{\`e}ge, Belgium},
  month = may,
  year = 1993,
  volume = {C-16},
  series = {IFIP Transactions},
  publisher = {North-Holland},
  editor = {Danthine, Andr{\'e} A. S. and Leduc, Guy and Wolper, Pierre},
  acronym = {{PSTV}'93},
  booktitle = {{P}roceedings of the {IFIP} {WG}6.1 
               13th {I}nternational {C}onference on {P}rotocol 
               {S}pecification, {T}esting and {V}erification
               ({PSTV}'93)},
  author = {Haddad, Serge and Taghelit, Mohamed and Zouari, Belhassen},
  title = {Assessment of {ESTELLE} and {EDT} Through Real Case Studies},
  pages = {223-238}
}
@inproceedings{HM-pnpm95,
  address = {Durham, North Carolina, USA},
  month = oct,
  year = 1995,
  publisher = {{IEEE} Computer Society Press},
  noeditor = {},
  acronym = {{PNPM}'95},
  booktitle = {{P}roceedings of the 6th {I}nternational {W}orkshop on {P}etri
                  {N}ets and {P}erformance {M}odels ({PNPM}'95)},
  author = {Haddad, Serge and Moreaux, Patrice},
  title = {Evaluation of High-Level {P}etri Nets by Means of Aggregation
                  and Decomposition},
  pages = {11-20},
  doi = {10.1109/PNPM.1995.524311}
}
@inproceedings{HITZ-atpn95,
  address = {Turin, Italy},
  month = jun,
  year = 1995,
  volume = 935,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {De Michelis, Giorgio and Diaz, Michel},
  acronym = {{APN}'95},
  booktitle = {{P}roceedings of the 16th
               {I}nternational {C}onference on
               {A}pplications and {T}heory of {P}etri {N}ets
               ({APN}'95)},
  author = {Haddad, Serge and Ili{\'e}, Jean-Michel and Taghelit, Mohamed
                  and Zouari, Belhassen},
  title = {Symbolic Reachability Graph and Partial Symmetries},
  pages = {238-251}
}
@inproceedings{EFH-maamaw96,
  address = {Eindhoven, The Netherlands},
  month = jan,
  year = 1996,
  volume = 1038,
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer},
  editor = {Van de Velde, Walter and Perram, John W.},
  acronym = {{MAAMAW}'96},
  booktitle = {{P}roceedings of the 7th {E}uropean {W}orkshop on {M}odelling
                  {A}utonomous {A}gents in a {M}ulti-{A}gent {W}orld ({MAAMAW}'96)},
  author = {El~Fallah Seghrouchni, Amal and Haddad, Serge},
  title = {A Coordination Algorithm for Multi-Agent Planning},
  pages = {86-99}
}
@inproceedings{EFH-icmas96,
  address = {Kyoto, Japan},
  month = dec,
  year = 1996,
  publisher = {AAAI Press},
  editor = {Tokoro, Mario},
  acronym = {{ICMAS}'96},
  booktitle = {Proceedings of the 2nd {I}nternational {C}onference on
	   {M}ulti-{A}gent {S}ystems ({ICMAS}'96)},
  author = {El~Fallah Seghrouchni, Amal and Haddad, Serge},
  title = {A Recursive Model for Distributed Planning},
  pages = {307-314}
}
@inproceedings{HM-icatpn1996,
  address = {Osaka, Japan},
  month = jun,
  year = 1996,
  volume = 1091,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Billington, Jonathan and Reisig, Wolfgang},
  acronym = {{APN}'96},
  booktitle = {{P}roceedings of the 17th
               {I}nternational {C}onference on
               {A}pplications and {T}heory of {P}etri {N}ets
               ({APN}'96)},
  author = {Haddad, Serge and Moreaux, Patrice},
  title = {Asynchronous Composition of High Level {P}etri Nets: A
                  Quantitative Approach},
  pages = {192-211}
}
@article{CDFH-tcs97,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Chiola, Giovanni and Dutheillet, Claude and Franceschinis,
                  Giuliana and Haddad, Serge},
  title = {A Symbolic Reachability Graph for Coloured {P}etri Nets},
  volume = 176,
  number = {1-2},
  pages = {39-65},
  month = apr,
  year = 1997,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDFH-tcs97.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CDFH-tcs97.ps},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDFH-tcs97.pdf},
  psg = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PSGZ/CDFH-tcs97.ps.gz},
  doi = {10.1016/S0304-3975(96)00010-2}
}
@inproceedings{HMC-atpn97,
  address = {Toulouse, France},
  month = jun,
  year = 1997,
  volume = 1248,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Az{\'e}ma, Pierre and Balbo, Gianfranco},
  acronym = {{ICATPN}'97},
  booktitle = {{P}roceedings of the 18th
               {I}nternational {C}onference on
               {A}pplications and {T}heory of {P}etri {N}ets
               ({ICATPN}'97)},
  author = {Haddad, Serge and Moreaux, Patrice and Chiola, Giovanni},
  title = {Efficient Handling of Phase-Type Distributions in Generalized
                  Stochastic {P}etri Nets},
  pages = {175-194}
}
@inproceedings{DHM-cpe98,
  address = {Palma de Mallorca, Spain},
  month = sep,
  year = 1998,
  volume = 1469,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Puigjaner, Ram{\'o}n and Savino, Nunzio N. and Serra, Bartomeu},
  acronym = {{TOOLS}'98},
  booktitle = {{P}roceedings of the 10th {I}nternational {C}onference on
                  {C}omputer {P}erformance {E}valuation ({TOOLS}'98)},
  author = {Donatelli, Susanna and Haddad, Serge and Moreaux, Patrice},
  title = {Structured Characterization of the Markov Chain of
                  Phase-Type~{SPN}},
  pages = {243-254}
}
@inproceedings{AHI-tacas98,
  address = {Lisbon, Portugal},
  month = mar # {-} # apr,
  year = 1998,
  volume = 1384,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Steffen, Bernhard},
  acronym = {{TACAS}'98},
  booktitle = {{P}roceedings of the 4th {I}nternational 
               {C}onference on {T}ools and {A}lgorithms for
               {C}onstruction and {A}nalysis of {S}ystems
               ({TACAS}'98)},
  author = {Ajami, Khalil and Haddad, Serge and Ili{\'e}, Jean-Michel},
  title = {Exploiting Symmetry in Linear Time Temporal Logic Model
                  Checking: One Step Beyond},
  pages = {52-67}
}
@techreport{SP-LIP6-1999,
  author = {Haddad, Serge and Poitrenaud, Denis},
  title = {Decidability and Undecidability Results for Recursive Petri Nets},
  type = {Report},
  number = {LIP6-019},
  year = {1999},
  month = sep,
  institution = {Laboratoire de l'Informatique de Paris~VI, 
               Universit\'e Pierre-et-Marie-Curie, France},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SP-LIP6-1999.pdf},
  abstract = {Recursive Petri nets (RPNs) have been introduced to model systems with dynamic structure.
 Whereas this model is a strict extension of Petri nets, reachability in RPNs remains decidable.
Here we focus on three complementary theoretical aspects.
At first, we develop decision procedures for new properties like boundedness and finiteness and we show that languages of RPNs are recursive.
Then we study the expressiveness of RPNs proving that any recursively enumerable language may be obtained as the image by an homomorphism of the intersection of a regular language and a RPN language.
Starting from this property, we deduce undecidability results including undecidablity for the kind of model checking which is decidable for Petri nets.
At last, we compare RPNs with two other models combining Petri nets and context-free grammars features showing that these models can be simulated by RPNs.}
}
@inproceedings{DHMS-nsmc99,
  address = {Zaragoza, Spain},
  month = sep,
  year = 1999,
  noeditor = {},
  acronym = {{NSMC}'99},
  booktitle = {{P}roceedings of the 3rd {I}nternational {M}eeting on the
                  {N}umerical {S}olution of {M}arkov {C}hain ({NSMC}'99)},
  author = {Donatelli, Susanna and Haddad, Serge and Moreaux, Patrice and
                  Sene, Mbaye},
  title = {Bounds for Renewal of Systems with Client{\slash}Server
                  Interaction},
  pages = {208-227}
}
@inproceedings{NH-pdcs99,
  address = {Fort Lauderdale, Florida, USA},
  month = aug,
  year = 1999,
  publisher = {International Society for Computers and their Applications},
  editor = {Olariu, Stephan and Wu, Jie},
  acronym = {{PDCS}'99},
  booktitle = {{P}roceedings of the {ISCA} 17th {I}nternational {C}onference on
	   {P}arallel and {D}istributed {C}omputing {S}ystems
	   ({PDCS}'99)},
  author = {Nguilla{ }Kooh, Fran{\c{c}}ois and Haddad, Serge},
  title = {Reaching Agreement in Hierarchical Groups},
  nopages = {}
}
@inproceedings{EFHM-maamaw99,
  address = {Valencia, Spain},
  month = jun # {-} # jul,
  year = 1999,
  volume = 1647,
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer},
  editor = {Garijo, Francisco J. and Boman, Magnus},
  acronym = {{MAAMAW}'99},
  booktitle = {{P}roceedings of the 9th {E}uropean {W}orkshop on {M}odelling
                  {A}utonomous {A}gents in a {M}ulti-{A}gent {W}orld ({MAAMAW}'99)},
  author = {El~Fallah Seghrouchni, Amal and Haddad, Serge and Mazouzi,
                  Hamza},
  title = {Protocol Engineering for Multi-agent Interaction},
  pages = {89-101},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/EFHM-maamaw99.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/EFHM-maamaw99.ps}
}
@inproceedings{HP-icatpn99,
  address = {Williamsburg, Virginia, USA},
  month = jun,
  year = 1999,
  volume = 1639,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Donatelli, Susanna and Kleijn, H. C. M.},
  acronym = {{ICATPN}'99},
  booktitle = {{P}roceedings of the 20th
               {I}nternational {C}onference on
               {A}pplications and {T}heory of {P}etri {N}ets
               ({ICATPN}'99)},
  author = {Haddad, Serge and Poitrenaud, Denis},
  title = {Theoretical Aspects of Recursive {P}etri Nets},
  pages = {228-247},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/HP-icatpn99.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/HP-icatpn99.ps}
}
@inproceedings{EFHM-cata99,
  address = {Cancun, Mexico},
  month = apr,
  year = 1999,
  publisher = {International Society for Computers and Their Applications},
  editor = {Lee, Roger Y.},
  acronym = {{CATA}'99},
  booktitle = {{P}roceedings of the {ISCA} 14th {I}nternational {C}onference on
                  {C}omputers and {T}heir {A}pplications ({CATA}'99)},
  author = {El~Fallah Seghrouchni, Amal and Haddad, Serge and Mazouzi,
                  Hamza},
  title = {A Formal Study of Interactions in Multi-Agent Systems},
  pages = {240-245}
}
@inproceedings{HN-cata99,
  address = {Cancun, Mexico},
  month = apr,
  year = 1999,
  publisher = {International Society for Computers and Their Applications},
  editor = {Lee, Roger Y.},
  acronym = {{CATA}'99},
  booktitle = {{P}roceedings of the {ISCA} 14th {I}nternational {C}onference on
                  {C}omputers and {T}heir {A}pplications ({CATA}'99)},
  author = {Haddad, Serge and Nguilla{ }Kooh, Fran{\c{c}}ois},
  title = {Combining different failure detectors for solving a
                  large-scale consensus problem},
  pages = {204-209}
}
@techreport{SP-LIP6-2000,
  author = {Haddad, Serge and Poitrenaud, Denis},
  title = {A Model Checking Decision Procedure for Sequential Recursive Petri Nets},
  type = {Report},
  number = {LIP6-024},
  year = {2000},
  month = sep,
  institution = {Laboratoire de l'Informatique de Paris~VI, 
               Universit\'e Pierre-et-Marie-Curie, France},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SP-LIP6-2000.pdf},
  abstract = {Recursive Petri nets (RPNs) have been introduced to model systems
with dynamic structure. Whereas this model is a strict extension
of Petri nets and context-free grammars (w.r.t. the language
criterion), reachability in RPNs remains decidable. However the
kind of model checking which is decidable for Petri nets becomes
undecidable for RPNs. In this work, we introduce a submodel of
RPNs called sequential recursive Petri nets (SRPNs) and we study
its theoretical features. First we show that we can decide whether
a RPN is a sequential one. Then, we analyze the language aspects
proving that the SRPN languages still strictly include the union
of Petri nets and context-free languages. Moreover the family of
languages of SRPNs is closed under intersection with regular
languages (unlike the one of RPNs). This property is the starting
point for the model checking of the action-based linear time logic
which is also shown to be decidable. To the best of our knowledge,
this is the first time such a result is obtained for a model
strictly including  Petri nets and context-free grammars.}
}
@inproceedings{HIA-forte00,
  address = {Pisa, Italy},
  month = oct,
  year = 2000,
  volume = 183,
  series = {{IFIP} Conference Proceedings},
  publisher = {Kluwer Academic Publishers},
  editor = {Bolognesi, Tommaso and Latella, Diego },
  acronym = {{FORTE'XIII}/{PSTV'XX}},
  booktitle = {{P}roceedings of {IFIP} {TC6} {WG6.1} {J}oint
               {I}nternational {C}onference on {F}ormal {D}escription
               {T}echniques for {D}istributed {S}ystems and 
               {C}ommunication {P}rotocols ({FORTE'XIII}) and 
               {P}rotocol {S}pecification, {T}esting and
               {V}erification ({PSTV'XX})},
  author = {Haddad, Serge and Ili{\'e}, Jean-Michel and
		 Ajami, Khalil},
  title = {A Model Checking Method for Partially Symmetric Systems},
  pages = {121-136},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/HIA-forte00.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/HIA-forte00.ps}
}
@inproceedings{HP-wodes00,
  address = {Ghent, Belgium},
  month = aug,
  year = 2000,
  publisher = {Kluwer Academic Publishers},
  editor = {Boel, Ren{\'e} and Stremersch, Geert},
  acronym = {{WODES}'00},
  booktitle = {{P}roceedings of the 5th {W}orkshop on {D}iscrete {E}vent {S}ystems
	   ({WODES}'00)},
  author = {Haddad, Serge and Poitrenaud, Denis},
  title = {Modelling and Analyzing Systems with Recursive {P}etri Nets},
  pages = {449-458},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/HP-wodes00.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/HP-wodes00.ps}
}
@article{EFHM-ijca01,
  publisher = {International Society for Computers and their Applications},
  journal = {International Journal of Computers \& their Applications},
  author = {El~Fallah Seghrouchni, Amal and Haddad, Serge and Mazouzi,
                  Hamza},
  title = {A Formal Study of Interactions in Multi-Agent Systems},
  volume = 8,
  number = 1,
  month = mar,
  year = 2001,
  pages = {23-32},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EFHM-ijca01.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EFHM-ijca01.pdf},
  abstract = {This paper presents an original approach to model, analyze,
                  and design interactions in multi-agent systems. It combines
                  two complementary paradigms: observation in distributed
                  systems and interaction in multi-agent systems. The rst
                  paradigm is frequently used to observe concurrent activities
                  in distributed systems through the causal dependency of
                  events. The second paradigm aims to identify
                  interaction-oriented designs and describes them with a
                  formalism enabling to prove their quality. Our approach is
                  based on distributed observation of events inherent to
                  agents' interactions, which may explain relationships within
                  conversations, or group utterances in order to improve
                  agent's behavior.}
}
@inproceedings{HMSS-atpn01,
  address = {Newcastle upon Tyne, UK},
  month = jun,
  year = 2001,
  volume = 2075,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Colom, Jos{\'e} Manuel and Koutny, Maciej},
  acronym = {{ICATPN}'01},
  booktitle = {{P}roceedings of the 22nd
               {I}nternational {C}onference on
               {A}pplications and {T}heory of {P}etri {N}ets
               ({ICATPN}'01)},
  author = {Haddad, Serge and Moreaux, Patrice and Sereno, Matteo and
                  Silva, Manuel},
  title = {Structural Characterization and Qualitative Properties of
                  Product Form Stochastic {P}etri Nets},
  pages = {164-183},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HMSS-atpn01.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HMSS-atpn01.pdf},
  abstract = {The model of Stochastic Petri nets (SPN) with a product form
                  solution (\(\Pi\)-net) is a class of nets for which there is an
                  analytic expression of the steady state probabilities w.r.t.
                  markings, as for product form queueing networks w.r.t. queue
                  lengths. In this paper, we prove new important properties of
                  this kind of nets. First we provide a polynomial time
                  (w.r.t. the size of the net structure) algorithm to check
                  whether a SPN is a \(\Pi\)-net. Then, we give a purely structural
                  characterization of SPN for which a product form solution
                  exists regardless the particular values of probabilistic
                  parameters of the SPN. We call such
                  nets~\(\overline{\Pi}\)-nets. We also present untimed
                  properties of \(\Pi\)-nets and \(\overline{\Pi}\)-nets such
                  like liveness, reachability, deadlock freeness and
                  characterization of reachable markings. The complexity of
                  the reachability and the liveness problems is also addressed
                  for \(\Pi\)-nets and \(\overline{\Pi}\)-nets. These results
                  complement previous studies on these classes of nets and
                  improve the applicability of Product Form solutions.}
}
@inproceedings{HP-time01,
  address = {Cividale del Friuli, Italy},
  month = jun,
  year = 2001,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{TIME}'01},
  booktitle = {{P}roceedings of the 8th {I}nternational {S}ymposium on
               {T}emporal {R}epresentation and {R}easoning
               ({TIME}'01)},
  author = {Haddad, Serge and Poitrenaud, Denis},
  title = {Checking Linear Temporal Formulas on Sequential Recursive
                  {P}etri Nets},
  pages = {198-205},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HP-time01.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HP-time01.pdf},
  abstract = { Recursive Petri nets (RPNs) have been introduced to model
    systems with dynamic structure. Whereas this model is a strict extension
    of Petri nets and context-free grammars (w.r.t. the language criterion),
    reachability in RPNs remains decidable. However the kind of model checking
    which is decidable for Petri nets becomes undecidable for RPNs. In this
    work, we introduce a submodel of RPNs called sequential recursive Petri
    nets (SRPNs) and we study the model checking of the action-based linear
    time logic on SRPNs. We prove that it is decidable for all its variants:
    finite sequences, finite maximal sequences, infinite sequences and
    divergent sequences. At the end, we analyze language aspects proving that
    the SRPN languages still strictly include the union of Petri nets and
    context-free languages and that the family of languages of SRPNs is closed
    under intersection with regular languages (unlike the one of RPNs).}
}
@incollection{HV-rpmf01,
  author = {Haddad, Serge and Vernadat, Fran{\c{c}}ois},
  title = {M{\'e}thodes d'analyse des r{\'e}seaux de Petri},
  booktitle = {Les r{\'e}seaux de {P}etri~--- Mod{\`e}les fondamentaux},
  chapter = 3,
  editor = {Michel Diaz},
  publisher = {Herm{\`e}s},
  year = 2001,
  month = may,
  pages = {69-117},
  url = {http://www.lavoisier.fr/notice/fr2746202500.html},
  isbn = {2-7462-0250-0}
}
@incollection{Had-rpmf01,
  author = {Haddad, Serge},
  title = {D{\'e}cidabilit{\'e} et complexit{\'e} des probl{\`e}mes de
		 r{\'e}seaux de Petri},
  booktitle = {Les r{\'e}seaux de {P}etri~--- Mod{\`e}les fondamentaux},
  chapter = 4,
  editor = {Michel Diaz},
  publisher = {Herm{\`e}s},
  year = 2001,
  month = may,
  pages = {119-158},
  url = {http://www.lavoisier.fr/notice/fr2746202500.html},
  isbn = {2-7462-0250-0}
}
@incollection{HM-rpmf01,
  author = {Haddad, Serge and Moreaux, Patrice},
  title = {Les r{\'e}seaux de Petri stochastiques},
  booktitle = {Les r{\'e}seaux de {P}etri~--- Mod{\`e}les fondamentaux},
  chapter = 9,
  editor = {Michel Diaz},
  publisher = {Herm{\`e}s},
  year = 2001,
  month = may,
  pages = {299-334},
  url = {http://www.lavoisier.fr/notice/fr2746202500.html},
  isbn = {2-7462-0250-0}
}
@incollection{HM2-rpmf01,
  author = {Haddad, Serge and Moreaux, Patrice},
  title = {Les r{\'e}seaux de Petri stochastiques bien form{\'e}s},
  booktitle = {Les r{\'e}seaux de {P}etri~--- Mod{\`e}les fondamentaux},
  chapter = 10,
  editor = {Michel Diaz},
  publisher = {Herm{\`e}s},
  year = 2001,
  month = may,
  pages = {335-353},
  url = {http://www.lavoisier.fr/notice/fr2746202500.html},
  isbn = {2-7462-0250-0}
}
@incollection{HM3-rpmf01,
  author = {Haddad, Serge and Moreaux, Patrice},
  title = {M{\'e}thodes tensorielles et r{\'e}seaux de Petri stochastiques},
  booktitle = {Les r{\'e}seaux de {P}etri~--- Mod{\`e}les fondamentaux},
  chapter = 11,
  editor = {Michel Diaz},
  publisher = {Herm{\`e}s},
  year = 2001,
  month = may,
  pages = {335-353},
  url = {http://www.lavoisier.fr/notice/fr2746202500.html},
  isbn = {2-7462-0250-0}
}
@incollection{Haddad-pnse03,
  author = {Haddad, Serge},
  title = {Issues in Verification},
  booktitle = {Petri Nets for Systems Engineering: A Guide to Modeling,
                  Verification and Applications},
  editor = {Girault, Claude and Valk, R{\"u}diger},
  publisher = {Springer},
  year = 2003,
  pages = {183-200},
  chapter = 13,
  url = {http://www.springer.com/978-3-540-41217-5},
  isbn = {978-3-540-41217-5}
}
@incollection{CTSH-pnse03,
  author = {Colom, Jos{\'e}-Manuel and Teruel, Enrique and Silva, Manuel
                  and Haddad, Serge},
  title = {Structural Methods},
  booktitle = {Petri Nets for Systems Engineering: A Guide to Modeling,
                  Verification and Applications},
  editor = {Girault, Claude and Valk, R{\"u}diger},
  publisher = {Springer},
  year = 2003,
  pages = {277-316},
  chapter = 15,
  url = {http://www.springer.com/978-3-540-41217-5},
  isbn = {978-3-540-41217-5}
}
@inproceedings{KHI-smc02,
  address = {Hammamet, Tunisia},
  month = oct,
  year = 2002,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{SMC}'02},
  booktitle = {{P}roceedings of the {IEEE} {I}nternational
               {C}onference on {S}ystems, {M}an and {C}ybernetics
               ({SMC}'02)},
  author = {Klai, Kais and Haddad, Serge and Ili{\'e}, Jean-Michel},
  title = {An Incremental Verification Technique using Decomposition of
                  {P}etri Nets},
  pages = {381-386},
  lsdate-new = 20080901,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KHI-smc02.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KHI-smc02.pdf},
  abstract = {We~propose a modular verification technique for bounded Petri
    nets which efficiency relies on both behavioral and structural features. By
    focusing on linear evenemential temporal logic formula, we demonstrate how to
    choose a subnet on which it is enough to perform the model checking.}
}
@inproceedings{MEFH-aamas02,
  address = {Bologna, Italy},
  month = jul,
  year = 2002,
  publisher = {ACM Press},
  acronym = {{AAMAS}'02},
  booktitle = {{P}roceedings of the 1st {I}nternational {J}oint {C}onference on
                  {A}utonomous {A}gents and {M}ulti-{A}gent {S}ystems
		  ({AAMAS}'02)},
  author = {Mazouzi, Hamza and El~Fallah Seghrouchni, Amal and Haddad,
                  Serge},
  title = {Open Protocol Design for Complex Interaction in Multi-Agent Systems},
  pages = {15-19},
  lsdate-new = 20080901,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MEFH-aamas02.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MEFH-aamas02.ps}
}
@inproceedings{HH-aiccsa2003,
  address = {Tunis, Tunisia},
  month = jul,
  year = 2003,
  publisher = {{IEEE} Computer Society Press},
  editor = {Zomaya, Albert Y.},
  acronym = {{AICCSA}'03},
  booktitle = {{P}roceedings of the 2nd {ACS}/{IEEE} {I}nternational {C}onference 
           on {C}omputer {S}ystems and {A}pplications ({AICCSA}'03)},
  author = {El~Haddad, Joyce and Haddad, Serge},
  title = {Self-stabilizing Scheduling Algorithm for Cooperating Robots},
  pages = {128},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HH-aiccsa03.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HH-aiccsa03.pdf},
  doi = {10.1109/AICCSA.2003.1227560},
  abstract = {We address the problem of autonomous robots which alternate
                  between execution of individual tasks and peer-to-peer
                  communication. Each robot keeps in its permanent memory a
                  set of locations where it can meet some of the other robots.
                  The proposed self-stabilizing algorithm solves the
                  management of visits to these locations ensuring that after
                  the stabilizing phase, every visit to a location will lead
                  to a communication. We model the untimed behaviour of a
                  robot by a Petri net and the timed behaviour by an
                  (infinite) discrete time Markov chain. Theoretical results
                  in this area are then combined in order to establish the
                  proof of the algorithm.}
}
@inproceedings{HH-msr03,
  address = {Metz, France},
  month = oct,
  year = 2003,
  publisher = {Herm{\`e}s},
  editor = {M{\'e}ry, Dominique and Rezg, Nidhal and
            Xie, Xiaolan},
  acronym = {{MSR}'03},
  booktitle = {{A}ctes du 4{\`e}me {C}olloque sur la 
               {M}od{\'e}lisation des {S}yst{\`e}mes
               {R}{\'e}actifs
               ({MSR}'03)},
  author = {El~Haddad, Joyce and Haddad, Serge},
  title = {Algorithmes de communication auto-stabilisants dans un
                  syst{\`e}me de robots mobiles},
  pages = {277-292},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HH-msr03.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HH-msr03.pdf},
  abstract = {This paper deals with communication in autonomous multi-robots
    system. We~propose a self-stabilizing scheduling algorithm that solves the
    management of visits to the locations ensuring that after stabilization
    phase, every visit will lead to a communication. Next, we present a second
    self-stabilizing algorithm, based on the above one, computing the
    shortest-path for all-pairs of locations.}
}
@inproceedings{MH-wsws03,
  address = {Pittsburgh, Pennsylvania, USA},
  month = sep,
  year = 2003,
  acronym = {{SWSEE}'03},
  booktitle = {{P}roceedings of the {W}orkshop on {S}emantic {W}eb {S}ervices
		for {E}ntreprise {A}pplication {I}ntegration and
                  {E}-{C}ommerce ({SWSEE}'03)},
  author = {Melliti, Tarek and Haddad, Serge},
  title = {Synthesis of Agents for Web Services Interaction},
  nopages = {},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MH-wsws03.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MH-wsws03.pdf},
  abstract = {With the development of the semantic Web, the specification of
    Web services has evolved from a {"}remote procedure call{"} style to a
    behavioral description including standard constructors of programming
    languages. Such a transformation introduces new problems since traditional
    clients will not be able to interact with these sophisticated services.
    In~this work, we develop a generic agent capable to fully control the
    interaction process with a Web service given its XLANG behavioral
    description (XLANG being one of these languages). At~first, we give an
    operational semantic to XLANG in terms of timed transition systems. Then
    we define a relation between two communicating systems which formalizes
    the concept of a correct interaction. Finally we propose an algorithm
    which either detects ambiguity of the Web service or generates a timed
    deterministic automaton which controls the agent behavior during the
    interaction with the service.}
}
@incollection{HV-vmorp03,
  author = {Haddad, Serge and Vernadat, Fran{\c{c}}ois},
  title = {V{\'e}rification de propri{\'e}t{\'e}s sp{\'e}cifiques},
  booktitle = {V{\'e}rification et mise en {\oe}uvre des r{\'e}seaux de {P}etri},
  chapter = 1,
  editor = {Michel Diaz},
  publisher = {Herm{\`e}s},
  year = 2003,
  month = jan,
  pages = {31-97},
  url = {http://www.lavoisier.fr/notice/fr2746204450.html},
  isbn = {2-7462-0445-2}
}
@incollection{HI-vmorp03,
  author = {Haddad, Serge and Ili{\'e}, Jean-Michel},
  title = {Sym{\'e}tries et logiques temporelles},
  booktitle = {V{\'e}rification et mise en {\oe}uvre des r{\'e}seaux de {P}etri},
  chapter = 4,
  editor = {Michel Diaz},
  publisher = {Herm{\`e}s},
  year = 2003,
  month = jan,
  pages = {163-187},
  url = {http://www.lavoisier.fr/notice/fr2746204450.html},
  isbn = {2-7462-0445-2}
}
@article{HH-ijpr04,
  publisher = {Taylor \& Francis},
  journal = {International Journal of Production Research},
  author = {El~Haddad, Joyce and Haddad, Serge},
  title = {A Fault-tolerant Communication Mechanism for Cooperative
                  Robots},
  volume = 42,
  number = 14,
  pages = {2793-2808},
  year = 2004,
  month = jul,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HH-ijpr04.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HH-ijpr04.pdf},
  doi = {10.1080/00207540410001705185},
  abstract = {Operations in unpredictable environments require coordinating
    teams of robots. This coordination implies peer-to-peer communication
    between the team's robots, resource allocation, and coordination. We
    address the problem of autonomous robots which alternate between execution
    of individual tasks and peer-to-peer communication. Each robot keeps in
    its permanent memory a set of locations where it can meet some of the
    other robots. The proposed protocol is constructed by two layered modules
    (sub-algorithms: a self-stabilizing scheduling and a construction of a
    minimum-hop path forest). The first self-stabilizing algorithm solves the
    management of visits to these locations ensuring that, after the
    stabilizing phase, every visit to a location will lead to a communication.
    We model the untimed behaviour of a robot by a Petri net and the timed
    behaviour by an (infinite) Discrete Time Markov Chain. Theoretical results
    in this area are then combined in order to establish the proof of the
    algorithm. The second self-stabilizing algorithm computes the minimum-hop
    path between a specific robot's location and the locations of all the
    other robots of the system in order to implement routing.}
}
@inproceedings{HIK-atva04,
  address = {Taipei, Taiwan},
  month = oct # {-} # nov,
  year = {2004},
  volume = {3299},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Wang, Farn},
  acronym = {{ATVA}'04},
  booktitle = {{P}roceedings of the 2nd {I}nternational
               {S}ymposium on {A}utomated {T}echnology
               for {V}erification and {A}nalysis
               ({ATVA}'04)},
  author = {Haddad, Serge and Ili{\'e}, Jean-Michel and Klai, Kais},
  title = {Design and Evaluation of a Symbolic and Abstraction-based
                  Model Checker},
  pages = {196-210},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HIK-atva04.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HIK-atva04.pdf},
  abstract = {Symbolic model-checking usually includes two steps: the building
     of a compact representation of a state graph and the evaluation of the
     properties of the system upon this data structure. In case of properties
     expressed with a linear time logic, it appears that the second step is
     often more time consuming than the first one. In this work, we present a
     mixed solution which builds an observation graph represented in a non
     symbolic way but where the nodes are essentially symbolic set of states.
     Due to the small number of events to be observed in a typical formula,
     this graph has a very moderate size and thus the complexity time of
     verification is neglectible w.r.t. the time to build the observation
     graph. Thus we propose different symbolic implementations for the
     construction of the nodes of this graph. The evaluations we have done on
     standard examples show that our method outperforms the pure symbolic
     methods which makes it attractive.}
}
@inproceedings{HM-mascots04,
  address = {Volendam, The Netherlands},
  month = oct,
  year = 2004,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{MASCOTS}'04},
  booktitle = {{P}roceedings of the 12th {IEEE} {I}nternational {S}ymposium
	   on {M}odeling, {A}nalysis, and {S}imulation of {C}omputer and
                  {T}elecommunication {S}ystems ({MASCOTS}'04)},
  author = {Haddad, Serge and Moreaux, Patrice},
  title = {Approximate Analysis of Non-{M}arkovian Stochastic Systems
                  with Multiple Time Scale Delays},
  pages = {23-30},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/HM-mascots04.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/HM-mascots04.ps},
  doi = {10.1109/MASCOT.2004.1348178},
  abstract = {We address the problem of transient and steady-state analysis of
    stochastic discrete event systems which include concurrent activities with
    multiple time scales finite support distributions (and consequently non
    Markovian). Rather than computing an approximate distribution of the model
    (as done in previous methods), we~develop an exact analysis of an
    approximate model. The design of this method leads to a uniform handling
    for the computation of the transient and steady-state behaviour of the
    model. We extend a previous result restricted to one time scale in order
    to handle different time scales. Furthermore, we show that some useful
    classes of non ergodic systems can be analyzed in an exact way with this
    method. We have evaluated our algorithms on standard queuing models
    benchmarks. Our results demonstrate that in most of the cases the solution
    of the approximate model converges quickly to the solution of the exact
    model, and in the difficult cases (e.g.~an heavy load on the queue) our
    method is more robust than the previous ones.}
}
@inproceedings{HH-pdcs04,
  address = {San Francisco, California, USA},
  month = sep,
  year = 2004,
  publisher = {International Society for Computers and their Applications},
  editor = {Bader, David A. and Khokhar, Ashfaq A.},
  acronym = {{PDCS}'04},
  booktitle = {{P}roceedings of the {ISCA} 17th {I}nternational {C}onference on
	   {P}arallel and {D}istributed {C}omputing {S}ystems
	   ({PDCS}'04)},
  author = {El~Haddad, Joyce and Haddad, Serge},
  title = {A Fault-contained Spanning Tree Protocol for Arbitrary Networks},
  pages = {410-415},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/HH-pdcs04.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/HH-pdcs04.ps},
  abstract = {Fault-containing self-stabilizing algorithms, introduced by
    A.~Gupta, fulll two requirements: they converge to a correct behavior
    starting from an arbitrary state and they quickly stabilize starting from
    a state corrupted by a single fault. Such algorithms are obtained either
    by an ad hoc transformation of a self-stabilizing algorithm or by a
    generic transformation which produces a slower stabilization in case of a
    single fault. In this paper, we transform a self-stabilizing algorithm for
    constructing a rooted spanning tree in an arbitrary network. This
    algorithm has two specic features with respect to previously adapted
    algorithms: there is no distinguished node (i.e. each site execute the
    same code), and the principle of stabilization involves a global
    coordination through requests and replies following paths of the
    communication graph.}
}
@inproceedings{BHI-wodes04,
  address = {Reims, France},
  month = sep,
  year = 2004,
  acronym = {{WODES}'04},
  booktitle = {{P}roceedings of the 7th {W}orkshop on {D}iscrete {E}vent {S}ystems
	   ({WODES}'04)},
  author = {Baarir, Souheib and Haddad, Serge and Ili{\'e}, Jean-Michel},
  title = {Exploiting Partial Symmetries in Well-formed Nets for the
                  Reachability and the Linear Time Model Checking Problems},
  pages = {223-228},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHI-wodes04.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHI-wodes04.pdf},
  abstract = {Taking advantage of the symmetries of a system is an efficient
    way to cope with the combinatory explosion involved by the verification
    process. Whereas numerous algorithms and tools efficiently deal with the
    verification of a symmetrical formula on a symmetrical model, the
    management of partial symmetries is still an open research topic. In this
    work, we present the design and the evaluation of two methods applicable
    on coloured Petri nets. These two methods are extensions of the symbolic
    reachability graph construction for the well-formed Petri nets. The first
    algorithm, called the extended symbolic reachability graph construction,
    tackles the reachability problem. The second one, called the symbolic
    synchronized product, checks a partially symmetric linear time formula on
    a net. The evaluations show that these two methods outperform the previous
    approaches dealing with partial symmetries. Furthermore they are
    complementary ones since the former while being less general gives better
    results than the latter when applied to the reachability problem. }
}
@inproceedings{EHP-wodes04,
  address = {Reims, France},
  month = sep,
  year = 2004,
  acronym = {{WODES}'04},
  booktitle = {{P}roceedings of the 7th {W}orkshop on {D}iscrete {E}vent {S}ystems
	   ({WODES}'04)},
  author = {Evangelista, Sami and Haddad, Serge and Pradat{-}Peyre,
                  Jean-Fran{\c{c}}ois},
  title = {New Coloured Reductionsfor Software Validation},
  pages = {355-360},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EHP-wodes04.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EHP-wodes04.pdf},
  abstract = {Structural model abstraction is a powerful technique for
    reducing the complexity of a state based enumeration analysis. We present
    in this paper accurate reductions for high-level Petri nets based on new
    ordinary Petri nets reductions. These reductions involve only structural
    and algebraical conditions. They preserve the liveness of the net and any
    LTL formula that does not observe the reduced transitions of the net. The
    mixed use of structural and algebraical conditions significantly enlarges
    their application area. Furthermore the specification of the
    transformation is parametric with respect to the cardinalities of coloured
    domains. }
}
@inproceedings{HMM-wodes04,
  address = {Reims, France},
  month = sep,
  year = 2004,
  acronym = {{WODES}'04},
  booktitle = {{P}roceedings of the 7th {W}orkshop on {D}iscrete {E}vent {S}ystems
	   ({WODES}'04)},
  author = {Haddad, Serge and Mokdad, Lynda and Moreaux, Patrice},
  title = {Performance Evaluation of non-{M}arkovian Stochastic
                  Discrete Event Systems~-- A~New Approach},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HMM-wodes04.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HMM-wodes04.pdf},
  abstract = {In this work, we address the problem of transient and
    steady-state analysis of a stochastic discrete event system which includes
    non Markovian distributions with a finite support. Rather than computing
    an approximate distribution of the model (as done in the previous
    methods), we develop an exact analysis of an approximate model. The design
    of this method leads to a uniform handling for the computation of the
    transient and steady-state behaviour of the model. We have evaluated our
    method on a standard benchmark (the~queuing model M/D/S/K). Our results
    demonstrate that: in most of the cases the solution of the approximate
    model converges quickly to the solution of the exact model, in the
    difficult cases (e.g.~an~heavy load on the queue) our method is more
    robust than the previous ones.}
}
@inproceedings{HMMR-iccta04,
  address = {Damascus, Syria},
  month = apr,
  year = 2004,
  acronym = {{ICCTA}'04},
  booktitle = {{P}roceedings of the {IEEE} 1st {I}nternational {C}onference on
	   {I}nformation and {C}ommunication {T}echnologies: From {T}heory to
                  {A}pplications ({ICCTA}'04)},
  author = {Haddad, Serge and Melliti, Tarek and Moreaux, Patrice and
                  Rampacek, Sylvain},
  title = {A Dense Time Semantics for Web Services Specification
                  Languages},
  pages = {647-648}
}
@inproceedings{HMMR-iceis04,
  address = {Porto, Portugal},
  month = apr,
  year = 2004,
  noeditor = {},
  acronym = {{ICEIS}'04},
  booktitle = {{P}roceedings of the 8th {I}nternational {C}onference on
           {E}nterprise {I}nformation {S}ystems ({ICEIS}'04)},
  author = {Haddad, Serge and Melliti, Tarek and Moreaux, Patrice and
                  Rampacek, Sylvain},
  title = {Modeling Web Services Interoperability},
  pages = {287-295}
}
@techreport{HPP-cedric634,
  author = {Haddad, Serge and Pradat{-}Peyre, Jean-Fran{\c{c}}ois},
  title = {Efficient Reductions for {LTL} Formulae Verification},
  institution = {Centre De Recherche en Informatique
                  du CNAM, Paris, France},
  type = {Research Report},
  number = {634},
  year = 2004,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HP-cedric634.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HP-cedric634.pdf},
  abstract = {Structural model abstraction is a powerful technique for
    reducing the complexity of a state based enumeration analysis. We present
    in this paper new efficient ordinary Petri nets reductions. At~first,
    we~define {"}behavioural{"} reductions (\textit{i.e.}, based on conditions
    related to the language of the net) which preserve a fundamental property
    of a net (\textit{i.e.}, liveness) and any LTL formula that does not
    observe reduced transitions of the net. We~substitute these conditions by
    structural or algebraical ones leading to reductions that can be
    efficiently checked and applied whereas enlarging the application spectrum
    of the previous reductions. At~last, we illustrate our method on
    significant and typical examples.}
}
@techreport{HM-crestic1,
  author = {Haddad, Serge and Moreaux, Patrice},
  title = {Sub-stochastic Matric Analysis and Performance Bounds},
  institution = {Centre de Recherche en Sciences et Technologies de
                  l'Information et de la Communication, Reims, France},
  type = {Research Report},
  number = {RAP-CReSTIC-1},
  year = 2004,
  month = oct,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HM-crestic1.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HM-crestic1.pdf},
  abstract = { On the one hand, the state space of complex Markovian models
    can often be partitioned between a small subset with a high steady-state
    probability and a large subset with a low steady-state probability. On the
    other hand, performance evaluation and reliability analysis require the
    computation of performance indices, often defined as functions of
    instantaneous rewards on the states of the model. Thus the time and space
    complexity of this computation would be greatly decreased by avoiding the
    explicit representation of a large part of the subset associated to the
    low probability. In this report, we present a method to derive bounds on
    such rewards directly from bounds on the parameters of the model -
    transition rates or probabilities. The method is based on the analysis of
    an aggregated Markov chain and on the properties of strong stochastic
    comparison for discrete as well as continuous Markov (sub-)chains. We also
    propose a specific method when the reward is the output rate towards a
    subset of states of a continuous Markov chain. Finally we illustrate our
    approach on some examples in order to show its interest. }
}
@inproceedings{EHMS-jfsma04,
  address = {Paris, France},
  month = nov,
  year = 2004,
  publisher = {Herm{\`e}s},
  editor = {Boissier Olivier and Guessoum, Zahia},
  acronym = {{JFSMA}'04},
  booktitle = {{A}ctes des 12{\`e}mes {J}ourn{\'e}es
           {F}rancophones des Syst{\`e}mes {M}ulti-{A}gents ({JFSMA}'04)},
  author = {El~Fallah Seghrouchni, Amal and Haddad, Serge and Melliti,
                  Tarek and Suna, Alexandru},
  title = {Interop{\'e}rabilit{\'e} des syst{\`e}mes multi-agents {\`a}
                  l'aide des services web},
  pages = {91-104},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EHMS-jfsma04.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EHMS-jfsma04.pdf},
  abstract = {In this paper we present a conceptual and architectural
    framework for the multi-agent systems' interoperability. Our approach
    uses the Web Services, that allow to applications to present their
    functionalities using standardized interfaces. They propose a
    service-oriented architecture, containing complex heterogenous distributed
    systems that can cooperate without a specific and costly integration. In
    our model, the agents publish their abilities as Web services that can be
    used by other agents, independently of conceptual (\textit{e.g.} architecture) or
    technical (\textit{e.g.} platform, programming language) aspects. The proposed
    architecture and concepts have been tested and validated using the CLAIM
    language and the SyMPA platform. }
}
@article{ehp-esta04,
  publisher = {Soci{\'e}t{\'e} de l'{\'E}lectricit{\'e}, de
                  l'{\'E}lectronique et des Technologies de 
		  l'Information et de la Communication},
  journal = {Revue {\'E}lectronique des Sciences et Technologies de
                  l'Automatique},
  author = {Evangelista, Sami and Haddad, Serge and Pradat{-}Peyre,
                  Jean-Fran{\c{c}}ois},
  title = {De nouvelles r{\'e}ductions color{\'e}es pour la validation
                  de logiciels},
  volume = 1,
  nopages = {},
  year = 2004,
  abstract = {Structural model abstraction is a powerful technique for
                  reducing the complexity of a state based enumeration
                  analysis.We present in this paper accurate reductions for
                  high-level Petri nets based on new ordinary Petri nets
                  reductions. These reductions involve only structural and
                  algebraical conditions. They preserve the liveness of the
                  net and any LTL formula that does not observe the reduced
                  transitions of the net. The mixed use of structural and
                  algebraical conditions significantly enlarges their
                  application area. Furthermore the specification of the
                  transformation is parametric with respect to the
                  cardinalities of coloured domains.}
}
@article{hmm-esta04,
  publisher = {Soci{\'e}t{\'e} de l'{\'E}lectricit{\'e}, de
                  l'{\'E}lectronique et des Technologies de 
		  l'Information et de la Communication},
  journal = {Revue {\'E}lectronique des Sciences et Technologies de
                  l'Automatique},
  author = {Haddad, Serge and Mokdad, Lynda and Moreaux, Patrice},
  title = {{\'E}valuation de performance des syst{\`e}mes 
		stochastiques {\`a} {\'e}v{\'e}nements discrets
		non {M}arkoviens~--- une~nouvelle approche},
  volume = 1,
  nopages = {},
  year = 2004,
  abstract = {In this work, we address the problem of transient and
                  steady-state analysis of a stochastic discrete event system
                  which includes (non Markovian) distributions with a finite
                  support. Rather than computing an approximate distribution
                  of the model (as done in the previous methods), we develop
                  an exact analysis of an approximate model. The design of
                  this method leads to a uniform handling for the computation
                  of the transient and steadystate behaviour of the model. We
                  have evaluated our method on a standard benchmark (the
                  queuing model M/D/S/K). Our results demonstrate that: in
                  most of the cases the solution of the approximate model
                  converges quickly to the solution of the exact model, in the
                  difficult cases (e.g. an heavy load on the queue) our method
                  is more robust than the previous ones.}
}
@inproceedings{BCHLR05-fsttcs,
  address = {Hyderabad, India},
  month = dec,
  year = 2005,
  volume = 3821,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Ramanujam, R. and Sen, Sandeep},
  acronym = {{FSTTCS}'05},
  booktitle = {{P}roceedings of the 25th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'05)},
  author = {B{\'e}rard, B{\'e}atrice and Cassez, Franck and Haddad,
                  Serge and Lime, Didier and Roux, Olivier H.},
  title = {When are Timed Automata Weakly Timed Bisimilar to Time
                  {P}etri Nets?},
  pages = {273-284},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCHLR-fsttcs05.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCHLR-fsttcs05.pdf},
  doi = {10.1007/11590156_22},
  abstract = {In this paper, we~compare Timed Automata~(TA) with Time Petri
    Nets~(TPN) with respect to weak timed bisimilarity. It is already known
    that the class of bounded TPNs is included in the class of~TA. It~is thus
    natural to try and identify the (strict) subclass
    \(\mathcal{TA}^{\text{wtb}}\) of TA that is equivalent to TPN for the weak
    time bisimulation relation. We give a characterisation of this subclass
    and we show that the membership problem and the reachability problem for
    \(\mathcal{TA}^{\text{wtb}}\) are PSPACE-complete. Furthermore we show
    that for a TA in \(\mathcal{TA}^{\text{wtb}}\) with integer constants,
    an~equivalent TPN can be built with integer bounds but with a size
    exponential w.r.t.~the original model. Surprisingly, using rational bounds
    yields a TPN whose size is linear. }
}
@inproceedings{EHP05-atva,
  address = {Taipei, Taiwan},
  month = oct,
  year = {2005},
  volume = 3707,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Peled, Doron A. and Tsay, Yih-Kuen},
  acronym = {{ATVA}'05},
  booktitle = {{P}roceedings of the 3rd {I}nternational
               {S}ymposium on {A}utomated {T}echnology
               for {V}erification and {A}nalysis
               ({ATVA}'05)},
  author = {Evangelista, Sami and Haddad, Serge and Pradat{-}Peyre,
                  Jean-Fran{\c{c}}ois},
  title = {Syntactical Colored {P}etri Nets Reductions},
  pages = {202-216},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EHP05-atva.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EHP05-atva.pdf},
  doi = {10.1007/11562948_17}
}
@inproceedings{BCHLR05-atva,
  address = {Taipei, Taiwan},
  month = oct,
  year = {2005},
  volume = 3707,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Peled, Doron A. and Tsay, Yih-Kuen},
  acronym = {{ATVA}'05},
  booktitle = {{P}roceedings of the 3rd {I}nternational
               {S}ymposium on {A}utomated {T}echnology
               for {V}erification and {A}nalysis
               ({ATVA}'05)},
  author = {B{\'e}rard, B{\'e}atrice and Cassez, Franck and Haddad,
                  Serge and Lime, Didier and Roux, Olivier H.},
  title = {Comparison of Different Semantics for Time {P}etri Nets},
  pages = {293-307},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCHLR05-atva.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCHLR05-atva.pdf},
  doi = {10.1007/11562948_23},
  abstract = {In this paper we study the model of Time Petri Nets
    (TPNs) where a time interval is associated with the firing of a
    transition, but we extend it by considering general intervals rather than
    closed ones. A key feature of timed models is the memory policy, i.e.
    which timing informations are kept when a transition is fired. The
    original model selects an \emph{intermediate} semantics where the
    transitions disabled after consuming the tokens, as well as the firing
    transition, are reinitialised. However this semantics is not appropriate
    for some applications. So we consider here two alternative semantics: the
    \emph{atomic} and the \emph{persistent atomic} ones. First we present
    relevant patterns of discrete event systems which show the interest of
    these semantics. Then we compare the expressiveness of the three semantics
    w.r.t. weak timed bisimilarity, establishing inclusion results in the
    general case. Furthermore we show that some inclusions are strict with
    unrestricted intervals even when nets are bounded. Then we focus on
    bounded TPNs with upper-closed intervals and we prove that the semantics
    are equivalent. Finally taking into account both the practical and the
    theoretical issues, we conclude that persistent atomic semantics should be
    preferred. }
}
@inproceedings{KHI-forte05,
  address = {Taipei, Taiwan},
  month = oct,
  year = 2005,
  volume = 3731,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Wang, Farn},
  acronym = {{FORTE}'05},
  booktitle = {{P}roceedings of 25th {IFIP} {WG6.1} 
           {I}nternational {C}onference on {F}ormal
           {T}echniques for {N}etworked and {D}istributed {S}ystems
	   ({FORTE}'05)},
  author = {Klai, Kais and Haddad, Serge and Ili{\'e}, Jean-Michel},
  title = {Modular Verification of {P}etri Nets Properties: A Structure-Based Approach},
  pages = {189-203},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KHI-forte05.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KHI-forte05.pdf},
  doi = {10.1007/11562436_15},
  abstract = {In this paper, we address the modular verication problem for a
    Petri net obtained by composition of two subnets. At rst, we show how to
    transform an asynchronous composition into a synchronous one where the new
    subnets are augmented from the original ones by means of linear
    invariants. Then we introduce a non-constraining relation between
    subnets based on their behaviour. Whenever this relation is satised,
    standard properties like the liveness and the boundedness and generic
    properties specied by a linear time logic may be checked by examination of
    the augmented subnets in isolation. Finally, we give a sucient condition
    for this relation which can be detected modularly using an ecient
    algorithm.}
}
@inproceedings{BCHLR-formats2005,
  address = {Uppsala, Sweden},
  month = nov,
  year = 2005,
  volume = 3829,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Pettersson, Paul and Yi, Wang},
  acronym = {{FORMATS}'05},
  booktitle = {{P}roceedings of the 3rd {I}nternational {C}onference
           on {F}ormal {M}odelling and {A}nalysis of {T}imed
           {S}ystems ({FORMATS}'05)},
  author = {B{\'e}rard, B{\'e}atrice and Cassez, Franck and Haddad,
                  Serge and Lime, Didier and Roux, Olivier H.},
  title = {Comparison of the Expressiveness of Timed Automata and Time
                  {P}etri Nets},
  pages = {211-225},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCHLR-formats2005.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCHLR-formats2005.pdf},
  doi = {10.1007/11603009_17},
  abstract = {In this paper we consider the model of Time Petri Nets~(TPN)
    {"}\`a~la Merlin{"} where a time interval is associated with the firing of a
    transition, but we extend it with open intervals. We also consider Timed
    Automata~(TA) as defined by Alur \&~Dill. We~investigate some questions
    related to expressiveness for these models : we study the impact of slight
    variations of semantics for TPN and we compare the expressive power of TA
    and TPN, with respect to both time language acceptance and weak time
    bisimilarity. We prove that TA and bounded TPNs (enlarged with strict
    constraints) are equivalent w.r.t. timed language equivalence, providing
    an efficient construction of a TPN equivalent to a~TA. We~then exhibit a
    TA~\(\mathcal{A}\) such that no~TPN (even unbounded) is weakly bisimilar
    to~\(\mathcal{A}\). Because of this last result, it is natural to try and
    identify the (strict) subclass of~TA that is equivalent to~TPN w.r.t.~weak
    timed bisimilarity. Thus we give some further results: 1)~we~characterize
    the subclass TA\textsuperscript{-} of TA that is equivalent to the
    original model of TPN as defined by Merlin, \textit{i.e.},~restricted to
    closed intervals, 2)~we~show that the associated membership problem for
    TA\textsuperscript{-} is PSPACE-complete and 3)~we~prove that the
    reachability problem for TA\textsuperscript{-} is also PSPACE-complete.}
}
@article{HMSS-pe59(4),
  publisher = {Elsevier Science Publishers},
  journal = {Performance Evaluation},
  author = {Haddad, Serge and Moreaux, Patrice and Sereno, Matteo and Silva, Manuel},
  title = {Product-form and Stochastic {P}etri Nets: A Structural
                  Approach},
  volume = 59,
  number = 4,
  pages = {313-336},
  month = mar,
  year = 2005,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HMSS-pe594.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HMSS-pe594.pdf},
  doi = {10.1016/j.peva.2004.08.004},
  abstract = {Stochastic Petri nets~(SPN) with product-form solution are nets
    for which there is an analytic expression of the steady-state
    probabilities with respect to place markings, as it is the case for
    product-form queueing networks with respect to queue lengths. The most
    general kind of SPNs with product-form solution introduced by Coleman
    \textit{et~al.} (and~denoted here by \(S\Pi\)-nets) suffers a serious
    drawback: the existence of such a solution depends on the values of the
    transition rates. Thus since their introduction, it is an open question to
    characterize \(S\Pi\)-nets with product-form solution for any values of
    the rates. A~partial characterization has been obtained by Henderson
    \textit{et al}. However this characterization does not hold for every
    initial marking and it is expressed in terms of the reachability graph.
    In~this paper, we~obtain a purely structural characterization of
    \(S\Pi\)-nets for which a product-form solution exists for any value of
    probabilistic parameters of the SPN and for any initial marking. This
    structural characterization leads to the definition of \(S\Pi^{2}\)-nets
    (Stochastic Parametric Product-form Petri nets). We also design a
    polynomial time (with respect to the size of the net structure) algorithm
    to check whether a SPN is a \(S\Pi^{2}\)-net. Then, we study qualitative
    properties of \(\Pi\)-nets and \(\Pi^{2}\)-nets, the non-stochastic
    versions of \(S\Pi\)-nets and \(S\Pi^{2}\)-nets: we~establish two results
    on the complexity bounds for the liveness and the reachability problems,
    which are central problems in Petri nets theory. This set of results
    complements previous studies on these classes of nets and improves the
    applicability of product-form solutions for~SPNs.}
}
@inproceedings{FHMS-ciat05,
  address = {Compi{\`e}gne, France},
  month = sep,
  year = 2005,
  publisher = {{IEEE} Computer Society Press},
  editor = {Skowron, Andrzej and Barth?s, Jean-Paul A. and Jain, Lakhmi C. and
            Sun, Ron and Morizet-Mahoudeaux, Pierre and Liu, Jiming and Zhong, Ning},
  acronym = {{IAT}'05},
  booktitle = {{P}roceedings of the 2005 {IEEE}/{WIC}/{ACM} {I}nternational
          {C}onference on {I}ntelligent {A}gent {T}echnology ({IAT}'05)},
  author = {Melliti, Tarek and Haddad, Serge and Suna, Alexandru and 
		  El~Fallah Seghrouchni, Amal},
  title = {{Web-MASI}: Multi-Agent Systems Interoperability Using
                  Web Services Based Approach},
  pages = {739-742},
  doi = {10.1109/IAT.2005.142}
}
@inproceedings{BDHI-qest05,
  address = {Turin, Italy},
  month = sep,
  year = 2005,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{QEST}'05},
  booktitle = {{P}roceedings of the 2nd {I}nternational
               {C}onference on {Q}uantitative 
               {E}valuation of {S}ystems
               ({QEST}'05)},
  author = {Baarir, Souheib and Dutheillet, Claude and Haddad, Serge and
                  Ili{\'e}, Jean-Michel},
  title = {On the Use of Exact Lumpability in Partially Symmetrical
                  Well-formed Nets},
  pages = {23-32},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDHI-qest05.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDHI-qest05.pdf},
  doi = {10.1109/QEST.2005.26},
  abstract = { Well-formed Nets (WNs) have proved an efficient model for
    building quotient reachability graphs that can be used either for
    qualitative or performance analysis. However, local asymmetries often
    break any possibility of grouping states into classes, thus drastically
    reducing the interest of the approach. An efficient solution has been
    proposed for qualitative analysis, which relies on a separate
    representation of the asymmetries in a so-called control automaton. The
    quotient graph is then obtained by synchronising the transitions of the WN
    model with the transitions of the control automaton. In this paper, we
    improve this approach to quantitative analysis. We show that it can be
    used to build an aggregated graph that is isomorphic to a Markov chain
    which verifies exact lumpability. Theoretical considerations and practical
    experiments show that our method outperforms previous approaches. }
}
@inproceedings{BHR06-acsd,
  address = {Turku, Finland},
  month = jun,
  year = 2006,
  publisher = {{IEEE} Computer Society Press},
  editor = {Goossens, Kees and Petrucci, Laure},
  acronym = {{ACSD}'06},
  booktitle = {{P}roceedings of the 6th {I}nternational
               {C}onference on {A}pplication of {C}oncurrency
               to {S}ystem {D}esign
               ({ACSD}'06)},
  author = {Bouyer, Patricia and Haddad, Serge and 
                  Reynier, Pierre-Alain},
  title = {Extended Timed Automata and Time {P}etri Nets},
  pages = {91-100},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-01.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-01.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
        rr-lsv-2006-01.ps},
  doi = {10.1109/ACSD.2006.6},
  abstract = {Timed Automata (TA) and Time Petri Nets (TPN) are two
 well-established formal models for real-time systems. Recently, a
 linear transformation of TA to TPNs preserving reachability
 properties and timed languages has been proposed, which does however
 not extend to larger classes of TA which would allow diagonal
 constraints or more general resets of clocks. Though these features
 do not add expressiveness, they yield exponentially more concise
 models. \par
 In this work, we propose two translations: one from extended TA to
 TPNs whose size is either linear or quadratic in the size of the
 original TA, depending on the features which are allowed; another
 one from a parallel composition of TA to TPNs, which is also linear.
 As a consequence, we get that TPNs are exponentially more concise
 than~TA.}
}
@inproceedings{BHR-ICALP2006,
  address = {Venice, Italy},
  month = jul,
  year = 2006,
  volume = 4052,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Buglesi, Michele and Preneel, Bart and Sassone, Vladimiro and Wegener, Ingo},
  acronym = {{ICALP}'06},
  booktitle = {{P}roceedings of the 33rd {I}nternational 
               {C}olloquium on {A}utomata, {L}anguages and 
               {P}rogramming ({ICALP}'06)~--- {P}art~{II}},
  author = {Bouyer, Patricia and Haddad, Serge and Reynier, Pierre-Alain},
  title = {Timed {P}etri Nets and Timed Automata: On the Discriminating Power of
            {Z}eno Sequences},
  pages = {420-431},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-icalp06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-icalp06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BHR-icalp06.ps},
  doi = {10.1007/11787006_36},
  abstract = {Timed Petri nets and timed 
	automata are two standard models for the 
	analysis of real-time systems. In this 
	paper, we prove that they are incomparable 
	for the timed language equivalence. Thus we 
	propose an extension of timed Petri nets 
	with read-arcs~(RA-TdPN), whose coverability 
	problem is decidable. We also show that this 
	model unifies timed Petri nets and timed 
	automata. Then, we establish numerous 
	expressiveness results and prove that Zeno 
	behaviours discriminate between several 
	sub-classes of RA-TdPNs. This has surprising 
	consequences on timed automata, 
	\emph{e.g.}~on the power of 
	non-deterministic clock resets.}
}
@inproceedings{BHR-atva06,
  address = {Beijing, China},
  month = oct,
  year = {2006},
  volume = 4218,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Graf, Susanne and Zhang, Wenhui},
  acronym = {{ATVA}'06},
  booktitle = {{P}roceedings of the 4th {I}nternational
               {S}ymposium on {A}utomated {T}echnology
               for {V}erification and {A}nalysis
               ({ATVA}'06)},
  author = {Bouyer, Patricia and Haddad, Serge and Reynier, Pierre-Alain},
  title = {Timed Unfoldings for Networks of Timed Automata},
  pages = {292-306},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-atva06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-atva06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BHR-atva06.ps},
  doi = {10.1007/11901914_23},
  abstract = {Whereas partial order methods have proved their efficiency for
the analysis of discrete-event systems, their application to
timed systems remains a challenging research topic. Here, we
design a verification algorithm for networks of timed automata
with invariants. Based on the unfolding technique, our method
produces a branching process as an acyclic Petri net extended
with read arcs. These arcs verify conditions on tokens without
consuming them, thus expressing concurrency between conditions
checks. They are useful for avoiding the explosion of the size
of the unfolding due to clocks which are compared with constants
but not reset. Furthermore, we attach zones to events, in addition
to markings. We~then compute a complete finite prefix of the
unfolding. The~presence of invariants goes against the concurrency
since it entails a global synchronization on time. The use of read
arcs and the analysis of the clock constraints appearing in
invariants will help increasing the concurrency relation between
events. Finally, the finite prefix we compute can be used to decide
reachability properties, and transition enabling.}
}
@inproceedings{HRS-formats06,
  address = {Paris, France},
  month = sep,
  year = 2006,
  volume = 4202,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Asarin, Eug{\`e}ne and Bouyer, Patricia},
  acronym = {{FORMATS}'06},
  booktitle = {{P}roceedings of the 4th {I}nternational {C}onference
           on {F}ormal {M}odelling and {A}nalysis of {T}imed
           {S}ystems ({FORMATS}'06)},
  author = {Haddad, Serge and Recalde, Laura and Silva, Manuel},
  title = {On the Computational Power of Timed Differentiable {P}etri Nets},
  pages = {230-244},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HRS-formats06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HRS-formats06.pdf},
  doi = {10.1007/11867340_17},
  abstract = {Well-known hierarchies discriminate between 
	the computational power of discrete time and space 
	dynamical systems. A~contrario the situation is more 
	confused for dynamical systems when time and space are 
	continuous. A~possible way to discriminate between these 
	models is to state whether they can simulate Turing 
	machine. For instance, it~is known that continuous 
	systems described by an ordinary differential 
	equation~(ODE) have this power. However, since the 
	involved ODE is defined by overlapping local ODEs inside 
	an infinite number of regions, this result has no 
	significant application for differentiable models whose 
	ODE is defined by an explicit representation. In this 
	work, we considerably strengthen this result by showing 
	that Time Differentiable Petri Nets~(TDPN) can simulate 
	Turing machines. Indeed the ODE ruling this model is 
	expressed by an explicit linear expression enlarged with 
	the minimum operator. More precisely, we~present two 
	simulations of a two counter machine by a TDPN in order 
	to fulfill opposite requirements: robustness and 
	boundedness. These simulations are performed by nets 
	whose dimension of associated ODEs is constant. At last, 
	we prove that marking coverability, submarking 
	reachability and the existence of a steady-state are 
	undecidable for TDPNs.}
}
@inproceedings{HMM-icatpn06,
  address = {Turku, Finland},
  month = jun,
  year = 2006,
  volume = 4024,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Donatelli, Susanna and Thiagarajan, P. S.},
  acronym = {{ICATPN}'06},
  booktitle = {{P}roceedings of the 27th
               {I}nternational {C}onference on
               {A}pplications and {T}heory of {P}etri {N}ets
               ({ICATPN}'06)},
  author = {Haddad, Serge and Mokdad, Lynda and 
		 Moreaux, Patrice},
  title = {A New Approach to the Evaluation of Non 
		 {M}arkovian Stochastic {P}etri Nets},
  pages = {221-240},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HMM-icatpn06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HMM-icatpn06.pdf},
  doi = {10.1007/11767589_13},
  abstract = {In this work, we address the 
	problem of transient and steady-state 
	analysis of a stochastic Petri net which 
	includes non Markovian distributions with a 
	finite support but without any additional 
	constraint. Rather than computing an 
	approximate distribution of the model (as 
	done in previous methods), we develop an 
	exact analysis of an approximate model. The 
	design of this method leads to a uniform 
	handling of the computation of the transient 
	and steady state behaviour of the model. This 
	method is an adaptation of a former one 
	developed by the same authors for general 
	stochastic processes (which was shown to be 
	more robust than alternative techniques). 
	Using Petri nets as the modelling formalism 
	enables us to express the behaviour of the 
	approximate process by tensorial expressions. 
	Such a representation yields significant 
	savings w.r.t.~time and space complexity.}
}
@inproceedings{HMR-iceis06,
  address = {Paphos, Cyprus},
  month = may,
  year = 2006,
  editor = {Manolopoulos, Yannis and Filipe, Joaquim and Constantopoulos, Panos and Cordeiro, Jos{\'e}},
  acronym = {{ICEIS}'06},
  booktitle = {{P}roceedings of the 8th {I}nternational {C}onference on
           {E}nterprise {I}nformation {S}ystems ({ICEIS}'06),
           volume~4},
  author = {Haddad, Serge and Moreaux, Patrice and Rampacek, Sylvain},
  title = {Client Synthesis for Web Services by Way of a Timed 
		 Semantics},
  pages = {19-26},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HMR-iceis06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HMR-iceis06.pdf},
  abstract = {A complexWeb service described with languages 
	like BPEL4WS, consists of an executable process and its 
	observable behaviour (called an abstract process) based on the 
	messages exchanged with the client. The abstract process 
	behaviour is non deterministic due to the internal choices 
	during the service execution. Furthermore the specification 
	often includes timing constraints which must be taken into 
	account by the client. Thus given a service specification, we 
	identify the synthesis of a client as a key issue for the 
	development ofWeb services. To~this end, we~propose an approach 
	based on (dense) timed automata to first describe the 
	observable service behaviour and then to build correct 
	interacting clients when possible. The~present work extends a 
	previous discrete time approach and overcomes its 
	limitations.}
}
@inproceedings{CHKKPT-ictac06,
  address = {Tunis, Tunisia},
  month = nov,
  year = 2006,
  volume = 4281,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Barkaoui, Kamel and Cavalcanti, Ana and Cerone, Antonio},
  acronym = {{ICTAC}'06},
  booktitle = {{P}roceedings of the 3rd {I}nternational {C}olloquium on
	{T}heoretical {A}spects of {C}omputing ({ICTAC}'06)},
  author = {Choppy, {\relax Ch}ristine and Haddad, Serge and Klaudel, Hanna
		 and Kordon, Fabrice and Petrucci, Laure and Thierry{-}Mieg, Yann},
  title = {Tutorial on Formal Methods for Distributed and Cooperative Systems},
  pages = {362-365},
  doi = {10.1007/11921240_25}
}
@article{HP-ppl06,
  publisher = {World Scientific},
  journal = {Parallel Processing Letters},
  author = {Haddad, Serge and Pradat{-}Peyre, Jean-Fran{\c{c}}ois},
  title = {New Efficient {P}etri Nets Reductions for Parallel Programs 
		Verification},
  year = 2006,
  month = mar,
  volume = 16,
  number = 1,
  pages = {101-116},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HP-ppl06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HP-ppl06.pdf},
  doi = {10.1142/S0129626406002502},
  abstract = {Structural model abstraction is a 
	powerful technique for reducing the complexity of 
	a state based enumeration analysis. We present in 
	this paper new efficient Petri nets reductions. 
	First, we~define {"}behavioural{"} reductions 
	(\textit{i.e.},~based on conditions related to 
	the language of the net) which preserve a 
	fundamental property of a net 
	(\textit{i.e.},~liveness) and any formula of the 
	(action-based) linear time logic that does not 
	observe reduced transitions of the net. We~show 
	how to replace these conditions by structural or 
	algebraical ones leading to reductions that can 
	be efficiently checked and applied whereas 
	enlarging the application spectrum of the 
	previous reductions. At~last, we~illustrate our 
	method on a significant and typical example of a 
	synchronisation pattern of parallel programs.}
}
@incollection{Had-mfsrc06,
  author = {Haddad, Serge},
  title = {Panorama de la v{\'e}rification},
  booktitle = {M{\'e}thodes formelles pour les syst{\`e}mes r{\'e}artis et
                  coop{\'e}ratifs},
  editor = {Haddad, Serge and Kordon, Fabrice and Petrucci, Laure},
  publisher = {Herm{\`e}s},
  chapter = 6,
  year = 2006,
  month = nov,
  pages = {121-138},
  url = {http://www.lavoisier.fr/notice/fr332846.html},
  isbn = {2-7462-1447-4}
}
@incollection{BHM-mfsrc06,
  author = {Boutrous{-}Saab, C{\'e}line and Haddad, Serge and Monfort, Val{\'e}rie},
  title = {Interop{\'e}rabilit{\'e} et services web},
  booktitle = {M{\'e}thodes formelles pour les syst{\`e}mes r{\'e}artis et
                  coop{\'e}ratifs},
  editor = {Haddad, Serge and Kordon, Fabrice and Petrucci, Laure},
  chapter = 12,
  publisher = {Herm{\`e}s},
  year = 2006,
  month = nov,
  pages = {289-315},
  url = {http://www.lavoisier.fr/notice/fr332846.html},
  isbn = {2-7462-1447-4}
}
@incollection{HM-mfsrc06,
  author = {Haddad, Serge and Moreaux, Patrice},
  title = {V{\'e}rification de syst{\`e}mes probabilis{\'e}s~:
                  m{\'e}thodes et outils},
  booktitle = {Syst{\`e}mes temps-r{\'e}el~1~: techniques de description
                et de v{\'e}rification},
  editor = {Navet, Nicolas},
  publisher = {Herm{\`e}s},
  year = 2006,
  month = jun,
  pages = {261-292},
  url = {http://www.lavoisier.fr/notice/fr2746213030.html},
  isbn = {2-7462-1303-6}
}
@inproceedings{BBHMT-wewst06,
  address = {Zurich, Switzerland},
  month = dec,
  year = 2006,
  editor = {Pautasso, Cesare and Bussler, Christoph},
  acronym = {{WEWST}'06},
  booktitle = {{P}roceedings of the {W}orkshop on {E}merging 
	   {W}eb {S}ervices {T}echnology ({WEWST}'06)},
  author = {Ben{ }Hmida, Mehdi and Boutrous{-}Saab, C{\'e}line and
                  Haddad, Serge and Monfort, Val{\'e}rie and Tomaz, Ricardo Ferraz},
  title = {Dynamically Adapting Clients to Web Services Changing},
  pages = {91-96},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBHMT-wewst06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBHMT-wewst06.pdf},
  abstract = {Web Service is the applicationtted technical solution
                  which provides the required loose coupling to achieve
                  Service Oriented Architecture~(SOA). However, there is still
                  much to be done in order to increase xibility and
                  adaptability to SOA-based applications. In previous
                  researches, we proposed approaches based on Aspect Oriented
                  Programming~(AOP) and Process Algebra~(PA) to address
                  xibility and client generation issues in theWeb Service
                  context. In this paper, we extend our previous formalism
                  descriptionned for abstract BPEL processes, with three AOP
                  constructs. The new formalism allows to specify dynamic
                  change-prone BPEL processes. We also define the extended
                  interaction relation which characterizes the concept of
                  correct interaction between the adaptable BPEL process and
                  its client. Then, we propose an algorithm to generate a
                  client which dynamically adapt itself to the service
                  changing.}
}
@article{BHR-ietc07,
  publisher = {Elsevier Science Publishers},
  journal = {Information and Computation},
  author = {Bouyer, Patricia and Haddad, Serge and Reynier, Pierre-Alain},
  title = {Timed {P}etri Nets and Timed Automata: On the Discriminating
           Power of {Z}eno Sequences},
  year = {2008},
  month = jan,
  volume = 206,
  number = 1,
  pages = {73-107},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-ic07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-ic07.pdf},
  doi = {10.1016/j.ic.2007.10.004},
  abstract = {Timed Petri nets and timed automata are two standard models for
    the analysis of real-time systems. We~study in this paper their
    relationship, and prove in particular that they are incomparable w.r.t.
    language equivalence. In~fact, we~study the more general model of timed
    Petri nets with read-arcs (RA-TdPN), already introduced in~[Ji{\v{r}}{\'\i}~Srba,
                  \textit{Timed-arc petri nets vs. networks of timed
                  automata}, Proc.\ ICATPN'05, LNCS~3536, Springer], which
    unifies both models of timed Petri nets and of timed automata, and prove
    that the coverability problem remains decidable for this model. Then, we
    establish numerous expressiveness results and prove that Zeno behaviours
    discriminate between several sub-classes of RA-TdPNs. This has surprising
    consequences on timed automata, for~instance on the power of
    non-deterministic clock resets.}
}
@inproceedings{RHS-atva07,
  address = {Tokyo, Japan},
  month = oct,
  year = {2007},
  volume = 4762,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Namjoshi, Kedar and Yoneda, Tomohiro},
  acronym = {{ATVA}'07},
  booktitle = {{P}roceedings of the 5th {I}nternational
               {S}ymposium on {A}utomated {T}echnology
               for {V}erification and {A}nalysis
               ({ATVA}'07)},
  author = {Recalde, Laura and Haddad, Serge and Silva, Manuel},
  title = {Continuous {P}etri Nets: Expressive Power and Decidability 
		Issues},
  pages = {362-377},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/RHS-atva07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/RHS-atva07.pdf},
  doi = {10.1007/978-3-540-75596-8_26},
  abstract = {State explosion is a 
	fundamental problem in the analysis and 
	synthesis of discrete event systems. 
	Continuous Petri nets can be seen as a 
	relaxation of discrete models. The 
	expected gains are twofold: improvements 
	in comlexity and in decidability. This 
	paper concentrates on the study of 
	decidability issues. In~the case of 
	autonomous nets it is proved that 
	properties like reachability, liveness 
	or deadlock-freeness remain decidable. 
	When time is introduced in the model 
	(using an infinite server semantics) 
	decidability of these properties is 
	lost, since continuous timed Petri nets 
	are able to simulate Turing machines.}
}
@inproceedings{HP-forte07,
  address = {Tallinn, Estonia},
  month = jun,
  year = 2007,
  volume = 4574,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Derrick, John and Vain, J{\"u}ri},
  acronym = {{FORTE}'07},
  booktitle = {{P}roceedings of 27th {IFIP} {WG6.1} 
           {I}nternational {C}onference on {F}ormal
           {T}echniques for {N}etworked and {D}istributed {S}ystems
	   ({FORTE}'07)},
  author = {Haddad, Serge and Poizat, Pascal},
  title = {Transactional Reduction of Component Compositions},
  pages = {341-357},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HP-forte07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HP-forte07.pdf},
  doi = {10.1007/978-3-540-73196-2_22},
  abstract = {Behavioural protocols are beneficial 
	to Component-Based Software Engineering and 
	Service-Oriented Computing as they foster 
	automatic procedures for discovery, composition, 
	composition correctness checking and adaptation. 
	However, resulting composition models 
	(\textit{e.g.},~orchestrations or adaptors) often 
	contain redundant or useless parts yielding the 
	state explosion problem. Mechanisms to reduce the 
	state space of behavioural composition models are 
	therefore required. While reduction techniques are 
	numerous, \textit{e.g.}, in~the process algebraic 
	framework, none is suited to compositions where 
	provided/required services correspond to 
	transactions of lower-level individual event based 
	communications. In~this article we address this 
	issue through the definition of a dedicated model 
	and reduction techniques. They support 
	transactions and are therefore applicable to 
	service architectures.}
}
@inproceedings{BFH-icatpn07,
  address = {Siedlce, Poland},
  month = jun,
  year = 2007,
  volume = 4546,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Kleijn, Jetty and Yakovlev, Alex},
  acronym = {{ICATPN}'07},
  booktitle = {{P}roceedings of the 28th
               {I}nternational {C}onference on
               {A}pplications and {T}heory of {P}etri {N}ets
               ({ICATPN}'07)},
  author = {Beccuti, Marco and Franceschinis, Giuliana and 
		 Haddad, Serge},
  title = {{M}arkov Decision {P}etri Net and {M}arkov Decision 
		 Well-Formed Net Formalisms},
  pages = {43-62},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFH-icatpn07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFH-icatpn07.pdf},
  doi = {10.1007/978-3-540-73094-1_6},
  abstract = {In this work, we propose two 
	high-level formalisms, \emph{Markov Decision 
	Petri Nets}~(MDPNs) and \emph{Markov 
	Decision Well-formed Nets}~(MDWNs), useful 
	for the modeling and analysis of distributed 
	systems with probabilistic and non 
	deterministic features: these formalisms 
	allow a high level representation of Markov 
	Decision Processes. The~main advantages of 
	both formalisms are: a~macroscopic point of 
	view of the alternation between the 
	probabilistic and the non deterministic 
	behaviour of the system and a syntactical 
	way to define the switch between the two 
	behaviours. Furthermore, MDWNs enable the 
	modeller to specify in a concise way similar 
	components. We~have also adapted the 
	technique of the symbolic reachability 
	graph, originally designed for Well-formed 
	Nets, producing a reduced Markov decision 
	process w.r.t.~the original one, on~which 
	the analysis may be performed more 
	efficiently. Our~new formalisms and analysis 
	methods are already implemented and 
	partially integrated in the GreatSPN tool, 
	so we also describe some experimental 
	results.}
}
@inproceedings{BBHMF-iceis07,
  address = {Funchal, Madeira, Portugal},
  month = jun,
  year = 2007,
  editor = {Cardoso, Jorge and Cordeiro, Jos{\'e} and Filipe, Joaquim},
  acronym = {{ICEIS}'07},
  booktitle = {{P}roceedings of the 9th {I}nternational {C}onference on 
	   {E}nterprise {I}nformation {S}ystems ({ICEIS}'07), 
	   volume~{EIS}},
  author = {Ben{ }Hmida, Mehdi and Boutrous{-}Saab, C{\'e}line and Haddad, Serge and 
		 Monfort, Val{\'e}rie and Tomaz, Ricardo Ferraz},
  title = {Towards the Dynamic Adaptability of~{SOA}},
  pages = {474-479}
}
@article{HP-acta07,
  publisher = {Springer},
  journal = {Acta Informatica},
  author = {Haddad, Serge and Poitrenaud, Denis},
  title = {Recursive {P}etri Nets~-- {T}heory and Application to
                  Discrete Event Systems},
  volume = {44},
  number = {7-8},
  pages = {463-508},
  year = 2007,
  month = dec,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HP-acta07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HP-acta07.pdf},
  doi = {10.1007/s00236-007-0055-y},
  abstract = { In order to design and analyse complex systems, 
	modelers need formal models with two contradictory 
	requirements: a high expressivity and the decidability of 
	behavioural property checking. Here we present and develop the 
	theory of such a model, the recursive Petri nets. First, we 
	show that the mechanisms supported by recursive Petri nets 
	enable to model patterns of discrete event systems related to 
	the dynamic structure of processes. Furthermore, we prove that 
	these patterns cannot be modelled by ordinary Petri nets. Then 
	we study the decidability of some problems: reachability, 
	finiteness and bisimulation. At last, we develop the concept 
	of linear invariants for this kind of nets and we design 
	efficient computations specifically tailored to take advantage 
	of their structure.}
}
@article{HM-ejor07,
  publisher = {Elsevier Science Publishers},
  journal = {European Journal of Operational Research},
  author = {Haddad, Serge and Moreaux, Patrice},
  title = {Sub-stochastic matrix analysis for bounds computation~--- 
		 {T}heoretical results},
  volume = 167,
  number = 2,
  pages = {},
  year = 2007,
  month = jan,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HM-ejor07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HM-ejor07.pdf},
  doi = {10.1016/j.ejor.2005.08.016},
  abstract = {Performance evaluation of complex 
	systems is a critical issue and bounds computation 
	provides confidence about service quality, 
	reliability,~etc.~of such systems. The stochastic 
	ordering theory has generated a lot of works on 
	bounds computation. Maximal lower and minimal 
	upper bounds of a Markov chain by a st-monotone 
	one exist and can be efficiently computed. In the 
	present work, we extend simultaneously this last 
	result in two directions. On the one hand, we 
	handle the case of a maximal monotone lower bound 
	of a \emph{family of Markov chains} where the 
	coefficients are given by numerical intervals. On 
	the other hand, these chains are \emph{sub-chains 
	associated to sub-stochastic matrices}. We~prove 
	the existence of this maximal bound and we provide 
	polynomial time algorithms to compute it both for 
	discrete and continuous Markov chains. Moreover, 
	it appears that the bounding sub-chain of a family 
	of strictly sub-stochastic ones is not necessarily 
	strictly sub-stochastic. We establish a 
	characterization of the families of sub-chains for 
	which these bounds are strictly sub-stochastic. 
	Finally, we show how to apply these results to a 
	classical model of repairable system. A 
	forthcoming paper will present detailed numerical 
	results and comparison with other methods.}
}
@inproceedings{DHS-qest07,
  address = {Edinburgh, Scotland, UK},
  month = sep,
  year = 2007,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{QEST}'07},
  booktitle = {{P}roceedings of the 4th {I}nternational
               {C}onference on {Q}uantitative 
               {E}valuation of {S}ystems
               ({QEST}'07)},
  author = {Donatelli, Susanna and Haddad, Serge and Sproston, Jeremy},
  title = {{CSL\textsuperscript{TA}}: an Expressive Logic for 
                 Continuous-Time {M}arkov Chains},
  pages = {31-40},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DHS-qest07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DHS-qest07.pdf},
  doi = {10.1109/QEST.2007.14},
  abstract = {The stochastic temporal logic CSL can be used to
    describe formally properties of continuous-time Markov
    chains, and has been extended with expressions over states
    and actions to obtain the logic asCSL. However, properties 
    referring to the probability of a finite sequence of timed
    events (such~as {"}with probability at least~\(0.75\), the~system 
    will be in state set~\(A\) at time~\(5\), then in state set~\(B\)
    at time~\(7\), then in state set~\(C\) at time~\(20\){"}) cannot 
    be expressed in either CSL or asCSL. With the aim of increasing 
    the expressive power of temporal logics for continuous-time 
    Markov chains, we introduce the logic CSL\textsuperscript{TA} 
    and its model-checking algorithm. CSL\textsuperscript{TA} extends 
    CSL and asCSL by allowing the specification of timed properties 
    through a deterministic one-clock timed automata.}
}
@inproceedings{BCFH-qest07,
  address = {Edinburgh, Scotland, UK},
  month = sep,
  year = 2007,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{QEST}'07},
  booktitle = {{P}roceedings of the 4th {I}nternational
               {C}onference on {Q}uantitative 
               {E}valuation of {S}ystems
               ({QEST}'07)},
  author = {Beccuti, Marco and Codetta{-}Raiteri, Daniele and
                  Franceschinis, Giuliana and Haddad, Serge},
  title = {A Framework to Design and Solve {M}arkov Decision Well-formed
                  Net Models},
  pages = {165-166},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFH-qest07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFH-qest07.pdf},
  doi = {10.1109/QEST.2007.2}
}
@inproceedings{SMH-incom06,
  address = {Saint-{\'E}tienne, France},
  month = may,
  year = 2006,
  editor = {Dolgui, Alexandre and Morel, G{\'e}rard and Pereira,
                  Carlos E.},
  acronym = {{INCOM}'06},
  booktitle = {{P}roceedings of the 12th {IFAC} Symposium on Information Control
                  Problems in Manufacturing ({INCOM}'06)},
  author = {Sene, Mbaye and Moreaux, Patrice and Haddad, Serge},
  title = {Performance Evaluation Of Distributed Database~-- A~Banking
                  System Case Study},
  pages = {351-356},
  abstract = {This paper presents a case study of performance evaluation of a
	distributed database system made of a real banking system with several
	branches interconnected via a Wide Area Network (WAN). Due to the
	complexity of such systems, we use Stochastic Well Formed Petri nets
	(a high level stochastic Petri net model) to model its activities; the
	model obtained allows us to compute performance indices of the system.
	This is done by taking into account the dimensional parameters, the
	behaviour of the clients submitting requests and the number of
	clients, the WAN contention and the locality level of the database
	which enables us to consider the local and remote write requests.
	Synthesizing these various results, we propose configuration settings
	matching given workloads and system structures.}
}
@inproceedings{BH-jfdlpa07,
  address = {Toulouse, France},
  month = mar,
  year = 2007,
  noeditor = {Douence, R{\'e}mi and Fradet, Pascal},
  acronym = {{JFDLPA}'07},
  booktitle = {{A}ctes des 3{\`e}mes {J}ourn{\'e}es
           {F}rancophones sur le D{\'e}veloppement de Logiciels Par Aspects
           ({JFDLPA}'07)},
  author = {Ben{ }Hmida, Mehdi and Haddad, Serge},
  title = {Vers une adaptabilit{\'e} dynamique des architectures
                  orient{\'e}es services},
  pages = {73-88},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BH-jfdlpa07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BH-jfdlpa07.pdf},
  abstract = {Currently, Web Services are the fitted technical solution to
                  implement Service Oriented Architecture~(SOA). However, this
                  technology presents limitations concerning dynamic service
                  adaptabilty. From one side, Web Services providers have no
                  mean to dynamically adapt an existing Web Service to
                  business requirements changes. From the other side, Web
                  Services clients have no way to dynamically adapt themselves
                  to the service changing in order to avoid execution
                  failures. In this paper, we show how we achieve a dynamic
                  adaptable SOA by introducing the Aspect Oriented
                  Programming~(AOP) paradigm and Process Algebra~(PA).We apply
                  the main AOP concepts (joinpoint, pointcut and advice) in
                  the Web Service context to modify the behaviour of an
                  existent Web Service without touching its implementation.
                  Then, we~propose a Process Algebra formalism to specify a
                  change-prone BPEL process (base service and aspect services)
                  and shows how to generate automatically a client which
                  dynamically adapt its behaviour to the service changes}
}
@incollection{DH-afsec08,
  author = {Donatelli, Susanna and Haddad, Serge},
  title = {V{\'e}rification quantitative de cha{\^\i}nes de {M}arkov},
  booktitle = {Approches formelles des syst{\`e}mes embarqu{\'e}s communicants},
  editor = {Roux, Olivier H. and Jard, Claude},
  publisher = {Herm{\`e}s},
  year = 2008,
  month = oct,
  pages = {177-198},
  chapter = 6,
  url = {http://www.lavoisier.fr/notice/fr335499.html},
  futureisbn = {}
}
@misc{dots-3.1,
  author = {Bollig, Benedikt and Bouyer, Patricia and Cassez, Franck and
                  Chatain, {\relax Th}omas and Gastin, Paul and Haddad, Serge
                  and Jard, Claude},
  title = {Model for distributed timed systems},
  howpublished = {Deliverable DOTS~3.1 (ANR-06-SETI-003)},
  year = 2008,
  month = sep
}
@inproceedings{BCFH-valuetools08,
  address = {Athens, Greece},
  month = oct,
  year = 2008,
  publisher = {Institute for Computer Sciences, Social-Informatics and 
   	Telecommunications Engineering},
  editor = {Chahed, Tijani and Toumpis, Stavros and Yechiali, Uri},
  acronym = {{VALUETOOLS}'08},
  booktitle = {{P}roceedings of the 3rd {I}nternational {C}onference 
	   on {P}erformance {E}valuation {M}ethodologies and {T}ools
           ({VALUETOOLS}'08)},
  author = {Beccuti, Marco and Codetta{-}Raiteri, Daniele and
		 Franceschinis, Giuliana and Haddad, Serge},
  title = {Non Deterministic Repairable Fault Trees for Computing
                  Optimal Repair Strategy},
  nopages = {},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFH-valuetools08.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFH-valuetools08.pdf},
  doi = {10.4108/ICST.VALUETOOLS2008.4411},
  abstract = {In~this paper, the Non deterministic Repairable Fault
    Tree~(NdRFT) formalism is proposed: it allows to model failure modes of
    complex systems as well as their repair processes. The originality of this
    formalism with respect to other Fault Tree extensions is that it allows to
    face repair strategies optimization problems: in~an NdRFT model, the
    decision on whether to start or not a given repair action is non
    deterministic, so that all the possibilities are left open. The formalism
    is rather powerful allowing to specify which failure events are
    observable, whether local repair or global repair can be applied, and the
    resources needed to start a repair action. The optimal repair strategy can
    then be computed by solving an optimization problem on a Markov Decision
    Process~(MDP) derived from the NdRFT. A~software framework is proposed in
    order to perform in automatic way the derivation of an MDP from a NdRFT
    model, and to deal with the solution of the MDP.}
}
@inproceedings{BHHKT-wodes08,
  address = {Gothenburg, Sweden},
  month = may,
  year = 2008,
  acronym = {{WODES}'08},
  booktitle = {{P}roceedings of the 9th {W}orkshop on {D}iscrete {E}vent {S}ystems
	   ({WODES}'08)},
  author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge and Hillah, Lom
                  Messan and Kordon, Fabrice and Thierry{-}Mieg, Yann},
  title = {Collision Avoidance in Intelligent Transport Systems: Towards
                  an Application of Control Theory},
  pages = {346-351},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHHKT-wodes08.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHHKT-wodes08.pdf},
  doi = {10.1109/WODES.2008.4605970},
  abstract = {Safety is a prevalent issue in Intelligent Transport
    Systems~(ITS). To~ensure such a vital requirement, methodologies must
    offer support for the careful design and analysis of such systems. Indeed
    these steps must cope with temporal and spatial constraints associated
    with mobility rules and parallelism which induce a high complexity. Here
    we handle the problem of unexpected and uncontrollable vehicles which
    significantly endanger the traffic. In~this context, we~propose to apply
    discrete control theory to a model of automatic motorway in order to
    synthesize a controller that handles collision avoidance. This approach
    includes two parts: the design of a formal model and an efficient
    implementation based on hierarchical decision diagrams.}
}
@incollection{HM-mvrts08,
  author = {Haddad, Serge and Moreaux, Patrice},
  title = {Verification of Probabilistic Systems Methods and 
		Tools},
  booktitle = {Modeling and Verification of Real-Time Systems},
  editor = {Merz, Stephan and Navet, Nicolas},
  year = {2008},
  month = jan,
  pages = {289-318},
  publisher = {ISTE Ltd. -- John Wiley \& Sons, Ltd.},
  url = {http://www.lavoisier.fr/notice/fr1848210130.html}
}
@article{BCHLR08-tcs,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {B{\'e}rard, B{\'e}atrice and Cassez, Franck and Haddad,
                  Serge and Lime, Didier and Roux, Olivier H.},
  title = {When are Timed Automata Weakly Timed Bisimilar to Time
                  {P}etri Nets?},
  year = 2008,
  month = sep,
  volume = 403,
  number = {2-3},
  pages = {202-220},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCHLR-tcs08.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCHLR-tcs08.pdf},
  doi = {10.1016/j.tcs.2008.03.030},
  abstract = {In this paper, we compare Timed Automata~(TA) and Time Petri
    Nets~(TPN) with respect to weak timed bisimilarity. It~is already known
    that the class of bounded TPNs is strictly included in the class of~TA.
    It~is thus natural to try and identify the
    subclass~\(\mathcal{TA}^{\textit{wtb}}\) of~TA equivalent to some TPN for
    the weak timed bisimulation relation. We~give a characterization of this
    subclass and we show that the membership problem and the reachability
    problem for \(\mathcal{TA}^{\textit{wtb}}\) are PSPACE-complete.
    Furthermore we show that for a TA in~\(\mathcal{TA}^{\textit{wtb}}\) with
    integer constants, an~equivalent TPN can be built with integer bounds but
    with a size exponential w.r.t.~the original model. Surprisingly, using
    rational bounds yields a TPN whose size is linear.}
}
@inproceedings{HMY-csndsp08,
  address = {Graz, Austria},
  month = jul,
  year = 2008,
  publisher = {{IEEE} Computer Society Press},
  noeditor = {},
  acronym = {{CSNDSP}'08},
  booktitle = {{P}roceedings of the 6th {S}ymposium on {C}ommunication {S}ystems,
                  {N}etworks and {D}igital {S}ignal {P}rocessing
		  ({CSNDSP}'08)},
  author = {Haddad, Serge and Mokdad, Lynda and Youcef, Samir},
  title = {Response Time Analysis of Composite Web Services},
  pages = {506-510},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/HMY-csndsp08.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HMY-csndsp08.pdf},
  abstract = {Service Oriented Computing (SOC) strives for applications with
    services as the fundamental items of design, and Web services acting as
    the enabling technology. Web services use open XML-based standards and are
    becoming the most important technology for communication between
    heterogenous business applications over Internet. In this paper, we focus
    on mean response times. Thus we propose analytical formulas for mean
    response times for structured BPEL constructors such as sequence, flow and
    switch. We propose also a response time formula for multi-choice pattern
    which is a generalization of switch constructor. Contrarily to previous
    studies in the literature, we consider that the servers can be
    heterogenous and the number of invoked elementary Web services can be
    variable.}
}
@incollection{DH-CES09,
  author = {Donatelli, Susanna and Haddad, Serge},
  title = {Quantitative Verification of {M}arkov Chains},
  booktitle = {Communicating Embedded Systems~-- Software and Design},
  editor = {Jard, Claude and Roux, Olivier H.},
  publisher = {Wiley-ISTE},
  year = 2009,
  month = oct,
  pages = {139-163},
  chapter = 5,
  url = {http://www.iste.co.uk/index.php?f=x&ACTION=View&id=288},
  nops = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/.ps},
  nopsgz = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PSGZ/.ps.gz},
  isbn = {9781848211438}
}
@article{BCHMMR-ijwsr09,
  publisher = {{IGI} Publishing},
  journal = {International Journal of Web Services Research},
  author = {Boutrous{-}Saab, C{\'e}line and Coulibaly, Demba and Haddad, Serge
                and Melliti, Tarek and Moreaux, Patrice and Rampacek, Sylvain},
  title = {An Integrated Framework for Web Services Orchestration},
  volume = 6,
  number = 4,
  pages = {1-29},
  year = 2009,
  month = sep,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCHMMR-ijwsr09.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCHMMR-ijwsr09.pdf},
  abstract = {Currently, Web services give place to active research and this
    is due both to industrial and theoretical factors. On one hand, Web
    services are essential as the design model of applications dedicated to
    the electronic business. On the other hand, this model aims to become one
    of the major formalisms for the design of distributed and cooperative
    applications in an open environment (the Internet). In this article, the
    authors will focus on two features of Web services. The first one concerns
    the interaction problem: given the interaction protocol of a Web service
    described in BPEL, how to generate the appropriate client? Their approach
    is based on a formal semantics for BPEL via process algebra and yields an
    algorithm which decides whether such a client exists and synthesizes the
    description of this client as a (timed) automaton. The second one concerns
    the design process of a service. They propose a method which proceeds by
    two successive refinements: first the service is described via UML, then
    refined in a BPEL model and finally enlarged with JAVA code using JCSWL, a
    new language that we introduce here. Their solutions are integrated in a
    service development framework that will be presented in a synthetic way.}
}
@incollection{HI-petrinet-diaz,
  year = 2009,
  publisher = {Wiley-ISTE},
  editor = {Diaz, Michel},
  booktitle = {Petri Nets: Fundamental Models, Verification and Applications},
  author = {Haddad, Serge and Ili{\'e}, Jean-Michel},
  title = {Symmetry and Temporal Logic},
  pages = {435-460},
  url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html}
}
@incollection{HV-petrinet-diaz-b,
  year = 2009,
  publisher = {Wiley-ISTE},
  editor = {Diaz, Michel},
  booktitle = {Petri Nets: Fundamental Models, Verification and Applications},
  author = {Haddad, Serge and Vernadat, Fran{\c{c}}ois},
  title = {Verification of Specific Properties},
  pages = {349-414},
  url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html}
}
@incollection{HM-petrinet-diaz-c,
  year = 2009,
  publisher = {Wiley-ISTE},
  editor = {Diaz, Michel},
  booktitle = {Petri Nets: Fundamental Models, Verification and Applications},
  author = {Haddad, Serge and Moreaux, Patrice},
  title = {Tensor Methods and Stochastic {P}etri Nets},
  pages = {321-346},
  url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html}
}
@incollection{HM-petrinet-diaz-b,
  year = 2009,
  publisher = {Wiley-ISTE},
  editor = {Diaz, Michel},
  booktitle = {Petri Nets: Fundamental Models, Verification and Applications},
  author = {Haddad, Serge and Moreaux, Patrice},
  title = {Stochastic Well-formed {P}etri Nets},
  pages = {303-320},
  url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html}
}
@incollection{HM-petrinet-diaz-a,
  year = 2009,
  publisher = {Wiley-ISTE},
  editor = {Diaz, Michel},
  booktitle = {Petri Nets: Fundamental Models, Verification and Applications},
  author = {Haddad, Serge and Moreaux, Patrice},
  title = {Stochastic {P}etri Nets},
  pages = {269-302},
  url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html}
}
@incollection{H-petrinet-diaz,
  year = 2009,
  publisher = {Wiley-ISTE},
  editor = {Diaz, Michel},
  booktitle = {Petri Nets: Fundamental Models, Verification and Applications},
  author = {Haddad, Serge},
  title = {Decidability and Complexity of {P}etri Net Problems},
  pages = {87-122},
  url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html}
}
@incollection{HV-petrinet-diaz-a,
  year = 2009,
  publisher = {Wiley-ISTE},
  editor = {Diaz, Michel},
  booktitle = {Petri Nets: Fundamental Models, Verification and Applications},
  author = {Haddad, Serge and Vernadat, Fran{\c{c}}ois},
  title = {Analysis Methods for {P}etri Nets},
  pages = {41-86},
  url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html}
}
@inproceedings{ZBH-lads09,
  address = {Turin, Italy},
  year = 2010,
  volume = 6039,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Dastani, Mehdi and El~Fallah Seghrouchni, Amal and Leite, Jo{\~a}o
                  and Torroni, Paolo},
  acronym = {{LADS}'09},
  booktitle = {{R}evised {S}elected {P}apers of the 2nd {W}orkshop on {LA}nguages, methodologies and
                  {D}evelopment tools for multi-agent system{S} ({LADS}'09)},
  author = {Zargayouna, Mahdi and Balbo, Flavien and Haddad, Serge},
  title = {Agents Secure Interaction in Data Driven Languages},
  pages = {72-91},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ZBH-lads09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ZBH-lads09.pdf},
  doi = {10.1007/978-3-642-13338-1_5},
  abstract = {This paper discusses the security issues in data driven
    coordination languages. These languages rely on a data space shared by the
    agents and used to coordinate their activities. We extend these languages
    with a main distinguishing feature, which is the possibility to define
    fine-grained security conditions, associated with every datum in the
    shared space. Two main ideas makes it possible: the consideration of an
    abstraction of agents' states in the form of data at language level and
    the introduction of a richer interaction mechanism than state-of-the-art
    templates. This novel security mechanism allows both agents and system
    designers to prohibit undesirable interactions.}
}
@techreport{LSV:09:16,
  author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge and Sassolas, Mathieu},
  title = {Verification on Interrupt Timed Automata},
  institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  year = {2009},
  month = jul,
  type = {Research Report},
  number = {LSV-09-16},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-16.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-16.pdf},
  note = {16~pages},
  abstract = {The class of Interrupt Timed Automata (ITA) has been introduced to
 model multi-task systems with interruptions in a single processor
 environment.  This is a subclass of hybrid automata in which real
 valued variables consist of a restricted type of stopwatches
 (variables with rate \(0\) or~\(1\)) organized along levels. While
 reachability is undecidable with usual stopwatches, it was proved
 that this problem is decidable in ITA and that untimed languages of
 ITA are effectively regular. Here we investigate the problem of
 model checking timed extensions of CTL over ITA and show in
 contrast that this problem is undecidable. On~the other hand, we
 prove that model checking is decidable for two relevant fragments of this
 timed logic: (1)~the~first one where formula contain only model
 clocks and (2)~the~second one where formulas have a single external
 clock.}
}
@inproceedings{HMY-msr09,
  address = {Nantes, France},
  month = nov,
  year = 2009,
  number = {7-9},
  volume = {43},
  series = {Journal Europ{\'e}en des Syst{\`e}mes Automatis{\'e}s},
  publisher = {Herm{\`e}s},
  editor = {Lime, Didier and Roux, Olivier H.},
  acronym = {{MSR}'09},
  booktitle = {{A}ctes du 7{\`e}me {C}olloque sur la 
               {M}od{\'e}lisation des {S}yst{\`e}mes
               {R}{\'e}actifs
               ({MSR}'09)},
  author = {Haddad, Serge and Mokdad, Lynda and Youcef, Samir},
  title = {Bornes du temps de r{\'e}ponse des services Web composites},
  pages = {969-983},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HMY-msr09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HMY-msr09.pdf},
  abstract = {The quality of service (QoS) of Web services is a key
    factor of their success. This requires to design new methods in order to
    study~it. Here we propose families of upper bounding models for the
    response time of composite Web services for two kinds of composition: the
    statical and random {"}fork and merge{"}. In~the first~case, the~complexity of
    bounding models belongs to~\(O(n\cdot \sqrt{n})\) where \(n\)~is the
    number of called services whereas the complexity of the exact model
    belongs to~\(O(n^2)\). In~the second~case, the~complexity of bounding
    models still belongs to~\(O(n\cdot \sqrt{n})\) whereas the complexity of
    the exact model belongs to~\(O(n^3)\). Furthermore, having a family of
    bounding models allows to choose the bounding model depending on the
    parameters of the exact model. The numerical results show the interest of
    our approach w.r.t. complexity and accuracy of the bound.}
}
@inproceedings{HP-qest09,
  address = {Budapest, Hungary},
  month = sep,
  year = 2009,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{QEST}'09},
  booktitle = {{P}roceedings of the 6th {I}nternational
               {C}onference on {Q}uantitative 
               {E}valuation of {S}ystems
               ({QEST}'09)},
  author = {Haddad, Serge and Pekergin, Nihal},
  title = {Using Stochastic Comparison for Efficient
		Model Checking of Uncertain {M}arkov Chains},
  pages = {177-186},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HP-qest09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HP-qest09.pdf},
  doi = {10.1109/QEST.2009.42},
  abstract = {We consider model checking of Discrete Time Markov Chains~(DTMC)
    with transition probabilities which are not exactly known but lie in a
    given interval. Model checking a Probabilistic Computation Tree
    Logic~(PCTL) formula for interval-valued DTMCs~(IMC) has been shown to be
    NP hard and co-NP hard. Since the state space of a realistic DTMC is
    generally huge, these lower bounds prevent the application of exact
    algorithms for such models. Therefore we propose to apply the stochastic
    comparison method to check an extended version of PCTL for IMCs. More
    precisely, we first design linear time algorithms to quantitatively
    analyze IMCs. Then we develop an efficient, semi-decidable PCTL model
    checking procedure for IMCs. Furthermore, our procedure returns more
    refined answers than traditional ones: YES, NO, DON'T~KNOW. Thus we may
    provide useful partial information for modelers in the {"}DON'T~KNOW{"}
    case.}
}
@incollection{EFH-tsmaai09,
  author = {El~Fallah Seghrouchni, Amal and Haddad, Serge},
  title = {Interop{\'e}rabilit{\'e} des syst{\`e}mes multi-agents 
		{\`a} l'aide des services web},
  booktitle = {Technologies des syst{\`e}mes multi-agents et 
		 applications industrielles},
  editor = {El~Fallah Seghrouchni, Amal and Briot, Jean-Pierre},
  publisher = {Herm{\`e}s},
  year = 2009,
  month = apr,
  pages = {77-99},
  chapter = 3,
  url = {http://www.lavoisier.fr/notice/fr2746217850.html},
  nops = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/.ps},
  nopsgz = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PSGZ/.ps.gz},
  futureisbn = {}
}
@inproceedings{HKPPT-acc09,
  address = {Saint Louis, Missouri, USA},
  month = jun,
  year = 2009,
  acronym = {{ACC}'09},
  booktitle = {{P}roceedings of the 28th {A}merican {C}ontrol 
	       {C}onference ({ACC}'09)},
  author = {Haddad, Serge and Kordon, Fabrice and Petrucci, Laure and 
		Pradat{-}Peyre, Jean-Fran{\c{c}}ois and Tr{\`e}ves, Nicolas},
  title = {Efficient State-Based Analysis by Introducing Bags in 
		{P}etri Nets Color Domains},
  pages = {5018-5025},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HKPPT-acc09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HKPPT-acc09.pdf},
  doi = {10.1109/ACC.2009.5160020},
  abstract = {The use of high-level nets, such as coloured Petri nets, is very
    convenient for modelling complex controllable systems in order to have a
    compact, readable and structured specification. However, when coming to
    the analysis phase, using too elaboratc types becomes a burden.\par
    A good trade-off between expressivene and analy is capabilities is then to
    have only imple types, which is achieved with symmetric nels. These latter
    nels enjoy the possibility of generating a symbolic reachability gralph,
    which is much smallcr than the whole state space and still allows for
    exhaustive analysis.\par
    In this paper, we extend the symmetric net model with bags on arcs. Hence,
    variables can be bags of tokens,leading to more flexible models. We show
    that symmetric nets with bags also allow for applying the symbolic
    reachability graph technique with application to deadlock detection and
    more generally for safety properties.}
}
@article{DHS-tose09,
  publisher = {{IEEE} Computer Society Press},
  journal = {IEEE Transactions on Software Engineering},
  author = {Donatelli, Susanna and Haddad, Serge and Sproston, Jeremy},
  title = {Model Checking Timed and Stochastic Properties with {CSL\textsuperscript{TA}}},
  volume = 35,
  number = 2,
  month = mar # {-} # apr,
  year = 2009,
  pages = {224-240},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DHS-tose09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DHS-tose09.pdf},
  doi = {10.1109/TSE.2008.108},
  abstract = {Markov chains are a well-known stochastic process that provide
    a balance between being able to adequately model the system's behavior and
    being able to afford the cost of the model solution. Systems can be
    modelled directly as Markov chains, or with a higher-level formalism for
    which Markov chains represent the underlying semantics. Markov chains are
    widely used to study the performance of computer and telecommunication
    systems. The definition of stochastic temporal logics like Continuous
    Stochastic Logic~(CSL) and its variant~asCSL, and of their model-checking
    algorithms, allows a unified approach to the verification of systems,
    allowing the mix of performance evaluation and probabilistic verification.
    \par
    In this paper we present the stochastic logic CSL\textsuperscript{TA} ,
    which is more expressive than CSL and~asCSL, and in which properties can
    be specified using automata (more precisely, timed automata with a single
    clock). The extension with respect to expressiveness allows the
    specification of properties referring to the probability of a finite
    sequence of timed events. A~typical example is the responsiveness property
    {"}with probability at least~0.75, a~message sent at time~0 by a
    system~\(A\) will be received before time~5 by system~\(B\) and the
    acknowledgment will be back at~\(A\) before time~7{"}, a property that
    cannot be expressed in either CSL or~asCSL. Furthermore, the choice of
    using automata rather than the classical temporal operators Next and Until
    should help in enlarging the accessibility of model checking to a larger
    public. We~also present a model-checking algorithm
    for~CSL\textsuperscript{TA}.}
}
@article{BHR-fi09,
  publisher = {{IOS} Press},
  journal = {Fundamenta Informaticae},
  author = {Bouyer, Patricia and Haddad, Serge and Reynier, Pierre-Alain},
  title = {Undecidability Results for Timed Automata with Silent
		   Transitions},
  year = 2009,
  volume = 92,
  number = {1-2},
  pages = {1-25},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-12.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-12.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
        rr-lsv-2007-12.ps},
  abstract = {In this work, we study decision problems related to timed
    automata with silent transitions (TA-epsilon) which strictly extend the
    expressiveness of timed automata~(TA). First, we answer negatively a
    central question raised by the introduction of silent transitions: can we
    decide whether the language recognized by a TA-epsilon can be recognized
    by some TA? Then we establish in the framework of TA-epsilon some old open
    conjectures that O.~Finkel has recently solved for~TA. Its proofs follow a
    generic scheme which relies on the fact that only a finite number of
    configurations can be reached by a TA while reading a timed word. This
    property does not hold for TA-epsilon, the proofs in the framework of
    TA-epsilon thus require more elaborated arguments. We~establish
    undecidability of complementability, minimization of the number of clocks,
    and closure under shuffle. We~also show these results in the framework of
    infinite timed languages.}
}
@inproceedings{BH-Fossacs09,
  address = {York, UK},
  month = mar,
  year = 2009,
  volume = 5504,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {de Alfaro, Luca},
  acronym = {{FoSSaCS}'09},
  booktitle = {{P}roceedings of the 12th {I}nternational
               {C}onference on {F}oundations of {S}oftware {S}cience
               and {C}omputation {S}tructures
               ({FoSSaCS}'09)},
  author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge},
  title = {Interrupt Timed Automata},
  pages = {197-211},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BH-fossacs09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BH-fossacs09.pdf},
  doi = {10.1007/978-3-642-00596-1_15},
  abstract = {In this work, we introduce the class of Interrupt Timed Automata
    (ITA), which are well suited to the description of multi-task systems with
    interruptions in a single processor environment. This model is a subclass
    of hybrid automata. While reachability is undecidable for hybrid automata
    we show that in ITA the reachability problem is in 2EXPSPACE and in PSPACE
    when the number of clocks is fixed, with a procedure based on a
    generalized class graph. Furthermore we consider a subclass ITA\(_{-}\)
    which still describes usual interrupt systems and for which the
    reachability problem is in NEXPTIME and in NP when the number of clocks is
    fixed (without any class graph). There exist languages accepted by an
    ITA\(_{-}\) but neither by timed automata nor by controlled real-time
    automata (CRTA), another extension of timed automata. However we
    conjecture that CRTA is not contained in ITA. So, we combine ITA with CRTA
    in a model which encompasses both classes and show that the reachability
    problem is still decidable.}
}
@techreport{rr-lsv-10-23,
  author = {Bonnet, R{\'e}mi and Finkel, Alain and Haddad, Serge and
                  Rosa{-}Velardo, Fernando},
  title = {Comparing Petri Data Nets and Timed Petri Nets},
  institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  year = {2010},
  month = dec,
  type = {Research Report},
  number = {LSV-10-23},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-23.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-23.pdf},
  note = {16~pages},
  abstract = {Well-Structured Transitions Systems (WSTS) constitute a generic
    class of infinite-state systems for which several properties like
    coverability remain decidable. The family of coverability languages that
    they generate is an appropriate criterium for measuring their
    expressiveness. Here we establish that Petri Data nets (PDNs) and Timed
    Petri nets (TdPNs), two powerful classes of WSTS are equivalent w.r.t this
    criterium.}
}
@article{bbdfh-pe10,
  publisher = {Elsevier Science Publishers},
  journal = {Performance Evaluation},
  author = {Baarir, Souheib and Beccuti, Marco and Dutheillet, Claude and
  	 	 Franceschinis, Giuliana and Haddad, Serge},
  title = {Lumping partially symmetrical stochastic models},
  volume = 76,
  nunmber = 1,
  month = jan,
  pages = {21-44},
  year = 2011,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/bbdfh-pe10.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bbdfh-pe10.pdf},
  doi = {10.1016/j.peva.2010.09.002},
  abstract = {The performance and dependability evaluation of complex systems
    by means of dynamic stochastic models (e.g. Markov chains) may be impaired
    by the combinatorial explosion of their state space. Among the possible
    methods to cope with this problem, symmetry-based ones can be applied to
    systems including several similar components. Often however these systems
    are only partially symmetric: their behavior is in general symmetric
    except for some local situation when the similar components need to be
    differentiated.\par 
    In this paper two methods to efficiently analyze partially symmetrical
    models are presented in a general setting and the requirements for their
    efficient implementation are discussed. Some case studies are presented to
    show the methods' effectiveness and their applicative interest.}
}
@inproceedings{hmy-bpsc10,
  address = {Leipzig, Germany},
  month = sep # {-} # oct,
  year = 2010,
  volume = {177},
  series = {Lecture Notes in Informatics},
  publisher = {Gesellschaft f{\"u}r Informatik},
  editor = {Abramowicz, Witold and Alt, Rainer and F{\"a}hnrich, Klaus-Peter
                  and Franczyk, Bogdan and Maciaszek, Leszek A.},
  acronym = {{ISSS}{\slash}{BPSC}'10},
  booktitle = {{P}roceedings of the 2nd {I}nternational {S}ymposium on {S}ervices
                  {S}cience and 3rd {I}nternational {C}onference on {B}usiness 
		  {P}rocess and {S}ervices {C}omputing 
		  ({ISSS}{\slash}{BPSC}'10)},
  author = {Haddad, Serge and Mokdad, Lynda and Youcef, Samir},
  title = {Selection of the Best composite Web Service Based on Quality
                  of Service},
  pages = {255-266},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/hmy-bpsc10.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/hmy-bpsc10.pdf},
  abstract = {The paper proposes a general framework to composite Web services
    selection based on multicriteria evaluation. The proposed framework
    extends the Web services architecture by adding, in the registry, a new
    Multicriteria Evaluation Component~(MEC) devoted to multicriteria
    evaluation. This additional component takes as input a set of composite
    Web services and a set of evaluation criteria and generates a set of
    recommended composite Web services. In~addition to the description of the
    conceptual architecture of the formwork, the paper also proposes solutions
    to construct and evaluate composite web services. In order to show the
    feasibility of the proposed architecture, we~have developed a prototype
    based on the open source jUDDI registry.}
}
@techreport{rr-lsv-10-17,
  author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge and Sassolas,
  	 	 Mathieu and Zeitoun, Marc},
  title = {Distributed Synthesis with Incomparable Information},
  institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  year = {2010},
  month = oct,
  type = {Research Report},
  number = {LSV-10-17},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-17.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-17.pdf},
  note = {20~pages},
  abstract = {Given (1)~an architecture defined by processes and communication
    channels between them or with the environment, and (2)~a~specification on
    the messages transmitted over the channels, distributed synthesis aims at
    deciding existence of local programs, one for each process, that together
    meet the specification, whatever the environment does. Recent work shows
    that this problem can be solved when a \emph{linear preorder} sorts the
    agents w.r.t. the information received from the environment.\par
    In this paper we show a new decidability result in the case where this
    preorder is broken by the addition of noisy agents embedded in a pipeline
    architecture. This case cannot be captured by the classical framework.
    Besides, this architecture makes it possible to model particular security
    threats, known as covert channels, where two users (the sender and the
    receiver) manage to communicate via a noisy protocol, and despite
    incomparable views over the environment.}
}
@inproceedings{BFCH-dsn09,
  address = {Estoril, Portugal},
  month = jun # {-} # jul,
  year = 2009,
  publisher = {{IEEE} Computer Society Press},
  noeditor = {},
  acronym = {{DSN}'09},
  booktitle = {{P}roceedings of the 39th {A}nnual {IEEE}{\slash}{IFIP}
                  {I}nternational {C}onference on {D}ependable {S}ystems and
                  {N}etworks ({DSN}'09)},
  author = {Beccuti, Marco and Franceschinis, Giuliana and
                  Codetta{-}Raiteri, Daniele and Haddad, Serge},
  title = {Parametric {NdRFT} for the derivation of optimal repair
                  strategies},
  pages = {399-408},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFCH-dsn09.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFCH-dsn09.pdf},
  doi = {10.1109/DSN.2009.5270312},
  abstract = {Non deterministic Repairable Fault Trees~(NdRFT) are a recently
    proposed modeling formalism for the study of optimal repair strategies:
    they are based on the widely adopted Fault Tree formalism, but in addition
    to the failure modes, NdRFTs allow to define possible repair actions. In a
    previous pa per the formalism has been introduced together with an
    analysis method and a tool allowing to automatically derive the best
    repair strategy to be applied in each state. The analysis technique is
    based on the generation and solution of a Markov Decision Process. In this
    paper we present an extension, ParNdRFT, that allows to exploit the
    presence of redundancy to reduce the complexity of the model and of the
    analysis. It is based on the translation of the ParNdRFT in to a Markov
    Decision Well-Formed Net, i.e. a model specified by means of an High Level
    Petri Net formalism. The translated model can be efficiently solved thanks
    to existing algorithms that generate a reduced state space automatically
    exploiting the model symmetries.}
}
@inproceedings{EHH-apnoc10,
  address = {Braga, Portugal},
  month = jun,
  year = 2010,
  editor = {Sidorova, Natalia and Serebrenik, Alexander},
  acronym = {{APNOC}'10},
  booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop on
                  {A}bstractions for {P}etri {N}ets and {O}ther {M}odels of
                  {C}oncurrency ({APNOC}'10)},
  author = {El{~}Hog{-}Benzina, Dorsaf and Haddad, Serge and Hennicker, Rolf},
  title = {Process Refinement and Asynchronous Composition with Modalities},
  nopages = {},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/EHH-apnoc10.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/EHH-apnoc10.pdf},
  abstract = {We propose a framework for the specification of infinite state
    systems based on Petri nets with distinguished may- and must-transitions
    (called modalities) which specify the allowed and the required behavior of
    refinements and hence of implementations. Formally, refinements are
    defined by relating the modal language specifications generated by two
    modal Petri nets according to the refinement relation for modal language
    specifications. We show that this refinement relation is decidable if the
    underlying modal Petri nets are weakly deterministic. We also show that
    the membership problem for the class of weakly deterministic modal Petri
    nets is decidable. As an important application of our approach we consider
    I/O-Petri nets which are obtained by asynchronous composition and thus
    exhibit inherently an infinite behavior.}
}
@inproceedings{BHS-time10,
  address = {Paris, France},
  month = sep,
  year = 2010,
  publisher = {{IEEE} Computer Society Press},
  editor = {Markey, Nicolas and Wijsen, Jef},
  acronym = {{TIME}'10},
  booktitle = {{P}roceedings of the 17th {I}nternational {S}ymposium on 
	       {T}emporal {R}epresentation and {R}easoning
	       ({TIME}'10)},
  author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge and Sassolas, Mathieu},
  title = {Real Time Properties for Interrupt Timed Automata},
  pages = {69-76},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHS-time10.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHS-time10.pdf},
  doi = {10.1109/TIME.2010.11},
  abstract = {Interrupt Timed Automata (ITA) have been introduced to model
    multi-task systems with interruptions. They form a~subclass of stopwatch
    automata, where the real valued variables (with rate \(0\) or~\(1\)) are
    organized along priority levels. While reachability is undecidable with
    usual stopwatches, the problem was proved decidable for~ITA. In~this work,
    after giving answers to some questions left open about expressiveness,
    closure, and complexity for~ITA, our~main purpose is to investigate the
    verification of real time properties over~ITA. While we prove that model
    checking a variant of the timed logic TCTL is undecidable, we nevertheless
    give model checking procedures for two relevant fragments of this logic:
    one where formulas contain only model clocks and another one where
    formulas have a single external clock.}
}
@inproceedings{HMY-iscc10,
  address = {Riccione, Italy},
  month = jun,
  year = 2010,
  publisher = {{IEEE} Computer Society Press},
  noeditor = {},
  acronym = {{ISCC}'10},
  booktitle = {{P}roceedings of the 15th {IEEE} {S}ymposium on {C}omputers and
		{C}ommunications ({ISCC}'10)},
  author = {Haddad, Serge and Mokdad, Lynda and Youcef, Samir},
  title = {Response time of {BPEL4WS} constructors},
  pages = {695-700},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/HMY-iscc10.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HMY-iscc10.pdf},
  doi = {10.1109/ISCC.2010.5546538},
  abstract = {Response time is an important factor for every software system
    and it becomes more salient when it is associated with introducing novel
    technologies, such as Web services. Most performance evaluation of Web
    services are focused toward composite Web services and their response
    time. One important limitation of existing work is in the fact that only
    constant or service exponential time distribution are considered. However,
    experimental results have shown that the Web services response times is
    typically heavy-tailed, in particulary, if there are heterogeneous. So,
    heavy-tailed response times should be considered in the dimensioning Web
    services. In this study, we propose analytical formulas for mean response
    times for structured BPEL constructors such as \emph{sequence},
    \emph{flow} and \emph{switch} constructors,~etc. The difference with
    previous studies in the literature, is that we consider heterogenous
    servers, the number of invoked elementary Web services can be variable and
    the elementary Web services response times are heavy-tailed.}
}
@inproceedings{BH-monterey2008,
  address = {Budapest, Hungary},
  month = apr,
  year = 2010,
  volume = 6028,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Choppy, {\relax Ch}ristine and Sokolsky, Oleg},
  acronym = {{MONTEREY}'08},
  booktitle = {{R}evised {S}elected {P}apers of the 15th {M}onterey 
           {W}orkshop on {F}oundations
	   of {C}omputer {S}oftware ({MONTEREY}'08)},
  author = {Ben{ }Hmida, Mehdi and Haddad, Serge},
  title = {Client Synthesis for Aspect Oriented Web Services},
  pages = {24-42},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BH-monterey08.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BH-monterey08.pdf},
  doi = {10.1007/978-3-642-12566-9_2},
  abstract = {Client synthesis for complex Web services is a critical and
                  still open topic as it will enable more flexibility in the
                  deployment of such services. In previous works, our team has
                  developed a theoretical framework based on process algebra
                  that has led to algorithms and tools for the client
                  interaction. Here, we show how to generalise our approach
                  for aspect oriented Web services.}
}
@article{RHS-ijfcs09,
  publisher = {World Scientific},
  journal = {International Journal of Foundations of Computer Science},
  author = {Recalde, Laura and Haddad, Serge and Silva, Manuel},
  title = {Continuous {P}etri Nets: Expressive Power and Decidability Issues},
  volume = 21,
  number = 2,
  pages = {235-256},
  year = 2010,
  month = apr,
  doi = {10.1142/S0129054110007222},
  abstract = {State explosion is a fundamental problem in the analysis and
    synthesis of discrete event systems. Continuous Petri nets can be seen as
    a relaxation of the corresponding discrete model. The expected gains are
    twofold: improvements in complexity and in decidability. In the case of
    autonomous nets we prove that liveness or deadlock-freeness remain
    decidable and can be checked more efficiently than in Petri nets. Then we
    introduce time in the model which now behaves as a dynamical system driven
    by differential equations and we study it w.r.t. expressiveness and
    decidability issues. On the one hand, we prove that this model is
    equivalent to timed differential Petri nets which are a slight extension
    of systems driven by linear differential equations~(LDE). On~the other
    hand, (contrary to the systems driven by~LDEs) we show that continuous
    timed Petri nets are able to simulate Turing machines and thus that basic
    properties become undecidable.}
}
@inproceedings{BHP-tacas12,
  address = {Tallinn, Estonia},
  month = mar,
  year = 2012,
  volume = {7214},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Flanagan, Cormac and K{\"o}nig, Barbara},
  acronym = {{TACAS}'12},
  booktitle = {{P}roceedings of the 18th {I}nternational 
               {C}onference on {T}ools and {A}lgorithms for
               {C}onstruction and {A}nalysis of {S}ystems
               ({TACAS}'12)},
  author = {Barbot, Beno{\^\i}t and Haddad, Serge and Picaronny, Claudine},
  title = {Coupling and Importance Sampling for Statistical Model Checking},
  pages = {331-346},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHP-tacas12.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHP-tacas12.pdf},
  doi = {10.1007/978-3-642-28756-5_23},
  abstract = {Statistical model-checking is an alternative verification
    technique applied on stochastic systems whose size is beyond numerical
    analysis ability. Given a model (most often a Markov chain) and a formula,
    it provides a confidence interval for the probability that the model
    satisfies the formula. One of the main limitations of the statistical
    approach is the computation time explosion triggered by the evaluation of
    very small probabilities. In order to solve this problem we develop a new
    approach based on importance sampling and coupling. The corresponding
    algorithms have been implemented in our tool cosmos. We present
    experimentation on several relevant systems, with estimated time
    reductions reaching a factor of~\(10^{120}\).}
}
@incollection{haddad-DS11b,
  author = {Haddad, Serge},
  title = {Introduction to Verification},
  booktitle = {Models and Analysis in Distributed Systems},
  editor = {Haddad, Serge and Kordon, Fabrice and Pautet, Laurent and
                  Petrucci, Laure},
  publisher = {John Wiley \& Sons, Ltd.},
  chapter = 6,
  pages = {137-154},
  year = 2011
}
@inproceedings{BHP-msr11,
  address = {Lille, France},
  month = nov,
  year = 2011,
  number = {1-3},
  volume = {45},
  series = {Journal Europ{\'e}en des Syst{\`e}mes Automatis{\'e}s},
  publisher = {Herm{\`e}s},
  editor = {Craye, {\'E}tienne and Gamati{\'e}, Abdoulaye},
  acronym = {{MSR}'11},
  booktitle = {{A}ctes du 8{\`e}me {C}olloque sur la 
               {M}od{\'e}lisation des {S}yst{\`e}mes
               {R}{\'e}actifs
               ({MSR}'11)},
  author = {Barbot, Beno{\^\i}t and Haddad, Serge and Picaronny, Claudine},
  title = {{\'E}chantillonnage pr{\'e}f{\'e}rentiel pour le model checking statistique},
  pages = {237-252},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-msr11.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-msr11.pdf},
  doi = {10.3166/jesa.45.237-252},
  abstract = {The statistical model checking can be usefully substituted for
    numerical model checking when the models to be studied are huge. However
    the statistical approach cannot evaluate too small probabilities. In order
    to solve the problem, we develop here a new approach based on importance
    sampling. While most of the techniques related to importance sampling are
    based on heuristics, we establish theoretical results under some
    hypotheses. These results ensure a reduction of the variance during
    application of importance sampling. We also characterize situations that
    fulfill the hypotheses and we extend our approach for handling other
    situations but then without theoretical guarantee. We have implemented
    this approach with the tool \textsc{Cosmos} after some extensions. At~last
    we have evaluated this approach for two examples and analysed the
    experimentations.}
}
@inproceedings{BDDHP-case11,
  address = {Trieste, Italy},
  month = aug,
  year = 2011,
  publisher = {{IEEE} Robotics \& Automation Society},
  noeditor = {},
  acronym = {{CASE}'11},
  booktitle = {{P}roceedings of the 7th {IEEE} {C}onference on {A}utomation 
           {S}cience and {E}ngineering ({CASE}'11)},
  author = {Ballarini, Paolo and Djafri, Hilal and Duflot, Marie and 
                 Haddad, Serge and Pekergin, Nihal},
  title = {{P}etri Nets Compositional Modeling and Verification
                  of Flexible Manufacturing Systems},
  pages = {588-593},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDDHP-case11.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDDHP-case11.pdf},
  doi = {10.1109/CASE.2011.6042488},
  abstract = {Flexible Manufacturing Systems (FMS) are amongst the
                  most studied types of systems, however due to their
                  increasing complexity, there is still room for
                  improvement in their modeling and analysis. In this
                  paper we consider the design and the analysis of
                  stochastic models of FMS in two complementary
                  respects.  First we describe a (stochastic) Petri
                  Nets based compositional framework which enables to
                  model an FMS by combination of an arbitrary number
                  of basic components. Second we demonstrate how
                  classical transient-analysis of manufacturing
                  systems, including reliability and performability
                  analysis, can be enriched by application of a novel,
                  sophisticated stochastic logic, namely the Hybrid
                  Automata Stochastic Logic (HASL). We demonstrate the
                  proposed methodology on an FMS example.}
}
@inproceedings{BDDHP-qest11,
  address = {Aachen, Germany},
  month = sep,
  year = 2011,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{QEST}'11},
  booktitle = {{P}roceedings of the 8th {I}nternational
               {C}onference on {Q}uantitative 
               {E}valuation of {S}ystems
               ({QEST}'11)},
  author = {Ballarini, Paolo and Djafri, Hilal and Duflot, Marie and 
                 Haddad, Serge and Pekergin, Nihal},
  title = {{COSMOS}: a~Statistical Model Checker for the
                  Hybrid Automata Stochastic Logic},
  pages = {143-144},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDDHP-qest11.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDDHP-qest11.pdf},
  doi = {10.1109/QEST.2011.24},
  abstract = {This tool paper introduces COSMOS, a statistical model
                  checker for the Hybrid Automata Stochastic Logic
                  (HASL). HASL employs Linear Hybrid Automata (LHA), a
                  generalization of Deterministic Timed Automata
                  (DTA), to describe accepting execution paths of a
                  Discrete Event Stochastic Process (DESP), a class of
                  stochastic models which includes, but is not limited
                  to, Markov chains. As a result HASL verification
                  turns out to be a unifying framework where
                  sophisticated temporal reasoning is naturally
                  blended with elaborate reward-based analysis. COSMOS
                  takes as input a DESP (described in terms of a
                  Generalized Stochastic Petri Net), an LHA and an
                  expression~\(Z\) representing the quantity to be
                  estimated. It returns a confidence interval
                  estimation of~\(Z\). COSMOS is written in C++ and is
                  freely available to the research community.}
}
@article{BFH-ijpe11,
  publisher = {RAMS Consultants},
  journal = {International Journal of Performability Engineering},
  author = {Beccuti, Marco and Franceschinis, Giuliana and Haddad, Serge},
  title = {{MDWN}solver: A~Framework to Design and Solve {M}arkov Decision {P}etri Nets},
  year = {2011},
  month = sep,
  volume = 7,
  number = 5,
  pages = {417-428},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFH-ijpe11.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFH-ijpe11.pdf},
  abstract = {MDWNsolver is a framework for system modeling and optimization
    of performability measures based on Markov Decision Petri Net (MDPN) and
    Markov Decision Well-formed Net (MDWN) formalisms, two Petri Net
    extensions for high level specification of Markov Decision Processes
    (MDP). It is integrated in the GreatSPN suite which provides a GUI to
    design MDPN/MDWN models. From the analysis point of view, MDWNsolver uses
    efficient algorithms that take advantage of system symmetries, thus
    reducing the analysis complexity. In this paper the MDWNsolver framework
    features and architecture are presented, and some application examples are
    discussed.}
}
@inproceedings{HMN-atpn11,
  address = {Newcastle upon Tyne, UK},
  month = jun,
  year = 2011,
  volume = {6709},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Kristensen, Lars M. and Petrucci, Laure},
  acronym = {{PETRI~NETS}'11},
  booktitle = {{P}roceedings of the 32nd
               {I}nternational {C}onference on
               {A}pplications and {T}heory of {P}etri {N}ets
               ({PETRI~NETS}'11)},
  author = {Haddad, Serge and Mairesse, Jean and Nguyen, Hoang-Thach},
  title = {Synthesis and Analysis of Product-form {P}etri Nets},
  pages = {288-307},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/HMN-atpn11.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HMN-atpn11.pdf},
  doi = {10.1007/978-3-642-21834-7_16},
  abstract = {For a large Markovian model, a {"}product form{"} is an explicit
    description of the steady-state behaviour which is otherwise generally
    untractable. Being first introduced in queueing networks, it has been
    adapted to Markovian Petri nets. Here we address three relevant issues for
    product-form Petri nets which were left fully or partially open:
    (1)~we~provide a sound and complete set of rules for the synthesis;
    (2)~we~characterise the exact complexity of classical problems like
    reachability; (3)~we~introduce a new subclass for which the normalising
    constant (a crucial value for product-form expression) can be efficiently
    computed.}
}
@inproceedings{BDDHP-valuetools11,
  address = {Cachan, France},
  month = may,
  year = 2011,
  acronym = {{VALUETOOLS}'11},
  booktitle = {{P}roceedings of the 5th {I}nternational {C}onference 
	   on {P}erformance {E}valuation {M}ethodologies and {T}ools
           ({VALUETOOLS}'11)},
  author = {Ballarini, Paolo and Djafri, Hilal and Duflot, Marie and
  	 	 Haddad, Serge and Pekergin, Nihal},
  title = {{HASL}: An~Expressive Language for Statistical Verification
                  of Stochastic Models},
  pages = {306-315},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDDHP-valuetools11.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDDHP-valuetools11.pdf},
  abstract = {We introduce the Hybrid Automata Stochastic Logic (HASL), a new
    temporal logic formalism for the verification of discrete event stochastic
    processes (DESP). HASL employs Linear Hybrid Automata (LHA) as machineries
    to select prefixes of relevant execution paths of a DESP~\(\mathcal{D}\).
    The advantage with LHA is that rather elaborate information can be
    collected \emph{on-the-fly} during path selection, providing the user with
    a powerful means to express sophisticated measures. A formula of HASL
    consists of an LHA~\(\mathcal{A}\) and an expression~\(Z\) referring to
    moments of \emph{path random variables}. A~simulation-based statistical
    engine is employed to obtained a confidence-interval estimate of the
    expected value of~\(Z\). In essence HASL provide a unifying verification
    framework where sophisticated temporal reasoning is naturally blended with
    elabo- rate reward-based analysis. We illustrate the HASL approach by
    means of some examples and a discussion about its expressivity. We also
    provide empirical evidence obtained through COSMOS, a prototype software
    tool for HASL verification.}
}
@inproceedings{BFHR-fossacs11,
  address = {Saarbr{\"u}cken, Germany},
  month = mar # {-} # apr,
  year = 2011,
  volume = {6604},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Hofmann, Martin},
  acronym = {{FoSSaCS}'11},
  booktitle = {{P}roceedings of the 14th {I}nternational
               {C}onference on {F}oundations of {S}oftware {S}cience
               and {C}omputation {S}tructures
               ({FoSSaCS}'11)},
  author = {Bonnet, R{\'e}mi and Finkel, Alain and Haddad, Serge and
                  Rosa{-}Velardo, Fernando},
  title = {Ordinal Theory for Expressiveness of Well Structured Transition Systems},
  pages = {153-167},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHR-fossacs11.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHR-fossacs11.pdf},
  doi = {10.1007/978-3-642-19805-2_11}
}
@article{BFHR-icomp13,
  publisher = {Elsevier Science Publishers},
  journal = {Information and Computation},
  author = {Bonnet, R{\'e}mi and Finkel, Alain and Haddad, Serge and
  	 	 Rosa{-}Velardo, Fernando},
  title = {Ordinal Theory for Expressiveness of Well-Structured
                  Transition Systems},
  year = 2013,
  month = mar,
  volume = 224,
  pages = {1-22},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHR-icomp12.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHR-icomp12.pdf},
  doi = {10.1016/j.ic.2012.11.003},
  abstract = {We characterize the importance of resources (like counters,
    channels, or alphabets) when measuring the expressiveness of
    Well-Structured Transition Systems~(WSTS). We establish, for usual classes
    of well partial orders, the equivalence between the existence of order
    reflections (non-monotonic order embeddings) and the simulations with
    respect to coverability languages. We show that the non-existence of order
    reflections can be proved by the computation of order types. This allows
    us to extend the current classification of WSTS, in particular solving
    some open problems, and to unify the existing proofs.}
}
@article{BCHLR-tcs13,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {B{\'e}rard, B{\'e}atrice and Cassez, Franck and Haddad, Serge
                  and Lime, Didier and Roux, Olivier~H.},
  title = {The Expressive Power of Time {P}etri Nets},
  year = 2013,
  month = feb,
  volume = 474,
  ftturenumber = {},
  pages = {1-20},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCHLR-tcs12.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCHLR-tcs12.pdf},
  doi = {10.1016/j.tcs.2012.12.005},
  abstract = {We investigate expressiveness questions for time Petri nets
    (TPNs) and some their most usefull extensions. We first introduce
    generalised time Petri nets (GTPNs) as an abstract model that encompasses
    variants of TPNs such as self modifications and read, reset and inhibitor
    arcs.\par
    We give a syntactical translation from bounded GTPNs to timed automata
    (TA) that generates isomorphic transition systems. We prove that the class
    of bounded GTPNs is stricly less expressive than TA w.r.t. weak timed
    bisimilarity. We prove that bounded GTPNs, bounded TPNs and TA are equally
    expressive w.r.t. timed language acceptance. Finally, we characterise a
    syntactical subclass of TA that is equally expressive to bounded GTPNs
    {"}\`a~la Merlin{"} w.r.t. weak timed bisimilarity. These results provide
    a unified comparison of the expressiveness of many variants of timed
    models often used in practice. It leads to new important results for TPNs.
    Among them are: 1-safe TPNs and bounded-TPNs are equally expressive;
    \(\epsilon\)-transitions strictly increase the expressive power of TPNs;
    self modifying nets as well as read, inhibitor and reset arcs do not add
    expressiveness to bounded TPNs.}
}
@inproceedings{BHP-simul12,
  address = {Lisbon, Portugal},
  month = nov,
  year = 2012,
  publisher = {XPS},
  editor = {Dini, Petre and Lorenz, Pascal},
  acronym = {{SIMUL}'12},
  booktitle = {{P}roceedings of the 4th {I}nternational {C}onference on {A}dvances in
                  {S}ystem {S}imulation ({SIMUL}'12)},
  author = {Barbot, Beno{\^\i}t and Haddad, Serge and Picaronny, Claudine},
  title = {Importance Sampling for Model Checking of Continuous Time
                  {M}arkov Chains},
  pages = {30-35},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHP-simul12.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHP-simul12.pdf},
  abstract = {Model checking real time properties on probabilistic systems
    requires computing transient probabilities on continuous time Markov
    chains. Beyond numerical analysis ability, a probabilistic framing can
    only be obtained using simulation. This statistical approach fails when
    directly applied to the estimation of very small probabilities. Here
    combining the uniformization technique and extending our previous results,
    we design a method which applies to continuous time Markov chains and
    formulas of a timed temporal logic. The corresponding algorithm has been
    implemented in our tool \textsc{cosmos}. We present experimentations on a
    relevant system, with drastic time reductions with respect to standard
    statistical model checking.}
}
@misc{impro-D2.1,
  author = {Akshay, S. and B{\'e}rard, B{\'e}atrice and Bouyer, Patricia
                  and Haar, Stefan and Haddad, Serge and Jard, Claude and
		  Lime, Didier and Markey, Nicolas and Reynier, Pierre-Alain
                  and Sankur, Ocan and Thierry-Mieg, Yann},
  title = {Overview of Robustness in Timed Systems},
  howpublished = {Deliverable ImpRo D~2.1 (ANR-2010-BLAN-0317)},
  year = 2012,
  month = jan,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d21.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d21.pdf}
}
@inproceedings{HSS-lics2012,
  address = {Dubrovnik, Croatia},
  month = jun,
  year = 2012,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{LICS}'12},
  booktitle = {{P}roceedings of the 27th
               {A}nnual {IEEE} {S}ymposium on
               {L}ogic in {C}omputer {S}cience
               ({LICS}'12)},
  author = {Haddad, Serge and Schmitz, Sylvain and Schnoebelen, {\relax Ph}ilippe},
  title = {The Ordinal-Recursive Complexity of Timed-Arc {P}etri
                     Nets, Data Nets, and Other Enriched Nets},
  pages = {355-364},
  url = {http://hal.archives-ouvertes.fr/hal-00793811},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HSS-lics12.pdf},
  doi = {10.1109/LICS.2012.46},
  abstract = {We show how to reliably compute fast-growing functions
                  with timed-arc Petri nets and data nets. This
                  construction provides ordinal-recursive lower bounds
                  on the complexity of the main decidable properties
                  (safety, termination, regular simulation,~etc.) of
                  these models. Since these new lower bounds match the
                  upper bounds that one can derive from wqo theory,
                  they precisely characterise the computational power
                  of these so-called {"}enriched{"} nets.}
}
@inproceedings{BHSS-concur12,
  address = {Newcastle, UK},
  month = sep,
  year = 2012,
  volume = 7454,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Koutny, Maciej and Ulidowski, Irek},
  acronym = {{CONCUR}'12},
  booktitle = {{P}roceedings of the 23rd
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'12)},
  author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge and Sassolas,
                  Mathieu and Sznajder, Nathalie},
  title = {Concurrent Games on~{VASS} with Inhibition},
  pages = {39-52},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHSS-CONCUR12.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHSS-CONCUR12.pdf},
  doi = {10.1007/978-3-642-32940-1_5},
  abstract = {We propose to study concurrent games on a new extension of
    Vector Addition Systems with States, where inhibition conditions are added
    for modeling purposes. Games are a well-suited framework to solve control
    problems, and concurrent semantics reflect realistic situations where the
    environment can always produce a move before the controller, although it
    is never required to do so. This is in contrast with previous works, which
    focused mainly on turn-based semantics. Moreover, we consider asymmetric
    games, where environment and controller do not have the same capabilities,
    although they both have restricted power. In this setting, we investigate
    reachability and safety objectives, which are not dual to each other
    anymore, and we prove that (i)~reachability games are undecidable for
    finite targets, (ii)~they are 2-EXPTIME-complete for upward-closed targets
    and (iii)~safety games are co-NP-complete for finite, upward-closed and
    semi-linear targets. Moreover, for the decidable cases, we build a finite
    representation of the corresponding controllers.}
}
@incollection{topnoc12-ehh,
  year = 2012,
  volume = 6900,
  series = {Lecture Notes in Computer Science},
  editor = {Jensen, Kurt and Donatelli, Susanna and Kleijn, Jetty},
  publisher = {Springer},
  booktitle = {Transactions on {P}etri Nets and Other Models of Concurrency~{V}},
  author = {El{~}Hog{-}Benzina, Dorsaf and Haddad, Serge and Hennicker, Rolf},
  title = {Refinement and Asynchronous Composition of Modal {P}etri Nets},
  pages = {96-120},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/topnoc12-ehh.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/topnoc12-ehh.pdf},
  doi = {10.1007/978-3-642-29072-5_4},
  abstract = {We propose a framework for the specification of infinite state
    systems based on Petri nets with distinguished \emph{may}- and
    \emph{must}-transitions (called modalities) which specify the allowed and
    the required behavior of refinements and hence of implementations. For any
    modal Petri net, we define its generated modal language specification
    which abstracts away silent transitions. On this basis we consider
    refinements of modal Petri nets by relating their generated modal language
    specifications. We show that this refinement relation is decidable if the
    underlying modal Petri nets are weakly deterministic. We also show that
    the membership problem for the class of weakly deterministic modal Petri
    nets is decidable. As an important application scenario of our approach we
    consider I/O-Petri nets and their asynchronous composition which typically
    leads to an infinite state system.}
}
@techreport{rr-lsv-12-04,
  author = {Barbot, Beno{\^\i}t and Haddad, Serge and Picaronny, Claudine},
  title = {Importance Sampling for Model Checking of Time-Bounded Until},
  institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  year = {2012},
  month = feb,
  type = {Research Report},
  number = {LSV-12-04},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2012-04.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2012-04.pdf},
  versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2012-04-v1.pdf, 20120227},
  note = {14~pages},
  abstract = {Statistical model-checking is an alternative verification
    technique applied on stochastic systems whose size is beyond numerical
    analysis ability. Given a model (most often a Markov chain) and a formula,
    it provides a confidence interval for the probability that the model
    satisfies the formula. In a previous contribution, we have overtaken the
    main limitation of the statistical approach, i.e. the computation time
    explosion associated with the evaluation of very small probabilities. This
    method was valid only for the standard ``Until'' of temporal logics. We
    establish a similar validity condition which applies to the ``Bounded
    Until'', using more elaborate arguments. We also address the problem of
    additional memory requirements necessary to apply the method and we design
    several algorithms depending on the intended trade-off between time and
    memory. The corresponding algorithms have been implemented in our tool
    Cosmos. We present experimentations on several relevant systems, with
    drastic time reductions w.r.t. standard statistical model checking.}
}
@article{BHS-fmsd2012,
  publisher = {Springer},
  journal = {Formal Methods in System Design},
  author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge and Sassolas, Mathieu},
  title = {Interrupt Timed Automata: Verification and Expressiveness},
  year = {2012},
  month = feb,
  volume = {40},
  number = {1},
  pages = {41-87},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHS-fmsd12.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHS-fmsd12.pdf},
  doi = {10.1007/s10703-011-0140-2},
  abstract = {We introduce the class of Interrupt Timed Automata (ITA), a
    subclass of hybrid automata well suited to the description of timed
    multi-task systems with interruptions in a single processor environment.\par
    While the reachability problem is undecidable for hybrid automata we show
    that it is decidable for ITA. More precisely we prove that the untimed
    language of an ITA is regular, by building a finite automaton as a
    generalized class graph. We then establish that the reachability problem
    for ITA is in NEXPTIME and in PTIME when the number of clocks is fixed. To
    prove the first result, we define a subclass ITA\(_{-}\) of ITA, and show
    that (1)~any ITA can be reduced to a language-equivalent automaton in
    ITA\(_{-}\) and (2)~the reachability problem in this subclass is in NEXPTIME
    (without any class graph).\par
    In the next step, we investigate the verification of real time properties
    over ITA. We prove that model checking SCL, a fragment of a timed linear
    time logic, is undecidable. On the other hand, we give model checking
    procedures for two fragments of timed branching time logic.\par
    We also compare the expressive power of classical timed automata and ITA
    and prove that the corresponding families of accepted languages are
    incomparable. The result also holds for languages accepted by controlled
    real-time automata (CRTA), that extend timed automata. We finally combine
    ITA with CRTA, in a model which encompasses both classes and show that the
    reachability problem is still decidable. Additionally we show that the
    languages of ITA are neither closed under complementation nor under
    intersection.}
}
@inproceedings{HHMS-fsttcs13,
  address = {Guwahati, India},
  month = dec,
  year = 2013,
  volume = {24},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Seth, Anil and Vishnoi, Nisheeth},
  acronym = {{FSTTCS}'13},
  booktitle = {{P}roceedings of the 33rd {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'13)},
  author = {Haar, Stefan and Haddad, Serge and Melliti, Tarek and Schwoon,
                  Stefan},
  title = {Optimal Constructions for Active Diagnosis},
  pages = {527-539},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/HHMS13-fsttcs.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HHMS13-fsttcs.pdf},
  doi = {10.4230/LIPIcs.FSTTCS.2013.527},
  abstract = {The task of diagnosis consists in detecting, without ambiguity,
    occurrence of faults in a partially observed system. Depending on the
    degree of observability, a discrete event system may be diagnosable or
    not. Active diagnosis aims at controlling the system in order to make it
    diagnosable. Solutions have already been proposed for the active diagnosis
    problem, but their complexity remains to be improved. We solve here the
    active diagnosability decision problem and the active diagnoser synthesis
    problem, proving that (1)~our procedures are optimal w.r.t. to
    computational complexity, and (2)~the memory required for the active
    diagnoser produced by the synthesis is minimal. Furthermore, focusing on
    the minimal delay before detection, we establish that the memory required
    for any active diagnoser achieving this delay may be highly greater than
    the previous one. So we refine our construction to build with the same
    complexity and memory requirement an active diagnoser that realizes a
    delay bounded by twice the minimal delay.}
}
@article{HMY-jocs13,
  publisher = {Elsevier Science Publishers},
  journal = {Journal of Computational Science},
  author = {Haddad, Serge and Mokdad, Lynda and Youcef, Samir},
  title = {Bounding models families for performance evaluation in composite
               Web services},
  volume = {4},
  number = {4},
  year = {2013},
  pages = {232-241},
  month = jul,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/HMY-jocs13.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HMY-jocs13.pdf},
  doi = {10.1016/j.jocs.2011.11.003},
  abstract = {One challenge of composite Web service architectures is the
    guarantee of the Quality of Service~(QoS). Performance evaluation of these
    architectures is essential but complex due to synchronizations inside the
    orchestration of services. We propose methods to automatically derive from
    the original model a family of bounding models for the composite Web
    response time. These models allow to find the appropriate trade-off
    between accuracy of the bounds and the computational complexity. The
    numerical results show the interest of our approach w.r.t. complexity and
    accuracy of the response time bounds.}
}
@inproceedings{BHJL-rp13,
  address = {Uppsala, Sweden},
  month = sep,
  year = 2013,
  volume = {8169},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Abdulla, Parosh Aziz and Potapov, Igor},
  acronym = {{RP}'13},
  booktitle = {{P}roceedings of the 7th {W}orkshop
           on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'13)},
  author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge and
                  Jovanovic, Aleksandra and Lime, Didier},
  title = {Parametric Interrupt Timed Automata},
  pages = {59-69},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHJL-rp13.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHJL-rp13.pdf},
  doi = {10.1007/978-3-642-41036-9_7},
  abstract = {Parametric reasoning is particularly relevant for timed models,
    but very often leads to undecidability of reachability problems. We
    propose a parametrised version of Interrupt Timed Automata (an~expressive
    model incomparable to Timed Automata), where polynomials of parameters can
    occur in guards and updates. We prove that different reachability
    problems, including robust reachability, are decidable for this model, and
    we give complexity upper bounds for a fixed or variable number of clocks
    and parameters.}
}
@inproceedings{ABHH-qest13,
  address = {Buenos Aires, Argentina},
  month = aug,
  year = 2013,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{QEST}'13},
  booktitle = {{P}roceedings of the 10th {I}nternational
               {C}onference on {Q}uantitative 
               {E}valuation of {S}ystems
               ({QEST}'13)},
  author = {Akshay, S. and Bertrand, Nathalie and Haddad, Serge and 
  	 	  H{\'e}lou{\"e}t, Lo{\"\i}c},
  title = {The steady-state control problem for Markov decision processes},
  pages = {290-304},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABHH-qest13.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABHH-qest13.pdf},
  doi = {10.1007/978-3-642-40196-1_26},
  abstract = {This paper addresses a control problem for probabilistic models
    in the setting of Markov decision processes~(MDP). We~are interested in
    the steady-state control problem which asks, given an ergodic MDP~\(M\)
    and a distribution~\(\delta_{\text{goal}}\), whether there exists a
    (history-dependent randomized) policy \(\pi\) ensuring that the
    steady-state distribution of~\(M\) under~\(\pi\) is
    exactly~\(\delta_{\text{goal}}\). We~first show that stationary randomized
    policies suffice to achieve a given steady-state distribution. Then we
    infer that the steady-state control problem is decidable for~MDP, and can
    be represented as a linear program which is solvable in PTIME. This
    decidability result extends to labeled MDP (LMDP) where the objective is a
    steady-state distribution on labels carried by the states, and we provide
    a PSPACE algorithm. We also show that a related steady-state language
    inclusion problem is decidable in EXPTIME for LMDP. Finally, we prove that
    if we consider MDP under partial observation (POMDP), the steady-state
    control problem becomes undecidable.}
}
@inproceedings{FH-pn13,
  address = {Milano, Italy},
  month = jun,
  year = 2013,
  volume = {7927},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Colom, Jos{\'e}-Manuel and Desel, J{\"o}rg},
  acronym = {{PETRI~NETS}'13},
  booktitle = {{P}roceedings of the 34th
               {I}nternational {C}onference on
               {A}pplications and {T}heory of {P}etri {N}ets
               ({PETRI~NETS}'13)},
  author = {Fraca, Est{\'\i}baliz and Haddad, Serge},
  title = { Complexity Analysis of Continuous {P}etri Nets},
  pages = {170-189},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/FH-pn13.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FH-pn13.pdf},
  doi = {10.1007/978-3-642-38697-8_10},
  abstract = {At the end of the eighties, continuous Petri nets were
    introduced for: (1)~alleviating the combinatory explosion triggered by
    discrete Petri nets and, (2)~modelling the behaviour of physical systems
    whose state is composed of continuous variables. Since then several works
    have established that the computational complexity of deciding some
    standard behavioural properties of Petri nets is reduced in this
    framework. Here we first establish the decidability of additional
    properties like boundedness and reachability set inclusion. We also design
    new decision procedures for the reachability and lim-reachability problems
    with a better computational complexity. Finally we provide lower bounds
    characterising the exact complexity class of the boundedness, the
    reachability, the deadlock freeness and the liveness problems.}
}
@inproceedings{HHM-pn13,
  address = {Milano, Italy},
  month = jun,
  year = 2013,
  volume = {7927},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Colom, Jos{\'e}-Manuel and Desel, J{\"o}rg},
  acronym = {{PETRI~NETS}'13},
  booktitle = {{P}roceedings of the 34th
               {I}nternational {C}onference on
               {A}pplications and {T}heory of {P}etri {N}ets
               ({PETRI~NETS}'13)},
  author = {Haddad, Serge and Hennicker, Rolf and M{\o}ller, Mikael H.},
  title = {Channel Properties of Asynchronously Composed {P}etri~Nets},
  pages = {369-388},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/HHM-pn13.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HHM-pn13.pdf},
  doi = {10.1007/978-3-642-38697-8_20},
  abstract = {We consider asynchronously composed I/O-Petri nets (AIOPNs) with
    built-in communication channels. They are equipped with a compositional
    semantics in terms of asynchronous I/O-transition systems (AIOTSs)
    admitting infinite state spaces. We study various channel properties that
    deal with the production and consumption of messages exchanged via the
    communication channels and establish useful relationships between them. In
    order to support incremental design we show that the channel properties
    considered in this work are preserved by asynchronous composition, i.e.
    they are compositional. As a crucial result we prove that the channel
    properties are decidable for AIOPNs.}
}
@article{HMN-fi13,
  publisher = {{IOS} Press},
  journal = {Fundamenta Informaticae},
  author = {Haddad, Serge and Mairesse, Jean and Nguyen, Hoang-Thach},
  title = {Synthesis and Analysis of Product-form {P}etri Nets},
  year = {2013},
  volume = {122},
  number = {1-2},
  pages = {147-172},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/HMN-fi13.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HMN-fi13.pdf},
  doi = {10.3233/FI-2013-786},
  abstract = {For a large Markovian model, a {"}product form{"} is an explicit
    description of the steady-state behaviour which is otherwise generally
    untractable. Being first introduced in queueing networks, it has been
    adapted to Markovian Petri nets. Here we address three relevant issues for
    product-form Petri nets which were left fully or partially open:
    (1)~we~provide a sound and complete set of rules for the synthesis;
    (2)~we~characterise the exact complexity of classical problems like
    reachability; (3)~we~introduce a new subclass for which the normalising
    constant (a~crucial value for product-form expression) can be efficiently
    computed.}
}
@article{BFCH-compj14,
  publisher = {Oxford University Press},
  journal = {The Computer Journal},
  author = {Beccuti, Marco and Franceschinis, Giuliana and
                  Codetta{-}Raiteri, Daniele and Haddad, Serge},
  title = {Computing Optimal Repair Strategies by Means of NdRFT
                  Modeling and Analysis},
  volume = 57,
  number = 12,
  month = dec,
  year = 2014,
  pages = {1870-1892},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFCH-compj14.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFCH-compj14.pdf},
  doi = {10.1093/comjnl/bxt134},
  abstract = {In this paper, the \emph{Non-deterministic Repairable Fault
    Tree}~(NdRFT) formalism is proposed: it allows the modeling of failures of
    complex systems in addition to their repair processes. Its originality
    with respect to other Fault Tree extensions allows us to address repair
    strategy optimization problems: in an NdRFT model, the decision as to
    whether to start or not a given repair action is non-deterministic, so
    that all the possibilities are left open. The formalism is rather
    powerful, it allows: the specification of self-revealing events, the
    representation of components degradation, the choice among local repair,
    global repair, preventive maintenance, and the specification of the
    resources needed to start a repair action. The optimal repair strategy
    with respect to some relevant system state function, e.g. system
    unavailability, can then be computed by solving an optimization problem on
    a Markov Decision Process derived from the NdRFT. Such derivation is
    obtained by converting the NdRFT model into an intermediate formalism
    called Markov Decision Petri Net~(MDPN). In the paper, the NdRFT syntax
    and semantics are formally described, together with the conversion rules
    to derive from the NdRFT the corresponding MDPN model. The application of
    NdRFT is illustrated through examples.}
}
@inproceedings{BHL-fsttcs14,
  address = {New~Dehli, India},
  month = dec,
  year = 2014,
  volume = {29},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Raman, Venkatesh and Suresh, S.~P.},
  acronym = {{FSTTCS}'14},
  booktitle = {{P}roceedings of the 34th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'14)},
  author = {Bertrand, Nathalie and Haddad, Serge and Lefaucheux, Engel},
  title = {Foundation of Diagnosis and Predictability in Probabilistic
                  Systems},
  pages = {417-429},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHL-fsttcs14.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHL-fsttcs14.pdf},
  doi = {10.4230/LIPIcs.FSTTCS.2014.417},
  abstract = {In discrete event systems prone to unobservable faults, a
    diagnoser must eventually detect fault occurrences. The diagnosability
    problem consists in deciding whether such a diagnoser exists. Here we
    investigate diagnosis for probabilistic systems modelled by partially
    observed Markov chains also called probabilistic labeled transition
    systems (pLTS). First we study different specifications of diagnosability
    and establish their relations both in finite and infinite pLTS. Then we
    analyze the complexity of the diagnosability problem for finite pLTS: we
    show that the polynomial time procedure earlier proposed is erroneous and
    that in fact for all considered specifications, the problem is
    PSPACE-complete. We also establish tight bounds for the size of
    diagnosers. Afterwards we consider the dual notion of predictability which
    consists in predicting that in a safe run, a fault will eventually occur.
    Predictability is an easier problem than diagnosability: it is
    NLOGSPACE-complete. Yet the predictor synthesis is as hard as the
    diagnoser synthesis. Finally we introduce and study the more flexible
    notion of prediagnosability that generalizes predictability and
    diagnosability.}
}
@inproceedings{BHHP-simul14,
  address = {Nice, France},
  month = oct,
  year = 2014,
  publisher = {XPS},
  editor = {Arisha, Amr and Bobashev, Georgiy},
  acronym = {{SIMUL}'14},
  booktitle = {{P}roceedings of the 6th {I}nternational {C}onference on {A}dvances in
                  {S}ystem {S}imulation ({SIMUL}'14)},
  author = {Barbot, Beno{\^\i}t and Haddad, Serge and Heiner, Monika
                    and Picaronny, Claudine},
  title = {Rare Event Handling in Signalling Cascades},
  pages = {126-131},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHHP-simul14.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHHP-simul14.pdf},
  abstract = {Signalling cascades are a recurrent pattern of biological
    regulatory systems whose analysis has deserved a lot of attention. It has
    been shown that stochastic Petri nets are appropriate to model such
    systems and evaluate the probabilities of specific properties. Such an
    evaluation can be done numerically when the combinatorial state space
    explosion is manageable or statistically otherwise. However, when the
    probabilities to be evaluated are too small, random simulation requires
    more sophisticated techniques for the handling of rare events. In this
    paper, we show how such involved methods can be successfully applied for
    signalling cascades. More precisely, we study three relevant properties of
    a signalling cascade with the help of the Cosmos tool. Our experiments
    point out interesting dependencies between quantitative parameters of the
    regulatory system and its transient behaviour. In addition, they
    demonstrate that we can go beyond the capabilities of Marcie which
    provides one of the most efficient numerical solvers.}
}
@inproceedings{HM-rp14,
  address = {Oxford, UK},
  month = sep,
  year = 2014,
  volume = {8762},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Ouaknine, Jo{\"e}l and Potapov, Igor and Worrell, James},
  acronym = {{RP}'14},
  booktitle = {{P}roceedings of the 8th {W}orkshop
           on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'14)},
  author = {Haddad, Serge and Monmege, Benjamin},
  title = {Reachability in {MDP}s: Refining Convergence of Value Iteration},
  pages = {125-137},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2014-07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2014-07.pdf},
  doi = {10.1007/978-3-319-11439-2_10},
  abstract = {Markov Decision Processes (MDP) are a widely used model
    including both non-deterministic and probabilistic choices. Minimal and
    maximal probabilities to reach a target set of states, with respect to a
    policy resolving non-determinism, may be computed by several methods
    including value iteration. This algorithm, easy to implement and efficient
    in terms of space complexity, consists in iteratively finding the
    probabilities of paths of increasing length. However, it raises three
    issues: (1)~defining a stopping criterion ensuring a bound on the
    approximation, (2)~analyzing the rate of convergence, and (3)~specifying
    an additional procedure to obtain the exact values once a sufficient
    number of iterations has been performed. The first two issues are still
    open and for the third one a {"}crude{"} upper bound on the number of
    iterations has been proposed. Based on a graph analysis and transformation
    of MDPs, we address these problems. First we introduce an interval
    iteration algorithm, for which the stopping criterion is straightforward.
    Then we exhibit convergence rate. Finally we significantly improve the
    bound on the number of iterations required to get the exact values.}
}
@inproceedings{BFHHH-fossacs14,
  address = {Grenoble, France},
  month = apr,
  year = 2014,
  volume = {8412},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Muscholl, Anca},
  acronym = {{FoSSaCS}'14},
  booktitle = {{P}roceedings of the 17th {I}nternational
               {C}onference on {F}oundations of {S}oftware {S}cience
               and {C}omputation {S}tructures
               ({FoSSaCS}'14)},
  author = {Bertrand, Nathalie and Fabre, {\'E}ric and Haar, Stefan and
                  Haddad, Serge and H{\'e}lou{\"e}t, Lo{\"\i}c},
  title = {Active diagnosis for probabilistic systems},
  pages = {29-42},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHHH-fossacs14.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHHH-fossacs14.pdf},
  doi = {10.1007/978-3-642-54830-7_4},
  abstract = {The diagnosis problem amounts to deciding whether some specific
    {"}fault{"} event occurred or not in a system, given the observations
    collected on a run of this system. This system is then diagnosable if the
    fault can always be detected, and the active diagnosis problem consists in
    controlling the system in order to ensure its diagnosability. We consider
    here a stochastic framework for this problem: once a control is selected,
    the system becomes a stochastic process. In this setting, the active
    diagnosis problem consists in deciding whether there exists some
    observation-based strategy that makes the system diagnosable with
    probability one. We prove that this problem is EXPTIME-complete, and that
    the active diagnosis strategies are belief-based. The safe active
    diagnosis problem is similar, but aims at enforcing diagnosability while
    preserving a positive probability to non faulty runs, i.e. without
    enforcing the occurrence of a fault. We prove that this problem requires
    non belief-based strategies, and that it is undecidable. However, it
    belongs to NEXPTIME when restricted to belief-based strategies. Our work
    also refines the decidability/undecidability frontier for verification
    problems on partially observed Markov decision processes.}
}
@inproceedings{HHM-tgc13,
  address = {Buenos Aires, Argentina},
  month = mar,
  year = 2014,
  volume = {8358},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Abadi, Mart{\'\i}n and Lluch{ }Lafuente, Alberto},
  acronym = {{TGC}'13},
  booktitle = {{R}evised {S}elected {P}apers of the 8th {S}ymposium on {T}rustworthy {G}lobal 
	   {C}omputing ({TGC}'13)},
  author = {Haddad, Serge and Hennicker, Rolf and M{\o}ller, Mikael H.},
  title = {Specification of Asynchronous Component Systems with 
  		 Modal {I}{{\slash}}{O}-{P}etri Nets},
  pages = {219-234},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/HHM-tgc13.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HHM-tgc13.pdf},
  doi = {10.1007/978-3-319-05119-2_13},
  abstract = {We consider Petri nets with distinguished labels for
    inputs, outputs, internal communications and silent actions and
    with {"}must{"} and {"}may{"} modalities for transitions. The
    input\slash output labels show the interaction capabilities of a
    net to the outside used to build larger nets by asynchronous
    composition via communication channels.  The modalities express
    constraints for Petri net refinement taking into account
    observational abstraction from silent transitions.  Modal
    I\slash O-Petri nets are equipped with a modal transition system
    semantics.  We show that refinement is preserved by asynchronous
    composition and by hiding of communication channels.  We study
    conformance properties which express communication requirements
    for composed systems and we show that those properties are
    preserved by refinement.  On this basis we propose a methodology
    for the specification of distributed systems in terms of modal
    I\slash O-Petri nets which supports incremental design, encapsulation of
    components and stepwise refinement.  Finally we show that our
    communication properties are decidable.}
}
@article{BHJL-fi15,
  publisher = {{IOS} Press},
  journal = {Fundamenta Informaticae},
  author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge and Jovanovi{\'c},
                  Aleksandra and Lime, Didier},
  title = {Interrupt Timed Automata with Auxiliary Clocks and Parameters},
  volume = {143},
  number = {3-4},
  pages = {235-259},
  month = mar,
  year = 2016,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHJL-fi15.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHJL-fi15.pdf},
  doi = {10.3233/FI-2016-1313},
  abstract = {Interrupt Timed Automata (ITA) are an expressive timed model,
    introduced to take into account interruptions according to levels. Due to
    this feature, this formalism is incomparable with Timed Automata.\par
    However several decidability results related to reachability and model
    checking have been obtained. We add auxiliary clocks to ITA, thereby
    extending its expressive power while preserving decidability of
    reachability. Moreover, we define a parametrized version of ITA, with
    polynomials of parameters appearing in guards and updates. While
    parametric reasoning is particularly relevant for timed models, it very
    often leads to undecidability results. We prove that various reachability
    problems, including robust reachability, are decidable for this model, and
    we give complexity upper bounds for a fixed or variable number of clocks,
    levels and parameters.}
}
@inproceedings{MLBHB-vecos15,
  address = {Bucharest, Romania},
  month = sep,
  year = 2015,
  volume = {1431},
  series = {CEUR Workshop Proceedings},
  publisher = {RWTH Aachen, Germany},
  editor = {Ben{~}Hedia, Belgacem and Popentiu{ }Vladicescu, Florin},
  acronym = {{VECoS}'15},
  booktitle = {{P}roceedings of the 9th {W}orkshop on {V}erification and
                  {E}valuation of {C}omputer and {C}ommunication
                  {S}ystems({VECoS}'15)},
  author = {Methni, Amira and Lemerre, Matthieu and Ben{~}Hedia,
                   Belgacem and Haddad, Serge and Barkaoui, Kamel},
  title = {State Space Reduction Strategie for Model Checking
                  Concurrent {C}~Programs},
  pages = {65-76},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/MLBHB-vecos15.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/MLBHB-vecos15.pdf},
  abstract = {Model checking is an effective technique for uncovering subtle
    errors in concurrent systems. Unfortunately, the state space explosion is
    the main bottleneck in model checking tools. Here we propose a state space
    reduction technique for model checking concurrent programs written in~C.
    The reduction technique consists in an analysis phase, which defines an
    approximate agglomeration predicate. This latter states whether a
    statement can be agglomerated or~not. We~implement this predicate using a
    syntactic analysis, as well as a semantic analysis based on abstract
    interpretation. We show the usefulness of using agglomeration technique to
    reduce the state space, as well as to generate an abstract TLA+
    specification from a~C~program.}
}
@inproceedings{BHHHS-cdc15,
  address = {Osaka, Japan},
  month = dec,
  year = 2015,
  publisher = {{IEEE} Control System Society},
  noeditor = {},
  acronym = {{CDC}'15},
  booktitle = {{P}roceedings of the 54th {IEEE} {C}onference on
                  {D}ecision and {C}ontrol ({CDC}'15)},
  author = {B{\"o}hm, Stanislav and Haar, Stefan and Haddad, Serge and
                  Hofman, Piotr and Schwoon, Stefan},
  title = {Active Diagnosis with Observable Quiescence},
  pages = {1663-1668},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHHHS-cdc15.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHHHS-cdc15.pdf},
  doi = {10.1109/CDC.2015.7402449},
  abstract = {Active diagnosis of a discrete-event system consists in
    controlling the system such that faults can be detected. Here we extend
    the framework of active diagnosis by introducing modalities for actions
    and states and a new capability for the controller, namely observing that
    the system is quiescent. We design a game-based construction for both the
    decision and the synthesis problems that is computationally optimal.
    Furthermore we prove that the size and the delay provided by the active
    diagnoser (when it exists) are almost optimal.}
}
@inproceedings{BHPSS-rp15,
  address = {Warsaw, Poland},
  month = sep,
  year = 2015,
  volume = {9328},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Boja{\'n}czyk, Miko{\l}aj and Lasota, S{\l}awomir and Potapov, Igor},
  acronym = {{RP}'15},
  booktitle = {{P}roceedings of the 9th {W}orkshop
           on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'15)},
  author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge and Picaronny,
                  Claudine and Safey{ }El{~}Din, Mohab and Sassolas, Mathieu},
  title = {Polynomial Interrupt Timed Automata},
  pages = {20-32},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHPSS-rp15.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHPSS-rp15.pdf},
  doi = {10.1007/978-3-319-24537-9_3},
  abstract = {Interrupt Timed Automata (ITA) form a subclass of stopwatch
    automata where reachability and some variants of timed model checking are
    decidable even in presence of parameters. They are well suited to model
    and analyze real-time operating systems. Here we extend ITA with
    polynomial guards and updates, leading to the class of polynomial ITA
    (PolITA). We prove that reachability is decidable in 2EXPTIME on PolITA,
    using an adaptation of the cylindrical decomposition method for the
    first-order theory of reals. Compared to previous approaches, our
    procedure handles parameters and clocks in a unified way. We also obtain
    decidability for the model checking of a timed version of CTL and for
    reachability in several extensions of PolITA.}
}
@inproceedings{MLBHB-ftscs15,
  address = {Luxembourg},
  optnmonth = 11,
  optmonth = nov,
  year = 2015,
  volume = {476},
  series = {Communications in Computer and Information Science},
  publisher = {Springer},
  editor = {Artho, Cyrille and {\"O}lveczky, Peter Csaba},
  acronym = {{FTSCS}'14},
  booktitle = {{P}roceedings of the 3rd {I}nternational {W}orkshop on {F}ormal {T}echniques for 
  {S}afety-{C}ritical {S}ystems, Nov. 2014 ({FTSCS}'14)},
  author = {Methni, Amira and Lemerre, Matthieu and Ben{~}Hedia, Belgacem and
                  Haddad, Serge and Barkaoui, Kamel},
  title = {Specifying and Verifying Concurrent {C}~Programs with {TLA+}},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/MLBHB-ftscs15.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/MLBHB-ftscs15.pdf},
  doi = {10.1007/978-3-319-17581-2_14},
  pages = {206-222},
  nonote = {17~pages},
  abstract = {Verifying software systems automatically from their source code
    rather than modelling them in a dedicated language gives more confidence
    in establishing their properties. Here we propose a formal specification
    and verification approach for concurrent C programs directly based on the
    semantics of~C. We define a set of translation rules and implement it in a
    tool~(C2TLA+) that automatically translates C code into a TLA+
    specification. The~TLC model checker can use this specification to
    generate a model, allowing to check the absence of runtime errors and dead
    code in the C program in a given configuration. In addition, we show how
    translated specifications interact with manually written ones~to: check
    the C code against safety or liveness properties; provide concurrency
    primitives or model hardware that cannot be expressed in~C; and use
    abstract versions of translated C functions to address the state explosion
    problem. All these verifications have been conducted on an industrial case
    study, which is a part of the microkernel of the PharOS real-time
    system.}
}
@article{FH-fundi15,
  publisher = {{IOS} Press},
  journal = {Fundamenta Informaticae},
  author = {Fraca, Est{\'\i}baliz and Haddad, Serge},
  title = {Complexity Analysis of Continuous Petri Nets},
  volume = 137,
  number = {1},
  pages = {1-28},
  year = 2015,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/FH-fundi15.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FH-fundi15.pdf},
  doi = {10.3233/FI-2015-1168},
  abstract = {At the end of the eighties, continuous Petri nets were
    introduced for: (1)~alleviating the combinatory explosion triggered by
    discrete Petri nets (i.e. usual Petri nets) and, (2)~modelling the
    behaviour of physical systems whose state is composed of continuous
    variables. Since then several works have established that the
    computational complexity of deciding some standard behavioural properties
    of Petri nets is reduced in this framework. Here we first establish the
    decidability of additional properties like coverability, boundedness and
    reachability set inclusion. We also design new decision procedures for
    reachability and lim-reachability problems with a better computational
    complexity. Finally we provide lower bounds characterising the exact
    complexity class of the reachability, the coverability, the boundedness,
    the deadlock freeness and the liveness problems. A~small case study is
    introduced and analysed with these new procedures.}
}
@article{BHHP-ijasm15,
  publisher = {IARIA},
  journal = {International Journal on Advances in Systems and Measurements},
  author = {Barbot, Beno{\^\i}t and Haddad, Serge and Heiner, Monika and
                  Picaronny, Claudine},
  title = {Rare Event Handling in Signalling Cascades},
  volume = 8,
  number = {1-2},
  pages = {69-79},
  year = 2015,
  month = jun,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHHP-ijasm15.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHHP-ijasm15.pdf},
  abstract = {Signalling cascades are a recurrent pattern of biological
    regulatory systems whose analysis has deserved a lot of attention. It has
    been shown that stochastic Petri nets are appropriate to model such
    systems and evaluate the probabilities of specific properties. Such an
    evaluation can be done numerically when the combinatorial state space
    explosion is manageable or statistically otherwise. However, when the
    probabilities to be evaluated are too small, random simulation requires
    more sophisticated techniques for the handling of rare events. In this
    paper, we show how such involved methods can be successfully applied for
    signalling cascades. More precisely, we study three relevant properties of
    a signalling cascade with the help of the COSMOS tool. Our experiments
    point out interesting dependencies between quantitative parameters of the
    regulatory system and its transient behaviour. In addition, they
    demonstrate that we can go beyond the capabilities of MARCIE, which
    provides one of the most efficient numerical solvers.}
}
@incollection{BH-im15,
  year = 2015,
  publisher = {CNRS \'Editions},
  editor = {Ollinger, Nicolas},
  booktitle = {Informatique Math{\'e}matique. Une~photographie en~2015},
  author = {Bertrand, Nathalie and Haddad, Serge},
  title = {Contr{\^o}le, probabilit{\'e}s et observation partielle},
  chapter = 5,
  pages = {177-227},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BH-im15.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BH-im15.pdf}
}
@article{BBDHP-peva15,
  publisher = {Elsevier Science Publishers},
  journal = {Performance Evaluation},
  author = {Ballarini, Paolo and Barbot, Beno{\^\i}t and Duflot, Marie and
                   Haddad, Serge and Pekergin, Nihal},
  title = {{HASL}: A~New Approach for Performance Evaluation and Model
                  Checking from Concepts to Experimentation},
  year = {2015},
  month = aug,
  volume = 90,
  pages = {53-77},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2015-04.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2015-04.pdf},
  doi = {10.1016/j.peva.2015.04.003},
  abstract = {We introduce the Hybrid Automata Stochastic Language (HASL), a
    new temporal logic formalism for the verification of Discrete Event
    Stochastic Processes (DESP). HASL employs a Linear Hybrid Automaton (LHA)
    to select prefixes of relevant execution paths of a DESP. LHA allows
    rather elaborate information to be collected \emph{on-the-fly} during path
    selection, providing the user with powerful means to express sophisticated
    measures. A~formula of HASL consists of an LHA and an expression~\(Z\)
    referring to moments of \emph{path random variables}. A~simulation-based
    statistical engine is employed to obtain a confidence interval estimate
    of the expected value of~\(Z\). In~essence, HASL~provides a unifying
    verification framework where temporal reasoning is naturally blended with
    elaborate reward-based analysis. Moreover, we have implemented a tool,
    named COSMOS, for performing analysis of HASL formula for DESP modelled by
    Petri nets. Using this tool we have developed two detailed case studies: a
    flexible manufacturing system and a genetic oscillator.}
}
@misc{qcover16,
  author = {Blondin, Michael and Finkel, Alain and Haase, Christoph and Haddad, Serge},
  title = {{QCover: an efficient coverability verifier for discrete and continuous Petri nets}},
  url = {https://github.com/blondimi/qcover},
  year = {2016}
}
@article{HHMS-jcss16,
  publisher = {Elsevier Science Publishers},
  journal = {Journal of Computer and System Sciences},
  author = {Stefan Haar and
               Serge Haddad and
               Tarek Melliti and
               Stefan Schwoon},
  title = {Optimal constructions for active diagnosis},
  pages = {101-120},
  volume = {83},
  number = {1},
  year = {2017},
  doi = {10.1016/j.jcss.2016.04.007},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HHMS-jcss16.pdf},
  abstract = {Diagnosis is the task of detecting fault occurrences in a partially observed sys- tem. Depending on the possible observations, a discrete-event system may be diagnosable or not. Active diagnosis aims at controlling the system to render it diagnosable. Past research has proposed solutions for this problem, but their complexity remains to be improved. Here, we solve the decision and synthesis problems for active diagnosability, proving that (1) our procedures are optimal with respect to computational complexity, and (2) the memory required for our diagnoser is minimal. We then study the delay between a fault occurrence and its detection by the diagnoser. We construct a memory-optimal diagnoser whose delay is at most twice the minimal delay, whereas the memory required to achieve optimal delay may be highly greater. We also provide a solution for parametrized active diagnosis, where we automatically construct the most permissive controller respecting a given delay.}
}
@inproceedings{BHL-concur16,
  address = {Qu{\'e}bec City, Canada},
  month = aug,
  year = 2016,
  volume = {59},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Desharnais, Jos{\'e}e and Jagadeesan, Radha},
  acronym = {{CONCUR}'16},
  booktitle = {{P}roceedings of the 27th
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'16)},
  author = {Nathalie Bertrand and Serge Haddad and Engel Lefaucheux},
  title = {Diagnosis in Infinite-State Probabilistic Systems},
  pages = {37:1-37:15},
  url = {https://hal.inria.fr/hal-01334218},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHL-concur16.pdf},
  doi = {10.4230/LIPIcs.CONCUR.2016.37},
  abstract = {In a recent work, we introduced four variants of
    diagnosability (\textsf{FA}, \textsf{IA}, \textsf{FF},~\textsf{IF})
    in (finite) probabilistic systems (pLTS) depending whether one
    considers (1)~finite or infinite runs and (2)~faulty or all runs. We
    studied their relationship and established that the corresponding
    decision problems are PSPACE-complete. A~key ingredient of the
    decision procedures was a characterisation of diagnosability by the
    fact that a random run almost surely lies in an open set whose
    specification only depends on the qualitative behaviour of the pLTS.
    Here we investigate similar issues for infinite pLTS. We~first show
    that this characterisation still holds for
    \textsf{FF}-diagnosability but with a~\(G_{\delta}\) set instead of
    an open set and also for \textsf{IF}-and \textsf{IA}-diagnosability
    when pLTS are finitely branching. We also prove that surprisingly
    \textsf{FA}-diagnosability cannot be characterised in this way even
    in the finitely branching case. Then we apply our characterisations
    for a partially observable probabilistic extension of visibly
    pushdown automata (POpVPA), yielding EXPSPACE procedures for solving
    diagnosability problems. In~addition, we~establish some
    computational lower bounds and show that slight extensions of POpVPA
    lead to undecidability.}
}
@comment{{B-arxiv16,
  author =		Bollig, Benedikt, 
  affiliation = 	aff-LSVmexico,
  title =    		One-Counter Automata with Counter Visibility, 
  institution = 	Computing Research Repository, 
  number =    		1602.05940, 
  month = 		feb, 
  nmonth =     		2,
  year = 		2016, 
  type = 		RR, 
  axeLSV = 		mexico,
  NOcontrat = 		"",
  
  url =			http://arxiv.org/abs/1602.05940, 
  PDF =			"http://www.lsv.fr/Publis/PAPERS/PDF/B-arxiv16.pdf",
  lsvdate-new =  	20160222,
  lsvdate-upd =  	20160222,
  lsvdate-pub =  	20160222,
  lsv-category = 	"rapl",
  wwwpublic =    	"public and ccsb",
  note = 		18~pages, 

  abstract = "In a one-counter automaton (OCA), one can read a letter
    from some finite alphabet, increment and decrement the counter by
    one, or test it for zero. It is well-known that universality and
    language inclusion for OCAs are undecidable. We consider here OCAs
    with counter visibility: Whenever the automaton produces a letter,
    it outputs the current counter value along with~it. Hence, its
    language is now a set of words over an infinite alphabet. We show
    that universality and inclusion for that model are in PSPACE, thus
    no harder than the corresponding problems for finite automata, which
    can actually be considered as a special case. In fact, we show that
    OCAs with counter visibility are effectively determinizable and
    closed under all boolean operations. As~a~strict generalization, we
    subsequently extend our model by registers. The general nonemptiness
    problem being undecidable, we impose a bound on the number of
    register comparisons and show that the corresponding nonemptiness
    problem is NP-complete.",
}}
@inproceedings{tacas16-BFHH,
  address = {Eindhoven, The Netherlands},
  month = apr,
  year = 2016,
  volume = {9636},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Chechik, Marsha and Raskin, Jean-Fran{\c{c}}ois},
  acronym = {{TACAS}'16},
  booktitle = {{P}roceedings of the 22th {I}nternational 
               {C}onference on {T}ools and {A}lgorithms for
               {C}onstruction and {A}nalysis of {S}ystems
               ({TACAS}'16)},
  author = {Blondin, Michael and Finkel, Alain and Haase, Christoph and
                  Haddad, Serge},
  title = {Approaching the Coverability Problem Continuously},
  pages = {480-496},
  url = {http://arxiv.org/abs/1510.05724},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/arxiv15-BFHH.pdf},
  doi = {10.1007/978-3-662-49674-9_28},
  abstract = {The coverability problem for Petri nets plays a central role in
    the verification of concurrent shared-memory programs. However, its high
    EXPSPACE-complete complexity poses a challenge when encountered in
    real-world instances. In this paper, we develop a new approach to this
    problem which is primarily based on applying forward coverability in
    continuous Petri nets as a pruning criterion inside a backward
    coverability framework. A cornerstone of our approach is the efficient
    encoding of a recently developed polynomial-time algorithm for
    reachability in continuous Petri nets into SMT. We demonstrate the
    effectiveness of our approach on standard benchmarks from the literature,
    which shows that our approach decides significantly more instances than
    any existing tool and is in addition often much faster, in particular on
    large instances.}
}
@inproceedings{BHL-lata16,
  address = {Prague, Czech Republic},
  month = mar,
  year = 2016,
  volume = {9618},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Mart{\'\i}n-Vide, Carlos},
  acronym = {{LATA}'16},
  booktitle = {{P}roceedings of the 10th {I}nternational {C}onference on {L}anguage 
	    and {A}utomata {T}heory and {A}pplications ({LATA}'16)},
  author = {Bertrand, Nathalie and Haddad, Serge and Lefaucheux, Engel},
  title = {Accurate Approximate Diagnosability of Stochastic Systems},
  pages = {549-561},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHL-lata16.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHL-lata16.pdf},
  doi = {10.1007/978-3-319-30000-9_42},
  abstract = {Diagnosis of partially observable stochastic systems prone to
    faults was introduced in the late nineties. Diagnosability, i.e. the
    existence of a diagnoser, may be specified in different ways: (1)~exact
    diagnosability (called A-diagnosability) requires that almost surely a
    fault is detected and that no fault is erroneously claimed while
    (2)~approximate diagnosability (called \(\varepsilon\)-diagnosability)
    allows a small probability of error when claiming a fault and (3)~accurate
    approximate diagnosability (called AA-diagnosability) requires that this
    error threshold may be chosen arbitrarily small. Here we mainly focus on
    approximate diagnoses. We first refine the almost sure requirement about
    finite delay introducing a uniform version and showing that while it does
    not discriminate between the two versions of exact diagnosability this is
    no more the case in approximate diagnosis. Then we establish a complete
    picture for the decidability status of the diagnosability problems:
    (uniform) \(\varepsilon\)-diagnosability and uniform AA-diagnosability are
    undecidable while AA-diagnosability is decidable in PTIME, answering a
    longstanding open question.}
}
@article{HM-tcs17,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Haddad, Serge and Monmege, Benjamin},
  title = {Interval iteration algorithm for {MDP}s and {IMDP}s},
  volume = {735},
  year = {2018},
  pages = {111-131},
  month = jul,
  doi = {10.1016/j.tcs.2016.12.003},
  url = {http://authors.elsevier.com/sd/article/S0304397516307095},
  abstract = {Markov Decision Processes (MDP) are a widely used model including both non-deterministic and probabilistic choices. Minimal and maximal probabilities to reach a target set of states, with respect to a policy resolving non-determinism, may be computed by several methods including value iteration. This algorithm, easy to implement and efficient in terms of space complexity, iteratively computes the probabilities of paths of increasing length. However, it raises three issues: (1) defining a stopping criterion ensuring a bound on the approximation, (2) analysing the rate of convergence, and (3) specifying an additional procedure to obtain the exact values once a sufficient number of iterations has been performed. The first two issues are still open and, for the third one, an upper bound on the number of iterations has been proposed. Based on a graph analysis and transformation of MDPs, we address these problems. First we introduce an interval iteration algorithm, for which the stopping criterion is straightforward. Then we exhibit its convergence rate. Finally we significantly improve the upper bound on the number of iterations required to get the exact values. We extend our approach to also deal with Interval Markov Decision Processes (IMDP) that can be seen as symbolic representations of MDPs.}
}
@inproceedings{BHL-msr17,
  address = {Marseille, France},
  month = nov,
  year = 2017,
  futureseries = {Journal Europ{\'e}en des Syst{\`e}mes Automatis{\'e}s},
  publisher = {HAL},
  editor = {Demongodin, Isabel and Reynier, Pierre-Alain},
  acronym = {{MSR}'17},
  booktitle = {{A}ctes du 11{\`e}me {C}olloque sur la 
               {M}od{\'e}lisation des {S}yst{\`e}mes
               {R}{\'e}actifs
               ({MSR}'17)},
  author = {Nathalie Bertrand and Serge Haddad and Engel Lefaucheux},
  title = {Diagnostic et contr{\^o}le de la d{\'e}gradation des syst{\`e}mes probabilistes},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHL-msr17.pdf},
  abstract = {Le diagnostic actif est op{\'e}r{\'e} par un contr{\^o}leur en vue de rendre un syst{\`e}me diagnosticable. Afin d'{\'e}viter que le contr{\^o}leur ne d{\'e}grade trop fortement le syst{`e}me, on lui affecte g{\'e}n{\'e}ralement un second objectif en termes de qualit{\'e} de service. Dans le cadre des syst{\`e}mes probabilistes, une sp{\'e}cification possible consiste {\`a} assurer une probabilit{\'e} positive qu'une ex{\'e}cution infinie soit correcte, ce qu'on appelle le diagnostic
actif s{\^u}r. Nous introduisons ici deux sp{\'e}cifications alternatives. La gamma-correction du syst{\`e}me affecte {\`a} une ex{\'e}cution une valeur de correction d{\'e}pendant d'un facteur de d{\'e}cote gamma et le contr{\^o}leur doit assurer une valeur moyenne sup{\'e}rieure {\`a} un seuil fix{\'e}. La alpha-d{\'e}gradation requiert qu'asymptotiquement, {\`a} chaque unit{\'e} de temps une proportion sup{\'e}rieure {\`a} alpha des ex{\'e}cutions jusqu'alors correctes le demeure. D'un point de vue s{\'e}mantique, nous explicitons des liens significatifs entre les diff{\'e}rentes notions. Algorithmiquement, nous {\'e}tablissons la fronti{\`e}re entre d{\'e}cidabilit{\'e} et ind{\'e}cidabilit{\'e} des probl{\`e}mes et dans le cas positif nous exhibons la complexit{\'e} pr{\'e}cise ainsi qu'une synth{\`e}se, potentiellement {\`a} m{\'e}moire infinie.}
}
@inproceedings{BHL-fsttcs17,
  address = {Kanpur, India},
  month = dec,
  year = 2017,
  volume = {93},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Satya Lokam and R. Ramanujam},
  acronym = {{FSTTCS}'17},
  booktitle = {{P}roceedings of the 37th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'17)},
  author = {B{\'e}atrice B{\'e}rard and Serge Haddad and Engel Lefaucheux},
  title = {Probabilistic Disclosure: Maximisation vs. Minimisation},
  pages = {13:1-13:14},
  url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=8384},
  pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/8384/pdf/LIPIcs-FSTTCS-2017-13.pdf},
  doi = {10.4230/LIPIcs.FSTTCS.2017.13},
  abstract = {We consider opacity questions where an observation function provides to an external attacker a view of the states along executions and secret executions are those visiting some state from a fixed subset. Disclosure occurs when the observer can deduce from a finite observation that the execution is secret, the epsilon-disclosure variant corresponding to the execution being secret with probability greater than 1 - epsilon. In a probabilistic and non deterministic setting, where an internal agent can choose between actions, there are two points of view, depending on the status of this agent: the successive choices can either help the attacker trying to disclose the secret, if the system has been corrupted, or they can prevent disclosure as much as possible if these choices are part of the system design. In the former situation, corresponding to a worst case, the disclosure value is the supremum over the strategies of the probability to disclose the secret (maximisation), whereas in the latter case, the disclosure is the infimum (minimisation). We address quantitative problems (comparing the optimal value with a threshold) and qualitative ones (when the threshold is zero or one) related to both forms of disclosure for a fixed or finite horizon. For all problems, we characterise their decidability status and their complexity. We discover a surprising asymmetry: on the one hand optimal strategies may be chosen among deterministic ones in maximisation problems, while it is not the case for minimisation. On the other hand, for the questions addressed here, more minimisation problems than maximisation ones are decidable.}
}
@techreport{Haddad-hal17,
  author = {Haddad, Serge},
  title = {Memoryless Determinacy of Finite Parity Games: Another Simple Proof},
  institution = {HAL-inria},
  number = {hal-01541508},
  month = jun,
  year = {2017},
  type = {Research Report},
  url = {https://hal.inria.fr/hal-01541508},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Haddad-hal17.pdf},
  note = {7~pages},
  abstract = {Memoryless determinacy of (infinite) parity games is an important result with numerous applications. It was first independently established by Emerson and Jutla [1] and Mostowski [2] but their proofs involve elaborate developments. The elegant and simpler proof of Zielonka [3] still requires a nested induction on the finite number of priorities and on ordinals for sets of vertices. There are other proofs for finite games like the one of Bj{\"o}rklund, Sandberg and Vorobyovin [4] that relies on relating infinite and finite duration games. We present here another simple proof that finite parity games are determined with memoryless strategies using induction on the number of relevant states. The closest proof that relies on induction over non absorbing states is the one of Graedel [5]. However instead of focusing on a single appropriate vertex for induction as we do here, he considers two reduced games per vertex, for all the vertices of the game. The idea of reasoning about a single state has been inspired to me by the analysis of finite stochastic priority games by Karelovic and Zielonka [6].}
}
@inproceedings{BHJ-concur17,
  address = {Berlin, Germany},
  month = sep,
  year = 2017,
  volume = {85},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Meyer, Roland and Nestmann, Uwe},
  acronym = {{CONCUR}'17},
  booktitle = {{P}roceedings of the 28th
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'17)},
  author = {Bouyer, Patricia and Haddad, Serge and Jug{\'e}, Vincent},
  title = {Unbounded product-form {P}etri nets},
  pages = {31:1--31:16},
  url = {http://drops.dagstuhl.de/opus/volltexte/2017/7795},
  pdf = {http://drops.dagstuhl.de/opus/volltexte/2017/7795/pdf/LIPIcs-CONCUR-2017-31.pdf},
  doi = {10.4230/LIPIcs.CONCUR.2017.31},
  abstract = {Computing steady-state distributions in infinite-state stochastic systems is in general a very difficult task. Product-form Petri nets are those Petri nets for which the steady-state distribution can be described as a natural product corresponding, up to a normalising constant, to an exponentiation of the markings. However, even though some classes of nets are known to have a product-form distribution, computing the normalising constant can be hard. The class of (closed) \(\Pi^3\)-nets has been proposed in an earlier work, for which it is shown that one can compute the steady-state distribution efficiently. However these nets are bounded. In this paper, we generalise queuing Markovian networks and closed \(\Pi^3\)-nets to obtain the class of open \(\Pi^3\)-nets, that generate infinite-state systems. We show interesting properties of these nets: (1) we prove that liveness can be decided in polynomial time, and that reachability in live \(\Pi^3\)-nets can be decided in polynomial time; (2) we show that we can decide ergodicity of such nets in polynomial time as well; (3) we provide a pseudo-polynomial time algorithm to compute the normalising constant.}
}
@article{BFHH-tocl17,
  publisher = {ACM Press},
  journal = {ACM Transactions on Computational Logic},
  author = {Blondin, Michael and Finkel, Alain and Haase, Christoph and
                  Haddad, Serge},
  title = {The Logical View on Continuous {P}etri Nets},
  volume = {18},
  number = {3},
  year = {2017},
  pages = {24:1--24:28},
  url = {http://doi.acm.org/10.1145/3105908},
  doi = {10.1145/3105908},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHH-tocl17.pdf},
  abstract = {Continuous Petri nets are a relaxation of classical discrete Petri nets in which transitions can be fired a fractional number of times, and consequently places may contain a fractional number of tokens. Such continuous Petri nets are an appealing object to study since they over approximate the set of reachable configurations of their discrete counterparts, and their reachability problem is known to be decidable in polynomial time. The starting point of this paper is to show that the reachability relation for continuous Petri nets is definable by a sentence of linear size in the existential theory of the rationals with addition and order. Using this characterization, we obtain decidability and complexity results for a number of classical decision problems for continuous Petri nets. In particular, we settle the open problem about the precise complexity of reachability set inclusion. Finally, we show how continuous Petri nets can be incorporated inside the classical backward coverability algorithm for discrete Petri nets as a pruning heuristic in order to tackle the symbolic state explosion problem. The cornerstone of the approach we present is that our logical characterization enables us to leverage the power of modern SMT-solvers in order to yield a highly performant and robust decision procedure for coverability in Petri nets. We demonstrate the applicability of our approach on a set of standard benchmarks from the literature.}
}
@inproceedings{BBDH-sia17,
  address = {Montigny-le-Bretonneux, France},
  month = mar,
  editor = {{Di Valentin}, Laurent and Landel, Eric},
  acronym = {SIA Simulation Num{\'e}rique},
  booktitle = {SIA Simulation Num{\'e}rique},
  author = {Barbot, Beno{\^i}t and B{\'e}rard, B{\'e}atrice and Duplouy, Yann and Haddad, Serge},
  title = {Statistical Model-Checking for Autonomous Vehicle Safety Validation},
  todopages = {},
  year = {2017},
  todolsvdate-pub = 20170320,
  tododoi = {},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBDH-sia17.pdf},
  url = {https://hal.archives-ouvertes.fr/hal-01491064},
  abstract = {We present an application of statistical
model-checking to the verification of an autonomous
vehicle controller. Our goal is to check safety properties
in various traffic situations. More specifically, we
focus on a traffic jam situation.\par    
The controller is specified by a C++ program. Using
sensors, it registers positions and velocities of nearby
vehicles and modifies the position and velocity of the
controlled vehicle to avoid collisions. We model the environment
using a stochastic high level Petri net, where
random behaviors of other vehicles can be described.
We use HASL, a quantitative variant of linear temporal
logic, to express the desired properties. A large family
of performance indicators can be specified in HASL
and we target in particular the expectation of travelled
distance or the collision probability.\par    
We evaluate the properties of this model using COSMOS1.
This simulation tool implements numerous statistical
techniques such as sequential hypothesis testing
and most confidence range computation methods.
Its efficiency allowed us to conduct several experiments
with success.}
}
@inproceedings{CHKP-valuetools17,
  address = {Venice, Italy},
  month = dec,
  year = 2017,
  acronym = {{VALUETOOLS}'17},
  booktitle = {{P}roceedings of the 11th {I}nternational {C}onference 
	   on {P}erformance {E}valuation {M}ethodologies and {T}ools
           ({VALUETOOLS}'17)},
  author = {Chatzikokolakis, Kostas and Haddad, Serge and Kassem, Ali and Palamidessi, Catuscia},
  title = {{Trading Optimality for Performance in Location Privacy}},
  pages = {221-222},
  url = {https://arxiv.org/abs/1710.05524},
  pdf = {https://arxiv.org/pdf/1710.05524.pdf},
  doi = {10.1145/3150928.3150962},
  abstract = {Location-Based Services (LBSs) provide invaluable aid in the everyday activities of many individuals, however they also pose serious threats to the user' privacy. There is, therefore, a growing interest in the development of mechanisms to protect location privacy during the use of LBSs. Nowadays, the most popular methods are probabilistic, and the so-called optimal method achieves an optimal trade-off between privacy and utility by using linear optimization techniques. Unfortunately, due to the complexity of linear programming, the method is unfeasible for a large number n of locations, because the constraints are \(O(n^3)\). In this paper, we propose a technique to reduce the number of constraints to \(O(n^2)\), at the price of renouncing to perfect optimality. We show however that on practical situations the utility loss is quite acceptable, while the gain in performance is significant.}
}
@article{BHL-icomp19,
  publisher = {Elsevier Science Publishers},
  journal = {Information and Computation},
  author = {Nathalie Bertrand and Serge Haddad and Engel Lefaucheux},
  title = {{A Tale of Two Diagnoses in Probabilistic Systems}},
  volume = {269},
  year = {2019},
  month = dec,
  doi = {10.1016/j.ic.2019.104441},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHL-icomp18.pdf},
  abstract = {Diagnosis of partially observable stochastic systems prone to faults was introduced
in the late nineties. Diagnosability, i.e. the existence of a diagnoser, may be specified in different ways: exact diagnosability requires that almost surely a fault is detected and that no fault is erroneously claimed; approximate diagnosability tolerates a small error probability when claiming a fault; last, accurate approximate diagnosability guarantees that the error probability can be chosen arbitrarily small. In this article, we  first refine the specification of diagnosability by identifying three criteria: (1) detecting faulty runs or providing information
for all runs (2) considering finite or infinite runs, and (3) requiring or not a uniform detection delay. We then give a complete picture of relations between the different diagnosability specifications for probabilistic systems and establish characterisations for most of them in the finite-state case. Based on these characterisations, we develop decision procedures, study their complexity and prove their optimality. We also design synthesis algorithms to construct diagnosers
and we analyse their memory requirements. Finally we establish undecidability of the diagnosability problems for which we provided no characterisation.}
}
@inproceedings{BBDH-atpn18,
  address = {Bratislava, Slovakia},
  month = jun,
  year = 2018,
  volume = {10877},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Victor Khomenko and {Olivier H.} Roux},
  acronym = {{PETRI~NETS}'18},
  booktitle = {{P}roceedings of the 39th
               {I}nternational {C}onference on
               {A}pplications and {T}heory of {P}etri {N}ets
               ({PETRI~NETS}'18)},
  author = {Barbot, Beno{\^i}t and B{\'e}rard, B{\'e}atrice and Duplouy, Yann and Haddad, Serge},
  title = {{Integrating Simulink Models into the Model Checker Cosmos}},
  pages = {363-373},
  url = {https://hal.archives-ouvertes.fr/hal-01725835/},
  pdf = {https://hal.archives-ouvertes.fr/hal-01725835/document},
  doi = {10.1007/978-3-319-91268-4_19},
  abstract = {We present an implementation for Simulink model executions in the statistical model-checker Cosmos. We take profit of this implementation for an hybrid modeling combining Petri nets and Simulink models.}
}
@techreport{BBFHP-hal18,
  author = {Barbot, Beno{\^i}t and Beccuti, Marco and Franceschinis, Giuliana and Haddad, Serge and Picaronny, Claudine},
  institution = {HAL-Inria},
  month = mar,
  number = {hal-01726011},
  type = {Research Report},
  title = {Bounds Computation for Symmetric Nets},
  year = {2018},
  url = {https://hal.inria.fr/hal-01726011},
  pdf = {https://hal.inria.fr/hal-01726011/file/main.pdf},
  abstract = {Monotonicity in Markov chains is the starting point for quantitative abstraction of complex probabilistic systems leading to (upper or lower) bounds for probabilities and mean values relevant to their analysis. While numerous case studies exist in the literature, there is no generic model for which monotonicity is directly derived from its structure. Here we propose such a model and formalize it as a subclass of Stochastic Symmetric (Petri) Nets (SSNs) called Stochastic Monotonic SNs (SMSNs). On this subclass the monotonicity is proven by coupling arguments that can be applied on an abstract description of the state (symbolic marking). Our class includes both process synchronizations and resource sharings and can be extended to model open or cyclic closed systems. Automatic methods for transforming a non monotonic system into a monotonic one matching the MSN pattern, or for transforming a monotonic system with large state space into one with reduced state space are presented. We illustrate the interest of the proposed method by expressing standard monotonic models and modelling a flexible manufacturing system case study.}
}
@article{H-ipl18,
  publisher = {Elsevier Science Publishers},
  journal = {Information Processing Letters},
  author = {Haddad, Serge},
  title = {{Memoryless determinacy of finite parity games: Another simple proof}},
  volume = {132},
  pages = {19-21},
  month = apr,
  year = {2018},
  pdf = {https://hal.inria.fr/hal-01541508/document},
  doi = {10.1016/j.ipl.2017.11.012},
  abstract = {Memoryless determinacy of (infinite) parity games is an important result with numerous applications. It was first independently established by Emerson and Jutla [1] and Mostowski [2] but their proofs involve elaborate developments. The elegant and simpler proof of Zielonka [3] still requires a nested induction on the finite number of priorities and on ordinals for sets of vertices. There are other proofs for finite games like the one of Björklund, Sandberg and Vorobyovin [4] that relies on relating infinite and finite duration games. We present here another simple proof that finite parity games are determined with memoryless strategies using induction on the number of relevant states. The closest proof that relies on induction over non absorbing states is the one of Grädel [5]. However instead of focusing on a single appropriate vertex for induction as we do here, he considers two reduced games per vertex, for all the vertices of the game. The idea of reasoning about a single state has been inspired to me by the analysis of finite stochastic priority games by Karelovic and Zielonka [6].}
}
@techreport{DH-hal19,
  author = {Donatelli, Susanna and Haddad, Serge},
  institution = {HAL},
  month = oct,
  note = {23~pages},
  number = {hal-02306021},
  type = {Research Report},
  title = {{Autonomous Transitions Enhance CSLTA Expressiveness and Conciseness}},
  year = {2019},
  url = {https://hal.inria.fr/hal-02306021},
  pdf = {https://hal.inria.fr/hal-02306021/document},
  abstract = {CSLTA is a stochastic temporal logic for continuous-time Markov chains (CTMC) where formulas similarly to those of CTL* are inductively defined by nesting of timed path formulas and state formulas. In particular a timed path formula of CSLTA is specified by a single-clock Deterministic Timed Automaton (DTA). Such a DTA features two kinds of transitions: synchronizing transitions triggered by CTMC transitions and autonomous transitions triggered by time elapsing that change the location of the DTA when the clock reaches a given threshold. It has already been shown that CSLTA strictly includes stochastic logics like CSL and asCSL. An interesting variant of CSLTA consists in equipping transitions rather than locations by boolean formulas. Here we answer the following question: do autonomous transitions and/or boolean guards on transitions enhance expressiveness and/or conciseness of DTAs? We show that this is indeed the case. In establishing our main results we also identify an accurate syntactical characterization of DTAs for which the autonomous transitions do not add expressive power but lead to exponentially more concise DTAs.}
}
@inproceedings{FHK-atpn19,
  address = {Aachen, Germany},
  month = jun,
  year = 2019,
  volume = {11522},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Susanna Donatelli and Stefan Haar},
  acronym = {{PETRI~NETS}'19},
  booktitle = {{P}roceedings of the 40th
               {I}nternational {C}onference on
               {A}pplications and {T}heory of {P}etri {N}ets
               ({PETRI~NETS}'19)},
  author = {Finkel, Alain and Haddad, Serge and Khmelnitsky, Igor},
  title = {Coverability and Termination in Recursive Petri Nets},
  pages = { 429-448},
  url = {https://hal.inria.fr/hal-02081019},
  pdf = {https://hal.inria.fr/hal-02081019/document},
  doi = {10.1007/978-3-030-21571-2_23},
  abstract = {In the early two-thousands, Recursive Petri nets have been introduced in order to model distributed planning of multi-agent systems for which counters and recursivity were necessary. Although Recursive Petri nets strictly extend Petri nets and stack automata, most of the usual property problems are solvable but using non primitive recursive algorithms, even for coverability and termination. For almost all other extended Petri nets models containing a stack the complexity of coverability and termination are unknown or strictly larger than EXPSPACE. In contrast, we establish here that for Recursive Petri nets, the coverability and termination problems are EXPSPACE-complete as for Petri nets. From an expressiveness point of view, we show that coverability languages of Recursive Petri nets strictly include the union of coverability languages of Petri nets and context-free languages. Thus we get for free a more powerful model than Petri net.}
}
@article{FHK-deds20,
  publisher = {Springer},
  journal = {Discrete Event Dynamic Systems: Theory and Applications},
  author = {Alain Finkel and Serge Haddad and Igor Khmelnitsky},
  title = {{Commodification of accelerations for the Karp and Miller Construction}},
  doi = {10.1007/s10626-020-00331-z},
  year = {2020},
  url = {https://link.springer.com/article/10.1007/s10626-020-00331-z}
}
@article{BHL-deds20,
  publisher = {Springer},
  journal = {Discrete Event Dynamic Systems: Theory and Applications},
  author = {Nathalie Bertrand and Serge Haddad and Engel Lefaucheux},
  title = {{Diagnosis and Degradation Control for Probabilistic Systems}},
  volume = {30},
  pages = {695–723},
  doi = {10.1007/s10626-020-00320-2},
  year = {2020},
  url = {https://link.springer.com/article/10.1007/s10626-020-00320-2}
}
@techreport{KY-arxiv20,
  author = {Khmelnitsky, Igor  and
               Neider, Daniel  and
               Roy, Rajarshi  and
               Barbot, Beno{\^{\i}}t  and
               Bollig, Benedikt  and
               Finkel, Alain  and
               Haddad, Serge and
               Leucker, Martin  and
              Ye,  Lina },
  institution = {Computing Research Repository},
  month = sep,
  number = {2009.10610},
  type = {Research Report},
  title = {Property-Directed Verification of Recurrent Neural Networks},
  year = {2020},
  url = {https://arxiv.org/abs/2009.10610},
  pdf = {https://arxiv.org/pdf/2009.10610.pdf}
}
@inproceedings{HHSY-fsttcs20,
  address = {Goa, India},
  month = dec,
  volume = {182},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Nitin Saxena and Sunil Simon},
  acronym = {{FSTTCS}'20},
  booktitle = {{P}roceedings of the 40th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'20)},
  author = {Stefan Haar and Serge Haddad and Stefan Schwoon and Lina Ye},
  title = {Active Prediction for Discrete Event Systems},
  pages = {48:1--48:16},
  year = {2020},
  doi = {https://doi.org/10.4230/LIPIcs.FSTTCS.2020.48},
  pdf = {https://drops.dagstuhl.de/opus/volltexte/2020/13289/pdf/LIPIcs-FSTTCS-2020-48.pdf},
  url = {https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=13289}
}
@inproceedings{DH-atpn20,
  address = {Vienna, Austria},
  month = sep,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = { Nathalie Bertrand and Nils Jansen},
  acronym = {{FORMATS}'20},
  booktitle = {{P}roceedings of the 18th {I}nternational {C}onference
           on {F}ormal {M}odelling and {A}nalysis of {T}imed
           {S}ystems ({FORMATS}'20)},
  author = {Susanna Donatelli and Serge Haddad},
  title = {Guarded Autonomous Transitions Increase Conciseness and Expressiveness of Timed Automata},
  pages = {215--230},
  year = {2020},
  url = {https://link.springer.com/chapter/10.1007%2F978-3-030-57628-8_13}
}
@inproceedings{HK-atpn20,
  address = {Paris, France},
  month = jun,
  volume = {12152},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Ryszard Janicki and Natalia Sidorova and Thomas Chatain},
  acronym = {{PETRI~NETS}'20},
  booktitle = {{P}roceedings of the 41st
               {I}nternational {C}onference on
               {A}pplications and {T}heory of {P}etri {N}ets
               ({PETRI~NETS}'20)},
  author = {Serge Haddad and Igor Khmelnitsky},
  title = {{D}ynamic {R}ecursive {P}etri {N}ets},
  pages = {345-366},
  doi = {10.1007/978-3-030-51831-8\_17},
  year = 2020,
  url = {https://hal.inria.fr/hal-02511321}
}
@inproceedings{DH-lata2020,
  address = {Milan, Italy},
  month = mar,
  volume = {12038},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Alberto Leporati and
               Carlos Mart{\'{\i}}n{-}Vide and
               Dana Shapira and
               Claudio Zandron},
  acronym = {{LATA}'20},
  booktitle = {{P}roceedings of the 14th {I}nternational {C}onference on {L}anguage 
	    and {A}utomata {T}heory and {A}pplications ({LATA}'20)},
  author = {Susanna Donatelli and Serge Haddad},
  title = {Expressiveness and Conciseness of Timed Automata for the Verification of Stochastic Models},
  pages = {170-183},
  year = 2020
}
@inproceedings{FHK-msr2019,
  address = {Angers, France},
  month = nov,
  futureseries = {Journal Europ{\'e}en des Syst{\`e}mes Automatis{\'e}s},
  publisher = {HAL},
  editor = {Beno{\^i}t Delahaye and S{\'e}bastien Lahaye and Mehdi Lhommeau},
  acronym = {{MSR}'19},
  booktitle = {{A}ctes du 12{\`e}me {C}olloque sur la 
               {M}od{\'e}lisation des {S}yst{\`e}mes
               {R}{\'e}actifs
               ({MSR}'19)},
  author = {Alain Finkel and Serge Haddad and Igor Khmelnitsky},
  title = {{R{\'e}ification des acc{\'e}l{\'e}rations pour la construction de Karp et Miller}},
  year = 2019,
  pdf = {https://hal.archives-ouvertes.fr/hal-02431913/file/MSR19_paper_17.pdf},
  url = {https://hal.archives-ouvertes.fr/hal-02431913}
}
@inproceedings{FHK-fossacs2020,
  address = {Dublin, Ireland},
  month = apr,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Barbara K{\"o}nig and Jean Goubault-Larrecq},
  acronym = {{FoSSaCS}'20},
  booktitle = {{P}roceedings of the 23rd {I}nternational
               {C}onference on {F}oundations of {S}oftware {S}cience
               and {C}omputation {S}tructures
               ({FoSSaCS}'20)},
  author = {Alain Finkel and Serge Haddad and Igor Khmelnitsky},
  title = {Minimal coverability tree construction made complete and efficient},
  pages = {237--256},
  doi = {10.1007/978-3-030-45231-5_13},
  year = 2020
}

This file was generated by bibtex2html 1.98.