@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}
}
@inproceedings{BB-CP-MFCS97,
address = {Bratislava, Slovakia},
month = aug,
year = 1997,
volume = 1295,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Pr{\'i}vara, Igor and Ruzicka, Peter},
acronym = {{MFCS}'97},
booktitle = {{P}roceedings of the 22nd
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'97)},
author = {B{\'e}rard, B{\'e}atrice and Picaronny, Claudine},
title = {Accepting {Z}eno Words without Making Time Stand
Still},
pages = {149-158},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BerPic-long.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BerPic-long.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BerPic-long.pdf}
}
@article{BCB-RC-AP-97,
address = {Les Ulis, France},
publisher = {EDP Sciences},
journal = {RAIRO Informatique Th{\'e}orique et Applications},
author = {Charron{-}Bost, Bernadette and Cori, Robert and
Petit, Antoine},
title = {Introduction {\`a} l'algorithmique en m{\'e}moire
partag{\'e}e},
volume = {31},
number = {2},
pages = {97-148},
year = {1997},
missingmonth = {},
missingnmonth = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCP-RAIRO97.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CCP-RAIRO97.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CCP-RAIRO97.pdf},
lsv-lang = {FR}
}
@inproceedings{CD-Renpar-97,
address = {Lausanne, Switzerland},
month = may,
year = 1997,
acronym = {{RENPAR}'97},
booktitle = {{A}ctes des 9{\`e}mes {R}encontres
{F}rancophones du {P}arall{\'e}lisme
({RENPAR}'97)},
author = {Dufourd, Catherine},
title = {Une extension d'un r{\'e}sultat d'ind{\'e}cidabilit{\'e}
pour les automates temporis{\'e}s},
pages = {219-222},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/Duf-renpar97.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Duf-renpar97.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Duf-renpar97.pdf},
lsv-lang = {FR}
}
@inproceedings{FB-LP-MOSIM-97,
address = {Rouen, France},
month = jun,
year = 1997,
publisher = {Herm{\`e}s},
acronym = {{MOSIM}'97},
booktitle = {{A}ctes de la 1{\`e}re {C}onf{\'e}rence
{F}rancophone de {M}od{\'e}lisation et de
{S}imulation
({MOSIM}'97)},
author = {Belala, F. and Petrucci, Laure},
missingauthor = {},
title = {{S}\'emantique des {ECATN}ets en termes de {CPN}ets :
application {\`a} un exemple de production},
missingpages = {},
lsv-lang = {FR}
}
@inproceedings{GC-Renpar-97,
address = {Lausanne, Switzerland},
month = may,
year = 1997,
acronym = {{RENPAR}'97},
booktitle = {{A}ctes des 9{\`e}mes {R}encontres
{F}rancophones du {P}arall{\'e}lisme
({RENPAR}'97)},
author = {C{\'e}c{\'e}, G{\'e}rard},
title = {Les programmes utilisant des canaux quasi-stables sont
effectivement reconnaissables},
pages = {215-218},
lsv-lang = {FR}
}
@book{JCB-HC-CK-DK-MM-JMM-AP-YR-livre96,
author = {Bajard, Jean-Claude and Comon, Hubert and
Kenyon, Claire and Krob, Daniel
and Morvan, Michel and Muller, Jean-Michel and
Petit, Antoine and Robert, Yves},
title = {Exercices d'algorithmique (oraux d'{ENS})},
year = {1997},
publisher = {Vuibert},
month = jan,
pages = {272},
isbn = {2-84180-105-5},
lsv-lang = {FR}
}
@techreport{LSV:97:10,
author = {Williams{-}Preston, Nicky},
title = {An Experiment in Reverse Engineering Using Algebraic
Specifications},
type = {Research Report},
number = {LSV-97-10},
year = {1997},
month = nov,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-1997-10.rr.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-1997-10.rr.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-1997-10.rr.ps}
}
@inproceedings{MM-MB-GB-LP-MOSIM-97,
address = {Rouen, France},
month = jun,
year = 1997,
publisher = {Herm{\`e}s},
acronym = {{MOSIM}'97},
booktitle = {{A}ctes de la 1{\`e}re {C}onf{\'e}rence
{F}rancophone de {M}od{\'e}lisation et de
{S}imulation
({MOSIM}'97)},
author = {Maouche, Mourad and Bettaz, Mohamed and
Berthelot, G{\'e}rard and Petrucci, Laure},
title = {Du vrai parall{\'e}lisme dans les r{\'e}seaux
alg{\'e}briques et de son application dans les syst{\`e}mes
de production},
pages = {417-424},
lsv-lang = {FR}
}
@inproceedings{RM-AP-mfcs97,
address = {Bratislava, Slovakia},
month = aug,
year = 1997,
volume = 1295,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Pr{\'i}vara, Igor and Ruzicka, Peter},
acronym = {{MFCS}'97},
booktitle = {{P}roceedings of the 22nd
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'97)},
author = {Meyer, Rapha{\"e}l and Petit, Antoine},
title = {Decomposition of {TrPTL} Formulas},
pages = {418-427},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/MeyPet-mfcs97.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MeyPet-mfcs97.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MeyPet-mfcs97.pdf}
}
@inproceedings{VD-PG-AP-stacs97,
address = {L{\"u}beck, Germany},
month = feb,
year = 1997,
volume = 1200,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Reischuk, R{\"u}diger and Morvan, Michel},
acronym = {{STACS}'97},
booktitle = {{P}roceedings of the 14th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'97)},
author = {Diekert, Volker and Gastin, Paul and Petit, Antoine},
title = {Removing {{\(\epsilon\)}}-Transitions in Timed Automata},
pages = {583-594},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DGP-stacs97.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DGP-stacs97.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DGP-stacs97.pdf},
abstract = {Timed automata are among the most widely studied models for
real-time systems. Silent transitions, \emph{i.e.},
\(\epsilon\)-transitions, have already been proposed in the
original paper on timed automata by Alur and Dill. B{\'e}rard,
Gastin and Petit have shown that \(\epsilon\)-transitions
can be removed, if they do not reset clocks; moreover
\(\epsilon\)-transitions strictly increase the power of timed
automata, if there is a self-loop containing
\(\epsilon\)-transitions which reset some clocks. This paper left
open the problem about the power of the \(\epsilon\)-transitions
which reset clocks, if they do not lie on any cycle.\par
The present paper settles this open question. Precisely, we
prove that a timed automaton such that no \(\epsilon\)-transition
with nonempty reset set lies on any directed cycle can be
effectively transformed into a timed automaton without
\(\epsilon\)-transitions. Interestingly, this main result holds
under the assumption of non-Zenoness and it is false
otherwise.\par
Besides, we develop a promising new technique based on a
notion of precise
time which allows to show that some timed languages are not
recognizable by any \(\epsilon\)-free timed automaton.}
}
@inproceedings{comon97lics,
address = {Warsaw, Poland},
month = jul,
year = 1997,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'97},
booktitle = {{P}roceedings of the 12th
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'97)},
author = {Comon, Hubert and Jacquemard, Florent},
title = {Ground Reducibility is {EXPTIME}-Complete},
pages = {26-34},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ComJac-lics97.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComJac-lics97.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ComJac-lics97.pdf}
}
@misc{comon97licsb,
author = {Comon, Hubert},
title = {Applications of Tree Automata in Rewriting and
Lambda-Calculus},
year = 1997,
month = jul,
howpublished = {Invited lecture, 12th
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'97), Warsaw, Poland}
}
@proceedings{comon97rta,
title = {{P}roceedings of the 8th {I}nternational
{C}onference on {R}ewriting {T}echniques
and {A}pplications
({RTA}'97)},
booktitle = {{P}roceedings of the 8th {I}nternational
{C}onference on {R}ewriting {T}echniques
and {A}pplications
({RTA}'97)},
editor = {Comon, Hubert},
publisher = {Springer},
volume = {1232},
series = {Lecture Notes in Computer Science},
pages = {348},
year = {1997},
month = jun,
isbn = {3-540-62950-5},
url = {http://www.springer.com/978-3-540-62950-5},
olderurl = {http://www.springer.de/cgi-bin/search_book.pl?isbn=3-540-62950-5}
}
@article{comon97tcs,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Comon, Hubert and Treinen, Ralf},
title = {The First-Order Theory of Lexicographic Path Orderings
is Undecidable},
volume = {176},
number = {1-2},
pages = {67-87},
year = {1997},
month = apr,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ComTre-TCS97.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComTre-TCS97.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ComTre-TCS97.pdf}
}
@misc{edf-comon-97,
author = {Comon, Hubert},
title = {Une approche logique des contr{\^o}les logiques},
year = {1997},
month = jun,
howpublished = {Rapport de contrat EDF/DER/MOS--LSV},
lsv-lang = {FR}
}
@techreport{forma-sric-BerBid-97,
author = {B{\'e}rard, B{\'e}atrice and Bidoit, Michel},
title = {Contribution du {LSV} {\`a} l'op{\'e}ration~2 <<~{\'E}tude de
cas {SRIC}~>>},
year = {1997},
month = oct,
type = {Contract Report},
institution = {Action FORMA},
note = {29 pages}
}
@article{hen-wir-bid-tcs-wadt,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Hennicker, Rolf and Wirsing, Martin and Bidoit, Michel},
title = {Proof Systems for Structured Specifications with
Observability Operators},
volume = {173},
number = {2},
pages = {393-443},
year = {1997},
month = feb
}
@inproceedings{kouchnarenko97,
address = {Yaroslavl, Russia},
month = sep,
year = 1997,
volume = 1277,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Malyshkin, Victor E.},
acronym = {{PaCT}'97},
booktitle = {{P}roceedings of the 4th {I}nternational
{C}onference on {P}arallel {C}omputing
{T}echnologies
({PaCT}'97)},
author = {Kouchnarenko, Olga and Schnoebelen, {\relax Ph}ilippe},
title = {A Formal Framework for the Analysis of
Recursive-Parallel Programs},
pages = {45-59},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/KusSch-pact97.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/KusSch-pact97.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KusSch-pact97.pdf},
doi = {10.1007/3-540-63371-5_6}
}
@inproceedings{kouchnarenko97b,
address = {Pisa, Italy},
year = 1997,
volume = 5,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Steffen, B. and Caucal, Didier},
acronym = {{INFINITY}'96},
booktitle = {{P}roceedings of the 1st {I}nternational
{W}orkshop on {V}erification of {I}nfinite
{S}tate {S}ystems
({INFINITY}'96)},
author = {Kouchnarenko, Olga and Schnoebelen, {\relax Ph}ilippe},
title = {A Model for Recursive-Parallel Programs},
pages = {30},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/KouSch-infin96.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/KouSch-infin96.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KouSch-infin96.pdf},
doi = {10.1016/S1571-0661(05)82512-5}
}
@inproceedings{kristoffersen97,
address = {Lille, France},
month = apr,
year = 1997,
volume = 1214,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Bidoit, Michel and Dauchet, Max},
acronym = {{TAPSOFT}'97},
booktitle = {{P}roceedings of the 7th
{I}nternational {J}oint {C}onference {CAAP}/{FASE} on
{T}heory and {P}ractice of {S}oftware {D}evelopment
({TAPSOFT}'97)},
author = {Kristoffersen, K{\aa}re J. and
Laroussinie, Fran{\c{c}}ois and
Larsen, Kim G. and Pettersson, Paul and Yi, Wang},
title = {A Compositional Proof of a Real-Time Mutual Exclusion
Protocol},
pages = {565-579},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/KLLPY-tapsoft97.pdf},
ps = {KLLPY-tapsoft97.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KLLPY-tapsoft97.pdf},
doi = {10.1007/BFb0030626}
}
@inproceedings{laroussinie97,
address = {Santa Margherita Ligure, Italy},
month = sep,
year = 1997,
volume = 7,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Palamidessi, Catuscia and Parrow, Joachim},
acronym = {{EXPRESS}'97},
booktitle = {{P}roceedings of the 4th {I}nternational
{W}orkshop on {E}xpressiveness in
{C}oncurrency
({EXPRESS}'97)},
author = {Laroussinie, Fran{\c{c}}ois and
Schnoebelen, {\relax Ph}ilippe},
title = {Specification in {CTL}+{P}ast, Verification in {CTL}},
pages = {161-184},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LarSch-express97.pdf},
ps = {LarSch-express97.ps},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LarSch-express97.pdf},
doi = {10.1016/S1571-0661(05)80472-4}
}
@inproceedings{lf-ho-concur-97,
address = {Warsaw, Poland},
month = jul,
year = 1997,
volume = 1243,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Mazurkiewicz, Antoni W. and Winkowski, J{\'o}zef},
acronym = {{CONCUR}'97},
booktitle = {{P}roceedings of the 8th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'97)},
author = {Fribourg, Laurent and Ols{\'e}n, Hans},
title = {Proving Safety Properties of Infinite State Systems by
Compilation into {P}resburger Arithmetic},
pages = {213-227},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LF-concur97.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LF-concur97.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LF-concur97.pdf}
}
@article{lf-ho-constraint-97,
publisher = {Kluwer Academic Publishers},
journal = {Constraints},
author = {Fribourg, Laurent and Ols{\'e}n, Hans},
title = {A Decompositional Approach for Computing Least
Fixed-Points of {D}atalog Programs with {Z}-Counters},
volume = {2},
number = {3-4},
pages = {305-335},
year = {1997},
missingmonth = {>oct},
missingnmonth = {>10},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LF-constraints97.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LF-constraints97.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LF-constraints97.pdf}
}
@inproceedings{lf-ho-infinity-97,
address = {Bologna, Italy},
month = jul,
year = 1997,
volume = 9,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Moller, Faron},
acronym = {{INFINITY}'97},
booktitle = {{P}roceedings of the 2nd {I}nternational
{W}orkshop on {V}erification of {I}nfinite
{S}tate {S}ystems
({INFINITY}'97)},
author = {Fribourg, Laurent and Ols{\'e}n, Hans},
title = {Reachability Sets of Parametrized Rings As Regular
Languages},
pages = {40},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LF-infinity97.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LF-infinity97.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LF-infinity97.pdf}
}
@proceedings{mb-max-tapsoft97,
title = {{P}roceedings of the 7th
{I}nternational {J}oint {C}onference {CAAP}/{FASE} on
{T}heory and {P}ractice of {S}oftware {D}evelopment
({TAPSOFT}'97)},
booktitle = {{P}roceedings of the 7th
{I}nternational {J}oint {C}onference {CAAP}/{FASE} on
{T}heory and {P}ractice of {S}oftware {D}evelopment
({TAPSOFT}'97)},
editor = {Bidoit, Michel and Max Dauchet},
publisher = {Springer},
volume = {1214},
series = {Lecture Notes in Computer Science},
pages = {889},
year = {1997},
month = apr,
organization = {Lille, France},
isbn = {3-540-62781-2},
url = {http://www.springer.com/978-3-540-62781-2},
olderurl = {http://www.springer.de/cgi-bin/search_book.pl?isbn=3-540-62781-2}
}
@incollection{plandedefense,
author = {Bidoit, Michel and Pellen, {\relax Ch}ristine and
Ryckbosch, J{\'e}r{\^o}me},
title = {Plan de D{\'e}fense~--- {F}ormalisation du cahier des
charges du {P}oint {C}entral {\`a} l'aide de sp{\'e}cifications
alg{\'e}briques},
booktitle = {Application des techniques formelles au logiciel},
chapter = {7},
type = {chapter},
pages = {123-132},
series = {ARAGO 20},
publisher = {Observatoire Fran\c{c}ais des Techniques Avanc\'ees},
year = {1997},
month = jun,
lsv-lang = {FR}
}
@mastersthesis{sutre97,
author = {Sutre, Gr{\'e}goire},
title = {V{\'e}rification de propri{\'e}t{\'e}s sur les automates
{\`a} file
r{\'e}actifs produits par compilation de programmes
{E}lectre},
year = {1997},
month = sep,
type = {Rapport de {DEA}},
school = {{DEA} Algorithmique, Paris, France},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/Sut-dea97.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Sut-dea97.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sut-dea97.pdf},
lsv-lang = {FR}
}
@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.",
}}
This file was generated by bibtex2html 1.98.