@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}
}
@misc{LP-cor-spin-99,
author = {Petrucci, Laure},
title = {{\scshape Promela} et {\scshape Spin} :
exercices corrig{\'e}s},
year = {1999},
missinghowpublished = {},
wrongurl = {http://www.lsv.ens-cachan.fr/~petrucci/cor_spin.ps.gz},
wrongpsgz = {http://www.lsv.ens-cachan.fr/~petrucci/cor_spin.ps.gz},
wrongps = {http://www.lsv.ens-cachan.fr/~petrucci/cor_spin.ps},
lsv-lang = {FR}
}
@misc{LP-cours-spin-99,
author = {Petrucci, Laure},
title = {Un exemple de langage parall{\`e}le asynchrone :
{\scshape Promela}},
year = {1999},
howpublished = {Polycopi{\'e} de cours, IEE, {\'E}vry, France},
wrongurl = {http://www.lsv.ens-cachan.fr/~petrucci/poly_spin.ps.gz},
wrongpsgz = {http://www.lsv.ens-cachan.fr/~petrucci/poly_spin.ps.gz},
wrongps = {http://www.lsv.ens-cachan.fr/~petrucci/poly_spin.ps},
lsv-lang = {FR}
}
@misc{LP-exos-spin-99,
author = {Petrucci, Laure},
title = {{\scshape Promela} et {\scshape Spin} : exercices},
year = {1999},
howpublished = {Polycopi{\'e}, IEE, {\'E}vry, France},
wrongurl = {http://www.lsv.ens-cachan.fr/~petrucci/exos_spin.ps.gz},
wrongpsgz = {http://www.lsv.ens-cachan.fr/~petrucci/exos_spin.ps.gz},
wrongps = {http://www.lsv.ens-cachan.fr/~petrucci/exos_spin.ps},
lsv-lang = {FR}
}
@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}
}
@techreport{LSV:99:5,
author = {Padovani, Vincent and Comon, Hubert and
Leneutre, J. and Tingaud, R.},
missingauthor = {},
title = {A Formal Verification of Telephone Supplementary
Service Interactions},
type = {Research Report},
number = {LSV-99-5},
year = {1999},
month = may,
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-5.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-1999-5.rr.ps}
}
@inproceedings{NWP-PASTE99,
address = {Toulouse, France},
month = sep,
year = 1999,
publisher = {ACM Press},
acronym = {{PASTE}'99},
booktitle = {{P}roceedings of the {ACM} {SIGPLAN}/{SIGSOFT}
{W}orkshop on {P}rogram {A}nalysis for
{S}oftware {T}ools and {E}ngineering
({PASTE}'99)},
author = {Williams{-}Preston, Nicky},
title = {New Type Signatures for Legacy {F}ortran
Subroutines},
pages = {76-85},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Pre-paste99.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Pre-paste99.ps}
}
@inproceedings{PB-AP-icalp99,
address = {Prague, Czech Republic},
month = jul,
year = 1999,
volume = 1644,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Wiedermann, Jir{\'i} and van Emde Boas, Peter and
Nielsen, Mogens},
acronym = {{ICALP}'99},
booktitle = {{P}roceedings of the 26th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming
({ICALP}'99)},
author = {Bouyer, Patricia and Petit, Antoine},
title = {Decomposition and Composition of Timed Automata},
pages = {210-219},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BP-icalp99.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BP-icalp99.ps},
abstract = {We propose in this paper a
decomposition theorem for the timed
automata introduced by Alur and Dill. To this
purpose, we define a new
simple and natural concatenation operation,
indexed by the set of
clocks to be reset, on timed automata
generalizing the classical
untimed concatenation. \par
Then we extend the famous Kleene's and B{\"u}chi's
theorems on classical
untimed automata by simply changing the basic
objects to take time
into account, keeping the union operation and
replacing the
concatenation, finite and infinite iterations by
the new timed
concatenations and their induced iterations.\par
Thus, and up to our knowledge, our result
provides the simplest known
algebraic characterization of recognizable timed
languages.}
}
@inproceedings{RM-PST-99,
address = {Williamsburg, Virginia, USA},
month = jun,
year = 1999,
publisher = {Kluwer Academic Publishers},
editor = {Yakovlev, Alex and Lavagno, Luciano},
acronym = {{HWPN}'99},
booktitle = {{P}roceedings of the 2nd {I}nternational
{W}orkshop on {H}ardware {D}esign and
{P}etri {N}ets
({HWPN}'99)},
author = {Meyer, Rapha{\"e}l and Thiagarajan, P. S.},
title = {{LTrL} Based Model-Checking for a Restricted Class
of Signal Transition Graphs},
pages = {3-14}
}
@techreport{alcatel-ComPad-99a,
author = {Comon, Hubert and Padovani, Vincent},
title = {Report on Specification Validation in
Telecommunication Services},
year = {1999},
month = jun,
type = {Contract Report},
missinginstitution = {}
}
@inproceedings{beauquier99,
address = {Bratislava, Slovak republic},
month = sep,
year = 1999,
volume = 1693,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Jayanti, Prasad},
acronym = {{DISC}'99},
booktitle = {{P}roceedings of the 13th {I}nternational
{S}ymposium on {D}istributed {C}omputing
({DISC}'99)},
author = {Beauquier, Joffroy and B{\'e}rard, B{\'e}atrice
and Fribourg, Laurent},
title = {A New Rewrite Method for Proving Convergence of
Self-Stabilizing Systems},
pages = {240-253},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBF-disc99.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBF-disc99.ps}
}
@inproceedings{berard99,
address = {Trento, Italy},
month = jul,
year = 1999,
volume = 1633,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Halbwachs, Nicolas and Peled, Doron},
acronym = {{CAV}'99},
booktitle = {{P}roceedings of the 11th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'99)},
author = {B{\'e}rard, B{\'e}atrice and Fribourg, Laurent},
title = {Automated Verification of a Parametric Real-Time
Program: {T}he {ABR} Conformance Protocol},
pages = {96-107},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BerFri-cav99.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BerFri-cav99.ps}
}
@inproceedings{berard99b,
address = {Eindhoven, The Netherlands},
month = aug,
year = 1999,
volume = 1664,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Baeten, Jos C. M. and Mauw, Sjouke},
acronym = {{CONCUR}'99},
booktitle = {{P}roceedings of the 10th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'99)},
author = {B{\'e}rard, B{\'e}atrice and Fribourg, Laurent},
title = {Reachability Analysis of (Timed) {P}etri Nets Using
Real Arithmetic},
pages = {178-193},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BerFri-concur99.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BerFri-concur99.ps}
}
@mastersthesis{blanc-dea,
author = {Blanc, Benjamin},
title = {Mod{\'e}lisation et sp{\'e}cification
d'architectures logicielles},
year = {1999},
month = sep,
type = {Rapport de {DEA}},
school = {{DEA} Programmation, Paris, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Bla-dea99.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Bla-dea99.ps},
lsv-lang = {FR}
}
@article{comon97cacm,
publisher = {Kluwer Academic Publishers},
journal = {Constraints},
author = {Comon, Hubert and Dincbas, Mehmet and
Jouannaud, Jean-Pierre and Kirchner, Claude},
title = {A Methodological View of Constraint Solving},
volume = {4},
number = {4},
pages = {337-361},
year = {1999},
month = dec,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Com-constraints.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Com-constraints.ps}
}
@inproceedings{comon99,
address = {Eindhoven, The Netherlands},
month = aug,
year = 1999,
volume = 1664,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Baeten, Jos C. M. and Mauw, Sjouke},
acronym = {{CONCUR}'99},
booktitle = {{P}roceedings of the 10th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'99)},
author = {Comon, Hubert and Jurski, Yan},
title = {Timed Automata and the Theory of Real Numbers},
pages = {242-257},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComJur-concur99.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComJur-concur99.ps}
}
@mastersthesis{cortier-dea,
author = {Cortier, V{\'e}ronique},
title = {V{\'e}rification de syst{\`e}mes {\`a} compteurs},
year = {1999},
month = sep,
type = {Rapport de {DEA}},
school = {{DEA} de Logique, Paris, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Cor-dea99.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Cor-dea99.ps},
lsv-lang = {FR}
}
@inproceedings{cortier-icalp99,
address = {Prague, Czech Republic},
month = jul,
year = 1999,
volume = 1644,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Wiedermann, Jir{\'i} and van Emde Boas, Peter and
Nielsen, Mogens},
acronym = {{ICALP}'99},
booktitle = {{P}roceedings of the 26th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming
({ICALP}'99)},
author = {Cortier, V{\'e}ronique and Ganzinger, Harald and
Jacquemard, Florent and Veanes, Margus},
title = {Decidable Fragments of Simultaneous Rigid
Reachability},
pages = {250-260},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CGJV-icalp99.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CGJV-icalp99.ps}
}
@book{docdor99,
author = {Schnoebelen, {\relax Ph}ilippe and
B{\'e}rard, B{\'e}atrice and Bidoit, Michel
and Laroussinie, Fran{\c{c}}ois and Petit, Antoine},
title = {V{\'e}rification de logiciels : techniques et
outils du model-checking},
year = {1999},
month = apr,
publisher = {Vuibert},
isbn = {2-7117-8646-3},
url = {http://www.vuibert.com/livre593.html},
lsv-lang = {FR}
}
@inproceedings{dufourd99,
address = {Prague, Czech Republic},
month = jul,
year = 1999,
volume = 1644,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Wiedermann, Jir{\'i} and van Emde Boas, Peter and
Nielsen, Mogens},
acronym = {{ICALP}'99},
booktitle = {{P}roceedings of the 26th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming
({ICALP}'99)},
author = {Dufourd, Catherine and Jan{\v c}ar, Petr and
Schnoebelen, {\relax Ph}ilippe},
title = {Boundedness of Reset {P/T} Nets},
pages = {301-310},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DJS-icalp99.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DJS-icalp99.ps},
abstract = {P/T nets with reset and transfer arcs can be seen as
counter-machines with some restricted set of
operations. Surprisingly, several problems related to
boundedness are harder for Reset nets than for the more
expressive Transfer nets. Our main result is that
boundedness is undecidable for nets with three reset
arcs, while it is decidable for nets with two resetable
places.}
}
@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}
}
@techreport{hcrt-disi99,
author = {Hu{\ss}mann, Heinrich and Cerioli, Maura and
Reggio, Gianna and Tort, Fran{\c{c}}oise},
title = {Abstract Data Types and {UML} Models},
type = {Technical Report},
number = {DISI-TR-99-15},
year = {1999},
missingmonth = {},
missingnmonth = {},
institution = {DISI, Universit{\'a} di Genova, Italy}
}
@phdthesis{jurski99,
author = {Jurski, Yan},
title = {Expression de la relation binaire d'accessibilit{\'e}
pour les automates {\`a} compteurs plats et les automates
temporis{\'e}s},
year = {1999},
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/Jurski-these.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Jurski-these.ps},
lsv-lang = {FR}
}
@inproceedings{laroussinie99,
address = {Szklarska Poreba, Poland},
month = sep,
year = 1999,
volume = 1672,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Kutylowski, Miroslaw and Pacholski, Leszek and
Wierzbicki, Tomasz},
acronym = {{MFCS}'99},
booktitle = {{P}roceedings of the 24th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'99)},
author = {Aceto, Luca and Laroussinie, Fran{\c{c}}ois},
title = {Is your Model Checker on Time?},
pages = {125-136},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/AceLar-mfcs99.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/AceLar-mfcs99.ps}
}
@mastersthesis{leroux-dea,
author = {Leroux, J{\'e}r{\^o}me},
title = {V{\'e}rification des syst{\`e}mes param{\'e}tr{\'e}s},
year = {1999},
month = sep,
type = {Rapport de {DEA}},
school = {{DEA} Algorithmique, Paris, France},
lsv-lang = {FR}
}
@inproceedings{mb-don-at-amast98,
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 = {Bidoit, Michel and Sannella, Donald and Tarlecki, Andrzej},
title = {Architectural Specifications in {CASL}},
pages = {341-357},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ECS-LFCS-99-407.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ECS-LFCS-99-407.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ECS-LFCS-99-407.ps}
}
@inproceedings{mb-rh-amast98,
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 = {Hennicker, Rolf and Bidoit, Michel},
title = {Observational Logic},
pages = {263-277},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MB-RH-amast99.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MB-RH-amast99.ps}
}
@inproceedings{mb-rolf-fm99,
address = {Toulouse, France},
month = sep,
year = 1999,
optaddress = {Bucharest, Romania},
publisher = {Theta, Bucharest, Romania},
editor = {Futatsugi, Kokichi and Goguen, Joseph and Meseguer, Jos{\'e}},
acronym = {{FM}'99},
booktitle = {{P}roceedings of the {OBJ}/{C}afe{OBJ}/{M}aude
{W}orkshop at {F}ormal {M}ethods
({FM}'99)},
author = {Bidoit, Michel and Hennicker, Rolf},
title = {Observer Complete Definitions are Behaviourally
Coherent},
pages = {83-94},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CafeOBJ.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CafeOBJ.ps}
}
@phdthesis{meyer-these99,
author = {Meyer, Rapha{\"e}l},
title = {Contributions {\`a} l'{\'e}tude des logiques temporelles sur
les traces},
year = {1999},
month = nov,
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/Meyer-these.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Meyer-these.ps},
lsv-lang = {FR}
}
@incollection{proofsystems,
author = {Bidoit, Michel and Cengarle, Mar{\'\i}a Victoria and
Hennicker, Rolf},
title = {Proof systems for structured specifications and their
refinements},
editor = {Astesiano, Egidio and Kreowski, Hans-J{\"o}rg and
Krieg-Br{\"u}ckner, Bernd},
booktitle = {Algebraic Foundations of Systems Specification},
type = {chapter},
chapter = {11},
pages = {385-433},
year = {1999},
missingmonth = {},
missingnmonth = {},
publisher = {Springer},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ch11AFSSbook.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ch11AFSSbook.ps}
}
@article{schnoebelen99,
publisher = {European Association for
Theoretical Computer Science},
journal = {EATCS Bulletin},
author = {Schnoebelen, {\relax Ph}ilippe},
title = {Decomposable Regular Languages and the Shuffle
Operator},
volume = {67},
pages = {283-289},
year = {1999},
month = feb,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Sch-BEATCS99.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Sch-BEATCS99.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sch-BEATCS99.pdf}
}
@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{sutre99b,
address = {Cachan, France},
month = mar,
year = 1999,
publisher = {Herm{\`e}s},
editor = {Lesage, Jean-Jacques},
acronym = {{MSR}'99},
booktitle = {{A}ctes du 2{\`e}me {C}ongr{\`e}s sur la
{M}od{\'e}lisation des {S}yst{\`e}mes
{R}{\'e}actifs
({MSR}'99)},
author = {Sutre, Gr{\'e}goire},
title = {V{\'e}rification des automates {\`a} file r{\'e}actifs : un
mod{\`e}le pour les syst{\'e}mes r{\'e}actifs {\'e}crits en
{E}lectre},
pages = {71-78},
lsv-lang = {FR}
}
@inproceedings{tbhw-uml99,
address = {Fort Collins, Colorado, USA},
month = oct,
year = 1999,
volume = 1723,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {France, Robert B. and Rumpe, Bernhard},
acronym = {{UML}'99},
booktitle = {{P}roceedings of the 2nd {I}nternational
{C}onference on the {U}nified {M}odeling
{L}anguage
({UML}'99)},
author = {Bidoit, Michel and Hennicker, Rolf and
Tort, Fran{\c{c}}oise and Wirsing, Martin},
title = {Correct Realization of Interface Constraints with
{OCL}},
pages = {399-415},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/TBHW-uml99.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/TBHW-uml99.ps}
}
@mastersthesis{turuani-dea,
author = {Turuani, Mathieu},
title = {Logique temporelle temporis{\'e}e pour la v{\'e}rification
de programmes : expressivit{\'e} et complexit{\'e}},
year = {1999},
month = sep,
type = {Rapport de {DEA}},
school = {{DEA} Programmation, Paris, France},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-1999-8.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-1999-8.rr.ps},
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.