@inproceedings{F-Petri82,
address = {Varenna, Italy},
month = sep,
year = 1982,
acronym = {{APN}'82},
booktitle = {{P}roceedings of the 3rd
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({APN}'82)},
author = {Finkel, Alain},
title = {About monogeneous fifo {P}etri nets},
missingpages = {}
}
@inproceedings{FM-Petri83,
address = {Dortmund, Germany},
year = 1982,
volume = 145,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Cremers, Armin B. and Kriegel, Hans-Peter},
booktitle = {{P}roceedings of the 6th {GI}-{C}onference
on Theoretical Computer Science},
author = {Finkel, Alain and Memmi, G{\'e}rard},
title = {Fifo nets: a new model of parallel computation},
pages = {111-121}
}
@inproceedings{F-fsttcs83,
address = {Bangalore, India},
month = dec,
year = 1983,
novolume = {},
noseries = {},
acronym = {{FSTTCS}'83},
booktitle = {{P}roceedings of the 3rd {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'83)},
author = {Finkel, Alain},
title = {Control of a {P}etri net by a finite automaton}
}
@inproceedings{F-stacs84,
address = {Paris, France},
month = apr,
year = 1984,
volume = 166,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Fontet, Max and Mehlhorn, Kurt},
acronym = {{STACS}'84},
booktitle = {{P}roceedings of the 1st {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'84)},
author = {Finkel, Alain},
title = {Blocage et vivacit{\'e} dans les r{\'e}seaux {\`a} pile-file},
pages = {151-162}
}
@article{FM-tcs85,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Finkel, Alain and Memmi, G{\'e}rard},
title = {An introduction to {F}ifo nets~-- monogeneous nets:
a subclass of {F}ifo nets},
year = {1985},
volume = {35},
pages = {191-214}
}
@article{F-tcs85,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Finkel, Alain},
title = {Une g{\'e}n{\'e}ralisation des th{\'e}or{\`e}mes de {H}igman
et de {S}imon aux mots infinis},
year = 1985,
volume = 38,
pages = {137-142}
}
@inproceedings{FC-Petri87,
address = {Zaragoza, Spain},
month = jun,
year = 1987,
novolume = {},
noseries = {},
acronym = {{APN}'87},
booktitle = {{P}roceedings of the 8th
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({APN}'87)},
author = {Finkel, Alain and Choquet, Annie},
title = {Simulation of linear fifo nets by {P}etri nets
having a structured set of terminal markings},
missingpages = {}
}
@inproceedings{F-icalp87,
address = {Karlsruhe, Germany},
month = jul,
year = 1987,
volume = 267,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Thomas Ottmann},
acronym = {{ICALP}'87},
booktitle = {{P}roceedings of the 14th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming
({ICALP}'87)},
author = {Finkel, Alain},
title = {A generalization of the procedure of {K}arp and {M}iller
to well structured transition system},
pages = {499-508},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/F-icalp87.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/F-icalp87.pdf}
}
@article{FC-ai88,
publisher = {Springer},
journal = {Acta Informatica},
author = {Finkel, Alain and Choquet, Annie},
title = {Fifo nets without order deadlock},
pages = {15-36},
year = 1987,
volume = 25
}
@inproceedings{FR-lncs-APetri88,
address = {Zaragoza, Spain},
year = 1988,
volume = 340,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Rozenberg, Grzegorz},
acronym = {{APN}'87},
booktitle = {{A}dvances in {P}etri {N}ets~1988,
{S}elected {P}apers from the 8th
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({APN}'87)},
author = {Finkel, Alain and Rosier, Louis},
title = {A Survey on the Decidability Questions for Classes of {FIFO} Nets},
pages = {106-132}
}
@inproceedings{F-ifip88,
address = {Atlantic City, New~Jersey, USA},
month = jun,
year = 1988,
publisher = {North-Holland},
editor = {Aggrawal, Sudhir and Sabnani, Krishan K.},
acronym = {{PSTV}'88},
booktitle = {{P}roceedings of the {IFIP} {WG}6.1
8th {I}nternational {C}onference on {P}rotocol
{S}pecification, {T}esting and {V}erification
({PSTV}'88)},
author = {Finkel, Alain},
title = {A new class of analysable {CFSM}s with unbounded {FIFO} channels},
missingpages = {}
}
@inproceedings{BF-isiis88,
address = {Tokyo, Japan},
month = nov,
year = 1988,
novolume = {},
noseries = {},
publisher = {{IOS} Press},
editor = {Tanaka, Hidehiko and Tojo, Akio},
acronym = {{ISIIS}'88},
booktitle = {{P}roceedings of the 2nd {I}nternational {S}ymposium on
{I}nteroperable {I}nformation {S}ystems
({ISIIS}'88)},
author = {Bochmann, Gregor and Finkel, Alain},
title = {Impact of queued interaction on protocol specification and verification},
missingpages = {}
}
@article{GB-AF-CJ-LP-PN-90,
address = {Bonn, Germany},
publisher = {Gesellschaft f{\"u}r Informatik},
journal = {Petri Net Newsletter},
author = {Berthelot, G{\'e}rard and Finkel, Alain and
Johnen, Colette and Petrucci, Laure},
title = {A Generic Example for Testing Performance of
Reachability and Covering Graphs Construction
Algorithms},
volume = {35},
pages = {6-7},
year = {1990},
month = apr
}
@article{F90,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Finkel, Alain},
title = {Reduction and covering of infinite reachability trees},
year = 1990,
pages = {144-179},
volume = 89,
number = 2
}
@techreport{AF-CJ-LP-92,
author = {Finkel, Alain and Johnen, Colette and
Petrucci, Laure},
title = {Decomposition of {P}etri Nets for Parallel
Analysis},
missingnumber = {??},
othernumber = {LRI - 706, dec. 1991 mais avec titre different...},
year = {1992},
missingyear = {1991, en fait ?},
missingmonth = {},
missingnmonth = {},
institution = {Laboratoire d'Informatique Fondamentale et
Appliqu\'ee de Cachan, ENS Cachan, France}
}
@inproceedings{AF-LP-CAV-91,
address = {Aalborg, Denmark},
year = 1992,
volume = 575,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Larsen, Kim G. and Skou, Arne},
acronym = {{CAV}'91},
booktitle = {{P}roceedings of the 3rd
{I}nternational {W}orkshop on
{C}omputer {A}ided {V}erification
({CAV}'91)},
author = {Finkel, Alain and Petrucci, Laure},
title = {Avoiding State Explosion by Composition of Minimal
Covering Graphs},
pages = {169-180}
}
@inproceedings{AF-APN-93-MCG,
address = {Gjern, Denmark},
year = 1993,
volume = 674,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Rozenberg, Grzegorz},
acronym = {{APN}'91},
booktitle = {{P}apers from the 12th
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({APN}'91)},
author = {Finkel, Alain},
title = {The Minimal Coverability Graph for {P}etri Nets},
pages = {210-243}
}
@article{AF-DistC-94,
publisher = {Springer},
journal = {Distributed Computing},
author = {Finkel, Alain},
title = {Decidability of the Termination Problem for
Completely Specified Protocols},
volume = {7},
number = {3},
pages = {129-135},
year = {1994},
missingnmonth = {},
missingmonth = {},
doi = {10.1007/BF02277857}
}
@inproceedings{AF-IT-SLL-94-CatGram,
address = {Noszvaj, Hungary},
month = sep,
year = 1994,
booktitle = {{P}roceedings of the 5th {S}ymposium
on {L}ogic and {L}anguage},
author = {Finkel, Alain and Tellier, Isabelle},
title = {An Algorithmic Overview On Categorial Grammars
(extended abstract)},
missingpages = {??}
}
@article{AF-LP-RAI-94,
address = {Les Ulis, France},
publisher = {EDP Sciences},
journal = {RAIRO Informatique Th{\'e}orique et Applications},
author = {Finkel, Alain and Petrucci, Laure},
title = {Propri{\'e}t{\'e}s de la
composition{\slash }d{\'e}composition
de r{\'e}seaux
de {P}etri et de leurs graphes de couverture},
volume = {28},
number = {2},
pages = {73-124},
year = {1994},
missingmonth = {},
missingnmonth = {}
}
@inproceedings{GC-AF-SPI-ACM-94,
address = {New Orleans, Louisiana, USA},
month = dec,
year = 1994,
number = 5,
volume = 19,
series = {{ACM} {SIGSOFT} Software Engineering Notes},
editor = {Wile, David S.},
acronym = {{SIGSOFT} {FSE}'94},
booktitle = {{P}roceedings of the 2nd {ACM} {SIGSOFT}
{S}ymposium on {F}oundations of {S}oftware
{E}ngineering
({SIGSOFT} {FSE}'94)},
author = {C{\'e}c{\'e}, G{\'e}rard and Finkel, Alain and
Purushothaman{ }Iyer, S.},
title = {Duplication, Insertion and Lossiness Errors in
Unreliable Communication Channels},
pages = {35-43}
}
@inproceedings{AF-IT-SLL-95-Cat,
address = {Donostia, San Sebastian, Spain},
year = 1998,
publisher = {Kluwer Academic Publishers},
editor = {Arrazola, Xavier and Korta, Kepa and
Pelletier, Francis J.},
acronym = {{ICCS}'95},
booktitle = {{P}roceedings of the 4th {I}nternational
{C}olloquium on {C}ognitive {S}cience
({ICCS}'95)},
author = {Finkel, Alain and Tellier, Isabelle},
title = {From Natural Language to Cognitive Style},
pages = {271-279},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FT-ICCS95.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FT-ICCS95.pdf}
}
@inproceedings{AF-OM-LP-CFIP-94,
address = {Rennes, France},
month = may,
year = 1995,
publisher = {Herm{\`e}s},
editor = {Jard, Claude and Rolin, Pierre},
booktitle = {{A}ctes du 4{\`e}me {C}olloque {F}rancophone
sur l'{I}ng{\'e}nierie des {P}rotocoles},
author = {Finkel, Alain and Marc{\'e}, Olivier and
Petrucci, Laure},
title = {Un algorithme en {\(n^{3/2}\)} pour le probl\`eme
de la
borne des bonnes places d'un r\'eseau de {P}etri},
pages = {401-418}
}
@inproceedings{AF-PM-ITCS-95,
address = {Ravello, Italy},
month = nov,
year = 1995,
publisher = {World Scientific},
editor = {De Santis, Alfredo},
acronym = {{ICTCS}'95},
booktitle = {{P}roceedings of the 5th {I}talian
{C}onference on {T}heoretical {C}omputer
{S}cience
({ICTCS}'95)},
author = {Finkel, Alain and McKenzie, Pierre},
title = {Verifying Identical Communicating Processes is
Undecidable},
pages = {307-322}
}
@inproceedings{AF-IT-DLS-CL-96,
missingorganization = {},
missingmonth = {},
missingnmonth = {},
year = 1996,
volume = 273,
series = {Duisburg L.A.U.D.\ Symposium, Series B: Applied
and Interdisciplinary Papers},
editor = {Endres-Niggemeyer, Brigitte and Inchaurralde, Carlos},
booktitle = {{T}he {C}ognitive {L}evel: {L}anguage and
{M}ind {M}odelized},
author = {Finkel, Alain and Tellier, Isabelle},
title = {The Cognitive Style of Decision Making Narrations},
pages = {41-59},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FT-LAUD96.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FT-LAUD96.pdf}
}
@techreport{AF-IT-RI-96-ICA,
author = {Finkel, Alain and Tellier, Isabelle},
title = {Individual Regularities and Cognitive Automata},
type = {Internal Report},
number = {96-2},
year = {1996},
month = mar,
institution = {Laboratoire d'Informatique Fondamentale et
Appliqu\'ee de Cachan, ENS Cachan, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FinkelTellier96.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FinkelTellier96.pdf}
}
@article{AF-IT-TCS-96,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Finkel, Alain and Tellier, Isabelle},
title = {A Polynomial Algorithm for the Membership Problem with
Categorial Grammars},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FT-tcs96.pdf},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FT-tcs96.pdf},
volume = {164},
number = {1-2},
pages = {207-221},
year = {1996},
month = sep
}
@techreport{AF-McKP-CP-MCT-96,
author = {Finkel, Alain and McKenzie, Pierre and
Picaronny, Claudine},
title = {Minimal Coverability Trees for High Level Nets},
type = {Internal Report},
number = {96-3},
year = {1996},
month = mar,
institution = {Laboratoire d'Informatique Fondamentale et
Appliqu\'ee de Cachan, ENS Cachan, France}
}
@techreport{CD-AF-ICAFL-96-Norm,
author = {Dufourd, Catherine and Finkel, Alain},
title = {A Polynomial {{\(\lambda\)}}-Bisimilar Normalization for
{P}etri Nets},
type = {Internal Report},
number = {96-1},
year = {1996},
month = mar,
institution = {Laboratoire d'Informatique Fondamentale et
Appliqu\'ee de Cachan, ENS Cachan, France},
missinglsv-category = {was autc}
}
@article{GC-AF-SPI-IC-96,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {C{\'e}c{\'e}, G{\'e}rard and Finkel, Alain and
Purushothaman{ }Iyer, S.},
title = {Unreliable Channels are Easier to Verify than Perfect
Channels},
volume = {124},
number = {1},
pages = {20-31},
year = {1996},
month = jan,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CFP-IC96.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CFP-IC96.ps}
}
@techreport{OM-AF-96,
author = {Finkel, Alain and Marc{\'e}, Olivier},
title = {Verification of Infinite Regular Communicating
Automata},
type = {Internal Report},
number = {96-4},
year = {1996},
month = apr,
institution = {Laboratoire d'Informatique Fondamentale et
Appliqu\'ee de Cachan, ENS Cachan, France}
}
@techreport{ZB-AF-RI-96-PNR,
author = {Bouziane, Zakaria and Finkel, Alain},
title = {La v{\'e}rification des r{\'e}seaux de {P}etri
r{\'e}versibles est primitive r{\'e}cursive},
type = {Internal Report},
number = {96-6},
year = {1996},
month = jun,
institution = {Laboratoire d'Informatique Fondamentale et
Appliqu\'ee de Cachan, ENS Cachan, France}
}
@inproceedings{AF-BW-PW-INF-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 = {Finkel, Alain and Willems, Bernard and Wolper, Pierre},
title = {A Direct Symbolic Approach to Model Checking Pushdown
Systems (Extended Abstract)},
pages = {27-39},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FWW-infinity97.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FWW-infinity97.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FWW-infinity97.pdf}
}
@misc{AF-CC-RG-GDR-PRC-ISIS-CHM-97,
author = {Collet, {\relax Ch}ristophe and Finkel, Alain and
Rachid Gherbi},
title = {Prise en compte dynamique des attitudes perceptive de
l'usager},
year = {1997},
missingmonth = {},
missingnmonth = {},
howpublished = {Rapport de synth{\`e}se (version~IV de l'Action Inter-{PRC}
10.2 {GDR}-{PRC} {ISIS} \& {CHM} : <<~Interaction
Syst{\`e}me-Environnement pour l'Interpr{\'e}tation des
Signaux et des Images~>>},
lsv-lang = {FR}
}
@inproceedings{AF-CC-RG-IEEE-97,
address = {Budapest, Hungary},
month = sep,
year = 1997,
publisher = {{IEEE} Press},
acronym = {{INES}'97},
booktitle = {{P}roceedings of the {IEEE} {I}nternational
{C}onference on {I}ntelligent {E}ngineering
{S}ystems
({INES}'97)},
author = {Collet, {\relax Ch}ristophe and Finkel, Alain and
Rachid Gherbi},
title = {Gaze Capture System in Man-Machine Interaction},
pages = {557-581},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CFG-ines97.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CFG-ines97.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CFG-ines97.pdf}
}
@inproceedings{AF-CC-RG-Inter-97,
address = {Montpellier, France},
month = may,
year = 1997,
booktitle = {{A}ctes des 6{\`e}mes {J}ourn{\'e}es
{I}nternationales {I}nterfaces},
author = {Collet, {\relax Ch}ristophe and Finkel, Alain and
Rachid Gherbi},
title = {{C}ap{R}e : un syst{\`e}me de capture du regard dans un
contexte d'interaction homme-machine},
pages = {36-39},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CFG-jiim97.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CFG-jiim97.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CFG-jiim97.pdf},
lsv-lang = {FR}
}
@inproceedings{AF-CD-FSTTCS-97,
address = {Kharagpur, India},
month = dec,
year = 1997,
volume = 1346,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ramesh, S. and Sivakumar, G.},
acronym = {{FSTTCS}'97},
booktitle = {{P}roceedings of the 17th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'97)},
author = {Dufourd, Catherine and Finkel, Alain},
title = {Polynomial-Time Many-One Reductions for {P}etri Nets},
pages = {312-326},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DufFin-fsttcs97.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DufFin-fsttcs97.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DufFin-fsttcs97.pdf}
}
@inproceedings{AF-CT-CAV-97,
address = {Haifa, Israel},
month = jun,
year = 1997,
volume = 1254,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Grumberg, Orna},
acronym = {{CAV}'97},
booktitle = {{P}roceedings of the 9th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'97)},
author = {C{\'e}c{\'e}, G{\'e}rard and Finkel, Alain},
title = {Programs with Quasi-Stable Channels are Effectively
Recognizable},
pages = {304-315},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CecFin-cav97.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CecFin-cav97.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CecFin-cav97.pdf}
}
@inproceedings{AF-GRE-97,
address = {Grenoble, France},
month = mar,
year = 1997,
booktitle = {{P}roceedings of the
{G}renoble-{A}lpes d'{H}uez {E}uropean {S}chool
of {C}omputer {S}cience, {M}ethods and {T}ools
for the {V}erification of {I}nfinite {S}tate
{S}ystems},
author = {Finkel, Alain},
title = {Algorithms and Semi-Algorithms for Infinite State
Systems},
pages = {189-190},
note = {Invited tutorial}
}
@article{AF-PMc-TCS-97,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Finkel, Alain and McKenzie, Pierre},
title = {Verifying Identical Communicating Processes is
Undecidable},
volume = {174},
number = {1-2},
pages = {217-230},
year = {1997},
month = mar,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FMK-TCS97.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FMK-TCS97.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FMK-TCS97.pdf}
}
@inproceedings{AF-ZB-INF-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 = {Bouziane, Zakaria and Finkel, Alain},
title = {Cyclic {P}etri Net Reachability Sets are Semi-Linear
Effectively Constructible},
pages = {15-24},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BF-infinity97.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BF-infinity97.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BF-infinity97.pdf}
}
@misc{AF-MOVEP-98,
author = {Finkel, Alain},
title = {Analyse des syst{\`e}mes infinis bien
structur{\'e}s ou <<~reconnaissables~>>},
howpublished = {Invited tutorial, 3{\`e}me {\'E}cole d'{\'e}t{\'e}
{M}od{\'e}lisation et {V}{\'e}rification des
{P}rocessus {P}arall{\`e}les
({MOVEP}'98), Nantes, France},
year = 1998,
month = jul,
lsv-lang = {FR}
}
@inproceedings{AF-ZB-98-RevPN,
address = {Kunming, China},
year = 1998,
publisher = {Springer},
editor = {Shum, Kar Ping and Guo, Yuqi and Ito, Massami
and Fong, Yuen},
booktitle = {{P}roceedings of the {I}nternational
{C}onference in {S}emigroups and its
{R}elated {T}opics},
author = {Bouziane, Zakaria and Finkel, Alain},
title = {The Equivalence Problem for Commutative
Semigroups and
Reversible {P}etri Nets is Complete in Exponential
Space under Log-Lin Reducibility},
pages = {63-76}
}
@article{CC-AF-RG-aci98,
address = {Tokyo, Japan},
publisher = {Fuji Technology Press},
journal = {Journal of Advanced
Computational Intelligence},
author = {Collet, {\relax Ch}ristophe and Finkel, Alain and
Gherbi, Rachid},
title = {{C}ap{R}e: {A}~Gaze Tracking System in Man-Machine
Interaction},
volume = {2},
number = {3},
pages = {77-81},
year = {1998},
missingnmonth = {},
missingmonth = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CFG-JACI98.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CFG-JACI98.ps}
}
@techreport{DD3-98,
author = {B{\'e}rard, B{\'e}atrice and
C{\'e}c{\'e}, G{\'e}rard and
Dufourd, Catherine and Finkel, Alain and
Laroussinie, Fran{\c{c}}ois and Petit, Antoine and
Schnoebelen, {\relax Ph}ilippe and
Sutre, Gr{\'e}goire},
title = {Le model-checking, une technique de
v{\'e}rification en
plein essor. {II}~--- {Q}uelques outils},
year = {1998},
month = oct,
type = {Contract Report},
institution = {EDF/DER/MOS - LSV},
lsv-lang = {FR}
}
@inproceedings{dufourd98,
address = {Aalborg, Denmark},
month = jul,
year = 1998,
volume = 1443,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Larsen, Kim G. and Skyum, Sven and Winskel, Glynn},
acronym = {{ICALP}'98},
booktitle = {{P}roceedings of the 25th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming
({ICALP}'98)},
author = {Dufourd, Catherine and Finkel, Alain and
Schnoebelen, {\relax Ph}ilippe},
title = {Reset Nets between Decidability and
Undecidability},
pages = {103-115},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DFS-icalp98.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DFS-icalp98.ps},
doi = {10.1007/BFb0055044},
abstract = {We study Petri nets with Reset arcs (also Transfer and
Doubling arcs) in combination with other extensions of
the basic Petri net model. While Reachability is
undecidable in all these extensions (indeed they are
Turing-powerful), we exhibit unexpected frontiers for
the decidability of Termination, Coverability,
Boundedness and place-Boundedness. In particular, we
show counter-intuitive separations between seemingly
related problems. Our main theorem is the very
surprising fact that boundedness is undecidable for
Petri nets with Reset arcs.}
}
@inproceedings{finkel98,
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 = {Finkel, Alain and Schnoebelen, {\relax Ph}ilippe},
title = {Fundamental Structures in Well-Structured Infinite
Transition Systems},
pages = {102-118},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FinSch-latin98.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FinSch-latin98.ps},
doi = {10.1007/BFb0054314}
}
@techreport{sscop-98,
author = {C{\'e}c{\'e}, G{\'e}rard and Deutsch, Pierre-{\'E}tienne
and Finkel, Alain},
title = {{FORMA}{\slash}{SSCOP}~--- {LSV}, bilan de l'ann{\'e}e~1998},
year = {1998},
month = nov,
type = {Contract Report},
institution = {FORMA},
lsv-lang = {FR}
}
@article{AF-CD-TCS-Note,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Dufourd, Catherine and Finkel, Alain},
title = {A Polynomial {{\(\lambda\)}}-Bisimilar Normalization
for Reset {P}etri Nets},
volume = {222},
number = {1-2},
pages = {187-194},
year = {1999},
month = jul,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DufFin-TCS99.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DufFin-TCS99.ps}
}
@techreport{LSV:99:2,
author = {Finkel, Alain and McKenzie, Pierre and
Picaronny, Claudine},
title = {A~Well-Structured Framework for Analysing {P}etri
Net Extensions},
type = {Research Report},
number = {LSV-99-2},
year = {1999},
month = feb,
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-1999-2.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-1999-2.rr.ps}
}
@inproceedings{esparza99,
address = {Trento, Italy},
month = jul,
year = 1999,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'99},
booktitle = {{P}roceedings of the 14th
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'99)},
author = {Esparza, Javier and Finkel, Alain and Mayr, Richard},
title = {On the verification of broadcast protocols},
pages = {352-359},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/EFM-lics99.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/EFM-lics99.ps}
}
@inproceedings{sutre99,
address = {Amazonia, Brasil},
month = jan,
year = 1999,
volume = 1548,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Haeberer, Armando Martin},
acronym = {{AMAST}'98},
booktitle = {{P}roceedings of the 7th {I}nternational
{C}onference on {A}lgebraic {M}ethodology and
{S}oftware {T}echnology
({AMAST}'98)},
author = {Sutre, Gr{\'e}goire and Finkel, Alain and
Roux, Olivier F. and Cassez, Franck},
title = {Effective Recognizability and Model Checking of
Reactive Fiffo Automata},
pages = {106-123},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-1998-10.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-1998-10.rr.ps}
}
@inproceedings{AF-GS-STACS-2000,
address = {Lille, France},
month = feb,
year = 2000,
volume = 1770,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Reichel, Horst and Tison, Sophie},
acronym = {{STACS} 2000},
booktitle = {{P}roceedings of the 17th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS} 2000)},
author = {Finkel, Alain and Sutre, Gr{\'e}goire},
title = {Decidability of Reachability Problems for Classes
of Two-Counter Automata},
pages = {346-357},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FinSut-stacs2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FinSut-stacs2000.ps},
doi = {10.1007/3-540-46541-3_29}
}
@article{BEFMRWW-ipl2000,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Bouajjani, Ahmed and Esparza, Javier and
Finkel, Alain and Maler, Oded
and Rossmanith, Peter and Willems, Bernard and
Wolper, Pierre},
title = {An Efficient Automata Approach to some Problems on
Context-Free Grammars},
volume = {74},
number = {5-6},
pages = {221-227},
year = {2000},
month = jun,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BEFMRWW-IPL2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BEFMRWW-IPL2000.ps}
}
@inproceedings{FPS-concur-2000,
address = {Pennsylvania State University, Pennsylvania, USA},
month = aug,
year = 2000,
volume = 1877,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Palamidessi, Catuscia},
acronym = {{CONCUR} 2000},
booktitle = {{P}roceedings of the 11th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR} 2000)},
author = {Finkel, Alain and Purushothaman{ }Iyer, S. and
Sutre, Gr{\'e}goire},
title = {Well-Abstracted Transition Systems},
pages = {566-580},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2000-6.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2000-6.rr.ps}
}
@inproceedings{FS-mfcs-2000,
address = {Bratislava, Slovakia},
month = aug,
year = 2000,
volume = 1893,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Nielsen, Mogens and Rovan, Branislav},
acronym = {{MFCS} 2000},
booktitle = {{P}roceedings of the 25th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS} 2000)},
author = {Finkel, Alain and Sutre, Gr{\'e}goire},
title = {An Algorithm Constructing the Semilinear {P}ost*
for
2-Dim {R}eset{{\slash}}{T}ransfer {VASS}},
pages = {353-362},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FinSut-mfcs2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FinSut-mfcs2000.ps}
}
@inproceedings{finkel-leroux-vcl2000,
address = {London, UK},
month = jul,
year = 2000,
publisher = {University of Southampton, Southampton, UK},
editor = {Leuschel, Michael and Podelski, Andreas and
Ramakrishnan, C. R. and Ultes{-}Nitsche, Ulrich},
acronym = {{VCL} 2000},
booktitle = {{P}roceedings of the {I}nternational
{W}orkshop on {V}erification and
{C}omputational {L}ogic
({VCL} 2000)},
author = {Finkel, Alain and Leroux, J{\'e}r{\^o}me},
title = {A Finite Covering Tree for Analysing Entropic
Broadcast Protocols},
nopages = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FinLer-vcl2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FinLer-vcl2000.ps}
}
@article{finkel98b,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Finkel, Alain and Schnoebelen, {\relax Ph}ilippe},
title = {Well-Structured Transition Systems Everywhere!},
volume = {256},
number = {1-2},
pages = {63-92},
year = {2001},
month = apr,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FinSch-TCS99.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FinSch-TCS99.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FinSch-TCS99.ps},
doi = {10.1016/S0304-3975(00)00102-X},
abstract = {Well-structured transition systems
(WSTS's) are a general class of infinite state
systems for which decidability results rely on the
existence of a well-quasi-ordering between states
that is compatible with the transitions.\par
In this article, we provide an extensive treatment
of the WSTS idea and show several new results.
Our improved definitions allow many examples of
classical systems to be seen as instances of
WSTS's.}
}
@book{lsvmcbook01,
author = {B{\'e}rard, B{\'e}atrice and Bidoit, Michel and Finkel, Alain
and Laroussinie, Fran{\c{c}}ois and
Petit, Antoine and Petrucci, Laure and
Schnoebelen, {\relax Ph}ilippe},
title = {Systems and Software Verification. {M}odel-Checking
Techniques and Tools},
year = {2001},
missingmonth = {},
missingnmonth = {},
publisher = {Springer},
isbn = {3-540-41523-8},
url = {http://www.springer.com/978-3-540-41523-8},
olderurl = {http://www.springer.de/cgi-bin/search_book.pl?isbn=3-540-41523-8}
}
@inproceedings{FRSV-infinity2002,
address = {Brno, Czech Republic},
month = aug,
year = 2002,
number = 6,
volume = 68,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Ku{\v c}era, Anton{\'\i}n and Mayr, Richard},
acronym = {{INFINITY}'02},
booktitle = {{P}roceedings of the 4th {I}nternational
{W}orkshop on {V}erification of {I}nfinite
{S}tate {S}ystems
({INFINITY}'02)},
author = {Finkel, Alain and Raskin, Jean-Fran{\c{c}}ois and
Samuelides, Mathias and Van{~}Begin, Laurent},
title = {Monotonic Extensions of {P}etri Nets: Forward and
Backward Search Revisited},
pages = {121-144},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FRSVB-infinity2002.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FRSVB-infinity2002.ps}
}
@inproceedings{FinLer-fsttcs2002,
address = {Kanpur, India},
month = dec,
year = 2002,
volume = 2556,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Agrawal, Manindra and Seth, Anil},
acronym = {{FSTTCS}'02},
booktitle = {{P}roceedings of the 22nd {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'02)},
author = {Finkel, Alain and Leroux, J{\'e}r{\^o}me},
title = {How To Compose {P}resburger-Accelerations:
Applications to Broadcast Protocols},
pages = {145-156},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2002-14.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2002-14.rr.ps}
}
@misc{FinLer-invit2002,
author = {Finkel, Alain and Leroux, J{\'e}r{\^o}me},
title = {Acceleration of Loops for Verification},
year = {2002},
month = oct,
howpublished = {Invited talk, Workshop on Mathematical Models and
Techniques for Analysing Systems,
Montr\'eal, Canada},
oldlsv-time = {ant}
}
@inproceedings{HCFRS-latin2002,
address = {Cancun, Mexico},
month = apr,
year = 2002,
volume = 2286,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Rajsbaum, Sergio},
acronym = {{LATIN}'02},
booktitle = {{P}roceedings of the 5th {L}atin {A}merican
{S}ymposium on {T}heoretical {I}nformatics
({LATIN}'02)},
author = {Herbreteau, Fr{\'e}d{\'e}ric and Cassez, Franck and
Finkel, Alain and Roux, Olivier F.
and Sutre, Gr{\'e}goire},
title = {Verification of Embedded Reactive Fiffo Systems},
pages = {400-414},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/HCFRS-latin2002.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/HCFRS-latin2002.ps}
}
@techreport{BFN-edf10,
author = {Bardin, S{\'e}bastien and Finkel, Alain and
Nowak, David},
title = {Note de synth{\`e}se {\`a}~10~mois},
year = {2003},
month = aug,
type = {Contract Report},
number = {P11L03/F01304/0 + 50.0241},
institution = {collaboration entre EDF et le LSV},
oldhowpublished = {Contrat P11L03/F01304/0 et 50.0241 de collaboration
entre EDF et le LSV},
note = {21~pages}
}
@techreport{BFN-edf12,
author = {Bardin, S{\'e}bastien and Finkel, Alain and
Nowak, David},
title = {Rapport final},
year = {2003},
month = nov,
type = {Contract Report},
number = {P11L03/F01304/0 + 50.0241},
institution = {collaboration entre EDF et le LSV},
oldhowpublished = {Contrat P11L03/F01304/0 et 50.0241 de collaboration
entre EDF et le~LSV},
note = {50~pages}
}
@techreport{BFNS-edf6,
author = {Bardin, S{\'e}bastien and Finkel, Alain and
Nowak, David and
Schnoebelen, {\relax Ph}ilippe},
title = {Note de synth{\`e}se {\`a} 6 mois},
year = {2003},
month = jul,
type = {Contract Report},
number = {P11L03/F01304/0 + 50.0241},
institution = {collaboration entre EDF et le LSV},
oldhowpublished = {Contrat P11L03/F01304/0 et 50.0241 de collaboration
entre EDF et le LSV},
note = {43~pages}
}
@inproceedings{FAST-cav03,
address = {Boulder, Colorado, USA},
month = jul,
year = 2003,
volume = 2725,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Hunt, Jr, Warren A. and Somenzi, Fabio},
acronym = {{CAV}'03},
booktitle = {{P}roceedings of the 15th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'03)},
author = {Bardin, S{\'e}bastien and Finkel, Alain and
Leroux, J{\'e}r{\^o}me and
Petrucci, Laure},
title = {{FAST}: {F}ast {A}cceleration of {S}ymbolic
{T}ransition Systems},
pages = {118-121},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FAST-cav03.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FAST-cav03.ps},
abstract = {FAST is a tool for the analysis
of infinite systems. This paper describes the
underlying theory, the architecture choices
that have been made in the tool design. The
user must provide a model to analyse, the
property to check and a computation policy.
Several such policies are proposed as a
standard in the package, others can be added by
the user. FAST capabilities are compared with
those of other tools. A range of case studies
from the literature has been investigated. }
}
@article{FPS-ICOMP,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Finkel, Alain and Purushothaman{ }Iyer, S. and
Sutre, Gr{\'e}goire},
title = {Well-Abstracted Transition Systems: {A}pplication to
{FIFO} Automata},
volume = {181},
number = {1},
pages = {1-31},
year = {2003},
month = feb,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FPS-ICOMP.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FPS-ICOMP.ps}
}
@misc{Fast1-manual,
author = {Bardin, S{\'e}bastien and Finkel, Alain and
Leroux, J{\'e}r{\^o}me and Petrucci, Laure
and Worobel, Laurent},
title = {{FAST} User's Manual},
year = {2003},
month = aug,
oldhowpublished = {Available at
\url{http://www.lsv.ens-cachan.fr/fast/doc/manual.ps}},
note = {33~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FAST-manual.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FAST-manual.ps}
}
@misc{FinLer-FAST2002,
author = {Bardin, S{\'e}bastien and Finkel, Alain and
Leroux, J{\'e}r{\^o}me},
title = {{FAST} v1.0: {F}ast {A}cceleration of {S}ymbolic
{T}ransition Systems},
year = {2003},
month = jul,
oldhowpublished = {Available at \url{www.lsv.ens-cachan.fr/fast/}},
note = {See~\cite{FAST-cav03} for description. Written in C++
(about 4400 lines on top of the MONA v1.4 library)},
note-fr = {Voir~\cite{FAST-cav03} pour la description. \'Ecrit en C++
(environ 4400 lignes ajout\'ees \`a la biblioth\`eque MONA~v1.4)},
url = {http://www.lsv.ens-cachan.fr/fast/}
}
@inproceedings{BDF-afadl2004,
address = {Besan{\c{c}}on, France},
month = jun,
year = 2004,
editor = {Julliand, Jacques},
acronym = {{AFADL}'04},
booktitle = {{A}ctes du 6{\`e}me {A}telier sur les {A}pproches {F}ormelles
dans l'{A}ssistance au {D}{\'e}veloppement de {L}ogiciels
({AFADL}'04)},
author = {Bardin, S{\'e}bastien and
Darlot, {\relax Ch}ristophe and Finkel, Alain},
title = {{FAST}: un model-checker pour syst{\`e}mes {\`a}
compteurs},
pages = {377-380},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BDF-afadl04.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BDF-afadl04.ps},
abstract = {FAST est un outil pour la
v\'erification de propri\'et\'es de s\^uret\'e
pour des syst\`emes \`a compteurs.
L'originalit\'e de l'outil tient dans
l'utilisation de repr\'esentations symboliques
pour repr\'esenter des ensembles infinis et de
techniques d'acc\'el\'eration pour augmenter
les chances de convergence. FAST a \'et\'e
appliqu\'e avec succ\`es \`a un grand nombre de
cas non triviaux.}
}
@inproceedings{BF-atva04,
address = {Taipei, Taiwan},
month = oct # {-} # nov,
year = {2004},
volume = {3299},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Wang, Farn},
acronym = {{ATVA}'04},
booktitle = {{P}roceedings of the 2nd {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'04)},
author = {Bardin, S{\'e}bastien and Finkel, Alain},
title = {Composition of accelerations to verify infinite
heterogeneous systems},
pages = {248-262},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BF-atva04.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BF-atva04.ps},
abstract = {Symbolic representations and
acceleration algorithms are emerging methods to
extend model-checking to infinite state space
systems. However until now, there is no general
theory of acceleration, and designing
acceleration algorithms for new data types is a
complex task. On the other hand, protocols
rarely manipulate new data types, rather new
combinations of well-studied data types. For
this reason, in this paper we focus on the
automatic construction of symbolic
representations and acceleration algorithms
from existing ones.}
}
@inproceedings{BFL-tacas04,
address = {Barcelona, Spain},
month = mar,
year = 2004,
volume = 2988,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Jensen, Kurt and Podelski, Andreas},
acronym = {{TACAS}'04},
booktitle = {{P}roceedings of the 10th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'04)},
author = {Bardin, S{\'e}bastien and Finkel, Alain and
Leroux, J{\'e}r{\^o}me},
title = {{FAST}er Acceleration of Counter Automata in
Practice},
pages = {576-590},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BFL-tacas04.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BFL-tacas04.ps},
abstract = {We compute reachability sets of
counter automata. Even if the reachability set
is not necessarily recursive, we use symbolic
representation and acceleration to increase
convergence. For functions defined by
translations over a polyhedral domain, we give
a new acceleration algorithm which is
polynomial in the size of the function and
exponential in its dimension, while the more
generic algorithm is exponential in both the
size of the function and its dimension. This
algorithm has been implemented in the tool
FAST. We apply it to a complex industrial
protocol, the TTP membership algorithm. This
protocol has been widely studied. For the first
time, the protocol is automatically proved to
be correct for \(1\)~fault and \(N\)~stations,
and using abstraction we prove the correctness
for \(2\)~faults and \(N\)~stations also.}
}
@inproceedings{BFN-avis2004,
address = {Barcelona, Spain},
month = apr,
year = 2004,
editor = {Bharadwaj, Ramesh},
acronym = {{AVIS}'04},
booktitle = {{P}roceedings of the 3rd {I}nternational
{W}orkshop on {A}utomated {V}erification
of {I}nfinite-{S}tate {S}ystems
({AVIS}'04)},
author = {Bardin, S{\'e}bastien and Finkel, Alain and
Nowak, David},
title = {Toward Symbolic Verification of Programs Handling
Pointers},
nopages = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BFN-avis2004.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BFN-avis2004.ps},
abstract = {We aim at checking safety
properties on systems with pointers which are
naturally infinite state systems. In this
paper, we introduce Symbolic Memory States, a
new symbolic representation well suited to the
verification of systems with pointers. We show
SMS enjoys all the good properties needed to
check safety properties, such as closure under
union, canonicity of the representation and
decidable inclusion. We also introduce pointer
automata, a model for programs using dynamic
allocation of memory. We define the properties
we want to check in this model and we give
undecidability results. The verification part
is still work in progress.}
}
@inproceedings{DFV-avocs04,
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 = {Darlot, {\relax Ch}ristophe and Finkel, Alain and Van{~}Begin, Laurent},
title = {About {F}ast and {TReX} Accelerations},
pages = {87-103},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DFV-avocs04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DFV-avocs04.pdf},
doi = {10.1016/j.entcs.2005.04.006}
}
@misc{FAST-v1.5,
author = {Bardin, S{\'e}bastien and Darlot, {\relax Ch}ristophe and
Finkel, Alain and Leroux, J{\'e}r{\^o}me and Van{~}Begin, Laurent},
futureauthor = {Il en manque ? Plus maintenant...},
title = {{FAST}~v1.5: {F}ast {A}cceleration of {S}ymbolic
{T}ransition Systems},
year = {2004},
month = jun,
howpublished = {Available at \url{http://www.lsv.ens-cachan.fr/fast/}},
url = {http://www.lsv.ens-cachan.fr/fast/}
}
@inproceedings{FGRV-express04,
address = {London, UK},
month = apr,
year = 2005,
number = 2,
volume = 128,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Baeten, Jos and Corradini, Flavio},
acronym = {{EXPRESS}'04},
booktitle = {{P}roceedings of the 11th {I}nternational
{W}orkshop on {E}xpressiveness in
{C}oncurrency
({EXPRESS}'04)},
author = {Finkel, Alain and Geeraerts, Gilles and Raskin, Jean-Fran{\c{c}}ois and
Van{~}Begin, Laurent},
title = {On the Omega-Language Expressive Power of Extended
{P}etri Nets},
pages = {87-101},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGRV-express04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGRV-express04.pdf},
doi = {10.1016/j.entcs.2004.11.030}
}
@article{FL-IPL04,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Finkel, Alain and Leroux, J{\'e}r{\^o}me},
title = {The Convex Hull of a Regular Set of Integer Vectors is
Polyhedral and Effectively Computable},
year = {2005},
month = oct,
volume = 96,
number = 1,
pages = {30-35},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FL-ipl05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FL-ipl05.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FL-ipl05.ps},
doi = {10.1016/j.ipl.2005.04.004},
abstract = {Number Decision Diagrams (NDD)
provide a natural finite symbolic representation
for regular set of integer vectors encoded as
strings of digit vectors (least or most
significant digit first). The convex hull of the
set of vectors represented by a~NDD is proved to
be an effectively computable convex
polyhedron.}
}
@inproceedings{FL-cav04,
address = {Boston, Massachusetts, USA},
month = jul,
year = 2004,
volume = 3114,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Alur, Rajeev and Peled, Doron A.},
acronym = {{CAV}'04},
booktitle = {{P}roceedings of the 16th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'04)},
author = {Finkel, Alain and Leroux, J{\'e}r{\^o}me},
title = {Image Computation in Infinite State Model Checking},
pages = {361-371},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FL-cav04.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FL-cav04.ps}
}
@inproceedings{FL-spin04,
address = {Barcelona, Spain},
month = apr,
year = 2004,
volume = 2989,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Graf, Susanne and Mounier, Laurent},
acronym = {{SPIN}'04},
booktitle = {{P}roceedings of the 11th {I}nternational
{SPIN} {W}orkshop on {M}odel {C}hecking {S}oftware
({SPIN}'04)},
author = {Finkel, Alain and Leroux, J{\'e}r{\^o}me},
title = {Polynomial Time Image Computation With
Interval-Definable Counters Systems},
pages = {182-197},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FL-spin04.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FL-spin04.ps}
}
@article{FMP-wstsPN-icomp,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Finkel, Alain and McKenzie, Pierre and Picaronny, Claudine},
title = {A Well-Structured Framework for Analysing {P}etri Net
Extensions},
volume = {195},
number = {1-2},
pages = {1-29},
year = {2004},
month = nov,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FMP-wstsPN-icomp.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FMP-wstsPN-icomp.ps},
doi = {10.1016/j.ic.2004.01.005}
}
@inproceedings{BFLS05-atva,
address = {Taipei, Taiwan},
month = oct,
year = {2005},
volume = 3707,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Peled, Doron A. and Tsay, Yih-Kuen},
acronym = {{ATVA}'05},
booktitle = {{P}roceedings of the 3rd {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'05)},
author = {Bardin, S{\'e}bastien and Finkel, Alain and
Leroux, J{\'e}r{\^o}me and Schnoebelen, {\relax Ph}ilippe},
title = {Flat acceleration in symbolic model checking},
pages = {474-488},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFLS05-atva.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFLS05-atva.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BFLS05-atva.ps},
doi = {10.1007/11562948_35},
abstract = {Symbolic model checking provides partially
effective verification procedures that can handle systems
with an infinite state space. So-called {"}acceleration
techniques{"} enhance the convergence of fixpoint
computations by computing the transitive closure of some
transitions. In this paper we develop a new framework for
symbolic model checking with accelerations. We also propose
and analyze new symbolic algorithms using accelerations to
compute reachability sets.}
}
@article{CF-icomp05,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {C{\'e}c{\'e}, G{\'e}rard and Finkel, Alain},
title = {Verification of Programs with Half-Duplex Communication},
year = 2005,
month = nov,
volume = 202,
number = 2,
pages = {166-190},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CF-icomp05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CF-icomp05.pdf},
doi = {10.1016/j.ic.2005.05.006},
abstract = {We consider the analysis of infinite
\emph{half-duplex systems} made of finite state machines
that communicate over unbounded channels. The
half-duplex property for two machines and two
channels (one in each direction) says that each
reachable configuration has at most one channel
non-empty. We prove in this paper that such
half-duplex systems have a recognizable
reachability set. We show how to compute, in
polynomial time, a symbolic representation of this
reachability set and how to use that description to
solve several verification problems. Furthermore,
though the model of communicating finite state
machines is Turing-powerful, we prove that
membership of the class of half-duplex systems is
decidable. Unfortunately, the natural
generalization to systems with more than two
machines is Turing-powerful. We also prove that the
model-checking of those systems against PLTL
(Propositional Linear Temporal Logic) or CTL
(Computational Tree Logic) is undecidable. Finally,
we show how to apply the previous decidability
results to the Regular Model Checking. We propose a
new symbolic reachability semi-algorithm with
accelerations which successfully terminates on
half-duplex systems of two machines and some
interesting non-half-duplex systems.}
}
@techreport{FGRV-ulb05,
author = {Finkel, Alain and Geeraerts, Gilles and Raskin, Jean-Fran{\c{c}}ois and
Van{~}Begin, Laurent},
title = {A counter-example the the minimal coverability tree algorithm},
institution = {Universit\'e Libre de Bruxelles, Belgium},
year = {2005},
number = {535},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FGRV-ulb05.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FGRV-ulb05.pdf},
abstract = {In [Finkel, 1993], an~algorithm to compute a minimal
coverability tree for Petri nets has been presented. This document
demonstrates, thanks to a simple counter-example, that this algorithm may
compute an under-approximation of a coverability tree, i.e., a~tree whose
set of nodes is not sufficient to cover all the reachable markings.}
}
@inproceedings{BFLS-avis06,
address = {Vienna, Austria},
month = apr,
year = 2006,
editor = {Bharadwaj, Ramesh},
acronym = {{AVIS}'06},
booktitle = {{P}roceedings of the 5th {I}nternational
{W}orkshop on {A}utomated {V}erification
of {I}nfinite-{S}tate {S}ystems
({AVIS}'06)},
author = {Bardin, S{\'e}bastien and Finkel, Alain and Lozes, {\'E}tienne
and Sangnier, Arnaud},
title = {From Pointer Systems to Counter Systems Using Shape Analysis},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFLS-AVIS-06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFLS-AVIS-06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BFLS-AVIS-06.ps},
abstract = {We aim at checking safety properties on systems
manipulating dynamic linked lists. First we prove that every
pointer system is bisimilar to an effectively constructible
counter system. We then deduce a two-step analysis procedure.
We first build an over-approximation of the reachability set
of the pointer system. If this over-approximation is too
coarse to conclude, we then extract from it a bisimilar
counter system which is analyzed via efficient symbolic
techniques developed for general counter systems.}
}
@inproceedings{DDFG-atva06,
address = {Beijing, China},
month = oct,
year = {2006},
volume = 4218,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Graf, Susanne and Zhang, Wenhui},
acronym = {{ATVA}'06},
booktitle = {{P}roceedings of the 4th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'06)},
author = {Demri, St{\'e}phane and Finkel, Alain
and Goranko, Valentin and van Drimmelen, Govert},
title = {Towards a model-checker for counter systems},
pages = {493-507},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDFG-atva06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDFG-atva06.pdf},
doi = {10.1007/11901914_36},
abstract = {This paper deals with model-checking of fragments and extensions
of~\(\mathrm{CTL}^{*}\) on infinite-state Presburger counter systems, where
the states are vectors of integers and the transitions are determined by means
of relations definable within Presburger arithmetic. We have identified a
natural class of admissible counter systems~(ACS) for which we show that the
quantification over paths in~\(\mathrm{CTL}^{*}\) can be simulated by
quantification over tuples of natural numbers, eventually allowing translation
of the whole Presburger-\(\mathrm{CTL}^{*}\) into Presburger arithmetic,
thereby enabling effective model checking. We have provided evidence that our
results are close to optimal with respect to the class of counter systems
described above. Finally, we design a complete semi-algorithm to verify
first-order~\(\mathrm{LTL}\) properties over trace-flattable counter systems,
extending the previous underlying FAST semi-algorithm to verify reachability
questions over flattable counter systems. }
}
@article{FGRV-tcs05,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Finkel, Alain and Geeraerts, Gilles and Raskin, Jean-Fran{\c{c}}ois and
Van{~}Begin, Laurent},
title = {On the \(\omega\)-Language Expressive Power of Extended
{P}etri Nets},
year = 2006,
month = may,
volume = 356,
number = 3,
pages = {374-386},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGRV-TCS04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGRV-TCS04.pdf},
doi = {10.1016/j.tcs.2006.02.008},
abstract = {In this paper, we study the expressive power of several
monotonic extensions of Petri
nets. We compare the expressive power of Petri nets, Petri nets extended
with \emph{non-blocking arcs} and Petri nets extended with \emph{transfer arcs},
in terms of \(\omega\)-languages.
We show that the hierarchy of expressive powers of those models is strict. To prove
these results, we propose \emph{original techniques} that rely on
well-quasi orderings and monotonicity properties.}
}
@inproceedings{FLS-ilc07,
address = {Cape Town, South Africa},
month = oct,
year = 2009,
volume = 5489,
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer-Verlag},
editor = {Archibald, Margaret and Brattka, Vasco and
Goranko, Valentin and L{\"o}we, Benedikt},
acronym = {{ILC}'07},
booktitle = {{R}evised {S}elected {P}apers of the
{I}nternational {C}onference on {I}nfinity
in {L}ogic {\&} {C}omputation ({ILC}'07)},
author = {Finkel, Alain and Lozes, {\'E}tienne and Sangnier, Arnaud},
title = {Towards Model Checking Pointer Systems},
pages = {56-82},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FLS-ilc07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FLS-ilc07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FLS-ilc07.ps},
doi = {10.1007/978-3-642-03092-5_6},
abstract = {We aim at checking safety and temporal properties over models
representing the behavior of programs manipulating dynamic singly-linked
lists. The properties we consider not only allow to perform a classical
shape analysis, but we also want to check quantitative aspect on the
manipulated memory heap. We first explain how a translation of programs
into counter systems can be used to check safety problems and temporal
properties. We then study the decidability of these two problems
considering some restricted classes of programs, namely flat programs
without destructive update. We obtain the following results: (1)~the
model-checking problem is decidable if the considered program works over
acyclic lists; (2)~the safety problem is decidable for programs without
alias test. We finally explain the limit of our decidability results,
showing that relaxing one of the hypothesis leads to undecidability
results.}
}
@inproceedings{EF-infinity07,
optaddress = {Lisbon, Portugal},
month = jul,
year = 2009,
volume = 239,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
realeditor = {Madhusudan, P. and Kahlon, Vineet},
editor = {Habermehl, Peter and Vojnar, Tom{\'a}{\v{s}}},
acronym = {{INFINITY}'06,'07,'08},
booktitle = {{J}oint {P}roceedings of the 8th, 9th and 10th {I}nternational
{W}orkshops on {V}erification of {I}nfinite
{S}tate {S}ystems
({INFINITY}'06,'07,'08)},
author = {Encrenaz, Emmanuelle and Finkel, Alain},
title = {Automatic verification of counter systems with ranking functions},
pages = {85-103},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EF-infinity07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EF-infinity07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/EF-infinity07.ps},
doi = {10.1016/j.entcs.2009.05.032},
abstract = {The verification of final termination for counter systems is
undecidable. For non flattable counter systems, the verification of this
type of property is generally based on the exhibition of a ranking
function. Proving the existence of a ranking function for general counter
systems is also undecidable. We~provide a framework in which the
verification whether a given function is a ranking function is decidable.
This framework is applicable to convex counter systems which admit a
Presburger or a LPDS ranking function. This extends the results of
[A.~Bradley, Z.~Manna, and B.~Sipma. \textit{Termination analysis of
integer linear loops}. In~CONCUR'05, LNCS~3653, p.~488-502. Springer].
From this framework, we derive a model-checking algorithm to verify
whether a final termination property is satisfied or not. This approach
has been successfully applied to the verification of a parametric version
of the ZCSP protocol.}
}
@inproceedings{AF-icme-08,
address = {Monterrey, Mexico},
month = jul,
year = 2008,
acronym = {{ICME}'08},
booktitle = {Proceedings of the 11th {I}nternational {C}ongress on
Mathematical Education ({ICME}'08)},
author = {Arnoux, Pierre and Finkel, Alain},
title = {Using mental imagery processes for teaching\slash searching
in mathematics and computer science},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AF-icme08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AF-icme08.pdf},
abstract = {The role of mental representations in mathematics and computer
sciences (for teaching or searching) is often downplayed or even completely
ignored. Using an ongoing work on the subject, we argue for a more systematic
study and use of mental representations, to get an intuition of mathematical
concepts, and also to understand and build proofs. We give several examples.}
}
@inproceedings{BFS-infinity08,
optaddress = {Toronto, Canada},
month = jul,
year = 2009,
volume = 239,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Habermehl, Peter and Vojnar, Tom{\'a}{\v{s}}},
acronym = {{INFINITY}'06,'07,'08},
booktitle = {{J}oint {P}roceedings of the 8th, 9th and 10th {I}nternational
{W}orkshops on {V}erification of {I}nfinite
{S}tate {S}ystems
({INFINITY}'06,'07,'08)},
author = {Bouchy, Florent and Finkel, Alain and Sangnier, Arnaud},
title = {Reachability in Timed Counter Systems},
pages = {167-178},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFS-infinity08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFS-infinity08.pdf},
doi = {10.1016/j.entcs.2009.05.038},
abstract = {We introduce Timed Counter Systems, a~new class of systems
mixing clocks and counters. Such systems have an infinite state space,
hence their reachability problems are undecidable. By~abstracting clock
values with a Region Graph, we~show the Counter Reachability Problem to be
decidable for three subclasses: Timed~VASS, Bounded Timed Counter Systems,
and Reversal-Bounded Timed Counter Systems.}
}
@inproceedings{FS-mfcs08,
address = {Toru{\'n}, Poland},
month = aug,
year = 2008,
volume = {5162},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ochma{\'n}ski, Edward and Tyszkiewicz, Jerzy},
acronym = {{MFCS}'08},
booktitle = {{P}roceedings of the 33rd
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'08)},
author = {Finkel, Alain and Sangnier, Arnaud},
title = {Reversal-bounded Counter Machines Revisited},
pages = {323-334},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-mfcs08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-mfcs08.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FS-mfcs08.ps},
doi = {10.1007/978-3-540-85238-4_26},
abstract = {We~extend the class of reversal-bounded counter machines by
authorizing a finite number of alternations between increasing and
decreasing mode over a given bound. We~prove that extended
reversal-bounded counter machines also have effective semi-linear
reachability sets. We~also prove that the property of being
reversal-bounded is undecidable in general even when we fix the bound,
whereas this problem becomes decidable when considering Vector Addition
System with States.}
}
@techreport{LSV:08:08,
author = {Finkel, Alain and Leroux, J{\'e}r{\^o}me},
title = {Presburger Functions are Piecewise Linear},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = 2008,
month = mar,
type = {Research Report},
number = {LSV-08-08},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-08.pdf},
note = {9~pages},
abstract = {In this paper we geometrically characterize sets and functions
definable in the first order additive theory of the reals and the
integers, a decidable extension of the Presburger arithmetic combining
both integral and real variables. We introduce the notion of polinear
sets, an extension of the linear sets that characterizes these sets and we
prove that a function is definable in this logic if and only if it is
piecewise rational linear.}
}
@inproceedings{BFL-time08,
address = {Montr{\'e}al, Canada},
month = jun,
year = 2008,
publisher = {{IEEE} Computer Society Press},
noeditor = {Demri, St{\'e}phane and Jensen, {\relax Ch}ristian S.},
acronym = {{TIME}'08},
booktitle = {{P}roceedings of the 15th {I}nternational {S}ymposium on
{T}emporal {R}epresentation and {R}easoning
({TIME}'08)},
author = {Bouchy, Florent and Finkel, Alain and Leroux, J{\'e}r{\^o}me},
title = {Decomposition of Decidable First-Order Logics over Integers
and Reals},
pages = {147-155},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFL-time08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFL-time08.pdf},
doi = {10.1109/TIME.2008.22},
abstract = {We tackle the issue of representing infinite sets of realvalued
vectors. This paper introduces an operator for combining
integer and real sets. Using this operator, we~decompose
three well-known logics extending Presburger with reals. Our
decomposition splits the logic into two parts: one~integer,
and one decimal (\textit{i.e.},~on the interval~\([0,1[\)).
We~also give some basis for an implementation of our
representation.}
}
@article{BFLP-sttt08,
publisher = {Springer},
journal = {International Journal on Software Tools
for Technology Transfer},
author = {Bardin, S{\'e}bastien and Finkel, Alain and
Leroux, J{\'e}r{\^o}me and Petrucci, Laure},
title = {{FAST}: Acceleration from theory to practice},
year = 2008,
month = oct,
volume = 10,
number = 5,
pages = {401-424},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-16.pdf},
doi = {10.1007/s10009-008-0064-3},
abstract = {Fast acceleration of symbolic transition
systems~(\textsc{Fast}) is a tool for the
analysis of systems manipulating unbounded integer variables. We~check
safety properties by
computing the reachability set of the system under study. Even if this
reachability set is not
necessarily recursive, we~use innovative techniques, namely symbolic
representation, acceleration and circuit selection, to~increase
convergence. \textsc{Fast} has proved to perform very well on case
studies. This~paper describes the tool, from the underlying theory to
the architecture choices. Finally, \textsc{Fast} capabilities are
compared with those of other tools. A~range of case studies from the
literature is investigated.}
}
@inproceedings{FS-sofsem10,
address = {\v{S}pindler\r{u}v Ml\'{y}n, Czech Republic},
month = jan,
year = 2010,
volume = 5901,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Peleg, David and Muscholl, Anca},
acronym = {{SOFSEM}'10},
booktitle = {{P}roceedings of the 36th International Conference on
Current Trends in Theory and Practice of
Computer Science ({SOFSEM}'10)},
author = {Finkel, Alain and Sangnier, Arnaud},
title = {Mixing coverability and reachability to analyze {VASS}
with one zero-test},
pages = {394-406},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-sofsem10.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-sofsem10.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FS-sofsem10.ps},
doi = {10.1007/978-3-642-11266-9_33},
abstract = {We study Vector Addition Systems with States (VASS) extended in
such a way that one of the manipulated integer variables can be tested to
zero. For this class of system, it has been proved that the reachability
problem is decidable. We prove here that boundedness, termination and
reversal-boundedness are decidable for VASS with one zero-test. To decide
reversal-boundedness, we provide an original method which mixes both the
construction of the coverability graph for VASS and the computation of the
reachability set of reversal-bounded counter machines. The same
construction can be slightly adapted to decide boundedness and hence
termination.}
}
@inproceedings{BFSP-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 = {Bouchy, Florent and Finkel, Alain and San{ }Pietro, Pierluigi},
title = {Dense-choice Counter Machines Revisited},
pages = {3-22},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFSP-infinity09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFSP-infinity09.pdf},
doi = {10.4204/EPTCS.10.1},
abstract = {This paper clarifies the picture about Dense-choice Counter
Machines, which have been less studied than (discrete) Counter Machines.
We revisit the definition of {"}Dense Counter Machines{"} so that it now
extends (discrete) Counter Machines, and we provide new undecidability and
decidability results. Using the first-order additive mixed theory of reals
and integers, we give a logical characterization of the sets of
configurations reachable by reversal-bounded Dense-choice Counter
Machines.}
}
@inproceedings{FGL-icalp09,
address = {Rhodes, Greece},
month = jul,
year = 2009,
volume = 5556,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Albers, Susanne and Marchetti-Spaccamela, Alberto and
Matias, Yossi and Thomas, Wolfgang},
acronym = {{ICALP}'09},
booktitle = {{P}roceedings of the 36th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'09)},
author = {Finkel, Alain and Goubault{-}Larrecq, Jean},
title = {Forward Analysis for {WSTS}, Part~{II}: Complete {WSTS}},
pages = {188-199},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGL-icalp09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGL-icalp09.pdf},
doi = {10.1007/978-3-642-02930-1_16},
abstract = {We~describe a simple, conceptual forward analysis procedure for
\(\infty\)-complete WSTS~\(\mathcal{S}\). This computes the \emph{clover}
of a state~\(s_0\) , \textit{i.e.}, a~finite description of the closure of
the cover of~\(s_0\) . When \(S\) is the completion of a
WSTS~\(\mathcal{X}\), the clover in~\(\mathcal{S}\) is a finite
description of the cover in~\(\mathcal{X}\). We~show that this applies
exactly when \(\mathcal{X}\) is an \(\omega^2\)-WSTS, a~new robust class
of WSTS. We~show that our procedure terminates in more cases than the
generalized Karp-Miller procedure on extensions of Petri nets. We
characterize the WSTS where our procedure terminates as those that are
\emph{clover-flattable}. Finally, we~apply this to well-structured counter
systems.}
}
@inproceedings{FGL-stacs2009,
address = {Freiburg, Germany},
month = feb,
year = 2009,
volume = 3,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Albers, Susanne and Marion, Jean-Yves},
acronym = {{STACS}'09},
booktitle = {{P}roceedings of the 26th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'09)},
author = {Finkel, Alain and Goubault{-}Larrecq, Jean},
title = {Forward Analysis for~{WSTS}, Part~{I}: Completions},
pages = {433-444},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGL-stacs2009.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGL-stacs2009.pdf},
abstract = {Well-structured transition systems provide the right foundation
to compute a finite basis of the set of predecessors of the upward closure
of a state. The~dual problem, to compute a finite representation of the
set of successors of the downward closure of a state, is~harder: Until
now, the theoretical framework for manipulating downward-closed sets was
missing. We~answer this problem, using insights from domain theory (dcpos
and ideal completions), from topology (sobrifications), and shed new light
on the notion of adequate domains of limits.}
}
@techreport{rr-lsv-10-23,
author = {Bonnet, R{\'e}mi and Finkel, Alain and Haddad, Serge and
Rosa{-}Velardo, Fernando},
title = {Comparing Petri Data Nets and Timed Petri Nets},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2010},
month = dec,
type = {Research Report},
number = {LSV-10-23},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-23.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-23.pdf},
note = {16~pages},
abstract = {Well-Structured Transitions Systems (WSTS) constitute a generic
class of infinite-state systems for which several properties like
coverability remain decidable. The family of coverability languages that
they generate is an appropriate criterium for measuring their
expressiveness. Here we establish that Petri Data nets (PDNs) and Timed
Petri nets (TdPNs), two powerful classes of WSTS are equivalent w.r.t this
criterium.}
}
@inproceedings{BFLZ-fsttcs10,
address = {Chennai, India},
month = dec,
year = 2010,
volume = 8,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Lodaya, Kamal and Mahajan, Meena},
acronym = {{FSTTCS}'10},
booktitle = {{P}roceedings of the 30th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'10)},
author = {Bonnet, R{\'e}mi and Finkel, Alain and Leroux, J{\'e}r{\^o}me
and Zeitoun, Marc},
title = {Place-Boundedness for Vector Addition Systems with one zero-test},
pages = {192-203},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLZ-fsttcs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLZ-fsttcs10.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2010.192},
abstract = {Reachability and boundedness problems have been shown decidable
for Vector Addition Systems with one zero-test. Surprisingly,
place-boundedness remained open. We provide here a variation of the
Karp-Miller algorithm to compute a basis of the downward closure of the
reachability set which allows to decide place-boundedness. This forward
algorithm is able to pass the zero-tests thanks to a finer cover, hybrid
between the reachability and cover sets, reclaiming accuracy on one
component. We show that this filtered cover is still recursive, but that
equality of two such filtered covers, even for usual Vector Addition
Systems (with no zero-test), is undecidable.}
}
@article{AF-ijmest10,
publisher = {Taylor \& Francis},
journal = {International Journal of Mathematical Education
in Science and Technology},
author = {Arnoux, Pierre and Finkel, Alain},
title = {Using mental imagery processes for teaching and research in
mathematics and computer science},
volume = 41,
number = 2,
month = jan,
year = 2010,
pages = {229-242},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AF-ijmest10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AF-ijmest10.pdf},
doi = {10.1080/00207390903372429},
abstract = {The role of mental representations in mathematics and computer
science (for teaching or research) is often downplayed or even completely
ignored. Using an ongoing work on the subject, we argue for a more
systematic study and use of mental representations, to get an intuition of
mathematical concepts, and also to understand and build proofs. We give
two detailed examples.}
}
@inproceedings{SBF-cnsfp11,
address = {Metz, France},
month = sep,
year = 2011,
acronym = {{SFP}'11},
booktitle = {{A}ctes du 53{\`e}me {C}ongr{\`e}s {N}ational de la {S}oci{\'e}t{\'e} {F}ran{\c{c}}aise
de {P}sychologie ({SFP}'11)},
author = {Saint{~}Bauzel, Roxanne and Finkel, Alain},
title = {Se repr{\'e}senter pour mieux apprendre: les repr{\'e}sentations mentales
comme outils didactiques favorisant la transmission du savoir},
pages = {171-173},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SBF-cnsfp11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SBF-cnsfp11.pdf}
}
@article{FG-lmcs12,
journal = {Logical Methods in Computer Science},
author = {Finkel, Alain and Goubault{-}Larrecq, Jean},
title = {Forward Analysis for {WSTS}, Part~{II}: Complete {WSTS}},
year = 2012,
month = sep,
volume = 8,
number = {3:28},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FG-lmcs12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FG-lmcs12.pdf},
doi = {10.2168/LMCS-8(3:28)2012},
abstract = {We describe a simple, conceptual forward analysis procedure for
\(\infty\)-complete WSTS~\(\mathfrak{S}\). This computes the so-called
\emph{clover} of a state. When \(\mathfrak{S}\) is the completion of a
WSTS~\(\mathfrak{X}\), the clover in~\(\mathfrak{S}\) is a finite
description of the downward closure of the reachability set. We show
that such completions are infinity-complete exactly when
\(\mathfrak{X}\) is an \(\omega^2\)-WSTS, a~new robust class of WSTS.
We show that our procedure terminates in more cases than the
generalized Karp-Miller procedure on extensions of Petri nets and on
lossy channel systems. We characterize the WSTS where our procedure
terminates as those that are \emph{clover-flattable}. Finally, we
apply this to well-structured counter systems.}
}
@inproceedings{CFM-ncma11,
address = {Milano, Italy},
month = jul,
year = 2011,
volume = 282,
series = {books@ocg.at},
publisher = {Austrian Computer Society},
editor = {Freund, Rudolf and Holzer, Markus and Mereghetti, Carlo
and Otto, Friedrich and Palano, Beatrice},
acronym = {{NCMA}'11},
booktitle = {{P}roceedings of the 3rd {W}orkshop on {N}on-{C}lassical {M}odels
of {A}utomata and {A}pplications ({NCMA}'11)},
author = {Cadilhac, Micha{\"e}l and Finkel, Alain and McKenzie, Pierre},
title = {On the Expressiveness of {P}arikh Automata and Related Models},
pages = {103-119},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-ncma11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-ncma11.pdf},
doi = {}
}
@inproceedings{CFM-words11,
address = {Prague, Czech Republic},
month = sep,
year = 2011,
volume = {63},
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Ambro{\v{z}}, Petr and Holub, {\v{S}}t{\v{e}}p{\'a}n and
Mas{\'a}kov{\'a}, Zuzana},
acronym = {{WORDS}'11},
booktitle = {{P}roceedings of the 8th {I}nternational {C}onference {WORDS} ({WORDS}'11)},
author = {Cadilhac, Micha{\"e}l and Finkel, Alain and McKenzie, Pierre},
title = {Bounded {P}arikh Automata},
pages = {93-102},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-words11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-words11.pdf},
doi = {10.4204/EPTCS.63.13}
}
@inproceedings{CFS-atpn2011,
address = {Newcastle upon Tyne, UK},
month = jun,
year = 2011,
volume = {6709},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Kristensen, Lars M. and Petrucci, Laure},
acronym = {{PETRI~NETS}'11},
booktitle = {{P}roceedings of the 32nd
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({PETRI~NETS}'11)},
author = {Chambart, Pierre and Finkel, Alain and Schmitz, Sylvain},
title = {Forward Analysis and Model Checking for Trace Bounded {WSTS}},
nopages = {49-68},
url = {http://arxiv.org/abs/1004.2802},
doi = {10.1007/978-3-642-21834-7_4},
abstract = {We investigate a subclass of well-structured transition
systems~(WSTS), the bounded---in the sense of Ginsburg and Spanier (Trans.
AMS 1964)---complete deterministic ones, which we claim provide an
adequate basis for the study of forward analyses as developed by Finkel
and Goubault-Larrecq (ICALP~2009). Indeed, we prove that, unlike other
conditions considered previously for the termination of forward analysis,
boundedness is decidable. Boundedness turns out to be a valuable
restriction for WSTS verification, as we show that it further allows to
decide all \(\omega\)-regular properties on the set of infinite traces of
the system.}
}
@article{DFGD-jancl10,
publisher = {Taylor \& Francis},
journal = {Journal of Applied Non-Classical Logics},
author = {Demri, St{\'e}phane and Finkel, Alain and Goranko, Valentin
and van Drimmelen, Govert},
title = {Model-checking \(\textsf{CTL}^{*}\) over Flat {P}resburger Counter
Systems},
year = {2010},
volume = {20},
number = {4},
pages = {313-344},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DFGD-jancl10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DFGD-jancl10.pdf},
doi = {10.3166/jancl.20.313-344},
abstract = {This paper studies model-checking of fragments and extensions of
\(\textsf{CTL}^{*}\) on infinite-state counter systems, where the states
are vectors of integers and the transitions are determined by means of
relations definable within Presburger arithmetic. In general, reachability
properties of counter systems are undecidable, but we have identified a
natural class of admissible counter systems (ACS) for which we show that
the quantification over paths in \(\textsf{CTL}^{*}\) can be simulated by
quantification over tuples of natural numbers, eventually allowing
translation of the whole Presburger-\(\textsf{CTL}^{*}\) into Presburger
arithmetic, thereby enabling effective model checking. We provide evidence
that our results are close to optimal with respect to the class of counter
systems described above.}
}
@inproceedings{BFHR-fossacs11,
address = {Saarbr{\"u}cken, Germany},
month = mar # {-} # apr,
year = 2011,
volume = {6604},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Hofmann, Martin},
acronym = {{FoSSaCS}'11},
booktitle = {{P}roceedings of the 14th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'11)},
author = {Bonnet, R{\'e}mi and Finkel, Alain and Haddad, Serge and
Rosa{-}Velardo, Fernando},
title = {Ordinal Theory for Expressiveness of Well Structured Transition Systems},
pages = {153-167},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHR-fossacs11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHR-fossacs11.pdf},
doi = {10.1007/978-3-642-19805-2_11}
}
@article{BFHR-icomp13,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Bonnet, R{\'e}mi and Finkel, Alain and Haddad, Serge and
Rosa{-}Velardo, Fernando},
title = {Ordinal Theory for Expressiveness of Well-Structured
Transition Systems},
year = 2013,
month = mar,
volume = 224,
pages = {1-22},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHR-icomp12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHR-icomp12.pdf},
doi = {10.1016/j.ic.2012.11.003},
abstract = {We characterize the importance of resources (like counters,
channels, or alphabets) when measuring the expressiveness of
Well-Structured Transition Systems~(WSTS). We establish, for usual classes
of well partial orders, the equivalence between the existence of order
reflections (non-monotonic order embeddings) and the simulations with
respect to coverability languages. We show that the non-existence of order
reflections can be proved by the computation of order types. This allows
us to extend the current classification of WSTS, in particular solving
some open problems, and to unify the existing proofs.}
}
@article{CFM-ijfcs12,
publisher = {World Scientific},
journal = {International Journal of Foundations of Computer Science},
author = {Cadilhac, Micha{\"e}l and Finkel, Alain and McKenzie, Pierre},
title = {Bounded {P}arikh automata},
year = 2012,
month = dec,
volume = {23},
number = {8},
pages = {1691-1710},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-ijfcs12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-ijfcs12.pdf},
doi = {10.1142/S0129054112400709},
abstract = {The Parikh finite word automaton model~(PA) was introduced and
studied by Klaedtke and Rue{\ss}. Here, we present some expressiveness
properties of a restriction of the deterministic affine PA recently
introduced, and use them as a tool to show that the bounded languages
recognized by PA are the same as those recognized by deterministic PA.
Moreover, this class of languages is shown equal to the class of bounded
languages with a semilinear iteration set.}
}
@article{CFM-rairo12,
address = {Les Ulis, France},
publisher = {EDP Sciences},
journal = {RAIRO Informatique Th{\'e}orique et Applications},
author = {Cadilhac, Micha{\"e}l and Finkel, Alain and McKenzie, Pierre},
title = {Affine {P}arikh automata},
year = 2012,
month = oct,
volume = 46,
number = 4,
pages = {511-545},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-rairo12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-rairo12.pdf},
doi = {10.1051/ita/2012013},
abstract = {The Parikh finite word automaton (PA) was introduced and studied
in 2003 by Klaedtke and Rue\ss. Natural variants of the PA arise from
viewing a PA equivalently as an automaton that keeps a count of its
transitions and semilinearly constrains their numbers. Here we adopt this
view and define the affine PA, that extends the PA by having each
transition induce an affine transformation on the PA registers, and the PA
on letters, that restricts the PA by forcing any two transitions on the
same letter to affect the registers equally. Then we report on the
expressiveness, closure, and decidability properties of such PA variants.
We note that deterministic PA are strictly weaker than deterministic
reversal-bounded counter machines.}
}
@inproceedings{CFM-dlt12,
address = {Taipei, Taiwan},
month = aug,
year = 2012,
volume = 7410,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Yen, Hsu-Chun and Ibarra, Oscar H.},
acronym = {{DLT}'12},
booktitle = {{P}roceedings of the 16th {I}nternational
{C}onference on {D}evelopments in {L}anguage {T}heory
({DLT}'12)},
author = {Cadilhac, Micha{\"e}l and Finkel, Alain and McKenzie, Pierre},
title = {Unambiguous Constrained Automata},
pages = {239-250},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-dlt12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-dlt12.pdf},
doi = {10.1007/978-3-642-31653-1_22},
abstract = {The class of languages captured by Constrained Automata~(CA)
that are unambiguous is shown to possess more closure properties than the
provably weaker class captured by deterministic~CA. Problems decidable for
deterministic CA are nonetheless shown to remain decidable for unambiguous
CA, and testing for \emph{regularity} is added to this set of decidable
problems. Unambiguous CA are then shown incomparable with deterministic
reversal-bounded machines in terms of expressivity, and a
\emph{deterministic} model equivalent to unambiguous CA is identified.}
}
@inproceedings{SBF-cnsfp12,
address = {Montpellier, France},
month = sep,
year = 2012,
acronym = {{SFP}'12},
booktitle = {{A}ctes du 54{\`e}me {C}ongr{\`e}s {N}ational de la
{S}oci{\'e}t{\'e} {F}ran{\c{c}}aise de {P}sychologie ({SFP}'12)},
author = {Saint{~}Bauzel, Roxanne and Finkel, Alain},
title = {Qu'est-ce qu'une repr{\'e}sentation efficace pour favoriser les
apprentissages~?},
pages = {89-91},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SBF-cnsfp12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SBF-cnsfp12.pdf}
}
@inproceedings{FGL-pn12,
address = {Hamburg, Germany},
month = jun,
year = 2012,
volume = 7347,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Haddad, Serge and Pomello, Lucia},
acronym = {{PETRI~NETS}'12},
booktitle = {{P}roceedings of the 33rd
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({PETRI~NETS}'12)},
author = {Finkel, Alain and Goubault{-}Larrecq, Jean},
title = {The~Theory of~{WSTS}: The~Case of Complete~{WSTS}},
pages = {3-31},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FGL-atpn12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FGL-atpn12.pdf},
doi = {10.1007/978-3-642-31131-4_2},
abstract = {We describe a simple, conceptual forward analysis procedure for
\(\infty\)-complete WSTS~\(\mathfrak{S}\). This computes the so-called
\emph{clover} of a state. When \(\mathfrak{S}\) is the completion of a
WSTS~\(\mathfrak{X}\), the clover in~\(\mathfrak{S}\) is a finite
description of the downward closure of the reachability set. We show that
such completions are \(\infty\)-complete exactly when \(\mathfrak{X}\) is
an \emph{\(\omega^{2}\)-WSTS}, a new robust class of WSTS. We show that
our procedure terminates in more cases than the generalized Karp-Miller
procedure on extensions of Petri nets. We characterize the WSTS where our
procedure terminates as those that are \emph{clover-flattable}. Finally,
we apply this to well-structured Presburger counter systems.}
}
@inproceedings{BFP-fsttcs12,
address = {Hyderabad, India},
month = dec,
year = 2012,
volume = 18,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
acronym = {{FSTTCS}'12},
booktitle = {{P}roceedings of the 32nd {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'12)},
author = {Bonnet, R{\'e}mi and Finkel, Alain and Praveen, M.},
title = {Extending the {R}ackoff technique to affine nets},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFP-fsttcs12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFP-fsttcs12.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2012.301},
abstract = {We study the possibility of extending the Rackoff
technique to Affine nets, which are Petri nets
extended with affine functions. The Rackoff
technique has been used for establishing \textsc{Expspace}
upper bounds for the coverability and boundedness
problems for Petri nets. We show that this technique
can be extended to strongly increasing Affine nets,
obtaining better upper bounds compared to known
results. The possible copies between places of a
strongly increasing Affine net make this extension
non-trivial. One cannot expect similar results for
the entire class of Affine nets since coverability
is Ackermann-hard and boundedness is
undecidable. Moreover, it can be proved that model
checking a logic expressing generalized coverability
properties is undecidable for strongly increasing
Affine nets, while it is known to be
\textsc{Expspace}-complete for Petri nets.}
}
@article{BFLZ-lmcs12,
journal = {Logical Methods in Computer Science},
author = {Bonnet, R{\'e}mi and Finkel, Alain and Leroux, J{\'e}r{\^o}me and
Zeitoun, Marc},
title = {Model Checking Vector Addition Systems with one zero-test},
year = 2012,
volume = {8},
number = {2:11},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLZ-lmcs12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLZ-lmcs12.pdf},
doi = {10.2168/LMCS-8(2:11)2012},
abstract = {We design a variation of the Karp-Miller algorithm to compute,
in a forward manner, a finite representation of the cover (i.e., the
downward closure of the reachability set) of a vector addition system with
one zero-test. This algorithm yields decision procedures for several
problems for these systems, open until now, such as place-boundedness or
LTL model-checking. The proof techniques to handle the zero-test are based
on two new notions of cover: the refined and the filtered cover. The
refined cover is a hybrid between the reachability set and the classical
cover. It inherits properties of the reachability set: equality of two
refined covers is undecidable, even for usual Vector Addition Systems
(with no zero-test), but the refined cover of a Vector Addition System is
a recursive set. The second notion of cover, called the filtered cover, is
the central tool of our algorithms. It inherits properties of the
classical cover, and in particular, one can effectively compute a finite
representation of this set, even for Vector Addition Systems with one
zero-test.}
}
@inproceedings{FGH-mfcs13,
address = {Klosterneuburg, Austria},
month = aug,
year = 2013,
volume = {8087},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Chatterjee, Krishnendu and Sgall, Ji{\v{r}}{\'\i}},
acronym = {{MFCS}'13},
booktitle = {{P}roceedings of the 38th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'13)},
author = {Finkel, Alain and G{\"o}ller, Stefan and Haase, Christoph},
title = {Reachability in Register Machines with Polynomial Updates},
pages = {409-420},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FGH-mfcs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FGH-mfcs13.pdf},
ps = {FGH-mfcs13.ps},
doi = {10.1007/978-3-642-40313-2_37},
abstract = {This paper introduces a class of register machines whose
registers can be updated by polynomial functions when a transition is
taken, and the domain of the registers can be constrained by linear
constraints. This model strictly generalises a variety of known formalisms
such as various classes of Vector Addition Systems with States. Our main
result is that reachability in our class is PSPACE-complete when
restricted to one register. We moreover give a classification of the
complexity of reachability according to the type of polynomials allowed
and the geometry induced by the range-constraining formula.}
}
@misc{reachard-18,
author = {Finkel, Alain},
title = {REACHARD~-- Compte-rendu interm{\'e}diaire},
month = mar,
year = {2013},
note = {9~pages},
type = {Contract Report},
howpublished = {Deliverable~D2 Reachard (ANR-11-BS02-001)}
}
@misc{reachard-30,
author = {Finkel, Alain},
title = {REACHARD~-- Compte-rendu interm{\'e}diaire},
month = feb,
year = {2014},
note = {18~pages},
type = {Contract Report},
howpublished = {Deliverable~D3 Reachard (ANR-11-BS02-001)}
}
@article{FL-sosym14,
publisher = {Springer},
journal = {Software~\& System Modeling},
author = {Finkel, Alain and Leroux, J{\'e}r{\^o}me},
title = {Recent and simple algorithms for {P}etri nets},
volume = 14,
number = 2,
year = {2015},
month = may,
pages = {719-725},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FL-sosym14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FL-sosym14.pdf},
doi = {10.1007/s10270-014-0426-0},
abstract = {We show how inductive invariants can be used to solve
coverability, boundedness and reachability problems for Petri nets. This
approach provides algorithms that are conceptually simpler than previously
pblished ones.}
}
@article{FL-is14,
publisher = {Springer},
journal = {Informatik Spektrum},
author = {Finkel, Alain and Leroux, J{\'e}r{\^o}me},
title = {Neue, einfache {A}lgorithmen f{\"u}r {P}etrinetze},
volume = 37,
number = {3},
month = jun,
year = 2014,
pages = {229-236},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FL-is14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FL-is14.pdf},
doi = {10.1007/s00287-013-0753-5},
abstract = {Wir zeigen, wie die Entscheidungsprobleme der {\"U}berdeckung,
der Beschr{\"a}nktheit und der Erreichbarkeit mithilfe induktiver
Invarianten einfacher l{\"o}sbar sind als mit herk{\"o}mmlichen
Methoden}
}
@article{BFSP-tcs14,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Bouchy, Florent and Finkel, Alain and San{ }Pietro, Pierluigi},
title = {Dense-choice Counter Machines Revisited},
volume = {542},
month = jul,
year = 2014,
pages = {17-31},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFSP-tcs14.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFSP-tcs14.pdf},
doi = {10.1016/j.tcs.2014.04.029},
abstract = {This paper clarifies the picture about Dense-choice
Counter Machines (DCM), a less studied version of
Counter Machines where counters range on a dense,
rather than discrete, domain. The definition of DCM
is revisited to make it extend (discrete) Counter
Machines, and new undecidability and decidability
results are proved. Using the first-order additive
mixed theory of reals and integers, the paper
presents a logical characterization of the sets of
configurations reachable by reversal-bounded DCM. We
also relate the DCM model to more common models of
systems.}
}
@inproceedings{BFM-icalp14,
address = {Copenhagen, Denmark},
month = jul,
year = 2014,
volume = 8573,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Esparza, Javier and Fraigniaud, Pierre and Koutsoupias, Elias},
acronym = {{ICALP}'14},
booktitle = {{P}roceedings of the 41st {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'14)~-- {P}art~{II}},
author = {Blondin, Michael and Finkel, Alain and McKenzie, Pierre},
title = {Handling Infinitely Branching {WSTS}},
pages = {13-25},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFM-icalp14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFM-icalp14.pdf},
doi = {10.1007/978-3-662-43951-7_2},
abstract = {Most decidability results concerning well-structured
transition systems apply to the \emph{finitely branching}
variant. Yet some models (inserting automata, \(\omega\)-Petri
nets,~...) are naturally infinitely branching. Here
we develop tools to handle infinitely branching WSTS
by exploiting the crucial property that in the
(ideal) completion of a well-quasi-ordered set,
downward-closed sets are finite unions of
ideals. Then, using these tools, we derive
decidability results and we delineate the
undecidability frontier in the case of the
termination, the control-state maintainability and
the coverability problems. Coverability and
boundedness under new effectivity conditions are
shown decidable.}
}
@article{CFM-ijfcs13,
publisher = {World Scientific},
journal = {International Journal of Foundations of Computer Science},
author = {Cadilhac, Micha{\"e}l and Finkel, Alain and McKenzie, Pierre},
title = {Unambiguous Contrained Automata},
volume = 24,
number = 7,
month = nov,
year = 2013,
pages = {1099-1116},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-ijfcs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-ijfcs13.pdf},
doi = {10.1142/S0129054113400339},
abstract = {The class of languages captured by Constrained Automata~(CA)
that are unambiguous is shown to possess more closure properties than the
provably weaker class captured by deterministic~CA. Problems decidable for
deterministic CA are nonetheless shown to remain decidable for
unambiguous~CA, and testing for regularity is added to this set of
decidable problems. Unambiguous CA~are then shown incomparable with
deterministic reversal-bounded machines in terms of expressivity, and a
deterministic model equivalent to unambiguous~CA is identified.}
}
@inproceedings{BFGHM-lics15,
address = {Kyoto, Japan},
month = jul,
year = 2015,
publisher = {{IEEE} Press},
acronym = {{LICS}'15},
booktitle = {{P}roceedings of the 30th {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'15)},
author = {Blondin, Michael and Finkel, Alain and G{\"o}ller, Stefan
and Haase, Christoph and McKenzie, Pierre},
title = {Reachability in Two-Dimensional Vector Addition
Systems with States is {PSPACE}-Complete},
pages = {32-43},
url = {http://arxiv.org/abs/1412.4259},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFGHM-lics15-long.pdf},
doi = {10.1109/LICS.2015.14},
abstract = {Determining the complexity of the reachability problem for
vector addition systems with states (VASS) is a long-standing open problem
in computer science. Long known to be decidable, the problem to this day
lacks any complexity upper bound whatsoever. In this paper, reachability
for two-dimensional VASS is shown PSPACE-complete. This improves on a
previously known doubly exponential time bound established by Howell,
Rosier, Huynh and Yen in~1986. The coverability and boundedness problems
are also noted to be PSPACE-complete. In addition, some complexity results
are given for the reachability problem in two-dimensional VASS and in
integer VASS when numbers are encoded in unary.}
}
@misc{qcover16,
author = {Blondin, Michael and Finkel, Alain and Haase, Christoph and Haddad, Serge},
title = {{QCover: an efficient coverability verifier for discrete and continuous Petri nets}},
url = {https://github.com/blondimi/qcover},
year = {2016}
}
@techreport{arxiv16-BFMK,
author = {Blondin, Michael and Finkel, Alain and McKenzie, Pierre},
title = {Well Behaved Transition Systems},
institution = {Computing Research Repository},
number = {1608.02636},
year = {2016},
month = aug,
type = {Research Report},
url = {http://arxiv.org/abs/1608.02636},
pdf = {http://arxiv.org/abs/1608.02636},
note = {18~pages},
abstract = {The well-quasi-ordering (i.e., a well-founded quasi-ordering such that all antichains are finite) that defines well-structured transition systems (WSTS) is shown not to be the weakest hypothesis that implies decidability of the coverability problem. We show coverability decidable for monotone transition systems that only require the absence of infinite antichains and call well behaved transitions systems (WBTS) the new strict superclass of the class of WSTS that arises. By contrast, we confirm that boundedness and termination are undecidable for WBTS under the usual hypotheses, and show that stronger monotonicity conditions can enforce decidability. Proofs are similar or even identical to existing proofs but the surprising message is that a hypothesis implicitely assumed minimal for twenty years in the theory of WSTS can meaningfully be relaxed, allowing more orderings to be handled in an abstract way.}
}
@article{ADFLP-fi2016,
publisher = {{IOS} Press},
journal = {Fundamenta Informaticae},
author = {Abdulla, Parosh Aziz and Demri, St{\'e}phane and Finkel, Alain and Leroux, J{\'e}r{\^o}me and Potapov, Igor},
editor = {Abdulla, Parosh Aziz and Demri, St{\'e}phane and Finkel, Alain and Leroux, J{\'e}r{\^o}me and Potapov, Igor},
number = {3--4},
title = {Selected papers of Reachability Problems Workshop 2012 (Bordeaux) and 2013 (Uppsala)},
url = {http://content.iospress.com/journals/fundamenta-informaticae/143/3-4},
volume = {143},
year = {2016}
}
@inproceedings{Finkel-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 = {Finkel, Alain},
title = {The Ideal Theory for {WSTS}},
pages = {1-22},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/Finkel-rp16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Finkel-rp16.pdf},
doi = {10.1007/978-3-319-45994-3_1},
abstract = {We begin with a survey on well structured transition systems and, in particular, we present the ideal framework [FG09a, BFM14] which was recently used to obtain new deep results on Petri nets and extensions. We argue that the theory of ideals prompts a renewal of the theory of WSTS by providing a way to define a new class of monotonic systems, the so-called Well Behaved Transition Systems, which properly contains WSTS, and for which coverability is still decidable by a forward algorithm. We then recall the completion of WSTS which leads to defining a conceptual Karp-Miller procedure that terminates in more cases than the generalized Karp-Miller procedure on extensions of Petri nets.}
}
@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.",
}}
@article{CFS-tcs16,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Chambart, Pierre and Finkel, Alain and Schmitz, Sylvain},
title = {Forward Analysis and Model Checking for Trace
Bounded~{WSTS}},
year = 2016,
volume = {637},
pages = {1-29},
month = jul,
url = {http://arxiv.org/abs/1004.2802},
doi = {10.1016/j.tcs.2016.04.020},
abstract = {We investigate a subclass of well-structured transition
systems~(WSTS), the bounded---in the sense of Ginsburg and Spanier
(Trans.~AMS, 1964)---complete deterministic ones, which we claim provide
an adequate basis for the study of forward analyses as developed by
Finkel and Goubault-Larrecq (ICALP~2009). Indeed, we prove that, unlike
other conditions considered previously for the termination of forward
analysis, boundedness is decidable. Boundedness turns out to be a
valuable restriction for WSTS verification, as we show that it further
allows to decide all {{\(\omega\)}}-regular properties on the set of infinite
traces of the system.}
}
@inproceedings{tacas16-BFHH,
address = {Eindhoven, The Netherlands},
month = apr,
year = 2016,
volume = {9636},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Chechik, Marsha and Raskin, Jean-Fran{\c{c}}ois},
acronym = {{TACAS}'16},
booktitle = {{P}roceedings of the 22th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'16)},
author = {Blondin, Michael and Finkel, Alain and Haase, Christoph and
Haddad, Serge},
title = {Approaching the Coverability Problem Continuously},
pages = {480-496},
url = {http://arxiv.org/abs/1510.05724},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/arxiv15-BFHH.pdf},
doi = {10.1007/978-3-662-49674-9_28},
abstract = {The coverability problem for Petri nets plays a central role in
the verification of concurrent shared-memory programs. However, its high
EXPSPACE-complete complexity poses a challenge when encountered in
real-world instances. In this paper, we develop a new approach to this
problem which is primarily based on applying forward coverability in
continuous Petri nets as a pruning criterion inside a backward
coverability framework. A cornerstone of our approach is the efficient
encoding of a recently developed polynomial-time algorithm for
reachability in continuous Petri nets into SMT. We demonstrate the
effectiveness of our approach on standard benchmarks from the literature,
which shows that our approach decides significantly more instances than
any existing tool and is in addition often much faster, in particular on
large instances.}
}
@article{BFM-lmcs17,
journal = {Logical Methods in Computer Science},
author = {Blondin, Michael and Finkel, Alain and McKenzie, Pierre},
title = {Well Behaved Transition Systems},
volume = {13},
number = {3},
year = {2017},
month = sep,
pages = {1-19},
doi = {10.23638/LMCS-13(3:24)2017},
url = {https://doi.org/10.23638/LMCS-13(3:24)2017}
}
@article{BFM-ic17,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Blondin, Michael and Finkel, Alain and McKenzie, Pierre},
title = {Handling Infinitely Branching Well-structured Transition Systems},
volume = {258},
year = {2018},
pages = {28--49},
doi = {10.1016/j.ic.2017.11.001}
}
@article{Finkel-pp17,
title = {L'analyse cognitive, la psychologie num{\'e}rique et la formation des enseignants {\`a} l'universit{\'e}},
author = {Finkel, Alain},
journal = {Pratiques Psychologiques},
volume = {23},
number = {3},
pages = {303-323},
year = {2017},
doi = {https://doi.org/10.1016/j.prps.2017.05.006},
url = {http://www.sciencedirect.com/science/article/pii/S126917631730055X},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Finkel-pp17.pdf}
}
@inproceedings{BFG-fsttcs17,
address = {Kanpur, India},
month = dec,
year = 2017,
volume = {93},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Satya Lokam and R. Ramanujam},
acronym = {{FSTTCS}'17},
booktitle = {{P}roceedings of the 37th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'17)},
author = {Michael Blondin and Alain Finkel and Jean Goubault{-}Larrecq},
title = {Forward Analysis for {WSTS}, {Part III}: {Karp-Miller} Trees},
pages = {16:1-16:15},
url = {https://hal.archives-ouvertes.fr/hal-01736704/},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/8403/pdf/LIPIcs-FSTTCS-2017-16.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2017.16},
abstract = {This paper is a sequel of ''Forward Analysis for WSTS, Part I: Completions'' [STACS 2009, LZI Intl. Proc. in Informatics 3, 433-444] and ''Forward Analysis for WSTS, Part II: Complete WSTS'' [Logical Methods in Computer Science 8(3), 2012]. In these two papers, we provided a framework to conduct forward reachability analyses of WSTS, using finite representations of downwards-closed sets. We further develop this framework to obtain a generic Karp-Miller algorithm for the new class of very-WSTS. This allows us to show that coverability sets of very-WSTS can be computed as their finite ideal decompositions. Under natural assumptions on positive sequences, we also show that LTL model checking for very-WSTS is decidable. The termination of our procedure rests on a new notion of acceleration levels, which we study. We characterize those domains that allow for only finitely many accelerations, based on ordinal ranks.}
}
@article{BFHH-tocl17,
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
author = {Blondin, Michael and Finkel, Alain and Haase, Christoph and
Haddad, Serge},
title = {The Logical View on Continuous {P}etri Nets},
volume = {18},
number = {3},
year = {2017},
pages = {24:1--24:28},
url = {http://doi.acm.org/10.1145/3105908},
doi = {10.1145/3105908},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHH-tocl17.pdf},
abstract = {Continuous Petri nets are a relaxation of classical discrete Petri nets in which transitions can be fired a fractional number of times, and consequently places may contain a fractional number of tokens. Such continuous Petri nets are an appealing object to study since they over approximate the set of reachable configurations of their discrete counterparts, and their reachability problem is known to be decidable in polynomial time. The starting point of this paper is to show that the reachability relation for continuous Petri nets is definable by a sentence of linear size in the existential theory of the rationals with addition and order. Using this characterization, we obtain decidability and complexity results for a number of classical decision problems for continuous Petri nets. In particular, we settle the open problem about the precise complexity of reachability set inclusion. Finally, we show how continuous Petri nets can be incorporated inside the classical backward coverability algorithm for discrete Petri nets as a pruning heuristic in order to tackle the symbolic state explosion problem. The cornerstone of the approach we present is that our logical characterization enables us to leverage the power of modern SMT-solvers in order to yield a highly performant and robust decision procedure for coverability in Petri nets. We demonstrate the applicability of our approach on a set of standard benchmarks from the literature.}
}
@inproceedings{FL-icalp17,
address = {Warsaw, Poland},
month = jul,
volume = {80},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Chatzigiannakis, Ioannis and Indyk, Piotr and Muscholl, Anca and Kuhn, Fabian},
acronym = {{ICALP}'17},
booktitle = {{P}roceedings of the 44th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'17)},
author = {Finkel, Alain and Lozes, {\'E}tienne},
title = {Synchronizability of Communicating Finite State Machines is not Decidable},
pages = {122:1-122:14},
year = {2017},
doi = {10.4230/LIPIcs.ICALP.2017.122},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2017/7402/pdf/LIPIcs-ICALP-2017-122.pdf},
url = {http://drops.dagstuhl.de/opus/volltexte/2017/7402},
abstract = {A system of communicating finite state machines is synchronizable if its send trace semantics, i.e. the set of sequences of sendings it can perform, is the same when its communications are FIFO asynchronous and when they are just rendez-vous synchronizations. This property was claimed to be decidable in several conference and journal papers for either mailboxes or peer-to-peer communications, thanks to a form of small model property. In this paper, we show that this small model property does not hold neither for mailbox communications, nor for peer-to-peer communications, therefore the decidability of synchronizability becomes an open question. We close this question for peer-to-peer communications, and we show that synchronizability is actually undecidable. We show that synchronizability is decidable if the topology of communications is an oriented ring. We also show that, in this case, synchronizability implies the absence of unspecified receptions and orphan messages, and the channel-recognizability of the reachability set.}
}
@inproceedings{FLS-fsttcs18,
address = {Ahmedabad, India},
month = dec,
year = 2018,
volume = {122},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Sumit Ganguly and Paritosh Pandya},
acronym = {{FSTTCS}'18},
booktitle = {{P}roceedings of the 38th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'18)},
author = {Alain Finkel and J{\'e}r{\^o}me Leroux and Gr{\'e}goire Sutre},
title = {Reachability for Two-Counter Machines with One Test and One Reset},
pages = {31:1-31:14},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9930},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/9930/pdf/LIPIcs-FSTTCS-2018-31.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2018.31},
abstract = {We prove that the reachability relation of two-counter machines with one zero-test and one reset is Presburger-definable and effectively computable. Our proof is based on the introduction of two classes of Presburger-definable relations effectively stable by transitive closure. This approach generalizes and simplifies the existing different proofs and it solves an open problem introduced by Finkel and Sutre in 2000.}
}
@article{CFMF-fac18,
publisher = {Springer},
journal = {Formal Aspects of Computing},
author = {Rapha{\"e}l Chane-Yack-Fa and Marc Frappier and Amel Mammar and Alain Finkel},
title = {{Parameterized Verification of Monotone Information Systems}},
volume = {30},
number = {3-4},
year = {2018},
pages = {463-489},
doi = {10.1007/s00165-018-0460-8},
url = {https://link.springer.com/article/10.1007/s00165-018-0460-8},
abstract = {In this paper, we study the information system verification problem as a parameterized verification one. Informations systems are modeled as multi-parameterized systems in a formal language based on the Algebraic State-Transition Diagrams (ASTD) notation. Then, we use the Well Structured Transition Systems (WSTS) theory to solve the coverability problem for an unbounded ASTD state space. Moreover, we define a new framework to prove the effective pred-basis condition of WSTSs, i.e. the computability of a base of predecessors for every states.}
}
@inproceedings{GF-fsttcs19,
address = {Bombay, India},
month = dec,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Arkadev Chattopadhyay and Paul Gastin},
acronym = {{FSTTCS}'19},
booktitle = {{P}roceedings of the 39th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'19)},
author = {Ekanshdeep Gupta and Alain Finkel},
title = {The well structured problem for Presburger counter machines},
pages = {41:1-41:15},
year = 2019,
doi = {10.4230/LIPIcs.FSTTCS.2019.41},
pdf = {https://drops.dagstuhl.de/opus/volltexte/2019/11603/pdf/LIPIcs-FSTTCS-2019-41.pdf},
url = {https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11603},
abstract = {We introduce the well structured problem as the question of whether a model (here a counter machine) is well structured (here for the usual ordering on integers). We show that it is undecidable for most of the (Presburger-defined) counter machines except for Affine VASS of dimension one. However, the strong well structured problem is decidable for all Presburger counter machines. While Affine VASS of dimension one are not, in general, well structured, we give an algorithm that computes the set of predecessors of a configuration; as a consequence this allows to decide the well structured problem for 1-Affine VASS.}
}
@inproceedings{FP-concur19,
address = {Amsterdam, The Netherlands},
month = aug,
volume = {140},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Wan Fokkink and Rob {van Glabbeek}},
acronym = {{CONCUR}'19},
booktitle = {{P}roceedings of the 30th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'19)},
author = {Alain Finkel and M. Praveen},
title = {Verification of Flat FIFO Systems},
pages = {12:1-12:17},
year = 2019,
doi = {10.4230/LIPIcs.CONCUR.2019.12},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2019/10914/pdf/LIPIcs-CONCUR-2019-12.pdf},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=10914},
abstract = {The decidability and complexity of reachability problems and model-checking for flat counter systems have been explored in detail. However, only few results are known for flat FIFO systems, only in some particular cases (a single loop or a single bounded expression). We prove, by establishing reductions between properties, and by reducing SAT to a subset of these properties that many verification problems like reachability, non-termination, unboundedness are NP-complete for flat FIFO systems, generalizing similar existing results for flat counter systems. We construct a trace-flattable counter system that is bisimilar to a given flat FIFO system, which allows to model-check the original flat FIFO system. Our results lay the theoretical foundations and open the way to build a verification tool for (general) FIFO systems based on analysis of flat subsystems.}
}
@inproceedings{FHK-atpn19,
address = {Aachen, Germany},
month = jun,
year = 2019,
volume = {11522},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Susanna Donatelli and Stefan Haar},
acronym = {{PETRI~NETS}'19},
booktitle = {{P}roceedings of the 40th
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({PETRI~NETS}'19)},
author = {Finkel, Alain and Haddad, Serge and Khmelnitsky, Igor},
title = {Coverability and Termination in Recursive Petri Nets},
pages = { 429-448},
url = {https://hal.inria.fr/hal-02081019},
pdf = {https://hal.inria.fr/hal-02081019/document},
doi = {10.1007/978-3-030-21571-2_23},
abstract = {In the early two-thousands, Recursive Petri nets have been introduced in order to model distributed planning of multi-agent systems for which counters and recursivity were necessary. Although Recursive Petri nets strictly extend Petri nets and stack automata, most of the usual property problems are solvable but using non primitive recursive algorithms, even for coverability and termination. For almost all other extended Petri nets models containing a stack the complexity of coverability and termination are unknown or strictly larger than EXPSPACE. In contrast, we establish here that for Recursive Petri nets, the coverability and termination problems are EXPSPACE-complete as for Petri nets. From an expressiveness point of view, we show that coverability languages of Recursive Petri nets strictly include the union of coverability languages of Petri nets and context-free languages. Thus we get for free a more powerful model than Petri net.}
}
@inproceedings{Finkel-vpthcvs2020,
address = {Dublin, Ireland},
month = april,
year = 2020,
publisher = {Electronic Proceedings in Theoretical Computer Science},
editor = {Laurent Fribourg and Matthias Heizmann},
acronym = {{VPT/HCVS@ETAPS}'20},
booktitle = {Proceedings of 8th {I}nternational {W}orkshop on {V}erification and
{P}rogram {T}ransformation and 7th {W}orkshop on {H}orn {C}lauses for {V}erification and {S}ynthesis
({VPT/HCVS@ETAPS 2020})},
author = {Alain Finkel},
title = {{From Well Structured Transition Systems to Program Verification}},
pages = {44--49},
url = {https://arxiv.org/abs/2008.02929v1},
pdf = {https://arxiv.org/abs/2008.02929v1},
doi = {10.4204/EPTCS.320.3}
}
@article{FHK-deds20,
publisher = {Springer},
journal = {Discrete Event Dynamic Systems: Theory and Applications},
author = {Alain Finkel and Serge Haddad and Igor Khmelnitsky},
title = {{Commodification of accelerations for the Karp and Miller Construction}},
doi = {10.1007/s10626-020-00331-z},
year = {2020},
url = {https://link.springer.com/article/10.1007/s10626-020-00331-z}
}
@article{FG-mscs20,
publisher = {Cambridge University Press},
journal = {Mathematical Structures in Computer Science},
author = {Finkel, Alain and Goubault{-}Larrecq, Jean},
title = {{Forward analysis for WSTS, part I: completions}},
volume = {30},
number = {7},
pages = {752-832},
doi = {10.1017/S0960129520000195},
year = {2020},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FG-mscs2020.pdf},
url = {http://dx.doi.org/10.1017/S0960129520000195}
}
@article{FP-lmcs20,
journal = {Logical Methods in Computer Science},
author = {Finkel, Alain and Praveen, M.},
title = {{Verification of Flat FIFO Systems}},
volume = {20},
number = {4},
doi = {10.23638/LMCS-16(4:4)2020},
year = {2020},
month = oct,
url = {https://lmcs.episciences.org/6839}
}
@techreport{KY-arxiv20,
author = {Khmelnitsky, Igor and
Neider, Daniel and
Roy, Rajarshi and
Barbot, Beno{\^{\i}}t and
Bollig, Benedikt and
Finkel, Alain and
Haddad, Serge and
Leucker, Martin and
Ye, Lina },
institution = {Computing Research Repository},
month = sep,
number = {2009.10610},
type = {Research Report},
title = {Property-Directed Verification of Recurrent Neural Networks},
year = {2020},
url = {https://arxiv.org/abs/2009.10610},
pdf = {https://arxiv.org/pdf/2009.10610.pdf}
}
@article{BFG-lmcs20,
journal = {Logical Methods in Computer Science},
author = {Michael Blondin and Alain Finkel and Jean Goubault{-}Larrecq},
title = {{Forward Analysis for WSTS, Part {III:} Karp-Miller Trees}},
volume = {16},
number = {2},
doi = {10.23638/LMCS-16(2:13)2020},
year = {2020},
url = {https://lmcs.episciences.org/6591}
}
@inproceedings{BDM-concur20,
address = {Vienna, Austria},
month = sep,
volume = {171},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Igor Konnov and Laura Kovacs},
acronym = {{CONCUR}'20},
booktitle = {{P}roceedings of the 31st
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'20)},
author = {Benedikt Bollig and Alain Finkel and Amrita Suresh},
title = {Bounded Reachability Problems are Decidable in {FIFO} Machines},
pages = {49:1--49:17},
year = 2020,
url = {https://drops.dagstuhl.de/opus/volltexte/2020/12861}
}
@inproceedings{FHK-msr2019,
address = {Angers, France},
month = nov,
futureseries = {Journal Europ{\'e}en des Syst{\`e}mes Automatis{\'e}s},
publisher = {HAL},
editor = {Beno{\^i}t Delahaye and S{\'e}bastien Lahaye and Mehdi Lhommeau},
acronym = {{MSR}'19},
booktitle = {{A}ctes du 12{\`e}me {C}olloque sur la
{M}od{\'e}lisation des {S}yst{\`e}mes
{R}{\'e}actifs
({MSR}'19)},
author = {Alain Finkel and Serge Haddad and Igor Khmelnitsky},
title = {{R{\'e}ification des acc{\'e}l{\'e}rations pour la construction de Karp et Miller}},
year = 2019,
pdf = {https://hal.archives-ouvertes.fr/hal-02431913/file/MSR19_paper_17.pdf},
url = {https://hal.archives-ouvertes.fr/hal-02431913}
}
@inproceedings{FHK-fossacs2020,
address = {Dublin, Ireland},
month = apr,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Barbara K{\"o}nig and Jean Goubault-Larrecq},
acronym = {{FoSSaCS}'20},
booktitle = {{P}roceedings of the 23rd {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'20)},
author = {Alain Finkel and Serge Haddad and Igor Khmelnitsky},
title = {Minimal coverability tree construction made complete and efficient},
pages = {237--256},
doi = {10.1007/978-3-030-45231-5_13},
year = 2020
}
This file was generated by bibtex2html 1.98.