@inproceedings{BC-asian06, address = {Tokyo, Japan}, month = jan, year = 2008, volume = 4435, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Okada, Mitsu and Satoh, Ichiro}, acronym = {{ASIAN}'06}, booktitle = {{R}evised {S}elected {P}apers of the 11th {A}sian {C}omputing {S}cience {C}onference ({ASIAN}'06)}, author = {Bernat, Vincent and Comon{-}Lundh, Hubert}, title = {Normal proofs in intruder theories}, pages = {151-166}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC-asian06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC-asian06.pdf}, doi = {10.1007/978-3-540-77505-8_12}, abstract = {Given an arbitrary intruder deduction capability, modeled as an inference system~\(\mathcal{S}\) and a protocol, we show how to compute an inference system~\(\widehat{\mathcal{S}}\) such that the security problem for an unbounded number of sessions is equivalent to the deducibility of some message in~\(\widehat{\mathcal{S}}\). Then, assuming that \(\mathcal{S}\)~has some subformula property, we lift such a property to~\(\widehat{\mathcal{S}}\), thanks to a proof normalisation theorem. In~general, for an unbounded number of sessions, this provides with a complete deduction strategy. In case of a bounded number of sessions, our theorem implies that the security problem is co-NP-complete. As an instance of our result we get a decision algorithm for the theory of blind-signatures, which, to our knowledge, was not known before.} }

@inproceedings{LNZ-asian06, address = {Tokyo, Japan}, month = jan, year = 2008, volume = 4435, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Okada, Mitsu and Satoh, Ichiro}, acronym = {{ASIAN}'06}, booktitle = {{R}evised {S}elected {P}apers of the 11th {A}sian {C}omputing {S}cience {C}onference ({ASIAN}'06)}, author = {Lasota, S{\l}awomir and Nowak, David and Yu, Zhang}, title = {On completeness of logical relations for monadic types}, pages = {223-230}, nmnote = {autc parce que c'est un short paper, pas ant pour Zhang Yu}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LNZ-monad-complete.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LNZ-monad-complete.pdf}, doi = {10.1007/978-3-540-77505-8_17}, abstract = {Software security can be ensured by specifying and verifying security properties of software using formal methods with strong theoretical bases. In~particular, programs can be modeled in the framework of lambda-calculi, and interesting properties can be expressed formally by contextual equivalence (a.k.a.~observational equivalence). Furthermore, imperative features, which exist in most real-life software, can be nicely expressed in the so-called computational lambda-calculus. Contextual equivalence is difficult to prove directly, but we can often use logical relations as a tool to establish it in lambda-calculi. We~have already defined logical relations for the computational lambda-calculus in previous work. We~devote this paper to the study of their completeness w.r.t.~contextual equivalence in the computational lambda-calculus.} }

@inproceedings{DLS-fossacs08, address = {Budapest, Hungary}, month = mar # {-} # apr, year = 2008, volume = 4962, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Amadio, Roberto}, acronym = {{FoSSaCS}'08}, booktitle = {{P}roceedings of the 11th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'08)}, author = {Demri, St{\'e}phane and Lazi{\'c}, Ranko and Sangnier, Arnaud}, title = {Model checking freeze {LTL} over one-counter automata}, pages = {490-504}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLS-fossacs08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLS-fossacs08.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DLS-fossacs08.ps}, doi = {10.1007/978-3-540-78499-9_34}, abstract = {We study complexity issues related to the model-checking problem for LTL with registers (a.k.a. freeze LTL) over one-counter automata. We~consider several classes of one-counter automata (mainly deterministic vs.~nondeterministic) and several syntactic fragments (restriction on the number of registers and on the use of propositional variables for control locations). The~logic has the ability to store a counter value and to test it later against the current counter value. By~introducing a non-trivial abstraction on counter values, we~show that model checking LTL with registers over deterministic one-counter automata is PSPACE-complete with infinite accepting runs. By~constrast, we prove that model checking LTL with registers over nondeterministic one-counter automata is \(\Sigma_{1}^{1}\)-complete [resp. \(\Sigma_{1}^{0}\)-complete] in the infinitary [resp. finitary] case even if only one register is used and with no propositional variable. This makes a difference with the facts that several verification problems for one-counter automata are known to be decidable with relatively low complexity, and that finitary satisfiability for LTL with a unique register is decidable. Our~results pave the way for model-checking LTL with registers over other classes of operational models, such as reversal-bounded counter machines and deterministic pushdown systems.} }

@inproceedings{HIV-fossacs08, address = {Budapest, Hungary}, month = mar # {-} # apr, year = 2008, volume = 4962, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Amadio, Roberto}, acronym = {{FoSSaCS}'08}, booktitle = {{P}roceedings of the 11th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'08)}, author = {Habermehl, Peter and Iosif, Radu and Vojnar, Tom{\'a}{\v{s}}}, title = {What else is decidable about arrays?}, pages = {474-489}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hiv07-TR.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hiv07-TR.pdf}, doi = {10.1007/978-3-540-78499-9_33}, abstract = {We introduce a new decidable logic for reasoning about infinite arrays of integers. The logic is in the \(\exists^{*}\forall^{*}\) first-order fragment and allows (1)~Presburger constraints on existentially quantified variables, (2)~difference constraints as well as periodicity constraints on universally quantified indices, and (3)~difference constraints on values. In~particular, using our logic, one can express constraints on consecutive elements of arrays (\emph{e.g.}~\(\forall i.\ 0 \leq i < n \rightarrow a[i + 1] = a[i] - 1\)) as well as periodic facts (\emph{e.g.}~\(\forall i.\ i \equiv_2 0 \rightarrow a[i] = 0\)). The decision procedure follows the automata-theoretic approach: we~translate formulae into a special class of B{\"u}chi counter automata such that any model of a formula corresponds to an accepting run of the automaton, and vice versa. The~emptiness problem for this class of counter automata is shown to be decidable, as a consequence of earlier results on counter automata with a flat control structure and transitions based on difference constraints. We~show interesting program properties expressible in our logic, and give an example of invariant verification for programs that handle integer arrays.} }

@inproceedings{BMR-fossacs08, address = {Budapest, Hungary}, month = mar # {-} # apr, year = 2008, volume = 4962, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Amadio, Roberto}, acronym = {{FoSSaCS}'08}, booktitle = {{P}roceedings of the 11th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'08)}, author = {Bouyer, Patricia and Markey, Nicolas and Reynier, Pierre-Alain}, title = {Robust Analysis of Timed Automata {\em via} Channel Machines}, pages = {157-171}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMR-fossacs08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMR-fossacs08.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BMR-fossacs08.ps}, doi = {10.1007/978-3-540-78499-9_12}, abstract = {Whereas formal verification of timed systems has become a very active field of research, the idealised mathematical semantics of timed automata cannot be faithfully implemented. Several works have thus focused on a modified semantics of timed automata which ensures implementability, and robust model-checking algorithms for safety, and later LTL properties have been designed. Recently, a~new approach has been proposed, which reduces (standard) model-checking of timed automata to other verification problems on channel machines. Thanks to a new encoding of the modified semantics as a network of timed systems, we propose an original combination of both approaches, and prove that robust model-checking for coFlat-MTL, a large fragment of~MTL, is EXPSPACE-Complete.} }

@inproceedings{CS-fossacs08, address = {Budapest, Hungary}, month = mar # {-} # apr, year = 2008, volume = 4962, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Amadio, Roberto}, acronym = {{FoSSaCS}'08}, booktitle = {{P}roceedings of the 11th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'08)}, author = {Chambart, Pierre and Schnoebelen, {\relax Ph}ilippe}, title = {The \(\omega\)-Regular {P}ost Embedding Problem}, pages = {97-111}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-fossacs08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-fossacs08.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CS-fossacs08.ps}, doi = {10.1007/978-3-540-78499-9_8}, abstract = {Post's Embedding Problem is a new variant of Post's Correspondence Problem where words are compared with embedding rather than equality. It~has been shown recently that adding regular constraints on the form of admissible solutions makes the problem highly non-trivial, and relevant to the study of lossy channel systems. Here we consider the infinitary version and its application to recurrent reachability in lossy channel systems.} }

@inproceedings{Gou-fossacs08b, address = {Budapest, Hungary}, month = mar # {-} # apr, year = 2008, volume = 4962, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Amadio, Roberto}, acronym = {{FoSSaCS}'08}, booktitle = {{P}roceedings of the 11th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'08)}, author = {Goubault{-}Larrecq, Jean}, title = {Simulation Hemi-Metrics Between Infinite-State Stochastic Games}, pages = {50-65}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-34.pdf}, doi = {10.1007/978-3-540-78499-9_5}, abstract = {We investigate simulation hemi-metrics between certain forms of turn-based \(2\frac{1}{2}\)-player games played on infinite topological spaces. They have the desirable property of bounding the difference in payoffs obtained by starting from one state or another. All constructions are described as the special case of a unique one, which we call the Hutchinson hemi-metric on various spaces of continuous previsions. We show a directed form of the Kantorovich-Rubinstein theorem, stating that the Hutchinson hemi-metric on spaces of continuous probability valuations coincides with a notion of trans-shipment hemi-metric. We also identify the class of so-called sym-compact spaces as the right class of topological spaces, where the theory works out as nicely as possible.} }

@inproceedings{Gou-fossacs08a, address = {Budapest, Hungary}, month = mar # {-} # apr, year = 2008, volume = 4962, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Amadio, Roberto}, acronym = {{FoSSaCS}'08}, booktitle = {{P}roceedings of the 11th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'08)}, author = {Goubault{-}Larrecq, Jean}, title = {Prevision Domains and Convex Powercones}, pages = {318-333}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-33.pdf}, doi = {10.1007/978-3-540-78499-9_23}, abstract = {Two recent semantic families of models for mixed probabilistic and non-deterministic choice over a space~\(X\) are the convex powercone models, due independently to Mislove, and to Tix, Keimel, and Plotkin, and the continuous prevision model of the author. We show that, up to some minor details, these models are isomorphic whenever \(X\) is a continuous, coherent cpo, and whether the particular brand of non-determinism we focus on is demonic, angelic, or chaotic. The construction also exhibits domains of continuous previsions as retracts of well-known continuous cpos, providing simple bases for the various continuous cpos of continuous previsions. This has practical relevance to computing approximations of operations on previsions.} }

@inproceedings{Kremer-tgc07, address = {Sophia-Antipolis, France}, year = 2008, volume = 4912, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Barthe, Gilles and Fournet, C{\'e}dric}, acronym = {{TGC}'07}, booktitle = {{R}evised {S}elected {P}apers from the 3rd {S}ymposium on {T}rustworthy {G}lobal {C}omputing ({TGC}'07)}, author = {Kremer, Steve}, title = {Computational soundness of equational theories (Tutorial)}, pages = {363-382}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Kremer-tgc07.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Kremer-tgc07.pdf}, doi = {10.1007/978-3-540-78663-4}, abstract = {We study the link between formal and cryptographic models for security protocols in the presence of passive and adaptive adversaries. We first describe the seminal result by Abadi and Rogaway and shortly discuss some of its extensions. Then we describe a general model for reasoning about the soundness of implementations of equational theories. We illustrate this model on several examples of computationally sound implementations of equational theories.} }

@article{JRV-jlap07, publisher = {Elsevier Science Publishers}, journal = {Journal of Logic and Algebraic Programming}, author = {Jacquemard, Florent and Rusinowitch, Micha{\"e}l and Vigneron, Laurent}, title = {Tree automata with equality constraints modulo equational theories}, year = 2008, month = apr, volume = 75, number = 2, pages = {182-208}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JRV-jlap08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JRV-jlap08.pdf}, doi = {10.1016/j.jlap.2007.10.006}, abstract = {This paper presents new classes of tree automata combining automata with equality test and automata modulo equational theories. We believe that these classes have 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.} }

@inproceedings{BMOSW-stacs08, address = {Bordeaux, France}, month = feb, year = 2008, volume = 1, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Albers, Susanne and Weil, Pascal}, acronym = {{STACS}'08}, booktitle = {{P}roceedings of the 25th {A}nnual {S}ymposium on {T}heoretical {A}spects of {C}omputer {S}cience ({STACS}'08)}, author = {Bouyer, Patricia and Markey, Nicolas and Ouaknine, Jo{\"e}l and Schnoebelen, {\relax Ph}ilippe and Worrell, James}, title = {On Termination for Faulty Channel Machines}, pages = {121-132}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bmosw-stacs08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bmosw-stacs08.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/bmosw-stacs08.ps}, abstract = {A channel machine consists of a finite controller together with several fifo channels; the controller can read messages from the head of a channel and write messages to the tail of a channel. In this paper, we focus on channel machines with \emph{insertion errors}, \textit{i.e.}, machines in whose channels messages can spontaneously appear. Such devices have been previously introduced in the study of Metric Temporal Logic. We~consider the termination problem: are all the computations of a given insertion channel machine finite? We~show that this problem has non-elementary, yet primitive recursive complexity.} }

@article{TED-todaes08, publisher = {ACM Press}, journal = {ACM Transactions on Design Automation of Electronic Systems}, author = {Taktak, Sami and Encrenaz, Emmanuelle and Desbarbieux, Jean-Lou}, title = {A tool for automatic detection of deadlocks in wormhole networks on chip}, nopages = {}, volume = 13, number = 1, year = 2008, month = jan, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/TED-todaes07.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/TED-todaes07.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/TED-todaes07.ps}, doi = {10.1145/1297666.1297672}, 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 \emph{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. We~provide comparative results with standard approach, highlighting the benefits of our method.} }

@article{BHR-ietc07, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, 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}, year = {2008}, month = jan, volume = 206, number = 1, pages = {73-107}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-ic07.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-ic07.pdf}, doi = {10.1016/j.ic.2007.10.004}, abstract = {Timed Petri nets and timed automata are two standard models for the analysis of real-time systems. We~study in this paper their relationship, and prove in particular that they are incomparable w.r.t. language equivalence. In~fact, we~study the more general model of timed Petri nets with read-arcs (RA-TdPN), already introduced in~[Ji{\v{r}}{\'\i}~Srba, \textit{Timed-arc petri nets vs. networks of timed automata}, Proc.\ ICATPN'05, LNCS~3536, Springer], which unifies both models of timed Petri nets and of timed automata, and prove that the coverability problem remains decidable for this model. 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, for~instance on the power of non-deterministic clock resets.} }

@article{DLLT-IC07, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Delaune, St{\'e}phanie and Lafourcade, Pascal and Lugiez, Denis and Treinen, Ralf}, title = {Symbolic protocol analysis for monoidal equational theories}, pages = {312-351}, volume = 206, number = {2-4}, year = 2008, month = feb # {-} # apr, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLLT-ic07.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLLT-ic07.pdf}, doi = {10.1016/j.ic.2007.07.005}, abstract = {We are interested in the design of automated procedures for analyzing the (in)security of cryptographic protocols in the Dolev-Yao model for a bounded number of sessions when we take into account some algebraic properties satisfied by the operators involved in the protocol. This~leads to a more realistic model than what we get under the perfect cryptography assumption, but it implies that protocol analysis deals with terms modulo some equational theory instead of terms in a free algebra. The main goal of this paper is to set up a general approach that works for a whole class of monoidal theories which contains many of the specific cases that have been considered so far in an ad-hoc way (e.g.~exclusive~or, Abelian groups, exclusive or in combination with the homomorphism axiom). We~follow a classical schema for cryptographic protocol analysis which proves first a locality result and then reduces the insecurity problem to a symbolic constraint solving problem. This approach strongly relies on the correspondence between a monoidal theory~{\(E\)} and a semiring~{\(S_E\)} which we use to deal with the symbolic constraints. We~show that the well-defined symbolic constraints that are generated by reasonable protocols can be solved provided that unification in the monoidal theory satisfies some additional properties. The~resolution process boils down to solving particular quadratic Diophantine equations that are reduced to linear Diophantine equations, thanks to linear algebra results and the well-definedness of the problem. Examples of theories that do not satisfy our additional properties appear to be undecidable, which suggests that our characterization is reasonably tight.} }

@article{BBL-fmsd06, publisher = {Springer}, journal = {Formal Methods in System Design}, author = {Bouyer, Patricia and Brinksma, Ed and Larsen, Kim G.}, title = {Optimal Infinite Scheduling for Multi-Priced Timed Automata}, volume = {32}, number = {1}, pages = {2-23}, year = 2008, month = feb, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBL-FMSD04.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBL-FMSD04.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBL-FMSD04.ps}, doi = {10.1007/s10703-007-0043-4}, abstract = {This paper is concerned with the derivation of infinite schedules for timed automata that are in some sense optimal. To~cover a wide class of optimality criteria we start out by introducing an extension of the (priced) timed automata model that includes both costs and rewards as separate modelling features. A~precise definition is then given of what constitutes optimal infinite behaviours for this class of models. We subsequently show that the derivation of optimal non-terminating schedules for such double-priced timed automata is computable. This is done by a reduction of the problem to the determination of optimal mean-cycles in finite graphs with weighted edges. This reduction is obtained by introducing the so-called corner-point abstraction, a~powerful abstraction technique of which we show that it preserves optimal schedules.} }

@article{DrGa06tocsys, publisher = {Springer}, journal = {Theory of Computing Systems}, author = {Droste, Manfred and Gastin, Paul}, title = {On aperiodic and star-free formal power series in partially commuting variables}, year = 2008, month = may, volume = 42, number = 4, pages = {608-631}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-12.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-12.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/ rr-lsv-2005-12.ps}, doi = {10.1007/s00224-007-9064-z}, abstract = {Formal power series over non-commuting variables have been investigated as representations of the behavior of automata with multiplicities. Here we introduce and investigate the concepts of aperiodic and of star-free formal power series over semirings and partially commuting variables. We prove that if the semiring~\(K\) is idempotent and commutative, or if \(K\) is idempotent and the variables are non-commuting, then the product of any two aperiodic series is again aperiodic. We also show that if \(K\) is idempotent and the matrix monoids over~\(K\) have a Burnside property (satisfied, \textit{e.g.}~by the tropical semiring), then the aperiodic and the star-free series coincide. This generalizes a classical result of Sch{\"u}tzenberger~(1961) for aperiodic regular languages and subsumes a result of Guaiana, Restivo and Salemi~(1992) on aperiodic trace languages. } }

@inproceedings{AA+-pvldb08, address = {Auckland, New Zealand}, month = aug, year = 2008, volume = 1, series = {Proceedings of the {VLDB} Endowment}, publisher = {ACM Press}, editor = {Weber, Gerald}, acronym = {{VLDB}'08}, booktitle = {{P}roceedings of the 34th {I}nternational {C}onference on {V}ery {L}arge {D}ata {B}ases ({VLDB}'08)}, author = {Abiteboul, Serge and Allard, Tristan and Chatalic, {\relax Ph}ilippe and Gardarin, Georges and Ghitescu, Anca and Goasdou{\'e}, Fran{\c{c}}ois and Manolescu, Ioana and Nguyen, Benjamin and Ouazara, Mohamed and Somani, Aditya and Travers, Nicolas and Vasile, Gabriel and Zoupanos, Spyros}, title = {Web{C}ontent: efficient {P2P} warehousing of web data}, pages = {1428-1431}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/Aetal-pvldb08.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Aetal-pvldb08.pdf}, abstract = {We present the WebContent platform for managing distributed repositories of XML and semantic Web data. The platform allows integrating various data processing building blocks (crawling, translation, semantic annotation, full-text search, structured XML querying, and semantic querying), presented as Web services, into a large-scale efficient platform. Calls to various services are combined inside ActiveXML documents, which are XML documents including service calls. An ActiveXML optimizer is used to: (i)~efficiently distribute computations among sites; (ii)~perform XQuery-specific optimizations by leveraging an algebraic XQuery optimizer; and (iii)~given an XML query, chose among several distributed indices the most appropriate in order to answer the query.} }

@article{ABM-vldb08, publisher = {ACM Press}, journal = {The VLDB Journal}, author = {Abiteboul, Serge and Benjelloun, Omar and Milo, Tova}, title = {The Active~{XML} project: an~overview}, volume = 17, number = 5, pages = {1019-1040}, year = {2008}, month = aug, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABM-vldb08.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABM-vldb08.pdf}, doi = {10.1007/s00778-007-0049-y}, abstract = {This paper provides an overview of the Active XML project developed at INRIA over the past five years. Active XML (AXML, for short), is a declarative framework that harnesses Web services for distributed data management, and is put to work in a peer-to-peer architecture.\par The model is based on AXML documents, which are XML documents that may contain embedded calls to Web services, and on AXML services, which are Web services capable of exchanging AXML documents. An AXML peer is a repository of AXML documents that acts both as a client by invoking the embedded service calls, and as a server by providing AXML services, which are generally defined as queries or updates over the persistent AXML documents.\par The approach gracefully combines stored information with data defined in an intensional manner as well as dynamic information. This simple, rather classical idea leads to a number of technically challenging problems, both theoretical and practical.\par In this paper, we describe and motivate the AXML model and language, overview the research results obtained in the course of the project, and show how all the pieces come together in our implementation.} }

@inproceedings{AMPPS-icde08, address = {Cancun, Mexico}, month = apr, year = 2008, publisher = {{IEEE} Computer Society Press}, editor = {Alonso, Gustavo and Blakeley, Jos{\'e} A. and Chen, Arbee L. P.}, acronym = {{ICDE}'08}, booktitle = {{P}roceedings of the 24th {I}nternational {C}onference on {D}ata {E}ngineering ({ICDE}'08)}, author = {Abiteboul, Serge and Manolescu, Ioana and Polyzotis, Neoklis and Preda, Nicoleta and Sun, Chong}, title = {{XML} processing in {DHT} networks}, pages = {606-615}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AMPPS-icde08.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AMPPS-icde08.pdf}, doi = {10.1109/ICDE.2008.4497469}, abstract = {We study the scalable management of XML data in P2P networks based on distributed hash tables (DHTs). We identify performance limitations in this context, and propose an array o ftechniques to lift them. First, we adapt the DHT platform to the needs of massive data processing. (This primarily consists of replacing the DHT store by an efficient native store and in streaming the communications with the DHT.) Second, we introduce a distributed hierarchical index and efficient algorithms taking advantage of this index to speed up query processing. Third, we present an innovative, XML-specific flavor of Bloom filters, to reduce data transfers entailed by query processing. Our approach is fully implemented in the KadoP DHT-based XML processing system, used in a real-life software manufacturing application. We present experiments that demonstrate the benefits of the proposed techniques.} }

@inproceedings{AMZ-icde08, address = {Cancun, Mexico}, month = apr, year = 2008, publisher = {{IEEE} Computer Society Press}, editor = {Alonso, Gustavo and Blakeley, Jos{\'e} A. and Chen, Arbee L. P.}, acronym = {{ICDE}'08}, booktitle = {{P}roceedings of the 24th {I}nternational {C}onference on {D}ata {E}ngineering ({ICDE}'08)}, author = {Abiteboul, Serge and Manolescu, Ioana and Zoupanos, Spyros}, title = {{O}ptim{AX}: efficient support for data-intensive mash-ups}, pages = {1564-1567}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AMZ-icde08.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AMZ-icde08.pdf}, doi = {10.1109/ICDE.2008.4497622}, abstract = {Mash-ups are being used in various Web-based applications of Web 2.0 which combine instantly information from different sources. Active XML (AXML, in short) language is a tool for decentralized, data-centric Web service integration. AXML document includes calls to services that may be either simple request-responses either long running subscriptions. Being fully composable and allowing resource sharing makes AXML ideal for mash-up style integration. In this demo we present how AXML can be used as a specification, optimization and distributed execution language for dynamic distributed mash-ups in varied P2P settings. We also demonstrate our AXML optimizer's (OptimAX) optimization rules and rewriting engine with a help of GUI.} }

@inproceedings{AMB-icde08, address = {Cancun, Mexico}, month = apr, year = 2008, publisher = {{IEEE} Computer Society Press}, editor = {Alonso, Gustavo and Blakeley, Jos{\'e} A. and Chen, Arbee L. P.}, acronym = {{ICDE}'08}, booktitle = {{P}roceedings of the 24th {I}nternational {C}onference on {D}ata {E}ngineering ({ICDE}'08)}, author = {Abiteboul, Serge and Marinoiu, Bogdan and Bourhis, Pierre}, title = {Distributed Monitoring of Peer-to-Peer Systems}, pages = {1572-1575}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AMB-icde08.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AMB-icde08.pdf}, doi = {10.1109/ICDE.2008.4497624}, abstract = {Observing highly dynamic Peer-to-Peer systems is essential for many applications such as fault management or business processing. We demonstrate P2PMonitor, a P2P system for monitoring such systems. Alerters deployed on the monitored peers are designed to detect particular kinds of local events. They generate streams of XML data that form the primary sources of information for P2PMonitor. The core of the system is composed of processing components implementing the operators of an algebra over data streams.\par From a user viewpoint, monitoring a P2P system can be as simple as querying an XML document. The document is an ActiveXML document that aggregates a (possibly very large) number of streams generated by alerters on the monitored peers. Behind the scene, P2PMonitor compiles the monitoring query into a distributed monitoring plan, deploys alerters and stream algebra processors and issues notifications that are sent to users.\par The system functionalities are demonstrated by simulating the supply chain of a large company.} }

@inproceedings{AMZ-icwe08, address = {Yorktown Heights, New York, USA}, month = jul, year = 2008, publisher = {{IEEE} Computer Society Press}, editor = {Schwabe, Daniel and Curbera, Francisco and Dantzig, Paul}, acronym = {{ICWE}'08}, booktitle = {{P}roceedings of the 8th {I}nternational {C}onference on {W}eb {E}ngineering ({ICWE}'08)}, author = {Abiteboul, Serge and Manolescu, Ioana and Zoupanos, Spyros}, title = {{O}ptim{AX}: Optimizing Distributed {A}ctive{XML} Applications}, pages = {299-310}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AMZ-icwe08.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AMZ-icwe08.pdf}, doi = {10.1109/ICWE.2008.11}, abstract = {The Web has become a platform of choice for the deployment of complex applications involving several business partners. Typically, such applications interoperate by means of Web services, exchanging XML information.\par We present OptimAX, an optimization Web service that applies at the static level (prior to enacting an application) in order to rewrite it into one whose execution will be more performant. OptimAX builds on the ActiveXML (AXML) data-centric Web service composition language, and demonstrates how database-style techniques can be efficiently integrated in a loosely-coupled, distributed application based on Web services. OptimAX has been fully implemented and we describe its experimental performance.} }

@inproceedings{AGM-widm08, address = {Napa Valley, California, USA}, month = oct, year = 2008, publisher = {ACM Press}, editor = {Chan, Chee Yong and Polyzotis, Neoklis}, acronym = {{WIDM}'08}, booktitle = {{P}roceedings of the 10th {ACM} {I}nternational {W}orkshop on {W}eb {I}nformation and {D}ata {M}anagement ({WIDM}'08)}, author = {Abiteboul, Serge and Greenshpan, Ohad and Milo, Tova}, title = {Modeling the mashup space}, pages = {87-94}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AGM-widm08.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGM-widm08.pdf}, doi = {10.1145/1458502.1458517}, abstract = {We introduce a formal model for capturing the notion of mashup in its globality. The basic component in our model is the mashlet. A mashlet may query data sources, import other mashlets, use external Web services, and specify complex interaction patterns between its components. A mashlet state is modeled by a set of relations and its logic specified by datalog-style active rules. We are primarily concerned with changes in a mashlet state relations and rules. The interactions with users and other applications, as well as the consequent effects on the mashlets composition and behavior, are captured by streams of changes. The model facilitates dynamic mashlets composition, interaction and reuse, and captures the fundamental behavioral aspects of mashups.} }

@article{SAG-ercim08, publisher = {European Research Consortium for Informatics and Mathematics}, journal = {ERCIM News}, author = {Senellart, Pierre and Abiteboul, Serge and Gilleron, R{\'e}mi}, title = {Understanding the Hidden Web}, volume = 72, pages = {32-33}, year = 2008, month = jan, url = {http://ercim-news.ercim.eu/en72/special/understanding-the-hidden-web} }

@inproceedings{HCL-fsttcs08, address = {Bangalore, India}, month = dec, year = 2008, volume = 2, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Hariharan, Ramesh and Mukund, Madhavan and Vinay, V.}, acronym = {{FSTTCS}'08}, booktitle = {{P}roceedings of the 28th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'08)}, author = {Comon{-}Lundh, Hubert}, title = {About models of security protocols}, nopages = {}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HCL-fsttcs08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HCL-fsttcs08.pdf}, abstract = {In this paper, mostly consisting of definitions, we~revisit the models of security protocols: we~show that the symbolic and the computational models (as~well as others) are instances of a same generic model. Our definitions are also parametrized by the security primitives, the notion of attacker and, to some extent, the process calculus.} }

@phdthesis{oreiby-these2008, author = {Oreiby, Ghassan}, title = {Logiques temporelles pour le contr{\^o}le temporis{\'e}}, year = 2008, month = dec, type = {Th{\`e}se de doctorat}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-GO08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-GO08.pdf} }

@article{GLLN-mscs08, publisher = {Cambridge University Press}, journal = {Mathematical Structures in Computer Science}, author = {Goubault{-}Larrecq, Jean and Lasota, S{\l}awomir and Nowak, David}, title = {Logical Relations for Monadic Types}, volume = 18, number = 6, pages = {1169-1217}, month = dec, year = 2008, note = {81~pages}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GLLN-arxiv05.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GLLN-arxiv05.pdf}, doi = {10.1017/S0960129508007172}, abstract = {Logical relations and their generalisations are a fundamental tool in proving properties of lambda calculi, for example, for yielding sound principles for observational equivalence. We propose a natural notion of logical relations that is able to deal with the monadic types of Moggi's computational lambda calculus. The treatment is categorical, and is based on notions of subsconing, mono factorisation systems and monad morphisms. Our approach has a number of interesting applications, including cases for lambda calculi with non-determinism (where being in a logical relation means being bisimilar), dynamic name creation and probabilistic systems.} }

@phdthesis{bursztein-these2008, author = {Bursztein, Elie}, title = {Anticipation games. Th{\'e}orie des jeux appliqu{\'e}s {\`a} la s{\'e}curit{\'e} r{\'e}seau}, year = 2008, month = nov, type = {Th{\`e}se de doctorat}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-EB08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-EB08.pdf}, futureslides = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/SLIDES/ these-AS07-slides.pdf} }

@phdthesis{sangnier-these2008, author = {Sangnier, Arnaud}, title = {V{\'e}rification de syst{\`e}mes avec compteurs et pointeurs}, year = 2008, month = nov, type = {Th{\`e}se de doctorat}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-AS07.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-AS07.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/these-AS07.ps} }

@phdthesis{arapinis-these2008, author = {Arapinis, Myrto}, title = {S{\'e}curit{\'e} des protocoles cryptographiques~: d{\'e}cidabilit{\'e} et r{\'e}sultats de r{\'e}duction}, year = 2008, month = nov, type = {Th{\`e}se de doctorat}, school = {Universit{\'e} Paris~12, Cr{\'e}teil, France}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-MA07.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-MA07.pdf}, futureslides = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/SLIDES/ these-FC07-slides.pdf} }

@article{BB-lmcs08, journal = {Logical Methods in Computer Science}, author = {Bollig, Benedikt}, title = {On the Expressive Power of {\(2\)}-Stack Visibly Pushdown Automata}, volume = 4, number = {4\string:16}, month = dec, year = 2008, nopages = {}, doi = {10.2168/LMCS-4(4:16)2008}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BB-lmcs08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BB-lmcs08.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BB-lmcs08.ps}, abstract = {Visibly pushdown automata are input-driven pushdown automata that recognize some non-regular context-free languages while preserving the nice closure and decidability properties of finite automata. Visibly pushdown automata with multiple stacks have been considered recently by La~Torre, Madhusudan, and Parlato, who exploit the concept of visibility further to obtain a rich automata class that can even express properties beyond the class of context-free languages. At the same time, their automata are closed under boolean operations, have a decidable emptiness and inclusion problem, and enjoy a logical characterization in terms of a monadic second-order logic over words with an additional nesting structure. These results require a restricted version of visibly pushdown automata with multiple stacks whose behavior can be split up into a fixed number of phases. In this paper, we~consider 2-stack visibly pushdown automata (i.e., visibly pushdown automata with two stacks) in their unrestricted form. We show that they are expressively equivalent to the existential fragment of monadic second-order logic. Furthermore, it turns out that monadic second-order quantifier alternation forms an infinite hierarchy wrt.~words with multiple nestings. Combining these results, we conclude that 2-stack visibly pushdown automata are not closed under complementation. Finally, we discuss the expressive power of B{\"u}chi 2-stack visibly pushdown automata running on infinite (nested) words. Extending the logic by an infinity quantifier, we can likewise establish equivalence to existential monadic second-order logic.} }

@incollection{DH-afsec08, author = {Donatelli, Susanna and Haddad, Serge}, title = {V{\'e}rification quantitative de cha{\^\i}nes de {M}arkov}, booktitle = {Approches formelles des syst{\`e}mes embarqu{\'e}s communicants}, editor = {Roux, Olivier H. and Jard, Claude}, publisher = {Herm{\`e}s}, year = 2008, month = oct, pages = {177-198}, chapter = 6, url = {http://www.lavoisier.fr/notice/fr335499.html}, futureisbn = {} }

@incollection{CM-afsec08, author = {Cassez, Franck and Markey, Nicolas}, title = {Contr{\^o}le des syst{\`e}mes temporis{\'e}s}, booktitle = {Approches formelles des syst{\`e}mes embarqu{\'e}s communicants}, editor = {Roux, Olivier H. and Jard, Claude}, publisher = {Herm{\`e}s}, year = 2008, month = oct, pages = {105-144}, chapter = 4, url = {http://www.lavoisier.fr/notice/fr335499.html}, nops = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/.ps}, nopsgz = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PSGZ/.ps.gz}, futureisbn = {} }

@misc{NM-AV2008, author = {Markey, Nicolas}, title = {Infinite Runs In Weighted Times Games with Energy Constraints}, year = 2008, month = aug, noslides = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/SLIDES/.pdf}, howpublished = {Invited talk, Workshop {A}utomata and {V}erification ({AV}'08), Mons, Belgium} }

@misc{PB-AV2008, author = {Bouyer, Patricia}, title = {Probabilities in Timed Automata}, year = 2008, month = aug, noslides = {}, howpublished = {Invited talk, Workshop {A}utomata and {V}erification ({AV}'08), Mons, Belgium} }

@misc{PhS-AV2008, author = {Schnoebelen, {\relax Ph}ilippe}, title = {The complexity of lossy channel systems}, year = 2008, month = aug, noslides = {}, howpublished = {Invited talk, Workshop {A}utomata and {V}erification ({AV}'08), Mons, Belgium} }

@inproceedings{CLC-ccs08, address = {Alexandria, Virginia, USA}, month = oct, year = 2008, publisher = {ACM Press}, acronym = {{CCS}'08}, booktitle = {{P}roceedings of the 15th {ACM} {C}onference on {C}omputer and {C}ommunications {S}ecurity ({CCS}'08)}, author = {Comon{-}Lundh, Hubert and Cortier, V{\'e}ronique}, title = {Computational Soundness of Observational Equivalence}, pages = {109-118}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CLC-ccs08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CLC-ccs08.pdf}, doi = {10.1145/1455770.1455786}, abstract = {Many security properties are naturally expressed as indistinguishability between two versions of a protocol. In this paper, we show that computational proofs of indistinguishability can be considerably simplified, for a class of processes that covers most existing protocols. More precisely, we show a soundness theorem, following the line of research launched by Abadi and Rogaway in~2000: computational indistinguishability in presence of an active attacker is implied by the observational equivalence of the corresponding symbolic processes. We prove our result for symmetric encryption, but the same techniques can be applied to other security primitives such as signatures and public-key encryption. The proof requires the introduction of new concepts, which are general and can be reused in other settings.} }

@mastersthesis{ciobaca-master, author = {Ciob{\^a}c{\u{a}}, {\c{S}}tefan}, title = {Verification of anonymity properties in e-voting protocols}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2008}, month = sep, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/master-ciobaca.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/master-ciobaca.pdf} }

@misc{dots-rapp-18m, author = {Fran{\c{c}}ois Laroussinie and others}, title = {Projet DOTS (ANR-06-SETI-003)~: Rapport {\`a} \(18\)~mois}, year = 2008, month = sep, type = {Contract Report}, note = {5~pages} }

@misc{dots-rapp-12m, author = {Fran{\c{c}}ois Laroussinie and others}, title = {Projet DOTS (ANR-06-SETI-003)~: Rapport {\`a} \(12\)~mois}, year = 2008, month = mar, type = {Contract Report}, note = {6~pages} }

@misc{dots-1.1, author = {Cassez, Franck and Laroussinie, Fran{\c{c}}ois and Lime, Didier and Markey, Nicolas}, title = {Quantitative Objectives in Timed Games}, howpublished = {Deliverable DOTS~1.1 (ANR-06-SETI-003)}, year = 2008, month = sep }

@misc{dots-3.1, author = {Bollig, Benedikt and Bouyer, Patricia and Cassez, Franck and Chatain, {\relax Th}omas and Gastin, Paul and Haddad, Serge and Jard, Claude}, title = {Model for distributed timed systems}, howpublished = {Deliverable DOTS~3.1 (ANR-06-SETI-003)}, year = 2008, month = sep }

@inproceedings{ADK-lpar08, address = {Doha, Qatar}, month = nov, year = 2008, volume = {5330}, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, editor = {Cervesato, Iliano and Veith, Helmut and Voronkov, Andrei}, acronym = {{LPAR}'08}, booktitle = {{P}roceedings of the 15th {I}nternational {C}onference on {L}ogic for {P}rogramming, {A}rtificial {I}ntelligence, and {R}easoning ({LPAR}'08)}, author = {Arapinis, Myrto and Delaune, St{\'e}phanie and Kremer, Steve}, title = {From One Session to Many: Dynamic Tags for Security Protocols}, pages = {128-142}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ADK-lpar08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ADK-lpar08.pdf}, doi = {10.1007/978-3-540-89439-1_9}, abstract = {The design and verification of cryptographic protocols is a notoriously difficult task, even in abstract Dolev-Yao models. This is mainly due to several sources of unboundedness (size of messages, number of sessions,~...). In~this paper, we~present a transformation which maps a protocol that is secure for a single session to a protocol that is secure for an unbounded number of sessions. The~transformation is surprisingly simple, computationally light and works for arbitrary protocols that rely on usual cryptographic primitives, such as symmetric and asymmetric encryption as well as digital signatures. Our~result provides an effective strategy to design secure protocols: (i)~design a protocol intended to be secure for one session (this can be verified with existing automated tools); (ii)~apply our transformation and obtain a protocol which is secure for an unbounded number of sessions. A~side-effect of this result is that we characterize a class of protocols for which secrecy for an unbounded number of sessions is decidable.} }

@inproceedings{HCL-ijcar08, address = {Sydney, Australia}, month = aug, year = 2008, volume = {5195}, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer-Verlag}, editor = {Armando, Alessandro and Baumgartner, Peter and Dowek, Gilles}, acronym = {{IJCAR}'08}, booktitle = {{P}roceedings of the 4th {I}nternational {J}oint {C}onference on {A}utomated {R}easoning ({IJCAR}'08)}, author = {Comon{-}Lundh, Hubert}, title = {Challenges in the Automated Verification of Security Protocols}, pages = {396-409}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HCL-ijcar08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HCL-ijcar08.pdf}, doi = {10.1007/978-3-540-71070-7_34}, abstract = {The application area of security protocols raises several problems that are relevant to automated deduction. We describe in this note some of these challenges.} }

@article{DG-tcs08, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {Demri, St{\'e}phane and Gascon, R{\'e}gis}, title = {Verification of Qualitative {\(\mathbb{\MakeUppercase{Z}}\)}~constraints}, volume = 409, number = 1, month = dec, year = 2008, pages = {24-40}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-tcs08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-tcs08.pdf}, doi = {10.1016/j.tcs.2008.07.023}, abstract = {We introduce an LTL-like logic with atomic formulae built over a constraint language interpreting variables in~\(\mathbb{Z}\). The~constraint language includes periodicity constraints, comparison constraints of the form \({x = y}\) and \({x < y}\), is~closed under Boolean operations and admits a restricted form of existential quantification. Such constraints are used for instance in calendar formalisms or abstractions of counter automata by using congruences modulo some power of two. Indeed, various programming languages perform arithmetic operators modulo some integer. We~show that the satisfiability and model-checking problems (with respect to an appropriate class of constraint automata) for this logic are decidable in polynomial space improving significantly known results about its strict fragments. This is the largest set of qualitative constraints over~\(\mathbb{Z}\) known so~far, shown to admit a decidable LTL extension.} }

@inproceedings{BCFH-valuetools08, address = {Athens, Greece}, month = oct, year = 2008, publisher = {Institute for Computer Sciences, Social-Informatics and Telecommunications Engineering}, editor = {Chahed, Tijani and Toumpis, Stavros and Yechiali, Uri}, acronym = {{VALUETOOLS}'08}, booktitle = {{P}roceedings of the 3rd {I}nternational {C}onference on {P}erformance {E}valuation {M}ethodologies and {T}ools ({VALUETOOLS}'08)}, author = {Beccuti, Marco and Codetta{-}Raiteri, Daniele and Franceschinis, Giuliana and Haddad, Serge}, title = {Non Deterministic Repairable Fault Trees for Computing Optimal Repair Strategy}, nopages = {}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFH-valuetools08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFH-valuetools08.pdf}, doi = {10.4108/ICST.VALUETOOLS2008.4411}, abstract = {In~this paper, the Non deterministic Repairable Fault Tree~(NdRFT) formalism is proposed: it allows to model failure modes of complex systems as well as their repair processes. The originality of this formalism with respect to other Fault Tree extensions is that it allows to face repair strategies optimization problems: in~an NdRFT model, the decision on whether to start or not a given repair action is non deterministic, so that all the possibilities are left open. The formalism is rather powerful allowing to specify which failure events are observable, whether local repair or global repair can be applied, and the resources needed to start a repair action. The optimal repair strategy can then be computed by solving an optimization problem on a Markov Decision Process~(MDP) derived from the NdRFT. A~software framework is proposed in order to perform in automatic way the derivation of an MDP from a NdRFT model, and to deal with the solution of the MDP.} }

@article{DDMR-fmsd08, publisher = {Springer}, journal = {Formal Methods in System Design}, author = {De{~}Wulf, Martin and Doyen, Laurent and Markey, Nicolas and Raskin, Jean-Fran{\c{c}}ois}, title = {Robust Safety of Timed Automata}, year = 2008, month = dec, volume = 33, number = {1-3}, pages = {45-84}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDMR-fmsd08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDMR-fmsd08.pdf}, doi = {10.1007/s10703-008-0056-7}, abstract = {Timed automata are governed by an idealized semantics that assumes a perfectly precise behavior of the clocks. The traditional semantics is not robust because the slightest perturbation in the timing of actions may lead to completely different behaviors of the automaton. Following several recent works, we consider a relaxation of this semantics, in which guards on transitions are widened by~\(\Delta>0\) and clocks can drift by~\(\epsilon>0\). The relaxed semantics encompasses the imprecisions that are inevitably present in an implementation of a timed automaton, due to the finite precision of digital clocks.\par We solve the safety verification problem for this robust semantics: given a timed automaton and a set of bad states, our algorithm decides if there exist positive values for the parameters~\(\Delta\) and~\(\epsilon\) such that the timed automaton never enters the bad states under the relaxed semantics.} }

@inproceedings{Bur-atva08, address = {Seoul, Korea}, month = oct, year = {2008}, volume = 5311, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Cha, Sungdeok and Choi, Jin-Young and Kim, Moonzoo and Lee, Insup and Viswanathan, Mahesh}, acronym = {{ATVA}'08}, booktitle = {{P}roceedings of the 6th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'08)}, author = {Bursztein, Elie}, title = {Net{Q}i: A~Model Checker for Anticipation Game}, pages = {246-251}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bur-atva08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bur-atva08.pdf}, doi = {10.1007/978-3-540-88387-6_22}, abstract = {NetQi is a freely available model-checker designed to analyze network incidents such as intrusion. This tool is an implementation of the anticipation game framework, a variant of timed game tailored for network analysis. The main purpose of NetQi is to find, given a network initial state and a set of rules, the best strategy that fulfills player objectives by model-checking the anticipation game and comparing the outcome of each play that fulfills strategy constraints. For instance, it can be used to find the best patching strategy. NetQi has been successfully used to analyze service failure due to hardware, network intrusion, worms and multiple-site intrusion defense cooperation.} }

@inproceedings{ACEF-rp08, address = {Liverpool, UK}, month = dec, year = 2008, volume = 223, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier Science Publishers}, editor = {Halava, Vesa and Potapov, Igor}, acronym = {{RP}'08}, booktitle = {{P}roceedings of the 2nd {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'08)}, author = {Andr{\'e}, {\'E}tienne and Chatain, {\relax Th}omas and Encrenaz, Emmanuelle and Fribourg, Laurent}, title = {An Inverse Method for Parametric Timed Automata}, pages = {29-46}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACEF-rp08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACEF-rp08.pdf}, doi = {10.1016/j.entcs.2008.12.029}, abstract = {Given a timed automaton with parametric timings, our objective is to describe a procedure for deriving constraints on the parametric timings in order to ensure that, for~each value of parameters satisfying these constraints, the behaviors of the timed automata are time-abstract equivalent. We~will exploit a reference valuation of the parameters that is supposed to capture a characteristic proper behavior of the system. The~method has been implemented and is illustrated on various examples of asynchronous circuits.} }

@techreport{LSV:08:18, author = {Goubault{-}Larrecq, Jean}, title = {A Cone-Theoretic {K}rein-{M}ilman Theorem}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = 2008, month = jun, type = {Research Report}, number = {LSV-08-18}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-18.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-18.pdf}, note = {8~pages}, abstract = {We prove the following analogue of the Krein-Milman Theorem: in any locally convex \(T_{0}\) topological cone, every convex compact saturated subset is the compact saturated convex hull of its extreme points.} }

@inproceedings{bbjlr-formats08, address = {Saint-Malo, France}, month = sep, year = 2008, volume = 5215, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Cassez, Franck and Jard, Claude}, acronym = {{FORMATS}'08}, booktitle = {{P}roceedings of the 6th {I}nternational {C}onference on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'08)}, author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and Jurdzi{\'n}ski, Marcin and Lazi{\'c}, Ranko and Rutkowski, Micha{\l}}, title = {Average-Price and Reachability-Price Games on Hybrid Automata with Strong Resets}, pages = {63-77}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bbjlr-formats08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bbjlr-formats08.pdf}, doi = {10.1007/978-3-540-85778-5_6}, abstract = {We introduce and study hybrid automata with strong resets. They generalize o-minimal hybrid automata, a class of hybrid automata which allows modeling of complex continuous dynamics. A number of analysis problems, such as reachability testing and controller synthesis, are decidable for classes of o-minimal hybrid automata. We generalize existing decidability results for controller synthesis on hybrid automata and we establish new ones by proving that average-price and reachability-price games on hybrid systems with strong resets are decidable, provided that the structure on which the hybrid automaton is defined has a decidable first-order theory. Our proof techniques include a novel characterization of values in games on hybrid systems by optimality equations, and a definition of a new finitary equivalence relation on the states of a hybrid system which enables a reduction of games on hybrid systems to games on finite graphs. } }

@inproceedings{bflms-formats08, address = {Saint-Malo, France}, month = sep, year = 2008, volume = 5215, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Cassez, Franck and Jard, Claude}, acronym = {{FORMATS}'08}, booktitle = {{P}roceedings of the 6th {I}nternational {C}onference on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'08)}, author = {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim G. and Markey, Nicolas and Srba, Ji{\v{r}}{\'\i}}, title = {Infinite Runs in Weighted Timed Automata with Energy Constraints}, pages = {33-47}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFLMS-formats08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFLMS-formats08.pdf}, doi = {10.1007/978-3-540-85778-5_4}, abstract = {We~study the problems of existence and construction of infinite schedules for finite weighted automata and one-clock weighted timed automata, subject to boundary constraints on the accumulated weight. More specifically, we~consider automata equipped with positive and negative weights on transitions and locations, corresponding to the production and consumption of some resource (\emph{e.g.}~energy). We~ask the question whether there exists an infinite path for which the accumulated weight for any finite prefix satisfies certain constraints (\emph{e.g.}~remains between~\(0\) and some given upper-bound). We~also consider a game version of the above, where certain transitions may be uncontrollable.} }

@article{CJP-lmcs08, journal = {Logical Methods in Computer Science}, author = {Comon{-}Lundh, Hubert and Jacquemard, Florent and Perrin, Nicolas}, title = {Visibly Tree Automata with Memory and Constraints}, year = 2008, month = jun, volume = 4, number = {2\string:8}, nopages = {}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CJP-lmcs08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CJP-lmcs08.pdf}, doi = {10.2168/LMCS-4(2:8)2008}, abstract = {Tree automata with one memory have been introduced in~2001. They generalize both pushdown (word) automata and the tree automata with constraints of equality between brothers of Bogaert and Tison. Though it has a decidable emptiness problem, the main weakness of this model is its lack of good closure properties.\par We propose a generalization of the visibly pushdown automata of Alur and~Madhusudan to a family of tree recognizers which carry along their (bottom-up) computation an auxiliary unbounded memory with a tree structure (instead of a symbol stack). In~other words, these recognizers, called Visibly Tree Automata with Memory~(VTAM) define a subclass of tree automata with one memory enjoying Boolean closure properties. We~show in particular that they can be determinized and the problems like emptiness, membership, inclusion and universality are decidable for VTAM. Moreover, we propose several extensions of VTAM whose transitions may be constrained by different kinds of tests between memories and also constraints \emph{{\`a}~la} Bogaert and~Tison. We~show that some of these classes of constrained VTAM keep the good closure and decidability properties, and we demonstrate their expressiveness with relevant examples of tree languages.} }

@inproceedings{ABH-dlt08, address = {Kyoto, Japan}, month = sep, year = 2008, volume = 5257, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Ito, Masami and Toyama, Masafumi}, acronym = {{DLT}'08}, booktitle = {{P}roceedings of the 12th {I}nternational {C}onference on {D}evelopments in {L}anguage {T}heory ({DLT}'08)}, author = {Atig, Mohamed Faouzi and Bollig, Benedikt and Habermehl, Peter}, title = {Emptiness of multi-pushdown automata is \(2\){ETIME}-complete}, pages = {121-133}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABH-dlt08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABH-dlt08.pdf}, doi = {10.1007/978-3-540-85780-8_9}, abstract = {We consider multi-pushdown automata, a multi-stack extension of pushdown automata that comes with a constraint on stack operations: a pop can only be performed on the first non-empty stack (which implies that we assume a linear ordering on the collection of stacks). We show that the emptiness problem for multi-pushdown automata is 2ETIME-complete wrt.~the number of stacks. Containment in 2ETIME is shown by translating an automaton into a grammar for which we can check if the generated language is empty. The lower bound is established by simulating the behavior of an alternating Turing machine working in exponential space. We also compare multi-pushdown automata with the model of bounded-phase multi-stack (visibly) pushdown automata.} }

@inproceedings{CDFPS-qest08, address = {Saint~Malo, France}, month = sep, year = 2008, publisher = {{IEEE} Computer Society Press}, acronym = {{QEST}'08}, booktitle = {{P}roceedings of the 5th {I}nternational {C}onference on {Q}uantitative {E}valuation of {S}ystems ({QEST}'08)}, author = {Chamseddine, Najla and Duflot, Marie and Fribourg, Laurent and Picaronny, Claudine and Sproston, Jeremy}, title = {Computing Expected Absorption Times for Parametric Determinate Probabilistic Timed Automata}, pages = {254-263}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDFPS-qest08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDFPS-qest08.pdf}, doi = {10.1109/QEST.2008.34}, abstract = {We consider a variant of probabilistic timed automata called \emph{parametric determinate probabilistic timed automata}. Such~automata are fully probabilistic: there~is a single distribution of outgoing transitions from each of the automaton's nodes, and~it~is possible to remain at a node only for a given amount of time. The~residence time within a node may be given in terms of a parameter, and~hence we do not assume that its concrete value is known.\par We claim that, often in practice, the maximal expected time to reach a given absorbing node of a probabilistic timed automaton can be captured using a parametric determinate probabilistic timed automaton. We give a method for computing the expected time for a parametric determinate probabilistic timed automaton to reach an absorbing node. The~method consists in constructing a variant of a Markov chain with costs (where the costs correspond to durations), and~is parametric in the sense that the expected absorption time is computed as a function of the model's parameters. The~complexity of the analysis is independent from the maximal constant bounding the values of the clocks, and is polynomial in the number of edges of the original parametric determinate probabilistic timed automaton.} }

@inproceedings{JR-rta2008, address = {Hagenberg, Austria}, month = jul, year = 2008, volume = 5117, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Voronkov, Andrei}, acronym = {{RTA}'08}, booktitle = {{P}roceedings of the 19th {I}nternational {C}onference on {R}ewriting {T}echniques and {A}pplications ({RTA}'08)}, author = {Jacquemard, Florent and Rusinowitch, Micha{\"e}l}, title = {Closure of {H}edge-Automata Languages by {H}edge Rewriting}, pages = {157-171}, doi = {10.1007/978-3-540-70590-1_11}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JR-rta08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JR-rta08.pdf}, abstact = {We consider rewriting systems for unranked ordered terms, \textit{i.e.}, trees where the number of successors of a node is not determined by its label, and is not \textit{a priori} bounded. The rewriting systems are defined such that variables in the rewrite rules can be substituted by hedges (sequences of terms) instead of just terms. Consequently, this notion of rewriting subsumes both standard term rewriting and word rewriting.\par We investigate some preservation properties for two classes of languages of unranked ordered terms under this generalization of term rewriting. The considered classes include languages of hedge automata (HA) and some extension (called CF-HA) with context-free languages in transitions, instead of regular languages.\par In particular, we show that the set of unranked terms reachable from a given HA language, using a so called inverse context-free rewrite system, is a HA language. The proof, based on a HA completion procedure, reuses and combines known techniques with non-trivial adaptations. Moreover, we prove, with different techniques, that the closure of CF-HA languages with respect to restricted context-free rewrite systems, the symmetric case of the above rewrite systems, is a CF-HA language. As a consequence, the problems of ground reachability and regular hedge model checking are decidable in both cases. We give several counter examples showing that we cannot relax the restrictions.} }

@proceedings{DJ-time2008, title = {{P}roceedings of the 15th {I}nternational {S}ymposium on {T}emporal {R}epresentation and {R}easoning ({TIME}'08)}, booktitle = {{P}roceedings of the 15th {I}nternational {S}ymposium on {T}emporal {R}epresentation and {R}easoning ({TIME}'08)}, editor = {Demri, St{\'e}phane and Jensen, {\relax Ch}ristian S.}, publisher = {{IEEE} Computer Society Press}, year = 2008, month = jun, address = {Montr{\'e}al, Canada} }

@inproceedings{CS-concur08, address = {Toronto, Canada}, month = aug, year = 2008, volume = 5201, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {van Breugel, Franck and Chechik, Marsha}, acronym = {{CONCUR}'08}, booktitle = {{P}roceedings of the 19th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'08)}, author = {Chambart, Pierre and Schnoebelen, {\relax Ph}ilippe}, title = {Mixing Lossy and Perfect Fifo Channels}, pages = {340-355}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-concur08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-concur08.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CS-concur08.ps}, doi = {10.1007/978-3-540-85361-9_28}, abstract = {We~consider asynchronous networks of finite-state systems communicating \emph{via} a combination of reliable and lossy fifo channels. Depending on the topology, the~reachability problem for such networks may be decidable. We~provide a complete classification of network topologies according to whether they lead to a decidable reachability problem. Furthermore, this classification can be decided in polynomial-time.} }

@inproceedings{BCHK-concur08, address = {Toronto, Canada}, month = aug, year = 2008, volume = 5201, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {van Breugel, Franck and Chechik, Marsha}, acronym = {{CONCUR}'08}, booktitle = {{P}roceedings of the 19th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'08)}, author = {Baldan, Paolo and Chatain, {\relax Th}omas and Haar, Stefan and K{\"o}nig, Barbara}, title = {Unfolding-based Diagnosis of Systems with an Evolving Topology}, pages = {203-217}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCHK-concur08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCHK-concur08.pdf}, doi = {10.1007/978-3-540-85361-9_19}, abstract = {We propose a framework for model-based diagnosis of systems with mobility and variable topologies, modelled as graph transformation systems. Generally speaking, model-based diagnosis is aimed at constructing explanations of observed faulty behaviours on the basis of a given model of the system. Since the number of possible explanations may be huge we exploit the unfolding as a compact data structure to store them, along the lines of previous work dealing with Petri net models. Given a model of a system and an observation, the explanations can be constructed by unfolding the model constrained by the observation, and then removing incomplete explanations in a pruning phase. The theory is formalised in a general categorical setting: constraining the system by the observation corresponds to taking a product in the chosen category of graph grammars, so that the correctness of the procedure can be proved by using the fact that the unfolding is a right adjoint and thus it preserves products. The theory thus should be easily applicable to a wide class of system models, including graph grammars and Petri nets.} }

@inproceedings{BKKL-concur08, address = {Toronto, Canada}, month = aug, year = 2008, volume = 5201, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {van Breugel, Franck and Chechik, Marsha}, acronym = {{CONCUR}'08}, booktitle = {{P}roceedings of the 19th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'08)}, author = {Bollig, Benedikt and Katoen, Joost-Pieter and Kern, Carsten and Leucker, Martin}, title = {{\itshape Smyle}: A Tool for Synthesizing Distributed Models from Scenarios by Learning}, pages = {162-166}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-concur08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-concur08.pdf}, doi = {10.1007/978-3-540-85361-9_15} }

@inproceedings{LV-concur08, address = {Toronto, Canada}, month = aug, year = 2008, volume = 5201, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {van Breugel, Franck and Chechik, Marsha}, acronym = {{CONCUR}'08}, booktitle = {{P}roceedings of the 19th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'08)}, author = {Lozes, {\'E}tienne and Villard, Jules}, title = {A Spatial Equational Logic for the Applied {{\(\pi\)}}-Calculus}, pages = {387-401}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LV-concur08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LV-concur08.pdf}, doi = {10.1007/978-3-540-85361-9_31}, abstract = {Spatial logics have been proposed to reason locally and modularly on algebraic models of distributed systems. In this paper we define the spatial equational logic A\(\pi\)L whose models are processes of the applied \(\pi\)-calculus. This extension of the \(\pi\)-calculus allows term manipulation and records communications as active substitutions in a frame, thus augmenting the underlying predefined equational theory. Our logic allows one to reason locally either on frames or on processes, thanks to static and dynamic spatial operators. We study the logical equivalences induced by various relevant fragments of~A\(\pi\)L, and~show in particular that the whole logic induces a coarser equivalence than structural congruence. We give characteristic formulae for some of these equivalences and for static equivalence. Going further into the exploration of A\(\pi\)L's expressivity, we~also show that it can eliminate standard term quantification.} }

@inproceedings{ABGMN-concur08, address = {Toronto, Canada}, month = aug, year = 2008, volume = 5201, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {van Breugel, Franck and Chechik, Marsha}, acronym = {{CONCUR}'08}, booktitle = {{P}roceedings of the 19th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'08)}, author = {Akshay, S. and Bollig, Benedikt and Gastin, Paul and Mukund, Madhavan and Narayan Kumar, K.}, title = {Distributed Timed Automata with Independently Evolving Clocks}, pages = {82-97}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABGMN-concur08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABGMN-concur08.pdf}, doi = {10.1007/978-3-540-85361-9_10}, abstract = { We propose a model of distributed timed systems where each component is a timed automaton with a set of local clocks that evolve at a rate independent of the clocks of the other components. A clock can be read by any component in the system, but it can only be reset by the automaton it belongs to.\par There are two natural semantics for such systems. The \emph{universal} semantics captures behaviors that hold under any choice of clock rates for the individual components. This is a natural choice when checking that a system always satisfies a positive specification. However, to check if a system avoids a negative specification, it is better to use the \emph{existential} semantics---the set of behaviors that the system can possibly exhibit under some choice of clock rates.\par We show that the existential semantics always describes a regular set of behaviors. However, in the case of universal semantics, checking emptiness turns out to be undecidable. As an alternative to the universal semantics, we propose a \emph{reactive} semantics that allows us to check positive specifications and yet describes a regular set of behaviors. } }

@inproceedings{FS-mfcs08, address = {Toru{\'n}, Poland}, month = aug, year = 2008, volume = {5162}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Ochma{\'n}ski, Edward and Tyszkiewicz, Jerzy}, acronym = {{MFCS}'08}, booktitle = {{P}roceedings of the 33rd {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'08)}, author = {Finkel, Alain and Sangnier, Arnaud}, title = {Reversal-bounded Counter Machines Revisited}, pages = {323-334}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-mfcs08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-mfcs08.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FS-mfcs08.ps}, doi = {10.1007/978-3-540-85238-4_26}, abstract = {We~extend the class of reversal-bounded counter machines by authorizing a finite number of alternations between increasing and decreasing mode over a given bound. We~prove that extended reversal-bounded counter machines also have effective semi-linear reachability sets. We~also prove that the property of being reversal-bounded is undecidable in general even when we fix the bound, whereas this problem becomes decidable when considering Vector Addition System with States.} }

@inproceedings{place-csl08, address = {Bertinoro, Italy}, month = sep, year = 2008, volume = 5213, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Kaminski, Michael and Martini, Simone}, acronym = {{CSL}'08}, booktitle = {{P}roceedings of the 17th {A}nnual {EACSL} {C}onference on {C}omputer {S}cience {L}ogic ({CSL}'08)}, author = {Place, {\relax Th}omas}, title = {Characterization of Logics Over Ranked Tree Languages}, pages = {401-415}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/place-csl08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/place-csl08.pdf}, doi = {10.1007/978-3-540-87531-4_29}, abstract = {We study the expressive power of the logics \(\textit{EF}+\textit{F}^{-1}\), \(\Delta_{2}\), and boolean combinations of \(\Sigma_{1}\) over ranked trees. In~particular, we provide effective characterizations of those three logics using algebraic identities. Characterizations had already been obtained for those logics over unranked trees, but both the algebra and the proofs were dependant on the properties of the unranked structure and the problem remained open for ranked trees.} }

@inproceedings{BDL-csl08, address = {Bertinoro, Italy}, month = sep, year = 2008, volume = 5213, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Kaminski, Michael and Martini, Simone}, acronym = {{CSL}'08}, booktitle = {{P}roceedings of the 17th {A}nnual {EACSL} {C}onference on {C}omputer {S}cience {L}ogic ({CSL}'08)}, author = {Brochenin, R{\'e}mi and Demri, St{\'e}phane and Lozes, {\'E}tienne}, title = {On~the Almighty Wand}, pages = {323-338}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDL-csl08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDL-csl08.pdf}, doi = {10.1007/978-3-540-87531-4_24}, abstract = {We investigate decidability, complexity and expressive power issues for (first-order) separation logic with one record field (herein called~SL) and its fragments. SL~can specify properties about the memory heap of programs with singly-linked lists. Separation logic with two record fields is known to be undecidable by reduction of finite satisfiability for classical predicate logic with one binary relation. Surprisingly, we~show that second-order logic is as expressive as SL and as a by-product we get undecidability of~SL. This is refined by showing that SL without the separating conjunction is as expressive as~SL, whence undecidable too. As~a consequence of this deep result, in~SL the magic wand can simulate the separating conjunction. By~contrast, we~establish that SL without the magic wand is decidable with non-elementary complexity by reduction from satisfiability for the first-order theory over finite words. Equivalence between second-order logic and separation logic extends to the case with more than one selector.} }

@inproceedings{bhhtv08ciaa, address = {San Francisco, California, USA}, month = jul, year = 2008, volume = 5148, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, editor = {Ibarra, Oscar H. and Ravikumar, Bala}, acronym = {{CIAA}'08}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {I}mplementation and {A}pplication of {A}utomata ({CIAA}'08)}, author = {Bouajjani, Ahmed and Habermehl, Peter and Hol\'{\i}k, Luk{\'a}{\v{s}} and Touili, Tayssir and Vojnar, Tom{\'a}{\v{s}}}, title = {Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata}, pages = {57-67}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bhhtv-ciaa08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bhhtv-ciaa08.pdf}, doi = {10.1007/978-3-540-70844-5_7}, abstract = {We propose new antichain-based algorithms for checking universality and inclusion of nondeterministic tree automata. We have implemented these algorithms in a prototype tool and we present experiments which show that the algorithms provide a significant improvement over the traditional determinisation-based approaches. Furthermore, we use the proposed antichain-based inclusion checking algorithm to build an abstract regular tree model checking framework based entirely on nondeterministic tree automata. We show the significantly improved efficiency of this framework on a series of experiments with verifying various programs over dynamic tree-shaped data structures linked by pointers.} }

@inproceedings{tCS-pods08, address = {Vancouver, Canada}, month = jun, year = 2008, publisher = {ACM Press}, editor = {Lenzerini, Maurizio and Lembo, Domenico}, acronym = {{PODS}'08}, booktitle = {{P}roceedings of the 27th {A}nnual {ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium on {P}rinciples of {D}atabase {S}ystems ({PODS}'08)}, author = {ten~Cate, Balder and Segoufin, Luc}, title = {{XP}ath, Transitive Closure Logic, and Nested Tree Walking Automata}, pages = {251-260}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/tCS-pods08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/tCS-pods08.pdf}, doi = {10.1145/1376916.1376952}, abstract = {We consider the navigational core of XPath, extended with two operators: the Kleene star for taking the transitive closure of path expressions, and a subtree relativisation operator, allowing one to restrict attention to a specific subtree while evaluating a subexpression. We show that the expressive power of this XPath dialect equals that of FO(MTC), first order logic extended with monadic transitive closure. We also give a characterization in terms of nested tree-walking automata. Using the latter we then proceed to show that the language is strictly less expressive than MSO. This solves an open question about the relative expressive power of FO(MTC) and MSO on trees. We~also investigate the complexity for our XPath dialect. We~show that query evaluation be done in polynomial time (combined complexity), but that satisfiability and query containment (as~well as emptiness for our automaton model) are 2ExpTime-complete (it is ExpTime-complete for Core XPath).} }

@inproceedings{ASV-pods08, address = {Vancouver, Canada}, month = jun, year = 2008, publisher = {ACM Press}, editor = {Lenzerini, Maurizio and Lembo, Domenico}, acronym = {{PODS}'08}, booktitle = {{P}roceedings of the 27th {A}nnual {ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium on {P}rinciples of {D}atabase {S}ystems ({PODS}'08)}, author = {Abiteboul, Serge and Segoufin, Luc and Vianu, Victor}, title = {Static Analysis of Active {XML} Systems}, pages = {221-230}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ASV-pods08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ASV-pods08.pdf}, doi = {10.1145/1376916.1376948}, abstract = {Active XML is a high-level specification language tailored to data-intensive, distributed, dynamic Web services. Active XML is based on XML documents with embedded function calls. The state of a document evolves depending on the result of internal function calls (local computations) or external ones (interactions with users or other services). Function calls return documents that may be active, so may activate new subtasks. The focus of the paper is on the verification of temporal properties of runs of Active XML systems, specified in a tree-pattern based temporal logic, Tree-LTL, that allows expressing a rich class of semantic properties of the application. The main results establish the boundary of decidability and the complexity of automatic verification of Tree-LTL properties.} }

@inproceedings{BBBM-qest08, address = {Saint~Malo, France}, month = sep, year = 2008, publisher = {{IEEE} Computer Society Press}, acronym = {{QEST}'08}, booktitle = {{P}roceedings of the 5th {I}nternational {C}onference on {Q}uantitative {E}valuation of {S}ystems ({QEST}'08)}, author = {Bertrand, Nathalie and Bouyer, Patricia and Brihaye, {\relax Th}omas and Markey, Nicolas}, title = {Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics}, pages = {55-64}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBM-qest08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBM-qest08.pdf}, doi = {10.1109/QEST.2008.19}, abstract = {In [Baier \emph{et~al.}, \textit{Probabilistic and Topological Semantics for Timed Automata}, FSTTCS'07] a probabilistic semantics for timed automata has been defined in order to rule out unlikely (sequences of) events. The qualitative model-checking problem for LTL properties has been investigated, where the aim is to check whether a given LTL property holds with probability~\(1\) in a timed automaton, and solved for the class of single-clock timed automata.\par In this paper, we consider the quantitative model-checking problem for \(\omega\)-regular properties: we aim at computing the exact probability that a given timed automaton satisfies an \(\omega\)-regular property. We develop a framework in which we can compute a closed-form expression for this probability; we furthermore give an approximation algorithm, and finally prove that we can decide the threshold problem in that framework.} }

@article{BLM-lmcs08, journal = {Logical Methods in Computer Science}, author = {Bouyer, Patricia and Larsen, Kim G. and Markey, Nicolas}, title = {Model Checking One-clock Priced Timed Automata}, volume = 4, number = {2\string:9}, nopages = {}, month = jun, year = 2008, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLM-lmcs08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLM-lmcs08.pdf}, doi = {10.2168/LMCS-4(2:9)2008}, abstract = {We consider the model of priced (a.k.a.~weighted) timed automata, an extension of timed automata with cost information on both locations and transitions, and we study various model-checking problems for that model based on extensions of classical temporal logics with cost constraints on modalities. We prove that, under the assumption that the model has only one clock, model-checking this class of models against the logic~WCTL, CTL with cost-constrained modalities, is PSPACE-complete (while it has been shown undecidable as soon as the model has three clocks). We~also prove that model checking WMTL (LTL with cost-constrained modalities) is decidable only if there is a single clock in the model and a single stopwatch cost variable (\textit{i.e.}, whose slopes lie in~\(\{0,1\}\)).} }

@inproceedings{AFFM-wollic08, address = {Edinburgh, Scotland, UK}, month = jul, year = 2008, volume = 5110, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Hodges, Wilfrid and de Queiroz, Ruy}, acronym = {{WoLLIC}'08}, booktitle = {{P}roceedings of the 15th {W}orkshop on {L}ogic, {L}anguage, {I}nformation and {C}omputation ({WoLLIC}'08)}, author = {Areces, Carlos and Figueira, Diego and Figueira, Santiago and Mera, Sergio}, title = {Expressive Power and Decidability for Memory Logics}, pages = {56-68}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AFFM-wollic08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AFFM-wollic08.pdf}, doi = {10.1007/978-3-540-69937-8_7}, abstract = {Taking as inspiration the hybrid logic~\(\mathcal{HL}(\downarrow)\), we~introduce a new family of logics that we call memory logics. In~this article we~present in detail two interesting members of this family defining their formal syntax and semantics. We then introduce a proper notion of bisimulation and investigate their expressive power (in comparison with modal and hybrid logics). We~will prove that in terms of expressive power, the memory logics we discuss in this paper are more expressive than orthodox modal logic, but less expressive than~\(\mathcal{HL}(\downarrow)\). We~also establish the undecidability of their satisfiability problems.} }

@inproceedings{EF-lix06, address = {Palaiseau, France}, month = apr, year = 2008, volume = 209, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier Science Publishers}, editor = {Palamidessi, Catuscia and Valencia, Franck}, acronym = {{LIX}'06}, booktitle = {{P}roceedings of the {LIX} {C}olloquium on {E}merging {T}rends in {C}oncurrency {T}heory ({LIX}'06)}, author = {Encrenaz, Emmanuelle and Fribourg, Laurent}, title = {Time Separation of Events: An Inverse Method}, pages = {135-148}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EF-lix06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EF-lix06.pdf}, doi = {10.1016/j.entcs.2008.04.008}, abstract = {The problem of {"}time separation{"} can be stated as follows: Given a system made of several connected components, each one entailing a local delay known with uncertainty, what is the maximum time for traversing the global system? This problem is useful, \textit{e.g.} in the domain of digital circuits, for determining the global traversal time of a signal from the knowledge of bounds on the component propagation delays. The uncertainty on each component delay is given under the form of an interval. The general problem is NP-complete. We focus here on the inverse problem: we seek intervals for component delays for which the global traversal time is guaranteed to be no greater than a specified maximum. We give a polynomial time method to solve it. As a typical application, we show how to use the method in order to relax some specified local delays while preserving the maximum traversal time. This is especially useful, in the area of digital circuits, for optimizing {"}setup{"} timings of input signals (minimum timings required for stability).} }

@article{LMO-lmcs08, journal = {Logical Methods in Computer Science}, author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas and Oreiby, Ghassan}, title = {On the Expressiveness and Complexity of~{ATL}}, volume = {4}, number = {2\string:7}, month = may, year = 2008, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LMO-lmcs08.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LMO-lmcs08.pdf}, corrigendumpdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LMO-lmcs08-erratum.pdf}, doi = {10.2168/LMCS-4(2:7)2008}, abstract = {ATL is a temporal logic geared towards the specification and verification of properties in multi-agents systems. It allows to reason on the existence of strategies for coalitions of agents in order to enforce a given property. We prove that the standard definition of~ATL (built on modalities {"}Next{"}, {"}Always{"} and~{"}Until{"}) has to be completed in order to express the duals of its modalities: it~is necessary to add the modality {"}Release{"}. We~then precisely characterize the complexity of ATL model-checking when the number of agents is not fixed. We prove that it is \(\Delta_{2}^{P}\) and \(\Delta_{3}^{P}\)-complete, depending on the underlying multi-agent model (ATS and CGS,~resp.). We also prove that~ATL\({}^{+}\) model-checking is \(\Delta_{3}^{P}\)-complete over both models, even with a fixed number of agents.} }

@inproceedings{BJ-ijcar08, address = {Sydney, Australia}, month = aug, year = 2008, volume = {5195}, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer-Verlag}, editor = {Armando, Alessandro and Baumgartner, Peter and Dowek, Gilles}, acronym = {{IJCAR}'08}, booktitle = {{P}roceedings of the 4th {I}nternational {J}oint {C}onference on {A}utomated {R}easoning ({IJCAR}'08)}, author = {Bouhoula, Adel and Jacquemard, Florent}, title = {Automated Induction with Constrained Tree Automata}, pages = {539-553}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BJ-ijcar08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BJ-ijcar08.pdf}, doi = {10.1007/978-3-540-71070-7_44}, abstract = {We propose a procedure for automated implicit inductive theorem proving for equational specifications made of rewrite rules with conditions and constraints. The constraints are interpreted over constructor terms (representing data values), and may express syntactic equality, disequality, ordering and also membership in a fixed tree language. Constrained equational axioms between constructor terms are supported and can be used in order to specify complex data structures like sets, sorted lists, trees, powerlists...\par Our procedure is based on tree grammars with constraints, a formalism which can describe exactly the initial model of the given specification (when it is sufficiently complete and terminating). They are used in the inductive proofs first as an induction scheme for the generation of subgoals at induction steps, second for checking validity and redundancy criteria by reduction to an emptiness problem, and third for defining and solving membership constraints.\par We show that the procedure is sound and refutationally complete. It~generalizes former test set induction techniques and yields natural proofs for several non-trivial examples presented in the paper, these examples are difficult (if not impossible) to specify and carry on automatically with other induction procedures.} }

@inproceedings{KMT-ijcar08, address = {Sydney, Australia}, month = aug, year = 2008, volume = {5195}, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer-Verlag}, editor = {Armando, Alessandro and Baumgartner, Peter and Dowek, Gilles}, acronym = {{IJCAR}'08}, booktitle = {{P}roceedings of the 4th {I}nternational {J}oint {C}onference on {A}utomated {R}easoning ({IJCAR}'08)}, author = {Kremer, Steve and Mercier, Antoine and Treinen, Ralf}, title = {Proving Group Protocols Secure Against Eavesdroppers}, pages = {116-131}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KMT-ijcar08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KMT-ijcar08.pdf}, doi = {10.1007/978-3-540-71070-7_9}, abstract = {Security protocols are small programs designed to ensure properties such as secrecy of messages or authentication of parties in a hostile environment. In this paper we investigate automated verification of a particular type of security protocols, called \emph{group protocols}, in the presence of an eavesdropper, i.e., a passive attacker. The specificity of group protocols is that the number of participants is not bounded.\par Our approach consists in representing an infinite set of messages exchanged during an unbounded number of sessions, one session for each possible number of participants, as well as the infinite set of associated secrets. We use so-called visibly tree automata with memory and structural constraints (introduced recently by Comon-Lundh \textit{et~al.}) to represent over-approximations of these two sets. We~identify restrictions on the specification of protocols which allow us to reduce the attacker capabilities guaranteeing that the above mentioned class of automata is closed under the application of the remaining attacker rules. The class of protocols respecting these restrictions is large enough to cover several existing protocols, such as the GDH family, GKE, and others.} }

@inproceedings{BHHKT-wodes08, address = {Gothenburg, Sweden}, month = may, year = 2008, acronym = {{WODES}'08}, booktitle = {{P}roceedings of the 9th {W}orkshop on {D}iscrete {E}vent {S}ystems ({WODES}'08)}, author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge and Hillah, Lom Messan and Kordon, Fabrice and Thierry{-}Mieg, Yann}, title = {Collision Avoidance in Intelligent Transport Systems: Towards an Application of Control Theory}, pages = {346-351}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHHKT-wodes08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHHKT-wodes08.pdf}, doi = {10.1109/WODES.2008.4605970}, abstract = {Safety is a prevalent issue in Intelligent Transport Systems~(ITS). To~ensure such a vital requirement, methodologies must offer support for the careful design and analysis of such systems. Indeed these steps must cope with temporal and spatial constraints associated with mobility rules and parallelism which induce a high complexity. Here we handle the problem of unexpected and uncontrollable vehicles which significantly endanger the traffic. In~this context, we~propose to apply discrete control theory to a model of automatic motorway in order to synthesize a controller that handles collision avoidance. This approach includes two parts: the design of a formal model and an efficient implementation based on hierarchical decision diagrams.} }

@proceedings{CKR-dagstuhl07, editor = {Chen, Liqun and Kremer, Steve and Ryan, Mark D.}, booktitle = {Formal Protocol Verification Applied}, title = {Formal Protocol Verification Applied}, year = 2008, address = {Dagstuhl, Germany}, series = {Dagstuhl Seminar Proceedings}, volume = {07421}, url = {http://drops.dagstuhl.de/portals/index.php?semnr=07421} }

@incollection{HM-mvrts08, author = {Haddad, Serge and Moreaux, Patrice}, title = {Verification of Probabilistic Systems Methods and Tools}, booktitle = {Modeling and Verification of Real-Time Systems}, editor = {Merz, Stephan and Navet, Nicolas}, year = {2008}, month = jan, pages = {289-318}, publisher = {ISTE Ltd. -- John Wiley \& Sons, Ltd.}, url = {http://www.lavoisier.fr/notice/fr1848210130.html} }

@inproceedings{BS-icalp08, address = {Reykjavik, Iceland}, month = jul, year = 2008, volume = 5126, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Aceto, Luca and Damg{\aa}rd, Ivan and Goldberg, Leslie~Ann and Halld{\'o}rsson, Magn{\'u}s M. and Ing{\'o}lfsd{\'o}ttir, Anna and Walukiewicz, Igor}, acronym = {{ICALP}'08}, booktitle = {{P}roceedings of the 35th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'08)~-- {P}art~{II}}, author = {Boja{\'n}czyk, Miko{\l}aj and Segoufin, Luc}, title = {Tree languages defined in first-order logic with one quantifier alternation}, pages = {233-245}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BS-icalp08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BS-icalp08.pdf}, doi = {10.1007/978-3-540-70583-3_20}, abstract = {We study tree languages that can be defined in \(\Delta_{2}\). These are tree languages definable by a first-order formula whose quantifier prefix is~\(\exists^{*}\forall^{*}\), and simultaneously by a first-order formula whose quantifier prefix is~\(\forall^{*}\exists^{*}\), both formulas over the signature with the descendant relation. We~provide an effective characterization of tree languages definable in~\(\Delta_{2}\). This characterization is in terms of algebraic equations. Over words, the class of word languages definable in~\(\Delta_{2}\) forms a robust class, which was given an effective algebraic characterization by Pin and Weil.} }

@inproceedings{BMOW-icalp08, address = {Reykjavik, Iceland}, month = jul, year = 2008, volume = 5126, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Aceto, Luca and Damg{\aa}rd, Ivan and Goldberg, Leslie~Ann and Halld{\'o}rsson, Magn{\'u}s M. and Ing{\'o}lfsd{\'o}ttir, Anna and Walukiewicz, Igor}, acronym = {{ICALP}'08}, booktitle = {{P}roceedings of the 35th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'08)~-- {P}art~{II}}, author = {Bouyer, Patricia and Markey, Nicolas and Ouaknine, Jo{\"e}l and Worrell, James}, title = {On Expressiveness and Complexity in Real-time Model Checking}, pages = {124-135}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMOW-icalp08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMOW-icalp08.pdf}, doi = {10.1007/978-3-540-70583-3_11}, abstract = {Metric Interval Temporal Logic (MITL) is a popular formalism for expressing real-time specifications. This logic achieves decidability by restricting the precision of timing constraints, in particular, by banning so-called \emph{punctual} specifications. In~this paper we~introduce a significantly more expressive logic that can express a wide variety of punctual specifications, but whose model-checking problem has the same complexity as that of~MITL. We~conclude that for model checking the most commonly occurring specifications, such as invariance and bounded response, punctuality can be accommodated at no cost.} }

@techreport{LSV:08:10, author = {Villard, Jules and Lozes, {\'E}tienne and Treinen, Ralf}, title = {A Spatial Equational Logic for the Applied pi-calculus}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = 2008, month = mar, type = {Research Report}, number = {LSV-08-10}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-10.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-10.pdf}, note = {44~pages}, abstract = {Spatial logics have been proposed to reason locally and modularly on algebraic models of distributed systems. In~this paper we~investigate a spatial equational logic (A\(\pi\)L) whose models are processes of the applied \(\pi\)-calculus, an extension of the \(\pi\)-calculus allowing term manipulation modulo a predefined equational theory, and wherein communications are recorded as active substitutions in a frame. Our logic allows us to reason locally either on frames or on processes, thanks to static and dynamic spatial operators. We study the logical equivalences induced by various relevant fragments of~A\(\pi\)L, and show in particular that the whole logic induces a coarser equivalence than structural congruence. We give characteristic formulae for this new equivalence as well as for static equivalence on frames. Going further into the exploration of A\(\pi\)L's expressivity, we also show that it can eliminate standard term quantication, and that the model-checking problem for the adjunct-free fragment of A\(\pi\)L can be reduced to satisfiability of a purely first-order logic of a term algebra.} }

@inproceedings{JGL:badweeds, address = {Budapest, Hungary}, month = mar, year = 2008, volume = 5289, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Leucker, Martin}, acronym = {{RV}'08}, booktitle = {{P}roceedings of the 8th {W}orkshop on {R}untime {V}erification ({RV}'08)}, author = {Goubault{-}Larrecq, Jean and Olivain, Julien}, title = {A Smell of Orchids}, pages = {1-20}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/go-rv08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/go-rv08.pdf}, doi = {10.1007/978-3-540-89247-2_1}, abstract = {Orchids is an intrusion detection tool based on techniques for fast, on-line model-checking. Orchids detects complex, correlated strands of events with very low overhead in practice, although its detec- tion algorithm has worst-case exponential time complexity.\par The purpose of this paper is twofold. First, we explain the salient features of the basic model-checking algorithm in an intuitive way, as a form of dynamically-spawned monitors. One distinctive feature of the Orchids algorithm is that fresh monitors need to be spawned at a pos- sibly alarming rate.\par The second goal of this paper is therefore to explain how we tame the complexity of the procedure, using abstract interpretation techniques to safely kill useless monitors. This includes monitors which will provably detect nothing, but also monitors that are subsumed by others, in the sense that they will definitely fail the so-called shortest run criterion. We take the opportunity to show how the Orchids algorithm maintains its monitors sorted in such a way that the subsumption operation is effected with no overhead, and we correct a small, but definitely annoying bug in its core algorithm, as it was published in~2001.} }

@article{BCHLR08-tcs, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {B{\'e}rard, B{\'e}atrice and Cassez, Franck and Haddad, Serge and Lime, Didier and Roux, Olivier H.}, title = {When are Timed Automata Weakly Timed Bisimilar to Time {P}etri Nets?}, year = 2008, month = sep, volume = 403, number = {2-3}, pages = {202-220}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCHLR-tcs08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCHLR-tcs08.pdf}, doi = {10.1016/j.tcs.2008.03.030}, abstract = {In this paper, we compare Timed Automata~(TA) and Time Petri Nets~(TPN) with respect to weak timed bisimilarity. It~is already known that the class of bounded TPNs is strictly included in the class of~TA. It~is thus natural to try and identify the subclass~\(\mathcal{TA}^{\textit{wtb}}\) of~TA equivalent to some TPN for the weak timed bisimulation relation. We~give a characterization of this subclass and we show that the membership problem and the reachability problem for \(\mathcal{TA}^{\textit{wtb}}\) are PSPACE-complete. Furthermore we show that for a TA in~\(\mathcal{TA}^{\textit{wtb}}\) with integer constants, an~equivalent TPN can be built with integer bounds but with a size exponential w.r.t.~the original model. Surprisingly, using rational bounds yields a TPN whose size is linear.} }

@inproceedings{JGL-csf08, address = {Pittsburgh, Pennsylvania, USA}, month = jun, year = 2008, publisher = {{IEEE} Computer Society Press}, acronym = {{CSF}'08}, booktitle = {{P}roceedings of the 21st {IEEE} {C}omputer {S}ecurity {F}oundations {S}ymposium ({CSF}'08)}, author = {Goubault{-}Larrecq, Jean}, title = {Towards Producing Formally Checkable Security Proofs, Automatically}, pages = {224-238}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-15.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-15.pdf}, doi = {10.1109/CSF.2008.21}, abstract = {First-order logic models of security for cryptographic protocols, based on variants of the Dolev-Yao model, are now well-established tools. Given that we have checked a given security protocol~\(\pi\) using a given first-order prover, how hard is it to extract a formally checkable proof of~it, as~required in, e.g., common criteria at evaluation level~\(7\)? We~demonstrate that this is surprisingly hard: the problem is non-recursive in general. On~the practical side, we show how we can extract finite models~\(\mathcal{M}\) from a set~\(\mathcal{S}\) of clauses representing~\(\pi\), automatically, in two ways. We~then define a model-checker testing \(\mathcal{M} \models \mathcal{S}\), and show how we can instrument it to output a formally checkable proof, e.g., in~Coq. This was implemented in the \texttt{h1} tool suite. Experience on a number of protocols shows that this is practical.} }

@inproceedings{DKR-csf08, address = {Pittsburgh, Pennsylvania, USA}, month = jun, year = 2008, publisher = {{IEEE} Computer Society Press}, acronym = {{CSF}'08}, booktitle = {{P}roceedings of the 21st {IEEE} {C}omputer {S}ecurity {F}oundations {S}ymposium ({CSF}'08)}, author = {Delaune, St{\'e}phanie and Kremer, Steve and Ryan, Mark D.}, title = {Composition of Password-based Protocols}, pages = {239-251}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-csf08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-csf08.pdf}, doi = {10.1109/CSF.2008.6}, abstract = {We investigate the composition of protocols that share a common secret. This situation arises when users employ the same password on different services. More precisely we study whether resistance against guessing attacks composes when the same password is used. We model guessing attacks using a common definition based on static equivalence in a cryptographic process calculus close to the applied pi calculus. We show that resistance against guessing attacks composes in the presence of a passive attacker. However, composition does not preserve resistance against guessing attacks for an active attacker. We therefore propose a simple syntactic criterion under which we show this composition to hold. Finally, we present a protocol transformation that ensures this syntactic criterion and preserves resistance against guessing attacks.} }

@inproceedings{DKS-csf08, address = {Pittsburgh, Pennsylvania, USA}, month = jun, year = 2008, publisher = {{IEEE} Computer Society Press}, acronym = {{CSF}'08}, booktitle = {{P}roceedings of the 21st {IEEE} {C}omputer {S}ecurity {F}oundations {S}ymposium ({CSF}'08)}, author = {Delaune, St{\'e}phanie and Kremer, Steve and Steel, Graham}, title = {Formal Analysis of {PKCS}\#11}, pages = {331-344}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKS-csf08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKS-csf08.pdf}, doi = {10.1109/CSF.2008.16}, abstract = {PKCS\#11 defines an API for cryptographic devices that has been widely adopted in industry. However, it~has been shown to be vulnerable to a variety of attacks that could, for example, compromise the sensitive keys stored on the device. In~this paper, we~set out a formal model of the operation of the API, which differs from previous security API models notably in that it accounts for non-monotonic mutable global state. We~give decidability results for our formalism, and describe an implementation of the resulting decision procedure using a model checker. We~report some new attacks and prove the safety of some configurations of the API in our model.} }

@techreport{LSV:08:08, author = {Finkel, Alain and Leroux, J{\'e}r{\^o}me}, title = {Presburger Functions are Piecewise Linear}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = 2008, month = mar, type = {Research Report}, number = {LSV-08-08}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-08.pdf}, note = {9~pages}, abstract = {In this paper we geometrically characterize sets and functions definable in the first order additive theory of the reals and the integers, a decidable extension of the Presburger arithmetic combining both integral and real variables. We introduce the notion of polinear sets, an extension of the linear sets that characterizes these sets and we prove that a function is definable in this logic if and only if it is piecewise rational linear.} }

@inproceedings{BSS-lics08, address = {Pittsburgh, Pennsylvania, USA}, month = jun, year = 2008, publisher = {{IEEE} Computer Society Press}, acronym = {{LICS}'08}, booktitle = {{P}roceedings of the 23rd {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'08)}, author = {Boja{\'n}czyk, Miko{\l}aj and Segoufin, Luc and Straubing, Howard}, title = {Piecewise Testable Tree Languages}, pages = {442-451}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BSS-lics08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BSS-lics08.pdf}, doi = {10.1109/LICS.2008.46}, abstract = {This paper presents a decidable characterization of tree languages that can be defined by a boolean combination of \(\Sigma_{1}\) formulas. This is a tree extension of the Simon theorem, which says that a string language can be defined by a boolean combination of \(\Sigma_{1}\) formulas if and only if its syntactic monoid is \(J\)-trivial. } }

@inproceedings{CS-lics08, address = {Pittsburgh, Pennsylvania, USA}, month = jun, year = 2008, publisher = {{IEEE} Computer Society Press}, acronym = {{LICS}'08}, booktitle = {{P}roceedings of the 23rd {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'08)}, author = {Chambart, Pierre and Schnoebelen, {\relax Ph}ilippe}, title = {The Ordinal Recursive Complexity of Lossy Channel Systems}, pages = {205-216}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-lics08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-lics08.pdf}, doi = {10.1109/LICS.2008.47}, abstract = {We show that reachability and termination for lossy channel systems is exactly at level \(\mathcal{F}_{\omega^{\omega}}\) in the Fast-Growing Hierarchy of recursive functions, the first level that dominates all multiply-recursive functions.} }

@inproceedings{BBBBG-lics08, address = {Pittsburgh, Pennsylvania, USA}, month = jun, year = 2008, publisher = {{IEEE} Computer Society Press}, acronym = {{LICS}'08}, booktitle = {{P}roceedings of the 23rd {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'08)}, author = {Baier, Christel and Bertrand, Nathalie and Bouyer, Patricia and Brihaye, {\relax Th}omas and Gr{\"o}{\ss}er, Marcus}, title = {Almost-Sure Model Checking of Infinite Paths in One-Clock Timed Automata}, pages = {217-226}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBBG-lics08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBBG-lics08.pdf}, doi = {10.1109/LICS.2008.25}, abstract = { In this paper, we~define two relaxed semantics (one based on probabilities and the other one based on the topological notion of largeness) for LTL over infinite runs of timed automata which rule out unlikely sequences of events. We~prove that these two semantics match in the framework of single-clock timed automata (and~only in that framework), and prove that the corresponding relaxed model-checking problems are PSPACE-Complete. Moreover, we~prove that the probabilistic non-Zenoness can be decided for single-clock timed automata in NLOGSPACE.} }

@inproceedings{DKS-TFIT2008, address = {Taipei, Taiwan}, month = mar, year = 2008, editor = {Kuo, Tei-Wei and Cruz-Lara, Samuel}, acronym = {{TFIT}'08}, booktitle = {{P}roceedings of the 4th {T}aiwanese-{F}rench {C}onference on {I}nformation {T}echnology ({TFIT}'08)}, author = {Delaune, St{\'e}phanie and Kremer, Steve and Steel, Graham}, title = {Formal Analysis of {PKCS}\#11}, pages = {267-278}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKS-tfit08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKS-tfit08.pdf}, abstract = {PKCS\#11 defines an API for cryptographic devices that has been widely adopted in industry. However, it~has been shown to be vulnerable to a variety of attacks that could, for~example, compromise the sensitive keys stored on the device. In~this paper, we~set out a formal model of the operation of the API, which differs from previous security API models notably in that it accounts for non-monotonic mutable global state. We give decidability results for our formalism, and describe an implementation of the resulting decision procedure using a model checker. We report some new attacks and prove the safety of some configurations of the API in our model.} }

@inproceedings{poti-TFIT2008, address = {Taipei, Taiwan}, month = mar, year = 2008, editor = {Kuo, Tei-Wei and Cruz-Lara, Samuel}, acronym = {{TFIT}'08}, booktitle = {{P}roceedings of the 4th {T}aiwanese-{F}rench {C}onference on {I}nformation {T}echnology ({TFIT}'08)}, author = {Bouyer, Patricia}, title = {Model-Checking Timed Temporal Logics}, pages = {132-142}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bouyer-tfit08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bouyer-tfit08.pdf}, abstract = {In this paper, we~present several timed extensions of temporal logics, that can be used for model-checking real-time systems. We~give different formalisms and the corresponding decidability\slash complexity results. We also give intuition to explain these results.} }

@inproceedings{DRS-ifiptm08, address = {Trondheim, Norway}, month = jun, year = 2008, volume = 263, series = {IFIP Conference Proceedings}, publisher = {Springer}, editor = {Karabulut, Yuecel and Mitchell, John and Herrmann, Peter and Jensen, Christian Damsgaard}, acronym = {IFIPTM'08}, booktitle = {{P}roceedings of the 2nd {J}oint i{T}rust and {PST} {C}onferences on {P}rivacy, {T}rust {M}anagement and {S}ecurity (IFIPTM'08)}, author = {Delaune, St{\'e}phanie and Ryan, Mark D. and Smyth, Ben}, title = {Automatic verification of privacy properties in the applied pi-calculus}, pages = {263-278}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DRS-ifiptm08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DRS-ifiptm08.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DRS-ifiptm08.ps}, abstract = {We develop a formal method verification technique for cryptographic protocols. We~focus on proving observational equivalences of the kind \(P \sim Q\), where the processes \(P\) and~\(Q\) have the same structure and differ only in the choice of terms. The calculus of ProVerif, a variant of the applied pi-calculus, makes some progress in this direction. We~expand the scope of ProVerif, to provide reasoning about further equivalences. We~also provide an extension which allows modelling of protocols which require global synchronisation. Finally we develop an algorithm to enable automated reasoning.\par We demonstrate the practicality of our work with two case studies.} }

@inproceedings{BFL-time08, address = {Montr{\'e}al, Canada}, month = jun, year = 2008, publisher = {{IEEE} Computer Society Press}, noeditor = {Demri, St{\'e}phane and Jensen, {\relax Ch}ristian S.}, acronym = {{TIME}'08}, booktitle = {{P}roceedings of the 15th {I}nternational {S}ymposium on {T}emporal {R}epresentation and {R}easoning ({TIME}'08)}, author = {Bouchy, Florent and Finkel, Alain and Leroux, J{\'e}r{\^o}me}, title = {Decomposition of Decidable First-Order Logics over Integers and Reals}, pages = {147-155}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFL-time08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFL-time08.pdf}, doi = {10.1109/TIME.2008.22}, abstract = {We tackle the issue of representing infinite sets of realvalued vectors. This paper introduces an operator for combining integer and real sets. Using this operator, we~decompose three well-known logics extending Presburger with reals. Our decomposition splits the logic into two parts: one~integer, and one decimal (\textit{i.e.},~on the interval~\([0,1[\)). We~also give some basis for an implementation of our representation.} }

@inproceedings{Bur-wistp08, address = {Sevilla, Spain}, month = may, year = 2008, volume = 5019, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Onieva, Jose A. and Sauveron, Damien and Chaumette, Serge and Gollmann, Dieter and Markantonakis, Konstantinos}, acronym = {{WISTP}'08}, booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop on {I}nformation {S}ecurity {T}heory and {P}ractices ({WISTP}'08)}, author = {Bursztein, Elie}, title = {Probabilistic Protocol Identification for Hard to Classify Protocol}, pages = {49-63}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bur-wistp08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bur-wistp08.pdf}, doi = {10.1007/978-3-540-79966-5_4}, note = {Best paper award}, abstract = {With the growing use of protocols obfuscation techniques, protocol identification for Q.O.S enforcement, traffic prohibition, and intrusion detection has became a complex task. This paper address this issue with a probabilistic identification analysis that combines multiples advanced identification techniques and returns an ordered list of probable protocols. It~combines a payload analysis with a classifier based on several discriminators, including packet entropy and size. We~show with its implementation, that it overcomes the limitations of traditional port-based protocol identification when dealing with hard to classify protocol such as peer to peer protocols. We also details how it deals with tunneled session and covert channel.} }

@inproceedings{BGMR-time08, address = {Montr{\'e}al, Canada}, month = jun, year = 2008, publisher = {{IEEE} Computer Society Press}, noeditor = {Demri, St{\'e}phane and Jensen, {\relax Ch}ristian S.}, acronym = {{TIME}'08}, booktitle = {{P}roceedings of the 15th {I}nternational {S}ymposium on {T}emporal {R}epresentation and {R}easoning ({TIME}'08)}, author = {Brihaye, {\relax Th}omas and Ghannem, Mohamed and Markey, Nicolas and Rieg, Lionel}, title = {Good friends are hard to find!}, pages = {32-40}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGMR-time08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGMR-time08.pdf}, doi = {10.1109/TIME.2008.10}, abstract = {We focus on the problem of finding (the~size of) a~minimal winning coalition in a multi-player game. More precisely, we~prove that deciding whether there is a winning coalition of size at most~\(k\) is NP-complete, while deciding whether \(k\) is the optimal size is DP-complete. We~also study different variants of our original problem: the function problem, where the aim is to effectively compute the coalition; more succinct encoding of the game; and richer families of winning objectives.} }

@article{DGK-ijfcs08, publisher = {World Scientific}, journal = {International Journal of Foundations of Computer Science}, author = {Diekert, Volker and Gastin, Paul and Kufleitner, Manfred}, title = {A Survey on Small Fragments of First-Order Logic over Finite Words}, volume = 19, number = 3, pages = {513-548}, year = 2008, month = jun, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DGK-ijfcs08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DGK-ijfcs08.pdf}, doi = {10.1142/S0129054108005802}, abstract = {We consider fragments of first-order logic over finite words. In~particular, we~deal with first-order logic with a restricted number of variables and with the lower levels of the alternation hierarchy. We~use the algebraic approach to show decidability of expressibility within these fragments. As~a byproduct, we~survey several characterizations of the respective fragments. We~give complete proofs for all characterizations and we provide all necessary background. Some of the proofs seem to be new and simpler than those which can be found elsewhere. We also give a proof of Simon's theorem on factorization forests restricted to aperiodic monoids because this is simpler and sufficient for our purpose.} }

@techreport{LSV:08:02, author = {Bursztein, Elie}, title = {Network Administrator and Intruder Strategies}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = 2008, month = feb, type = {Research Report}, number = {LSV-08-02}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-02.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-02.pdf}, note = {23~pages}, abstract = {The anticipation game framework is an extension of attack graphs based on game theory. It is used to anticipate and analyze intruder and administrator interactions with the network. In this paper we extend this framework with cost and reward in order to analyze and find player strategies. Additionally this extension allows to take into account the financial aspect of network security in the analysis. Intuitively a strategy is the best succession of actions that the administrator or the intruder can perform to achieve his objectives. Player objectives range from patching the network efficiently to compromising the most valuable network assets. We prove that finding the optimal strategy is decidable and only requires a linear memory space. Finally we show that finding strategy can be done in practice by evaluating the performance of our analyzer called NetQi.} }

@article{BFLP-sttt08, publisher = {Springer}, journal = {International Journal on Software Tools for Technology Transfer}, author = {Bardin, S{\'e}bastien and Finkel, Alain and Leroux, J{\'e}r{\^o}me and Petrucci, Laure}, title = {{FAST}: Acceleration from theory to practice}, year = 2008, month = oct, volume = 10, number = 5, pages = {401-424}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-16.pdf}, doi = {10.1007/s10009-008-0064-3}, abstract = {Fast acceleration of symbolic transition systems~(\textsc{Fast}) is a tool for the analysis of systems manipulating unbounded integer variables. We~check safety properties by computing the reachability set of the system under study. Even if this reachability set is not necessarily recursive, we~use innovative techniques, namely symbolic representation, acceleration and circuit selection, to~increase convergence. \textsc{Fast} has proved to perform very well on case studies. This~paper describes the tool, from the underlying theory to the architecture choices. Finally, \textsc{Fast} capabilities are compared with those of other tools. A~range of case studies from the literature is investigated.} }

@incollection{BL-litron08, author = {Bouyer, Patricia and Laroussinie, Fran{\c{c}}ois}, title = {Model Checking Timed Automata}, booktitle = {Modeling and Verification of Real-Time Systems}, editor = {Merz, Stephan and Navet, Nicolas}, year = {2008}, month = jan, pages = {111-140}, publisher = {ISTE Ltd. -- John Wiley \& Sons, Ltd.}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BL-litron08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BL-litron08.pdf} }

@article{PPSLBCH-commag08, publisher = {{IEEE} Communications Society}, journal = {IEEE Communications Magazine}, author = {Papadimitratos, Panos and Poturalski, Marcin and Schaller, Patrick and Lafourcade, Pascal and Basin, David and {\v{C}}apkun, Srdjan and Hubaux, Jean-Pierre}, title = {Secure Neighborhood Discovery: A~Fundamental Element for Mobile Ad Hoc Networking}, year = 2008, month = feb, volume = 46, number = 2, pages = {132-139}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PPSLBCH-commag08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PPSLBCH-commag08.pdf}, doi = {10.1109/MCOM.2008.4473095}, abstract = {Pervasive computing systems will likely be deployed in the near future, with the proliferation of wireless devices and the emergence of ad hoc networking as key enablers. Coping with mobility and the volatility of wireless communications in such systems is critical. Neighborhood Discovery~(ND), namely, the discovery of devices directly reachable for communication or in physical proximity, becomes a fundamental requirement and a building block for various applications. However, the very nature of wireless mobile networks makes it easy to abuse ND and thereby compromise the overlying protocols and applications. Thus, providing methods to mitigate this vulnerability and to secure ND is crucial. In~this article, we~focus on this problem and provide definitions of neighborhood types and ND protocol properties, as well as a broad classification of attacks. Our ND literature survey reveals that securing ND is indeed a difficult and largely open problem. Moreover, given the severity of the problem, we advocate the need to formally model neighborhood and to analyze ND schemes.} }

@article{BK-IC08, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Bollig, Benedikt and Kuske, Dietrich}, title = {{M}uller Message-Passing Automata and Logics}, volume = 206, number = {9-10}, pages = {1084-1094}, year = 2008, month = sep # {-} # oct, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BK-IC08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BK-IC08.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BK-IC08.ps}, doi = {10.1016/j.ic.2008.03.010}, abstract = {We study nonterminating message-passing automata whose behavior is described by infinite message sequence charts. As~a first result, we~show that Muller, B{\"u}chi, and termination-detecting Muller acceptance are equivalent for these devices. To~describe the expressive power of these automata, we give a logical characterization. More precisely, 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. This result is based on Vinner's extension of the classical Ehrenfeucht-Fra{\"\i}ss{\'e} game to cope with the infinity quantifier.} }

@misc{netanalyser-v0.7.5, author = {Bursztein, Elie}, title = {NetAnalyzer~v0.7.5}, year = {2008}, month = jan, nohowpublished = {Available at .... }, note = {Written in~C and Perl (about 25000 lines)}, note-fr = {\'Ecrit en~C et en Perl (environ 25000 lignes)} }

@incollection{DiGa08Thomas, author = {Diekert, Volker and Gastin, Paul}, title = {First-order definable languages}, booktitle = {Logic and Automata: History and Perspectives}, editor = {Flum, J{\"o}rg and Gr{\"a}del, Erich and Wilke, Thomas}, publisher = {Amsterdam University Press}, series = {Texts in Logic and Games}, volume = 2, year = 2008, pages = {261-306}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-WT08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-WT08.pdf}, abstract = {We give an essentially self-contained presentation of some principal results for first-order definable languages over finite and infinite words. We~introduce the notion of a \emph{counter-free} B{\"u}chi automaton; and we relate counter-freeness to \emph{aperiodicity} and to the notion of \emph{very weak alternation}. We also show that aperiodicity of a regular \(\infty\)-language can be decided in polynomial space, if the language is specified by some B{\"u}chi automaton.} }

@inproceedings{HMY-csndsp08, address = {Graz, Austria}, month = jul, year = 2008, publisher = {{IEEE} Computer Society Press}, noeditor = {}, acronym = {{CSNDSP}'08}, booktitle = {{P}roceedings of the 6th {S}ymposium on {C}ommunication {S}ystems, {N}etworks and {D}igital {S}ignal {P}rocessing ({CSNDSP}'08)}, author = {Haddad, Serge and Mokdad, Lynda and Youcef, Samir}, title = {Response Time Analysis of Composite Web Services}, pages = {506-510}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/HMY-csndsp08.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HMY-csndsp08.pdf}, abstract = {Service Oriented Computing (SOC) strives for applications with services as the fundamental items of design, and Web services acting as the enabling technology. Web services use open XML-based standards and are becoming the most important technology for communication between heterogenous business applications over Internet. In this paper, we focus on mean response times. Thus we propose analytical formulas for mean response times for structured BPEL constructors such as sequence, flow and switch. We propose also a response time formula for multi-choice pattern which is a generalization of switch constructor. Contrarily to previous studies in the literature, we consider that the servers can be heterogenous and the number of invoked elementary Web services can be variable.} }

@article{RBHJ-tsc08, publisher = {{IEEE} Computer Society Press}, journal = {IEEE Transactions on Services Computing}, author = {Rosario, Sidney and Benveniste, Albert and Haar, Stefan and Jard, Claude}, title = {Probabilistic {Q}o{S} and Soft Contracts for Transaction-Based Web Services Orchestrations}, pages = {187-200}, volume = 1, number = 4, month = oct # {-} # dec, year = 2008, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/RBHJ-tsc08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/RBHJ-tsc08.pdf}, doi = {10.1109/TSC.2008.17}, abstract = {Service level agreements (SLAs), or contracts, have an important role in web services. They define the obligations and rights between the provider of a web service and its client, about the function and the Quality of the service (QoS). For composite services like orchestrations, contracts are deduced by a process called QoS contract composition, based on contracts established between the orchestration and the called web services. Contracts are typically stated as hard guarantees (e.g., response time always less than 5 msec). Using hard bounds is not realistic, however, and more statistical approaches are needed. In this paper we propose using soft probabilistic contracts instead, which consist of a probability distribution for the considered QoS parameter---in this paper, we focus on timing. We show how to compose such contracts, to yield a global probabilistic contract for the orchestration. Our approach is implemented by the TOrQuE tool. Experiments on TOrQuE show that overly pessimistic contracts can be avoided and significant room for safe overbooking exists. An essential component of SLA management is then the continuous monitoring of the performance of called web services, to check for violations of the SLA. We propose a statistical technique for run-time monitoring of soft contracts.} }

@article{BHK-njc09, journal = {Nordic Journal of Computing}, author = {Boichut, Yohan and H{\'e}am, Pierre-Cyrille and Kouchnarenko, Olga}, title = {Approximation-based Tree Regular Model-Checking}, volume = {14}, number = {3}, pages = {216-241}, month = oct, year = 2008, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHK-njc09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHK-njc09.pdf}, abstract = {This paper addresses the following general problem of tree regular model-checking: decide whether \(\mathcal{R}^*(L)\cap L_{p} = \varnothing\) where \(\mathcal{R}^*\) is the reflexive and transitive closure of a successor relation induced by a term rewriting system~\(\mathcal{R}\), and \(L\) and \(L_p\) are both regular tree languages. We develop an automatic approximation-based technique to handle this---undecidable in general---problem in most practical cases, extending a recent work by Feuillade, Genet and Viet~Triem~Tong. We also make this approach fully automatic for practical validation of security protocols.} }

@article{LHS-lmcs08, journal = {Logical Methods in Computer Science}, author = {Lozes, {\'E}tienne and Hirschkoff, Daniel and Sangiorgi, Davide}, title = {Separability in the Ambient Logic}, volume = 4, number = {3:4}, year = 2008, month = sep, nopages = {}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LHS-lmcs08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LHS-lmcs08.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LHS-lmcs08.ps}, doi = {10.2168/LMCS-4(3:4)2008}, abstract = {The Ambient Logic~(AL) has been proposed for expressing properties of process mobility in the calculus of Mobile Ambients~(MA), and as a basis for query languages on semistructured data. \par We study some basic questions concerning the discriminating power of~AL, focusing on the equivalence on processes induced by the logic~(\(=_{L}\)). As underlying calculi besides~MA we~consider a subcalculus in which an image-finiteness condition holds and that we prove to be Turing complete. Synchronous variants of these calculi are studied as well. \par In these calculi, we provide two operational characterisations of~\(=_{L}\): a~coinductive one (as a form of bisimilarity) and an inductive one (based on structual properties of processes). After showing \(=_{L}\) to be stricly finer than barbed congruence, we establish axiomatisations of~\(=_{L}\) on the subcalculus of~MA (both the asynchronous and the synchronous version), enabling us to relate~\(=_{L}\) to structural congruence. We~also present some (un)decidability results that are related to the above separation properties for~AL: the~undecidability of~\(=_{L}\) on~MA and its decidability on the subcalculus.} }

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