@phdthesis{lf-these-82,
author = {Fribourg, Laurent},
title = {D{\'e}monstration automatique: r{\'e}futation par
superposition de clauses {\'e}quationnelles},
year = {1982},
month = sep,
type = {Th{\`e}se de doctorat},
school = {Universit{\'e} Paris~7, Paris, France}
}
@inproceedings{lf-ijcai-83,
address = {Karlsruhe, West Germany},
month = aug,
year = 1983,
publisher = {William Kaufmann},
editor = {Bundy, Alan},
acronym = {{IJCAI}'83},
booktitle = {{P}roceedings of the 8th {I}nternational {J}oint
{C}onference on {A}rtificial {I}ntelligence
({IJCAI}'83)},
author = {Fribourg, Laurent},
title = {A Superposition Oriented Theorem Prover},
pages = {923-925}
}
@inproceedings{lf-cade-84,
address = {Napa, California, USA},
month = may,
year = 1984,
volume = 170,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Shostak, Robert E.},
acronym = {{CADE}'84},
booktitle = {{P}roceedings of the 7th {I}nternational
{C}onference on {A}utomated {D}eduction
({CADE}'84)},
author = {Fribourg, Laurent},
title = {A Narrowing Procedure for Theories with Constructors},
pages = {259-281}
}
@inproceedings{lf-icalp-84,
address = {Antwerp, Belgium},
month = jul,
year = 1984,
volume = 172,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Paredaens, Jan},
acronym = {{ICALP}'84},
booktitle = {{P}roceedings of the 11th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming
({ICALP}'84)},
author = {Fribourg, Laurent},
title = {Oriented Equational Clauses as a Programming
Language},
pages = {162-173}
}
@article{lf-jlp-84,
publisher = {Elsevier Science Publishers},
journal = {Journal of Logic Programming},
author = {Fribourg, Laurent},
title = {Oriented Equational Clauses as a Programming
Language},
volume = 1,
number = 2,
pages = {165-177},
year = {1984},
month = aug
}
@inproceedings{lf-ilps-85,
address = {Boston, Massachusetts, USA},
month = jul,
year = 1985,
publisher = {{IEEE} Computer Society Press},
acronym = {{SLP}'85},
booktitle = {{P}roceedings of the 2nd
{IEEE} {S}ymposium on
{L}ogic {P}rogramming
({SLP}'85)},
author = {Fribourg, Laurent},
title = {{SLOG}: {A} Logic Programming Language Interpreter
Based on Clausal Superposition and Rewriting},
pages = {172-184}
}
@inproceedings{lf-tapsoft-85,
address = {Berlin, Germany},
month = mar,
year = 1985,
volume = 186,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Ehrig, Hartmut and Floyd, Christiane and
Nivat, Maurice and Thatcher, James W.},
acronym = {{TAPSOFT}'89},
booktitle = {{P}roceedings of the 1st
{I}nternational {J}oint {C}onference on
{T}heory and {P}ractice of {S}oftware {D}evelopment
({TAPSOFT}'89),
{V}olume~2: {C}olloquium on {S}oftware {E}ngineering
({CSE})},
author = {Boug{\'e}, Luc and Choquet, N. and
Fribourg, Laurent and
Gaudel, Marie-Claude},
missingauthor = {},
title = {Application of {P}rolog to Test Sets Generation from
Algebraic Specifications},
pages = {261-275}
}
@article{lf-tcs-85,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Fribourg, Laurent},
title = {A Superposition Oriented Theorem Prover},
volume = {35},
number = {2-3},
pages = {129-164},
year = {1985},
month = feb
}
@inproceedings{lf-icalp-86,
address = {Rennes, France},
month = jul,
year = 1986,
volume = 226,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Kott, Laurent},
acronym = {{ICALP}'86},
booktitle = {{P}roceedings of the 13th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming
({ICALP}'86)},
author = {Fribourg, Laurent},
title = {A Strong Restriction of the Inductive Completion
Procedure},
pages = {105-115}
}
@article{lf-jss-86,
publisher = {Elsevier Science Publishers},
journal = {Journal of Systems and Software},
author = {Boug{\'e}, Luc and Choquet, N. and
Fribourg, Laurent and Gaudel, Marie-Claude},
missingauthor = {},
title = {Test Sets Generation From Algebraic Specifications
Using Logic Programming},
volume = {6},
number = {4},
pages = {343-360},
year = {1986},
month = nov
}
@inproceedings{lf-protocol-85,
address = {Toulouse-Moissac, France},
month = jun,
year = 1985,
publisher = {North-Holland},
editor = {Diaz, Michel},
acronym = {{PSTV}'85},
booktitle = {{P}roceedings of the {IFIP} {WG}6.1
5th {I}nternational {C}onference on {P}rotocol
{S}pecification, {T}esting and {V}erification
({PSTV}'85)},
author = {Choquet, N. and Fribourg, Laurent and Mauboussin, A.},
missingauthor = {Mauboussin, Anne ?},
title = {Runnable Protocol Specifications Using the Logic
Interpreter {SLOG}},
pages = {149-168}
}
@inproceedings{lf-alp-88,
address = {Gaussig, German Democratic Republic},
month = nov,
year = 1988,
volume = 343,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Grabowski, Jan and Lescanne, Pierre and
Wechler, Wolfgang},
acronym = {{ALP}'88},
booktitle = {{P}roceedings of the 1st {I}nternational
{W}orkshop on {A}lgebraic and {L}ogic {P}rogramming
({ALP}'88)},
author = {Fribourg, Laurent},
title = {Functional Extensions to {P}rolog: {A}re They Needed?},
pages = {21-29},
note = {Invited paper}
}
@inproceedings{lf-ilps-88,
address = {Seattle, Washington, USA},
month = aug,
year = 1988,
publisher = {MIT Press},
editor = {Kowalski, Robert A. and Bowen, Kenneth A.},
acronym = {{ICLP}/{SLP}'88},
booktitle = {{P}roceedings of the 5th
{I}nternational {C}onference and {S}ymposium on
{L}ogic {P}rogramming
({ICLP}/{SLP}'88)},
author = {Fribourg, Laurent},
title = {Equivalence-Preserving Transformations of Inductive
Properties of {P}rolog Programs},
pages = {893-908}
}
@incollection{lf-academic-89,
author = {Laurent Fribourg},
title = {Proofs by Combinatory Induction on Recursively
Reducible Expressions},
editor = {Ait-Kaci, Hassan and Nivat, Maurice},
booktitle = {Resolution of Equations in Algebraic Structures},
chapter = {5},
pages = {117-141},
year = {1989},
publisher = {Academic Press},
month = mar
}
@article{lf-jsc-89,
publisher = {Elsevier Science Publishers},
journal = {Journal of Symbolic Computation},
author = {Fribourg, Laurent},
title = {A Strong Restriction of the Inductive Completion
Procedure},
volume = {8},
number = {3},
pages = {253-276},
year = {1989},
month = sep
}
@phdthesis{lf-hab-90,
author = {Fribourg, Laurent},
title = {Contribution {\`a} la v{\'e}rification des programmes
logiques},
year = {1990},
month = oct,
type = {M{\'e}moire d'habilitation},
school = {Universit{\'e} Paris~7, Paris, France}
}
@inproceedings{lf-iclp-90,
address = {Jerusalem, Israel},
month = jun,
year = 1990,
publisher = {MIT Press},
editor = {Warren, David H. D. and Szeredi, P{\'e}ter},
acronym = {{ICLP}'90},
booktitle = {{P}roceedings of the 7th
{I}nternational {C}onference on
{L}ogic {P}rogramming
({ICLP}'90)},
author = {Fribourg, Laurent},
title = {Extracting Logic Programs from Proofs that use
Extended {P}rolog Execution and Induction},
pages = {685-699}
}
@inproceedings{lf-plilp-90,
address = {Link{\"o}ping, Sweden},
month = aug,
year = 1990,
volume = 456,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Deransart, Pierre and Maluszynski, Jan},
acronym = {{PLILP}'90},
booktitle = {{P}roceedings of the 2nd {I}nternational
{W}orkshop on {P}rogramming {L}anguage
{I}mplementation and {L}ogic {P}rogramming
({PLILP}'90)},
author = {Fribourg, Laurent},
title = {A New {P}resburger Arithmetic Decision Procedure
Based on Extended {P}rolog Execution},
pages = {174-188}
}
@inproceedings{lf-ilps-91,
address = {San Diego, California, USA},
month = oct,
year = 1991,
publisher = {MIT Press},
editor = {Saraswat, Vijay A. and Ueda, Kazunori},
acronym = {{ICLP}'91},
booktitle = {{P}roceedings of the 8th
{I}nternational {C}onference on
{L}ogic {P}rogramming
({ICLP}'91)},
author = {Fribourg, Laurent},
title = {Automatic Generation of Simplification Lemmas for
Inductive Proofs},
pages = {103-116}
}
@inproceedings{lf-plilp-91,
address = {Passau, Germany},
month = aug,
year = 1991,
volume = 528,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Maluszynski, Jan and Wirsing, Martin},
acronym = {{PLILP}'91},
booktitle = {{P}roceedings of the 3rd {I}nternational
{S}ymposium on {P}rogramming {L}anguage
{I}mplementation and {L}ogic {P}rogramming
({PLILP}'91)},
author = {Cheong, Pui Hung and Fribourg, Laurent},
title = {Efficient Integration of Simplification into
{P}rolog},
pages = {359-370}
}
@inproceedings{lf-ho-lopstr-92,
address = {Manchester, UK},
year = 1993,
publisher = {Springer-Verlag},
editor = {Lau, Kung-Liu and Clement, Tim P.},
acronym = {{LOPSTR}'92},
booktitle = {{P}roceedings of the 2nd {I}nternational
{W}orkshop on {L}ogic {P}rogram {S}ynthesis
and {T}ransformation
({LOPSTR}'92)},
author = {Fribourg, Laurent and Ols{\'e}n, Hans},
title = {A Unifying View of Structural Induction and
Computation Induction for Logic Programs},
pages = {46-60},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LF-olsen92.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LF-olsen92.ps}
}
@inproceedings{lf-lics-92,
address = {Santa Cruz, California, USA},
month = jun,
year = 1992,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'92},
booktitle = {{P}roceedings of the 7th
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'92)},
author = {Fribourg, Laurent},
title = {Mixing List Recursion and Arithmetic},
pages = {419-429},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LF-lics92.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LF-lics92.ps}
}
@incollection{lf-wiley-93,
author = {Fribourg, Laurent},
title = {Extracting Logic Programs from Proofs that Use
Extended {P}rolog Execution with Induction},
editor = {J. M. Jacquet},
booktitle = {Constructing Logic Programs},
chapter = {2},
type = {chapter},
pages = {39-66},
year = {1993},
publisher = {John Wiley \& Sons, Ltd.},
month = mar,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LF-wiley93.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LF-wiley93.ps}
}
@incollection{phc-lf-mit-93,
author = {Cheong, Pui Hung and Fribourg, Laurent},
title = {Implementation of Narrowing: The {Prolog}-Based
Approach},
editor = {Apt, Krzysztof R. and de Bakker, Jaco W. and
Rutten, Jan J. M. M.},
booktitle = {Current Trends in Logic Programming Languages:
{I}ntegration with Functions, Constraints and
Objects},
chapter = {1},
type = {chapter},
pages = {1-20},
year = {1993},
month = mar,
publisher = {MIT Press},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LF-cheong93.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LF-cheong93.ps}
}
@inproceedings{lf-mvp-cade-94,
address = {Nancy, France},
month = jun,
year = 1994,
volume = 814,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Bundy, Alan},
acronym = {{CADE}'94},
booktitle = {{P}roceedings of the 12th {I}nternational
{C}onference on {A}utomated {D}eduction
({CADE}'94)},
author = {Fribourg, Laurent and Veloso{ }Peixoto, Marcos},
title = {Bottom-up Evaluation of {D}atalog Programs with
Arithmetical Constraints},
pages = {311-325}
}
@article{lf-mvp-tsi-94,
publisher = {Herm{\`e}s},
journal = {Technique et Science Informatiques},
author = {Fribourg, Laurent and Veloso{ }Peixoto, Marcos},
title = {Automates Concurrents \`a Contraintes},
volume = {13},
number = {6},
pages = {837-866},
year = {1994},
missingmonth = {},
missingnmonth = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LF-TSI94.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LF-TSI94.ps}
}
@inproceedings{lf-ho-lopstr-96,
address = {Stockholm, Sweden},
year = 1997,
volume = 1207,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Gallagher, John P.},
acronym = {{LOPSTR}'96},
booktitle = {{P}roceedings of the 6th {I}nternational
{W}orkshop on {L}ogic {P}rogram {S}ynthesis
and {T}ransformation
({LOPSTR}'96)},
author = {Fribourg, Laurent and Ols{\'e}n, Hans},
title = {Reductions of {P}etri Nets and Unfolding of
Propositional Logic Programs},
pages = {187-203}
}
@inproceedings{lf-jr-lopstr-96,
address = {Stockholm, Sweden},
year = 1997,
volume = 1207,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Gallagher, John P.},
acronym = {{LOPSTR}'96},
booktitle = {{P}roceedings of the 6th {I}nternational
{W}orkshop on {L}ogic {P}rogram {S}ynthesis
and {T}ransformation
({LOPSTR}'96)},
author = {Fribourg, Laurent and Richardson, Julian},
title = {Symbolic Verification with Gap-Order Constraints},
pages = {20-37},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LF-richardson96.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LF-richardson96.ps}
}
@inproceedings{lf-ho-concur-97,
address = {Warsaw, Poland},
month = jul,
year = 1997,
volume = 1243,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Mazurkiewicz, Antoni W. and Winkowski, J{\'o}zef},
acronym = {{CONCUR}'97},
booktitle = {{P}roceedings of the 8th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'97)},
author = {Fribourg, Laurent and Ols{\'e}n, Hans},
title = {Proving Safety Properties of Infinite State Systems by
Compilation into {P}resburger Arithmetic},
pages = {213-227},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LF-concur97.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LF-concur97.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LF-concur97.pdf}
}
@article{lf-ho-constraint-97,
publisher = {Kluwer Academic Publishers},
journal = {Constraints},
author = {Fribourg, Laurent and Ols{\'e}n, Hans},
title = {A Decompositional Approach for Computing Least
Fixed-Points of {D}atalog Programs with {Z}-Counters},
volume = {2},
number = {3-4},
pages = {305-335},
year = {1997},
missingmonth = {>oct},
missingnmonth = {>10},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LF-constraints97.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LF-constraints97.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LF-constraints97.pdf}
}
@inproceedings{lf-ho-infinity-97,
address = {Bologna, Italy},
month = jul,
year = 1997,
volume = 9,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Moller, Faron},
acronym = {{INFINITY}'97},
booktitle = {{P}roceedings of the 2nd {I}nternational
{W}orkshop on {V}erification of {I}nfinite
{S}tate {S}ystems
({INFINITY}'97)},
author = {Fribourg, Laurent and Ols{\'e}n, Hans},
title = {Reachability Sets of Parametrized Rings As Regular
Languages},
pages = {40},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LF-infinity97.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LF-infinity97.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LF-infinity97.pdf}
}
@techreport{LSV:98:2,
author = {Fribourg, Laurent},
title = {A Closed-Form Evaluation for Extended Timed Automata},
type = {Research Report},
number = {LSV-98-2},
year = {1998},
month = mar,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-1998-2.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-1998-2.rr.ps}
}
@inproceedings{lf-mvp-latin-98,
address = {Campinas, Brasil},
month = apr,
year = 1998,
volume = 1380,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Lucchesi, Claudio L. and Moura, Arnaldo V.},
acronym = {{LATIN}'98},
booktitle = {{P}roceedings of the 3rd {L}atin {A}merican
{S}ymposium on {T}heoretical {I}nformatics
({LATIN}'98)},
author = {Veloso{ }Peixoto, Marcos and Fribourg, Laurent},
title = {Unfolding Parametric Automata},
pages = {88-101}
}
@inproceedings{beauquier99,
address = {Bratislava, Slovak republic},
month = sep,
year = 1999,
volume = 1693,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Jayanti, Prasad},
acronym = {{DISC}'99},
booktitle = {{P}roceedings of the 13th {I}nternational
{S}ymposium on {D}istributed {C}omputing
({DISC}'99)},
author = {Beauquier, Joffroy and B{\'e}rard, B{\'e}atrice
and Fribourg, Laurent},
title = {A New Rewrite Method for Proving Convergence of
Self-Stabilizing Systems},
pages = {240-253},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBF-disc99.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBF-disc99.ps}
}
@inproceedings{berard99,
address = {Trento, Italy},
month = jul,
year = 1999,
volume = 1633,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Halbwachs, Nicolas and Peled, Doron},
acronym = {{CAV}'99},
booktitle = {{P}roceedings of the 11th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'99)},
author = {B{\'e}rard, B{\'e}atrice and Fribourg, Laurent},
title = {Automated Verification of a Parametric Real-Time
Program: {T}he {ABR} Conformance Protocol},
pages = {96-107},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BerFri-cav99.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BerFri-cav99.ps}
}
@inproceedings{berard99b,
address = {Eindhoven, The Netherlands},
month = aug,
year = 1999,
volume = 1664,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Baeten, Jos C. M. and Mauw, Sjouke},
acronym = {{CONCUR}'99},
booktitle = {{P}roceedings of the 10th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'99)},
author = {B{\'e}rard, B{\'e}atrice and Fribourg, Laurent},
title = {Reachability Analysis of (Timed) {P}etri Nets Using
Real Arithmetic},
pages = {178-193},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BerFri-concur99.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BerFri-concur99.ps}
}
@misc{Calife-1.1,
author = {B{\'e}rard, B{\'e}atrice and Cast{\'e}ran, Pierre
and Fleury, Emmanuel and
Fribourg, Laurent and Monin, Jean-Fran{\c{c}}ois
and Paulin, {\relax Ch}ristine and Petit, Antoine and
Rouillard, Davy},
title = {Document de sp{\'e}cification du mod{\`e}le
commun},
year = {2000},
month = apr,
howpublished = {Fourniture~1.1 du projet RNRT Calife},
lsv-lang = {FR}
}
@misc{Calife-4.1,
author = {Fribourg, Laurent},
title = {Document de synth{\`e}se sur les techniques
d'abstraction},
year = {2000},
month = jan,
howpublished = {Fourniture~4.1 du projet RNRT Calife},
lsv-lang = {FR}
}
@inproceedings{LF-LOPSTR-99,
address = {Venezia, Italy},
year = 2000,
volume = 1817,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Bossi, Annalisa},
acronym = {{LOPSTR}'99},
booktitle = {{P}roceedings of the 9th {I}nternational
{W}orkshop on {L}ogic {P}rogram {S}ynthesis
and {T}ransformation
({LOPSTR}'99)},
author = {Laurent Fribourg},
title = {Constraint Logic Programming Applied to Model
Checking},
pages = {31-42},
note = {Invited tutorial},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Fri-lopstr99.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Fri-lopstr99.ps}
}
@inproceedings{LF-WFPL-99,
address = {Benicassim, Spain},
month = sep,
year = 2000,
optaddress = {Valencia, Spain},
publisher = {Universidad Polit{\'e}cnica de Valencia, Spain},
editor = {Alpuente, Mar{\'i}a},
acronym = {{WFLP} 2000},
booktitle = {{P}roceedings of the 9th {I}nternational
{W}orkshop on {F}unctional and {L}ogic
{P}rogramming
({WFLP} 2000)},
author = {Laurent Fribourg},
title = {{P}etri Nets, Flat Languages and Linear Arithmetic},
pages = {344-365},
note = {Invited lecture},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Fri-wflp00.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Fri-wflp00.ps}
}
@misc{stabilo,
author = {Nilsson, Ulf and Duflot, Marie and Fribourg, Laurent},
title = {{STABILO}, a tool computing inevitable configurations
in distributed protocols},
year = {2000},
month = nov,
note = {See description in~\cite{DFN-concur-2001}.
Written in PROLOG (about 500 lines on top of
Gertjan van Noord's finite automata package)}
}
@article{BBFM-DISTCOMP,
publisher = {Springer},
journal = {Distributed Computing},
author = {Beauquier, Joffroy and B{\'e}rard, B{\'e}atrice and
Fribourg, Laurent and Magniette, Fr{\'e}d{\'e}ric},
title = {Proving Convergence of Self-Stabilizing Systems Using
First-Order Rewriting and Regular Languages},
volume = {14},
number = {2},
pages = {83-95},
year = {2001},
missingmonth = {},
missingnmonth = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBFM-DISCOMP2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBFM-DISCOMP2000.ps},
doi = {10.1007/PL00008931}
}
@inproceedings{DFN-concur-2001,
address = {Aalborg, Denmark},
month = aug,
year = 2001,
volume = 2154,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Larsen, Kim G. and Nielsen, Modens},
acronym = {{CONCUR}'01},
booktitle = {{P}roceedings of the 12th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'01)},
author = {Duflot, Marie and Fribourg, Laurent and Nilsson, Ulf},
title = {Unavoidable Configurations of Parameterized Rings of
Processes},
pages = {472-486},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DFN-concur2001.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DFN-concur2001.ps}
}
@inproceedings{DFP-disc2001,
address = {Lisbon, Portugal},
month = oct,
year = 2001,
volume = 2180,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Welch, Jennifer L.},
acronym = {{DISC}'01},
booktitle = {{P}roceedings of the 15th {I}nternational
{S}ymposium on {D}istributed {C}omputing
({DISC}'01)},
author = {Duflot, Marie and Fribourg, Laurent and Picaronny, Claudine},
title = {Randomized Finite-State Distributed Algorithms as
{M}arkov Chains},
pages = {240-254},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DFP-disc2001.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DFP-disc2001.ps}
}
@inproceedings{DFP-tcs2002,
address = {Montr{\'e}al, Qu{\'e}bec, Canada},
month = aug,
year = 2002,
volume = 223,
series = {IFIP Conference Proceedings},
publisher = {Kluwer Academic Publishers},
editor = {Baeza-Yates, Ricardo A. and Montanari, Ugo and
Santoro, Nicolas},
acronym = {{IFIP~TCS}'02},
booktitle = {{P}roceedings of the 2nd {IFIP} {I}nternational
{C}onference on {T}heoretical {C}omputer
{S}cience
({IFIP~TCS}'02)},
author = {Duflot, Marie and Fribourg, Laurent and
Picaronny, Claudine},
title = {Randomized Dining Philosophers without Fairness
Assumption},
pages = {169-180},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DFP-tcs02.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DFP-tcs02.ps}
}
@techreport{LSV:02:12,
author = {Fribourg, Laurent and Messika, St{\'e}phane and
Picaronny, Claudine},
title = {Traces of Randomized Distributed Algorithms as {G}ibbs
Fields},
type = {Research Report},
number = {LSV-02-12},
year = {2002},
month = sep,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
note = {16 pages},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2002-12.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2002-12.rr.ps}
}
@article{BFKM-FMSD,
publisher = {Kluwer Academic Publishers},
journal = {Formal Methods in System Design},
author = {B{\'e}rard, B{\'e}atrice and Fribourg, Laurent and
Klay, Francis and
Monin, Jean-Fran{\c{c}}ois},
title = {A Compared Study of Two Correctness Proofs for the
Standardized Algorithm of {ABR} Conformance},
volume = {22},
number = {1},
pages = {59-86},
year = {2003},
month = jan,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BFKM-FMSD.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BFKM-FMSD.ps},
doi = {10.1023/A:1021704214464}
}
@techreport{LSV:03:10,
author = {Fribourg, Laurent and Messika, St{\'e}phane and
Picaronny, Claudine},
title = {Traces of Randomized Distributed Algorithms As
{M}arkov Fields. {A}pplication to Rapid Mixing},
type = {Research Report},
number = {LSV-03-10},
year = {2003},
month = jul,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
note = {19~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2003-10.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2003-10.rr.ps}
}
@techreport{LSV:03:7,
author = {Fribourg, Laurent and Messika, St{\'e}phane and
Picaronny, Claudine},
title = {On the Absence of Phase Transition in Randomized
Distributed Algorithms},
type = {Research Report},
number = {LSV-03-7},
year = {2003},
month = apr,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
note = {17~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2003-7.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2003-7.rr.ps}
}
@techreport{Averroes-4.2.2,
author = {Duflot, Marie and Fribourg, Laurent and
H{\'e}rault, {\relax Th}omas and
Lassaigne, Richard and
Magniette, Fr{\'e}d{\'e}ric and
Messika, St{\'e}phane and
Peyronnet, Sylvain and Picaronny, Claudine},
title = {Probabilistic Model Checking of the {CSMA/CD} Protocol
Using {PRISM} and {APMC}},
year = {2004},
month = jun,
type = {Contract Report},
number = {(Lot 4.2 fourniture 2)},
institution = {projet RNTL Averroes},
oldhowpublished = {Lot 4.2 fourniture 2, du projet RNTL Averroes},
note = {22~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Averroes-4.2.2.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Averroes-4.2.2.ps}
}
@techreport{Averroes-4.2.3,
author = {Fribourg, Laurent and Messika, St{\'e}phane and
Picaronny, Claudine},
title = {Parametric and Probabilistic Verification of
{N}icollin-{S}ifakis-{Y}ovine's Model of
the {CSMA/CD} Protocol},
year = {2004},
month = jun,
type = {Contract Report},
number = {(Lot 4.2 fourniture 3)},
institution = {projet RNTL Averroes},
oldhowpublished = {Lot 4.2 fourniture 3, du projet RNTL Averroes},
note = {17~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Averroes-4.2.3.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Averroes-4.2.3.ps}
}
@inproceedings{DFH-avocs2004,
address = {London, UK},
month = may,
year = {2005},
number = 6,
volume = {128},
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Huth, Michael R. A.},
acronym = {{AVoCS}'04},
booktitle = {{P}roceedings of the 4th {I}nternational
{W}orkshop on {A}utomated {V}erification
of {C}ritical {S}ystems
({AVoCS}'04)},
author = {Duflot, Marie and Fribourg, Laurent and
H{\'e}rault, {\relax Th}omas and
Lassaigne, Richard and Magniette, Fr{\'e}d{\'e}ric
and Messika, St{\'e}phane and
Peyronnet, Sylvain and Picaronny, Claudine},
title = {Probabilistic Model Checking of the {CSMA/CD} Protocol
Using {PRISM} and {APMC}},
pages = {195-214},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DFH-avocs2004.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DFH-avocs2004.pdf},
doi = {10.1016/j.entcs.2005.04.012}
}
@article{DFP-DISTCOMP,
publisher = {Springer},
journal = {Distributed Computing},
author = {Duflot, Marie and Fribourg, Laurent and
Picaronny, Claudine},
title = {Randomized Dining Philosophers Without Fairness
Assumption},
volume = {17},
number = {1},
pages = {65-76},
year = {2004},
month = feb,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DFP-DISCOMP.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DFP-DISCOMP.ps},
doi = {10.1007/s00446-003-0102-z}
}
@inproceedings{FMP-disc04,
address = {Amsterdam, The Netherlands},
month = oct,
year = 2004,
volume = 3274,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Guerraoui, Rachid},
acronym = {{DISC}'04},
booktitle = {{P}roceedings of the 18th {I}nternational
{S}ymposium on {D}istributed {C}omputing
({DISC}'04)},
author = {Fribourg, Laurent and Messika, St{\'e}phane and
Picaronny, Claudine},
title = {Coupling and Self-Stabilization},
pages = {201-215},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FMP-disc04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FMP-disc04.pdf}
}
@techreport{LSV:04:12,
author = {Fribourg, Laurent and Messika, St{\'e}phane and
Picaronny, Claudine},
title = {Mixing Time of the Asymmetric Simple Exclusion Problem
on a Ring with Two Particles},
type = {Research Report},
number = {LSV-04-12},
year = {2004},
month = jun,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
note = {15~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2004-12.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2004-12.rr.ps}
}
@inproceedings{FM-podc05,
address = {Las Vegas, Nevada, USA},
month = jul,
year = 2005,
publisher = {ACM Press},
editor = {Aguilera, Marcos Kawazoe and Aspnes, James},
acronym = {{PODC}'05},
booktitle = {{P}roceedings of the {T}wenty-{F}ourth {A}nnual
{ACM} {SIGACT}-{SIGOPS} {S}ymposium
on {P}rinciples of {D}istributed {C}omputing
({PODC}'05)},
author = {Fribourg, Laurent and Messika, St{\'e}phane},
title = {Brief Announcement: Coupling for {M}arkov Decision
Processes~--- {A}pplication to Self-Stabilization with Arbitrary
Schedulers},
pages = {322},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ba173-messika.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ba173-messika.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ba173-messika.ps},
doi = {10.1145/1073814.1073875}
}
@inproceedings{CEFX-formats06,
address = {Paris, France},
month = sep,
year = 2006,
volume = 4202,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Asarin, Eug{\`e}ne and Bouyer, Patricia},
acronym = {{FORMATS}'06},
booktitle = {{P}roceedings of the 4th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'06)},
author = {Chevallier, R{\'e}my and Encrenaz{-}Tiph{\`e}ne, Emmanuelle and
Fribourg, Laurent and Xu, Weiwen},
title = {Verification of the Generic Architecture of a Memory Circuit Using
Parametric Timed Automata},
pages = {113-127},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CEFX-formats06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CEFX-formats06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CEFX-formats06.ps},
econtrat = {MEDEA+ Blueberries},
doi = {10.1007/11867340_9},
abstract = {Using a variant of Clariso-Cortadella's parametric method
for verifying asynchronous circuits, we formally derive a set of linear
constraints that ensure the correctness of some crucial timing behaviours
of the architecture of SPSMALL memory. This allows us to check two
different implementations of this architecture.}
}
@article{CEFX-wseas06,
publisher = {World Scientific and Engineering Academy and Society},
journal = {WSEAS Transactions on Circuits and Systems},
author = {Chevallier, R{\'e}my and Encrenaz{-}Tiph{\`e}ne, Emmanuelle and
Fribourg, Laurent and Xu, Weiwen},
title = {Timing analysis of an embedded memory: {SPSMALL}},
pages = {973-978},
volume = 5,
number = 7,
year = 2006,
month = jul,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CEFX-wseas06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CEFX-wseas06.pdf},
abstract = {This paper proposes a high-level formalism, called
Abstract Functional and Timing Graph~(AFTG), for describing a memory
architecture, which combines logical functionality and timing. After
translation of the~AFTG into the form a timed automaton, we are able to
compute the response times of the modeled memory, and check their consistency
with the values specified in the datasheet. We also address the problem of
finding optimal values of setup timings.}
}
@article{FMP-dc05,
publisher = {Springer},
journal = {Distributed Computing},
author = {Fribourg, Laurent and Messika, St{\'e}phane and
Picaronny, Claudine},
title = {Coupling and Self-Stabilization},
year = 2006,
month = feb,
volume = 18,
number = 3,
pages = {221-232},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/dcmessika.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/dcmessika.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/dcmessika.pdf},
doi = {10.1007/s00446-005-0142-7},
abstract = {A randomized self-stabilizing algorithm~\(\mathcal{A}\)
is an algorithm that, whatever the initial configuration
is, reaches a set~\(\mathcal{L}\) of \emph{legal configurations} in finite time
with probability~1. The proof of convergence towards~\(\mathcal{L}\)
is generally done by exhibiting a potential function~\(\varphi\),
which measures the {"}vertical{"} distance of any configuration
to~\(\mathcal{L}\), such that \(\varphi\) decreases with non-null probability
at each step of~\(\mathcal{A}\). We propose here a method, based on
the notion of coupling, which makes use of a {"}horizontal{"}
distance~\(\delta\) between any pair of configurations, such that \(\delta\)
decreases in expectation at each step of~\(\mathcal{A}\). In contrast
with classical methods, our coupling method does not
require the knowledge of~\(\mathcal{L}\). In addition to the proof of
convergence, the method allows us to assess the convergence
rate according to two different measures. Proofs
produced by the method are often simpler or give better
upper bounds than their classical counterparts, as
examplified here on Herman's mutual exclusion and Iterated
Prisoner's Dilemma algorithms in the case of cyclic
graphs.}
}
@techreport{Averroes-4.2.6,
author = {Fribourg, Laurent and Picaronny, Claudine and Pinot, Simon},
title = {Manipulation de backoff dans~{CSMA/CA}},
year = 2006,
month = mar,
type = {Contract Report},
number = {(Lot~4.2 fourniture~6)},
institution = {projet RNTL Averroes},
note = {20~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Averroes-4.2.6.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Averroes-4.2.6.pdf}
}
@article{CEFX-fmsd08,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Chevallier, R{\'e}my and Encrenaz{-}Tiph{\`e}ne, Emmanuelle and
Fribourg, Laurent and Xu, Weiwen},
title = {Timed Verification of the Generic Architecture of a Memory
Circuit Using Parametric Timed Automata},
volume = 34,
number = 1,
pages = {59-81},
year = 2009,
month = feb,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CEFX-fmsd08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CEFX-fmsd08.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CEFX-fmsd08.ps},
doi = {10.1007/s10703-008-0061-x},
abstract = {Using a variant of Clariso-Cortadella's parametric
method for verifying asynchronous circuits, we analyse some crucial timing
behaviors of the architecture of SPSMALL memory, a~commercial product of
STMicroelectronics. Using the model of parametric timed automata and model
checker HYTECH, we~formally derive a set of linear constraints that ensure
the correctness of the response times of the memory. We are also able to
infer the constraints characterizing the optimal setup timings of input
signals. We have checked, for two different implementations of this
architecture, that the values given by our model match remarkably with the
values obtained by the designer through electrical simulation. }
}
@techreport{LSV:07:21,
author = {Chamseddine, Najla and Duflot, Marie and Fribourg, Laurent and Picaronny, Claudine},
title = {Determinate Probabilistic Timed Automata as {M}arkov Chains with
Parametric Costs},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = 2007,
month = may,
type = {Research Report},
number = {LSV-07-21},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-21.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-21.pdf},
note = {17~pages},
abstract = {We consider probabilistic systems modeled under the form of a
special class of probabilistic timed automata. Such automata have {"}no
choice{"}: when the automaton arrives at a node, the time at which it will
leave it is determined; and when the automaton leaves the node, there is
just one distribution of target nodes.\par
In the paper, we give a method for computing the expected time~\(A\) for
the automaton to reach an {"}absorbing{"} node. Roughly speaking, the
method consists in putting the automaton under the form of a Markov chain
with costs (corresponding to durations). Under certain conditions, the
method is parametric in the sense that \(A\)~is computed as a function of
the constants appearing in the outgoing conditions and the invariants of
nodes, but does not assume known their explicit values.\par
We illustrate the method on the CSMA/CD protocol.}
}
@inproceedings{ACEF-rp08,
address = {Liverpool, UK},
month = dec,
year = 2008,
volume = 223,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Halava, Vesa and Potapov, Igor},
acronym = {{RP}'08},
booktitle = {{P}roceedings of the 2nd {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'08)},
author = {Andr{\'e}, {\'E}tienne and Chatain, {\relax Th}omas and
Encrenaz, Emmanuelle and Fribourg, Laurent},
title = {An Inverse Method for Parametric Timed Automata},
pages = {29-46},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACEF-rp08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACEF-rp08.pdf},
doi = {10.1016/j.entcs.2008.12.029},
abstract = {Given a timed automaton with parametric timings, our objective
is to describe a procedure for deriving constraints on the parametric
timings in order to ensure that, for~each value of parameters satisfying
these constraints, the behaviors of the timed automata are time-abstract
equivalent. We~will exploit a reference valuation of the parameters that
is supposed to capture a characteristic proper behavior of the system.
The~method has been implemented and is illustrated on various examples of
asynchronous circuits.}
}
@inproceedings{EF-lix06,
address = {Palaiseau, France},
month = apr,
year = 2008,
volume = 209,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Palamidessi, Catuscia and Valencia, Franck},
acronym = {{LIX}'06},
booktitle = {{P}roceedings of the {LIX} {C}olloquium on {E}merging
{T}rends in {C}oncurrency {T}heory
({LIX}'06)},
author = {Encrenaz, Emmanuelle and Fribourg, Laurent},
title = {Time Separation of Events: An Inverse Method},
pages = {135-148},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EF-lix06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EF-lix06.pdf},
doi = {10.1016/j.entcs.2008.04.008},
abstract = {The problem of {"}time separation{"} can be stated as follows:
Given a system made of several connected components, each
one entailing a local delay known with uncertainty, what is
the maximum time for traversing the global system? This
problem is useful, \textit{e.g.} in the domain of digital circuits,
for determining the global traversal time of a signal from
the knowledge of bounds on the component propagation delays.
The uncertainty on each component delay is given under the
form of an interval. The general problem is NP-complete. We
focus here on the inverse problem: we seek intervals for
component delays for which the global traversal time is
guaranteed to be no greater than a specified maximum. We
give a polynomial time method to solve it. As a typical
application, we show how to use the method in order to relax
some specified local delays while preserving the maximum
traversal time. This is especially useful, in the area of
digital circuits, for optimizing {"}setup{"} timings of input
signals (minimum timings required for stability).}
}
@unpublished{LF-probastab,
author = {Fribourg, Laurent},
title = {Probabilistic Self-Stabilizing Algorithms, {M}arkov Chains and
{M}arkov Decision Processes},
year = {2007},
month = oct # {-} # nov,
note = {Course notes, {M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LF-probastab.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LF-probastab.pdf}
}
@inproceedings{AFS-avocs09,
address = {Swansea, UK},
month = sep,
year = {2009},
volume = 23,
series = {Electronic Communications of the EASST},
publisher = {European Association of Software Science and Technology},
editor = {Roggenbach, Markus},
acronym = {{AVoCS}'09},
booktitle = {{P}roceedings of the 9th {I}nternational
{W}orkshop on {A}utomated {V}erification
of {C}ritical {S}ystems
({AVoCS}'09)},
author = {Andr{\'e}, {\'E}tienne and Fribourg, Laurent and Sproston,
Jeremy},
title = {An Extension of the Inverse Method to Probabilistic Timed Automata},
nopages = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AFS-avocs09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AFS-avocs09.pdf},
abstract = {Probabilistic timed automata can be used to model systems in
which probabilistic and timing behavior coexist. Verification of
probabilistic timed automata models is generally performed with regard to
a single reference valuation of the timing parameters. Given such a
parameter valuation, we present a method for obtaining automatically a
constraint on timing parameters for which the reachability probabilities
(1)~remain invariant and (2)~are~equal to the reachability probabilities
for the reference valuation. The method relies on parametric analysis of a
non-probabilistic version of the probabilistic timed automata model using
the {"}inverse method{"}. Our approach is useful for avoiding repeated
executions of probabilistic model checking analyses for the same model
with different parameter valuations. We provide examples of the
application of our technique to models of randomized protocols.}
}
@techreport{LSV:09:13,
author = {Andr{\'e}, {\'E}tienne and Encrenaz, Emmanuelle and Fribourg, Laurent},
title = {Synthesizing Parametric Constraints on Various Case Studies Using {IMITATOR}},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2009},
month = jun,
type = {Research Report},
number = {LSV-09-13},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-13.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-13.pdf},
note = {18~pages},
abstract = {We present here applications of IMITATOR, a tool for
synthesizing constraints on timing bounds (seen as parameters) in the
framework of timed automata. Unlike classical synthesis methods, we take
advantage of a given reference valuation of the parameters for which the
system is known to behave properly. Our aim is to generate a constraint
such that, under any valuation satisfying this constraint, the system is
guaranteed to behave, in terms of alternating sequences of locations and
actions, as under the reference valuation. This is useful for safely
relaxing some values of the reference valuation, and optimizing timing
bounds of the system. We have successfully applied our tool to various
examples of asynchronous circuits and protocols, which are detailed in
this report.}
}
@inproceedings{AF-infinity09,
address = {Bologna, Italy},
month = nov,
year = 2009,
volume = 10,
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Farzan, Azadeh and Legay, Axel},
acronym = {{INFINITY}'09},
booktitle = {{P}roceedings of the 11th {I}nternational
{W}orkshops on {V}erification of {I}nfinite
{S}tate {S}ystems
({INFINITY}'09)},
author = {Andr{\'e}, {\'E}tienne and Fribourg, Laurent},
title = {An Inverse Method for Policy-Iteration Based Algorithms},
pages = {44-61},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AF-infinity09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AF-infinity09.pdf},
doi = {10.4204/EPTCS.10.4},
abstract = {We present an extension of two policy-iteration based algorithms
on weighted graphs (viz.,~Markov Decision Problems and Max-Plus Algebras).
This extension allows us to solve the following inverse problem:
considering the weights of the graph to be unknown constants or
parameters, we suppose that a reference instantiation of those weights is
given, and we aim at computing a constraint on the parameters under which
an optimal policy for the reference instantiation is still optimal. The
original algorithm is thus guaranteed to behave well around the reference
instantiation, which provides us with some criteria of robustness. We
present an application of both methods to simple examples. A prototype
implementation has been done.}
}
@inproceedings{ACDFR-msr09,
address = {Nantes, France},
month = nov,
year = 2009,
number = {7-9},
volume = {43},
series = {Journal Europ{\'e}en des Syst{\`e}mes Automatis{\'e}s},
publisher = {Herm{\`e}s},
editor = {Lime, Didier and Roux, Olivier H.},
acronym = {{MSR}'09},
booktitle = {{A}ctes du 7{\`e}me {C}olloque sur la
{M}od{\'e}lisation des {S}yst{\`e}mes
{R}{\'e}actifs
({MSR}'09)},
author = {Andr{\'e}, {\'E}tienne and Chatain, {\relax Th}omas and
De{ }Smet, Olivier and Fribourg, Laurent and Ruel, Silvain},
title = {Synth{\`e}se de contraintes temporis{\'e}es pour
une architecture d'automatisation en r{\'e}seau},
pages = {1049-1064},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACDFR-msr09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACDFR-msr09.pdf},
abstract = {We deal with the problem of synthesis of timing constraints for
concurrent systems. Such systems are modeled by networks of timed automata
where some constants, represented as parameters, can be tuned. A suitable
value of these parameters is assumed to be known from a preliminarily
simulation process. We present a method which infers a zone of suitable
points around this reference functioning point. This zone is defined by a
system of linear inequalities over the parameters. This method is applied
to the case study of a networked automation system.}
}
@article{ACEF-ijfcs09,
publisher = {World Scientific},
journal = {International Journal of Foundations of Computer Science},
author = {Andr{\'e}, {\'E}tienne and Chatain, {\relax Th}omas and
Encrenaz, Emmanuelle and Fribourg, Laurent},
title = {An Inverse Method for Parametric Timed Automata},
volume = 20,
number = 5,
pages = {819-836},
month = oct,
year = 2009,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACEF-ijfcs09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACEF-ijfcs09.pdf},
doi = {10.1142/S0129054109006905},
abstract = {We consider in this paper systems modeled by timed automata. The
timing bounds involved in the action guards and location invariants of our
timed automata are not constants, but parameters. Those parametric timed
automata allow the modelling of various kinds of timed systems,
\textit{e.g.} communication protocols or asynchronous circuits. We will
also assume that we are given an initial tuple~\(\pi_0\) of values for the
parameters, which corresponds to values for which the system is known to
behave properly. Our goal is to compute a constraint~\(K_0\) on the
parameters, satisfied by~\(\pi_0\), guaranteeing that, under any parameter
valuation satisfying~\(K_0\), the system behaves in the same manner: for any
two parameter valuations satisfying~\(K_0\), the behaviors of the timed
automata are (time-abstract) equivalent, \textit{i.e.}, the traces of execution
viewed as alternating sequences of actions and locations are identical. We
present an algorithm \texttt{InverseMethod} that terminates in the case of acyclic
models, and discuss how to extend it in the cyclic case. We also explain
how to combine our method with classical synthesis methods which are based
on the avoidance of a given set of bad states. A prototype implementation
has been done, and various experiments are described.}
}
@misc{valmem-D4243,
author = {Andr{\'e}, {\'E}tienne and Bara, Abdelrezzak and
Bazargan{-}Sabet, Pirouz and Chevallier, R{\'e}my and Le{~}D{\^u},
Dominique and Encrenaz, Emmanuelle and Fribourg, Laurent and
Renault, Patricia},
title = {Experiments of Prototype Tools on Case Studies,
Comparison of Obtained Results and Conclusion},
note = {31~pages},
type = {Contract Report},
year = {2010},
month = dec,
howpublished = {Deliverables VALMEM~4.2 and~4.3, (ANR-06-ARFU-005)},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/valmem-d4243.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/valmem-d4243.pdf},
abstract = {This document concludes the VALMEM project by applying the set
of tools developed during the project to (some~of) the case studies defined
initially. The obtained results are discussed and compared with standard
methodologies outcomes.}
}
@inproceedings{AF-rp10,
address = {Brno, Czech Republic},
month = aug,
year = 2010,
volume = 6227,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ku{\v c}era, Anton{\'\i}n and Potapov, Igor},
acronym = {{RP}'10},
booktitle = {{P}roceedings of the 4th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'10)},
author = {Andr{\'e}, {\'E}tienne and Fribourg, Laurent},
title = {Behavioral Cartography of Timed Automata},
pages = {76-90},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AF-rp10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AF-rp10.pdf},
doi = {10.1007/978-3-642-15349-5_5},
abstract = {We aim at finding a set of timing parameters for which a given
timed automaton has a {"}good{"} behavior. We~present here a novel
approach based on the decomposition of the parametric space into
behavioral tiles, \textit{i.e.}, sets of parameter valuations for which
the behavior of the system is uniform. This gives us a behavioral
cartography according to the values of the parameters.\par
It is then straightforward to partition the space into a {"}good{"} and a
{"}bad{"} subspace, according to the behavior of the tiles. We extend this
method to probabilistic systems, allowing to decompose the parametric
space into tiles for which the minimal (resp. maximal) probability of
reaching a given location is uniform. An~implementation has been made, and
experiments successfully conducted.}
}
@inproceedings{FRS-infinity11,
address = {Taipei, Taiwan},
month = oct,
year = 2011,
volume = 73,
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Chen, Yu-Fang and Wang, Chao},
acronym = {{INFINITY}'11},
booktitle = {{P}roceedings of the 13th {I}nternational
{W}orkshops on {V}erification of {I}nfinite
{S}tate {S}ystems
({INFINITY}'11)},
author = {Fribourg, Laurent and Revol, Bertrand and Soulat, Romain},
title = {Synthesis of Switching Rules for Ensuring Reachability
Properties of Sampled Linear Systems},
pages = {35-48},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FRS-infinity11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FRS-infinity11.pdf},
doi = {10.4204/EPTCS.73.6},
abstract = {We consider here systems with piecewise linear dynamics that are
periodically sampled with a given period~\(\tau\). At each sampling time,
the mode of the system, i.e., the parameters of the linear dynamics, can
be switched, according to a switching rule. Such systems can be modelled
as a special form of hybrid automata, called {"}switched systems{"}, that
are automata with an \emph{infinite} real state space. The problem is to
find a switching rule that guarantees the system to still be in a given
area~\(V\) at the next sampling time, and so on indefinitely. In this
paper, we will consider two approaches: the~\emph{indirect} one that
abstracts the system under the form of a finite discrete event system, and
the \emph{direct} one that works on the continuous state space.\par
Our methods rely on previous works, but we specialize them to a simplified
context (linearity, periodic switching instants, absence of control
input), which is motivated by the features of a focused case study:
a~DC-DC boost converter built by electronics laboratory SATIE
(ENS~Cachan). Our enhanced methods allow us to treat successfully this
real-life example.}
}
@inproceedings{FK-RP11,
address = {Genova, Italy},
month = sep,
year = 2011,
volume = {6945},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Delzanno, Giorgio and Potapov, Igor},
acronym = {{RP}'11},
booktitle = {{P}roceedings of the 5th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'11)},
author = {Fribourg, Laurent and K{\"u}hne, Ulrich},
title = {Parametric Verification and Test Coverage for Hybrid Automata
Using the Inverse Method},
pages = {191-204},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FK-RP11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FK-RP11.pdf},
doi = {10.1007/978-3-642-24288-5_17},
abstract = {Hybrid systems combine continuous and discrete behavior. Hybrid
Automata are a powerful formalism for the modeling and verification of
such systems. A~common problem in hybrid system verification is the good
parameters problem, which consists in identifying a set of parameter
valuations which guarantee a certain behavior of a system. Recently, a
method has been presented for attacking this problem for Timed Automata.
In this paper, we show the extension of this methodology for hybrid
automata with linear and affine dynamics. The method is demonstrated with
a hybrid system benchmark from the literature.}
}
@techreport{lsv-11-18,
author = {Florentin, {\'E}ric and Fribourg, Laurent and K{\"u}hne, Ulrich and
Lefebvre, St{\'e}phane and Rey, {\relax Ch}ristian},
title = {{COUPLET}: Coupled Electrothermal Simulation},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2011},
month = jun,
type = {Research Report},
number = {LSV-11-18},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2011-18.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2011-18.pdf},
note = {32~pages},
abstract = {The~aim of the project COUPLET (supported by Institut
Farman) is to study the electrothermal effects of
the degradation of the metallisation layer of power
semiconductor dies. In this first technical report
of the project, we describe our work of modeling and
simulation of the behavior of a power
transistor. The die is represented by four
elementary transistors driven by a distributed gate
signal. A~simplified electrical model is used to
simulate the transistor behavior at turn-off. The
thermal model is realized by finite elements methods
and allows to estimate the maximum temperature on
each elementary transistor. By~coupling the thermal
model with the electric simulation, it is possible
to take into account silicon and metallisation
heating in the electrical model.}
}
@techreport{rr-lsv-11-04,
author = {Fribourg, Laurent and K{\"u}hne, Ulrich},
title = {Parametric Verification of Hybrid Automata Using the Inverse Method},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2011},
month = mar,
type = {Research Report},
number = {LSV-11-04},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2011-04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2011-04.pdf},
note = {25~pages},
abstract = {Hybrid systems combine continuous and discrete behavior. Hybrid
Automata are a powerful formalism for the modeling and verification of
such systems. A~common problem in hybrid system verification is the good
parameters problem, which consists in identifying a subset of parameters
which guarantee a certain behavior of a system. Recently, a method has
been presented for attacking this problem for Timed Automata. In this
report, we show the extension of this methodology for hybrid automata with
linear and affine dynamics. The method is demonstrated with a distributed
temperature control system and several other hybrid system benchmarks from
the literature.}
}
@misc{valmem-final,
author = {Andr{\'e}, {\'E}tienne and Bara, Abdelrezzak and
Bazargan{-}Sabet, Pirouz and Chevallier, R{\'e}my and Le{~}D{\^u},
Dominique and Encrenaz, Emmanuelle and Fribourg, Laurent and
Renault, Patricia},
title = {Compte-rendu de fin du projet {ANR} {VALMEM}},
note = {14~pages},
type = {Contract Report},
year = {2011},
month = jan,
nohowpublished = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/valmem-final.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/valmem-final.pdf}
}
@techreport{rr-lsv-12-25,
author = {Feld, Gilles and Fribourg, Laurent and Labrousse, Denis and
Revol, Bertrand and Soulat, Romain},
title = {Correct-by-Design Control of 5-level and 7-level Power Converters},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2012},
month = dec,
type = {Research Report},
number = {LSV-12-25},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-25.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-25.pdf},
versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2012-25-v1.pdf, 20121205},
note = {8~pages},
abstract = {High-power converters based on elementary switching cells are
more and more used in the industry of power electronics owing to various
advantages such as lower voltage stress and reduced power loss. However,
the complexity of controlling such converters is a major challenge that
the power manufacturing industry has to face with. The synthesis of
industrial switching controllers relies today on heuristic rules and
empiric simulation. The state of the system is not guaranteed to stay
within the limits that are admissible for its correct electrical behavior.
We show here how to apply a formal method in order to synthesise a
correct-by-design control that guarantees that the power converter will
always stay within a predened safe zone of variations for its input
parameters. Our method nds local invariants by decomposing the safety
space into smaller zones. The method is applied in order to synthesize
correct-by-design controls for a 5-level and 7-level power converters. We
check the validity of our approach by numerical simulations and physical
experimentations done with a prototype built by SATIE laboratory.}
}
@techreport{rr-lsv-12-24,
author = {Fribourg, Laurent and Soulat, Romain},
title = {Controlled Recurrent Subspaces for Sampled Switched Linear Systems},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2012},
month = dec,
type = {Research Report},
number = {LSV-12-24},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-24.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-24.pdf},
versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2012-24-v1.pdf, 20121205},
note = {11~pages},
abstract = {Sampled switched linear systems are governed by piecewise linear
dynamics that are periodically sampled with a given period~\(\tau\). At
each sampling time, the {"}mode{"} of the system, i.e., the parameters of
the linear dynamics, are switched according to a control rule. We give
here a procedure for showing that a given area~\(R\) of the state space
has a {"}\(k\)-recurrent decomposition: such a decomposition induces a
control that makes every trajectory starting from~\(R\) go back to~\(R\)
within at most \(k\) steps (i.e, \(k\tau\)\ time). We can then determine
an extended zone that contains all the trajectories issued from~\(R\);
this allows us to check safety properties of the system. We show the
practical interest of our approach on several examples of the literature.
We also give a geometrical condition on~\(R\) that ensures the existence
of a \(k\)-recurrent decomposition.}
}
@article{AFS-fmsd12,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Andr{\'e}, {\'E}tienne and Fribourg, Laurent and Sproston,
Jeremy},
title = {An~Extension of the Inverse Method to Probabilistic Timed
Automata},
year = 2013,
month = apr,
volume = 42,
number = 2,
pages = {119-145},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AFS-fmsd12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AFS-fmsd12.pdf},
doi = {10.1007/s10703-012-0169-x},
abstract = {Probabilistic timed automata can be used to model systems in
which probabilistic and timing behaviour coexist. Verification of
probabilistic timed automata models is generally performed with regard to
a single reference valuation pi0 of the timing parameters. Given such a
parameter valuation, we present a method for obtaining automatically a
constraint~\(K_0\) on timing parameters for which the reachability
probabilities (1)~remain invariant and (2)~are equal to the reachability
probabilities for the reference valuation. The method relies on parametric
analysis of a non-probabilistic version of the probabilistic timed
automata model using the {"}inverse method{"}. The method presents the
following advantages. First, since \(K_0\) corresponds to a dense domain
around pi0 on which the system behaves uniformly, it gives us a measure of
robustness of the system. Second, it allows us to obtain a valuation
satisfying \(K_0\) which is as small as possible while preserving
reachability probabilities, thus making the probabilistic analysis of the
system easier and faster in practice. We provide examples of the
application of our technique to models of randomized protocols, and
introduce an extension of the method allowing the generation of a
{"}probabilistic cartography{"} of a system.}
}
@techreport{rr-lsv-12-16,
author = {Feld, Gilles and Fribourg, Laurent and Labrousse, Denis and
Revol, Bertrand and Soulat, Romain},
title = {Numerical simulation and physical experimentation of a
5-level and 7-level power converter under a control
designed by a formal method},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2012},
month = jul,
type = {Research Report},
number = {LSV-12-16},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-16.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-16.pdf},
versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2012-16-v1.pdf, 20120727},
note = {18~pages},
abstract = {High-power converters based on elementary switching cells are
more and more used in the industry of power electronics owing to various
advantages such as lower voltage stress and reduced power loss. However,
the complexity of controlling such converters is a major challenge that
the power manufacturing industry has to face with. The synthesis of
industrial switching controllers relies today on heuristic rules and
empiric simulation. There is no formal guarantee of correctness in zones
around nominal values. In [3], we have applied a backward-oriented formal
method to guarantee the good behavior of the systems within predefined
zones of variations for the input parameters. Here, for numerical
stability reasons, we choose to use a forward-oriented method. We apply
this method to a 5-level and 7-level power converters. We check the
correctness of our approach by numerical simulations and physical
experimentations.}
}
@techreport{rr-lsv-12-14,
author = {Feld, Gilles and Fribourg, Laurent and Labrousse, Denis and
Lefebvre, St{\'e}phane and Revol, Bertrand
and Soulat, Romain},
title = {Control of Multilevel Power Converters using Formal Methods},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2012},
month = jun,
type = {Research Report},
number = {LSV-12-14},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-14.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2012-14.pdf},
versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2012-14-v1.pdf, 20120626},
note = {14~pages},
abstract = {High-power converters based on elementary switching cells are
more and more used in the industry of power electronics owing to various
advantages such as lower voltage stress and reduced power loss. However,
the complexity of controlling such converters is a major challenge that
the power manufacturing industry has to face with. The synthesis of
industrial switching controllers relies today on heuristic rules and
empiric simulation. There is no formal guarantee of correctness in zones
around nominal values. It is therefore interesting to apply formal methods
to guarantee the good behavior of the systems within predefined zones of
variations for the input parameters. As far as we know, such formal
methods have been applied only to small electronic power devices (like
DC-DC boost converters) containing one switching cell. We show in this
paper that one can apply formal methods to more complicated systems, such
as multi-level converters containing several pairs of switching cells.}
}
@inproceedings{FLMS-time12,
address = {Leicester, UK},
month = sep,
year = 2012,
publisher = {{IEEE} Computer Society Press},
editor = {Reynolds, Mark and Terenziani, Paolo and Moszkowski, Ben},
acronym = {{TIME}'12},
booktitle = {{P}roceedings of the 19th {I}nternational {S}ymposium on
{T}emporal {R}epresentation and {R}easoning
({TIME}'12)},
author = {Fribourg, Laurent and Lesens, David and Moro, Pierre and
Soulat, Romain},
title = {Robustness Analysis for Scheduling Problems using the Inverse
Method},
pages = {73-80},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FLMS-time12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FLMS-time12.pdf},
doi = {10.1109/TIME.2012.10},
abstract = {Given a Parametric Timed Automaton (PTA)~\(\mathcal{A}\) and a
tuple~\(\pi_{0}\) of reference valuations for timings, the \emph{Inverse
Method~(IM)} synthesizes a constraint around~\(\pi_{0}\) where
\(\mathcal{A}\) behaves in the same time-abstract manner. This provides us
with a quantitative measure of robustness of the behavior
of~\(\mathcal{A}\) around~\(\pi_{0}\). We~show in this paper how
\textit{IM} can be applied in a specific way to treat the robustness of
scheduling systems. We also explain how to use the method in order to
synthesize large zones of the timing parameter space where the system is
guaranteed to be schedulable. We illustrate the method on several examples
of the literature as well as a case study originating from an industrial
design project.}
}
@inproceedings{AFKS12,
address = {Paris, France},
month = aug,
year = 2012,
volume = {7436},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Giannakopoulou, Dimitra and M{\'e}ry, Dominique},
acronym = {{FM}'12},
booktitle = {{P}roceedings of the 18th {I}nternational {S}ymposium on {F}ormal
{M}ethods ({FM}'12)},
author = {Andr{\'e}, {\'E}tienne and Fribourg, Laurent and K{\"u}hne,
Ulrich and Soulat, Romain},
title = {{IMITATOR}~2.5: A~Tool for Analyzing Robustness in Scheduling
Problems},
pages = {33-36},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AFKS-fm12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AFKS-fm12.pdf},
doi = {10.1007/978-3-642-32759-9_6},
abstract = {The tool \textsc{Imitator} implements the \emph{Inverse
Method~(IM)} for Timed Automata~(TAs). Given a TA~\(\mathcal{A}\) and a
tuple~\(\pi_{0}\) of reference valuations for timings, \textit{IM}
synthesizes a constraint around~\(\pi_{0}\) where \(\mathcal{A}\) behaves
in the same discrete manner. This provides us with a quantitative measure
of robustness of the behavior of~\(\mathcal{A}\) around~\(\pi_{0}\). The
new version \textsc{Imitator}~2.5 integrates the new features of
stopwatches (in~addition to standard clocks) and updates (in addition to
standard clock resets), as well as powerful algorithmic improvements for
state space reduction. These new features make the tool well-suited to
analyze the robustness of solutions in several classes of preemptive
scheduling problems.}
}
@inproceedings{AFS-nfm12,
address = {Norfolk, Virginia, USA},
month = apr,
year = 2012,
volume = 7226,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Goodloe, Alwyn and Person, Suzette},
acronym = {{NFM}'12},
booktitle = {{P}roceedings of the 4th {NASA} {F}ormal {M}ethods {S}ymposium ({NFM}'12)},
author = {Andr{\'e}, {\'E}tienne and Fribourg, Laurent and Soulat,
Romain},
title = {Enhancing the Inverse Method with State Merging},
pages = {100-105},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AFS-nfm12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AFS-nfm12.pdf},
doi = {10.1007/978-3-642-28891-3_10},
abstract = {Keeping the state space small is essential when verifying
real-time systems using Timed Automata~(TA). In~the model-checker Uppaal,
the merging operation has been used extensively in order to reduce the
number of states. Actually, Uppaal's merging technique applies within the
more general setting of Parametric Timed Automata (PTA). The \emph{Inverse
Method~(IM)} for a PTA~\(\mathcal{A}\) is a procedure that synthesizes a
zone around a given point~\(\pi^{0}\) (parameter valuation) over which
\(\mathcal{A}\) is guaranteed to behave similarly. We show that the
integration of merging into~\emph{IM} leads to the synthesis of larger
zones around~\(\pi^{0}\). It~also often improves the performance
of~\emph{IM}, both in terms of computational space and time, as shown by
our experimental results.}
}
@misc{minimator,
author = {Fribourg, Laurent and K{\"u}hne, Ulrich and Soulat, Romain},
title = {Minimator: a~tool for controller synthesis and computation of
minimal invariant sets for linear switched systems},
year = 2013,
month = mar,
number = {v1.0},
url = {https://bitbucket.org/ukuehne/minimator/wiki/Home},
abstract = {Minimator is a tool for analyzing switched systems, a class of
hybrid systems recently used with success in various domains
such as automotive systems and power electronics. The tool
produces a state-dependent control strategy which makes the
trajectories of the analyzed system converge to limit
cycles. The method relies on a technique of decomposition of
the state space into local regions where the control is
uniform. The tool has been succesfully applied to several
examples of the literature and power electronics.}
}
@misc{imitator,
author = {Andr{\'e}, {\'E}tienne and Fribourg, Laurent and K{\"u}hne,
Ulrich and Soulat, Romain},
title = {Imitator: a~tool for efficient synthesis of parameters for timed automata},
year = {2013},
month = feb,
number = {v2.6.0},
url = {http://www.lsv.ens-cachan.fr/Software/imitator/},
abstract = {Imitator (standing for Inverse Method for Inferring Time
AbstracT behaviOR) is an implementation of algorithm \texttt{InverseMethod},
described in [Andr{\'e} \textit{et~al.}, IJFCS 20(5):819-836, 2009].
It~allows to generalize a concrete behavior of a Parametric Timed
Automata, by synthesizing a constraint on the parameters.}
}
@book{FS-book13,
author = {Fribourg, Laurent and Soulat, Romain},
title = {Control of Switching Systems by Invariance Analysis: Application to Power Electronics},
publisher = {Wiley-ISTE},
year = 2013,
month = jul,
isbn = {9781848216068},
note = {144~pages},
url = {http://www.iste.co.uk/index.php?f=a&ACTION=View&id=684},
abstract = {This book presents correct-by-design control techniques for
switching systems, using different methods of stability analysis.
Switching systems are increasingly used in the electronics and mechanical
industries; in power electronics and the automotive industry, for example.
This is due to their flexibility and simplicity in accurately controlling
industrial mechanisms. By adopting appropriate control rules, we can steer
a switching system to a region centered at a desired equilibrium point,
while avoiding {"}unsafe{"} regions of parameter saturation.\par
The authors explain various correct-by-design methods for control
synthesis, using different methods of stability and invariance analysis.
They also provide several applications of these methods to industrial
examples of power electronics.}
}
@inproceedings{SSLAF-ftscs13,
address = {Queenstown, New Zealand},
month = oct,
year = 2013,
editor = {Artho, Cyrille and {\"O}lveczky, Peter Csaba},
acronym = {{FTSCS}'13},
booktitle = {{P}reproceedings of the 2nd {I}nternational {W}orkshop on
{F}ormal {T}echniques for {S}afety-{C}ritical {S}ystems ({FTSCS}'13)},
author = {Sun, Youcheng and Soulat, Romain and Lipari, Giuseppe and
Andr{\'e}, {\'E}tienne and Fribourg, Laurent},
title = {Parametric Schedulability Analysis of Fixed Priority Real-Time
Distributed Systems},
pages = {179-194},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SSLAF-ftscs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SSLAF-ftscs13.pdf},
abstract = {In this paper, we address the problem of parametric
schedulability analysis of distributed real-time systems scheduled by
fixed priority. We propose two different approaches to parametric
analysis. The first one is a novel analytic technique that extends
single-processor sensitivity analysis to the case of distributed systems.
The second approach is based on model checking of Parametric Stopwatch
Automata~(PSA): we~generate a PSA model from a high-level description of
the system, and then we apply the Inverse Method to obtain all possible
behaviours of the system. Both techniques have been implemented in two
software tools, and they have been compared with classical holistic
analysis on two meaningful test cases. The results show that the analytic
method provides results similar to classical holistic analysis in a very
efficient way, whereas the PSA approach is slower but covers the entire
space of solutions.}
}
@inproceedings{FS-rp13,
address = {Uppsala, Sweden},
month = sep,
year = 2013,
volume = {8169},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abdulla, Parosh Aziz and Potapov, Igor},
acronym = {{RP}'13},
booktitle = {{P}roceedings of the 7th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'13)},
author = {Fribourg, Laurent and Soulat, Romain},
title = {Stability Controllers for Sampled Switched Systems},
pages = {135-145},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FS-rp13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FS-rp13.pdf},
doi = {10.1007/978-3-642-41036-9_13},
abstract = {We consider in this paper switched systems, a class of hybrid
systems recently used with success in various domains such as automotive
industry and power electonics. We propose a state-dependent control
strategy which makes the trajectories of the analyzed system converge to
finite cyclic sequences of points. Our method relies on a technique of
decomposition of the state space into local regions where the control is
uniform. We have implemented the procedure using zonotopes, and applied it
successfully to several examples of the literature.}
}
@inproceedings{Fribourg-fsfma13,
address = {Singapore},
month = jul,
year = 2013,
volume = 31,
series = {Open Access Series in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Choppy, {\relax Ch}ristine and Sun, Jun},
acronym = {{FSFMA}'13},
booktitle = {{P}roceedings of the 1st {F}rench-{S}ingaporean {W}orkshop
on {F}ormal {M}ethods and {A}pplications ({FSFMA}'13)},
author = {Fribourg, Laurent},
title = {Control of Switching Systems by Invariance Analysis (Invited~Talk)},
pages = {1},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/F-fsfma13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/F-fsfma13.pdf},
doi = {10.4230/OASIcs.FSFMA.2013.1},
abstract = {Switched systems are embedded devices widespread in industrial
applications such as power electronics and automotive
control. They consist of continuous-time dynamical
subsystems and a rule that controls the switching between
them. Under a suitable control rule, the system can improve
its steady-state performance and meet essential properties
such as safety and stability in desirable operating zones.
We explain that such controller synthesis problems are
related to the construction of appropriate invariants of the
state space, which approximate the limit sets of the system
trajectories. We present a new approach of invariant
construction based on a technique of state space
decomposition interleaved with forward fixed point
computation. The method is illustrated in a case study taken
from the field of power electronics.}
}
@inproceedings{FKS-fsfma13,
address = {Singapore},
month = jul,
year = 2013,
volume = 31,
series = {Open Access Series in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Choppy, {\relax Ch}ristine and Sun, Jun},
acronym = {{FSFMA}'13},
booktitle = {{P}roceedings of the 1st {F}rench-{S}ingaporean {W}orkshop
on {F}ormal {M}ethods and {A}pplications ({FSFMA}'13)},
author = {Fribourg, Laurent and K{\"u}hne, Ulrich and Soulat, Romain},
title = {Constructing Attractors of Nonlinear Dynamical Systems by
State Space Decomposition},
pages = {53-60},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FKS-fsfma13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FKS-fsfma13.pdf},
doi = {10.4230/OASIcs.FSFMA.2013.53},
abstract = {In a previous work, we have shown how to generate attractor sets
of affine hybrid systems using a method of state space decomposition. We
show here how to adapt the method to polynomial dynamics systems by
approximating them as switched affine systems. We show the practical
interest of the method on standard examples of the literature.}
}
@inproceedings{SHLRFLF-epe13,
address = {Lille, France},
month = sep,
year = 2013,
publisher = {{IEEE} Power Electronics Society},
editor = {Lataire, {\relax Ph}ilippe},
booktitle = {{P}roceedings of the 15th {E}uropean {C}onference
on {P}ower {E}lectronics and {A}pplications ({EPE}'13)},
author = {Soulat, Romain and H{\'e}rault, Guillaume and Labrousse,
Denis and Revol, Bertrand and Feld, Gilles and Lefebvre,
St{\'e}phane and Fribourg, Laurent},
title = {Use of a full wave correct-by-design command to control a
multilevel modular converter},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SHLRFLF-epe13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SHLRFLF-epe13.pdf},
doi = {10.1109/EPE.2013.6634448},
abstract = {This paper proposes a method to synthesize a full wave control
applied to a multilevel modular converter~(MMC). This method guarantees
the output waveform and the balancing of the capacitors. Numerical
simulations and experiments are used to check the validity of the
approach.}
}
@inproceedings{AFS-atva13,
address = {Hanoi, Vietnam},
month = oct,
year = {2013},
volume = {8172},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Dang{-}Van, Hung and Ogawa, Mizuhito},
acronym = {{ATVA}'13},
booktitle = {{P}roceedings of the 11th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'13)},
author = {Andr{\'e}, {\'E}tienne and Fribourg, Laurent and Soulat, Romain},
title = {Merge and Conquer: State Merging in Parametric Timed Automata},
pages = {381-396},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AFS-atva13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AFS-atva13.pdf},
doi = {10.1007/978-3-319-02444-8_27},
abstract = {Parameter synthesis for real-time systems aims at synthesizing
dense sets of valuations for the timing requirements, guaranteeing a good
behavior. A popular formalism for modeling parameterized realtime systems
is parametric timed automata (PTAs). Compacting the state space of PTAs as
much as possible is fundamental. We present here a state merging reduction
based on convex union, that reduces the state space, but yields an
over-approximation of the executable paths. However, we show that it
preserves the sets of reachable locations and executable actions. We also
show that our merging technique associated with the inverse method, an
algorithm for parameter synthesis, preserves locations as well, and
outputs larger sets of parameter valuations.}
}
@inproceedings{FS-ncmip13,
address = {Cachan, France},
month = may,
year = 2013,
number = {012007},
volume = 464,
series = {Journal of Physics: Conference Series},
publisher = {{IOS} Press},
editor = {Blanc{-}F{\'e}raud, Laure and Joubert, Pierre-Yves},
acronym = {{NCMIP}'13},
booktitle = {{P}roceedings of the 3rd {I}nternational {W}orkshop on {N}ew
{C}omputational {M}ethods for {I}nverse {P}roblems ({NCMIP}'13)},
author = {Fribourg, Laurent and Soulat, Romain},
title = {Limit Cycles of Controlled Switched Systems: Existence,
Stability, Sensitivity},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FS-ncmip13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FS-ncmip13.pdf},
doi = {10.1088/1742-6596/464/1/012007},
abstract = {We present a control method which makes the trajectories
of a switched system converge to a stable limit cycle lying in a
desired region of equilibrium. The method is illustrated on the
boost DC-DC converter example. We also point out in this example
the sensitivity of limit cycles to parameter variations by showing
how the limit cycle evolves in presence of small perturbations of
some system parameters. This suggests that limit cycles are good
candidates for reliable estimations of the physical parameters of
switched systems, using an appropriate inverse approach.}
}
@article{FK-ijfcs13,
publisher = {World Scientific},
journal = {International Journal of Foundations of Computer Science},
author = {Fribourg, Laurent and K{\"u}hne, Ulrich},
title = {Parametric Verification and Test Coverage for Hybrid Automata
using the Inverse Method},
year = 2013,
month = feb,
volume = 24,
number = 2,
pages = {233-249},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FK-ijfcs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FK-ijfcs13.pdf},
doi = {10.1142/S0129054113400091},
abstract = {Hybrid systems combine continuous and discrete behavior. Hybrid
Automata are a powerful formalism for the modeling and verification of
such systems. A~common problem in hybrid system verification is the good
parameters problem, which consists in identifying a set of parameter
valuations which guarantee a certain behavior of a system. Recently, a
method has been presented for attacking this problem for Timed Automata.
In this paper, we show the extension of this methodology for hybrid
automata with linear and affine dynamics. The method is demonstrated with
a hybrid system benchmark from the literature.}
}
@misc{LF-turing12,
author = {Fribourg, Laurent},
title = {En quoi {T}uring a-t-il chang{\'e} ma vie~?},
year = 2012,
month = apr,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LF-turing12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LF-turing12.pdf}
}
@inproceedings{BLLJKFSFR-revet12,
address = {Hammamet, Tunisia},
month = mar,
year = 2012,
publisher = {{IEEE} Power~\& Energy Society},
editor = {Neji, Rafik},
acronym = {{REVET}'12},
booktitle = {{P}roceedings of the 1st {I}nternational {C}onference on
{R}enewable {E}nergies and {VE}hicular {T}echnology
({REVET}'12)},
author = {Belkacem, Ghania and Labrousse, Denis and Lefebvre, St{\'e}phane and
Joubert, Pierre-Yves and K{\"u}hne, Ulrich and Fribourg,
Laurent and Soulat, Romain and Florentin, {\'E}ric and Rey,
{\relax Ch}ristian},
title = {Distributed and Coupled Electrothermal Model of Power
Semiconductor Devices},
pages = {84-89},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BLLJKFSFR-revet12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BLLJKFSFR-revet12.pdf},
doi = {10.1109/REVET.2012.6195253},
abstract = {Electro-thermal model of power semiconductor devices are of key
importance in order to optimize their thermal design and increase their
reliability. The development of such an electro-thermal model for power
MOSFET transistors (COOLMOS\textsuperscript{(TM)}) based on the coupling
between two computation softwares (Matlab and Cast3M) is described in the
paper. The elaborated 2D electro-thermal model is able to predict
i)~the~temperature distribution on chip surface well as in volume,
ii)~the~effect of the temperature on the distribution of the current
flowing within the die and iii)~the~effects of the ageing of the
metallization layer on the current density and the temperature. In the
paper, the used electrical and thermal models are described as well as the
implemented coupling scheme.}
}
@inproceedings{FFLRS-fsfma14,
address = {Singapore},
month = may,
year = 2014,
volume = 156,
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Lin, Shang{-}Wei and Petrucci, Laure},
acronym = {{FSFMA}'14},
booktitle = {{P}roceedings of the 2nd {F}rench-{S}ingaporean {W}orkshop
on {F}ormal {M}ethods and {A}pplications ({FSFMA}'14)},
author = {Feld, Gilles and Fribourg, Laurent and Labrousse, Denis and
Revol, Bertrand and Soulat, Romain},
title = {Correct-by-design Control Synthesis for Multilevel
Converters using State Space Decomposition},
pages = {5-16},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FFLRS-fsfma14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FFLRS-fsfma14.pdf},
doi = {10.4204/EPTCS.156.5},
abstract = {High-power converters based on elementary switching cells are
more and more used in the industry of power electronics owing to various
advantages such as lower voltage stress and reduced power loss. However,
the complexity of controlling such converters is a major challenge that
the power manufacturing industry has to face with. The synthesis of
industrial switching controllers relies today on heuristic rules and
empiric simulation. The state of the system is not guaranteed to stay
within the limits that are admissible for its correct electrical behavior.
We show here how to apply a formal method in order to synthesize a
correct-by-design control that guarantees that the power converter will
always stay within a predefined safe zone of variations for its input
parameters. The method is applied in order to synthesize a
correct-by-design control for 5-level and 7-level power converters with a
flying capacitor topology. We check the validity of our approach by
numerical simulations for 5 and 7 levels. We also perform physical
experimentations using a prototype built by SATIE laboratory for 5
levels}
}
@article{FKS-fmsd14,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Fribourg, Laurent and K{\"u}hne, Ulrich and Soulat, Romain},
title = {Finite Controlled Invariants for Sampled Switched Systems},
year = 2014,
month = dec,
volume = 45,
number = 3,
pages = {303-329},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FKS-fmsd14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FKS-fmsd14.pdf},
doi = {10.1007/s10703-014-0211-2},
abstract = {We consider in this paper switched systems, a class of hybrid
systems recently used with success in various domains such as automotive
industry and power electronics. We propose a state-dependent control
strategy which makes the trajectories of the analyzed system converge to
finite cyclic sequences of points. Our method relies on a technique of
decomposition of the state space into local regions where the control is
uniform. We have implemented the procedure using zonotopes, and applied it
successfully to several examples of the literature and industrial case
studies in power electronics.}
}
@inproceedings{SLAF-syncop14,
address = {Grenoble, France},
volume = 145,
series = {Electronic Proceedings in Theoretical Computer Science},
month = apr,
year = 2014,
editor = {Andr{\'e}, {\'E}tienne and Frehse, Goran},
acronym = {{SYNCOP}'14},
booktitle = {{P}roceedings of the 1st {I}nternational {W}orkshop on {S}ynthesis
of {C}ontinuous {P}arameters ({SYNCOP}'14)},
author = {Sun, Youcheng and Lipari, Giuseppe and
Andr{\'e}, {\'E}tienne and Fribourg, Laurent},
title = {Toward Parametric Timed Interfaces for Real-Time Components},
pages = {49-64},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SLAF-syncop14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SLAF-syncop14.pdf},
doi = {10.4204/EPTCS.145.6},
abstract = {We propose here a framework to model real-time components
consisting of concurrent real-time tasks running on a single processor,
using parametric timed automata. Our framework is generic and modular, so
as to be easily adapted to different schedulers and more complex task
models. We first perform a parametric schedulability analysis of the
components using the inverse method. We show that the method unfortunately
does not provide satisfactory results when the task periods are considered
as parameters. After identifying and explaining the problem, we present a
solution adapting the model by making use of the worst-case scenario in
schedulability analysis. We show that the analysis with the inverse method
always converges on the modified model when the system load is strictly
less than~\(100\%\). Finally, we show how to use our parametric analysis for
the generation of timed interfaces in compositional system design.}
}
@inproceedings{SLSFM-rtcsa14,
address = {Chongqing, China},
month = aug,
year = 2014,
publisher = {{IEEE} Computer Society Press},
acronym = {{RTCSA}'14},
booktitle = {{P}roceedings of the 20th {IEEE} {I}nternational {C}onference on {E}mbedded
and {R}eal-{T}ime {C}omputing {S}ystems and {A}pplications
({RTCSA}'14)},
author = {Sun, Youcheng and Lipari, Giuseppe and
Soulat, Romain and Fribourg, Laurent and
Markey, Nicolas},
title = {Component-Based Analysis of Hierarchical Scheduling using Linear Hybrid Automata},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SLSFM-rtcsa14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SLSFM-rtcsa14.pdf},
doi = {10.1109/RTCSA.2014.6910502},
abstract = {Formal methods (e.g. Timed Automata or Linear Hybrid Automata)
can be used to analyse a real-time system by performing a reachability
analysis on the model. The advantage of using formal methods is that they
are more expressive than classical analytic models used in schedulability
analysis. For example, it is possible to express state-dependent
behaviour, arbitrary activation patterns,~etc.\par
In this paper we use the formalism of Linear Hybrid Automata to encode a
hierarchical scheduling system. In particular, we model a dynamic server
algorithm and the tasks contained within, abstracting away the rest of the
system, thus enabling component-based scheduling analysis. We prove the
correctness of the model and the decidability of the reachability analysis
for the case of periodic tasks. Then, we compare the results of our model
against classical schedulability analysis techniques, showing that our
analysis performs better than analytic methods in terms of resource
utilisation. We further present two case studies: a~component with
state-dependent tasks, and a simplified model of a real avionics system.
Finally, through extensive tests with various configurations, we
demonstrate that this approach is usable for medium size components.}
}
@techreport{rr-lsv-14-03,
author = {Fribourg, Laurent and Goubault, {\'E}ric and Mohamed, Sameh
and Putot, Sylvie and Soulat, Romain},
title = {Synthesis of robust boundary control for systems
governed by semi-discrete differential equations},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2014},
month = feb,
type = {Research Report},
number = {LSV-14-03},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2014-03.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2014-03.pdf},
versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2014-03-v1.pdf, 20140228},
note = {8~pages},
abstract = {The topic of boundary control of PDEs has been the subject of a
considerable literature since the seminal works of J.-L. Lions in the 90s.
In this paper, we consider the boundary control of systems represented by
spatial discretizations of~PDEs (i.e.,~semi-discrete equations). We~focus
on control laws which are sampled and piecewise constant: periodically, at
every sampling time, a fixed control amplitude is applied to the system
until the next sampling instant. We show that, under some conditions,
sampled piecewise-constant boundary control allows to achieve
{"}approximate controllability{"}: Given a time \(T>0\), the controlled system
evolves to a neighborhood of a given final state. The result is
illustrated on the boundary control of the semi-discrete version of the
heat equation.}
}
@inproceedings{FGMMP-rp15,
address = {Warsaw, Poland},
month = sep,
year = 2015,
volume = {9328},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Boja{\'n}czyk, Miko{\l}aj and Lasota, S{\l}awomir and Potapov, Igor},
acronym = {{RP}'15},
booktitle = {{P}roceedings of the 9th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'15)},
author = {Fribourg, Laurent and Goubault, {\'E}ric and Mohamed, Sameh
and Mrozek, Marian and Putot, Sylvie},
title = {A~Topological Method for Finding Invariants of
Continuous Systems},
pages = {63-75},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FGMMP-rp15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FGMMP-rp15.pdf},
doi = {10.1007/978-3-319-24537-9_7},
abstract = {A~usual way to find positive invariant sets of ordinary
differential equations is to restrict the search to predefined finitely
generated shapes, such as linear templates, or ellipsoids as in classical
quadratic Lyapunov function based approaches. One then looks for
generators or parameters for which the corresponding shape has the
property that the flow of the ODE goes inwards on its border. But for
non-linear systems, where the structure of invariant sets may be very
complicated, such simple predefined shapes are generally not well suited.
The present work proposes a more general approach based on a topological
property, namely Wa\.{z}ewski's property. Even for complicated non-linear
dynamics, it is possible to successfully restrict the search for isolating
blocks of simple shapes, that are bound to contain non-empty invariant
sets. This approach generalizes the Lyapunov-like approaches, by allowing
for inwards and outwards flow on the boundary of these shapes, with extra
topological conditions. We developed and implemented an algorithm based on
Wa\.{z}ewski's property, SOS optimization and some extra combinatorial and
algebraic properties, that shows very nice results on a number of
classical polynomial dynamical systems.}
}
@inproceedings{FKM-syncop15,
address = {London, UK},
volume = 44,
series = {Open Access Series in Informatics},
month = apr,
year = 2015,
editor = {Andr{\'e}, {\'E}tienne and Frehse, Goran},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
acronym = {{SYNCOP}'15},
booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop on {S}ynthesis
of {C}ontinuous {P}arameters ({SYNCOP}'15)},
author = {Fribourg, Laurent and K{\"u}hne, Ulrich and Markey, Nicolas},
title = {Game-based Synthesis of Distributed Controllers for Sampled Switched Systems},
pages = {47-61},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FKM-syncop15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FKM-syncop15.pdf},
doi = {10.4230/OASIcs.SynCoP.2015.47},
abstract = {Switched systems are a convenient formalism for modeling
physical processes interacting with a digital controller. Unfortunately,
the formalism does not capture the distributed nature encountered e.g. in
cyber-physical systems, which are organized as networks of elements
interacting with each other and with local controllers. Most current
methods for control synthesis can only produce a centralized controller,
which is assumed to have complete knowledge of all the component states
and can interact with all of them. In~this paper, we~consider a controller
synthesis method based on state space decomposition, and propose a
game-based approach in order to extend it within a distributed framework.}
}
@inproceedings{LDRCF-syncop15,
address = {London, UK},
volume = 44,
series = {Open Access Series in Informatics},
month = apr,
year = 2015,
editor = {Andr{\'e}, {\'E}tienne and Frehse, Goran},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
acronym = {{SYNCOP}'15},
booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop on {S}ynthesis
of {C}ontinuous {P}arameters ({SYNCOP}'15)},
author = {Le{~}Co{\"e}nt, Adrien and De{~}Vuyst, Florian and Rey,
{\relax Ch}ristian and Chamoin, Ludovic and Fribourg, Laurent},
title = {Guaranteed control of switched control systems
using model order reduction and state-space bisection},
pages = {32-46},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LDCRF-syncop15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LDCRF-syncop15.pdf},
doi = {10.4230/OASIcs.SynCoP.2015.32},
abstract = {This paper considers discrete-time linear systems controlled by
a quantized law, i.e., a piecewise constant time function taking a finite
set of values. We show how to generate the control by, first, applying
model reduction to the original system, then using a {"}state-space
bisection{"} method for synthesizing a control at the reduced-order
level, and finally computing an upper bound to the deviations between the
controlled output trajectories of the reduced-order model and those of the
original model. The effectiveness of our approach is illustrated on
several examples of the literature.}
}
@article{AFG-sif15,
publisher = {SIF},
journal = {1024~-- Bulletin de la soci{\'e}t{\'e} informatique de France},
author = {Abiteboul, Serge and Fribourg, Laurent and
Goubault{-}Larrecq, Jean},
title = {{G}{\'e}rard {B}erry~: un~informaticien m{\'e}daille d'or du {CNRS}~2014},
volume = 4,
pages = {139-142},
month = oct,
year = 2014,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AFG-sif15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AFG-sif15.pdf},
abstract = {C'est un chercheur en informatique qui vient de recevoir la
m{\'e}daille d'or du CNRS, la plus haute distinction scientifique fran{\c
c}aise toutes disciplines confondues. Les informaticiens sont rares {\`a}
avoir {\'e}t{\'e} ainsi honor{\'e}s : ce n'est que la seconde fois
apr{\`e}s Jacques Stern en~2006.}
}
@inproceedings{LFS-rp16,
address = {Aalborg, Denmark},
month = sep,
year = 2016,
volume = {9899},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Larsen, Kim G. and Srba, Ji{\v{r}}{\'\i}},
acronym = {{RP}'16},
booktitle = {{P}roceedings of the 10th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'16)},
author = {Le{~}Co{\"e}nt, Adrien and Fribourg, Laurent and
Soulat, Romain},
title = {Compositional analysis of Boolean networks using local fixed-point
iterations},
pages = {134-147},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LFS-rp16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LFS-rp16.pdf},
doi = {10.1007/978-3-319-45994-3_10},
abstract = {We present a compositional method which allows to
over-approximate the set of attractors and under-approximate the set
of basins of attraction of a Boolean network~(BN). This merely
consists in replacing a global fixed-point computation by a
composition of local fixed-point computations. Once these
approximations have been computed, it~becomes much more tractable to
generate the exact sets of attractors and basins of attraction. We
illustrate the interest of our approach on several examples, among
which is a BN modeling a railway interlocking system with 50 nodes
and millions of attractors.}
}
@inproceedings{LFMDC-rp16,
address = {Aalborg, Denmark},
month = sep,
year = 2016,
volume = {9899},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Larsen, Kim G. and Srba, Ji{\v{r}}{\'\i}},
acronym = {{RP}'16},
booktitle = {{P}roceedings of the 10th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'16)},
author = {Le{~}Co{\"e}nt, Adrien and Fribourg, Laurent and
Markey, Nicolas and De{~}Vuyst, Florian and Chamoin, Ludovic},
title = {Distributed Synthesis of State-Dependent Switching Control},
pages = {119-133},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LFMDC-rp16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LFMDC-rp16.pdf},
doi = {10.1007/978-3-319-45994-3_9},
abstract = {We present a correct-by-design method of state-dependent
control synthesis for linear discrete-time switching systems. Given
an objective region~\(R\) of the state space, the method builds a
capture set~\(S\) and a control which steers any element of~\(S\)
into~\(R\). The method works by iterated backward reachability
from~\(R\). More precisely, \(S\)~is given as a parametric extension
of~\(R\), and the maximum value of the parameter is solved by linear
programming. The method can also be used to synthesize a stability
control which maintains indefinitely within~\(R\) all the states
starting at~\(R\). We~explain how the synthesis method can be
performed in a distributed manner. The method has been implemented
and successfully applied to the synthesis of a distributed control
of a concrete floor heating system with 11 rooms and \(2^11 = 2048\)
switching modes.}
}
@article{LDRCF-ijdc16,
publisher = {Springer},
journal = {International Journal of Dynamics and Control},
author = {Le{~}Co{\"e}nt, Adrien and De{~}Vuyst, Florian and Rey,
Christian and Chamoin, Ludovic and Fribourg, Laurent},
title = {Control of mechanical systems using set-based methods},
pages = {1-17},
year = 2016,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LDRCF-ijdc16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LDRCF-ijdc16.pdf},
doi = {10.1007/s40435-016-0245-y},
abstract = {This paper considers large discrete-time linear systems obtained
from discretized partial differential equations, and controlled by a
\emph{quantized} law, i.e., a piecewise constant time function taking a
finite set of values. We show how to generate the control by, first,
applying \emph{model reduction} to the original system, then using a
{"}state-space bisection{"} method for synthesizing a control at the
reduced-order level, and finally computing an upper bound on the
deviations between the controlled output trajectories of the reduced-order
model and those of the original model. The effectiveness of our approach
is illustrated on several examples of the literature.}
}
@inproceedings{LACF-snr16,
address = {Vienna, Austria},
month = apr,
year = 2016,
publisher = {{IEEE} Computer Society Press},
acronym = {{SNR}'16},
booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop
on {S}ymbolic and {N}umerical {M}ethods for
{R}eachability {A}nalysis ({SNR}'16)},
author = {Le{~}Co{\"e}nt, Adrien and Alexandre{ }dit{ }Sandretto,
Julien and Chapoutot, Alexandre and Fribourg,
Laurent},
title = {Control of Nonlinear Switched Systems Based on
Validated Simulation},
pages = {1-6},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LACF-snr16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LACF-snr16.pdf},
abstract = {We present an algorithm of control synthesis for nonlinear
switched systems, based on an existing procedure of state-space
bisection and made available for nonlinear systems with the help of
validated simulation. The use of validated simulation also permits
to take bounded perturbations and varying parameters into account.
The whole approach is entirely guaranteed and the induced
controllers are correct-by-design.}
}
@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{FGMP-hscc16,
address = {Vienna, Austria},
month = apr,
year = 2016,
publisher = {ACM Press},
editor = {Abate, Alessandro and Fainekos, Georgios},
acronym = {{HSCC}'16},
booktitle = {{P}roceedings of the 19th {ACM} {I}nternational {C}onference
on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
({HSCC}'16)},
author = {Fribourg, Laurent and Goubault, {\'E}ric and Mohamed, Sameh
and Putot, Sylvie},
title = {A~Topological Method for Finding Invariant Sets of Switched Systems},
pages = {61-70},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FGMP-hscc16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FGMP-hscc16.pdf},
doi = {10.1145/2883817.2883822},
abstract = {We~revisit the problem of finding controlled invariants sets
(viability), for a class of differential inclusions, using topological
methods based on Wazewski property. In~many ways, this generalizes the
Viability Theorem approach, which is itself a generalization of the
Lyapunov function approach for systems described by ordinary differential
equations. We give a computable criterion based on SoS methods for a class
of differential inclusions to have a non-empty viability kernel within
some given region. We use this method to prove the existence of
(controlled) invariant sets of switched systems inside a region described
by a polynomial template, both with time-dependent switching and with
state-based switching through a finite set of hypersurfaces. A~Matlab
implementation allows us to demonstrate its use.}
}
@inproceedings{LDCF-snr17,
address = {Uppsala, Sweden},
month = apr,
year = 2017,
volume = 247,
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Erika {\'{A}}brah{\'{a}}m and Sergiy Bogomolov},
acronym = {{SNR}'17},
booktitle = {{P}roceedings of the 3rd {I}nternational {W}orkshop
on {S}ymbolic and {N}umerical {M}ethods for
{R}eachability {A}nalysis ({SNR}'17)},
author = {Adrien Le{ }Co{\"e}nt and
Florian De{ }Vuyst and
Ludovic Chamoin and
Laurent Fribourg},
title = {Control Synthesis of Nonlinear Sampled Switched Systems using Euler's Method},
pages = {18-33},
url = {https://arxiv.org/abs/1704.03102v1},
pdf = {https://arxiv.org/pdf/1704.03102v1.pdf},
doi = {10.4204/EPTCS.247.2},
abstract = {In this paper, we propose a symbolic control synthesis method for nonlinear sampled switched systems whose vector fields are one-sided Lipschitz. The main idea is to use an approximate model obtained from the forward Euler method to build a guaranteed control. The benefit of this method is that the error introduced by symbolic modeling is bounded by choosing suitable time and space discretizations. The method is implemented in the interpreted language Octave. Several examples of the literature are performed and the results are compared with results obtained with a previous method based on the Runge-Kutta integration method.}
}
@inproceedings{F-formats17,
address = {Berlin, Germany},
month = sep,
year = 2017,
volume = {10419},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abate, Alessandro and Geeraerts, Gilles},
acronym = {{FORMATS}'17},
booktitle = {{P}roceedings of the 15th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'17)},
author = {Fribourg, Laurent},
title = {Euler's Method Applied to the Control of Switched Systems},
pages = {3-21},
url = {https://doi.org/10.1007/978-3-319-65765-3_1},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/F-formats17.pdf},
doi = {10.1007/978-3-319-65765-3_1},
abstract = {Hybrid systems are a powerful formalism for modeling and reasoning about cyber-physical systems. They mix the continuous and discrete natures of the evolution of computerized systems. Switched systems are a special kind of hybrid systems, with restricted discrete behaviours: those systems only have finitely many different modes of (continuous) evolution, with isolated switches between modes. Such systems provide a good balance between expressiveness and controllability, and are thus in widespread use in large branches of industry such as power electronics and automotive control. The control law for a switched system defines the way of selecting the modes during the run of the system. Controllability is the problem of (automatically) synthesizing a control law in order to satisfy a desired property, such as safety (maintaining the variables within a given zone) or stabilisation (confinement of the variables in a close neighborhood around an objective point). In order to compute the control of a switched system, we need to compute the solutions of the differential equations governing the modes. Euler's method is the most basic technique for approximating such solutions. We present here an estimation of the Euler's method local error, using the notion of ''one-sided Lispchitz constant'' for modes. This yields a general control synthesis approach which can encompass several features such as bounded disturbance and compositionality.}
}
@inproceedings{LACFDC-rp17,
address = {London, UK},
month = sep,
year = 2017,
volume = {10506},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Matthew Hague and Igor Potapov},
acronym = {{RP}'17},
booktitle = {{P}roceedings of the 11th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'17)},
author = {Adrien Le{ }Co{\"{e}}nt and
Julien {Alexandre dit Sandretto} and
Alexandre Chapoutot and
Laurent Fribourg and
Florian De{ }Vuyst and
Ludovic Chamoin},
title = {Distributed Control Synthesis Using Euler's Method},
pages = {118-131},
url = {https://link.springer.com/chapter/10.1007/978-3-319-67089-8_9},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LACFDC-rp17.pdf},
doi = {10.1007/978-3-319-67089-8_9},
abstract = {In a previous work, we explained how Euler's method for computing approximate solutions of systems of ordinary differential equations can be used to synthesize safety controllers for sampled switched systems. We continue here this line of research by showing how Euler's method can also be used for synthesizing safety controllers in a distributed manner. The global system is seen as an interconnection of two (or more) sub-systems where, for each component, the sub-state corresponding to the other component is seen as an ?input?; the method exploits (a variant of) the notions of incremental input-to-state stability (\(\delta\)-ISS) and ISS Lyapunov function. We illustrate this distributed control synthesis method on a building ventilation example.}
}
@inproceedings{AFMS-vmcai2019,
address = {Cascais/Lisbon, Portugal},
month = jan,
year = 2019,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Enea, Constantin and Piskac, Ruzica},
acronym = {{VMCAI}'19},
booktitle = {{P}roceedings of the 20th {I}nternational {C}onference on
{V}erification, {M}odel {C}hecking and {A}bstract {I}nterpretation
({VMCAI}'19)},
author = {Andr{\'e}, {\'E}tienne and Fribourg, Laurent and Mota, Jean-Marc and Soulat, Romain},
title = {Verification of an industrial asynchronous leader election algorithm using abstractions and parametric model checking},
pages = {409-424},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AFMS-vmcai19.pdf},
abstract = {The election of a leader in a network is a challenging task, especially when the processes are asynchronous, i.e., execute an algorithm with time-varying periods. Thales developed an industrial election algorithm with an arbitrary number of processes, that can possibly fail. In this work, we prove the correctness of a variant of this industrial algorithm. We use a method combining abstraction, the SafeProver solver, and a parametric timed model-checker. This allows us to prove the correctness of the algorithm for a large number \(p\) of processes (\(p = 5000\)).}
}
@inproceedings{SGF-hscc18,
address = {Porto, Portugal},
month = apr,
publisher = {ACM Press},
editor = {Prandini, Maria and Deshmukh, Jyotirmoy V.},
acronym = {{HSCC}'18},
booktitle = {{P}roceedings of the 21st {ACM} {I}nternational {C}onference
on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
({HSCC}'18)},
author = {Saoud, Adnane and Girard, Antoine and Fribourg, Laurent},
title = {Contract based Design of Symbolic Controllers for Vehicle Platooning},
pages = {277-278},
year = {2018},
doi = {10.1145/3178126.3187001},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SGF-hscc18.pdf},
abstract = {In this work, we present an application of symbolic control and contract
based design techniques to vehicle platooning. We use a compositional approach based on continuous-time assume-guarantee contracts. Each vehicle in the platoon is assigned an assumeguarantee contract; and a controller is synthesized using symbolic control to enforce the satisfaction of this contract. The assumeguarantee framework makes it possible to deal with different types of vehicles and asynchronous controllers (i.e controllers with different
sampling periods). Numerical results illustrate the effectiveness of the approach.},
note = {Poster}
}
@inproceedings{LFV-adhs18,
address = {Oxford, UK},
month = jul,
year = 2018,
number = 16,
volume = 51,
series = {IFAC-PapersOnLine},
publisher = {Elsevier Science Publishers},
editor = {Alessandro Abate and Antoine Girard and Maurice Heemels},
acronym = {{ADHS}'18},
booktitle = {{P}roceedings of the 6th {IFAC} {C}onference on {A}nalysis and
{D}esign of {H}ybrid {S}ystems ({ADHS}'18)},
author = {Adrien Le{ }Co{\"e}nt and Laurent Fribourg and Jonathan Vacher},
title = {Control Synthesis for Stochastic Switched Systems using the Tamed Euler Method},
pages = {259-264},
url = {https://doi.org/10.1016/j.ifacol.2018.08.044},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LFV-adhs18.pdf},
doi = {10.1016/j.ifacol.2018.08.044},
abstract = {In this paper, we explain how, under the one-sided Lipschitz (OSL) hypothesis, one can find an error bound for a variant of the Euler-Maruyama approximation method for stochastic switched systems. We then explain how this bound can be used to control stochastic switched switched system in order to stabilize them in a given region. The method is illustrated on several examples of the literature.}
}
@inproceedings{SGF-ecc18,
address = {Limassol, Cyprus},
month = jun,
year = 2018,
publisher = {{IEEE} Press},
editor = {Thomas Parisini},
acronym = {{ECC}'18},
booktitle = {{P}roceedings of the European Control Conference ({ECC}'18)},
author = {Adnane Saoud and Antoine Girard and Laurent Fribourg},
title = {On the Composition of Discrete and Continuous-time Assume-Guarantee Contracts for Invariance},
pages = {435-440},
url = {https://ieeexplore.ieee.org/document/8550622},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SGF-ecc18.pdf},
doi = {10.23919/ECC.2018.8550622},
abstract = {Many techniques for verifying invariance prop- erties are limited to systems of moderate size. In this paper, we propose an approach based on assume-guarantee contracts and compositional reasoning for verifying invariance properties of a broad class of discrete-time and continuous-time systems consisting of interconnected components. The notion of assume- guarantee contracts makes it possible to divide responsibil- ities among the system components: a contract specifies an invariance property that a component must fulfill under some assumptions on the behavior of its environment (i.e. of the other components). We define weak and strong semantics of assume- guarantee contracts for both discrete-time and continuous-time systems. We then establish a certain number of results for compositional reasoning, which allow us to show that a global invariance property of the whole system is satisfied when all components satisfy their own contract. Interestingly, we show that the weak satisfaction of the contract is sufficient to deal with cascade compositions, while strong satisfaction is needed to reason about feedback composition. Specific results for systems described by differential inclusions are then developed. Throughout the paper, the main results are illustrated using simple examples.}
}
@article{LFMDC-tcs18,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Adrien Le{ }Co{\"e}nt and
Laurent Fribourg and
Nicolas Markey and
Florian De{ }Vuyst and
Ludovic Chamoin},
title = {Compositional synthesis of state-dependent switching control},
volume = {750},
year = {2018},
pages = {53-68},
doi = {10.1016/j.tcs.2018.01.021},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LFMDC-tcs18.pdf},
url = {https://doi.org/10.1016/j.tcs.2018.01.021},
abstract = {We present a correct-by-design method of state-dependent control synthesis for sampled switching systems. Given a target region R of the state space, our method builds a capture set S and a control that steers any element of S into R. The method works by iterated backward reachability from R. The method is also used to synthesize a recurrence control that makes any state of R return to R infinitely often. We explain how the synthesis method can be performed in a compositional manner, and apply it to the synthesis of a compositional control of a concrete floor-heating system with 11 rooms and up to 2^11=2048 toswitching modes.}
}
@article{LACF-fmsd18,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Adrien Le{ }Co{\"{e}}nt and
Julien {Alexandre dit Sandretto} and
Alexandre Chapoutot and
Laurent Fribourg},
title = {An improved algorithm for the control synthesis of nonlinear sampled switched systems},
volume = {53},
number = {3},
year = {2018},
pages = {363-383},
doi = {10.1007/s10703-017-0305-8},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LACF-fmsd18.pdf},
url = {https://link.springer.com/article/10.1007/s10703-017-0305-8},
abstract = {A novel algorithm for the control synthesis for nonlinear switched systems is presented in this paper. Based on an existing procedure of state-space bisection and made available for nonlinear systems with the help of guaranteed integration, the algorithm has been improved to be able to consider longer patterns of modes with a better pruning approach. Moreover, the use of guaranteed integration also permits to take bounded perturbations and varying parameters into account. It is particularly interesting for safety critical applications, such as in aeronautical, military or medical fields. The whole approach is entirely guaranteed and the induced controllers are correct-by-design. Some experimentations are performed to show the important gain of the new algorithm.}
}
@techreport{JFA-arxiv20,
author = {Jawher Jerray and
Laurent Fribourg and
{\'E}tienne Andr{\'e}},
institution = {Computing Research Repository},
month = june,
number = {2006.09993},
type = {Research Report},
title = {{Guaranteed phase synchronization of hybrid oscillators using symbolic Euler's method: The Brusselator and biped examples}},
year = {2020},
url = {https://arxiv.org/abs/2006.09993},
pdf = {https://arxiv.org/abs/2006.09993}
}
@techreport{JFA-arxiv20bis,
author = {Jawher Jerray and
Laurent Fribourg and
{\'E}tienne Andr{\'e}},
institution = {Computing Research Repository},
month = july,
number = {2007.13644},
type = {Research Report},
title = {{Robust optimal control using dynamic programming and guaranteed Euler's method}},
year = {2020},
url = {https://arxiv.org/abs/2007.13644},
pdf = {https://arxiv.org/abs/2007.13644}
}
@techreport{JF-arxiv20,
author = {Jawher Jerray and Laurent Fribourg},
institution = {Computing Research Repository},
month = december,
number = {2012.09310},
type = {Research Report},
title = {{Generation of bounded invariants via stroboscopic set-valued maps: Application to the stability analysis of parametric time-periodic systems}},
year = {2020},
url = {https://arxiv.org/abs/2012.09310},
pdf = {https://arxiv.org/abs/2012.09310}
}
@inproceedings{ZSGF-ecc19,
address = {Naples, Italy},
month = jun,
publisher = {{IEEE} Press},
acronym = {{ECC}'19},
booktitle = {{P}roceedings of the 18th {E}uropean {C}ontrol {C}onference ({ECC}'19)},
author = {Daniele Zonetti and Adnane Saoud and Antoine Girard and Laurent Fribourg},
title = {A symbolic approach to voltage stability and power sharing in time-varying{DC} microgrids},
pages = {903-909},
year = {2019},
doi = {10.23919/ECC.2019.8796095},
url = {https://doi.org/10.23919/ECC.2019.8796095}
}
@inproceedings{CF-cyphy19,
address = {New York City, NY, USA},
month = oct,
editor = {Roger D. Chamberlain and Martin Grimheden and Walid Taha},
volume = {11971},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
noeditor = {},
acronym = {{CyPhy/WESE}'19},
booktitle = {9th International Workshop on Cyber Physical Systems ({CyPhy}'19) and 15th International Workshop on Model-Based Design ({WESE}'19), Revised Selected Papers},
author = {Adrien {Le Co{\"{e}}nt} and Laurent Fribourg},
title = {Guaranteed Optimal Reachability Control of Reaction-Diffusion Equations Using One-Sided Lipschitz Constants and Model Reduction},
pages = {181-202},
year = {2019},
doi = {10.1007/978-3-030-41131-2_9},
url = {https://doi.org/10.1007/978-3-030-41131-2_9}
}
@inproceedings{DFKN-dsd19,
address = {Kallithea, Greece},
month = aug,
publisher = {{IEEE} Press},
noeditor = {},
acronym = {{DSD}'19},
booktitle = {{P}roceedings of the 22nd {E}uromicro {C}onference on {D}igital {S}ystem {D}esign ({DSD}'19)},
author = {Jean{-}Luc Danger and Laurent Fribourg and Ulrich K{\"u}hne and Maha Naceur},
title = {LAOCO{\"O}N: {A} Run-Time Monitoring and Verification Approach for Hardware Trojan Detection},
pages = {269-276},
year = {2019},
doi = {10.1109/DSD.2019.00047},
url = {https://doi.org/10.1109/DSD.2019.00047}
}
@inproceedings{CF-cdc19,
address = {Nice, France},
month = dec,
publisher = {{IEEE} Control System Society},
noeditor = {},
acronym = {{CDC}'19},
booktitle = {{P}roceedings of the 58th {IEEE} {C}onference on
{D}ecision and {C}ontrol ({CDC}'19)},
author = {Adrien {Le Co{\"e}nt} and Laurent Fribourg},
title = {Guaranteed Control of Sampled Switched Systems using Semi-Lagrangian Schemes and One-Sided Lipschitz Constants},
pages = {599-604},
year = {2019},
doi = {10.1109/CDC40024.2019.9029376},
pdf = {https://arxiv.org/pdf/1903.05882.pdf},
url = {https://doi.org/10.1109/CDC40024.2019.9029376}
}
@inproceedings{ACFJL-acsd19,
address = {Aachen, Germany},
month = jun,
publisher = {{IEEE} Computer Society Press},
editor = {J{\"o}rg Keller and Wojciech Penczek},
acronym = {{ACSD}'19},
booktitle = {{P}roceedings of the 19th {I}nternational
{C}onference on {A}pplication of {C}oncurrency
to {S}ystem {D}esign
({ACSD}'19)},
author = {{\'E}tienne Andr{\'e} and Emmanuel Coquard and Laurent Fribourg and Jawher Jerray and David Lesens},
title = {Parametric Schedulability Analysis of a Launcher Flight Control System Under Reactivity Constraints},
pages = {13-22},
year = {2019},
doi = {10.1109/ACSD.2019.00006},
url = {https://doi.org/10.1109/ACSD.2019.00006}
}
This file was generated by bibtex2html 1.98.