@inproceedings{ABGR-datalog10, address = {Oxford, UK}, month = mar, year = 2011, volume = 6702, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {de Moor, Oege and Gottlob, Georg and Furche, Tim and Sellers, Andrew Jon}, acronym = {{D}atalog'10}, booktitle = {{R}evised {S}elected {P}apers of the 1st {I}nternational {W}orkshop {D}atalog {R}eloaded ({D}atalog'10)}, author = {Abiteboul, Serge and Bienvenu, Meghyn and Galland, Alban and Rousset, Marie-{\relax Ch}ristine}, title = {Distributed {D}atalog Revisited}, pages = {252-261}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGR-datalog10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGR-datalog10.pdf}, doi = {10.1007/978-3-642-24206-9_15} }

@article{bbdfh-pe10, publisher = {Elsevier Science Publishers}, journal = {Performance Evaluation}, author = {Baarir, Souheib and Beccuti, Marco and Dutheillet, Claude and Franceschinis, Giuliana and Haddad, Serge}, title = {Lumping partially symmetrical stochastic models}, volume = 76, nunmber = 1, month = jan, pages = {21-44}, year = 2011, url = {http://www.lsv.fr/Publis/PAPERS/PDF/bbdfh-pe10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bbdfh-pe10.pdf}, doi = {10.1016/j.peva.2010.09.002}, abstract = {The performance and dependability evaluation of complex systems by means of dynamic stochastic models (e.g. Markov chains) may be impaired by the combinatorial explosion of their state space. Among the possible methods to cope with this problem, symmetry-based ones can be applied to systems including several similar components. Often however these systems are only partially symmetric: their behavior is in general symmetric except for some local situation when the similar components need to be differentiated.\par In this paper two methods to efficiently analyze partially symmetrical models are presented in a general setting and the requirements for their efficient implementation are discussed. Some case studies are presented to show the methods' effectiveness and their applicative interest.} }

@article{JKV-icomp10, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Jacquemard, Florent and Klay, Francis and Vacher, Camille}, title = {Rigid Tree Automata}, volume = {209}, number = 3, pages = {486-512}, year = 2011, month = mar, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JKV-icomp11.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JKV-icomp11.pdf}, doi = {10.1016/j.ic.2010.11.015}, 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.} }

@article{AFFM-rsl10, publisher = {Cambridge University Press}, journal = {Review of Symbolic Logic}, author = {Areces, Carlos and Figueira, Diego and Figueira, Santiago and Mera, Sergio}, title = {The Expressive Power of Memory Logics}, year = {2011}, month = jun, volume = 4, number = 2, pages = {290 - 318 }, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AFFM-rsl10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AFFM-rsl10.pdf}, doi = {10.1017/S1755020310000389}, abstract = {We investigate the expressive power of \emph{memory logics}. These are modal logics extended with the possibility to store (or remove) the current node of evaluation in (or from) a \emph{memory}, and to perform membership tests on the current memory. From this perspective, the hybrid logic \(\mathcal{HL}(\downarrow)\), for example, can be thought of as a particular case of a memory logic where the memory is an indexed list of elements of the domain.\par This work focuses in the case where the memory is a set, and we can test whether the current node belongs to the set or not. We prove that, in terms of expressive power, the memory logics we discuss here lie between the basic modal logic \(\mathcal{K}\) and \(\mathcal{HL}(\downarrow)\). We show that the satisfiability problem of most of the logics we cover is undecidable. The only logic with a decidable satisfiability problem is obtained by imposing strong constraints on which elements can be memorized.} }

@inproceedings{CSV-vmcai11, address = {Austin, Texas, USA}, month = jan, year = 2011, volume = 6538, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Jhala, Ranjit and Schmidt, David}, acronym = {{VMCAI}'11}, booktitle = {{P}roceedings of the 12th {I}nternational {C}onference on {V}erification, {M}odel {C}hecking and {A}bstract {I}nterpretation ({VMCAI}'11)}, author = {Chadha, Rohit and Sistla, A. Prasad and Viswanathan, Mahesh}, title = {Probabilistic {B}{\"u}chi automata with non-extremal acceptance thresholds}, pages = {103-117}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CSV-vmcai11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CSV-vmcai11.pdf}, doi = {10.1007/978-3-642-18275-4_9}, abstract = {This paper investigates the power of Probabilistic B{\"u}chi Automata~(PBA) when the threshold probability of acceptance is non-extremal, i.e., is a value strictly between 0 and 1. Many practical randomized algorithms are designed to work under non-extremal threshold probabilities and thus it is important to study power of PBAs for such cases.\par The paper presents a number of surprising expressiveness and decidability results for PBAs when the threshold probability is non-extremal. Some of these results sharply contrast with the results for extremal threshold probabilities. The paper also presents results for Hierarchical PBAs and for an interesting subclass of them called simple PBAs.} }

@incollection{DR-lgtcs10, month = jan, year = 2011, publisher = {Cambridge University Press}, booktitle = {Lectures in Game Theory for Computer Scientists}, editor = {Apt, Krzysztof R. and Gr{\"a}del, Erich}, author = {Doyen, Laurent and Raskin, Jean-Fran{\c{c}}ois}, title = {Games with Imperfect Information: Theory and Algorithms}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DR-lgtcs10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DR-lgtcs10.pdf}, ps = {DR-lgtcs10.ps} }

@article{GLK-mscs10, publisher = {Cambridge University Press}, journal = {Mathematical Structures in Computer Science}, author = {Goubault{-}Larrecq, Jean and Keimel, Klaus}, title = {{C}hoquet-{K}endall-{M}atheron Theorems for Non-{H}ausdorff Spaces}, volume = 21, number = 3, pages = {511-561}, month = jun, year = 2011, url = {http://www.lsv.fr/Publis/PAPERS/PDF/GLK-mscs10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLK-mscs10.pdf}, doi = {10.1017/S0960129510000617}, abstract = {We establish Choquet-Kendall-Matheron theorems on non-Hausdorff topological spaces. This typical result of random set theory is profitably recast in purely topological terms, using intuitions and tools from domain theory. We obtain three variants of the theorem, each one characterizing distributions, in the form of continuous valuations, over relevant powerdomains of demonic, resp. angelic, resp. erratic non-determinism.} }

@article{BCL-jlli10, publisher = {Kluwer Academic Publishers}, journal = {Journal of Logic, Language and Information}, author = {Bouyer, Patricia and Cassez, Franck and Laroussinie, Fran{\c{c}}ois}, title = {Timed Modal Logics for Real-Time Systems: Specification, Verification and Control}, volume = 20, number = 2, pages = {169-203}, year = 2011, month = apr, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCL-jlli10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCL-jlli10.pdf}, doi = {10.1007/s10849-010-9127-4}, abstract = {In this paper, a timed modal logic~\(L_{c}\) is presented for the specification and verification of real-time systems. Several important results for~\(L_{c}\) are discussed. First we address the model checking problem and we show that it is an EXPTIME-complete problem. Secondly we consider expressiveness and we explain how to express strong timed bisimilarity and how to build characteristic formulas for timed automata. We also propose a compositional algorithm for~\(L_{c}\) model checking. Finally we consider several control problems for which \(L_{c}\) can be used to check controllability.} }

@article{AGM-jcss11, publisher = {Elsevier Science Publishers}, journal = {Journal of Computer and System Sciences}, author = {Abiteboul, Serge and Gottlob, Georg and Manna, Marco}, title = {Distributed {XML} design}, volume = 77, number = 6, pages = {936-964}, month = nov, year = 2011, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AGM-jcss11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGM-jcss11.pdf}, doi = {10.1016/j.jcss.2011.02.003}, abstract = {A distributed XML document is an XML document that spans several machines. We assume that a distribution design of the document tree is given, consisting of an \emph{XML kernel-document} \(T_{[\mathbf{f}_{1},...,\mathbf{f}_{n}]}\) where some leaves are {"}docking points{"} for external resources providing XML subtrees (\(\mathbf{f}_{1},...,\mathbf{f}_{n}\) standing, e.g., for Web services or peers at remote locations). The top-down design problem consists in, given a \emph{type} (a~schema document that may vary from a DTD to a tree automaton) for the distributed document, {"}propagating{"} locally this type into a collection of types, that we call \emph{typing}, while preserving desirable properties. We also consider the bottom-up design which consists in, given a type for each external resource, exhibiting a global type that is enforced by the local types, again with natural desirable properties. In the article, we lay out the fundamentals of a theory of distributed XML design, analyze problems concerning typing issues in this setting, and study their complexity.} }

@article{ACKNS-tods11, publisher = {ACM Press}, journal = {ACM Transactions on Database Systems}, author = {Abiteboul, Serge and Chan, T.-H. Hubert and Kharlamov, Evgeny and Nutt, Werner and Senellart, Pierre}, title = {Capturing continuous data and answering aggregate queries in probabilistic~{XML}}, volume = {36}, number = {4:25}, month = dec, year = 2011, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ACKNS-tods11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ACKNS-tods11.pdf}, doi = {10.1145/2043652.2043658}, abstract = {Sources of data uncertainty and imprecision are numerous. A way to handle this uncertainty is to associate probabilistic annotations to data. Many such probabilistic database models have been proposed, both in the relational and in the semi-structured setting. The latter is particularly well adapted to the management of uncertain data coming from a variety of automatic processes. An important problem, in the context of probabilistic XML databases, is that of answering aggregate queries (count, sum, avg, etc.), which has received limited attention so~far. In a model unifying the various (discrete) semi-structured probabilistic models studied up to now, we present algorithms to compute the distribution of the aggregation values (exploiting some regularity properties of the aggregate functions) and probabilistic moments (especially expectation and variance) of this distribution. We also prove the intractability of some of these problems and investigate approximation techniques. We finally extend the discrete model to a continuous one, in order to take into account continuous data values, such as measurements from sensor networks, and extend our algorithms and complexity results to the continuous case.} }

@inproceedings{SGA-iswc11, address = {Bonn, Germany}, month = oct, year = 2011, volume = 7031, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Aroyo, Lora and Welty, Chris and Alani, Harith and Taylor, Jamie and Bernstein, Abraham and Kagal, Lalana and Fridman{ }Noy,Natasha and Blomqvist, Eva}, acronym = {{ISWC}'11}, booktitle = {{P}roceedings of the 10th {I}nternational {S}emantic {W}eb {C}onference ({ISWC}'11)}, author = {Suchanek, Fabian M. and Gross{-}Amblard, David and Abiteboul, Serge}, title = {Watermarking for Ontologies}, pages = {697-713}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/SGA-iswc11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SGA-iswc11.pdf}, doi = {10.1007/978-3-642-25073-6_44}, abstract = {In this paper, we study watermarking methods to prove the ownership of an ontology. Different from existing approaches, we propose to watermark not by altering existing statements, but by removing them. Thereby, our approach does not introduce false statements into the ontology. We show how ownership of ontologies can be established with provably tight probability bounds, even if only parts of the ontology are being re-used. We finally demonstrate the viability of our approach on real-world ontologies.} }

@inproceedings{AGP-webdb11, address = {Athens, Greece}, month = jun, year = 2011, editor = {Marian, Am{\'e}lie and Vassalos, Vasilis}, acronym = {({W}eb{DB}'11)}, booktitle = {{P}roceedings of the 14th {I}nternational {W}orkshop on the {W}eb and {D}atabases ({W}eb{DB}'11)}, author = {Abiteboul, Serge and Galland, Alban and Polyzotis, Neoklis}, title = {Web information management with access control}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AGP-webdb11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGP-webdb11.pdf}, abstract = {We investigate the problem of sharing private information on the Web, where the information is hosted on different machines that may use different access control and distribution schemes. We introduce a distributed knowledge-base model, termed WebdamExchange, that comprises logical statements for specifying data, access control, distribution and knowledge about other peers. The statements can be communicated, replicated, queried, and updated, while keeping track of time and provenance. This unified base allows applications to reason declaratively about what data is accessible, where it resides, and how to retrieve it securely.} }

@inproceedings{ABKT-icde11, editor = {Abiteboul, Serge and B{\"o}hm, Klemens and Koch, Christoph and Tan, Kian-Lee}, author = {Abiteboul, Serge and B{\"o}hm, Klemens and Koch, Christoph and Tan, Kian-Lee}, title = {{P}roceedings of the 27th {I}nternational {C}onference on {D}ata {E}ngineering ({ICDE}'11)}, booktitle = {{P}roceedings of the 27th {I}nternational {C}onference on {D}ata {E}ngineering ({ICDE}'11)}, year = 2011, month = apr, publisher = {{IEEE} Computer Society Press}, address = {Hannover, Germany}, doi = {10.1109/ICDE.2011.5767975}, url = {http://ieeexplore.ieee.org/xpl/tocresult.jsp?punumber=5765035} }

@inproceedings{ACK-icdt11, address = {Uppsala, Sweden}, month = mar, year = 2011, publisher = {ACM Press}, editor = {Milo, Tova}, acronym = {{ICDT}'11}, booktitle = {{P}roceedings of the 14th {I}nternational {C}onference on {D}atabase {T}heory ({ICDT}'11)}, author = {Abiteboul, Serge and ten~Cate, Balder and Katsis, Yannis}, title = {On the equivalence of distributed systems with queries and communication}, pages = {126-137}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ACK-icdt11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ACK-icdt11.pdf}, doi = {10.1145/1938551.1938570}, abstract = {Distributed data management systems consist of peers that store, exchange and process data in order to collaboratively achieve a common goal, such as evaluate some query. We study the equivalence of such systems. We model a distributed system by a collection of Active XML documents, i.e., trees augmented with function calls for performing tasks such as sending, receiving and querying data. As our model is quite general, the equivalence problem turns out to be undecidable. However, we exhibit several restrictions of the model, for which equivalence can be effectively decided. We also study the computational complexity of the equivalence problem, and present an axiomatization of equivalence, in the form of a set of equivalence-preserving rewrite rules allowing us to optimize a system by rewriting it into an equivalent, but possibly more efficient system.} }

@inproceedings{ABV-icdt11, address = {Uppsala, Sweden}, month = mar, year = 2011, publisher = {ACM Press}, editor = {Milo, Tova}, acronym = {{ICDT}'11}, booktitle = {{P}roceedings of the 14th {I}nternational {C}onference on {D}atabase {T}heory ({ICDT}'11)}, author = {Abiteboul, Serge and Bourhis, Pierre and Vianu, Victor}, title = {Comparing workflow specification languages: a~matter of views}, pages = {78-89}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABV-icdt11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABV-icdt11.pdf}, doi = {10.1145/1938551.1938564}, abstract = {We address the problem of comparing the expressiveness of workflow specification formalisms using a notion of view of a workflow. Views allow to compare widely different workflow systems by mapping them to a common representation capturing the observables relevant to the comparison. Using this framework, we compare the expressiveness of several workflow specification mechanisms, including automata, temporal constraints, and pre-and-post conditions, with XML and relational databases as underlying data models. One surprising result shows the considerable power of static constraints to simulate apparently much richer workflow control mechanisms.} }

@inproceedings{DMS-iwigp11, address = {Saarbr{\"u}cken, Germany}, month = mar, year = 2011, volume = 50, series = {Electronic Proceedings in Theoretical Computer Science}, editor = {Reich, Johannes and Finkbeiner, Bernd}, acronym = {{iWIGP}'11}, booktitle = {{P}roceedings of the {I}nternational {W}orkshop on {I}nteractions, {G}ames and {P}rotocols ({iWIGP}'11)}, author = {Doyen, Laurent and Massart, {\relax Th}ierry and Shirmohammadi, Mahsa}, title = {Synchronizing Objectives for {M}arkov Decision Processes}, pages = {61-75}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DMS-iwigp11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DMS-iwigp11.pdf} }

@inproceedings{CD-memics11, address = {Lednice, Czech Republic }, month = oct, year = 2011, volume = 7119, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Bouda, Jan and {\v{C}}ern{\'a}, Ivana and Sekanina, Luk{\'a}{\v{s}} and Vojnar, Tom{\'a}{\v{s}}}, acronym = {{MEMICS}'11}, booktitle = {{P}roceedings of the 7th {A}nnual {D}octoral {W}orkshop on {M}athematical and {E}ngineering {M}ethods in {C}omputer {S}cience ({MEMICS}'11)}, author = {Chatterjee, Krishnendu and Doyen, Laurent}, title = {Games and Markov Decision Processes with Mean-payoff Parity and Energy Parity Objectives}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-memics11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-memics11.pdf}, abstract = {The analysis of games and probabilistic systems with quantitative objectives (such as mean-payoff and energy objectives) and \(\omega\)-regular objectives (such as parity objectives) provide the mathematical foundation for performance analysis and verification of various classes of systems. In this talk, we will present a survey of both classical results and recent results about mean-payoff, energy, and parity objectives. We will discuss about how to solve their combinations, their inter-relationship, and mention interesting open problems.} }

@inproceedings{BBDDR-atva11, address = {Taipei, Taiwan}, month = oct, year = {2011}, volume = 6996, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Bultan, Tevfik and Hsiung, Pao-Ann}, acronym = {{ATVA}'11}, booktitle = {{P}roceedings of the 9th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'11)}, author = {Brihaye, {\relax Th}omas and Bruy{\`e}re, V{\'e}ronique and Doyen, Laurent and Ducobu, Marc and Raskin, Jean-Fran{\c{c}}ois}, title = {Antichain-based {QBF} Solving}, pages = {183-197}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBDDR-atva11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBDDR-atva11.pdf}, doi = {10.1007/978-3-642-24372-1_14} }

@article{BCDGR-fmsd2011, publisher = {Springer}, journal = {Formal Methods in System Design}, author = {Brim, Lubos and Chaloupka, Jakub and Doyen, Laurent and Gentilini, Raffaella and Raskin, Jean-Fran{\c{c}}ois}, title = {Faster algorithms for mean-payoff games}, year = {2011}, month = apr, volume = {38}, number = {2}, pages = {97-118}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCDGR-fmsd2011.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCDGR-fmsd2011.pdf}, doi = {10.1007/s10703-010-0105-x} }

@misc{JGL-tacl11, author = {Jean Goubault{-}Larrecq}, title = {A Few Pearls in the Theory of Quasi-Metric Spaces}, year = {2011}, month = jul, howpublished = {Invited talk, Fifth International Conference on Topology, Algebra, and Categories in Logic (TACL'11), Marseilles, France, July~2011} }

@article{BDMSS-tocl11, publisher = {ACM Press}, journal = {ACM Transactions on Computational Logic}, author = {Boja{\'n}czyk, Miko{\l}aj and David, Claire and Muscholl, Anca and Schwentick, {\relax Th}omas and Segoufin, Luc}, title = {Two-variable logic on data words}, volume = 12, number = {4:27}, nopages = {}, year = 2011, month = jul, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDMSS-tocl11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDMSS-tocl11.pdf}, doi = {10.1145/1970398.1970403} }

@article{KS-lmcs11, journal = {Logical Methods in Computer Science}, author = {Kazana, Wojciech and Segoufin, Luc}, title = {First-order query evaluation on structures of bounded degree}, volume = 7, number = {2:20}, year = 2011, month = jun, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-lmcs11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-lmcs11.pdf}, doi = {10.2168/LMCS-7(2:20)2011} }

@article{PS-lmcs11, journal = {Logical Methods in Computer Science}, author = {Place, {\relax Th}omas and Segoufin, Luc}, title = {A decidable characterization of locally testable tree languages}, volume = 7, number = {4:03}, year = 2011, month = nov, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/PS-lmcs11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PS-lmcs11.pdf}, doi = {10.2168/LMCS-7(4:3)2011} }

@inproceedings{AGLMP-icde11, address = {Hannover, Germany}, month = apr, year = 2011, publisher = {{IEEE} Computer Society Press}, editor = {Abiteboul, Serge and B{\"o}hm, Klemens and Koch, Christoph and Tan, Kian-Lee}, acronym = {{ICDE}'11}, booktitle = {{P}roceedings of the 27th {I}nternational {C}onference on {D}ata {E}ngineering ({ICDE}'11)}, author = {Antoine, {\'E}milien and Galland, Alban and Lyngbaek, Kristian and Marian, Am{\'e}lie and Polyzotis, Neoklis}, title = {Social networking on top of the WebdamExchange system}, pages = {1300-1303}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AGLMP-icde11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGLMP-icde11.pdf}, doi = {10.1109/ICDE.2011.5767939}, abstract = {The demonstration presents the WebdamExchange system, \emph{a~distributed knowledge base management system with access rights, localization and provenance}. This system is based on the exchange of logical statements that describe documents, collections, access rights, keys and localization information and updates of this data.\par We illustrate how the model can be used in a social-network context to help users keep control on their data on the web. In particular, we show how users within very different schemes of data-distribution (centralized, dht, unstructured P2P,~etc.) can still transparently collaborate while keeping a good control over their own data.} }

@inproceedings{ABGA-pods11, address = {Athens, Greece}, month = jun, year = 2011, publisher = {ACM Press}, editor = {Lenzerini, Maurizio and Schwentick, {\relax Th}omas}, acronym = {{PODS}'11}, booktitle = {{P}roceedings of the 30th {A}nnual {ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium on {P}rinciples of {D}atabase {S}ystems ({PODS}'11)}, author = {Abiteboul, Serge and Bienvenu, Meghyn and Galland, Alban and Antoine, {\'E}milien}, title = {A rule-based language for Web data management}, pages = {293-304}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGA-pods11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGA-pods11.pdf}, doi = {10.1145/1989284.1989320}, abstract = {There is a new trend to use Datalog-style rule-based languages to specify modern distributed applications, notably on the Web. We introduce here such a language for a distributed data model where peers exchange messages (i.e.,~logical facts) as well as rules. The model is formally defined and its interest for distributed data management is illustrated through a variety of examples. A~contribution of our work is a study of the impact on expressiveness of {"}delegations{"} (the installation of rules by a peer in some other peer) and explicit timestamps. We also validate the semantics of our model by showing that under certain natural conditions, our semantics converges to the same semantics as the centralized system with the same rules. Indeed, we show this is even true when updates are considered.} }

@techreport{LSV-11-24, author = {Arnaud, Mathilde and Cortier, V{\'e}ronique and Delaune, St{\'e}phanie}, title = {Modeling and Verifying Ad~Hoc Routing Protocols}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2011}, month = dec, type = {Research Report}, number = {LSV-11-24}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2011-24.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2011-24.pdf}, versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2011-24-v1.pdf, 20111220}, note = {66~pages}, abstract = {Mobile ad hoc networks consist of mobile wireless devices which autonomously organize their infrastructure. In such networks, 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 malicious nodes from compromising the discovered route.\par Our contribution is twofold. We first propose 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. Our second main contribution is a decision procedure for analyzing routing protocols for any network topology. By using constraint solving techniques, we show that it is possible to automatically discover (in~NPTIME) whether there exists a network topology that would allow malicious nodes to mount an attack against the protocol, for a bounded number of sessions. We also provide a decision procedure for detecting attacks in case the network topology is given a priori. We demonstrate the usage and usefulness of our approach by analyzing protocols of the literature, such as SRP applied to DSR and SDMSR.} }

@phdthesis{bourhis-phd2011, author = {Bourhis, Pierre}, title = {On the dynamics of active documents for distributed data management}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2011, month = feb, url = {http://www.lsv.fr/Publis/PAPERS/PDF/bourhis-these.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bourhis-these.pdf} }

@phdthesis{arnaud-phd2011, author = {Arnaud, Mathilde}, title = {Formal verification of secured routing protocols}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2011, month = dec, url = {http://www.lsv.fr/Publis/PAPERS/PDF/arnaud-these11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/arnaud-these11.pdf} }

@phdthesis{ciobaca-phd2011, author = {Ciob{\^a}c{\u{a}}, {\c{S}}tefan}, title = {Automated Verification of Security Protocols with Appplications to Electronic Voting}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2011, month = dec, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ciobaca-these11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ciobaca-these11.pdf} }

@techreport{lsv-11-23, author = {Lozes, {\'E}tienne and Villard, Jules}, title = {Sharing Contract-Obedient Endpoints}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2011}, month = dec, type = {Research Report}, number = {LSV-11-23}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2011-23.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2011-23.pdf}, versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2011-23-v1.pdf, 20111207}, note = {42~pages}, abstract = {Most of the existing verification techniques for programs based on message passing suppose either that channel endpoints are used in a linear fashion, where at most one thread can be considered as the owner of an endpoint at any given time, or that endpoints may be used arbitrarily by any number of threads. The former approach forbids the sharing of channels, while the latter limits what is provable about programs, since no constraint is put on the usage of channels. In this paper, we propose a midpoint between these techniques by extending a previously published proof system based on separation logic to allow the sharing of endpoints. We identify two independent mechanisms for supporting sharing: the standard technique based on reasoning with permissions, and a new technique based on what we call ownership on demand. We formalize these two techniques in a proof system, illustrate them on several examples, and we extend Villard's semantics and soundness proofs to support sharing.} }

@article{BCJST-ijis11, publisher = {Springer}, journal = {International Journal on Information Security}, author = {Backes, Michael and Cervesato, Iliano and Jaggard, Aaron and Scedrov, Andre and Tsay, Joe-Kai}, title = {Cryptographically sound security proofs for basic and public-key {K}erberos}, pages = {107-134}, volume = {10}, number = {2}, year = {2011}, month = jun, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCJST-ijis11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCJST-ijis11.pdf}, doi = {10.1007/s10207-011-0125-6} }

@inproceedings{ILV-imacc11, address = {Oxford, UK}, month = dec, year = 2011, volume = {7089}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Chen, Liqun}, acronym = {{IMACC}'11}, booktitle = {{P}roceedings of the 13th {IMA} {I}nternational {C}onference on {C}ryptography and {C}oding ({IMACC}'11)}, author = {Izabach{\`e}ne, Malika and Libert, Beno{\^\i}t and Vergnaud, Damien}, title = {Block-wise {P}-Signatures and Non-Interactive Anonymous Credentials with Efficient Attributes}, pages = {431-450}, doi = {10.1007/978-3-642-25516-8_26}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ILV-imacc11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ILV-imacc11.pdf}, abstract = {Anonymous credentials are protocols in which users obtain certificates from organizations and subsequently demonstrate their possession in such a way that transactions carried out by the same user cannot be linked. We present an anonymous credential scheme with non-interactive proofs of credential possession where credentials are associated with a number of attributes. Following recent results of Camenisch and Gro\ss{} (CCS~2008), the proof simultaneously convinces the verifier that certified attributes satisfy a certain predicate. Our construction relies on a new kind of P-signature, termed \emph{block-wise P-signature}, that allows a user to obtain a signature on a committed vector of messages and makes it possible to generate a short witness that serves as a proof that the signed vector satisfies the predicate. A~non-interactive anonymous credential is obtained by combining our \emph{block-wise} P-signature scheme with the Groth-Sahai proof system. It allows efficiently proving possession of a credential while simultaneously demonstrating that underlying attributes satisfy a predicate corresponding to the evaluation of inner products (and therefore disjunctions or polynomial evaluations). The security of our scheme is proved in the standard model under non-interactive assumptions.} }

@book{LPS-book11, author = {Luccio, Fabrizio and Pagli, Linda and Steel, Graham}, title = {Mathematical and Algorithmic Foundations of the Internet}, publisher = {CRC Press}, year = 2011, month = jul, url = {https://www.crcpress.com/9781439831380} }

@incollection{steel-crypt2011, author = {Steel, Graham}, title = {Formal Analysis of Security~{API}s}, booktitle = {Encyclopedia of Cryptography and Security}, edition = {2nd}, editor = {van Tilborg, Henk C. A. and Jajodia, Sushil}, year = {2011}, pages = {492-494}, publisher = {Springer}, doi = {10.1007/978-1-4419-5906-5_873} }

@inproceedings{JKS-frocos11, address = {Saarbr{\"u}cken, Germany}, month = oct, year = 2011, volume = 6989, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, editor = {Tinelli, Cesare and Sofronie-Stokkermans, Viorica}, acronym = {{FroCoS}'11}, booktitle = {{P}roceedings of the 8th {I}nternational {S}ymposium on {F}rontiers of {C}ombining {S}ystems ({FroCoS}'11)}, author = {Jacquemard, Florent and Kojima, Yoshiharu and Sakai, Masahiko}, title = {Controlled Term Rewriting}, pages = {179-194}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/JKS-frocos11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JKS-frocos11.pdf}, doi = {}, abstract = {Motivated by the problem of verification of imperative tree transformation programs, we study the combination, called controlled term rewriting systems~(CTRS), of term rewriting rules with constraints selecting the possible rewrite positions. These constraints are specified, for each rewrite rule, by a selection automaton which defines a set of positions in a term based on tree automata computations.\par We show that reachability is PSPACE-complete for so-called monotonic CTRS, such that the size of every left-hand-side of every rewrite rule is larger or equal to the size of the corresponding right-hand-side, and also for the class of context-free non-collapsing CTRS, which transform CF tree language into CF tree languages.\par When allowing size-reducing rules, reachability becomes undecidable, even for flat CTRS (both sides of rewrite rules are of depth at most one) when restricting to words (i.e. function symbols have arity at most one), and for ground CTRS (rewrite rules have no variables).\par We also consider a restricted version of the control such that a position is selected if the sequence of symbols on the path from that position to the root of the tree belongs to a given regular language. This restriction enables decision results in the above cases.} }

@phdthesis{jacquemard-HDR11, author = {Jacquemard, Florent}, title = {Extended Tree Automata for the Verification of Infinite State Systems}, year = 2011, month = nov, type = {M{\'e}moire d'habilitation}, school = {{\'E}cole Normale Sup{\'e}rieure de Cachan, France}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/hdr-fj11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/hdr-fj11.pdf} }

@article{CSV-lmcs11, journal = {Logical Methods in Computer Science}, author = {Chadha, Rohit and Sistla, A. Prasad and Viswanathan, Mahesh}, title = {Power of Randomization in Automata on Infinite Strings}, year = {2011}, month = sep, volume = {7}, number = {3:22}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CSV-lmcs11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CSV-lmcs11.pdf}, doi = {10.2168/LMCS-7(3:22)2011}, abstract = {Probabilistic B{\"u}chi Automata~(PBA) are randomized, finite state automata that process input strings of infinite length. Based on the threshold chosen for the acceptance probability, different classes of languages can be defined. In this paper, we present a number of results that clarify the power of such machines and properties of the languages they define. The broad themes we focus on are as follows. We present results on the decidability and precise complexity of the emptiness, universality and language containment problems for such machines, thus answering questions central to the use of these models in formal verification. Next, we characterize the languages recognized by PBAs topologically, demonstrating that though general PBAs can recognize languages that are not regular, topologically the languages are as simple as \(\omega\)-regular languages. Finally, we introduce Hierarchical PBAs, which are syntactically restricted forms of PBAs that are tractable and capture exactly the class of \(\omega\)-regular languages.} }

@inproceedings{FRS-infinity11, address = {Taipei, Taiwan}, month = oct, year = 2011, volume = 73, series = {Electronic Proceedings in Theoretical Computer Science}, editor = {Chen, Yu-Fang and Wang, Chao}, acronym = {{INFINITY}'11}, booktitle = {{P}roceedings of the 13th {I}nternational {W}orkshops on {V}erification of {I}nfinite {S}tate {S}ystems ({INFINITY}'11)}, author = {Fribourg, Laurent and Revol, Bertrand and Soulat, Romain}, title = {Synthesis of Switching Rules for Ensuring Reachability Properties of Sampled Linear Systems}, pages = {35-48}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FRS-infinity11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FRS-infinity11.pdf}, doi = {10.4204/EPTCS.73.6}, abstract = {We consider here systems with piecewise linear dynamics that are periodically sampled with a given period~\(\tau\). At each sampling time, the mode of the system, i.e., the parameters of the linear dynamics, can be switched, according to a switching rule. Such systems can be modelled as a special form of hybrid automata, called {"}switched systems{"}, that are automata with an \emph{infinite} real state space. The problem is to find a switching rule that guarantees the system to still be in a given area~\(V\) at the next sampling time, and so on indefinitely. In this paper, we will consider two approaches: the~\emph{indirect} one that abstracts the system under the form of a finite discrete event system, and the \emph{direct} one that works on the continuous state space.\par Our methods rely on previous works, but we specialize them to a simplified context (linearity, periodic switching instants, absence of control input), which is motivated by the features of a focused case study: a~DC-DC boost converter built by electronics laboratory SATIE (ENS~Cachan). Our enhanced methods allow us to treat successfully this real-life example.} }

@mastersthesis{kumardhar-master, author = {Kumar Dhar, Amit}, title = {Counter Systems with {P}resburger-definable Reachability Sets: Decidability and Complexity}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2011}, month = sep, url = {http://www.lsv.fr/Publis/PAPERS/PDF/akd11-m2.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/akd11-m2.pdf} }

@inproceedings{BD-frocos11, address = {Saarbr{\"u}cken, Germany}, month = oct, year = 2011, volume = 6989, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, editor = {Tinelli, Cesare and Sofronie-Stokkermans, Viorica}, acronym = {{FroCoS}'11}, booktitle = {{P}roceedings of the 8th {I}nternational {S}ymposium on {F}rontiers of {C}ombining {S}ystems ({FroCoS}'11)}, author = {Bersani, Marcello and Demri, St{\'e}phane}, title = {The complexity of reversal-bounded model-checking}, pages = {71-86}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BD-frocos11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BD-frocos11.pdf}, doi = {10.1007/978-3-642-24364-6_6}, abstract = {We study model-checking problems on counter systems when guards are quantifier-free Presburger formulae, the specification languages are LTL-like dialects with arithmetical constraints and the runs are restricted to reversal-bounded ones. We introduce a generalization of reversal-boundedness and we show the NExpTime-completeness of the reversal-bounded model-checking problem as well as for related reversalbounded reachability problems. As a by-product, we show the effective Presburger definability for sets of configurations for which there is a reversal-bounded run verifying a given temporal formula. Our results generalize existing results about reversal-bounded counter automata and provides a uniform and more general framework.} }

@phdthesis{chambart-phd2011, author = {Chambart, Pierre}, title = {Du Probl{\`e}me de sous-mot de {P}ost et de la complexit{\'e} des canaux non fiables}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2011, month = sep, url = {http://www.lsv.fr/Publis/PAPERS/PDF/chambart-these11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/chambart-these11.pdf} }

@phdthesis{galland-phd2011, author = {Galland, Alban}, title = {Distributed Data Management with Access Control}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2011, month = sep, url = {http://www.lsv.fr/Publis/PAPERS/PDF/galland-these11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/galland-these11.pdf} }

@book{webdam2011, author = {Abiteboul, Serge and Manolescu, Ioana and Rigaux, {\relax Ph}ilippe and Rousset, Marie-{\relax Ch}ristine and Senellart, Pierre}, title = {Web Data Management}, year = 2011, publisher = {Cambridge University Press}, url = {http://webdam.inria.fr/Jorge/} }

@article{UW-lmcs11, journal = {Logical Methods in Computer Science}, author = {Ummels, Michael and Wojtczak, Dominik}, title = {The Complexity of {N}ash Equilibria in Stochastic Multiplayer Games}, year = {2011}, month = sep, volume = {7}, number = {3:20}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/UW-lmcs11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/UW-lmcs11.pdf}, doi = {10.2168/LMCS-7(3:20)2011}, abstract = {We analyse the computational complexity of finding Nash equilibria in turn-based stochastic multiplayer games with omega-regular objectives. We show that restricting the search space to equilibria whose payoffs fall into a certain interval may lead to undecidability. In particular, we prove that the following problem is undecidable: Given a game~\(G\), does there exist a Nash equilibrium of~\(G\) where Player~\(0\) wins with probability~\(1\)? Moreover, this problem remains undecidable when restricted to pure strategies or (pure) strategies with finite memory. One way to obtain a decidable variant of the problem is to restrict the strategies to be positional or stationary. For the complexity of these two problems, we obtain a common lower bound of NP and upper bounds of NP and PSPACE respectively. Finally, we single out a special case of the general problem that, in many cases, admits an efficient solution. In particular, we prove that deciding the existence of an equilibrium in which each player either wins or loses with probability~\(1\) can be done in polynomial time for games where the objective of each player is given by a parity condition with a bounded number of priorities.} }

@techreport{lsv-11-20, author = {Berwanger, Dietmar and Kaiser, {\L}ukasz and Le{\ss}enich, Simon}, title = {Imperfect Recall and Counter Games}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2011}, month = oct, type = {Research Report}, number = {LSV-11-20}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2011-20.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2011-20.pdf}, note = {21~pages}, abstract = {We study a class of omega-regular games with imperfect information and imperfect recall, and present a solution method which relies on the MSO-compatibility of graph unfoldings. Furthermore, we show a reduction from a large class of counter parity games to such games with imperfect recall. By combining the two results, we obtain the first elementary algorithm for solving counter parity games, which provides substantially improved complexity bounds for several problems in computational logic.} }

@phdthesis{dacosta-phd2011, author = {Da{~}Costa, Arnaud}, title = {Propri{\'e}t{\'e}s de jeux multi-agents}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2011, month = sep, url = {http://www.lsv.fr/Publis/PAPERS/PDF/dacosta-these11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/dacosta-these11.pdf} }

@mastersthesis{pasaila-master, author = {Pasail{\u{a}}, Daniel}, title = {Verifying equivalence properties of security protocols}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2011}, month = sep, url = {http://www.lsv.fr/Publis/PAPERS/PDF/dp11-m2.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/dp11-m2.pdf} }

@mastersthesis{degriek-master, author = {Degrieck, Jan}, title = {R{\'e}duction de graphes pour l'analyse de protocoles de routage s{\'e}curis{\'e}s}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2011}, month = sep, url = {http://www.lsv.fr/Publis/PAPERS/PDF/jd11-m2.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/jd11-m2.pdf} }

@inproceedings{CFM-ncma11, address = {Milano, Italy}, month = jul, year = 2011, volume = 282, series = {books@ocg.at}, publisher = {Austrian Computer Society}, editor = {Freund, Rudolf and Holzer, Markus and Mereghetti, Carlo and Otto, Friedrich and Palano, Beatrice}, acronym = {{NCMA}'11}, booktitle = {{P}roceedings of the 3rd {W}orkshop on {N}on-{C}lassical {M}odels of {A}utomata and {A}pplications ({NCMA}'11)}, author = {Cadilhac, Micha{\"e}l and Finkel, Alain and McKenzie, Pierre}, title = {On the Expressiveness of {P}arikh Automata and Related Models}, pages = {103-119}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-ncma11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-ncma11.pdf}, doi = {} }

@inproceedings{CFM-words11, address = {Prague, Czech Republic}, month = sep, year = 2011, volume = {63}, series = {Electronic Proceedings in Theoretical Computer Science}, editor = {Ambro{\v{z}}, Petr and Holub, {\v{S}}t{\v{e}}p{\'a}n and Mas{\'a}kov{\'a}, Zuzana}, acronym = {{WORDS}'11}, booktitle = {{P}roceedings of the 8th {I}nternational {C}onference {WORDS} ({WORDS}'11)}, author = {Cadilhac, Micha{\"e}l and Finkel, Alain and McKenzie, Pierre}, title = {Bounded {P}arikh Automata}, pages = {93-102}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-words11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-words11.pdf}, doi = {10.4204/EPTCS.63.13} }

@inproceedings{SR-dcfs11, address = {Limburg, Germany}, month = jul, year = 2011, volume = {6808}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Holzer, Markus and Kutrib, Martin and Pighizzini, Giovanni}, acronym = {{DCFS}'11}, booktitle = {{P}roceedings of the 13th {I}nternational {W}orkshop on {D}escriptional {C}omplexity of {F}ormal {S}ystems ({DCFS}'11)}, author = {Schwoon, Stefan and Rodr{\'\i}guez, C{\'e}sar}, title = {Construction and {SAT}-based verification of Contextual Unfoldings}, pages = {34-42}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/SR-dcfs11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SR-dcfs11.pdf}, doi = {10.1007/978-3-642-22600-7_3}, nonote = {Invited paper}, abstract = {Unfoldings succinctly represent the set of reachable markings of a Petri net. Here, we shall consider the case of contextual nets, which extend Petri nets with read arcs, and which are more suitable to represent the case of concurrent read access. We discuss the problem of (efficiently) constructing unfoldings of such nets. On the basis of these unfoldings, various verification problems can be encoded as satisfiability problems in propositional logic.} }

@inproceedings{HKS-gandalf11, address = {Minori, Italy}, month = jun, year = 2011, volume = 54, series = {Electronic Proceedings in Theoretical Computer Science}, editor = {D'Agostino, Giovanna and La{~}Torre, Salvatore}, acronym = {{GandALF}'11}, booktitle = {{P}roceedings of the 2nd {I}nternational {S}ymposium on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification ({GandALF}'11)}, author = {Haar, Stefan and Kern, Christian and Schwoon, Stefan}, title = {Computing the Reveals Relation in Occurrence Nets}, pages = {31-44}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/HKS-gandalf11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HKS-gandalf11.pdf}, doi = {10.4204/EPTCS.54.3}, abstract = {Petri net unfoldings are a useful tool to tackle state-space explosion in verification and related tasks. Moreover, their structure allows to access directly the relations of causal precedence, concurrency, and conflict between events. Here, we explore the data structure further, to determine the following relation: event~\(a\) is said to reveal event~\(b\) iff the occurrence of~\(a\) implies that~\(b\) inevitably occurs, too, be it before, after, or concurrently with~\(a\). Knowledge of reveals facilitates in particular the analysis of partially observable systems, in the context of diagnosis, testing, or verification; it can also be used to generate more concise representations of behaviours via abstractions. The reveals relation was previously introduced in the context of fault diagnosis, where it was shown that the reveals relation was decidable: for a given pair~\(a,b\) in the unfolding~\(U\) of a safe Petri net~\(N\), a finite prefix~\(P\) of~\(U\) is sufficient to decide whether or not \(a\) reveals~\(b\). In this paper, we first considerably improve the bound on~\(|P|\). We then show that there exists an efficient algorithm for computing the relation on a given prefix. We have implemented the algorithm and report on experiments.} }

@inproceedings{CDS-fct11, address = {Oslo, Norway}, month = aug, year = 2011, volume = 6914, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Owe, Olaf and Steffen, Martin and Telle, Jan Arne}, acronym = {{FCT}'11}, booktitle = {{P}roceedings of the 18th {I}nternational {S}ymposium on {F}undamentals of {C}omputation {T}heory ({FCT}'11)}, author = {Chatterjee, Krishnendu and Doyen, Laurent and Singh, Rohit}, title = {On Memoryless Quantitative Objectives}, pages = {148-159}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDS-fct11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDS-fct11.pdf}, doi = {10.1007/978-3-642-22953-4_13}, abstract = {In two-player games on graph, the players construct an infinite path through the game graph and get a reward computed by a payoff function over infinite paths. Over weighted graphs, the typical and most studied payoff functions compute the limit-average or the discounted sum of the rewards along the path. Besides their simple definition, these two payoff functions enjoy the property that memoryless optimal strategies always exist.\par In an attempt to construct other simple payoff functions, we define a class of payoff functions which compute an (infinite) weighted average of the rewards. This new class contains both the limit-average and the discounted sum functions, and we show that they are the only members of this class which induce memoryless optimal strategies, showing that there is essentially no other simple payoff functions.} }

@inproceedings{DDMM-fsttcs11, address = {Mumbai, India}, month = dec, year = 2011, volume = 13, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Chakraborty, Supratik and Kumar, Amit}, acronym = {{FSTTCS}'11}, booktitle = {{P}roceedings of the 31st {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'11)}, author = {Darondeau, {\relax Ph}ilippe and Demri, St{\'e}phane and Meyer, Roland and Morvan, {\relax Ch}ristophe}, title = {{P}etri Net Reachability Graphs: Decidability Status of {FO} Properties}, pages = {140-151}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DDMM-fsttcs11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDMM-fsttcs11.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2011.140}, abstract = {We investigate the decidability and complexity status of model-checking problems on unlabelled reachability graphs of Petri nets by considering first-order, modal and pattern-based languages without labels on transitions or atomic propositions on markings. We consider several parameters to separate decidable problems from undecidable ones. Not only are we able to provide precise borders and a systematic analysis, but we also demonstrate the robustness of our proof techniques.} }

@inproceedings{SBM-fsttcs11, address = {Mumbai, India}, month = dec, year = 2011, volume = 13, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Chakraborty, Supratik and Kumar, Amit}, acronym = {{FSTTCS}'11}, booktitle = {{P}roceedings of the 31st {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'11)}, author = {Sankur, Ocan and Bouyer, Patricia and Markey, Nicolas}, title = {Shrinking Timed Automata}, pages = {90-102}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/SBM-fsttcs11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SBM-fsttcs11.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2011.90}, abstract = {We define and study a new approach to the implementability of timed automata, where the semantics is perturbed by imprecisions and finite frequency of the hardware. In order to circumvent these effects, we introduce \emph{parametric shrinking} of clock constraints, which corresponds to tightening the guards. We propose symbolic procedures to decide the existence of (and then compute) parameters under which the shrunk version of a given timed automaton is non-blocking and can time-abstract simulate the exact semantics. We then define an implementation semantics for timed automata with a digital clock and positive reaction times, and show that for shrinkable timed automata both properties are preserved in implementation.} }

@inproceedings{CDK-fsttcs11, address = {Mumbai, India}, month = dec, year = 2011, volume = 13, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Chakraborty, Supratik and Kumar, Amit}, acronym = {{FSTTCS}'11}, booktitle = {{P}roceedings of the 31st {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'11)}, author = {Chevalier, C{\'e}line and Delaune, St{\'e}phanie and Kremer, Steve}, title = {Transforming Password Protocols to Compose}, pages = {204-216}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDK-fsttcs11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDK-fsttcs11.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2011.204}, abstract = {Formal, symbolic techniques are extremely useful for modelling and analysing security protocols. They improved our understanding of security protocols, allowed to discover flaws, and also provide support for protocol design. However, such analyses usually consider that the protocol is executed in isolation or assume a bounded number of protocol sessions. Hence, no security guarantee is provided when the protocol is executed in a more complex environment.\par In this paper, we study whether password protocols can be safely composed, even when a same password is reused. More precisely, we present a transformation which maps a password protocol that is secure for a single protocol session (a~decidable problem) to a protocol that is secure for an unbounded number of sessions. Our result provides an effective strategy to design secure password protocols: (i)~design a protocol intended to be secure for one protocol session; (ii)~apply our transformation and obtain a protocol which is secure for an unbounded number of sessions. Our technique also applies to compose different password protocols allowing us to obtain both inter-protocol and inter-session composition.} }

@inproceedings{BBMU-fsttcs11, address = {Mumbai, India}, month = dec, year = 2011, volume = 13, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Chakraborty, Supratik and Kumar, Amit}, acronym = {{FSTTCS}'11}, booktitle = {{P}roceedings of the 31st {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'11)}, author = {Bouyer, Patricia and Brenguier, Romain and Markey, Nicolas and Ummels, Michael}, title = {{N}ash Equilibria in Concurrent Games with {B}{\"u}chi Objectives}, pages = {375-386}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBMU-fsttcs11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBMU-fsttcs11.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2011.375}, abstract = {We study the problem of the existence (and computation) of Nash equilibria in multi-player concurrent games with B{\"u}chi-definable objectives. First, when the objectives are B{\"u}chi conditions on the game, we prove that the existence problem can be solved in polynomial time. In a second part, we extend our technique to objectives defined by deterministic B{\"u}chi automata, and prove that the problem then becomes EXPTIME-complete. We prove PSPACE-completeness for the case where the B{\"u}chi automata are 1-weak.} }

@inproceedings{BLP-fsttcs11, address = {Mumbai, India}, month = dec, year = 2011, volume = 13, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Chakraborty, Supratik and Kumar, Amit}, acronym = {{FSTTCS}'11}, booktitle = {{P}roceedings of the 31st {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'11)}, author = {Berwanger, Dietmar and Kaiser, {\L}ukasz and Puchala, Bernd}, title = {Perfect-Information Construction for Coordination in Games}, pages = {387-398}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BLP-fsttcs11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BLP-fsttcs11.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2011.387}, abstract = {We present a general construction for eliminating imperfect information from games with several players who coordinate against nature, and to transform them into two-player games with perfect information while preserving winning strategy profiles. The construction yields an infinite game tree with epistemic models associated to nodes. To obtain a more succinct representation, we define an abstraction based on homomorphic equivalence, which we prove to be sound for games with observable winning conditions. The abstraction generates finite game graphs in several relevant cases, and leads to a new semi-decision procedure for multi-player games with imperfect information.} }

@incollection{FLS-fosad11, noaddress = {}, month = sep, year = 2011, volume = 6858, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Aldini, Alessandro and Gorrieri, Roberto}, acronym = {{FOSAD}'{VI}}, booktitle = {{F}oundations of {S}ecurity {A}nalysis and {D}esign~-- {FOSAD} {T}utorial {L}ectures ({FOSAD}'{VI})}, author = {Focardi, Riccardo and Luccio, Flaminia L. and Steel, Graham}, title = {An Introduction to Security {API} Analysis}, pages = {35-65}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FLS-fosad11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FLS-fosad11.pdf}, doi = {10.1007/978-3-642-23082-0_2}, abstract = {A~security API is an Application Program Interface that allows untrusted code to access sensitive resources in a secure way. Examples of security APIs include the interface between the tamper-resistant chip on a smartcard (trusted) and the card reader (untrusted), the~interface between a~cryptographic Hardware Security Module, or~HSM (trusted) and the client machine (untrusted), and the Google maps API (an~interface between a server, trusted by Google, and the rest of the Internet).} }

@inproceedings{CCD-ccs11, address = {Chicago, Illinois, USA}, month = oct, year = 2011, publisher = {ACM Press}, editor = {Chen, Yan and Danezis, George and Shmatikov, Vitaly}, acronym = {{CCS}'11}, booktitle = {{P}roceedings of the 18th {ACM} {C}onference on {C}omputer and {C}ommunications {S}ecurity ({CCS}'11)}, author = {Cheval, Vincent and Comon{-}Lundh, Hubert and Delaune, St{\'e}phanie}, title = {Trace Equivalence Decision: Negative Tests and Non-determinism}, pages = {321-330}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-ccs11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-ccs11.pdf}, doi = {10.1145/2046707.2046744}, abstract = {We consider security properties of cryptographic protocols that can be modeled using the notion of trace equivalence. The notion of equivalence is crucial when specifying privacy-type properties, like anonymity, vote-privacy, and unlinkability.\par In this paper, we give a calculus that is close to the applied pi calculus and that allows one to capture most existing protocols that rely on classical cryptographic primitives. First, we propose a symbolic semantics for our calculus relying on constraint systems to represent infinite sets of possible traces, and we reduce the decidability of trace equivalence to deciding a notion of symbolic equivalence between sets of constraint systems. Second, we develop an algorithm allowing us to decide whether two sets of constraint systems are in symbolic equivalence or not. Altogether, this yields the first decidability result of trace equivalence for a general class of processes that may involve else branches and\slash or private channels (for a bounded number of sessions).} }

@incollection{haddad-DS11b, author = {Haddad, Serge}, title = {Introduction to Verification}, booktitle = {Models and Analysis in Distributed Systems}, editor = {Haddad, Serge and Kordon, Fabrice and Pautet, Laurent and Petrucci, Laure}, publisher = {John Wiley \& Sons, Ltd.}, chapter = 6, pages = {137-154}, year = 2011 }

@incollection{DP-DS11b, author = {Demri, St{\'e}phane and Poitrenaud, Denis}, title = {Verification of Infinite-State Systems}, booktitle = {Models and Analysis in Distributed Systems}, editor = {Haddad, Serge and Kordon, Fabrice and Pautet, Laurent and Petrucci, Laure}, publisher = {John Wiley \& Sons, Ltd.}, chapter = 8, pages = {221-269}, year = 2011, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DP-DS11b.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DP-DS11b.pdf} }

@book{HKPP-DS11a, editor = {Haddad, Serge and Kordon, Fabrice and Pautet, Laurent and Petrucci, Laure}, title = {Distributed Systems Design and Algorithms}, publisher = {John Wiley \& Sons, Ltd.}, year = {2011}, url = {http://www.iste.co.uk/index.php?f=a&ACTION=View&id=415} }

@book{HKPP-DS11b, editor = {Haddad, Serge and Kordon, Fabrice and Pautet, Laurent and Petrucci, Laure}, title = {Models and Analysis in Distributed Systems}, publisher = {John Wiley \& Sons, Ltd.}, year = {2011}, url = {http://www.iste.co.uk/index.php?f=a&ACTION=View&id=416} }

@inproceedings{ECGJ-msr11, address = {Lille, France}, month = nov, year = 2011, number = {1-3}, volume = {45}, series = {Journal Europ{\'e}en des Syst{\`e}mes Automatis{\'e}s}, publisher = {Herm{\`e}s}, editor = {Craye, {\'E}tienne and Gamati{\'e}, Abdoulaye}, acronym = {{MSR}'11}, booktitle = {{A}ctes du 8{\`e}me {C}olloque sur la {M}od{\'e}lisation des {S}yst{\`e}mes {R}{\'e}actifs ({MSR}'11)}, author = {Echeveste, Jod{\'e} and Cont, Arshia and Giavitto, Jean-Louis and Jacquemard, Florent}, title = {Formalisation des relations temporelles entre une partition et une performance musicale dans un contexte d'accompagnement automatique}, pages = {109-124}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ECGJ-msr11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ECGJ-msr11.pdf}, doi = {10.3166/jesa.45.109-124}, abstract = {We sketch the real-time features required by automatic musical accompaniment seen as a reactive system. We formalize the datation of musical event taking into account the various temporal scales used in music. Various strategies for the handling of synchronization constraints and the handling of errors are presented.} }

@inproceedings{BHP-msr11, address = {Lille, France}, month = nov, year = 2011, number = {1-3}, volume = {45}, series = {Journal Europ{\'e}en des Syst{\`e}mes Automatis{\'e}s}, publisher = {Herm{\`e}s}, editor = {Craye, {\'E}tienne and Gamati{\'e}, Abdoulaye}, acronym = {{MSR}'11}, booktitle = {{A}ctes du 8{\`e}me {C}olloque sur la {M}od{\'e}lisation des {S}yst{\`e}mes {R}{\'e}actifs ({MSR}'11)}, author = {Barbot, Beno{\^\i}t and Haddad, Serge and Picaronny, Claudine}, title = {{\'E}chantillonnage pr{\'e}f{\'e}rentiel pour le model checking statistique}, pages = {237-252}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-msr11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-msr11.pdf}, doi = {10.3166/jesa.45.237-252}, abstract = {The statistical model checking can be usefully substituted for numerical model checking when the models to be studied are huge. However the statistical approach cannot evaluate too small probabilities. In order to solve the problem, we develop here a new approach based on importance sampling. While most of the techniques related to importance sampling are based on heuristics, we establish theoretical results under some hypotheses. These results ensure a reduction of the variance during application of importance sampling. We also characterize situations that fulfill the hypotheses and we extend our approach for handling other situations but then without theoretical guarantee. We have implemented this approach with the tool \textsc{Cosmos} after some extensions. At~last we have evaluated this approach for two examples and analysed the experimentations.} }

@inproceedings{BMS-formats11, address = {Aalborg, Denmark}, month = sep, year = 2011, volume = 6919, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Fahrenberg, Uli and Tripakis, Stavros}, acronym = {{FORMATS}'11}, booktitle = {{P}roceedings of the 9th {I}nternational {C}onference on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'11)}, author = {Bouyer, Patricia and Markey, Nicolas and Sankur, Ocan}, title = {Robust Model-Checking of Timed Automata via Pumping in Channel Machines}, pages = {97-112}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-formats11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-formats11.pdf}, doi = {10.1007/978-3-642-24310-3_8}, abstract = {Timed automata are governed by a mathematical semantics which assumes perfectly continuous and precise clocks. This requirement is not satised by digital hardware on which the models are implemented. In~fact, it~was shown that the presence of imprecisions, however small they may be, may yield extra behaviours. Therefore correctness proven on the formal model does not imply correctness of the real system.\par The problem of robust model-checking was then dened to circumvent this inconsistency. It consists in computing a bound on the imprecision under which the system will be correct.\par In this work, we show that robust model-checking against \(\omega\)-regular properties for timed automata can be reduced to standard model-checking of timed automata, by computing an adequate bound on the imprecision. This yields a new algorithm for robust model-checking of \(\omega\)-regular properties, which is both optimal and valid for general timed automata.} }

@inproceedings{bonnet-RP11, address = {Genova, Italy}, month = sep, year = 2011, volume = {6945}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Delzanno, Giorgio and Potapov, Igor}, acronym = {{RP}'11}, booktitle = {{P}roceedings of the 5th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'11)}, author = {Bonnet, R{\'e}mi}, title = {Decidability of {LTL} Model Checking for Vector Addition Systems with one Zero-test}, pages = {85-95}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/bonnet-RP11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bonnet-RP11.pdf}, doi = {10.1007/978-3-642-24288-5_9}, abstract = {We consider the class of Vector Addition Systems with one zero-test and we show that the model-checking problem for LTL is decidable thanks to a reduction to the computability of the cover and the decidability of reachability. Our proof uses the notion of increasing loop, that we refine to fit the non-standard monotony of our system.} }

@inproceedings{FK-RP11, address = {Genova, Italy}, month = sep, year = 2011, volume = {6945}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Delzanno, Giorgio and Potapov, Igor}, acronym = {{RP}'11}, booktitle = {{P}roceedings of the 5th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'11)}, author = {Fribourg, Laurent and K{\"u}hne, Ulrich}, title = {Parametric Verification and Test Coverage for Hybrid Automata Using the Inverse Method}, pages = {191-204}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FK-RP11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FK-RP11.pdf}, doi = {10.1007/978-3-642-24288-5_17}, abstract = {Hybrid systems combine continuous and discrete behavior. Hybrid Automata are a powerful formalism for the modeling and verification of such systems. A~common problem in hybrid system verification is the good parameters problem, which consists in identifying a set of parameter valuations which guarantee a certain behavior of a system. Recently, a method has been presented for attacking this problem for Timed Automata. In this paper, we show the extension of this methodology for hybrid automata with linear and affine dynamics. The method is demonstrated with a hybrid system benchmark from the literature.} }

@inproceedings{AS-RP11, address = {Genova, Italy}, month = sep, year = 2011, volume = {6945}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Delzanno, Giorgio and Potapov, Igor}, acronym = {{RP}'11}, booktitle = {{P}roceedings of the 5th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'11)}, author = {Andr{\'e}, {\'E}tienne and Soulat, Romain}, title = {Synthesis of Timing Parameters Satisfying Safety Properties}, pages = {31-44}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AS-RP11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AS-RP11.pdf}, doi = {10.1007/978-3-642-24288-5_5}, abstract = {Safety properties are crucial when verifying real-time concurrent systems. When reasoning parametrically, i.e., with unknown constants, it is of high interest to infer a set of parameter valuations consistent with such safety properties. We present here algorithms based on the inverse method for parametric timed automata: given a reference parameter valuation, it infers a constraint such that, for any valuation satisfying this constraint, the discrete behavior of the system is the same as under the reference valuation in terms of traces, i.e., alternating sequences of locations and actions. These algorithms do not guarantee the equality of the trace sets, but are significantly quicker, synthesize larger sets of parameter valuations than the original method, and still preserve various properties including safety (i.e., non-reachability) properties. Those algorithms have been implemented in Imitator~II and applied to various examples of asynchronous circuits and communication protocols. } }

@techreport{lsv-11-18, author = {Florentin, {\'E}ric and Fribourg, Laurent and K{\"u}hne, Ulrich and Lefebvre, St{\'e}phane and Rey, {\relax Ch}ristian}, title = {{COUPLET}: Coupled Electrothermal Simulation}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2011}, month = jun, type = {Research Report}, number = {LSV-11-18}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2011-18.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2011-18.pdf}, note = {32~pages}, abstract = {The~aim of the project COUPLET (supported by Institut Farman) is to study the electrothermal effects of the degradation of the metallisation layer of power semiconductor dies. In this first technical report of the project, we describe our work of modeling and simulation of the behavior of a power transistor. The die is represented by four elementary transistors driven by a distributed gate signal. A~simplified electrical model is used to simulate the transistor behavior at turn-off. The thermal model is realized by finite elements methods and allows to estimate the maximum temperature on each elementary transistor. By~coupling the thermal model with the electric simulation, it is possible to take into account silicon and metallisation heating in the electrical model.} }

@inproceedings{SC-unif11, address = {Wroc{\l}aw, Poland}, month = jul, year = 2011, editor = {Baader, Franz}, acronym = {{UNIF}'11}, booktitle = {{P}roceedings of the 25th {I}nternational {W}orkshop on {U}nification ({UNIF}'11)}, author = {Ciob{\^a}c{\u{a}}, {\c{S}}tefan}, title = {Computing finite variants for subterm convergent rewrite systems}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/SC-unif11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SC-unif11.pdf}, abstract = {Driven by an application in the verification of security protocols, we introduce the strong finite variant property, an extention of the finite variant property, and we show that subterm convergent rewrite systems enjoy the strong finite variant property modulo the empty equational theory.\par We argue that the strong finite variant property is more natural and more useful in practice than the finite variant property. We also compare the two properties and we provide a prototype implementation of an algorithm that computes a finite strongly complete set of variants for any term t with respect to a subterm convergent rewrite system.} }

@inproceedings{BMOU-atva11, address = {Taipei, Taiwan}, month = oct, year = {2011}, volume = 6996, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Bultan, Tevfik and Hsiung, Pao-Ann}, acronym = {{ATVA}'11}, booktitle = {{P}roceedings of the 9th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'11)}, author = {Bouyer, Patricia and Markey, Nicolas and Olschewski, J{\"o}rg and Ummels, Michael}, title = {Measuring Permissiveness in Parity Games: Mean-Payoff Parity Games Revisited}, pages = {135-149}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMOU-atva11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMOU-atva11.pdf}, doi = {10.1007/978-3-642-24372-1_11}, abstract = {We study nondeterministic strategies in parity games with the aim of computing a most permissive winning strategy. Following earlier work, we measure permissiveness in terms of the average number{\slash}weight of transitions blocked by a strategy. Using a translation into mean-payoff parity games, we prove that deciding (the permissiveness~of) a~most permissive winning strategy is in \(\textsf{NP}\cap\textsf{coNP}\). Along the way, we~provide a new study of mean-payoff parity games. In particular, we give a new algorithm for solving these games, which beats all previously known algorithms for this problem.} }

@inproceedings{CKVAK-qest11, address = {Aachen, Germany}, month = sep, year = 2011, publisher = {{IEEE} Computer Society Press}, acronym = {{QEST}'11}, booktitle = {{P}roceedings of the 8th {I}nternational {C}onference on {Q}uantitative {E}valuation of {S}ystems ({QEST}'11)}, author = {Chadha, Rohit and Korthikranthi, Vijay and Viswanathan, Mahesh and Agha, Gul and Kwon, Youngmin}, title = {Model Checking {MDP}s with a Unique Compact Invariant Set of Distributions}, pages = {121-130}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CKVAK-qest11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CKVAK-qest11.pdf}, doi = {10.1109/QEST.2011.22}, abstract = {The semantics of Markov Decision Processes (MDPs), when viewed as transformers of probability distributions, can described as a labeled transition system over the probability distributions over the states of the MDP. The MDP can be seen as defining a set of executions, where each execution is a sequence of probability distributions. Reasoning about sequences of distributions allows one to express properties not expressible in logics like PCTL; examples include expressing bounds on transient rewards and expected values of random variables, as well as comparing the probability of being in one set of states at a given time with another set of states. With respect to such a semantics, the problem of checking that the MDP never reaches a bad distribution is undecidable. In this paper, we identify a special class of MDPs called \emph{semi-regular} MDPs that have a unique non-empty, compact, invariant set of distributions, for which we show that checking any \(\omega\)-regular property is decidable. Our decidability result also implies that for semi-regular probabilistic finite automata with isolated cut-points, the emptiness problem is decidable.} }

@inproceedings{CD-mfcs11, address = {Warsaw, Poland}, month = aug, year = 2011, volume = 6907, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Murlak, Filip and Sankowski, Piotr}, acronym = {{MFCS}'11}, booktitle = {{P}roceedings of the 36th {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'11)}, author = {Chatterjee, Krishnendu and Doyen, Laurent}, title = {Energy and Mean-Payoff Parity {M}arkov Decision Processes}, pages = {206-218}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-mfcs11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-mfcs11.pdf}, doi = {10.1007/978-3-642-22993-0_21}, abstract = {We consider Markov Decision Processes (MDPs) with mean-payoff parity and energy parity objectives. In system design, the parity objective is used to encode \(\omega\)-regular specifications, while the mean-payoff and energy objectives can be used to model quantitative resource constraints. The energy condition requires that the resource level never drops below~\(0\), and the mean-payoff condition requires that the limit-average value of the resource consumption is within a threshold. While these two (energy and mean-payoff) classical conditions are equivalent for two-player games, we~show that they differ for MDPs. We show that the problem of deciding whether a state is almost-sure winning (i.e., winning with probability~\(1\)) in energy parity MDPs is in \(\textsf{NP}\cap\textsf{coNP}\), while for mean-payoff parity MDPs, the problem is solvable in polynomial time.} }

@inproceedings{DMS-mfcs11, address = {Warsaw, Poland}, month = aug, year = 2011, volume = 6907, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Murlak, Filip and Sankowski, Piotr}, acronym = {{MFCS}'11}, booktitle = {{P}roceedings of the 36th {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'11)}, author = {Doyen, Laurent and Massart, {\relax Th}ierry and Shirmohammadi, Mahsa}, title = {Infinite Synchronizing Words for Probabilistic Automata}, pages = {278-289}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DMS-mfcs11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DMS-mfcs11.pdf}, doi = {10.1007/978-3-642-22993-0_27}, abstract = {Probabilistic automata are finite-state automata where the transitions are chosen according to fixed probability distributions. We consider a semantics where on an input word the automaton produces a sequence of probability distributions over states. An~infinite word is accepted if the produced sequence is synchronizing, i.e. the sequence of the highest probability in the distributions tends to~\(1\). We show that this semantics generalizes the classical notion of synchronizing words for deterministic automata. We consider the emptiness problem, which asks whether some word is accepted by a given probabilistic automaton, and the universality problem, which asks whether all words are accepted. We provide reductions to establish the PSPACE-completeness of the two problems.} }

@inproceedings{BCGZ-mfcs11, address = {Warsaw, Poland}, month = aug, year = 2011, volume = 6907, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Murlak, Filip and Sankowski, Piotr}, acronym = {{MFCS}'11}, booktitle = {{P}roceedings of the 36th {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'11)}, author = {Bollig, Benedikt and Cyriac, Aiswarya and Gastin, Paul and Zeitoun, Marc}, title = {Temporal Logics for Concurrent Recursive Programs: Satisfiability and Model Checking}, pages = {132-144}, url = {http://hal.archives-ouvertes.fr/hal-00591139/en/}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGZ-mfcs11.pdf}, doi = {10.1007/978-3-642-22993-0_15}, abstract = {We develop a general framework for the design of temporal logics for concurrent recursive programs. A program execution is modeled as a partial order with multiple nesting relations. To specify properties of executions, we consider any temporal logic whose modalities are definable in monadic second-order logic and that, in addition, allows PDL-like path expressions. This captures, in a unifying framework, a wide range of logics defined for trees, nested words, and Mazurkiewicz traces that have been studied separately. We show that satisfiability and model checking are decidable in EXPTIME and 2EXPTIME, depending on the precise path modalities.} }

@inproceedings{Schmitz-fsmnlp11, address = {Blois, France}, month = jul, year = 2011, publisher = {ACL Press}, editor = {Maletti, Andreas}, acronym = {{FSMNLP}'11}, booktitle = {{P}roceedings of the 9th {I}nternational {W}orkshop on {F}inite-{S}tate {M}ethods and {N}atural {L}anguage {P}rocessing ({FSMNLP}'11)}, author = {Sylvain Schmitz}, title = {A~Note on Sequential Rule-Based {POS} Tagging}, pages = {83-87}, url = {http://hal.archives-ouvertes.fr/hal-00600260/}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Schmitz-fsmnlp11.pdf}, abstract = {Brill's part-of-speech tagger is defined through a cascade of leftmost rewrite rules. We revisit the compilation of such rules into a single sequential transducer given by Roche and Schabes (\textit{Comput. Ling.}~1995) and provide a direct construction of the minimal sequential transducer for each individual rule.} }

@inproceedings{BS-mfcs11, address = {Warsaw, Poland}, month = aug, year = 2011, volume = 6907, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Murlak, Filip and Sankowski, Piotr}, acronym = {{MFCS}'11}, booktitle = {{P}roceedings of the 36th {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'11)}, author = {Blockelet, Michel and Schmitz, Sylvain}, title = {Model-Checking Coverability Graphs of Vector Addition Systems}, pages = {108-119}, url = {http://hal.archives-ouvertes.fr/hal-00600077/}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-mfcs11.pdf}, doi = {10.1007/978-3-642-22993-0_13}, abstract = {A large number of properties of a vector addition system---for instance coverability, boundedness, or regularity---can be decided using its coverability graph, by looking for some characteristic pattern. We propose to unify the known exponential-space upper bounds on the complexity of such problems on vector addition systems, by seeing them as instances of the model-checking problem for a suitable extension of computation tree logic, which allows to check for the existence of these patterns. This provides new insights into what constitutes a {"}coverability-like{"} property.} }

@inproceedings{Sankur-mfcs11, address = {Warsaw, Poland}, month = aug, year = 2011, volume = 6907, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Murlak, Filip and Sankowski, Piotr}, acronym = {{MFCS}'11}, booktitle = {{P}roceedings of the 36th {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'11)}, author = {Sankur, Ocan}, title = {Untimed Language Preservation in Timed Systems}, pages = {556-567}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/OS-mfcs11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/OS-mfcs11.pdf}, corrigendumpdf = {http://www.lsv.fr/Publis/PAPERS/PDF/OS-mfcs11-erratum.pdf}, doi = {10.1007/978-3-642-22993-0_50}, abstract = {Timed automata are a model that is extensively used in formal verification of real-time systems. However, their mathematical semantics is an idealization which assumes perfectly precise clocks, but does not correspond to real hardware. In fact, it is known that imprecisions, however small they may be, may yield extra behaviours. Several works concentrated on a relaxation of the semantics of timed automata to model the imprecisions of the clocks. Algorithms were given, first for safety, then for richer linear-time properties, to decide the robustness of timed systems, that is, the existence of a bound on the imprecisions under which the system satisfies a given property. In this work, we study a stronger notion of robustness: we show how to decide whether the untimed language of a timed automaton is preserved under small enough imprecisions, and provide a bound on the imprecision parameter.} }

@inproceedings{Bonnet-mfcs11, address = {Warsaw, Poland}, month = aug, year = 2011, volume = 6907, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Murlak, Filip and Sankowski, Piotr}, acronym = {{MFCS}'11}, booktitle = {{P}roceedings of the 36th {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'11)}, author = {Bonnet, R{\'e}mi}, title = {The reachability problem for Vector Addition Systems with one zero-test}, pages = {145-157}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/RB-mfcs11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RB-mfcs11.pdf}, doi = {10.1007/978-3-642-22993-0_16}, abstract = {We consider here a variation of Vector Addition Systems where one counter can be tested for zero. We extend the reachability proof for Vector Addition System recently published by Leroux to this model. This provides an alternate, more conceptual proof of the reachability problem that was originally proved by Reinhardt.} }

@inproceedings{NM-sies11, address = {V{\"a}ster{\aa}s, Sweden}, month = jun, year = 2011, publisher = {{IEEE} Computer Society Press}, noeditor = {}, acronym = {{SIES}'11}, booktitle = {{P}roceedings of the 6th {IEEE} {I}nternational {S}ymposium on {I}ndustrial {E}mbedded {S}ystems ({SIES}'11)}, author = {Markey, Nicolas}, title = {Robustness in Real-time Systems}, pages = {28-34}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/NM-sies11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/NM-sies11.pdf}, doi = {10.1109/SIES.2011.5953652}, abstract = {We~review several aspects of robustness of real-time systems, and present recent results on the robust verification of timed automata.} }

@inproceedings{BDDHP-case11, address = {Trieste, Italy}, month = aug, year = 2011, publisher = {{IEEE} Robotics \& Automation Society}, noeditor = {}, acronym = {{CASE}'11}, booktitle = {{P}roceedings of the 7th {IEEE} {C}onference on {A}utomation {S}cience and {E}ngineering ({CASE}'11)}, author = {Ballarini, Paolo and Djafri, Hilal and Duflot, Marie and Haddad, Serge and Pekergin, Nihal}, title = {{P}etri Nets Compositional Modeling and Verification of Flexible Manufacturing Systems}, pages = {588-593}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDDHP-case11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDDHP-case11.pdf}, doi = {10.1109/CASE.2011.6042488}, abstract = {Flexible Manufacturing Systems (FMS) are amongst the most studied types of systems, however due to their increasing complexity, there is still room for improvement in their modeling and analysis. In this paper we consider the design and the analysis of stochastic models of FMS in two complementary respects. First we describe a (stochastic) Petri Nets based compositional framework which enables to model an FMS by combination of an arbitrary number of basic components. Second we demonstrate how classical transient-analysis of manufacturing systems, including reliability and performability analysis, can be enriched by application of a novel, sophisticated stochastic logic, namely the Hybrid Automata Stochastic Logic (HASL). We demonstrate the proposed methodology on an FMS example.} }

@inproceedings{BDDHP-qest11, address = {Aachen, Germany}, month = sep, year = 2011, publisher = {{IEEE} Computer Society Press}, acronym = {{QEST}'11}, booktitle = {{P}roceedings of the 8th {I}nternational {C}onference on {Q}uantitative {E}valuation of {S}ystems ({QEST}'11)}, author = {Ballarini, Paolo and Djafri, Hilal and Duflot, Marie and Haddad, Serge and Pekergin, Nihal}, title = {{COSMOS}: a~Statistical Model Checker for the Hybrid Automata Stochastic Logic}, pages = {143-144}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDDHP-qest11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDDHP-qest11.pdf}, doi = {10.1109/QEST.2011.24}, abstract = {This tool paper introduces COSMOS, a statistical model checker for the Hybrid Automata Stochastic Logic (HASL). HASL employs Linear Hybrid Automata (LHA), a generalization of Deterministic Timed Automata (DTA), to describe accepting execution paths of a Discrete Event Stochastic Process (DESP), a class of stochastic models which includes, but is not limited to, Markov chains. As a result HASL verification turns out to be a unifying framework where sophisticated temporal reasoning is naturally blended with elaborate reward-based analysis. COSMOS takes as input a DESP (described in terms of a Generalized Stochastic Petri Net), an LHA and an expression~\(Z\) representing the quantity to be estimated. It returns a confidence interval estimation of~\(Z\). COSMOS is written in C++ and is freely available to the research community.} }

@article{BFH-ijpe11, publisher = {RAMS Consultants}, journal = {International Journal of Performability Engineering}, author = {Beccuti, Marco and Franceschinis, Giuliana and Haddad, Serge}, title = {{MDWN}solver: A~Framework to Design and Solve {M}arkov Decision {P}etri Nets}, year = {2011}, month = sep, volume = 7, number = 5, pages = {417-428}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFH-ijpe11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFH-ijpe11.pdf}, abstract = {MDWNsolver is a framework for system modeling and optimization of performability measures based on Markov Decision Petri Net (MDPN) and Markov Decision Well-formed Net (MDWN) formalisms, two Petri Net extensions for high level specification of Markov Decision Processes (MDP). It is integrated in the GreatSPN suite which provides a GUI to design MDPN/MDWN models. From the analysis point of view, MDWNsolver uses efficient algorithms that take advantage of system symmetries, thus reducing the analysis complexity. In this paper the MDWNsolver framework features and architecture are presented, and some application examples are discussed.} }

@inproceedings{UW-concur11, address = {Aachen, Germany}, month = sep, year = 2011, volume = 6901, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Katoen, Joost-Pieter and K{\"o}nig, Barbara}, acronym = {{CONCUR}'11}, booktitle = {{P}roceedings of the 22nd {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'11)}, author = {Ummels, Michael and Wojtczak, Dominik}, title = {The Complexity of {N}ash Equilibria in Limit-Average Games}, pages = {482-496}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/UW-concur11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/UW-concur11.pdf}, doi = {10.1007/978-3-642-23217-6_32}, abstract = {We study the computational complexity of Nash equilibria in concurrent games with limit-average objectives. In particular, we prove that the existence of a Nash equilibrium in randomised strategies is undecidable, while the existence of a Nash equilibrium in pure strategies is decidable, even if we put a constraint on the payoff of the equilibrium. Our undecidability result holds even for a restricted class of concurrent games, where nonzero rewards occur only on terminal states. Moreover, we show that the constrained existence problem is undecidable not only for concurrent games but for turn-based games with the same restriction on rewards. Finally, we prove that the constrained existence problem for Nash equilibria in (pure or randomised) stationary strategies is decidable and analyse its complexity.} }

@inproceedings{Bol-concur11, address = {Aachen, Germany}, month = sep, year = 2011, volume = 6901, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Katoen, Joost-Pieter and K{\"o}nig, Barbara}, acronym = {{CONCUR}'11}, booktitle = {{P}roceedings of the 22nd {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'11)}, author = {Bollig, Benedikt}, title = {An automaton over data words that captures {EMSO} logic}, pages = {171-186}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/B-concur11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/B-concur11.pdf}, doi = {10.1007/978-3-642-23217-6_12}, abstract = {We develop a general framework for the specification and implementation of systems whose executions are words, or partial orders, over an infinite alphabet. As a model of an implementation, we introduce class register automata, a one-way automata model over words with multiple data values. Our model combines register automata and class memory automata. It has natural interpretations. In particular, it captures communicating automata with an unbounded number of processes, whose semantics can be described as a set of (dynamic) message sequence charts. On the specification side, we provide a local existential monadic second-order logic that does not impose any restriction on the number of variables. We study the realizability problem and show that every formula from that logic can be effectively, and in elementary time, translated into an equivalent class register automaton.} }

@inproceedings{RSB-concur11, address = {Aachen, Germany}, month = sep, year = 2011, volume = 6901, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Katoen, Joost-Pieter and K{\"o}nig, Barbara}, acronym = {{CONCUR}'11}, booktitle = {{P}roceedings of the 22nd {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'11)}, author = {Rodr{\'\i}guez, C{\'e}sar and Schwoon, Stefan and Baldan, Paolo}, title = {Efficient contextual unfolding}, pages = {342-357}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/RSB-concur11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RSB-concur11.pdf}, doi = {10.1007/978-3-642-23217-6_23}, abstract = {A~contextual net is a Petri net extended with read arcs, which allow transitions to check for tokens without consuming them. Contextual nets allow for better modelling of concurrent read access than Petri nets, and their unfoldings can be exponentially more compact than those of a corresponding Petri net. A~constructive but abstract procedure for generating those unfoldings was proposed in earlier work; however, no concrete implementation existed. Here, we~close this gap providing two concrete methods for computing contextual unfoldings, with a view to efficiency. We report on experiments carried out on a number of benchmarks. These show that not only are contextual unfoldings more compact than Petri net unfoldings, but they can be computed with the same or better efficiency, in~particular with respect to the place-replication encoding of contextual nets into Petri nets.} }

@inproceedings{BLMST-concur11, address = {Aachen, Germany}, month = sep, year = 2011, volume = 6901, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Katoen, Joost-Pieter and K{\"o}nig, Barbara}, acronym = {{CONCUR}'11}, booktitle = {{P}roceedings of the 22nd {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'11)}, author = {Bouyer, Patricia and Larsen, Kim~G. and Markey, Nicolas and Sankur, Ocan and Thrane, Claus}, title = {Timed automata can always be made implementable}, pages = {76-91}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BLMST-concur11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BLMST-concur11.pdf}, doi = {10.1007/978-3-642-23217-6_6}, abstract = {Timed automata follow a mathematical semantics, which assumes perfect precision and synchrony of clocks. Since this hypothesis does not hold in digital systems, properties proven formally on a timed automaton may be lost at implementation. In order to ensure implementability, several approaches have been considered, corresponding to different hypotheses on the implementation platform. We address two of these: a~timed automaton is samplable if its semantics is preserved under a discretization of time; it is robust if its semantics is preserved when all timing constraints are relaxed by some small positive parameter. We propose a construction which makes timed automata implementable in the above sense: From any timed automaton~\(\mathcal{A}\), we build a timed automaton~\(\mathcal{A}'\) that exhibits the same behaviour as~\(\mathcal{A}\), and moreover is both robust and samplable by construction.} }

@inproceedings{BBBS-icalp11, address = {Z{\"u}rich, Switzerland}, month = jul, year = 2011, volume = 6756, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Aceto, Luca and Henzinger, Monika and Sgall, Jir{\'\i}}, acronym = {{ICALP}'11}, booktitle = {{P}roceedings of the 38th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'11)~-- {P}art~{II}}, author = {Bertrand, Nathalie and Bouyer, Patricia and Brihaye, {\relax Th}omas and Stainer, Am{\'e}lie}, title = {Emptiness and Universality Problems in Timed Automata with Positive Frequency}, pages = {246-257}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBBS-icalp11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBBS-icalp11.pdf}, doi = {10.1007/978-3-642-22012-8_19}, abstract = {The languages of infinite timed words accepted by timed automata are traditionally dened using B{\"u}chi-like conditions. These acceptance conditions focus on the set of locations visited infinitely often along a run, but completely ignore quantitative timing aspects. In this paper we propose a natural quantitative semantics for timed automata based on the so-called frequency, which measures the proportion of time spent in the accepting locations. We study various properties of timed languages accepted with positive frequency, and in particular the emptiness and universality problems.} }

@inproceedings{BDGORW-icalp11, address = {Z{\"u}rich, Switzerland}, month = jul, year = 2011, volume = 6756, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Aceto, Luca and Henzinger, Monika and Sgall, Jir{\'\i}}, acronym = {{ICALP}'11}, booktitle = {{P}roceedings of the 38th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'11)~-- {P}art~{II}}, author = {Brihaye, {\relax Th}omas and Doyen, Laurent and Geeraerts, Gilles and Ouaknine, Jo{\"e}l and Raskin, Jean-Fran{\c{c}}ois and Worrell, James}, title = {On~Reachability for Hybrid Automata over Bounded Time}, pages = {416-427}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDGORW-icalp11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDGORW-icalp11.pdf}, doi = {10.1007/978-3-642-22012-8_33}, abstract = {This paper investigates the time-bounded version of the reachability problem for hybrid automata. This problem asks whether a given hybrid automaton can reach a given target location within~\(\mathbf{T}\) time units, where \(\mathbf{T}\) is a constant rational value. We show that, in contrast to the classical (unbounded) reachability problem, the timed-bounded version is decidable for rectangular hybrid automata provided only non-negative rates are allowed. This class of systems is of practical interest and subsumes, among others, the class of stopwatch automata. We also show that the problem becomes undecidable if either diagonal constraints or both negative and positive rates are allowed.} }

@inproceedings{BCS-icalp11, address = {Z{\"u}rich, Switzerland}, month = jul, year = 2011, volume = 6756, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Aceto, Luca and Henzinger, Monika and Sgall, Jir{\'\i}}, acronym = {{ICALP}'11}, booktitle = {{P}roceedings of the 38th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'11)~-- {P}art~{II}}, author = {B{\'a}r{\'a}ny, Vince and ten~Cate, Balder and Segoufin, Luc}, title = {Guarded negation}, pages = {356-367}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCS-icalp11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCS-icalp11.pdf}, doi = {10.1007/978-3-642-22012-8_28}, abstract = {We consider restrictions of first-order logic and of fixpoint logic in which all occurrences of negation are required to be guarded by an atomic predicate. In terms of expressive power, the logics in question, called GNFO and GNFP, extend the guarded fragment of first-order logic and guarded least fixpoint logic, respectively. They also extend the recently introduced unary negation fragments of first-order logic and of least fixpoint logic.\par We show that the satisfiability problem for GNFO and for GNFP is 2ExpTime-complete, both on arbitrary structures and on finite structures. We also study the complexity of the associated model checking problems. Finally, we show that GNFO and GNFP are not only computationally well behaved, but also model theoretically: we show that GNFO and GNFP have the tree-like model property and that GNFO has the finite model property, and we characterize the expressive power of GNFO in terms of invariance for an appropriate notion of bisimulation.} }

@inproceedings{SS-icalp11, address = {Z{\"u}rich, Switzerland}, month = jul, year = 2011, volume = 6756, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Aceto, Luca and Henzinger, Monika and Sgall, Jir{\'\i}}, acronym = {{ICALP}'11}, booktitle = {{P}roceedings of the 38th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'11)~-- {P}art~{II}}, author = {Schmitz, Sylvain and Schnoebelen, {\relax Ph}ilippe}, title = {Multiply-Recursive Upper Bounds with {H}igman's Lemma}, pages = {441-452}, url = {http://arxiv.org/abs/1103.4399}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SS-icalp11.pdf}, doi = {10.1007/978-3-642-22012-8_35}, abstract = {We develop a new analysis for the length of controlled bad sequences in well-quasi-orderings based on Higman's Lemma. This leads to tight multiply-recursive upper bounds that readily apply to several verification algorithms for well-structured systems.} }

@inproceedings{AMSS-icalp11, address = {Z{\"u}rich, Switzerland}, month = jul, year = 2011, volume = 6756, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Aceto, Luca and Henzinger, Monika and Sgall, Jir{\'\i}}, acronym = {{ICALP}'11}, booktitle = {{P}roceedings of the 38th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'11)~-- {P}art~{II}}, author = {Anderson, Matthew and van~Melkebeek, Dieter and Schweikardt, Nicole and Segoufin, Luc}, title = {Locality of queries definable in invariant first-order logic with arbitrary built-in predicates}, pages = {368-379}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AMSS-icalp11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AMSS-icalp11.pdf}, doi = {10.1007/978-3-642-22012-8_29}, abstract = {We consider first-order formulas over relational structures which may use arbitrary numerical predicates. We require that the validity of the formula is independent of the particular interpretation of the numerical predicates and refer to such formulas as Arb-invariant first-order.\par Our main result shows a Gaifman locality theorem: two tuples of a structure with n elements, having the same neighborhood up to distance \((\log n)^{\omega(1)}\), cannot be distinguished by Arb-invariant first-order formulas. When restricting attention to word structures, we can achieve the same quantitative strength for Hanf locality. In both cases we show that our bounds are tight.\par Our proof exploits the close connection between Arb-invariant first-order formulas and the complexity class \(\textsf{AC}^{0}\), and hinges on the tight lower bounds for parity on constant-depth circuits.} }

@techreport{rr-lsv-11-08, author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin and Zeitoun, Marc}, title = {Weighted Expressions and {DFS} Tree Automata}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2011}, month = apr, type = {Research Report}, number = {LSV-11-08}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2011-08.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2011-08.pdf}, note = {32~pages}, abstract = {We introduce weighted expressions, a~calculus to express quantitative properties over unranked trees. They involve products and sums from a semiring as well as classical boolean formulas. We~show that weighted expressions are expressively equivalent to a new class of weighted tree-walking automata. This new automata model is equipped with pebbles, and follows a depth-first-search policy in the tree.} }

@inproceedings{benzina-iccans11, address = {Republic of Maldives}, month = may, year = 2011, noeditor = {}, acronym = {{ICCANS}'11}, booktitle = {{P}roceedings of the {I}nternational {C}onference on {C}omputer {A}pplications and {N}etwork {S}ecurity ({ICCANS}'11)}, author = {Benzina, Hedi}, title = {Logic in Virtualized Systems}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/benzina-iccans11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/benzina-iccans11.pdf}, abstract = {As virtualized systems grow in complexity, they are increasingly vulnerable to denial-of-service (DoS) attacks involving resource exhaustion. A malicious driver downloaded and installed by the system administrator can trigger high-complexity behavior exhausting CPU time or stack space and making the whole system unavailable. Virtualized systems such as Xen or VirtualBox have been proposed to increase the level of security on computers. On the other hand, such virtualized systems are now targets for attacks. The weak spot of such systems is domain zero administration, which is left entirely under the administrator's responsibility, and is in particular vulnerable to attacks. \par We propose to let the administrator write and deploy security policies and rely on RuleGen, a policy compiler, and Orchids' fast, real-time monitoring engine to raise alerts in case any policy violation, expressed in a fragment of linear temporal logic, is detected. This approach has shown its efficiency against real DoS exploits. } }

@phdthesis{markey-HDR11, author = {Markey, Nicolas}, title = {Verification of Embedded Systems -- Algorithms and Complexity}, year = 2011, month = apr, type = {M{\'e}moire d'habilitation}, school = {{\'E}cole Normale Sup{\'e}rieure de Cachan, France}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hdr-nm.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hdr-nm.pdf} }

@incollection{CDM-fmtasp11, author = {Comon{-}Lundh, Hubert and Delaune, St{\'e}phanie and Millen, Jonathan K.}, title = {Constraint solving techniques and enriching the model with equational theories}, booktitle = {Formal Models and Techniques for Analyzing Security Protocols}, editor = {Cortier, V{\'e}ronique and Kremer, Steve}, series = {Cryptology and Information Security Series}, volume = 5, publisher = {{IOS} Press}, nochapter = {}, pages = {35-61}, year = 2011, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDM-fmtasp11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDM-fmtasp11.pdf}, abstract = {Derivability constraints represent in a symbolic way the infinite set of possible executions of a finite protocol, in presence of an arbitrary active attacker. Solving a derivability constraint consists in computing a simplified representation of such executions, which is amenable to the verification of any (trace) security property. Our goal is to explain this method on a non-trivial combination of primitives.\par In this chapter we explain how to model the protocol executions using derivability constraints, and how such constraints are interpreted, depending on the cryptographic primitives and the assumed attacker capabilities. Such capabilities are represented as a deduction system that has some specific properties. We choose as an example the combination of exclusive-or, symmetric encryption{\slash}decryption and pairing{\slash}unpairing. We explain the properties of the deduction system in this case and give a complete and terminating set of rules that solves derivability constraints. A similar set of rules has been already published for the classical Dolev-Yao attacker, but it is a new result for the combination of primitives that we consider. This allows to decide trace security properties for this combination of primitives and arbitrary finite protocols.} }

@inproceedings{ACD-cade11, address = {Wroc{\l}aw, Poland}, month = jul, year = 2011, volume = {6803}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Bj{\o}rner, Nikolaj and Sofronie-Stokkermans, Viorica}, acronym = {{CADE}'11}, booktitle = {{P}roceedings of the 23rd {I}nternational {C}onference on {A}utomated {D}eduction ({CADE}'11)}, author = {Arnaud, Mathilde and Cortier, V{\'e}ronique and Delaune, St{\'e}phanie}, title = {Deciding security for protocols with recursive tests}, pages = {49-63}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ACD-cade11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ACD-cade11.pdf}, doi = {10.1007/978-3-642-22438-6_6}, abstract = {Security protocols aim at securing communications over public networks. Their design is notoriously dicult and error-prone. Formal methods have shown their usefulness for providing a careful security analysis in the case of standard authentication and condentiality protocols. However, most current techniques do not apply to protocols that perform recursive computation e.g. on a list of messages received from the network.\par While considering general recursive input{\slash}output actions very quickly yields undecidability, we focus on protocols that perform recursive tests on received messages but output messages that depend on the inputs in a standard way. This is in particular the case of secured routing protocols, distributed right delegation or PKI certication paths. We provide NPTIME decision procedures for protocols with recursive tests and for a bounded number of sessions. We also revisit constraint system solving, providing a complete symbolic representation of the attacker knowledge.} }

@inproceedings{KSW-csf11, address = {Cernay-la-Ville, France}, month = jun, year = 2011, publisher = {{IEEE} Computer Society Press}, acronym = {{CSF}'11}, booktitle = {{P}roceedings of the 24th {IEEE} {C}omputer {S}ecurity {F}oundations {S}ymposium ({CSF}'11)}, author = {Kremer, Steve and Steel, Graham and Warinschi, Bogdan}, title = {Security for Key Management Interfaces}, pages = {266-280}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/KSW-csf11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KSW-csf11.pdf}, nolongps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/ rr-lsv-2011-07.ps}, nolongpsgz = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PSGZ/ rr-lsv-2011-07.ps.gz}, doi = {10.1109/CSF.2011.25}, abstract = {We propose a much-needed formal definition of security for cryptographic key management APIs. The advantages of our definition are that it is general, intuitive, and applicable to security proofs in both symbolic and computational models of cryptography. Our definition relies on an idealized API which allows only the most essential functions for generating, exporting and importing keys, and takes into account dynamic corruption of keys. Based on this we can define the security of more expressive APIs which support richer functionality. We illustrate our approach by showing the security of APIs both in symbolic and computational models.} }

@inproceedings{DKRS-csf11, address = {Cernay-la-Ville, France}, month = jun, year = 2011, publisher = {{IEEE} Computer Society Press}, acronym = {{CSF}'11}, booktitle = {{P}roceedings of the 24th {IEEE} {C}omputer {S}ecurity {F}oundations {S}ymposium ({CSF}'11)}, author = {Delaune, St{\'e}phanie and Kremer, Steve and Ryan, Mark D. and Steel, Graham}, title = {Formal analysis of protocols based on {TPM} state registers}, pages = {66-82}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DKRS-csf11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DKRS-csf11.pdf}, doi = {10.1109/CSF.2011.12}, abstract = {We~present a Horn-clause-based framework for analysing security protocols that use platform configuration registers~(PCRs), which are registers for maintaining state inside the Trusted Platform Module~(TPM). In~our model, the~PCR state space is unbounded, and our experience shows that a na{\"i}ve analysis using ProVerif or SPASS does not terminate. To address this, we extract a set of instances of the Horn clauses of our model, for which ProVerif does terminate on our examples. We~prove the soundness of this extraction process: no~attacks are lost, that~is, any query derivable in the more general set of clauses is also derivable from the extracted instances. The~effectiveness of our framework is demonstrated in two case studies: a~simplified version of Microsoft Bitlocker, and a digital envelope protocol that allows a user to choose whether to perform a decryption, or to verifiably renounce the ability to perform the decryption.} }

@techreport{rr-lsv-11-04, author = {Fribourg, Laurent and K{\"u}hne, Ulrich}, title = {Parametric Verification of Hybrid Automata Using the Inverse Method}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2011}, month = mar, type = {Research Report}, number = {LSV-11-04}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2011-04.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2011-04.pdf}, note = {25~pages}, abstract = {Hybrid systems combine continuous and discrete behavior. Hybrid Automata are a powerful formalism for the modeling and verification of such systems. A~common problem in hybrid system verification is the good parameters problem, which consists in identifying a subset of parameters which guarantee a certain behavior of a system. Recently, a method has been presented for attacking this problem for Timed Automata. In this report, we show the extension of this methodology for hybrid automata with linear and affine dynamics. The method is demonstrated with a distributed temperature control system and several other hybrid system benchmarks from the literature.} }

@inproceedings{CLC-stacs11, address = {Dortmund, Germany}, month = mar, year = 2011, volume = 9, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {D{\"u}rr, Christoph and Schwentick, {\relax Th}omas}, acronym = {{STACS}'11}, booktitle = {{P}roceedings of the 28th {A}nnual {S}ymposium on {T}heoretical {A}spects of {C}omputer {S}cience ({STACS}'11)}, author = {Comon{-}Lundh, Hubert and Cortier, V{\'e}ronique}, title = {How to prove security of communication protocols? A~discussion on the soundness of formal models w.r.t. computational ones}, pages = {29-44}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CLC-stacs11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CLC-stacs11.pdf}, doi = {10.4230/LIPIcs.STACS.2011.29}, abstract = {Security protocols are short programs that aim at securing communication over a public network. Their design is known to be error-prone with flaws found years later. That is why they deserve a careful security analysis, with rigorous proofs. Two main lines of research have been (independently) developed to analyse the security of protocols. On the one hand, formal methods provide with symbolic models and often automatic proofs. On the other hand, cryptographic models propose a tighter modeling but proofs are more difficult to write and to check. An approach developed during the last decade consists in bridging the two approaches, showing that symbolic models are sound w.r.t. symbolic ones, yielding strong security guarantees using automatic tools. These results have been developed for several cryptographic primitives (e.g. symmetric and asymmetric encryption, signatures, hash) and security properties. While proving soundness of symbolic models is a very promising approach, several technical details are often not satisfactory. Focusing on symmetric encryption, we describe the difficulties and limitations of the available results.} }

@inproceedings{CS-stacs11, address = {Dortmund, Germany}, month = mar, year = 2011, volume = 9, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {D{\"u}rr, Christoph and Schwentick, {\relax Th}omas}, acronym = {{STACS}'11}, booktitle = {{P}roceedings of the 28th {A}nnual {S}ymposium on {T}heoretical {A}spects of {C}omputer {S}cience ({STACS}'11)}, author = {ten~Cate, Balder and Segoufin, Luc}, title = {Unary negation}, pages = {344-355}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-stacs11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-stacs11.pdf}, doi = {10.4230/LIPIcs.STACS.2011.344}, abstract = {We study fragments of first-order logic and of least fixed point logic that allow only unary negation: negation of formulas with at most one free variable. These logics generalize many interesting known formalisms, including modal logic and the \(\mu\)-calculus, as well as conjunctive queries and monadic Datalog. We show that satisfiability and finite satisfiability are decidable for both fragments, and we pinpoint the complexity of satisfiability, finite satisfiability, and model checking. We also show that the unary negation fragment of first-order logic is model-theoretically very well behaved. In particular, it enjoys Craig interpolation and the Beth property.} }

@inproceedings{ST-stacs11, address = {Dortmund, Germany}, month = mar, year = 2011, volume = 9, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {D{\"u}rr, Christoph and Schwentick, {\relax Th}omas}, acronym = {{STACS}'11}, booktitle = {{P}roceedings of the 28th {A}nnual {S}ymposium on {T}heoretical {A}spects of {C}omputer {S}cience ({STACS}'11)}, author = {Segoufin, Luc and Toru{\'n}czyk, Szymon}, title = {Automata based verification over linearly ordered data domains}, pages = {81-92}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ST-stacs11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ST-stacs11.pdf}, doi = {10.4230/LIPIcs.STACS.2011.81}, abstract = {In this paper we work over linearly ordered data domains equipped with finitely many unary predicates and constants. We consider nondeterministic automata processing words and storing finitely many variables ranging over the domain. During a transition, these automata can compare the data values of the current configuration with those of the previous configuration using the linear order, the unary predicates and the constants.\par We show that emptiness for such automata is decidable, both over finite and infinite words, under reasonable computability assumptions on the linear order.\par Finally, we show how our automata model can be used for verifying properties of workflow specifications in the presence of an underlying database.} }

@article{LS-jcss11, publisher = {Elsevier Science Publishers}, journal = {Journal of Computer and System Sciences}, author = {Libkin, Leonid and Sirangelo, Cristina}, title = {Data exchange and schema mappings in open and closed worlds}, year = {2011}, month = may, volume = {77}, number = {3}, pages = {542-571}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-jcss11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-jcss11.pdf}, doi = {10.1016/j.jcss.2010.04.010} }

@phdthesis{kremer-HDR11, author = {Kremer, Steve}, title = {Modelling and analyzing security protocols in cryptographic process calculi}, year = 2011, month = mar, type = {M{\'e}moire d'habilitation}, school = {{\'E}cole Normale Sup{\'e}rieure de Cachan, France}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hdr-SK.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hdr-SK.pdf}, noslides = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/SLIDES/} }

@phdthesis{steel-HDR11, author = {Steel, Graham}, title = {Formal Analysis of Security {API}s}, year = 2011, month = mar, type = {M{\'e}moire d'habilitation}, school = {{\'E}cole Normale Sup{\'e}rieure de Cachan, France}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hdr-GS.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hdr-GS.pdf}, noslides = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/SLIDES/} }

@phdthesis{delaune-HDR11, author = {Delaune, St{\'e}phanie}, title = {Verification of security protocols: from confidentiality to privacy}, year = 2011, month = mar, type = {M{\'e}moire d'habilitation}, school = {{\'E}cole Normale Sup{\'e}rieure de Cachan, France}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hdr-SD.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hdr-SD.pdf}, abstract = {Security is a very old concern, which until quite recently was mostly of interest for military purposes. The deployment of electronic commerce changes this drastically. The security of exchanges is ensured by cryptographic protocols which are notoriously error prone. The formal verification of cryptographic protocols is a difficult problem that can be seen as a particular model-checking problem in an hostile environment. Many results and tools have been developed to automatically verify cryptographic protocols.\par Recently, new type of applications have emerged, in order to face new technological and societal challenges, e.g. electronic voting protocols, secure routing protocols for mobile ad hoc networks,~... These applications involve some features that are not taken into account by the existing verification tools, e.g. complex cryptographic primitives, privacy-type security properties,~... This prevents us from modelling these protocols in an accurate way. Moreover, protocols are often analysed in isolation and this is well-known to be not sufficient. In this thesis, we use formal methods to study these aspects concerning the verification of cryptographic protocols.} }

@inproceedings{pas-icdt11, address = {Uppsala, Sweden}, month = mar, year = 2011, publisher = {ACM Press}, editor = {Milo, Tova}, acronym = {{ICDT}'11}, booktitle = {{P}roceedings of the 14th {I}nternational {C}onference on {D}atabase {T}heory ({ICDT}'11)}, author = {Pasail{\u{a}}, Daniel}, title = {Conjunctive queries determinacy and rewriting}, pages = {220-231}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/pasaila-icdt11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/pasaila-icdt11.pdf}, doi = {10.1145/1938551.1938580} }

@inproceedings{BCH-acsd11, address = {Newcastle upon Tyne, UK}, month = jun, year = 2011, publisher = {{IEEE} Computer Society Press}, editor = {Caillaud, Beno{\^\i}t and Carmona, Josep}, acronym = {{ACSD}'11}, booktitle = {{P}roceedings of the 11th {I}nternational {C}onference on {A}pplication of {C}oncurrency to {S}ystem {D}esign ({ACSD}'11)}, author = {Balaguer, Sandie and Chatain, {\relax Th}omas and Haar, Stefan}, title = {Building Tight Occurrence Nets from Reveals Relations}, pages = {44-53}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCH-acsd11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCH-acsd11.pdf}, doi = {10.1109/ACSD.2011.16}, abstract = {Occurrence nets are a well known partial order model for the concurrent behavior of Petri nets. The causality and conflict relations between events, which are explicitly represented in occurrence nets, induce logical dependencies between event occurrences: the occurrence of an event~\(e\) in a run implies that all its causal predecessors also occur, and that no event in conflict with \(e\) occurs. But these structural relations do not express all the logical dependencies between event occurrences in maximal runs: in particular, the occurrence of~\(e\) in any maximal run may imply the occurrence of another event that is not a causal predecessor of~\(e\), in that run. The \emph{reveals} relation has been introduced in~[Haar, IEEE TAC 55(10):2310-2320, 2010] to express this dependency between two events. Here we generalize the reveals relation to express more general dependencies, involving more than two events, and we introduce ERL logic to express them as boolean formulas. Finally we answer the synthesis problem that arises: given an ERL formula~\(\varphi\), is there an occurrence net~\(\mathcal{N}\) such that \(\varphi\) describes exactly the dependencies between the events of~\(\mathcal{N}\)?} }

@inproceedings{HMN-atpn11, address = {Newcastle upon Tyne, UK}, month = jun, year = 2011, volume = {6709}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Kristensen, Lars M. and Petrucci, Laure}, acronym = {{PETRI~NETS}'11}, booktitle = {{P}roceedings of the 32nd {I}nternational {C}onference on {A}pplications and {T}heory of {P}etri {N}ets ({PETRI~NETS}'11)}, author = {Haddad, Serge and Mairesse, Jean and Nguyen, Hoang-Thach}, title = {Synthesis and Analysis of Product-form {P}etri Nets}, pages = {288-307}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/HMN-atpn11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HMN-atpn11.pdf}, doi = {10.1007/978-3-642-21834-7_16}, abstract = {For a large Markovian model, a {"}product form{"} is an explicit description of the steady-state behaviour which is otherwise generally untractable. Being first introduced in queueing networks, it has been adapted to Markovian Petri nets. Here we address three relevant issues for product-form Petri nets which were left fully or partially open: (1)~we~provide a sound and complete set of rules for the synthesis; (2)~we~characterise the exact complexity of classical problems like reachability; (3)~we~introduce a new subclass for which the normalising constant (a crucial value for product-form expression) can be efficiently computed.} }

@inproceedings{CFS-atpn2011, address = {Newcastle upon Tyne, UK}, month = jun, year = 2011, volume = {6709}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Kristensen, Lars M. and Petrucci, Laure}, acronym = {{PETRI~NETS}'11}, booktitle = {{P}roceedings of the 32nd {I}nternational {C}onference on {A}pplications and {T}heory of {P}etri {N}ets ({PETRI~NETS}'11)}, author = {Chambart, Pierre and Finkel, Alain and Schmitz, Sylvain}, title = {Forward Analysis and Model Checking for Trace Bounded {WSTS}}, nopages = {49-68}, url = {http://arxiv.org/abs/1004.2802}, doi = {10.1007/978-3-642-21834-7_4}, abstract = {We investigate a subclass of well-structured transition systems~(WSTS), the bounded---in the sense of Ginsburg and Spanier (Trans. AMS 1964)---complete deterministic ones, which we claim provide an adequate basis for the study of forward analyses as developed by Finkel and Goubault-Larrecq (ICALP~2009). Indeed, we prove that, unlike other conditions considered previously for the termination of forward analysis, boundedness is decidable. Boundedness turns out to be a valuable restriction for WSTS verification, as we show that it further allows to decide all \(\omega\)-regular properties on the set of infinite traces of the system.} }

@inproceedings{ACGP-rsa11, address = {San Francisco, California, USA}, month = feb, year = 2011, volume = 6558, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Kiayias, Aggelos}, acronym = {{CT-RSA}'11}, booktitle = {{P}roceedings of the {C}ryptographers' {T}rack at the {RSA} {C}onference 2011 ({CT-RSA}'11)}, author = {Abdalla, Michel and Chevalier, C{\'e}line and Granboulan, Louis and Pointcheval, David}, title = {Contributory Password-Authenticated Group Key Exchange with Join Capability}, pages = {142-160}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ACGP-rsa11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ACGP-rsa11.pdf}, doi = {10.1007/978-3-642-19074-2_11}, abstract = {Password-based authenticated group key exchange allows any group of users in possession of a low-entropy secret key to establish a common session key even in the presence of adversaries. In this paper, we propose a new generic construction of password-authenticated group key exchange protocol from any two-party password-authenticated key exchange with explicit authentication. Our new construction has several advantages when compared to existing solutions. First, our construction only assumes a common reference string and does not rely on any idealized models. Second, our scheme enjoys a simple and intuitive security proof in the universally composable framework and is optimal in the sense that it allows at most one password test per user instance. Third, our scheme also achieves a strong notion of security against insiders in that the adversary cannot bias the distribution of the session key as long as one of the players involved in the protocol is honest. Finally, we show how to easily extend our protocol to the dynamic case in a way that the costs of establishing a common key between two existing groups is significantly smaller than computing a common key from scratch.} }

@inproceedings{FFSS-lics2011, address = {Toronto, Canada}, month = jun, year = 2011, publisher = {{IEEE} Computer Society Press}, acronym = {{LICS}'11}, booktitle = {{P}roceedings of the 26th {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'11)}, author = {Figueira, Diego and Figueira, Santiago and Schmitz, Sylvain and Schnoebelen, {\relax Ph}ilippe}, title = {{A}ckermannian and Primitive-Recursive Bounds with {D}ickson's Lemma}, pages = {269-278}, url = {http://arxiv.org/abs/1007.2989}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FFSS-lics11.pdf}, doi = {10.1109/LICS.2011.39}, abstract = {Dickson's Lemma is a simple yet powerful tool widely used in decidability proofs, especially when dealing with counters or related data structures in algorithmics, verification and model-checking, constraint solving, logic, etc. While Dickson's Lemma is well-known, most computer scientists are not aware of the complexity upper bounds that are entailed by its use. This is mainly because, on this issue, the existing literature is not very accessible.\par We propose a new analysis of the length of bad sequences over \((\mathbb{N}^{k},\leq)\), improving on earlier results and providing upper bounds that are essentially tight. This analysis is complemented by a {"}user guide{"} explaining through practical examples how to easily derive complexity upper bounds from Dickson's Lemma.} }

@inproceedings{GLV-lics2011, address = {Toronto, Canada}, month = jun, year = 2011, publisher = {{IEEE} Computer Society Press}, acronym = {{LICS}'11}, booktitle = {{P}roceedings of the 26th {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'11)}, author = {Goubault{-}Larrecq, Jean and Varacca, Daniele}, title = {Continuous Random Variables}, pages = {97-106}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/GLV-lics2011.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLV-lics2011.pdf}, corrigendumpdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLV-lics2011-errata.pdf}, doi = {10.1109/LICS.2011.23}, abstract = {We introduce the domain of continuous random variables (CRV) over a domain, as an alternative to Jones and Plotkin's probabilistic powerdomain. While no known Cartesian-closed category is stable under the latter, we show that the so-called thin (uniform) CRVs define a strong monad on the Cartesian-closed category of bc-domains. We also characterize their inequational theory, as (fair-)coin algebras. We apply this to solve a recent problem posed by M. Escard{\'o}: testing is semi-decidable for EPCF terms. CRVs arose from the study of the second author's (layered) Hoare indexed valuations, and we also make the connection apparent.} }

@inproceedings{Fig-lics2011, address = {Toronto, Canada}, month = jun, year = 2011, publisher = {{IEEE} Computer Society Press}, acronym = {{LICS}'11}, booktitle = {{P}roceedings of the 26th {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'11)}, author = {Figueira, Diego}, title = {A decidable two-way logic on data words}, pages = {365-374}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/Fig-lics2011.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Fig-lics2011.pdf}, doi = {10.1109/LICS.2011.18}, abstract = {We study the satisfiability problem for a logic on data words. A~data word is a finite word where every position carries a label from a finite alphabet and a data value from an infinite domain. The logic we consider is two-way, contains \emph{future} and \emph{past} modalities, which are considered as reflexive and transitive relations, and data equality and inequality tests. This logic corresponds to the fragment of XPath with the 'followingsibling- or-self' and 'preceding-sibling-or-self' axes over data words. We show that this problem is decidable, EXPSPACE-complete. This is surprising considering that with the strict (non-reflexive) navigation relations the satisfiability problem is undecidable. To~prove this, we~first reduce the problem to a derivation problem for an infinite transition system, and then we show how to abstract this problem into a reachability problem of a finite transition system.} }

@phdthesis{villard-phd2010, author = {Villard, Jules}, title = {Heaps and Hops}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2011, month = feb, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/villard-phd.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/villard-phd.pdf}, abstract = {This thesis is about the specification and verification of copyless message-passing programs, a particular kind of concurrent programs that communicate by message passing. Instead of copying messages over channels, processes exchange pointers into a shared memory where the actual contents of messages are stored. Channels are themselves objects in the heap that can be communicated, thus achieving full mobility. This flexible and efficient programming paradigm must be used carefully: every pointer that is communicated becomes shared between its sender and its recipient, which may introduce races. To err on the side of caution, the sender process should not attempt to access the area of storage circumscribed by a message once it has been sent. Indeed, this right is now reserved to the recipient, who may already have modified it or even disposed of it. In other words, the ownership of pieces of heap hops from process to process following the flow of messages.\par Copyless message passing combines two features of programs that make formal verification challenging: explicit memory management and concurrency. To tackle these difficulties, we base our approach on two recent developments. On the one hand, concurrent separation logic produces concise proofs of pointer-manipulating programs by keeping track only of those portions of storage owned by the program. We use such local reasoning techniques to analyse the fluxes of ownership in programs, and ensure in particular that no dangling pointer will be dereferenced or freed at runtime. On the other hand, channel contracts, a form of session types introduced by the Sing\# programming language, provide an abstraction of the exchanges of messages that can be used to statically verify that programs never face unexpected message receptions and that all messages are delivered before a channel is closed.\par The contributions contained in this thesis fall into three categories. First, we give a semantics to copyless message-passing programs, the ownership transfers they induce and contracts, and link the three together. In doing so, we provide the first formal model of a theoretically significant subset of the Sing\# programming language. In particular, we show that some properties of their contracts rub off on programs, which justifies their use as protocol specifications. Second, we introduce the first proof system for copyless message passing, based on separation logic and contracts. The proof system discharges parts of the verification of programs on the verification of their contracts. The marriage of these two techniques allows one to prove that programs are free from memory faults, race conditions and message-passing errors such as unspecified receptions and undelivered messages. Moreover, we show how the logic and contracts cooperate to prove the absence of memory leaks. Third, we give an implementation of our analysis, Heap-Hop, that takes annotated programs as input and automatically checks the given specifications and deduces which of the properties above are enjoyed by the program. The only annotations needed by Heap-Hop are pre and postconditions of each function, loop invariants, and the contracts followed by the communications.} }

@book{CK-ios2011, editor = {Cortier, V{\'e}ronique and Kremer, Steve}, title = {Formal Models and Techniques for Analyzing Security Protocols}, publisher = {{IOS} Press}, year = {2011}, series = {Cryptology and Information Security Series}, volume = 5, url = {http://www.iospress.nl/loadtop/load.php?isbn=9781607507130} }

@inproceedings{BDDHP-valuetools11, address = {Cachan, France}, month = may, year = 2011, acronym = {{VALUETOOLS}'11}, booktitle = {{P}roceedings of the 5th {I}nternational {C}onference on {P}erformance {E}valuation {M}ethodologies and {T}ools ({VALUETOOLS}'11)}, author = {Ballarini, Paolo and Djafri, Hilal and Duflot, Marie and Haddad, Serge and Pekergin, Nihal}, title = {{HASL}: An~Expressive Language for Statistical Verification of Stochastic Models}, pages = {306-315}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDDHP-valuetools11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDDHP-valuetools11.pdf}, abstract = {We introduce the Hybrid Automata Stochastic Logic (HASL), a new temporal logic formalism for the verification of discrete event stochastic processes (DESP). HASL employs Linear Hybrid Automata (LHA) as machineries to select prefixes of relevant execution paths of a DESP~\(\mathcal{D}\). The advantage with LHA is that rather elaborate information can be collected \emph{on-the-fly} during path selection, providing the user with a powerful means to express sophisticated measures. A formula of HASL consists of an LHA~\(\mathcal{A}\) and an expression~\(Z\) referring to moments of \emph{path random variables}. A~simulation-based statistical engine is employed to obtained a confidence-interval estimate of the expected value of~\(Z\). In essence HASL provide a unifying verification framework where sophisticated temporal reasoning is naturally blended with elabo- rate reward-based analysis. We illustrate the HASL approach by means of some examples and a discussion about its expressivity. We also provide empirical evidence obtained through COSMOS, a prototype software tool for HASL verification.} }

@article{BFLM-cacm11, publisher = {ACM Press}, journal = {Communications of the~{ACM}}, author = {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim~G. and Markey, Nicolas}, title = {Quantitative analysis of real-time systems using priced timed automata}, volume = 54, number = 9, month = sep, pages = {78-87}, year = 2011, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLM-cacm11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLM-cacm11.pdf}, doi = {10.1145/1995376.1995396}, abstract = {The problems of time-dependent behavior in general, and dynamic resource allocation in particular, pervade many aspects of modern life. Prominent examples range from reliability and efficient use of communication resources in a telecommunication network to the allocation of tracks in a continental railway network, from scheduling the usage of computational resources on a chip for durations of nano-seconds to the weekly, monthly, or longer-range reactive planning in a factory or a supply chain.} }

@inproceedings{BFHR-fossacs11, address = {Saarbr{\"u}cken, Germany}, month = mar # {-} # apr, year = 2011, volume = {6604}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Hofmann, Martin}, acronym = {{FoSSaCS}'11}, booktitle = {{P}roceedings of the 14th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'11)}, author = {Bonnet, R{\'e}mi and Finkel, Alain and Haddad, Serge and Rosa{-}Velardo, Fernando}, title = {Ordinal Theory for Expressiveness of Well Structured Transition Systems}, pages = {153-167}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHR-fossacs11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHR-fossacs11.pdf}, doi = {10.1007/978-3-642-19805-2_11} }

@inproceedings{FS-stacs11, address = {Dortmund, Germany}, month = mar, year = 2011, volume = 9, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {D{\"u}rr, Christoph and Schwentick, {\relax Th}omas}, acronym = {{STACS}'11}, booktitle = {{P}roceedings of the 28th {A}nnual {S}ymposium on {T}heoretical {A}spects of {C}omputer {S}cience ({STACS}'11)}, author = {Figueira, Diego and Segoufin, Luc}, title = {Bottom-up automata on data trees and vertical {XP}ath}, pages = {93-104}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FS-stacs11.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FS-stacs11.pdf}, doi = {10.4230/LIPIcs.STACS.2011.93}, abstract = {A data tree is a tree whose every node carries a label from a finite alphabet and a datum from some infinite domain. We introduce a new model of automata over unranked data trees with a decidable emptiness problem. It is essentially a bottom-up alternating automaton with one register, enriched with epsilon-transitions that perform tests on the data values of the subtree. We show that it captures the expressive power of the vertical fragment of XPath --containing the child, descendant, parent and ancestor axes-- obtaining thus a decision procedure for its satisfiability problem.} }

@inproceedings{BKKL-ceeset2008, address = {Brno, Czech Republic}, year = 2011, volume = {4980}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Huzar, Zbigniew and Koc{\'\i}, Radek and Meyer, Bertrand and Walter, Bartosz and Zendulka, Jaroslav}, acronym = {{CEE-SET}'08}, booktitle = {{R}evised {S}elected {P}apars of the 3rd {IFIP} {TC2} {C}entral and {E}ast {E}uropean {C}onference on {S}oftware {E}ngineering {T}echniques ({CEE-SET}'08)}, author = {Bollig, Benedikt and Katoen, Joost-Pieter and Kern, Carsten and Leucker, Martin}, title = {{SMA}---The {S}myle Modeling Approach}, pages = {103-117}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-ceeset2008.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-ceeset2008.pdf}, doi = {10.1007/978-3-642-22386-0_8}, abstract = {This paper introduces the model-based software development methodology SMA---the Smyle Modeling Approach---which is centered around Smyle, a dedicated learning procedure to support engineers to interactively obtain design models from requirements, characterized as either being desired (positive) or unwanted (negative) system behavior. The learning approach is complemented by scenario patterns where the engineer can specify clearly desired or unwanted behavior. This~way, user interaction is reduced to the interesting scenarios limiting the design effort considerably. In~SMA, the learning phase is complemented by an effective analysis phase that allows for detecting design flaws at an early design stage. This paper describes the approach and reports on first practical experiences.} }

@article{JGL-jyg10, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {Goubault{-}Larrecq, Jean}, title = {Musings Around the Geometry of Interaction, and Coherence}, volume = 412, number = 20, pages = {1998-2014}, year = 2011, month = apr, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/jgl-jyg10.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/jgl-jyg10.pdf}, doi = {10.1016/j.tcs.2010.12.023}, abstract = {We introduce the Danos-R{\'e}gnier category \(\mathcal{DR}(M)\) of a linear inverse monoid~\(M\), as~a categorical description of geometries of interaction~(GOI) inspired from the weight algebra. The natural setting for GOI is that of a so-called weakly Cantorian linear inverse monoid, in which case \(\mathcal{DR}(M)\) is a kind of symmetrized version of the classical Abramsky-Haghverdi-Scott construction of a weak linear category from a GOI situation. It is well-known that GOI is perfectly suited to describe the multiplicative fragment of linear logic, and indeed \(\mathcal{DR}(M)\) will be a \(\star\)-autonomous category in this case. It is also well-known that the categorical interpretation of the other linear connectives conflicts with GOI interpretations. We make this precise, and show that \(\mathcal{DR}(M)\) has no terminal object, no cartesian product of any two objects, and no exponential---whatever \(M\)~is, unless \(M\)~is trivial. However, a form of coherence completion of \(\mathcal{DR}(M)\) \textit{{\`a} la} Hu-Joyal (which for additives resembles a layered approach \textit{{\`a} la} Hughes-van Glabbeek), provides a model of full classical linear logic, as soon as \(M\) is weakly Cantorian. One finally notes that Girard's notion of \emph{coherence} is pervasive, and instrumental in every aspect of this work.} }

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