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