@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.*