@article{CL-tsi06, publisher = {Herm{\`e}s}, journal = {Technique et Science Informatiques}, author = {Cassez, Franck and Laroussinie, Fran{\c{c}}ois}, editor = {Cassez, Franck and Laroussinie, Fran{\c{c}}ois}, title = {Contr{\^o}le des applications temps-r{\'e}el~: mod{\`e}les temporis{\'e}s et hybrides}, volume = 25, number = 3, year = 2006, url = {http://www.lavoisier.fr/notice/fr2746214830.html} }

@incollection{jgl-encyc06, author = {Goubault{-}Larrecq, Jean}, title = {Preuve et v{\'e}rification pour la s{\'e}curit{\'e} et la s{\^u}ret{\'e}}, booktitle = {Encyclop{\'e}die de l'informatique et des syst{\`e}mes d'information}, editor = {Akoka, Jacky and Comyn-Wattiau, Isabelle}, pages = {683-703}, publisher = {Vuibert}, year = 2006, month = dec, chapter = {I.6}, url = {http://www.vuibert.com/livre12401.html}, abstract = {La s\^uret\'e, comme la s\'ecurit\'e, \'enonce qu'un mal n'arrive jamais. Le but de cet article est de d\'efinir la notion de propri\'et\'e de s\^uret\'e, et d'en d\'ecrire quelques techniques de v\'erification et de preuve~: model-checking, interpr\'etation abstraite notamment. Apr\`es avoir remarqu\'e qu'il n'y avait pas de s\'ecurit\'e sans s\^uret\'e, il est expliqu\'e que l'analyse de s\'ecurit\'e d'un syst\`eme repose sur un mod\`ele, des hypoth\`eses, des propri\'et\'es \`a v\'erifier, et une architecture de s\'ecurit\'e. Finalement, il est donn\'e un aper\c{c}u de quelques mod\`eles et m\'ethodes de preuve de protocoles cryptographiques.} }

@inproceedings{BJ-secret06, address = {Venice, Italy}, month = jul, year = 2006, editor = {Fern{\'a}ndez, Maribel and Kirchner, Claude}, acronym = {{SecReT}'06}, booktitle = {{P}reliminary {P}roceedings of the 1st {I}nternational {W}orkshop on {S}ecurity and {R}ewriting {T}echniques ({SecReT}'06)}, author = {Bouhoula, Adel and Jacquemard, Florent}, title = {Security Protocols Verification with Implicit Induction and Explicit Destructors}, pages = {37-44}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BJ-secret06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BJ-secret06.pdf}, abstract = {We present a new method for automatic implicit induction theorem proving, and its application for the verification of a key distribution cryptographic protocol. The~method can handle axioms between constructor terms, a~feature generally not supported by other induction procedure. We~use such axioms in order to specify explicit destructors representing cryptographic operators.} }

@inproceedings{BBS-forte06, address = {Paris, France}, month = sep, year = 2006, volume = 4229, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Najm, Elie and Pradat{-}Peyre, Jean-Fran{\c{c}}ois and Vigui{\'e} Donzeau-Gouge, V{\'e}ronique}, acronym = {{FORTE}'06}, booktitle = {{P}roceedings of 26th {IFIP} {WG6.1} {I}nternational {C}onference on {F}ormal {T}echniques for {N}etworked and {D}istributed {S}ystems ({FORTE}'06)}, author = {Baier, Christel and Bertrand, Nathalie and Schnoebelen, {\relax Ph}ilippe}, title = {Symbolic verification of communicating systems with probabilistic message losses: liveness and fairness}, pages = {212-227}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBS-forte06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBS-forte06.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBS-forte06.ps}, doi = {10.1007/11888116_17}, abstract = {NPLCS's are a new model for nondeterministic channel systems where unreliable communication is modeled by probabilistic message losses. We~show that, for \(\omega\)-regular linear-time properties and finite-memory schedulers, qualitative model-checking is decidable. The~techniques extend smoothly to questions where fairness restrictions are imposed on the schedulers. The~symbolic procedure underlying our decidability proofs has been implemented and used to study a simple protocol handling two-way transfers in an unreliable setting.} }

@inproceedings{BP06, address = {Taipei, Taiwan}, month = aug, year = 2006, volume = 4094, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, editor = {Ibarra, Oscar H. and Yen, Hsu-Chun}, acronym = {{CIAA}'06}, booktitle = {{P}roceedings of the 11th {I}nternational {C}onference on {I}mplementation and {A}pplication of {A}utomata ({CIAA}'06)}, author = {Baclet, Manuel and Pagetti, Claire}, title = {Around {H}opcroft's Algorithm}, pages = {114-125}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BP-ciaa06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BP-ciaa06.pdf}, doi = {10.1007/11812128_12}, abstract = {In this paper, a reflection is made on an indeterminism inherent to Hopcroft's minimization algorithm: the splitter choice. We have implemented two natural policies (FIFO and~FILO) for managing the set of splitters for which we obtain the following practical results: the FILO strategy performs better than the FIFO strategy, in the case of a one letter alphabet, the FILO practical complexity never exceeds a linear one and our implementation is more efficient than the minimization algorithm of the FSM tool. This implementation is being integrated in a finite automata library, the Dash library. Thus, we present an efficient manner to manipulate automata by using canonical minimal automata.} }

@inproceedings{abw-fossacs2006, address = {Vienna, Austria}, month = mar, year = 2006, volume = 3921, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Aceto, Luca and Ing{\'o}lfsd{\'o}ttir, Anna}, acronym = {{FoSSaCS}'06}, booktitle = {{P}roceedings of the 9th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'06)}, author = {Abadi, Mart{\'\i}n and Baudet, Mathieu and Warinschi, Bogdan}, title = {Guessing Attacks and the Computational Soundness of Static Equivalence}, pages = {398-412}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABW_Fossacs06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABW_Fossacs06.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ABW_Fossacs06.ps}, doi = {10.1007/11690634_27}, abstract = {The indistinguishability of two pieces of data (or two lists of pieces of data) can be represented formally in terms of a relation called static equivalence. Static equivalence depends on an underlying equational theory. The choice of an inappropriate equational theory can lead to overly pessimistic or overly optimistic notions of indistinguishability, and in turn to security criteria that require protection against impossible attacks or ---worse yet--- that ignore feasible ones. In this paper, we define and justify an equational theory for standard, fundamental cryptographic operations. This equational theory yields a notion of static equivalence that implies computational indistinguishability. Static equivalence remains liberal enough for use in applications. In particular, we develop and analyze a principled formal account of guessing attacks in terms of static equivalence.} }

@inproceedings{BKRS-fsttcs2006, address = {Kolkata, India}, month = dec, year = 2006, volume = 4337, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Garg, Naveen and Arun-Kumar, S.}, acronym = {{FSTTCS}'06}, booktitle = {{P}roceedings of the 26th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'06)}, author = {Bozzelli, Laura and K{\v{r}}et{\'\i}nsk{\'y}, Mojm{\'\i}r and {\v{R}}eh{\'a}k, Vojt{\v{e}}ch and Strej{\v c}ek, Jan}, title = {On Decidability of {LTL} Model Checking for Process Rewrite Systems}, pages = {248-259}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKRS-fsttcs06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKRS-fsttcs06.pdf}, doi = {10.1007/11944836_24} }

@inproceedings{BLMR-fsttcs2006, address = {Kolkata, India}, month = dec, year = 2006, volume = 4337, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Garg, Naveen and Arun-Kumar, S.}, acronym = {{FSTTCS}'06}, booktitle = {{P}roceedings of the 26th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'06)}, author = {Bouyer, Patricia and Larsen, Kim G. and Markey, Nicolas and Rasmussen, Jacob Illum}, title = {Almost Optimal Strategies in One-Clock Priced Timed Automata}, pages = {345-356}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLMR-fsttcs06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLMR-fsttcs06.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BLMR-fsttcs06.ps}, doi = {10.1007/11944836_32}, abstract = {We consider timed games extended with cost information, and prove computability of the optimal cost and of \(\epsilon\)-optimal memoryless strategies in timed games with one~clock. In~contrast, this problem has recently been proved undecidable for timed games with three clocks.} }

@proceedings{GDV06, editor = {Bouyer, Patricia and Madhusudan, P.}, title = {Proceedings of the 3rd Workshop on Games in Design and Verification ({GDV}'06)}, booktitle = {Proceedings of the 3rd Workshop on Games in Design and Verification ({GDV}'06)}, address = {Seattle, Washington, USA}, year = 2006, month = aug }

@inproceedings{BBBL-atva06, address = {Beijing, China}, month = oct, year = {2006}, volume = 4218, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Graf, Susanne and Zhang, Wenhui}, acronym = {{ATVA}'06}, booktitle = {{P}roceedings of the 4th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'06)}, author = {Bel{ }mokadem, Houda and B{\'e}rard, B{\'e}atrice and Bouyer, Patricia and Laroussinie, Fran{\c{c}}ois}, title = {Timed temporal logics for abstracting transient states}, pages = {337-351}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBL-atva06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBL-atva06.pdf}, doi = {10.1007/11901914_26}, abstract = {In previous work, the timed logic TCTL was extended with an {"}almost everywhere{"} Until modality which abstracts negligible sets of positions (i.e.,~with a null duration) along a run of a timed automaton. We~propose here an extension of this logic with more powerful modalities, in order to specify properties abstracting transient states, which are events that last for less than k time units. Our main result is that modelchecking is still decidable and PSPACE-complete for this extension. On the other hand, a second semantics is defined, in which we consider the total duration where the property does not hold along a run. In~this case, we prove that model-checking is undecidable.} }

@inproceedings{BBC-concur06, address = {Bonn, Germany}, month = aug, year = 2006, volume = 4137, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Baier, Christel and Hermanns, Holger}, acronym = {{CONCUR}'06}, booktitle = {{P}roceedings of the 17th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'06)}, author = {Bouyer, Patricia and Bozzelli, Laura and Chevalier, Fabrice}, title = {Controller Synthesis for {MTL} Specifications}, pages = {450-464}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-concur06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-concur06.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBC-concur06.ps}, doi = {10.1007/11817949_30}, abstract = {We consider the control problem for timed automata against specifications given as MTL formulas. The logic MTL is a linear-time timed temporal logic which extends LTL with timing constraints on modalities, and recently, its model-checking has been proved decidable in several cases. We investigate these decidable fragments of MTL (full MTL when interpreted over finite timed words, and SafetyMTL when interpreted over infinite timed words), and prove two kinds of results. (1)~We first prove that, contrary to model-checking, the control problem is undecidable. Roughly, the computation of a lossy channel system could be encoded as a model-checking problem, and we prove here that a perfect channel system can be encoded as a control problem. (2)~We then prove that if we fix the resources of the controller (by resources we mean clocks and constants that the controller can use), the control problem becomes decidable. This decidability result relies on properties of well (and better) quasi-orderings.} }

@article{BBLP-STTT05, publisher = {Springer}, journal = {International Journal on Software Tools for Technology Transfer}, author = {Behrmann, Gerd and Bouyer, Patricia and Larsen, Kim G. and Pel{\'a}nek, Radek}, title = {Lower and Upper Bounds in Zone-Based Abstractions of Timed Automata}, year = 2006, month = jun, pages = {204-215}, number = 3, volume = 8, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBLP-STTT05.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBLP-STTT05.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBLP-STTT05.ps}, doi = {10.1007/s10009-005-0190-0}, abstract = {The semantics of timed automata is defined using an infinite-state transition system. For verification purposes, one usually uses zone based abstractions w.r.t.~the maximal constants to which clocks of the timed automaton are compared. We show that by distinguishing maximal lower and upper bounds, significantly coarser abstractions can be obtained. We show soundness and completeness of the new abstractions w.r.t.~reachability. We demonstrate how information about lower and upper bounds can be used to optimise the algorithm for bringing a difference bound matrix into normal form. Finally, we experimentally demonstrate that the new techniques dramatically increases the scalability of the real-time model checker~{\scshape Uppaal}.} }

@article{BC06-beatcs, publisher = {European Association for Theoretical Computer Science}, journal = {EATCS Bulletin}, author = {Bouyer, Patricia and Chevalier, Fabrice}, title = {On the Control of Timed and Hybrid Systems}, volume = 89, year = {2006}, month = jun, pages = {79-96}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC-beatcs89.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC-beatcs89.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BC-beatcs89.ps}, abstract = {In this paper, we survey some of the results which have been obtained the last ten years on the control of hybrid and timed systems.} }

@inproceedings{BBC-lics2006, address = {Seattle, Washington, USA}, month = aug, year = 2006, publisher = {{IEEE} Computer Society Press}, acronym = {{LICS}'06}, booktitle = {{P}roceedings of the 21st {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'06)}, author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and Chevalier, Fabrice}, title = {Control in o-Minimal Hybrid Systems}, pages = {367-378}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-lics06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-lics06.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBC-lics06.ps}, doi = {10.1109/LICS.2006.22}, abstract = {In this paper, we consider the control of general hybrid systems. In this context we show that time-abstract bisimulation is not adequate for solving such a problem. That is why we consider an other equivalence, namely the suffix equivalence based on the encoding of trajectories through words. We show that this suffix equivalence is in general a correct abstraction for control problems. We apply this result to o-minimal hybrid systems, and get decidability and computability results in this framework.} }

@inproceedings{BLP-cav06, address = {Seattle, Washington, USA}, month = aug, year = 2006, volume = 4144, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Ball, {\relax Th}omas and Jones, Robert B.}, acronym = {{CAV}'06}, booktitle = {{P}roceedings of the 18th {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV}'06)}, author = {Bardin, S{\'e}bastien and Leroux, J{\'e}r{\^o}me and Point, G{\'e}rald}, title = {{FAST} {E}xtended {R}elease}, pages = {63-66}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLP-cav06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLP-cav06.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BLP-cav06.ps}, doi = {10.1007/11817963_9}, abstract = {{\scshape Fast} is a tool designed for the analysis of counter systems, \emph{i.e.}~automata extended with unbounded integer variables. Despite the reachability set is not recursive in general, Fast implements several innovative techniques such as acceleration and circuit selection to solve this problem in practice. In its latest version, the tool is built upon an open architecture: the Presburger library is manipulated through a clear and convenient interface, thus any Presburger arithmetics package can be plugged to the tool. We provide four implementations of the interface using Lash, Mona, Omega and a new shared automata package with computation cache. Finally new features are available, like different acceleration algorithms.} }

@inproceedings{BFLS-avis06, address = {Vienna, Austria}, month = apr, year = 2006, editor = {Bharadwaj, Ramesh}, acronym = {{AVIS}'06}, booktitle = {{P}roceedings of the 5th {I}nternational {W}orkshop on {A}utomated {V}erification of {I}nfinite-{S}tate {S}ystems ({AVIS}'06)}, author = {Bardin, S{\'e}bastien and Finkel, Alain and Lozes, {\'E}tienne and Sangnier, Arnaud}, title = {From Pointer Systems to Counter Systems Using Shape Analysis}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFLS-AVIS-06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFLS-AVIS-06.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BFLS-AVIS-06.ps}, abstract = {We aim at checking safety properties on systems manipulating dynamic linked lists. First we prove that every pointer system is bisimilar to an effectively constructible counter system. We then deduce a two-step analysis procedure. We first build an over-approximation of the reachability set of the pointer system. If this over-approximation is too coarse to conclude, we then extract from it a bisimilar counter system which is analyzed via efficient symbolic techniques developed for general counter systems.} }

@inproceedings{edos2006wsl, address = {Porto Allegre, Brazil}, month = apr, year = 2006, editor = {Berger, Olivier}, acronym = {{IWFS}'06}, booktitle = {{P}roceedings of the {I}nternational {W}orkshop on {F}ree {S}oftware ({IWFS}'06)}, author = {Boender, Jaap and Di Cosmo, Roberto and Durak, Berke and Leroy, Xavier and Mancinelli, Fabio and Morgado, Mario and Pinheiro, David and Treinen, Ralf and Trezentos, Paulo and Vouillon, J{\'e}r{\^o}me}, title = {News from the {EDOS} project: improving the maintenance of free software distributions}, pages = {199-207}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/wsl06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/wsl06.pdf}, abstract = {The EDOS research project aims at contributing to the quality assurance of free software distributions. This is a major technical and engineering challenge, due to the size and complexity of these distributions (tens of thousands of software packages). We present here some of the challenges that we have tackled so far, and some of the advanced tools that are already available to the community as an outcome of the first year of work. } }

@inproceedings{edos2006ase, address = {Tokyo, Japan}, month = sep, year = 2006, publisher = {{IEEE} Computer Society Press}, acronym = {{ASE}'06}, booktitle = {{P}roceedings of the 21st {IEEE}/{ACM} {I}nternational {C}onference on {A}utomated {S}oftware {E}ngineering ({ASE}'06)}, author = {Mancinelli, Fabio and Boender, Jaap and Di Cosmo, Roberto and Vouillon, J{\'e}r{\^o}me and Durak, Berke and Leroy, Xavier and Treinen, Ralf}, title = {Managing the Complexity of Large Free and Open Source Package-Based Software Distributions}, pages = {199-208}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/edos-ase06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/edos-ase06.pdf}, doi = {10.1109/ASE.2006.49}, abstract = {The widespread adoption of Free and Open Source Software~(FOSS) in many strategic contexts of the information technology society has drawn the attention on the issues regarding how to handle the complexity of assembling and managing a huge number of (packaged) components in a consistent and effective~way. FOSS~distributions (and~in particular GNU\slash Linux-based~ones) have always provided tools for managing the tasks of installing, removing and upgrading the (packaged) components they were made~of. While these tools provide a (not always effective) way to handle these tasks on the client side, there is still a lack of tools that could help the distribution editors to maintain, on the server side, large and high-quality distributions. In~this paper we present our research whose main goal is to fill this gap: we~show our approach, the tools we have developed and their application with experimental results. Our~contribution provides an effective and automatic way to support distribution editors in handling those issues that were, until now, mostly addressed using ad-hoc tools and manual techniques.} }

@inproceedings{BKSS-tacas06, address = {Vienna, Austria}, month = mar, year = 2006, volume = {3920}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Hermanns, Holger and Palsberg, Jens}, acronym = {{TACAS}'06}, booktitle = {{P}roceedings of the 12th {I}nternational {C}onference on {T}ools and {A}lgorithms for {C}onstruction and {A}nalysis of {S}ystems ({TACAS}'06)}, author = {Bollig, Benedikt and Kern, Carsten and Schl{\"u}tter, Markus and Stolz, Volker}, title = {{MSC}an: A Tool for Analyzing {MSC} Specifications}, pages = {455-458}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSCan.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSCan.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MSCan.ps}, doi = {10.1007/11691372_32}, abstract = {We present the tool MSCan, which supports MSC-based system development. In particular, it automatically checks high-level MSC specifications for implementability.} }

@article{BBM-ipl06, publisher = {Elsevier Science Publishers}, journal = {Information Processing Letters}, author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and Markey, Nicolas}, title = {Improved Undecidability Results on Weighted Timed Automata}, year = 2006, month = jun, volume = 98, number = 5, pages = {188-194}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/IPL-BBM06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/IPL-BBM06.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/IPL-BBM06.ps}, doi = {10.1016/j.ipl.2006.01.012}, abstract = {In this paper, we improve two recent undecidability results of Brihaye, Bruy{\`e}re and Raskin about weighted timed automata, an extension of timed automata with a cost variable. Our results rely on a new encoding of the two counters of a Minsky machine that only require three clocks and one stopwatch cost, while previous reductions required five clocks and one stopwatch cost.} }

@inproceedings{BBS-lpar06, address = {Phnom Penh, Cambodia}, month = nov, year = 2006, volume = 4246, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, editor = {Hermann, Miki and Voronkov, Andrei}, acronym = {{LPAR}'06}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {L}ogic for {P}rogramming, {A}rtificial {I}ntelligence, and {R}easoning ({LPAR}'06)}, author = {Baier, Christel and Bertrand, Nathalie and Schnoebelen, {\relax Ph}ilippe}, title = {On Computing Fixpoints in Well-Structured Regular Model Checking, with Applications to Lossy Channel Systems}, pages = {347-361}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBS-lpar06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBS-lpar06.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBS-lpar06.ps}, doi = {10.1007/11916277_24}, abstract = {We prove a general finite convergence theorem for {"}upward-guarded{"} fixpoint expressions over a well-quasi-ordered~set. This has immediate applications in regular model checking of well-structured systems, where a main issue is the eventual convergence of fixpoint computations. In~particular, we are able to directly obtain several new decidability results on lossy channel systems.} }

@article{BBS-ipl05, publisher = {Elsevier Science Publishers}, journal = {Information Processing Letters}, author = {Baier, Christel and Bertrand, Nathalie and Schnoebelen, {\relax Ph}ilippe}, title = {A note on the attractor-property of infinite-state {M}arkov chains}, year = 2006, month = jan, number = 2, volume = 97, pages = {58-63}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/IPL-BBS.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/IPL-BBS.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/IPL-BBS.ps}, doi = {10.1016/j.ipl.2005.09.011}, abstract = {In the past five years, a series of verification algorithms has been proposed for infinite Markov chains that have a finite attractor, \emph{i.e.}, a set that will be visited infinitely often almost surely starting from any state. \par In this paper, we establish a sufficient criterion for the existence of an attractor. We show that if the states of a Markov chain can be given levels (positive integers) such that the expected next level for states at some level \(n > 0\) is less than \(n-\Delta\) for some positive \(\Delta\), then the states at level~\(0\) constitute an attractor for the chain. As an application, we obtain a direct proof that some probabilistic channel systems combining message losses with duplication and insertion errors have a finite attractor.} }

@inproceedings{BG-lpar06, address = {Phnom Penh, Cambodia}, month = nov, year = 2006, volume = 4246, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, editor = {Hermann, Miki and Voronkov, Andrei}, acronym = {{LPAR}'06}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {L}ogic for {P}rogramming, {A}rtificial {I}ntelligence, and {R}easoning ({LPAR}'06)}, author = {Bozzelli, Laura and Gascon, R{\'e}gis}, title = {Branching Time Temporal Logic Extended with {P}resburger Constraints}, pages = {197-211}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BG-LPAR06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BG-LPAR06.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BG-LPAR06.ps}, doi = {10.1007/11916277_14}, abstract = {Recently, \(\mathrm{LTL}\) extended with atomic formulas built over a constraint language interpreting variables in~\(\mathbb{Z}\) has been shown to have a decidable satisfiability and model-checking problem. This~language allows to compare the variables at different states of the model and include periodicity constraints, comparison constraints, and a restricted form of quantification. On the other hand, the \(\mathrm{CTL}\) counterpart of this logic (and hence also its \(\mathrm{CTL}^{*}\) counterpart which subsumes both \(\mathrm{LTL}\) and~\(\mathrm{CTL}\)) has an undecidable model-checking problem. In~this paper, we substantially extend the decidability border, by considering a meaningful fragment of \(\mathrm{CTL}^{*}\) extended with such constraints (which subsumes both the universal and existential fragments, as well as the \(\mathrm{EF}\)-like fragment) and show that satisfiability and model-checking over relational automata that are abstraction of counter machines are decidable. The~correctness and the termination of our algorithm rely on a suitable well quasi-ordering defined over the set of variable valuations.} }

@misc{chevalier-prefsttcs06, author = {Chevalier, Fabrice}, title = {Decision procedures for timed logics}, year = 2006, month = dec, howpublished = {Invited talk, Advances and Issues in Timed Systems, Kolkata, India} }

@misc{gastin-prefsttcs06, author = {Gastin, Paul}, title = {Refinements and Abstractions of Signal-Event (Timed) Languages}, year = 2006, month = dec, howpublished = {Invited talk, Advances and Issues in Timed Systems, Kolkata, India} }

@misc{gastin-wata06, author = {Gastin, Paul}, title = {Weigthed logics and weighted automata}, year = 2006, month = mar, howpublished = {Invited talk, Workshop Weighted Automata: Theory and Applications, Leipzig, Germany} }

@misc{gastin-epit06, author = {Gastin, Paul}, title = {Distributed synthesis: synchronous and asynchronous semantics}, year = 2006, month = may, howpublished = {Invited talk, 34{\`e}me {\'E}cole de Printemps en Informatique Th{\'e}orique, Ile de R{\'e}, France} }

@misc{gastin-mfps22, author = {Gastin, Paul}, title = {Refinements and Abstractions of Signal-Event (Timed) Languages}, year = 2006, month = may, howpublished = {Invited talk, 22nd {C}onference on {M}athematical {F}oundations of {P}rogramming {S}emantics ({MFPS}'06)} }

@inproceedings{Bouyer-MFPS22, address = {Genova, Italy}, month = may, year = 2006, volume = 158, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier Science Publishers}, editor = {Brookes, Steve and Mislove, Michael}, acronym = {{MFPS}'06}, booktitle = {{P}roceedings of the 22nd {C}onference on {M}athematical {F}oundations of {P}rogramming {S}emantics ({MFPS}'06)}, author = {Bouyer, Patricia}, title = {Weighted Timed Automata: {M}odel-Checking and Games}, pages = {3-17}, note = {Invited paper}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-mfps06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-mfps06.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/bouyer-mfps06.ps}, doi = {10.1016/j.entcs.2006.04.002}, abstract = {In this paper, we present weighted\slash priced timed automata, an extension of timed automaton with costs, and solve several interesting problems on that model.} }

@article{bid-hen-JLAP-2005, publisher = {Elsevier Science Publishers}, journal = {Journal of Logic and Algebraic Programming}, author = {Bidoit, Michel and Hennicker, Rolf}, title = {Constructor-Based Observational Logic}, year = {2006}, month = apr # {-} # may, number = {1-2}, volume = 67, pages = {3-51}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BID-HEN-JLAP.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BID-HEN-JLAP.pdf}, doi = {10.1016/j.jlap.2005.09.002}, abstract = {This paper focuses on the integration of reachability and observability concepts within an algebraic, institution-based framework. In the first part of this work, we develop the essential ingredients that are needed to define the constructor-based observational logic institution, called COL, which takes into account both the generation- and observation-oriented aspects of software systems. The underlying paradigm of our approach is that the semantics of a specification should be as loose as possible to capture all its correct realizations. We also consider the {"}black box{"} semantics of a specification which is useful to study the behavioral properties a user can observe when he\slash she is experimenting with the system.\par In the second part of this work, we develop proof techniques for structured COL-specifications. For this purpose we introduce an institution encoding from the COL institution to the institution of many-sorted first-order logic with equality and sort-generation constraints. Using this institution encoding, we can then reduce proofs of consequences of structured specifications built over COL to proofs of consequences of structured specifications written in a simple subset of the algebraic specification language {\scshape Casl}. This means, in particular, that any inductive theorem prover, such as \emph{e.g.} the Larch Prover or PVS, can be used to prove theorems over structured COL-specifications.} }

@inproceedings{BH-Goguen06, address = {San Diego, California, USA}, month = jun, year = 2006, volume = 4060, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Futatsugi, Kokichi and Jouannaud, Jean-Pierre and Meseguer, Jos{\'e}}, acronym = {{A}lgebra, {M}eaning and {C}omputation}, booktitle = {{A}lgebra, {M}eaning and {C}omputation~--- Essays dedicated to Joseph~A.~Goguen on the Occasion of His 65th~Birthday}, author = {Bidoit, Michel and Hennicker, Rolf}, title = {Proving Behavioral Refinements of {COL}-Specifications}, pages = {333-354}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BH-Goguen06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BH-Goguen06.pdf}, doi = {10.1007/11780274_18}, abstract = {The COL institution (constructor-based observational logic) has been introduced as a formal framework to specify both generation- and observation-oriented properties of software systems. In this paper we consider behavioral refinement relations between COL-specifications taking into account implementation constructions. We propose a general strategy for proving the correctness of such refinements by reduction to (standard) first-order theorem proving with induction. Technically our strategy relies on appropriate proof rules and on a lifting construction to encode the reachability and observability notions of the COL institution.} }

@inproceedings{BHR06-acsd, address = {Turku, Finland}, month = jun, year = 2006, publisher = {{IEEE} Computer Society Press}, editor = {Goossens, Kees and Petrucci, Laure}, acronym = {{ACSD}'06}, booktitle = {{P}roceedings of the 6th {I}nternational {C}onference on {A}pplication of {C}oncurrency to {S}ystem {D}esign ({ACSD}'06)}, author = {Bouyer, Patricia and Haddad, Serge and Reynier, Pierre-Alain}, title = {Extended Timed Automata and Time {P}etri Nets}, pages = {91-100}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-01.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-01.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/ rr-lsv-2006-01.ps}, doi = {10.1109/ACSD.2006.6}, abstract = {Timed Automata (TA) and Time Petri Nets (TPN) are two well-established formal models for real-time systems. Recently, a linear transformation of TA to TPNs preserving reachability properties and timed languages has been proposed, which does however not extend to larger classes of TA which would allow diagonal constraints or more general resets of clocks. Though these features do not add expressiveness, they yield exponentially more concise models. \par In this work, we propose two translations: one from extended TA to TPNs whose size is either linear or quadratic in the size of the original TA, depending on the features which are allowed; another one from a parallel composition of TA to TPNs, which is also linear. As a consequence, we get that TPNs are exponentially more concise than~TA.} }

@inproceedings{BHR-ICALP2006, address = {Venice, Italy}, month = jul, year = 2006, volume = 4052, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Buglesi, Michele and Preneel, Bart and Sassone, Vladimiro and Wegener, Ingo}, acronym = {{ICALP}'06}, booktitle = {{P}roceedings of the 33rd {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'06)~--- {P}art~{II}}, author = {Bouyer, Patricia and Haddad, Serge and Reynier, Pierre-Alain}, title = {Timed {P}etri Nets and Timed Automata: On the Discriminating Power of {Z}eno Sequences}, pages = {420-431}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-icalp06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-icalp06.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BHR-icalp06.ps}, doi = {10.1007/11787006_36}, abstract = {Timed Petri nets and timed automata are two standard models for the analysis of real-time systems. In this paper, we prove that they are incomparable for the timed language equivalence. Thus we propose an extension of timed Petri nets with read-arcs~(RA-TdPN), whose coverability problem is decidable. We also show that this model unifies timed Petri nets and timed automata. Then, we establish numerous expressiveness results and prove that Zeno behaviours discriminate between several sub-classes of RA-TdPNs. This has surprising consequences on timed automata, \emph{e.g.}~on the power of non-deterministic clock resets.} }

@inproceedings{BHR-atva06, address = {Beijing, China}, month = oct, year = {2006}, volume = 4218, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Graf, Susanne and Zhang, Wenhui}, acronym = {{ATVA}'06}, booktitle = {{P}roceedings of the 4th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'06)}, author = {Bouyer, Patricia and Haddad, Serge and Reynier, Pierre-Alain}, title = {Timed Unfoldings for Networks of Timed Automata}, pages = {292-306}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-atva06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-atva06.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BHR-atva06.ps}, doi = {10.1007/11901914_23}, abstract = {Whereas partial order methods have proved their efficiency for the analysis of discrete-event systems, their application to timed systems remains a challenging research topic. Here, we design a verification algorithm for networks of timed automata with invariants. Based on the unfolding technique, our method produces a branching process as an acyclic Petri net extended with read arcs. These arcs verify conditions on tokens without consuming them, thus expressing concurrency between conditions checks. They are useful for avoiding the explosion of the size of the unfolding due to clocks which are compared with constants but not reset. Furthermore, we attach zones to events, in addition to markings. We~then compute a complete finite prefix of the unfolding. The~presence of invariants goes against the concurrency since it entails a global synchronization on time. The use of read arcs and the analysis of the clock constraints appearing in invariants will help increasing the concurrency relation between events. Finally, the finite prefix we compute can be used to decide reachability properties, and transition enabling.} }

@incollection{BL-VAT06, author = {Bouyer, Patricia and Laroussinie, Fran{\c{c}}ois}, title = {V{\'e}rification par automates temporis{\'e}s}, booktitle = {Syst{\`e}mes temps-r{\'e}el~1~: techniques de description et de v{\'e}rification}, editor = {Navet, Nicolas}, publisher = {Herm{\`e}s}, year = 2006, month = jun, pages = {121-150}, url = {http://www.lavoisier.fr/fr/livres/index.asp?texte=2746213030&select=isbn&from=Hermes}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BL-VAT06.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BL-VAT06.ps}, isbn = {2-7462-1303-6} }

@inproceedings{BMR-latin06, address = {Valdivia, Chile}, month = mar, year = 2006, volume = 3887, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Correa, Jose R. and Hevia, Alejandro and Kiwi, Marcos}, acronym = {{LATIN}'06}, booktitle = {{P}roceedings of the 7th {L}atin {A}merican {S}ymposium on {T}heoretical {I}nformatics ({LATIN}'06)}, author = {Bouyer, Patricia and Markey, Nicolas and Reynier, Pierre-Alain}, title = {Robust Model-Checking of Linear-Time Properties in Timed Automata}, pages = {238-249}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMR-latin06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMR-latin06.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BMR-latin06.ps}, doi = {10.1007/11682462_25}, abstract = {Formal verification of timed systems is well understood, but their \emph{implementation} is still challenging. Recent works by Raskin \emph{et al.} have brought out a model of parameterized timed automata that can be used to prove \emph{implementability} of timed systems for safety properties. We define here a more general notion of robust model-checking for linear-time properties, which consists in verifying whether a property still holds even if the transitions are slightly delayed or expedited. We provide PSPACE algorithms for the robust model-checking of B{\"u}chi-like and LTL properties. We also verify bounded-response-time properties. } }

@book{Bollig06, author = {Bollig, Benedikt}, title = {Formal Models of Communicating Systems~--- Languages, Automata, and Monadic Second-Order Logic}, year = {2006}, month = jun, publisher = {Springer}, isbn = {3-540-32922-6}, otherurl = {http://www.springer.com/978-3-540-32922-6}, url = {http://www.lsv.ens-cachan.fr/~bollig/fmcs/}, abstract = {This book studies the relationship between automata and monadic second-order logic, focusing on classes of automata that describe the concurrent behavior of distributed systems.\par It provides a unifying theory of communicating automata and their logical properties. Based on Hanf's Theorem and Thomas's graph acceptors, it develops a result that allows us to characterize many popular models of distributed computation in terms of the existential fragment of monadic second-order logic. In particular, the book covers finite automata, asynchronous (cellular) automata, communicating finite-state machines, and lossy channel systems. Model behavior is described using graphs and partial orders, leading to the notions of Mazurkiewicz traces, message sequence charts, and live sequence charts.\par This book is suitable for senior undergraduate and graduate courses on advanced automata theory, concurrency and communication issues. It can also be used as a reference by researchers concerned with the formal modeling of concurrent systems. Some knowledge of automata theory is a prerequisite. Numerous exercises, chapter summaries, and suggested reading allow for self-study, while the book is supported with a website containing course material and solutions.} }

@inproceedings{BS05-express, address = {San Francisco, California, USA}, month = jul, year = 2006, number = 3, volume = 154, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier Science Publishers}, editor = {Baeten, Jos and Phillips, Iain}, acronym = {{EXPRESS}'05}, booktitle = {{P}roceedings of the 12th {I}nternational {W}orkshop on {E}xpressiveness in {C}oncurrency ({EXPRESS}'05)}, author = {Bertrand, Nathalie and Schnoebelen, {\relax Ph}ilippe}, title = {A short visit to the {STS} hierarchy}, pages = {59-69}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BS05-express.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BS05-express.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BS05-express.ps}, doi = {10.1016/j.entcs.2006.05.007}, abstract = {The hierarchy of Symbolic Transition Systems, introduced by Henzinger, Majumdar and Raskin, is an elegant classification tool for some families of infinite-state operational models that support some variants of a symbolic {"}backward closure{"} verification algorithm. It was first used and illustrated with families of hybrid systems.\par In this paper we investigate whether the STS hierarchy can account for classical families of infinite-state systems outside of timed or hybrid systems.} }

@inproceedings{TED-hldvt06, address = {Monterey, California, USA}, month = nov, year = 2006, publisher = {{IEEE} Computer Society Press}, acronym = {{HLDVT}'06}, booktitle = {{P}roceedings of the {IEEE} {H}igh {L}evel {D}esign {V}erification and {T}est Workshop ({HLDVT}'06)}, author = {Taktak, Sami and Encrenaz, Emmanuelle and Desbarbieux, Jean-Lou}, title = {A Tool for Automatic Detection of Deadlock in Wormhole Networks on Chip}, pages = {203-210}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/TED-hldvt06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/TED-hldvt06.pdf}, doi = {10.1109/HLDVT.2006.319992}, abstract = {We present an extension of Duato's necessary and sufficient condition a routing function must satisfy in order to be deadlock-free, to support environment constraints inducing extra-dependencies between messages. We also present an original algorithm to automatically check the deadlock-freeness of a network with a given routing function. A~prototype tool has been developed and automatic deadlock checking of large scale networks with various routing functions have been successfully achieved.} }

@inproceedings{BE-rsp06, address = {Chania, Crete}, month = jun, year = 2006, publisher = {{IEEE} Computer Society Press}, acronym = {{RSP}'06}, booktitle = {{P}roceedings of the 17th {I}nternational {W}orkshop on {R}apid {S}ystem {P}rototyping ({RSP}'06)}, author = {Braunstein, C{\'e}cile and Encrenaz, Emmanuelle}, title = {Formalizing the incremental design and verification process of a pipelined protocol converter}, pages = {103-109}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BE-rsp06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BE-rsp06.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BE-rsp06.ps}, doi = {10.1109/RSP.2006.19}, abstract = {This work studies the relations between pipeline architectures and their specification expressed in~CTL. We propose a method to build pipeline structures incrementally from a simple one (already verified) to a more complex one. Moreover, we show how each increment can be integrated in a CTL specification. We define increments to model treatment delay and treatment abortion of a pipeline flow, and we formalize the composition of the different increments. In order to represent the increments added to an architecture, we derive a set of CTL formulae transformations. Finally we model a control flow of a protocol converter by composition of these increments. We show how CTL properties of the complex architecture are built by applying automatic transformations on the set of CTL properties of the simplest architecture.} }

@inproceedings{GSZ-fsttcs2006, address = {Kolkata, India}, month = dec, year = 2006, volume = 4337, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Garg, Naveen and Arun-Kumar, S.}, acronym = {{FSTTCS}'06}, booktitle = {{P}roceedings of the 26th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'06)}, author = {Gastin, Paul and Sznajder, Nathalie and Zeitoun, Marc}, title = {Distributed synthesis for well-connected architectures}, pages = {321-332}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GSZ-fsttcs2006.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GSZ-fsttcs2006.pdf}, doi = {10.1007/11944836_30}, abstract = {We study the synthesis problem for external linear or branching specifications and distributed, synchronous architectures with arbitrary delays on processes. External means that the specification only relates input and output variables. We~introduce the subclass of uniformly well-connected~(UWC) architectures for which there exists a routing allowing each output process to get the values of all inputs it is connected to, as soon as possible. We~prove that the distributed synthesis problem is decidable on UWC architectures if and only if the set of all sets of input variables visible by output variables is totally ordered, under set inclusion. We~also show that if we extend this class by letting the routing depend on the output process, then the previous decidability result fails. Finally, we provide a natural restriction on specifications under which the whole class of~UWC architectures is decidable.} }

@proceedings{AB-lncs4202, title = {{P}roceedings of the 4th {I}nternational {C}onference on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'06)}, booktitle = {{P}roceedings of the 4th {I}nternational {C}onference on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'06)}, editor = {Asarin, Eug{\`e}ne and Bouyer, Patricia}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = 4202, year = 2006, month = sep, address = {Paris, France}, isbn = {3-540-45026-2}, url = {http://www.springer.com/978-3-540-45026-2}, doi = {10.1007/11867340} }

@inproceedings{BGP1-formats06, address = {Paris, France}, month = sep, year = 2006, volume = 4202, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Asarin, Eug{\`e}ne and Bouyer, Patricia}, acronym = {{FORMATS}'06}, booktitle = {{P}roceedings of the 4th {I}nternational {C}onference on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'06)}, author = {B{\'e}rard, B{\'e}atrice and Gastin, Paul and Petit, Antoine}, title = {Refinements and abstractions of signal-event (timed) languages}, pages = {67-81}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGP1-formats06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGP1-formats06.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BGP1-formats06.ps}, doi = {10.1007/11867340_6}, abstract = {In the classical framework of formal languages, a refinement operation is modeled by a substitution and an abstraction by an inverse substitution. These mechanisms have been widely studied, because they describe a change in the specification level, from an abstract view to a more concrete one, or conversely. For~timed systems, there is up to now no uniform notion of substitutions. In~this paper, we study the timed substitutions in the general framework of signal-event languages, where both signals and events are taken into account. We~prove that regular signal-event languages are closed under substitutions and inverse substitutions. } }

@inproceedings{BGP2-formats06, address = {Paris, France}, month = sep, year = 2006, volume = 4202, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Asarin, Eug{\`e}ne and Bouyer, Patricia}, acronym = {{FORMATS}'06}, booktitle = {{P}roceedings of the 4th {I}nternational {C}onference on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'06)}, author = {B{\'e}rard, B{\'e}atrice and Gastin, Paul and Petit, Antoine}, title = {Intersection of regular signal-event (timed) languages}, pages = {52-66}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGP2-formats06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGP2-formats06.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BGP2-formats06.ps}, doi = {10.1007/11867340_5}, abstract = {We propose in this paper a construction for a {"}well known{"} result: regular signal-event languages are closed by intersection. In~fact, while this result is indeed trivial for languages defined by Alur and Dill's timed automata (the proof is an immediate extension of the one in the untimed case), it turns out that the construction is much more tricky when considering the most involved model of signal-event automata. While several constructions have been proposed in particular cases, it is the first time, up to our knowledge, that a construction working on finite and infinite signal-event words and taking into account signal stuttering, unobservability of zero-duration \(\tau\)-signals and Zeno runs is proposed.} }

@inproceedings{CDP-fsttcs2006, address = {Kolkata, India}, month = dec, year = 2006, volume = 4337, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Garg, Naveen and Arun-Kumar, S.}, acronym = {{FSTTCS}'06}, booktitle = {{P}roceedings of the 26th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'06)}, author = {Chevalier, Fabrice and D'Souza, Deepak and Prabhakar, Pavithra}, title = {On continuous timed automata with input-determined guards}, pages = {369-380}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDP-fsttcs06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDP-fsttcs06.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CDP-fsttcs06.ps}, doi = {10.1007/11944836_34}, abstract = {We consider a general class of timed automata parameterized by a set of {"}input-determined{"} operators, in a continuous time setting. We show that for any such set of operators, we have a monadic second order logic characterization of the class of timed languages accepted by the corresponding class of automata. Further, we consider natural timed temporal logics based on these operators, and show that they are expressively equivalent to the first-order fragment of the corresponding MSO logics. As~a~corollary of these general results we obtain an expressive completeness result for the continuous version of MTL.} }

@inproceedings{CKKW-fsttcs2006, address = {Kolkata, India}, month = dec, year = 2006, volume = 4337, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Garg, Naveen and Arun-Kumar, S.}, acronym = {{FSTTCS}'06}, booktitle = {{P}roceedings of the 26th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'06)}, author = {Cortier, V{\'e}ronique and Kremer, Steve and K{\"u}sters, Ralf and Warinschi, Bogdan}, title = {Computationally Sound Symbolic Secrecy in the Presence of Hash Functions}, pages = {176-187}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CKKW-fsttcs06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CKKW-fsttcs06.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CKKW-fsttcs06.ps}, doi = {10.1007/11944836_18}, abstract = {The standard symbolic, deducibility-based notions of secrecy are in general insufficient from a cryptographic point of view, especially in presence of hash functions. In~this paper we devise and motivate a more appropriate secrecy criterion which exactly captures a standard cryptographic notion of secrecy for protocols involving public-key enryption and hash functions: protocols that satisfy it are computationally secure while any violation of our criterion directly leads to an attack. Furthermore, we prove that our criterion is decidable via an NP decision procedure. Our~results hold for standard security notions for encryption and hash functions modeled as random oracles.} }

@article{CDL05-survey, publisher = {{IOS} Press}, journal = {Journal of Computer Security}, author = {Cortier, V{\'e}ronique and Delaune, St{\'e}phanie and Lafourcade, Pascal}, title = {A Survey of Algebraic Properties Used in Cryptographic Protocols}, year = {2006}, volume = 14, number = 1, pages = {1-43}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/surveyCDL.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/surveyCDL.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/surveyCDL.ps}, abstract = {Cryptographic protocols are successfully analyzed using formal methods. However, formal approaches usually consider the encryption schemes as black boxes and assume that an adversary cannot learn anything from an encrypted message except if he has the key. Such an assumption is too strong in general since some attacks exploit in a clever way the interaction between protocol rules and properties of cryptographic operators. Moreover, the executability of some protocols relies explicitly on some algebraic properties of cryptographic primitives such as commutative encryption. We give a list of some relevant algebraic properties of cryptographic operators, and for each of them, we provide examples of protocols or attacks using these properties. We also give an overview of the existing methods in formal approaches for analyzing cryptographic protocols.} }

@inproceedings{CEFX-formats06, address = {Paris, France}, month = sep, year = 2006, volume = 4202, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Asarin, Eug{\`e}ne and Bouyer, Patricia}, acronym = {{FORMATS}'06}, booktitle = {{P}roceedings of the 4th {I}nternational {C}onference on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'06)}, author = {Chevallier, R{\'e}my and Encrenaz{-}Tiph{\`e}ne, Emmanuelle and Fribourg, Laurent and Xu, Weiwen}, title = {Verification of the Generic Architecture of a Memory Circuit Using Parametric Timed Automata}, pages = {113-127}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CEFX-formats06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CEFX-formats06.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CEFX-formats06.ps}, econtrat = {MEDEA+ Blueberries}, doi = {10.1007/11867340_9}, abstract = {Using a variant of Clariso-Cortadella's parametric method for verifying asynchronous circuits, we formally derive a set of linear constraints that ensure the correctness of some crucial timing behaviours of the architecture of SPSMALL memory. This allows us to check two different implementations of this architecture.} }

@article{CEFX-wseas06, publisher = {World Scientific and Engineering Academy and Society}, journal = {WSEAS Transactions on Circuits and Systems}, author = {Chevallier, R{\'e}my and Encrenaz{-}Tiph{\`e}ne, Emmanuelle and Fribourg, Laurent and Xu, Weiwen}, title = {Timing analysis of an embedded memory: {SPSMALL}}, pages = {973-978}, volume = 5, number = 7, year = 2006, month = jul, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CEFX-wseas06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CEFX-wseas06.pdf}, abstract = {This paper proposes a high-level formalism, called Abstract Functional and Timing Graph~(AFTG), for describing a memory architecture, which combines logical functionality and timing. After translation of the~AFTG into the form a timed automaton, we are able to compute the response times of the modeled memory, and check their consistency with the values specified in the datasheet. We also address the problem of finding optimal values of setup timings.} }

@inproceedings{DDFG-atva06, address = {Beijing, China}, month = oct, year = {2006}, volume = 4218, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Graf, Susanne and Zhang, Wenhui}, acronym = {{ATVA}'06}, booktitle = {{P}roceedings of the 4th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'06)}, author = {Demri, St{\'e}phane and Finkel, Alain and Goranko, Valentin and van Drimmelen, Govert}, title = {Towards a model-checker for counter systems}, pages = {493-507}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDFG-atva06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDFG-atva06.pdf}, doi = {10.1007/11901914_36}, abstract = {This paper deals with model-checking of fragments and extensions of~\(\mathrm{CTL}^{*}\) on infinite-state Presburger counter systems, where the states are vectors of integers and the transitions are determined by means of relations definable within Presburger arithmetic. We have identified a natural class of admissible counter systems~(ACS) for which we show that the quantification over paths in~\(\mathrm{CTL}^{*}\) can be simulated by quantification over tuples of natural numbers, eventually allowing translation of the whole Presburger-\(\mathrm{CTL}^{*}\) into Presburger arithmetic, thereby enabling effective model checking. We have provided evidence that our results are close to optimal with respect to the class of counter systems described above. Finally, we design a complete semi-algorithm to verify first-order~\(\mathrm{LTL}\) properties over trace-flattable counter systems, extending the previous underlying FAST semi-algorithm to verify reachability questions over flattable counter systems. } }

@inproceedings{DL-lics2006, address = {Seattle, Washington, USA}, month = aug, year = 2006, publisher = {{IEEE} Computer Society Press}, acronym = {{LICS}'06}, booktitle = {{P}roceedings of the 21st {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'06)}, author = {Demri, St{\'e}phane and Lazi{\'c}, Ranko}, title = {{LTL} with the freeze quantifier and register automata}, pages = {17-26}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DL-lics2006.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DL-lics2006.pdf}, doi = {10.1109/LICS.2006.31}, abstract = {Temporal logics, first-order logics, and automata over data words have recently attracted considerable attention. A~data word is a word over a finite alphabet, together with a datum (an element of an infinite domain) at each position. Examples include timed words and XML documents. To refer to the data, temporal logics are extended with the freeze quantifier, first-order logics with predicates over the data domain, and automata with registers or pebbles.\par We investigate relative expressiveness and complexity of standard decision problems for~\(\mathrm{LTL}\) with the freeze quantifier~(\(\mathrm{LTL}^{\downarrow}\)), 2-variable first-order logic (\(\mathrm{FO}^{2}\)) over data words, and register automata. The only predicate available on data is equality. Previously undiscovered connections among those formalisms, and to counter automata with in- crementing errors, enable us to answer several questions left open in recent literature.\par We show that the future-time fragment of~\(\mathrm{LTL}^{\downarrow}\) which corresponds to \(\mathrm{FO}^{2}\) over finite data words can be extended considerably while preserving decidability, but at the expense of non-primitive recursive complexity, and that most of further extensions are undecidable. We also prove that surprisingly, over infinite data words, \(\mathrm{LTL}^{\downarrow}\) without the `until' operator, as well as nonemptiness of one-way universal register automata, are undecidable even when there is only one register.} }

@inproceedings{DL-ijcar06, address = {Seattle, Washington, USA}, month = aug, year = 2006, volume = 4130, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer-Verlag}, editor = {Furbach, Ulrich and Shankar, Natarajan}, acronym = {{IJCAR}'06}, booktitle = {{P}roceedings of the 3rd {I}nternational {J}oint {C}onference on {A}utomated {R}easoning ({IJCAR}'06)}, author = {Demri, St{\'e}phane and Lugiez, Denis}, title = {{P}resburger Modal Logic is Only {PSPACE}-complete}, pages = {541-556}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-25.pdf}, doi = {10.1007/11814771_44}, abstract = {We introduce a Presburger modal logic PML with regularity constraints and full Presburger constraints on the number of children that generalize graded modalities, also known as number restrictions in description logics. We~show that PML satisfiability is only PSPACE-complete by designing a Ladner-like algorithm that can be turned into an analytic proof system algorithm. This extends a well-known and non-trivial PSPACE upper bound for graded modal logic. Furthermore, we provide a detailed comparison with logics that contain Presburger constraints and that are dedicated to query XML documents. As~an application, we show that satisfiability for Sheaves Logic SL is PSPACE-complete, improving significantly its best known upper bound.} }

@article{delaune-tcs06, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {Delaune, St{\'e}phanie}, title = {An Undecidability Result for~{\textsf{\MakeUppercase{AG}h}}}, volume = 368, number = {1-2}, pages = {161-167}, year = 2006, month = dec, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/delaune-tcs06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/delaune-tcs06.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/delaune-tcs06.ps}, doi = {10.1016/j.tcs.2006.08.018}, abstract = {We present an undecidability result for the verification of security protocols. Since the \emph{perfect cryptography assumption} is unrealistic for cryptographic primitives with visible algebraic properties, several recent works relax this assumption, allowing the intruder to exploit these properties. We are interested in the \emph{Abelian groups} theory in combination with the homomorphism axiom. We show that satisfaisability of symbolic deducibility constraints is undecidable, obtaining in this way the first undecidability result concerning a theory for which unification is known to be decidable~[F.~Baader, Unification in commutative theories, Hilbert's basis theorem, and Gr{\"{o}}bner bases, J.~ACM~40(3) (1993)~477-503].} }

@inproceedings{DKR-wote06, address = {Cambridge, UK}, month = jun, year = 2006, acronym = {{WOTE}'06}, booktitle = {{P}roceedings of the {IAVoSS} {W}orkshop {O}n {T}rustworthy {E}lections ({WOTE}'06)}, author = {Delaune, St{\'e}phanie and Kremer, Steve and Ryan, Mark D.}, title = {Verifying Properties of Electronic Voting Protocols}, pages = {45-52}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-wote06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-wote06.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DKR-wote06.ps}, abstract = {In this paper we report on some recent work to formally specify and verify electronic voting protocols. In particular, we use the formalism of the applied pi calculus: the applied pi calculus is a formal language similar to the pi calculus but with useful extensions for modelling cryptographic protocols. We model several important properties, namely fairness, eligibility, privacy, receipt-freeness and coercion-resistance. Verification of these properties is illustrated on two cases studies and has been partially automated using the Blanchet's ProVerif tool.} }

@inproceedings{DKR-csfw06, address = {Venice, Italy}, month = jul, year = 2006, publisher = {{IEEE} Computer Society Press}, acronym = {{CSFW}'06}, booktitle = {{P}roceedings of the 19th {IEEE} {C}omputer {S}ecurity {F}oundations {W}orkshop ({CSFW}'06)}, author = {Delaune, St{\'e}phanie and Kremer, Steve and Ryan, Mark D.}, title = {Coercion-Resistance and Receipt-Freeness in Electronic Voting}, pages = {28-39}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-csfw06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-csfw06.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DKR-csfw06.ps}, doi = {10.1109/CSFW.2006.8}, abstract = {In this paper we formally study important properties of electronic voting protocols. In particular we are interested in coercion-resistance and receipt-freeness. Intuitively, an election protocol is coercion-resistant if a voter \(A\) cannot prove to a potential coercer~\(C\) that she voted in a particular way. We assume that \(A\) cooperates with~\(C\) in an interactive way. Receipt-freeness is a weaker property, for which we assume that \(A\) and~\(C\) cannot interact during the protocol, but \(A\) later provides evidence (the receipt) of how she voted. While receipt-freeness can be expressed using observational equivalence from the applied pi calculus, we need to introduce a new relation to capture coercion-resistance. Our formalization of coercion-resistance and receipt-freeness are quite different. Nevertheless, we show in accordance with intuition that coercion-resistance implies receipt-freeness, which implies privacy, the basic anonymity property of voting protocols, as defined in previous work. Finally we illustrate the definitions on a simplified version of the Lee~\emph{et~al.}\ voting protocol.} }

@inproceedings{DLLT-ICALP2006, address = {Venice, Italy}, month = jul, year = 2006, volume = 4052, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Buglesi, Michele and Preneel, Bart and Sassone, Vladimiro and Wegener, Ingo}, acronym = {{ICALP}'06}, booktitle = {{P}roceedings of the 33rd {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'06)~--- {P}art~{II}}, author = {Delaune, St{\'e}phanie and Lafourcade, Pascal and Lugiez, Denis and Treinen, Ralf}, title = {Symbolic Protocol Analysis in Presence of a Homomorphism Operator and {\emph{Exclusive~Or}}}, pages = {132-143}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLLT-icalp06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLLT-icalp06.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DLLT-icalp06.ps}, doi = {10.1007/11787006_12}, abstract = {Security of a cryptographic protocol for a bounded number of sessions is usually expressed as a symbolic trace reachability problem. We show that symbolic trace reachability for well-defined protocols is decidable in presence of the exclusive or theory in combination with the homomorphism axiom. These theories allow us to model basic properties of important cryptographic operators. This trace reachability problem can be expressed as a system of symbolic deducibility constraints for a certain inference system describing the capabilities of the attacker. One main step of our proof consists in reducing deducibility constraints to constraints for deducibility in one step of the inference system. This constraint system, in turn, can be expressed as a system of quadratic equations of a particular form over \(\mathbb{Z}/2\mathbb{Z}[h]\), the ring of polynomials in one indeterminate over the finite field \(\mathbb{Z}/2\mathbb{Z}\). We show that satisfiability of such systems is decidable. } }

@proceedings{CK-fcc2006, editor = {Cortier, V{\'e}ronique and Kremer, Steve}, booktitle = {{P}roceedings of the 2nd {W}orkshop on {F}ormal and {C}omputational {C}ryptography ({FCC}'06)}, title = {{P}roceedings of the 2nd {W}orkshop on {F}ormal and {C}omputational {C}ryptography ({FCC}'06)}, address = {Venice, Italy}, year = 2006, month = jul, url = {http://hal.inria.fr/FCC2006/} }

@article{CKS-jar2005, publisher = {Springer}, journal = {Journal of Automated Reasoning}, author = {Chadha, Rohit and Kremer, Steve and Scedrov, Andre}, title = {Formal Analysis of Multi-Party Contract Signing}, volume = 36, number = {1-2}, pages = {39-83}, year = 2006, month = jan, nmnote = {Special Issue on Automated Reasoning for Security Protocol Analysis}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/mpcs-CKS.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/mpcs-CKS.pdf}, doi = {10.1007/s10817-005-9019-5}, abstract = {We analyze the multi-party contract-signing protocols of Garay and MacKenzie (GM) and of Baum and Waidner (BW). We use a finite-state tool, {\scshape Mocha}, which allows specification of protocol properties in a branching-time temporal logic with game semantics. While our analysis does not reveal any errors in the BW protocol, in the GM protocol we discover serious problems with fairness for four signers and an oversight regarding abuse-freeness for three signers. We propose a complete revision of the GM subprotocols in order to restore fairness.} }

@article{dj-jar05, publisher = {Springer}, journal = {Journal of Automated Reasoning}, author = {Delaune, St{\'e}phanie and Jacquemard, Florent}, title = {Decision Procedures for the Security of Protocols with Probabilistic Encryption against Offline Dictionary Attacks}, volume = 36, number = {1-2}, year = 2006, month = jan, pages = {85-124}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DJ-jar05.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DJ-jar05.ps}, doi = {10.1007/s10817-005-9017-7}, abstract = {We consider the problem of formal automatic verification of cryptographic protocols when some data, like poorly chosen passwords, can be guessed by dictionary attacks. First, we define a theory of these attacks and propose an inference system modeling the deduction capabilities of an intruder. This system extends a set of well studied deduction rules for symmetric and public key encryption often called Dolev-Yao rules with the introduction of a probabilistic encryption operator and guessing abilities for the intruder. Then, we show that the intruder deduction problem in this extended model is decidable in~PTIME. The proof is based on a locality lemma for our inference system. This first result yields to an NP decision procedure for the protocol insecurity problem in presence of a passive intruder. In the active case, the same problem is proved to be NP-complete: we give a procedure for simultaneously solving symbolic constraints with variables which represent intruder deductions. We illustrate the procedure with examples of published protocols and compare our model to other recent formal definitions of dictionary attacks.} }

@article{SD-ipl05, publisher = {Elsevier Science Publishers}, journal = {Information Processing Letters}, author = {Delaune, St{\'e}phanie}, title = {Easy Intruder Deduction Problems with Homomorphisms}, volume = 97, number = 6, pages = {213-218}, month = mar, year = 2006, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SD-ipl05.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SD-ipl05.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/SD-ipl05.ps}, doi = {10.1016/j.ipl.2005.11.008}, abstract = {We present complexity results for the verification of security protocols. Since the perfect cryptography assumption is unrealistic for cryptographic primitives with visible algebraic properties, we extend the classical \emph{Dolev-Yao} model by permitting the intruder to exploit these properties. More precisely, we are interested in theories such as \emph{Exclusive or} and \emph{Abelian groups} in combination with the homomorphism axiom. We show that the intruder deduction problem is in PTIME in both cases, improving the EXPTIME complexity results presented in~(Lafourcade, Lugiez, Treinen,~2005).} }

@article{Demri06, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {Demri, St{\'e}phane}, title = {{LTL} over integer periodicity constraints}, year = {2006}, volume = 360, number = {1-3}, pages = {96-123}, month = aug, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-tcs06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-tcs06.pdf}, doi = {10.1016/j.tcs.2006.02.019}, abstract = {Periodicity constraints are used in many logical formalisms, in fragments of Presburger~LTL, in calendar logics, and in logics for access control, to quote a few examples. In the paper, we introduce the logic PLTL\(^{\mathrm{mod}}\), an extension of Linear-Time Temporal Logic LTL with past-time operators whose atomic formulae are defined from a first-order constraint language dealing with periodicity. Although the underlying constraint language is a fragment of Presburger arithmetic shown to admit a {\scshape pspace}-complete satisfiability problem, we establish that PLTL\(^{\mathrm{mod}}\) model-checking and satisfiability problems remain in {\scshape pspace} as plain~LTL (full Presburger LTL is known to be highly undecidable). This is particularly interesting for dealing with periodicity constraints since the language of PLTL\(^{\mathrm{mod}}\) has a language more concise than existing languages and the temporalization of our first-order language of periodicity constraints has the same worst case complexity as the underlying constraint language. Finally, we show examples of introduction the quantification in the logical language that provide to PLTL\(^{\mathrm{mod}}\), {\scshape expspace}-complete problems. As another application, we establish that the equivalence problem for extended single-string automata, known to express the equality of time granularities, is {\scshape pspace}-complete by designing a reduction from~QBF and by using our results for PLTL\(^{\mathrm{mod}}\). } }

@article{DLS-jcss-param, publisher = {Elsevier Science Publishers}, journal = {Journal of Computer and System Sciences}, author = {Demri, St{\'e}phane and Laroussinie, Fran{\c{c}}ois and Schnoebelen, {\relax Ph}ilippe}, title = {A Parametric Analysis of the State Explosion Problem in Model Checking}, year = 2006, month = jun, volume = 72, number = 4, pages = {547-575}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLS-jcss-param.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLS-jcss-param.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DLS-jcss-param.ps}, doi = {10.1016/j.jcss.2005.11.003}, abstract = {In model checking, the state-explosion problem occurs when one checks a non-flat system, \emph{i.e.}, a system implicitly described as a synchronized product of elementary subsystems. In this paper, we investigate the complexity of a wide variety of model checking problems for non-flat systems under the light of parameterized complexity, taking the number of synchronized components as a parameter. We provide precise complexity measures (in the parameterized sense) for most of the problems we investigate, and evidence that the results are robust.} }

@article{FGRV-tcs05, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, 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}, year = 2006, month = may, volume = 356, number = 3, pages = {374-386}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGRV-TCS04.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGRV-TCS04.pdf}, doi = {10.1016/j.tcs.2006.02.008}, abstract = {In this paper, we study the expressive power of several monotonic extensions of Petri nets. We compare the expressive power of Petri nets, Petri nets extended with \emph{non-blocking arcs} and Petri nets extended with \emph{transfer arcs}, in terms of \(\omega\)-languages. We show that the hierarchy of expressive powers of those models is strict. To prove these results, we propose \emph{original techniques} that rely on well-quasi orderings and monotonicity properties.} }

@article{FMP-dc05, publisher = {Springer}, journal = {Distributed Computing}, author = {Fribourg, Laurent and Messika, St{\'e}phane and Picaronny, Claudine}, title = {Coupling and Self-Stabilization}, year = 2006, month = feb, volume = 18, number = 3, pages = {221-232}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/dcmessika.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/dcmessika.ps}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/dcmessika.pdf}, doi = {10.1007/s00446-005-0142-7}, abstract = {A randomized self-stabilizing algorithm~\(\mathcal{A}\) is an algorithm that, whatever the initial configuration is, reaches a set~\(\mathcal{L}\) of \emph{legal configurations} in finite time with probability~1. The proof of convergence towards~\(\mathcal{L}\) is generally done by exhibiting a potential function~\(\varphi\), which measures the {"}vertical{"} distance of any configuration to~\(\mathcal{L}\), such that \(\varphi\) decreases with non-null probability at each step of~\(\mathcal{A}\). We propose here a method, based on the notion of coupling, which makes use of a {"}horizontal{"} distance~\(\delta\) between any pair of configurations, such that \(\delta\) decreases in expectation at each step of~\(\mathcal{A}\). In contrast with classical methods, our coupling method does not require the knowledge of~\(\mathcal{L}\). In addition to the proof of convergence, the method allows us to assess the convergence rate according to two different measures. Proofs produced by the method are often simpler or give better upper bounds than their classical counterparts, as examplified here on Herman's mutual exclusion and Iterated Prisoner's Dilemma algorithms in the case of cyclic graphs.} }

@inproceedings{BGM-atva2006, address = {Beijing, China}, month = oct, year = {2006}, volume = 4218, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Graf, Susanne and Zhang, Wenhui}, acronym = {{ATVA}'06}, booktitle = {{P}roceedings of the 4th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'06)}, author = {Bhateja, Puneet and Gastin, Paul and Mukund, Madhavan}, title = {A fresh look at testing for asynchronous communication}, pages = {369-383}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGM-atva06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGM-atva06.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BGM-atva06.ps}, doi = {10.1007/11901914_28}, abstract = {Testing is one of the fundamental techniques for verifying if a computing system conforms to its specification. We~take a fresh look at the theory of testing for message-passing systems based on a natural notion of observability in terms of input-output relations. We~propose two notions of test equivalence: one which corresponds to presenting all test inputs up front and the other which corresponds to interactively feeding inputs to the system under test. We compare our notions with those studied earlier, notably the equivalence proposed by Tretmans. In~Tretmans' framework, asynchrony is modelled using synchronous communication by augmenting the state space of the system with queues. We~show that the first equivalence we consider is strictly weaker than Tretmans' equivalence and undecidable, whereas the second notion is incomparable. We~also establish (un)decidability results for these equivalences.} }

@article{DG-icomp2006, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Diekert, Volker and Gastin, Paul}, title = {Pure future local temporal logics are expressively complete for {M}azurkiewicz traces}, pages = {1597-1619}, year = 2006, month = nov, volume = 204, number = 11, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-icomp06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-icomp06.pdf}, doi = {10.1016/j.ic.2006.07.002}, abstract = {The paper settles a long standing problem for Mazurkiewicz traces: the pure future local temporal logic defined with the basic modalities exists-next and until is expressively complete. This means every first-order definable language of Mazurkiewicz traces can be defined in a pure future local temporal logic. The~analogous result with a global interpretation has been known, but the treatment of a local interpretation turned out to be much more involved. Local logics are interesting because both the satisfiability problem and the model checking problem are solvable in PSPACE for these logics whereas they are non-elementary for global logics. Both, the (previously known) global and the (new) local results generalize Kamp's Theorem for words, because for sequences local and global viewpoints coincide. } }

@article{DG06-TCS, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {Diekert, Volker and Gastin, Paul}, title = {From local to global temporal logics over {M}azurkiewicz traces}, year = 2006, month = may, volume = 356, number = {1-2}, pages = {126-135}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG06-TCS.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG06-TCS.pdf}, doi = {10.1016/j.tcs.2006.01.035}, abstract = {We review some results on global and local temporal logic on Mazurkiewicz traces. Our~main contribution is to show how to derive the expressive completeness of global temporal logic with respect to first-order logic [V.~Diekert, P.~Gastin, LTL~is expressively complete for Mazurkiewicz traces, J.~Comput. System Sci.~64 (2002) 396-418] from the similar result on local temporal logic [V.~Diekert, P.~Gastin, Pure future local temporal logics are expressively complete for Mazurkiewicz traces, in: M.~Farach-Colton~(Ed.), Proc.~LATIN'04, Lecture Notes in Computer Science, Vol.~2976, Springer, Berlin, 2004, pp.~232-241, Full version available as Research Report LSV-05-22, Laboratoire Sp\'ecification et V\'erification, ENS Cachan, France].} }

@inproceedings{JRV-ijcar06, address = {Seattle, Washington, USA}, month = aug, year = 2006, volume = 4130, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer-Verlag}, editor = {Furbach, Ulrich and Shankar, Natarajan}, acronym = {{IJCAR}'06}, booktitle = {{P}roceedings of the 3rd {I}nternational {J}oint {C}onference on {A}utomated {R}easoning ({IJCAR}'06)}, author = {Jacquemard, Florent and Rusinowitch, Micha{\"e}l and Vigneron, Laurent}, title = {Tree automata with equality constraints modulo equational theories}, pages = {557-571}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-07.pdf}, doi = {10.1007/11814771_45}, abstract = {This paper presents new classes of tree automata combining automata with equality test and automata modulo equational theories. We believe that this class has a good potential for application in \emph{e.g.}~software verification. These tree automata are obtained by extending the standard Horn clause representations with equational conditions and rewrite systems. We show in particular that a generalized membership problem (extending the emptiness problem) is decidable by proving that the saturation of tree automata presentations with suitable paramodulation strategies terminates. Alternatively our results can be viewed as new decidable classes of first-order formula.} }

@misc{markey-SynthVerif06, author = {Markey, Nicolas}, title = {Verification of Multi-Agent Systems with~{ATL}}, year = 2006, month = oct, howpublished = {Invited talk, FNRS meeting on {"}Synthesis and Verification{"}} }

@article{KucSch-TCS, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {Ku{\v c}era, Anton{\'\i}n and Schnoebelen, {\relax Ph}ilippe}, title = {A General Approach to Comparing Infinite-State Systems with Their Finite-State Specifications}, number = {2-3}, volume = {358}, pages = {315-333}, month = aug, year = 2006, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KucSch-TCS.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KucSch-TCS.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/KucSch-TCS.ps}, doi = {10.1016/j.tcs.2006.01.021}, abstract = {We introduce a generic family of behavioral relations for which the regular equivalence problem (\emph{i.e.}, comparing an arbitrary transition system to some finite-state specification) can be reduced to the model checking problem against simple modal formulae. As an application, we derive decidability of several regular equivalence problems for well-known families of infinite-state systems. } }

@inproceedings{LLT-unif2006, address = {Seattle, Washington, USA}, month = aug, year = 2006, editor = {Levy, Jordi}, acronym = {{UNIF}'06}, booktitle = {{P}roceedings of the 20th {I}nternational {W}orkshop on {U}nification ({UNIF}'06)}, author = {Lafourcade, Pascal and Lugiez, Denis and Treinen, Ralf}, title = {{ACUNh}: Unification and Disunification Using Automata Theory}, pages = {6-20}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LLT-unif06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LLT-unif06.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LLT-unif06.ps}, abstract = {We show several results about unification problems in the equational theory~ACUNh consisting of the theory of exclusive or with one homomorphism. These results are shown using only techniques of automata and combinations of unification problems. We~show how to construct a most-general unifier for ACUNh-unification problems with constants using automata. We also prove that the first-order theory of ground terms modulo~ACUNh is decidable if the signature does not contain free non-constant function symbols, and that the existential fragment is decidable in the general case. Furthermore, we show a technical result about the set of most-general unifiers obtained for general unification problems.} }

@inproceedings{BJ-unif2006, address = {Seattle, Washington, USA}, month = aug, year = 2006, editor = {Levy, Jordi}, acronym = {{UNIF}'06}, booktitle = {{P}roceedings of the 20th {I}nternational {W}orkshop on {U}nification ({UNIF}'06)}, author = {Bouhoula, Adel and Jacquemard, Florent}, title = {Automating Sufficient Completeness Check for Conditional and Constrained~{TRS}}, nopages = {}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BJ-unif06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BJ-unif06.pdf}, abstract = {We present a procedure for checking sufficient completeness for conditional and constrained term rewriting systems containing axioms for constructors which may be constrained (by~e.g.~equalities, disequalities, ordering, membership...). Such axioms allow to specify complex data structures like e.g.~sets, sorted lists or powerlists. Our approach is integrated in a framework for inductive theorem proving based on tree grammars with constraints, a formalism which permits an exact representation of languages of ground constructor terms in normal form. The key technique used in the procedure is a generalized form of narrowing where, given a term, instead of unifying it with left members of rewrite rules, we instantiate it, at selected variables, following the productions of a constrained tree grammar, and test whether it can be rewritten. Our~procedure is sound and complete and has been successfully applied to several examples, yielding very natural proofs and, in case of negative answer, a counter example suggesting how to complete the specification. Moreover, it is a decision procedure when the TRS is unconditional but constrained, for a large class of constrained constructor axioms.} }

@inproceedings{LMO-formats06, address = {Paris, France}, month = sep, year = 2006, volume = 4202, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Asarin, Eug{\`e}ne and Bouyer, Patricia}, acronym = {{FORMATS}'06}, booktitle = {{P}roceedings of the 4th {I}nternational {C}onference on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'06)}, author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas and Oreiby, Ghassan}, title = {Model Checking Timed {ATL} for Durational Concurrent Game Structures}, pages = {245-259}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMO-formats06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMO-formats06.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LMO-formats06.ps}, doi = {10.1007/11867340_18}, abstract = {We extend the framework of ATL model-checking to {"}simply timed{"} concurrent game structures, i.e., multi-agent structures where each transition carry an integral duration (or interval thereof). While the case of single durations is easily handled from the semantics point of view, intervals of durations raise several interesting questions. Moreover subtle algorithmic problems have to be handled when dealing with model checking. We propose a semantics for which we develop efficient (PTIME) algorithms for timed ATL without equality constraints, while the general case is shown to be EXPTIME-complete.} }

@article{LMS-tcs05, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe}, title = {Efficient Timed Model Checking for Discrete-Time Systems}, volume = 353, number = {1-3}, pages = {249-271}, month = mar, year = 2006, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMS-TCS05.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMS-TCS05.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LMS-TCS05.ps}, doi = {10.1016/j.tcs.2005.11.020}, abstract = {We consider model checking of timed temporal formulae in \emph{durational transition graphs} (DTGs), \emph{i.e.}, Kripke structures where transitions have integer durations. Two semantics for DTGs are presented and motivated. We consider timed versions of CTL where subscripts put quantitative constraints on the time it takes before a property is satisfied. \par We exhibit an important gap between logics where subscripts of the form {"}\(= c\){"} (exact duration) are allowed, and simpler logics that only allow subscripts of the form {"}\(\leq c\){"} or {"}\(\geq c\){"} (bounded duration).\par Without exact durations, model checking can be done in polynomial time, but with exact durations, it becomes \(\Delta_{2}^{P}\)-complete or PSPACE-complete depending on the considered semantics.} }

@inproceedings{MOJ-aisc2006, address = {Beijing, China}, month = sep, year = 2006, volume = 4120, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, editor = {Calmet, Jacques and Ida, Tetsuo and Wang, Dongming}, acronym = {{AISC}'06}, booktitle = {{P}roceedings of the 8th {I}nternational {C}onference on {A}rtificial {I}ntelligence and {S}ymbolic {C}omputation ({AISC}'06)}, author = {Mitsuhashi, Ichiro and Oyamaguchi, Michio and Jacquemard, Florent}, title = {The Confluence Problem for Flat~{TRSs}}, pages = {68-81}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MOJ-aisc06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MOJ-aisc06.pdf}, doi = {10.1007/11856290_8}, abstract = {We prove that the properties of reachability, joinability and confluence are undecidable for flat~TRSs. Here, a~TRS is flat if the heights of the left and right-hand sides of each rewrite rule are at most one.} }

@article{MR-TCS05, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {Markey, Nicolas and Raskin, Jean-Fran{\c{c}}ois}, title = {Model Checking Restricted Sets of Timed Paths}, year = {2006}, month = aug, volume = 358, number = {2-3}, pages = {273-292}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Markey-Raskin-TCS05.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Markey-Raskin-TCS05.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ Markey-Raskin-TCS05.ps}, doi = {10.1016/j.tcs.2006.01.019}, abstract = {In this paper, we study the complexity of model-checking formulas of four important real-time logics (TPTL, MTL, MITL, and TCTL) over restricted sets of timed paths. The classes of restricted sets of timed paths that we consider are \textit{(i)}~a~single finite (or ultimately periodic) timed path, \textit{(ii)}~an~infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a region graph, \textit{(iii)}~an~infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a zone graph. \par Several results are quite negative: TPTL and MTL remain undecidable along region- and zone-paths. On the other hand, we obtained PTIME algorithms for model checking TCTL along a region path, and for MTL along a single timed path.} }

@article{MS05-IPL, publisher = {Elsevier Science Publishers}, journal = {Information Processing Letters}, author = {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe}, title = {Mu-Calculus Path Checking}, volume = 97, number = 6, month = mar, year = 2006, pages = {225-230}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MS05-IPL.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MS05-IPL.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MS05-IPL.ps}, doi = {10.1016/j.ipl.2005.11.010}, abstract = {We investigate the path model checking problem for the \(\mu\)-calculus. Surprisingly, restricting to deterministic structures does not allow for more efficient model checking algorithm, as we prove that it can encode any instance of the standard model checking problem for the \(\mu\)-calculus. } }

@article{RS-btl2, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Rabinovich, Alexander and Schnoebelen, {\relax Ph}ilippe}, title = {{\(\mathit{\MakeUppercase{BTL}}_2\)} and the expressive power of {\(\mathit{\MakeUppercase{ECTL}}^+\)}}, year = 2006, month = jul, volume = 204, number = 7, pages = {1023-1044}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BTL2-InfComp.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BTL2-InfComp.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BTL2-InfComp.ps}, doi = {10.1016/j.ic.2005.07.006}, abstract = {We show that \(\mathit{ECTL}^+\), the classical extension of \(\mathit{CTL}\) with fairness properties, is expressively equivalent to \(\mathit{BTL}_2\), a natural fragment of the monadic logic of order. \(\mathit{BTL}_2\)~is the branching-time logic with arbitrary quantification over paths, and where path formulae are restricted to quantifier depth~\(2\) first-order formulae in the monadic logic of order. This result, linking \(\mathit{ECTL}^+\) to a natural fragment of the monadic logic of order, provides a characterization that other branching-time logics, \emph{e.g.}, \(\mathit{CTL}\), lack. \par We then go on to show that \(\mathit{ECTL}^+\) and \(\mathit{BTL}_2\) are not finitely based (\emph{i.e.}, they cannot be defined by a finite set of temporal modalities) and that their model-checking problems are of the same complexity. } }

@misc{phs-lipn2006, author = {Schnoebelen, {\relax Ph}ilippe}, title = {De nouvelles applications pour le model-checking}, year = {2006}, month = nov, howpublished = {Invited lecture, Journ{\'e}es {\`a} l'occasion des 20~ans du~LIPN, Villetaneuse, France} }

@phdthesis{THESE-bernat06, author = {Bernat, Vincent}, title = {Th{\'e}ories de l'intrus pour la v{\'e}rification des protocoles cryptographiques}, year = 2006, month = jun, 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-bernat.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-bernat.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/these-bernat.ps} }

@phdthesis{THESE-delaune06, author = {Delaune, St{\'e}phanie}, title = {V{\'e}rification des protocoles cryptographiques et propri{\'e}t{\'e}s alg{\'e}briques}, year = 2006, month = jun, 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-delaune.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-delaune.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/these-delaune.ps}, abstract = {Cryptographic protocols are small concurrent programs designed to guarantee the security of exchanges between participants using non-secure medium. Establishing the correctness of these protocols is crucial given the increasing number of applications, such as electronic commerce, that exchange information on the Internet. Unfortunately, the existence of cryptographic primitives such as encryption is not sufficient to ensure security. The security of exchanges is ensured by cryptographic protocols which are notoriously error-prone.\par The formal verification of cryptographic protocols is a difficult problem that can be seen as a particular model-checking problem in an hostile environment. To verify such protocols, a line of research consists in considering encryption as a black box and assuming that an adversary can't learn anything from an encrypted message except if he has the key. This is called the \emph{perfect cryptography} assumption. Many results have been obtained under this assumption, but such an assumption is too strong in general. Some attacks exploit in a clever way the interaction between protocol rules and properties of cryptographic operators. \par In this thesis, we relax the perfect cryptography assumption by taking into account some algebraic properties of cryptographic primitives. We give decision procedures for the security problem in presence of several algebraic operators.} }

@phdthesis{THESE-lafourcade06, author = {Lafourcade, Pascal}, title = {V{\'e}rification des protocoles cryptographiques en pr{\'e}sence de th{\'e}ories {\'e}quationnelles}, year = 2006, month = sep, 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-lafourcade.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-lafourcade.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/these-lafourcade.ps}, note = {209~pages}, abstract = {The rise of the internet of new technologies has reinforced the key role of computer science in communication technology. The recent progress in these technologies has brought a dramatic change in the ways how we communicate and consume. All these communication activities are subject to complex communication protocols that a user does not control completely. Users of communication protocols require that their communications are {"}secure{"}. The developers of these communication protocols aim to secure communications in a hostile environment by cryptographic means. Such an environment consists of a dishonest communication participant, called an {"}intruder{"} or {"}attacker{"}... We suppose that the intruder controls the network on which the messages are exchanged.\par The verification of a cryptographic protocol either ensures that no attack is possible against the execution of the protocol in presence of a certain intruder, or otherwise exhibits an attack. One important assumption in the verification of cryptographic protocols is the so-called {"}perfect cryptography assumption{"}, which states that the only way to obtain knowledge about an encrypted message is to know its decryption key. This hypothesis is not sufficient to guarantee security in reality. It is possible that certain properties used in the protocol allow the intruder to obtain some information.\par One way to weaken this perfect cryptography assumption is to take into account in the model certain algebraic properties. We develop a formal approach for verifying the so-called secrecy property of cryptographic protocols in the presence of equational theories and of homomorphism.} }

@phdthesis{THESE-belmokadem06, author = {Bel{ }mokadem, Houda}, title = {V{\'e}rification des propri{\'e}t{\'e}s temporis{\'e}es des automates programmables industriels}, year = 2006, month = sep, 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-mokadem.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-mokadem.pdf} }

@phdthesis{THESE-bertrand06, author = {Bertrand, Nathalie}, title = {Mod{\`e}les stochastiques pour les pertes de messages dans les protocoles asynchrones et techniques de v{\'e}rification automatique}, year = 2006, 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/these-bertrand.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-bertrand.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/these-bertrand.ps} }

@mastersthesis{naves-master, author = {Naves, Guyslain}, title = {Accessibilit{\'e} dans les automates temporis{\'e}s {\`a} deux horloges}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = 2006, month = sep, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/master-naves.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/master-naves.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/master-naves.ps} }

@mastersthesis{akshay-master, author = {Akshay, S.}, title = {Formal Specification and Verification of Timed Communicating Systems}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, month = sep, year = 2006, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Akshay-M2.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Akshay-M2.pdf} }

@mastersthesis{brochenin-master, author = {Brochenin, R{\'e}mi}, title = {Techniques d'automates pour raisonner sur la m{\'e}moire}, school = {{M}aster {R}echerche {I}nformatique de {L}yon~--- {I}nformatique {F}ondamentale, Lyon, France}, type = {Rapport de {M}aster}, month = jun, year = 2006, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Brochenin-M2.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Brochenin-M2.ps} }

@mastersthesis{bursuc-master, author = {Bursuc, Sergiu}, title = {Contraintes de d{\'e}ductibilit{\'e} modulo Associativit{\'e}-Commutativit{\'e}}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, month = sep, year = 2006, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bursuc-M2.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bursuc-M2.pdf} }

@techreport{LSV:06:11, author = {Bollig, Benedikt and Kuske, Dietrich}, title = {Distributed {M}uller Automata and Logics}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = 2006, month = may, type = {Research Report}, number = {LSV-06-11}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-11.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-11.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/ rr-lsv-2006-11.ps}, note = {23~pages}, abstract = {We consider Muller asynchronous cellular automata running on infinite dags over distributed alphabets. We show that they have the same expressive power as the existential fragment of a monadic second-order logic featuring a first-order quantifier to express that there are infinitely many elements satisfying some property. Our result is based on an extension of the classical Ehrenfeucht-Fra{\"\i}ss{\'e} game to cope with infinite structures and the new first-order quantifier. As a byproduct, we obtain a logical characterization of unbounded Muller message-passing automata running on infinite message sequence charts.} }

@techreport{LSV:06:13, author = {Olivain, Julien and Goubault{-}Larrecq, Jean}, title = {Detecting Subverted Cryptographic Protocols by Entropy Checking}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = 2006, month = jun, type = {Research Report}, number = {LSV-06-13}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-13.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-13.pdf}, note = {19~pages}, abstract = {What happens when your implementation of SSL or some other cryptographic protocol is subverted through a buffer overflow attack? You have been hacked, right. Unfortunately, you may be unaware of~it: since normal traffic is encrypted, most IDSs cannot monitor~it. We propose a simple, yet efficient technique to detect such attacks, by computing the entropy of the flow and comparing it against known thresholds. This was implemented in the Net-Entropy sensor.} }

@techreport{Prouve:rap9, author = {Klay, Francis and Bozga, Liana and Lakhnech, Yassine and Mazar{\'e}, Laurent and Delaune, St{\'e}phanie and Kremer, Steve}, title = {Retour d'exp{\'e}rience sur la validation du vote {\'e}lectronique}, institution = {projet RNTL PROUV{\'E}}, month = nov, year = 2006, type = {Technical Report}, number = 9, note = {47~pages}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/prouve-rap9.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/prouve-rap9.pdf}, abstract = {Dans ce rapport, nous pr{\'e}sentons le travail de v{\'e}rification qui a {\'e}t{\'e} r{\'e}alis{\'e} sur le protocole de vote {\'e}lectronique que nous avons introduit et formalis{\'e} dans le rapport RNTL Prouv{\'e} num{\'e}ro~\(6\). Ce protocole a {\'e}t{\'e} mis au point par J.~Traor{\'e}, ing{\'e}nieur de recherche chez France T{\'e}l{\'e}com. Il est bas{\'e} sur le m{\'e}canisme de signature en aveugle et peut {\^e}tre consid{\'e}r{\'e} comme un d{\'e}riv{\'e} du protocole de Fujioka, Okamoto et~Ohta.\par La formalisation de ce protocole {\`a} mis en {\'e}vidence une grande complexit{\'e} due en particulier aux structures de donn{\'e}es et aux primitives cryptographiques manipul{\'e}es. D'un autre c{\^o}t{\'e} ce travail a {\'e}galement r{\'e}v{\'e}l{\'e} que les propri{\'e}t{\'e}s de s{\^u}ret{\'e} {\`a} garantir sont particuli{\`e}rement subtiles. Ce~document pr{\'e}sente les r{\'e}sultats qui ont {\'e}t{\'e} obtenus lors de la v{\'e}rification de ce protocole. En particulier nous montrons que certaines propri{\'e}t{\'e}s de s{\^u}ret{\'e} ont pu {\^e}tre prouv{\'e}es automatiquement alors que pour d'autres une preuve manuelle s'est av{\'e}r{\'e}e n{\'e}cessaire.} }

@misc{versydis-final, author = {Gastin, Paul and others}, title = {{ACI} {S}{\'e}curit{\'e} {I}nformatique {VERSYDIS}~--- Rapport final}, year = 2006, month = oct, type = {Contract Report}, note = {10~pages}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Versydis-final.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Versydis-final.pdf} }

@misc{cortos-final, author = {Bouyer, Patricia and others}, title = {{ACI} {S}{\'e}curit{\'e} {I}nformatique {CORTOS}~--- Rapport final}, year = 2006, month = nov, type = {Contract Report}, note = {17~pages}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Cortos-final.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Cortos-final.pdf} }

@misc{persee-final, author = {Schnoebelen, {\relax Ph}ilippe and Bouajjani, Ahmed and Sutre, Gr{\'e}goire}, title = {{ACI} {S}{\'e}curit{\'e} {I}nformatique {PERS{\'E}E}~--- Rapport final}, year = 2006, month = nov, type = {Contract Report}, note = {12~pages}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Persee-final.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Persee-final.pdf} }

@article{Baudet05jalc, journal = {Journal of Automata, Languages and Combinatorics}, author = {Baudet, Mathieu}, title = {Random Polynomial-Time Attacks and {D}olev-{Y}ao Models}, year = 2006, volume = 11, number = 1, pages = {7-21}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bau05-jalc.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bau05-jalc.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Bau05-jalc.ps}, abstract = {In this paper we present an extension of Dolev-Yao models for security protocols with a notion of random polynomial-time (Las Vegas) computability. First we notice that Dolev-Yao models can be seen as transition systems, possibly infinite. We then extend these transition systems with computation times and probabilities. The extended models can account for normal Dolev-Yao transitions as well as nonstandard operations such as inverting a one-way function. Our main contribution consists of showing that under reasonable assumptions the extended models are equivalent to standard Dolev-Yao models as far as (safety) security properties are concerned.} }

@article{Demri-jancl06, publisher = {Taylor \& Francis}, journal = {Journal of Applied Non-Classical Logics}, author = {Demri, St{\'e}phane}, title = {Linear-Time Temporal Logics with {P}resburger Constraints: An~Overview}, year = 2006, volume = 16, number = {3-4}, pages = {311-347}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-jancl06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/demri-jancl06.pdf}, abstract = {We present an overview of linear-time temporal logics with Presburger constraints whose models are sequences of tuples of integers. Such formal specification languages are well-designed to specify and verify systems that can be modelled with counter systems. The paper recalls the general framework of LTL over concrete domains and presents the main decidability and complexity results related to fragments of Presburger~LTL. Related formalisms are also briefly presented.} }

@misc{NB-SuMo-2006, author = {Bertrand, Nathalie}, title = {SuMo~-- Reachability analysis for lossy channels}, month = feb, year = {2006}, note = {See~\cite{BBS-forte06} for a description. Written in~OCaml (3000~lines)}, note-fr = {Voir la description dans~\cite{BBS-forte06}. {\'E}crit en~OCaml (3000~lignes)} }

@misc{gastex-v2.8, author = {Gastin, Paul}, title = {Gas{{\TeX}}: Graphs and Automata Simplified in~{{\TeX}} (v2.8)}, year = {2006}, month = nov, nohowpublished = {Available at http://www.lsv.ens-cachan.fr/~gastin/gastex/gastex.html}, note = {Written in~\TeX (about 2000 lines)}, note-fr = {\'Ecrit en~\TeX (environ 2000 lignes)}, url = {http://www.lsv.ens-cachan.fr/~gastin/gastex/gastex.html} }

@proceedings{AGHMR-sasyft04, title = {Selected papers of the International Workshop on Security Analysis of Systems: Formalisms and Tools ({SASYFT}'04)}, booktitle = {Selected papers of the International Workshop on Security Analysis of Systems: Formalisms and Tools ({SASYFT}'04)}, editor = {Anantharaman, Siva and Gastin, Paul and Hains, Ga{\'e}tan and Mullins, John and Rusinowitch, Micha{\"e}l}, year = 2006, address = {Orl{\'e}ans, France}, journal = {jalc}, volume = 11, number = 1 }

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