@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.