@inproceedings{GCH-atpn86,
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)},
title = {Specification and Properties of a Cache Coherence Protocol
Model},
pages = {1-20}
}

@inproceedings{HG-atpn86,
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)},
title = {Algebraic Structure of Flows of a Regular Coloured Net},
pages = {73-88}
}

@inproceedings{DH-pnpm89,
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)},
title = {Aggregation of States in Colored Stochastic {P}etri Nets:
Application to a Multiprocessor Architecture},
pages = {40-49}
}

@inproceedings{BMBH-atpn88,
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
title = {{AMI}: An Extensible {P}etri Nets Interactive Workshop},
nopages = {}
}

@inproceedings{CH-atpn88,
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)},
title = {Towards a General and Powerful Computation of Flows for
Parameterized Coloured Nets},
nopages = {}
}

@inproceedings{HC-pp88,
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)},
title = {Validation of Parallel Systems with Coloured {P}etri Nets},
pages = {377-390}
}

@inproceedings{CHP-atpn91,
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)},
Jean-Fran{\c{c}}ois},
title = {Generative Families of Positive Invariants in Coloured Nets
Sub-Classes},
pages = {51-70}
}

@inproceedings{Had-atpn88,
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)},
title = {A Reduction Theory for Coloured {P}etri Nets},
pages = {209-235}
}

@inproceedings{DH-atpn89,
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)},
title = {Regular Stochastic {P}etri Nets},
pages = {186-209}
}

@incollection{CDFH-hlpn91,
author = {Chiola, Giovanni and Dutheillet, Claude and Franceschinis,
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,
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,
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)},
title = {An Algorithm Providing Fault-Tolerance for Layered
Distributed Systems},
nopages = {}
}

@inproceedings{DH-iscis92,
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)},
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,
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,
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)},
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)},
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)},
title = {A Protocol Specification Language with a High-Level {P}etri Net Semantics},
pages = {225-241}
}

@inproceedings{BDH-atpn93,
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)},
title = {An Efficient Algorithm for Finding Structural Deadlocks in
Colored {P}etri Nets},
pages = {69-88}
}

@inproceedings{HTZ-pstv93,
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)},
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)},
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,
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)},
and Zouari, Belhassen},
title = {Symbolic Reachability Graph and Partial Symmetries},
pages = {238-251}
}

@inproceedings{EFH-maamaw96,
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)},
title = {A Coordination Algorithm for Multi-Agent Planning},
pages = {86-99}
}

@inproceedings{EFH-icmas96,
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)},
title = {A Recursive Model for Distributed Planning},
pages = {307-314}
}

@inproceedings{HM-icatpn1996,
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)},
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,
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,
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)},
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)},
title = {Structured Characterization of the Markov Chain of
Phase-Type~{SPN}},
pages = {243-254}
}

@inproceedings{AHI-tacas98,
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)},
title = {Exploiting Symmetry in Linear Time Temporal Logic Model
Checking: One Step Beyond},
pages = {52-67}
}

@techreport{SP-LIP6-1999,
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,
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)},
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)},
title = {Reaching Agreement in Hierarchical Groups},
nopages = {}
}

@inproceedings{EFHM-maamaw99,
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)},
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,
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)},
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,
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)},
Hamza},
title = {A Formal Study of Interactions in Multi-Agent Systems},
pages = {240-245}
}

@inproceedings{HN-cata99,
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)},
title = {Combining different failure detectors for solving a
large-scale consensus problem},
pages = {204-209}
}

@techreport{SP-LIP6-2000,
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,
month = oct,
year = 2000,
volume = 183,
series = {{IFIP} Conference Proceedings},
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})},
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,
month = aug,
year = 2000,
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)},
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},
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,
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)},
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)},
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,
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,
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,
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,
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,
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,
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
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,
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)},
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,
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)},
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,
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)},
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,
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)},
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,
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)},
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,
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,
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},
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,
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)},
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,
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)},
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)},
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,
month = sep,
year = 2004,
acronym = {{WODES}'04},
booktitle = {{P}roceedings of the 7th {W}orkshop on {D}iscrete {E}vent {S}ystems
({WODES}'04)},
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,
month = sep,
year = 2004,
acronym = {{WODES}'04},
booktitle = {{P}roceedings of the 7th {W}orkshop on {D}iscrete {E}vent {S}ystems
({WODES}'04)},
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,
month = sep,
year = 2004,
acronym = {{WODES}'04},
booktitle = {{P}roceedings of the 7th {W}orkshop on {D}iscrete {E}vent {S}ystems
({WODES}'04)},
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,
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)},
Rampacek, Sylvain},
title = {A Dense Time Semantics for Web Services Specification
Languages},
pages = {647-648}
}

@inproceedings{HMMR-iceis04,
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)},
Rampacek, Sylvain},
title = {Modeling Web Services Interoperability},
pages = {287-295}
}

@techreport{HPP-cedric634,
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,
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,
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)},
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},
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},
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,
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)},
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,
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)},
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,
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)},
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,
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)},
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,
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)},
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,
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)},
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,
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)},
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,
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)},
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,
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}},
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
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,
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)},
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,
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)},
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,
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)},
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
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,
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},
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,
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)},
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},
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,
title = {Panorama de la v{\'e}rification},
booktitle = {M{\'e}thodes formelles pour les syst{\e}mes r{\'e}artis et
coop{\'e}ratifs},
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,
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},
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,
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,
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
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},
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
\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,
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)},
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
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,
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)},
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,
However, resulting composition models
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
issue through the definition of a dedicated model
and reduction techniques. They support
transactions and are therefore applicable to
service architectures.}
}

@inproceedings{BFH-icatpn07,
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
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
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
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
partially integrated in the GreatSPN tool,
so we also describe some experimental
results.}
}

@inproceedings{BBHMF-iceis07,
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},
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},
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
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,
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)},
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,
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
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,
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)},
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,
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)},
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,
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
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,
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
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,
month = may,
year = 2008,
acronym = {{WODES}'08},
booktitle = {{P}roceedings of the 9th {W}orkshop on {D}iscrete {E}vent {S}ystems
({WODES}'08)},
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,
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},
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,
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)},
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,
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},
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
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},
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},
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},
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},
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},
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},
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},
title = {Analysis Methods for {P}etri Nets},
pages = {41-86},
url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html}
}

@inproceedings{ZBH-lads09,
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},
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)},
title = {Agents Secure Interaction in Data Driven Languages},
pages = {72-91},
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,
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,
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)},
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,
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)},
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
provide useful partial information for modelers in the {"}DON'T~KNOW{"}
case.}
}

@incollection{EFH-tsmaai09,
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)},
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},
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},
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,
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)},
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,
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
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,
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)},
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,
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,
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
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,
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)},
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,
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)},
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,
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,
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)},
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,
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)},
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},
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,
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)},
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,
title = {Introduction to Verification},
booktitle = {Models and Analysis in Distributed Systems},
Petrucci, Laure},
publisher = {John Wiley \& Sons, Ltd.},
chapter = 6,
pages = {137-154},
year = 2011
}

@inproceedings{BHP-msr11,
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)},
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,
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
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,
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
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},
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)},
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,
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
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,
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)},
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},
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},
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,
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)},
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
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,
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)},
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,
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)},
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
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}},
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,
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},
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,
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},
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,
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)},
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,
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)},
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,
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)},
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,
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)},
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},
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
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,
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)},
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,
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)},
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,
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)},
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,
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
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,
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)},
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},
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,
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,
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,
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)},
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,
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)},
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
(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,
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
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},
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},
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},
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
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
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,
month = aug,
year = 2016,
volume = {59},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
acronym = {{CONCUR}'16},
booktitle = {{P}roceedings of the 27th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'16)},
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
computational lower bounds and show that slight extensions of POpVPA
}

@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,
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
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,
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)},
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},
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,
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)},
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,
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)},
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,
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},
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,
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)},
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
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,
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,
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},
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,
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},
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,
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,
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)},
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.}
}

@inproceedings{HK-atpn20,
month = jun,
futureseries = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {{\'E}tienne Andr{\'e} and Laure Petrucci},
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)},
title = {{D}ynamic {R}ecursive {P}etri {N}ets},
year = 2020,
url = {https://hal.inria.fr/hal-02511321}
}

@inproceedings{DH-lata2020,
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)},
title = {Expressiveness and Conciseness of Timed Automata for the Verification of Stochastic Models},
pages = {170-183},
year = 2020
}

@inproceedings{FHK-msr2019,
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)},
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,
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)},