@inproceedings{Laf-secret06,
  address = {Venice, Italy},
  month = jul,
  year = 2007,
  number = 4,
  volume = 171,
  series = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier Science Publishers},
  editor = {Fern{\'a}ndez, Maribel and Kirchner, Claude},
  acronym = {{SecReT}'06},
  booktitle = {{P}roceedings of the 1st 
           {I}nternational {W}orkshop on {S}ecurity and {R}ewriting {T}echniques
           ({SecReT}'06)},
  author = {Lafourcade, Pascal},
  title = {Intruder Deduction for the Equational Theory of 
                {\emph{Exclusive-or}}
                with Commutative and Distributive Encryption},
  pages = {37-57},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Laf-secret06-long.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Laf-secret06-long.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Laf-secret06-long.ps},
  nomorelongpdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/
        rr-lsv-2005-21.pdf},
  nomorelongps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
        rr-lsv-2005-21.ps},
  nomorelongpsgz = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PSGZ/
        rr-lsv-2005-21.ps.gz},
  doi = {10.1016/j.entcs.2007.02.054},
  abstract = {The first step in the verification of cryptographic protocols is
    to decide the intruder deduction problem, that is the vulnerability to a
    so-called passive attacker. We~extend the Dolev-Yao model in order to
    model this problem in presence of the equational theory of a commutative
    encryption operator which distributes over the \emph{exclusive-or}
    operator. The~interaction between the commutative distributive law of the
    encryption and \emph{exclusive-or} offers more possibilities to decrypt an
    encrypted message than in the non-commutative case, which imply a more
    careful analysis of the proof system. We~prove decidability of the
    intruder deduction problem for a commutative encryption which distributes
    over \emph{exclusive-or} with a DOUBLE-EXPTIME procedure. And~we obtain
    that this problem is EXPSPACE-hard in the binary case.}
}
@inproceedings{BJ-arspa07,
  address = {Wroc{\l}aw, Poland},
  month = jul,
  year = 2007,
  editor = {Degano, Pierpaolo and K{\"u}sters, Ralf and Vigan{\`o}, Luca and
                  Zdancewic, Steve},
  acronym = {{FCS-ARSPA}'07},
  booktitle = {{P}roceedings of the {J}oint {W}orkshop on {F}oundations of
                  {C}omputer {S}ecurity  and {A}utomated {R}easoning 
		  for {S}ecurity {P}rotocol {A}nalysis ({FCS-ARSPA}'07)},
  author = {Adel Bouhoula and Florent Jacquemard},
  title = {Verifying Regular Trace Properties of Security Protocols
		  with Explicit Destructors and Implicit Induction},
  pages = {27-44},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BJ-arspa07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BJ-arspa07.pdf},
  abstract = {We present a procedure for the verification of
    cryptographic protocols based on a new method for automatic implicit
    induction theorem proving for specifications made of conditional and
    constrained rewrite rules. The~method handles axioms between constructor
    terms which are used to introduce explicit destructor symbols for the
    specification of cryptographic operators. Moreover, it can deal with
    non-confluent rewrite systems. This is required in the context of the
    verification of security protocols because of the non-deterministic
    behavior of attackers. Our~induction method makes an intensive use of
    constrained tree grammars, which are used in proofs both as induction
    schemes and as oracles for checking validity and redundancy criteria by
    reduction to an emptiness problem. The grammars make possible the
    development of a generic framework for the specification and verification
    of protocols, where the specifications can be parametrized with (possibly
    infinite) regular sets of user names or attacker's initial knowledge and
    complex security properties can be expressed, referring to some fixed
    regular sets of bad traces representing potential vulnerabilities. 
    We present some case studies giving very promising results, for the detection
    of attacks (our~procedure is complete for refutation), and also for the
    validation of protocols.}
}
@mastersthesis{chambart-master,
  author = {Chambart, Pierre},
  title = {Canaux fiables et non-fiables~: fronti{\`e}res de la d{\'e}cidabilit{\'e}},
  school = {{M}aster {P}arisien de {R}echerche en 
	{I}nformatique, Paris, France},
  type = {Rapport de {M}aster},
  year = 2007,
  month = sep,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/chambart-m2.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/chambart-m2.pdf}
}
@phdthesis{gascon-these2007,
  author = {Gascon, R{\'e}gis},
  title = {Sp{\'e}cification et v{\'e}rification de propri{\'e}t{\'e}s 
		 quantitatives sur des automates {\`a} contraintes},
  year = 2007,
  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-RG07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-RG07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/these-RG07.ps},
  futureslides = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/SLIDES/
                these-FC07-slides.pdf}
}
@inproceedings{Bur-nordsec07,
  address = {Reykjavik, Iceland},
  month = oct,
  year = 2007,
  editor = {Erlingsson, {\'U}lfar and Sabelfeld, Andrei},
  acronym = {{NordSec}'07},
  booktitle = {{P}roceedings of the 12th {N}ordic {W}orkshop on {S}ecure {IT}
                  {S}ystems ({NordSec}'07)},
  author = {Bursztein, Elie},
  title = {Time has something to tell us about network address
                  translation},
  nopages = {},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bur-nordsec07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bur-nordsec07.pdf},
  abstract = { In this paper we introduce a new technique to count the number
    of host behind a~NAT. This technique based on TCP timestamp option, work
    with Linux and BSD system and therefore is complementary to the previous
    one base on IPID than does not work for those systems. Our~implementation
    demonstrates the practicability of this method.}
}
@inproceedings{BE-acsd07,
  address = {Bratislava, Slovak Republik},
  month = jul,
  year = 2007,
  publisher = {{IEEE} Computer Society Press},
  editor = {Basten, Twan and Shukla, Sandeep},
  acronym = {{ACSD}'07},
  booktitle = {{P}roceedings of the 7th {I}nternational
               {C}onference on {A}pplication of {C}oncurrency
               to {S}ystem {D}esign
               ({ACSD}'07)},
  author = {Braunstein, C{\'e}cile and Encrenaz, Emmanuelle},
  title = {Using {CTL} formulae as component abstraction in a design and
                  verification flow},
  pages = {80-89},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BE-acsd07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BE-acsd07.pdf},
  doi = {10.1109/ACSD.2007.76},
  abstract = {The verification of global properties (involving several
    components) is difficult to achieve, due to combinatorial explosion
    problem, while the verification of each component is easier to perform.
    Following the idea of~[F.~Xie and J.~Browne. \textit{Verified Systems by
    Composition from Verified Components}. In~ESEC/FSE'03, pages~277-286,
    Helsinki, Finland, 2003. ACM~Press], we~propose to build an abstraction
    of a component already verified, starting from a subset of its
    specification described as CTL formulae. This abstraction replaces the
    concrete component in the context of global properties verification. }
}
@techreport{Prouve:rap10,
  author = {Delaune, St{\'e}phanie and Klay, Francis},
  title = {Synth{\`e}se des exp{\'e}rimentations},
  institution = {projet RNTL PROUV{\'E}},
  month = may,
  year = 2007,
  type = {Technical Report},
  number = 10,
  note = {10~pages},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/prouve-rap10.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/prouve-rap10.pdf},
  abstract = {Dans ce document nous pr{\'e}sentons une synth{\`e}se des deux
    cas d'{\'e}tude trait{\'e}s durant le projet. Rappelons qu'il s'agit d'une
    part d'un protocole de commerce {\'e}lectronique et d'autre part d'un
    protocole de vote. Pour chacun de ces protocoles, nous analysons les
    r{\'e}sultats obtenus afin de d{\'e}gager l'apport des travaux issus du
    projet et les aspects qui n'ont pas pu etre compl{\`e}tement trait{\'e}s.
    Compte tenu des enseignements tir{\'e}s, dans la derni{\`e}re partie nous
    mettons en perspectives les axes de recherches envisageables pour traiter
    compl{\`e}tement des protocoles aussi complexes que celui du vote
    {\'e}lectronique.}
}
@techreport{LSV:07:31,
  author = {Jacquemard, Florent and Rusinowitch, Micha{\"e}l},
  title = {Rewrite Closure of {H}edge-Automata Languages},
  institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  year = 2007,
  month = oct,
  type = {Research Report},
  number = {LSV-07-31},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-31.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-31.pdf},
  note = {22~pages},
  abstract = {We investigate some preservation properties for classes of
    regular languages of unranked ordered terms under an appropriate
    generalization of term rewriting subsuming both standard term rewriting
    and word rewriting.\par
    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. In~particular, we~show, with a HA completion
    procedure, that the set of unranked terms reachable from a given HA
    language, using a so called inverse context-free rewrite system, is an HA
    language. Moreover, we~prove, using different techniques, the closure of
    CF-HA languages with respect to context-free rewrite systems, the
    symmetric case of the above rewrite systems. As~a consequence,
    the~problems of ground reachability and regular hedge model checking are
    decidable in both cases. We~give several several counter examples showing
    that we cannot relax the restrictions.}
}
@mastersthesis{dacosta-master,
  author = {Da{~}Costa, Arnaud},
  title = {Propri{\'e}t{\'e}s de jeux multi-agents},
  school = {{M}aster de {L}ogique {M}ath{\'e}matique
	et {F}ondements de l'{I}nformatique, Paris, France},
  type = {Rapport de {M}aster},
  year = 2007,
  month = sep,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/dacosta-m2.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/dacosta-m2.pdf}
}
@mastersthesis{villard-master,
  author = {Villard, Jules},
  title = {Logique spatiale pour le pi-calcul appliqu{\'e}},
  school = {{M}aster {P}arisien de {R}echerche en 
	{I}nformatique, Paris, France},
  type = {Rapport de {M}aster},
  year = 2007,
  month = sep,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/villard-m2.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/villard-m2.pdf}
}
@mastersthesis{vacher-master,
  author = {Vacher, Camille},
  title = {Accessibilit{\'e} inverse dans les automates d'arbres {\`a}
	 	 m{\'e}moire d'ordre sup{\'e}rieur},
  school = {{M}aster {P}arisien de {R}echerche en 
	{I}nformatique, Paris, France},
  type = {Rapport de {M}aster},
  year = 2007,
  month = sep,
  oldurl = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/vacher-m2.pdf},
  oldpdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/vacher-m2.pdf},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-35.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-35.pdf}
}
@inproceedings{CL-avocs07,
  address = {Oxford, UK},
  month = sep,
  year = {2007},
  editor = {Goldsmith, Michael and Roscoe, Bill},
  acronym = {{AVoCS}'07},
  booktitle = {{P}re-proceedings of the 7th {I}nternational
               {W}orkshop on {A}utomated {V}erification
               of {C}ritical {S}ystems
               ({AVoCS}'07)},
  author = {Cremers, Cas and Lafourcade, Pascal},
  title = {Comparing State Spaces in Automatic Security Protocol Verification},
  nmnote = {Pas paru dans les proceedings ENTCS},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CL-avocs07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CL-avocs07.pdf},
  abstract = {Many tools exist for automatic security protocol verification,
    and most of them have their own particular language for specifying
    protocols and properties. Several protocol specification models and
    security properties have been already formally related to each other.
    However, there is a further difference between verification tools, which
    has not been investigated in depth before: the~explored state space. Some
    tools explore all possible behaviors, whereas others explore strict
    subsets, often by using so-called scenarios. Ignoring such differences can
    lead to wrong interpretations of the output of a tool. We~relate the
    explored state spaces to each other and find previously unreported
    differences between the various approaches. We~apply our study of state
    space relations in a performance comparison of several well-known
    automatic tools for security protocol verification. We~model a set of
    protocols and their properties as homogeneous as possible for each tool.
    We~analyze the performance of the tools over comparable state spaces. This
    work allows us for the first time to compare these automatic tools fairly,
    i.e.,~using the same protocol description and exploring the same state
    space. We~also propose some explanations for our experimental results,
    leading to a better understanding of the tools.}
}
@inproceedings{BG-asian07,
  address = {Doha, Qatar},
  month = dec,
  year = 2007,
  volume = 4846,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Cervesato, Iliano},
  acronym = {{ASIAN}'07},
  booktitle = {{P}roceedings of the 12th {A}sian
               {C}omputing {S}cience {C}onference
               ({ASIAN}'07)},
  author = {Bursztein, Elie and Goubault{-}Larrecq, Jean},
  title = {A Logical Framework for Evaluating Network Resilience Against
                  Faults and Attacks},
  pages = {212-227},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGL-asian07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGL-asian07.pdf},
  doi = {10.1007/978-3-540-76929-3_20},
  abstract = {We present a logic-based framework to evaluate the resilience of
                  computer networks in the face of incidents, i.e., attacks
                  from malicious intruders as well as random faults. Our model
                  uses a two-layered presentation of dependencies between
                  files and services, and of timed games to represent not just
                  incidents, but also the dynamic responses from
                  administrators and their respective delays. We demonstrate
                  that a variant TATL\(\Diamond\) of timed alternating-time temporal
                  logic is a convenient language to express several desirable
                  properties of networks, including several forms of
                  survivability. We illustrate this on a simple redundant Web
                  service architecture, and show that checking such timed
                  games against the so-called TATL\(\Diamond\) variant of the timed
                  alternating time temporal logic TATL is EXPTIME-complete.}
}
@inproceedings{HIRV-atva2007,
  address = {Tokyo, Japan},
  month = oct,
  year = {2007},
  volume = 4762,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Namjoshi, Kedar and Yoneda, Tomohiro},
  acronym = {{ATVA}'07},
  booktitle = {{P}roceedings of the 5th {I}nternational
               {S}ymposium on {A}utomated {T}echnology
               for {V}erification and {A}nalysis
               ({ATVA}'07)},
  author = {Habermehl, Peter and Iosif, Radu and Rogalewicz, Adam and
                  Vojnar, Tom{\'a}{\v{s}}},
  title = {Proving Termination of Tree Manipulating Programs},
  pages = {145-161},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HIRV-atva07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HIRV-atva07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/HIRV-atva07.ps},
  doi = {10.1007/978-3-540-75596-8_12},
  abstract = {We consider the termination problem of programs manipulating
    tree-like dynamic data structures. Our~approach is based on a
    counter-example guided abstraction refinement loop. We use abstract
    regular tree model-checking to infer invariants of the program. Then,
    we~translate the program to a counter automaton~(CA) which simulates~it.
    If~the CA can be shown to terminate using existing techniques, the~program
    terminates. If~not, we analyse the possible counterexample given by a~CA
    termination checker and either conclude that the program does not
    terminate, or else refine the abstraction and repeat. We~show that the
    spuriousness problem for lasso-shaped counterexamples is decidable in some
    non-trivial cases. We~applied the method successfully on several
    interesting case studies. }
}
@inproceedings{BHJS-fct07,
  address = {Budapest, Hungary},
  month = aug,
  year = 2007,
  volume = 4639,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Csuhaj-Varj{\'u}, Erzs{\'e}bet and {\'E}sik, Zolt{\'a}n},
  acronym = {{FCT}'07},
  booktitle = {{P}roceedings of the 16th {I}nternational {S}ymposium
	  on {F}undamentals of {C}omputation {T}heory
	  ({FCT}'07)},
  author = {Bouajjani, Ahmed and Habermehl, Peter and 
           Jurski, Yan and Sighireanu, Mihaela},
  title = {Rewriting Systems with Data~-- {A} Framework for Reasoning About Systems with Unbounded 
		Structures over Infinite Data Domains},
  pages = {1-22},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHJS-fct07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHJS-fct07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BHJS-fct07.ps},
  doi = {10.1007/978-3-540-74240-1_1},
  abstract = {We introduce a uniform framework for reasoning about
    infinite-state systems with unbounded control structures and unbounded
    data domains. Our~framework is based on constrained rewriting systems on
    words over an infinite alphabet. We~consider several rewriting semantics:
    factor, prefix, and multiset rewriting. Constraints are expressed in a
    logic on such words which is parametrized by a first-order theory on the
    considered data domain. We show that our framework is suitable for
    reasoning about various classes of systems such as recursive sequential
    programs, multithreaded programs, parametrized and dynamic networks of
    processes,~etc. Then, we provide generic results (1)~for the decidability
    of the satisfiability problem of the fragment of this logic provided that
    the underlying logic on data is decidable, and (2)~for proving inductive
    invariance and for carrying out Hoare style reasoning within this
    fragment. We also show that the reachability problem if decidable for a
    class of prefix rewriting systems with integer data.}
}
@inproceedings{GPT-aplas07,
  address = {Singapore},
  month = nov # {-} # dec,
  year = 2007,
  volume = 4807,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Shao, Zhong},
  acronym = {{APLAS}'07},
  booktitle = {{P}roceedings of the 5th {A}sian {S}ymposium
               on {P}rogramming {L}anguages and {S}ystems
               ({APLAS}'07)},
  author = {Goubault{-}Larrecq, Jean and Palamidessi, Catuscia and
                  Troina, Angelo},
  title = {A Probabilistic Applied Pi-Calculus},
  pages = {175-290},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GPT-aplas07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GPT-aplas07.pdf},
  doi = {10.1007/978-3-540-76637-7_12},
  abstract = {We propose an extension of the Applied Pi-calculus by
    introducing nondeterministic and probabilistic choice operators. The
    semantics of the resulting model, in which probability and nondeterminism
    are combined, is given by Segala's Probabilistic Automata driven by
    schedulers which resolve the nondeterministic choice among the probability
    distributions over target states. Notions of static and observational
    equivalence are given for the enriched calculus. In order to model the
    possible interaction of a process with its surrounding environment a
    labeled semantics is given together with a notion of weak bisimulation
    which is shown to coincide with the observational equivalence. Finally, we
    prove that results in the probabilistic framework are preserved in a
    purely nondeterministic setting.}
}
@inproceedings{ABG-fsttcs07,
  address = {New~Delhi, India},
  month = dec,
  year = 2007,
  volume = 4855,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Arvind, V. and Prasad, Sanjiva},
  acronym = {{FSTTCS}'07},
  booktitle = {{P}roceedings of the 27th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'07)},
  author = {Akshay, S. and Bollig, Benedikt and Gastin, Paul},
  title = {Automata and Logics for Timed Message Sequence Charts},
  pages = {290-302},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABG-fsttcs07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABG-fsttcs07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ABG-fsttcs07.ps},
  doi = {10.1007/978-3-540-77050-3_24},
  abstract = {We provide a framework for distributed systems that impose timing constraints 
    on their executions. We~propose a timed model of communicating finite-state machines, 
    which communicate by exchanging messages through channels and use event clocks to 
    generate collections of timed message sequence charts~(T-MSCs). As~a specification 
    language, we~propose a monadic second-order logic equipped with timing predicates and 
    interpreted over~T-MSCs. We establish expressive equivalence of our automata and logic. 
    Moreover, we prove that, for (existentially) bounded channels, emptiness and 
    satisfiability are decidable for our automata and logic.}
}
@inproceedings{CS-fsttcs07,
  address = {New~Delhi, India},
  month = dec,
  year = 2007,
  volume = 4855,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Arvind, V. and Prasad, Sanjiva},
  acronym = {{FSTTCS}'07},
  booktitle = {{P}roceedings of the 27th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'07)},
  author = {Chambart, Pierre and Schnoebelen, {\relax Ph}ilippe},
  title = {{P}ost Embedding Problem is not Primitive Recursive, 
		 with Applications to Channel Systems},
  pages = {265-276},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-fsttcs07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-fsttcs07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CS-fsttcs07.ps},
  doi = {10.1007/978-3-540-77050-3_22},
  abstract = {We introduce \textsf{PEP}, the Post Embedding Problem, a variant
    of \textsf{PCP} where one compares strings with the subword relation, and
    \textsf{PEP}\textsuperscript{reg}, a further variant where solutions are
    constrained and must belong to a given regular language.
    \textsf{PEP}\textsuperscript{reg} is decidable but not primitive
    recursive. This entails the decidability of reachability for
    unidirectional systems with one reliable and one lossy channel. }
}
@inproceedings{CDD-fsttcs07,
  address = {New~Delhi, India},
  month = dec,
  year = 2007,
  volume = 4855,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Arvind, V. and Prasad, Sanjiva},
  acronym = {{FSTTCS}'07},
  booktitle = {{P}roceedings of the 27th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'07)},
  author = {Cortier, V{\'e}ronique and Delaitre, J{\'e}r{\'e}mie and
                  Delaune, St{\'e}phanie},
  title = {Safely Composing Security Protocols},
  pages = {352-363},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDD-fsttcs07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDD-fsttcs07.pdf},
  addendumpdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/
  		CDD-fsttcs07-addendum.pdf},
  doi = {10.1007/978-3-540-77050-3_29},
  abstract = {Security protocols are small programs that are executed in
    hostile environments. Many results and tools have been developed to
    formally analyze the security of a protocol in the presence of active
    attackers that may block, intercept and send new messages. However even
    when a protocol has been proved secure, there is absolutely no guarantee
    if the protocol is executed in an environment where other protocols,
    possibly sharing some common identities and keys like public keys or
    long-term symmetric keys, are executed.\par
    In this paper, we show that security of protocols can be easily composed.
    More precisely, we show that whenever a protocol is secure, it remains
    secure even in an environment where arbitrary protocols are executed,
    provided each encryption contains some tag identifying each protocol, like
    e.g.~the name of the protocol.}
}
@inproceedings{BBBBG-fsttcs07,
  address = {New~Delhi, India},
  month = dec,
  year = 2007,
  volume = 4855,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Arvind, V. and Prasad, Sanjiva},
  acronym = {{FSTTCS}'07},
  booktitle = {{P}roceedings of the 27th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'07)},
  author = {Baier, Christel and Bertrand, Nathalie and Bouyer, Patricia
                  and Brihaye, {\relax Th}omas and Gr{\"o}{\ss}er, Marcus},
  title = {Probabilistic and Topological Semantics for Timed Automata},
  pages = {179-191},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBBG-fsttcs07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBBG-fsttcs07.pdf},
  doi = {10.1007/978-3-540-77050-3_15},
  abstract = {Like most models used in model-checking, timed automata are an
    idealized mathematical model used for representing systems with strong
    timing requirements. In~such mathematical models, properties can be
    violated, due to unlikely (sequences~of) events. We~propose two new
    semantics for the satisfaction of LTL formulas, one based on
    probabilities, and the other one based on topology, to rule out these
    sequences. We~prove that the two semantics are equivalent and lead to a
    PSPACE-Complete model-checking problem for LTL over finite executions.}
}
@inproceedings{BKM-fsttcs07,
  address = {New~Delhi, India},
  month = dec,
  year = 2007,
  volume = 4855,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Arvind, V. and Prasad, Sanjiva},
  acronym = {{FSTTCS}'07},
  booktitle = {{P}roceedings of the 27th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'07)},
  author = {Bollig, Benedikt and Kuske, Dietrich and Meinecke, Ingmar},
  title = {Propositional Dynamic Logic for Message-Passing Systems},
  pages = {303-315},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKM-fsttcs07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKM-fsttcs07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BKM-fsttcs07.ps},
  doi = {10.1007/978-3-540-77050-3_25},
  abstract = {We examine a bidirectional Propositional Dynamic Logic~(PDL) for message 
    sequence charts~(MSCs) extending LTL and~TLC\textsuperscript{-}.
    Every formula is translated into an equivalent communicating finite-state
    machine~(CFM) of exponential size. This synthesis problem is solved in full generality, 
    i.e.,~also for MSCs with unbounded channels. The model checking problems for CFMs and 
    for HMSCs against PDL formulas are shown to be in PSPACE for existentially 
    bounded~MSCs. It~is shown that CFMs are to weak to capture the semantics of PDL with 
    intersection.}
}
@inproceedings{DKR-fsttcs07,
  address = {New~Delhi, India},
  month = dec,
  year = 2007,
  volume = 4855,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Arvind, V. and Prasad, Sanjiva},
  acronym = {{FSTTCS}'07},
  booktitle = {{P}roceedings of the 27th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'07)},
  author = {Delaune, St{\'e}phanie and Kremer, Steve and Ryan, Mark D.},
  title = {Symbolic Bisimulation for the Applied Pi-Calculus},
  pages = {133-145},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-fsttcs07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-fsttcs07.pdf},
  doi = {10.1007/978-3-540-77050-3_11},
  abstract = {We propose a symbolic semantics for the finite applied pi
    calculus, which is a variant of the pi calculus with extensions for
    modelling cryptgraphic protocols. By~treating inputs symbolically, our
    semantics avoids potentially infinite branching of execution trees due to
    inputs from the environment. Correctness is maintained by associating with
    each process a set of constraints on symbolic terms. Based on the
    semantics, we~define a sound symbolic labelled bisimulation relation.
    This~is an important step towards automation of observational equivalence
    for the finite applied pi calculus, \emph{e.g.}, for verification of
    anonymity or strong secrecy properties of protocols with a bounded number
    of sessions.}
}
@inproceedings{DR-lpar07,
  address = {Yerevan, Armenia},
  month = oct,
  year = 2007,
  volume = 4790,
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer},
  editor = {Dershowitz, Nachum and Voronkov, Andrei},
  acronym = {{LPAR}'07},
  booktitle = {{P}roceedings of the 14th {I}nternational
               {C}onference on {L}ogic for {P}rogramming,
               {A}rtificial {I}ntelligence, and {R}easoning
               ({LPAR}'07)},
  author = {Demri, St{\'e}phane and Rabinovich, Alexander},
  title = {The complexity of temporal logic with until and since over ordinals},
  pages = {531-545},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DR-lpar07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DR-lpar07.pdf},
  doi = {10.1007/978-3-540-75560-9_38},
  abstract = {We consider the temporal logic with since and until 
    modalities. This temporal logic is expressively equivalent over the 
    class of ordinals to first-order logic thanks to Kamp's theorem. 
    We~show that it has a PSPACE-complete satisfiability problem over the 
    class of ordinals. Among the consequences of our proof, we show that 
    given the code of some countable ordinal~\(\alpha\) and a formula, we 
    can decide in PSPACE whether the formula has a model over~\(\alpha\). 
    In~order to show these results, we~introduce a class of simple ordinal 
    automata, as expressive as B{\"u}chi ordinal automata. The PSPACE 
    upper bound for the satisfiability problem of the temporal logic is 
    obtained through a reduction to the nonemptiness problem for the 
    simple ordinal automata.}
}
@inproceedings{DLL-lpar07,
  address = {Yerevan, Armenia},
  month = oct,
  year = 2007,
  volume = 4790,
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer},
  editor = {Dershowitz, Nachum and Voronkov, Andrei},
  acronym = {{LPAR}'07},
  booktitle = {{P}roceedings of the 14th {I}nternational
               {C}onference on {L}ogic for {P}rogramming,
               {A}rtificial {I}ntelligence, and {R}easoning
               ({LPAR}'07)},
  author = {Delaune, St{\'e}phanie and Lin, Hai and Lynch, {\relax Ch}ristopher},
  title = {Protocol verification via rigid{\slash}flexible resolution},
  pages = {242-256},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLL-lpar07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLL-lpar07.pdf},
  doi = {10.1007/978-3-540-75560-9_19},
  abstract = {In this paper we propose a decision procedure, 
	i.e., an~inference system for clauses containing rigid and 
	flexible variables. Rigid variables are only allowed to have 
	one instantiation, whereas flexible variables are allowed as 
	many instantiations as desired. We~assume a set of clauses 
	containing only rigid variables together with a set of clauses 
	containing only flexible variables. When the flexible clauses 
	fall into a particular class, we propose an inference system 
	based on ordered resolution that is sound and complete and for 
	which the inference procedure will halt.\par
	    An interest in this form of problem is for cryptographic 
	protocol verification for a bounded number of protocol 
	instances. Our class allows us to obtain a generic decidability 
	result for a large class of cryptographic protocols that may 
	use for instance~CBC (Cipher Block Chaining) encryption and 
	blind signature. }
}
@inproceedings{CD-lpar07,
  address = {Yerevan, Armenia},
  month = oct,
  year = 2007,
  volume = 4790,
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer},
  editor = {Dershowitz, Nachum and Voronkov, Andrei},
  acronym = {{LPAR}'07},
  booktitle = {{P}roceedings of the 14th {I}nternational
               {C}onference on {L}ogic for {P}rogramming,
               {A}rtificial {I}ntelligence, and {R}easoning
               ({LPAR}'07)},
  author = {Cortier, V{\'e}ronique and Delaune, St{\'e}phanie},
  title = {Deciding Knowledge in Security Protocols for 
		 Monoidal Equational Theories},
  pages = {196-210},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CD-lpar07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CD-lpar07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CD-lpar07.ps},
  doi = {10.1007/978-3-540-75560-9_16},
  abstract = {In formal approaches, messages sent over a 
	network are usually modeled by terms together with an 
	equational theory, axiomatizing the properties of the 
	cryptographic functions (encryption, exclusive or,~...). 
	The~analysis of cryptographic protocols requires a 
	precise understanding of the attacker knowledge. Two 
	standard notions are usually used: deducibility and 
	indistinguishability. Only few results have been obtained 
	(in~an ad-hoc~way) for equational theories with 
	associative and commutative properties, especially in the 
	case of static equivalence. The~main contribution of this 
	paper is to propose a general setting for solving 
	deducibility and indistinguishability for an important 
	class (called monoidal) of these theories. Our~setting 
	relies on the correspondence between a monoidal 
	theory~{\(E\)} and a semiring~{\(S_E\)} which allows us 
	to give an algebraic characterization of the deducibility 
	and indistinguishability problems. As~a consequence we 
	recover easily existing decidability results and obtain 
	several new ones.}
}
@proceedings{secret2007-pre,
  title = {{P}reliminary {P}roceedings of the 2nd 
           {I}nternational {W}orkshop on {S}ecurity and {R}ewriting {T}echniques
           ({SecReT}'07)},
  booktitle = {{P}reliminary {P}roceedings of the 2nd 
           {I}nternational {W}orkshop on {S}ecurity and {R}ewriting {T}echniques
           ({SecReT}'07)},
  editor = {Nesi, Monica and Treinen, Ralf},
  year = 2007,
  month = jul,
  address = {Paris, France}
}
@inproceedings{phs-time07,
  address = {Alicante, Spain},
  month = jun,
  year = 2007,
  publisher = {{IEEE} Computer Society Press},
  editor = {Goranko, Valentin and Wang, X. Sean},
  acronym = {{TIME}'07},
  booktitle = {{P}roceedings of the 14th {I}nternational {S}ymposium on 
	       {T}emporal {R}epresentation and {R}easoning
	       ({TIME}'07)},
  author = {Schnoebelen, {\relax Ph}ilippe},
  title = {Model Checking Branching-Time Logics},
  pages = {5},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/phs-time07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/phs-time07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/phs-time07.ps},
  doi = {10.1109/TIME.2007.52}
}
@inproceedings{CDP-formats07,
  address = {Salzburg, Austria},
  month = oct,
  year = 2007,
  volume = 4763,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Raskin, Jean-Fran{\c{c}}ois and Thiagarajan, P. S.},
  acronym = {{FORMATS}'07},
  booktitle = {{P}roceedings of the 5th {I}nternational {C}onference
           on {F}ormal {M}odelling and {A}nalysis of {T}imed
           {S}ystems ({FORMATS}'07)},
  author = {Chevalier, Fabrice and D'Souza, Deepak and Prabhakar,
                  Pavithra},
  title = {Counter-free Input Determined Timed Automata},
  pages = {82-97},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDP-formats07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDP-formats07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CDP-formats07.ps},
  doi = {10.1007/978-3-540-75454-1_8},
  abstract = {We identify a class of timed automata, which we call
                  counter-free input-determined automata, which characterize
                  the class of timed languages definable by several timed
                  temporal logics in the literature, including~MTL. We~make
                  use of this characterization to show that MTL+Past satisfies
                  an {"}ultimate stability{"} property with respect to periodic
                  sequences of timed words. Our results hold for both the
                  pointwise and continuous semantics. Along the way we
                  generalize the result of McNaughton-Papert to show a
                  counter-free automata characterization of FO-definable
                  finitely varying functions.}
}
@inproceedings{BM-formats07,
  address = {Salzburg, Austria},
  month = oct,
  year = 2007,
  volume = 4763,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Raskin, Jean-Fran{\c{c}}ois and Thiagarajan, P. S.},
  acronym = {{FORMATS}'07},
  booktitle = {{P}roceedings of the 5th {I}nternational {C}onference
           on {F}ormal {M}odelling and {A}nalysis of {T}imed
           {S}ystems ({FORMATS}'07)},
  author = {Bouyer, Patricia and Markey, Nicolas},
  title = {Costs are Expensive!},
  pages = {53-68},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BM-formats07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BM-formats07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BM-formats07.ps},
  doi = {10.1007/978-3-540-75454-1_6},
  abstract = {We study the model-checking problem for WMTL, 
    a~cost-extension of the linear-time timed temporal logic MTL, that is
    interpreted over weighted timed automata. We~draw a complete picture of
    the decidability for that problem: it~is decidable only for the class of
    one-clock weighted timed automata with a restricted stopwatch cost, and
    any slight extension of this model leads to undecidability. We~finally
    give some consequences on the undecidability of linear hybrid automata.}
}
@inproceedings{BCD-jouannaud,
  address = {Cachan, France},
  month = jun,
  year = 2007,
  volume = 4600,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  acronym = {{R}ewriting, {C}omputation and {P}roof},
  booktitle = {{R}ewriting, {C}omputation and {P}roof~--- {E}ssays {D}edicated to
                  {J}ean-{P}ierre {J}ouannaud on the {O}ccasion of his 60th {B}irthday},
  editor = {Comon{-}Lundh, Hubert and Kirchner, Claude and Kirchner,
                  H{\'e}l{\`e}ne},
  author = {Bursuc, Sergiu and Comon{-}Lundh, Hubert and Delaune,
                  St{\'e}phanie},
  title = {Deducibility Constraints, Equational Theory and Electronic Money},
  pages = {196-212},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCD-jpj07.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCD-jpj07.ps},
  doi = {10.1007/978-3-540-73147-4_10},
  abstract = {The starting point of this work is a case study (from France
    T\'el\'ecom) of an electronic purse protocol. The~goal was to prove that
    the protocol is secure or that there is an attack. Modeling the protocol
    requires algebraic properties of a fragment of arithmetic, typically
    containing modular exponentiation. The~usual equational theories described
    in papers on security protocols are too weak: the~protocol cannot even be
    executed in these models. We~consider here an equational theory which is
    powerful enough for the protocol to be executed, and for which unification
    is still decidable.\par
    Our main result is the decidability of the so-called intruder deduction
    problem, i.e.,~security in presence of a passive attacker, taking the
    algebraic properties into account. Our~equational theory is a combination
    of several equational theories over non-disjoint signatures.}
}
@proceedings{CLKK-jouannaud07,
  editor = {Comon{-}Lundh, Hubert and Kirchner, Claude and Kirchner,
                  H{\'e}l{\`e}ne},
  booktitle = {Rewriting, Computation and Proof~--- Essays Dedicated to
                  Jean-Pierre Jouannaud on the Occasion of his 60th Birthday},
  title = {Rewriting, Computation and Proof~--- Essays Dedicated to
                  Jean-Pierre Jouannaud on the Occasion of his 60th Birthday},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = 4600,
  year = 2007,
  month = jun,
  address = {Cachan, France},
  url = {http://www.springerlink.com/content/p0p40764x486/},
  doi = {10.1007/978-3-540-73147-4},
  isbn = {978-3-540-73146-7}
}
@phdthesis{chevalier-these2007,
  author = {Chevalier, Fabrice},
  title = {Logiques pour les syst{\`e}mes temporis{\'e}s~: contr{\^o}le et expressivit{\'e}},
  year = 2007,
  month = jun,
  type = {Th{\`e}se de doctorat},
  school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-FC07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-FC07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/these-FC07.ps}
}
@phdthesis{reynier-these2007,
  author = {Reynier, Pierre-Alain},
  title = {V{\'e}rification de syst{\`e}mes temporis{\'e}s et
                  distribu{\'e}s~: mod{\`e}les, algorithmes et impl{\'e}mentabilit{\'e}},
  year = 2007,
  month = jun,
  type = {Th{\`e}se de doctorat},
  school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-reynier.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-reynier.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/these-reynier.ps}
}
@phdthesis{demri-hab2007,
  author = {Demri, St{\'e}phane},
  title = {Logiques pour la sp{\'e}cification et v{\'e}rification},
  year = 2007,
  month = jun,
  type = {M{\'e}moire d'habilitation},
  school = {Universit{\'e} Paris~7, Paris, France},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SD-habil07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SD-habil07.pdf},
  futureslides = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/SLIDES/
                SD-habil-slides.ps.gz}
}
@phdthesis{encrenaz-hab2007,
  author = {Encrenaz{-}Tiph{\`e}ne, Emmanuelle},
  title = {Contributions pour la conception et la v{\'e}rification de
		syst{\`e}mes mat{\'e}riels embarqu{\'e}s},
  year = 2007,
  month = jun,
  type = {M{\'e}moire d'habilitation},
  school = {Universit{\'e} Paris~6, Paris, France},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EE-habil07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EE-habil07.pdf},
  futureslides = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/SLIDES/
                EE-habil-slides.ps.gz}
}
@techreport{LSV:07:21,
  author = {Chamseddine, Najla and Duflot, Marie and Fribourg, Laurent and Picaronny, Claudine},
  title = {Determinate Probabilistic Timed Automata as {M}arkov Chains with
                  Parametric Costs},
  institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  year = 2007,
  month = may,
  type = {Research Report},
  number = {LSV-07-21},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-21.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-21.pdf},
  note = {17~pages},
  abstract = {We consider probabilistic systems modeled under the form of a
    special class of probabilistic timed automata. Such automata have {"}no
    choice{"}: when the automaton arrives at a node, the time at which it will
    leave it is determined; and when the automaton leaves the node, there is
    just one distribution of target nodes.\par
    In the paper, we give a method for computing the expected time~\(A\) for
    the automaton to reach an {"}absorbing{"} node. Roughly speaking, the
    method consists in putting the automaton under the form of a Markov chain
    with costs (corresponding to durations). Under certain conditions, the
    method is parametric in the sense that \(A\)~is computed as a function of
    the constants appearing in the outgoing conditions and the invariants of
    nodes, but does not assume known their explicit values.\par
    We illustrate the method on the CSMA/CD protocol.}
}
@techreport{LSV:07:20,
  author = {Bresciani, Riccardo},
  title = {The {ZRTP} Protocol~--- Security Considerations},
  institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  year = 2007,
  month = may,
  type = {Research Report},
  number = {LSV-07-20},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-20.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-20.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
        rr-lsv-2007-20.ps},
  note = {23~pages},
  abstract = {ZRTP is draft of key agreement protocol by Phil~Zimmermann,
    which relies on a Diffie-Hellman exchange to generate SRTP session
    parameters, providing confidentiality and protecting against
    \emph{Man-in-the-Middle} attacks even without a public key infrastructure or
    endpoint certificates. This is an analysis of the protocol performed with
    AVISPA and ProVerif, which tests security properties of ZRTP; in~order to
    perform the analysis, the protocol has been modeled in HLPSL (for~AVISPA)
    and in the applied \(\pi\)-calculus (for~Proverif). An improvement to gather
    some extra resistance against \emph{Man-in-the-Middle} attacks is also proposed.}
}
@inproceedings{AMN-concur07,
  address = {Lisbon, Portugal},
  month = sep,
  year = 2007,
  volume = 4703,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Caires, Lu{\'\i}s and Vasconcelos, Vasco T.},
  acronym = {{CONCUR}'07},
  booktitle = {{P}roceedings of the 18th 
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'07)},
  author = {Akshay, S. and Mukund, Madhavan and Narayan Kumar, K.},
  title = {Checking Coverage for Infinite Collections of Timed Scenarios},
  pages = {181-196},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AMN-concur07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AMN-concur07.pdf},
  doi = {	10.1007/978-3-540-74407-8_13},
  abstract = {We consider message sequence charts enriched with timing
    constraints between pairs of events. As in the untimed setting, an
    infinite family of time-constrained message sequence charts~(TC-MSCs) is
    generated using an HMSC ---a finite-state automaton whose nodes are
    labelled by TC-MSCs. A~timed MSC is an MSC in which each event is assigned
    an explicit time-stamp. A~timed MSC covers a TC-MSC if it satisfies all
    the time constraints of the~TC-MSC. A~natural recognizer for timed MSCs is
    a message-passing automaton~(MPA) augmented with clocks. The~question we
    address is the following: given a timed system specified as a
    time-constrained HMSC H and an implementation in the form of a timed
    MPA~\(A\), is~every TC-MSC generated by~\(H\) covered by some timed MSC
    recognized by~\(A\)? We~give a complete solution for locally synchronized
    time-constrained HMSCs, whose underlying behaviour is always regular.
    We~also describe a restricted solution for the general case.}
}
@inproceedings{ACD-frocos07,
  address = {Liverpool, UK},
  month = sep,
  year = 2007,
  volume = 4720,
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer},
  editor = {Wolter, Franck},
  acronym = {{FroCoS}'07},
  booktitle = {{P}roceedings of the 6th {I}nternational {S}ymposium on {F}rontiers of
                  {C}ombining {S}ystems ({FroCoS}'07)},
  author = {Arnaud, Mathilde and Cortier, V{\'e}ronique and Delaune,
                  St{\'e}phanie},
  title = {Combining algorithms for deciding knowledge in security
                  protocols},
  pages = {103-117},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACD-frocos07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACD-frocos07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ACD-frocos07.ps},
  doi = {10.1007/978-3-540-74621-8_7},
  abstract = {In formal approaches, messages sent over a network are
                  usually modeled by terms together with an equational theory,
                  axiomatizing the properties of the cryptographic functions
                  (encryption, exclusive or,~...). The analysis of
                  cryptographic protocols requires a precise understanding of
                  the attacker knowledge. Two standard notions are usually
                  used: deducibility and indistinguishability. Those notions
                  are well-studied and a lot of decidability results already
                  exist to deal with a variety of equational theories.\par
                  We~show that decidability results can be easily combined for
                  any disjoint equational theories: if the deducibility and
                  indistinguishability relations are decidable for two
                  disjoint theories, they are also decidable for their union.
                  As~an application, new decidability results can be obtained
                  using this combination theorem.}
}
@inproceedings{KM-esorics07,
  address = {Dresden, Germany},
  month = sep,
  year = 2007,
  volume = 4734,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Biskup, Joachim and Lopez, Javier},
  acronym = {{ESORICS}'07},
  booktitle = {{P}roceedings of the 12th {E}uropean {S}ymposium on
		{R}esearch in {C}omputer {S}ecurity ({ESORICS}'07)},
  author = {Kremer, Steve and Mazar{\'e}, Laurent},
  title = {Adaptive Soundness of Static Equivalence},
  pages = {610-625},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KM-esorics07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KM-esorics07.pdf},
  doi = {10.1007/978-3-540-74835-9_40},
  abstract = {We define a framework to reason about implementations of 
   equational theories in the presence of an adaptive adversary. We 
   particularly focus on soundess of static equivalence. We illustrate our 
   framework on several equational theories: symmetric encryption, XOR, 
   modular exponentiation and also joint theories of encryption and modular 
   exponentiation. This last example relies on a combination result for 
   reusing proofs for the separate theories. Finally, we~define a model for 
   symbolic analysis of dynamic group key exchange protocols, and show its 
   computational soundness.}
}
@inproceedings{BLMO-concur07,
  address = {Lisbon, Portugal},
  month = sep,
  year = 2007,
  volume = 4703,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Caires, Lu{\'\i}s and Vasconcelos, Vasco T.},
  acronym = {{CONCUR}'07},
  booktitle = {{P}roceedings of the 18th 
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'07)},
  author = {Brihaye, {\relax Th}omas and Laroussinie, Fran{\c{c}}ois and
		 Markey, Nicolas and Oreiby, Ghassan},
  title = {Timed Concurrent Game Structures},
  pages = {445-459},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLMO-concur07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLMO-concur07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BLMO-concur07.ps},
  doi = {10.1007/978-3-540-74407-8_30},
  abstract = {We propose a new model for timed games, based on concurrent game
    structures~(CGSs). Compared to the classical \emph{timed game automata}
    of~Asarin \emph{et~al.}, our timed~CGSs are {"}more concurrent{"}, in the
    sense that they always allow all the agents to act on the system,
    independently of the delay they want to elapse before their action. Timed
    CGSs weaken the {"}element of surprise{"} of timed game automata reported
    by de~Alfaro \emph{et~al.}\par
    We prove that our model has nice properties, in particular that
    model-checking timed CGSs against timed \(\textsf{ATL}\) is decidable
    \emph{via} region abstraction, and in particular that strategies are
    {"}region-stable{"} if winning objectives are. We also propose a new
    extension of \(\textsf{TATL}\), containing~\(\textsf{ATL}^{*}\), which we
    call~\(\textsf{TALTL}\). We~prove that model-checking this logic remains
    decidable on timed CGSs. Last, we explain how our algorithms can be
    adapted in order to rule out Zeno (co-)strategies, based on the ideas of
    Henzinger \emph{et~al.}}
}
@inproceedings{Gou-csl07,
  address = {Lausanne, Switzerland},
  month = sep,
  year = 2007,
  volume = 4646,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Duparc, Jacques and Henzinger, {\relax Th}omas A.},
  acronym = {{CSL}'07},
  booktitle = {{P}roceedings of the 16th {A}nnual {EACSL} {C}onference on
                  {C}omputer {S}cience {L}ogic ({CSL}'07)},
  author = {Goubault{-}Larrecq, Jean},
  title = {Continuous Previsions},
  pages = {542-557},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-csl07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-csl07.pdf},
  doi = {10.1007/978-3-540-74915-8_40},
  abstract = {We define strong monads of continuous (lower, upper) previsions,
    and of forks, modeling both probabilistic and non-deterministic choice.
    This is an elegant alternative to recent proposals by Mislove, Tix,
    Keimel, and Plotkin. We show that our monads are sound and complete, in
    the sense that they model exactly the interaction between probabilistic
    and (demonic, angelic, chaotic) choice.}
}
@article{bozzelli-tcs07,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Bozzelli, Laura},
  title = {Complexity results on branching-time pushdown model checking},
  year = 2007,
  volume = 379,
  number = {1-2},
  pages = {286-297},
  month = jun,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bozzelli-tcs07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bozzelli-tcs07.pdf},
  doi = {10.1016/j.tcs.2007.03.049},
  abstract = {The model checking problem of pushdown systems (PMC~problem,
    for~short) against standard branching temporal logics has been intensively
    studied in the literature. In particular, for the modal \(\mu\)-calculus,
    the most powerful branching temporal logic used for verification, the
    problem is known to be EXPTIME-complete (even~for a fixed~formula).
    The~problem remains EXPTIME-complete also for the logic~CTL, which
    corresponds to a fragment of the alternation-free modal \(\mu\)-calculus.
    For~the logic~CTL\(^{*}\), the problem is known to be in 2EXPTIME. In~this
    paper, we~show that the complexity of the PMC problem for CTL\(^{\*}\) is
    in fact 2EXPTIME-complete. Moreover, we give a new optimal algorithm to
    solve this problem based on automata theoretic techniques. Finally, we
    prove that the program complexity of the PMC problem against CTL
    (i.e.,~the complexity of the problem in terms of the size of the~system)
    is EXPTIME-complete.}
}
@inproceedings{BGMN-fct07,
  address = {Budapest, Hungary},
  month = aug,
  year = 2007,
  volume = 4639,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Csuhaj-Varj{\'u}, Erzs{\'e}bet and {\'E}sik, Zolt{\'a}n},
  acronym = {{FCT}'07},
  booktitle = {{P}roceedings of the 16th {I}nternational {S}ymposium
	  on {F}undamentals of {C}omputation {T}heory
	  ({FCT}'07)},
  author = {Bhateja, Puneet and Gastin, Paul and Mukund, Madhavan and Narayan
                  Kumar, K.},
  title = {Local testing of message sequence charts is difficult},
  pages = {76-87},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGMN-fct07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGMN-fct07.pdf},
  doi = {10.1007/978-3-540-74240-1_8},
  abstract = {Message sequence charts are an attractive visual formalism used
    to specify distributed communicating systems. One~way to test such a
    system is to substitute a component by a test process and observe its
    interaction with the rest of the system. We~study the question of whether
    we can characterize the distributed behaviour of the system based on such
    local observations. The~main difficulty is that local observations can
    combine in unexpected ways to define implied scenarios not present in the
    original specification. It~is known that checking whether a scenario
    specification is closed with respect to implied scenarios is undecidable
    when observations are made one process at a time, even for regular
    specifications. We~show that this undecidability holds even if we have
    only two processes in the system. We then strengthen the observer to be
    able to observe multiple processes simultaneously. Even in this stronger
    framework, the problem remains undecidable. In~fact, undecidability
    continues to hold even without message labels, provided we observe two or
    more processes simultaneously. On~the other hand, if we do not have
    message labels and we restrict observations to one process at a time, the
    problem of checking for implied scenarios is decidable.}
}
@inproceedings{GM-spin07,
  address = {Berlin, Germany},
  month = jul,
  year = 2007,
  volume = 4595,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Bo{\v{s}}nacki, Dragan and Edelkamp, Stefan},
  acronym = {{SPIN}'07},
  booktitle = {{P}roceedings of the 14th {I}nternational
               {SPIN} {W}orkshop on {M}odel {C}hecking {S}oftware
               ({SPIN}'07)},
  author = {Gastin, Paul and Moro, Pierre},
  title = {Minimal counter-example generation for {SPIN}},
  pages = {24-38},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GM-spin07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GM-spin07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GM-spin07.ps},
  doi = {10.1007/978-3-540-73370-6_4},
  abstract = {In this paper, we propose an algorithm to compute a counter-example of
  minimal size to some property in a finite state program, using the same
  programmation constraints than~SPIN. This algorithm uses nested
  Breadth-first searches guided by priority queues.
  This algorithm works in quadratic time and is linear in memory.}
}
@article{GK-fi07,
  publisher = {{IOS} Press},
  journal = {Fundamenta Informaticae},
  author = {Gastin, Paul and Kuske, Dietrich},
  title = {Uniform satisfiability in {PSPACE} for local temporal logics
	  over {M}azurkiewicz traces},
  volume = 80,
  number = {1-3},
  pages = {169-197},
  year = 2007,
  month = nov,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GK-fi07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GK-fi07.pdf},
  abstract = {We study the complexity of temporal logics over
  concurrent systems that can be described by Mazurkiewicz traces. We
  develop a general method to prove that the uniform satisfiability
  problem of local temporal logics is in~PSPACE. We~also
  demonstrate that this method applies to all known local temporal
  logics.}
}
@techreport{DGA:rap3,
  author = {Lafourcade, Pascal},
  title = {Rapport final d'activit{\'e} {\`a}~{\(11\)}~mois, contrat~{CNRS/DGA} 
         r{\'e}f{\'e}rence~: 06~60~019~00~470~75~01
         <<~{U}tilisation et exploitation des th{\'e}ories {\'e}quationnelles 
	    dans l'analyse des protocoles cryptographiques~>>},
  type = {Contract Report},
  institution = {DGA},
  year = {2007},
  month = oct,
  note = {6~pages},
  url = {http://www.lsv.ens-cachan.fr/Publis/PS/DGA-rap3.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PS/DGA-rap3.ps}
}
@techreport{DGA:rap2,
  author = {Lafourcade, Pascal},
  title = {Rapport d'activit{\'e}s {\`a}~{\(6\)}~mois, contrat~{CNRS/DGA} 
         r{\'e}f{\'e}rence~: 06~60~019~00~470~75~01
         <<~{U}tilisation et exploitation des th{\'e}ories {\'e}quationnelles 
	    dans l'analyse des protocoles cryptographiques~>>},
  type = {Contract Report},
  institution = {DGA},
  year = {2007},
  month = apr,
  note = {5~pages},
  url = {http://www.lsv.ens-cachan.fr/Publis/PS/DGA-rap2.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PS/DGA-rap2.ps}
}
@techreport{DGA:rap1,
  author = {Lafourcade, Pascal},
  title = {Rapport d'activit{\'e}s {\`a}~{\(3\)}~mois, contrat~{CNRS/DGA} 
         r{\'e}f{\'e}rence~: 06~60~019~00~470~75~01
         <<~{U}tilisation et exploitation des th{\'e}ories {\'e}quationnelles 
	    dans l'analyse des protocoles cryptographiques~>>},
  type = {Contract Report},
  institution = {DGA},
  year = {2007},
  month = jan,
  note = {3~pages},
  url = {http://www.lsv.ens-cachan.fr/Publis/PS/DGA-rap1.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PS/DGA-rap1.ps}
}
@inproceedings{DG-time07,
  address = {Alicante, Spain},
  month = jun,
  year = 2007,
  publisher = {{IEEE} Computer Society Press},
  editor = {Goranko, Valentin and Wang, X. Sean},
  acronym = {{TIME}'07},
  booktitle = {{P}roceedings of the 14th {I}nternational {S}ymposium on 
	       {T}emporal {R}epresentation and {R}easoning
	       ({TIME}'07)},
  author = {Demri, St{\'e}phane and Gascon, R{\'e}gis},
  title = {The Effects of Bounding Syntactic Resources on {P}resburger
		  {LTL} (Extended Abstract)},
  pages = {94-104},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-time07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-time07.pdf},
  doi = {10.1109/TIME.2007.63},
  abstract = {We study decidability and complexity issues for fragments of LTL
    with Presburger constraints by restricting the syntactic resources of the
    formulae (the~class of constraints, the number of variables and the
    distance between two states for which counters can be compared) while
    preserving the strength of the logical operators. We provide a complete
    picture refining known results from the literature, in some cases pushing
    forward the known decidability limits. By~way of example, we show that
    model-checking formulae from LTL with quantifier-free Presburger
    arithmetic over one-counter automata is only PSPACE-complete. In~order to
    establish the PSPACE upper bound, we show that the nonemptiness problem
    for Buchi one-counter automata taking values in~\(\mathbb{Z}\) and
    allowing zero tests and sign tests, is only NLOGSPACE-complete.}
}
@article{BGP-fmsd07,
  publisher = {Springer},
  journal = {Formal Methods in System Design},
  author = {B{\'e}rard, B{\'e}atrice and Gastin, Paul and Petit,
                  Antoine},
  title = {Timed substitutions for regular signal-event languages},
  volume = 31,
  number = 2,
  pages = {101-134},
  year = 2007,
  month = oct,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGP-fmsd07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGP-fmsd07.pdf},
  doi = {10.1007/s10703-007-0034-5},
  abstract = {In the classical framework of formal languages, a refinement
   operation is modeled by a substitution and an abstraction by an inverse
   substitution. These mechanisms have been widely studied, because they
   describe a change in the specification level, from an abstract view to a
   more concrete one, or conversely. For timed systems, there is up to now no
   uniform notion of substitution. In~this paper, we~study timed substitutions
   in the general framework of signal-event languages, where both signals and
   events are taken into account. We prove that regular signal-event languages
   are closed under substitution and inverse substitution.\par
   To obtain these results, we use in a crucial way a {"}well known{"} result:
   regular signal-event languages are closed under intersection. In fact,
   while this result is indeed easy for languages defined by Alur and Dill's
   timed automata, it turns out that the construction is much more tricky when
   considering the most involved model of signal-event automata. We give here
   a construction working on finite and infinite signal-event words and taking
   into account signal stuttering, unobservability of zero-duration \(\tau\)-signals
   and Zeno runs. Note that if several constructions have been proposed in
   particular cases, it is the first time that a general construction is
   provided.}
}
@inproceedings{JGL-icalp07,
  address = {Wroc{\l}aw, Poland},
  month = jul,
  year = 2007,
  volume = 4596,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Arge, Lars and Cachin, {\relax Ch}ristian and Jurdzi{\'n}ski, Tomasz
	 	and Tarlecki, Andrzej},
  acronym = {{ICALP}'07},
  booktitle = {{P}roceedings of the 34th {I}nternational 
               {C}olloquium on {A}utomata, {L}anguages and 
               {P}rogramming ({ICALP}'07)},
  author = {Goubault{-}Larrecq, Jean},
  title = {Continuous Capacities on Continuous State Spaces},
  pages = {764-776},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-icalp07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-icalp07.pdf},
  doi = {10.1007/978-3-540-73420-8_66},
  abstract = {We propose axiomatizing some stochastic games, in a
    continuous state
    space setting, using continuous belief functions, resp.
    plausibilities, instead of measures.  Then, stochastic games are
    just variations on continuous Markov chains.  We argue that drawing
    at random along a belief function is the same as letting the
    probabilistic player~\(P\) play first, then letting the
    non-deterministic player~\(C\) play demonically.  The same
    holds for an angelic~\(C\), using plausibilities instead.
    We then define a simple modal logic, and characterize simulation in
    terms of formulae of this logic.  Finally, we show that (discounted)
    payoffs are defined and unique, where in the demonic case, 
    \(P\)~maximizes payoff, while \(C\)~minimizes it}
}
@inproceedings{BHPR-icalp07,
  address = {Wroc{\l}aw, Poland},
  month = jul,
  year = 2007,
  volume = 4596,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Arge, Lars and Cachin, {\relax Ch}ristian and Jurdzi{\'n}ski, Tomasz
	 	and Tarlecki, Andrzej},
  acronym = {{ICALP}'07},
  booktitle = {{P}roceedings of the 34th {I}nternational 
               {C}olloquium on {A}utomata, {L}anguages and 
               {P}rogramming ({ICALP}'07)},
  author = {Brihaye, {\relax Th}omas and Henzinger, {\relax Th}omas A. and
                  Prabhu, Vinayak and Raskin, Jean-Fran{\c{c}}ois},
  title = {Minimum-Time Reachability in Timed Games},
  pages = {825-837},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHPR-icalp07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHPR-icalp07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BHPR-icalp07.ps},
  doi = {10.1007/978-3-540-73420-8_71},
  abstract = {We consider the minimum-time reachability problem in concurrent
    two-player timed automaton game structures. We~show how to compute the
    minimum time needed by a player to reach a location against all possible
    choices of the opponent. We~do not put any syntactic restriction on the
    game structure, nor do we require any player to guarantee time divergence.
    We~only require players to use physically realizable strategies.
    The~minimal time is computed in part using a fixpoint expression which we
    show can be used on equivalence classes of a non-trivial extension of the
    region equivalence relation.}
}
@inproceedings{CDS-csf07,
  address = {Venice, Italy},
  month = jul,
  year = 2007,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{CSF}'07},
  booktitle = {{P}roceedings of the 
               20th {IEEE} {C}omputer {S}ecurity {F}oundations
               {S}ymposium ({CSF}'07)},
  author = {Cortier, V{\'e}ronique and Delaune, St{\'e}phanie and Steel, Graham},
  title = {A Formal Theory of Key Conjuring},
  pages = {79-93},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDS-csf07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDS-csf07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CDS-csf07.ps},
  doi = {10.1109/CSF.2007.5},
  abstract = {We describe a formalism for \emph{key conjuring}, the process by
    which an attacker obtains an unknown, encrypted key by repeatedly calling
    a cryptographic API function with random values in place of keys. This
    technique has been used to attack the security APIs of several Hardware
    Security Modules~(HSMs), which are widely deployed in the ATM (cash
    machine) network. We~propose a formalism for detecting computationally
    feasible key conjuring operations, incorporated into a Dolev-Yao style
    model of the security~API. We~show that security in the presence of key
    conjuring operations is decidable for a particular class of~APIs, which
    includes the key management~API of IBM's Common Cryptographic
    Architecture~(CCA).}
}
@inproceedings{Gou-lics07,
  address = {Wroc{\l}aw, Poland},
  month = jul,
  year = 2007,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{LICS}'07},
  booktitle = {{P}roceedings of the 22nd
               {A}nnual {IEEE} {S}ymposium on
               {L}ogic in {C}omputer {S}cience
               ({LICS}'07)},
  author = {Goubault{-}Larrecq, Jean},
  title = {On {N}oetherian Spaces},
  pages = {453-462},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-lics07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-lics07.pdf},
  doi = {10.1109/LICS.2007.34},
  abstract = {A topological space is Noetherian iff every open is compact.
  Our~starting point is that this notion generalizes that of
  well-quasi order, in the sense that an Alexandroff-discrete space is
  Noetherian iff its specialization quasi-ordering is well.  For~more
  general spaces, this opens the way to verifying infinite transition
  systems based on non-well quasi ordered sets, but where the preimage
  operator satisfies an additional continuity assumption.  The
  technical development rests heavily on techniques arising from
  topology and domain theory, including sobriety and the de Groot dual
  of a stably compact space.  We~show that the category Nthr of
  Noetherian spaces is finitely complete and finitely cocomplete.
  Finally, we note that if \(X\)~is a Noetherian space, then the set of
  all (even infinite) subsets of~\(X\) is again Noetherian, a~result
  that fails for well-quasi orders.}
}
@inproceedings{BMOW-lics07,
  address = {Wroc{\l}aw, Poland},
  month = jul,
  year = 2007,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{LICS}'07},
  booktitle = {{P}roceedings of the 22nd
               {A}nnual {IEEE} {S}ymposium on
               {L}ogic in {C}omputer {S}cience
               ({LICS}'07)},
  author = {Bouyer, Patricia and Markey, Nicolas and Ouaknine, Jo{\"e}l and
	    Worrell, James},
  title = {The Cost of Punctuality},
  pages = {109-118},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMOW-lics07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMOW-lics07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BMOW-lics07.ps},
  doi = {10.1109/LICS.2007.49},
  abstract = {In an influential paper titled {"}The Benefits of
      Relaxing Punctuality{"}, Alur, Feder, and~Henzinger introduced
      Metric Interval Temporal Logic~(MITL) as a fragment of the real-time
      logic Metric Temporal Logic~(MTL) in which exact or punctual timing
      constraints are banned. Their main result showed that model checking and
      satisfiability for~MITL are both EXPSPACE-Complete.\par
      Until recently, it was widely believed that admitting even the simplest
      punctual specifications in any linear-time temporal logic would
      automatically lead to undecidability. Although this was recently
      disproved, until now no punctual fragment of~MTL was known to have even
      primitive recursive complexity (with certain decidable fragments having
      provably non-primitive recursive complexity).\par
      In this paper we identify a `co-flat' subset of~MTL that is capable of
      expressing a large class of punctual specifications and for which model
      checking (although not satisfiability) has no complexity cost over~MITL.
      Our logic is moreover qualitatively different from~MITL in that it can
      express properties that are not timed-regular. Correspondingly, our
      decision procedures do not involve translating formulas into
      finite-state automata, but rather into certain kinds of reversal-bounded
      Turing machines. Using this translation we show that the model checking
      problem for our logic is EXPSPACE-Complete, and is even PSPACE-Complete
      if timing constraints are encoded in unary.}
}
@inproceedings{BDL-hav07,
  address = {Braga, Portugal},
  month = mar,
  year = 2007,
  editor = {Berdine, Josh and Sagiv, Mooly},
  acronym = {{HAV}'07},
  booktitle = {{P}roceedings of the 1st {W}orkshop on {H}eap {A}nalysis and 
		{V}erification ({HAV}'07)},
  author = {Brochenin, R{\'e}mi and Demri, St{\'e}phane and Lozes, {\'E}tienne},
  title = {Reasoning about Sequences of Memory States},
  preliminary-version-of = {BDL-lfcs2007},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDL-hav07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDL-hav07.pdf},
  abstract = {In order to verify programs with pointer variables, 
    we introduce a temporal logic LTL\textsuperscript{mem} whose 
    underlying 
    assertion language is the 
    quantifier-free fragment of separation logic and the temporal logic on 
    the 
    top of it is  the standard linear-time temporal logic~LTL. We~state 
    the 
    complexity of various model-checking and satisfiability problems for 
    LTL\textsuperscript{mem} , considering various  
    fragments of separation logic (including pointer arithmetic), various 
    classes of models (with or without constant heap), and the influence  
    of fixing the initial memory state.
    Our main decidability result is PSPACE-completeness of the 
    satisfiability problems on the record fragment and on a classical 
    fragment allowing pointer arithmetic. 
    \(\Sigma^{0}_{1}\)-completeness or \(\Sigma^{1}_{1}\)-completeness 
    results 
    are established for various problems, and underline the tightness of 
    our decidability results.}
}
@techreport{LSV:07:10,
  author = {Bouhoula, Adel and Jacquemard, Florent},
  title = {Tree Automata, Implicit Induction and Explicit Destructors for 
	    Security Protocol Verification},
  institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  year = 2007,
  month = feb,
  type = {Research Report},
  number = {LSV-07-10},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-10.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-10.pdf},
  note = {21~pages},
  abstract = {We present a new method for automatic implicit induction theorem
    proving, and its application for the verification of cryptographic
    protocols. The~method is based on constrained tree grammars and handles
    non-confluent rewrite systems which are required in the context of the
    verification of security protocols because of the non-deterministic
    behavior of attackers. It~also handles axioms between constructor terms
    which allows us to specify explicit destructors representing cryptographic
    operators. Constrained tree grammars are used in our procedure both as
    induction schemes and as oracles for checking validity and redundancy by
    reduction to an emptiness problem. They also permit to characterize
    security failure of cryptographic protocols as sets of execution traces
    corresponding to an attack. This~way, we obtain a generic framework for
    the verification of protocols, in~which we can verify reachability
    properties like confidentiality, but also more complex properties like
    authentication. We present three case studies which gave very promising
    results.}
}
@techreport{KL-eth07,
  author = {Ksi{\k e}{\. z}opolski, Bogdan and Lafourcade, Pascal},
  title = {Attack and Revison of an Electronic Auction Protocol using~{OFMC}},
  institution = {Department of Computer Science, ETH Zurich, Switzerland},
  year = 2007,
  month = feb,
  type = {Technical Report},
  number = {549},
  note = {13~pages},
  nmnote = {on peut pas dire que ce soit un papier du labo... Si en fait,
                  car Pascal etait la-bas sur un contrat gere par le LSV},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KL-eth549.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KL-eth549.pdf},
  abstract = {In the article we show an attack on the cryptographic protocol
                  of electronic auction with extended requirements
                  [Ksiezopolski and Kotulski, \textit{Cryptographic protocol
                  for electronic auctions with extended requirements},~2004].
                  The found attack consists of authentication breach and
                  secret retrieval. It~is a kind of {"}man-in-the-middle
                  attack{"}. The intruder impersonates an agent and learns some
                  secret information. We have discovered this flaw unsing OFMC
                  an automatic tool of cryptographic protocol verification.
                  After a description of this attack, we propose a new version
                  of the e-auction protocol. We also check with OFMC the
                  secrecy for the new protocol and give an informal proof of
                  the other properties that this new e-auction protocol has to
                  guarantee.}
}
@inproceedings{Maz-wits07,
  address = {Braga, Portugal},
  month = mar,
  year = 2007,
  editor = {Focardi, Riccardo},
  acronym = {{WITS}'07},
  booktitle = {{P}reliminary {P}roceedings of the 7th {I}nternational {W}orkshop 
           on {I}ssues in the {T}heory of {S}ecurity ({WITS}'07)},
  author = {Mazar{\'e}, Laurent},
  title = {Computationally Sound Analysis of Protocols using Bilinear Pairings},
  pages = {6-21},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Maz-wits07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Maz-wits07.pdf},
  abstract = {In this paper, we introduce a symbolic model to analyse
    protocols that use a bilinear pairing between two cyclic groups. This
    model consists in an extension of the Abadi-Rogaway logic and we prove
    that the logic is still computationally sound: symbolic
    indistinguishability implies computational indistinguishability provided
    that the Bilinear Decisional Diffie-Hellman assumption is verified and
    that the encryption scheme is IND-CPA secure. We~illustrate our results on
    classical protocols using bilinear pairing like Joux tripartite
    Diffie-Hellman protocol or the TAK-2 and TAK-3 protocols.}
}
@inproceedings{BDL-lfcs2007,
  address = {New~York, New~York, USA},
  month = jun,
  year = 2007,
  volume = 4514,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Artemov, Sergei N. and Nerode, Anil},
  acronym = {{LFCS}'07},
  booktitle = {{P}roceedings of the {S}ymposium on {L}ogical {F}oundations of
	{C}omputer {S}cience ({LFCS}'07)},
  author = {Brochenin, R{\'e}mi and Demri, St{\'e}phane and Lozes, {\'E}tienne},
  title = {Reasoning about sequences of memory states},
  pages = {100-114},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDL-lfcs07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDL-lfcs07.pdf},
  doi = {	10.1007/978-3-540-72734-7_8},
  abstract = {Motivated by the verification of programs with pointer
    variables, we introduce a temporal logic LTL\textsuperscript{mem} whose
    underlying assertion language is the quantifier-free fragment of
    separation logic and the temporal logic on the top of it is the standard
    linear-time temporal logic~LTL. We analyze the complexity of various
    model-checking and satisfiability problems for LTL\textsuperscript{mem},
    considering various fragments of separation logic (including pointer
    arithmetic), various classes of models (with or without constant heap),
    and the influence of fixing the initial memory state. We~provide a
    complete picture based on these criteria. Our main decidability result is
    PSPACE-completeness of the satisfiability problems on the record fragment
    and on a classical fragment allowing pointer arithmetic. 
    \(\Sigma^{0}_{1}\)-completeness or \(\Sigma^{1}_{1}\)-completeness
    results are established for various problems by reducing standard problems
    for Minsky machines, and underline the tightness of our decidability
    results.}
}
@inproceedings{BK-lata2007,
  address = {Tarragona, Spain},
  month = mar # {-} # apr,
  year = 2007,
  futureseries = {Lecture Notes in Computer Science},
  nmnote = {published as Report 35/07 Research Group on Mathematical
                  Linguistics, Universitat Rovira i Virgili, Tarragona},
  editor = {{\'E}sik, Zolt{\'a}n and Mart{\'\i}n-Vide, Carlos and 
                  Mitrana, Victor},
  acronym = {{LATA}'07},
  booktitle = {{P}reliminary {P}roceedings of the 1st {I}nternational {C}onference on {L}anguage 
	    and {A}utomata {T}heory and {A}pplications ({LATA}'07)},
  author = {Bollig, Benedikt and Kuske, Dietrich},
  title = {{M}uller Message-Passing Automata and Logics},
  nopages = {},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BK-lata07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BK-lata07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BK-lata07.ps},
  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. Our
    result is based on a new extension of the classical Ehrenfeucht-Fra{\"\i}ss{\'e}
    game to cope with infinite structures and the new first-order quantifier.}
}
@techreport{LSV:07:03,
  author = {Goubault{-}Larrecq, Jean},
  title = {Believe It Or Not, {GOI}~is a Model of Classical Linear Logic},
  institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  year = 2007,
  month = jan,
  type = {Research Report},
  number = {LSV-07-03},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-03.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-03.pdf},
  note = {18~pages},
  othernote = {a draft of the longer version of this report is available at 
          http://www.lsv.ens-cachan.fr/~goubault/isg.pdf},
  abstract = {We introduce the Danos-R\'egnier category \(\mathcal{DR}(M)\) of a linear
  inverse monoid~\(M\), a categorical description of geometries of
  interaction~(GOI).  The usual setting for GOI is that of a weakly
  Cantorian linear inverse monoid.  It is well-known that GOI is
  perfectly suited to describe the multiplicative fragment of linear
  logic, and indeed \(\mathcal{DR}(M)\) will be a \(*\)-autonomous category in this
  case.  It is also well-known that the categorical interpretation of
  the other linear connectives conflicts with GOI interpretations.  We
  make this precise, and show that \(\mathcal{DR}(M)\) has no terminal object, no
  cartesian product, and no exponential---whatever \(M\) is, unless \(M\)
  is trivial.  However, a form of coherence completion of~\(\mathcal{DR}(M)\) \`a
  la Hu-Joyal provides a model of full classical linear logic, as soon
  as \(M\) is weakly Cantorian.}
}
@article{LS-ipl07,
  publisher = {Elsevier Science Publishers},
  journal = {Information Processing Letters},
  author = {Laroussinie, Fran{\c{c}}ois and Sproston, Jeremy},
  title = {State Explosion in Almost-Sure Probabilistic Reachability},
  year = 2007,
  volume = {102},
  number = {6},
  pages = {236-241},
  month = jun,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LS-ipl07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LS-ipl07.pdf},
  doi = {10.1016/j.ipl.2007.01.003},
  abstract = {We show that the problem of reaching a state set with
    probability~\(1\) in probabilistic-nondeterministic systems operating in
    parallel is EXPTIME-complete. We then show that this probabilistic
    reachability problem is EXPTIME-complete also for probabilistic timed
    automata.}
}
@article{DO-fi2007,
  publisher = {{IOS} Press},
  journal = {Fundamenta Informaticae},
  author = {Demri, St{\'e}phane and Or{\l}owska, Ewa},
  title = {Relative Nondeterministic Information Logic is 
		  {EXPTIME}-complete},
  year = {2007},
  volume = {75},
  number = {1-4},
  pages = {163-178},
  nmnote = {Special issue in memory of Z.~Paw{\l}ak},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DO-fi07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DO-fi07.pdf},
  abstract = {We define a relative version of the logic NIL introduced by
                  Or{\l}owska, Paw{\l}ak and Vakarelov and we show that its
                  satisfiability is not only decidable but also
                  EXPTIME-complete. Such a logic combines two ingredients that
                  are seldom present simultaneously in information logics:
                  frame conditions involving more than one information
                  relation and relative frames. The~EXPTIME upper bound is
                  obtained by designing a well-suited decision procedure based
                  on the nonemptiness problem of B{\"u}chi automata on
                  infinite trees. The paper provides evidence that B{\"u}chi
                  automata on infinite trees are crucial language acceptors
                  even for relative information logics with multiple types of
                  relations.}
}
@techreport{LSV:07:02,
  author = {Reynier, Pierre-Alain},
  title = {Diagonal constraints handled efficiently in~{UPPAAL}},
  institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  year = 2007,
  month = jan,
  type = {Research Report},
  number = {LSV-07-02},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-02.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-02.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
	rr-lsv-2007-02.ps},
  note = {4~pages},
  abstract = {Timed automata (TA) are widely used to model real-time systems,
and UPPAAL is one of the most popular model-checker for this framework which
has been successfully applied over numerous industrial case studies. Diagonal
constraints are a natural extension of TA, that does not increase expressive
power, but gives conciseness. Unfortunately the classical forward algorithm
for reachability analysis cannot be used to deal directly with diagonal
constraints. Thus the current method implemented consists in removing them
on-the-fly, which implies a complexity blow-up. In~[P.~Bouyer, F.~Laroussinie,
and P.-A.~Reynier. \textit{Diagonal constraints in timed automata: Forward analysis of
timed systems}. Proceedings of FORMATS'06, LNCS~3829, p.~112-126, Springer], a
counter-example guided refinement algorithm has been proposed. In~this paper,
we present its implementation, and give some benchmarks on a variant of
Fischer's protocol. }
}
@phdthesis{THESE-baudet07,
  author = {Baudet, Mathieu},
  title = {S{\'e}curit{\'e} des protocoles cryptographiques~: 
	 	  aspects logiques et calculatoires},
  year = 2007,
  month = jan,
  type = {Th{\`e}se de doctorat},
  school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-baudet.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-baudet.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/these-baudet.ps},
  abstract = {This thesis is dedicated to the automatic verification of
    cryptographic protocols in the logical and computational settings. \par
    The~first part concerns the security of procotols in the logical
    ({"}formal{"}) framework. To~begin with, we show how to specify various
    security properties of protocols in a concurrent language, and how to
    analyze them automatically for a bounded number of sessions.
    The~properties under consideration include notably simple secrecy,
    authentication and resistance to dictionary attacks. \par
    The~second part deals with the computational soundness of logical models.
    The~main question here is to what extent the fact that no logical attack
    exists on a protocol implies that it is provably secure in the usual
    cryptographic model (called the computational model). We~concentrate on
    static equivalence, applied notably to several kinds of encryption and
    data vulnerable to dictionary attacks (such as passwords). We~show that
    under simple conditions, any (logical) proof of static equivalence between
    two messages implies their (computational) indistinguishability. This
    entails computational soundness in the passive case for the notion of
    dictionary attacks developped in the first part.}
}
@inproceedings{BM-lfcs2007,
  address = {New~York, New~York, USA},
  month = jun,
  year = 2007,
  volume = 4514,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Artemov, Sergei N. and Nerode, Anil},
  acronym = {{LFCS}'07},
  booktitle = {{P}roceedings of the {S}ymposium on {L}ogical {F}oundations of
	{C}omputer {S}cience ({LFCS}'07)},
  author = {Bollig, Benedikt and Meinecke, Ingmar},
  title = {Weighted Distributed Systems and Their Logics},
  pages = {54-68},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BM-lfcs07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BM-lfcs07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BM-lfcs07.ps},
  doi = {10.1007/978-3-540-72734-7_5},
  abstract = {We provide a model of weighted distributed systems and give a
    logical characterization thereof. Distributed systems are represented as
    weighted asynchronous cellular automata. Running over directed acyclic
    graphs, Mazurkiewicz traces, or (lossy) message sequence charts, they
    allow for modeling several communication paradigms in a unifying
    framework, among them probabilistic shared-variable and probabilistic
    lossy-channel systems. We~show that any such system can be described by a
    weighted existential MSO formula and, vice versa, any formula gives rise
    to a weighted asynchronous cellular automaton.}
}
@inproceedings{DDG-lfcs2007,
  address = {New~York, New~York, USA},
  month = jun,
  year = 2007,
  volume = 4514,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Artemov, Sergei N. and Nerode, Anil},
  acronym = {{LFCS}'07},
  booktitle = {{P}roceedings of the {S}ymposium on {L}ogical {F}oundations of
	{C}omputer {S}cience ({LFCS}'07)},
  author = {Demri, St{\'e}phane and D'Souza, Deepak and Gascon, R{\'e}gis},
  title = {Decidable Temporal Logic with Repeating Values},
  pages = {180-194},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDG-lfcs07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDG-lfcs07.pdf},
  doi = {10.1007/978-3-540-72734-7_13},
  abstract = {Various logical formalisms with the freeze quantifier have been
    recently considered to model computer systems even though this is a
    powerful mechanism that often leads to undecidability. In~this paper, we
    study a linear-time temporal logic with past-time operators such that the
    freeze operator is only used to express that some value from an infinite
    set is repeated in the future or in the past. Such a restriction has been
    inspired by a recent work on spatio-temporal logics. We~show decidability
    of finitary and infinitary satisfiability by reduction into the
    verification of temporal properties in Petri nets. This is a surprising
    result since the logic is closed under negation, contains future-time and
    past-time temporal operators and can express the nonce property and its
    negation. These ingredients are known to lead to undecidability with a
    more liberal use of the freeze quantifier. The~paper contains also
    insights about the relationships between temporal logics with the freeze
    operator and counter automata.}
}
@inproceedings{BBC-lfcs2007,
  address = {New~York, New~York, USA},
  month = jun,
  year = 2007,
  volume = 4514,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Artemov, Sergei N. and Nerode, Anil},
  acronym = {{LFCS}'07},
  booktitle = {{P}roceedings of the {S}ymposium on {L}ogical {F}oundations of
	{C}omputer {S}cience ({LFCS}'07)},
  author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and 
		  Chevalier, Fabrice},
  title = {Weighted O-Minimal Hybrid Systems are more 
		   Decidable than Weighted Timed Automata!},
  pages = {69-83},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-lfcs07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-lfcs07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBC-lfcs07.ps},
  doi = {10.1007/978-3-540-72734-7_6},
  abstract = {We consider weighted o-minimal hybrid systems, which
extend classical o-minimal hybrid systems with cost functions. These cost
functions are {"}observer variables{"} which increase while the system evolves
but do not constrain the behaviour of the system. In this paper, we prove
two main results: (i)~optimal o-minimal hybrid games are decidable; (ii)~the
model-checking of~WCTL, an extension of CTL which can constrain the cost
variables, is decidable over that model. This has to be compared with the
same problems in the framework of timed automata where both problems are
undecidable in general, while they are decidable for the restricted class of
one-clock timed automata. }
}
@article{VG-icomp2007,
  publisher = {Elsevier Science Publishers},
  journal = {Information and Computation},
  author = {Verma, Kumar N. and Goubault{-}Larrecq, Jean},
  title = {Alternating Two-Way {AC}-Tree Automata},
  pages = {817-869},
  year = {2007},
  month = jun,
  volume = 205,
  number = 6,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/VG-icomp07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/VG-icomp07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/VG-icomp07.ps},
  doi = {10.1016/j.ic.2006.12.006},
  abstract = {We explore the notion of alternating two-way tree automata
                  modulo the theory of finitely many associative-commutative
                  (AC) symbols. This was prompted by questions arising in
                  cryptographic protocol verification, in~particular in
                  modeling group key agreement schemes based on
                  Diffie-Hellman-like functions, where the emptiness question
                  for intersections of such automata is fundamental. This also
                  has independent interest. We~show that the use of general
                  push clauses, or of alternation, leads to undecidability,
                  already in the case of one AC symbol, with only functions of
                  arity zero. On~the other hand, emptiness is decidable in the
                  general case of several function symbols, including several
                  AC symbols, provided push clauses are unconditional and
                  intersection clauses are final. This class of automata is
                  also shown to be closed under intersection.}
}
@inproceedings{JLS-tacas07,
  address = {Braga, Portugal},
  month = mar,
  year = 2007,
  volume = {4424},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Grumberg, Orna and Huth, Michael},
  acronym = {{TACAS}'07},
  booktitle = {{P}roceedings of the 13th {I}nternational 
               {C}onference on {T}ools and {A}lgorithms for
               {C}onstruction and {A}nalysis of {S}ystems
               ({TACAS}'07)},
  author = {Jurdzi{\'n}ski, Marcin and Laroussinie, Fran{\c{c}}ois and
                  Sproston, Jeremy},
  title = {Model Checking Probabilistic Timed Automata with One or Two Clocks},
  pages = {170-184},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JLS-tacas07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JLS-tacas07.pdf},
  doi = {10.1007/978-3-540-71209-1_15},
  abstract = {Probabilistic timed automata are an extension of timed automata
	with discrete probability distributions. We~consider model-checking
	algorithms for the subclasses of probabilistic timed automata which
	have one or two clocks. Firstly, we show that PCTL probabilistic
	model-checking problems (such~as determining whether a set of target
	states can be reached with probability at least~0.99 re- gardless of
	how nondeterminism is resolved) are PTIME-complete for one clock
	probabilistic timed automata, and are EXPTIME-complete for
	probabilistic timed automata with two clocks. Secondly, we show that
	the model-checking problem for the probabilistic timed temporal logic
	PTCTL is EXPTIME-complete for one clock probabilistic timed automata.
	However, the corresponding model-checking problem for the subclass of
	PTCTL which does not permit both (1)~punctual tim- ing bounds, which
	require the occurrence of an event at an exact time point, and
	(2)~comparisons with probability bounds other than 0 or~1, is
	PTIME-complete.}
}
@inproceedings{DADSS-tacas07,
  address = {Braga, Portugal},
  month = mar,
  year = 2007,
  volume = {4424},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Grumberg, Orna and Huth, Michael},
  acronym = {{TACAS}'07},
  booktitle = {{P}roceedings of the 13th {I}nternational 
               {C}onference on {T}ools and {A}lgorithms for
               {C}onstruction and {A}nalysis of {S}ystems
               ({TACAS}'07)},
  author = {D'Aprile, Davide and Donatelli, Susanna and Sangnier, 
		  Arnaud and Sproston, Jeremy},
  title = {From Time {P}etri Nets to Timed Automata: An Untimed 
		  Approach},
  pages = {216-230},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DADSS-tacas07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DADSS-tacas07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DADSS-tacas07.ps},
  doi = {10.1007/978-3-540-71209-1_18},
  abstract = {Time Petri Nets~(TPN) and Timed Automata~(TA) are widely-used
              formalisms for the modeling and analysis of timed systems. A
              recently-developed approach for the analysis of TPNs concerns
              their translation to~TAs, at which point efficient analysis
              tools for TAs can then be applied. One~feature of much of this
              previous work has been the use of timed reachability analysis on
              the TPN in order to construct the~TA. In this paper we present a
              method for the translation from TPNs to~TAs which bypasses the
              timed reachability analysis step. Instead, our method relies on
              the reachability graph of the underlying untimed Petri~net. We
              show that our approach is competitive for the translation of a
              wide class of TPNs to~TAs in comparison with previous
              approaches, both with regard to the time required to perform the
              translation, and with regard to the number of locations and
              clocks of the produced~TA.}
}
@inproceedings{BKKL-tacas07,
  address = {Braga, Portugal},
  month = mar,
  year = 2007,
  volume = {4424},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Grumberg, Orna and Huth, Michael},
  acronym = {{TACAS}'07},
  booktitle = {{P}roceedings of the 13th {I}nternational 
               {C}onference on {T}ools and {A}lgorithms for
               {C}onstruction and {A}nalysis of {S}ystems
               ({TACAS}'07)},
  author = {Bollig, Benedikt and Katoen, Joost-Pieter and Kern, Carsten
                  and Leucker, Martin},
  title = {Replaying Play in and Play out: Synthesis of Design Models
                  from Scenarios by Learning},
  pages = {435-450},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-tacas07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-tacas07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BKKL-tacas07.ps},
  doi = {10.1007/978-3-540-71209-1_33},
  abstract = {This paper is concerned with bridging the
    gap between requirements, provided
    as a set of scenarios, and conforming design models. The~novel aspect
    of our approach is to exploit learning for the synthesis of design
    models. In particular, we present a procedure that infers a
    message-passing automaton~(MPA) from a given set of positive and 
    negative scenarios of the systems behavior provided as message 
    sequence 
    charts~(MSCs). The~paper investigates which classes of regular MSC 
    languages and corresponding MPAs can (not) be learned, and presents a 
    dedicated tool based on the learning library LearnLib that supports 
    our approach.}
}
@inproceedings{CJP-fossacs07,
  address = {Braga, Portugal},
  month = mar,
  year = 2007,
  volume = 4423,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Seidl, Helmut},
  acronym = {{FoSSaCS}'07},
  booktitle = {{P}roceedings of the 10th {I}nternational
               {C}onference on {F}oundations of {S}oftware {S}cience
               and {C}omputation {S}tructures
               ({FoSSaCS}'07)},
  author = {Comon{-}Lundh, Hubert and Jacquemard, Florent and
		  Perrin, Nicolas},
  title = {Tree Automata with Memory, Visibility and Structural 
		  Constraints},
  pages = {168-182},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CJP-fossacs07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CJP-fossacs07.pdf},
  doi = {10.1007/978-3-540-71389-0_13},
  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. 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,
inclusion and universality are decidable for~VTAM. Moreover, we propose an
extension of VTAM whose transitions may be constrained by structural equality
and disequality tests between memories, and show that this extension preserves
the good closure and decidability properties. }
}
@inproceedings{LMO-fossacs07,
  address = {Braga, Portugal},
  month = mar,
  year = 2007,
  volume = 4423,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Seidl, Helmut},
  acronym = {{FoSSaCS}'07},
  booktitle = {{P}roceedings of the 10th {I}nternational
               {C}onference on {F}oundations of {S}oftware {S}cience
               and {C}omputation {S}tructures
               ({FoSSaCS}'07)},
  author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas and Oreiby, Ghassan},
  title = {On the Expressiveness and Complexity of~{ATL}},
  pages = {243-257},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMO-fossacs07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMO-fossacs07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LMO-fossacs07.ps},
  corrigendumpdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LMO-lmcs08-erratum.pdf},
  doi = {10.1007/978-3-540-71389-0_18},
  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{BLM-fossacs07,
  address = {Braga, Portugal},
  month = mar,
  year = 2007,
  volume = 4423,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Seidl, Helmut},
  acronym = {{FoSSaCS}'07},
  booktitle = {{P}roceedings of the 10th {I}nternational
               {C}onference on {F}oundations of {S}oftware {S}cience
               and {C}omputation {S}tructures
               ({FoSSaCS}'07)},
  author = {Bouyer, Patricia and Larsen, Kim G. and Markey, Nicolas},
  title = {Model-Checking One-Clock Priced Timed Automata},
  pages = {108-122},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLM-fossacs07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLM-fossacs07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BLM-fossacs07.ps},
  doi = {10.1007/978-3-540-71389-0_9},
  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. We prove that model-checking this class of models
against the logic~WCTL, CTL~with cost-constrained modalities, is
PSPACE-complete under the {"}single-clock{"} assumption. In~contrast, it~has been
recently proved that the model-checking problem is undecidable for this model
as soon as the system has three clocks. We also prove that the model-checking
of~WCTL becomes undecidable, even under this {"}single-clock{"} assumption. }
}
@article{DLN-icomp2006,
  publisher = {Elsevier Science Publishers},
  journal = {Information and Computation},
  author = {Demri, St{\'e}phane and Lazi{\'c}, Ranko and Nowak, David},
  title = {On the freeze quantifier in constraint~{LTL}: Decidability
		   and complexity},
  pages = {2-24},
  year = {2007},
  month = jan,
  volume = 205,
  number = 1,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLN-icomp06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLN-icomp06.pdf},
  doi = {10.1016/j.ic.2006.08.003},
  abstract = {Constraint LTL, a generalisation of LTL over Presburger
constraints, is often used as a formal language to specify the behavior of
operational models with constraints. The freeze quantifier can be part of the
language, as in some real-time logics, but this variable-binding mechanism is
quite general and ubiquitous in many logical languages (first-order temporal
logics, hybrid logics, logics for sequence diagrams, navigation logics, logics
with \(\lambda\)-abstraction,~etc.). We show that Constraint~LTL over the
simple domain~\(\langle\mathbb{N}, =\rangle\) augmented with the freeze
quantifier is undecidable which is a surprising result in view of the poor
language for constraints (only equality tests). Many versions of freeze-free
Constraint LTL are decidable over domains with qualitative predicates and our
undecidability result actually establishes \(\Sigma_{1}^{1}\)-completeness. On
the positive side, we provide complexity results when the domain is finite
({\scshape ExpSpace}-completeness) or when the formulae are flat in a sense
introduced in the paper. Our undecidability results are sharp
(\emph{i.e.}~with restrictions on the number of variables) and all our
complexity characterisations ensure completeness with respect to some
complexity class (mainly {\scshape PSpace} and {\scshape ExpSpace}).}
}
@article{DN-ijfcs07,
  publisher = {World Scientific},
  journal = {International Journal of Foundations of Computer Science},
  author = {Demri, St{\'e}phane and Nowak, David},
  title = {Reasoning about transfinite sequences},
  year = 2007,
  volume = {18},
  number = {1},
  pages = {87-112},
  month = feb,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DN-ijfcs07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DN-ijfcs07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DN-ijfcs07.ps},
  doi = {10.1142/S0129054107004589},
  abstract = {We introduce a family of temporal logics to specify the behavior
of systems with Zeno behaviors. We~extend linear-time temporal logic LTL to
authorize models admitting Zeno sequences of actions and quantitative temporal
operators indexed by ordinals replace the standard next-time and until
future-time operators. Our aim is to control such systems by designing
controllers that safely work on \(\omega\)-sequences but interact
synchronously with the system in order to restrict their behaviors. We show
that the satisfiability and model-checking for the logics working on
\(\omega^{k}\)-sequences is \textsc{expspace}-complete when the integers are
represented in binary, and pspace-complete with a unary representation. To do
so, we substantially extend standard results about LTL by introducing a new
class of succinct ordinal automata that can encode the interaction between the
different quantitative temporal operators. }
}
@inproceedings{BCD-stacs2007,
  address = {Aachen, Germany},
  month = feb,
  year = 2007,
  volume = 4393,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Thomas, Wolfgang and Weil, Pascal},
  acronym = {{STACS}'07},
  booktitle = {{P}roceedings of the 24th {A}nnual
               {S}ymposium on {T}heoretical {A}spects of
               {C}omputer {S}cience
               ({STACS}'07)},
  author = {Bursuc, Sergiu and Comon{-}Lundh, Hubert and Delaune,
                  St{\'e}phanie},
  title = {Associative-Commutative Deducibility Constraints},
  pages = {634-645},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCD-stacs07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCD-stacs07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCD-stacs07.ps},
  doi = {10.1007/978-3-540-70918-3_54},
  abstract = {We consider deducibility constraints, which are equivalent to
  particular Diophantine systems, arising in the automatic verification of
  security protocols, in presence of associative and commutative symbols. We
  show that deciding such Diophantine systems is, in general, undecidable. Then,
  we consider a simple subclass, which we show decidable. Though the solutions
  of these problems are not necessarily semi-linear sets, we show that there are
  (computable) semi-linear sets whose minimal solutions are not too far from the
  minimal solutions of the system. Finally, we consider a small variant of the
  problem, for which there is a much simpler decision algorithm. }
}
@article{BBBR-fmsd06,
  publisher = {Springer},
  journal = {Formal Methods in System Design},
  author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and
                 Bruy{\`e}re, V{\'e}ronique and Raskin, Jean-Fran{\c{c}}ois},
  title = {On the optimal reachability problem on weighted timed 
		automata},
  volume = 31,
  number = 2,
  year = 2007,
  month = oct,
  pages = {135-175},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBR-FMSD06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBR-FMSD06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBBR-FMSD06.ps},
  doi = {10.1007/s10703-007-0035-4},
  abstract = {We study the cost-optimal reachability problem for weighted 
timed automata such that positive and negative costs are allowed on edges 
and locations. By~optimality, we mean an infimum cost as well as a 
supremum cost. We show that this problem is PSPACE-complete. Our~proof 
uses techniques of linear programming, and thus exploits an important 
property of optimal runs : their time-transitions use a time which is 
arbitrarily closed to an integer. We~then propose an extension of the 
region graph, the weighted discrete graph, whose structure gives light on 
the way to solve the cost-optimal reachability problem. We~also give an 
application of the cost-optimal reachability problem in the context of 
timed games.}
}
@article{BBS-arxiv05,
  publisher = {ACM Press},
  journal = {ACM Transactions on Computational Logic},
  author = {Baier, Christel and Bertrand, Nathalie and
                   Schnoebelen, {\relax Ph}ilippe},
  title = {Verifying nondeterministic probabilistic channel
                systems against {{\(\omega\)}}-regular linear-time
                properties},
  year = 2007,
  volume = 9,
  number = 1,
  nopages = {},
  month = dec,
  url = {http://arxiv.org/abs/cs.LO/0511023},
  pdf = {http://arxiv.org/pdf/cs.LO/0511023},
  ps = {http://arxiv.org/ps/cs.LO/0511023},
  doi = {10.1145/1297658.1297663},
  abstract = {Lossy channel systems (LCS's) are systems of finite state processes that
  communicate via unreliable unbounded fifo channels. We introduce NPLCS's,
  a variant of LCS's where message losses have a probabilistic behavior
  while the component processes behave nondeterministically, and study the
  decidability of qualitative verification problems for \(\omega\)-regular
  linear-time properties.\par
  We show that ---in contrast to finite-state Markov decision processes---
  the satisfaction relation for linear-time formulas depends on the type of
  schedulers that resolve the nondeterminism. While the qualitative model
  checking problems for the full class of history-dependent schedulers is
  undecidable, the same questions for finite-memory schedulers can be
  solved algorithmically. Additionally, some special kinds of reachability,
  or recurrent reachability, qualitative properties yield decidable
  verification problems for the full class of schedulers, which ---for this
  restricted class of problems--- are as powerful as finite-memory
  schedulers, or even a subclass of them.}
}
@article{DD-icomp06,
  publisher = {Elsevier Science Publishers},
  journal = {Information and Computation},
  author = {Demri, St{\'e}phane and D'Souza, Deepak},
  title = {An automata-theoretic approach to constraint~{LTL}},
  year = 2007,
  pages = {380-415},
  volume = 205,
  number = 3,
  month = mar,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DD-icomp06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DD-icomp06.pdf},
  doi = {10.1016/j.ic.2006.09.006},
  abstract = {We consider an extension of linear-time temporal logic~(LTL)
with constraints interpreted over a concrete domain. We~use a new
automata-theoretic technique to show pspace decidability of the logic for the
constraint systems \((\mathbb{Z}, <, =)\) and \((\mathbb{N}, <, =)\). Along
the way, we give an automata-theoretic proof of a result of [Ph.~Balbiani,
J.~Condotta, \textit{Computational complexity of propositional linear temporal logics
based on qualitative spatial or temporal reasoning}, 2002] when the constraint system
satisfies the completion property. Our decision procedures extend easily to
handle extensions of the logic with past-time operators and constants, as well
as an extension of the temporal language itself to monadic second order logic.
Finally we show that the logic becomes undecidable when one considers
constraint systems that allow a counting mechanism.}
}
@article{DrGa07tcs,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Droste, Manfred and Gastin, Paul},
  title = {Weighted automata and weighted logics},
  year = 2007,
  month = jun,
  volume = 380,
  number = {1-2},
  pages = {69-86},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-13.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-13.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
		rr-lsv-2005-13.ps},
  doi = {10.1016/j.tcs.2007.02.055},
  abstract = {Weighted automata are used to describe quantitative properties
                  in various areas such as probabilistic systems, image
                  compression, speech-to-text processing. The~behaviour of
                  such an automaton is a mapping, called a formal power
                  series, assigning to each word a weight in some semiring. 
		  We~generalize B{\"u}chi's and Elgot's fundamental theorems to this
                  quantitative setting. We~introduce a weighted version of MSO
                  logic and prove that, for commutative semirings, the
                  behaviours of weighted automata are precisely the formal
                  power series definable with particular sentences of our
                  weighted logic. We~also consider weighted first-order logic
                  and show that aperiodic series coincide with the first-order
                  definable ones, if the semiring is locally finite,
                  commutative and has some aperiodicity property.},
  oldnote = {Special issue of ICALP'05. To appear. 
               Also available as Research Report LSV-05-13, 
               Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, 
               France, July 2005.}
}
@article{LLT-icomp07,
  publisher = {Elsevier Science Publishers},
  journal = {Information and Computation},
  author = {Lafourcade, Pascal and Lugiez, Denis and Treinen, Ralf},
  title = {Intruder Deduction for the Equational Theory of {A}belian Groups with 
                  Distributive Encryption},
  year = 2007,
  volume = 205,
  number = 4,
  pages = {581-623},
  month = apr,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LLT-icomp07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LLT-icomp07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LLT-icomp07.ps},
  doi = {10.1016/j.ic.2006.10.008},
  abstract = {Cryptographic protocols are small programs which involve a high
  level of concurrency and which are difficult to analyze by hand. The~most
  successful methods to verify such protocols are based on rewriting
  techniques and automated deduction in order to implement or mimic the
  process calculus describing the execution of a protocol. We~are interested
  in the intruder deduction problem, that is vulnerability to passive attacks
  in presence of equational theories which model the protocol specification
  and properties of the cryptographic operators.\par
  In the present paper we consider the case where the encryption distributes
  over the operator of an Abelian group or over an exclusive-or 
  operator. We~prove decidability of the intruder deduction problem in both 
  cases. We~obtain a PTIME decision procedure in a restricted case, the  
  so-called binary case.\par
  These decision procedures are based on a careful analysis of the proof
  system modeling the deductive power of the intruder, taking into account the
  algebraic properties of the equational theories under consideration.
  The~analysis of the deduction rules interacting with the equational theory
  relies on the manipulation of \(\mathbb{Z}\)-modules in the general case,
  and on results from prefix rewriting in the binary case.}
}
@book{TATA07,
  author = {Comon{-}Lundh, Hubert and Dauchet, Max and Gilleron, R{\'e}mi  and
                L{\"o}ding, Cristof and Jacquemard, Florent and 
		Lugiez, Denis and Tison, Sophie and  Tommasi, Marc},
  title = {Tree Automata Techniques and Applications},
  year = 2007,
  month = nov,
  url = {http://www.grappa.univ-lille3.fr/tata/},
  nmhowpublished = {Available on: \url{http://www.grappa.univ-lille3.fr/tata}},
  nmnote = {release October, 12th 2007}
}
@misc{dots-rapp-6m,
  author = {Fran{\c{c}}ois Laroussinie and others},
  title = {Projet DOTS (ANR-06-SETI-003)~: Rapport {\`a} \(6\)~mois},
  year = 2007,
  month = aug,
  type = {Contract Report},
  note = {7~pages}
}
@misc{hcl:lecture07,
  author = {Comon{-}Lundh, Hubert},
  title = {Soundness of abstract cryptography},
  oldhowpublished = {Lecture notes, part 1. 
         Available at \url{http://staff.aist.go.jp/h.comon-lundh/}},
  year = {2007},
  note = {Course notes (part~1), Symposium on Cryptography and
                  Information Security (SCIS2008), Tokai, Japan},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CL-sac08.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CL-sac08.pdf}
}
@unpublished{JLC-rc,
  author = {Carr{\'e}, Jean-Loup},
  title = {R{\'e}{\'e}criture, confluence},
  year = {2007},
  month = dec,
  note = {Course notes, {P}r{\'e}paration {\`a} l'agr{\'e}gation, 
	 ENS Cachan, France}
}
@misc{averiles07-f1.6,
  author = {Ourghanlian, Alain and Bozga, Marius and Roglewicz, Adam and
                  Sangnier, Arnaud},
  title = {Projet {RNTL} {A}veriles~-- Fourniture F1.6~: Exp{\'e}rimentation},
  year = 2007,
  month = sep,
  type = {Contract Report},
  note = {16~pages},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/averiles-f16.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/averiles-f16.pdf}
}
@misc{averiles07-f1.4,
  author = {LIAFA and LSV and Verimag},
  title = {Projet {RNTL} {A}veriles~-- Fourniture F1.4~: Prototypes d'outil},
  year = 2007,
  month = sep,
  type = {Contract Report},
  note = {3~pages},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/averiles-f14.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/averiles-f14.pdf}
}
@misc{averiles07-f1.3,
  author = {LIAFA and {CRIL Technology} and {EDF R\&D} and LSV and Verimag},
  title = {Projet {RNTL} {A}veriles~-- Fourniture F1.3~: Algorithmes de v{\'e}rification},
  year = 2007,
  month = sep,
  type = {Contract Report},
  note = {19~pages},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/averiles-f13.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/averiles-f13.pdf}
}
@misc{averiles07-f1.2,
  author = {LIAFA and {CRIL Technology} and {EDF R\&D} and LSV and Verimag},
  title = {Projet {RNTL} {A}veriles~-- Fourniture F1.2~: Extraction de mod{\`e}les},
  year = 2007,
  month = sep,
  type = {Contract Report},
  note = {19~pages},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/averiles-f12.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/averiles-f12.pdf}
}
@misc{averiles07-f1.1,
  author = {LIAFA and {CRIL Technology} and {EDF R\&D} and LSV and Verimag},
  title = {Projet {RNTL} {A}veriles~-- Fourniture F1.1~: Mod{\`e}les},
  year = 2007,
  month = sep,
  type = {Contract Report},
  note = {6~pages},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/averiles-f11.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/averiles-f11.pdf}
}
@misc{averiles07,
  author = {LIAFA and {CRIL Technology} and {EDF R\&D} and LSV and Verimag},
  title = {Rapport {\`a} mi-parcours du projet {RNTL} {A}veriles (analyse et
                  v{\'e}rification de logiciels embarqu{\'e}s avec structures
                  de m{\'e}moire dynamique},
  year = 2007,
  month = sep,
  type = {Contract Report},
  note = {4~pages},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/averiles-MP.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/averiles-MP.pdf}
}
@unpublished{PG-algo,
  author = {Gastin, Paul},
  title = {Algorithmique},
  year = {2007},
  month = nov,
  note = {Course notes, {M}agist{\`e}re STIC, ENS Cachan, France}
}
@unpublished{PG-languages,
  author = {Gastin, Paul},
  title = {Langages formels},
  year = {2007},
  month = may,
  note = {Course notes, {M}agist{\`e}re STIC, ENS Cachan, France}
}
@misc{ltl2ba-v1.1,
  author = {Gastin, Paul and Oddoux, Denis},
  title = {LTL2BA~v1.1},
  year = {2007},
  month = aug,
  nohowpublished = {Available at http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/},
  note = {Written in~C++ (about 4000 lines)},
  note-fr = {\'Ecrit en~C++ (environ 4000 lignes)},
  url = {http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/}
}
@misc{pronobis-final,
  author = {ARC ProNoBis},
  title = {ProNoBis: Probability and Nondeterminism, Bisimulations and
                  Security~-- {R}apport Final},
  year = 2007,
  month = oct,
  type = {Contract Report},
  nonote = {78~slides},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/SLIDES/pronobis-final.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/SLIDES/pronobis-final.pdf}
}
@misc{netqi-v1,
  author = {Bursztein, Elie},
  title = {NetQi~v1rc1},
  year = {2007},
  month = dec,
  howpublished = {Available at \url{http://www.netqi.org/}},
  note = {Written in~C and Java (about 10000 lines)},
  note-fr = {\'Ecrit en~C et en Java (environ 10000 lignes)},
  url = {http://www.netqi.org}
}
@inproceedings{SC-fcc07,
  address = {Venice, Italy},
  month = jul,
  year = 2007,
  editor = {Backes, Michael and Lakhnech, Yassine},
  acronym = {{FCC}'07},
  booktitle = {{P}roceedings of the 3rd {W}orkshop on {F}ormal and
		 {C}omputational {C}ryptography ({FCC}'07)},
  author = {Steel ,Graham and Courant, Judica{\"e}l},
  title = {A formal model for detecting parallel key search attacks},
  nopages = {},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/SC-fcc07.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SC-fcc07.pdf}
}
@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.",
}}
@misc{GL:ARC-ProNoBis-16,
  author = {Goubault-Larrecq, Jean},
  howpublished = {Rapport final ARC ProNoBis},
  month = oct,
  title = {{Pronobis: Probability and nondeterminism,
bisimulations and security}},
  year = {2007}
}

This file was generated by bibtex2html 1.98.