@inproceedings{CB-post13, address = {Rome, Italy}, month = mar, year = 2013, volume = {7796}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Basin, David and Mitchell, John}, acronym = {{POST}'13}, booktitle = {{P}roceedings of the 2nd {I}nternational {C}onference on {P}rinciples of {S}ecurity and {T}rust ({POST}'13)}, author = {Cheval, Vincent and Blanchet, Bruno}, title = {Proving More Observational Equivalences with ProVerif}, pages = {226-246}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CB-post13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CB-post13.pdf}, doi = {10.1007/978-3-642-36830-1_12}, abstract = {This paper presents an extension of the automatic protocol verifier ProVerif in order to prove more observational equivalences. ProVerif can prove observational equivalence between processes that have the same structure but differ by the messages they contain. In order to extend the class of equivalences that ProVerif handles, we extend the language of terms by defining more functions (destructors) by rewrite rules. In particular, we allow rewrite rules with inequalities as side-conditions, so that we can express tests {"}if then else{"} inside terms. Finally, we provide an automatic procedure that translates a process into an equivalent process that performs as many actions as possible inside terms, to allow ProVerif to prove the desired equivalence. These extensions have been implemented in ProVerif and allow us to automatically prove anonymity in the private authentication protocol by Abadi and Fournet.} }

@inproceedings{CD-post13, address = {Rome, Italy}, month = mar, year = 2013, volume = {7796}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Basin, David and Mitchell, John}, acronym = {{POST}'13}, booktitle = {{P}roceedings of the 2nd {I}nternational {C}onference on {P}rinciples of {S}ecurity and {T}rust ({POST}'13)}, author = {Chr{\'e}tien, R{\'e}my and Delaune, St{\'e}phanie}, title = {Formal analysis of privacy for routing protocols in mobile ad~hoc networks}, pages = {1-20}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-post13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-post13.pdf}, doi = {10.1007/978-3-642-36830-1_1}, abstract = {Routing protocols aim at establishing a route between distant nodes in ad hoc networks. Secured versions of routing protocols have been proposed to provide more guarantees on the resulting routes, and some of them have been designed to protect the privacy of the users. In this paper, we propose a framework for analysing privacy-type properties for routing protocols. We use a variant of the applied-pi calculus as our basic modelling formalism. More precisely, using the notion of equivalence between traces, we formalise three security properties related to privacy, namely indistinguishability, unlinkability, and anonymity. We study the relationship between these definitions and we illustrate them using two versions of the ANODR routing protocol.} }

@article{BFHR-icomp13, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Bonnet, R{\'e}mi and Finkel, Alain and Haddad, Serge and Rosa{-}Velardo, Fernando}, title = {Ordinal Theory for Expressiveness of Well-Structured Transition Systems}, year = 2013, month = mar, volume = 224, pages = {1-22}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHR-icomp12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHR-icomp12.pdf}, doi = {10.1016/j.ic.2012.11.003}, abstract = {We characterize the importance of resources (like counters, channels, or alphabets) when measuring the expressiveness of Well-Structured Transition Systems~(WSTS). We establish, for usual classes of well partial orders, the equivalence between the existence of order reflections (non-monotonic order embeddings) and the simulations with respect to coverability languages. We show that the non-existence of order reflections can be proved by the computation of order types. This allows us to extend the current classification of WSTS, in particular solving some open problems, and to unify the existing proofs.} }

@article{BCHLR-tcs13, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {B{\'e}rard, B{\'e}atrice and Cassez, Franck and Haddad, Serge and Lime, Didier and Roux, Olivier~H.}, title = {The Expressive Power of Time {P}etri Nets}, year = 2013, month = feb, volume = 474, ftturenumber = {}, pages = {1-20}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCHLR-tcs12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCHLR-tcs12.pdf}, doi = {10.1016/j.tcs.2012.12.005}, abstract = {We investigate expressiveness questions for time Petri nets (TPNs) and some their most usefull extensions. We first introduce generalised time Petri nets (GTPNs) as an abstract model that encompasses variants of TPNs such as self modifications and read, reset and inhibitor arcs.\par We give a syntactical translation from bounded GTPNs to timed automata (TA) that generates isomorphic transition systems. We prove that the class of bounded GTPNs is stricly less expressive than TA w.r.t. weak timed bisimilarity. We prove that bounded GTPNs, bounded TPNs and TA are equally expressive w.r.t. timed language acceptance. Finally, we characterise a syntactical subclass of TA that is equally expressive to bounded GTPNs {"}\`a~la Merlin{"} w.r.t. weak timed bisimilarity. These results provide a unified comparison of the expressiveness of many variants of timed models often used in practice. It leads to new important results for TPNs. Among them are: 1-safe TPNs and bounded-TPNs are equally expressive; \(\epsilon\)-transitions strictly increase the expressive power of TPNs; self modifying nets as well as read, inhibitor and reset arcs do not add expressiveness to bounded TPNs.} }

@article{ABG-fmsd12, publisher = {Springer}, journal = {Formal Methods in System Design}, author = {Akshay, S. and Bollig, Benedikt and Gastin, Paul}, title = {Event-clock Message Passing Automata: A~Logical Characterization and an Emptiness-Checking Algorithm}, year = 2013, month = jun, volume = 42, number = {3}, pages = {262-300}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABG-fmsd12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABG-fmsd12.pdf}, doi = {10.1007/s10703-012-0179-8}, abstract = {We are interested in modeling behaviors and verifying properties of systems in which time and concurrency play a crucial role. We introduce a model of distributed automata which are equipped with event clocks as in [Alur, Fix, Henzinger. Event-clock automata: A~determinizable class of timed automata. TCS 211(1-2):253-273, 1999.], which we call Event Clock Message Passing Automata (ECMPA). To describe the behaviors of such systems we use timed partial orders (modeled as message sequence charts with timing).\par Our first goal is to extend the classical B{\"u}chi-Elgot-Trakhtenbrot equivalence to the timed and distributed setting, by showing an equivalence between ECMPA and a timed extension of monadic second-order (MSO) logic. We obtain such a constructive equivalence in two different ways: (1)~by~restricting the semantics by bounding the set of timed partial orders (2)~by~restricting the timed MSO logic to its existential fragment. We next consider the emptiness problem for ECMPA, which asks if a given ECMPA has some valid timed execution. In general this problem is undecidable and we show that by considering only bounded timed executions, we can obtain decidability. We do this by constructing a timed automaton which accepts all bounded timed executions of the ECMPA and checking emptiness of this timed automaton.} }

@article{BCH-fi12, publisher = {{IOS} Press}, journal = {Fundamenta Informaticae}, author = {Balaguer, Sandie and Chatain, {\relax Th}omas and Haar, Stefan}, title = {Building Occurrence Nets from Reveals Relations}, year = 2013, month = may, volume = 123, number = 3, pages = {245-272}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCH-fi12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCH-fi12.pdf}, doi = {10.3233/FI-2013-809}, abstract = {Occurrence nets are a well known partial order model for the concurrent behavior of Petri nets. The causality and conflict relations between events, which are explicitly represented in occurrence nets, induce logical dependencies between event occurrences: the occurrence of an event~\(e\) in a run implies that all its causal predecessors also occur, and that no event in conflict with~\(e\) occurs. But these structural relations do not express all the logical dependencies between event occurrences in maximal runs: in particular, the occurrence of~\(e\) in any maximal run may imply the occurrence of another event that is not a causal predecessor of~\(e\), in that run. The \emph{reveals} relation has been introduced to express this dependency between two events. Here we generalize the reveals relation to express more general dependencies, involving more than two events, and we introduce ERL logic to express them as boolean formulas. Finally we answer the synthesis problem that arises: given an ERL formula~\(\varphi\), is there an occurrence net~\(\mathcal{N}\) such that \(\varphi\)~describes exactly the dependencies between the events of~\(\mathcal{N}\)?} }

@article{GS-tocl12, publisher = {ACM Press}, journal = {ACM Transactions on Computational Logic}, author = {Gastin, Paul and Sznajder, Nathalie}, title = {Fair Synthesis for Asynchronous Distributed Systems}, nopages = {}, volume = 14, number = {2:9}, month = jun, year = 2013, url = {http://www.lsv.fr/Publis/PAPERS/PDF/GS-tocl12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GS-tocl12.pdf}, doi = {10.1145/2480759.2480761}, abstract = {We study the synthesis problem in an asynchronous distributed setting: a finite set of processes interact locally with an uncontrollable environment and communicate with each other by sending signals---actions controlled by a sender process and that are immediately received by the target process. The fair synthesis problem is to come up with a local strategy for each process such that the resulting fair behaviors of the system meet a given specification. We consider external specifications satisfying some natural closure properties related to the architecture. We present this new setting for studying the fair synthesis problem for distributed systems, and give decidability results for the subclass of networks where communications happen through a strongly connected graph. We claim that this framework for distributed synthesis is natural, convenient and avoids most of the usual sources of undecidability for the synthesis problem. Hence, it may open the way to a decidable theory of distributed synthesis.} }

@article{BS-fmsd2012, publisher = {Springer}, journal = {Formal Methods in System Design}, author = {Bertrand, Nathalie and Schnoebelen, {\relax Ph}ilippe}, title = {Computable fixpoints in well-structured symbolic model checking}, pages = {233-267}, volume = 43, number = 2, month = oct, year = 2013, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-fmsd12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-fmsd12.pdf}, doi = {10.1007/s10703-012-0168-y}, abstract = {We prove a general finite-time convergence theorem for fixpoint expressions over a well-quasi-ordered set. This has immediate applications for the verification of well-structured systems, where a main issue is the computability of fixpoint expressions, and in particular for game-theoretical properties and probabilistic systems where nesting and alternation of least and greatest fixpoints are common.} }

@incollection{HM-lncis433, author = {Haar, Stefan and Masopust, Tom{\'a}{\v{s}}}, title = {Languages, Decidability, and Complexity}, booktitle = {Control of Discrete-Event Systems~-- Automata and {P}etri Net Perspectives}, editor = {Seatzu, Carla and Silva, Manuel and van Schuppen, Jan H.}, year = {2013}, pages = {23-43}, publisher = {Springer}, series = {Lecture Notes in Control and Information Sciences}, volume = 433, doi = {10.1007/978-1-4471-4276-8_2}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/HM-lncis433.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HM-lncis433.pdf} }

@incollection{HS-lncis433, author = {Haar, Stefan and Fabre, {\'E}ric}, title = {Diagnosis with {P}etri Net Unfoldings}, booktitle = {Control of Discrete-Event Systems~-- Automata and {P}etri Net Perspectives}, editor = {Seatzu, Carla and Silva, Manuel and van Schuppen, Jan H.}, year = {2013}, pages = {301-318}, publisher = {Springer}, series = {Lecture Notes in Control and Information Sciences}, volume = 433, doi = {10.1007/978-1-4471-4276-8_15}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/HS-lncis433.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HS-lncis433.pdf} }

@article{AFS-fmsd12, publisher = {Springer}, journal = {Formal Methods in System Design}, author = {Andr{\'e}, {\'E}tienne and Fribourg, Laurent and Sproston, Jeremy}, title = {An~Extension of the Inverse Method to Probabilistic Timed Automata}, year = 2013, month = apr, volume = 42, number = 2, pages = {119-145}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AFS-fmsd12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AFS-fmsd12.pdf}, doi = {10.1007/s10703-012-0169-x}, abstract = {Probabilistic timed automata can be used to model systems in which probabilistic and timing behaviour coexist. Verification of probabilistic timed automata models is generally performed with regard to a single reference valuation pi0 of the timing parameters. Given such a parameter valuation, we present a method for obtaining automatically a constraint~\(K_0\) on timing parameters for which the reachability probabilities (1)~remain invariant and (2)~are equal to the reachability probabilities for the reference valuation. The method relies on parametric analysis of a non-probabilistic version of the probabilistic timed automata model using the {"}inverse method{"}. The method presents the following advantages. First, since \(K_0\) corresponds to a dense domain around pi0 on which the system behaves uniformly, it gives us a measure of robustness of the system. Second, it allows us to obtain a valuation satisfying \(K_0\) which is as small as possible while preserving reachability probabilities, thus making the probabilistic analysis of the system easier and faster in practice. We provide examples of the application of our technique to models of randomized protocols, and introduce an extension of the method allowing the generation of a {"}probabilistic cartography{"} of a system.} }

@article{BCD-tocl12, publisher = {ACM Press}, journal = {ACM Transactions on Computational Logic}, author = {Baudet, Mathieu and Cortier, V{\'e}ronique and Delaune, St{\'e}phanie}, title = {{YAPA}: A~generic tool for computing intruder knowledge}, year = 2013, month = feb, nopages = {}, number = {1:4}, volume = 14, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCD-tocl12.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCD-tocl12.pdf}, doi = {10.1145/2422085.2422089}, abstract = {Reasoning about the knowledge of an attacker is a necessary step in many formal analyses of security protocols. In the framework of the applied pi calculus, as in similar languages based on equational logics, knowledge is typically expressed by two relations: deducibility and static equivalence. Several decision procedures have been proposed for these relations under a variety of equational theories. However, each theory has its particular algorithm, and none has been implemented so far. \par We provide a generic procedure for deducibility and static equivalence that takes as input any convergent rewrite system. We show that our algorithm covers most of the existing decision procedures for convergent theories. We also provide an efficient implementation, and compare it briefly with the tools ProVerif and KiSs.} }

@book{JGL-topology, author = {Goubault{-}Larrecq, Jean}, title = {Non-{H}ausdorff Topology and Domain Theory---Selected Topics in Point-Set Topology}, publisher = {Cambridge University Press}, series = {New Mathematical Monographs}, volume = {22}, year = {2013}, month = mar, url = {http://www.cambridge.org/9781107034136}, isbn = {9781107034136} }

@inproceedings{GLS-rr13, address = {Mannheim, Germany}, month = jul, year = 2013, volume = 7994, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Faber, Wolfgang and Lembo, Domenico}, acronym = {{WRRS}'13}, booktitle = {{P}roceedings of the 7th {I}nternational {C}onference on {W}eb {R}easoning and {R}ule {S}ystems ({WRRS}'13)}, author = {Gheerbrant, Am{\'e}lie and Libkin, Leonid and Sirangelo, Cristina}, affiliaton = {Scotland, University of Edinburgh, School of Informatics and Scotland, University of Edinburgh, School of Informatics and France, ENS Cachan \& CNRS \& INRIA, LSV[Dahu]}, title = {Reasoning About Pattern-Based {XML} Queries}, pages = {4-18}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/GLS-rr13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLS-rr13.pdf}, doi = {10.1007/978-3-642-39666-3_2}, abstract = {We survey results about static analysis of pattern-based queries over XML documents. These queries are analogs of conjunctive queries, their unions and Boolean combinations, in which tree patterns play the role of atomic formulae. As in the relational case, they can be viewed as both queries and incomplete documents, and thus static analysis problems can also be viewed as finding certain answers of queries over such documents. We look at satisfiability of patterns under schemas, containment of queries for various features of XML used in queries, finding certain answers, and applications of pattern-based queries in reasoning about schema mappings for data exchange.} }

@incollection{AV-buneman13, noaddress = {}, month = sep, year = 2013, volume = 8000, series = {Lecture Notes in Computer Science}, editor = {Tannen, Val and Wong, Limsoon and Libkin, Leonid and Fan, Wenfei and Tan, Wang-Chiew and Fourman, Michael}, publisher = {Springer}, booktitle = {{I}n~{S}earch of {E}legance in the {T}heory and {P}ractice of {C}omputation~-- {E}ssays {D}edicated to {P}eter~{B}uneman}, author = {Abiteboul, Serge and Vianu, Victor}, title = {Models for Data-Centric Workflows}, pages = {1-12}, doi = {10.1007/978-3-642-41660-6_1}, abstract = {We present two models for data-centric workflows: the first based on business artifacts and the second on Active XML. We then compare the two models and argue that Active XML is strictly more expressive, based on a natural semantics and choice of observables. Finally, we mention several verification results for the two models.} }

@inproceedings{AAMST-sigmod13, address = {New~York, New~York, USA}, month = jun, year = 2013, publisher = {ACM Press}, editor = {Ross, Kenneth A. and Srivastava, Divesh and Papadias, Dimitris}, acronym = {{SIGMOD}'13}, booktitle = {{P}roceedings of the {ACM} {SIGMOD} {I}nternaitonal {C}onference on {M}anagement of {D}ata ({SIGMOD}'13)}, author = {Abiteboul, Serge and Antoine, {\'E}milien and Miklau, Gerome and Stoyanovich, Julia and Testard, Jules}, title = {Rule-based application development using Webdamlog}, pages = {965-968}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AAMST-sigmod13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AAMST-sigmod13.pdf}, doi = {10.1145/2463676.2465251}, abstract = {We present the WebdamLog system for managing distributed data on the Web in a peer-to-peer manner. We demonstrate the main features of the system through an application called Wepic for sharing pictures between attendees of the sigmod conference. Using Wepic, the attendees will be able to share, download, rate and annotate pictures in a highly decentralized manner. We show how WebdamLog handles heterogeneity of the devices and services used to share data in such a Web setting. We exhibit the simple rules that define the Wepic application and show how to easily modify the Wepic application.} }

@inproceedings{BD-csr13, address = {Ekaterinburg, Russia}, month = jun, year = 2013, volume = {7913}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Bulatov, Andrei A. and Shur, Arseny M.}, acronym = {{CSR}'13}, booktitle = {{P}roceedings of the 8th {I}nternational {C}omputer {S}cience {S}ymposium in {R}ussia ({CSR}'13)}, author = {Bansal, Kshitij and Demri, St{\'e}phane}, title = {Model-checking bounded multi-pushdown systems}, pages = {405-417}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BD-csr13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BD-csr13.pdf}, doi = {10.1007/978-3-642-38536-0_35}, abstract = {We provide complexity characterizations of model checking multi-pushdown systems. We consider three standard notions for boundedness: context boundedness, phase boundedness and stack ordering. The logical formalism is a linear-time temporal logic extending well-known logic \texttt{CaRet} but dedicated to multi-pushdown systems in which abstract operators are parameterized by stacks. We show that the problem is ExpTime-complete for context-bounded runs and unary encoding of the number of context switches; we also prove that the problem is 2ExpTime-complete for phase-bounded runs and unary encoding of the number of phase switches. In both cases, the value~\(k\) is given as an input, which makes a substantial difference in the complexity.} }

@misc{cassting-D41, author = {Markey, Nicolas and Larsen, Kim G. and Skou, Arne and Lux, Daniel and Rozenkilde, Jesper and Pedersen, Keld L. and S{\o}rensen, Susanne M.}, title = {Description of case studies}, howpublished = {Cassting deliverable~D4.1 (FP7-ICT-601148)}, month = oct, year = {2013}, note = {19~pages}, type = {Contract Report}, nourlnote = {confidentiel} }

@misc{cassting-D51, author = {Valette, Sophie and Markey, Nicolas}, title = {Cassting website}, howpublished = {Cassting deliverable~D6.1 (FP7-ICT-601148)}, month = jun, year = {2013}, note = {10~pages}, type = {Contract Report}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/cassting-d51.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/cassting-d51.pdf} }

@misc{cassting-D61, author = {Valette, Sophie and Markey, Nicolas}, title = {Minutes of the Kick-Off Meeting}, howpublished = {Cassting deliverable~D6.1 (FP7-ICT-601148)}, month = apr, year = {2013}, note = {9~pages}, type = {Contract Report}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/cassting-d61.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/cassting-d61.pdf} }

@phdthesis{chatain-HDR13, author = {Chatain, {\relax Th}omas}, title = {Concurrency in Real-Time Distributed Systems, from Unfoldings to Implementability}, year = 2013, month = dec, type = {M{\'e}moire d'habilitation}, school = {{\'E}cole Normale Sup{\'e}rieure de Cachan, France}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/hdr-chatain13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/hdr-chatain13.pdf} }

@phdthesis{crodriguez-phd2013, author = {Rodr{\'\i}guez, C{\'e}sar}, title = {Verification Based on Unfoldings of {P}etri Nets with Read Arcs}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2013, month = dec, url = {http://www.lsv.fr/Publis/PAPERS/PDF/cr-phd13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/cr-phd13.pdf} }

@misc{impro-D31, author = {B{\'e}rard, B{\'e}atrice and Bouyer, Patricia and Larsen, Kim G. and Markey, Nicolas and Mullins, John and Sankur, Ocan and Sassolas, Mathieu and Thrane, Claus}, title = {Measuring the robustness}, howpublished = {Deliverable ImpRo~3.1, (ANR-10-BLAN-0317)}, month = jan, year = {2013}, note = {59~pages}, type = {Contract Report}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d31.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d31.pdf} }

@misc{impro-D51, author = {Bouyer, Patricia and Faucou, S{\'e}bastien and Haar, Stefan and Jovanivi{\'c}, Aleksandra and Lime, Didier and Markey, Nicolas and Roux, Olivier H. and Sankur, Ocan}, title = {Control tasks for Timed System; Robustness issues}, howpublished = {Deliverable ImpRo~5.1, (ANR-10-BLAN-0317)}, month = jan, year = {2013}, note = {34~pages}, type = {Contract Report}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d51.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d51.pdf} }

@phdthesis{schwoon-HDR13, author = {Schwoon, Stefan}, title = {Efficient verification of sequential and concurrent systems}, year = 2013, month = dec, type = {M{\'e}moire d'habilitation}, school = {{\'E}cole Normale Sup{\'e}rieure de Cachan, France}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/hdr-schwoon13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/hdr-schwoon13.pdf} }

@phdthesis{eantoine-phd2013, author = {Antoine, {\'E}milien}, title = {Distributed data management with a declarative rule-based language: \emph{Webdamlog}}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2013, month = dec, url = {http://www.lsv.fr/Publis/PAPERS/PDF/eantoine-phd13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/eantoine-phd13.pdf} }

@article{CS-lmcs13, journal = {Logical Methods in Computer Science}, author = {ten~Cate, Balder and Segoufin, Luc}, title = {Unary negation}, volume = 9, number = {3:25}, month = sep, year = 2013, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-lmcs13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-lmcs13.pdf}, doi = {10.2168/LMCS-9(3:25)2013}, abstract = {We study fragments of first-order logic and of least fixed point logic that allow only unary negation: negation of formulas with at most one free variable. These logics generalize many interesting known formalisms, including modal logic and the \(\mu\)-calculus, as well as conjunctive queries and monadic Datalog. We show that satisfiability and finite satisfiability are decidable for both fragments, and we pinpoint the complexity of satisfiability, finite satisfiability, and model checking. We also show that the unary negation fragment of first-order logic is model-theoretically very well behaved. In particular, it enjoys Craig Interpolation and the Projective Beth Property.} }

@inproceedings{BC-fossacs13, address = {Rome, Italy}, month = mar, year = 2013, volume = {7794}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Pfenning, Frank}, acronym = {{FoSSaCS}'13}, booktitle = {{P}roceedings of the 16th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'13)}, author = {Bonnet, R{\'e}mi and Chadha, Rohit}, title = {Bounded Context-Switching and Reentrant Locking}, pages = {65-80}, doi = {10.1007/978-3-642-37075-5_5}, abstract = {Reentrant locking is a \emph{recursive locking} mechanism which allows a thread in a multi-threaded program to acquire the reentrant lock multiple times. The thread must release this lock an equal number of times before another thread can acquire this lock. We consider the control state reachability problem for recursive multi-threaded programs synchronizing via a finite number of reentrant locks. Such programs can be abstracted as multi-pushdown systems with a finite number of counters. The pushdown stacks model the call stacks of the threads and the counters model the reentrant locks. The control state reachability problem is already undecidable for non-reentrant locks. As a consequence, for non-reentrant locks, under-approximation techniques which restrict the search space have gained traction. One popular technique is to limit the number of context switches. Our main result is that the problem of checking whether a control state is reachable within a bounded number of context switches is decidable for recursive multi-threaded programs synchronizing via a finite number of reentrant locks if we restrict the lock-usage to contextual locking: a release of an instance of reentrant lock can only occur if the instance was acquired before in the same procedure and each instance of a reentrant lock acquired in a procedure call must be released before the procedure returns. The decidability is obtained by a reduction to the reachability problem of Vector Addition Systems with States~(VASS).} }

@article{BCMV-lmcs13, journal = {Logical Methods in Computer Science}, author = {Bonnet, R{\'e}mi and Chadha, Rohit and Madhusudan, P. and Viswanathan, Mahesh}, title = {Reachability under contextual locking}, volume = 9, number = {3:21}, month = sep, year = 2013, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCMV-lmcs13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCMV-lmcs13.pdf}, doi = {10.2168/LMCS-9(3:21)2013}, abstract = {The pairwise reachability problem for a multi-threaded program asks, given control locations in two threads, whether they can be simultaneously reached in an execution of the program. The problem is important for static analysis and is used to detect statements that are concurrently enabled. This problem is in general undecidable even when data is abstracted and when the threads (with recursion) synchronize only using a finite set of locks. Popular programming paradigms that limit the lock usage patterns have been identified under which the pairwise reachability problem becomes decidable. In this paper, we consider a new natural programming paradigm, called contextual locking, which ties the lock usage to calling patterns in each thread: we assume that locks are released in the same context that they were acquired and that every lock acquired by a thread in a procedure call is released before the procedure returns. Our main result is that the pairwise reachability problem is polynomial-time decidable for this new programming paradigm as well. The problem becomes undecidable if the locks are reentrant; reentrant locking is a recursive locking mechanism which allows a thread in a multi-threaded program to acquire the reentrant lock multiple times.} }

@proceedings{BF-formats2013, title = {{P}roceedings of the 11th {I}nternational {C}onference on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'13)}, booktitle = {{P}roceedings of the 11th {I}nternational {C}onference on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'13)}, acronym = {{FORMATS}'13}, editor = {Braberman, V{\'\i}ctor and Fribourg, Laurent}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = 8053, url = {http://link.springer.com/978-3-642-40228-9}, year = 2013, month = aug, address = {Buenos Aires, Argentina} }

@article{BC-lmcs13, journal = {Logical Methods in Computer Science}, author = {Balaguer, Sandie and Chatain, {\relax Th}omas}, title = {Avoiding Shared Clocks in Networks of Timed Automata}, volume = 9, number = {4:13}, nopages = {}, year = 2013, month = nov, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BC-lmcs13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BC-lmcs13.pdf}, doi = {10.2168/LMCS-9(4:13)2013}, abstract = {Networks of timed automata~(NTA) are widely used to model distributed real-time systems. Quite often in the literature, the automata are allowed to share clocks. This is a problem when one considers implementing such model in a distributed architecture, since reading clocks a priori requires communications which are not explicitly described in the model. We focus on the following question: given a NTA \(A_{1} \parallel A_{2}\) where \(A_{2}\) reads some clocks reset by~\(A_{1}\), does there exist a NTA \(A'_{1} \parallel A'_{2}\) without shared clocks with the same behavior as the initial NTA? For this, we allow the automata to exchange information during synchronizations only. We discuss a formalization of the problem and give a criterion using the notion of contextual timed transition system, which represents the behavior of~\(A_{2}\) when in parallel with~\(A_{1}\). Finally, we effectively build \(A'_{1} \parallel A'_{2}\) when it exists.} }

@article{CD-pourlascience13, publisher = {Belin}, journal = {Pour La Science}, author = {Chr{\'e}tien, R{\'e}my and Delaune, St{\'e}phanie}, title = {La protection des informations sensibles}, volume = {433}, month = nov, year = 2013, pages = {70-77}, url = {http://www.pourlascience.fr/ewb_pages/a/article-la-protection-des-informations-sensibles-32228.php} }

@phdthesis{monmege-phd2013, author = {Monmege, Benjamin}, title = {Sp{\'e}cification et v{\'e}rification de propri{\'e}t{\'e}s quantitatives~: expressions, logiques, et automates}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2013, month = oct, url = {http://www.lsv.fr/Publis/PAPERS/PDF/monmege-phd13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/monmege-phd13.pdf} }

@book{FS-book13, author = {Fribourg, Laurent and Soulat, Romain}, title = {Control of Switching Systems by Invariance Analysis: Application to Power Electronics}, publisher = {Wiley-ISTE}, year = 2013, month = jul, isbn = {9781848216068}, note = {144~pages}, url = {http://www.iste.co.uk/index.php?f=a&ACTION=View&id=684}, abstract = {This book presents correct-by-design control techniques for switching systems, using different methods of stability analysis. Switching systems are increasingly used in the electronics and mechanical industries; in power electronics and the automotive industry, for example. This is due to their flexibility and simplicity in accurately controlling industrial mechanisms. By adopting appropriate control rules, we can steer a switching system to a region centered at a desired equilibrium point, while avoiding {"}unsafe{"} regions of parameter saturation.\par The authors explain various correct-by-design methods for control synthesis, using different methods of stability and invariance analysis. They also provide several applications of these methods to industrial examples of power electronics.} }

@inproceedings{BL-ewili13, address = {Toulouse, France}, month = aug, year = 2013, noeditor = {}, acronym = {{EW}i{L}i'13}, booktitle = {{P}roceedings of the 3rd {E}mbedded {O}perating {S}ystems {W}orkshop ({EW}i{L}i'13)}, author = {Benedetto, Salvatore and Lipari, Giuseppe}, title = {{{ADOK}: A~Minimal Object Oriented Real-Time Operating System in~{C++}}}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BL-ewili13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BL-ewili13.pdf}, abstract = {Most embedded software is currently developed using the C programming language, even though its low level of abstraction requires a lot of effort to the programmer. The C++ language is a better choice because: it raises the level of abstraction; it is strongly typed, so it prevents many common programming mistakes; it can be made as efficient as C through fine-grained customisation of memory mechanisms; it can be easily adapted to domain-specific needs. In addition, recent compilers have grown in maturity and performance, and the new standard considerably improves the language by introducing new concepts and an easier syntax.\par In this paper we present ADOK, a minimal Real-Time Operating System entirely written in C++ with the exception of a few lines of assembler code. It directly offers a C++ interface to the developer, and it provides a flexible scheduling framework which allows the developer to customise the scheduling to its needs. In particular, we implement a two-level scheduler based on Earliest Deadline First, the Stack Resource Policy protocol for sharing resources and support for mode changes. We demonstrate through examples and a small case-study that ADOK can substantially improve productivity without sacrificing on performance.} }

@inproceedings{BLBL-iceac13, address = {Istanbul, Turkey}, month = dec, year = 2013, publisher = {{IEEE} Circuits and Systems Society}, noeditor = {}, acronym = {{ICEAC}'13}, booktitle = {{P}roceedings of the 4th {I}nternational {C}onference on {E}nergy-{A}ware {C}omputing {S}ystems and {A}pplications ({ICEAC}'14),}, author = {Bambagini, Mario and Lelli, Juri and Buttazzo, Giorgio and Lipari, Giuseppe}, title = {On the Energy-Aware Partitioning of Real-Time Tasks on Homogeneous Multi-Processor Systems}, pages = {69-74}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BLBL-iceac13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BLBL-iceac13.pdf}, doi = {10.1109/ICEAC.2013.6737640}, abstract = {In high-performance computing systems, efficient energy management is a key feature for keeping energy bills low and avoiding thermal dissipation problems, as well as for controlling the application performance. This paper considers the problem of partitioning and scheduling a set of real-time tasks on a realistic hardware platform consisting of a number of homogeneous processors. Several well-known heuristics are compared to identify the approach that better reduces the overall energy consumption of the entire system. Despite the actual state of art, the approach which minimizes the number of active cores is the most energy efficient.} }

@inproceedings{PLML-rtlws2013, address = {Lugano-Manno, Switzerland}, month = oct, year = 2013, publisher = {Open Source Automation Development Lab (OSADL)}, noeditor = {}, acronym = {{RTLWS}'13}, booktitle = {{P}roceedings of the 15th {R}eal-{T}ime {L}inux {W}orkshop ({RTLWS}'13)}, author = {Parri, Andrea and Lelli, Juri and Marinoni, Mauro and Lipari, Giuseppe}, title = {Design and Implementation of the Multiprocessor Bandwidth Inheritance Protocol on {L}inux}, oldtitle = {An~implementation of the Bandwidth Inheritance Protocol in the {L}inux Kernel}, pages = {41-54}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/PLML-rtlws13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PLML-rtlws13.pdf}, abstract = {The Resource Reservation (RR) framework has been proven very effective in the joint scheduling of hard real time and soft real time application in Open Systems. A fundamental problem in this context concerns the extension of the Resource Reservation approach to systems where tasks interact through shared resources.\par The Bandwidth Inheritance (BWI) protocol was first proposed in [Lamastra~G., Lipari~G., Abeni~L.~(2001). A~bandwidth inheritance algorithm for real-time task synchronization in open systems. In:~Proc. 22nd IEEE Real-Time Systems Symposium] to preserve Bandwidth Isolation between independent groups of tasks, and to enable a schedulability analysis for hard real time tasks.\par In this paper, we present the first implementation of the BWI protocol within the Linux kernel. We describe the protocol, the way it has been implemented in Linux, and we report some early experiments to measure its overhead. Our work is based on the SCHED\_DEADLINE patch, a scheduling class for the Linux kernel that provides Resource Reservation using the Constant Bandwidth Server algorithm. The BWI implementation extends Linux's current implementation of the Priority Inheritance protocol, without affecting past design decisions. Our implementation is neutral to the underlying scheduling scheme and can be adopted in global, clustered and partitioned scheduling.\par Results show agreement with theoretical analysis, and performance{\slash}overheads comparable with the current implementation of Priority Inheritance in Linux.\par The work presented here has practical implications for applications running on Linux with SCHED\_DEADLINE scheduling policy and share resources through mutex semaphores. In fact, the protocol guarantees temporal isolation between non-interacting threads, hence real-time guarantees are possible even where no a-priori information about tasks' scheduling parameters are available.} }

@inproceedings{LGBB-burns13, address = {York, UK}, month = mar, year = 2013, editor = {Audsley, Neil and Baruah, Sanjoy}, publisher = {CreateSpace Independent Publishing Platform}, booktitle = {Real-Time Sytems: the past, the present, and the future~-- {P}roceedings of a conference organized in celebration of {P}rofessor {A}lan~{B}urns' sixtieth birthday}, author = {Lipari, Giuseppe and George, Laurent and Bini, Enrico and Bertogna, Marko}, title = {On the Average Complexity of the Processor Demand Analysis for Earliest Deadline Scheduling}, pages = {75-86}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LGBB-burns13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LGBB-burns13.pdf}, abstract = {Schedulability analysis of a set of sporadic tasks scheduled by EDF on a single processor system is a well known and solved problem: the Processor Demand Analysis is a necessary and sufficient test for EDF with pseudo-polynomial complexity. Over the years, many researchers have tried to find efficient methods for reducing the average-case running time of this test. The problem becomes relevant when doing sensitivity analysis of the worst-case execution times of the tasks: the number of constraints to check is directly linked to the complexity of the analysis. In this paper we describe the problem and present some known facts, with the aim of summarising the state of the art and stimulate research in this direction.} }

@inproceedings{LB-burns13, address = {York, UK}, month = mar, year = 2013, editor = {Audsley, Neil and Baruah, Sanjoy}, publisher = {CreateSpace Independent Publishing Platform}, booktitle = {Real-Time Sytems: the past, the present, and the future~-- {P}roceedings of a conference organized in celebration of {P}rofessor {A}lan~{B}urns' sixtieth birthday}, author = {Lipari, Giuseppe and Buttazzo, Giorgio}, title = {{Resource reservation for Mixed Criticality Systems}}, pages = {60-74}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LB-burns13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LB-burns13.pdf}, abstract = {This paper presents a reservation-based approach to schedule mixed criticality systems in a way that guarantees the schedulability of high-criticality tasks independently of the behaviour of low-criticality tasks. Two key ideas are presented: first, to reduce the system uncertainty and advance the time at which a high-criticality task reveals its actual execution time, the initial portion of its code is handled by a dedicated server with a bandwidth reserved for the worst-case, but with a shorter deadline; second, to avoid the pessimism related to off-line budget allocation, an efficient reclaiming mechanism, namely the GRUB algorithm, is used to exploit the budget left by high-criticality tasks in favor of those low-criticality tasks that can still complete within their deadline.} }

@inproceedings{SSLAF-ftscs13, address = {Queenstown, New Zealand}, month = oct, year = 2013, editor = {Artho, Cyrille and {\"O}lveczky, Peter Csaba}, acronym = {{FTSCS}'13}, booktitle = {{P}reproceedings of the 2nd {I}nternational {W}orkshop on {F}ormal {T}echniques for {S}afety-{C}ritical {S}ystems ({FTSCS}'13)}, author = {Sun, Youcheng and Soulat, Romain and Lipari, Giuseppe and Andr{\'e}, {\'E}tienne and Fribourg, Laurent}, title = {Parametric Schedulability Analysis of Fixed Priority Real-Time Distributed Systems}, pages = {179-194}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/SSLAF-ftscs13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SSLAF-ftscs13.pdf}, abstract = {In this paper, we address the problem of parametric schedulability analysis of distributed real-time systems scheduled by fixed priority. We propose two different approaches to parametric analysis. The first one is a novel analytic technique that extends single-processor sensitivity analysis to the case of distributed systems. The second approach is based on model checking of Parametric Stopwatch Automata~(PSA): we~generate a PSA model from a high-level description of the system, and then we apply the Inverse Method to obtain all possible behaviours of the system. Both techniques have been implemented in two software tools, and they have been compared with classical holistic analysis on two meaningful test cases. The results show that the analytic method provides results similar to classical holistic analysis in a very efficient way, whereas the PSA approach is slower but covers the entire space of solutions.} }

@inproceedings{BL-etfa13, address = {Cagliari, Italy}, month = sep, year = 2013, publisher = {{IEEE} Industrial Electronics Society}, noeditor = {}, acronym = {{ETFA}'13}, booktitle = {{P}roceedings of the 18th {IEEE} {I}nternational {C}onference on {E}merging {T}echnologies and {F}actory {A}utomation ({ETFA}'13)}, author = {Buttazzo, Giorgio and Lipari, Giuseppe}, title = {Ptask: An~Educational {C}~Library for Programming Real-Time Systems on Linux}, nopages = {}, doi = {10.1109/ETFA.2013.6648001}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BL-etfa13.pdf}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BL-etfa13.pdf}, abstract = {When learning real-time programming, the novice is faced with many technical difficulties due to low-level C libraries that require considerable programming effort even for implementing a simple periodic task. For example, the POSIX Real-Time standard only provides a low level notion of thread, hence programmers usually build higher level code on top of the POSIX API, every time re-inventing the wheel.\par In this paper we present a simple C library that simplifies real-time programming in Linux by hiding low-level details of task creation, allocation and synchronization, and provides utilities for more high-level functionalities, like support for mode-change and adaptive systems. The library is released as open-source and it is currently being employed to teach real-time programming in university courses in embedded systems.} }

@phdthesis{brochenin-phd2013, author = {Brochenin, R{\'e}mi}, title = {Separation Logic: Expressiveness, Complexity, Temporal Extension}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2013, month = sep, url = {http://www.lsv.fr/Publis/PAPERS/PDF/brochenin-phd13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/brochenin-phd13.pdf} }

@phdthesis{kazana-phd2013, author = {Kazana, Wojciech}, title = {Query Evaluation with Constant Delay}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2013, month = sep, url = {http://www.lsv.fr/Publis/PAPERS/PDF/kazana-phd13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/kazana-phd13.pdf} }

@inproceedings{HHMS-fsttcs13, address = {Guwahati, India}, month = dec, year = 2013, volume = {24}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Seth, Anil and Vishnoi, Nisheeth}, acronym = {{FSTTCS}'13}, booktitle = {{P}roceedings of the 33rd {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'13)}, author = {Haar, Stefan and Haddad, Serge and Melliti, Tarek and Schwoon, Stefan}, title = {Optimal Constructions for Active Diagnosis}, pages = {527-539}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/HHMS13-fsttcs.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HHMS13-fsttcs.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2013.527}, abstract = {The task of diagnosis consists in detecting, without ambiguity, occurrence of faults in a partially observed system. Depending on the degree of observability, a discrete event system may be diagnosable or not. Active diagnosis aims at controlling the system in order to make it diagnosable. Solutions have already been proposed for the active diagnosis problem, but their complexity remains to be improved. We solve here the active diagnosability decision problem and the active diagnoser synthesis problem, proving that (1)~our procedures are optimal w.r.t. to computational complexity, and (2)~the memory required for the active diagnoser produced by the synthesis is minimal. Furthermore, focusing on the minimal delay before detection, we establish that the memory required for any active diagnoser achieving this delay may be highly greater than the previous one. So we refine our construction to build with the same complexity and memory requirement an active diagnoser that realizes a delay bounded by twice the minimal delay.} }

@inproceedings{EJS-fsttcs13, address = {Guwahati, India}, month = dec, year = 2013, volume = {24}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Seth, Anil and Vishnoi, Nisheeth}, acronym = {{FSTTCS}'13}, booktitle = {{P}roceedings of the 33rd {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'13)}, author = {Esparza, Javier and Jezequel, Lo{\"\i}g and Schwoon, Stefan}, title = {Computation of summaries using net unfoldings}, pages = {225-236}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/EJS-fsttcs13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/EJS-fsttcs13.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2013.225}, abstract = {We study the following summarization problem: given a parallel composition \(A = A_1\Vert\cdots\Vert A_n\) of labelled transition systems communicating with the environment through a distinguished component \(A_i\), efficiently compute a summary~\(S_i\) such that \(E\Vert A\) and \(E\Vert S_i\) are trace-equivalent for every environment~\(E\). While \(S_i\) can be computed using elementary automata theory, the resulting algorithm suffers from the state-explosion problem. We present a new, simple but subtle algorithm based on net unfoldings, a partial-order semantics, give some experimental results using an implementation on top of Mole, and show that our algorithm can handle divergences and compute weighted summaries with minor modifications.} }

@inproceedings{RS-fsfma13, address = {Singapore}, month = jul, year = 2013, volume = 31, series = {Open Access Series in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Choppy, {\relax Ch}ristine and Sun, Jun}, acronym = {{FSFMA}'13}, booktitle = {{P}roceedings of the 1st {F}rench-{S}ingaporean {W}orkshop on {F}ormal {M}ethods and {A}pplications ({FSFMA}'13)}, author = {Rodr{\'\i}guez, C{\'e}sar and Schwoon, Stefan}, title = {An Improved Construction of {P}etri Net Unfoldings}, pages = {47-52}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/RS-fsfma13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RS-fsfma13.pdf}, doi = {10.4230/OASIcs.FSFMA.2013.47}, abstract = {Petri nets are a well-known model language for concurrent systems. The unfolding of a Petri net is an acyclic net bisimilar to the original one. Because it is acyclic, it admits simpler decision problems though it is in general larger than the net. In this paper, we revisit the problem of efficiently constructing an unfolding. We propose a new method that avoids computing the concurrency relation and therefore uses less memory than some other methods but still represents a good time-space tradeoff. We implemented the approach and report on experiments.} }

@article{HMY-jocs13, publisher = {Elsevier Science Publishers}, journal = {Journal of Computational Science}, author = {Haddad, Serge and Mokdad, Lynda and Youcef, Samir}, title = {Bounding models families for performance evaluation in composite Web services}, volume = {4}, number = {4}, year = {2013}, pages = {232-241}, month = jul, url = {http://www.lsv.fr/Publis/PAPERS/PDF/HMY-jocs13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HMY-jocs13.pdf}, doi = {10.1016/j.jocs.2011.11.003}, abstract = {One challenge of composite Web service architectures is the guarantee of the Quality of Service~(QoS). Performance evaluation of these architectures is essential but complex due to synchronizations inside the orchestration of services. We propose methods to automatically derive from the original model a family of bounding models for the composite Web response time. These models allow to find the appropriate trade-off between accuracy of the bounds and the computational complexity. The numerical results show the interest of our approach w.r.t. complexity and accuracy of the response time bounds.} }

@techreport{rr-lsv-13-13, author = {Hirschi, Lucca}, title = {R{\'e}duction d'entrelacements pour l'{\'e}quivalence de traces}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2013}, month = sep, type = {Research Report}, number = {LSV-13-13}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2013-13.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2013-13.pdf}, versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2013-13-v1.pdf, 20130910}, note = {22~pages}, abstract = {La trace \'equivalence permet notamment de mod\'eliser l'anonymat de protocoles cryptographiques. Cette propri\'et\'e est d\'ecidable pour de nombreuses classes de protocoles et quelques outils permettent de la prouver automatiquement. Mais malheureusement, tous ces outils sont tr\`es lents et peu de protocoles r\'eellement int\'eressants peuvent \^etre analys\'es dans un temps raisonnable. Ces outils doivent r\'ealiser un parcours exhaustif des traces (symboliques) possibles. Mais le parall\`ele introduit de nombreux entrelacements dont un grand nombre sont peu pertinents. Cette explosion combinatoire est une des causes de cette inefficacit\'e.\par Une optimisation dont l'id\'ee est emprunt\'ee \`a la POR (Partial Order Reduction) permet de r\'eduire significativement l'espace de recherche en reconnaissant certaines redondances entre les traces. Elle a \'et\'e d\'evelopp\'ee dans le cas des propri\'et\'es d'accessibilit\'e. L'objectif est de l'adapter au cas de l'\'equivalence, de l'automatiser, d'augmenter son champ d'action et de l'introduire dans un outil existant.} }

@inproceedings{BMS-rp13, address = {Uppsala, Sweden}, month = sep, year = 2013, volume = {8169}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Abdulla, Parosh Aziz and Potapov, Igor}, acronym = {{RP}'13}, booktitle = {{P}roceedings of the 7th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'13)}, author = {Bouyer, Patricia and Markey, Nicolas and Sankur, Ocan}, title = {Robustness in timed automata}, pages = {1-18}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-rp13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-rp13.pdf}, doi = {10.1007/978-3-642-41036-9_1}, abstract = {In this paper we survey several approaches to the robustness of timed automata, that~is, the ability of a system to resist to slight perturbations or errors. We will concentrate on robustness against timing errors which can be due to measuring errors, imprecise clocks, and unexpected runtime behaviors such as execution times that are longer or shorter than expected.\par We consider the perturbation model of guard enlargement and formulate several robust verification problems that have been studied recently, including robustness analysis, robust implementation, and robust control.} }

@inproceedings{CH-pnse13, address = {Milano, Italy}, month = jun, year = 2013, volume = 969, series = {CEUR Workshop Proceedings}, publisher = {RWTH Aachen, Germany}, editor = {Moldt, Daniel and R{\"o}lke, Heiko}, acronym = {{PNSE}'13}, booktitle = {{P}roceedings of the 7th {I}nternational {W}orkshop on {P}etri {N}ets and {S}oftware {E}ngineering ({PNSE}'13)}, author = {Chatain, {\relax Th}omas and Haar, Stefan}, title = {A~Canonical Contraction for Safe {P}etri Nets}, pages = {25-39}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CH-pnse13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CH-pnse13.pdf}, abstract = {Under maximal semantics, the occurrence of an event~\(a\) in a concurrent run of an occurrence net may imply the occurrence of other events, not causally related to~\(a\), in the same run. In recent works, we have formalized this phenomenon as the \emph{reveals} relation, and used it to obtain a contraction of sets of events called \emph{facets} in the context of occurrence nets. Here, we extend this idea to propose a canonical contraction of general safe Petri nets into pieces of partial-order behaviour which can be seen as {"}macro-transitions{"} since all their events must occur together in maximal semantics. On occurrence nets, our construction coincides with the facets abstraction. Our contraction preserves the maximal semantics in the sense that the maximal processes of the contracted net are in bijection with those of the original net.} }

@inproceedings{PHL-ictss13, address = {Istanbul, Turkey}, month = nov, year = 2013, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Yenig{\"u}n, H{\"u}sn{\"u} and Yilmaz, Cemal and Ulrich, Andreas}, acronym = {{ICTSS}'13}, booktitle = {{P}roceedings of the 25th {IFIP} {I}nternational {C}onference on {T}esting {S}oftware and {S}ystems ({ICTSS}'13)}, author = {Ponce{ }de{~}Le{\'o}n, Hern{\'a}n and Haar, Stefan and Longuet, Delphine}, title = {Unfolding-based Test Selection for Concurrent Conformance}, pages = {98-113}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-ictss13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-ictss13.pdf}, doi = {10.1007/978-3-642-41707-8_7}, abstract = {Model-based testing has mainly focused on models where currency is interpreted as interleaving (like the ioco theory for labeled transition systems), which may be too coarse when one wants concurrency to be preserved in the implementation. In order to test such concurrent systems, we choose to use Petri nets as specifications and define a concurrent conformance relation named co-ioco. We propose a test generation algorithm based on Petri net unfolding able to build a complete test suite w.r.t our co-ioco conformance relation. In addition we propose a coverage criterion based on a dedicated notion of complete prefixes that selects a manageable test suite.} }

@inproceedings{PBB-dx13, address = {Jerusalem, Israel}, month = oct, year = 2013, editor = {Kalech, Meir and Feldman, Alexander and Provan, Gregory}, acronym = {{DX}'13}, booktitle = {{P}roceedings of the 24th {I}nternational {W}orkshop on {P}rinciples of {D}iagnosis ({DX}'13)}, author = {Ponce{ }de{~}Le{\'o}n, Hern{\'a}n and Bonigo, Gonzalo and Brand{\'a}n{ }Briones, Laura}, title = {Distributed Analysis of Diagnosability in Concurrent Systems}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/PBB-dx13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PBB-dx13.pdf}, abstract = {Complex systems often exhibit unexpected faults that are difficult to handle. Such systems are desirable to be diagnosable, i.e. faults can be automatically detected as they occur (or shortly afterwards), enabling the system to handle the fault or recover. A system is diagnosable if it is possible to detect every fault, in a finite time after they occurred, by only observing the available information from the system. Complex systems are usually built from simpler components running concurrently. We study how to infer the diagnosability property of a complex system (distributed and with multiple faults) from a parallelized analysis of the diagnosability of each of its components synchronizing with fault free versions of the others. In this paper we make the following contributions: (1)~we~address the diagnosability problem of concurrent systems with arbitrary faults occurring freely in each component. (2)~We~distribute the diagnosability analysis and illustrate our approach with examples. Moreover, (3)~we~present a prototype tool that implements our techniques showing promising results.} }

@inproceedings{reichert-rp13, address = {Uppsala, Sweden}, month = sep, year = 2013, volume = {8169}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Abdulla, Parosh Aziz and Potapov, Igor}, acronym = {{RP}'13}, booktitle = {{P}roceedings of the 7th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'13)}, author = {Reichert, Julien}, title = {On The Complexity of Counter Reachability Games}, pages = {196-208}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/JR-rp13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JR-rp13.pdf}, doi = {10.1007/978-3-642-41036-9_18}, abstract = {Counter reachability games are played by two players on a graph with labelled edges. Each move consists in picking an edge from the current location and adding its label to a counter vector. The objective is to reach a given counter value in a given location. We distinguish three semantics for counter reachability games, according to what happens when a counter value would become negative: the edge is either disabled, or enabled but the counter value becomes zero, or enabled. We consider the problem of deciding the winner in counter reachability games and show that, in most cases, it has the same complexity under all semantics. Surprisingly, under one semantics, the complexity in dimension one depends on whether the objective value is zero or any other integer.} }

@inproceedings{BHJL-rp13, address = {Uppsala, Sweden}, month = sep, year = 2013, volume = {8169}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Abdulla, Parosh Aziz and Potapov, Igor}, acronym = {{RP}'13}, booktitle = {{P}roceedings of the 7th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'13)}, author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge and Jovanovic, Aleksandra and Lime, Didier}, title = {Parametric Interrupt Timed Automata}, pages = {59-69}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHJL-rp13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHJL-rp13.pdf}, doi = {10.1007/978-3-642-41036-9_7}, abstract = {Parametric reasoning is particularly relevant for timed models, but very often leads to undecidability of reachability problems. We propose a parametrised version of Interrupt Timed Automata (an~expressive model incomparable to Timed Automata), where polynomials of parameters can occur in guards and updates. We prove that different reachability problems, including robust reachability, are decidable for this model, and we give complexity upper bounds for a fixed or variable number of clocks and parameters.} }

@inproceedings{FS-rp13, address = {Uppsala, Sweden}, month = sep, year = 2013, volume = {8169}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Abdulla, Parosh Aziz and Potapov, Igor}, acronym = {{RP}'13}, booktitle = {{P}roceedings of the 7th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'13)}, author = {Fribourg, Laurent and Soulat, Romain}, title = {Stability Controllers for Sampled Switched Systems}, pages = {135-145}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FS-rp13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FS-rp13.pdf}, doi = {10.1007/978-3-642-41036-9_13}, abstract = {We consider in this paper switched systems, a class of hybrid systems recently used with success in various domains such as automotive industry and power electonics. We propose a state-dependent control strategy which makes the trajectories of the analyzed system converge to finite cyclic sequences of points. Our method relies on a technique of decomposition of the state space into local regions where the control is uniform. We have implemented the procedure using zonotopes, and applied it successfully to several examples of the literature.} }

@incollection{DKNPPPS-book13, author = {Duflot, Marie and Kwiatkowska, Marta and Norman, Gethin and Parker, David and Peyronnet, Sylvain and Picaronny, Claudine and Sproston, Jeremy}, title = {Practical Applications of Probabilistic Model Checking to Communication Protocols}, booktitle = {Formal Methods for Industrial Critical Systems: A Survey of Applications}, editor = {Gnesi, Stefania and Margaria, Tiziana}, publisher = {John Wiley \& Sons, Ltd. and {IEEE} Computer Society Press}, year = 2013, chapter = 7, pages = {133-150}, month = mar, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DKNPPPS-book13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DKNPPPS-book13.pdf}, doi = {10.1002/9781118459898.ch7} }

@inproceedings{DDS-icalp13, address = {Riga, Latvia}, month = jul, year = 2013, volume = {7966}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Fomin, Fedor V. and Freivalds, R{\=u}si{\c{n}}{\v{s}} and Kwiatkowska, Marta and Peleg, David}, acronym = {{ICALP}'13}, booktitle = {{P}roceedings of the 40th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'13)~-- {P}art~{II}}, author = {Demri, St{\'e}phane and Dhar, Amit Kumar and Sangnier, Arnaud}, title = {On the Complexity of Verifying Regular Properties on Flat Counter Systems}, pages = {162-173}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-icalp13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-icalp13.pdf}, doi = {10.1007/978-3-642-39212-2_17}, abstract = {Among the approximation methods for the verification of counter systems, one of them consists in model-checking their flat unfoldings. Unfortunately, the complexity characterization of model-checking problems for such operational models is not always well studied except for reachability queries or for Past LTL. In this paper, we characterize the complexity of model-checking problems on flat counter systems for the specification languages including first-order logic, linear mu-calculus, infinite automata, and related formalisms. Our results span different complexity classes (mainly from PTime to PSpace) and they apply to languages in which arithmetical constraints on counter values are systematically allowed. As far as the proof techniques are concerned, we provide a uniform approach that focuses on the main issues.} }

@inproceedings{JGL-mfcs13, address = {Klosterneuburg, Austria}, month = aug, year = 2013, volume = {8087}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Chatterjee, Krishnendu and Sgall, Ji{\v{r}}{\'\i}}, acronym = {{MFCS}'13}, booktitle = {{P}roceedings of the 38th {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'13)}, author = {Goubault{-}Larrecq, Jean}, title = {A Constructive Proof of the Topological {K}ruskal Theorem}, pages = {22-41}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-mfcs13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-mfcs13.pdf}, doi = {10.1007/978-3-642-40313-2_3}, abstract = {We give a constructive proof of Kruskal's Tree Theorem---precisely, of a topological extension of~it. The proof is in the style of a constructive proof of Higman's Lemma due to Murthy and Russell~(1990), and illuminates the role of regular expressions there. In the process, we discover an extension of Dershowitz' recursive path ordering to a form of cyclic terms which we call \(\mu\)-terms. This all came from recent research on Noetherian spaces, and serves as a teaser for their theory.} }

@inproceedings{Fribourg-fsfma13, address = {Singapore}, month = jul, year = 2013, volume = 31, series = {Open Access Series in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Choppy, {\relax Ch}ristine and Sun, Jun}, acronym = {{FSFMA}'13}, booktitle = {{P}roceedings of the 1st {F}rench-{S}ingaporean {W}orkshop on {F}ormal {M}ethods and {A}pplications ({FSFMA}'13)}, author = {Fribourg, Laurent}, title = {Control of Switching Systems by Invariance Analysis (Invited~Talk)}, pages = {1}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/F-fsfma13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/F-fsfma13.pdf}, doi = {10.4230/OASIcs.FSFMA.2013.1}, abstract = {Switched systems are embedded devices widespread in industrial applications such as power electronics and automotive control. They consist of continuous-time dynamical subsystems and a rule that controls the switching between them. Under a suitable control rule, the system can improve its steady-state performance and meet essential properties such as safety and stability in desirable operating zones. We explain that such controller synthesis problems are related to the construction of appropriate invariants of the state space, which approximate the limit sets of the system trajectories. We present a new approach of invariant construction based on a technique of state space decomposition interleaved with forward fixed point computation. The method is illustrated in a case study taken from the field of power electronics.} }

@inproceedings{FKS-fsfma13, address = {Singapore}, month = jul, year = 2013, volume = 31, series = {Open Access Series in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Choppy, {\relax Ch}ristine and Sun, Jun}, acronym = {{FSFMA}'13}, booktitle = {{P}roceedings of the 1st {F}rench-{S}ingaporean {W}orkshop on {F}ormal {M}ethods and {A}pplications ({FSFMA}'13)}, author = {Fribourg, Laurent and K{\"u}hne, Ulrich and Soulat, Romain}, title = {Constructing Attractors of Nonlinear Dynamical Systems by State Space Decomposition}, pages = {53-60}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FKS-fsfma13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FKS-fsfma13.pdf}, doi = {10.4230/OASIcs.FSFMA.2013.53}, abstract = {In a previous work, we have shown how to generate attractor sets of affine hybrid systems using a method of state space decomposition. We show here how to adapt the method to polynomial dynamics systems by approximating them as switched affine systems. We show the practical interest of the method on standard examples of the literature.} }

@inproceedings{GHPR-pn13, address = {Milano, Italy}, month = jun, year = 2013, volume = {7927}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Colom, Jos{\'e}-Manuel and Desel, J{\"o}rg}, acronym = {{PETRI~NETS}'13}, booktitle = {{P}roceedings of the 34th {I}nternational {C}onference on {A}pplications and {T}heory of {P}etri {N}ets ({PETRI~NETS}'13)}, author = {Geeraerts, Gilles and Heu{\ss}ner, Alexander and Praveen, M. and Raskin, Jean-Fran{\c{c}}ois}, title = {{{\(\omega\)}}-{P}etri nets}, pages = {49-69}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/GHPR-atpn13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GHPR-atpn13.pdf}, doi = {10.1007/978-3-642-38697-8_4}, abstract = {We introduce \(\omega\)-Petri nets (\(\omega\)PN), an extension of plain Petri nets with \(\omega\)-labeled input and output arcs, that is well-suited to analyse parametric concurrent systems with dynamic thread creation. Most techniques (such as the Karp and Miller tree or the Rackoff technique) that have been proposed in the setting of plain Petri nets do not apply directly to \(\omega\)PN because \(\omega\)PN define transition systems that have infinite branching. This motivates a thorough analysis of the computational aspects of~\(\omega\)PN. We show that an \(\omega\)PN can be turned into a plain Petri net that allows to recover the reachability set of the \(\omega\)PN, but that does not preserve termination. This yields complexity bounds for the reachability, (place) boundedness and coverability problems on \(\omega\)PN. We provide a practical algorithm to compute a coverability set of the \(\omega\)PN and to decide termination by adapting the classical Karp and Miller tree construction. We also adapt the Rackoff technique to \(\omega\)PN, to obtain the exact complexity of the termination problem. Finally, we consider the extension of \(\omega\)PN with reset and transfer arcs, and show how this extension impacts the decidability and complexity of the aforementioned problems.} }

@article{KS-tocl13, publisher = {ACM Press}, journal = {ACM Transactions on Computational Logic}, author = {Kazana, Wojciech and Segoufin, Luc}, title = {Enumeration of monadic second-order queries on trees}, volume = 14, number = {4}, year = 2013, month = nov, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-tocl13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-tocl13.pdf}, doi = {10.1145/2528928}, abstract = {We consider the enumeration problem of monadic second-order (MSO) queries with first-order free variables over trees. In [Bagan 2006] it was shown that this problem is in \textsc{Constant-Delay}\(_{\text{lin}}\). An enumeration problem belongs to \textsc{Constant-Delay}\(_{\text{lin}}\) if for an input structure of size~\(n\) it can be solved by: \begin{itemize} \item an \(O(n)\) precomputation phase building an index structure, \item followed by a phase enumerating the answers with no repetition and a constant delay between two consecutive outputs. \end{itemize} In this article we give a different proof of this result based on the deterministic factorization forest decomposition theorem of Colcombet [Colcombet~2007].} }

@inproceedings{BST-pods13, address = {New~York, New~York, USA}, month = jun, year = 2013, publisher = {ACM Press}, editor = {Fan, Wenfei}, acronym = {{PODS}'13}, booktitle = {{P}roceedings of the 32nd {A}nnual {ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium on {P}rinciples of {D}atabase {S}ystems ({PODS}'13)}, author = {Boja{\'n}czyk, Miko{\l}aj and Segoufin, Luc and Toru{\'n}czyk, Szymon}, title = {Verification of Database-driven Systems via Amalgamation}, pages = {63-74}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BST-pods13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BST-pods13.pdf}, doi = {10.1145/2463664.2465228}, abstract = {We describe a general framework for static verification of systems that base their decisions upon queries to databases. The database is specified using constraints, typically a schema, and is not modified during a run of the system. The system is equipped with a finite number of registers for storing intermediate information from the database and the specification consists of a transition table described using quantifier-free formulas that can query either the database or the registers.\par Our main result concerns systems querying XML databases---modeled as data trees---using quantifier-free formulas with predicates such as the descendant axis or comparison of data values. In this scenario we show an ExpSpace algorithm for deciding reachability.\par Our technique is based on the notion of amalgamation and is quite general. For instance it also applies to relational databases (with an optimal \textsc{PSpace} algorithm).\par We also show that minor extensions of the model lead to undecidability.} }

@inproceedings{GLS-pods13, address = {New~York, New~York, USA}, month = jun, year = 2013, publisher = {ACM Press}, editor = {Fan, Wenfei}, acronym = {{PODS}'13}, booktitle = {{P}roceedings of the 32nd {A}nnual {ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium on {P}rinciples of {D}atabase {S}ystems ({PODS}'13)}, author = {Gheerbrant, Am{\'e}lie and Libkin, Leonid and Sirangelo, Cristina}, title = {When is Na{\"\i}ve Evaluation Possible?}, pages = {75-86}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/GLS-pods13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLS-pods13.pdf}, doi = {10.1145/2463664.2463674}, abstract = {The term na{\"\i}ve evaluation refers to evaluating queries over incomplete databases as if nulls were usual data values, i.e., to using the standard database query evaluation engine. Since the semantics of query answering over incomplete databases is that of certain answers, we would like to know when na{\"\i}ve evaluation computes them: i.e., when certain answers can be found without inventing new specialized algorithms. For relational databases it is well known that unions of conjunctive queries possess this desirable property, and results on preservation of formulae under homomorphisms tell us that within relational calculus, this class cannot be extended under the open-world assumption.\par Our goal here is twofold. First, we develop a general framework that allows us to determine, for a given semantics of incompleteness, classes of queries for which na{\"\i}ve evaluation computes certain answers. Second, we apply this approach to a variety of semantics, showing that for many classes of queries beyond unions of conjunctive queries, na{\"\i}ve evaluation makes perfect sense under assumptions different from open-world. Our key observations are: (1)~na{\"\i}ve evaluation is equivalent to monotonicity of queries with respect to a semantics-induced ordering, and (2)~for most reasonable semantics, such monotonicity is captured by preservation under various types of homomorphisms. Using these results we find classes of queries for which na{\"\i}ve evaluation works, e.g., positive first-order formulae for the closed-world semantics. Even more, we introduce a general relation-based framework for defining semantics of incompleteness, show how it can be used to capture many known semantics and to introduce new ones, and describe classes of first-order queries for which na{\"\i}ve evaluation works under such semantics.} }

@inproceedings{AV-pods13, address = {New~York, New~York, USA}, month = jun, year = 2013, publisher = {ACM Press}, editor = {Fan, Wenfei}, acronym = {{PODS}'13}, booktitle = {{P}roceedings of the 32nd {A}nnual {ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium on {P}rinciples of {D}atabase {S}ystems ({PODS}'13)}, author = {Abiteboul, Serge and Vianu, Victor}, title = {Collaborative Data-Driven Workflows: Think Global, Act Local}, pages = {91-102}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AV-pods13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AV-pods13.pdf}, doi = {10.1145/2463664.2463672}, abstract = {We introduce and study a model of collaborative data-driven workflows. In a local-as-view style, each peer has a partial view of a global instance that remains purely virtual. Local updates have side effects on other peers' data, defined via the global instance. We also assume that the peers provide (an abstraction of) their specifications, so that each peer can actually see and reason on the specification of the entire system. We study the ability of a peer to carry out runtime reasoning about the global run of the system, and in particular about actions of other peers, based on its own local observations. A main contribution is to show that, under a reasonable restriction (namely, key-visibility ), one can construct a finite symbolic representation of the infinite set of global runs consistent with given local observations. Using the symbolic representation, we show that we can evaluate in pspace a large class of properties over global runs, expressed in an extension of first-order logic with past linear-time temporal operators, PLTL-FO. We also provide a variant of the algorithm allowing to incrementally monitor a statically defined property, and then develop an extension allowing to monitor an infinite class of properties sharing the same temporal structure, defined dynamically as the run unfolds. Finally, we consider an extension of the language, augmeting workflow control with PLTL-FO formulas. We prove that this does not increase the power of the workflow specification language, thereby showing that the language is closed under such introspective reasoning.} }

@inproceedings{KS-pods13, address = {New~York, New~York, USA}, month = jun, year = 2013, publisher = {ACM Press}, editor = {Fan, Wenfei}, acronym = {{PODS}'13}, booktitle = {{P}roceedings of the 32nd {A}nnual {ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium on {P}rinciples of {D}atabase {S}ystems ({PODS}'13)}, author = {Kazana, Wojciech and Segoufin, Luc}, title = {Enumeration of First-Order Queries on Classes of Structures With Bounded Expansion}, pages = {297-308}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-pods13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-pods13.pdf}, doi = {10.1145/2463664.2463667}, abstract = {We consider the evaluation of first-order queries over classes of databases with bounded expansion. The notion of bounded expansion is fairly broad and generalizes bounded degree, bounded treewidth and exclusion of at least one minor. It was known that over a class of databases with bounded expansion, first-order sentences could be evaluated in time linear in the size of the database. We first give a different proof of this result. Moreover, we show that answers to first-order queries can be enumerated with constant delay after a linear time preprocessing. We also show that counting the number of answers to a query can be done in time linear in the size of the database.} }

@inproceedings{SHLRFLF-epe13, address = {Lille, France}, month = sep, year = 2013, publisher = {{IEEE} Power Electronics Society}, editor = {Lataire, {\relax Ph}ilippe}, booktitle = {{P}roceedings of the 15th {E}uropean {C}onference on {P}ower {E}lectronics and {A}pplications ({EPE}'13)}, author = {Soulat, Romain and H{\'e}rault, Guillaume and Labrousse, Denis and Revol, Bertrand and Feld, Gilles and Lefebvre, St{\'e}phane and Fribourg, Laurent}, title = {Use of a full wave correct-by-design command to control a multilevel modular converter}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/SHLRFLF-epe13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SHLRFLF-epe13.pdf}, doi = {10.1109/EPE.2013.6634448}, abstract = {This paper proposes a method to synthesize a full wave control applied to a multilevel modular converter~(MMC). This method guarantees the output waveform and the balancing of the capacitors. Numerical simulations and experiments are used to check the validity of the approach.} }

@inproceedings{ABDHHKLP-icfem13, address = {Queenstown, New~Zealand}, month = oct # {-} # nov, year = 2013, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Groves, Lindsay and Sub, Jing}, acronym = {{ICFEM}'13}, booktitle = {{P}roceedings of the 15th {I}nternational {C}onference on {F}ormal {E}ngineering {M}ethods ({ICFEM}'13)}, author = {Andr{\'e}, {\'E}tienne and Barbot, Beno{\^\i}t and D{\'e}moulins, Cl{\'e}ment and Hillah, Lom Messan and Hulin{-}Hubard, Francis and Kordon, Fabrice and Linard, Alban and Petrucci, Laure}, title = {A Modular Approach for Reusing Formalisms in Verification Tools of Concurrent Systems}, pages = {199-214}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABDHHKLP-icfem13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABDHHKLP-icfem13.pdf}, doi = {10.1007/978-3-642-41202-8_14}, abstract = {Over the past two decades, numerous verification tools have been successfully used for verifying complex concurrent systems, modelled using various formalisms. However, it is still hard to coordinate these tools since they rely on such a large number of formalisms. Having a proper syntactical mechanism to interrelate them through variability would increase the capability of effective integrated formal methods. In this paper, we propose a modular approach for defining new formalisms by reusing existing ones and adding new features and/or constraints. Our approach relies on standard XML technologies; their use provides the capability of rapidly and automatically obtaining tools for representing and validating models. It thus enables fast iterations in developing and testing complex formalisms. As a case study, we applied our modular definition approach on families of Petri nets and timed automata.} }

@inproceedings{AHHKLLP-iceccs13, address = {Singapore}, month = jul, year = 2013, publisher = {{IEEE} Computer Society Press}, editor = {Liu, Yang and Martin, Andrew}, acronym = {{ICECCS}'13}, booktitle = {{P}roceedings of the 18th {IEEE} {I}nternational {C}onference on {E}ngineering of {C}omplex {C}omputer {S}ystems ({ICECCS}'13)}, author = {Andr{\'e}, {\'E}tienne and Hillah, Lom Messan and Hulin{-}Hubard, Francis and Kordon, Fabrice and Lembachar, Yousra and Linard, Alban and Petrucci, Laure}, title = {{C}osy{V}erif: An~Open Source Extensible Verification Environment}, pages = {33-36}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AHHKLLP-iceccs13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AHHKLLP-iceccs13.pdf}, doi = {10.1109/ICECCS.2013.15}, abstract = {CosyVerif aims at gathering within a common framework various existing tools for specification and verification. It has been designed in order to 1)~support different formalisms with the ability to easily create new ones, 2)~provide a graphical user interface for every formalism, 3)~include verification tools called via the graphical interface or via an API as a Web service, and 4)~offer the possibility for a developer to integrate his/her own tool without much effort, also allowing it to interact with the other tools. Several tools have already been integrated for the formal verification of (extensions~of) Petri nets and timed automata.} }

@inproceedings{LM-gandalf13, address = {Borca di Cadore, Italy}, month = aug, year = 2013, volume = {119}, series = {Electronic Proceedings in Theoretical Computer Science}, editor = {Puppis, Gabriele and Villa, Tiziano}, acronym = {{GandALF}'13}, booktitle = {{P}roceedings of the 4th {I}nternational {S}ymposium on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification ({GandALF}'13)}, author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas}, title = {Satisfiability of {ATL} with strategy contexts}, pages = {208-223}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LM-gandalf13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LM-gandalf13.pdf}, doi = {10.4204/EPTCS.119.18}, abstract = {Various extensions of the temporal logic ATL have recently been introduced to express rich properties of multi-agent systems. Among these, ATLsc extends ATL with \emph{strategy contexts}, while Strategy Logic has \emph{first-order quantification} over strategies. There is a price to pay for the rich expressiveness of these logics: model-checking is non-elementary, and satisfiability is undecidable.\par We prove in this paper that satisfiability is decidable in several special cases. The most important one is when restricting to \emph{turn-based} games. We~prove that decidability also holds for concurrent games if the number of moves available to the agents is bounded. Finally, we~prove that restricting strategy quantification to memoryless strategies brings back undecidability.} }

@inproceedings{BDGORW-atva13, address = {Hanoi, Vietnam}, month = oct, year = {2013}, volume = {8172}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Dang{-}Van, Hung and Ogawa, Mizuhito}, acronym = {{ATVA}'13}, booktitle = {{P}roceedings of the 11th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'13)}, author = {Brihaye, {\relax Th}omas and Doyen, Laurent and Geeraerts, Gilles and Ouaknine, Jo{\"e}l and Raskin, Jean-Fran{\c{c}}ois and Worrell, James}, title = {Time-Bounded Reachability for Monotonic Hybrid Automata: Complexity and Fixed Points}, pages = {55-70}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDGORW-atva13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDGORW-atva13.pdf}, doi = {10.1007/978-3-319-02444-8_6}, abstract = {We study the \emph{time-bounded reachability problem} for \emph{monotonic hybrid automata} (MHA), i.e., rectangular hybrid automata for which the rate of each variable is either always non-negative or always non-positive. In this paper, we revisit the decidability results presented in [Brihaye et~al., \textit{On reachability for hybrid automata over bounded time}, ICALP~2011] and show that the problem is NExpTime-complete. We also show that we can effectively compute fixed points that characterise the sets of states that are reachable (resp. co-reachable) within \(T\) time units from a given state.} }

@inproceedings{CDRR-atva13, address = {Hanoi, Vietnam}, month = oct, year = {2013}, volume = {8172}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Dang{-}Van, Hung and Ogawa, Mizuhito}, acronym = {{ATVA}'13}, booktitle = {{P}roceedings of the 11th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'13)}, author = {Chatterjee, Krishnendu and Doyen, Laurent and Randour, Mickael and Raskin, Jean-Fran{\c{c}}ois}, title = {Looking at Mean-Payoff and Total-Payoff through Windows}, pages = {118-132}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDRR-atva13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDRR-atva13.pdf}, doi = {10.1007/978-3-319-02444-8_10}, abstract = {We consider two-player games played on weighted directed graphs with mean-payoff and total-payoff objectives, two classical quantitative objectives. While for single-dimensional games the complexity and memory bounds for both objectives coincide, we show that in contrast to multi-dimensional mean-payoff games that are known to be coNP-complete, multi-dimensional total-payoff games are undecidable. We introduce conservative approximations of these objectives, where the payoff is considered over a local finite window sliding along a play, instead of the whole play. For single dimension, we show that (i)~if the window size is polynomial, deciding the winner takes polynomial time, and (ii)~the existence of a bounded window can be decided in NP coNP, and is at least as hard as solving mean-payoff games. For multiple dimensions, we show that (i)~the problem with fixed window size is EXPTIME-complete, and (ii)~there is no primitive-recursive algorithm to decide the existence of a bounded window.} }

@inproceedings{RS-atva13, address = {Hanoi, Vietnam}, month = oct, year = {2013}, volume = {8172}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Dang{-}Van, Hung and Ogawa, Mizuhito}, acronym = {{ATVA}'13}, booktitle = {{P}roceedings of the 11th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'13)}, author = {Rodr{\'\i}guez, C{\'e}sar and Schwoon, Stefan}, title = {Cunf: A~Tool for Unfolding and Verifying Petri Nets with Read Arcs}, pages = {492-495}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/RS-atva13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RS-atva13.pdf}, doi = {10.1007/978-3-319-02444-8_42}, abstract = {Cunf is a tool for building and analyzing unfoldings of Petri nets with read arcs. An unfolding represents the behaviour of a net by a partial order, effectively coping with the state-explosion problem stemming from the interleaving of concurrent actions. C-net unfoldings can be up to exponentially smaller than Petri net unfoldings, and recent work proposed algorithms for their construction and verification. Cunf is the first implementation of these techniques, it has been carefully engineered and optimized to ensure that the theoretical gains are put into practice.} }

@inproceedings{AFS-atva13, address = {Hanoi, Vietnam}, month = oct, year = {2013}, volume = {8172}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Dang{-}Van, Hung and Ogawa, Mizuhito}, acronym = {{ATVA}'13}, booktitle = {{P}roceedings of the 11th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'13)}, author = {Andr{\'e}, {\'E}tienne and Fribourg, Laurent and Soulat, Romain}, title = {Merge and Conquer: State Merging in Parametric Timed Automata}, pages = {381-396}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AFS-atva13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AFS-atva13.pdf}, doi = {10.1007/978-3-319-02444-8_27}, abstract = {Parameter synthesis for real-time systems aims at synthesizing dense sets of valuations for the timing requirements, guaranteeing a good behavior. A popular formalism for modeling parameterized realtime systems is parametric timed automata (PTAs). Compacting the state space of PTAs as much as possible is fundamental. We present here a state merging reduction based on convex union, that reduces the state space, but yields an over-approximation of the executable paths. However, we show that it preserves the sets of reachable locations and executable actions. We also show that our merging technique associated with the inverse method, an algorithm for parameter synthesis, preserves locations as well, and outputs larger sets of parameter valuations.} }

@article{CCD-tcs13, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {Cheval, Vincent and Cortier, V{\'e}ronique and Delaune, St{\'e}phanie}, title = {Deciding equivalence-based properties using constraint solving}, year = {2013}, month = jun, volume = {492}, pages = {1-39}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-tcs13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-tcs13.pdf}, doi = {10.1016/j.tcs.2013.04.016}, abstract = {Formal methods have proved their usefulness for analyzing the security of protocols. Most existing results focus on trace properties like secrecy or authentication. There are however several security properties, which cannot be defined (or cannot be naturally defined) as trace properties and require a notion of behavioural equivalence. Typical examples are anonymity, privacy related properties or statements closer to security properties used in cryptography.\par In this paper, we consider three notions of equivalence defined in the applied pi calculus: observational equivalence, may-testing equivalence, and trace equivalence. First, we study the relationship between these three notions. We show that for determinate processes, observational equivalence actually coincides with trace equivalence, a notion simpler to reason with. We exhibit a large class of determinate processes, called simple processes, that capture most existing protocols and cryptographic primitives. While trace equivalence and may-testing equivalence seem very similar, we show that may-testing equivalence is actually strictly stronger than trace equivalence. We prove that the two notions coincide for image-finite processes, such as processes without replication.\par Second, we reduce the decidability of trace equivalence (for finite processes) to deciding symbolic equivalence between sets of constraint systems. For simple processes without replication and with trivial else branches, it turns out that it is actually sufficient to decide symbolic equivalence between pairs of positive constraint systems. Thanks to this reduction and relying on a result first proved by M. Baudet, this yields the first decidability result of observational equivalence for a general class of equational theories (for processes without else branch nor replication). Moreover, based on another decidability result for deciding equivalence between sets of constraint systems, we get decidability of trace equivalence for processes with else branch for standard primitives.} }

@inproceedings{SS-concur13, address = {Buenos Aires, Argentina}, month = aug, year = 2013, volume = 8052, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {D'Argenio, Pedro R. and Melgratti, Hern{\'a}n)}, acronym = {{CONCUR}'13}, booktitle = {{P}roceedings of the 24th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'13)}, author = {Schmitz, Sylvain and Schnoebelen, {\relax Ph}ilippe}, title = {The Power of Well-Structured Systems}, pages = {5-24}, url = {http://arxiv.org/abs/1402.2908}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SS-concur13.pdf}, doi = {10.1007/978-3-642-40184-8_2}, abstract = {Well-structured systems, aka WSTS, are computational models where the set of possible configurations is equipped with a well-quasi-ordering which is compatible with the transition relation between configurations. This structure supports generic decidability results that are important in verification and several other fields. This paper recalls the basic theory underlying well-structured systems and shows how two classic decision algorithms can be formulated as an exhaustive search for some {"}bad{"} sequences. This lets us describe new powerful techniques for the complexity analysis of WSTS algorithms. Recently, these techniques have been successful in precisely characterizing the power, in a complexity-theoretical sense, of several important WSTS models like unreliable channel systems, monotonic counter machines, or networks of timed systems.} }

@inproceedings{CCS-cade2013, address = {Lake Placid, New~York, USA}, month = jun, year = 2013, volume = 7898, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, editor = {Bonacina, Maria Paola}, acronym = {{CADE}'13}, booktitle = {{P}roceedings of the 24th {I}nternational {C}onference on {A}utomated {D}eduction ({CADE}'13)}, author = {Comon{-}Lundh, Hubert and Cortier, V{\'e}ronique and Scerri, Guillaume}, title = {Tractable inference systems: an extension with a deducibility predicate}, pages = {91-108}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCS-cade2013.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCS-cade2013.pdf}, doi = {10.1007/978-3-642-38574-2_6}, abstract = {The main contribution of the paper is a PTIME decision procedure for the satisfiability problem in a class of first-order Horn clauses. Our result is an extension of the tractable classes of Horn clauses of Basin & Ganzinger in several respects. For instance, our clauses may contain atomic formulas \(S \vdash t\) where \(\vdash\) is a predicate symbol and \(S\) is a finite set of terms instead of a term. \(\vdash\)~is used to represent any possible computation of an attacker, given a set of messages~\(S\). The class of clauses that we consider encompasses the clauses designed by Bana~\& Comon-Lundh for security proofs of protocols in a computational model. \par Because of the (variadic) \(\vdash\) predicate symbol, we cannot use ordered resolution strategies only, as in Basin~\& Ganzinger: given \(S \vdash t\), we must avoid computing \(S' \vdash t\) for all subsets \(S'\) of~\(S\). Instead, we design PTIME entailment procedures for increasingly expressive fragments, such procedures being used as oracles for the next fragment. \par Finally, we obtain a PTIME procedure for arbitrary ground clauses and saturated Horn clauses (as in Basin~\& Ganzinger), together with a particular class of (non saturated) Horn clauses with the \(\vdash\) predicate and constraints (which are necessary to cover the application).} }

@inproceedings{HRS-acsd13, address = {Barcelona, Spain}, month = jul, year = 2013, publisher = {{IEEE} Computer Society Press}, editor = {Pietkiewicz{-}Koutny, Marta and Lazarescu, Mihai Teodor}, acronym = {{ACSD}'13}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {A}pplication of {C}oncurrency to {S}ystem {D}esign ({ACSD}'13)}, author = {Haar, Stefan and Rodr{\'\i}guez, C{\'e}sar and Schwoon, Stefan}, title = {Reveal Your Faults: It's Only Fair!}, pages = {120-129}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/HRS-acsd13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HRS-acsd13.pdf}, doi = {10.1109/ACSD.2013.15}, abstract = {We present a methodology for fault diagnosis in concurrent, partially observable systems with additional fairness constraints. In this weak diagnosis, one asks whether a concurrent chronicle of observed events allows to determine that a non-observable fault will inevitably occur, sooner or later, on any maximal system run compatible with the observation. The approach builds on strengths and techniques of unfoldings of safe Petri nets, striving to compute a compact prefix of the unfolding that carries sufficient information for the diagnosis algorithm. Our work extends and generalizes the unfolding-based diagnosis approaches by Benveniste \textit{et~al.} as well as Esparza and Kern. Both of these focused mostly on the use of sequential observations, in particular did not exploit the capacity of unfoldings to reveal inevitable occurrences of concurrent or future events studied by Balaguer \textit{et~al.}. Our diagnosis method captures such indirect, revealed dependencies. We~develop theoretical foundations and an algorithmic solution to the diagnosis problem, and present a SAT solving method for practical diagnosis with our approach.} }

@article{HKS-tcs13, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {Haar, Stefan and Kern, Christian and Schwoon, Stefan}, title = {Computing the Reveals Relation in Occurrence Nets}, year = 2013, month = jul, volume = 493, pages = {66-79}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/HKS-tcs13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HKS-tcs13.pdf}, doi = {10.1016/j.tcs.2013.04.028}, abstract = {Petri net unfoldings are a useful tool to tackle state-space explosion in verification and related tasks. Moreover, their structure allows to access directly the relations of causal precedence, concurrency, and conflict between events. Here, we explore the data structure further, to determine the following relation: event~\(a\) is said to reveal event~\(b\) iff the occurrence of~\(a\) implies that~\(b\) inevitably occurs, too, be it before, after, or concurrently with~\(a\). Knowledge of reveals facilitates in particular the analysis of partially observable systems, in the context of diagnosis, testing, or verification; it can also be used to generate more concise representations of behaviours via abstractions. The reveals relation was previously introduced in the context of fault diagnosis, where it was shown that the reveals relation was decidable: for a given pair~\(a,b\) in the unfolding~\(U\) of a safe Petri net~\(N\), a finite prefix~\(P\) of~\(U\) is sufficient to decide whether or not \(a\) reveals~\(b\). In this paper, we first considerably improve the bound on~\(|P|\). We then show that there exists an efficient algorithm for computing the relation on a given prefix. We have implemented the algorithm and report on experiments.} }

@inproceedings{FS-ncmip13, address = {Cachan, France}, month = may, year = 2013, number = {012007}, volume = 464, series = {Journal of Physics: Conference Series}, publisher = {{IOS} Press}, editor = {Blanc{-}F{\'e}raud, Laure and Joubert, Pierre-Yves}, acronym = {{NCMIP}'13}, booktitle = {{P}roceedings of the 3rd {I}nternational {W}orkshop on {N}ew {C}omputational {M}ethods for {I}nverse {P}roblems ({NCMIP}'13)}, author = {Fribourg, Laurent and Soulat, Romain}, title = {Limit Cycles of Controlled Switched Systems: Existence, Stability, Sensitivity}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FS-ncmip13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FS-ncmip13.pdf}, doi = {10.1088/1742-6596/464/1/012007}, abstract = {We present a control method which makes the trajectories of a switched system converge to a stable limit cycle lying in a desired region of equilibrium. The method is illustrated on the boost DC-DC converter example. We also point out in this example the sensitivity of limit cycles to parameter variations by showing how the limit cycle evolves in presence of small perturbations of some system parameters. This suggests that limit cycles are good candidates for reliable estimations of the physical parameters of switched systems, using an appropriate inverse approach.} }

@inproceedings{ABHH-qest13, address = {Buenos Aires, Argentina}, month = aug, year = 2013, publisher = {{IEEE} Computer Society Press}, acronym = {{QEST}'13}, booktitle = {{P}roceedings of the 10th {I}nternational {C}onference on {Q}uantitative {E}valuation of {S}ystems ({QEST}'13)}, author = {Akshay, S. and Bertrand, Nathalie and Haddad, Serge and H{\'e}lou{\"e}t, Lo{\"\i}c}, title = {The steady-state control problem for Markov decision processes}, pages = {290-304}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABHH-qest13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABHH-qest13.pdf}, doi = {10.1007/978-3-642-40196-1_26}, abstract = {This paper addresses a control problem for probabilistic models in the setting of Markov decision processes~(MDP). We~are interested in the steady-state control problem which asks, given an ergodic MDP~\(M\) and a distribution~\(\delta_{\text{goal}}\), whether there exists a (history-dependent randomized) policy \(\pi\) ensuring that the steady-state distribution of~\(M\) under~\(\pi\) is exactly~\(\delta_{\text{goal}}\). We~first show that stationary randomized policies suffice to achieve a given steady-state distribution. Then we infer that the steady-state control problem is decidable for~MDP, and can be represented as a linear program which is solvable in PTIME. This decidability result extends to labeled MDP (LMDP) where the objective is a steady-state distribution on labels carried by the states, and we provide a PSPACE algorithm. We also show that a related steady-state language inclusion problem is decidable in EXPTIME for LMDP. Finally, we prove that if we consider MDP under partial observation (POMDP), the steady-state control problem becomes undecidable.} }

@inproceedings{KKS-esorics13, address = {Egham, U.K.}, month = sep, year = 2013, volume = {8134}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Crampton, Jason and Jajodia, Sushil and Mayes, Keith}, acronym = {{ESORICS}'13}, booktitle = {{P}roceedings of the 18th {E}uropean {S}ymposium on {R}esearch in {C}omputer {S}ecurity ({ESORICS}'13)}, author = {Kremer, Steve and K{\"u}nnemann, Robert and Steel, Graham}, title = {Universally Composable Key-Management}, pages = {327-344}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/KKS-esorics13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KKS-esorics13.pdf}, doi = {10.1007/978-3-642-40203-6_19}, abstract = {We present the first universally composable key-management functionality, formalized in the GNUC framework by Hofheinz and Shoup. It allows the enforcement of a wide range of security policies and can be extended by diverse key usage operations with no need to repeat the security proof. We illustrate its use by proving an implementation of a security token secure with respect to arbitrary key-usage operations and explore a proof technique that allows the storage of cryptographic keys externally, a novel development in simulation-based security frameworks.} }

@phdthesis{sankur-phd2013, author = {Sankur, Ocan}, title = {Robustness in Timed Automata: Analysis, Synthesis, Implementation}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2013, month = may, url = {http://www.lsv.fr/Publis/PAPERS/PDF/sankur-phd13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/sankur-phd13.pdf} }

@article{FK-ijfcs13, publisher = {World Scientific}, journal = {International Journal of Foundations of Computer Science}, author = {Fribourg, Laurent and K{\"u}hne, Ulrich}, title = {Parametric Verification and Test Coverage for Hybrid Automata using the Inverse Method}, year = 2013, month = feb, volume = 24, number = 2, pages = {233-249}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FK-ijfcs13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FK-ijfcs13.pdf}, doi = {10.1142/S0129054113400091}, abstract = {Hybrid systems combine continuous and discrete behavior. Hybrid Automata are a powerful formalism for the modeling and verification of such systems. A~common problem in hybrid system verification is the good parameters problem, which consists in identifying a set of parameter valuations which guarantee a certain behavior of a system. Recently, a method has been presented for attacking this problem for Timed Automata. In this paper, we show the extension of this methodology for hybrid automata with linear and affine dynamics. The method is demonstrated with a hybrid system benchmark from the literature.} }

@inproceedings{CJ-formats13, address = {Buenos Aires, Argentina}, month = aug, year = 2013, volume = 8053, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Braberman, V{\'\i}ctor and Fribourg, Laurent}, acronym = {{FORMATS}'13}, booktitle = {{P}roceedings of the 11th {I}nternational {C}onference on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'13)}, author = {Chatain, {\relax Th}omas and Jard, Claude}, title = {Back in Time {P}etri Nets}, pages = {91-105}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CJ-formats13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CJ-formats13.pdf}, doi = {10.1007/978-3-642-40229-6_7}, abstract = {The time progress assumption is at the core of the semantics of real-time formalisms. It is also the major obstacle to the development of partial-order techniques for real-time distributed systems since the events are ordered both by causality and by their occurrence in time. Anyway, extended free choice safe time Petri nets (TPNs) were already identified as a class where partial order semantics behaves well. We show that, for this class, the time progress assumption can even be dropped (time may go back in case of concurrency), which establishes a nice relation between partial-order semantics and time progress assumption.} }

@inproceedings{BMS-formats13, address = {Buenos Aires, Argentina}, month = aug, year = 2013, volume = 8053, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Braberman, V{\'\i}ctor and Fribourg, Laurent}, acronym = {{FORMATS}'13}, booktitle = {{P}roceedings of the 11th {I}nternational {C}onference on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'13)}, author = {Bouyer, Patricia and Markey, Nicolas and Sankur, Ocan}, title = {Robust Weighted Timed Automata and Games}, pages = {31-46}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-formats13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-formats13.pdf}, doi = {10.1007/978-3-642-40229-6_3}, abstract = {Weighted timed automata extend timed automata with cost variables that can be used to model the evolution of various quantities. Although cost-optimal reachability is decidable (in polynomial space) on this model, it becomes undecidable on weighted timed games. This paper studies cost-optimal reachability problems on weighted timed automata and games under robust semantics. More precisely, we consider two perturbation game semantics that introduce imprecisions in the standard semantics, and bring robustness properties w.r.t. timing imprecisions to controllers. We give a polynomial-space algorithm for weighted timed automata, and prove the undecidability of cost-optimal reachability on weighted timed games, showing that the problem is robustly undecidable.} }

@inproceedings{HSS-concur13, address = {Buenos Aires, Argentina}, month = aug, year = 2013, volume = 8052, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {D'Argenio, Pedro R. and Melgratti, Hern{\'a}n)}, acronym = {{CONCUR}'13}, booktitle = {{P}roceedings of the 24th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'13)}, author = {Haase, Christoph and Schmitz, Sylvain and Schnoebelen, {\relax Ph}ilippe}, title = {The Power of Priority Channel Systems}, pages = {319-333}, url = {http://arxiv.org/abs/1301.5500}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HSS-corr13.pdf}, arxivpdf = {http://arxiv.org/pdf/1301.5500}, doi = {10.1007/978-3-642-40184-8_23}, abstract = {We introduce Priority Channel Systems, a new natural class of channel systems where messages carry a numeric priority and where higher-priority messages can supersede lower-priority messages preceding them in the fifo communication buffers. The decidability of safety and inevitability properties is shown via the introduction of a \emph{priority embedding}, a~well-quasi-ordering that has not previously been used in well-structured systems. We then show how Priority Channel Systems can compute Fast-Growing functions and prove that the aforementioned verification problems are \(F_{\epsilon_{0}}\)-complete.} }

@inproceedings{SBMR-concur13, address = {Buenos Aires, Argentina}, month = aug, year = 2013, volume = 8052, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {D'Argenio, Pedro R. and Melgratti, Hern{\'a}n)}, acronym = {{CONCUR}'13}, booktitle = {{P}roceedings of the 24th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'13)}, author = {Sankur, Ocan and Bouyer, Patricia and Markey, Nicolas and Reynier, Pierre-Alain}, title = {Robust Controller Synthesis in Timed Automata}, pages = {546-560}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/SBMR-concur13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SBMR-concur13.pdf}, doi = {10.1007/978-3-642-40184-8_38}, abstract = {We consider the fundamental problem of B{\"u}chi acceptance in timed automata in a robust setting. The problem is formalised in terms of controller synthesis: timed automata are equipped with a parametrised game-based semantics that models the possible perturbations of the decisions taken by the controller. We characterise timed automata that are robustly controllable for some parameter, with a simple graph theoretic condition, by showing the equivalence with the existence of an aperiodic lasso that satisfies the winning condition (aperiodicity was defined and used earlier in different contexts to characterise convergence phenomena in timed automata). We then show decidability and PSPACE-completeness of our problem.} }

@inproceedings{FGH-mfcs13, address = {Klosterneuburg, Austria}, month = aug, year = 2013, volume = {8087}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Chatterjee, Krishnendu and Sgall, Ji{\v{r}}{\'\i}}, acronym = {{MFCS}'13}, booktitle = {{P}roceedings of the 38th {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'13)}, author = {Finkel, Alain and G{\"o}ller, Stefan and Haase, Christoph}, title = {Reachability in Register Machines with Polynomial Updates}, pages = {409-420}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FGH-mfcs13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FGH-mfcs13.pdf}, ps = {FGH-mfcs13.ps}, doi = {10.1007/978-3-642-40313-2_37}, abstract = {This paper introduces a class of register machines whose registers can be updated by polynomial functions when a transition is taken, and the domain of the registers can be constrained by linear constraints. This model strictly generalises a variety of known formalisms such as various classes of Vector Addition Systems with States. Our main result is that reachability in our class is PSPACE-complete when restricted to one register. We moreover give a classification of the complexity of reachability according to the type of polynomials allowed and the geometry induced by the range-constraining formula.} }

@article{ACK-jcss13, publisher = {Elsevier Science Publishers}, journal = {Journal of Computer and System Sciences}, author = {Abiteboul, Serge and ten~Cate, Balder and Katsis, Yannis}, title = {On the equivalence of distributed systems with queries and communication}, volume = 79, number = 6, pages = {739-762}, year = 2013, month = sep, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ACK-jcss13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ACK-jcss13.pdf}, doi = {10.1016/j.jcss.2013.01.001}, abstract = {Distributed data management systems consist of peers that store, exchange and process data in order to collaboratively achieve a common goal, such as evaluating some query. We study the equivalence of such systems. We model a distributed system by a collection of Active XML documents, i.e., trees augmented with function calls for performing tasks such as sending, receiving and querying data. As our model is quite general, the equivalence problem turns out to be undecidable. However, we exhibit several restrictions of the model, for which equivalence can be effectively decided. We also study the computational complexity of the equivalence problem, and present an axiomatization of equivalence, in the form of a set of equivalence-preserving rewrite rules allowing us to optimize a system by rewriting it into an equivalent, but possibly more efficient system.} }

@inproceedings{McK-dcfs13, address = {London, Ontario, Canada}, month = jul, year = 2013, volume = {8031}, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, acronym = {{DCFS}'13}, booktitle = {{P}roceedings of the 15th {W}orkshop on {D}escriptional {C}omplexity of {F}ormal {S}ystems ({DCFS}'13)}, author = {McKenzie, Pierre}, title = {Can chimps go it alone?}, pages = {17}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/McK-dcfs13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/McK-dcfs13.pdf}, doi = {10.1007/978-3-642-39310-5_3} }

@inproceedings{CCD-icalp13, address = {Riga, Latvia}, month = jul, year = 2013, volume = {7966}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Fomin, Fedor V. and Freivalds, R{\=u}si{\c{n}}{\v{s}} and Kwiatkowska, Marta and Peleg, David}, acronym = {{ICALP}'13}, booktitle = {{P}roceedings of the 40th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'13)~-- {P}art~{II}}, author = {Chr{\'e}tien, R{\'e}my and Cortier, V{\'e}ronique and Delaune, St{\'e}phanie}, title = {From security protocols to pushdown automata}, pages = {137-149}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-icalp13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-icalp13.pdf}, doi = {10.1007/978-3-642-39212-2_15}, abstract = {Formal methods have been very successful in analyzing security protocols for reachability properties such as secrecy or authentication. In contrast, there are very few results for equivalence-based properties, crucial for studying e.g. privacy-like properties such as anonymity or vote secrecy.\par We study the problem of checking equivalence of security protocols for an unbounded number of sessions. Since replication leads very quickly to undecidability (even in the simple case of secrecy), we focus on a limited fragment of protocols (standard primitives but pairs, one variable per protocol's rules) for which the secrecy preservation problem is known to be decidable. Surprisingly, this fragment turns out to be undecidable for equivalence. Then, restricting our attention to deterministic protocols, we propose the first decidability result for checking equivalence of protocols for an unbounded number of sessions. This result is obtained through a characterization of equivalence of protocols in terms of equality of languages of (generalized, real-time) deterministic pushdown automata.} }

@inproceedings{ABMW-icdt13, address = {Genoa, Italy}, month = mar, year = 2013, publisher = {ACM Press}, editor = {Tan, Wang-Chiew and Guerrini, Giovanna and Catania, Barbara and Gounaris, Anastasios}, acronym = {{ICDT}'13}, booktitle = {{P}roceedings of the 16th {I}nternational {C}onference on {D}atabase {T}heory ({ICDT}'13)}, author = {Abiteboul, Serge and Bourhis, Pierre and Muscholl, Anca and Wu, Zhilin}, title = {Recursive queries on trees and data trees}, pages = {93-104}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABMW-icdt13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABMW-icdt13.pdf}, doi = {10.1145/2448496.2448509}, abstract = {The analysis of datalog programs over relational structures has been studied in depth, most notably the problem of containment. The analysis problems that have been considered were shown to be undecidable with the exception of (i)~containment of arbitrary programs in nonrecursive ones, (ii)~containment of monadic programs, and (iii)~emptiness. In~this paper, we are concerned with a much less studied problem, the analysis of datalog programs over data trees. We show that the analysis of datalog programs is more complex for data trees than for arbitrary structures. In particular we prove that the three aforementioned problems are undecidable for data trees. But in practice, data trees (e.g., XML trees) are often of bounded depth. We prove that all three problems are decidable over bounded depth data trees. Another contribution of the paper is the study of a new form of automata called pattern automata, that are essentially equivalent to linear datalog programs. We use pattern automata to show that the emptiness problem for linear monadic datalog programs with data value inequalities is decidable over arbitrary data trees.} }

@article{BCGJV-lmcs13, journal = {Logical Methods in Computer Science}, author = {Bargu{\~n}{\'o}, Luis and Creus, Carles and Godoy, Guillem and Jacquemard, Florent and Vacher, Camille}, title = {Decidable Classes of Tree Automata Mixing Local and Global Constraints Modulo Flat Theories}, volume = 9, number = 2, nopages = {}, month = apr, year = 2013, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGJV-lmcs13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGJV-lmcs13.pdf}, doi = {10.2168/LMCS-9(2:1)2013}, abstract = {We define a class of ranked tree automata TABG generalizing both the tree automata with local tests between brothers of Bogaert and Tison (1992) and with global equality and disequality constraints (TAGED) of Filiot et al. (2007). TABG can test for equality and disequality modulo a given flat equational theory between brother subterms and between subterms whose positions are defined by the states reached during a computation. In particular, TABG 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. We prove decidability of the emptiness problem for TABG. This solves, in particular, the open question of the 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 equivalence classes of subterms (modulo a given flat equational theory) reaching some state during a computation. We also adapt the model to unranked ordered terms. As a consequence of our results for TABG, 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{BKM-lics13, address = {New-Orleans, Louisiana, USA}, month = jun, year = 2013, publisher = {{IEEE} Computer Society Press}, acronym = {{LICS}'13}, booktitle = {{P}roceedings of the 28th {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'13)}, author = {Bollig, Benedikt and Kuske, Dietrich and Mennicke, Roy}, title = {The Complexity of Model Checking Multi-Stack Systems}, pages = {163-170}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BKM-lics13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BKM-lics13.pdf}, doi = {10.1109/LICS.2013.22}, abstract = {We consider the linear-time model-checking problem for boolean concurrent programs with recursive procedure calls. While sequential recursive programs are usually modeled as pushdown automata, concurrent recursive programs involve several processes and can be naturally abstracted as pushdown automata with multiple stacks. Their behavior can be understood as words with multiple nesting relations, each relation connecting a procedure call with its corresponding return. To reason about multiply nested words, we consider the class of all temporal logics as defined in the book by Gabbay, Hodkinson, and Reynolds~(1994). The unifying feature of these temporal logics is that their modalities are defined in monadic second-order~(MSO) logic. In particular, this captures numerous temporal logics over concurrent and/or recursive programs that have been defined so far. Since the general model checking problem is undecidable, we restrict attention to phase bounded executions as proposed by La~Torre, Madhusudan, and Parlato (LICS~2007). While the MSO model checking problem in this case is non-elementary, our main result states that the model checking (and satisfiability) problem for all MSO-definable temporal logics is decidable in elementary time. More precisely, it is solvable in \((n+2)\)-EXPTIME where \(n\) is the maximal level of the MSO modalities in the monadic quantifier alternation hierarchy. We complement this result and provide, for each level~\(n\), a~temporal logic whose model checking problem is \(n\)-EXPSPACE-hard.} }

@inproceedings{DFP-lics13, address = {New-Orleans, Louisiana, USA}, month = jun, year = 2013, publisher = {{IEEE} Computer Society Press}, acronym = {{LICS}'13}, booktitle = {{P}roceedings of the 28th {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'13)}, author = {Demri, St{\'e}phane and Figueira, Diego and Praveen, M.}, title = {Reasoning about Data Repetitions with Counter Systems}, pages = {33-42}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DFP-lics13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DFP-lics13.pdf}, doi = {10.1109/LICS.2013.8}, abstract = {We study linear-time temporal logics interpreted over data words with multiple attributes. We restrict the atomic formulas to equalities of attribute values in successive positions and to repetitions of attribute values in the future or past. We demonstrate correspondences between satisfiability problems for logics and reachability-like decision problems for counter systems. We show that allowing/disallowing atomic formulas expressing repetitions of values in the past corresponds to the reachability\slash coverability problem in Petri nets. This gives us 2EXPSPACE upper bounds for several satisfiability problems. We prove matching lower bounds by reduction from a reachability problem for a newly introduced class of counter systems. This new class is a succinct version of vector addition systems with states in which counters are accessed via pointers, a potentially useful feature in other contexts. We strengthen further the correspondences between data logics and counter systems by characterizing the complexity of fragments, extensions and variants of the logic. For instance, we precisely characterize the relationship between the number of attributes allowed in the logic and the number of counters needed in the counter system.} }

@inproceedings{BS-lics13, address = {New-Orleans, Louisiana, USA}, month = jun, year = 2013, publisher = {{IEEE} Computer Society Press}, acronym = {{LICS}'13}, booktitle = {{P}roceedings of the 28th {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'13)}, author = {Boral, Anudhyan and Schmitz, Sylvain}, title = {Model Checking Parse Trees}, pages = {153-162}, url = {http://arxiv.org/abs/1211.5256}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-lics13.pdf}, arxivpdf = {http://arxiv.org/pdf/1211.5256}, doi = {10.1109/LICS.2013.21}, abstract = {Parse trees are fundamental syntactic structures in both computational linguistics and compilers construction. We argue in this paper that, in both fields, there are good incentives for model-checking sets of parse trees for some word according to a context-free grammar. We put forward the adequacy of propositional dynamic logic (PDL) on trees in these applications, and study as a sanity check the complexity of the corresponding model-checking problem: although complete for exponential time in the general case, we find natural restrictions on grammars for our applications and establish complexities ranging from nondeterministic polynomial time to polynomial space in the relevant cases.} }

@inproceedings{ABBDF-pads13, address = {Montreal, Canada}, month = may, year = 2013, publisher = {ACM Press}, editor = {Wainer, Gabriel A.}, acronym = {{PADS}'13}, booktitle = {{P}roceedings of the 1st {ACM} {SIGSIM} {C}onference on {P}rinciples of {A}dvanced {D}iscrete {S}imulation ({PADS}'13)}, author = {Amparore, Elvio Gilberto and Barbot, Beno{\^\i}t and Beccuti, Marco and Donatelli, Susanna and Franceschinis, Giuliana}, title = {Simulation-based Verification of Hybrid Automata Stochastic Logic Formulas for Stochastic Symmetric Nets}, pages = {253-264}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABBDF-pads13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABBDF-pads13.pdf}, doi = {10.1145/2486092.2486124}, abstract = {The Hybrid Automata Stochastic Logic (HASL) has been recently defined as a flexible way to express classical performance measures as well as more complex, path-based ones (generically called {"}HASL formulas{"}). The considered paths are executions of Generalized Stochastic Petri Nets (GSPN), which are an extension of the basic Petri net formalism to define discrete event stochastic processes. The computation of the HASL formulas for a GSPN model is demanded to the COSMOS tool, that applies simulation techniques to the formula computation. Stochastic Symmetric Nets (SSN) are an high level Petri net formalism, of the \emph{colored} type, in which tokens can have an identity, and it is well known that colored Petri nets allow one to describe systems in a more compact and parametric form than basic (uncolored) Petri nets. In this paper we propose to extend HASL and COSMOS to support colors, so that performance formulas for SSN can be easily defined and evaluated. This requires a new definition of the logic, to ensure that colors are taken into account in a correct and useful manner, and a significant extension of the COSMOS tool.} }

@inproceedings{BHLM-dlt13, address = {Marne-la-Vall{\'e}e, France}, month = jun, year = 2013, volume = {7907}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {B{\'e}al, Marie-Pierre and Carton, Olivier}, acronym = {{DLT}'13}, booktitle = {{P}roceedings of the 17th {I}nternational {C}onference on {D}evelopments in {L}anguage {T}heory ({DLT}'13)}, author = {Bollig, Benedikt and Habermehl, Peter and Leucker, Martin and Monmege, Benjamin}, title = {A~Fresh Approach to Learning Register Automata}, pages = {118-130}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHLM-dlt13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHLM-dlt13.pdf}, doi = {10.1007/978-3-642-38771-5_12}, abstract = {This paper provides an Angluin-style learning algorithm for a class of register automata supporting the notion of \emph{fresh} data values. More specifically, we introduce \emph{session automata} which are well suited for modeling protocols in which sessions using fresh values are of major interest, like in security protocols or ad-hoc networks. We show that session automata (i)~have an expressiveness partly extending, partly reducing that of register automata, (ii)~admit a symbolic regular representation, and (iii)~have a decidable equivalence and model-checking problem (unlike register automata). Using these results, we establish a learning algorithm to infer session automata through membership and equivalence queries. Finally, we strengthen the robustness of our automaton by its characterization in monadic second-order logic.} }

@inproceedings{BCHKS-lata13, address = {Bilbao, Spain}, month = apr, year = 2013, volume = {7810}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Dediu, Adrian Horia and Mart{\'\i}n-Vide, Carlos and Truthe, Bianca}, acronym = {{LATA}'13}, booktitle = {{P}roceedings of the 7th {I}nternational {C}onference on {L}anguage and {A}utomata {T}heory and {A}pplications ({LATA}'13)}, author = {Bollig, Benedikt and Cyriac, Aiswarya and H{\'e}lou{\"e}t, Lo{\"\i}c and Kara, Ahmet and Schwentick, {\relax Th}omas}, title = {Dynamic Communicating Automata and Branching High-Level {MSC}s}, pages = {177-189}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCHKS-lata13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCHKS-lata13.pdf}, doi = {10.1109/REVET.2012.6195253}, abstract = {We study dynamic communicating automata~(DCA), an~extension of classical communicating finite-state machines that allows for dynamic creation of processes. The behavior of a DCA can be described as a set of message sequence charts~(MSCs). While DCA serve as a model of an implementation, we propose branching high-level MSCs~(bHMSCs) on the specification side. Our focus is on the implementability problem: given a bHMSC, can one construct an equivalent DCA? As this problem is undecidable, we introduce the notion of executability, a decidable necessary criterion for implementability. We show that executability of bHMSCs is EXPTIME-complete. We~then identify a class of bHMSCs for which executability effectively implies implementability.} }

@inproceedings{CCP-cav13, address = {Saint Petersburg, Russia}, month = jul, year = 2013, volume = {8044}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Sharygina, Natasha and Veith, Helmut}, acronym = {{CAV}'13}, booktitle = {{P}roceedings of the 25th {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV}'13)}, author = {Cheval, Vincent and Cortier, V{\'e}ronique and Plet, Antoine}, title = {Lengths may break privacy~---or~how to check for equivalences with length}, pages = {708-723}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCP-cav13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCP-cav13.pdf}, doi = {10.1007/978-3-642-39799-8_50}, abstract = {Security protocols have been successfully analyzed using symbolic models, where messages are represented by terms and protocols by processes. Privacy properties like anonymity or untraceability are typically expressed as equivalence between processes. While some decision procedures have been proposed for automatically deciding process equivalence, all existing approaches abstract away the information an attacker may get when observing the length of messages.\par In this paper, we study process equivalence with length tests. We first show that, in the static case, almost all existing decidability results (for static equivalence) can be extended to cope with length tests. In the active case, we prove decidability of trace equivalence with length tests, for a bounded number of sessions and for standard primitives. Our result relies on a previous decidability result from Cheval~\emph{et~al.} (without length tests). Our procedure has been implemented and we have discovered a new flaw against privacy in the biometric passport protocol.} }

@inproceedings{HIOP-cav13, address = {Saint Petersburg, Russia}, month = jul, year = 2013, volume = {8044}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Sharygina, Natasha and Veith, Helmut}, acronym = {{CAV}'13}, booktitle = {{P}roceedings of the 25th {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV}'13)}, author = {Haase, Christoph and Ishtiaq, Samin and Ouaknine, Jo{\"e}l and Parkinson, Matthew}, title = {SeLoger: A~Tool for Graph-Based Reasoning in Separation Logic}, pages = {790-795}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/HIOP-cav13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HIOP-cav13.pdf}, doi = {10.1007/978-3-642-39799-8_55}, abstract = {This paper introduces the tool SeLoger, which is a reasoner for satisfiability and entailment in a fragment of separation logic with pointers and linked lists. SeLoger builds upon and extends graph-based algorithms that have recently been introduced in order to settle both decision problems in polynomial time. Running SeLoger on standard benchmarks shows that the tool outperforms current state-of-the-art tools by orders of magnitude.} }

@inproceedings{OS-cav13, address = {Saint Petersburg, Russia}, month = jul, year = 2013, volume = {8044}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Sharygina, Natasha and Veith, Helmut}, acronym = {{CAV}'13}, booktitle = {{P}roceedings of the 25th {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV}'13)}, author = {Sankur, Ocan}, title = {Shrinktech: A~Tool for the Robustness Analysis of Timed Automata}, pages = {1006-1012}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/OS-cav13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/OS-cav13.pdf}, doi = {10.1007/978-3-642-39799-8_72}, abstract = {We present a tool for the robustness analysis of timed automata, that can check whether a given time-abstract behaviour of a timed automaton is still present when the guards are perturbed. The perturbation model we consider is shrinking, which corresponds to increasing lower bounds and decreasing upper bounds in the clock guards by parameters. The tool synthesizes these parameters for which the given behaviour is preserved in the new automaton if possible, and generates a counter-example otherwise. This can be used for 1)~robustness analysis, and for 2)~deriving implementations under imprecisions.} }

@inproceedings{RB-cav13, address = {Saint Petersburg, Russia}, month = jul, year = 2013, volume = {8044}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Sharygina, Natasha and Veith, Helmut}, acronym = {{CAV}'13}, booktitle = {{P}roceedings of the 25th {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV}'13)}, author = {Brenguier, Romain}, title = {{PRALINE}: A~Tool for Computing Nash Equilibria in Concurrent Games}, pages = { 890-895}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/RB-cav13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RB-cav13.pdf}, doi = {10.1007/978-3-642-39799-8_63}, abstract = {We present PRALINE, which is the first tool to compute Nash equilibria in games played over graphs. We consider concurrent games: at each step, players choose their actions independently. There can be an arbitrary number of players. The preferences of the players are given by payoff functions that map states to integers, the goal for a player is then to maximize the limit superior of her payoff; this can be seen as a generalization of B{\"u}chi objectives. PRALINE looks for pure Nash equilibria in these games. It can construct the strategies of the equilibrium and users can play against it to test the equilibrium. We give the idea behind its implementation and present examples of its practical use.} }

@inproceedings{RSK-pn13, address = {Milano, Italy}, month = jun, year = 2013, volume = {7927}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Colom, Jos{\'e}-Manuel and Desel, J{\"o}rg}, acronym = {{PETRI~NETS}'13}, booktitle = {{P}roceedings of the 34th {I}nternational {C}onference on {A}pplications and {T}heory of {P}etri {N}ets ({PETRI~NETS}'13)}, author = {Rodr{\'\i}guez, C{\'e}sar and Schwoon, Stefan and Khomenko, Victor}, title = {Contextual Merged Processes}, pages = {29-48}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/RSK-atpn13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RSK-atpn13.pdf}, doi = {10.1007/978-3-642-38697-8_3}, abstract = {We integrate two compact data structures for representing state spaces of Petri nets: merged processes and contextual prefixes. The resulting data structure, called contextual merged processes (CMP), combines the advantages of the original ones and copes with several important sources of state space explosion: concurrency, sequences of choices, and concurrent read accesses to shared resources. In particular, we demonstrate on a number of benchmarks that CMPs are more compact than either of the original data structures. Moreover, we sketch a polynomial (in the CMP size) encoding into SAT of the model-checking problem for reachability properties.} }

@inproceedings{FH-pn13, address = {Milano, Italy}, month = jun, year = 2013, volume = {7927}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Colom, Jos{\'e}-Manuel and Desel, J{\"o}rg}, acronym = {{PETRI~NETS}'13}, booktitle = {{P}roceedings of the 34th {I}nternational {C}onference on {A}pplications and {T}heory of {P}etri {N}ets ({PETRI~NETS}'13)}, author = {Fraca, Est{\'\i}baliz and Haddad, Serge}, title = { Complexity Analysis of Continuous {P}etri Nets}, pages = {170-189}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FH-pn13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FH-pn13.pdf}, doi = {10.1007/978-3-642-38697-8_10}, abstract = {At the end of the eighties, continuous Petri nets were introduced for: (1)~alleviating the combinatory explosion triggered by discrete Petri nets and, (2)~modelling the behaviour of physical systems whose state is composed of continuous variables. Since then several works have established that the computational complexity of deciding some standard behavioural properties of Petri nets is reduced in this framework. Here we first establish the decidability of additional properties like boundedness and reachability set inclusion. We also design new decision procedures for the reachability and lim-reachability problems with a better computational complexity. Finally we provide lower bounds characterising the exact complexity class of the boundedness, the reachability, the deadlock freeness and the liveness problems.} }

@inproceedings{HHM-pn13, address = {Milano, Italy}, month = jun, year = 2013, volume = {7927}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Colom, Jos{\'e}-Manuel and Desel, J{\"o}rg}, acronym = {{PETRI~NETS}'13}, booktitle = {{P}roceedings of the 34th {I}nternational {C}onference on {A}pplications and {T}heory of {P}etri {N}ets ({PETRI~NETS}'13)}, author = {Haddad, Serge and Hennicker, Rolf and M{\o}ller, Mikael H.}, title = {Channel Properties of Asynchronously Composed {P}etri~Nets}, pages = {369-388}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/HHM-pn13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HHM-pn13.pdf}, doi = {10.1007/978-3-642-38697-8_20}, abstract = {We consider asynchronously composed I/O-Petri nets (AIOPNs) with built-in communication channels. They are equipped with a compositional semantics in terms of asynchronous I/O-transition systems (AIOTSs) admitting infinite state spaces. We study various channel properties that deal with the production and consumption of messages exchanged via the communication channels and establish useful relationships between them. In order to support incremental design we show that the channel properties considered in this work are preserved by asynchronous composition, i.e. they are compositional. As a crucial result we prove that the channel properties are decidable for AIOPNs.} }

@inproceedings{AR-qapl2013, address = {Rome, Italy}, volume = {117}, series = {Electronic Proceedings in Theoretical Computer Science}, month = jun, year = 2013, editor = {Bortolussi, Luca and Wiklicky, Herbert}, acronym = {{QAPL}'13}, booktitle = {{P}roceedings of the 11th {I}nternational {W}orkshop on {Q}uantitative {A}spects of {P}rogramming {L}anguages ({QAPl}'13)}, author = {Arul, Arjun and Reichert, Julien}, title = {The Complexity of Robot Games on the Integer Line}, pages = {132-148}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AR-qapl13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AR-qapl13.pdf}, doi = {10.4204/EPTCS.117.9}, abstract = {In robot games on~\(\mathbb{Z}\), two players add integers to a counter. Each player has a finite set from which he picks the integer to add, and the objective of the first player is to let the counter reach~\(0\). We present an exponential-time algorithm for deciding the winner of a robot game given the initial counter value, and prove a matching lower bound.} }

@inproceedings{BS-qapl2013, address = {Rome, Italy}, volume = {117}, series = {Electronic Proceedings in Theoretical Computer Science}, month = jun, year = 2013, editor = {Bortolussi, Luca and Wiklicky, Herbert}, acronym = {{QAPL}'13}, booktitle = {{P}roceedings of the 11th {I}nternational {W}orkshop on {Q}uantitative {A}spects of {P}rogramming {L}anguages ({QAPl}'13)}, author = {Bertrand, Nathalie and Schnoebelen, {\relax Ph}ilippe}, title = {Solving stochastic B{\"u}chi games on infinite arenas with a finite attractor}, pages = {116-131}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-qapl2013.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-qapl2013.pdf}, doi = {10.4204/EPTCS.117.8}, abstract = {We consider games played on an infinite probabilistic arena where the first player aims at satisfying generalized B{\"u}chi objectives almost surely, i.e., with probability one. We provide a fixpoint characterization of the winning sets and associated winning strategies in the case where the arena satisfies the finite-attractor property. From this we directly deduce the decidability of these games on probabilistic lossy channel systems.} }

@book{AS-book13, author = {Andr{\'e}, {\'E}tienne and Soulat, Romain}, title = {The~Inverse Method}, publisher = {Wiley-ISTE}, year = 2013, month = jan, isbn = {9781848214477}, note = {176~pages}, url = {http://www.iste.co.uk/index.php?f=a&ACTION=View&id=546}, abstract = {This book introduces state-of-the-art verification techniques for real-time embedded systems, based on the inverse method for parametric timed automata. It reviews popular formalisms for the specification and verification of timed concurrent systems and, in particular, timed automata as well as several extensions such as timed automata equipped with stopwatches, linear hybrid automata and affine hybrid automata.\par The inverse method is introduced, and its benefits for guaranteeing robustness in real-time systems are shown. Then, it is shown how an iteration of the inverse method can solve the good parameters problem for parametric timed automata by computing a behavioral cartography of the system. Different extensions are proposed particularly for hybrid systems and applications to scheduling problems using timed automata with stopwatches. Various examples, both from the literature and industry, illustrate the techniques throughout the book.\par Various parametric verifications are performed, in particular of abstractions of a memory circuit sold by the chipset manufacturer ST-Microelectronics, as well as of the prospective flight control system of the next generation of spacecraft designed by ASTRIUM Space Transportation.} }

@article{CDH-fmsd13, publisher = {Springer}, journal = {Formal Methods in System Design}, author = {Chatterjee, Krishnendu and Doyen, Laurent and Henzinger, {\relax Th}omas A.}, title = {A~survey of partial-observation stochastic parity games}, volume = 43, number = 2, pages = {268-284}, month = oct, year = 2013, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDH-fmsd13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDH-fmsd13.pdf}, doi = {10.1007/s10703-012-0164-2}, abstract = {We consider two-player zero-sum stochastic games on graphs with \(\omega\)-regular winning conditions specified as parity objectives. These games have applications in the design and control of reactive systems. We survey the complexity results for the problem of deciding the winner in such games, and in classes of interest obtained as special cases, based on the information and the power of randomization available to the players, on the class of objectives and on the winning mode.\par On the basis of information, 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). The one-sided partial-observation games have two important subclasses: the one-player games, known as partial-observation Markov decision processes~(POMDPs), and the blind one-player games, known as probabilistic automata.\par On the basis of randomization, (a)~the players may not be allowed to use randomization (pure strategies), or (b)~they may choose a probability distribution over actions but the actual random choice is external and not visible to the player (actions invisible), or (c)~they may use full randomization.\par Finally, various classes of games are obtained by restricting the parity objective to a reachability, safety, B{\"u}chi, or coB{\"u}chi condition. We also consider several winning modes, such as sure-winning (i.e., all outcomes of a strategy have to satisfy the winning condition), almost-sure winning (i.e., winning with probability~\(1\)), limit-sure winning (i.e., winning with probability arbitrarily close to~\(1\)), and value-threshold winning (i.e., winning with probability at least~\(v\), where \(v\) is a given rational).} }

@article{CDKR-fmsd13, publisher = {Springer}, journal = {Formal Methods in System Design}, author = {Chevalier, C{\'e}line and Delaune, St{\'e}phanie and Kremer, Steve and Ryan, Mark D.}, title = {Composition of Password-based Protocols}, volume = {43}, number = {3}, pages = {369-413}, month = dec, year = 2013, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDKR-fmsd13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDKR-fmsd13.pdf}, doi = {10.1007/s10703-013-0184-6}, abstract = {Formal and symbolic techniques are extremely useful for modelling and analysing security protocols. They have helped to improve our understanding of such protocols, allowed us to discover flaws, and they also provide support for protocol design. However, such analyses usually consider that the protocol is executed in isolation or assume a bounded number of protocol sessions. Hence, no security guarantee is provided when the protocol is executed in a more complex environment.\par In this paper, we study whether password protocols can be safely composed, even when a same password is reused. More precisely, we present a transformation which maps a password protocol that is secure for a single protocol session (a~decidable problem) to a protocol that is secure for an unbounded number of sessions. Our result provides an effective strategy to design secure password protocols: (i)~design a protocol intended to be secure for one protocol session; (ii)~apply our transformation and obtain a protocol which is secure for an unbounded number of sessions. Our technique also applies to compose different password protocols allowing us to obtain both inter-protocol and inter-session composition.} }

@article{HMN-fi13, publisher = {{IOS} Press}, journal = {Fundamenta Informaticae}, author = {Haddad, Serge and Mairesse, Jean and Nguyen, Hoang-Thach}, title = {Synthesis and Analysis of Product-form {P}etri Nets}, year = {2013}, volume = {122}, number = {1-2}, pages = {147-172}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/HMN-fi13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HMN-fi13.pdf}, doi = {10.3233/FI-2013-786}, abstract = {For a large Markovian model, a {"}product form{"} is an explicit description of the steady-state behaviour which is otherwise generally untractable. Being first introduced in queueing networks, it has been adapted to Markovian Petri nets. Here we address three relevant issues for product-form Petri nets which were left fully or partially open: (1)~we~provide a sound and complete set of rules for the synthesis; (2)~we~characterise the exact complexity of classical problems like reachability; (3)~we~introduce a new subclass for which the normalising constant (a~crucial value for product-form expression) can be efficiently computed.} }

@inproceedings{BGM-fossacs13, address = {Rome, Italy}, month = mar, year = 2013, volume = {7794}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Pfenning, Frank}, acronym = {{FoSSaCS}'13}, booktitle = {{P}roceedings of the 16th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'13)}, author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin}, title = {Weighted Specifications over Nested Words}, pages = {385-400}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-fossacs13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-fossacs13.pdf}, doi = {10.1007/978-3-642-37075-5_25}, abstract = {This paper studies several formalisms to specify quantitative properties of finite nested words (or~equivalently finite unranked trees). These can be used for XML documents or recursive programs: for~instance, counting how often a given entry occurs in an XML document, or~computing the memory required for a recursive program execution. Our main interest is to translate these properties, as efficiently as possible, into an automaton, and to use this computational device to decide problems related to the properties (e.g.,~emptiness, model checking, simulation) or to compute the value of a quantitative specification over a given nested word. The specification formalisms are weighted regular expressions (with forward and backward moves following linear edges or call-return edges), weighted first-order logic, and weighted temporal logics. We~introduce weighted automata walking in nested words, possibly dropping\slash lifting (reusable) pebbles during the traversal. We prove that the evaluation problem for such automata can be done very efficiently if the number of pebble names is small, and we also consider the emptiness problem.} }

@article{demri-jcss13, publisher = {Elsevier Science Publishers}, journal = {Journal of Computer and System Sciences}, author = {Demri, St{\'e}phane}, title = {On selective unboundedness of~{VASS}}, year = {2013}, volume = {79}, number = {5}, pages = {689-713}, month = aug, url = {http://www.lsv.fr/Publis/PAPERS/PDF/demri-jcss13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/demri-jcss13.pdf}, doi = {10.1016/j.jcss.2013.01.014}, abstract = {Numerous properties of vector addition systems with states amount to checking the (un)boundedness of some selective feature (e.g., number of reversals, counter values, run lengths). 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., regularity detection problem and reversal-boundedness detection problem. 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 are present in the paper), strong promptness detection problem and regularity detection. Our analysis is sufficiently refined so as to obtain a polynomial-space bound when the dimension is fixed.} }

@incollection{GLJ-hg13, noaddress = {}, month = jan, year = 2013, volume = 7797, series = {Lecture Notes in Computer Science}, publisher = {Springer}, noacronym = {}, booktitle = {Programming Logics~-- Essays in Memory of {H}arald {G}anzinger}, editor = {Voronkov, Andrei and Weidenbach, Christoph}, author = {Goubault{-}Larrecq, Jean and Jouannaud, Jean-Pierre}, title = {The Blossom of Finite Semantic Trees}, pages = {90-122}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/GLJ-hg13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLJ-hg13.pdf} }

@phdthesis{bonnet-phd2013, author = {Bonnet, R{\'e}mi}, title = {Theory of Well-Structured Transition Systems and Extended Vector-Addition Systems}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2013, month = jan, url = {http://www.lsv.fr/Publis/PAPERS/PDF/bonnet-phd13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bonnet-phd13.pdf} }

@techreport{rr-lsv-13-02, author = {Doyen, Laurent and Rabinovich, Alexander}, title = {Robot games}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2013}, month = jan, type = {Research Report}, number = {LSV-13-02}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2013-02.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2013-02.pdf}, versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2013-02-v1.pdf, 20130124}, note = {2~pages}, abstract = {We introduce robot games, and we give the simplest definition for which decidability is open.} }

@inproceedings{BNS-cc13, address = {Rome, Italy}, month = mar, year = 2013, volume = {7791}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {De{~}Bosschere, Koen and Jhala, Ranjit}, acronym = {{CC}'13}, booktitle = {{P}roceedings of the 22nd {I}nternational {C}onference on {C}ompiler {C}onstruction ({CC}'13)}, author = {Eberhard Bertsch and Mark-Jan Nederhof and Sylvain Schmitz}, title = {On {LR} Parsing with Selective Delays}, pages = {244-263}, url = {http://hal.archives-ouvertes.fr/hal-00769668}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BNS-cc13.pdf}, doi = {10.1007/978-3-642-37051-9_13}, abstract = {The paper investigates an extension of LR parsing that allows the delay of parsing decisions until a sufficient amount of context has been processed. We provide two characterizations for the resulting class of grammars, one based on grammar transformations, the other on the direct construction of a parser. We also report on experiments with a grammar collection.} }

@inproceedings{KS-fossacs13, address = {Rome, Italy}, month = mar, year = 2013, volume = {7794}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Pfenning, Frank}, acronym = {{FoSSaCS}'13}, booktitle = {{P}roceedings of the 16th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'13)}, author = {Karandikar, Prateek and Schmitz, Sylvain}, title = {The Parametric Ordinal-Recursive Complexity of {P}ost Embedding Problems}, pages = {273-288}, url = {http://arxiv.org/abs/1211.5259}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-fossacs13.pdf}, doi = {10.1007/978-3-642-37075-5_18}, abstract = {Post Embedding Problems are a family of decision problems based on the interaction of a rational relation with the subword embedding ordering, and are used in the literature to prove non multiply-recursive complexity lower bounds. We refine the construction of Chambart and Schnoebelen (LICS~2008) and prove parametric lower bounds depending on the size of the alphabet.} }

@misc{reachard-18, author = {Finkel, Alain}, title = {REACHARD~-- Compte-rendu interm{\'e}diaire}, month = mar, year = {2013}, note = {9~pages}, type = {Contract Report}, howpublished = {Deliverable~D2 Reachard (ANR-11-BS02-001)} }

@article{CFM-ijfcs13, publisher = {World Scientific}, journal = {International Journal of Foundations of Computer Science}, author = {Cadilhac, Micha{\"e}l and Finkel, Alain and McKenzie, Pierre}, title = {Unambiguous Contrained Automata}, volume = 24, number = 7, month = nov, year = 2013, pages = {1099-1116}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-ijfcs13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-ijfcs13.pdf}, doi = {10.1142/S0129054113400339}, abstract = {The class of languages captured by Constrained Automata~(CA) that are unambiguous is shown to possess more closure properties than the provably weaker class captured by deterministic~CA. Problems decidable for deterministic CA are nonetheless shown to remain decidable for unambiguous~CA, and testing for regularity is added to this set of decidable problems. Unambiguous CA~are then shown incomparable with deterministic reversal-bounded machines in terms of expressivity, and a deterministic model equivalent to unambiguous~CA is identified.} }

@inproceedings{BDD-frocos13, address = {Nancy, France}, month = sep, year = 2013, volume = 8152, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, editor = {Fontaine, Pascal and Ringeissen, Christophe and Schmidt, Renate A.}, acronym = {{FroCoS}'13}, booktitle = {{P}roceedings of the 9th {I}nternational {S}ymposium on {F}rontiers of {C}ombining {S}ystems ({FroCoS}'13)}, author = {Barrett, Clark and Demri, St{\'e}phane and Deters, Morgan}, title = {Witness runs for counter machines}, pages = {120-150}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDD-frocos13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDD-frocos13.pdf}, doi = {10.1007/978-3-642-40885-4_9}, abstract = {In this paper, we present recent results about the verification of counter machines by using decision procedures for Presburger arithmetic. We recall several known classes of counter machines for which the reachability sets are Presburger-definable as well as temporal logics with arithmetical constraints. We discuss issues related to flat counter machines, path schema enumeration, and the use of SMT solvers.} }

@mastersthesis{m2-stan13, author = {Stan, Daniel}, title = {{\'E}quilibres mixtes dans les jeux concurrents}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2013}, month = sep, url = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-stan13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-stan13.pdf}, note = {29~pages} }

@article{BS13-TSI-games, publisher = {Herm{\`e}s}, journal = {Technique et Science Informatiques}, author = {Berwanger, Dietmar and Serre, Olivier}, editor = {Berwanger, Dietmar and Serre, Olivier}, title = {Th{\'e}orie des jeux en informatique}, booktitle = {Th{\'e}orie des jeux en informatique}, volume = 32, number = {9-10}, year = 2013, month = dec, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BS13-TSI-games.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BS13-TSI-games.pdf} }

@inproceedings{GLO-fps13, address = {La Rochelle, France}, month = oct, year = 2013, volume = 8352, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Danger, Jean-Luc and Debbabi, Mourad and Marion, Jean-Yves and Garcia{-}Alfaro, Joaquin and Zincir{-}Heywood,Nur}, acronym = {{FPS}'13}, booktitle = {{R}evised {S}elected {P}apers of the 6th {I}nternational {S}ymposium on {F}oundations and {P}ractice of {S}ecurity ({FPS}'13)}, author = {Goubault{-}Larrecq, Jean and Olivain, Julien}, title = {On~the Efficiency of Mathematics in Intrusion Detection: The NetEntropy Case.}, pages = {3-16}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/GLO-fps13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLO-fps13.pdf}, doi = {10.1007/978-3-319-05302-8_1}, abstract = {NetEntropy is a plugin to the Orchids intrusion detection tool that is originally meant to detect some subtle attacks on implementations of cryptographic protocols such as {SSL\slash TLS}. NetEntropy compares the sample entropy of a data stream to a known profile, and flags any significant variation. Our point is to stress the \emph{mathematics} behind NetEntropy: the reason of the rather incredible precision of NetEntropy is to be found in theorems due to Paninski and Moddemeijer.} }

@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.", }}

@mastersthesis{m2-hirschi, author = {Hirschi, Lucca}, title = {Reduction of interleavings for trace equivalence checking of security protocols}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2013}, month = aug }

@misc{JGL:stc13, author = {Goubault{-}Larrecq, Jean}, howpublished = {Invited talk (semi-plenary speaker), Summer Topology Conference, North Bay, Ontario, CA}, month = jul, title = {A few pearls in the theory of quasi-metric spaces}, year = {2013} }

@misc{JGL:dga13, author = {Goubault{-}Larrecq, Jean}, howpublished = {S{\'e}minaire DGA Innosciences. DGA, Bagneux}, month = jun, title = {{OrchIDS}, ou : de l'importance de la s{\'e}mantique}, year = {2013} }

@misc{JGL:at13, author = {Goubault{-}Larrecq, Jean}, howpublished = {Invited talk, Workshop on Asymmetric Topology, Summer Topology Conference, North Bay, Ontario, CA}, month = jul, title = {A short proof of the {Schr{\"o}der-Simpson} theorem}, year = {2013} }

@mastersthesis{m2-Fang, author = {Fang, Erwin}, title = {{Permissive multi-strategies in timed games}}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2013}, month = aug }

*This file was generated by
bibtex2html 1.98.*