@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}
}
@techreport{AP-mc98,
author = {Petit, Antoine},
title = {Le model-checking, une technique de
v{\'e}rification en plein essor. {I}ntroduction},
year = {1998},
month = oct,
type = {Contract Report},
institution = {EDF/DER/MOS - LSV},
lsv-lang = {FR}
}
@techreport{BB-MB-AP-src98,
author = {B{\'e}rard, B{\'e}atrice and Bidoit, Michel and
Petit, Antoine},
title = {Recommandations sur le cahier des charges {SRC}},
year = {1998},
missingmonth = {},
missingnmonth = {},
type = {Contract Report},
institution = {EDF/DER/MOS - LSV},
lsv-lang = {FR}
}
@article{BB-VD-PG-AP-98,
publisher = {{IOS} Press},
journal = {Fundamenta Informaticae},
author = {B{\'e}rard, B{\'e}atrice and Diekert, Volker and
Gastin, Paul and Petit, Antoine},
title = {Characterization of the Expressive Power of Silent
Transitions in Timed Automata},
volume = {36},
number = {2},
pages = {145-182},
year = {1998},
month = nov,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BDGP-FUNDI98.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BDGP-FUNDI98.ps},
abstract = {Timed automata are among the
most widely studied models for real-time
systems. Silent transitions (or
\(\epsilon\)-transitions) have already been
proposed in the original paper on timed
automata by Alur and~Dill. We show that the
class of timed languages recognized by
automata with \(\epsilon\)-transitions, is more
robust and more expressive than the
corresponding class without
\(\epsilon\)-transitions. \par
We then focus on \(\epsilon\)-transitions which do
not reset clocks. We propose an algorithm to
construct, given a timed automaton, an
equivalent one without such transitions. This
algorithm is in two steps, it first suppresses
the cycles of \(\epsilon\)-transitions without
reset and then the remaining ones.\par
Then, we prove that a timed automaton such
that no \(\epsilon\)-transition which resets clocks
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
To complete the picture, we exhibit a simple
timed automaton with an \(\epsilon\)-transition,
which resets some clock, on a cycle and which
is not equivalent to any \(\epsilon\)-free timed
automaton. To show this, we develop a
promising new technique based on the notion of
precise action.}
}
@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}
}
@inproceedings{CC-AP-mteac98,
address = {Las Vegas, Nevada, USA},
month = jan,
year = 1998,
editor = {B{\"o}hm, A. P. Wim and Najjar, Walid A.},
acronym = {{MTEAC}'98},
booktitle = {{P}roceedings of the {W}orkshop on
{M}ultithreaded {E}xecution, {A}rchitecture
and {C}ompilation
({MTEAC}'98)},
author = {C{\'e}rin, {\relax Ch}ristophe and Petit, Antoine},
title = {Application of Algebraic Techniques to Compute the
Efficiency Measure for Multithreaded Architecture},
missingpages = {??},
howpublished = {Proceedings published as
Technical Report CS-98-102,
Colorado State University},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CP-mteac98.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CP-mteac98.ps}
}
@techreport{DD1-98,
author = {Laroussinie, Fran{\c{c}}ois and Petit, Antoine and
Schnoebelen, {\relax Ph}ilippe},
title = {Le model-checking, une technique de
v{\'e}rification en
plein essor. {I}~--- {P}rincipes et techniques},
year = {1998},
month = oct,
type = {Contract Report},
institution = {EDF/DER/MOS - LSV},
lsv-lang = {FR}
}
@techreport{DD2-98,
author = {Schnoebelen, {\relax Ph}ilippe},
title = {Le model-checking, une technique de
v{\'e}rification en
plein essor. {III}~--- {S}p{\'e}cifier pour
v{\'e}rifier},
year = {1998},
month = oct,
type = {Contract Report},
institution = {EDF/DER/MOS - LSV},
lsv-lang = {FR}
}
@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}
}
@article{GG-RM-AP-PW-98,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Guaiana, Giovana and Meyer, Rapha{\"e}l and
Petit, Antoine and Weil, Pascal},
title = {An Extension of the Wreath Product Principle for
Finite {M}azurkiewicz Traces},
volume = {67},
number = {6},
pages = {277-282},
year = {1998},
month = sep,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GMPW-IPL98.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GMPW-IPL98.ps}
}
@inproceedings{KB-LP-WFM-98,
address = {Lisbon, Portugal},
month = jun,
year = 1998,
volume = {98/7},
series = {Computing Science Report},
optaddress = {Eindhoven, The Netherlands},
publisher = {Eindhoven University of Technology, Eindhoven, The Netherlands},
editor = {van der Aalst, Wil M. P. and De Michelis, Giorgio and
Ellis, Clarence A.},
acronym = {{WFM}'98},
booktitle = {{P}roceedings of {W}orkflow {M}anagement:
{N}et-{B}ased {C}oncepts, {M}odels,
{T}echniques and {T}ools
({WFM}'98)},
author = {Barkaoui,Kamel and Petrucci, Laure},
title = {Structural Analysis of Workflow Nets with Shared
Resources},
pages = {82-95},
howpublished = {Proceedings published as Computing Science Report
98/7, Eindhoven University of Technology, NL},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BarPet-wfm98.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BarPet-wfm98.ps}
}
@inproceedings{LA-PB-AB-KL-fsttcs98,
address = {Chennai, India},
month = dec,
year = 1998,
volume = 1530,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Arvind, Vikraman and Ramanujam, R.},
acronym = {{FSTTCS}'98},
booktitle = {{P}roceedings of the 18th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'98)},
author = {Aceto, Luca and Bouyer, Patricia and
Burgue{\~n}o, Augusto and Larsen, Kim G.},
title = {The Power of Reachability Testing for
Timed Automata},
pages = {245-256},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ABBL-fsttcs98.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ABBL-fsttcs98.ps},
abstract = {In this paper we provide a
complete characterization of the class of
properties of (networks of) timed automata for
which model checking
can be reduced to reachability checking in the
context of testing
automata.}
}
@book{LA-PG-BP-AP-NP-PW-livre98,
author = {Albert, Luc and Gastin, Paul and
Petazzoni, Bruno and Petit, Antoine
and Puech, Nicolas and Weil, Pascal},
title = {Cours et exercices d'informatique, Classes
pr{\'e}paratoires, premier et second cycles
universitaires},
year = {1998},
month = jun,
publisher = {Vuibert},
isbn = {2-7117-8621-8},
lsv-lang = {FR}
}
@techreport{LSV:98:2,
author = {Fribourg, Laurent},
title = {A Closed-Form Evaluation for Extended Timed Automata},
type = {Research Report},
number = {LSV-98-2},
year = {1998},
month = mar,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-1998-2.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-1998-2.rr.ps}
}
@mastersthesis{Labroue-dea,
author = {Labroue, Anne},
title = {Conditions de vivacit{\'e} dans les automates
temporis{\'e}s},
year = {1998},
month = jul,
type = {Rapport de {DEA}},
school = {{DEA} Informatique, Orsay, France},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-1998-7.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-1998-7.rr.ps},
lsv-lang = {FR}
}
@mastersthesis{PB-dea98,
author = {Bouyer, Patricia},
title = {Automates temporis{\'e}s et modularit{\'e}},
year = {1998},
month = jun,
type = {Rapport de {DEA}},
school = {{DEA} Algorithmique, Paris, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Bou-dea98.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Bou-dea98.ps},
lsv-lang = {FR}
}
@inproceedings{PG-RM-AP-mfcs98,
address = {Brno, Czech Republic},
month = aug,
year = 1998,
volume = 1450,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Brim, Lubos and Gruska, Jozef and Zlatuska, Jir{\'i}},
acronym = {{MFCS}'98},
booktitle = {{P}roceedings of the 23rd
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'98)},
author = {Gastin, Paul and Meyer, Rapha{\"e}l and
Petit, Antoine},
title = {A (non-elementary) modular decision procedure for
{LTrL}},
pages = {356-365},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GMP-mfcs98.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GMP-mfcs98.ps},
abstract = {Thiagarajan and Walukiewicz have defined a
temporal logic~LTrL on Mazurkiewicz
traces, patterned on the famous
propositional temporal logic of linear
time~LTL defined by Pnueli. They have
shown that this logic is equal in
expressive power to the first order theory
of finite and infinite traces.\par
The hopes to get an {"}easy{"} decision
procedure for~LTrL, as it is the case
for~LTL, vanished very recently due to a
result of Walukiewicz who showed that the
decision procedure for~LTrL is
non-elementary. However, tools like Mona
or Mosel show that it is possible to
handle non-elementary logics on
significant examples. Therefore, it
appears worthwhile to have a direct
decision procedure for LTrL.\par
In this paper we propose such a decision
procedure, in a modular way. Since the
logic~LTrL is not pure future, our
algorithm constructs by induction a finite
family of B{\"u}chi automata for each
LTrL-formula. As expected by the results
of Walukiewicz, the main difficulty comes
from the {"}Until{"} operator.}
}
@inproceedings{RM-AP-stacs98,
address = {Paris, France},
month = feb,
year = 1998,
volume = 1373,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Morvan, Michel and Meinel, {\relax Ch}ristoph and
Krob, Daniel},
acronym = {{STACS}'98},
booktitle = {{P}roceedings of the 15th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'98)},
author = {Meyer, Rapha{\"e}l and Petit, Antoine},
title = {Expressive Completeness of {LTrL} on Finite Traces:
{A}n Algebraic Proof},
pages = {533-543}
}
@inproceedings{SC-LP-SMC-98,
address = {San Diego, California, USA},
month = oct,
year = 1998,
publisher = {Argos Press},
acronym = {{SMC} 2000},
booktitle = {{P}roceedings of the {IEEE} {I}nternational
{C}onference on {S}ystems, {M}an and {C}ybernetics
({SMC} 2000)},
author = {Christensen, S{\o}ren and Petrucci, Laure},
title = {How to Determine and Use Place Flows in Coloured
{P}etri Nets},
pages = {66-71}
}
@phdthesis{THESE-CECE-98,
author = {C{\'e}c{\'e}, G{\'e}rard},
title = {V{\'e}rification, analyse et approximations
symboliques
des automates communicants},
year = {1998},
month = jan,
type = {Th{\`e}se de doctorat},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Cece-these.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Cece-these.ps},
lsv-lang = {FR}
}
@phdthesis{THESE-DUFOURD-98,
author = {Dufourd, Catherine},
title = {R{\'e}seaux de {P}etri avec
Reset{\slash}Transfert :
d{\'e}cidabilit{\'e} et ind{\'e}cidabilit{\'e}},
year = {1998},
month = oct,
type = {Th{\`e}se de doctorat},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Dufourd-these.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Dufourd-these.ps},
lsv-lang = {FR}
}
@techreport{alcatel-ComPad-98a,
author = {Comon, Hubert and Padovani, Vincent},
title = {Specifications Consistency Verification.
{I}ntermediate Report},
year = {1998},
month = sep,
type = {Contract Report},
number = {MAR/UAO/C/98/0051}
}
@techreport{alcatel-ComPad-98b,
author = {Comon, Hubert and Padovani, Vincent},
title = {Specifications Consistency Verification. {F}inal
Report},
year = {1998},
month = dec,
type = {Contract Report},
number = {MAR/UAO/C/98/0080},
note = {280 pages}
}
@article{bid-hen-acta-amast,
publisher = {Springer},
journal = {Acta Informatica},
author = {Bidoit, Michel and Hennicker, Rolf},
title = {Modular Correctness Proofs of Behavioural
Implementations},
volume = {35},
number = {11},
pages = {951-1005},
year = {1998},
month = nov,
doi = {10.1007/s002360050149}
}
@inproceedings{comon97csl,
address = {{\AA}rhus, Denmark},
year = 1998,
volume = 1414,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Nielsen, Mogens and Thomas, Wolfgang},
acronym = {{CSL}'97},
booktitle = {{S}elected {P}apers from the 11th {I}nternational
{W}orkshop on {C}omputer {S}cience {L}ogic
({CSL}'97)},
author = {Comon, Hubert and Jurski, Yan},
title = {Higher-order matching and tree automata},
pages = {157-176},
note = {Invited lecture},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComJur-csl97.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComJur-csl97.ps}
}
@article{comon97jsc1,
publisher = {Elsevier Science Publishers},
journal = {Journal of Symbolic Computation},
author = {Comon, Hubert},
title = {Completion of Rewrite Systems with Membership
Constraints. {P}art~{I}: {D}eduction Rules},
volume = {25},
number = {4},
pages = {397-420},
year = {1998},
month = apr,
optnote = {This is a first part of a paper whose abstract
appeared in Proc.\ {ICALP '92}, Vienna.},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Com-cirs1.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Com-cirs1.ps}
}
@article{comon97jsc2,
publisher = {Elsevier Science Publishers},
journal = {Journal of Symbolic Computation},
author = {Comon, Hubert},
title = {Completion of Rewrite Systems with Membership
Constraints. {P}art~{II}: {C}onstraint Solving},
volume = {25},
number = {4},
pages = {421-454},
year = {1998},
month = apr,
optnote = {This is the second part of a paper whose abstract
appeared in Proc.\ {ICALP '92}, Vienna.},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Com-cirs2.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Com-cirs2.ps}
}
@inproceedings{comon98cav,
address = {Vancouver, British Columbia, Canada},
month = jun,
year = 1998,
volume = 1427,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Hu, Alan J. and Vardi, Moshe Y.},
acronym = {{CAV}'98},
booktitle = {{P}roceedings of the 10th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'98)},
author = {Comon, Hubert and Jurski, Yan},
title = {Multiple Counters Automata, Safety Analysis and
{P}resburger Arithmetic},
pages = {268-279},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComJur-cav98.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComJur-cav98.ps}
}
@inproceedings{comon98lics,
address = {Indianapolis, Indiana, USA},
month = jun,
year = 1998,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'98},
booktitle = {{P}roceedings of the 13th
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'98)},
author = {Comon, Hubert and Narendran, Paliath and
Nieuwenhuis, Robert and Rusinowitch, Micha{\"e}l},
title = {Decision Problems in Ordered Rewriting},
pages = {276-286},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CNNR-lics98.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CNNR-lics98.ps}
}
@inproceedings{comon98rta,
address = {Tsukuba, Japan},
month = mar,
year = 1998,
volume = 1379,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Nipkow, Tobias},
acronym = {{RTA}'98},
booktitle = {{P}roceedings of the 9th {I}nternational
{C}onference on {R}ewriting {T}echniques
and {A}pplications
({RTA}'98)},
author = {Comon, Hubert},
title = {About proofs by consistency},
pages = {136-137},
note = {Invited lecture}
}
@inproceedings{demri98,
address = {Paris, France},
month = feb,
year = 1998,
volume = 1373,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Morvan, Michel and Meinel, {\relax Ch}ristoph and
Krob, Daniel},
acronym = {{STACS}'98},
booktitle = {{P}roceedings of the 15th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'98)},
author = {Demri, St{\'e}phane and Schnoebelen, {\relax Ph}ilippe},
title = {The Complexity of Propositional Linear Temporal Logics
in Simple Cases (Extended Abstract)},
pages = {61-72},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DemSch-stacs98.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DemSch-stacs98.ps},
doi = {10.1007/BFb0028549}
}
@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{forma98,
author = {Sifakis, Joseph},
editor = {Sifakis, Joseph},
title = {Action {FORMA}. {B}ilan de la premi{\`e}re ann{\'e}e},
year = {1998},
month = jan,
type = {Contract Report},
institution = {DSP-STTC/CNRS/MENRT},
lsv-lang = {FR}
}
@inproceedings{laroussinie98b,
address = {Paris, France},
month = nov,
year = 1998,
volume = 135,
series = {{IFIP} Conference Proceedings},
publisher = {Kluwer Academic Publishers},
editor = {Budkowski, Stanislaw and Cavalli, Ana R. and Najm, Elie},
acronym = {{FORTE'XI}/{PSTV'XVIII}},
booktitle = {{P}roceedings of {IFIP} {TC6} {WG6.1} {J}oint
{I}nternational {C}onference on {F}ormal {D}escription
{T}echniques for {D}istributed {S}ystems and
{C}ommunication {P}rotocols ({FORTE'XI}) and
{P}rotocol {S}pecification, {T}esting and
{V}erification ({PSTV'XVIII})},
author = {Laroussinie, Fran{\c{c}}ois and Larsen, Kim G.},
title = {{CMC}: {A}~Tool for Compositional Model-Checking of
Real-Time Systems},
pages = {439-456},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LarLar-forte98.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LarLar-forte98.ps}
}
@inproceedings{lf-mvp-latin-98,
address = {Campinas, Brasil},
month = apr,
year = 1998,
volume = 1380,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Lucchesi, Claudio L. and Moura, Arnaldo V.},
acronym = {{LATIN}'98},
booktitle = {{P}roceedings of the 3rd {L}atin {A}merican
{S}ymposium on {T}heoretical {I}nformatics
({LATIN}'98)},
author = {Veloso{ }Peixoto, Marcos and Fribourg, Laurent},
title = {Unfolding Parametric Automata},
pages = {88-101}
}
@inproceedings{lugiez98,
address = {Nice, France},
month = sep,
year = 1998,
volume = 1466,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Sangiorgi, Davide and de Simone, Robert},
acronym = {{CONCUR}'98},
booktitle = {{P}roceedings of the 9th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'98)},
author = {Lugiez, Denis and Schnoebelen, {\relax Ph}ilippe},
title = {The Regular Viewpoint on {PA}-Processes},
pages = {50-66},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LugSch-concur98.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LugSch-concur98.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LugSch-concur98.ps},
doi = {10.1007/BFb0055615}
}
@misc{phs-infinity98,
author = {Schnoebelen, {\relax Ph}ilippe},
title = {Regular Tree Languages for Process Algebra},
year = 1998,
month = jul,
howpublished = {Invited lecture, 3rd {I}nternational
{W}orkshop on {V}erification of {I}nfinite
{S}tate {S}ystems
({INFINITY}'98), Aalborg, Denmark}
}
@techreport{rap-icc-1,
author = {Laroussinie, Fran{\c{c}}ois},
title = {Analyse de l'{ICC}: mod{\'e}lisation},
year = {1998},
month = mar,
type = {Contract Report},
institution = {EDF/DER/MOS - LSV},
lsv-lang = {FR}
}
@techreport{rap-icc-2,
author = {Duflot, Marie and Markey, Nicolas},
title = {{\'E}valuation de l'outil {UPPAAL} sur le probl{\`e}me de
l'{ICC}},
year = {1998},
month = sep,
type = {Contract Report},
institution = {EDF/DER/MOS - LSV},
lsv-lang = {FR}
}
@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}
}
@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.