@inproceedings{BCFL-gdv04,
  address = {Boston, Massachusetts, USA},
  month = feb,
  year = {2005},
  number = 1,
  volume = 119,
  series = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier Science Publishers},
  editor = {De Alfaro, Luca},
  acronym = {{GDV}'04},
  booktitle = {{P}roceedings of the {W}orkshop on
               {G}ames in {D}esign and {V}erification
               ({GDV}'04)},
  author = {Bouyer, Patricia and Cassez, Franck and 
                 Fleury, Emmanuel and 
                 Larsen, Kim G.},
  title = {Synthesis of Optimal Strategies Using {HyTech}},
  pages = {11-31},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFL-gdv04.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFL-gdv04.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCFL-gdv04.ps},
  doi = {10.1016/j.entcs.2004.07.006},
  abstract = {Priced timed (game) automata extend timed 
	(game) automata with costs on both locations and 
	transitions. The problem of synthesizing an optimal 
	winning strategy for a priced timed game under some 
	hypotheses has been shown decidable in~[BCFL04]. In this 
	paper, we present an algorithm for computing the optimal 
	cost and for synthesizing an optimal strategy in case 
	there exists one. We also describe the implementation of 
	this algorithm with the tool HyTech and present an 
	example. }
}
@article{ComonCortier-TCS1,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Comon, Hubert and Cortier, V{\'e}ronique},
  title = {Tree Automata with One Memory, Set Constraints and
                 Cryptographic Protocols},
  year = {2005},
  volume = 331,
  number = 1,
  pages = {143-214},
  month = feb,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComonCortierTCS1.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComonCortierTCS1.ps},
  doi = {10.1016/j.tcs.2004.09.036}
}
@inproceedings{DFH-avocs2004,
  address = {London, UK},
  month = may,
  year = {2005},
  number = 6,
  volume = {128},
  series = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier Science Publishers},
  editor = {Huth, Michael R. A.},
  acronym = {{AVoCS}'04},
  booktitle = {{P}roceedings of the 4th {I}nternational
               {W}orkshop on {A}utomated {V}erification
               of {C}ritical {S}ystems
               ({AVoCS}'04)},
  author = {Duflot, Marie and Fribourg, Laurent and 
                 H{\'e}rault, {\relax Th}omas and 
                 Lassaigne, Richard and Magniette, Fr{\'e}d{\'e}ric 
                 and Messika, St{\'e}phane and
                 Peyronnet, Sylvain and Picaronny, Claudine},
  title = {Probabilistic Model Checking of the {CSMA/CD} Protocol
                 Using {PRISM} and {APMC}},
  pages = {195-214},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DFH-avocs2004.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DFH-avocs2004.pdf},
  doi = {10.1016/j.entcs.2005.04.012}
}
@inproceedings{DFV-avocs04,
  address = {London, UK},
  month = may,
  year = {2005},
  number = 6,
  volume = {128},
  series = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier Science Publishers},
  editor = {Huth, Michael R. A.},
  acronym = {{AVoCS}'04},
  booktitle = {{P}roceedings of the 4th {I}nternational
               {W}orkshop on {A}utomated {V}erification
               of {C}ritical {S}ystems
               ({AVoCS}'04)},
  author = {Darlot, {\relax Ch}ristophe and Finkel, Alain and Van{~}Begin, Laurent},
  title = {About {F}ast and {TReX} Accelerations},
  pages = {87-103},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DFV-avocs04.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DFV-avocs04.pdf},
  doi = {10.1016/j.entcs.2005.04.006}
}
@inproceedings{FGRV-express04,
  address = {London, UK},
  month = apr,
  year = 2005,
  number = 2,
  volume = 128,
  series = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier Science Publishers},
  editor = {Baeten, Jos and Corradini, Flavio},
  acronym = {{EXPRESS}'04},
  booktitle = {{P}roceedings of the 11th {I}nternational
               {W}orkshop on {E}xpressiveness in
               {C}oncurrency
               ({EXPRESS}'04)},
  author = {Finkel, Alain and Geeraerts, Gilles and Raskin, Jean-Fran{\c{c}}ois and
                 Van{~}Begin, Laurent},
  title = {On the Omega-Language Expressive Power of Extended
                 {P}etri Nets},
  pages = {87-101},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGRV-express04.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGRV-express04.pdf},
  doi = {10.1016/j.entcs.2004.11.030}
}
@article{FL-IPL04,
  publisher = {Elsevier Science Publishers},
  journal = {Information Processing Letters},
  author = {Finkel, Alain and Leroux, J{\'e}r{\^o}me},
  title = {The Convex Hull of a Regular Set of Integer Vectors is 
		  Polyhedral and Effectively Computable},
  year = {2005},
  month = oct,
  volume = 96,
  number = 1,
  pages = {30-35},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FL-ipl05.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FL-ipl05.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FL-ipl05.ps},
  doi = {10.1016/j.ipl.2005.04.004},
  abstract = {Number Decision Diagrams (NDD) 
	provide a natural finite symbolic representation 
	for regular set of integer vectors encoded as 
	strings of digit vectors (least or most 
	significant digit first). The convex hull of the 
	set of vectors represented by a~NDD is proved to 
	be an effectively computable convex 
	polyhedron.}
}
@article{GLRV:acm,
  publisher = {Elsevier Science Publishers},
  journal = {Journal of Logic and Algebraic Programming},
  author = {Goubault{-}Larrecq, Jean and Roger, Muriel and 
                  Verma, Kumar N.},
  title = {Abstraction and Resolution Modulo~{AC}: {H}ow to 
                  Verify
                 {D}iffie-{H}ellman-like Protocols Automatically},
  volume = 64,
  number = 2,
  pages = {219-251},
  year = {2005},
  month = aug,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GLRV-acm.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GLRV-acm.ps},
  doi = {10.1016/j.jlap.2004.09.004}
}
@article{JGL:val:ext,
  publisher = {Cambridge University Press},
  journal = {Mathematical Structures in Computer Science},
  author = {Goubault{-}Larrecq, Jean},
  title = {Extensions of Valuations},
  year = {2005},
  volume = 15,
  number = 2,
  pages = {271-297},
  month = apr,
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2002-17.rr.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
		  rr-lsv-2002-17.rr.ps},
  doi = {10.1017/S096012950400461X}
}
@inproceedings{KremerRyan2004,
  address = {London, UK},
  month = may,
  year = 2005,
  number = 5,
  volume = {128},
  series = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier Science Publishers},
  editor = {Focardi, Riccardo and Zavattaro, Gianluigi},
  acronym = {{SecCo}'04},
  booktitle = {{P}roceedings of the 2nd {I}nternational
               {W}orkshop on {S}ecurity {I}ssues in
               {C}oordination {M}odels, {L}anguages and
               {S}ystems ({SecCo}'04)},
  author = {Kremer, Steve and Ryan, Mark D.},
  title = {Analysing the Vulnerability of Protocols to Produce 
                  Known-pair and Chosen-text Attacks},
  pages = {84-107},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Kremer-secco04.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Kremer-secco04.pdf},
  doi = {10.1016/j.entcs.2004.11.043},
  abstract = {In this paper we report on an analysis 
	for finding known-pair and chosen-text attacks in 
	protocols. As these attacks are at the level of 
	blocks, we extend the attacker by special capabilities 
	related to block chaining techniques. The analysis is 
	automated using Blanchet's protocol verifier and 
	illustrated on two well-known protocols, the 
	Needham-Schroeder-Lowe public-key protocol as well as 
	the Needham-Schroeder symmetric-key protocol. On the 
	first protocol, we show how the special intruder 
	capabilities related to chaining may compromise the 
	secrecy of nonces and that chosen-ciphertext attacks 
	are possible. We propose two modified versions of the 
	protocol which strengthen its security. We then 
	illustrate known-pair and chosen-plaintext attacks on 
	the second protocol.}
}
@inproceedings{couvreur-ciaa04,
  address = {Kingston, Ontario, Canada},
  month = jan,
  year = 2005,
  volume = 3317,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Domaratzki, Michael and Okhotin, Alexander and 
		  Salomaa, Kai and Yu, Sheng},
  acronym = {{CIAA}'04},
  booktitle = {{R}evised {S}elected {P}apers of the 9th {I}nternational 
               {C}onference on {I}mplementation and
               {A}pplication of {A}utomata
               ({CIAA}'04)},
  author = {Couvreur, Jean-Michel},
  title = {A {BDD}-like Implementation of an Automata Package},
  pages = {310-311},
  doi = {10.1007/b105090}
}
@article{ABRS-lossy,
  publisher = {Elsevier Science Publishers},
  journal = {Information and Computation},
  author = {Abdulla, Parosh Aziz and Bertrand, Nathalie and 
	    Rabinovich, Alexander and Schnoebelen, {\relax Ph}ilippe},
  title = {Verification of Probabilistic Systems with Faulty
	   Communication},
  year = 2005,
  month = nov,
  volume = 202,
  number = 2,
  pages = {141-165},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/InfComp-ABRS.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/InfComp-ABRS.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/InfComp-ABRS.ps},
  doi = {10.1016/j.ic.2005.05.008},
  abstract = {Many protocols are designed to 
	operate correctly even in the case where the 
	underlying communication medium is faulty. To 
	capture the behavior of such protocols, 
	\emph{Lossy Channel Systems}~(LCS's) have been 
	proposed. In an LCS the communication channels 
	are modeled as unbounded FIFO buffers which are 
	unreliable in the sense that they can 
	nondeterministically lose messages. \par
	Recently, several attempts have been made to 
	study \emph{Probabilistic Lossy Channel 
	Systems}~(PLCS's) in which the probability of 
	losing messages is taken into account. In this 
	article, we consider a variant of PLCS's which 
	is more realistic than those studied 
	previously. More precisely, we assume that 
	during each step in the execution of the 
	system, each message may be lost with a certain 
	predefined probability. We show that for such 
	systems the following model-checking problem is 
	decidable: to verify whether a linear-time 
	property definable by a finite-state 
	\(\omega\)-automaton holds with probability one. 
	We also consider other types of faulty 
	behavior, such as corruption and duplication of 
	messages, and insertion of new messages, and 
	show that the decidability results extend to 
	these models.}
}
@inproceedings{baudet-ccs2005,
  address = {Alexandria, Virginia, USA},
  month = nov,
  year = 2005,
  publisher = {ACM Press},
  acronym = {{CCS}'05},
  booktitle = {{P}roceedings of the 12th {ACM} {C}onference
               on {C}omputer and {C}ommunications {S}ecurity
               ({CCS}'05)},
  author = {Baudet, Mathieu},
  title = {Deciding Security of Protocols against Off-line Guessing 
		Attacks},
  pages = {16-25},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Baudet_CCS05revised.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Baudet_CCS05revised.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Baudet_CCS05revised.ps},
  doi = {10.1145/1102120.1102125},
  abstract = {We provide an effective procedure for 
	deciding the existence of off-line guessing attacks 
	on security protocols, for a bounded number of 
	sessions.\par
	The procedure consists of a constraint solving 
	algorithm for determining satisfiability and 
	equivalence of a class of second-order E-unification 
	problems, where the equational theory~E is presented 
	by a convergent subterm rewriting system.\par
	To the best of our knowledge, this is the first 
	decidability result to use the generic definition of 
	off-line guessing attacks due to Corin~\emph{et al.} 
	based on static equivalence in the applied 
	pi-calculus.}
}
@inproceedings{BCM05-fsttcs,
  address = {Hyderabad, India},
  month = dec,
  year = 2005,
  volume = 3821,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Ramanujam, R. and Sen, Sandeep},
  acronym = {{FSTTCS}'05},
  booktitle = {{P}roceedings of the 25th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'05)},
  author = {Bouyer, Patricia and Chevalier, Fabrice and
                 Markey, Nicolas},
  title = {On the Expressiveness of {TPTL} and~{MTL}},
  pages = {432-443},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCM-fsttcs05.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCM-fsttcs05.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCM-fsttcs05.ps},
  doi = {10.1007/11590156_35},
  abstract = {TPTL and MTL are two classical timed extensions of LTL.
    In this paper, we positively answer a 15-year-old conjecture that TPTL
    is strictly more expressive than MTL. But we show that, surprisingly,
    the TPTL formula proposed by Alur and Henzinger for witnessing 
    this conjecture can be expressed in MTL. More generally, we show that 
    TPTL formulae using only the F modality can be translated into MTL.}
}
@inproceedings{BFLS05-atva,
  address = {Taipei, Taiwan},
  month = oct,
  year = {2005},
  volume = 3707,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Peled, Doron A. and Tsay, Yih-Kuen},
  acronym = {{ATVA}'05},
  booktitle = {{P}roceedings of the 3rd {I}nternational
               {S}ymposium on {A}utomated {T}echnology
               for {V}erification and {A}nalysis
               ({ATVA}'05)},
  author = {Bardin, S{\'e}bastien and Finkel, Alain and
		Leroux, J{\'e}r{\^o}me and Schnoebelen, {\relax Ph}ilippe},
  title = {Flat acceleration in symbolic model checking},
  pages = {474-488},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFLS05-atva.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFLS05-atva.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BFLS05-atva.ps},
  doi = {10.1007/11562948_35},
  abstract = {Symbolic model checking provides partially 
	effective verification procedures that can handle systems 
	with an infinite state space. So-called {"}acceleration 
	techniques{"} enhance the convergence of fixpoint 
	computations by computing the transitive closure of some 
	transitions. In this paper we develop a new framework for 
	symbolic model checking with accelerations. We also propose 
	and analyze new symbolic algorithms using accelerations to 
	compute reachability sets.}
}
@inproceedings{BBGRS-ETFA05,
  address = {Catania, Italy},
  month = sep,
  year = 2005,
  publisher = {{IEEE} Industrial Electronics Society},
  editor = {Lo Bello, Lucia and Sauter, Thilo},
  acronym = {{ETFA}'05},
  booktitle = {{P}roceedings of the 10th {IEEE} {I}nternational 
	{C}onference on {E}merging {T}echnologies and {F}actory 
	{A}utomation ({ETFA}'05)},
  author = {Bel{ }mokadem, Houda and B{\'e}rard, B{\'e}atrice and
		 Gourcuff, Vincent and Roussel, Jean-Marc and
		 De{~}Smet, Olivier},
  title = {Verification of a timed multitask system with {U}ppaal},
  pages = {347-354},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ETFA05-FV.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ETFA05-FV.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ETFA05-FV.ps},
  abstract = {Since it is an important issue for users and system designers,
  verification of PLC programs has already been studied in various
  contexts, mostly for untimed programs. More recently, timed features
  were introduced and modeled with timed automata. In this case study,
  we consider a part of the so-called MSS (Mecatronic Standard System)
  platform from Bosh Group, a framework where time aspects are
  combined with multitask programming.  Our model for station~2 of the
  MSS platform is a network of timed automata, including automata for
  the operative part and for the control program, written in
  \emph{Ladder Diagram}. This model is constrained with atomicity
  hypotheses concerning program execution and model
  checking of a reaction time property is performed with the 
  tool~{\scshape Uppaal}.}
}
@inproceedings{BC-icmtd05,
  address = {Giens, France},
  nmnote = {Informal proceedings. Selected papers to appear in a journal},
  month = may,
  year = 2005,
  acronym = {{ICMTD}'05},
  booktitle = {Proceedings of the 1st {I}nternational {C}onference on
   	      {M}emory {T}echnology and {D}esign
	      ({ICMTD}'05)},
  author = {Baclet, Manuel and Chevallier, R{\'e}my},
  title = {Timed Verification of the {SPSMALL} Memory},
  pages = {89-92},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC05-spsmall.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC05-spsmall.pdf},
  abstract = {The aim of the paper is to verify a small 
	synchronous memory component with the real-time
	model checker Uppaal, taking into account the 
	electrical propagation delays through gates and 
	along wires.},
  missingdoi = {}
}
@inproceedings{BH-ICTAC05,
  address = {Hanoi, Vietnam},
  month = oct,
  year = 2005,
  volume = 3722,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Hung, Dang Van and Wirsing, Martin},
  acronym = {{ICTAC}'05},
  booktitle = {{P}roceedings of the 2nd {I}nternational {C}olloquium on
	{T}heoretical {A}spects of {C}omputing ({ICTAC}'05)},
  author = {Bidoit, Michel and Hennicker, Rolf},
  title = {Externalized and Internalized Notions of Behavioral 
		Refinement},
  pages = {334-350},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ictac05-ID128.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ictac05-ID128.pdf},
  doi = {10.1007/11560647_22},
  abstract = {Many different behavioral refinement notions for algebraic
specifications have been proposed in the literature but the relationship
between the various concepts is still unclear. In this paper we provide a
classification and a comparative study of behavioral refinements according
to two directions, the externalized approach which uses an explicit
behavioral abstraction operator that is applied to the specification to
be implemented, and the internalized approach which uses a built-in
behavioral semantics of specifications. We show that both concepts are
equivalent under suitable conditions. The formal basis of our study is
provided by the COL institution (constructor-based observational logic).
Hence, as a side-effect of our study on internalized behavioral refinements,
we introduce also a novel concept of behavioral refinement for
COL-specifications.}
}
@misc{bouyer-jsi05,
  author = {Bouyer, Patricia},
  title = {Timed Automata and Extensions: Decidability Limits},
  year = 2005,
  month = mar,
  howpublished = {Invited talk, 5{\`e}mes Journ{\'e}es Syst{\`e}mes Infinis ({JSI}'05), 
		Cachan, France}
}
@misc{bouyer-games05,
  author = {Bouyer, Patricia},
  title = {Synthesis of Timed Systems},
  year = 2005,
  month = mar,
  howpublished = {Invited lecture, Spring School on Infinite Games and 
		Their Applications, Bonn, Germany}
}
@misc{bouyer-gdv05,
  author = {Bouyer, Patricia},
  title = {Partial Observation of Timed Systems},
  year = 2005,
  month = jul,
  howpublished = {Invited talk, 2nd Workshop on Games in Design and 
		Verification, Edinburgh, Scotland}
}
@misc{gastin-wpv05,
  author = {Gastin, Paul},
  title = {On the synthesis of distributed controllers},
  year = 2005,
  month = nov,
  howpublished = {Invited talk, Workshop Perspectives in  
		Verification, in honor of Wolfgang Thomas on the occasion of his
                Doctorate Honoris Causa, Cachan, France}
}
@inproceedings{BCD-fossacs05,
  address = {Edinburgh, Scotland, UK},
  month = apr,
  year = 2005,
  volume = 3441,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Sassone, Vladimiro},
  acronym = {{FoSSaCS}'05},
  booktitle = {{P}roceedings of the 8th {I}nternational 
               {C}onference on {F}oundations of {S}oftware {S}cience
               and {C}omputation {S}tructures
               ({FoSSaCS}'05)},
  author = {Bouyer, Patricia and Chevalier, Fabrice and D'Souza, Deepak},
  title = {Fault Diagnosis Using Timed Automata},
  pages = {219-233},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/fossacs05-BCD.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/fossacs05-BCD.ps},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/fossacs05-BCD.pdf},
  doi = {10.1007/b106850},
  abstract = {Fault diagnosis consists in 
	observing behaviours of systems, and in detecting 
	online whether an error has occurred or not. In the 
	context of discrete event systems this problem has 
	been well-studied, but much less work has been done 
	in the timed framework. In this paper, we consider 
	the problem of diagnosing faults in behaviours of 
	timed plants. We focus on the problem of 
	synthesizing fault diagnosers which are realizable 
	as deterministic timed automata, with the 
	motivation that such diagnosers would function as 
	efficient online fault detectors. We study two 
	classes of such mechanisms, the class of 
	deterministic timed automata~(DTA) and the class of 
	event-recording timed automata~(ERA). We show that 
	the problem of synthesizing diagnosers in each of 
	these classes is decidable, provided we are given a 
	bound on the resources available to the diagnoser. 
	We prove that under this assumption diagnosability 
	is 2EXPTIME-complete in the case of DTA's whereas 
	it becomes PSPACE-complete for ERA's.}
}
@inproceedings{BBBL-concur2005,
  address = {San Francisco, California, USA},
  month = aug,
  year = 2005,
  volume = 3653,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Abadi, Mart{\'\i}n and de Alfaro, Luca},
  acronym = {{CONCUR}'05},
  booktitle = {{P}roceedings of the 16th 
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'05)},
  author = {Bel{ }mokadem, Houda and B{\'e}rard, B{\'e}atrice and 
		 Bouyer, Patricia and Laroussinie, Fran{\c{c}}ois},
  title = {A New Modality for Almost Everywhere Properties in 
	 	 Timed Automata},
  pages = {110-124},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBL05-concur.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBL05-concur.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBBL05-concur.ps},
  doi = {10.1007/11539452_12},
  abstract = {The context of this study is timed temporal logics 
	for timed automata. In this paper, we propose an extension of the 
	classical logic TCTL with a new Until modality, called {"}Until 
	almost everywhere{"}. In the extended logic, it is possible, for 
	instance, to express that a property is true at all positions of 
	all runs, except on a negligible set of positions. Such 
	properties are very convenient, for example in the framework of 
	boolean program verification, where transitions result from 
	changing variable values. We investigate the expressive power of 
	this modality and in particular, we prove that it cannot be 
	expressed with classical TCTL modalities. However, we show that 
	model-checking the extended logic remains PSPACE-complete as 
	for~TCTL.}
}
@inproceedings{BCL-concur2005,
  address = {San Francisco, California, USA},
  month = aug,
  year = 2005,
  volume = 3653,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Abadi, Mart{\'\i}n and de Alfaro, Luca},
  acronym = {{CONCUR}'05},
  booktitle = {{P}roceedings of the 16th 
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'05)},
  author = {Bouyer, Patricia and Cassez, Franck and Laroussinie, 
		  Fran{\c{c}}ois},
  title = {Modal Logics for Timed Control},
  pages = {81-94},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCL05-concur.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCL05-concur.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCL05-concur.ps},
  doi = {10.1007/11539452_10},
  abstract = {In this paper we use the timed 
	modal logic \(L_{\nu}\) to specify control 
	objectives for timed plants. We show that the 
	control problem for a large class of objectives 
	can be reduced to a model-checking problem for 
	an extension (\(L_{\nu}^{\mathrm{\small cont}}\)) 
	of the logic \(L_{\nu}\) with a new modality.
	\par
	More precisely we define a fragment of~\(L_{\nu}\),
	namely \(L_{\nu}^{\mathrm{\small det}}\), 
	such that any control objective 
	of~\(L_{\nu}^{\mathrm{\small det}}\)
	can be translated into an \(L_{\nu}^{\mathrm{\small cont}}\) 
	formula that holds for the plant if and only if 
	there is a controller that can enforce the 
	control objective.
	\par
	We also show that the new modality
	of~\(L_{\nu}^{\mathrm{\small cont}}\)
	strictly increases the expressive power 
	of~\(L_{\nu}\), while model-checking 
	of~\(L_{\nu}^{\mathrm{\small cont}}\) remains 
	EXPTIME-complete. }
}
@inproceedings{BLR-formats2005,
  address = {Uppsala, Sweden},
  month = nov,
  year = 2005,
  volume = 3829,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Pettersson, Paul and Yi, Wang},
  acronym = {{FORMATS}'05},
  booktitle = {{P}roceedings of the 3rd {I}nternational {C}onference
           on {F}ormal {M}odelling and {A}nalysis of {T}imed
           {S}ystems ({FORMATS}'05)},
  author = {Bouyer, Patricia and Laroussinie, Fran{\c{c}}ois and 
		Reynier, Pierre-Alain},
  title = {Diagonal Constraints in Timed Automata: Forward 
		Analysis of Timed Systems},
  pages = {112-126},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLR05-DBM.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLR05-DBM.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BLR05-DBM.ps},
  doi = {10.1007/11603009_10},
  abstract = {Timed automata (TA) are a 
	widely used model for real-time systems. Several 
	tools are dedicated to this model, and they mostly 
	implement a forward analysis for checking 
	reachability properties. Though diagonal 
	constraints do not add expressive power to 
	classical~TA, the standard forward analysis 
	algorithm is not correct for this model. In this 
	paper we survey several approaches to handle 
	diagonal constraints and propose a 
	refinement-based method for patching the usual 
	algorithm: erroneous traces found by the classical 
	algorithm are analyzed, and used for refining the 
	model.}
}
@inproceedings{BCK-ICALP2005,
  address = {Lisboa, Portugal},
  month = jul,
  year = 2005,
  volume = {3580},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Caires, Lu{\'\i}s and Italiano, Giuseppe F. and
	    Monteiro, Lu{\'\i}s and Palamidessi, Catuscia and Yung, Moti},
  acronym = {{ICALP}'05},
  booktitle = {{P}roceedings of the 32nd {I}nternational 
               {C}olloquium on {A}utomata, {L}anguages and 
               {P}rogramming
               ({ICALP}'05)},
  author = {Baudet, Mathieu and Cortier, V{\'e}ronique and Kremer,Steve},
  title = {Computationally Sound Implementations of Equational 
		 Theories against Passive Adversaries},
  pages = {652-663},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCK-icalp05.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCK-icalp05.pdf},
  doi = {10.1007/11523468_53},
  abstract = {In this paper we study the link between formal and
    cryptographic models for security protocols in the presence of a passive
    adversary. In contrast to other works, we do not consider a fixed set of
    primitives but aim at results for an arbitrary equational theory. We
    define a framework for comparing a cryptographic implementation and its
    idealization w.r.t.\ various security notions. In particular, we
    concentrate on the computationnal soundness of static equivalence, a
    standard tool in cryptographic \(\pi\)-calculi. We present a soundness
    criterion, which for many theories is not only sufficient but also
    necessary. Finally, we establish new soundness results for the Exclusive
    Or, as well as a theory of ciphers and lists.}
}
@book{lncs3426,
  editor = {Bouyssonouse, Bruno and Sifakis, Joseph},
  title = {Embedded Systems Design: The {ARTIST} Roadmap for Research and 
		Development},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  volume = 3436,
  year = 2005,
  url = {http://www.springer.com/978-3-540-25107-3},
  olderurl = {http://www.springer.de/cgi-bin/search_book.pl?isbn=3-540-25107-3},
  isbn = {3-540-25107-3},
  doi = {10.1007/b106761}
}
@inproceedings{ComDel-rta2005,
  address = {Nara, Japan},
  month = apr,
  year = 2005,
  volume = 3467,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Giesl, J{\"u}rgen},
  acronym = {{RTA}'05},
  booktitle = {{P}roceedings of the 16th {I}nternational
               {C}onference on {R}ewriting {T}echniques
               and {A}pplications
               ({RTA}'05)},
  author = {Comon{-}Lundh, Hubert and Delaune, St{\'e}phanie},
  title = {The finite variant property: {H}ow to get rid of some 
	 	 algebraic properties},
  pages = {294-307},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/rta05-CD.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/rta05-CD.ps},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/rta05-CD.pdf},
  doi = {10.1007/b135673},
  abstract = {We consider the following problem: Given a term
             \(t\), a rewrite system \(\mathcal{R}\), a finite set
             of equations \(E'\) such that \(\mathcal{R}\) is
             convergent modulo~\(E'\), compute finitely many
             instances of~\(t\): \(t_1,\ldots,t_n\) such that, for
             every substitution~\(\sigma\), there is an index
             \(i\) and a substitution~\(\theta\) such that \(
             t\sigma\mathord{\downarrow}=_{E'} t_i\theta\) (where
             \(t\sigma\mathord{\downarrow}\) is the normal form of
             \(t\sigma\) w.r.t.~\(\mathcal{R}/E'\)). \par 

             The goal of this paper is to give equivalent (resp.
             sufficient) conditions for the finite variant
             property and to systematically investigate this
             property for equational theories, which are relevant
             to security protocols verification. For instance, we
             prove that the finite variant property holds for
             Abelian Groups, and a theory of modular
             exponentiation and does not hold for the
             theory~\textit{ACUNh} (Associativity, Commutativity,
             Unit, Nilpotence, homomorphism).}
}
@article{CF-icomp05,
  publisher = {Elsevier Science Publishers},
  journal = {Information and Computation},
  author = {C{\'e}c{\'e}, G{\'e}rard and Finkel, Alain},
  title = {Verification of Programs with Half-Duplex Communication},
  year = 2005,
  month = nov,
  volume = 202,
  number = 2,
  pages = {166-190},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CF-icomp05.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CF-icomp05.pdf},
  doi = {10.1016/j.ic.2005.05.006},
  abstract = {We consider the analysis of infinite 
	\emph{half-duplex systems} made of finite state machines 
	that communicate over unbounded channels. The 
	half-duplex property for two machines and two 
	channels (one in each direction) says that each 
	reachable configuration has at most one channel 
	non-empty. We prove in this paper that such 
	half-duplex systems have a recognizable 
	reachability set. We show how to compute, in 
	polynomial time, a symbolic representation of this 
	reachability set and how to use that description to 
	solve several verification problems. Furthermore, 
	though the model of communicating finite state 
	machines is Turing-powerful, we prove that 
	membership of the class of half-duplex systems is 
	decidable. Unfortunately, the natural 
	generalization to systems with more than two 
	machines is Turing-powerful. We also prove that the 
	model-checking of those systems against PLTL 
	(Propositional Linear Temporal Logic) or CTL 
	(Computational Tree Logic) is undecidable. Finally, 
	we show how to apply the previous decidability 
	results to the Regular Model Checking. We propose a 
	new symbolic reachability semi-algorithm with 
	accelerations which successfully terminates on 
	half-duplex systems of two machines and some 
	interesting non-half-duplex systems.}
}
@misc{cortos05,
  author = {Bouyer, Patricia and others},
  title = {{ACI} {S}{\'e}curit{\'e} {I}nformatique {CORTOS} 
	  <<~{C}ontrol and {O}bservation of {R}eal-{T}ime {O}pen 
	  {S}ystems~>>~--- Rapport {\`a} mi-parcours},
  year = 2005,
  month = apr,
  type = {Contract Report},
  note = {6~pages},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/cortos-MP.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/cortos-MP.pdf},
  missingdoi = {}
}
@inproceedings{Cortos-MSR05-impl,
  address = {Autrans, France},
  month = oct,
  year = 2005,
  publisher = {Herm{\`e}s},
  editor = {Alla, Hassane and Rutten, {\'E}ric},
  acronym = {{MSR}'05},
  booktitle = {{A}ctes du 5{\`e}me {C}olloque sur la 
               {M}od{\'e}lisation des {S}yst{\`e}mes
               {R}{\'e}actifs
               ({MSR}'05)},
  author = {Altisen, Karine and Markey, Nicolas and Reynier, Pierre-Alain and
            Tripakis, Stavros},
  title = {Impl{\'e}mentabilit{\'e} des automates temporis{\'e}s},
  pages = {395-406},
  nonote = {Invited paper},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSR05-impl.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSR05-impl.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MSR05-impl.ps},
  abstract = {In this paper, we present the problem 
	of the implementability of timed automata. The 
	theoretical semantics of timed automata can not be 
	exactly implemented in practice, because computers 
	are digital and more or less precise; the properties 
	verified on a timed automaton are not necessarily 
	preserved when implementing it. We deal with two 
	approaches: the first one is based on the modeling of 
	the execution platform and the second studies an 
	enlarged semantics for timed automata that takes the 
	imprecision into account.}
}
@inproceedings{Cortos-MSR05-obs,
  address = {Autrans, France},
  month = oct,
  year = 2005,
  publisher = {Herm{\`e}s},
  editor = {Alla, Hassane and Rutten, {\'E}ric},
  acronym = {{MSR}'05},
  booktitle = {{A}ctes du 5{\`e}me {C}olloque sur la 
               {M}od{\'e}lisation des {S}yst{\`e}mes
               {R}{\'e}actifs
               ({MSR}'05)},
  author = {Bouyer, Patricia and Chevalier, Fabrice and Krichen, Moez and
            Tripakis, Stavros},
  title = {Observation partielle des syst{\`e}mes temporis{\'e}s},
  pages = {381-393},
  nonote = {Invited paper},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSR05-obs.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSR05-obs.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MSR05-obs.ps},
  abstract = {In this paper, we present the partial 
	observability constraint, which naturally appears when 
	modeling real-time systems. We have selected three 
	problems in which this hypothesis is fundamental but 
	leads to more difficult problems: control of timed 
	systems, fault diagnosis, and conformance testing. We 
	describe methods which can be used for solving such 
	problems. }
}
@inproceedings{Cortos-MSR05-control,
  address = {Autrans, France},
  month = oct,
  year = 2005,
  publisher = {Herm{\`e}s},
  editor = {Alla, Hassane and Rutten, {\'E}ric},
  acronym = {{MSR}'05},
  booktitle = {{A}ctes du 5{\`e}me {C}olloque sur la 
               {M}od{\'e}lisation des {S}yst{\`e}mes
               {R}{\'e}actifs
               ({MSR}'05)},
  author = {Altisen, Karine and Bouyer, Patricia and Cachat, Thierry and 
            Cassez, Franck and Gardey, Guillaume},
  title = {Introduction au contr{\^o}le des syst{\`e}mes temps-r{\'e}el},
  pages = {367-380},
  nonote = {Invited paper},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSR05-control.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSR05-control.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MSR05-control.ps},
  abstract = {In this paper we give a quick overview 
	of the area of control of real-time systems.}
}
@misc{demri-RSFDGrC05,
  author = {Demri, St{\'e}phane},
  title = {On the complexity of information logics},
  year = 2005,
  month = aug,
  howpublished = {Invited talk, Workshop on Logical and Algebraic 
		Foundations of Rough Sets, Regina, Canada}
}
@article{demri-JLC05,
  publisher = {Oxford University Press},
  journal = {Journal of Logic and Computation},
  author = {Demri, St{\'e}phane},
  title = {A reduction from {DLP} to~{PDL}},
  year = 2005,
  month = oct,
  volume = 15,
  number = 5,
  pages = {767-785},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-jlc05.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-jlc05.pdf},
  doi = {10.1093/logcom/exi043},
  abstract = {We present a reduction from a new logic extending van der Meyden's
dynamic logic of permission~(DLP) into propositional dynamic logic (PDL),
providing a 2EXPTIME decision procedure and showing that all the machinery 
for~PDL can be reused for reasoning about dynamic policies. As a 
side-effect, we establish that DLP is EXPTIME-complete. The logic we introduce
extends the logic~DLP so that the policy set can be updated depending on its
current value and such an update corresponds to add\slash delete transitions 
in the model, showing similarities with van Benthem's sabotage modal logic.}
}
@article{ddn-jlli05,
  publisher = {Kluwer Academic Publishers},
  journal = {Journal of Logic, Language and Information},
  author = {Demri, St{\'e}phane and de Nivelle, Hans},
  title = {Deciding Regular Grammar Logics with Converse through 
		  First-Order Logic},
  volume = 14,
  number = 3,
  pages = {289-319},
  year = {2005},
  month = jun,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ddn-gf-issue.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ddn-gf-issue.pdf},
  oldnote = {special issue dedicated to guarded logics.},
  doi = {10.1007/s10849-005-5788-9},
  abstract = {We provide a simple translation of the satisfiability problem for regular
grammar logics with converse into GF2 , which is the intersection of the guarded
fragment and the 2-variable fragment of first-order logic. The translation is theoretically 
interesting because it translates modal logics with certain frame conditions into
first-order logic, without explicitly expressing the frame conditions. It is practically
relevant because it makes it possible to use a decision procedure for the guarded
fragment in order to decide regular grammar logics with converse. The class of
regular grammar logics includes numerous logics from various application domains.\par
A consequence of the translation is that the general satisfiability problem for
every regular grammar logics with converse is in~EXPTIME. This extends a previous
result of the first author for grammar logics without converse. Other logics that
can be translated into GF2 include nominal tense logics and intuitionistic logic.
In our view, the results in this paper show that the natural first-order fragment
corresponding to regular grammar logics is simply GF2 without extra machinery
such as fixed point-operators.}
}
@inproceedings{DZG05-aplas,
  address = {Tsukuba, Japan},
  month = nov,
  year = 2005,
  volume = 3780,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Yi, Kwangkeun},
  acronym = {{APLAS}'05},
  booktitle = {{P}roceedings of the 3rd {A}sian {S}ymposium
               on {P}rogramming {L}anguages and {S}ystems
               ({APLAS}'05)},
  author = {Dal Zilio, Silvano and Gascon, R{\'e}gis},
  title = {Resource Bound Certification for a Tail-Recursive
                  Virtual Machine},
  pages = {247-263},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DZG-APLAS05.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DZG-APLAS05.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DZG-APLAS05.ps},
  doi = {10.1007/11575467_17},
  abstract = {We define a method to statically bound the size of values
computed during the execution of a program as a function of the size
of its parameters. More precisely, we consider bytecode programs that
should be executed on a simple stack machine with support for algebraic 
data types, pattern-matching and tail-recursion. Our size verification 
method is expressed as a static analysis, performed at the level
of the bytecode, that relies on machine-checkable certificates. We follow
here the usual assumption that code and certificates may be forged and
should be checked before execution.\par
Our approach extends a system of static analyses based on the notion
of quasi-interpretations that has already been used to enforce resource
bounds on first-order functional programs. This paper makes two additional 
contributions. First, we are able to check optimized programs,
containing instructions for unconditional jumps and tail-recursive calls,
and remove restrictions on the structure of the bytecode that was imposed 
in previous works. Second, we propose a direct algorithm that
depends only on solving a set of arithmetical constraints.}
}
@inproceedings{DG-concur2005,
  address = {San Francisco, California, USA},
  month = aug,
  year = 2005,
  volume = 3653,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Abadi, Mart{\'\i}n and de Alfaro, Luca},
  acronym = {{CONCUR}'05},
  booktitle = {{P}roceedings of the 16th 
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'05)},
  author = {Demri, St{\'e}phane and Gascon, R{\'e}gis},
  title = {Verification of Qualitative 
		 {\(\mathbb{\MakeUppercase{Z}}\)}-Constraints},
  pages = {518-532},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-Concur05.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-Concur05.pdf},
  doi = {10.1007/11539452_39},
  abstract = {We introduce an LTL-like logic with atomic formulae built
over a constraint language interpreting variables in~\(\mathbb{Z}\). The constraint
language includes periodicity constraints, comparison constraints of the
form \(x = y\) and \(x < y\), it is closed under Boolean operations and it
admits a restricted form of existential quantification. This is the largest
set of qualitative constraints over~\(\mathbb{Z}\) known so far, shown to admit a
decidable LTL extension. Such constraints are those used for instance
in calendar formalisms or in abstractions of counter automata by using
congruences modulo some power of two. Indeed, various programming
languages perform arithmetic operators modulo some integer. We show
that the satisfiability and model-checking problems (with respect to an
appropriate class of constraint automata) for this logic are decidable in
polynomial space improving significantly known results about its strict
fragments. As a by-product, LTL model-checking over integral relational
automata is proved complete for polynomial space which contrasts with
the known undecidability of its CTL counterpart.}
}
@inproceedings{DKR-FEE2005,
  address = {Milan, Italy},
  month = sep,
  year = 2005,
  optaddress = {},
  acronym = {{FEE} 2005},
  booktitle = {{P}roceedings of the {W}orkshop {F}rontiers in {E}lectronic 
	   {E}lections ({FEE} 2005)},
  author = {Delaune, St{\'e}phanie and Kremer, Steve and 
		   Ryan, Mark D.},
  title = {Receipt-Freeness: Formal Definition and Fault 
		   Attacks (Extended Abstract)},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-fee05.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-fee05.pdf},
  preliminary-version-of = {DKR-csfw06}
}
@inproceedings{DLN-time05,
  address = {Burlington, Vermont, USA},
  month = jun,
  year = 2005,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{TIME}'05},
  booktitle = {{P}roceedings of the 12th {I}nternational {S}ymposium on 
	       {T}emporal {R}epresentation and {R}easoning
	       ({TIME}'05)},
  author = {Demri, St{\'e}phane and Lazi{\'c}, Ranko and  
		 Nowak, David},
  title = {On the Freeze Quantifier in Constraint {LTL}: 
		Decidability and Complexity},
  pages = {113-121},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-03.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
		  rr-lsv-2005-03.ps},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-03.pdf},
  doi = {10.1109/TIME.2005.28},
  abstract = {Constraint LTL, a generalization of LTL over Presburger
constraints, is often used as a formal language to specify the
behavior of operational models with constraints. The freeze
quantifier can be part of the language, as in some real-time
logics, but this variable-binding mechanism is quite general
and ubiquitous in many logical languages (first-order temporal 
logics, hybrid logics, logics for sequence diagrams,
navigation logics, etc.). We show that Constraint LTL over
the simple domain \(\langle \mathbb{N}, = \rangle\) augmented 
with the freeze operator is undecidable which is a 
surprising result regarding the
poor language for constraints (only equality tests). Many
versions of freeze-free Constraint LTL are decidable over
domains with qualitative predicates and our undecidability
result actually establishes \(\Sigma_{1}^{1}\)-completeness. 
On the positive side, we provide complexity results when the domain is
finite (EXPSPACE-completeness) or when the formulae are
flat in a sense introduced in the paper. Our undecidability
results are quite sharp (\emph{i.e.}~with restrictions on the 
number of variables) and all our complexity characterizations
insure completeness with respect to some complexity class
(mainly PSPACE and~EXPSPACE).}
}
@inproceedings{DN-atva05,
  address = {Taipei, Taiwan},
  month = oct,
  year = {2005},
  volume = 3707,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Peled, Doron A. and Tsay, Yih-Kuen},
  acronym = {{ATVA}'05},
  booktitle = {{P}roceedings of the 3rd {I}nternational
               {S}ymposium on {A}utomated {T}echnology
               for {V}erification and {A}nalysis
               ({ATVA}'05)},
  author = {Demri, St{\'e}phane and Nowak, David},
  title = {Reasoning about transfinite sequences (extended abstract)},
  pages = {248-262},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DN-atva2005.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DN-atva2005.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DN-atva2005.ps},
  doi = {10.1007/11562948_20},
  abstract = {We introduce a family of temporal logics to specify the 
behavior of systems with Zeno behaviors. We extend linear-time temporal
logic LTL to authorize models admitting Zeno sequences of actions and
quantitative temporal operators indexed by ordinals replace the standard 
next-time and until future-time operators. Our aim is to control
such systems by designing controllers that safely work on \(\omega\)-sequences
but interact synchronously with the system in order to restrict their behaviors. 
We show that the satisfiability problem for the logics working
on \(\omega^{k}\)-sequences is EXPSPACE-complete when the integers are represented
in binary, and PSPACE-complete with a unary representation. To do so,
we substantially extend standard results about LTL by introducing a
new class of succinct ordinal automata that can encode the interaction
between the different quantitative temporal operators.}
}
@inproceedings{FM-podc05,
  address = {Las Vegas, Nevada, USA},
  month = jul,
  year = 2005,
  publisher = {ACM Press},
  editor = {Aguilera, Marcos Kawazoe and Aspnes, James},
  acronym = {{PODC}'05},
  booktitle = {{P}roceedings of the {T}wenty-{F}ourth {A}nnual 
	  {ACM} {SIGACT}-{SIGOPS} {S}ymposium 
	  on {P}rinciples of {D}istributed {C}omputing
	  ({PODC}'05)},
  author = {Fribourg, Laurent and Messika, St{\'e}phane},
  title = {Brief Announcement: Coupling for {M}arkov Decision 
	Processes~--- {A}pplication to Self-Stabilization with Arbitrary 
	Schedulers},
  pages = {322},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ba173-messika.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ba173-messika.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ba173-messika.ps},
  doi = {10.1145/1073814.1073875}
}
@inproceedings{Gascon-m4m2005,
  address = {Berlin, Germany},
  month = dec,
  year = 2005,
  volume = 194,
  series = {Informatik Bericht},
  publisher = {Humboldt Universit{\"a}t zu Berlin},
  editor = {Schlingloff, Holger},
  acronym = {{M4M-4}},
  booktitle = {{P}roceedings of the 4th
               {W}orkshop on {M}ethods for {M}odalities
               ({M4M-4})},
  author = {Gascon, R{\'e}gis},
  title = {Verifying qualitative and quantitative properties with~{LTL} 
                 over concrete domains},
  pages = {54-61},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Gascon-M4M05.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Gascon-M4M05.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Gascon-M4M05.ps},
  abstract = {We introduce different 
	extensions of LTL where propositional 
	variables are replaced by constraints 
	interpreted in~\(\mathbb{Z}\). We show 
	different decidability and complexity results 
	for the satisfiability and model checking 
	problems of these logics. The extension of 
	LTL over a wide set of qualitative 
	constraints is shown to be PSPACE-complete. 
	When introducing some quantitative 
	constraints, we must consider strong 
	restrictions to regain decidability.}
}
@inproceedings{Gastin-ICALP2005,
  address = {Lisboa, Portugal},
  month = jul,
  year = 2005,
  volume = {3580},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Caires, Lu{\'\i}s and Italiano, Giuseppe F. and
	    Monteiro, Lu{\'\i}s and Palamidessi, Catuscia and Yung, Moti},
  acronym = {{ICALP}'05},
  booktitle = {{P}roceedings of the 32nd {I}nternational 
               {C}olloquium on {A}utomata, {L}anguages and 
               {P}rogramming
               ({ICALP}'05)},
  author = {Droste, Manfred and Gastin, Paul},
  title = {Weighted Automata and Weighted Logics},
  pages = {513-525},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/icalp05dg-final.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/icalp05dg-final.ps},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/icalp05dg-final.pdf},
  doi = {10.1007/11523468_42},
  abstract = {Weighted automata are used to 
	describe quantitative properties in various 
	areas such as probabilistic systems, image 
	compression, speech-to-text processing. The 
	behaviour of such an automaton is a mapping, 
	called a formal power series, assigning to 
	each word a weight in some semiring. We 
	generalize B{\"{u}}chi's and Elgot's 
	fundamental theorems to this quantitative 
	setting. We introduce a weighted version of 
	MSO~logic and prove that, for commutative 
	semirings, the behaviours of weighted 
	automata are precisely the formal power 
	series definable with our weighted logic. We 
	also consider weighted first-order logic and 
	show that aperiodic series coincide with the 
	first-order definable ones, if the semiring 
	is locally finite, commutative and has some 
	aperiodicity property.}
}
@inproceedings{GLP:VMCAI,
  address = {Paris, France},
  month = jan,
  year = 2005,
  volume = 3385,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Cousot, Radhia},
  acronym = {{VMCAI}'05},
  booktitle = {{P}roceedings of the 6th {I}nternational {C}onference on
   	       {V}erification, {M}odel {C}hecking and {A}bstract {I}nterpretation
	       ({VMCAI}'05)},
  author = {Goubault{-}Larrecq, Jean and Parrennes, Fabrice},
  title = {Cryptographic Protocol Analysis on Real {C}~Code},
  pages = {363-379},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GouPar-VMCAI2005.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GouPar-VMCAI2005.pdf},
  doi = {10.1007/b105073},
  abstract = {Implementations of 
	cryptographic protocols, such as OpenSSL for 
	example, contain bugs affecting security, 
	which cannot be detected by just analyzing 
	abstract protocols (e.g., SSL or TLS). We 
	describe how cryptographic protocol 
	verification techniques based on solving 
	clause sets can be applied to detect 
	vulnerabilities of C programs in the 
	Dolev-Yao model, statically. This involves 
	integrating fairly simple pointer analysis 
	techniques with an analysis of which messages 
	an external intruder may collect and forge. 
	This also involves relating concrete run-time 
	data with abstract, logical terms 
	representing messages. To this end, we make 
	use of so-called trust assertions.

	The output of the analysis is a set of 
	clauses in the decidable class H1, which can 
	then be solved independently. This can be 
	used to establish secrecy properties, and to 
	detect some other bugs. }
}
@article{JGL-ipl2005,
  publisher = {Elsevier Science Publishers},
  journal = {Information Processing Letters},
  author = {Goubault{-}Larrecq, Jean},
  title = {Deciding {\(\mathcal{\MakeUppercase{H}}_1\)} 
                    by Resolution},
  year = {2005},
  volume = 95,
  number = 3,
  pages = {401-408},
  month = aug,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Goubault-h1.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Goubault-h1.pdf},
  doi = {10.1016/j.ipl.2005.04.007},
  abstract = {Nielson, Nielson and Seidl's 
	class \(\mathcal{H}_1\) is a decidable class 
	of first-order Horn clause sets, describing 
	strongly regular relations.  We give 
	another proof of decidability, and of the 
	regularity of the defined languages, based 
	on fairly standard automated deduction 
	techniques. }
}
@article{VGL-dmtcs05,
  journal = {Discrete Mathematics \& Theoretical Computer Science},
  author = {Verma, Kumar N. and Goubault{-}Larrecq, Jean},
  title = {{K}arp-{M}iller Trees for a Branching Extension of~{VASS}},
  volume = 7,
  number = 1,
  pages = {217-230},
  year = 2005,
  month = nov,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/VGL-dmtcs05.pdf},
  secondurl = {http://www.dmtcs.org/volumes/abstracts/dm070113.abs.html},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/VGL-dmtcs05.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/VGL-dmtcs05.ps},
  abstract = {We study BVASS (Branching VASS) 
	which extend VASS (Vector Addition Systems with 
	States) by allowing addition transitions that 
	merge two configurations. Runs in BVASS are 
	tree-like structures instead of linear ones as 
	for VASS. We show that the construction of 
	Karp-Miller trees for VASS can be extended to 
	BVASS. This entails that the coverability set 
	for BVASS is computable. This allows us to 
	obtain decidability results for certain classes 
	of equational tree automata with an 
	associative-commutative symbol. Recent 
	independent work by de Groote \emph{et al.} implies 
	that decidability of reachability in BVASS is 
	equivalent to decidability of provability in 
	MELL (multiplicative exponential linear logic), 
	which is still an open problem. Hence our 
	results are also a step towards answering this 
	question in the affirmative.}
}
@inproceedings{MukhamedovKremerRitter2005,
  address = {Roseau, The Commonwealth Of Dominica},
  month = aug,
  year = 2005,
  volume = 3570,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Patrick, Andrew S. and Yung, Moti},
  acronym = {{FC}'05},
  booktitle = {{R}evised {P}apers from the 9th {I}nternational {C}onference
               on {F}inancial {C}ryptography and {D}ata {S}ecurity
               ({FC}'05)},
  author = {Mukhamedov, Aybek and Kremer, Steve and
                   Ritter, Eike},
  title = {Analysis of a Multi-Party Fair Exchange Protocol and
                   Formal Proof of Correctness in the Strand Space
                   Model},
  pages = {255-269},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MKR-fcrypto05.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MKR-fcrypto05.pdf},
  doi = {10.1007/11507840_23},
  abstract = {A multi-party fair 
	exchange protocol is a cryptographic 
	protocol allowing several parties to 
	exchange commodities in such a way that 
	everyone gives an item away if and only 
	if it receives an item in return. In this 
	paper we discuss a multi-party fair 
	exchange protocol originally proposed by 
	Franklin and Tsudik, and subsequently 
	shown to have flaws and fixed by Gonz\'alez 
	and Markowitch. We identify flaws in the 
	fixed version of the protocol, propose a 
	corrected version, and give a formal 
	proof of correctness in the strand space 
	model.}
}
@inproceedings{KremerRyan2005,
  address = {Edinburgh, Scotland, UK},
  month = apr,
  year = 2005,
  volume = 3444,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Sagiv, Mooly},
  acronym = {{ESOP}'05},
  booktitle = {{P}rogramming {L}anguages and {S}ystems~---
               {P}roceedings of the 14th
               {E}uropean {S}ymposium on {P}rogramming
               ({ESOP}'05)},
  author = {Kremer, Steve and Ryan, Mark D.},
  title = {Analysis of an Electronic Voting Protocol in the
           Applied Pi-Calculus},
  pages = {186-200},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Kremer-esop05.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Kremer-esop05.ps},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Kremer-esop05.pdf},
  doi = {10.1007/b107380},
  abstract = {Electronic voting promises the 
	possibility of a convenient, efficient and 
	secure facility for recording and tallying votes 
	in an election.  Recently highlighted 
	inadequacies of implemented systems have 
	demonstrated the importance of formally 
	verifying the underlying voting protocols.  The 
	applied pi calculus is a formalism for modelling 
	such protocols, and allows us to verify 
	properties by using automatic tools, and to rely 
	on manual proof techniques for cases that 
	automatic tools are unable to handle.  We model 
	a known protocol for elections known as FOO~92 
	in the applied pi calculus, and we formalise 
	three of its expected properties, namely 
	fairness, eligibility, and privacy. We use the 
	ProVerif tool to prove that the first two 
	properties are satisfied. In the case of the 
	third property, ProVerif is unable to prove it 
	directly, because its ability to prove 
	observational equivalence between processes is 
	not complete.  We provide a manual proof of the 
	required equivalence.}
}
@inproceedings{GK-concur05,
  address = {San Francisco, California, USA},
  month = aug,
  year = 2005,
  volume = 3653,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Abadi, Mart{\'\i}n and de Alfaro, Luca},
  acronym = {{CONCUR}'05},
  booktitle = {{P}roceedings of the 16th 
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'05)},
  author = {Gastin, Paul and Kuske, Dietrich},
  title = {Uniform Satisfiability Problem for Local Temporal Logics
		 over {M}azurkiewicz Traces},
  pages = {533-547},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/concur05gk-final.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/concur05gk-final.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/concur05gk-final.ps},
  doi = {10.1007/11539452_40},
  abstract = {We continue our study of the complexity 
	of temporal logics over concurrent systems that can be 
	described by Mazurkiewicz traces. In a previous paper 
	(CONCUR~2003), we investigated the class of local and 
	MSO definable temporal logics that capture all known 
	temporal logics and we showed that the satisfiability 
	problem for any such logic is in PSPACE (provided the 
	dependence alphabet is fixed). In this paper, we 
	concentrate on the uniform satisfiability problem: we 
	consider the dependence alphabet (\emph{i.e.}, the 
	architecture of the distributed system) as part of the 
	input. We prove lower and upper bounds for the uniform 
	satisfiability problem that depend on the number of 
	monadic quantifier alternations present in the chosen 
	MSO-modalities.}
}
@inproceedings{LLT-rta2005,
  address = {Nara, Japan},
  month = apr,
  year = 2005,
  volume = 3467,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Giesl, J{\"u}rgen},
  acronym = {{RTA}'05},
  booktitle = {{P}roceedings of the 16th {I}nternational
               {C}onference on {R}ewriting {T}echniques
               and {A}pplications
               ({RTA}'05)},
  author = {Lafourcade, Pascal and Lugiez, Denis and Treinen, Ralf},
  title = {Intruder Deduction for {AC}-like Equational Theories 
		 with Homomorphisms},
  pages = {308-322},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/rta05-LLT.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/rta05-LLT.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/rta05-LLT.ps},
  doi = {10.1007/b135673},
  abstract = {Cryptographic protocols are 
	small programs which involve a high level 
	of concurrency and which are difficult to 
	analyze by hand. The most successful 
	methods to verify such protocols rely on 
	rewriting techniques and automated 
	deduction in order to implement or mimic 
	the process calculus describing the 
	protocol execution. \par 
	We focus on the 
	intruder deduction problem, that is the 
	vulnerability to passive attacks, in 
	presence of several variants of 
	\textit{AC}-like axioms (from \textit{AC} 
	to Abelian groups, including the theory 
	of \emph{exclusive or}) and homomorphism 
	which are the most frequent axioms 
	arising in cryptographic protocols. 
	Solutions are known for the cases of 
	\emph{exclusive or}, of Abelian groups, 
	and of homomorphism alone. In this paper 
	we address the combination of these 
	\textit{AC}-like theories with the law of 
	homomorphism which leads to much more 
	complex decision problems.\par 
	We prove 
	decidability of the intruder deduction 
	problem in all cases considered. Our 
	decision procedure is in EXPTIME, except 
	for a restricted case in which we have 
	been able to get a PTIME decision 
	procedure using a property of one-counter 
	and pushdown automata.}
}
@inproceedings{Laroussinie-m4m05,
  address = {Berlin, Germany},
  month = dec,
  year = 2005,
  volume = 194,
  series = {Informatik Bericht},
  publisher = {Humboldt Universit{\"a}t zu Berlin},
  editor = {Schlingloff, Holger},
  acronym = {{M4M-4}},
  booktitle = {{P}roceedings of the 4th
               {W}orkshop on {M}ethods for {M}odalities
               ({M4M-4})},
  author = {Laroussinie, Fran{\c{c}}ois},
  title = {Timed modal logics for the verification of real-time systems},
  pages = {293-305},
  nonote = {Invited paper},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Lar-M4M05.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Lar-M4M05.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Lar-M4M05.ps},
  abstract = {The timed modal logic \(L_{\nu}\) has 
	been proposed in order to express timed properties 
	over real-time systems modeled as (compositions of) 
	timed automata. In this paper, we present a short 
	survey of results about~\(L_{\nu}\): complexity of 
	model checking, expressivity, compositional methods, 
	relationship with strong timed bisimulation etc. We 
	also show how \(L_{\nu}\) can be extended in order to 
	express new properties. }
}
@inproceedings{LS-fossacs05,
  address = {Edinburgh, Scotland, UK},
  month = apr,
  year = 2005,
  volume = 3441,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Sassone, Vladimiro},
  acronym = {{FoSSaCS}'05},
  booktitle = {{P}roceedings of the 8th {I}nternational 
               {C}onference on {F}oundations of {S}oftware {S}cience
               and {C}omputation {S}tructures
               ({FoSSaCS}'05)},
  author = {Laroussinie, Fran{\c{c}}ois and Sproston, Jeremy},
  title = {Model Checking Durational Probabilistic Systems},
  pages = {140-154},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/fossacs05-FS.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/fossacs05-FS.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/fossacs05-FS.ps},
  doi = {10.1007/b106850},
  abstract = {We consider model-checking algorithms for durational probabilistic
systems, which are systems exhibiting nondeterministic, probabilistic and
discrete-timed behaviour. We present two semantics for durational probabilistic
systems, and show how formulae of the probabilistic and timed temporal logic
PTCTL can be verified on such systems. We also address complexity issues, in
particular identifying the cases in which model checking durational probabilistic
systems is harder than verifying non-probabilistic durational systems.}
}
@inproceedings{LNZ-appsem05,
  address = {Frauenchiemsee, Germany},
  month = sep,
  year = 2005,
  editor = {Hofmann, Martin and Loidl, Hans-Wolfgang},
  acronym = {{APPSEM}'05},
  booktitle = {{P}roceedings of the 3rd {APPSEM~II} Workshop
           ({APPSEM}'05)},
  author = {Lasota, S{\l}awomir and Nowak, David and
		 Zhang, Yu},
  title = {On completeness of logical relations for monadic types},
  nopages = {},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LNZ-monad-complete.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LNZ-monad-complete.pdf},
  abstract = {Interesting properties of programs can be expressed using
contextual equivalence. The latter is difficult to prove directly, hence 
(pre-)logical relations are often used as a tool to prove it.
Whereas pre-logical relations are complete at all types, logical 
relations are only complete up to first-order types. We propose a 
notion of contextual equivalence for Moggi's computational lambda calculus, 
and define pre-logical and logical relations for this calculus. Monads 
introduce new difficulties: in particular the usual proofs of completeness 
up to first-order types do not go through. We prove completeness up to 
first order for several of Moggi's monads. In the case of the non-determinism 
monad we obtain, as a corollary, completness of strong bisimulation 
w.r.t.~contextual equivalence in lambda calculus with monadic non-determinism.}
}
@techreport{rr-LSV:05:11,
  author = {Bouhoula, Adel and Jacquemard, Florent},
  title = {Automated Induction for Complex Data Structures},
  institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  year = {2005},
  month = jul,
  type = {Research Report},
  number = {LSV-05-11},
  note = {24~pages},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-11.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-11.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
		  rr-lsv-2005-11.ps},
  abstract = {We develop a new approach for mechanizing induction
                   on complex data structures (like sets, sorted lists,
                   trees, powerlists...). The key idea is to compute a
                   tree grammar with constraints which describes exactly
                   the initial model of the given specification, unlike
                   test sets or cover sets which are approximative
                   induction schemes when the constructors are not free.
                   This grammar is used for the generation of subgoals
                   during the proof by induction. Our procedure is sound
                   and refutationally complete even with constrained
                   axioms for constructors. it subsumes all test set
                   induction techniques, and yields very natural proofs
                   for several examples on which other approaches
                   failed.}
}
@techreport{rr-LSV:05:17,
  author = {Bouhoula, Adel and Jacquemard, Florent},
  title = {Automatic Verification of Sufficient Completeness for Specifications 
                  of Complex Data Structures},
  institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  year = 2005,
  month = aug,
  type = {Research Report},
  number = {LSV-05-17},
  note = {14~pages},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-17.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-17.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
		  rr-lsv-2005-17.ps},
  abstract = {We present a new procedure for testing sufficient
                  completeness for conditional and constrained term
                  rewriting systems in presence of constrained axioms
                  for constructors. Such axioms allow to specify
                  complex data structures like e.g. sets or sorted lists. 
                  Our approach is based on tree grammars with
                  constraints, a formalism which permits an exact
                  representation of languages of ground constructor
                  terms in normal form. The procedure is sound and
                  complete and has been successfully used for checking
                  the sufficient completeness of several
                  specifications where related former techniques fail.}
}
@techreport{LSV:05:19,
  author = {Lafourcade, Pascal and Lugiez, Denis and Treinen, Ralf},
  title = {Intruder Deduction for the Equational Theory of Exclusive-or
		  with Distributive Encryption},
  institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  year = 2005,
  month = oct,
  type = {Research Report},
  number = {LSV-05-19},
  note = {39~pages},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-19.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-19.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
	rr-lsv-2005-19.ps},
  abstract = {Cryptographic protocols are small programs which involve a high
  level of concurrency and which are difficult to analyze by hand. The
  most successful methods to verify such protocols are based on
  rewriting techniques and automated deduction in order to implement
  or mimic the process calculus describing the execution of a 
  protocol.\par
  We are interested in the intruder deduction problem, that is the
  vulnerability to passive attacks, in presence of the theory of an
  encryption
  operator which distributes over the \emph{exclusive-or}. This
  equational
  theory describes very common properties of cryptographic primitives.
  Solutions to the intruder deduction problem modulo an equational theory
  are known for the cases of \emph{exclusive-or}, of Abelian groups, of a
  homomorphism symbol alone, and of combinations of these theories. In
  this paper we consider the case where the encryption distributes over
  \emph{exclusive-or}. The interaction of the distributive law of the
  encryption with the cancellation law of \emph{exclusive-or} leads to a
  much more complex decision problem. We prove decidability of the intruder
  deduction problem for an encryption which distributes over
  \emph{exclusive-or} with an EXPTIME procedure and we give a PTIME
  decision
  procedure relying on prefix rewrite systems for a restricted case, the
  \emph{binary} case.}
}
@article{LugSch-IC,
  publisher = {Elsevier Science Publishers},
  journal = {Information and Computation},
  author = {Lugiez, Denis and Schnoebelen, {\relax Ph}ilippe},
  title = {Decidable first-order transition logics for
	 {PA}-processes},
  year = 2005,
  month = nov,
  volume = 203,
  number = 1,
  pages = {75-113},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/InfComp-C2707.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/InfComp-C2707.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/InfComp-C2707.ps},
  doi = {10.1016/j.ic.2005.02.003},
  abstract = {We show the decidability of 
	model checking PA-processes against 
	several first-order logics
	based upon the reachability predicate. 
	The main tool for this result is the
	recognizability by tree automata of the 
	reachability relation. The tree
	automata approach and the transition 
	logics we use allow a smooth and
	general treatment of parameterized model 
	checking for PA. This approach is
	extended to handle a quite general notion 
	of costs of PA-steps.
	In particular, when costs are Parikh 
	images of traces, we show decidability
	of a transition logic extended by some 
	form of first-order reasoning over
	costs.}
}
@inproceedings{Orchids-cav05,
  address = {Edinburgh, Scotland, UK},
  month = jul,
  year = 2005,
  volume = 3576,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Etessami, Kousha and Rajamani, Sriram},
  acronym = {{CAV}'05},
  booktitle = {{P}roceedings of the 17th
               {I}nternational {C}onference on 
               {C}omputer {A}ided {V}erification
               ({CAV}'05)},
  author = {Olivain, Julien and Goubault{-}Larrecq, Jean},
  title = {The {O}rchids Intrusion Detection Tool},
  pages = {286-290},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/OG-cav05.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/OG-cav05.pdf},
  doi = {10.1007/11513988_28}
}
@misc{PERSEE-RC1,
  author = {Bardin, S{\'e}bastien and Herbreteau, Fr{\'e}d{\'e}ric 
		and Sighireanu, Mihaela and Sutre, Gr{\'e}goire
                  and Vincent, Aymeric},
  title = {Int{\'e}gration des outils {PERS\'EE} (Proposition
		d'architecture)},
  howpublished = {D\'elivrable~3.1~--- Partie~1 du Projet PERS\'EE de 
		l'ACI S\'ecurit\'e Informatique},
  year = 2005,
  month = jun,
  url = {http://www.labri.fr/perso/herbrete/persee/downloads/integration/deliverable3.1.pdf},
  pdf = {http://www.labri.fr/perso/herbrete/persee/downloads/integration/deliverable3.1.pdf},
  note = {35~pages}
}
@misc{persee-miparcours05,
  author = {Schnoebelen, {\relax Ph}ilippe and others},
  title = {{ACI} {S}{\'e}curit{\'e} {I}nformatique {PERS{\'E}E}~--- 
	    Rapport {\`a} mi-parcours},
  year = 2005,
  month = nov,
  type = {Contract Report},
  note = {8~pages}
}
@techreport{Prouve:rap5,
  author = {Bozga, Liana and Delaune, St{\'e}phanie and 
		 Klay, Francis and Vigneron, Laurent},
  title = {Retour d'exp{\'e}rience sur la validation du 
		 porte-monnaie {\'e}lectronique},
  institution = {projet RNTL PROUV{\'E}},
  month = mar,
  year = 2005,
  type = {Technical Report},
  number = 5,
  note = {29~pages},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/prouve-rap5.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/prouve-rap5.ps},
  abstract = {Le domaine de la 
	mod{\'e}lisation et de la v{\'e}rification 
	est une activit{\'e} d{\'e}licate et 
	importante qui a connu une v{\'e}ritable 
	explosion dans les ann{\'e}es~1990. On 
	dispose {\`a} l'entr{\'e}e des 
	ann{\'e}es~2000 de toute une gamme de 
	mod{\`e}les et de m{\'e}thodes plus ou moins 
	avanc{\'e}s en ce qui concerne 
	l'expressivit{\'e} et l'automatisation.
	\par
	Afin de d{\'e}finir les besoins et les 
	priorit{\'e}s {\`a} mettre sur les outils 
	consacr{\'e}s {\`a} la v{\'e}rification de 
	protocoles cryptographiques qui seront 
	d{\'e}velopp{\'e}s au sein du projet RNTL 
	PROUV{\'E}, nous proposons de travailler en 
	situation r{\'e}elle, sur des protocoles 
	plut{\^o}t <<~durs~>>, en effectuant le cycle 
	suivant: mod{\'e}lisation, formalisation puis 
	validation dans des outils existants.  Ce 
	travail est effectu{\'e} ici pour deux 
	versions d'un protocole de porte-monnaie 
	{\'e}lectronique, dont l'une a {\'e}t{\'e} 
	d{\'e}velopp{\'e}e r{\'e}cemment par une 
	{\'e}quipe de France T{\'e}l{\'e}com.  Les 
	outils retenus pour la r{\'e}alisation de 
	cette {\'e}tude sont ProVerif, Hermes et 
	Casrul, en raison de leurs 
	caract{\'e}ristiques tr{\`e}s 
	diff{\'e}rentes.}
}
@techreport{Prouve:rap6,
  author = {Delaune, St{\'e}phanie and 
		 Klay, Francis and Kremer, Steve},
  title = {Sp{\'e}cification du protocole de vote  
		 {\'e}lectronique},
  institution = {projet RNTL PROUV{\'E}},
  month = nov,
  year = 2005,
  type = {Technical Report},
  number = 6,
  note = {19~pages},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Prouve-rap6.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Prouve-rap6.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Prouve-rap6.ps},
  abstract = {Cette nouvelle \'etude de cas a pour 
	but de tester les limites du 
	langage~{\scshape Prouv\'e}.  En effet, le 
	protocole que nous avons choisi d'\'etudier est 
	volontairement complexe tant au niveau de la 
	mod\'elisation des propri\'et\'es de s\'ecurit\'e que de la 
	description du protocole lui-m\^eme en raison de la 
	manipulation de structures de donn\'ees telles que 
	les listes.\par
	Notre \'etude de cas est un protocole de vote qui a 
	\'et\'e mis au point par J.~Traor\'e, ing\'enieur de 
	recherche chez France~T\'el\'ecom. Ce protocole est 
	bas\'e sur le m\'ecanisme de signature en aveugle et 
	peut \^etre consid\'er\'e comme un d\'eriv\'e du protocole 
	de Fujioka, Okamoto et~Ohta.  Ce document 
	introduit dans un premier temps le probl\`eme du 
	vote \'electronique en g\'en\'eral avant de d\'ecrire le 
	protocole en lui-m\^eme et sa formalisation dans le 
	langage~{\scshape Prouv\'e}.}
}
@techreport{Prouve:rap7,
  author = {Kremer, Steve and Lakhnech, Yassine and Treinen, Ralf},
  title = {The {P}{\scshape rouv\'e} Manual: Specifications, Semantics, and Logics},
  institution = {projet RNTL PROUV{\'E}},
  month = dec,
  year = 2005,
  type = {Technical Report},
  number = 7,
  note = {49~pages},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Prouve-rap7.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Prouve-rap7.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Prouve-rap7.ps},
  abstract = { In this report we describe the {\scshape Prouv\'e}
	specification language for cryptographic protocols. A main 
	feature of the language is that it separates the roles of a 
	protocol, which are defined in a simple imperative 
	programming language, from the scenario which defines how 
	instances of the roles are created.\par
	We give a formal semantics of the protocol specification 
	language, and define both an expressive logics for safety 
	conditions of protocols and a more limited assertion 
	language.\par
	This version of the report~(2.0.x) describes version~2.0 of 
	the {\scshape Prouv\'e} language.}
}
@inproceedings{PinchinatRiedweg05,
  address = {Portland, Oregon, USA},
  month = jun,
  year = 2005,
  publisher = {IEEECSP},
  editor = {Balakrishnan, S. N.},
  acronym = {{ACC}'05},
  booktitle = {{P}roceedings of the 24th {A}merican {C}ontrol 
	       {C}onference ({ACC}'05)},
  author = {Pinchinat, Sophie and Riedweg, St{\'e}phane},
  title = {You Can Always Compute Maximally Permissive 
		Controllers Under Partial Observation When They Exist},
  pages = {2287-2292},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PR-ACC05.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PR-ACC05.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/PR-ACC05.ps},
  abstract = {The maximal permissivity property of controllers
is an optimal criterion that is often taken for granted as the
result of synthesis algorithms: the algorithms are designed
for frameworks where the existence and the uniqueness of
a maximal permissive controller is demonstrated apart, as
it fulfills sufficient hypotheses; these algorithms precisely
compute this object. Still, maximally permissive solutions
might exist in circumstances which do not fall into such
identified frameworks, but there is no way to ensure that
the algorithms deliver an optimal solution. In this paper, we
propose a general synthesis procedure which always computes
a maximal permissive controller when it exists.}
}
@inproceedings{PR-cdc05,
  address = {Seville, Spain},
  month = dec,
  year = 2005,
  publisher = {{IEEE} Control System Society},
  acronym = {{CDC-ECC}'05},
  booktitle = {{P}roceedings of the 44th {IEEE} {C}onference on Decision 
		and Control and European Control Conference 
		({CDC-ECC}'05)},
  author = {Pinchinat, Sophie and Riedweg, St{\'e}phane},
  title = {On the Architectures in Decentralized Supervisory 
		Control},
  pages = {12-17},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PR-cdc05.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PR-cdc05.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/PR-cdc05.ps},
  abstract = {In this paper, we clarify the notion of architecture in 
decentralized control, in order to investigate the realizability problem: 
given a discrete-event system, a desired behavior and an architecture for 
a decentralized control, can the desired behavior be achieved by 
decentralized controllers in accordance with the given architecture? We 
consider the problem for any mu-calculus definable behavior and for 
classic architectures from the literature. The method consists in 
compiling in a single formula both the desired behavior and the 
architecture. Applications of this approach are a single synthesis 
algorithm of decentralized controllers (with full observation) for the 
whole considered family of architectures, and the development of a 
convenient mathematical framework for a theory of decentralized control 
architectures.}
}
@article{PR-IPL05,
  publisher = {Elsevier Science Publishers},
  journal = {Information Processing Letters},
  author = {Pinchinat, Sophie and Riedweg, St{\'e}phane},
  title = {A Decidable Class of Problems for Control under Partial Observation},
  year = 2005,
  month = aug,
  volume = 95,
  number = 4,
  pages = {454-465},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PR-IPL05.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PR-IPL05.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/PR-IPL05.ps},
  doi = {10.1016/j.ipl.2005.04.011}
}
@phdthesis{THESE-bardin05,
  author = {Bardin, S{\'e}bastien},
  title = {Vers un model checking avec acc{\'e}l{\'e}ration plate 
		 de syst{\`e}mes h{\'e}t{\'e}rog{\`e}nes},
  year = 2005,
  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/PDF/bardin-THESE.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bardin-THESE.pdf}
}
@phdthesis{THESE-zhang05,
  author = {Zhang, Yu},
  title = {Cryptographic logical relations~-- What is the 
		contextual equivalence for 
		cryptographic protocols and how to prove~it?},
  year = 2005,
  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/PDF/zy-thesis.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/zy-thesis.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/zy-thesis.ps}
}
@phdthesis{THESE-baclet05,
  author = {Baclet, Manuel},
  title = {Applications du model-checking {\`a} des probl{\`e}mes de
		v{\'e}rification de syst{\`e}mes sur puce},
  year = 2005,
  month = dec,
  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/PDF/these-baclet.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-baclet.pdf}
}
@phdthesis{treinen-hab2005,
  author = {Treinen, Ralf},
  title = {R{\'e}solution symbolique de contraintes},
  year = 2005,
  month = nov,
  type = {M{\'e}moire d'habilitation},
  school = {Universit{\'e} Paris-Sud~11, Orsay, France},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/RT-habil.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/RT-habil.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/RT-habil.ps}
}
@phdthesis{FL-hab2005,
  author = {Laroussinie, Fran{\c{c}}ois},
  title = {Model checking temporis{\'e}~--- Algorithmes efficaces et complexit{\'e}},
  year = 2005,
  month = dec,
  type = {M{\'e}moire d'habilitation},
  school = {Universit{\'e} Paris~7, Paris, France},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FL-habil.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FL-habil.pdf}
}
@mastersthesis{pinot-master,
  author = {Pinot, Simon},
  title = {Analyse de stabilit{\'e} d'algorithme 
		 distribu{\'e}s probabilistes},
  school = {{M}aster de {L}ogique {M}ath{\'e}matique
	et {F}ondements de l'{I}nformatique, Paris, France},
  type = {Rapport de {M}aster},
  year = 2005,
  month = sep,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Pinot-M2.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Pinot-M2.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Pinot-M2.ps}
}
@mastersthesis{sznajder-master,
  author = {Sznajder, Nathalie},
  title = {Synth{\`e}se de contr{\^o}leur pour les
		syst{\`e}mes distribu{\'e}s synchrones},
  school = {{M}aster {P}arisien de {R}echerche en 
	{I}nformatique, Paris, France},
  type = {Rapport de {M}aster},
  year = 2005,
  month = sep,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sznajder-M2.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sznajder-M2.pdf}
}
@article{FL-ACMtecs05,
  publisher = {ACM Press},
  journal = {ACM Transactions in Embedded Computing Systems},
  author = {{The Artist Education Group}},
  fullauthor = {Caspi, Paul and
               Sangiovanni-Vincentelli, Alberto L. and
               Almeida Lu{\'\i}s and
               Benveniste, Albert and
               Bouyssounouse, Bruno and
               Buttazzo, Giorgio C. and
               Crnkovic, Ivica and
               Damm, Werner and
               Engblom, Jakob and
               Fohler, Gerhard and
               Garc{\'\i}a-Valls, Marisol and
               Kopetz, hermann and
               Lakhnech, Yassine and
               Laroussinie, Fran{\c{c}}ois and
               Lavagno, Luciano and
               Lipari, Guiseppe and
               Maraninchi, Florence and
               Peti, Philipp and
               Antonio de la Puente, Juan and
               Scaife, Norman and
               Sifakis, Joseph and
               de{ }Simone, Robert and
               T{\"o}rngren, Martin and
               Ver{\'\i}ssimo, Paulo and
               Wellings, Andy J. and
               Wilhelm, Reinhard and
               Willemse, Tim A. C. and
               Yi, Wang},
  title = {Guidelines for a graduate curriculum on embedded software
               and systems},
  volume = 4,
  number = 3,
  year = 2005,
  month = aug,
  pages = {587-611},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Artist-tecs05.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Artist-tecs05.pdf},
  doi = {10.1145/1086519.1086526},
  abstract = {The design of embedded real-time systems requires skills from
multiple specific disciplines, including, but not limited to, control,
computer science, and electronics. This often involves experts from differing
backgrounds, who do not recognize that they address similar, if not identical,
issues from complementary angles. Design methodologies are lacking in rigor
and discipline so that demonstrating correctness of an embedded design, if at
all possible, is a very expensive proposition that may delay significantly the
introduction of a critical product. While the economic importance of embedded
systems is widely acknowledged, academia has not paid enough attention to the
education of a community of high-quality embedded system designers, an obvious
difficulty being the need of interdisciplinarity in a period where
specialization has been the target of most education systems. This paper
presents the reflections that took place in the European Network of Excellence
Artist leading us to propose principles and structured contents for building
curricula on embedded software and systems.}
}
@techreport{FGRV-ulb05,
  author = {Finkel, Alain and Geeraerts, Gilles and Raskin, Jean-Fran{\c{c}}ois and
 	       Van{~}Begin, Laurent},
  title = {A counter-example the the minimal coverability tree algorithm},
  institution = {Universit\'e Libre de Bruxelles, Belgium},
  year = {2005},
  number = {535},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/FGRV-ulb05.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FGRV-ulb05.pdf},
  abstract = {In [Finkel, 1993], an~algorithm to compute a minimal
    coverability tree for Petri nets has been presented. This document
    demonstrates, thanks to a simple counter-example, that this algorithm may
    compute an under-approximation of a coverability tree, i.e., a~tree whose
    set of nodes is not sufficient to cover all the reachable markings.}
}
@article{BC-JALC2005,
  journal = {Journal of Automata, Languages and Combinatorics},
  author = {Bouyer, Patricia and Chevalier, Fabrice},
  title = {On Conciseness of Extensions of Timed Automata},
  year = 2005,
  volume = 10,
  number = 4,
  pages = {393-405},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC05-jalc.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC05-jalc.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BC05-jalc.ps},
  abstract = {In this paper we study conciseness of 
	various extensions of timed automata, and prove
	that several features like diagonal constraints or 
	updates lead to exponentially more concise timed 
	models.}
}
@misc{bouyer-cortos06,
  author = {Bouyer, Patricia},
  title = {Weighted Timed Automata: Model-Checking and Games},
  year = {2005},
  month = aug,
  howpublished = {Invited talk, Workshop CORTOS'06, Bonn, Germany}
}
@misc{bouyer-avocs05,
  author = {Bouyer, Patricia},
  title = {Optimal Timed Games},
  year = {2005},
  month = sep,
  howpublished = {Invited talk,  5th {I}nternational {W}orkshop
                  on {A}utomated {V}erification of {C}ritical {S}ystems
                  ({AVoCS}'05), Warwick, UK}
}
@misc{bouyer-infinity05,
  author = {Bouyer, Patricia},
  title = {Optimal Reachability Timed Games},
  year = {2005},
  month = aug,
  howpublished = {Invited talk, 7th {I}nternational {W}orkshop
                  on {V}erification of {I}nfinite {S}tate {S}ystems
                  ({INFINITY}'05), San Francisco, USA}
}
@inproceedings{bouyer-etr05,
  address = {Nancy, France},
  month = sep,
  year = 2005,
  noeditor = {},
  acronym = {{ETR}'05},
  booktitle = {{A}ctes de la 4{\`e}me {\'E}cole {T}emps-{R}{\'e}el ({ETR}'05)},
  author = {Bouyer, Patricia},
  title = {An Introduction to Timed Automata},
  pages = {111-123},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-etr05.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-etr05.pdf}
}
@inproceedings{bouyer-artist2-05,
  author = {Bouyer, Patricia},
  title = {Foundations of Timed Systems},
  booktitle = {Proc. of the ARTIST2 Summer School on Component \&
   Modelling, Testing \& Verification, and Statical Analysis of Embedded
   Systems},
  address = {N{\"a}sslingen, Sweden},
  month = sep # {-} # oct,
  year = {2005},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-nasslingen.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-nasslingen.pdf}
}
@misc{Demri0506,
  author = {Demri, St{\'e}phane},
  title = {Temporal logics},
  year = {2005},
  note = {Course notes, {M}aster {P}arisien de {R}echerche en 
	{I}nformatique, Paris, France},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Demri-2.8-TL.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Demri-2.8-TL.pdf}
}
@mastersthesis{bouchy-master,
  author = {Bouchy, Florent},
  title = {Biblioth{\`e}que de m{\'e}thodes pour la 
            classification},
  school = {{M}aster {R}echerche 
	{I}nformatique, Tours, France},
  type = {Rapport de {M}aster},
  year = 2005,
  month = sep
}
@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.