@inproceedings{BFLM-hscc10, address = {Stockholm, Sweden}, month = apr, year = 2010, publisher = {ACM Press}, editor = {Johansson, Karl Henrik and Yi, Wang}, acronym = {{HSCC}'10}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {H}ybrid {S}ystems: {C}omputation and {C}ontrol ({HSCC}'10)}, author = {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim G. and Markey, Nicolas}, title = {Timed Automata with Observers under Energy Constraints}, pages = {61-70}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLM-hscc10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLM-hscc10.pdf}, doi = {10.1145/1755952.1755963}, abstract = {In this paper, we study one-clock priced timed automata in which prices can grow linearly (\(\frac{dp}{dt}=k\)) or exponentially (\(\frac{dp}{dt}=kp\)), with discontinuous updates on edges. We propose EXPTIME algorithms to decide the existence of controllers that ensure existence of infinite runs or reachability of some goal location with non-negative observer value all along the run. These algorithms consist in computing the optimal delays that should be elapsed in each location along a run, so that the final observer value is maximized (and never goes below zero).} }

@inproceedings{VLC-tacas10, address = {Paphos, Cyprus}, month = mar, year = 2010, volume = {6015}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Esparza, Javier and Majumdar, Rupak}, acronym = {{TACAS}'10}, booktitle = {{P}roceedings of the 16th {I}nternational {C}onference on {T}ools and {A}lgorithms for {C}onstruction and {A}nalysis of {S}ystems ({TACAS}'10)}, author = {Villard, Jules and Lozes, {\'E}tienne and Calcagno, Cristiano}, title = {Tracking Heaps that Hop with Heap-Hop}, pages = {275-279}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/VLC-tacas10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/VLC-tacas10.pdf}, doi = {10.1007/978-3-642-12002-2_23}, abstract = {Heap-Hop is a program prover for concurrent heap-manipulating programs that use Hoare monitors and message-passing synchronization. Programs are annotated with pre and post-conditions and loop invariants, written in a fragment of separation logic. Communications are governed by a form of session types called contracts. Heap-Hop can prove safety and race-freedom and, thanks to contracts, absence of memory leaks and deadlock-freedom. It has been used in several case studies, including concurrent programs for copyless list transfer, service provider protocols, and load-balancing parallel tree disposal.} }

@inproceedings{DS-fossacs10, address = {Paphos, Cyprus}, month = mar, year = 2010, volume = {6014}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Ong, C.-H. Luke}, acronym = {{FoSSaCS}'10}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'10)}, author = {Demri, St{\'e}phane and Sangnier, Arnaud}, title = {When Model-Checking Freeze {LTL} over Counter Machines Becomes Decidable}, pages = {176-190}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DS-fossacs10.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DS-fossacs10.pdf}, doi = {10.1007/978-3-642-12032-9_13}, abstract = {We study the decidability status of model-checking freeze LTL over various subclasses of counter machines for which the reachability problem is known to be decidable (reversal-bounded counter machines, vector additions systems with states, flat counter machines, one-counter machines). In freeze LTL, a register can store a counter value and at some future position an equality test can be done between a register and a counter value. Herein, we complete an earlier work started on one-counter machines by considering other subclasses of counter machines, and especially the class of reversal-bounded counter machines. This gives us the opportuniy to provide a systematic classification that distinguishes determinism vs. nondeterminism and we consider subclasses of formulae by restricting the set of atomic formulae or\slash and the polarity of the occurrences of the freeze operators, leading to the flat fragment.} }

@inproceedings{tCF-fossacs10, address = {Paphos, Cyprus}, month = mar, year = 2010, volume = {6014}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Ong, C.-H. Luke}, acronym = {{FoSSaCS}'10}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'10)}, author = {ten~Cate, Balder and Fontaine, Ga{\"e}lle}, title = {An Easy Completeness Proof for the Modal \(\mu\)-Calculus on Finite Trees}, pages = {161-175}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/tCF-fossacs10.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/tCF-fossacs10.pdf}, doi = { 10.1007/978-3-642-12032-9_12}, abstract = {We give a complete axiomatization for the modal \(\mu\)-calculus on finite trees. While the completeness of our axiomatization already follows from a more powerful result by Igor Walukiewicz, our proof is easier and uses very different tools, inspired from model theory. We show that our approach generalizes to certain axiomatic extensions, and to the extension of the \(\mu\)-calculus with graded modalities. We hope that the method might be helpful for other completeness proofs as well.} }

@inproceedings{CS-fossacs10, address = {Paphos, Cyprus}, month = mar, year = 2010, volume = {6014}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Ong, C.-H. Luke}, acronym = {{FoSSaCS}'10}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'10)}, author = {Chambart, Pierre and Schnoebelen, {\relax Ph}ilippe}, title = {Toward a compositional theory of leftist grammars and transformations}, pages = {237-251}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-fossacs10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-fossacs10.pdf}, doi = {10.1007/978-3-642-12032-9_17}, abstract = {Leftist grammars [Motwani \textit{et~al.}, STOC~2000] are special semi-Thue systems where symbols can only insert or erase to their left. We~develop a theory of leftist grammars seen as word transformers as a tool toward rigorous analyses of their computational power. Our~main contributions in this first paper are (1)~constructions proving that leftist transformations are closed under compositions and transitive closures, and (2)~a~proof that bounded reachability is NP-complete even for leftist grammars with acyclic rules.} }

@article{schmitz-scp10, publisher = {Elsevier Science Publishers}, journal = {Science of Computer Programming}, author = {Sylvain Schmitz}, title = {An Experimental Ambiguity Detection Tool}, volume = 75, number = {1-2}, pages = {71-84}, month = jan, year = 2010, doi = {10.1016/j.scico.2009.07.002}, url = {http://hal.archives-ouvertes.fr/hal-00436398}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/schmitz-scp10.pdf}, abstract = {Although programs convey an unambiguous meaning, the grammars used in practice to describe their syntax are often ambiguous, and completed with disambiguation rules. Whether these rules achieve the removal of all the ambiguities while preserving the original intended language can be difficult to ensure. We present an experimental ambiguity detection tool for GNU Bison, and illustrate how it can assist a grammatical development for a subset of Standard~ML.} }

@inproceedings{CLPV-vmcai10, address = {Madrid, Spain}, month = jan, year = 2010, volume = 5944, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Barthe, Gilles and Hermenegildo, Manuel}, acronym = {{VMCAI}'10}, booktitle = {{P}roceedings of the 11th {I}nternational {C}onference on {V}erification, {M}odel {C}hecking and {A}bstract {I}nterpretation ({VMCAI}'10)}, author = {Chadha, Rohit and Legay, Axel and Prabhakar, Pavithra and Viswanathan, Mahesh}, title = {Complexity bounds for the verification of real-time software}, pages = {95-111}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CLPV-vmcai10.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CLPV-vmcai10.pdf}, doi = {10.1007/978-3-642-11319-2_10}, abstract = {We present uniform approaches to establish complexity bounds for decision problems such as reachability and simulation, that arise naturally in the verification of timed software systems. We model timed software systems as timed automata augmented with a data store (like a pushdown stack) and show that there is at least an exponential blowup in complexity of verification when compared with untimed systems. Our proof techniques also establish complexity results for boolean programs, which are automata with stores that have additional boolean variables.} }

@article{JGL-mscs09, publisher = {Cambridge University Press}, journal = {Mathematical Structures in Computer Science}, author = {Goubault{-}Larrecq, Jean}, title = {{D}e~{G}root Duality and Models of Choice: Angels, Demons, and Nature}, volume = {20}, number = 2, pages = {169-237}, month = apr, year = 2010, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-mscs09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-mscs09.pdf}, doi = {10.1017/S0960129509990363}, abstract = {We introduce convex-concave duality for various models of non-deterministic choice, probabilistic choice, and the two of them together. This complements the well-known duality of stably compact spaces in a pleasing way: convex-concave duality swaps angelic and demonic choice, and leaves probabilistic choice invariant.} }

@article{bbc09-lmcs, journal = {Logical Methods in Computer Science}, author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and Chevalier, Fabrice}, title = {O-Minimal Hybrid Reachability Games}, year = 2010, month = jan, volume = 6, number = {1:1}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBC-lmcs09.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBC-lmcs09.pdf}, doi = {10.2168/LMCS-6(1:1)2010}, abstract = {In this paper, we consider reachability games over general hybrid systems, and distinguish between two possible observation frameworks for those games: either the precise dynamics of the system is seen by the players (this is the perfect observation framework), or only the starting point and the delays are known by the players (this is the partial observation framework). In the first more classical framework, we show that time-abstract bisimulation is not adequate for solving this problem, although it is sufficient in the case of timed automata. That is why we consider an other equivalence, namely the suffix equivalence based on the encoding of tra jectories through words. We show that this suffix equivalence is in general a correct abstraction for games. We apply this result to o-minimal hybrid systems, and get decidability and computability results in this framework. For the second framework which assumes a partial observation of the dynamics of the system, we propose another abstraction, called the superword encoding, which is suitable to solve the games under that assumption. In that framework, we also provide decidability and computability results.} }

@article{BCM-icomp2009, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Bouyer, Patricia and Chevalier, Fabrice and Markey, Nicolas}, title = {On the Expressiveness of {TPTL} and~{MTL}}, volume = {208}, number = 2, pages = {97-116}, month = feb, year = 2010, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCM-icomp09.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCM-icomp09.pdf}, doi = {10.1016/j.ic.2009.10.004}, abstract = {TPTL and MTL are two classical timed extensions of~LTL. In~this paper, we prove the 20-year-old conjecture that TPTL is strictly more expressive than~MTL. But we show that, surprisingly, the TPTL~formula proposed by Alur and Henzinger for witnessing this conjecture \emph{can} be expressed in~MTL. More generally, we show that TPTL formulae using only modality~F can be translated into~MTL.} }

@inproceedings{FS-sofsem10, address = {\v{S}pindler\r{u}v Ml\'{y}n, Czech Republic}, month = jan, year = 2010, volume = 5901, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Peleg, David and Muscholl, Anca}, acronym = {{SOFSEM}'10}, booktitle = {{P}roceedings of the 36th International Conference on Current Trends in Theory and Practice of Computer Science ({SOFSEM}'10)}, author = {Finkel, Alain and Sangnier, Arnaud}, title = {Mixing coverability and reachability to analyze {VASS} with one zero-test}, pages = {394-406}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-sofsem10.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-sofsem10.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FS-sofsem10.ps}, doi = {10.1007/978-3-642-11266-9_33}, abstract = {We study Vector Addition Systems with States (VASS) extended in such a way that one of the manipulated integer variables can be tested to zero. For this class of system, it has been proved that the reachability problem is decidable. We prove here that boundedness, termination and reversal-boundedness are decidable for VASS with one zero-test. To decide reversal-boundedness, we provide an original method which mixes both the construction of the coverability graph for VASS and the computation of the reachability set of reversal-bounded counter machines. The same construction can be slightly adapted to decide boundedness and hence termination.} }

@article{BKKL-tse09, publisher = {{IEEE} Computer Society Press}, journal = {IEEE Transactions on Software Engineering}, author = {Bollig, Benedikt and Katoen, Joost-Pieter and Kern, Carsten and Leucker, Martin}, title = {Learning Communicating Automata from~{MSCs}}, volume = {36}, number = {3}, pages = {390-408}, month = may # {-} # jun, year = 2010, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-tse09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-tse09.pdf}, doi = {10.1109/TSE.2009.89}, abstract = {This paper is concerned with bridging the gap between requirements and distributed systems. Requirements are defined as basic message sequence charts (MSCs) specifying positive and negative scenarios. Communicating finite-state machines (CFMs), \textit{i.e.}, finite automata that communicate via FIFO buffers, act as system realizations. The key contribution is a generalization of Angluin's learning algorithm for synthesizing CFMs from MSCs. This approach is exact---the resulting CFM precisely accepts the set of positive scenarions and rejects all negative ones---and yields fully asynchronous implementations. The paper investigates for which classes of MSC languages CFMs can be learned, presents an optimization technique for learning partial orders, and provides substantial empirical evidence indicating the practical feasibility of the approach.} }

@article{BKKL-cai09, publisher = {Slovak Academy of Sciences}, journal = {Computing and Informatics}, author = {Bollig, Benedikt and Katoen, Joost-Pieter and Kern, Carsten and Leucker, Martin}, title = {{SMA}---The Smyle Modeling Approach}, volume = {29}, number = {1}, pages = {45-72}, year = 2010, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-cai09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-cai09.pdf}, abstract = {This paper introduces the model-based software development lifecycle model \emph{SMA}---the Smyle \emph{Modeling Approach}---which is centered around \emph{Smyle}. \emph{Smyle} is 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. Within \emph{SMA}, the learning approach is complemented by so-called \emph{scenario patterns} where the engineer can specify \emph{clearly} desired or unwanted behavior. This way, user interaction is reduced to the interesting scenarios limiting the design effort considerably. In~\emph{SMA}, the learning phase is further complemented by an effective analysis phase that allows for detecting design flaws at an early design stage. Using learning techniques allows us to gradually develop and refine requirements, naturally supporting evolving requirements, and allows for a rather inexpensive redesign in case anomalous system behavior is detected during analysis, testing, or maintenance. This paper describes the approach and reports on first practical experiences.} }

@inproceedings{ZBH-lads09, address = {Turin, Italy}, year = 2010, volume = 6039, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Dastani, Mehdi and El~Fallah Seghrouchni, Amal and Leite, Jo{\~a}o and Torroni, Paolo}, acronym = {{LADS}'09}, booktitle = {{R}evised {S}elected {P}apers of the 2nd {W}orkshop on {LA}nguages, methodologies and {D}evelopment tools for multi-agent system{S} ({LADS}'09)}, author = {Zargayouna, Mahdi and Balbo, Flavien and Haddad, Serge}, title = {Agents Secure Interaction in Data Driven Languages}, pages = {72-91}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ZBH-lads09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ZBH-lads09.pdf}, doi = {10.1007/978-3-642-13338-1_5}, abstract = {This paper discusses the security issues in data driven coordination languages. These languages rely on a data space shared by the agents and used to coordinate their activities. We extend these languages with a main distinguishing feature, which is the possibility to define fine-grained security conditions, associated with every datum in the shared space. Two main ideas makes it possible: the consideration of an abstraction of agents' states in the form of data at language level and the introduction of a richer interaction mechanism than state-of-the-art templates. This novel security mechanism allows both agents and system designers to prohibit undesirable interactions.} }

@article{DKS-jcs09, publisher = {{IOS} Press}, journal = {Journal of Computer Security}, author = {Delaune, St{\'e}phanie and Kremer, Steve and Steel, Graham}, title = {Formal Analysis of {PKCS\#11} and Proprietary Extensions}, volume = 18, number = 6, pages = {1211-1245}, year = 2010, month = nov, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKS-jcs09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKS-jcs09.pdf}, doi = {10.3233/JCS-2009-0394}, abstract = {PKCS\#11 denes an API for cryptographic devices that has been widely adopted in industry. However, it has been shown to be vulnerable to a variety of attacks that could, for example, compromise the sensitive keys stored on the device. In this paper, we set out a formal model of the operation of the API, which diers from previous security API models notably in that it accounts for non-monotonic mutable global state. We give decidability results for our formalism, and describe an implementation of the resulting decision procedure using the model checker NuSMV. We report some new attacks and prove the safety of some congurations of the API in our model. We also analyse proprietary extensions proposed by nCipher (Thales) and Eracom (Safenet), designed to address the shortcomings of PKCS\#11.} }

@article{goubault-jcs09, publisher = {{IOS} Press}, journal = {Journal of Computer Security}, author = {Goubault{-}Larrecq, Jean}, title = {Finite Models for Formal Security Proofs}, volume = 18, number = 6, pages = {1247-1299}, year = 2010, month = nov, url = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-jcs09.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-jcs09.pdf}, doi = {10.3233/JCS-2009-0395}, abstract = {First-order logic models of security for cryptographic protocols, based on variants of the Dolev-Yao model, are now well-established tools. Given that we have checked a given security protocol using a given first-order prover, how hard is it to extract a formally checkable proof of it, as required in, \textit{e.g.}, common criteria at the highest evaluation level~(EAL7)? We~demonstrate that this is surprisingly hard in the general case: the problem is non-recursive. Nonetheless, we show that we can instead extract finite models~\(\mathcal{M}\) from a set~\(S\) of clauses representing~\(\pi\), automatically, and give two ways of doing~so. We~then define a model-checker testing \(\mathcal{M} \models S\), and show how we can instrument it to output a formally checkable proof, \textit{e.g.}, in~Coq. Experience on a number of protocols shows that this is practical, and that even complex (secure) protocols modulo equational theories have small finite models, making our approach suitable.} }

@article{LAL-jar09, publisher = {Springer}, journal = {Journal of Automated Reasoning}, author = {Longuet, Delphine and Aiguier, Marc and Le{~}Gall, Pascale}, title = {Proof-guided test selection from first-order specifications with equality}, year = {2010}, month = dec, volume = 45, number = 4, pages = {437-473}, nmnote = {special issue on Tests and Proofs}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LAL-jar09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LAL-jar09.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LAL-jar09.ps}, doi = {10.1007/s10817-009-9128-7}, abstract = {This paper deals with test case selection from axiomatic specifications whose axioms are quantifier-free first-order formulas with equality. We first prove the existence of an ideal exhaustive test set to start the selection from. We then propose an extension of the test selection method called axiom unfolding, originally defined for algebraic specifications, to quantifier-free first-order specifications with equality. This method basically consists of a case analysis of the property under test (the test purpose) according to the specification axioms. It is based on a proof search for the different instances of the test purpose. Since the calculus is sound and complete, this allows us to provide a full coverage of this property. The generalisation we propose allows to deal with any kind of predicate (not only equality) and with any form of axiom and test purpose (not only equations or Horn clauses). Moreover, it improves our previous works with efficiently dealing with the equality predicate, thanks to the paramodulation rule.} }

@article{CCZ-tocl08, publisher = {ACM Press}, journal = {ACM Transactions on Computational Logic}, author = {Comon{-}Lundh, Hubert and Cortier, V{\'e}ronique and Z{\u{a}}linescu, Eugen}, title = {Deciding security properties for cryptographic protocols. Application to key cycles}, volume = 11, number = 2, nopages = {}, month = jan, year = 2010, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CCZ-tocl09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CCZ-tocl09.pdf}, doi = {10.1145/1656242.1656244}, abstract = {There is a large amount of work dedicated to the formal verification of security protocols. In~this paper, we~revisit and extend the NP-complete decision procedure for a bounded number of sessions. We use a, now standard, deducibility constraint formalism for modeling security protocols. Our~first contribution is to give a simple set of constraint simplification rules, that allows to reduce any deducibility constraint to a set of solved forms, representing all solutions (within the bound on sessions).\par As a consequence, we prove that deciding the existence of key cycles is NP-complete for a bounded number of sessions. The problem of key-cycles has been put forward by recent works relating computational and symbolic models. The so-called soundness of the symbolic model requires indeed that no key cycle (\textit{e.g.},~enc\((k, k)\)) ever occurs in the execution of the protocol. Otherwise, stronger security assumptions (such as KDM-security) are required.\par We show that our decision procedure can also be applied to prove again the decidability of authentication-like properties and the decidability of a significant fragment of protocols with timestamps.} }

@article{KM-jcs09, publisher = {{IOS} Press}, journal = {Journal of Computer Security}, author = {Kremer, Steve and Mazar{\'e}, Laurent}, title = {Computationally Sound Analysis of Protocols using Bilinear Pairings}, year = 2010, month = nov, volume = 18, number = 6, pages = {999-1033}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KM-jcs09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KM-jcs09.pdf}, doi = {10.3233/JCS-2009-0388}, abstract = {In this paper, we introduce a symbolic model to analyse protocols that use a bilinear pairing between two cyclic groups. This model consists in an extension of the Abadi-Rogaway logic and we prove that the logic is still computationally sound: symbolic indistinguishability implies computational indistinguishability provided that the Bilinear Decisional Diffie-Hellman assumption holds and that the encryption scheme is \textsf{IND-CPA} secure. We~illustrate our results on classical protocols using bilinear pairing like Joux tripartite Diffie-Hellman protocol or the TAK-2 and TAK-3 protocols. We also investigate the security of a newly designed variant of the Burmester-Desmedt protocol using bilinear pairings. More precisely, we show for each of these protocols that the generated key is indistinguishable from a random element.} }

@article{DKR-jcs09, publisher = {{IOS} Press}, journal = {Journal of Computer Security}, author = {Delaune, St{\'e}phanie and Kremer, Steve and Ryan, Mark D.}, title = {Symbolic bisimulation for the applied pi~calculus}, year = 2010, month = mar, volume = 18, number = 2, pages = {317-377}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-jcs09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-jcs09.pdf}, doi = {10.3233/JCS-2010-0363}, abstract = {We propose a symbolic semantics for the finite applied pi~calculus. The~applied pi calculus is a variant of the pi~calculus with extensions for modelling cryptographic protocols. By~treating inputs symbolically, our semantics avoids potentially infinite branching of execution trees due to inputs from the environment. Correctness is maintained by associating with each process a set of constraints on terms. We~define a symbolic labelled bisimulation relation, which is shown to be sound but not complete with respect to standard bisimulation. We explore the lack of completeness and demonstrate that the symbolic bisimulation relation is sufficient for many practical examples. This~work is an important step towards automation of observational equivalence for the finite applied pi calculus, \textit{e.g.}~for verification of anonymity or strong secrecy properties.} }

@techreport{rr-lsv-10-23, author = {Bonnet, R{\'e}mi and Finkel, Alain and Haddad, Serge and Rosa{-}Velardo, Fernando}, title = {Comparing Petri Data Nets and Timed Petri Nets}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2010}, month = dec, type = {Research Report}, number = {LSV-10-23}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-23.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-23.pdf}, note = {16~pages}, abstract = {Well-Structured Transitions Systems (WSTS) constitute a generic class of infinite-state systems for which several properties like coverability remain decidable. The family of coverability languages that they generate is an appropriate criterium for measuring their expressiveness. Here we establish that Petri Data nets (PDNs) and Timed Petri nets (TdPNs), two powerful classes of WSTS are equivalent w.r.t this criterium.} }

@phdthesis{vacher-phd2010, author = {Vacher, Camille}, title = {Automates {\`a} contraintes globales pour la v{\'e}rification de propri{\'e}t{\'e}s de s{\'e}curit{\'e}}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2010, month = dec, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/vacher-phd.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/vacher-phd.pdf} }

@phdthesis{place-phd2010, author = {Place, {\relax Th}omas}, title = {Decidable Characterizations for Tree Logics}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2010, month = dec, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/place-phd.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/place-phd.pdf} }

@phdthesis{figueira-phd2010, author = {Figueira, Diego}, title = {On decidable automata on data words and data trees in relation to satisfiability of {LTL} and {XP}ath}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2010, month = dec, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/figueira-phd.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/figueira-phd.pdf} }

@phdthesis{andre-phd2010, author = {Andr{\'e}, {\'E}tienne}, title = {An Inverse Method for the Synthesis of Timing Parameters in Concurrent Systems}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2010, month = dec, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/andre-phd.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/andre-phd.pdf}, abstract = {This thesis proposes a novel approach for the synthesis of delays for timed systems. When verifying a real-time system, e.g., a hardware device or a communication protocol, it is important to check that not only the functional but also the timed behavior is correct. This correctness depends on the values of the delays of internal operations and of the environment.\par Formal verification methods guarantee the correctness of a timed system for a given set of delays, but do not give information for other values of the delays. Checking the correctness of for various values of those delays can be difficult and time consuming. It is thus interesting to consider that these delays are parameters. The problem then consists in synthesizing {"}good values{"} for those parameters, i.e., values for which the system is guaranteed to behave well.\par We are here interested in the synthesis of parameters in the framework of timed automata, a model for verifying real-time systems. Our approach relies on the following inverse method: given a reference valuation of the parameters, we synthesize a constraint on the parameters, guaranteeing the same time-abstract linear behavior as for the reference valuation. This gives a criterion of robustness to the system. By iterating this inverse method on various points of a bounded parameter domain, we are then able to partition the parametric space into good and bad zones, with respect to a given property one wants to verify. This gives a behavioral cartography of the system.\par This method extended to probabilistic systems allows to preserve minimum and maximum probabilities of reachability properties. We also present variants of the inverse method for directed weighted graphs and Markov Decision Processes. Several prototypes have been implemented; in particular, IMITATOR II implements the inverse method and the cartography for timed automata. It allowed us to synthesize parameter values for several case studies such as an abstract model of a memory circuit sold by the chipset manufacturer ST-Microelectronics, and various communication protocols. } }

@techreport{rr-lsv-10-22, author = {Soulat, Romain}, title = {On Properties of the Inverse Method: Commutation of Instanciation and Full Covering of the Behavioral Cartography}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2010}, month = dec, type = {Research Report}, number = {LSV-10-22}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-22.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-22.pdf}, note = {14~pages}, abstract = {When one performs an Inverse Method on a Parametric Timed Automata over an instance \(\pi_0\), one can instantiate some parameters at the very beginning of the analysis or at the end, with a restriction of the constraint \(K_0\) obtained in order to get a constraint over a subset of the parameters. In this report, we show that the results of either methods are the same. We present a theoretical proof and then an illustration of this property on the flip-flop example and the Root Contention protocol. We also present some results about the coverage of behavioral cartography and an illustration of the full covering on the SPSMALL memory.} }

@techreport{rr-lsv-10-21, author = {Andr{\'e}, {\'E}tienne}, title = {Synthesizing Parametric Constraints on Various Case Studies Using {IMITATOR}~{II}}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2010}, month = dec, type = {Research Report}, number = {LSV-10-21}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-21.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-21.pdf}, note = {66~pages}, abstract = {We present here various case studies analyzed using IMITATOR II, a tool implementing the {"}inverse method{"} in the framework of parametric timed automata: given a reference valuation of the parameters, it synthesizes a constraint such that the system behaves the same as under the reference valuation in terms of traces, i.e., alternating sequences of locations and actions.\par This is useful for safely relaxing some values of the reference valuation, and optimizing timing bounds of the system.\par Besides the inverse method, IMITATOR~II also implements the {"}behavioral cartography algorithm{"}, allowing to solve the following good parameters problem: find a set of valuations within a given rectangle for which the system behaves well.\par We present here a range of case studies, communication protocols, hardware circuits and industrial case studies for which constraints guaranteeing a good behavior were synthesized using IMITATOR~II.} }

@techreport{rr-lsv-10-20, author = {Andr{\'e}, {\'E}tienne}, title = {{IMITATOR}~{II} User Manual}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2010}, month = nov, type = {Research Report}, number = {LSV-10-20}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-20.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-20.pdf}, note = {31~pages}, abstract = {We present here the user manual of IMITATOR~II, a~tool implementing the {"}inverse method{"} in the framework of parametric timed automata: given a reference valuation of the parameters, its generates a constraint such that the system behaves the same as under the reference valuation in terms of traces, i.e., alternating sequences of locations and actions. This is useful for safely relaxing some values of the reference valuation, and optimizing timing bounds of the system.\par Besides the inverse method, IMITATOR II also implements the {"}behavioral cartography algorithm{"}, allowing to solve the following good parameters problem: find a set of valuations within a given rectangle for which the system behaves well.\par We give here the installation requirements and the launching commands of IMITATOR~II, as~well as the source code of a toy example.} }

@mastersthesis{rodriguez-master, author = {Rodr{\'\i}guez, C{\'e}sar}, title = {Implementation of a complete prefix unfolder for contextual nets}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2010}, month = sep, url = {http://www.lsv.fr/Publis/PAPERS/PDF/cr-m2.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/cr-m2.pdf} }

@inproceedings{hmy-bpsc10, address = {Leipzig, Germany}, month = sep # {-} # oct, year = 2010, volume = {177}, series = {Lecture Notes in Informatics}, publisher = {Gesellschaft f{\"u}r Informatik}, editor = {Abramowicz, Witold and Alt, Rainer and F{\"a}hnrich, Klaus-Peter and Franczyk, Bogdan and Maciaszek, Leszek A.}, acronym = {{ISSS}{\slash}{BPSC}'10}, booktitle = {{P}roceedings of the 2nd {I}nternational {S}ymposium on {S}ervices {S}cience and 3rd {I}nternational {C}onference on {B}usiness {P}rocess and {S}ervices {C}omputing ({ISSS}{\slash}{BPSC}'10)}, author = {Haddad, Serge and Mokdad, Lynda and Youcef, Samir}, title = {Selection of the Best composite Web Service Based on Quality of Service}, pages = {255-266}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/hmy-bpsc10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/hmy-bpsc10.pdf}, abstract = {The paper proposes a general framework to composite Web services selection based on multicriteria evaluation. The proposed framework extends the Web services architecture by adding, in the registry, a new Multicriteria Evaluation Component~(MEC) devoted to multicriteria evaluation. This additional component takes as input a set of composite Web services and a set of evaluation criteria and generates a set of recommended composite Web services. In~addition to the description of the conceptual architecture of the formwork, the paper also proposes solutions to construct and evaluate composite web services. In order to show the feasibility of the proposed architecture, we~have developed a prototype based on the open source jUDDI registry.} }

@mastersthesis{scerri-master, author = {Scerri, Guillaume}, title = {Mod{\'e}lisation des cl{\'e}s de l'intrus}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2010}, month = sep, nmnote = {Hubert prefere ne pas diffuser le rapport, et prepare une version 'conf'} }

@mastersthesis{bonnet-master, author = {Bonnet, R{\'e}mi}, title = {Well-structured {P}etri-nets extensions with data}, school = {{M}aster Computer Science, EPFL, Lausanne, Switzerland}, type = {Rapport de {M}aster}, year = {2010}, month = mar, url = {http://www.lsv.fr/Publis/PAPERS/PDF/bonnet-m2.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bonnet-m2.pdf} }

@article{LMT-tcs10, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {Lanotte, Ruggero and Maggiolo{-}Schettini, Andrea and Troina, Angelo}, title = {Weak bisimulation for Probabilistic Timed Automata?}, volume = 411, number = 50, year = 2010, month = nov, pages = {4291-4322}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LMT-tcs10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LMT-tcs10.pdf}, doi = {10.1016/j.tcs.2010.09.003}, abstract = {We are interested in describing timed systems that exhibit probabilistic behaviour. To this purpose, we consider a model of Probabilistic Timed Automata and introduce a concept of weak bisimulation for these automata, together with an algorithm to decide it. The weak bisimulation relation is shown to be preserved when either time, or probability is abstracted away. As an application, we use weak bisimulation for Probabilistic Timed Automata to model and analyze a timing attack on the dining cryptographers protocol.} }

@techreport{rr-lsv-10-17, author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge and Sassolas, Mathieu and Zeitoun, Marc}, title = {Distributed Synthesis with Incomparable Information}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2010}, month = oct, type = {Research Report}, number = {LSV-10-17}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-17.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-17.pdf}, note = {20~pages}, abstract = {Given (1)~an architecture defined by processes and communication channels between them or with the environment, and (2)~a~specification on the messages transmitted over the channels, distributed synthesis aims at deciding existence of local programs, one for each process, that together meet the specification, whatever the environment does. Recent work shows that this problem can be solved when a \emph{linear preorder} sorts the agents w.r.t. the information received from the environment.\par In this paper we show a new decidability result in the case where this preorder is broken by the addition of noisy agents embedded in a pipeline architecture. This case cannot be captured by the classical framework. Besides, this architecture makes it possible to model particular security threats, known as covert channels, where two users (the sender and the receiver) manage to communicate via a noisy protocol, and despite incomparable views over the environment.} }

@article{CDH-lmcs10, journal = {Logical Methods in Computer Science}, author = {Chatterjee, Krishnendu and Doyen, Laurent and Henzinger, {\relax Th}omas A.}, title = {Expressiveness and Closure Properties for Quantitative Languages}, volume = 6, number = {3:10}, nopages = {}, month = sep, year = 2010, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDH-lmcs10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDH-lmcs10.pdf}, ps = {CDH-lmcs10.ps}, doi = {10.2168/LMCS-6(3:10)2010}, abstract = {Weighted automata are nondeterministic automata with numerical weights on transitions. They can define quantitative languages~\(L\) that assign to each word~\(w\) a real number~\(L(w)\). In the case of infinite words, the value of a run is naturally computed as the maximum, limsup, liminf, limit-average, or discounted-sum of the transition weights. The value of a word \(w\) is the supremum of the values of the runs over \(w\). We study expressiveness and closure questions about these quantitative languages.\par We first show that the set of words with value greater than a threshold can be non-\(omega\)-regular for deterministic limit-average and discounted-sum automata, while this set is always \(omega\)-regular when the threshold is isolated (i.e., some neighborhood around the threshold contains no word). In the latter case, we prove that the \(omega\)-regular language is robust against small perturbations of the transition weights.\par We next consider automata with transition weights~\(0\) or \(1\) and show thatthey are as expressive as general weighted automata in the limit-average case, but not in the discounted-sum case.\par Third, for quantitative languages \(L_1\) and~\(L_2\), we consider the operations\(max(L_1,L_2)\), \(min(L_1,L_2)\), and \(1-L_1\), which generalize the booleanoperations on languages, as well as the sum \(L_1 + L_2\). We establish the closure properties of all classes of quantitative languages with respect to these four operations.} }

@inproceedings{CD-lpar10, address = {Yogyakarta, Indonesia}, month = oct, year = 2010, volume = {6397}, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, editor = {Fernm{\"u}ller, Chrisaitn G. and Voronkov, Andrei}, acronym = {{LPAR}'10}, booktitle = {{P}roceedings of the 17th {I}nternational {C}onference on {L}ogic for {P}rogramming, {A}rtificial {I}ntelligence, and {R}easoning ({LPAR}'10)}, author = {Chatterjee, Krishnendu and Doyen, Laurent}, title = {The Complexity of Partial-Observation Parity Games}, pages = {1-14}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-lpar10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-lpar10.pdf}, ps = {CD-lpar10.ps}, doi = {10.1007/978-3-642-16242-8_1}, abstract = {We consider two-player zero-sum games on graphs. On the basis of the information available to the players these games can be classified as follows: (a)~partial-observation (both players have partial view of the game); (b)~one-sided partial-observation (one player has partial-observation and the other player has complete-observation); and (c)~complete-observation (both players have complete view of the game). We survey the complexity results for the problem of deciding the winner in various classes of partial-observation games with \(\omega\)-regular winning conditions specified as parity objectives. We present a reduction from the class of parity objectives that depend on sequence of states of the game to the sub-class of parity objectives that only depend on the sequence of observations. We also establish that partial-observation acyclic games are PSPACE-complete.} }

@inproceedings{haar-wodes10, address = {Berlin, Germany}, month = aug # {-} # sep, year = 2010, publisher = {IFAC}, editor = {Raisch, J{\"o}rg and Giua, Alessandro and Lafortune, St{\'e}phane and Moor, Thomas}, acronym = {{WODES}'10}, booktitle = {{P}roceedings of the 10th {W}orkshop on {D}iscrete {E}vent {S}ystems ({WODES}'10)}, author = {Haar, Stefan}, title = {What Topology Tells us about Diagnosability in Partial Order Semantics}, pages = {221-226}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/SH-wodes10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SH-wodes10.pdf}, abstract = {From a partial observation of the behaviour of a labeled Discrete Event System, fault Diagnosis strives to determine whether or not a given {"}invisible{"} fault event has occurred. The diagnosability problem can be stated as follows: does the labeling allow for an outside observer to determine the occurrence of the fault, no later than a bounded number of events after that unobservable occurrence? In concurrent systems, partial order semantics adds to the difficulty of the problem, but also provides a richer and more complex picture of observation and diagnosis. In particular, it is crucial to clarify the intuitive notion of {"}time after fault occurrence{"}. To this end, we will use a unifying metric framework for event structures, providing a general topological description of diagnosability in both sequential and nonsequential semantics for Petri nets.} }

@inproceedings{AJRG-comnet10, address = {Tozeur, Tunisia}, month = nov, year = 2010, publisher = {{IEEE} Computer Society Press}, noeditor = {}, acronym = {{C}om{N}et'10}, booktitle = {{P}roceedings of the 2nd {I}nternational {C}onference on {C}ommunications and {N}etworking ({C}om{N}et'10)}, author = {Abassi, Ryma and Jacquemard, Florent and Rusinowitch, Micha{\"e}l and Guemara{ }El{~}Fatmi, Sihem}, title = {{XML} Access Control: from {XACML} to Annotated Schemas}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AJRG-comnet10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AJRG-comnet10.pdf}, doi = {10.1109/COMNET.2010.5699810}, abstract = {XML became the \textit{de facto} standard for the data representation and exchange on the internet. Regarding XML documents access control policy definition, OASIS ratified the XACML standard. It is a declarative language allowing the specification of authorizations as rules. Furthermore, it is common to formally represent XML documents as labeled trees and to handle secure requests through `user views'. A user view is the part of the document accessible to a given user according to the existing policy. Moreover, control access polices can be depicted as annotated rules where annotations define for each document node whether it is accessible. Hence, an annotated schema is a formal representation of `user views'.\par Our main contribution in this paper is then three folds. First, we compare XACML policies and annotated schemas. Second, we identify a significant fragment of XACML since this latter is very expressive and consequently complex. Third, we define adequate translation algorithms from XACML policies to annotated schemas.} }

@inproceedings{JR-ppdp10, address = {Hagenberg, Austria}, month = jul, year = 2010, publisher = {ACM Press}, editor = {Kutsia, Temur and Schreiner, Wolfgang and Fern{\'a}ndez, Maribel}, acronym = {{PPDP}'10}, booktitle = {{P}roceedings of the 12th {I}nternational {ACM} {SIGPLAN} {C}onference on {P}rinciples and {P}ractice of {D}eclarative {P}rogramming ({PPDP}'10)}, author = {Jacquemard, Florent and Rusinowitch, Micha{\"e}l}, title = {Rewrite-based verification of {XML} updates}, pages = {119-130}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/JR-ppdp10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JR-ppdp10.pdf}, doi = {10.1145/1836089.1836105}, abstract = {We propose a model for XML update primitives of the W3C XQuery Update Facility as parameterized rewriting rules of the form: {"}insert an unranked tree from a regular tree language~\(L\) as the first child of a node labeled by~\(a\){"}. For these rules, we give type inference algorithms, considering types defined by several classes of unranked tree automata. These type inference algorithms are directly applicable to XML static typechecking, which is the problem of verifying whether, a given document transformation always converts source documents of a given input type into documents of a given output type. We show that typechecking for arbitrary sequences of XML update primitives can be done in polynomial time when the unranked tree automaton defining the output type is deterministic and complete, and that it is EXPTIME-complete otherwise.\par We then apply the results to the verification of access control policies for XML updates. We propose in particular a polynomial time algorithm for the problem of local consistency of a policy, that is, for deciding the non-existence of a sequence of authorized update operations starting from a given document that simulates a forbidden update operation.} }

@article{NSV-tods10, publisher = {ACM Press}, journal = {ACM Transactions on Database Systems}, author = {Nash, Alan and Segoufin, Luc and Vianu, Victor}, title = {Views and queries: Determinacy and rewriting}, volume = 35, number = 3, month = jul, year = 2010, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/NSV-tods10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/NSV-tods10.pdf}, doi = {10.1145/1806907.1806913}, abstract = {We investigate the question of whether a query~\(Q\) can be answered using a set~\(\textbf{V}\) of views. We first define the problem in information-theoretic terms: we say that \(\textbf{V}\) determines~\(Q\) if \(\textbf{V}\)~provides enough information to uniquely determine the answer to~\(Q\). Next, we look at the problem of rewriting~\(Q\) in terms of~\(\textbf{V}\) using a specific language. Given a view language~\(\textbf{V}\) and query language~\(\mathcal{Q}\), we say that a rewriting language is complete for \(\mathcal{V}\)-to-\(\mathcal{Q}\) rewritings if every \(Q\in\mathcal{Q}\) can be rewritten in terms of \(\textbf{V}\in\mathcal{V}\) using a query in~\(\mathcal{R}\), whenever \(\textbf{V}\) determines~\(Q\). While query rewriting using views has been extensively investigated for some specific languages, the connection to the information-theoretic notion of determinacy, and the question of completeness of a rewriting language, have received little attention. In this paper we investigate systematically the notion of determinacy and its connection to rewriting. The results concern decidability of determinacy for various view and query languages, as well as the power required of complete rewriting languages. We consider languages ranging from first-order to conjunctive queries.} }

@inproceedings{KBBB-fmcad10, address = {Lugano, Switzerland}, month = oct, year = 2010, publisher = {{IEEE} Computer Society Press}, editor = {Bloem, Roderick and Sharygina, Natasha}, acronym = {{FMCAD}'10}, booktitle = {{P}roceedings of the 10th {I}nternational {C}onference on {F}ormal {M}ethods in {C}omputer {A}ided {D}esign ({FMCAD}'10)}, author = {K{\"u}hne, Ulrich and Beyer, Sven and Bormann, J{\"o}rg and Barstow, John}, title = {Automated Formal Verification of Processors Based on Architectural Models}, pages = {129-136}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/KBBB-fmcad10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KBBB-fmcad10.pdf}, abstract = {To keep up with the growing complexity of digital systems, high level models are used in the design process. In today's processor design, a comprehensive tool chain can be built automatically from architectural or transaction level models, but disregarding formal verification. We present an approach to automatically generate a complete property suite from an architecture description, that can be used to formally verify a register transfer level (RTL) implementation of a processor. The property suite is complete by construction, i.e. an exhaustive verification of all the functionality of the processor is ensured by the method. It allows for the efficient verification of single pipeline processors, including several advanced processor features like multicycle instructions. At the same time, the structured approach reduces the effort for verification significantly compared to a manual complete formal verification. The presented techniques have been implemented in the tool FISACo, which is demonstrated on an industrial processor.} }

@article{AHLNW-mscs10, publisher = {Cambridge University Press}, journal = {Mathematical Structures in Computer Science}, author = {Antonik, Adam and Huth, Michael and Larsen, Kim~G. and Nyman, Ulrik and W{\k{a}}sowski, Andrzej}, title = {Modal and mixed specifications: key decision problems and their complexities}, volume = 10, number = 1, month = feb, year = 2010, pages = {75-103}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AHLNW-mscs10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AHLNW-mscs10.pdf}, doi = {10.1017/S0960129509990260}, abstract = {Modal and mixed transition systems are specification formalisms that allow the mixing of over- and under-approximation. We discuss three fundamental decision problems for such specifications: \begin{itemize} \item whether a set of specifications has a common implementation; \item whether an individual specification has an implementation; and \item whether all implementations of an individual specification are implementations of another one. \end{itemize} For each of these decision problems we investigate the worst-case computational complexity for the modal and mixed cases. We show that the first decision problem is EXPTIME-complete for both modal and mixed specifications. We prove that the second decision problem is EXPTIME-complete for mixed specifications (it is known to be trivial for modal ones). The third decision problem is also shown to be EXPTIME-complete for mixed specifications.} }

@inproceedings{BGGLP-scan10, address = {Lyon, France}, month = sep, year = 2010, noeditor = {}, acronym = {SCAN'10}, booktitle = {{P}roceedings of the 14th {GAMM}-{IMACS} {I}nternational {S}ymposium on {S}cientific {C}omputing, {C}omputer {A}rithmetic and {V}alidated {N}umerics ({SCAN}'10)}, author = {Bouissou, Olivier and Goubault, {\'E}ric and Goubault{-}Larrecq, Jean and Putot, Sylvie}, title = {A Generalization of {P}-boxes to Affine Arithmetic, and Applications to Static Analysis of Programs}, nopages = {} }

@article{DR-lmcs10, journal = {Logical Methods in Computer Science}, author = {Demri, St{\'e}phane and Rabinovich, Alexander}, title = {The Complexity of Linear-time Temporal Logic over the Class of Ordinals}, volume = 6, number = 4, nopages = {}, month = dec, year = 2010, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DR-lmcs10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DR-lmcs10.pdf}, doi = {10.2168/LMCS-6(4:9)2010}, abstract = {We consider the temporal logic with since and until modalities. This temporal logic is expressively equivalent over the class of ordinals to first-order logic by Kamp's theorem. We show that it has a PSPACE-complete satisfiability problem over the class of ordinals. Among the consequences of our proof, we show that given the code of some countable ordinal~\(\alpha\) and a formula, we can decide in PSPACE whether the formula has a model over~\(\alpha\). In order to show these results, we introduce a class of simple ordinal automata, as expressive as B{\"u}chi ordinal automata. The PSPACE upper bound for the satisfiability problem of the temporal logic is obtained through a reduction to the nonemptiness problem for the simple ordinal automata.} }

@inproceedings{SD-jelia10, address = {Helsinki, Finland}, month = sep, year = 2010, volume = 6431, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, editor = {Niemel{\"a}, Ilkka and Janhunen, Tomi}, acronym = {{JELIA}'10}, booktitle = {{P}roceedings of the 12th {E}uropean {C}onference on {L}ogics in {A}rtificial {I}ntelligence ({JELIA}'10)}, author = {Demri, St{\'e}phane}, title = {Counter Systems for Data Logics}, pages = {10}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/SD-jelia10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SD-jelia10.pdf}, doi = {10.1007/978-3-642-15675-5_3}, abstract = {Data logics are logical formalisms that are used to specify properties on structures equipped with data (data words, data trees, runs from counter systems, timed words, etc.). In this survey talk, we shall see how satisfiability problems for such data logics are related to reachability problems for counter systems (including counter automata with errors, vector addition systems with states, etc.). This is the opportunity to provide an overview about the relationships between data logics and verification problems for counter systems.} }

@inproceedings{CSV-fsttcs10, address = {Chennai, India}, month = dec, year = 2010, volume = 8, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Lodaya, Kamal and Mahajan, Meena}, acronym = {{FSTTCS}'10}, booktitle = {{P}roceedings of the 30th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'10)}, author = {Chadha, Rohit and Sistla, A. Prasad and Viswanathan, Mahesh}, title = {Model Checking Concurrent Programs with Nondeterminism and Randomization}, pages = {364-375}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CSV-fsttcs10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CSV-fsttcs10.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2010.364}, abstract = {For concurrent probabilistic programs having process-level nondeterminism, it is often necessary to restrict the class of schedulers that resolve nondeterminism to obtain sound and precise model checking algorithms. In this paper, we introduce two classes of schedulers called \emph{view consistent} and \emph{locally Markovian} schedulers and consider the model checking problem of concurrent, probabilistic programs under these alternate semantics. Specifically, given a B{\"u}chi automaton~\(\textsf{Spec}\), a~threshold~\(x\in[0,1]\), and a concurrent program~\(\mathbb{P}\), the model checking problem asks if the measure of computations of~\(\mathbb{P}\) that satisfy~\(\textsf{Spec}\) is at least~\(x\), under all view consistent (or locally Markovian) schedulers. We give precise complexity results for the model checking problem (for different classes of B{\"u}chi automata specifications) and contrast it with the complexity under the standard semantics that considers all schedulers. } }

@inproceedings{AGMN-fsttcs10, address = {Chennai, India}, month = dec, year = 2010, volume = 8, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Lodaya, Kamal and Mahajan, Meena}, acronym = {{FSTTCS}'10}, booktitle = {{P}roceedings of the 30th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'10)}, author = {Akshay, S. and Gastin, Paul and Mukund, Madhavan and Narayan Kumar, K.}, title = {Model checking time-constrained scenario-based specifications}, pages = {204-215}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AGMN-fsttcs10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGMN-fsttcs10.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2010.204}, abstract = {We consider the problem of model checking message-passing systems with real-time requirements. As behavioural specifications, we use message sequence charts (MSCs) annotated with timing constraints. Our system model is a network of communicating finite state machines with local clocks, whose global behaviour can be regarded as a timed automaton. Our goal is to verify that all timed behaviours exhibited by the system conform to the timing constraints imposed by the specification. In general, this corresponds to checking inclusion for timed languages, which is an undecidable problem even for timed regular languages. However, we show that we can translate regular collections of time-constrained MSCs into a special class of event-clock automata that can be determinized and complemented, thus permitting an algorithmic solution to the model checking problem.} }

@inproceedings{CDHR-fsttcs10, address = {Chennai, India}, month = dec, year = 2010, volume = 8, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Lodaya, Kamal and Mahajan, Meena}, acronym = {{FSTTCS}'10}, booktitle = {{P}roceedings of the 30th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'10)}, author = {Chatterjee, Krishnendu and Doyen, Laurent and Henzinger, {\relax Th}omas A. and Raskin, Jean-Fran{\c{c}}ois}, title = {Generalized Mean-payoff and Energy Games}, pages = {505-516}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDHR-fsttcs10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDHR-fsttcs10.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2010.505} }

@inproceedings{BFLZ-fsttcs10, address = {Chennai, India}, month = dec, year = 2010, volume = 8, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Lodaya, Kamal and Mahajan, Meena}, acronym = {{FSTTCS}'10}, booktitle = {{P}roceedings of the 30th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'10)}, author = {Bonnet, R{\'e}mi and Finkel, Alain and Leroux, J{\'e}r{\^o}me and Zeitoun, Marc}, title = {Place-Boundedness for Vector Addition Systems with one zero-test}, pages = {192-203}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLZ-fsttcs10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLZ-fsttcs10.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2010.192}, abstract = {Reachability and boundedness problems have been shown decidable for Vector Addition Systems with one zero-test. Surprisingly, place-boundedness remained open. We provide here a variation of the Karp-Miller algorithm to compute a basis of the downward closure of the reachability set which allows to decide place-boundedness. This forward algorithm is able to pass the zero-tests thanks to a finer cover, hybrid between the reachability and cover sets, reclaiming accuracy on one component. We show that this filtered cover is still recursive, but that equality of two such filtered covers, even for usual Vector Addition Systems (with no zero-test), is undecidable.} }

@inproceedings{HBMOW-fsttcs10, address = {Chennai, India}, month = dec, year = 2010, volume = 8, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Lodaya, Kamal and Mahajan, Meena}, acronym = {{FSTTCS}'10}, booktitle = {{P}roceedings of the 30th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'10)}, author = {Hunter, Paul and Bouyer, Patricia and Markey, Nicolas and Ouaknine, Jo{\"e}l and Worrell, James}, title = {Computing rational radical sums in uniform \(\textsf{TC}^{0}\)}, pages = {308-316}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/HBMOW-fsttcs10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HBMOW-fsttcs10.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2010.308}, abstract = {A~fundamental problem in numerical computation and computational geometry is to determine the sign of arithmetic expressions in radicals. Here we consider the simpler problem of deciding whether \(\sum_{i=1}^m C_i \cdot A_i^{X_i}\) is zero for given rational numbers~\(A_i\), \(C_i\),~\(X_i\). It~has been known for almost twenty years that this can be decided in polynomial time. In this paper we improve this result by showing membership in uniform \(\textsf{TC}^0\). This requires several significant departures from Bl{\"o}mer's polynomial-time algorithm as the latter crucially relies on primitives, such as gcd computation and binary search, that are not known to be in~\(\textsf{TC}^0\).} }

@inproceedings{DLM-fsttcs10, address = {Chennai, India}, month = dec, year = 2010, volume = 8, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Lodaya, Kamal and Mahajan, Meena}, acronym = {{FSTTCS}'10}, booktitle = {{P}roceedings of the 30th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'10)}, author = {Da{~}Costa, Arnaud and Laroussinie, Fran{\c{c}}ois and Markey, Nicolas}, title = {{ATL} with strategy contexts: Expressiveness and Model Checking}, pages = {120-132}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DLM-fsttcs10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DLM-fsttcs10.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2010.120}, abstract = {We study the alternating-time temporal logics \(\textsf{ATL}\) and~\(\textsf{ATL}^{*}\) extended with strategy contexts: these make agents commit to their strategies during the evaluation of formulas, contrary to plain \(\textsf{ATL}\) and~\(\textsf{ATL}^{*}\) where strategy quantifiers reset previously selected strategies.\par We illustrate the important expressive power of strategy contexts by proving that they make the extended logics, namely \(\textsf{ATL}_{\textsf{sc}}\) and~\(\textsf{ATL}_{\textsf{sc}}^{*}\), equally expressive: any~formula in~\(\textsf{ATL}_{\textsf{sc}}^{*}\) can be translated into an equivalent, linear-size \(\textsf{ATL}_{\textsf{sc}}\) formula. Despite the high expressiveness of these logics, we prove that they remain decidable by designing a tree-automata-based algorithm for model-checking \(\textsf{ATL}_{\textsf{sc}}\) on the full class of \(n\)-player concurrent game structures.} }

@proceedings{MW-time2010, author = {Markey, Nicolas and Wijsen, Jef}, editor = {Markey, Nicolas and Wijsen, Jef}, title = {{P}roceedings of the 17th {I}nternational {S}ymposium on {T}emporal {R}epresentation and {R}easoning ({TIME}'10)}, booktitle = {{P}roceedings of the 17th {I}nternational {S}ymposium on {T}emporal {R}epresentation and {R}easoning ({TIME}'10)}, year = 2010, month = sep, publisher = {{IEEE} Computer Society Press}, address = {Paris, France}, url = {http://ieeexplore.ieee.org/xpl/tocresult.jsp?reload=true&isnumber=5601852}, doi = {10.1109/TIME.2010.4} }

@proceedings{GL-concur10, author = {Gastin, Paul and Laroussinie, Fran{\c{c}}ois}, editor = {Gastin, Paul and Laroussinie, Fran{\c{c}}ois}, title = {{P}roceedings of the 21st {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'10)}, booktitle = {{P}roceedings of the 21st {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'10)}, year = 2010, month = aug # {-} # sep, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {6269}, url = {http://www.springerlink.com/content/978-3-642-15374-7}, doi = {10.1007/978-3-642-15375-4} }

@inproceedings{FHL-express2010, address = {Paris, France}, month = aug, year = 2010, volume = 41, series = {Electronic Proceedings in Theoretical Computer Science}, editor = {Fr{\"o}schle, Sibylle and Valencia, Franck}, acronym = {{EXPRESS}'10}, booktitle = {{P}roceedings of the 17th {I}nternational {W}orkshop on {E}xpressiveness in {C}oncurrency ({EXPRESS}'10)}, author = {Figueira, Diego and Hofman, Piotr and Lasota, S{\l}awomir}, title = {Relating timed and register automata}, pages = {61-75}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FHL-express10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FHL-express10.pdf}, doi = {10.4204/EPTCS.41.5}, abstract = {Timed automata and register automata are well-known models of computation over timed and data words respectively. The former has clocks that allow to test the lapse of time between two events, whilst the latter includes registers that can store data values for later comparison. Although these two models behave in appearance differently, several decision problems have the same (un)decidability and complexity results for both models. As a prominent example, emptiness is decidable for alternating automata with one clock or register, both with non-primitive recursive complexity. This is not by chance.\par This work confirms that there is indeed a tight relationship between the two models. We show that a run of a timed automaton can be simulated by a register automaton, and conversely that a run of a register automaton can be simulated by a timed automaton. Our results allow to transfer complexity and decidability results back and forth between these two kinds of models. We justify the usefulness of these reductions by obtaining new results on register automata.} }

@inproceedings{DKRS-fast10, address = {Pisa, Italy}, month = sep, year = 2010, volume = 6561, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Degano, Pierpaolo and Etalle, Sandro and Guttman, Joshua}, acronym = {{FAST}'10}, booktitle = {{R}evised {S}elected {P}apers of the 7th {I}nternational {W}orkshop on {F}ormal {A}spects in {S}ecurity and {T}rust ({FAST}'10)}, author = {Delaune, St{\'e}phanie and Kremer, Steve and Ryan, Mark D. and Steel, Graham}, title = {A~Formal Analysis of Authentication in the {TPM}}, pages = {111-125}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DKRS-fast10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DKRS-fast10.pdf}, ps = {DKRS-fast10.ps}, doi = {10.1007/978-3-642-19751-2_8}, abstract = {The Trusted Platform Module~(TPM) is a hardware chip designed to enable computers to achieve a greater level of security than is possible in software alone. To this end, the TPM provides a way to store cryptographic keys and other sensitive data in its shielded memory. Through its API, one can use those keys to achieve some security goals. The TPM is a complex security component, whose specification consists of more than \(700\)~pages.\par We model a collection of four TPM commands, and we identify and formalise their security properties. Using the tool ProVerif, we rediscover some known attacks and some new variations on them. We propose modifications to the API and verify our properties for the modified API.} }

@inproceedings{DKRS-secco10, address = {Paris, France}, month = aug, year = 2010, editor = {Cortier, V{\'e}ronique and Chatzikokolakis, Kostas}, acronym = {{SecCo}'10}, booktitle = {{P}reliminary {P}roceedings of the 8th {I}nternational {W}orkshop on {S}ecurity {I}ssues in {C}oordination {M}odels, {L}anguages and {S}ystems ({SecCo}'10)}, author = {Delaune, St{\'e}phanie and Kremer, Steve and Ryan, Mark D. and Steel, Graham}, title = {A~Formal Analysis of Authentication in the~{TPM} (short paper)}, nopages = {}, nmnote = {did not appear in postproc. EPTCS 51}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DKRS-secco10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DKRS-secco10.pdf}, ps = {DKRS-secco10.ps} }

@article{bwa-jcs10, publisher = {{IOS} Press}, journal = {Journal of Computer Security}, author = {Baudet, Mathieu and Warinschi, Bogdan and Abadi, Mart{\'\i}n}, title = {Guessing Attacks and the Computational Soundness of Static Equivalence}, volume = 18, number = 5, pages = {909-968}, month = sep, year = 2010, url = {http://www.lsv.fr/Publis/PAPERS/PDF/bwa-jcs10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bwa-jcs10.pdf}, doi = {10.3233/JCS-2009-0386}, abstract = {The indistinguishability of two pieces of data (or two lists of pieces of data) can be represented formally in terms of a relation called static equivalence. Static equivalence depends on an underlying equational theory. The choice of an inappropriate equational theory can lead to overly pessimistic or overly optimistic notions of indistinguishability, and in turn to security criteria that require protection against impossible attacks or---worse yet---that ignore feasible ones. In this paper, we define and justify an equational theory for standard, fundamental cryptographic operations. This equational theory yields a notion of static equivalence that implies computational indistinguishability. Static equivalence remains liberal enough for use in applications. In particular, we develop and analyze a principled formal account of guessing attacks in terms of static equivalence.} }

@inproceedings{bgl-setop10, address = {Athens, Greece}, month = sep, year = 2010, volume = 6514, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Cavalli, Ana and Leneutre, Jean}, acronym = {{DPM}{{\slash}}{SETOP}'10}, booktitle = {{R}evised {S}elected {P}apers of the 5th {I}nternational {W}orkshop on {D}ata {P}rivacy {M}anagement and {A}utonomous {S}pontaneous {S}ecurity ({DPM}'10) and 3rd {I}nternational {W}orkshop on {A}utonomous and {S}pontaneous {S}ecurity ({SETOP}'10)}, author = {Benzina, Hedi and Goubault{-}Larrecq, Jean}, title = {Some Ideas on Virtualized Systems Security, and Monitors}, pages = {244-258}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/bgl-setop10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bgl-setop10.pdf}, doi = {10.1007/978-3-642-19348-4_18}, abstract = {Virtualized systems such as Xen, VirtualBox, VMWare or QEmu have been proposed to increase the level of security achievable on personal computers. On the other hand, such virtualized systems are now targets for attacks. We propose an intrusion detection architecture for virtualized systems, and discuss some of the security issues that arise. We argue that a weak spot of such systems is domain zero administration, which is left entirely under the administrator's responsibility, and is in particular vulnerable to trojans. To~avert some of the risks, we~propose to install a role-based access control model with possible role delegation, and to describe all undesired activity ows through simple temporal formulas. We show how the latter are compiled into Orchids rules, via a fragment of linear temporal logic, through a generalization of the so-called history variable mechanism.} }

@article{LV-dc10, publisher = {Springer}, journal = {Distributed Computing}, author = {Lozes, {\'E}tienne and Villard, Jules}, title = {A~spatial equational logic for the applied \(\pi\)-calculus}, pages = {61-83}, volume = 23, number = 1, year = 2010, month = sep, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LV-discomp10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LV-discomp10.pdf}, doi = {10.1007/s00446-010-0112-6}, abstract = {Spatial logics have been proposed to reason locally and modularly on algebraic models of distributed systems. In this paper we define the spatial equational logic \(\textsf{A}\pi\textsf{L}\) whose models are processes of the applied \(\pi\)-calculus. This extension of the \(\pi\)-calculus allows term manipulation and records communications as aliases in a frame, thus augmenting the predefined underlying equational theory. Our logic allows one to reason locally either on frames or on processes, thanks to static and dynamic spatial operators. We study the logical equivalences induced by various relevant fragments of \(\textsf{A}\pi\textsf{L}\), and show in particular that the whole logic induces a coarser equivalence than structural congruence. We give characteristic formulae for some of these equivalences and for static equivalence. Going further into the exploration of \(\textsf{A}\pi\textsf{L}\)'s expressivity, we also show that it can eliminate standard term quantification.} }

@inproceedings{andre-infinity2010, address = {Singapore}, month = sep, year = 2010, volume = 39, series = {Electronic Proceedings in Theoretical Computer Science}, editor = {Chen, Yu-Fang and Rezine, Ahmed}, acronym = {{INFINITY}'10}, booktitle = {{P}roceedings of the 12th {I}nternational {W}orkshops on {V}erification of {I}nfinite {S}tate {S}ystems ({INFINITY}'10)}, author = {Andr{\'e}, {\'E}tienne}, title = {{IMITATOR~II}: A~Tool for Solving the Good Parameters Problem in Timed Automata}, pages = {91-99}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/andre-infinity10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/andre-infinity10.pdf}, doi = {10.4204/EPTCS.39.7}, abstract = {We present here IMITATOR~II, a~new version of IMITATOR, a~tool implementing the {"}inverse method{"} for parametric timed automata: given a reference valuation of the parameters, it~synthesizes a constraint such that, for any valuation satisfying this constraint, the system behaves the same as under the reference valuation in terms of traces, \textit{i.e.}, alternating sequences of locations and actions.\par IMITATOR~II also implements the {"}behavioral cartography algorithm{"}, allowing us to solve the following good parameters problem: find a set of valuations within a given bounded parametric domain for which the system behaves well.\par We present new features and optimizations of the tool, and give results of applications to various examples of asynchronous circuits and communication protocols.} }

@inproceedings{demri-infinity2010, address = {Singapore}, month = sep, year = 2010, volume = 39, series = {Electronic Proceedings in Theoretical Computer Science}, editor = {Chen, Yu-Fang and Rezine, Ahmed}, acronym = {{INFINITY}'10}, booktitle = {{P}roceedings of the 12th {I}nternational {W}orkshops on {V}erification of {I}nfinite {S}tate {S}ystems ({INFINITY}'10)}, author = {Demri, St{\'e}phane}, title = {On Selective Unboundedness of~{VASS}}, pages = {1-15}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/demri-infinity10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/demri-infinity10.pdf}, doi = {10.4204/EPTCS.39.1}, abstract = {Numerous properties of vector addition systems with states amount to checking the (un)boundedness of some selective feature (\textit{e.g.}, number of reversals, run length). Some of these features can be checked in exponential space by using Rackoff's proof or its variants, combined with Savitch's theorem. However, the question is still open for many others, e.g., reversal-boundedness. In the paper, we introduce the class of generalized unboundedness properties that can be verified in exponential space by extending Rackoff's technique, sometimes in an unorthodox way. We obtain new optimal upper bounds, for example for place-boundedness problem, reversal-boundedness detection (several variants exist), strong promptness detection problem and regularity detection. Our analysis is sufficiently refined so as we also obtain a polynomial-space bound when the dimension is fixed.} }

@phdthesis{carre-phd2010, author = {Carr{\'e}, Jean-Loup}, title = {Analyse statique de programmes multi-thread pour l'embarqu{\'e}}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2010, month = jul, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/carre-these10.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/carre-these10.pdf} }

@phdthesis{akshay-phd2010, author = {Akshay, S.}, title = {Sp{\'e}cification et v{\'e}rification pour des syst{\`e}mes distribu{\'e}s et temporis{\'e}s}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2010, month = jul, url = {http://www.lsv.fr/Publis/PAPERS/PDF/akshay-phd.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/akshay-phd.pdf} }

@inproceedings{BDF-nsmc10, address = {Williamsburg, Virginia, USA}, month = sep, year = 2010, editor = {Benzi, Michele and Dayar, Tugrul}, acronym = {{NSMC}'10}, booktitle = {{P}roceedings of the 6th {I}nternational {M}eeting on the {N}umerical {S}olution of {M}arkov {C}hain ({NSMC}'10)}, author = {Bu\v{s}i\'{c}, Ana and Djafri, Hilal and Fourneau, Jean-Michel}, title = {Stochastic Bounds for Censored {M}arkov Chains}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDF-nsmc10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDF-nsmc10.pdf}, abstract = {Censored Markov chains~(CMC) allow to represent the conditional behavior of a system within a subset of observed states. They provide a theoretical framework to study the truncation of a discrete-time Markov chain when the generation of the state-space is too hard or when the number of states is too large. But the stochastic matrix of a CMC may be difficult to obtain. Dayar \textit{et~al.}~(2006) have proposed an algorithm, called DPY, that computes a stochastic bounding matrix for a CMC with a smaller complexity with only a partial knowledge of the chain. We prove that this algorithm is optimal for the information they take into account. We also show how some additional knowledge on the chain can improve stochastic bounds for~CMC.} }

@inproceedings{BCFS-ccs10, address = {Chicago, Illinois, USA}, month = oct, year = 2010, publisher = {ACM Press}, acronym = {{CCS}'10}, booktitle = {{P}roceedings of the 17th {ACM} {C}onference on {C}omputer and {C}ommunications {S}ecurity ({CCS}'10)}, author = {Bortolozzo, Matteo and Centenaro, Matteo and Focardi, Riccardo and Steel, Graham}, title = {Attacking and Fixing {PKCS}\#11 Security Tokens}, pages = {260-269}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCFS-ccs10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCFS-ccs10.pdf}, doi = {10.1145/1866307.1866337}, abstract = {We show how to extract sensitive cryptographic keys from a variety of commercially available tamper resistant cryptographic security tokens, exploiting vulnerabilities in their RSA PKCS\#11 based APIs. The attacks are performed by Tookan, an automated tool we have developed, which reverse-engineers the particular token in use to deduce its functionality, constructs a model of its API for a model checker, and then executes any attack trace found by the model checker directly on the token. We describe the operation of Tookan and give results of testing the tool on 17 commercially available tokens: 9~were vulnerable to attack, while the other 8 had severely restricted functionality. One of the attacks found by the model checker has not previously appeared in the literature. We show how Tookan may be used to verify patches to insecure devices, and give a secure configuration that we have implemented in a patch to a software token simulator. This is the first such configuration to appear in the literature that does not require any new cryptographic mechanisms to be added to the standard. We comment on lessons for future key management APIs.} }

@article{BJLMO-jwcn10, publisher = {Hindawi Publishing Corp.}, journal = {EURASIP Journal on Wireless Communications and Networking}, author = {Brihaye, {\relax Th}omas and Jungers, Marc and Lasaulce, Samson and Markey, Nicolas and Oreiby, Ghassan}, title = {Using Model Checking for Analyzing Distributed Power Control Problems}, year = 2010, volume = {2010}, number = {861472}, nopages = {}, month = jun, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BJLMO-jwcn10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BJLMO-jwcn10.pdf}, doi = {10.1155/2010/861472}, abstract = {Model checking~(MC) is a formal verification technique which has been known and still knows a resounding success in the computer science community. Realizing that the distributed power control~(PC) problem can be modeled by a timed game between a given transmitter and its environment, the authors wanted to know whether this approach can be applied to distributed~PC. It~turns out that it can be applied successfully and allows one to analyze realistic scenarios including the case of discrete transmit powers and games with incomplete information. The proposed methodology is as follows. We state some objectives a transmitter-receiver pair would like to reach. The network is modeled by a game where transmitters are considered as timed automata interacting with each other. The objectives are then translated into timed alternating-time temporal logic formulae and MC is exploited to know whether the desired properties are verified and determine a winning strategy.} }

@article{CKW-jar2010, publisher = {Springer}, journal = {Journal of Automated Reasoning}, author = {Cortier, V{\'e}ronique and Kremer, Steve and Warinschi, Bogdan}, title = {A~Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems}, year = 2010, month = apr, pages = {225-259}, number = {3-4}, volume = {46}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CKW-jar10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CKW-jar10.pdf}, doi = {10.1007/s10817-010-9187-9}, abstract = {Since the 1980s, two approaches have been developed for analyzing security protocols. One of the approaches relies on a computational model that considers issues of complexity and probability. This approach captures a strong notion of security, guaranteed against all probabilistic polynomial-time attacks. The other approach relies on a symbolic model of protocol executions in which cryptographic primitives are treated as black boxes. Since the seminal work of Dolev and Yao, it has been realized that this latter approach enables significantly simpler and often automated proofs. However, the guarantees that it offers with respect to the more detailed computational models have been quite unclear.\par For more than twenty years the two approaches have coexisted but evolved mostly independently. Recently, significant research efforts attempt to develop paradigms for cryptographic systems analysis that combines the best of both worlds. There are two broad directions that have been followed. Computational soundness aims to establish sufficient conditions under which results obtained using symbolic models imply security under computational models. The direct approach aims to apply the principles and the techniques developed in the context of symbolic models directly to computational ones.\par In this paper we survey existing results along both of these directions. Our goal is to provide a rather complete summary that could act as a quick reference for researchers who want to contribute to the field, want to make use of existing results, or just want to get a better picture of what results already exist.} }

@inproceedings{KRS-esorics10, address = {Athens, Greece}, month = sep, year = 2010, volume = {6345}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Gritzalis, Dimitris and Preneel, Bart}, acronym = {{ESORICS}'10}, booktitle = {{P}roceedings of the 15th {E}uropean {S}ymposium on {R}esearch in {C}omputer {S}ecurity ({ESORICS}'10)}, author = {Kremer, Steve and Ryan, Mark D. and Smyth, Ben}, title = {Election verifiability in electronic voting protocols}, pages = {389-404}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/KRS-esorics10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KRS-esorics10.pdf}, doi = {10.1007/978-3-642-15497-3_24}, abstract = {We present a formal, symbolic definition of election verifiability for electronic voting protocols in the context of the applied pi calculus. Our definition is given in terms of boolean tests which can be performed on the data produced by an election. The definition distinguishes three aspects of verifiability: individual, universal and eligibility verifiability. It also allows us to determine precisely which aspects of the system's hardware and software must be trusted for the purpose of election verifiability. In contrast with earlier work our definition is compatible with a large class of electronic voting schemes, including those based on blind signatures, homomorphic encryption and mixnets. We demonstrate the applicability of our formalism by analysing three protocols: FOO, Helios~2.0, and Civitas (the latter two have been deployed).} }

@inproceedings{DDS-esorics10, address = {Athens, Greece}, month = sep, year = 2010, volume = {6345}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Gritzalis, Dimitris and Preneel, Bart}, acronym = {{ESORICS}'10}, booktitle = {{P}roceedings of the 15th {E}uropean {S}ymposium on {R}esearch in {C}omputer {S}ecurity ({ESORICS}'10)}, author = {Dahl, Morten and Delaune, St{\'e}phanie and Steel, Graham}, title = {Formal Analysis of Privacy for Vehicular Mix-Zones}, pages = {55-70}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-esorics10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-esorics10.pdf}, ps = {DDS-esorics10.ps}, doi = {10.1007/978-3-642-15497-3_4}, abstract = {Safety critical applications for recently proposed vehicle to vehicle ad-hoc networks~(VANETs) rely on a beacon signal, which poses a threat to privacy since it could allow a vehicle to be tracked. Mix-zones, where vehicles encrypt their transmissions and then change their identifiers, have been proposed as a solution to this problem. \par In this work, we~describe a formal analysis of mix-zones. We~model a mix-zone and propose a formal definition of privacy for such a zone. We~give a set of necessary conditions for any mix-zone protocol to preserve privacy. We~analyse, using the tool ProVerif, a~particular proposal for key distribution in mix-zones, the CMIX protocol. We~report attacks on privacy and we propose a fix.} }

@inproceedings{phs-rp10, address = {Brno, Czech Republic}, month = aug, year = 2010, volume = 6227, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Ku{\v c}era, Anton{\'\i}n and Potapov, Igor}, acronym = {{RP}'10}, booktitle = {{P}roceedings of the 4th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'10)}, author = {Schnoebelen, {\relax Ph}ilippe}, title = {Lossy Counter Machines Decidability Cheat Sheet}, pages = {51-75}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/phs-rp10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/phs-rp10.pdf}, doi = {10.1007/978-3-642-15349-5_4}, abstract = {Lossy counter machines (LCM's) are a variant of Minsky counter machines based on weak (or~unreliable) counters in the sense that they can decrease nondeterministically and without notification. This model, introduced by R.~Mayr [TCS~297:337-354 (2003)], is not yet very well known, even though it has already proven useful for establishing hardness results.\par In this paper we survey the basic theory of LCM's and their verification problems, with a focus on the decidability/undecidability divide. } }

@inproceedings{AF-rp10, address = {Brno, Czech Republic}, month = aug, year = 2010, volume = 6227, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Ku{\v c}era, Anton{\'\i}n and Potapov, Igor}, acronym = {{RP}'10}, booktitle = {{P}roceedings of the 4th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'10)}, author = {Andr{\'e}, {\'E}tienne and Fribourg, Laurent}, title = {Behavioral Cartography of Timed Automata}, pages = {76-90}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AF-rp10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AF-rp10.pdf}, doi = {10.1007/978-3-642-15349-5_5}, abstract = {We aim at finding a set of timing parameters for which a given timed automaton has a {"}good{"} behavior. We~present here a novel approach based on the decomposition of the parametric space into behavioral tiles, \textit{i.e.}, sets of parameter valuations for which the behavior of the system is uniform. This gives us a behavioral cartography according to the values of the parameters.\par It is then straightforward to partition the space into a {"}good{"} and a {"}bad{"} subspace, according to the behavior of the tiles. We extend this method to probabilistic systems, allowing to decompose the parametric space into tiles for which the minimal (resp. maximal) probability of reaching a given location is uniform. An~implementation has been made, and experiments successfully conducted.} }

@inproceedings{CJ-notere10, address = {Tozeur, Tunisia}, month = may # {-} # jun, year = 2010, publisher = {{IEEE} Computer Society Press}, noeditor = {}, acronym = {{NOTERE}'10}, booktitle = {{A}ctes de la 10{\`e}me {C}onf{\'e}rence {I}nternationale sur les {NO}uvelles {TE}chnologies de la {R\'E}partition ({NOTERE}'10)}, author = {Chatain, {\relax Th}omas and Jard, Claude}, title = {S{\'e}mantique concurrente symbolique des r{\'e}seaux de {P}etri saufs et d{\'e}pliages finis des r{\'e}seaux temporels}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CJ-notere10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CJ-notere10.pdf}, abstract = {On consid\`ere des r\'eseaux de Petri color\'es, \`a contraintes lin\'eaires et pouvant poss\'eder des arcs de lecture. Sur cette classe, on d\'efinit une s\'emantique concurrente en termes de processus d'ordre partiel permettant de garder explicite l'ind\'ependance entre des tirs de transitions. L'ensemble des processus peut \^etre repr\'esent\'e en utilisant la notion de d\'epliage symbolique. Nous montrons alors comment les r\'eseaux de Petri temporels peuvent \^etre cod\'es dans ce mod\`ele \`a l'aide d'une transformation syntaxique pr\'eservant la concurrence. Cette transformation permet de d\'efinir la notion de d\'epliage de r\'eseaux de Petri temporels et d'en donner une repr\'esentation par pr\'efixe fini.} }

@inproceedings{DHLN-acsd10, address = {Braga, Portugal}, month = jun, year = 2010, publisher = {{IEEE} Computer Society Press}, editor = {Gomes, Lu{\'\i}s and Khomenko, Victor}, acronym = {{ACSD}'10}, booktitle = {{P}roceedings of the 10th {I}nternational {C}onference on {A}pplication of {C}oncurrency to {S}ystem {D}esign ({ACSD}'10)}, author = {Doyen, Laurent and Henzinger, {\relax Th}omas A. and Legay, Axel and Nickovic, Dejan}, title = {Robustness of Sequential Circuits}, pages = {77-84}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DHLN-acsd10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DHLN-acsd10.pdf}, doi = {10.1109/ACSD.2010.26}, abstract = {Digital components play a central role in the design of complex embedded systems. These components are interconnected with other, possibly analog, devices and the physical environment. This environment cannot be entirely captured and can provide inaccurate input data to the component. It~is thus important for digital components to have a robust behavior, \textit{i.e.},~the presence of a small change in the input sequences should not result in a drastic change in the output sequences.\par In this paper, we study a notion of robustness for sequential circuits. However, since sequential circuits may have parts that are naturally discontinuous (\textit{e.g.},~digital controllers with switching behavior), we~need a flexible framework that accommodates this fact and leaves discontinuous parts of the circuit out from the robustness analysis. As a consequence, we~consider sequential circuits that have their input variables partitioned into two disjoint sets: control and disturbance variables. Our contributions are (1)~a~definition of robustness for sequential circuits as a form of continuity with respect to disturbance variables, (2)~the~characterization of the exact class of sequential circuits that are robust according to our definition, (3)~an~algorithm to decide whether a sequential circuit is robust or~not.} }

@inproceedings{DDGRT-csl10, address = {Brno, Czech Republic}, month = aug, year = 2010, volume = {6247}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Dawar, Anuj and Veith, Helmut}, acronym = {{CSL}'10}, booktitle = {{P}roceedings of the 19th {A}nnual {EACSL} {C}onference on {C}omputer {S}cience {L}ogic ({CSL}'10)}, author = {Degorre, Aldric and Doyen, Laurent and Gentilini, Raffaella and Raskin, Jean-Fran{\c{c}}ois and Toru{\'n}czyk, Szymon}, title = {Energy and Mean-Payoff Games with Imperfect Information}, pages = {260-274}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DDGRT-csl10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDGRT-csl10.pdf}, doi = {10.1007/978-3-642-15205-4_22}, abstract = {We consider two-player games with imperfect information and quantitative objective. The game is played on a weighted graph with a state space partitioned into classes of indistinguishable states, giving players partial knowledge of the state. In an energy game, the weights represent resource consumption and the objective of the game is to maintain the sum of weights always nonnegative. In a mean-payoff game, the objective is to optimize the limit-average usage of the resource. We show that the problem of determining if an energy game with imperfect information with fixed initial credit has a winning strategy is decidable, while the question of the existence of some initial credit such that the game has a winning strategy is undecidable. This undecidability result carries over to mean-payoff games with imperfect information. On the positive side, using a simple restriction on the game graph (namely, that the weights are visible), we show that these problems become EXPTIME-complete.} }

@inproceedings{PhS-mfcs10, address = {Brno, Czech Republic}, month = aug, year = 2010, volume = 6281, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Hlin{\v e}n{\'y}, Petr and Ku{\v c}era, Anton{\'\i}n}, acronym = {{MFCS}'10}, booktitle = {{P}roceedings of the 35th {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'10)}, author = {Schnoebelen, {\relax Ph}ilippe}, title = {Revisiting {A}ckermann-Hardness for Lossy Counter Machines and Reset {P}etri Nets}, pages = {616-628}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/phs-mfcs10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/phs-mfcs10.pdf}, doi = {10.1007/978-3-642-15155-2_54}, abstract = {We prove that coverability and termination are not primitive-recursive for lossy counter machines and for Reset Petri nets.} }

@inproceedings{CDGH-mfcs10, address = {Brno, Czech Republic}, month = aug, year = 2010, volume = 6281, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Hlin{\v e}n{\'y}, Petr and Ku{\v c}era, Anton{\'\i}n}, acronym = {{MFCS}'10}, booktitle = {{P}roceedings of the 35th {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'10)}, author = {Chatterjee, Krishnendu and Doyen, Laurent and Gimbert, Hugo and Henzinger, {\relax Th}omas A.}, title = {Randomness for Free}, pages = {246-257}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDGH-mfcs10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDGH-mfcs10.pdf}, doi = {10.1007/978-3-642-15155-2_23}, abstract = {We consider two-player zero-sum games on graphs. These games can be classified on the basis of the information of the players and on the mode of interaction between them. On the basis of information the classification is as follows: (a)~partial-observation (both players have partial view of the game); (b)~one-sided complete-observation (one player has complete observation); and (c)~complete-observation (both players have complete view of the game). On~the basis of mode of interaction we have the following classification: (a)~concurrent (players interact simultaneously); and (b)~turn-based (players interact in turn). The~two sources of randomness in these games are randomness in transition function and randomness in strategies. In general, randomized strategies are more powerful than deterministic strategies, and randomness in transitions gives more general classes of games. We~present a complete characterization for the classes of games where randomness is not helpful~in: (a)~the~transition function (probabilistic transition can be simulated by deterministic transition); and (b)~strategies (pure strategies are as powerful as randomized strategies). As~consequence of our characterization we obtain new undecidability results for these games.} }

@inproceedings{FP-mfcs10, address = {Brno, Czech Republic}, month = aug, year = 2010, volume = 6281, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Hlin{\v e}n{\'y}, Petr and Ku{\v c}era, Anton{\'\i}n}, acronym = {{MFCS}'10}, booktitle = {{P}roceedings of the 35th {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'10)}, author = {Fontaine, Ga{\"e}lle and Place, {\relax Th}omas}, title = {Classes of trees definable in the {{\(\mu\)}}-calculus}, pages = {381-392}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FP-mfcs10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FP-mfcs10.pdf}, doi = {10.1007/978-3-642-15155-2_34}, abstract = {We are interested in frame definability of classes of trees, using formulas of the \(\mu\)-calculus. In this set up, the proposition letters (or in other words, the free variables) in the \(\mu\)-formulas correspond to second order variables over which universally quantify. Our main result is a semantic characterization of the \textbf{MSO} definable classes of trees that are definable by a \(\mu\)-formula. We~also show that it is decidable whether a given \textbf{MSO} formula corresponds to a \(\mu\)-formula, in the sense that they define the same class of trees.} }

@inproceedings{CDH-mfcs10, address = {Brno, Czech Republic}, month = aug, year = 2010, volume = 6281, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Hlin{\v e}n{\'y}, Petr and Ku{\v c}era, Anton{\'\i}n}, acronym = {{MFCS}'10}, booktitle = {{P}roceedings of the 35th {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'10)}, author = {Chatterjee, Krishnendu and Doyen, Laurent and Henzinger, {\relax Th}omas A.}, title = {Qualitative Analysis of Partially-observable {M}arkov Decision Processes}, pages = {258-269}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDH-mfcs10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDH-mfcs10.pdf}, doi = {10.1007/978-3-642-15155-2_24}, abstract = {We study observation-based strategies for partially-observable Markov decision processes (POMDPs) with parity objectives. An~observation-based strategy relies on partial information about the history of a play, namely, on the past sequence of observations. We~consider qualitative analysis problems: given a POMDP with a parity objective, decide whether there exists an observation-based strategy to achieve the objective with probability~\(1\) (almost-sure winning), or with positive probability (positive winning). Our main results are twofold. First, we present a complete picture of the computational complexity of the qualitative analysis problem for POMDPs with parity objectives and its subclasses: safety, reachability, B{\"u}chi, and coB{\"u}chi objectives. We~establish several upper and lower bounds that were not known in the literature. Second, we give optimal bounds (matching upper and lower bounds) for the memory required by pure and randomized observation-based strategies for each class of objectives.} }

@inproceedings{OU-mfcs10, address = {Brno, Czech Republic}, month = aug, year = 2010, volume = 6281, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Hlin{\v e}n{\'y}, Petr and Ku{\v c}era, Anton{\'\i}n}, acronym = {{MFCS}'10}, booktitle = {{P}roceedings of the 35th {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'10)}, author = {Olschewski, J{\"o}rg and Ummels, Michael}, title = {The Complexity of Finding Reset Words in Finite Automata}, pages = {568-579}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/OU-mfcs10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/OU-mfcs10.pdf}, doi = {10.1007/978-3-642-15155-2_50}, abstract = {We study several problems related to finding reset words in deterministic finite automata. In~particular, we~establish that the problem of deciding whether a shortest reset word has length~\(k\) is complete for the complexity class~\(DP\). This result answers a question posed by Volkov. For the search problems of finding a shortest reset word and the length of a shortest reset word, we establish membership in the complexity classes FP\textsuperscript{NP} and FP\textsuperscript{NP[log]}, respectively. Moreover, we show that both these problems are hard for FP\textsuperscript{NP[log]}. Finally, we~observe that computing a reset word of a given length is FNP-complete.} }

@inproceedings{EHH-apnoc10, address = {Braga, Portugal}, month = jun, year = 2010, editor = {Sidorova, Natalia and Serebrenik, Alexander}, acronym = {{APNOC}'10}, booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop on {A}bstractions for {P}etri {N}ets and {O}ther {M}odels of {C}oncurrency ({APNOC}'10)}, author = {El{~}Hog{-}Benzina, Dorsaf and Haddad, Serge and Hennicker, Rolf}, title = {Process Refinement and Asynchronous Composition with Modalities}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/EHH-apnoc10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/EHH-apnoc10.pdf}, abstract = {We propose a framework for the specification of infinite state systems based on Petri nets with distinguished may- and must-transitions (called modalities) which specify the allowed and the required behavior of refinements and hence of implementations. Formally, refinements are defined by relating the modal language specifications generated by two modal Petri nets according to the refinement relation for modal language specifications. We show that this refinement relation is decidable if the underlying modal Petri nets are weakly deterministic. We also show that the membership problem for the class of weakly deterministic modal Petri nets is decidable. As an important application of our approach we consider I/O-Petri nets which are obtained by asynchronous composition and thus exhibit inherently an infinite behavior.} }

@inproceedings{CDEHR-concur10, address = {Paris, France}, month = aug # {-} # sep, year = 2010, volume = {6269}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Gastin, Paul and Laroussinie, Fran{\c{c}}ois}, acronym = {{CONCUR}'10}, booktitle = {{P}roceedings of the 21st {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'10)}, author = {Chatterjee, Krishnendu and Doyen, Laurent and Edelsbrunner, Herbert and Henzinger, {\relax Th}omas A. and Rannou, Philippe}, title = {Mean-Payoff Automaton Expressions}, pages = {269-283}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDEHR-concur10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDEHR-concur10.pdf}, doi = {10.1007/978-3-642-15375-4_19}, abstract = {Quantitative languages are an extension of boolean languages that assign to each word a real number. Mean-payoff automata are finite automata with numerical weights on transitions that assign to each infinite path the long-run average of the transition weights. When the mode of branching of the automaton is deterministic, nondeterministic, or alternating, the corresponding class of quantitative languages is not robust as it is not closed under the pointwise operations of max, min, sum, and numerical complement. Nondeterministic and alternating mean-payoff automata are not decidable either, as the quantitative generalization of the problems of universality and language inclusion is undecidable. We introduce a new class of quantitative languages, defined by mean-payoff automaton expressions, which is robust and decidable: it is closed under the four pointwise operations, and we show that all decision problems are decidable for this class. Mean-payoff automaton expressions subsume deterministic mean-payoff automata, and we show that they have expressive power incomparable to nondeterministic and alternating mean-payoff automata. We also present for the first time an algorithm to compute distance between two quantitative languages, and in our case the quantitative languages are given as mean-payoff automaton expressions.} }

@inproceedings{BBM-concur10, address = {Paris, France}, month = aug # {-} # sep, year = 2010, volume = {6269}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Gastin, Paul and Laroussinie, Fran{\c{c}}ois}, acronym = {{CONCUR}'10}, booktitle = {{P}roceedings of the 21st {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'10)}, author = {Bouyer, Patricia and Brenguier, Romain and Markey, Nicolas}, title = {{N}ash Equilibria for Reachability Objectives in Multi-player Timed Games}, pages = {192-206}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBM-concur10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBM-concur10.pdf}, doi = {10.1007/978-3-642-15375-4_14}, abstract = {We propose a procedure for computing Nash equilibria in multi-player timed games with reachability objectives. Our procedure is based on the construction of a finite concurrent game, and on a generic characterization of Nash equilibria in (possibly infinite) concurrent games. Along the way, we~use our characterization to compute Nash equilibria in finite concurrent games.} }

@inproceedings{BBM-formats10, address = {Vienna, Austria}, month = sep, year = 2010, volume = {6246}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Chatterjee, Krishnendu and Henziner, Thomas A.}, acronym = {{FORMATS}'10}, booktitle = {{P}roceedings of the 8th {I}nternational {C}onference on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'10)}, author = {Bouyer, Patricia and Brenguier, Romain and Markey, Nicolas}, title = {Computing Equilibria in Two-Player Timed Games {\textit{via}}~Turn-Based Finite Games}, pages = {62-76}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBM-formats10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBM-formats10.pdf}, doi = {10.1007/978-3-642-15297-9_7}, abstract = {We study two-player timed games where the objectives of the two players are not opposite. We focus on the standard notion of Nash equilibrium and propose a series of transformations that builds two finite turn-based games out of a timed game, with a precise correspondence between Nash equilibria in the original and in final games. This provides us with an algorithm to compute Nash equilibria in two-player timed games for large classes of properties.} }

@inproceedings{BCH-time10, address = {Paris, France}, month = sep, year = 2010, publisher = {{IEEE} Computer Society Press}, editor = {Markey, Nicolas and Wijsen, Jef}, acronym = {{TIME}'10}, booktitle = {{P}roceedings of the 17th {I}nternational {S}ymposium on {T}emporal {R}epresentation and {R}easoning ({TIME}'10)}, author = {Balaguer, Sandie and Chatain, {\relax Th}omas and Haar, Stefan}, title = {A~Concurrency-Preserving Translation from Time {P}etri Nets to Networks of Timed Automata}, pages = {77-84}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCH-time10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCH-time10.pdf}, doi = {10.1109/TIME.2010.12}, abstract = {Real-time distributed systems may be modeled in different formalisms such as time Petri nets~(TPN) and networks of timed automata~(NTA). This paper focuses on translating a \(1\)-bounded TPN into an NTA and considers an equivalence which takes the distribution of actions into account. This translation is extensible to bounded~TPNs. We~first use \(S\)-invariants to decompose the net into components that give the structure of the automata, then we add clocks to provide the timing information. Although we have to use an extended syntax in the timed automata, this is a novel approach since the other transformations and comparisons of these models did not consider the preservation of concurrency.} }

@inproceedings{BHS-time10, address = {Paris, France}, month = sep, year = 2010, publisher = {{IEEE} Computer Society Press}, editor = {Markey, Nicolas and Wijsen, Jef}, acronym = {{TIME}'10}, booktitle = {{P}roceedings of the 17th {I}nternational {S}ymposium on {T}emporal {R}epresentation and {R}easoning ({TIME}'10)}, author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge and Sassolas, Mathieu}, title = {Real Time Properties for Interrupt Timed Automata}, pages = {69-76}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHS-time10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHS-time10.pdf}, doi = {10.1109/TIME.2010.11}, abstract = {Interrupt Timed Automata (ITA) have been introduced to model multi-task systems with interruptions. They form a~subclass of stopwatch automata, where the real valued variables (with rate \(0\) or~\(1\)) are organized along priority levels. While reachability is undecidable with usual stopwatches, the problem was proved decidable for~ITA. In~this work, after giving answers to some questions left open about expressiveness, closure, and complexity for~ITA, our~main purpose is to investigate the verification of real time properties over~ITA. While we prove that model checking a variant of the timed logic TCTL is undecidable, we nevertheless give model checking procedures for two relevant fragments of this logic: one where formulas contain only model clocks and another one where formulas have a single external clock.} }

@inproceedings{HMY-iscc10, address = {Riccione, Italy}, month = jun, year = 2010, publisher = {{IEEE} Computer Society Press}, noeditor = {}, acronym = {{ISCC}'10}, booktitle = {{P}roceedings of the 15th {IEEE} {S}ymposium on {C}omputers and {C}ommunications ({ISCC}'10)}, author = {Haddad, Serge and Mokdad, Lynda and Youcef, Samir}, title = {Response time of {BPEL4WS} constructors}, pages = {695-700}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/HMY-iscc10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HMY-iscc10.pdf}, doi = {10.1109/ISCC.2010.5546538}, abstract = {Response time is an important factor for every software system and it becomes more salient when it is associated with introducing novel technologies, such as Web services. Most performance evaluation of Web services are focused toward composite Web services and their response time. One important limitation of existing work is in the fact that only constant or service exponential time distribution are considered. However, experimental results have shown that the Web services response times is typically heavy-tailed, in particulary, if there are heterogeneous. So, heavy-tailed response times should be considered in the dimensioning Web services. In this study, we propose analytical formulas for mean response times for structured BPEL constructors such as \emph{sequence}, \emph{flow} and \emph{switch} constructors,~etc. The difference with previous studies in the literature, is that we consider heterogenous servers, the number of invoked elementary Web services can be variable and the elementary Web services response times are heavy-tailed.} }

@inproceedings{DDS-fcsprivmod10, address = {Edinburgh, Scotland, UK}, month = jul, year = 2010, editor = {Cortier, V{\'e}ronique and Ryan, Mark D. and Shmatikov, Vitaly}, acronym = {{FCS-PrivMod}'10}, booktitle = {{P}roceedings of the {W}orkshop on {F}oundations of {S}ecurity and {P}rivacy ({FCS-PrivMod}'10)}, author = {Dahl, Morten and Delaune, St{\'e}phanie and Steel, Graham}, title = {Formal Analysis of Privacy for Vehicular Mix-Zones}, pages = {55-70}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-10.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-10.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/ rr-lsv-2010-10.ps}, doi = {10.1007/978-3-642-15497-3_4}, abstract = {Safety critical applications for recently proposed vehicle to vehicle ad-hoc networks (VANETs) rely on a beacon signal, which poses a threat to privacy since it could allow a vehicle to be tracked. Mix-zones, where vehicles encrypt their transmissions and then change their identifiers, have been proposed as a solution to this problem.\par In this work, we describe a formal analysis of mix-zones. We model a mix-zone and propose a formal definition of privacy for such a zone. We give a set of necessary conditions for any mix-zone protocol to preserve privacy. We analyse, using the tool ProVerif, a particular proposal for key distribution in mix-zones, the CMIX protocol. We report attacks on privacy and we propose a fix.} }

@article{BKM-lmcs10, journal = {Logical Methods in Computer Science}, author = {Bollig, Benedikt and Kuske, Dietrich and Meinecke, Ingmar}, title = {Propositional Dynamic Logic for Message-Passing Systems}, year = 2010, month = sep, volume = 6, number = {3:16}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BKM-lmcs10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BKM-lmcs10.pdf}, doi = {10.2168/LMCS-6(3:16)2010}, abstract = {We examine a bidirectional propositional dynamic logic~(PDL) for finite and infinite message sequence charts~(MSCs) extending \(\textsf{LTL}\) and \(\textsf{TLC}^{-}\). By~this kind of multi-modal logic we can express properties both in the entire future and in the past of an event. Path expressions strengthen the classical until operator of temporal logic. For every formula defining an MSC language, we construct a communicating finite-state machine~(CFM) accepting the same language. The CFM obtained has size exponential in the size of the formula. This synthesis problem is solved in full generality, \textit{i.e.}, also for MSCs with unbounded channels. The model checking problem for CFMs and HMSCs turns out to be in PSPACE for existentially bounded MSCs. Finally, we show that, for PDL with intersection, the semantics of a formula cannot be captured by a CFM anymore.} }

@inproceedings{CS-dlt2010, address = {London, Ontario, Canada}, month = aug, year = 2010, volume = {6224}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Gao, Yuan and Lu, Hanlin and Seki, Shinnosuke and Yu, Sheng}, acronym = {{DLT}'10}, booktitle = {{P}roceedings of the 14th {I}nternational {C}onference on {D}evelopments in {L}anguage {T}heory ({DLT}'10)}, author = {Chambart, Pierre and Schnoebelen, {\relax Ph}ilippe}, title = {Computing blocker sets for the Regular {P}ost Embedding Problem}, pages = {136-147}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-dlt10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-dlt10.pdf}, doi = {10.1007/978-3-642-14455-4_14}, abstract = {Blocker and coblocker sets are regular languages involved in the algorithmic solution of the Regular Post Embedding Problem. We investigate the computability of these languages and related decision problems.} }

@inproceedings{Schmitz-acl10, address = {Uppsala, Sweden}, month = jul, year = 2010, publisher = {Association for Computational Linguistics}, acronym = {{ACL}'10}, booktitle = {{P}roceedings of the 48th {A}nnual {M}eeting of the {A}ssociation for {C}omputational {L}inguistics ({ACL}'10)}, author = {Schmitz, Sylvain}, title = {On the Computational Complexity of Dominance Links in Grammatical Formalisms}, pages = {514-524}, url = {http://hal.archives-ouvertes.fr/hal-00482396}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Schmitz-acl10.pdf}, abstract = {Dominance links were introduced in grammars to model long distance scrambling phenomena, motivating the definition of multiset-valued linear indexed grammars (MLIGs) by Rambow~(1994b), and inspiring quite a few recent formalisms. It~turns out that MLIGs have since been rediscovered and reused in a variety of contexts, and that the complexity of their emptiness problem has become the key to several open questions in computer science. We survey complexity results and open issues on MLIGs and related formalisms, and provide new complexity bounds for some linguistically motivated restrictions.} }

@article{HNS-tcs10, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {H{\'e}am, Pierre-Cyrille and Nicaud, Cyril and Schmitz, Sylvain}, title = {Parametric Random Generation of Deterministic Tree Automata}, year = 2010, volume = 411, number = {38-39}, pages = {3469-3480}, month = aug, url = {http://hal.inria.fr/inria-00511450}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HNS-tcs10.pdf}, doi = {10.1016/j.tcs.2010.05.036}, abstract = {Uniform random generators deliver a simple empirical means to estimate the average complexity of an algorithm. We present a general rejection algorithm that generates sequential letter-to-letter transducers up to isomorphism. We~also propose an original parametric random generation algorithm to produce sequential letter-to-letter transducers with a fixed number of transitions. We~tailor this general scheme to randomly generate deterministic tree walking automata and deterministic top-down tree automata. We~apply our implementation of the generator to the estimation of the average complexity of a deterministic tree walking automata to nondeterministic top-down tree automata construction we also implemented.} }

@incollection{DKR-lncs6000, noaddress = {}, month = may, year = 2010, volume = 6000, series = {Lecture Notes in Computer Science}, publisher = {Springer}, noacronym = {}, booktitle = {{T}owards {T}rustworthy {E}lections -- {N}ew {D}irections in {E}lectronic {V}oting}, editor = {Chaum, David and Jakobsson, Markus and Rivest, Ronald L. and Ryan, Peter Y. A. and Benaloh, Josh and Kuty{\l}owski, Miros{\l}aw and Adida, Ben}, author = {Delaune, St{\'e}phanie and Kremer, Steve and Ryan, Mark D.}, title = {Verifying Privacy-Type Properties of Electronic Voting Protocols: A~Taster}, pages = {289-309}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DKR-lncs6000.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DKR-lncs6000.pdf}, doi = {10.1007/978-3-642-12980-3_18}, abstract = {While electronic elections promise the possibility of convenient, efficient and secure facilities for recording and tallying votes, recent studies have highlighted inadequacies in implemented systems. These inadequacies provide additional motivation for applying formal methods to the validation of electronic voting protocols.\par In this paper we report on some of our recent efforts in using the applied pi calculus to model and analyse properties of electronic elections. We particularly focus on anonymity properties, namely vote-privacy and receipt-freeness. These properties are expressed using observational equivalence and we show in accordance with intuition that receipt-freeness implies vote-privacy.\par We illustrate our definitions on two electronic voting protocols from the literature. Ideally, these properties should hold even if the election officials are corrupt. However, protocols that were designed to satisfy privacy or receipt-freeness may not do so in the presence of corrupt officials. Our model and definitions allow us to specify and easily change which authorities are supposed to be trustworthy.} }

@inproceedings{CCD-ijcar10, address = {Edinburgh, Scotland, UK}, month = jul, year = 2010, volume = {6173}, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer-Verlag}, editor = {Giesl, J{\"u}rgen and Haehnle, Reiner}, acronym = {{IJCAR}'10}, booktitle = {{P}roceedings of the 5th {I}nternational {J}oint {C}onference on {A}utomated {R}easoning ({IJCAR}'10)}, author = {Cheval, Vincent and Comon{-}Lundh, Hubert and Delaune, St{\'e}phanie}, title = {Automating security analysis: symbolic equivalence of constraint systems}, pages = {412-426}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-ijcar10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-ijcar10.pdf}, doi = {10.1007/978-3-642-14203-1_35}, abstract = {We consider security properties of cryptographic protocols, that are either trace properties (such as confidentiality or authenticity) or equivalence properties (such as anonymity or strong secrecy).\par Infinite sets of possible traces are symbolically represented using \emph{deducibility constraints}. We give a new algorithm that decides the trace equivalence for the traces that are represented using such constraints, in the case of signatures, symmetric and asymmetric encryptions. Our algorithm is implemented and performs well on typical benchmarks. This is the first implemented algorithm, deciding symbolic trace equivalence.} }

@inproceedings{BH-monterey2008, address = {Budapest, Hungary}, month = apr, year = 2010, volume = 6028, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Choppy, {\relax Ch}ristine and Sokolsky, Oleg}, acronym = {{MONTEREY}'08}, booktitle = {{R}evised {S}elected {P}apers of the 15th {M}onterey {W}orkshop on {F}oundations of {C}omputer {S}oftware ({MONTEREY}'08)}, author = {Ben{ }Hmida, Mehdi and Haddad, Serge}, title = {Client Synthesis for Aspect Oriented Web Services}, pages = {24-42}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BH-monterey08.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BH-monterey08.pdf}, doi = {10.1007/978-3-642-12566-9_2}, abstract = {Client synthesis for complex Web services is a critical and still open topic as it will enable more flexibility in the deployment of such services. In previous works, our team has developed a theoretical framework based on process algebra that has led to algorithms and tools for the client interaction. Here, we show how to generalise our approach for aspect oriented Web services.} }

@inproceedings{JGL-icalp10, address = {Bordeaux, France}, month = jul, year = 2010, volume = 6199, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Abramsky, Samson and Meyer{ }auf{ }der{ }Heide, Friedhelm and Spirakis, Paul}, acronym = {{ICALP}'10}, booktitle = {{P}roceedings of the 37th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'10)~-- {P}art~{II}}, author = {Goubault{-}Larrecq, Jean}, title = {Noetherian Spaces in Verification}, pages = {2-21}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-icalp10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-icalp10.pdf}, doi = {10.1007/978-3-642-14162-1_2}, abstract = {Noetherian spaces are a topological concept that generalizes well quasiorderings. We explore applications to infinite-state verification problems, and show how this stimulated the search for infinite procedures \`a la Karp-Miller.} }

@inproceedings{CS-icalp10, address = {Bordeaux, France}, month = jul, year = 2010, volume = 6199, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Abramsky, Samson and Meyer{ }auf{ }der{ }Heide, Friedhelm and Spirakis, Paul}, acronym = {{ICALP}'10}, booktitle = {{P}roceedings of the 37th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'10)~-- {P}art~{II}}, author = {Chambart, Pierre and Schnoebelen, {\relax Ph}ilippe}, title = {Pumping and Counting on the Regular {P}ost Embedding Problem}, pages = {64-75}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-icalp10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-icalp10.pdf}, doi = {10.1007/978-3-642-14162-1_6}, abstract = {The Regular Post Embedding Problem is a variant of Post's Correspondence Problem where one compares strings with the subword relation and imposes additional regular constraints on admissible solutions. It is known that this problem is decidable, albeit with very high complexity.\par We consider and solve variant problems where the set of solutions is compared to regular constraint sets and where one counts the number of solutions. Our positive results rely on two non-trivial pumping lemmas for Post-embedding languages and their complements.} }

@inproceedings{CD-icalp10, address = {Bordeaux, France}, month = jul, year = 2010, volume = 6199, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Abramsky, Samson and Meyer{ }auf{ }der{ }Heide, Friedhelm and Spirakis, Paul}, acronym = {{ICALP}'10}, booktitle = {{P}roceedings of the 37th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'10)~-- {P}art~{II}}, author = {Chatterjee, Krishnendu and Doyen, Laurent}, title = {Energy Parity Games}, pages = {599-610}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-icalp10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-icalp10.pdf}, doi = {10.1007/978-3-642-14162-1_50}, abstract = {Energy parity games are infinite two-player turn-based games played on weighted graphs. The objective of the game combines a (qualitative) parity condition with the (quantitative) requirement that the sum of the weights (\textit{i.e.}, the level of energy in the game) must remain positive. Beside their own interest in the design and synthesis of resource-constrained omega-regular specifications, energy parity games provide one of the simplest model of games with combined qualitative and quantitative objective. Our main results are as follows: (a)~exponential memory is sufficient and may be necessary for winning strategies in energy parity games; (b)~the~problem of deciding the winner in energy parity games can be solved in NP\(\cap\)coNP; and (c)~we~give an algorithm to solve energy parity by reduction to energy games. We~also show that the problem of deciding the winner in energy parity games is polynomially equivalent to the problem of deciding the winner in mean-payoff parity games, which can thus be solved in NP\(\cap\)coNP. As~a consequence we also obtain a conceptually simple algorithm to solve mean-payoff parity games.} }

@inproceedings{BGMZ-icalp10, address = {Bordeaux, France}, month = jul, year = 2010, volume = 6199, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Abramsky, Samson and Meyer{ }auf{ }der{ }Heide, Friedhelm and Spirakis, Paul}, acronym = {{ICALP}'10}, booktitle = {{P}roceedings of the 37th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'10)~-- {P}art~{II}}, author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin and Zeitoun, Marc}, title = {Pebble weighted automata and transitive closure logics}, pages = {587-598}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-icalp10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-icalp10.pdf}, doi = {10.1007/978-3-642-14162-1_49}, abstract = {We introduce new classes of weighted automata on words. Equipped with pebbles and a two-way mechanism, they go beyond the class of recognizable formal power series, but capture a weighted version of first-order logic with bounded transitive closure. In contrast to previous work, this logic allows for unrestricted use of universal quantification. Our main result states that pebble weighted automata, nested weighted automata, and this weighted logic are expressively equivalent. We also give new logical characterizations of the recognizable series.} }

@inproceedings{CC-csf10, address = {Edinburgh, Scotland, UK}, month = jul, year = 2010, publisher = {{IEEE} Computer Society Press}, acronym = {{CSF}'10}, booktitle = {{P}roceedings of the 23rd {IEEE} {C}omputer {S}ecurity {F}oundations {S}ymposium ({CSF}'10)}, author = {Ciob{\^a}c{\u{a}}, {\c{S}}tefan and Cortier, V{\'e}ronique}, title = {Protocol composition for arbitrary primitives}, pages = {322-336}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-09.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2010-09.pdf}, doi = {10.1109/CSF.2010.29}, abstract = {We study the composition of security protocols when protocols share secrets such as keys. We show (in a Dolev-Yao model) that if two protocols use disjoint cryptographic primitives, their composition is secure if the individual protocols are secure, even if they share data. Our result holds for any cryptographic primitives that can be modeled using equational theories, such as encryption, signature, MAC, exclusive-or, and Diffie-Hellman. Our main result transforms any attack trace of the combined protocol into an attack trace of one of the individual protocols. This allows various ways of combining protocols such as sequentially or in parallel, possibly with inner replications. As an application, we show that a protocol using preestablished keys may use any (secure) key-exchange protocol without jeopardizing its security, provided that they do not use the same primitives. This allows us, for example, to securely compose a Diffie-Hellman key exchange protocol with any other protocol using the exchanged key, provided that the second protocol does not use the Diffie-Hellman primitives. We also explore tagging, which is a way of forcing the disjointness of two protocols that share cryptographic primitives We explain why composing protocols which use tagged cryptographic primitives like encryption and hash functions is secure by reducing this problem to the previous one.} }

@inproceedings{ACD-csf10, address = {Edinburgh, Scotland, UK}, month = jul, year = 2010, publisher = {{IEEE} Computer Society Press}, acronym = {{CSF}'10}, booktitle = {{P}roceedings of the 23rd {IEEE} {C}omputer {S}ecurity {F}oundations {S}ymposium ({CSF}'10)}, author = {Arnaud, Mathilde and Cortier, V{\'e}ronique and Delaune, St{\'e}phanie}, title = {Modeling and Verifying Ad Hoc Routing Protocols}, pages = {59-74}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ACD-csf10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ACD-csf10.pdf}, doi = {10.1109/CSF.2010.12}, 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 the protocol \textsf{SRP} applied to~\textsf{DSR}.} }

@inproceedings{BKKLNP-cav10, address = {Edinburgh, Scotland, UK}, month = jul, year = 2010, volume = {6174}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Cook, Byron and Jackson, Paul and Touili, Tayssir}, acronym = {{CAV}'10}, booktitle = {{P}roceedings of the 22nd {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV}'10)}, author = {Bollig, Benedikt and Katoen, Joost-Pieter and Kern, Carsten and Leucker, Martin and Neider, Daniel and Piegdon, David R.}, title = {libalf: the Automata Learning Framework}, pages = {360-364}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BKKLNP-cav10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BKKLNP-cav10.pdf}, doi = {10.1007/978-3-642-14295-6_32}, abstract = {This paper presents \texttt{libalf}, a comprehensive, open-source library for learning formal languages. \texttt{libalf} covers various well-known learning techniques for finite automata (e.g. Angluin's~\(\textsf{L}^*\), \textsf{Biermann}, \textsf{RPNI},~etc.) as well as novel learning algorithms (such as for NFA and visibly one-counter automata). \texttt{libalf}~is flexible and allows facilely interchanging learning algorithms and combining domain-specific features in a plug-and-play fashion. Its modular design and C++ implementation make it a suitable platform for adding and engineering further learning algorithms for new target models (\textit{e.g.}, B{\"u}chi automata).} }

@article{RHS-ijfcs09, publisher = {World Scientific}, journal = {International Journal of Foundations of Computer Science}, author = {Recalde, Laura and Haddad, Serge and Silva, Manuel}, title = {Continuous {P}etri Nets: Expressive Power and Decidability Issues}, volume = 21, number = 2, pages = {235-256}, year = 2010, month = apr, doi = {10.1142/S0129054110007222}, abstract = {State explosion is a fundamental problem in the analysis and synthesis of discrete event systems. Continuous Petri nets can be seen as a relaxation of the corresponding discrete model. The expected gains are twofold: improvements in complexity and in decidability. In the case of autonomous nets we prove that liveness or deadlock-freeness remain decidable and can be checked more efficiently than in Petri nets. Then we introduce time in the model which now behaves as a dynamical system driven by differential equations and we study it w.r.t. expressiveness and decidability issues. On the one hand, we prove that this model is equivalent to timed differential Petri nets which are a slight extension of systems driven by linear differential equations~(LDE). On~the other hand, (contrary to the systems driven by~LDEs) we show that continuous timed Petri nets are able to simulate Turing machines and thus that basic properties become undecidable.} }

@inproceedings{SS-lics10, address = {Edinburgh, Scotland, UK}, month = jul, year = 2010, publisher = {{IEEE} Computer Society Press}, acronym = {{LICS}'10}, booktitle = {{P}roceedings of the 25th {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'10)}, author = {Schweikardt, Nicole and Segoufin, Luc}, title = {Addition-invariant {FO} and regularity}, pages = {273-282}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/SS-lics10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SS-lics10.pdf}, doi = {10.1109/LICS.2010.16}, abstract = {We consider formulas which, in addition to the symbols in the vocabulary, may use two designated symbols~\(\prec\) and~\(+\) that must be interpreted as a linear order and its associated addition. Such a formula is called addition-invariant if, for each fixed interpretation of the initial vocabulary, its result is independent of the particular interpretation of~\(\prec\) and~\(+\).\par This paper studies the expressive power of addition-invariant first-order logic, \(+\)-inv-FO, on the class of finite strings. Our first main result gives a characterization of the regular languages definable in \(+\)-inv-FO: we show that these are exactly the languages definable in FO with extra predicates, denoted by {"}lm{"} for short, for testing the length of the string modulo some fixed number. Our second main result shows that every language definable in \(+\)-inv-FO, that is bounded or commutative or deterministic context-free, is regular. As an immediate consequence of these two main results, we obtain that \(+\)-inv-FO is equivalent to FO(lm) on the class of finite colored sets.\par Our proof methods involve Ehrenfeucht-Fra{\"\i}ss{\'e} games, tools from algebraic automata theory, and reasoning about semi-linear sets.} }

@inproceedings{PS-lics10, address = {Edinburgh, Scotland, UK}, month = jul, year = 2010, publisher = {{IEEE} Computer Society Press}, acronym = {{LICS}'10}, booktitle = {{P}roceedings of the 25th {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'10)}, author = {Place, {\relax Th}omas and Segoufin, Luc}, title = {Deciding definability in \(\textrm{FO}_{2}(<)\) on trees}, pages = {253-262}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/PS-lics10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PS-lics10.pdf}, doi = {10.1109/LICS.2010.17}, abstract = { We prove that it is decidable whether a regular unranked tree language is definable in~\(\textsf{FO}_{2}(<_{h}, <_{v})\). By~\(\textsf{FO}_{2}(<_{h}, <_{v})\) we refer to the two variable fragment of first order logic built from the descendant and following sibling predicates. In terms of expressive power it corresponds to a fragment of the navigational core of XPath that contains modalities for going up to some ancestor, down to some descendant, left to some preceding sibling, and right to some following sibling.\par We also investigate definability in some other fragments of XPath.} }

@inproceedings{JGL-lics10, address = {Edinburgh, Scotland, UK}, month = jul, year = 2010, publisher = {{IEEE} Computer Society Press}, acronym = {{LICS}'10}, booktitle = {{P}roceedings of the 25th {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'10)}, author = {Goubault{-}Larrecq, Jean}, title = {{{\(\omega\)}}{\textbf{\MakeUppercase{QRB}}}-Domains and the Probabilistic Powerdomain}, pages = {352-361}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-lics10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-lics10.pdf}, doi = {10.1109/LICS.2010.50}, abstract = {Is there any cartesian-closed category of continuous domains that would be closed under Jones and Plotkin's probabilistic powerdomain construction? This is a major open problem in the area of denotational semantics of probabilistic higher-order languages. We relax the question, and look for quasi-continuous dcpos instead. We introduce a natural class of such quasi-continuous dcpos, the \(\omega\textbf{QRB}\)-domains. We show that they form a category \(\omega\textbf{QRB}\) with pleasing properties: \(\omega\textbf{QRB}\) is closed under the probabilistic powerdomain functor, has all finite products, all bilimits, and is stable under retracts, and even under so-called quasiretracts. But... \(\omega\textbf{QRB}\) is not cartesian closed.} }

@inproceedings{BCGJV-lics10, address = {Edinburgh, Scotland, UK}, month = jul, year = 2010, publisher = {{IEEE} Computer Society Press}, acronym = {{LICS}'10}, booktitle = {{P}roceedings of the 25th {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'10)}, author = {Bargu{\~n}{\'o}, Luis and Creus, Carles and Godoy, Guillem and Jacquemard, Florent and Vacher, Camille}, title = {The Emptiness Problem for Tree Automata with Global Constraints}, pages = {263-272}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGJV-lics10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGJV-lics10.pdf}, doi = {10.1109/LICS.2010.28}, abstract = {We define tree automata with global constraints~(TAGC), generalizing the class of tree automata with global equality and disequality constraints~(TAGED). TAGC~can test for equality and disequality between subterms whose positions are defined by the states reached during a computation. In~particular, TAGC~can check that all the subterms reaching a given state are distinct. This constraint is related to monadic key constraints for XML documents, meaning that every two distinct positions of a given type have different values.\par We prove decidability of the emptiness problem for~TAGC. This solves, in particular, the open question of decidability of emptiness for TAGED. We further extend our result by allowing global arithmetic constraints for counting the number of occurrences of some state or the number of different subterms reaching some state during a computation. We also allow local equality and disequality tests between sibling positions and the extension to unranked ordered trees. As a consequence of our results for TAGC, we prove the decidability of a fragment of the monadic second order logic on trees extended with predicates for equality and disequality between subtrees, and cardinality.} }

@inproceedings{CF-pn10, address = {Braga, Portugal}, month = jun, year = 2010, volume = 6128, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Lilius, Johan and Penczek, Wojciech}, acronym = {{PETRI~NETS}'10}, booktitle = {{P}roceedings of the 31st {I}nternational {C}onference on {A}pplications and {T}heory of {P}etri {N}ets ({PETRI~NETS}'10)}, author = {Chatain, {\relax Th}omas and Fabre, {\'E}ric}, title = {Factorization Properties of Symbolic Unfoldings of Colored {P}etri Nets}, pages = {165-184}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CF-pn10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CF-pn10.pdf}, doi = {10.1007/978-3-642-13675-7_11}, abstract = {The unfolding technique is an efficient tool to explore the runs of a Petri net in a true concurrency semantics, \textit{i.e.}, without constructing all the interleavings of concurrent actions. But even small real systems are never modeled directly as ordinary Petri nets: they use many high-level features that were designed as extensions of Petri nets. We focus here on two such features: colors and compositionality. We show that the symbolic unfolding of a product of colored Petri nets can be expressed as the product of the symbolic unfoldings of these nets. This is a necessary result in view of distributed computations based on symbolic unfoldings, as they have been developed already for standard unfoldings, to design modular verification techniques, or modular diagnosis procedures, for example. The factorization property of symbolic unfoldings is valid for several classes of colored or high-level nets. We derive it here for a class of (high-level) open nets, for which the composition is performed by connecting places rather than transitions.} }

@article{DL-jal10, publisher = {Elsevier Science Publishers}, journal = {Journal of Applied Logic}, author = {Demri, St{\'e}phane and Lugiez, Denis}, title = {Complexity of Modal Logics with {P}resburger Constraints}, year = {2010}, volume = {8}, number = {3}, pages = {233-252}, month = sep, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DL-jal10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DL-jal10.pdf}, doi = {10.1016/j.jal.2010.03.001}, abstract = {We introduce the extended modal logic EML with regularity constraints and full Presburger constraints on the number of children that generalize graded modalities, also known as number restrictions in description logics. We show that EML satisfiability is only \textsc{pspace}-complete by designing a Ladner-like algorithm. This extends a well-known and non-trivial \textsc{pspace} upper bound for graded modal logic. Furthermore, we provide a detailed comparison with logics that contain Presburger constraints and that are dedicated to query XML documents. As an application, we provide a logarithmic space reduction from a variant of Sheaves logic SL into EML that allows us to establish that its satisfiability problem is also \textsc{pspace}-complete, significantly improving the best known upper bound.} }

@article{LS-jal10, publisher = {Elsevier Science Publishers}, journal = {Journal of Applied Logic}, author = {Libkin, Leonid and Sirangelo, Cristina}, title = {Reasoning about {XML} with temporal logics and automata}, year = {2010}, volume = {8}, number = {2}, pages = {210-232}, month = jun, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-jal10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-jal10.pdf}, doi = {10.1016/j.jal.2009.09.005}, abstract = {We show that problems arising in static analysis of XML specifications and transformations can be dealt with using techniques similar to those developed for static analysis of programs. Many properties of interest in the XML context are related to navigation, and can be formulated in temporal logics for trees. We choose a logic that admits a simple single-exponential translation into unranked tree automata, in the spirit of the classical LTL-to-B{\"u}chi automata translation. Automata arising from this translation have a number of additional properties; in particular, they are convenient for reasoning about unary node-selecting queries, which are important in the XML context. We give two applications of such reasoning: one deals with a classical XML problem of reasoning about navigation in the presence of schemas, and the other relates to verifying security properties of XML views.} }

@article{DLS-tcs10, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {Demri, St{\'e}phane and Lazi{\'c}, Ranko and Sangnier, Arnaud}, title = {Model checking memoryful linear-time logics over one-counter automata}, year = {2010}, volume = {411}, number = {22-24}, pages = {2298-2316}, month = may, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DLS-tcs10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DLS-tcs10.pdf}, doi = {10.1016/j.tcs.2010.02.021}, abstract = {We study complexity of the model-checking problems for LTL with registers (also known as freeze LTL and written LTL\(^{\downarrow}\)) and for first-order logic with data equality tests (written \(\textrm{FO}(\sim, <, +1)\)) over one-counter automata. We consider several classes of one-counter automata (mainly deterministic vs. nondeterministic) and several logical fragments (restriction on the number of registers or variables and on the use of propositional variables for control states). The logics have the ability to store a counter value and to test it later against the current counter value. We show that model checking LTL\(^{\downarrow}\) and \(\textrm{FO}(\sim , <, +1)\) over deterministic one-counter automata is PSpace-complete with infinite and finite accepting runs. By constrast, we prove that model checking LTL\(^{\downarrow}\) in which the until operator~\(\mathbf{U}\) is restricted to the eventually~\(\mathbf{F}\) over nondeterministic one-counter automata is \(\Sigma_1^1\)-complete [resp. \(\Sigma_1^0\)-complete] in the infinitary [resp. finitary] case even if only one register is used and with no propositional variable. As a corollary of our proof, this also holds for \(\textrm{FO}(\sim, <, +1)\) restricted to two variables (written \(\textrm{FO}_2 (\sim, <, +1)\)). This makes a difference with the facts that several verification problems for one-counter automata are known to be decidable with relatively low complexity, and that finitary satisfiability for LTL\(^{\downarrow}\) and \(\textrm{FO}_2 (\sim, <, +1)\) are decidable. Our results pave the way for model-checking memoryful (linear-time) logics over other classes of operational models, such as reversal-bounded counter machines.} }

@article{AF-ijmest10, publisher = {Taylor \& Francis}, journal = {International Journal of Mathematical Education in Science and Technology}, author = {Arnoux, Pierre and Finkel, Alain}, title = {Using mental imagery processes for teaching and research in mathematics and computer science}, volume = 41, number = 2, month = jan, year = 2010, pages = {229-242}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AF-ijmest10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AF-ijmest10.pdf}, doi = {10.1080/00207390903372429}, abstract = {The role of mental representations in mathematics and computer science (for teaching or research) is often downplayed or even completely ignored. Using an ongoing work on the subject, we argue for a more systematic study and use of mental representations, to get an intuition of mathematical concepts, and also to understand and build proofs. We give two detailed examples.} }

@article{GK-icomp10, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Gastin, Paul and Kuske, Dietrich}, title = {Uniform satisfiability problem for local temporal logics over {M}azurkiewicz traces}, volume = 208, number = 7, month = jul, year = 2010, pages = {797-816}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/GK-icomp10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GK-icomp10.pdf}, doi = {10.1016/j.ic.2009.12.003}, abstract = {We continue our study of the complexity of MSO-definable local temporal logics over concurrent systems that can be described by Mazurkiewicz traces. In previous papers, we showed that the satisfiability problem for any such logic is in PSPACE (provided the dependence alphabet is fixed) and remains in PSPACE for all classical local temporal logics even if the dependence alphabet is part of the input. In~this paper, we consider the uniform satisfiability problem for arbitrary MSO-definable local temporal logics. For this problem, we prove multi-exponential lower and upper bounds that depend on the number of alternations of set quantifiers present in the chosen MSO-modalities.} }

@article{Haar-tac10, publisher = {{IEEE} Computer Society Press}, journal = {IEEE Transactions on Automatic Control}, author = {Haar, Stefan}, title = {Types of Asynchronous Diagnosability and the {\emph{Reveals}}-Relation in Occurrence Nets}, volume = 55, number = 10, month = oct, year = 2010, pages = {2310-2320}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/haar-tac10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/haar-tac10.pdf}, doi = {10.1109/TAC.2010.2063490}, abstract = {We consider asynchronous diagnosis in (safe) Petri net models of distributed systems, using the partial order semantics of occurrence net unfoldings. Both the observability and diagnosability properties will appear in two different forms, depending on the semantics chosen: \emph{strong} observability and diagnosability are the classical notions from the state machine model and correspond to interleaving semantics in Petri nets. By contrast, the \emph{weak} form is linked to characteristics of nonsequential processes, and requires an asynchronous \emph{progress} assumption on those processes. We give algebraic characterizations for both types, and give verification methods. The study of weak diagnosability leads us to the analysis of a relation in occurrence nets, first presented in~[S.~Haar~(2007): \textit{Unfold and Cover: Qualitative Diagnosability for Petri Nets.}]: given the occurrence of some event~\(a\) that \emph{reveals}~\(b\), the occurrence of~\(b\) is inevitable. Then \(b\) may already have occurred, be concurrent to, or even in the future of~\(a\). We show that the \emph{reveals}-relation can be effectively computed recursively---for each pair, a suitable finite prefix of bounded depth is sufficient---and show its use in asynchronous diagnosis. Based on this relation, a~decomposition of the Petri net unfolding into \emph{facets} is defined, yielding an abstraction technique that preserves and reflects maximal partially ordered runs.} }

@inproceedings{SRKK-arspawits10, address = {Paphos, Cyprus}, month = oct, year = 2010, volume = 6186, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Armando, Alessandro and Lowe, Gavin}, acronym = {{ARSPA-WITS}'10}, booktitle = {{P}roceedings of the {J}oint {W}orkshop on {A}utomated {R}easoning for {S}ecurity {P}rotocol {A}nalysis and {I}ssues in the {T}heory of {S}ecurity ({ARSPA-WITS}'10)}, author = {Smyth, Ben and Ryan, Mark D. and Kremer, Steve and Kourjieh, Mounira}, title = {Towards automatic analysis of election verifiability properties}, pages = {146-163}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/SRKK-arspawits10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SRKK-arspawits10.pdf}, doi = {10.1007/978-3-642-16074-5_11}, abstract = {We present a symbolic definition that captures some cases of election verifiability for electronic voting protocols. Our definition is given in terms of reachability assertions in the applied pi calculus and is amenable to automated reasoning using the software tool ProVerif. The definition distinguishes three aspects of verifiability, which we call individual, universal, and eligibility verifiability. We demonstrate the applicability of our formalism by analysing the protocols due to Fujioka, Okamoto~\& Ohta and a variant of the one by Juels, Catalano~\& Jakobsson (implemented as Civitas by Clarkson, Chong~\& Myers).} }

@inproceedings{BH-csr10, address = {Kazan, Russia}, month = jun, year = 2010, volume = 6072, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Mayr, Ernst W.}, acronym = {{CSR}'10}, booktitle = {{P}roceedings of the 5th {I}nternational {C}omputer {S}cience {S}ymposium in {R}ussia ({CSR}'10)}, author = {Bollig, Benedikt and H{\'e}lou{\"e}t, Lo{\"\i}c}, title = {Realizability of Dynamic {MSC} Languages}, pages = {48-59}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BH-csr10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BH-csr10.pdf}, doi = {10.1007/978-3-642-13182-0_5}, abstract = {We introduce dynamic communicating automata~(DCA), an~extension of communicating finite-state machines that allows for dynamic creation of processes. Their behavior can be described as sets of message sequence charts~(MSCs). We~consider the realizability problem for DCA: given a dynamic MSC grammar (a~high-level MSC specification), is there a DCA defining the same set of MSCs? We~show that this problem is decidable in doubly exponential time, and identify a class of realizable grammars that can be implemented by \emph{finite} DCA.} }

@article{CS-jacm10, publisher = {ACM Press}, journal = {Journal of the~{ACM}}, author = {ten~Cate, Balder and Segoufin, Luc}, title = {Transitive Closure Logic, Nested Tree Walking Automata, and {XP}ath}, volume = 57, number = 3, month = mar, year = 2010, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-jacm10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-jacm10.pdf}, doi = {10.1145/1706591.1706598}, abstract = {We study \textsf{FO(MTC)}, first-order logic with monadic transitive closure, a logical formalism in between \textsf{FO} and \textsf{MSO} on trees. We characterize the expressive power of \textsf{FO(MTC)} in terms of nested tree-walking automata. Using the latter we show that \textsf{FO(MTC)} is strictly less expressive than \textsf{MSO}, solving an open problem. We also present a temporal logic on trees that is expressivel complete for \textsf{FO(MTC)}, in the form of an extension of the XML document navigation language XPath with two operators: the Kleene star for taking the transitive closure of path expressions, and a subtree relativisation operator, allowing one to restrict attention to a specific subtree while evaluating a subexpression. We show that the expressive power of this XPath dialect equals that of \textsf{FO(MTC)} for Boolean, unary and binary queries. We also investigate the complexity of the automata model as well as the XPath dialect. We show that query evaluation be done in polynomial time (combined complexity), but that emptiness (or, satisfiability) is 2ExpTime-complete.} }

@article{BCHK-icomp10, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Baldan, Paolo and Chatain, {\relax Th}omas and Haar, Stefan and K{\"o}nig, Barbara}, title = {Unfolding-based Diagnosis of Systems with an Evolving Topology}, volume = 208, number = 10, pages = {1169-1192}, year = 2010, month = oct, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCHK-icomp10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCHK-icomp10.pdf}, doi = {10.1016/j.ic.2009.11.009}, abstract = {We propose a framework for model-based diagnosis of systems with mobility and variable topologies, modelled as graph transformation systems. Generally speaking, model-based diagnosis is aimed at constructing explanations of observed faulty behaviours on the basis of a given model of the system. Since the number of possible explanations may be huge, we exploit the unfolding as a compact data structure to store them, along the lines of previous work dealing with Petri net models. Given a model of a system and an observation, the explanations can be constructed by unfolding the model constrained by the observation, and then removing incomplete explanations in a pruning phase. The theory is formalised in a general categorical setting: constraining the system by the observation corresponds to taking a product in the chosen category of graph grammars, so that the correctness of the procedure can be proved by using the fact that the unfolding is a right adjoint and thus it preserves products. The theory should hence be easily applicable to a wide class of system models, including graph grammars and Petri nets.} }

@incollection{Berwanger09, year = 2010, volume = 6006, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, editor = {Bonnano, Giacomo and L{\"o}we, Benedikt and van der Hoek, Wiebe}, booktitle = {Logic and the Foundations of Game and Decision Theory (LOFT8)}, author = {Berwanger, Dietmar}, title = {Infinite Coordination Games}, pages = {1-19}, futurechapter = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/Ber-loft8.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Ber-loft8.pdf}, doi = {10.1007/978-3-642-15164-4_1}, abstract = {We investigate the prescriptive power of sequential iterated admissibility in coordination games of the Gale-Stewart style, \textit{i.e.}, perfect-information games of infinite duration with only two payoffs. We show that, on this kind of games, the procedure of eliminating weakly dominated strategies is independent of the elimination order and that, under maximal simultaneous elimination, the procedure converges after at most omega many stages.} }

@article{BK-jlli10, publisher = {Kluwer Academic Publishers}, journal = {Journal of Logic, Language and Information}, author = {Berwanger, Dietmar and Kaiser, {\L}ukasz}, title = {Information Tracking in Games on Graphs}, volume = 19, number = 4, pages = {395-412}, year = 2010, month = oct, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BK-jlli10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BK-jlli10.pdf}, doi = {10.1007/s10849-009-9115-8}, abstract = {When seeking to coordinate in a game with imperfect information, it is often relevant for a player to know what other players know. Keeping track of the information acquired in a play of infinite duration may, however, lead to infinite hierarchies of higher-order knowledge. We present a construction that makes explicit which higher-order knowledge is relevant in a game and allows us to describe a class of games that admit coordinated winning strategies with finite memory.} }

@proceedings{Seg-icdt10, author = {Segoufin, Luc}, editor = {Segoufin, Luc}, title = {Proceedings of the 13th {I}nternational {C}onference on {D}atabase {T}heory ({ICDT}'10)}, booktitle = {Proceedings of the 13th {I}nternational {C}onference on {D}atabase {T}heory ({ICDT}'10)}, year = 2010, month = mar, url = {http://portal.acm.org/citation.cfm?id=1804669&coll=ACM&dl=ACM} }

@inproceedings{ACKNS-icdt10, address = {Lausanne, Switzerland}, month = mar, year = 2010, publisher = {ACM Press}, editor = {Segoufin, Luc}, acronym = {{ICDT}'10}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {D}atabase {T}heory ({ICDT}'10)}, author = {Abiteboul, Serge and Chan, T.-H. Hubert and Kharlamov, Evgeny and Nutt, Werner and Senellart, Pierre}, title = {Aggregate queries for discrete and continuous probabilistic~{XML}}, pages = {50-61}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ACKNS-icdt10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ACKNS-icdt10.pdf}, doi = {10.1145/1804669.1804679}, 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 present algorithms to compute distribution functions and moments for various classes of continuous distributions of data values.} }

@inproceedings{Fig-icdt10, address = {Lausanne, Switzerland}, month = mar, year = 2010, publisher = {ACM Press}, editor = {Segoufin, Luc}, acronym = {{ICDT}'10}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {D}atabase {T}heory ({ICDT}'10)}, author = {Figueira, Diego}, title = {Forward-{XP}ath and extended register automata on data-trees}, pages = {230-240}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/fig-icdt10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/fig-icdt10.pdf}, ps = {fig-icdt10.ps}, doi = {10.1145/1804669.1804699}, abstract = {We consider a fragment of XPath named {"}forward-XPath{"}, which contains all descendant and rightwards sibling axes as well as data equality and inequality tests. The satisfiability problem for forward-XPath in the presence of DTDs and even of primary key constraints is shown here to be decidable.\par To show decidability we introduce a model of alternating automata on data trees that can move downwards and rightwards in the tree, have one register for storing data and compare them for equality, and have the ability to (1)~nondeterministically guess a data value and store it, and (2)~quantify universally over the set of data values seen so far during the run. This model extends the work of Jurdzi{\'n}ski and Lazi{\'c}. Decidability of the finitary non-emptiness problem for this model is obtained by a direct reduction to a well-structured transition system, contrary to previous approaches.} }

@article{CDH-tocl10, publisher = {ACM Press}, journal = {ACM Transactions on Computational Logic}, author = {Chatterjee, Krishnendu and Doyen, Laurent and Henzinger, {\relax Th}omas A.}, title = {Quantitative Languages}, volume = 11, number = 4, nopages = {}, year = 2010, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDH-tocl10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDH-tocl10.pdf}, ps = {CDH-tocl10.ps}, abstract = {Quantitative generalizations of classical languages, which assign to each word a real number in- stead of a boolean value, have applications in modeling resource-constrained computation. We use weighted automata (finite automata with transition weights) to define several natural classes of quantitative languages over finite and infinite words; in particular, the real value of an infinite run is computed as the maximum, limsup, liminf, limit average, or discounted sum of the transition weights. We define the classical decision problems of automata theory (emptiness, universality, language inclusion, and language equivalence) in the quantitative setting and study their compu- tational complexity. As the decidability of the language-inclusion problem remains open for some classes of weighted automata, we introduce a notion of quantitative simulation that is decidable and implies language inclusion. We also give a complete characterization of the expressive power of the various classes of weighted automata. In particular, we show that most classes of weighted automata cannot be determinized.} }

@inproceedings{DR-tacas10, address = {Paphos, Cyprus}, month = mar, year = 2010, volume = {6015}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Esparza, Javier and Majumdar, Rupak}, acronym = {{TACAS}'10}, booktitle = {{P}roceedings of the 16th {I}nternational {C}onference on {T}ools and {A}lgorithms for {C}onstruction and {A}nalysis of {S}ystems ({TACAS}'10)}, author = {Doyen, Laurent and Raskin, Jean-Fran{\c{c}}ois}, title = {Antichains Algorithms for Finite Automata}, pages = {2-22}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DR-tacas10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DR-tacas10.pdf}, ps = {DR-tacas10.ps}, doi = {10.1007/978-3-642-12002-2_2}, abstract = {We present a general theory that exploits simulation relations on transition systems to obtain antichain algorithms for solving the reachability and repeated reachability problems. Antichains are more succinct than the sets of states manipulated by the traditional fixpoint algorithms. The theory justifies the correctness of the antichain algorithms, and applications such as the universality problem for finite automata illustrate efficiency improvements. Finally, we show that new and provably better antichain algorithms can be obtained for the emptiness problem of alternating automata over finite and infinite words.} }

@article{BCDDH-icomp10, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Berwanger, Dietmar and Chatterjee, Krishnendu and Doyen, Laurent and De{~}Wulf, Martin and Henzinger, {\relax Th}omas A.}, title = {Strategy Construction for Parity Games with Imperfect Information}, volume = 208, number = 10, pages = {1206-1220}, year = 2010, month = oct, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCDDH-icomp10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCDDH-icomp10.pdf}, ps = {BCDDH-icomp10.ps}, doi = {10.1016/j.ic.2009.09.006}, abstract = {We consider two-player parity games with imperfect information in which strategies rely on observations that provide imperfect information about the history of a play. To solve such games, \textit{i.e.}, to determine the winning regions of players and corresponding winning strategies, one can use the subset construction to build an equivalent perfect-information game. Recently, an algorithm that avoids the inefficient subset construction has been proposed. The algorithm performs a fixed-point computation in a lattice of antichains, thus maintaining a succinct representation of state sets. However, this representation does not allow to recover winning strategies.\par In this paper, we build on the antichain approach to develop an algorithm for constructing the winning strategies in parity games of imperfect information. One major obstacle in adapting the classical procedure is that the complementation of attractor sets would break the invariant of downward-closedness on which the antichain representation relies. We overcome this difficulty by decomposing problem instances recursively into games with a combination of reachability, safety, and simpler parity conditions. We also report on an experimental implementation of our algorithm; to our knowledge, this is the first implementation of a procedure for solving imperfect-information parity games on graphs.} }

@misc{Quasimodo-3.4, author = {Markey, Nicolas and Li, Shuhao and Raskin, Jean-Fran{\c{c}}ois and Stoelinga, Mari{\"e}lle}, title = {Synthesizing controllers with bounded resources}, howpublished = {Deliverable QUASIMODO~3.4 (ICT-FP7-STREP-214755)}, year = 2010, month = jan }

@article{LS-ipl10, publisher = {Elsevier Science Publishers}, journal = {Information Processing Letters}, author = {Libkin, Leonid and Sirangelo, Cristina}, title = {Disjoint pattern matching and implication in strings}, volume = 110, number = 4, pages = {143-147}, year = 2010, month = jan, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-ipl10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-ipl10.pdf}, doi = {10.1016/j.ipl.2009.11.009}, abstract = {We deal with the problem of deciding whether a given set of string patterns implies the presence of a fixed pattern. While checking whether a set of patterns occurs in a string is solvable in polynomial time, this implication problem is well known to be intractable. Here we consider a version of the problem when patterns in the set are required to be disjoint. We show that for such a version of the problem the situation is reversed: checking whether a set of patterns occurs in a string is NP-complete, but the implication problem is solvable in polynomial time.} }

@mastersthesis{sankur-master, author = {Sankur, Ocan}, title = {Model-checking robuste des automates temporis{\'e}s \textit{via} les machines {\`a} canaux}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2010}, month = sep, url = {http://www.lsv.fr/Publis/PAPERS/PDF/sankur-m2.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/sankur-m2.pdf} }

@mastersthesis{soulat-master, author = {Soulat, Romain}, title = {Am{\'e}liorations algorithmiques d'un moteur de model-checking et {\'e}tudes de cas}, school = {{M}aster 2 {R}echerche {I}nformatique {P}aris {S}ud~11}, type = {Rapport de {M}aster}, year = {2010}, month = sep, url = {http://www.lsv.fr/Publis/PAPERS/PDF/soulat-m2.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/soulat-m2.pdf} }

@mastersthesis{boiret-master, author = {Boiret, Adrien}, title = {Grammaires context-free pour les arbres sans rang}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2010}, month = sep, url = {http://www.lsv.fr/Publis/PAPERS/PDF/boiret-m2.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/boiret-m2.pdf} }

@mastersthesis{dimino-master, author = {Dimino, J{\'e}r{\'e}mie}, title = {Sur les arbres de rang non born{\'e} avec donn{\'e}es}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2010}, month = sep, url = {http://www.lsv.fr/Publis/PAPERS/PDF/dimino-m2.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/dimino-m2.pdf} }

@mastersthesis{monmege-master, author = {Monmege, Benjamin}, title = {Propri{\'e}t{\'e}s quantitatives des mots et des arbres~-- Applications aux langages~{XML}}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2010}, month = sep, url = {http://www.lsv.fr/Publis/PAPERS/PDF/monmege-m2.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/monmege-m2.pdf} }

@inproceedings{ABMG-vldb10, address = {Singapore}, month = sep, year = 2010, volume = 3, series = {Proceedings of the {VLDB} Endowment}, publisher = {ACM Press}, editor = {Chen, Yi and Tay, Y.C.}, acronym = {{VLDB}'10}, booktitle = {{P}roceedings of the 36th {I}nternational {C}onference on {V}ery {L}arge {D}ata {B}ases ({VLDB}'10)}, author = {Abiteboul, Serge and Bourhis, Pierre and Marinoiu, Bogdan and Galland, Alban}, title = {{AXART}~-- {E}nabling Collaborative Work with {AXML} Artifacts}, pages = {1553-1556}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABMG-vldb10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABMG-vldb10.pdf}, abstract = {The workflow models have been essentially operation-centric for many years, ignoring almost completely the data aspects. Recently, a new paradigm of data-centric workflows, called \emph{business artifacts}, has been introduced by Nigam and Caswell. We follow this approach and propose a model where artifacts are XML documents that evolve in time due to interactions with their environment, i.e. human users or Web services. This paper proposes the AXART system as a distributed platform for collaborative work that harnesses the power of our model. We will illustrate AXART with an example taken from the movie industry. Indeed, applying for a role in a film is a typical collaborative process that involves various participants, inside and outside the film company. The demonstration scenario considers both standard workflow process and dynamic workflow modifications, based on two extension mechanisms: workflow specialization and workflow exception. The workflows, modeled using artifacts, are supported by the AXART system by combining techniques specific to active documents, like view maintenance, with security techniques to manage access rights.} }

@inproceedings{GAMS-wsdm10, address = {New~York, New~York, USA}, month = feb, year = 2010, publisher = {ACM Press}, editor = {Davison, Brian D. and Suel, Torsten and Craswell, Nick and Liu, Bing}, acronym = {{WSDM}'10}, booktitle = {{P}roceedings of the 3rd {I}nternational {C}onference on {W}eb {S}earch and {W}eb {D}ata {M}ining ({WSDM}'10)}, author = {Galland, Alban and Abiteboul, Serge and Marian, Am{\'e}lie and Senellart, Pierre}, title = {Corroborating information from disagreeing views}, pages = {131-140}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/GAMS-wsdm10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GAMS-wsdm10.pdf}, doi = {10.1145/1718487.1718504}, abstract = {We consider a set of views stating possibly conflicting facts. Negative facts in the views may come, e.g., from functional dependencies in the underlying database schema. We want to predict the truth values of the facts. Beyond simple methods such as voting (typically rather accurate), we explore techniques based on {"}corroboration{"}, i.e., taking into account trust in the views. We introduce three fixpoint algorithms corresponding to different levels of complexity of an underlying probabilistic model. They all estimate both truth values of facts and trust in the views. We present experimental studies on synthetic and real-world data. This analysis illustrates how and in which context these methods improve corroboration results over baseline methods. We believe that corroboration can serve in a wide range of applications such as source selection in the semantic Web, data quality assessment or semantic annotation cleaning in social networks. This work sets the bases for a wide range of techniques for solving these more complex problems.} }

@inproceedings{BHB-sbmf10, address = {}, month = nov, year = 2010, volume = 6527, series = {Lecture Notes in Computer Science}, editor = {Davies, Jim and Silva, Leila and da~Silva Sim{\~a}o, Adenilso}, publisher = {Springer}, acronym = {{SBMF}'10}, booktitle = {{R}evised {S}elected {P}apers of the 13th {B}razilian {S}ymposium on {F}ormal {M}ethods ({SBMF}'10)}, author = {Bauer, Sebastian S. and Hennicker, Rolf and Bidoit, Michel}, title = {A~Modal Interface Theory with Data Constraints}, pages = {80-95}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHB-sbmf10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHB-sbmf10.pdf}, doi = {10.1007/978-3-642-19829-8_6}, abstract = {For the design of component-based software, the behavioral specification of component interfaces is crucial. We propose an extension of the theory of modal I{\slash}O-transition systems by Larsen \textit{et~al.} to cope with both control flow and data states of reactive components at the same time. In our framework, transitions model incoming or outgoing operation calls which are constrained by pre- and postconditions expressing the mutual assumptions and guarantees of the receiver and the sender of a message. We define a new interface theory by adapting synchronous composition, modal refinement and modal compatibility to the case of modal I{\slash}O-transition systems with data constraints. We show that in this formalism modal compatibility is preserved by refinement and modal refinement is preserved by composition which are basic requirements for any interface theory.} }

@inproceedings{bbcks-icgt10, address = {Enschede, The Netherlands}, month = sep # {-} # oct, year = 2010, volume = 6372, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Ehrig, Hartmut and Rensink, Arend and Rozenberg, Grzegorz and Sch{\"u}rr, Andy}, acronym = {{ICGT}'10}, booktitle = {{P}roceedings of the 5th {I}nternational {C}onference on {G}raph {T}ransformations ({ICGT}'10)}, author = {Baldan, Paolo and Bruni, Alessandro and Corradini, Andrea and K{\"o}nig, Barbara and Schwoon, Stefan}, title = {On the Computation of {M}c{M}illan's Prefix for Contextual Nets and Graph Grammars}, pages = {91-106}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/bbcks-icgt10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bbcks-icgt10.pdf}, doi = {10.1007/978-3-642-15928-2_7}, abstract = {In recent years, a research thread focused on the use of the unfolding semantics for verification purposes. This started with a paper by McMillan, which devises an algorithm for constructing a finite complete prefix of the unfolding of a safe Petri net, providing a compact representation of the reachability graph. The extension to contextual nets and graph transformation systems is far from being trivial because events can have multiple causal histories. Recently, we proposed an abstract algorithm that generalizes McMillan's construction to bounded contextual nets without resorting to an encoding into plain P\slash T nets. Here, we provide a more explicit construction that renders the algorithm effective. To allow for an inductive definition of concurrency, missing in the original proposal and essential for an efficient unfolding procedure, the key intuition is to associate histories not only with events, but also with places. Additionally, we outline how the proposed algorithm can be extended to graph transformation systems, for which previous algorithms based on the encoding of read arcs would not be applicable.} }

@article{BS-lmcs10, journal = {Logical Methods in Computer Science}, author = {Boja{\'n}czyk, Miko{\l}aj and Segoufin, Luc}, title = {Tree Languages Defined in First-Order Logic with One Quantifier Alternation}, volume = 6, number = {4:1}, nopages = {}, month = oct, year = 2010, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-lmcs10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-lmcs10.pdf}, doi = {10.2168/LMCS-6(4:1)2010}, abstract = {We study tree languages that can be defined in~\(\Delta_{2}\). These are tree languages definable by a first-order formula whose quantifier prefix is \(\exists^{*}\forall^{*}\), and simultaneously by a first-order formula whose quantifier prefix is \(\forall^{*}\exists^{*}\). For the quantifier free part we consider two signatures, either the descendant relation alone or together with the lexicographical order relation on nodes. We provide an effective characterization of tree and forest languages definable in~\(\Delta_{2}\). This characterization is in terms of algebraic equations. Over words, the class of word languages definable in~\(\Delta_{2}\) forms a robust class, which was given an effective algebraic characterization by Pin and Weil.} }

@article{BLPS-jacm10, publisher = {ACM Press}, journal = {Journal of the~{ACM}}, author = {Barcel{\'o}, Pablo and Libkin, Leonid and Poggi, Antonella and Sirangelo, Cristina}, title = {{XML} with incomplete information}, volume = {58}, number = {1}, year = {2010}, month = dec, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BLPS-jacm10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BLPS-jacm10.pdf}, doi = {10.1145/1870103.1870107} }

@article{LBDLNP-fmsd2010, publisher = {Springer}, journal = {Formal Methods in System Design}, author = {Li, Shuhao and Balaguer, Sandie and David, Alexandre and Larsen, Kim G. and Nielsen, Brian and Pusinskas, Saulius}, title = {Scenario-based verification of real-time systems using {\textsc{Uppaal}}}, year = {2010}, month = nov, volume = {37}, number = {2-3}, pages = {200-264}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LBDLNP-fmsd2010.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LBDLNP-fmsd2010.pdf}, doi = {10.1007/s10703-010-0103-z}, abstract = {This article proposes two approaches to tool-supported automatic verification of dense real-time systems against scenario-based requirements, where a system is modeled as a network of timed automata (TAs) or as a set of driving live sequence charts (LSCs), and a requirement is specified as a separate monitored LSC chart. We make timed extensions to a kernel subset of the LSC language and define a trace-based semantics. By translating a monitored LSC chart to a behavior-equivalent observer TA and then non-intrusively composing this observer with the original TA-modeled real-time system, the problems of scenario-based verification reduce to computation tree logic (CTL) real-time model checking problems. When the real-time system is modeled as a set of driving LSC charts, we translate these driving charts and the monitored chart into a behavior-equivalent network of TAs by using a {"}one-TA-per-instance line{"} approach, and then reduce the problems of scenario-based verification also to CTL real-time model checking problems. We show how we exploit the expressivity of the TA formalism and the CTL query language of the real-time model checker Uppaal to accomplish these tasks. The proposed two approaches are implemented in the Uppaal tool and built as a tool chain, respectively. We carry out a number of experiments with both verification approaches, and the results indicate that these methods are viable, computationally feasible, and the tools are effective.} }

@article{DFGD-jancl10, publisher = {Taylor \& Francis}, journal = {Journal of Applied Non-Classical Logics}, author = {Demri, St{\'e}phane and Finkel, Alain and Goranko, Valentin and van Drimmelen, Govert}, title = {Model-checking \(\textsf{CTL}^{*}\) over Flat {P}resburger Counter Systems}, year = {2010}, volume = {20}, number = {4}, pages = {313-344}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DFGD-jancl10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DFGD-jancl10.pdf}, doi = {10.3166/jancl.20.313-344}, abstract = {This paper studies model-checking of fragments and extensions of \(\textsf{CTL}^{*}\) on infinite-state counter systems, where the states are vectors of integers and the transitions are determined by means of relations definable within Presburger arithmetic. In general, reachability properties of counter systems are undecidable, but we have identified a natural class of admissible counter systems (ACS) for which we show that the quantification over paths in \(\textsf{CTL}^{*}\) can be simulated by quantification over tuples of natural numbers, eventually allowing translation of the whole Presburger-\(\textsf{CTL}^{*}\) into Presburger arithmetic, thereby enabling effective model checking. We provide evidence that our results are close to optimal with respect to the class of counter systems described above.} }

@mastersthesis{cyriac-master, author = {Cyriac, Aiswarya}, title = {Temporal Logics for Concurrent Recursive Programs}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2010}, month = sep, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ac-m2.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ac-m2.pdf} }

@inproceedings{AC-clodem10, address = {Edinburgh, Scotland, UK}, month = jul, year = 2010, acronym = {{CL}o{D}e{M}'10}, booktitle = {{P}roceedings of the {W}orkshop on {C}omparing {L}ogical {D}ecision {M}ethods ({CL}o{D}e{M}'10)}, author = {Cyriac, Aiswarya}, title = {A~New Version of Focus Games for {LTL} Satisfiability}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ac-clodem10.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ac-clodem10.pdf} }

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

*This file was generated by
bibtex2html 1.98.*