@inproceedings{FLS-ilc07, address = {Cape Town, South Africa}, month = oct, year = 2009, volume = 5489, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer-Verlag}, editor = {Archibald, Margaret and Brattka, Vasco and Goranko, Valentin and L{\"o}we, Benedikt}, acronym = {{ILC}'07}, booktitle = {{R}evised {S}elected {P}apers of the {I}nternational {C}onference on {I}nfinity in {L}ogic {\&} {C}omputation ({ILC}'07)}, author = {Finkel, Alain and Lozes, {\'E}tienne and Sangnier, Arnaud}, title = {Towards Model Checking Pointer Systems}, pages = {56-82}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FLS-ilc07.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FLS-ilc07.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FLS-ilc07.ps}, doi = {10.1007/978-3-642-03092-5_6}, abstract = {We aim at checking safety and temporal properties over models representing the behavior of programs manipulating dynamic singly-linked lists. The properties we consider not only allow to perform a classical shape analysis, but we also want to check quantitative aspect on the manipulated memory heap. We first explain how a translation of programs into counter systems can be used to check safety problems and temporal properties. We then study the decidability of these two problems considering some restricted classes of programs, namely flat programs without destructive update. We obtain the following results: (1)~the model-checking problem is decidable if the considered program works over acyclic lists; (2)~the safety problem is decidable for programs without alias test. We finally explain the limit of our decidability results, showing that relaxing one of the hypothesis leads to undecidability results.} }

@article{CEFX-fmsd08, publisher = {Springer}, journal = {Formal Methods in System Design}, author = {Chevallier, R{\'e}my and Encrenaz{-}Tiph{\`e}ne, Emmanuelle and Fribourg, Laurent and Xu, Weiwen}, title = {Timed Verification of the Generic Architecture of a Memory Circuit Using Parametric Timed Automata}, volume = 34, number = 1, pages = {59-81}, year = 2009, month = feb, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CEFX-fmsd08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CEFX-fmsd08.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CEFX-fmsd08.ps}, doi = {10.1007/s10703-008-0061-x}, abstract = {Using a variant of Clariso-Cortadella's parametric method for verifying asynchronous circuits, we analyse some crucial timing behaviors of the architecture of SPSMALL memory, a~commercial product of STMicroelectronics. Using the model of parametric timed automata and model checker HYTECH, we~formally derive a set of linear constraints that ensure the correctness of the response times of the memory. We are also able to infer the constraints characterizing the optimal setup timings of input signals. We have checked, for two different implementations of this architecture, that the values given by our model match remarkably with the values obtained by the designer through electrical simulation. } }

@inproceedings{EF-infinity07, optaddress = {Lisbon, Portugal}, month = jul, year = 2009, volume = 239, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier Science Publishers}, realeditor = {Madhusudan, P. and Kahlon, Vineet}, editor = {Habermehl, Peter and Vojnar, Tom{\'a}{\v{s}}}, acronym = {{INFINITY}'06,'07,'08}, booktitle = {{J}oint {P}roceedings of the 8th, 9th and 10th {I}nternational {W}orkshops on {V}erification of {I}nfinite {S}tate {S}ystems ({INFINITY}'06,'07,'08)}, author = {Encrenaz, Emmanuelle and Finkel, Alain}, title = {Automatic verification of counter systems with ranking functions}, pages = {85-103}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EF-infinity07.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EF-infinity07.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/EF-infinity07.ps}, doi = {10.1016/j.entcs.2009.05.032}, abstract = {The verification of final termination for counter systems is undecidable. For non flattable counter systems, the verification of this type of property is generally based on the exhibition of a ranking function. Proving the existence of a ranking function for general counter systems is also undecidable. We~provide a framework in which the verification whether a given function is a ranking function is decidable. This framework is applicable to convex counter systems which admit a Presburger or a LPDS ranking function. This extends the results of [A.~Bradley, Z.~Manna, and B.~Sipma. \textit{Termination analysis of integer linear loops}. In~CONCUR'05, LNCS~3653, p.~488-502. Springer]. From this framework, we derive a model-checking algorithm to verify whether a final termination property is satisfied or not. This approach has been successfully applied to the verification of a parametric version of the ZCSP protocol.} }

@inproceedings{Bouyer-M4M5, address = {Cachan, France}, month = mar, year = 2009, volume = 231, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier Science Publishers}, editor = {Areces, Carlos and Demri, St{\'e}phane}, acronym = {{M4M-5}}, booktitle = {{P}roceedings of the 4th {W}orkshop on {M}ethods for {M}odalities ({M4M-5})}, author = {Bouyer, Patricia}, title = {Model-Checking Timed Temporal Logics}, pages = {323-341}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-M4M5.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-M4M5.pdf}, doi = {10.1016/j.entcs.2009.02.044}, abstract = {In this paper, we present several timed extensions of temporal logics, that can be used for model-checking real-time systems. We give different formalisms and the corresponding decidability/complexity results. We also give intuition to explain these results.} }

@proceedings{M4M5-AD, editor = {Areces, Carlos and Demri, St{\'e}phane}, title = {{P}roceedings of the 5th {I}nternational {W}orkshop on {M}ethods for {M}odalities ({M4M-5})}, booktitle = {{P}roceedings of the 5th {I}nternational {W}orkshop on {M}ethods for {M}odalities ({M4M-5})}, publisher = {Elsevier Science Publishers}, series = {Electronic Notes in Theoretical Computer Science}, volume = 231, year = 2009, month = mar, address = {Cachan, France}, url = {http://www.sciencedirect.com/science/journal/15710661/231}, doi = {10.1016/j.entcs.2009.02.025} }

@article{CD-fmsd08, publisher = {Springer}, journal = {Formal Methods in System Design}, author = {Cortier, V{\'e}ronique and Delaune, St{\'e}phanie}, title = {Safely Composing Security Protocols}, volume = 34, number = 1, pages = {1-36}, month = feb, year = 2009, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CD-fmsd08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CD-fmsd08.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CD-fmsd08.ps}, doi = {10.1007/s10703-008-0059-4}, 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 an active attacker 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 are executed, possibly sharing some common keys like public keys or long-term symmetric keys.\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 satisfying a reasonable (syntactic) condition are executed. This result holds for a large class of security properties that encompasses secrecy and various formulations of authentication.} }

@inproceedings{GGJ-wrs08, address = {Castle of Hagenberg, Austria}, month = apr, year = 2009, volume = 237, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier Science Publishers}, editor = {Middeldorp, Aart}, acronym = {{WRS}'08}, booktitle = {{P}roceedings of the 8th {I}nternational {W}orkshop on {R}eduction {S}trategies in {R}ewriting and {P}rogramming ({WRS}'08)}, author = {Gasc{\'o}n, Adri{\`a} and Godoy, Guillem and Jacquemard, Florent}, title = {Closure of Tree Automata Languages under Innermost Rewriting}, pages = {23-38}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GGJ-wrs08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GGJ-wrs08.pdf}, doi = {10.1016/j.entcs.2009.03.033}, abstract = {Preservation of regularity by a term rewriting system~(TRS) states that the set of reachable terms from a tree automata~(TA) language (a.k.a.~regular term set) is also a TA language. It~is an important and useful property, and there have been many works on identifying classes of TRS ensuring~it; unfortunately, regularity is not preserved for restricted classes of TRS like shallow~TRS. Nevertheless, this property has not been studied for important strategies of rewriting like the innermost strategy which corresponds to the call by value computation of programming languages.\par We prove that the set of innermost-reachable terms from a TA language by a shallow TRS is not necessarily regular, but it can be recognized by a TA with equality and disequality constraints between brothers. As~a consequence we conclude decidability of regularity of the reachable set of terms from a TA language by innermost rewriting and shallow TRS. This result is in contrast with plain (not necessarily innermost) rewriting for which we prove undecidability. We also show that, like for plain rewriting, innermost rewriting with linear and right-shallow TRS preserves regularity.} }

@inproceedings{EB-fast08, address = {Malaga, Spain}, month = apr, year = 2009, volume = 5491, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Degano, Pierpaolo and Guttman, Joshua and Martinelli, Fabio}, acronym = {{FAST}'08}, booktitle = {{R}evised {S}elected {P}apers of the 5th {I}nternational {W}orkshop on {F}ormal {A}spects in {S}ecurity and {T}rust ({FAST}'08)}, author = {Bursztein, Elie}, title = {Extending Anticipation Games with Location, Penalty and Timeline}, pages = {272-286}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/eb-fast08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/eb-fast08.pdf}, doi = {10.1007/978-3-642-01465-9_18}, abstract = {Over the last few years, attack graphs have became a well recognized tool to analyze and model complex network attack. The most advanced evolution of attack graphs, called anticipation games, is based on game theory. However even if anticipation games allow to model time, collateral effects and player interactions with the network, there is still key aspects of the network security that cannot be modeled in this framework. Theses aspects are network cooperation to fight unknown attack, the cost of attack based on its duration and the introduction of new attack over the time. In this paper we address these needs, by introducing a three-fold extension to anticipation games. We prove that this extension does not change the complexity of the framework. We illustrate the usefulness of this extension by presenting how it can be used to find a defense strategy against 0 days that use an honey net. Finally, we have implemented this extension into a prototype, to show that it can be used to analyze large networks security.} }

@article{DKR-jcs08, publisher = {{IOS} Press}, journal = {Journal of Computer Security}, author = {Delaune, St{\'e}phanie and Kremer, Steve and Ryan, Mark D.}, title = {Verifying Privacy-type Properties of Electronic Voting Protocols}, volume = 17, number = 4, month = jul, year = 2009, pages = {435-487}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-jcs08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-jcs08.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DKR-jcs08.ps}, doi = {10.3233/JCS-2009-0340}, abstract = {Electronic voting promises the possibility of a convenient, efficient and secure facility for recording and tallying votes in an election. Recently highlighted inadequacies of implemented systems have demonstrated the importance of formally verifying the underlying voting protocols. We study three privacy-type properties of electronic voting protocols: in increasing order of strength, they are vote-privacy, receipt-freeness, and coercion-resistance.\par We use the applied pi calculus, a formalism well adapted to modelling such protocols, which has the advantages of being based on well-understood concepts. The privacy-type properties are expressed using observational equivalence and we show in accordance with intuition that coercion-resistance implies receipt-freeness, which implies vote-privacy.\par We illustrate our definitions on three electronic voting protocols from the literature. Ideally, these three properties should hold even if the election officials are corrupt. However, protocols that were designed to satisfy receipt-freeness or coercion-resistance may not do so in the presence of corrupt officials. Our model and definitions allow us to specify and easily change which authorities are supposed to be trustworthy.} }

@inproceedings{BFS-infinity08, optaddress = {Toronto, Canada}, month = jul, year = 2009, volume = 239, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier Science Publishers}, editor = {Habermehl, Peter and Vojnar, Tom{\'a}{\v{s}}}, acronym = {{INFINITY}'06,'07,'08}, booktitle = {{J}oint {P}roceedings of the 8th, 9th and 10th {I}nternational {W}orkshops on {V}erification of {I}nfinite {S}tate {S}ystems ({INFINITY}'06,'07,'08)}, author = {Bouchy, Florent and Finkel, Alain and Sangnier, Arnaud}, title = {Reachability in Timed Counter Systems}, pages = {167-178}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFS-infinity08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFS-infinity08.pdf}, doi = {10.1016/j.entcs.2009.05.038}, abstract = {We introduce Timed Counter Systems, a~new class of systems mixing clocks and counters. Such systems have an infinite state space, hence their reachability problems are undecidable. By~abstracting clock values with a Region Graph, we~show the Counter Reachability Problem to be decidable for three subclasses: Timed~VASS, Bounded Timed Counter Systems, and Reversal-Bounded Timed Counter Systems.} }

@proceedings{HV-infinity2008, title = {{J}oint {P}roceedings of the 8th, 9th and 10th {I}nternational {W}orkshops on {V}erification of {I}nfinite {S}tate {S}ystems ({INFINITY}'06,'07,'08)}, booktitle = {{J}oint {P}roceedings of the 8th, 9th and 10th {I}nternational {W}orkshops on {V}erification of {I}nfinite {S}tate {S}ystems ({INFINITY}'06,'07,'08)}, optacronym = {{INFINITY}'06,'07,'08}, editor = {Habermehl, Peter and Vojnar, Tom{\'a}{\v{s}}}, publisher = {Elsevier Science Publishers}, doi = {10.1016/j.entcs.2009.05.026}, series = {Electronic Notes in Theoretical Computer Science}, volume = 239, year = 2009, month = jul, optaddress = {Toronto, Canada} }

@incollection{DG-hwa08, year = 2009, series = {EATCS Monographs in Theoretical Computer Science}, publisher = {Springer}, editor = {Kuich, Werner and Vogler, Heiko and Droste, Manfred}, booktitle = {Handbook of Weighted Automata}, author = {Droste, Manfred and Gastin, Paul}, title = {Weighted automata and weighted logics}, pages = {175-211}, chapter = 5, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-hwa08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-hwa08.pdf} }

@incollection{DG-pct08, futureaddress = {}, month = jan, year = 2009, series = {IARCS-Universities}, publisher = {Universities Press}, booktitle = {Perspectives in Concurrency Theory}, editor = {Lodaya, Kamal and Mukund, Madhavan and Ramanujam, R.}, author = {Diekert, Volker and Gastin, Paul}, title = {Local safety and local liveness for distributed systems}, pages = {86-106}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-pct08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-pct08.pdf}, abstract = {We introduce local safety and local liveness for distributed systems whose executions are modeled by Mazurkiewicz traces. We characterize local safety by local closure and local liveness by local density. Restricting to first-order definable properties, we prove a decomposition theorem in the spirit of the separation theorem for linear temporal logic. We then characterize local safety and local liveness by means of canonical local temporal logic formulae.} }

@article{DL-tocl08, publisher = {ACM Press}, journal = {ACM Transactions on Computational Logic}, author = {Demri, St{\'e}phane and Lazi{\'c}, Ranko}, title = {{LTL} with the freeze quantifier and register automata}, volume = 10, number = 3, nopages = {}, month = apr, year = 2009, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DL-tocl08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DL-tocl08.pdf}, doi = {10.1145/1507244.1507246}, abstract = {A data word is a sequence of pairs of a letter from a finite alphabet and an element from an infinite set, where the latter can only be compared for equality. To reason about data words, linear temporal logic is extended by the freeze quantifier, which stores the element at the current word position into a register, for equality comparisons deeper in the formula. By translations from the logic to alternating automata with registers and then to faulty counter automata whose counters may erroneously increase at any time, and from faulty and error-free counter automata to the logic, we obtain a complete complexity table for logical fragments defined by varying the set of temporal operators and the number of registers. In~particular, the~logic with future-time operators and \(1\)~register is decidable but not primitive recursive over finite data words. Adding past-time operators or \(1\)~more register, or switching to infinite data words, cause undecidability.} }

@article{AP-ieeedeb09, publisher = {{IEEE} Computer Society Press}, journal = {IEEE Data Engineering Bulletin}, author = {Abiteboul, Serge and Polyzotis, Neoklis}, title = {Searching Shared Content in Communities with the Data Ring}, volume = 32, number = 2, pages = {44-51}, year = 2009, month = jun, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AP-ieeedeb09.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AP-ieeedeb09.pdf}, doi = {}, abstract = {Information ubiquity has created a large crowd of users (most notably scientists), who could employ DBMS technology to share and search their data more effectively. Still, this user base prefers to keep its data in files that can be easily managed by applications such as spreadsheets, rather than deal with the complexity and rigidity of modern database systems.\par In this article, we describe a vision for enabling non-experts, such as scientists, to build content sharing communities in a true database fashion: declaratively. The proposed infrastructure, called the data ring, enables users to share and search their data with minimal effort; the user points to the data that should be shared, and the data ring becomes responsible for automatically indexing the data (to make it accessible), replicating it (for availability), and reorganizing its physical storage (for better query performance). We outline the salient features of our proposal, and outline recent technical advancements in realizing data rings.} }

@article{ASV-ieeedeb09, publisher = {{IEEE} Computer Society Press}, journal = {IEEE Data Engineering Bulletin}, author = {Abiteboul, Serge and Segoufin, Luc and Vianu, Victor}, title = {Modeling and Verifying Active {XML} Artifacts}, volume = 32, number = 3, pages = {10-15}, year = 2009, month = sep, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ASV-ieeedeb09.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ASV-ieeedeb09.pdf}, doi = {} }

@article{AKSS-jvldb09, publisher = {ACM Press}, journal = {The VLDB Journal}, author = {Abiteboul, Serge and Kimelfeld, Benny and Sagiv, Yehoshua and Senellart, Pierre}, title = {On the expressiveness of probabilistic {XML} models}, volume = 18, number = 5, pages = {1041-1064}, year = 2009, month = oct, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AKSS-jvldb09.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AKSS-jvldb09.pdf}, doi = {10.1007/s00778-009-0146-1}, abstract = {Various known models of probabilistic XML can be represented as instantiations of the abstract notion of \emph{p-documents}. In addition to ordinary nodes, p-documents have \emph{distributional} nodes that specify the possible worlds and their probabilistic distribution. Particular families of p-documents are determined by the types of distributional nodes that can be used as well as by the structural constraints on the placement of those nodes in a p-document. Some of the resulting families provide natural extensions and combinations of previously studied probabilistic XML models. The focus of the paper is on the expressive power of families of p-documents. In particular, two main issues are studied. The first is the ability to (efficiently) \emph{translate} a given p-document of one family into another family. The second is \emph{closure under updates}, namely, the ability to (efficiently) represent the result of updating the instances of a p-document of a given family as another p-document of that family. For both issues, we distinguish two variants corresponding to \emph{value-based} and \emph{object-based} semantics of p-documents.} }

@inproceedings{ABM-edbt09, address = {Saint Petersburg, Russia}, month = mar, year = 2009, novolume = {}, series = {ACM International Conference Proceeding Series}, publisher = {Springer}, editor = {Kersten, Martin L. and Novikov, Boris and Teubner, Jens and Polutin, Vladimir and Manegold, Stefan}, acronym = {{EDBT}'09}, booktitle = {{A}dvances in {D}atabase {T}echnology~--- {P}roceedings of the 12th {I}nternational {C}onference on {E}xtending {D}atabase {T}echnology ({EDBT}'09)}, author = {Abiteboul, Serge and Bourhis, Pierre and Marinoiu, Bogdan}, title = {Efficient maintenance techniques for views over active documents}, pages = {1076-1087}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABM-edbt09.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABM-edbt09.pdf}, doi = {10.1145/1516360.1516483}, abstract = {Many Web applications are based on dynamic interactions between Web components exchanging flows of information. Such a situation arises for instance in mashup systems or when monitoring distributed autonomous systems. Our work is in this challenging context that has generated recently a lot of attention; see Web~2.0. We introduce the axlog formal model for capturing such interactions and show how this model can be supported efficiently. The central component is the axlog widget defined by one tree-pattern query or more, over an active document (in the Active XML style) that includes some input streams of updates. A widget generates a stream of updates for each query, the updates that are needed to maintain the view corresponding to the query. We exploit an array of known technologies: datalog optimization techniques such as Differential or MagicSet, constraint query languages, and efficient XML filtering (YFilter). The novel optimization technique we propose is based on fundamental new notions: a relevance (different than that of MagicSet), satisfiability and provenance for active documents. We briefly discuss an implementation of an axlog engine, an application that we used to test the approach, and results of experiments.} }

@inproceedings{AGMP-icde2009, address = {Shanghai, China}, month = mar # {-} # apr, year = 2009, publisher = {{IEEE} Computer Society Press}, editor = {Ioannidis, Yannis E. and Lee, Dik Lun and Ng, Raymond T.}, acronym = {{ICDE}'09}, booktitle = {{P}roceedings of the 25th {I}nternational {C}onference on {D}ata {E}ngineering ({ICDE}'09)}, author = {Abiteboul, Serge and Greenshpan, Ohad and Milo, Tova and Polyzotis, Neoklis}, title = {Match{U}p: Autocompletion for Mashups}, pages = {1479-1482}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AGMP-icde2009.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGMP-icde2009.pdf}, doi = {10.1109/ICDE.2009.47}, abstract = {A~\emph{mashup} is a Web application that integrates data, computation and GUI provided by several systems into a unique tool. The concept originated from the understanding that the number of applications available on the Web and the need for combining them to meet user requirements, are growing very rapidly. This demo presents \emph{MatchUp}, a system that supports rapid, on-demand, intuitive development of \emph{mashups}, based on a novel \emph{autocompletion} mechanism. The key observation guiding the development of \emph{MatchUp} is that mashups developed by different users typically share common characteristics; they use similar classes of mashup components and glue them together in a similar manner. \emph{MatchUp} exploits these similarities to predict, given a user's partial mashup specification, what are the most likely potential \emph{completions} (missing components and connection between them) for the specification. Using a novel ranking algorithm, users are then offered top-k completions from which they choose and refine according to their needs.} }

@article{CDMP-apal09, publisher = {Elsevier Science Publishers}, journal = {Annals of Pure and Applied Logics}, author = {Chevalier, Fabrice and D'Souza, Deepak and Matteplackel, Raj Mohan and Prabhakar, Pavithra}, title = {Automata and logics over finitely varying functions}, year = {2009}, month = dec, volume = {161}, number = {3}, pages = {324-336}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDMP-apal09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDMP-apal09.pdf}, doi = {10.1016/j.apal.2009.07.007}, abstract = {We extend some of the classical connections between automata and logic due to B{\"u}chi~(1960) and McNaughton and Papert~(1971) to languages of finitely varying functions or {"}signals{"}. In particular, we introduce a natural class of automata for generating finitely varying functions called ST-NFAs, and show that it coincides in terms of language definability with a natural monadic second-order logic interpreted over finitely varying functions (Rabinovich, 2002). We also identify a {"}counter-free{"} subclass of ST-NFAs which characterise the first-order definable languages of finitely varying functions. Our proofs mainly factor through the classical results for word languages. These results have applications in automata characterisations for continuously interpreted real-time logics like Metric Temporal Logic (MTL) (Chevalier \emph{et~al.}, 2006,~2007).} }

@phdthesis{mercier-phd2009, author = {Mercier, Antoine}, title = {Contributions {\`a} l'analyse automatique des protocoles cryptographiques en pr{\'e}sence de propri{\'e}t{\'e}s alg{\'e}briques : protocoles de groupe, {\'e}quivalence statique}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2009, month = dec, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AM-these09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AM-these09.pdf} }

@phdthesis{bursuc-phd2009, author = {Bursuc, Sergiu}, title = {Contraintes de d{\'e}ductibilit{\'e} dans une alg{\`e}bre quotient: r{\'e}duction de mod{\`e}les et applications {\`a} la s{\'e}curit{\'e}}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2009, month = dec, url = {http://www.lsv.fr/Publis/PAPERS/PDF/SB-these09.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SB-these09.pdf} }

@incollection{CM-CES09, author = {Cassez, Franck and Markey, Nicolas}, title = {Control of Timed Systems}, booktitle = {Communicating Embedded Systems~-- Software and Design}, editor = {Jard, Claude and Roux, Olivier H.}, publisher = {Wiley-ISTE}, year = 2009, month = oct, pages = {83-120}, chapter = 3, url = {http://www.iste.co.uk/index.php?f=x&ACTION=View&id=288}, nops = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/.ps}, nopsgz = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PSGZ/.ps.gz}, isbn = {9781848211438} }

@incollection{DH-CES09, author = {Donatelli, Susanna and Haddad, Serge}, title = {Quantitative Verification of {M}arkov Chains}, booktitle = {Communicating Embedded Systems~-- Software and Design}, editor = {Jard, Claude and Roux, Olivier H.}, publisher = {Wiley-ISTE}, year = 2009, month = oct, pages = {139-163}, chapter = 5, url = {http://www.iste.co.uk/index.php?f=x&ACTION=View&id=288}, nops = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/.ps}, nopsgz = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PSGZ/.ps.gz}, isbn = {9781848211438} }

@inproceedings{JGL-asian09, address = {Seoul, Korea}, month = dec, year = 2009, volume = 5913, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Datta, Anupam}, acronym = {{ASIAN}'09}, booktitle = {{P}roceedings of the 13th {A}sian {C}omputing {S}cience {C}onference ({ASIAN}'09)}, author = {Goubault{-}Larrecq, Jean}, title = {{\textquotedbl}{L}ogic Wins!{\textquotedbl}}, pages = {1-16}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-asian09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-asian09.pdf}, doi = {10.1007/978-3-642-10622-4_1}, abstract = {Clever algorithm design is sometimes superseded by simple encodings into logic. We apply this motto to a few case studies in the formal verification of security properties. In particular, we examine confidentiality objectives in hardware circuit descriptions written in VHDL.} }

@phdthesis{chamseddine-phd2009, author = {Chamseddine, Najla}, title = {Analyse quantitative parametr{\'e}e d'automates temporis{\'e}s probabilistes}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2009, month = oct, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/NC-these09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/NC-these09.pdf} }

@phdthesis{bouchy-phd2009, author = {Bouchy, Florent}, title = {Logiques et mod{\`e}les pour la v{\'e}rification de syst{\`e}mes infinis}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2009, month = nov, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FB-these09.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FB-these09.pdf} }

@phdthesis{sznajder-phd2009, author = {Sznajder, Nathalie}, title = {Synth{\`e}se de syst{\`e}mes distribu{\'e}s ouverts}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2009, month = nov, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/NS-these09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/NS-these09.pdf} }

@inproceedings{SRKK-wissec09, address = {Louvain-la-Neuve, Belgium}, month = nov, year = 2009, editor = {Pereira, Olivier and Quisquater, Jean-Jacques and Standaert, Fran\c{c}ois-Xavier}, acronym = {{WISSEC}'09}, booktitle = {{P}roceedings of the 4th {B}enelux {W}orkshop on {I}nformation and {S}ystem {S}ecurity ({WISSEC}'09)}, author = {Smyth, Ben and Ryan, Mark D. and Kremer, Steve and Kourjieh, Mounira}, title = {Election verifiability in electronic voting protocols (Preliminary version)}, nopages = {}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SRKK-wissec09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SRKK-wissec09.pdf}, abstract = {We~present a symbolic definition of election verifiability for electronic voting protocols. Our definition is given in terms of reachability assertions in the applied pi calculus and is amenable to automated reasoning using the tool ProVerif. The~definition distinguishes three aspects of verifiability, which we call individual, universal, and eligibility verifiability. It also allows us to determine precisely what aspects of the system are required to be trusted. We demonstrate our formalism by analysing the protocols due to Fujioka, Okamoto \&~Ohta and Juels, Catalano \&~Jakobsson; the~latter of which has been implemented by Clarkson, Chong \&~Myers. } }

@inproceedings{CCD-secco09, address = {Bologna, Italy}, month = oct, year = 2009, editor = {Boreale, Michele and Kremer, Steve}, acronym = {{SecCo}'09}, booktitle = {{P}reliminary {P}roceedings of the 7th {I}nternational {W}orkshop on {S}ecurity {I}ssues in {C}oordination {M}odels, {L}anguages and {S}ystems ({SecCo}'09)}, author = {Cheval, Vincent and Comon{-}Lundh, Hubert and Delaune, St{\'e}phanie}, title = {A~decision procedure for proving observational equivalence}, nmnote = {did not appear in postproceedings EPTCS7}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CCD-secco09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CCD-secco09.pdf} }

@proceedings{BK-secco2009, title = {{P}roceedings of the 7th {I}nternational {W}orkshop on {S}ecurity {I}ssues in {C}oncurrency ({S}ec{C}o'09)}, booktitle = {{P}roceedings of the 7th {I}nternational {W}orkshop on {S}ecurity {I}ssues in {C}oncurrency ({S}ec{C}o'09)}, acronym = {{S}ec{C}o'09}, editor = {Boreale, Michele and Kremer, Steve}, doi = {10.4204/EPTCS.7}, url = {http://eptcs.web.cse.unsw.edu.au/content.cgi?SECCO2009}, series = {Electronic Proceedings in Theoretical Computer Science}, volume = 7, year = 2009, month = aug, address = {Bologna, Italy} }

@mastersthesis{dimino-m1, author = {Dimino, J{\'e}r{\'e}mie}, title = {Les syst{\`e}mes {\`a} canaux non-fiables vus comme des transducteurs}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de stage de {M1}}, year = {2009}, month = oct, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/dimino-m1.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/dimino-m1.pdf} }

@mastersthesis{cheval-master, author = {Cheval, Vincent}, title = {Algorithme de d{\'e}cision de l'{\'e}quivalence symbolique de syst{\`e}mes de contraintes}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2009}, month = sep, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/master-cheval.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/master-cheval.pdf} }

@mastersthesis{brenguier-master, author = {Brenguier, Romain}, title = {Calcul des {\'e}quilibres de Nash dans les jeux temporis{\'e}s}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2009}, month = sep, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/master-brenguier.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/master-brenguier.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/master-brenguier.ps} }

@techreport{LSV:09:20, author = {Andr{\'e}, {\'E}tienne}, title = {Everything You Always Wanted to Know About {IMITATOR} (But~Were Afraid to~Ask)}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2009}, month = jul, type = {Research Report}, number = {LSV-09-20}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-20.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-20.pdf}, note = {11~pages}, abstract = {We present here the user manual of IMITATOR, a tool for synthesizing constraints on timing bounds (seen as parameters) in the framework of timed automata. Unlike classical synthesis methods, the tool IMITATOR takes advantage of a given reference valuation of the parameters for which the system is known to behave properly. The goal of IMITATOR is to generate a constraint such that, under any valuation satisfying this constraint, the system is guaranteed to behave, in terms of alternating sequences of locations and actions, as under the reference valuation.\par We give here the installation requirements and the launching commands of IMITATOR, as well as the source code of a toy example.} }

@inproceedings{DJLL-fsttcs09, address = {Kanpur, India}, month = dec, year = 2009, volume = 4, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Kannan, Ravi and Narayan Kumar, K.}, acronym = {{FSTTCS}'09}, booktitle = {{P}roceedings of the 29th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'09)}, author = {Demri, St{\'e}phane and Jurdzi{\'n}ski, Marcin and Lachish, Oded and Lazi{\'c}, Ranko}, title = {The covering and boundedness problems for branching vector addition systems}, pages = {181-192}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/djll-fsttcs09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/djll-fsttcs09.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2009.2317}, abstract = {The covering and boundedness problems for branching vector addition systems are shown complete for doubly-exponential time.} }

@inproceedings{DKP-fsttcs09, address = {Kanpur, India}, month = dec, year = 2009, volume = 4, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Kannan, Ravi and Narayan Kumar, K.}, acronym = {{FSTTCS}'09}, booktitle = {{P}roceedings of the 29th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'09)}, author = {Delaune, St{\'e}phanie and Kremer, Steve and Pereira, Olivier}, title = {Simulation based security in the applied pi calculus}, pages = {169-180}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DKP-fsttcs09.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DKP-fsttcs09.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2009.2316}, abstract = {We present a symbolic framework for refinement and composition of security protocols. The framework uses the notion of ideal functionalities. These are abstract systems which are secure by construction and which can be combined into larger systems. They can be separately refined in order to obtain concrete protocols implementing them. Our work builds on ideas from computational models such as the universally composable security and reactive simulatability frameworks. The underlying language we use is the applied pi calculus which is a general language for specifying security protocols. In our framework we can express the different standard flavours of simulation-based security which happen to all coincide. We illustrate our framework on an authentication functionality which can be realized using the Needham-Schroeder-Lowe protocol. For this we need to define an ideal functionality for asymmetric encryption and its realization. We also show a joint state result for this functionality which allows composition (even though the same key material is reused) using a tagging mechanism.} }

@article{BCHMMR-ijwsr09, publisher = {{IGI} Publishing}, journal = {International Journal of Web Services Research}, author = {Boutrous{-}Saab, C{\'e}line and Coulibaly, Demba and Haddad, Serge and Melliti, Tarek and Moreaux, Patrice and Rampacek, Sylvain}, title = {An Integrated Framework for Web Services Orchestration}, volume = 6, number = 4, pages = {1-29}, year = 2009, month = sep, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCHMMR-ijwsr09.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCHMMR-ijwsr09.pdf}, abstract = {Currently, Web services give place to active research and this is due both to industrial and theoretical factors. On one hand, Web services are essential as the design model of applications dedicated to the electronic business. On the other hand, this model aims to become one of the major formalisms for the design of distributed and cooperative applications in an open environment (the Internet). In this article, the authors will focus on two features of Web services. The first one concerns the interaction problem: given the interaction protocol of a Web service described in BPEL, how to generate the appropriate client? Their approach is based on a formal semantics for BPEL via process algebra and yields an algorithm which decides whether such a client exists and synthesizes the description of this client as a (timed) automaton. The second one concerns the design process of a service. They propose a method which proceeds by two successive refinements: first the service is described via UML, then refined in a BPEL model and finally enlarged with JAVA code using JCSWL, a new language that we introduce here. Their solutions are integrated in a service development framework that will be presented in a synthetic way.} }

@inproceedings{VLC-aplas09, address = {Seoul, Korea}, month = dec, year = 2009, volume = {5904}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Hu, Zhenjiang}, acronym = {{APLAS}'09}, booktitle = {{P}roceedings of the 7th {A}sian {S}ymposium on {P}rogramming {L}anguages and {S}ystems ({APLAS}'09)}, author = {Villard, Jules and Lozes, {\'E}tienne and Calcagno, Cristiano}, title = {Proving Copyless Message Passing}, pages = {194-209}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/VLC-aplas09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/VLC-aplas09.pdf}, doi = {10.1007/978-3-642-10672-9_15}, abstract = {Handling concurrency using a shared memory and locks is tedious and error-prone. One solution is to use message passing instead. We study here a particular, contract-based flavor that makes the ownership transfer of messages explicit. In this case, ownership of the heap region representing the content of a message is lost upon sending, which can lead to efficient implementations. In this paper, we define a proof system for a concurrent imperative programming language implementing this idea and inspired by the Singularity OS. The proof system, for which we prove soundness, is an extension of separation logic, which has already been used successfully to study various ownership-oriented paradigms.} }

@inproceedings{AFS-avocs09, address = {Swansea, UK}, month = sep, year = {2009}, volume = 23, series = {Electronic Communications of the EASST}, publisher = {European Association of Software Science and Technology}, editor = {Roggenbach, Markus}, acronym = {{AVoCS}'09}, booktitle = {{P}roceedings of the 9th {I}nternational {W}orkshop on {A}utomated {V}erification of {C}ritical {S}ystems ({AVoCS}'09)}, author = {Andr{\'e}, {\'E}tienne and Fribourg, Laurent and Sproston, Jeremy}, title = {An Extension of the Inverse Method to Probabilistic Timed Automata}, nopages = {}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AFS-avocs09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AFS-avocs09.pdf}, abstract = {Probabilistic timed automata can be used to model systems in which probabilistic and timing behavior coexist. Verification of probabilistic timed automata models is generally performed with regard to a single reference valuation of the timing parameters. Given such a parameter valuation, we present a method for obtaining automatically a constraint on timing parameters for which the reachability probabilities (1)~remain invariant and (2)~are~equal to the reachability probabilities for the reference valuation. The method relies on parametric analysis of a non-probabilistic version of the probabilistic timed automata model using the {"}inverse method{"}. Our approach is useful for avoiding repeated executions of probabilistic model checking analyses for the same model with different parameter valuations. We provide examples of the application of our technique to models of randomized protocols.} }

@incollection{HI-petrinet-diaz, year = 2009, publisher = {Wiley-ISTE}, editor = {Diaz, Michel}, booktitle = {Petri Nets: Fundamental Models, Verification and Applications}, author = {Haddad, Serge and Ili{\'e}, Jean-Michel}, title = {Symmetry and Temporal Logic}, pages = {435-460}, url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html} }

@incollection{HV-petrinet-diaz-b, year = 2009, publisher = {Wiley-ISTE}, editor = {Diaz, Michel}, booktitle = {Petri Nets: Fundamental Models, Verification and Applications}, author = {Haddad, Serge and Vernadat, Fran{\c{c}}ois}, title = {Verification of Specific Properties}, pages = {349-414}, url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html} }

@incollection{HM-petrinet-diaz-c, year = 2009, publisher = {Wiley-ISTE}, editor = {Diaz, Michel}, booktitle = {Petri Nets: Fundamental Models, Verification and Applications}, author = {Haddad, Serge and Moreaux, Patrice}, title = {Tensor Methods and Stochastic {P}etri Nets}, pages = {321-346}, url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html} }

@incollection{HM-petrinet-diaz-b, year = 2009, publisher = {Wiley-ISTE}, editor = {Diaz, Michel}, booktitle = {Petri Nets: Fundamental Models, Verification and Applications}, author = {Haddad, Serge and Moreaux, Patrice}, title = {Stochastic Well-formed {P}etri Nets}, pages = {303-320}, url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html} }

@incollection{HM-petrinet-diaz-a, year = 2009, publisher = {Wiley-ISTE}, editor = {Diaz, Michel}, booktitle = {Petri Nets: Fundamental Models, Verification and Applications}, author = {Haddad, Serge and Moreaux, Patrice}, title = {Stochastic {P}etri Nets}, pages = {269-302}, url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html} }

@incollection{H-petrinet-diaz, year = 2009, publisher = {Wiley-ISTE}, editor = {Diaz, Michel}, booktitle = {Petri Nets: Fundamental Models, Verification and Applications}, author = {Haddad, Serge}, title = {Decidability and Complexity of {P}etri Net Problems}, pages = {87-122}, url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html} }

@incollection{HV-petrinet-diaz-a, year = 2009, publisher = {Wiley-ISTE}, editor = {Diaz, Michel}, booktitle = {Petri Nets: Fundamental Models, Verification and Applications}, author = {Haddad, Serge and Vernadat, Fran{\c{c}}ois}, title = {Analysis Methods for {P}etri Nets}, pages = {41-86}, url = {http://eu.wiley.com/WileyCDA/WileyTitle/productCd-1848210795.html} }

@article{BBC-apal09, publisher = {Elsevier Science Publishers}, journal = {Annals of Pure and Applied Logics}, author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and Chevalier, Fabrice}, title = {Weighted O-Minimal Hybrid Systems}, year = {2009}, month = dec, volume = {161}, number = {3}, pages = {268-288}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-apal09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-apal09.pdf}, doi = {10.1016/j.apal.2009.07.014}, 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.} }

@inproceedings{FLS-nordsec09, address = {Oslo, Norway}, month = oct, year = 2009, volume = 5838, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {J{\o}sang, Audun and Maseng, Torleiv and Knapskog, Svein Johan}, acronym = {{NordSec}'09}, booktitle = {{P}roceedings of the 14th {N}ordic {W}orkshop on {S}ecure {IT} {S}ystems ({NordSec}'09)}, author = {Focardi, Riccardo and Luccio, Flaminia L. and Steel, Graham}, title = {Blunting Differential Attacks on {PIN} Processing {API}s}, pages = {88-103}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FLS-nordsec09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FLS-nordsec09.pdf}, doi = {10.1007/978-3-642-04766-4_7}, abstract = {We~propose a countermeasure for a class of known attacks on the PIN processing API used in the ATM (cash machine) network. This API controls access to the tamper-resistant Hardware Security Modules where PIN encryption, decryption and verification takes place. The~attacks are differential attacks, whereby an attacker gains information about the plaintext values of encrypted customer PINs by making changes to the non-confidential inputs to a command. Our~proposed fix adds an integrity check to the parameters passed to the command. It~is novel in that it involves very little change to the existing ATM network infrastructure.} }

@inproceedings{KMT-asian09, address = {Seoul, Korea}, month = dec, year = 2009, volume = 5913, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Datta, Anupam}, acronym = {{ASIAN}'09}, booktitle = {{P}roceedings of the 13th {A}sian {C}omputing {S}cience {C}onference ({ASIAN}'09)}, author = {Kremer, Steve and Mercier, Antoine and Treinen, Ralf}, title = {Reducing Equational Theories for the Decision of Static Equivalence}, pages = {94-108}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KMT-asian09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KMT-asian09.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/KMT-asian09.ps}, doi = {10.1007/978-3-642-10622-4_8}, abstract = {Static equivalence is a well established notion of indistinguishability of sequences of terms which is useful in the symbolic analysis of cryptographic protocols. Static equivalence modulo equational theories allows a more accurate representation of cryptographic primitives by modelling properties of operators by equational axioms. We develop a method that allows in some cases to simplify the task of deciding static equivalence in a multi-sorted setting, by removing a symbol from the term signature and reducing the problem to several simpler equational theories. We illustrate our technique at hand of bilinear pairings.} }

@inproceedings{AF-ijcai09, address = {Pasadena, California, USA}, month = jul, year = 2009, publisher = {AAAI Press}, editor = {Boutilier, Craig}, acronym = {{IJCAI}'09}, booktitle = {{P}roceedings of the 21st {I}nternational {J}oint {C}onference on {A}rtificial {I}ntelligence ({IJCAI}'09)}, author = {Areces, Carlos and Figueira, Diego}, title = {Which Semantics for Neighbourhood Semantics?}, pages = {671-676}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AF-ijcai09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AF-ijcai09.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/AF-ijcai09.ps}, abstract = {In this article we discuss two alternative proposals for neighbourhood semantics (which we call strict and loose neighbourhood semantics, NSS~and~NSL respectively) that have been previously introduced in the literature. Our~main tools are suitable notions of bisimulation. While an elegant notion of bisimulation exists for NSL, the required bisimulation for NSS is rather involved. We~propose a simple extension of NSS with a universal modality that we call NSS(E), which comes together with a natural notion of bisimulation. We~also investigate the complexity of the satisfiability problem for NSL and NSS(E).} }

@techreport{LSV:09:16, author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge and Sassolas, Mathieu}, title = {Verification on Interrupt Timed Automata}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2009}, month = jul, type = {Research Report}, number = {LSV-09-16}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-16.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-16.pdf}, note = {16~pages}, abstract = {The class of Interrupt Timed Automata (ITA) has been introduced to model multi-task systems with interruptions in a single processor environment. This is a subclass of hybrid automata in which real valued variables consist of a restricted type of stopwatches (variables with rate \(0\) or~\(1\)) organized along levels. While reachability is undecidable with usual stopwatches, it was proved that this problem is decidable in ITA and that untimed languages of ITA are effectively regular. Here we investigate the problem of model checking timed extensions of CTL over ITA and show in contrast that this problem is undecidable. On~the other hand, we prove that model checking is decidable for two relevant fragments of this timed logic: (1)~the~first one where formula contain only model clocks and (2)~the~second one where formulas have a single external clock.} }

@techreport{LSV:09:15, author = {H{\'e}am, Pierre-Cyrille and Nicaud, Cyril}, title = {Seed: an Easy-to-Use Random Generator of Recursive Data Structures for Testing}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2009}, month = jul, type = {Research Report}, number = {LSV-09-15}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-15.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-15.pdf}, note = {16~pages}, abstract = {Random testing represents a simple and tractable way for software assessment. This paper presents the Seed tool dedicated to the uniform random generation of recursive data structures as labelled trees or logical formulas. We show how Seed can be used in several testing contexts, from model based testing to performance testing. Generated data structures are defined by grammar-like rules, given in an XML format, multiplying Seed possible applications. Seed is based on combinatorial techniques, and can generate uniformly at random \(k\)~structures of size~\(n\) with a time complexity in \(O(n^{2}+ kn\cdot \log(n))\). Finally, Seed is available as a free java application and a great effort has been made to make it easy-to-use.} }

@techreport{LSV:09:13, author = {Andr{\'e}, {\'E}tienne and Encrenaz, Emmanuelle and Fribourg, Laurent}, title = {Synthesizing Parametric Constraints on Various Case Studies Using {IMITATOR}}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2009}, month = jun, type = {Research Report}, number = {LSV-09-13}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-13.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-13.pdf}, note = {18~pages}, abstract = {We present here applications of IMITATOR, a tool for synthesizing constraints on timing bounds (seen as parameters) in the framework of timed automata. Unlike classical synthesis methods, we take advantage of a given reference valuation of the parameters for which the system is known to behave properly. Our aim is to generate a constraint such that, under any valuation satisfying this constraint, the system is guaranteed to behave, in terms of alternating sequences of locations and actions, as under the reference valuation. This is useful for safely relaxing some values of the reference valuation, and optimizing timing bounds of the system. We have successfully applied our tool to various examples of asynchronous circuits and protocols, which are detailed in this report.} }

@inproceedings{BFSP-infinity09, address = {Bologna, Italy}, month = nov, year = 2009, volume = 10, series = {Electronic Proceedings in Theoretical Computer Science}, editor = {Farzan, Azadeh and Legay, Axel}, acronym = {{INFINITY}'09}, booktitle = {{P}roceedings of the 11th {I}nternational {W}orkshops on {V}erification of {I}nfinite {S}tate {S}ystems ({INFINITY}'09)}, author = {Bouchy, Florent and Finkel, Alain and San{ }Pietro, Pierluigi}, title = {Dense-choice Counter Machines Revisited}, pages = {3-22}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFSP-infinity09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFSP-infinity09.pdf}, doi = {10.4204/EPTCS.10.1}, abstract = {This paper clarifies the picture about Dense-choice Counter Machines, which have been less studied than (discrete) Counter Machines. We revisit the definition of {"}Dense Counter Machines{"} so that it now extends (discrete) Counter Machines, and we provide new undecidability and decidability results. Using the first-order additive mixed theory of reals and integers, we give a logical characterization of the sets of configurations reachable by reversal-bounded Dense-choice Counter Machines.} }

@inproceedings{AF-infinity09, address = {Bologna, Italy}, month = nov, year = 2009, volume = 10, series = {Electronic Proceedings in Theoretical Computer Science}, editor = {Farzan, Azadeh and Legay, Axel}, acronym = {{INFINITY}'09}, booktitle = {{P}roceedings of the 11th {I}nternational {W}orkshops on {V}erification of {I}nfinite {S}tate {S}ystems ({INFINITY}'09)}, author = {Andr{\'e}, {\'E}tienne and Fribourg, Laurent}, title = {An Inverse Method for Policy-Iteration Based Algorithms}, pages = {44-61}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AF-infinity09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AF-infinity09.pdf}, doi = {10.4204/EPTCS.10.4}, abstract = {We present an extension of two policy-iteration based algorithms on weighted graphs (viz.,~Markov Decision Problems and Max-Plus Algebras). This extension allows us to solve the following inverse problem: considering the weights of the graph to be unknown constants or parameters, we suppose that a reference instantiation of those weights is given, and we aim at computing a constraint on the parameters under which an optimal policy for the reference instantiation is still optimal. The original algorithm is thus guaranteed to behave well around the reference instantiation, which provides us with some criteria of robustness. We present an application of both methods to simple examples. A prototype implementation has been done.} }

@inproceedings{BCLD-asian09, address = {Seoul, Korea}, month = dec, year = 2009, volume = 5913, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Datta, Anupam}, acronym = {{ASIAN}'09}, booktitle = {{P}roceedings of the 13th {A}sian {C}omputing {S}cience {C}onference ({ASIAN}'09)}, author = {Bursuc, Sergiu and Delaune, St{\'e}phanie and Comon{-}Lundh, Hubert}, title = {Deducibility constraints}, pages = {24-38}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCD-asian09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCD-asian09.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCD-asian09.ps}, doi = {10.1007/978-3-642-10622-4_3}, abstract = {In their work on tractable deduction systems, D.~McAllester and later D.~Basin and H.~Ganzinger have identified a property of inference systems (the~locality property) that ensures the tractability of the \textit{Entscheidungsproblem}.\par On~the other hand, deducibility constraints are sequences of deduction problems in which some parts (formulas) are unknown. The~problem is to decide their satisfiability and to represent the set of all possible solutions. Such constraints have also been used for deciding some security properties of cryptographic protocols.\par In this paper we show that local inference systems (actually a slight modification of such systems) yield not only a tractable deduction problem, but also decidable deducibility constraints. Our algorithm not only allows to decide the existence of a solution, but also gives a representation of all solutions.} }

@incollection{ACL-fps09, noaddress = {}, month = may, year = 2009, volume = 5458, series = {Lecture Notes in Computer Science}, publisher = {Springer}, noacronym = {}, booktitle = {{F}ormal to {P}ractical {S}ecurity}, editor = {Cortier, V{\'e}ronique and Kirchner, Claude and Okada, Mitsuhiro and Sakurada, Hideki}, author = {Affeldt, Reynald and Comon{-}Lundh, Hubert}, title = {Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables}, pages = {1-20}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACL-fps09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACL-fps09.pdf}, doi = {10.1007/978-3-642-02002-5_1}, abstract = {First-order logic resolution is a standard way to automate the verification of security protocols. However, it sometimes fails to produce security proofs for secure protocols because of the detection of false attacks. For the verification of a bounded number of sessions, false attacks can be avoided by introducing rigid variables. Unfortunately, this yields complicated resolution procedures. We show here that there is a simple translation of the security problem for a bounded number of sessions into first-order logic, that does not introduce false attacks. This is shown by translating clauses involving rigid variables into classical first-order clauses, while preserving satisfiability. We illustrate this approach by giving a complete and terminating strategy for a first-order logic fragment resulting from the above translation, that yields a decision procedure for a bounded number of sessions.} }

@inproceedings{HMY-msr09, address = {Nantes, France}, month = nov, year = 2009, number = {7-9}, volume = {43}, series = {Journal Europ{\'e}en des Syst{\`e}mes Automatis{\'e}s}, publisher = {Herm{\`e}s}, editor = {Lime, Didier and Roux, Olivier H.}, acronym = {{MSR}'09}, booktitle = {{A}ctes du 7{\`e}me {C}olloque sur la {M}od{\'e}lisation des {S}yst{\`e}mes {R}{\'e}actifs ({MSR}'09)}, author = {Haddad, Serge and Mokdad, Lynda and Youcef, Samir}, title = {Bornes du temps de r{\'e}ponse des services Web composites}, pages = {969-983}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HMY-msr09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HMY-msr09.pdf}, abstract = {The quality of service (QoS) of Web services is a key factor of their success. This requires to design new methods in order to study~it. Here we propose families of upper bounding models for the response time of composite Web services for two kinds of composition: the statical and random {"}fork and merge{"}. In~the first~case, the~complexity of bounding models belongs to~\(O(n\cdot \sqrt{n})\) where \(n\)~is the number of called services whereas the complexity of the exact model belongs to~\(O(n^2)\). In~the second~case, the~complexity of bounding models still belongs to~\(O(n\cdot \sqrt{n})\) whereas the complexity of the exact model belongs to~\(O(n^3)\). Furthermore, having a family of bounding models allows to choose the bounding model depending on the parameters of the exact model. The numerical results show the interest of our approach w.r.t. complexity and accuracy of the bound.} }

@inproceedings{ACDFR-msr09, address = {Nantes, France}, month = nov, year = 2009, number = {7-9}, volume = {43}, series = {Journal Europ{\'e}en des Syst{\`e}mes Automatis{\'e}s}, publisher = {Herm{\`e}s}, editor = {Lime, Didier and Roux, Olivier H.}, acronym = {{MSR}'09}, booktitle = {{A}ctes du 7{\`e}me {C}olloque sur la {M}od{\'e}lisation des {S}yst{\`e}mes {R}{\'e}actifs ({MSR}'09)}, author = {Andr{\'e}, {\'E}tienne and Chatain, {\relax Th}omas and De{ }Smet, Olivier and Fribourg, Laurent and Ruel, Silvain}, title = {Synth{\`e}se de contraintes temporis{\'e}es pour une architecture d'automatisation en r{\'e}seau}, pages = {1049-1064}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACDFR-msr09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACDFR-msr09.pdf}, abstract = {We deal with the problem of synthesis of timing constraints for concurrent systems. Such systems are modeled by networks of timed automata where some constants, represented as parameters, can be tuned. A suitable value of these parameters is assumed to be known from a preliminarily simulation process. We present a method which infers a zone of suitable points around this reference functioning point. This zone is defined by a system of linear inequalities over the parameters. This method is applied to the case study of a networked automation system.} }

@inproceedings{ABC-cav09, address = {Grenoble, France}, month = jun # {-} # jul, year = 2009, volume = 5643, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Bouajjani, Ahmad and Maler, Oded}, acronym = {{CAV}'09}, booktitle = {{P}roceedings of the 21st {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV}'09)}, author = {Abadi, Mart{\'\i}n and Blanchet, Bruno and Comon{-}Lundh, Hubert}, title = {Models and Proofs of Protocol Security: A~Progress Report}, pages = {35-49}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABC-cav09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABC-cav09.pdf}, doi = {10.1007/978-3-642-02658-4_5}, abstract = {This paper discusses progress in the verification of security protocols. Focusing on a small, classic example, it stresses the use of program-like representations of protocols, and their automatic analysis in symbolic and computational models.} }

@inproceedings{CDL-adhs09, address = {Zaragoza, Spain}, month = sep, year = 2009, editor = {Giua, Alessandro and Silva, Manuel and Zaytoon, Janan}, acronym = {{ADHS}'09}, booktitle = {{P}roceedings of the 3rd {IFAC} {C}onference on {A}nalysis and {D}esign of {H}ybrid {S}ystems ({ADHS}'09)}, author = {Chatain, {\relax Th}omas and David, Alexandre and Larsen, Kim G.}, title = {Playing Games with Timed Games}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDL-adhs09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDL-adhs09.pdf}, abstract = {In this paper we focus on property-preserving preorders between timed game automata and their application to control of partially observable systems. Following the example of timed simulation between timed automata, we define timed alternating simulation as a preorder between timed game automata, which preserves controllability. We define a method to reduce the timed alternating simulation problem to a safety game. We show how timed alternating simulation can be used to control efficiently a partially observable system. This method is illustrated by a generic case study.} }

@inproceedings{BHK-rp09, address = {Palaiseau, France}, month = sep, year = 2009, volume = 5797, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Bournez, Olivier and Potapov, Igor}, acronym = {{RP}'09}, booktitle = {{P}roceedings of the 3rd {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'09)}, author = {Boichut, Yohan and H{\'e}am, Pierre-Cyrille and Kouchnarenko, Olga}, title = {How to Tackle Integer Weighted Automata Positivity}, pages = {79-92}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHK-rp09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHK-rp09.pdf}, doi = {10.1007/978-3-642-04420-5_9}, abstract = {This paper is dedicated to candidate abstractions to capture relevant aspects of the integer weighted automata. The expected effect of applying these abstractions is studied to build the deterministic reachability graphs allowing us to semi-decide the positivity problem on these automata. Moreover, the papers reports on the implementations and experimental results, and discusses other encodings.} }

@article{BCHK-ijfcs09, publisher = {World Scientific}, journal = {International Journal of Foundations of Computer Science}, author = {Boichut, Yohan and Courbis, Rom{\'e}o and H{\'e}am, Pierre-Cyrille and Kouchnarenko, Olga}, title = {Handling Non-left Linear Rules when Completing Tree Automata}, volume = 20, number = 5, pages = {837-849}, year = 2009, month = oct, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCHK-ijfcs09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCHK-ijfcs09.pdf}, doi = {10.1142/S0129054109006917}, abstract = {This paper addresses the following general problem of tree regular model-checking: decide whether \(\mathcal{R}^*(\mathcal{L}) \cap \mathcal{L}_p = \emptyset\) where \(\mathcal{R}^*\) is the reflexive and transitive closure of a successor relation induced by a term rewriting system~\(\mathcal{R}\), and \(\mathcal{L}\) and~\(\mathcal{L}_p\) are both regular tree languages. We~develop an automatic approximation-based technique to handle this---undecidable in general---problem in the case when term rewriting system rules are non left-linear.} }

@article{BDL-apal09, publisher = {Elsevier Science Publishers}, journal = {Annals of Pure and Applied Logics}, author = {Brochenin, R{\'e}mi and Demri, St{\'e}phane and Lozes, {\'E}tienne}, title = {Reasoning about sequences of memory states}, volume = {161}, number = {3}, pages = {305-323}, year = 2009, month = dec, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDL-apal09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDL-apal09.pdf}, doi = {10.1016/j.apal.2009.07.004}, 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_1^0\)-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{BCDL-formats09, address = {Budapest, Hungary}, month = sep, year = 2009, volume = 5813, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Ouaknine, Jo{\"e}l and Vaandrager, Frits}, acronym = {{FORMATS}'09}, booktitle = {{P}roceedings of the 7th {I}nternational {C}onference on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'09)}, author = {Bulychev, Peter and Chatain, {\relax Th}omas and David, Alexandre and Larsen, Kim G.}, title = {Checking simulation relation between timed game automata}, pages = {73-87}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCDL-formats09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCDL-formats09.pdf}, doi = {10.1007/978-3-642-04368-0_8}, abstract = {In this paper we focus on property-preserving preorders between timed game automata and their application to control of partially observable systems. We define timed weak alternating simulation as a preorder between timed game automata, which preserves controllability. We define the rules of building a symbolic turn-based two-player game such that the existence of a winning strategy is equivalent to the simulation being satisfied. We also propose an on-the-fly algorithm for solving this game. This simulation checking method can be applied to the case of non-alternating or strong simulations as well. We illustrate our algorithm by a case study and report on results.} }

@inproceedings{HP-qest09, address = {Budapest, Hungary}, month = sep, year = 2009, publisher = {{IEEE} Computer Society Press}, acronym = {{QEST}'09}, booktitle = {{P}roceedings of the 6th {I}nternational {C}onference on {Q}uantitative {E}valuation of {S}ystems ({QEST}'09)}, author = {Haddad, Serge and Pekergin, Nihal}, title = {Using Stochastic Comparison for Efficient Model Checking of Uncertain {M}arkov Chains}, pages = {177-186}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HP-qest09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HP-qest09.pdf}, doi = {10.1109/QEST.2009.42}, abstract = {We consider model checking of Discrete Time Markov Chains~(DTMC) with transition probabilities which are not exactly known but lie in a given interval. Model checking a Probabilistic Computation Tree Logic~(PCTL) formula for interval-valued DTMCs~(IMC) has been shown to be NP hard and co-NP hard. Since the state space of a realistic DTMC is generally huge, these lower bounds prevent the application of exact algorithms for such models. Therefore we propose to apply the stochastic comparison method to check an extended version of PCTL for IMCs. More precisely, we first design linear time algorithms to quantitatively analyze IMCs. Then we develop an efficient, semi-decidable PCTL model checking procedure for IMCs. Furthermore, our procedure returns more refined answers than traditional ones: YES, NO, DON'T~KNOW. Thus we may provide useful partial information for modelers in the {"}DON'T~KNOW{"} case.} }

@inproceedings{CFLS-esorics09, address = {Saint~Malo, France}, month = sep, year = 2009, volume = 5789, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Backes, Michael and Ning, Peng}, acronym = {{ESORICS}'09}, booktitle = {{P}roceedings of the 14th {E}uropean {S}ymposium on {R}esearch in {C}omputer {S}ecurity ({ESORICS}'09)}, author = {Centenaro, Matteo and Focardi, Riccardo and Luccio, Flaminia L. and Steel, Graham}, title = {Type-based Analysis of {PIN} Processing {API}s}, pages = {53-68}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CFLS-esorics09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CFLS-esorics09.pdf}, doi = {10.1007/978-3-642-04444-1_4}, abstract = {We examine some known attacks on the PIN verification framework, based on weaknesses of the security API for the tamper-resistant Hardware Security Modules used in the network. We specify this API in an imperative language with cryptographic primitives, and show how its flaws are captured by a notion of robustness that extends the one of Myers, Sabelfeld and Zdancewic to our cryptographic setting. We~propose an improved API, give an extended type system for assuring integrity and for preserving confidentiality via randomized and non-randomized encryptions, and show our new API to be type-checkable.} }

@inproceedings{CS-esorics09, address = {Saint~Malo, France}, month = sep, year = 2009, volume = 5789, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Backes, Michael and Ning, Peng}, acronym = {{ESORICS}'09}, booktitle = {{P}roceedings of the 14th {E}uropean {S}ymposium on {R}esearch in {C}omputer {S}ecurity ({ESORICS}'09)}, author = {Cortier, V{\'e}ronique and Steel, Graham}, title = {A~generic security {API} for symmetric key management on cryptographic devices}, pages = {605-620}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-esorics09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-esorics09.pdf}, doi = {10.1007/978-3-642-04444-1_37}, abstract = {Security APIs are used to define the boundary between trusted and untrusted code. The security properties of existing APIs are not always clear. In~this paper, we~give a new generic API for managing symmetric keys on a trusted cryptographic device. We state and prove security properties for our API. In~particular, our API offers a high level of security even when the host machine is controlled by an attacker. Our API is generic in the sense that it can implement a wide variety of (symmetric~key) protocols. As a proof of concept, we give an algorithm for automatically instantiating the API commands for a given key management protocol. We demonstrate the algorithm on a set of key establishment protocols from the Clark-Jacob suite.} }

@article{CAM-jcss09, publisher = {Elsevier Science Publishers}, journal = {Journal of Computer and System Sciences}, author = {Cautis, Bogdan and Abiteboul, Serge and Milo, Tova}, title = {Reasoning about {XML} update constraints}, month = sep, year = 2009, volume = 75, number = 6, pages = {336-358}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CAM-jcss09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CAM-jcss09.pdf}, doi = {10.1016/j.jcss.2009.02.001}, abstract = {We introduce in this paper a class of constraints for describing how an XML document can evolve, namely \emph{XML update constraints}. For these constraints, we~study the implication problem, giving algorithms and complexity results for constraints of varying expressive power. Besides classical constraint implication, we also consider an instance-based approach in which we take into account data. More precisely, we study implication with respect to a current tree instance, resulting from a series of unknown updates. The main motivation of our work is reasoning about data integrity under update restrictions in contexts where owners may lose control over their data, such as in publishing or exchange.} }

@inproceedings{FS-mfcs09, address = {Novy Smokovec, Slovakia}, month = aug, year = 2009, volume = 5734, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Kr{\'a}lovi{\v c}, Rastislav and Niwi{\'n}ski, Damian}, acronym = {{MFCS}'09}, booktitle = {{P}roceedings of the 34th {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'09)}, author = {Figueira, Diego and Segoufin, Luc}, title = {Future-looking logics on data words and trees}, pages = {331-343}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-mfcs09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-mfcs09.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FS-mfcs09.ps}, doi = {10.1007/978-3-642-03816-7_29}, abstract = {In a data word or a data tree each position carries a label from a finite alphabet and a data value from an infinite domain. These models have been considered in the realm of semistructured data, timed automata and extended temporal logics.\par Over data words we consider the logic 1-reg-LTL(\(\textbf{F}\)), that extends LTL(\(\textbf{F}\)) with one register for storing data values for later comparisons. We show that satisfiability over data words of 1-reg-LTL(\(\textbf{F}\)) is already not primitive recursive. We also show that the extension of 1-reg-LTL(\(\textbf{F}\)) with either the reverse modality \(\textbf{F}^{-1}\) or with one extra register is undecidable. All those lower bounds were already known for 1-reg-LTL(\(\textbf{X}\),\(\textbf{F}\)) and our results essentially show that the \(\textbf{X}\) modality was not necessary.\par Moreover we show that over data trees similar lower bounds hold for certain fragments of XPATH.} }

@article{DG-jlc09, publisher = {Oxford University Press}, journal = {Journal of Logic and Computation}, author = {Demri, St{\'e}phane and Gascon, R{\'e}gis}, title = {The Effects of Bounding Syntactic Resources on {P}resburger {LTL}}, pages = {1541-1575}, volume = {19}, number = {6}, month = dec, year = 2009, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DG-jlc09.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DG-jlc09.pdf}, doi = {10.1093/logcom/exp037}, abstract = {LTL over Presburger constraints is the extension of LTL where the atomic formulae are quantifier-free Presburger formulae having as free variables the counters at different states of the model. This logic is known to admit undecidable satisfiability and model-checking problems. We~study decidability and complexity issues for fragments of LTL with Presburger constraints obtained by restricting the syntactic resources of the formulae (the number of variables, the maximal distance between two states for which counters can be compared and, to a smaller extent, the set of Presburger constraints) while preserving the strength of the logical operators. We~provide a complete picture refining known results from the literature. We~show that model-checking and satisfiability problems for the fragments of LTL with difference constraints restricted to two variables and distance one and to one variable and distance two are highly undecidable, enlarging significantly the class of known undecidable fragments. On the positive side, we prove that the fragment restricted to one variable and to distance one augmented with propositional variables is \textsc{pspace}-complete. Since the atomic formulae can state quantitative properties on the counters, this extends some results about model-checking pushdown systems and one-counter automata. In~order to establish the pspace upper bound, we show that the nonemptiness problem for B{\"u}chi one-counter automata taking values in~\(\mathbb{Z}\) and allowing zero tests and sign tests, is~only \textsc{nlogspace}-complete. Finally, we~establish that model-checking one-counter automata with complete quantifier-free Presburger LTL restricted to one variable is also \textsc{pspace}-complete whereas the satisfiability problem is undecidable.} }

@inproceedings{KAS-arspawits09, address = {York, UK}, month = aug, year = 2009, volume = 5511, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Degano, Pierpaolo and Vigan{\`o}, Luca}, acronym = {{ARSPA-WITS}'09}, booktitle = {{R}evised {S}elected {P}apers of the {J}oint {W}orkshop on {A}utomated {R}easoning for {S}ecurity {P}rotocol {A}nalysis and {I}ssues in the {T}heory of {S}ecurity ({ARSPA-WITS}'09)}, author = {Keighren, Gavin and Aspinall, David and Steel, Graham}, title = {Towards a Type System for Security {API}s}, pages = {173-192}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KAS-arspawits09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KAS-arspawits09.pdf}, doi = {10.1007/978-3-642-03459-6_12}, abstract = {Security API analysis typically only considers a subset of an API's functions, with results bounded by the number of function calls. Furthermore, attacks involving partial leakage of sensitive information are usually not covered. Type-based static analysis has the potential to alleviate these shortcomings. To that end, we present a type system for secure information flow based upon the one of Volpano, Smith and Irvine, extended with types for cryptographic keys and ciphertext similar to those in Sumii and Pierce. In~contrast to some other type systems, the encryption and decryption of keys does not require special treatment. We show that a well-typed sequence of commands is non-interferent, based upon a definition of indistinguishability where, in certain circumstances, the adversary can distinguish between ciphertexts that correspond to encrypted public data.} }

@inproceedings{FS-arspawits09, address = {York, UK}, month = aug, year = 2009, volume = 5511, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Degano, Pierpaolo and Vigan{\`o}, Luca}, acronym = {{ARSPA-WITS}'09}, booktitle = {{R}evised {S}elected {P}apers of the {J}oint {W}orkshop on {A}utomated {R}easoning for {S}ecurity {P}rotocol {A}nalysis and {I}ssues in the {T}heory of {S}ecurity ({ARSPA-WITS}'09)}, author = {Fr{\"o}schle, Sibylle and Steel, Graham}, title = {Analysing {PKCS}\#11 Key Management {API}s with Unbounded Fresh Data}, pages = {92-106}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-arspawits09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-arspawits09.pdf}, doi = {10.1007/978-3-642-03459-6_7}, abstract = {We extend Delaune, Kremer and Steel's framework for analysis of PKCS#11-based APIs from bounded to unbounded fresh data. We achieve this by: formally defining the notion of an \emph{attribute policy}; showing that a well-designed API should have a certain class of policy we call \emph{complete}; showing that APIs with complete policies may be safely abstracted to APIs where the attributes are fixed; and proving that these \emph{static} APIs can be analysed in a small bounded model such that security properties will hold for the unbounded case. We automate analysis in our framework using the SAT-based security protocol model checker SATMC. We show that a symmetric key management subset of the Eracom PKCS#11 API, used in their ProtectServer product, preserves the secrecy of sensitive keys for unbounded numbers of fresh keys and \emph{handles}, i.e.~pointers to keys. We also show that this API is not robust: if~an encryption key is lost to the intruder, SATMC finds an attack whereby all the keys may be compromised.} }

@inproceedings{CDK-secret09, address = {Port Jefferson, New~York, USA}, month = jul, year = 2009, editor = {Comon{-}Lundh, Hubert and Meadows, Catherine}, acronym = {{SecReT}'09}, booktitle = {{P}reliminary {P}roceedings of the 4th {I}nternational {W}orkshop on {S}ecurity and {R}ewriting {T}echniques ({SecReT}'09)}, author = {Ciob{\^a}c{\u{a}}, {\c{S}}tefan and Delaune, St{\'e}phanie and Kremer, Steve}, title = {Computing knowledge in security protocols under convergent equational theories}, pages = {47-58}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDK-secret09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDK-secret09.pdf}, abstract = {We propose a procedure for the intruder deduction problem and for the static equivalence problem, in the case where cryptographic primitives are modeled by a convergent equational theory. Our~procedure terminates on a wide range of equational theories. In~particular, we~obtain a new decidability result for a theory of trapdoor commitment that we encountered in the study of e-voting protocols. We~also provide a prototype implementation.} }

@inproceedings{ACD-secret09, address = {Port Jefferson, New~York, USA}, month = jul, year = 2009, editor = {Comon{-}Lundh, Hubert and Meadows, Catherine}, acronym = {{SecReT}'09}, booktitle = {{P}reliminary {P}roceedings of the 4th {I}nternational {W}orkshop on {S}ecurity and {R}ewriting {T}echniques ({SecReT}'09)}, author = {Arnaud, Mathilde and Cortier, V{\'e}ronique and Delaune, St{\'e}phanie}, title = {Modeling and Verifying Ad Hoc Routing Protocol}, pages = {33-46}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACD-secret09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACD-secret09.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ACD-secret09.ps}, abstract = {Mobile ad hoc networks consist of mobile wireless devices which autonomously organize their infrastructure. In~such a network, a~central issue, ensured by routing protocols, is to find a route from one device to another. Those protocols use cryptographic mechanisms in order to prevent a malicious node from compromising the discovered route.\par We present a calculus for modeling and reasoning about security protocols, including in particular secured routing protocols. Our calculus extends standard symbolic models to take into account the characteristics of routing protocols and to model wireless communication in a more accurate way. Then, by using constraint solving techniques, we propose a decision procedure for analyzing routing protocols for a bounded number of sessions and for a fixed network topology. We~demonstrate the usage and usefulness of our approach by analyzing the protocol SRP applied to~DSR.} }

@inproceedings{KMT-secret09, address = {Port Jefferson, New~York, USA}, month = jul, year = 2009, editor = {Comon{-}Lundh, Hubert and Meadows, Catherine}, acronym = {{SecReT}'09}, booktitle = {{P}reliminary {P}roceedings of the 4th {I}nternational {W}orkshop on {S}ecurity and {R}ewriting {T}echniques ({SecReT}'09)}, author = {Kremer, Steve and Mercier, Antoine and Treinen, Ralf}, title = {Reducing Equational Theories for the Decision of Static Equivalence (Preliminary Version)}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KMT-secret09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KMT-secret09.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/KMT-secret09.ps}, abstract = {Static equivalence is a well established notion of indistinguishability of sequences of terms which is useful in the symbolic analysis of cryptographic protocols. Static equivalence modulo equational theories allows a more accurate representation of cryptographic primitives by modelling properties of operators by equational axioms. We develop a method that allows in some cases to simplify the task of deciding static equivalence in a multi-sorted setting, by removing a symbol from the term signature and reducing the problem to several simpler equational theories. We illustrate our technique at hand of bilinear pairings.} }

@article{ACEF-ijfcs09, publisher = {World Scientific}, journal = {International Journal of Foundations of Computer Science}, author = {Andr{\'e}, {\'E}tienne and Chatain, {\relax Th}omas and Encrenaz, Emmanuelle and Fribourg, Laurent}, title = {An Inverse Method for Parametric Timed Automata}, volume = 20, number = 5, pages = {819-836}, month = oct, year = 2009, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACEF-ijfcs09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACEF-ijfcs09.pdf}, doi = {10.1142/S0129054109006905}, abstract = {We consider in this paper systems modeled by timed automata. The timing bounds involved in the action guards and location invariants of our timed automata are not constants, but parameters. Those parametric timed automata allow the modelling of various kinds of timed systems, \textit{e.g.} communication protocols or asynchronous circuits. We will also assume that we are given an initial tuple~\(\pi_0\) of values for the parameters, which corresponds to values for which the system is known to behave properly. Our goal is to compute a constraint~\(K_0\) on the parameters, satisfied by~\(\pi_0\), guaranteeing that, under any parameter valuation satisfying~\(K_0\), the system behaves in the same manner: for any two parameter valuations satisfying~\(K_0\), the behaviors of the timed automata are (time-abstract) equivalent, \textit{i.e.}, the traces of execution viewed as alternating sequences of actions and locations are identical. We present an algorithm \texttt{InverseMethod} that terminates in the case of acyclic models, and discuss how to extend it in the cyclic case. We also explain how to combine our method with classical synthesis methods which are based on the avoidance of a given set of bad states. A prototype implementation has been done, and various experiments are described.} }

@techreport{LSV:09:09, author = {Goubault{-}Larrecq, Jean}, title = {On a Generalization of a Result by {V}alk and {J}antzen}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2009}, month = may, type = {Research Report}, number = {LSV-09-09}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-09.pdf}, note = {18~pages}, abstract = {We~show that, under mild assumptions on the effective, well quasi-ordered set~\(X\), one~can compute a finite basis of an upward-closed subset~\(U\) of~\(X\) if and only if one can decide whether \(U \cap \downarrow z\) is empty for every \(z \in \widehat{X}\). Here \(\widehat{X}\) is the completion of \(X\) as defined in Finkel and Goubault-Larrecq, {\em Forward Analysis for WSTS, Part~{I:} Completions}, STACS'09, pages 433-444, 2009. This generalizes a useful result proved by Valk and Jantzen in~1985, which is the case \(X = \\mathbb{N}^k\).} }

@inproceedings{RBH-formats09, address = {Budapest, Hungary}, month = sep, year = 2009, volume = 5813, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Ouaknine, Jo{\"e}l and Vaandrager, Frits}, acronym = {{FORMATS}'09}, booktitle = {{P}roceedings of the 7th {I}nternational {C}onference on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'09)}, author = {Bouillard, Anne and Haar, Stefan and Rosario, Sidney}, title = {Critical paths in the Partial Order Unfolding of a Stochastic {P}etri Net}, pages = {43-57}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-formats09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-formats09.pdf}, doi = {10.1007/978-3-642-04368-0_6}, abstract = {In concurrent real-time processes, the speed of individual components has a double impact: on the one hand, the overall latency of a compound process is affected by the latency of its components. But, if the composition has race conditions, the very outcome of the process will also depend on the latency of component processes. Using stochastic Petri nets, we investigate the probability of a transition occurrence being critical for the entire process, i.e. such that a small increase or decrease of the duration of the occurrence entails an increase or decrease of the total duration of the process. The first stage of the analysis focuses on occurrence nets, as obtained by partial order unfoldings, to determine criticality of events; we then lift to workflow nets to investigate criticality of transitions inside a workflow.} }

@inproceedings{LA-ictac09, address = {Kuala Lumpur, Malaysia}, month = aug, year = 2009, volume = 5684, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Leucker, Martin and Morgan, Carroll}, acronym = {{ICTAC}'09}, booktitle = {{P}roceedings of the 6th {I}nternational {C}olloquium on {T}heoretical {A}spects of {C}omputing ({ICTAC}'09)}, author = {Longuet, Delphine and Aiguier, Marc}, title = {Integration Testing from Structured First-Order Specifications via Deduction Modulo}, pages = {261-276}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LA-ictac09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LA-ictac09.pdf}, doi = {10.1007/978-3-642-03466-4_17}, abstract = {Testing from first-order specifications has mainly been studied for flat specifications, that are specifications of a single software module. However, the specifications of large software systems are generally built out of small specifications of individual modules, by enriching their union. The aim of integration testing is to test the composition of modules assuming that they have previously been verified, i.e. assuming their correctness. One of the main method for the selection of test cases from first-order specifications, called axiom unfolding, is based on a proof search for the different instances of the property to be tested, thus allowing the coverage of this property. The idea here is to use deduction modulo as a proof system for structured first-order specifications in the context of integration testing, so as to take advantage of the knowledge of the correctness of the individual modules.} }

@inproceedings{andre-ictac09, address = {Kuala Lumpur, Malaysia}, month = aug, year = 2009, volume = 5684, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Leucker, Martin and Morgan, Carroll}, acronym = {{ICTAC}'09}, booktitle = {{P}roceedings of the 6th {I}nternational {C}olloquium on {T}heoretical {A}spects of {C}omputing ({ICTAC}'09)}, author = {Andr{\'e}, {\'E}tienne}, title = {{IMITATOR}: A~Tool for Synthesizing Constraints on Timing Bounds of Timed Automata}, pages = {336-342}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/andre-ictac09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/andre-ictac09.pdf}, doi = {10.1007/978-3-642-03466-4_22}, abstract = {We present here Imitator, a tool for synthesizing constraints on timing bounds (seen as parameters) in the framework of timed automata. Unlike classical synthesis methods, we take advantage of a given reference valuation of the parameters for which the system is known to behave properly. Our aim is to generate a constraint such that, under any valuation satisfying this constraint, the system is guaranteed to behave, in terms of alternating sequences of locations and actions, as under the reference valuation. This is useful for safely relaxing some values of the reference valuation, and optimizing timing bounds of the system. We have successfully applied our tool to various examples of asynchronous circuits and protocols.} }

@inproceedings{BRBH-atpn09, address = {Paris, France}, month = jun, year = 2009, volume = 5606, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Franceschinis, Giuliana and Wolf, Karsten}, acronym = {{PETRI~NETS}'09}, booktitle = {{P}roceedings of the 30th {I}nternational {C}onference on {A}pplications and {T}heory of {P}etri {N}ets ({PETRI~NETS}'09)}, author = {Bouillard, Anne and Rosario, Sidney and Benveniste, Albert and Haar, Stefan}, title = {Monotonicity in Service Orchestrations}, pages = {263-282}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BRBH-atpn09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BRBH-atpn09.pdf}, doi = {10.1007/978-3-642-02424-5_16}, abstract = {Web Service orchestrations are compositions of different Web Services to form a new service. The services called during the orchestration guarantee a given performance to the orchestrater, usually in the form of contracts.\par These contracts can be used by the orchestrater to deduce the contract it can offer to its own clients, by performing contract composition. An implicit assumption in contract based QoS management is: {"}the better the component services perform, the better the orchestration's performance will~be{"}. Thus, contract based QoS management for Web services orchestrations implicitly assumes monotony.\par In some orchestrations, however, monotony can be violated, i.e., the performance of the orchestration improves when the performance of a component service degrades. This is highly undesirable since it can render the process of contract composition inconsistent.\par In this paper we define monotony for orchestrations modelled by Colored Occurrence Nets (CO-nets) and we characterize the classes of monotonic orchestrations. We show that few orchestrations are indeed monotonic, mostly since latency can be traded for quality of data. We also propose a sound refinement of monotony, called \emph{conditional monotony}, which forbids this kind of cheating and show that conditional monotony is widely satisfied by orchestrations. This finding leads to reconsidering the way SLAs should be formulated.} }

@inproceedings{BDMR-concur09, address = {Bologna, Italy}, month = sep, year = 2009, volume = 5710, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Bravetti, Mario and Zavattaro, Gianluigi}, acronym = {{CONCUR}'09}, booktitle = {{P}roceedings of the 20th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'09)}, author = {Bouyer, Patricia and Duflot, Marie and Markey, Nicolas and Renault, Gabriel}, title = {Measuring Permissivity in Finite Games}, pages = {196-210}, doi = {10.1007/978-3-642-04081-8_14}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDMR-concur09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDMR-concur09.pdf}, abstract = {In this paper, we extend the classical notion of strategies in turn-based finite games by allowing several moves to be selected. We~define and study a quantitative measure for permissivity of such strategies by assigning penalties when blocking transitions. We~prove that for reachability objectives, most permissive strategies exist, can be chosen memoryless, and can be computed in polynomial time, while it is in \(\textsf{NP}\cap\textsf{coNP}\) for discounted and mean penalties.} }

@incollection{EFH-tsmaai09, author = {El~Fallah Seghrouchni, Amal and Haddad, Serge}, title = {Interop{\'e}rabilit{\'e} des syst{\`e}mes multi-agents {\`a} l'aide des services web}, booktitle = {Technologies des syst{\`e}mes multi-agents et applications industrielles}, editor = {El~Fallah Seghrouchni, Amal and Briot, Jean-Pierre}, publisher = {Herm{\`e}s}, year = 2009, month = apr, pages = {77-99}, chapter = 3, url = {http://www.lavoisier.fr/notice/fr2746217850.html}, nops = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/.ps}, nopsgz = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PSGZ/.ps.gz}, futureisbn = {} }

@inproceedings{HKPPT-acc09, address = {Saint Louis, Missouri, USA}, month = jun, year = 2009, acronym = {{ACC}'09}, booktitle = {{P}roceedings of the 28th {A}merican {C}ontrol {C}onference ({ACC}'09)}, author = {Haddad, Serge and Kordon, Fabrice and Petrucci, Laure and Pradat{-}Peyre, Jean-Fran{\c{c}}ois and Tr{\`e}ves, Nicolas}, title = {Efficient State-Based Analysis by Introducing Bags in {P}etri Nets Color Domains}, pages = {5018-5025}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HKPPT-acc09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HKPPT-acc09.pdf}, doi = {10.1109/ACC.2009.5160020}, abstract = {The use of high-level nets, such as coloured Petri nets, is very convenient for modelling complex controllable systems in order to have a compact, readable and structured specification. However, when coming to the analysis phase, using too elaboratc types becomes a burden.\par A good trade-off between expressivene and analy is capabilities is then to have only imple types, which is achieved with symmetric nels. These latter nels enjoy the possibility of generating a symbolic reachability gralph, which is much smallcr than the whole state space and still allows for exhaustive analysis.\par In this paper, we extend the symmetric net model with bags on arcs. Hence, variables can be bags of tokens,leading to more flexible models. We show that symmetric nets with bags also allow for applying the symbolic reachability graph technique with application to deadlock detection and more generally for safety properties.} }

@misc{dots-2.2, author = {Chatain, {\relax Th}omas and Gastin, Paul and Muscholl, Anca and Sznajder, Nathalie and Walukiewicz, Igor and Zeitoun, Marc}, title = {Distributed control for restricted specifications}, howpublished = {Deliverable DOTS~2.2 (ANR-06-SETI-003)}, year = 2009, month = mar }

@misc{dots-1.2a, author = {Bouyer, Patricia and Laroussinie, Fran{\c{c}}ois and Lime, Didier and Markey, Nicolas}, title = {Synthesis of timed controllers}, howpublished = {Deliverable DOTS~1.2a (ANR-06-SETI-003)}, year = 2009, month = mar }

@article{DHS-tose09, publisher = {{IEEE} Computer Society Press}, journal = {IEEE Transactions on Software Engineering}, author = {Donatelli, Susanna and Haddad, Serge and Sproston, Jeremy}, title = {Model Checking Timed and Stochastic Properties with {CSL\textsuperscript{TA}}}, volume = 35, number = 2, month = mar # {-} # apr, year = 2009, pages = {224-240}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DHS-tose09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DHS-tose09.pdf}, doi = {10.1109/TSE.2008.108}, abstract = {Markov chains are a well-known stochastic process that provide a balance between being able to adequately model the system's behavior and being able to afford the cost of the model solution. Systems can be modelled directly as Markov chains, or with a higher-level formalism for which Markov chains represent the underlying semantics. Markov chains are widely used to study the performance of computer and telecommunication systems. The definition of stochastic temporal logics like Continuous Stochastic Logic~(CSL) and its variant~asCSL, and of their model-checking algorithms, allows a unified approach to the verification of systems, allowing the mix of performance evaluation and probabilistic verification. \par In this paper we present the stochastic logic CSL\textsuperscript{TA} , which is more expressive than CSL and~asCSL, and in which properties can be specified using automata (more precisely, timed automata with a single clock). The extension with respect to expressiveness allows the specification of properties referring to the probability of a finite sequence of timed events. A~typical example is the responsiveness property {"}with probability at least~0.75, a~message sent at time~0 by a system~\(A\) will be received before time~5 by system~\(B\) and the acknowledgment will be back at~\(A\) before time~7{"}, a property that cannot be expressed in either CSL or~asCSL. Furthermore, the choice of using automata rather than the classical temporal operators Next and Until should help in enlarging the accessibility of model checking to a larger public. We~also present a model-checking algorithm for~CSL\textsuperscript{TA}.} }

@inproceedings{AFGM-tableaux09, address = {Oslo, Norway}, month = jul, year = 2009, volume = 5607, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, editor = {Giese, Martin and Waaler, Arild}, acronym = {{TABLEAUX}'09}, booktitle = {{P}roceedings of the 18th {I}nternational {W}orkshop on {T}heorem {P}roving with {A}nalytic {T}ableaux and {R}elated {M}ethods ({TABLEAUX}'09)}, author = {Areces, Carlos and Figueira, Diego and Gor{\'\i}n, Daniel and Mera, Sergio}, title = {Tableaux and Model Checking for Memory Logics}, pages = {47-61}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AFGM-tableaux09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AFGM-tableaux09.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/AFGM-tableaux09.ps}, doi = {10.1007/978-3-642-02716-1_5}, abstract = {Memory logics are modal logics whose semantics is specified in terms of relational models enriched with additional data structure to represent memory. The logical language is then extended with a collection of operations to access and modify the data structure. In~this paper we study their satisfiability and the model checking problems.\par We first give sound and complete tableaux calculi for the memory logic \(ML(k,r,e)\) (the basic modal language extended with the operator \(r\) used to memorize a state, the operator \(e\) used to wipe out the memory, and the operator \(k\) used to check if the current point of evaluation is memorized) and some of its sublanguages. As the satisfiability problem of \(ML(k,r,e)\) is undecidable, the tableau calculus we present is non terminating. Hence, we furthermore study a variation that ensures termination, at the expense of completeness, and we use model checking to ensure soundness. Secondly, we show that the model checking problem is PSpace-complete.} }

@inproceedings{DHL-mbt09, address = {York, UK}, month = oct, year = 2009, number = {2}, volume = {253}, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier Science Publishers}, acronym = {{MBT}'09}, booktitle = {{P}roceedings of the 5th Workshop on Model-Based Testing ({MBT}'09)}, author = {Dadeau, Fr{\'e}d{\'e}ric and H{\'e}am, Pierre-Cyrille and Levrey, Jocelyn}, title = {On the Use of Uniform Random Generation of Automata for Testing}, pages = {37-51}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DHL-mbt09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DHL-mbt09.pdf}, doi = {10.1016/j.entcs.2009.09.050 }, abstract = {Developing efficient and automatic testing techniques is one of the major challenges facing software validation community. In this paper, we show how a uniform random generation process of finite automata, developed in a recent work by Bassino and Nicaud, is relevant for many faces of automatic testing. The main contribution is to show how to combine two major testing approaches: model-based testing and random testing. This leads to a new testing technique successfully experimented on a realistic case study. We also illustrate how the power of random testing, applied on a Chinese Postman Problem implementation, points out an error in a well-known algorithm. Finally, we provide some statistics on model-based testing algorithms.} }

@inproceedings{CDK-cade09, address = {Montreal, Canada}, month = aug, year = 2009, volume = {5663}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Schmidt, Renate}, acronym = {{CADE}'09}, booktitle = {{P}roceedings of the 22nd {I}nternational {C}onference on {A}utomated {D}eduction ({CADE}'09)}, author = {Ciob{\^a}c{\u{a}}, {\c{S}}tefan and Delaune, St{\'e}phanie and Kremer, Steve}, title = {Computing knowledge in security protocols under convergent equational theories}, pages = {355-370}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDK-cade09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDK-cade09.pdf}, doi = {10.1007/978-3-642-02959-2_27}, abstract = {In the symbolic analysis of security protocols, two classical notions of knowledge, deducibility and indistinguishability, yield corresponding decision problems. We~propose a procedure for both problems under arbitrary convergent equational theories. Our~procedure terminates on a wide range of equational theories. In~particular, we~obtain a new decidability result for a theory we encountered when studying electronic voting protocols. We~also provide a prototype implementation.} }

@inproceedings{CHK-ciaa09, address = {Sydney, Australia}, month = jul, year = 2009, volume = 5642, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, editor = {Maneth, Sebastian}, acronym = {{CIAA}'09}, booktitle = {{P}roceedings of the 14th {I}nternational {C}onference on {I}mplementation and {A}pplication of {A}utomata ({CIAA}'09)}, author = {Courbis, Rom{\'e}o and H{\'e}am, Pierre-Cyrille and Kouchnarenko, Olga}, title = {{TAGED} Approximations for Veriying Temporal Patterns}, pages = {135-144}, doi = {10.1007/978-3-642-02979-0_17}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CHK-ciaa09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CHK-ciaa09.pdf}, abstract = {This paper investigates the use of tree automata with global equalities and disequalities (TAGED for short) in reachability analysis over term rewriting systems (TRSs). The reachability problem being in general undecidable on non terminating TRSs, we provide TAGED-based construction, and then design approximation-based semi-decision procedures to model-check useful temporal patterns on infinite state rewriting graphs. To show that the above TAGED-based construction can be effectively carried out, complexity analysis for rewriting TAGED-definable languages is given.} }

@inproceedings{HNS-ciaa09, address = {Sydney, Australia}, month = jul, year = 2009, volume = 5642, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, editor = {Maneth, Sebastian}, acronym = {{CIAA}'09}, booktitle = {{P}roceedings of the 14th {I}nternational {C}onference on {I}mplementation and {A}pplication of {A}utomata ({CIAA}'09)}, author = {H{\'e}am, Pierre-Cyrille and Nicaud, Cyril and Schmitz, Sylvain}, title = {Random Generation of Deterministic Tree (Walking) Automata}, pages = {115-124}, doi = {10.1007/978-3-642-02979-0_15}, url = {http://hal.inria.fr/inria-00408316}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HNS-ciaa09.pdf}, abstract = {Uniform random generators deliver a simple empirical means to estimate the average complexity of an algorithm. We present a general rejection algorithm that generates sequential letter-to-letter transducers up to isomorphism. We tailor this general scheme to randomly generate deterministic tree walking automata and deterministic top-down tree automata. We apply our implementation of the generator to the estimation of the average complexity of a deterministic tree walking automata to nondeterministic top-down tree automata construction we also implemented.} }

@inproceedings{BG-dlt09, address = {Stuttgart, Germany}, month = jun # {-} # jul, year = 2009, volume = {5583}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Diekert, Volker and Nowotka, Dirk}, acronym = {{DLT}'09}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {D}evelopments in {L}anguage {T}heory ({DLT}'09)}, author = {Bollig, Benedikt and Gastin, Paul}, title = {Weighted versus Probabilistic Logics}, pages = {18-38}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BG-dlt09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BG-dlt09.pdf}, doi = {10.1007/978-3-642-02737-6_2}, abstract = {While a mature theory around logics such as MSO, LTL, and CTL has been developed in the pure boolean setting of finite automata, weighted automata lack such a natural connection with (temporal) logic and related verification algorithms. In this paper, we will identify weighted versions of MSO and CTL that generalize the classical logics and even other quantitative extensions such as probabilistic CTL. We establish expressiveness results on our logics giving translations from weighted and probabilistic CTL into weighted MSO.} }

@inproceedings{AGM-pods09, address = {Providence, Rhode Island, USA}, month = jun # {-} # jul, year = 2009, publisher = {ACM Press}, editor = {Su, Jianwen}, acronym = {{PODS}'09}, booktitle = {{P}roceedings of the 28th {A}nnual {ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium on {P}rinciples of {D}atabase {S}ystems ({PODS}'09)}, author = {Abiteboul, Serge and Gottlob, Georg and Manna, Marco}, title = {Distributed {XML} Design}, pages = {247-258}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AGM-pods09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AGM-pods09.pdf}, doi = {10.1145/1559795.1559833}, abstract = {A \emph{distributed XML document} is an XML document that spans several machines or Web repositories. We assume that a distribution design of the document tree is given, providing an XML tree some of whose leaves are {"}docking points{"}, to which XML subtrees can be attached. These subtrees may be provided and controlled by peers at remote locations, or may correspond to the result of function calls, e.g., Web services. If a global type~\(t\), e.g. a DTD, is specified for a distributed document~\(T\), it~would be most desirable to be able to break this type into a collection of local types, called a local typing, such that the document satisfies~\(t\) if and only if each peer (or~function) satisfies its local type. In this paper we lay out the fundamentals of a theory of local typing and provide formal definitions of three main variants of locality: local typing, maximal local typing, and perfect typing, the latter being the most desirable. We study the following relevant decision problems: (i)~given a typing for a design, determine whether it is local, maximal local, or perfect; (ii)~given a design, establish whether a (maximal) local, or perfect typing does exist. For some of these problems we provide tight complexity bounds (polynomial space), while for the others we show exponential upper bounds. A~main contribution is a polynomial-space algorithm for computing a perfect typing in this context, if it exists.} }

@inproceedings{ABM-pods09, address = {Providence, Rhode Island, USA}, month = jun # {-} # jul, year = 2009, publisher = {ACM Press}, editor = {Su, Jianwen}, acronym = {{PODS}'09}, booktitle = {{P}roceedings of the 28th {A}nnual {ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium on {P}rinciples of {D}atabase {S}ystems ({PODS}'09)}, author = {Abiteboul, Serge and Bourhis, Pierre and Marinoiu, Bogdan}, title = {Satisfiability and relevance for queries over active documents}, pages = {87-96}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABM-pods09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABM-pods09.pdf}, doi = {10.1145/1559795.1559810}, abstract = {Many Web applications are based on dynamic interactions between Web components exchanging flows of information. Such a situation arises for instance in mashup systems or when monitoring distributed autonomous systems. This is a challenging problem that has generated recently a lot of attention; see~Web~2.0. For capturing interactions between Web components, we use active documents interacting with the rest of the world via streams of updates. Their input streams specify updates to the document (in the spirit of RSS feeds), whereas their output streams are defined by queries on the document. In most of the paper, the focus is on input streams where the updates are only insertions, although we do consider also deletions. \par We introduce and study two fundamental concepts in this setting, namely, satisfiability and relevance. Some fact is \emph{satisfiable} for an active document and a query if it has a chance to be in the result of the query in some future state. Given an active document and a query, a call in the document is \emph{relevant} if the data brought by this call has a chance to impact the answer to the query. We analyze the complexity of computing satisfiability in our core model (insertions only) and for extensions (e.g., with deletions). We also analyze the complexity of computing relevance in the core model.} }

@inproceedings{BLPS-pods09, address = {Providence, Rhode Island, USA}, month = jun # {-} # jul, year = 2009, publisher = {ACM Press}, editor = {Su, Jianwen}, acronym = {{PODS}'09}, booktitle = {{P}roceedings of the 28th {A}nnual {ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium on {P}rinciples of {D}atabase {S}ystems ({PODS}'09)}, author = {Barcel{\'o}, Pablo and Libkin, Leonid and Poggi, Antonella and Sirangelo, Cristina}, title = {{XML} with Incomplete Information: Models, Properties, and Query Answering}, pages = {237-246}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLPS-pods09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLPS-pods09.pdf}, doi = {10.1145/1559795.1559832}, abstract = {We study models of incomplete information for XML, their computational properties, and query answering. While our approach is motivated by the study of relational incompleteness, incomplete information in XML documents may appear not only as null values but also as missing structural information. Our goal is to provide a classification of incomplete descriptions of XML documents, and separate features---or groups of features---that lead to hard computational problems from those that admit efficient algorithms. Our classification of incomplete information is based on the combination of null values with partial structural descriptions of documents. The key computational problems we consider are consistency of partial descriptions, representability of complete documents by incomplete ones, and query answering. We show how factors such as schema information, the presence of node ids, and missing structural information affect the complexity of these main computational problems, and find robust classes of incomplete XML descriptions that permit tractable query evaluation.} }

@inproceedings{fig-pods09, address = {Providence, Rhode Island, USA}, month = jun # {-} # jul, year = 2009, publisher = {ACM Press}, editor = {Su, Jianwen}, acronym = {{PODS}'09}, booktitle = {{P}roceedings of the 28th {A}nnual {ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium on {P}rinciples of {D}atabase {S}ystems ({PODS}'09)}, author = {Figueira, Diego}, title = {Satisfiability of Downward {XP}ath with Data Equality Tests}, pages = {197-206}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/fig-pods09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/fig-pods09.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/fig-pods09.ps}, doi = {10.1145/1559795.1559827}, abstract = {In this work we investigate the satisfiability problem for the logic \(\textup{XPath}(\downarrow,\downarrow^{*},=)\), that includes all downward axes as well as equality and inequality tests. We address this problem in the absence of DTDs and the sibling axis. We prove that this fragment is decidable, and we nail down its complexity, showing the problem to be ExpTime-complete. The result also holds when path expressions allow closure under the Kleene star operator. To obtain these results, we introduce a new automaton model over data trees that captures \(\textup{XPath}(\downarrow,\downarrow^*,=)\) and has an ExpTime emptiness problem. Furthermore, we give the exact complexity of several downward-looking fragments. } }

@inproceedings{PS-icalp09, address = {Rhodes, Greece}, month = jul, year = 2009, volume = 5556, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Albers, Susanne and Marchetti-Spaccamela, Alberto and Matias, Yossi and Thomas, Wolfgang}, acronym = {{ICALP}'09}, booktitle = {{P}roceedings of the 36th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'09)}, author = {Place, {\relax Th}omas and Segoufin, Luc}, title = {A decidable characterization of Locally Testable Tree Languages}, pages = {285-296}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PS-icalp09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PS-icalp09.pdf}, doi = {10.1007/978-3-642-02930-1_24}, abstract = {A regular tree language~\(L\) is locally testable if the membership of a tree into~\(L\) depends only on the presence or absence of some neighborhoods in the tree. In~this paper we show that it is decidable whether a regular tree language is locally testable.} }

@inproceedings{FGL-icalp09, address = {Rhodes, Greece}, month = jul, year = 2009, volume = 5556, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Albers, Susanne and Marchetti-Spaccamela, Alberto and Matias, Yossi and Thomas, Wolfgang}, acronym = {{ICALP}'09}, booktitle = {{P}roceedings of the 36th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'09)}, author = {Finkel, Alain and Goubault{-}Larrecq, Jean}, title = {Forward Analysis for {WSTS}, Part~{II}: Complete {WSTS}}, pages = {188-199}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGL-icalp09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGL-icalp09.pdf}, doi = {10.1007/978-3-642-02930-1_16}, abstract = {We~describe a simple, conceptual forward analysis procedure for \(\infty\)-complete WSTS~\(\mathcal{S}\). This computes the \emph{clover} of a state~\(s_0\) , \textit{i.e.}, a~finite description of the closure of the cover of~\(s_0\) . When \(S\) is the completion of a WSTS~\(\mathcal{X}\), the clover in~\(\mathcal{S}\) is a finite description of the cover in~\(\mathcal{X}\). We~show that this applies exactly when \(\mathcal{X}\) is an \(\omega^2\)-WSTS, a~new robust class of WSTS. We~show that our procedure terminates in more cases than the generalized Karp-Miller procedure on extensions of Petri nets. We characterize the WSTS where our procedure terminates as those that are \emph{clover-flattable}. Finally, we~apply this to well-structured counter systems.} }

@inproceedings{BBBB-icalp09, address = {Rhodes, Greece}, month = jul, year = 2009, volume = 5556, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Albers, Susanne and Marchetti-Spaccamela, Alberto and Matias, Yossi and Thomas, Wolfgang}, acronym = {{ICALP}'09}, booktitle = {{P}roceedings of the 36th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'09)}, author = {Baier, Christel and Bertrand, Nathalie and Bouyer, Patricia and Brihaye, {\relax Th}omas}, title = {When are Timed Automata Determinizable?}, pages = {43-54}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBB-icalp09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBB-icalp09.pdf}, doi = {10.1007/978-3-642-02930-1_4}, abstract = {In this paper, we propose an abstract procedure which, given a timed automaton, produces a language-equivalent deterministic infinite timed tree. We~prove that under a certain boundedness condition, the infinite timed tree can be reduced into a classical deterministic timed automaton. The boundedness condition is satisfied by several subclasses of timed automata, some of them were known to be determinizable (event-clock timed automata, automata with integer resets), but some others were not. We prove for instance that strongly non-Zeno timed automata can be determinized. As a corollary of those constructions, we get for those classes the decidability of the universality and of the inclusion problems, and compute their complexities (the inclusion problem is for instance EXPSPACE-complete for strongly non-Zeno timed automata).} }

@inproceedings{BF-icalp09, address = {Rhodes, Greece}, month = jul, year = 2009, volume = 5556, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Albers, Susanne and Marchetti-Spaccamela, Alberto and Matias, Yossi and Thomas, Wolfgang}, acronym = {{ICALP}'09}, booktitle = {{P}roceedings of the 36th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'09)}, author = {Bouyer, Patricia and Forejt, Vojt{\v e}ch}, title = {Reachability in Stochastic Timed Games}, pages = {103-114}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BF-icalp09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BF-icalp09.pdf}, doi = {10.1007/978-3-642-02930-1_9}, abstract = {We define stochastic timed games, which extend two-player timed games with probabilities (following a recent approach by Baier \textit{et~al.}), and which extend in a natural way continuous-time Markov decision processes. We~focus on the reachability problem for these games, and ask whether one of the players has a strategy to ensure that the probability of reaching a fixed set of states is equal~to (or~below, resp.~above) a~certain number~\(r\), whatever the second player does. We~show that the problem is undecidable in general, but that it becomes decidable if we restrict to single-clock 1\(\frac{1}{2}\)-player games and ask whether the player can ensure that the probability of reaching the set is~\(=1\) (or~\(>0\),~\(=0\)).} }

@inproceedings{CD-csf09, address = {Port Jefferson, New York, USA}, month = jul, year = 2009, publisher = {{IEEE} Computer Society Press}, acronym = {{CSF}'09}, booktitle = {{P}roceedings of the 22nd {IEEE} {C}omputer {S}ecurity {F}oundations {S}ymposium ({CSF}'09)}, author = {Cortier, V{\'e}ronique and Delaune, St{\'e}phanie}, title = {A~method for proving observational equivalence}, pages = {266-276}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CD-csf09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CD-csf09.pdf}, doi = {10.1109/CSF.2009.9}, abstract = {Formal methods have proved their usefulness for analyzing the security of protocols. Most existing results focus on trace properties like secrecy or authentication. There are however several security properties, which cannot be defined (or cannot be naturally defined) as trace properties and require the notion of \emph{observational equivalence}. Typical examples are anonymity, privacy related properties or statements closer to security properties used in cryptography.\par In this paper, we consider the applied pi calculus and we show that for \emph{determinate} processes, observational equivalence actually coincides with trace equivalence, a notion simpler to reason with. We~exhibit a large class of determinate processes, called \emph{simple processes}, that capture most existing protocols and cryptographic primitives. Then, for simple processes without replication, we~reduce the decidability of trace equivalence to deciding an equivalence relation introduced by M.~Baudet. Altogether, this yields the first decidability result of observational equivalence for a general class of equational theories.} }

@inproceedings{CDK-forte09, address = {Lisbon, Portugal}, month = jun, year = 2009, volume = {5522}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Lee, David and Lopes, Ant{\'o}nia and Poetzsch-Heffter, Arnd}, acronym = {{FMOODS/FORTE}'09}, booktitle = {{P}roceedings of {IFIP} {I}nternational {C}onference on {F}ormal {T}echniques for {D}istributed {S}ystems ({FMOODS/FORTE}'09)}, author = {Chadha, Rohit and Delaune, St{\'e}phanie and Kremer, Steve}, title = {Epistemic Logic for the Applied Pi Calculus}, pages = {182-197}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/cdk-forte09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/cdk-forte09.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/cdk-forte09.ps}, doi = {10.1007/978-3-642-02138-1_12}, abstract = {We propose an epistemic logic for the applied pi calculus, which is a variant of the pi calculus with extensions for modeling cryptographic protocols. In such a calculus, the security guarantees are usually stated as equivalences. While process calculi provide a natural means to describe the protocols themselves, epistemic logics are often better suited for expressing certain security properties such as secrecy and anonymity.\par We intend to bridge the gap between these two approaches: using the set of traces generated by a process as models, we define a logic which has constructs for reasoning about both intruder's epistemic knowledge and the set of messages in possession of the intruder. As an example we consider two formalizations of privacy in electronic voting and study the relationship between them.} }

@inproceedings{BHKL-ijcai2009, address = {Pasadena, California, USA}, month = jul, year = 2009, publisher = {AAAI Press}, editor = {Boutilier, Craig}, acronym = {{IJCAI}'09}, booktitle = {{P}roceedings of the 21st {I}nternational {J}oint {C}onference on {A}rtificial {I}ntelligence ({IJCAI}'09)}, author = {Bollig, Benedikt and Habermehl, Peter and Kern, Carsten and Leucker, Martin}, title = {Angluin-Style Learning of~{NFA}}, pages = {1004-1009}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHKL-ijcai09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHKL-ijcai09.pdf}, abstract = {We introduce NL\(^{*}\), a learning algorithm for inferring non-deterministic finite-state automata using membership and equivalence queries. More specifically, residual finite-state automata (RFSA) are learned similarly as in Angluin's popular L\(^{*}\) algorithm, which, however, learns deterministic finite-state automata~(DFA). Like in a~DFA, the~states of an RFSA represent residual languages. Unlike a~DFA, an~RFSA restricts to prime residual languages, which cannot be described as the union of other residual languages. In~doing~so, RFSA can be exponentially more succinct than~DFA. They are, therefore, the preferable choice for many learning applications. The implementation of our algorithms is applied to a collection of examples and confirms the expected advantage of NL\(^{*}\) over L\(^{*}\).} }

@inproceedings{BCDDH-tacas09, address = {York, UK}, month = mar, year = 2009, volume = {5505}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Kowalewski, Stefan and Philippou, Anna}, acronym = {{TACAS}'09}, booktitle = {{P}roceedings of the 15th {I}nternational {C}onference on {T}ools and {A}lgorithms for {C}onstruction and {A}nalysis of {S}ystems ({TACAS}'09)}, author = {Berwanger, Dietmar and Chatterjee, Krishnendu and De{~}Wulf, Martin and Doyen, Laurent and Henzinger, {\relax Th}omas~A.}, title = {Alpaga: A~Tool for Solving Parity Games with Imperfect Information}, pages = {58-61}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCDDH-tacas09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCDDH-tacas09.pdf}, doi = {10.1007/978-3-642-00768-2_7}, abstract = {Alpaga is a solver for two-player parity games with imperfect information. Given the description of a game, it~determines whether the first player can ensure to win and, if~so, it~constructs a winning strategy. The~tool provides a symbolic implementation of a recent algorithm based on antichains.} }

@inproceedings{BCL-rta09, address = {Bras{\'\i}lia, Brazil}, month = jun # {-} # jul, year = 2009, volume = 5595, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Treinen, Ralf}, acronym = {{RTA}'09}, booktitle = {{P}roceedings of the 20th {I}nternational {C}onference on {R}ewriting {T}echniques and {A}pplications ({RTA}'09)}, author = {Bursuc, Sergiu and Comon{-}Lundh, Hubert}, title = {Protocol security and algebraic properties: decision results for a bounded number of sessions}, pages = {133-147}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCL-rta09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCL-rta09.pdf}, doi = {10.1007/978-3-642-02348-4_10}, abstract = {We consider the problem of deciding the security of cryptographic protocols for a bounded number of sessions, taking into account some algebraic properties of the security primitives, for instance Abelian group properties. We propose a general method for deriving decision algorithms, splitting the task into 4 properties of the rewriting system describing the intruder capabilities: locality, conservativity, finite variant property and decidability of one-step deducibility constraints. We illustrate this method on a non trivial example, combining several Abelian Group properties, exponentiation and a homomorphism, showing a decidability result for this combination. } }

@inproceedings{GJ-rta09, address = {Bras{\'\i}lia, Brazil}, month = jun # {-} # jul, year = 2009, volume = 5595, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Treinen, Ralf}, acronym = {{RTA}'09}, booktitle = {{P}roceedings of the 20th {I}nternational {C}onference on {R}ewriting {T}echniques and {A}pplications ({RTA}'09)}, author = {Godoy, Guillem and Jacquemard, Florent}, title = {Unique Normalization for Shallow {TRS}}, pages = {63-77}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-21.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-21.pdf}, doi = {10.1007/978-3-642-02348-4_5}, abstract = {Computation with a term rewrite system (TRS) consists in the application of its rules from a given starting term until a normal form is reached, which is considered the result of the computation. The unique normalization (UN) property for a TRS~\(R\) states that any starting term can reach at most one normal form when \(R\) is used, i.e. that the computation with R is unique. \par We study the decidability of this property for classes of TRS defined by syntactic restrictions such as linearity (variables can occur only once in each side of the rules), flatness (sides of the rules have depth at most one) and shallowness (variables occur at depth at most one in the rules).\par We prove that UN is decidable in polynomial time for shallow and linear TRS, using tree automata techniques. This result is very near to the limits of decidability, since this property is known undecidable even for very restricted classes like right-ground TRS, flat TRS and also right-flat and linear TRS. We also show that that UN is even undecidable for flat and right-linear TRS. The latter result is in contrast with the fact that many other natural properties like reachability, termination, confluence, weak normalization... are decidable for this class of TRS.} }

@inproceedings{BCD-rta09, address = {Bras{\'\i}lia, Brazil}, month = jun # {-} # jul, year = 2009, volume = 5595, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Treinen, Ralf}, acronym = {{RTA}'09}, booktitle = {{P}roceedings of the 20th {I}nternational {C}onference on {R}ewriting {T}echniques and {A}pplications ({RTA}'09)}, author = {Baudet, Mathieu and Cortier, V{\'e}ronique and Delaune, St{\'e}phanie}, title = {{YAPA}: A~generic tool for computing intruder knowledge}, pages = {148-163}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCD-rta09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCD-rta09.pdf}, doi = {10.1007/978-3-642-02348-4_11}, abstract = {Reasoning about the knowledge of an attacker is a necessary step in many formal analyses of security protocols. In the framework of the applied pi calculus, as in similar languages based on equational logics, knowledge is typically expressed by two relations: deducibility and static equivalence. Several decision procedures have been proposed for these relations under a variety of equational theories. However, each theory has its particular algorithm, and none has been implemented so~far.\par We provide a generic procedure for deducibility and static equivalence that takes as input any convergent rewrite system. We show that our algorithm covers all the existing decision procedures for convergent theories. We also provide an efficient implementation, and compare it briefly with the more general tool ProVerif.} }

@article{BHR-fi09, publisher = {{IOS} Press}, journal = {Fundamenta Informaticae}, author = {Bouyer, Patricia and Haddad, Serge and Reynier, Pierre-Alain}, title = {Undecidability Results for Timed Automata with Silent Transitions}, year = 2009, volume = 92, number = {1-2}, pages = {1-25}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-12.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-12.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/ rr-lsv-2007-12.ps}, abstract = {In this work, we study decision problems related to timed automata with silent transitions (TA-epsilon) which strictly extend the expressiveness of timed automata~(TA). First, we answer negatively a central question raised by the introduction of silent transitions: can we decide whether the language recognized by a TA-epsilon can be recognized by some TA? Then we establish in the framework of TA-epsilon some old open conjectures that O.~Finkel has recently solved for~TA. Its proofs follow a generic scheme which relies on the fact that only a finite number of configurations can be reached by a TA while reading a timed word. This property does not hold for TA-epsilon, the proofs in the framework of TA-epsilon thus require more elaborated arguments. We~establish undecidability of complementability, minimization of the number of clocks, and closure under shuffle. We~also show these results in the framework of infinite timed languages.} }

@techreport{LSV:09:02, author = {Bursuc, Sergiu and Comon{-}Lundh, Hubert}, title = {Protocols, insecurity decision and combination of equational theories}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2009}, month = feb, type = {Research Report}, number = {LSV-09-02}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-02.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-02.pdf}, note = {43~pages}, abstract = {We consider the problem of finding attacks for a bounded number of sessions of security protocols. We~contribute to this field, showing how to decompose the problem into pieces for a class of equational theories, which includes the hierarchical combinations, as well as non-hierarchical ones. We apply this result to an electronic purse case study: we~show the decidability in co-NP of the insecurity problem for a complex equational theory mixing three Abelian groups, exponentiation and homomorphism properties.\par The main technical contributions rely on equational logic, term rewriting and combination of theories.} }

@article{BS-tocl08, publisher = {ACM Press}, journal = {ACM Transactions on Computational Logic}, author = {Benedikt, Michael and Segoufin, Luc}, title = {Regular tree languages definable in {FO} and in {FO}\(_{\textit{mod}}\)}, volume = 11, number = 1, nopages = {}, month = oct, year = 2009, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-tocl09.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-tocl09.pdf}, doi = {10.1145/1614431.1614435}, abstract = {We~consider regular languages of labeled trees. We~give an effective characterization of the regular languages over such trees that are definable in first-order logic in the language of labeled graphs. These languages are the analog on trees of the {"}locally threshold testable{"} languages on strings. We~show that this characterization yields a decision procedure for determining whether a regular tree language is first-order definable: the~procedure is polynomial time in the minimal automaton presenting the regular language. We~also provide an algorithm for deciding whether a regular language is definable in first-order logic supplemented with modular quantifiers.} }

@misc{Quasimodo-3.1, author = {Bouyer, Patricia and Katoen, Joost-Pieter and Langerak, Rom and Laroussinie, Fran{\c{c}}ois and Markey, Nicolas and Raskin, Jean-Fran{\c{c}}ois}, title = {Transfer of correctness from models to implementation}, howpublished = {Deliverable QUASIMODO~3.1 (ICT-FP7-STREP-214755)}, year = 2009, month = jan }

@inproceedings{JKV-lata09, address = {Tarragona, Spain}, month = apr, year = 2009, volume = 5457, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Dediu, Adrian Horia and Mihai Ionescu, Armand and Mart{\'\i}n-Vide, Carlos}, acronym = {{LATA}'09}, booktitle = {{P}roceedings of the 3rd {I}nternational {C}onference on {L}anguage and {A}utomata {T}heory and {A}pplications ({LATA}'09)}, author = {Jacquemard, Florent and Klay, Francis and Vacher, Camille}, title = {Rigid Tree Automata}, pages = {446-457}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JKV-lata09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JKV-lata09.pdf}, doi = {10.1007/978-3-642-00982-2_38}, abstract = {We introduce the class of Rigid Tree Automata (RTA), an extension of standard bottom-up automata on ranked trees with distinguished states called rigid. Rigid states define a restriction on the computation of RTA on trees: RTA can test for equality in subtrees reaching the same rigid state. RTA are able to perform local and global tests of equality between subtrees, non-linear tree pattern matching, and restricted disequality tests as well. Properties like determinism, pumping lemma, boolean closure, and several decision problems are studied in detail. In particular, the emptiness problem is shown decidable in linear time for RTA whereas membership of a given tree to the language of a given RTA is NP-complete. Our main result is the decidability of whether a given tree belongs to the rewrite closure of a RTA language under a restricted family of term rewriting systems, whereas this closure is not a RTA language. This result, one of the first on rewrite closure of languages of tree automata with constraints, is enabling the extension of model checking procedures based on finite tree automata techniques. Finally, a comparison of RTA with several classes of tree automata with local and global equality tests, and with dag automata is also provided.} }

@phdthesis{bouyer-hab2009, author = {Bouyer, Patricia}, title = {From Qualitative to Quantitative Analysis of Timed Systems}, school = {Universit{\'e} Paris~7, Paris, France}, type = {M{\'e}moire d'habilitation}, year = 2009, month = jan, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PB-hdr09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PB-hdr09.pdf} }

@incollection{GMN-pct08, futureaddress = {}, month = jan, year = 2009, series = {IARCS-Universities}, publisher = {Universities Press}, booktitle = {Perspectives in Concurrency Theory}, editor = {Lodaya, Kamal and Mukund, Madhavan and Ramanujam, R.}, author = {Gastin, Paul and Mukund, Madhavan and Narayan Kumar, K.}, title = {Reachability and boundedness in time-constrained {MSC} graphs}, pages = {157-183}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GMN-pct08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GMN-pct08.pdf}, abstract = {Channel boundedness is a necessary condition for a message-passing system to exhibit regular, finite-state behaviour at the global level. For Message Sequence Graphs~(MSGs), the most basic form of High-level Message Sequence Charts~(HMSCs), channel boundedness can be characterized in terms of structural conditions on the underlying graph. We consider MSGs enriched with timing constraints between events. These constraints restrict the global behaviour and can impose channel boundedness even when it is not guaranteed by the graph structure of the MSG. We~show that we can use MSGs with timing constraints to simulate computations of a two-counter machine. As~a consequence, even the more fundamental problem of reachability, which is trivial for untimed MSGs, becomes undecidable when we add timing constraints. Different forms of channel boundedness also then turn out to be undecidable, using reductions from the reachability problem.} }

@incollection{BP-pct08, futureaddress = {}, month = jan, year = 2009, series = {IARCS-Universities}, publisher = {Universities Press}, booktitle = {Perspectives in Concurrency Theory}, editor = {Lodaya, Kamal and Mukund, Madhavan and Ramanujam, R.}, author = {Bouyer, Patricia and Petit, Antoine}, title = {On extensions of timed automata}, pages = {35-63}, abstract = {Since their definition in the early nineties, timed automata have been one of the most used and widely studied models for representing and analyzing real-time systems. In their seminal paper, Alur and Dill proved the probably most important property of timed automata: checking emptiness of the language accepted by a timed automaton, or equivalently checking a reachability property in a timed automaton, is decidable. This result relies on the construction of the so-called region automaton, which abstracts behaviours of a timed automaton into behaviours of a finite automaton. Since then, symbolic algorithms have been developed to solve that problem, several model-checkers have been implemented, and numerous case studies have been verified.\par Lots of works have naturally aimed at proposing extensions of timed automata with new features, while preserving the above-mentioned fundamental decidability result. The motivation for these extensions is basically twofold. First it can increase the expressiveness of timed automata, allowing to model larger classes of systems. Then it can improve the conciseness (and hence the readability) of models by constructing more compact representations for a given system.\par In this paper, we discuss and compare some of the most important extensions of timed automata that have been considered in the literature.} }

@inproceedings{BBL-Fossacs09, address = {York, UK}, month = mar, year = 2009, volume = 5504, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {de Alfaro, Luca}, acronym = {{FoSSaCS}'09}, booktitle = {{P}roceedings of the 12th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'09)}, author = {Bansal, Kshitij and Brochenin, R{\'e}mi and Lozes, {\'E}tienne}, title = {Beyond Shapes: Lists with Ordered Data}, pages = {425-439}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBL-fossacs09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBL-fossacs09.pdf}, doi = {10.1007/978-3-642-00596-1_30}, abstract = {Standard analysis on recursive data structures restrict their attention to shape properties (for instance, a program that manipulates a list returns a list), excluding properties that deal with the actual content of these structures. For instance, these analysis would not establish that the result of merging two ordered lists is an ordered list. Separation logic, one of the prominent framework for these kind of analysis, proposed a heap model that could represent data, but, to our knowledge, no predicate dealing with data has ever been integrated to the logic while preserving decidability. We~establish decidability for (first-order) separation logic with a predicate that allows to compare two successive data in a list. We~then consider the extension where two data in arbitrary positions may be compared, and establish the undecidability in general. We~define a guarded fragment that turns out to be both decidable and sufficiently expressive to prove the preservation of the loop invariant of a standard program merging ordered lists. We~finally consider the extension with the magic-wand and prove that, by constrast with the data-free case, even a very restricted use of the magic wand already introduces undecidability.} }

@article{GSZ-fmsd09, publisher = {Springer}, journal = {Formal Methods in System Design}, author = {Gastin, Paul and Sznajder, Nathalie and Zeitoun, Marc}, title = {Distributed synthesis for well-connected architectures}, volume = 34, number = 3, pages = {215-237}, month = jun, year = 2009, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GSZ-fmsd09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GSZ-fmsd09.pdf}, doi = {10.1007/s10703-008-0064-7}, abstract = {We study the synthesis problem for external linear or branching specifications and distributed, synchronous architectures with arbitrary delays on processes. External means that the specification only relates input and output variables. We introduce the subclass of uniformly well-connected (UWC) architectures for which there exists a routing allowing each output process to get the values of all inputs it is connected to, as soon as possible. We prove that the distributed synthesis problem is decidable on UWC architectures if and only if the output variables are totally ordered by their knowledge of input variables. We also show that if we extend this class by letting the routing depend on the output process, then the previous decidability result fails. Finally, we provide a natural restriction on specifications under which the whole class of UWC architectures is decidable.} }

@proceedings{KP-secco2008, title = {{P}roceedings of the 6th {I}nternational {W}orkshop on {S}ecurity {I}ssues in {C}oncurrency ({S}ec{C}o'08)}, booktitle = {{P}roceedings of the 6th {I}nternational {W}orkshop on {S}ecurity {I}ssues in {C}oncurrency ({S}ec{C}o'08)}, editor = {Kremer, Steve and Panangaden, Prakash}, publisher = {Elsevier Science Publishers}, doi = {10.1016/j.entcs.2009.07.077}, url = {http://www.sciencedirect.com/science/journal/15710661/242/3}, series = {Electronic Notes in Theoretical Computer Science}, volume = 242, number = 3, year = 2009, month = aug, address = {Toronto, Canada} }

@article{BCK-IC09, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Baudet, Mathieu and Cortier, V{\'e}ronique and Kremer, Steve}, title = {Computationally Sound Implementations of Equational Theories against Passive Adversaries}, year = {2009}, month = apr, volume = 207, number = 4, pages = {496-520}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCK-ic09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCK-ic09.pdf}, doi = {10.1016/j.ic.2008.12.005}, abstract = {In~this paper we study the link between formal and cryptographic models for security protocols in the presence of passive adversaries. In~contrast to other works, we~do not consider a fixed set of primitives but aim at results for arbitrary equational theories. We~define a framework for comparing a cryptographic implementation and its idealization with respect to various security notions. In~particular, we concentrate on the computational soundness of static equivalence, a standard tool in cryptographic pi calculi. We~present a soundness criterion, which for many theories is not only sufficient but also necessary. Finally, to~illustrate our framework, we~establish the soundness of static equivalence for the exclusive OR and a theory of ciphers and lists.} }

@inproceedings{BH-Fossacs09, address = {York, UK}, month = mar, year = 2009, volume = 5504, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {de Alfaro, Luca}, acronym = {{FoSSaCS}'09}, booktitle = {{P}roceedings of the 12th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'09)}, author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge}, title = {Interrupt Timed Automata}, pages = {197-211}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BH-fossacs09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BH-fossacs09.pdf}, doi = {10.1007/978-3-642-00596-1_15}, abstract = {In this work, we introduce the class of Interrupt Timed Automata (ITA), which are well suited to the description of multi-task systems with interruptions in a single processor environment. This model is a subclass of hybrid automata. While reachability is undecidable for hybrid automata we show that in ITA the reachability problem is in 2EXPSPACE and in PSPACE when the number of clocks is fixed, with a procedure based on a generalized class graph. Furthermore we consider a subclass ITA\(_{-}\) which still describes usual interrupt systems and for which the reachability problem is in NEXPTIME and in NP when the number of clocks is fixed (without any class graph). There exist languages accepted by an ITA\(_{-}\) but neither by timed automata nor by controlled real-time automata (CRTA), another extension of timed automata. However we conjecture that CRTA is not contained in ITA. So, we combine ITA with CRTA in a model which encompasses both classes and show that the reachability problem is still decidable.} }

@inproceedings{BGH-Fossacs09, address = {York, UK}, month = mar, year = 2009, volume = 5504, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {de Alfaro, Luca}, acronym = {{FoSSaCS}'09}, booktitle = {{P}roceedings of the 12th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'09)}, author = {Bollig, Benedikt and Grindei, Manuela-Lidia and Habermehl, Peter}, title = {Realizability of Concurrent Recursive Programs}, pages = {410-424}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGH-fossacs09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGH-fossacs09.pdf}, doi = {10.1007/978-3-642-00596-1_29}, abstract = {We define and study an automata model of concurrent recursive programs. An~automaton consists of a finite number of pushdown systems running in parallel and communicating via shared actions. Actually, we combine multi-stack visibly pushdown automata and Zielonka's asynchronous automata towards a model with an undecidable emptiness problem. However, a reasonable restriction allows us to lift Zielonka's Theorem to this recursive setting and permits a logical characterization in terms of a suitable monadic second-order logic. Building on results from Mazurkiewicz trace theory and work by La~Torre, Madhusudan, and Parlato, we thus develop a framework for the specification, synthesis, and verification of concurrent recursive processes.} }

@inproceedings{FGL-stacs2009, address = {Freiburg, Germany}, month = feb, year = 2009, volume = 3, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Albers, Susanne and Marion, Jean-Yves}, acronym = {{STACS}'09}, booktitle = {{P}roceedings of the 26th {A}nnual {S}ymposium on {T}heoretical {A}spects of {C}omputer {S}cience ({STACS}'09)}, author = {Finkel, Alain and Goubault{-}Larrecq, Jean}, title = {Forward Analysis for~{WSTS}, Part~{I}: Completions}, pages = {433-444}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGL-stacs2009.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGL-stacs2009.pdf}, abstract = {Well-structured transition systems provide the right foundation to compute a finite basis of the set of predecessors of the upward closure of a state. The~dual problem, to compute a finite representation of the set of successors of the downward closure of a state, is~harder: Until now, the theoretical framework for manipulating downward-closed sets was missing. We~answer this problem, using insights from domain theory (dcpos and ideal completions), from topology (sobrifications), and shed new light on the notion of adequate domains of limits.} }

@inproceedings{CGS-sofsem09, address = {\v{S}pindler\r{u}v Ml\'{y}n, Czech Republic}, month = jan, year = 2009, volume = 5404, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Nielsen, Mogens and Ku{\v c}era, Anton{\'\i}n and Bro Miltersen, Peter and Palamidessi, Catuscia and T{\r{u}}ma, Petr and Valencia, Franck}, acronym = {{SOFSEM}'09}, booktitle = {{P}roceedings of the 35th International Conference on Current Trends in Theory and Practice of Computer Science ({SOFSEM}'09)}, author = {Chatain, {\relax Th}omas and Gastin, Paul and Sznajder, Nathalie}, title = {Natural Specifications Yield Decidability for Distributed Synthesis of Asynchronous Systems}, pages = {141-152}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CGS-sofsem09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CGS-sofsem09.pdf}, doi = {10.1007/978-3-540-95891-8_16}, abstract = {We study the synthesis problem in an asynchronous distributed setting: a finite set of processes interact locally with an uncontrollable environment and communicate with each other by sending signals---actions that are immediately received by the target process. The synthesis problem is to come up with a local strategy for each process such that the resulting behaviours of the system meet a given specification. We consider external specifications over partial orders. External means that specifications only relate input and output actions from and to the environment and not signals exchanged by processes. We also ask for some closure properties of the specification. We present this new setting for studying the distributed synthesis problem, and give decidability results: the non-distributed case, and the subclass of networks where communication happens through a strongly connected graph. We believe that this framework for distributed synthesis yields decidability results for many more architectures.} }

@inproceedings{BDLM-lfcs09, address = {Deerfield Beach, Florida, USA}, month = jan, year = 2009, volume = 5407, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Artemov, Sergei N. and Nerode, Anil}, notefortitle = {6th edition of the conference}, acronym = {{LFCS}'09}, booktitle = {{P}roceedings of the {S}ymposium on {L}ogical {F}oundations of {C}omputer {S}cience ({LFCS}'09)}, author = {Brihaye, {\relax Th}omas and Da{~}Costa, Arnaud and Laroussinie, Fran{\c{c}}ois and Markey, Nicolas}, title = {{ATL}~with Strategy Contexts and Bounded Memory}, pages = {92-106}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDLM-lfcs09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDLM-lfcs09.pdf}, doi = {10.1007/978-3-540-92687-0_7}, abstract = {We extend the alternating-time temporal logics ATL and ATL\textsuperscript{*} with \emph{strategy contexts} and \emph{memory constraints}: the first extension make strategy quantifiers to not {"}forget{"} the strategies being executed by the other players. The second extension allows strategy quantifiers to restrict to memoryless or bounded-memory strategies.\par We first consider expressiveness issues. We show that our logics can express important properties such as equilibria, and we formally compare them with other similar formalisms (ATL, ATL\textsuperscript{*}, Game Logic, Strategy Logic,~...). We~then address the problem of model-checking for our logics, providing a PSPACE algoritm for the sublogics involving only memoryless strategies and an EXPSPACE algorithm for the bounded-memory case.} }

@inproceedings{steel-escar09, address = {D{\"u}sseldorf, Germany}, month = nov, year = 2009, editor = {Paar, Christof and Wollinger, Thomas}, acronym = {{ESCAR}'09}, booktitle = {{P}roceedings of the 7th {C}onference on {E}mbedded {S}ecurity in {C}ars ({ESCAR}'09)}, author = {Steel, Graham}, title = {Towards a Formal Analysis of the {S}e{V}e{C}o{M}~{API}}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/steel-escar09.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/steel-escar09.pdf} }

@inproceedings{steel-fcc09, address = {Port Jefferson, New York, USA}, month = jul, year = 2009, editor = {K{\"u}sters, Ralf}, acronym = {{FCC}'09}, booktitle = {{P}roceedings of the 5th {W}orkshop on {F}ormal and {C}omputational {C}ryptography ({FCC}'09)}, author = {Steel, Graham}, title = {Computational Soundness for {API}s}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/steel-fcc09.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/steel-fcc09.pdf} }

@inproceedings{LS-DL09, address = {Oxford, UK}, month = jul, year = 2009, volume = 477, series = {CEUR Workshop Proceedings}, publisher = {RWTH Aachen, Germany}, editor = {Cuenca Grau, Bernardo and Horrocks, Ian and Motik, Boris and Sattler, Ulrike }, acronym = {{DL}'09}, booktitle = {{P}roceedings of the 22nd {I}nternational {W}orkshop {D}escription {L}ogic ({DL}'09)}, author = {Libkin, Leonid and Sirangelo, Cristina}, title = {Open and closed world assumptions in data exchange}, pages = {1-6}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-DL09.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-DL09.pdf} }

@inproceedings{BFCH-dsn09, address = {Estoril, Portugal}, month = jun # {-} # jul, year = 2009, publisher = {{IEEE} Computer Society Press}, noeditor = {}, acronym = {{DSN}'09}, booktitle = {{P}roceedings of the 39th {A}nnual {IEEE}{\slash}{IFIP} {I}nternational {C}onference on {D}ependable {S}ystems and {N}etworks ({DSN}'09)}, author = {Beccuti, Marco and Franceschinis, Giuliana and Codetta{-}Raiteri, Daniele and Haddad, Serge}, title = {Parametric {NdRFT} for the derivation of optimal repair strategies}, pages = {399-408}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFCH-dsn09.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFCH-dsn09.pdf}, doi = {10.1109/DSN.2009.5270312}, abstract = {Non deterministic Repairable Fault Trees~(NdRFT) are a recently proposed modeling formalism for the study of optimal repair strategies: they are based on the widely adopted Fault Tree formalism, but in addition to the failure modes, NdRFTs allow to define possible repair actions. In a previous pa per the formalism has been introduced together with an analysis method and a tool allowing to automatically derive the best repair strategy to be applied in each state. The analysis technique is based on the generation and solution of a Markov Decision Process. In this paper we present an extension, ParNdRFT, that allows to exploit the presence of redundancy to reduce the complexity of the model and of the analysis. It is based on the translation of the ParNdRFT in to a Markov Decision Well-Formed Net, i.e. a model specified by means of an High Level Petri Net formalism. The translated model can be efficiently solved thanks to existing algorithms that generate a reduced state space automatically exploiting the model symmetries.} }

@article{ASV-tods09, publisher = {ACM Press}, journal = {ACM Transactions on Database Systems}, author = {Abiteboul, Serge and Segoufin, Luc and Vianu, Victor}, title = {Static Analysis of {A}ctive {XML} Systems}, volume = 34, number = 4, month = dec, year = 2009, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ASV-tods09.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ASV-tods09.pdf}, doi = {10.1145/1620585.1620590}, abstract = {Active XML is a high-level specification language tailored to data-intensive, distributed, dynamic Web services. Active XML is based on XML documents with embedded function calls. The state of a document evolves depending on the result of internal function calls (local computations) or external ones (interactions with users or other services). Function calls return documents that may be active, and so may activate new subtasks. The focus of this article is on the verification of temporal properties of runs of Active XML systems, specified in a tree-pattern-based temporal logic, Tree-LTL, which allows expressing a rich class of semantic properties of the application. The main results establish the boundary of decidability and the complexity of automatic verification of Tree-LTL properties.} }

@article{BMSS-jacm09, publisher = {ACM Press}, journal = {Journal of the~{ACM}}, author = {Boja{\'n}czyk, Miko{\l}aj and Muscholl, Anca and Schwentick, {\relax Th}omas and Segoufin, Luc}, title = {Two-variable logic on data trees and applications to {XML} reasoning}, volume = 56, number = 3, month = may, year = 2009, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMSS-jacm09.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMSS-jacm09.pdf}, doi = {10.1145/1516512.1516515}, abstract = {Motivated by reasoning tasks for XML languages, the satisfiability problem of logics on \emph{data trees} is investigated. The nodes of a data tree have a \emph{label} from a finite set and a \emph{data value} from a possibly infinite set. It is shown that satisfiability for two-variable first-order logic is decidable if the tree structure can be accessed only through the \emph{child} and the \emph{next sibling} predicates and the access to data values is restricted to equality tests. From this main result, decidability of satisfiability and containment for a data-aware fragment of XPath and of the implication problem for unary key and inclusion constraints is concluded.} }

@article{BS-jsl09, publisher = {Association for Symbolic Logic}, journal = {Journal of Symbolic Logic}, author = {Benedikt, Michael and Segoufin, Luc}, title = {Towards a Characterization of Order-Invariant Queries over Tame Structures}, volume = 74, number = 1, pages = {168-186}, month = mar, year = 2009, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-jsl09.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-jsl09.pdf}, doi = {10.2178/jsl/1231082307}, abstract = {This work deals with the expressive power of logics on finite graphs with access to an additional {"}arbitrary{"} linear order. The queries that can be expressed this way are the \emph{order-invariant queries} for the logic. For the standard logics used in computer science, such as first-order logic, it is known that access to an arbitrary linear order increases the expressiveness of the logic. However, when we look at the separating examples, we find that they have satisfying models whose Gaifman Graph is complex---unbounded in valence and in treewidth. We thus explore the expressiveness of order-invariant queries over well-behaved graphs. We prove that first-order order-invariant queries over strings and trees have no additional expressiveness over first-order logic in the original signature. We also prove new upper bounds on order-invariant queries over bounded treewidth and bounded valence graphs. Our results make use of a new technique of independent interest: the application of algebraic characterizations of definability to show collapse results.} }

@incollection{DBBetal-CES09, author = {David, Alexandre and Behrmann, Gerd and Bulychev, Peter and Byg, Joakin and Chatain, {\relax Th}omas and Larsen, Kim G. and Pettersson, Paul and Rasmussen, Jacob Illum and Srba, Ji{\v{r}}{\'\i} and Yi, Wang and Joergensen, Kenneth Y. and Lime, Didier and Magnin, Morgan and Roux, Olivier H. and Traonouez, Louis-Marie}, title = {Tools for Model-Checking Timed Systems}, booktitle = {Communicating Embedded Systems~-- Software and Design}, editor = {Jard, Claude and Roux, Olivier H.}, publisher = {Wiley-ISTE}, year = 2009, month = oct, pages = {165-225}, chapter = 6, url = {http://www.iste.co.uk/index.php?f=x&ACTION=View&id=288}, nops = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/.ps}, nopsgz = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PSGZ/.ps.gz}, isbn = {9781848211438} }

@misc{avote-D21, nocontributor = {Ciob{\^a}c{\u{a}}, {\c{S}}tefan and Delaune, St{\'e}phanie and Kremer, Steve}, author = {Ciob{\^a}c{\u{a}}, {\c{S}}tefan and Cortier, V{\'e}ronique}, title = {Algorithmes pour l'{\'e}quivalence statique}, year = 2009, month = sep, type = {Contract Report}, howpublished = {Deliverable AVOTE~2.1 (ANR-07-SESU-002)}, note = {17~pages}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/avote-d21.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/avote-d21.pdf} }

@inproceedings{BBJ-iscc09, address = {Sousse, Tunisia}, month = jul, year = 2009, publisher = {{IEEE} Computer Society Press}, noeditor = {}, acronym = {{ISCC}'09}, booktitle = {{P}roceedings of the 14th {IEEE} {S}ymposium on {C}omputers and {C}ommunications ({ISCC}'09)}, author = {Ben Youssef, Nihel and Bouhoula, Adel and Jacquemard, Florent}, title = {Automatic Verification of Conformance of Firewall Configurations to Security Policies}, pages = {526 - 531}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBJ-iscc09.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBJ-iscc09.pdf}, doi = {10.1109/ISCC.2009.5202309}, abstract = {The configuration of firewalls is highly error prone and automated solution are needed in order to analyze its correctness. We propose a formal and automatic method for checking whether a firewall reacts correctly with respect to a security policy given in an high level declarative language. When errors are detected, some feedback is returned to the user in order to correct the firewall configuration. Furthermore, the procedure verifies that no conflicts exist within the security policy. We show that our method is both correct and complete. Finally, it has been implemented in a prototype of verifier based on a satisfiability solver modulo theories (SMT). Experiment conducted on relevant case studies demonstrate the efficiency and scalability of the approach.} }

@misc{averiles09-f2.2, author = {LIAFA and CRIL and EDF and LSV and Verimag}, title = {Projet {RNTL} {A}veriles~-- Fourniture F2.2~: Algorithmes de v{\'e}rification~-- Rapport final}, year = 2009, month = nov, type = {Contract Report}, note = {25~pages}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/averiles-f22.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/averiles-f22.pdf} }

@inproceedings{haar-cdcccc09, address = {Shanghai, China}, month = dec, year = 2009, publisher = {{IEEE} Control System Society}, acronym = {{CDC/CCC}'09}, booktitle = {{P}roceedings of the Joint 48th {IEEE} {C}onference on {D}ecision and {C}ontrol ({CDC}'09) and 28th {C}hinese {C}ontrol {C}onference ({CCC}'09)}, author = {Haar, Stefan}, title = {Qualitative Diagnosability of Labeled {P}etri Nets Revisited}, pages = {1248-1253}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/haar-cdc09.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/haar-cdc09.pdf}, doi = {10.1109/CDC.2009.5400917}, abstract = {In recent years, classical discrete event fault diagnosis techniques have been extended to Petri Net system models under partial order semantics. In~a recent paper, we showed how to take further advantage of the partial order representation of concurrent processes, by decomposing the unfolding into 'facets', formed by subnets whose events either all occur eventually, or none of them occurs. A~notion of \emph{q(ualitative)}-diagnosability was proposed based on this decomposition. The present paper corrects the definition of q-diagnosability and develops its properties. Sufficient and necessary criteria, on the transition labeling, for q-diagnosability are shown; for their verification, and diagnosis itself, compact data structures are sufficient.} }

@misc{Quasimodo-3.5, author = {Laroussinie, Fran{\c{c}}ois and Vaandrager, Frits and Neuh{\"a}u{\ss}er, Martin}, title = {Extended timed automata for scheduling}, howpublished = {Deliverable QUASIMODO~3.5 (ICT-FP7-STREP-214755)}, year = 2009, month = jul }

@misc{Quasimodo-2.2, author = {Markey, Nicolas and Berendsen, Jasper and David, Alexandre and Han, Tingting and Hermanns, Holger and Larsen, Kim G. and Neuh{\"a}u{\ss}er, Martin}, title = {Symbolic data structures and analysis of models with multiple quantitative aspects}, howpublished = {Deliverable QUASIMODO~2.2 (ICT-FP7-STREP-214755)}, year = 2009, month = jul }

@inproceedings{ABGM-time09, address = {Brixen-Bressanone, Italy}, month = jul, year = 2009, publisher = {{IEEE} Computer Society Press}, noeditor = {Lutz, Carsten and Raskin, Jean-Fran{\c{c}}ois}, acronym = {{TIME}'09}, booktitle = {{P}roceedings of the 16th {I}nternational {S}ymposium on {T}emporal {R}epresentation and {R}easoning ({TIME}'09)}, title = {The {AXML} Artifact Model}, author = {Abiteboul, Serge and Bourhis, Pierre and Galland, Alban and Marinoiu, Bogdan}, pages = {11-17}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGM-time09.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGM-time09.pdf}, abstract = {Towards a data-centric workflow approach, we introduce an \emph{artifact model} to capture data and workflow management activities in distributed settings. The model is built on Active XML, \textit{i.e.}, XML trees including Web service calls. We argue that the model captures the essential features of business artifacts as described informally in [Nigam and Caswell~(2003)] or discussed in [Hull~(2008)]. To illustrate, we briefly consider the \emph{monitoring} of distributed systems and the \emph{verification} of temporal properties for them.} }

@comment{{B-arxiv16, author = Bollig, Benedikt, affiliation = aff-LSVmexico, title = One-Counter Automata with Counter Visibility, institution = Computing Research Repository, number = 1602.05940, month = feb, nmonth = 2, year = 2016, type = RR, axeLSV = mexico, NOcontrat = "", url = http://arxiv.org/abs/1602.05940, PDF = "http://www.lsv.fr/Publis/PAPERS/PDF/B-arxiv16.pdf", lsvdate-new = 20160222, lsvdate-upd = 20160222, lsvdate-pub = 20160222, lsv-category = "rapl", wwwpublic = "public and ccsb", note = 18~pages, abstract = "In a one-counter automaton (OCA), one can read a letter from some finite alphabet, increment and decrement the counter by one, or test it for zero. It is well-known that universality and language inclusion for OCAs are undecidable. We consider here OCAs with counter visibility: Whenever the automaton produces a letter, it outputs the current counter value along with~it. Hence, its language is now a set of words over an infinite alphabet. We show that universality and inclusion for that model are in PSPACE, thus no harder than the corresponding problems for finite automata, which can actually be considered as a special case. In fact, we show that OCAs with counter visibility are effectively determinizable and closed under all boolean operations. As~a~strict generalization, we subsequently extend our model by registers. The general nonemptiness problem being undecidable, we impose a bound on the number of register comparisons and show that the corresponding nonemptiness problem is NP-complete.", }}

*This file was generated by
bibtex2html 1.98.*