@article{JKS-lmcs14, journal = {Logical Methods in Computer Science}, author = {Jancar, Petr and Karandikar, Prateek and Schnoebelen, {\relax Ph}ilippe}, title = {On Reachability for Unidirectional Channel Systems Extended with Regular Tests}, year = {2015}, volume = 11, number = {{2:2}}, month = apr, nopages = {}, url = {http://arxiv.org/abs/1406.5067}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JKS-lmcs14.pdf}, doi = {10.2168/LMCS-11(2:2)2015}, abstract = {{"}Unidirectional channel systems{"} (Chambart~\& Schnoebelen, CONCUR~2008) are finite-state systems where one-way communication from a Sender to a Receiver goes via one reliable and one unreliable unbounded fifo channel. While reachability is decidable for these systems, equipping them with the possibility of testing regular properties on the contents of channels makes it undecidable. Decidability is preserved when only emptiness and nonemptiness tests are considered: the proof relies on an elaborate reduction to a generalized version of Post's Embedding Problem.} }

@article{KKS-ipl14, publisher = {Elsevier Science Publishers}, journal = {Information Processing Letters}, author = {Karandikar, Prateek and Kufleitner, Manfred and Schnoebelen, {\relax Ph}ilippe}, title = {On the index of {S}imon's congruence for piecewise testability}, year = {2015}, month = apr, volume = {15}, number = {4}, pages = {515-519}, url = {http://arxiv.org/abs/1310.1278}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KKS-ipl14.pdf}, doi = {10.1016/j.ipl.2014.11.008}, abstract = {Simon's congruence, denoted \(\sim_{n}\), relates words having the same subwords of length up to~\(n\). We~show that, over a \(k\)-letter alphabet, the~number of words modulo~\(\sim_{n}\) is in \(2^{\Theta(n^{k-1}\cdot\log n)}\).} }

@article{ABV-tocsys15, publisher = {Springer}, journal = {Theory of Computing Systems}, author = {Abiteboul, Serge and Bourhis, Pierre and Vianu, Victor}, title = {Highly Expressive Query Languages for Unordered Data Trees}, pages = {927-966}, year = 2015, month = nov, volume = {57}, number = {4}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABV-tocsys15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABV-tocsys15.pdf}, doi = {10.1007/s00224-015-9617-5}, abstract = {We study highly expressive query languages for unordered data trees, using as formal vehicles Active XML and extensions of languages in the while family. All languages may be seen as adding some form of control on top of a set of basic pattern queries. The results highlight the impact and interplay of different factors: the expressive power of basic queries, the embedding of computation into data (as in Active XML), and the use of deterministic vs. nondeterministic control. All languages are Turing complete, but not necessarily query complete in the sense of Chandra and Harel. Indeed, we show that some combinations of features yield serious limitations, analogous to FO\(^{k}\) definability in the relational context. On the other hand, the limitations come with benefits such as the existence of powerful normal forms providing opportunities for optimization. Other languages are {"}almost{"} complete, but fall short because of subtle limitations reminiscent of the copy elimination problem in object databases.} }

@article{AADMS-tocsys14, publisher = {Springer}, journal = {Theory of Computing Systems}, author = {Abiteboul, Serge and Amsterdamer, Yael and Deutch, Daniel and Milo, Tova and Senellart, Pierre}, title = {Optimal Probabilistic Generation of {XML} Documents}, pages = {806-842}, year = 2015, month = nov, volume = {57}, number = {4}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AADMS-tocsys14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AADMS-tocsys14.pdf}, doi = {10.1007/s00224-014-9581-5}, abstract = {We study the problem of, given a corpus of XML documents and its schema, finding an optimal (generative) probabilistic model, where optimality here means maximizing the likelihood of the particular corpus to be generated. Focusing first on the structure of documents, we present an efficient algorithm for finding the best generative probabilistic model, in the absence of constraints. We further study the problem in the presence of integrity constraints, namely key, inclusion, and domain constraints. We study in this case two different kinds of generators. First, we consider a continuation-test generator that performs, while generating documents, tests of schema satisfiability; these tests prevent from generating a document violating the constraints but, as we will see, they are computationally expensive. We also study a restart generator that may generate an invalid document and, when this is the case, restarts and tries again. Finally, we consider the injection of data values into the structure, to obtain a full XML document. We study different approaches for generating these values.} }

@article{CDGH-ic15, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Chatterjee, Krishnendu and Doyen, Laurent and Gimbert, Hugo and Henzinger, Thomas A.}, title = {Randomness for free}, volume = {245}, month = dec, year = 2015, pages = {3-16}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDGH-ic15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDGH-ic15.pdf}, doi = {10.1016/j.ic.2015.06.003}, abstract = {We consider two-player zero-sum games on finite-state graphs. These games can be classified on the basis of the information of the players and on the mode of interaction between them. On the basis of information the classification is as follows: (a)~partial-observation (both players have partial view of the game); (b)~one-sided complete-observation (one player has complete observation); and (c)~complete-observation (both players have complete view of the game). On~the basis of mode of interaction we have the following classification: (a)~concurrent (players interact simultaneously); and (b)~turn-based (players interact in turn). The~two sources of randomness in these games are randomness in the transition function and randomness in the strategies. In general, randomized strategies are more powerful than deterministic strategies, and probabilistic transitions give more general classes of games. We present a complete characterization for the classes of games where randomness is not helpful~in: (a)~the transition function (probabilistic transitions can be simulated by deterministic transitions); and (b)~strategies (pure strategies are as powerful as randomized strategies). As~a consequence of our characterization we obtain new undecidability results for these games.} }

@article{LM-ic14, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas}, title = {Augmenting {ATL} with strategy contexts}, volume = {245}, month = dec, year = 2015, pages = {98-123}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2014-05.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2014-05.pdf}, doi = {10.1016/j.ic.2014.12.020}, abstract = {We study the extension of the alternating-time temporal logic (ATL) with strategy contexts: contrary to the original semantics, in this semantics the strategy quantifiers do not reset the previously selected strategies.\par We show that our extension ATLsc is very expressive, but that its decision problems are quite hard: model checking is \(k\)-EXPTIME-complete when the formula has k nested strategy quantifiers; satisfiability is undecidable, but we prove that it is decidable when restricting to turn-based games. Our algorithms are obtained through a very convenient translation to QCTL (the~computation-tree logic CTL extended with atomic quantification), which we show also applies to Strategy Logic, as well as when strategy quantification ranges over memoryless strategies.} }

@article{jgl-jlap14, publisher = {Elsevier Science Publishers}, journal = {Journal of Logic and Algebraic Methods in Programming}, author = {Goubault{-}Larrecq, Jean}, title = {Full Abstraction for Non-Deterministic and Probabilistic Extensions of {PCF}~{I}: the~Angelic Cases}, volume = 84, number = 1, year = 2015, month = jan, pages = {155-184}, opteditor = {Berger, Ulrich}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/jgl-jlap14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/jgl-jlap14.pdf}, doi = {10.1016/j.jlamp.2014.09.003}, abstract = {We examine several extensions and variants of Plotkin's language~PCF, including non-deterministic and probabilistic choice constructs. For~each, we give an operational and a denotational semantics, and compare them. In each case, we show soundness and computational adequacy: the two semantics compute the same values at ground types. Beyond this, we establish full abstraction (the~observational preorder coincides with the denotational preorder) in a number of cases. In~the probabilistic cases, this requires the addition of so-called statistical termination testers to the language.} }

@article{BMS-tcs14, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {Bouyer, Patricia and Markey, Nicolas and Sankur, Ocan}, title = {Robust Reachability in Timed Automata and Games: A~Game-based Approach}, volume = 563, year = {2015}, month = jan, pages = {43-74}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-tcs14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-tcs14.pdf}, doi = {10.1016/j.tcs.2014.08.014 }, abstract = {Reachability checking is one of the most basic problems in verification. By solving this problem in a game, one can synthesize a strategy that dictates the actions to be performed for ensuring that the target location is reached. In this work, we are interested in synthesizing {"}robust{"} strategies for ensuring reachability of a location in timed automata. By robust, we mean that it must still ensure reachability even when the delays are perturbed by the environment. We model this perturbed semantics as a game between the controller and its environment, and solve the parameterized robust reachability problem: we show that the existence of an upper bound on the perturbations under which there is a strategy reaching a target location is EXPTIME-complete. We also extend our algorithm, with the same complexity, to turn-based timed games, where the successor state is entirely determined by the environment in some locations.} }

@article{FL-sosym14, publisher = {Springer}, journal = {Software~\& System Modeling}, author = {Finkel, Alain and Leroux, J{\'e}r{\^o}me}, title = {Recent and simple algorithms for {P}etri nets}, volume = 14, number = 2, year = {2015}, month = may, pages = {719-725}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FL-sosym14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FL-sosym14.pdf}, doi = {10.1007/s10270-014-0426-0}, abstract = {We show how inductive invariants can be used to solve coverability, boundedness and reachability problems for Petri nets. This approach provides algorithms that are conceptually simpler than previously pblished ones.} }

@article{KS-msttocs14, publisher = {Springer}, journal = {Theory of Computing Systems}, author = {Karandikar, Prateek and Schnoebelen, {\relax Ph}ilippe}, title = {Generalized {P}ost Embedding Problems}, year = {2015}, volume = 56, number = 4, pages = {697-716}, month = may, url = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-msttocs14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-msttocs14.pdf}, doi = {10.1007/s00224-014-9561-9}, abstract = {The Regular Post Embedding Problem extended with partial (co)directness is shown decidable. This extends to universal and\slash or counting versions. It is also shown that combining directness and codirectness in Post Embedding problems leads to undecidability.} }

@article{BBMU-lmcs14, journal = {Logical Methods in Computer Science}, author = {Bouyer, Patricia and Brenguier, Romain and Markey, Nicolas and Ummels, Michael}, title = {Pure {N}ash Equilibria in Concurrent Games}, volume = {11}, number = {2:9}, nopages = {}, month = jun, year = 2015, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBMU-lmcs15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBMU-lmcs15.pdf}, doi = {10.2168/LMCS-11(2:9)2015}, abstract = {We study pure-strategy Nash equilibria in multiplayer concurrent games, for a variety of omega-regular objectives. For simple objectives (e.g. reachability, B{\"u}chi objectives), we transform the problem of deciding the existence of a Nash equilibrium in a given concurrent game into that of deciding the existence of a winning strategy in a turn-based two-player game (with a refined objective). We use that transformation to design algorithms for computing Nash equilibria, which in most cases have optimal worst-case complexity. For automata-defined objectives, we extend the above algorithms using a simulation relation which allows us to consider the product of the game with the automata defining the objectives. Building on previous algorithms for simple qualitative objectives, we define and study a semi-quantitative framework, where all players have several boolean objectives equipped with a preorder; a player may for instance want to satisfy all her objectives, or to maximise the number of objectives that she achieves. In most cases, we prove that the algorithms we obtain match the complexity of the problem they address.} }

@article{GL-mscs13, publisher = {Cambridge University Press}, journal = {Mathematical Structures in Computer Science}, author = {Goubault{-}Larrecq, Jean}, title = {A~short proof of the {S}chr{\"o}der-{S}impson theorem}, volume = 25, number = 1, year = 2015, month = jan, pages = {1-5}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/GL-mscs13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GL-mscs13.pdf}, doi = {10.1017/S0960129513000467}, abstract = {We give a short and elementary proof of the Schr{\"o}der-Simpson Theorem, which states that the space of all continuous maps from a given space~\(X\) to the non-negative reals with their Scott topology is the cone-theoretic dual of the probabilistic powerdomain on~\(X\).} }

@inproceedings{Lozes-fics15, address = {Berlin, Germany}, month = sep, year = 2015, volume = 191, series = {Electronic Proceedings in Theoretical Computer Science}, editor = {Matthes, Ralph and Mio, Matteo}, acronym = {{FICS}'15}, booktitle = {{P}roceedings of the 10th {W}orkshop on {F}ixed {P}oints in {C}omputer {S}cience ({FICS}'15)}, author = {Lozes, {\'{E}}tienne}, title = {A Type-Directed Negation Elimination}, pages = {132-142}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/Lozes-fics15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Lozes-fics15.pdf}, doi = {10.4204/EPTCS.191.12}, abstract = {In the modal mu-calculus, a formula is well-formed if each recursive variable occurs underneath an even number of negations. By means of De Morgan's laws, it is easy to transform any well-formed formula into an equivalent formula without negations - its negation normal form. Moreover, if the formula is of size n, its negation normal form of is of the same size O(n). The full modal mu-calculus and the negation normal form fragment are thus equally expressive and concise. In this paper we extend this result to the higher-order modal fixed point logic (HFL), an extension of the modal mu-calculus with higher-order recursive predicate transformers. We present a procedure that converts a formula into an equivalent formula without negations of quadratic size in the worst case and of linear size when the number of variables of the formula is fixed.} }

@article{LV-scp15, publisher = {Elsevier Science Publishers}, journal = {Science of Computer Programming}, author = {Lozes, {\'{E}}tienne and Villard, Jules}, title = {Shared contract-obedient channels}, year = 2015, month = mar, volume = {100}, pages = {28-60}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LV-scp15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LV-scp15.pdf}, doi = {10.1016/j.scico.2014.09.008}, abstract = {Recent advances in the formal verification of message-passing programs are based on proving that programs correctly implement a given protocol. Many existing verification techniques for message-passing programs assume that at most one thread may attempt to send or receive on a channel endpoint at any given point in time, and expressly forbid endpoint sharing. Approaches that do allow such sharing often do not prove that channels obey their protocols. In this paper, we identify two principles that can guarantee obedience to a communication protocol even in the presence of endpoint sharing. Firstly, threads may concurrently use an endpoint in any way that does not advance the state of the protocol. Secondly, threads may compete for receiving on an endpoint provided that the successful reception of the message grants them ownership of that endpoint retrospectively. We develop a program logic based on separation logic that unifies these principles and allows fine-grained reasoning about endpoint-sharing programs. We demonstrate its applicability on a number of examples. The program logic is shown sound against an operational semantics of programs, and proved programs are guaranteed to follow the given protocols and to be free of data races, memory leaks, and communication errors.} }

@inproceedings{LL-fct15, address = {Gda{\'{n}}sk, Poland}, month = aug, year = 2015, volume = 9210, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Kosowski, Adrian and Walukiewicz, Igor}, acronym = {{FCT}'15}, booktitle = {{P}roceedings of the 20th {I}nternational {S}ymposium on {F}undamentals of {C}omputation {T}heory ({FCT}'15)}, author = {Lange, Martin and Lozes, {\'{E}}tienne}, title = {Conjunctive Visibly-Pushdown Path Queries}, pages = {327-338}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LL-fct15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LL-fct15.pdf}, doi = {10.1007/978-3-319-22177-9_25}, abstract = {Weinvestigateanextensionofconjunctiveregularpathqueries in which path properties and path relations are defined by visibly push- down automata. We study the problem of query evaluation for extended conjunctive visibly pushdown path queries and their subclasses, and give a complete picture of their combined and data complexity. In particular, we introduce a weaker notion called extended conjunctive reachability queries for which query evaluation has a polynomial data complexity. We also show that query containment is decidable in 2-EXPTIME for (non-extended) conjunctive visibly pushdown path queries.} }

@mastersthesis{m2-dallon, author = {Dallon, Antoine}, title = {Verification of Cryptographic Protocols : a bound on the number of agents}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2015}, month = sep, url = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-dallon.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-dallon.pdf}, note = {38~pages} }

@proceedings{KDH-topnoc2015, editor = {Koutny, Maciej and Desel, J{\"o}rg and Haddad, Serge}, title = {Transactions on {P}etri Nets and Other Models of Concurrency~{X}}, booktitle = {Transactions on {P}etri Nets and Other Models of Concurrency~{X}}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = 9410, year = {2015}, noaddress = {}, url = {http://www.springer.com/978-3-662-48649-8} }

@misc{cassting-D13, author = {Markey, Nicolas and Doyen, Laurent and Berwanger, Dietmar}, title = {Models for large-scale systems}, howpublished = {Cassting deliverable~D1.3 (FP7-ICT-601148)}, month = sep, year = {2015}, note = {17~pages}, type = {Contract Report}, url = {http://www.cassting-project.eu/wp-content/uploads/deliv-13.pdf}, pdf = {http://www.cassting-project.eu/wp-content/uploads/deliv-13.pdf} }

@misc{cassting-D21, author = {Geeraerts, Gilles and Dehouck, Samuel and Markey, Nicolas and Larsen, Kim G.}, title = {Efficient algorithms for multi-player games with quantitative aspects}, howpublished = {Cassting deliverable~D2.1 (FP7-ICT-601148)}, month = mar, year = {2015}, note = {22~pages}, type = {Contract Report}, url = {http://www.cassting-project.eu/wp-content/uploads/deliv-21.pdf}, pdf = {http://www.cassting-project.eu/wp-content/uploads/deliv-21.pdf} }

@misc{cassting-D63, author = {Markey, Nicolas and Delaborde, Arthur}, title = {Annual report for Year~2}, howpublished = {Cassting deliverable~D6.3 (FP7-ICT-601148)}, month = may, year = {2015}, note = {34~pages}, type = {Contract Report}, nourlnote = {confidentiel} }

@article{GHKS-tecs15, publisher = {ACM Press}, journal = {ACM Transactions in Embedded Computing Systems}, author = {Germanos, Vasileios and Haar, Stefan and Khomenko, Victor and Schwoon, Stefan}, title = {Diagnosability under Weak Fairness}, volume = 14, number = {4:69}, nopages = {}, month = dec, year = 2015, url = {http://www.lsv.fr/Publis/PAPERS/PDF/GHKS-tecs15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GHKS-tecs15.pdf}, doi = {10.1145/2832910}, abstract = {In partially observed Petri nets, diagnosis is the task of detecting whether or not the given sequence of observed labels indicates that some unobservable fault has occurred. Diagnosability is an associated property of the Petri net, stating that in any possible execution an occurrence of a fault can eventually be diagnosed.\par In this paper we consider diagnosability under the weak fairness (WF) assumption, which intuitively states that no transition from a given set can stay enabled forever---it~must eventually either fire or be disabled. We show that a previous approach to WF-diagnosability in the literature has a major flaw, and present a corrected notion. Moreover, we present an efficient method for verifying WF-diagnosability based on a reduction to LTL-X model checking. An~important advantage of this method is that the LTL-X formula is fixed---in~particular, the WF assumption does not have to be expressed as a part of it (which would make the formula length proportional to the size of the specification), but rather the ability of existing model checkers to handle weak fairness directly is exploited.} }

@inproceedings{BGHLM-fsttcs15, address = {Bangalore, India}, month = dec, year = 2015, volume = {45}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Harsha, Prahladh and Ramalingam, G.}, acronym = {{FSTTCS}'15}, booktitle = {{P}roceedings of the 35th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'15)}, author = {Brihaye, {\relax Th}omas and Geeraerts, Gilles and Haddad, Axel and Lefaucheux, Engel and Monmege, Benjamin}, title = {Simple Priced Timed Games Are Not That Simple}, pages = {278-292}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGHLM-fsttcs15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGHLM-fsttcs15.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2015.278}, abstract = {Priced timed games are two-player zero-sum games played on priced timed automata (whose locations and transitions are labeled by weights modeling the costs of spending time in a state and executing an action, respectively). The goals of the players are to minimise and maximise the cost to reach a target location, respectively. We consider priced timed games with one clock and arbitrary (positive and negative) weights and show that, for an important subclass of theirs (the so-called simple priced timed games), one can compute, in exponential time, the optimal values that the players can achieve, with their associated optimal strategies. As side results, we also show that one-clock priced timed games are determined and that we can use our result on simple priced timed games to solve the more general class of so-called reset-acyclic priced timed games (with arbitrary weights and one-clock).} }

@inproceedings{MLBHB-vecos15, address = {Bucharest, Romania}, month = sep, year = 2015, volume = {1431}, series = {CEUR Workshop Proceedings}, publisher = {RWTH Aachen, Germany}, editor = {Ben{~}Hedia, Belgacem and Popentiu{ }Vladicescu, Florin}, acronym = {{VECoS}'15}, booktitle = {{P}roceedings of the 9th {W}orkshop on {V}erification and {E}valuation of {C}omputer and {C}ommunication {S}ystems({VECoS}'15)}, author = {Methni, Amira and Lemerre, Matthieu and Ben{~}Hedia, Belgacem and Haddad, Serge and Barkaoui, Kamel}, title = {State Space Reduction Strategie for Model Checking Concurrent {C}~Programs}, pages = {65-76}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/MLBHB-vecos15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/MLBHB-vecos15.pdf}, abstract = {Model checking is an effective technique for uncovering subtle errors in concurrent systems. Unfortunately, the state space explosion is the main bottleneck in model checking tools. Here we propose a state space reduction technique for model checking concurrent programs written in~C. The reduction technique consists in an analysis phase, which defines an approximate agglomeration predicate. This latter states whether a statement can be agglomerated or~not. We~implement this predicate using a syntactic analysis, as well as a semantic analysis based on abstract interpretation. We show the usefulness of using agglomeration technique to reduce the state space, as well as to generate an abstract TLA+ specification from a~C~program.} }

@inproceedings{BHHHS-cdc15, address = {Osaka, Japan}, month = dec, year = 2015, publisher = {{IEEE} Control System Society}, noeditor = {}, acronym = {{CDC}'15}, booktitle = {{P}roceedings of the 54th {IEEE} {C}onference on {D}ecision and {C}ontrol ({CDC}'15)}, author = {B{\"o}hm, Stanislav and Haar, Stefan and Haddad, Serge and Hofman, Piotr and Schwoon, Stefan}, title = {Active Diagnosis with Observable Quiescence}, pages = {1663-1668}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHHHS-cdc15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHHHS-cdc15.pdf}, doi = {10.1109/CDC.2015.7402449}, abstract = {Active diagnosis of a discrete-event system consists in controlling the system such that faults can be detected. Here we extend the framework of active diagnosis by introducing modalities for actions and states and a new capability for the controller, namely observing that the system is quiescent. We design a game-based construction for both the decision and the synthesis problems that is computationally optimal. Furthermore we prove that the size and the delay provided by the active diagnoser (when it exists) are almost optimal.} }

@article{AGMN-tcs15, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {Akshay, S. and Gastin, Paul and Mukund, Madhavan and Kumar, K. Narayan}, title = {Checking conformance for time-constrained scenario-based specifications}, volume = {594}, pages = {24-43}, month = aug, year = {2015}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AGMN-tcs15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGMN-tcs15.pdf}, doi = {10.1016/j.tcs.2015.03.030}, abstract = {We consider the problem of model checking message-passing systems with real-time requirements. As behavioral specifications, we use message sequence charts (MSCs) annotated with timing constraints. Our system model is a network of communicating finite state machines with local clocks, whose global behavior can be regarded as a timed automaton. Our goal is to verify that all timed behaviors exhibited by the system conform to the timing constraints imposed by the specification. In general, this corresponds to checking inclusion for timed languages, which is an undecidable problem even for timed regular languages. However, we show that we can translate regular collections of time-constrained MSCs into a special class of event-clock automata that can be determinized and complemented, thus permitting an algorithmic solution to the model checking/conformance problem.} }

@inproceedings{BV-fsttcs15, address = {Bangalore, India}, month = dec, year = 2015, volume = {45}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Harsha, Prahladh and Ramalingam, G.}, acronym = {{FSTTCS}'15}, booktitle = {{P}roceedings of the 35th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'15)}, author = {Berwanger, Dietmar and Van{ }den{ }Bogaard, Marie}, title = {Games with Delays. A~{F}rankenstein Approach}, pages = {307-319}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BV-fsttcs15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BV-fsttcs15.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2015.307}, abstract = {We investigate infinite games on finite graphs where the information flow is perturbed by non-deterministic signalling delays. It is known that such perturbations make synthesis problems virtually unsolvable, in the general case. On the classical model where signals are attached to states, tractable cases are rare and difficult to identify. In this paper, we propose a model where signals are detached from control states, and we identify a subclass on which equilibrium outcomes can be preserved, even if signals are delivered with a delay that is finitely bounded. To offset the perturbation, our solution procedure combines responses from a collection of virtual plays following an equilibrium strategy in the instant-signalling game to synthesise, in a Dr.~Frankenstein manner, an equivalent equilibrium strategy for the delayed-signalling game.} }

@inproceedings{KS-fsttcs15, address = {Bangalore, India}, month = dec, year = 2015, volume = {45}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Harsha, Prahladh and Ramalingam, G.}, acronym = {{FSTTCS}'15}, booktitle = {{P}roceedings of the 35th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'15)}, author = {Karandikar, Prateek and Schnoebelen, {\relax Ph}ilippe}, title = {Decidability in the logic of subsequences and supersequences}, pages = {84-97}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-fsttcs15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-fsttcs15.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2015.84}, abstract = {We consider first-order logics of sequences ordered by the subsequence ordering, aka sequence embedding. We show that the \(\Sigma_{2}\)-theory is undecidable, answering a question left open by Kuske. Regarding fragments with a bounded number of variables, we show that the \(\textsf{FO}^{2}\)-theory is decidable while the \(\textsf{FO}^{3}\)-theory is undecidable.} }

@inproceedings{BGM-fsttcs15, address = {Bangalore, India}, month = dec, year = 2015, volume = {45}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Harsha, Prahladh and Ramalingam, G.}, acronym = {{FSTTCS}'15}, booktitle = {{P}roceedings of the 35th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'15)}, author = {Bouyer, Patricia and Gardy, Patrick and Markey, Nicolas}, title = {Weighted strategy logic with boolean goals over one-counter games}, pages = {69-83}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-fsttcs15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-fsttcs15.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2015.69}, abstract = {Strategy Logic is a powerful specification language for expressing non-zero-sum properties of multi-player games. SL conveniently extends the logic ATL with explicit quantification and assignment of strategies. In this paper, we consider games over one-counter automata, and a quantitative extension 1cSL of SL with assertions over the value of the counter. We prove two results: we first show that, if decidable, model checking the so-called Boolean-goal fragment of 1cSL has non-elementary complexity; we actually prove the result for the Boolean-goal fragment of SL over finite-state games, which was an open question in (Mogavero \emph{et~al.} Reasoning about strategies: On the model-checking problem. 2014). As a first step towards proving decidability, we then show that the Boolean-goal fragment of 1cSL over one-counter games enjoys a nice periodicity property.} }

@inproceedings{adhs15-HT, address = {Atlanta, Georgia, USA}, month = oct, year = 2015, number = 27, volume = 48, series = {IFAC-PapersOnLine}, publisher = {Elsevier Science Publishers}, editor = {Lennartson, Bengt and Tabuada, Paulo}, acronym = {{ADHS}'15}, booktitle = {{P}roceedings of the 5th {IFAC} {C}onference on {A}nalysis and {D}esign of {H}ybrid {S}ystems ({ADHS}'15)}, author = {Haar, Stefan and Theissing, Simon}, title = {A~Hybrid-Dynamical Model for Passenger-flow in Transportation Systems}, pages = {236-241}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/adhs15-HT.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/adhs15-HT.pdf}, doi = {10.1016/j.ifacol.2015.11.181}, abstract = {In a network with different transportation modes, or multimodal public transportation system (MPTS), modes are linked among one another not by resources or infrastructure elements---which are not shared, e.g., between different metro lines---but by the flow of passengers between them. Now, the movements of passengers are steered by the destinations that individual passengers have, and by which they can be grouped into trip profiles. To use the strength of fluid dynamics, we therefore introduce a multiphase hybrid Petri net model, in which the vehicle dynamics is rendered by individual tokens moving in an infrastructure net, while passenger quantities are given as vectors---whose components correspond to trip profiles---and evolve at stations according to fluid dynamics. This model is intended as a building block for obtaining supervisory control, via transport operator actions, to mitigate congestion.} }

@inproceedings{ncma2015-bou, address = {Porto, Portugal}, month = aug, year = 2015, volume = 318, series = {books@ocg.at}, publisher = {Austrian Computer Society}, editor = {Freund, Rudolf and Holzer, Markus and Moreira, Nelma and Reis, Rog{\'e}rio}, acronym = {{NCMA}'15}, booktitle = {{P}roceedings of the 7th {W}orkshop on {N}on-{C}lassical {M}odels of {A}utomata and {A}pplications ({NCMA}'15)}, author = {Bouyer, Patricia}, title = {On the optimal reachability problem in weighted timed automata and games}, pages = {11-36}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ncma15-bou.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ncma15-bou.pdf}, abstract = {In these notes, we survey works made on the models of weighted timed automata and games, and more specifically on the optimal reachability problem.} }

@inproceedings{MAS-sigspatial15, address = {Seattle, Washington, USA}, month = nov, year = 2015, editor = {Ali, Mohamed and Huang Yan and Gertz, Michael and Renz, Matthias and Sankaranarayanan, Jagan}, acronym = {{GIS}'15}, booktitle = {{P}roceedings of the 23rd {ACM} {SIGSPATIAL} {I}nternational {C}onference on {A}dvances in {G}eographic {I}nformation {S}ystems ({GIS}'15)}, author = {Montoya, David and Abiteboul, Serge and Senellart, Pierre}, title = {Hup-Me: Inferring and Reconciling a Timeline of User Activity with Smartphone and Personal Data}, pages = {62:1-4}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/MAS-sigspatial15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/MAS-sigspatial15.pdf}, doi = {10.1145/2820783.2820852}, abstract = {We designed a system to infer multimodal itineraries traveled by a user from a combination of smartphone sensor data (e.g., GPS, Wi-Fi, accelerometer) and knowledge of the transport network infrastructure (e.g., road and rail maps, public transportation timetables). The system uses a Transportation network that captures the set of possible paths of this network for the modes, e.g., foot, bicycle, road_vehicle, and rail. This Transportation network is constructed from OpenStreetMap data and public transportation routes published online by transportation agencies in GTFS format. The system infers itineraries from a sequence of smartphone observations in two phases. The first phase uses a dynamic Bayesian network that models the probabilistic relationship between paths in Transportation network and sensor data. The second phase attempts to match portions recognized as road_vehicle or rail with possible public transportation routes of type bus, train, metro, or tram extracted from the GTFS source. We evaluated the performance of our system with data from users traveling over the Paris area who were asked to record data for different trips via an Android application. Itineraries were annotated with modes and public transportation routes taken and we report on the results of the recognition.} }

@article{CCD-tocl15, publisher = {ACM Press}, journal = {ACM Transactions on Computational Logic}, author = {Chr{\'e}tien, R{\'e}my and Cortier, V{\'e}ronique and Delaune, St{\'e}phanie}, title = {From security protocols to pushdown automata}, volume = {17}, number = {1:3}, nopages = {}, year = 2015, month = sep, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-tocl15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-tocl15.pdf}, doi = {10.1145/2811262}, 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. We further show that checking for equivalence of protocols is actually equivalent to checking for equivalence of generalized, real-time deterministic pushdown automata.\par Very recently, the algorithm for checking for equivalence of deterministic pushdown automata has been implemented. We have implemented our translation from protocols to pushdown automata, yielding the first tool that decides equivalence of (some class of) protocols, for an unbounded number of sessions. As an application, we have analyzed some protocols of the literature including a simplified version of the basic access control (BAC) protocol used in biometric passports.} }

@inproceedings{CCD-esorics15, address = {Vienna, Austria}, month = sep, year = 2015, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Ryan, Peter and Weippl, Edgar}, acronym = {{ESORICS}'15}, booktitle = {{P}roceedings of the 20th {E}uropean {S}ymposium on {R}esearch in {C}omputer {S}ecurity ({ESORICS}'15)}, author = {Chr{\'e}tien, R{\'e}my and Cortier, V{\'e}ronique and Delaune, St{\'e}phanie}, title = {Checking trace equivalence: How to get rid of nonces?}, pages = {230-251}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-esorics15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-esorics15.pdf}, doi = {10.1007/978-3-319-24177-7_12}, abstract = {Security protocols can be successfully analysed using formal methods. When proving security in symbolic settings for an unbounded number of sessions, a typical technique consists in abstracting away fresh nonces and keys by a bounded set of constants. While this abstraction is clearly sound in the context of secrecy properties (for protocols without else branches), this is no longer the case for equivalence properties.\par In this paper, we study how to soundly get rid of nonces in the context of equivalence properties. We show that nonces can be replaced by constants provided that each nonce is associated to two constants (instead of typically one constant for secrecy properties). Our result holds for deterministic (simple) protocols and a large class of primitives that includes e.g. standard primitives, blind signatures, and zero-knowledge proofs.} }

@phdthesis{karandikar-phd15, author = {Karandikar, Prateek}, title = {Subwords: automata, embedding problems, and verification}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France and Chennai Mathematical Institute, India}, type = {Th{\`e}se de doctorat}, year = 2015, month = feb, url = {http://www.lsv.fr/Publis/PAPERS/PDF/karandikar-phd15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/karandikar-phd15.pdf} }

@phdthesis{francis-phd15, author = {Francis, Nadime}, title = {View-based Query Determinacy and Rewritings over Graph Databases}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2015, month = dec, url = {https://tel.archives-ouvertes.fr/tel-01247115} }

@phdthesis{reichert-phd15, author = {Reichert, Julien}, title = {D{\'e}cidabilit{\'e} et complexit{\'e} de jeux d'accessibilit{\'e} sur des syst{\`e}mes {\`a} compteurs}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2015, month = jul, url = {http://www.lsv.fr/Publis/PAPERS/PDF/reichert-phd15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/reichert-phd15.pdf} }

@inproceedings{FGMMP-rp15, address = {Warsaw, Poland}, month = sep, year = 2015, volume = {9328}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Boja{\'n}czyk, Miko{\l}aj and Lasota, S{\l}awomir and Potapov, Igor}, acronym = {{RP}'15}, booktitle = {{P}roceedings of the 9th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'15)}, author = {Fribourg, Laurent and Goubault, {\'E}ric and Mohamed, Sameh and Mrozek, Marian and Putot, Sylvie}, title = {A~Topological Method for Finding Invariants of Continuous Systems}, pages = {63-75}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FGMMP-rp15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FGMMP-rp15.pdf}, doi = {10.1007/978-3-319-24537-9_7}, abstract = {A~usual way to find positive invariant sets of ordinary differential equations is to restrict the search to predefined finitely generated shapes, such as linear templates, or ellipsoids as in classical quadratic Lyapunov function based approaches. One then looks for generators or parameters for which the corresponding shape has the property that the flow of the ODE goes inwards on its border. But for non-linear systems, where the structure of invariant sets may be very complicated, such simple predefined shapes are generally not well suited. The present work proposes a more general approach based on a topological property, namely Wa\.{z}ewski's property. Even for complicated non-linear dynamics, it is possible to successfully restrict the search for isolating blocks of simple shapes, that are bound to contain non-empty invariant sets. This approach generalizes the Lyapunov-like approaches, by allowing for inwards and outwards flow on the boundary of these shapes, with extra topological conditions. We developed and implemented an algorithm based on Wa\.{z}ewski's property, SOS optimization and some extra combinatorial and algebraic properties, that shows very nice results on a number of classical polynomial dynamical systems.} }

@inproceedings{LS-rp15, address = {Warsaw, Poland}, month = sep, year = 2015, volume = {9328}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Boja{\'n}czyk, Miko{\l}aj and Lasota, S{\l}awomir and Potapov, Igor}, acronym = {{RP}'15}, booktitle = {{P}roceedings of the 9th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'15)}, author = {Lazi{\'c}, Ranko and Schmitz, Sylvain}, title = {The Ideal View on {R}ackoff's Coverability Technique}, pages = {76-88}, url = {https://hal.inria.fr/hal-01176755}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-rp15.pdf}, doi = {10.1007/978-3-319-24537-9_8}, abstract = {Rackoff's small witness property for the coverability problem is the standard means to prove tight upper bounds in vector addition systems (VAS) and many extensions. We show how to derive the same bounds directly on the computations of the VAS instantiation of the generic backward coverability algorithm. This relies on a dual view of the algorithm using ideal decompositions of downwards-closed sets, which exhibits a key structural invariant in the VAS case. The same reasoning readily generalises to several VAS extensions.} }

@inproceedings{BHPSS-rp15, address = {Warsaw, Poland}, month = sep, year = 2015, volume = {9328}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Boja{\'n}czyk, Miko{\l}aj and Lasota, S{\l}awomir and Potapov, Igor}, acronym = {{RP}'15}, booktitle = {{P}roceedings of the 9th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'15)}, author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge and Picaronny, Claudine and Safey{ }El{~}Din, Mohab and Sassolas, Mathieu}, title = {Polynomial Interrupt Timed Automata}, pages = {20-32}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHPSS-rp15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHPSS-rp15.pdf}, doi = {10.1007/978-3-319-24537-9_3}, abstract = {Interrupt Timed Automata (ITA) form a subclass of stopwatch automata where reachability and some variants of timed model checking are decidable even in presence of parameters. They are well suited to model and analyze real-time operating systems. Here we extend ITA with polynomial guards and updates, leading to the class of polynomial ITA (PolITA). We prove that reachability is decidable in 2EXPTIME on PolITA, using an adaptation of the cylindrical decomposition method for the first-order theory of reals. Compared to previous approaches, our procedure handles parameters and clocks in a unified way. We also obtain decidability for the model checking of a timed version of CTL and for reachability in several extensions of PolITA.} }

@inproceedings{BFM-avocs15, address = {Edinburgh, UK}, month = sep, year = {2015}, volume = 72, series = {Electronic Communications of the EASST}, publisher = {European Association of Software Science and Technology}, editor = {Grov, Gudmund and Ireland, Andrew}, acronym = {{AVoCS}'15}, booktitle = {{P}roceedings of the 15th {I}nternational {W}orkshop on {A}utomated {V}erification of {C}ritical {S}ystems ({AVoCS}'15)}, author = {Bouyer, Patricia and Fang, Erwin and Markey, Nicolas}, title = {Permissive strategies in timed automata and games}, nopages = {263-277}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFM-avocs15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFM-avocs15.pdf}, doi = {10.14279/tuj.eceasst.72.1015}, abstract = {Timed automata are a convenient framework for modelling and reasoning about real-time systems. While these models are now very well-understood, they do not offer a convenient way of taking timing imprecisions into account. Several solutions (e.g. parametric guard enlargement) have recently been proposed over the last ten years to take such imprecisions into account. In this paper, we propose a new approach for handling robust reachability, based on permissive strategies. While classical strategies propose to play an action at an exact point in time, permissive strategies return an interval of possible dates when to play the selected action. With such a permissive strategy, we associate a penalty, which is the inverse of the length of the proposed interval, and accumulates along the run. We show that in that setting, optimal strategies can be computed in polynomial time for one-clock timed automata.} }

@inproceedings{B-time15, address = {Kassel, Germany}, month = sep, year = 2015, publisher = {{IEEE} Computer Society Press}, editor = {Grandi, Fabio and Lange, Martin and Lomuscio, Alessio}, acronym = {{TIME}'15}, booktitle = {{P}roceedings of the 22nd {I}nternational {S}ymposium on {T}emporal {R}epresentation and {R}easoning ({TIME}'15)}, author = {Bollig, Benedikt}, title = {Towards Formal Verification of Distributed Algorithms}, pages = {3}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/B-time15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/B-time15.pdf}, doi = {10.1109/TIME.2015.23} }

@inproceedings{B-ciaa15, address = {Ume{\aa}, Sweden}, month = aug, year = 2015, volume = {9223}, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, editor = {Drewes, Frank}, acronym = {{CIAA}'15}, booktitle = {{P}roceedings of the 20th {I}nternational {C}onference on {I}mplementation and {A}pplication of {A}utomata ({CIAA}'15)}, author = {Bollig, Benedikt}, title = {Automata and Logics for Concurrent Systems: Five Models in Five Pages}, pages = {3-12}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/B-ciaa15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/B-ciaa15.pdf}, doi = {10.1007/978-3-319-22360-5_1}, abstract = {We~survey various automata models of concurrent systems and their connection with monadic second-order logic: finite automata, class memory automata, nested-word automata, asynchronous automata, and message-passing automata.} }

@inproceedings{RG-bda15, address = {{\^I}le de Porquerolles, France}, month = sep, year = 2015, noeditor = {}, acronym = {{BDA}'15}, booktitle = {{A}ctes de la 31{\`e}me {C}onf{\'e}rence sur la {G}estion de {D}onn{\'e}es~-- {P}rincipes, {T}echnologies et {A}pplications ({BDA}'15)}, author = {Rafes, Karima and Germain, C{\'e}cile}, title = {A~platform for scientific data sharing}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/RG-bda15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RG-bda15.pdf}, abstract = {In this paper, we use the semantic web technology, notably RDF, SPARQL and Linked Open Data in the context of scientific data sharing. More precisely, we present the LinkedWiki platform that is being developed at the Center for Data Science of Paris-Saclay University for scientific data integration. The~goal is to facilitate the discovery and exploitation of scientists' datasets by their colleagues. For this, we notably rely on the use by scientists of Wikipedia for specifying the semantics of datasets, and the use of Wikidata (the~Wikipedia's knowledge base) identifiers for annotating these datasets and thereby facilitating their discovery.} }

@inproceedings{BMRLL-gandalf15, address = {Genova, Italy}, month = sep, year = 2015, volume = {193}, series = {Electronic Proceedings in Theoretical Computer Science}, editor = {Esparza, Javier and Tronci, Enrico}, acronym = {{GandALF}'15}, booktitle = {{P}roceedings of the 6th {I}nternational {S}ymposium on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification ({GandALF}'15)}, author = {Bouyer, Patricia and Markey, Nicolas and Randour, Mickael and Larsen, Kim G. and Laursen, Simon}, title = {Average-energy games}, pages = {1-15}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMRLL-gandalf15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMRLL-gandalf15.pdf}, doi = {10.4204/EPTCS.193.1}, abstract = {Two-player quantitative zero-sum games provide a natural framework to synthesize controllers with performance guarantees for reactive systems within an uncontrollable environment. Classical settings include mean-payoff games, where the objective is to optimize the long-run average gain per action, and energy games, where the system has to avoid running out of energy.\par We study \emph{average-energy} games, where the goal is to optimize the long-run average of the accumulated energy. We show that this objective arises naturally in several applications, and that it yields interesting connections with previous concepts in the literature. We prove that deciding the winner in such games is in \textsf{NP}{{\(\cap\)}}\textsf{coNP} and at least as hard as solving mean-payoff games, and we establish that memoryless strategies suffice to win. We also consider the case where the system has to minimize the average-energy while maintaining the accumulated energy within predefined bounds at all times: this corresponds to operating with a finite-capacity storage for energy. We give results for one-player and two-player games, and establish complexity bounds and memory requirements.} }

@inproceedings{LMS-gandalf15, address = {Genova, Italy}, month = sep, year = 2015, volume = {193}, series = {Electronic Proceedings in Theoretical Computer Science}, editor = {Esparza, Javier and Tronci, Enrico}, acronym = {{GandALF}'15}, booktitle = {{P}roceedings of the 6th {I}nternational {S}ymposium on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification ({GandALF}'15)}, author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas and Sangnier, Arnaud}, title = {{{\(\textsf{ATL}_{\textsf{sc}}\)}} with partial observation}, pages = {43-57}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LMS-gandalf15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LMS-gandalf15.pdf}, doi = {10.4204/EPTCS.193.4}, abstract = {Alternating-time temporal logic with strategy contexts ({{\(\textsf{ATL}_{\textsf{sc}}\)}}) is a powerful formalism for expressing properties of multi-agent systems: it~extends \textsf{CTL} with \emph{strategy quantifiers}, offering a convenient way of expressing both collaboration and antagonism between several agents. Incomplete observation of the state space is a desirable feature in such a framework, but it quickly leads to undecidable verification problems. In this paper, we prove that \emph{uniform} incomplete observation (where all players have the same observation) preserves decidability of the model checking problem, even for very expressive logics such as {{\(\textsf{ATL}_{\textsf{sc}}\)}}.} }

@inproceedings{BV-dlt15, address = {Liverpool, UK}, month = jul, year = 2015, volume = {9168}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Potapov, Igor}, acronym = {{DLT}'15}, booktitle = {{P}roceedings of the 19th {I}nternational {C}onference on {D}evelopments in {L}anguage {T}heory ({DLT}'15)}, author = {Berwanger, Dietmar and Van{ }den{ }Bogaard, Marie}, title = {Consensus Game Acceptors}, pages = {108-119}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BV-dlt15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BV-dlt15.pdf}, doi = {10.1007/978-3-319-21500-6_8}, abstract = {We study a game for recognising formal languages, in which two players with imperfect information need to coordinate on a common decision, given private input strings correlated by a finite graph. The players have a joint objective to avoid an inadmissible decision, in spite of the uncertainty induced by the input.\par We show that the acceptor model based on consensus games characterises context-sensitive languages, and conversely, that winning strategies in such games can be described by context-sensitive languages. We also discuss consensus game acceptors with a restricted observation pattern that describe nondeterministic linear-time languages.} }

@inproceedings{BMV-atva15, address = {Shanghai, China}, month = oct, year = {2015}, volume = {9364}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Finkbeiner, Bernd and Pu, Geguang and Zhang, Lijun}, acronym = {{ATVA}'15}, booktitle = {{P}roceedings of the 13th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'15)}, author = {Berwanger, Dietmar and Mathew, Anup Basil and Van{ }den{ }Bogaard, Marie}, title = {Hierarchical Information Patterns and Distributed Strategy Synthesis}, pages = {378-393}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMV-atva15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMV-atva15.pdf}, doi = {10.1007/978-3-319-24953-7_28}, abstract = {Infinite games with imperfect information tend to be undecidable unless the information flow is severely restricted. One fundamental decidable case occurs when there is a total ordering among players, such that each player has access to all the information that the following ones receive.\par In this paper we consider variations of this hierarchy principle for synchronous games with perfect recall, and identify new decidable classes for which the distributed synthesis problem is solvable with finite-state strategies. In particular, we show that decidability is maintained when the information hierarchy may change along the play, or when transient phases without hierarchical information are allowed.} }

@inproceedings{PRCHH-atva15, address = {Shanghai, China}, month = oct, year = {2015}, volume = {9364}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Finkbeiner, Bernd and Pu, Geguang and Zhang, Lijun}, acronym = {{ATVA}'15}, booktitle = {{P}roceedings of the 13th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'15)}, author = {Ponce{ }de{~}Le{\'o}n, Hern{\'a}n and Rodr{\'\i}guez, C{\'e}sar and Carmona, Josep and Heljanko, Keijo and Haar, Stefan}, title = {Unfolding-Based Process Discovery}, pages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/PRCHH-atva15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PRCHH-atva15.pdf}, doi = {10.1007/978-3-319-24953-7_4}, abstract = {This paper presents a novel technique for process discovery. In contrast to the current trend, which only considers an event log for discovering a process model, we assume two additional inputs: an independence relation on the set of logged activities, and a collection of negative traces. After deriving an intermediate net unfolding from them, we perform a controlled folding giving rise to a Petri net which contains both the input log and all independence-equivalent traces arising from~it. Remarkably, the derived Petri net cannot execute any trace from the negative collection. The entire chain of transformations is fully automated. A tool has been developed and experimental results are provided that witness the significance of the contribution of this paper.} }

@inproceedings{BDS-csl15, address = {Berlin, Germany}, month = sep, year = 2015, volume = {41}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Kreuzer, Stephan}, acronym = {{CSL}'15}, booktitle = {{P}roceedings of the 24th {A}nnual {EACSL} {C}onference on {C}omputer {S}cience {L}ogic ({CSL}'15)}, author = {Baelde, David and Doumane, Amina and Saurin, Alexis}, title = {Least and Greatest Fixed Points in Ludics}, pages = {549-566}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDS-csl15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDS-csl15.pdf}, doi = {10.4230/LIPIcs.CSL.2015.549}, abstract = {Various logics have been introduced in order to reason over (co)inductive specifications and, through the Curry-Howard correspondence, to study computation over inductive and coinductive data. The logic mu-MALL is one of those logics, extending multiplicative and additive linear logic with least and greatest fixed point operators.\par In this paper, we investigate the semantics of mu-MALL proofs in (computational) ludics. This framework is built around the notion of design, which can be seen as an analogue of the strategies of game semantics. The infinitary nature of designs makes them particularly well suited for representing computations over infinite data.\par We provide mu-MALL with a denotational semantics, interpreting proofs by designs and formulas by particular sets of designs called behaviours. Then we prove a completeness result for the class of {"}essentially finite designs{"}, which are those designs performing a finite computation followed by a copycat. On the way to completeness, we investigate semantic inclusion, proving its decidability (given two formulas, we can decide whether the semantics of one is included in the other's) and completeness (if semantic inclusion holds, the corresponding implication is provable in mu-MALL).} }

@article{CLMT-dagstuhl15, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, journal = {Dagstuhl Reports}, editor = {Chatterjee, Krishnendu and Lafortune, St{\'e}phane and Markey, Nicolas and Thomas, Wolfgang}, author = {Chatterjee, Krishnendu and Lafortune, St{\'e}phane and Markey, Nicolas and Thomas, Wolfgang}, title = {Non-Zero-Sum-Games and Control ({D}agstuhl Seminar~15061)}, pages = {1-25}, year = {2015}, volume = {5}, number = {2}, month = jun, url = {http://drops.dagstuhl.de/opus/volltexte/2015/5042}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CLMT-dagstuhl15.pdf}, doi = {10.4230/DagRep.5.2.1}, abstract = {In this report, the program, research issues, and results of Dagstuhl Seminar 15061 {"}Non-Zero-Sum-Games and Control{"} are described. The area of non-zero-sum games is addressed in a wide range of topics: multi-player games, partial-observation games, quantitative game models, and---as~a special focus---connections with control engineering (supervisory control).} }

@inproceedings{HPRV-ppdp15, address = {Siena, Italy}, month = jul, year = 2015, publisher = {ACM Press}, editor = {Albert, Elvira}, acronym = {{PPDP}'15}, booktitle = {{P}roceedings of the 17th {I}nternational {C}onference on {P}rinciples and {P}ractice of {D}eclarative {P}rogramming ({PPDP}'15)}, author = {Haar, Stefan and Perchy, Salim and Rueda, Camilo and Valencia, Franck}, title = {An Algebraic View of Space{{\slash}}Belief and Extrusion{{\slash}}Utterance for Concurrency{{\slash}}Epistemic Logic}, pages = {161-172}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/HPRV-ppdp15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HPRV-ppdp15.pdf}, doi = {10.1007/978-3-319-19488-2_6}, abstract = {We enrich spatial constraint systems with operators to specify information and processes moving from a space to another. We shall refer to these news structures as spatial constraint systems with extrusion. We shall investigate the properties of this new family of constraint systems and illustrate their applications. From a computational point of view the new operators provide for process\slash information extrusion, a central concept in formalisms for mobile communication. From an epistemic point of view extrusion corresponds to a notion we shall call utterance; a~piece of information that an agent communicates to others but that may be inconsistent with the agent's beliefs. Utterances can then be used to express instances of epistemic notions, which are common place in social media, such as hoaxes or intentional lies. Spatial constraint systems with extrusion can be seen as complete Heyting algebras equipped with maps to account for spatial and epistemic specifications.} }

@inproceedings{BMPS-formats15, address = {Madrid, Spain}, month = sep, year = 2015, volume = {9268}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Sankaranarayanan, Sriram and Vicario, Enrico}, acronym = {{FORMATS}'15}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'15)}, author = {Bouyer, Patricia and Markey, Nicolas and Perrin, Nicolas and Schlehuber, Philipp}, title = {Timed automata abstraction of switched dynamical systems using control funnels}, pages = {60-75}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMPS-formats15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMPS-formats15.pdf}, doi = {10.1007/978-3-319-22975-1_5}, abstract = {The~development of formal methods for control design is an important challenge with potential applications in a wide range of safety-critical cyber-physical systems. Focusing on switched dynamical systems, we~propose a new abstraction, based on time-varying regions of invariance (the~\emph{control funnels}), that models behaviors of systems as timed automata. The main advantage of this method is that it allows automated verification of formal specifications and reactive controller synthesis without discretizing the evolution of the state of the system. Efficient constructions are possible in the case of linear dynamics. We~demonstrate the potential of our approach with two examples.} }

@inproceedings{AM-formats15, address = {Madrid, Spain}, month = sep, year = 2015, volume = {9268}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Sankaranarayanan, Sriram and Vicario, Enrico}, acronym = {{FORMATS}'15}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'15)}, author = {Andr{\'e}, {\'E}tienne and Markey, Nicolas}, title = {Language Preservation Problems in Parametric Timed Automata}, pages = {27-43}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AM-formats15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AM-formats15.pdf}, doi = {10.1007/978-3-319-22975-1_3}, abstract = {Parametric timed automata (PTA) are a powerful formalism to model and reason about concurrent systems with some unknown timing delays. In this paper, we address the (untimed) language- and trace-preservation problems: given a reference parameter valuation, does there exist another parameter valuation with the same untimed language (or trace)? We show that these problems are undecidable both for general PTA, and even for the restricted class of L/U-PTA. On the other hand, we exhibit decidable subclasses: 1-clock PTA, and 1-parameter deterministic L-PTA and U-PTA.} }

@inproceedings{ABG-concur15, address = {Madrid, Spain}, month = sep, year = 2015, volume = {42}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Aceto, Luca and de Frutos-Escrig, David}, acronym = {{CONCUR}'15}, booktitle = {{P}roceedings of the 26th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'15)}, author = {Aiswarya, C. and Bollig, Benedikt and Gastin, Paul}, title = {An Automata-Theoretic Approach to the Verification of Distributed Algorithms}, pages = {340-353}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABG-concur15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABG-concur15.pdf}, doi = {10.4230/LIPIcs.CONCUR.2015.340}, abstract = {We introduce an automata-theoretic method for the verification of distributed algorithms running on ring networks. In a distributed algorithm, an arbitrary number of processes cooperate to achieve a common goal (e.g., elect a leader). Processes have unique identifiers (pids) from an infinite, totally ordered domain. An algorithm proceeds in synchronous rounds, each round allowing a process to perform a bounded sequence of actions such as send or receive a pid, store it in some register, and compare register contents wrt. the associated total order. An algorithm is supposed to be correct independently of the number of processes. To specify correctness properties, we introduce a logic that can reason about processes and pids. Referring to leader election, it may say that, at the end of an execution, each process stores the maximum pid in some dedicated register. Since the verification of distributed algorithms is undecidable, we propose an underapproximation technique, which bounds the number of rounds. This is an appealing approach, as the number of rounds needed by a distributed algorithm to conclude is often exponentially smaller than the number of processes. We provide an automata-theoretic solution, reducing model checking to emptiness for alternating two-way automata on words. Overall, we show that round-bounded verification of distributed algorithms over rings is PSPACE-complete.} }

@inproceedings{BDH-concur15, address = {Madrid, Spain}, month = sep, year = 2015, volume = {42}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Aceto, Luca and de Frutos-Escrig, David}, acronym = {{CONCUR}'15}, booktitle = {{P}roceedings of the 26th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'15)}, author = {Baelde, David and Delaune, St{\'e}phanie and Hirschi, Lucca}, title = {Partial Order Reduction for Security Protocols}, pages = {497-510}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDH-concur15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDH-concur15.pdf}, doi = {10.4230/LIPIcs.CONCUR.2015.497}, abstract = {Security protocols are concurrent processes that communicate using cryptography with the aim of achieving various security properties. Recent work on their formal verification has brought procedures and tools for deciding trace equivalence properties (\textit{e.g.},~anonymity, unlinkability, vote secrecy) for a bounded number of sessions. However, these procedures are based on a naive symbolic exploration of all traces of the considered processes which, unsurprisingly, greatly limits the scalability and practical impact of the verification tools.\par In this paper, we mitigate this difficulty by developing partial order reduction techniques for the verification of security protocols. We provide reduced transition systems that optimally elim- inate redundant traces, and which are adequate for model-checking trace equivalence properties of protocols by means of symbolic execution. We have implemented our reductions in the tool \textsf{Apte}, and demonstrated that it achieves the expected speedup on various protocols.} }

@inproceedings{BJM-concur15, address = {Madrid, Spain}, month = sep, year = 2015, volume = {42}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Aceto, Luca and de Frutos-Escrig, David}, acronym = {{CONCUR}'15}, booktitle = {{P}roceedings of the 26th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'15)}, author = {Bouyer, Patricia and Jaziri, Samy and Markey, Nicolas}, title = {On~the Value Problem in Weighted Timed Games}, pages = {311-324}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BJM-concur15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BJM-concur15.pdf}, doi = {10.4230/LIPIcs.CONCUR.2015.311}, abstract = {A~weighted timed game is a timed game with extra quantitative information representing e.g. energy consumption. Optimizing the cost for reaching a target is a natural question, which has been investigated for ten years. Existence of optimal strategies is known to be undecidable in general, and only very restricted classes of games have been described for which optimal cost and almost-optimal strategies can be computed.\par In this paper, we show that the value problem is undecidable in general weighted timed games. The undecidability proof relies on that for the existence of optimal strategies and on a diagonalization construction recently designed in the context of quantitative temporal logics. We then provide an algorithm to compute arbitrary approximations of the value in a game, and almost-optimal strategies. The algorithm applies in a large subclass of weighted timed games, and is the first approximation scheme which is designed in the current context.} }

@inproceedings{CDV-icalp15, address = {Kyoto, Japan}, month = jul, year = 2015, volume = {9135}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Halld{\'o}rsson, Magnus M. and Iwama, Kazuo and Kobayashi, Naoki and Speckmann, Bettina}, acronym = {{ICALP}'15}, booktitle = {{P}roceedings of the 42nd {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'15)~-- {P}art~{II}}, author = {Chatterjee, Krishnendu and Doyen, Laurent and Vardi, Moshe}, title = {The Complexity of Synthesis from Probabilistic Components}, pages = {108-120}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDV-icalp15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDV-icalp15.pdf}, doi = {10.1007/978-3-662-47666-6_9}, abstract = {The synthesis problem asks for the automatic construction of a system from its specification. In the traditional setting, the system is {"}constructed from scratch{"} rather than composed from reusable components. However, this is rare in practice, and almost every non-trivial software system relies heavily on the use of libraries of reusable components. Recently, Lustig and Vardi introduced dataflow and controlflow synthesis from libraries of reusable components. They proved that dataflow synthesis is undecidable, while controlflow synthesis is decidable. The problem of controlflow synthesis from libraries of probabilistic components was considered by Nain, Lustig and Vardi, and was shown to be decidable for qualitative analysis (that asks that the specification be satisfied with probability~1). Our main contribution for controlflow synthesis from probabilistic components is to establish better complexity bounds for the qualitative analysis problem, and to show that the more general quantitative problem is undecidable. For the qualitative analysis, we show that the problem (i)~is EXPTIME-complete when the specification is given as a deterministic parity word automaton, improving the previously known 2EXPTIME upper bound; and (ii)~belongs to UP\(\cap\)coUP and is parity-games hard, when the specification is given directly as a parity condition on the components, improving the previously known EXPTIME upper bound.} }

@inproceedings{JLS-icalp15, address = {Kyoto, Japan}, month = jul, year = 2015, volume = {9135}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Halld{\'o}rsson, Magnus M. and Iwama, Kazuo and Kobayashi, Naoki and Speckmann, Bettina}, acronym = {{ICALP}'15}, booktitle = {{P}roceedings of the 42nd {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'15)~-- {P}art~{II}}, author = {Jurdzi{\'n}ski, Marcin and Lazi{\'c}, Ranko and Schmitz, Sylvain}, title = {Fixed-Dimensional Energy Games are in Pseudo Polynomial Time}, pages = {260-272}, url = {http://arxiv.org/abs/1502.06875}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JLS-arxiv15.pdf}, doi = {10.1007/978-3-662-47666-6_21}, abstract = {We generalise the hyperplane separation technique (Chatterjee and Velner,~2013) from multi-dimensional mean-payoff to energy games, and achieve an algorithm for solving the latter whose running time is exponential only in the dimension, but not in the number of vertices of the game graph. This answers an open question whether energy games with arbitrary initial credit can be solved in pseudo-polynomial time for fixed dimensions~\(3\) or larger (Chaloupka,~2013). It~also improves the complexity of solving multi-dimensional energy games with given initial credit from non-elementary (Br\'azdil, Jan\v{c}ar, and Ku\v{c}era,~2010) to 2EXPTIME, thus establishing their 2EXPTIME-completeness.} }

@phdthesis{bollig-HDR15, author = {Bollig, Benedikt}, title = {Automata and Logics for Concurrent Systems: Realizability and Verification}, year = 2015, month = jun, 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-bollig15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/hdr-bollig15.pdf} }

@inproceedings{CCD-csf15, address = {Verona, Italy}, month = jul, year = 2015, publisher = {{IEEE} Computer Society Press}, acronym = {{CSF}'15}, booktitle = {{P}roceedings of the 28th {IEEE} {C}omputer {S}ecurity {F}oundations {S}ymposium ({CSF}'15)}, author = {Chr{\'e}tien, R{\'e}my and Cortier, V{\'e}ronique and Delaune, St{\'e}phanie}, title = {Decidability of trace equivalence for protocols with nonces}, pages = {170-184}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-csf15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-csf15.pdf}, doi = {10.1109/CSF.2015.19}, abstract = {Privacy properties such as anonymity, unlinkability, or vote secrecy are typically expressed as equivalence properties.\par In this paper, we provide the first decidability result for trace equivalence of security protocols, for an unbounded number of sessions and unlimited fresh nonces. Our class encompasses most symmetric key protocols of the literature, in their tagged variant.} }

@inproceedings{MLBHB-ftscs15, address = {Luxembourg}, optnmonth = 11, optmonth = nov, year = 2015, volume = {476}, series = {Communications in Computer and Information Science}, publisher = {Springer}, editor = {Artho, Cyrille and {\"O}lveczky, Peter Csaba}, acronym = {{FTSCS}'14}, booktitle = {{P}roceedings of the 3rd {I}nternational {W}orkshop on {F}ormal {T}echniques for {S}afety-{C}ritical {S}ystems, Nov. 2014 ({FTSCS}'14)}, author = {Methni, Amira and Lemerre, Matthieu and Ben{~}Hedia, Belgacem and Haddad, Serge and Barkaoui, Kamel}, title = {Specifying and Verifying Concurrent {C}~Programs with {TLA+}}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/MLBHB-ftscs15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/MLBHB-ftscs15.pdf}, doi = {10.1007/978-3-319-17581-2_14}, pages = {206-222}, nonote = {17~pages}, abstract = {Verifying software systems automatically from their source code rather than modelling them in a dedicated language gives more confidence in establishing their properties. Here we propose a formal specification and verification approach for concurrent C programs directly based on the semantics of~C. We define a set of translation rules and implement it in a tool~(C2TLA+) that automatically translates C code into a TLA+ specification. The~TLC model checker can use this specification to generate a model, allowing to check the absence of runtime errors and dead code in the C program in a given configuration. In addition, we show how translated specifications interact with manually written ones~to: check the C code against safety or liveness properties; provide concurrency primitives or model hardware that cannot be expressed in~C; and use abstract versions of translated C functions to address the state explosion problem. All these verifications have been conducted on an industrial case study, which is a part of the microkernel of the PharOS real-time system.} }

@article{FH-fundi15, publisher = {{IOS} Press}, journal = {Fundamenta Informaticae}, author = {Fraca, Est{\'\i}baliz and Haddad, Serge}, title = {Complexity Analysis of Continuous Petri Nets}, volume = 137, number = {1}, pages = {1-28}, year = 2015, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FH-fundi15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FH-fundi15.pdf}, doi = {10.3233/FI-2015-1168}, abstract = {At the end of the eighties, continuous Petri nets were introduced for: (1)~alleviating the combinatory explosion triggered by discrete Petri nets (i.e. usual 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 coverability, boundedness and reachability set inclusion. We also design new decision procedures for reachability and lim-reachability problems with a better computational complexity. Finally we provide lower bounds characterising the exact complexity class of the reachability, the coverability, the boundedness, the deadlock freeness and the liveness problems. A~small case study is introduced and analysed with these new procedures.} }

@article{BHHP-ijasm15, publisher = {IARIA}, journal = {International Journal on Advances in Systems and Measurements}, author = {Barbot, Beno{\^\i}t and Haddad, Serge and Heiner, Monika and Picaronny, Claudine}, title = {Rare Event Handling in Signalling Cascades}, volume = 8, number = {1-2}, pages = {69-79}, year = 2015, month = jun, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHHP-ijasm15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHHP-ijasm15.pdf}, abstract = {Signalling cascades are a recurrent pattern of biological regulatory systems whose analysis has deserved a lot of attention. It has been shown that stochastic Petri nets are appropriate to model such systems and evaluate the probabilities of specific properties. Such an evaluation can be done numerically when the combinatorial state space explosion is manageable or statistically otherwise. However, when the probabilities to be evaluated are too small, random simulation requires more sophisticated techniques for the handling of rare events. In this paper, we show how such involved methods can be successfully applied for signalling cascades. More precisely, we study three relevant properties of a signalling cascade with the help of the COSMOS tool. Our experiments point out interesting dependencies between quantitative parameters of the regulatory system and its transient behaviour. In addition, they demonstrate that we can go beyond the capabilities of MARCIE, which provides one of the most efficient numerical solvers.} }

@inproceedings{RNG-ldq15, address = {Portoro{\v z}, Slovenia}, month = jun, year = 2015, volume = {1376}, series = {CEUR Workshop Proceedings}, publisher = {RWTH Aachen, Germany}, editor = {Rula, Anisa and Zaveri, Amrapali and Knuth, Magnus and Kontokostas, Dimitris}, acronym = {{LDQ}'15}, booktitle = {{P}roceedings of the 2nd {W}orkshop on {L}inked {D}ata {Q}uality ({LDQ}'15)}, author = {Rafes, Karima and Nauroy, Julien and Germain, C{\'e}cile}, title = {Certifying the interoperability of {RDF} database systems}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/RNG-ldq15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RNG-ldq15.pdf}, abstract = {In~March~2013, the W3C recommended SPARQL~1.1 to retrieve and manipulate decentralized RDF data. Real-world usage requires advanced features of SPARQL~1.1. recommendations As these are not consistently implemented, we propose a test framework named TFT (Tests for Triple stores) to test the interoperability of the SPARQL end-point of RDF database systems. This framework can execute the W3C's SPARQL~1.1 test suite and also its own tests of interoperability. To help the developers and end-users of RDF databases, we perform daily tests on Jena-Fuseki, Marmotta-KiWistore, 4Store and three other commercial databases. With these tests, we have built a scoring system named SPARQLScore and share our results on the website \url{http://sparqlscore.com}.} }

@inproceedings{RRS-cav15, address = {San Francisco, CA, USA}, month = jul, year = 2015, volume = 9206, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Kroening, Daniel and Pasareanu, Corina}, acronym = {{CAV}'15}, booktitle = {{P}roceedings of the 27th {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV}'15)~-- Part~{I}}, author = {Randour, Mickael and Raskin, Jean-Fran{\c{c}}ois and Sankur, Ocan}, title = {Percentile Queries in Multi-Dimensional {M}arkov Decision Processes}, pages = {123-139}, url = {http://arxiv.org/abs/1410.4801}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RRS-arxiv14.pdf}, doi = {10.1007/978-3-319-21690-4_8}, abstract = {Multi-dimensional weighted Markov decision processes (MDPs) are useful to analyze systems with multiple objectives that are potentially conflicting and make necessary the analysis of trade-offs. In this paper, we study the complexity of percentile queries in such MDPs and provide algorithms to synthesize strategies that enforce such constraints. Given a multi-dimensional weighted MDP and a quantitative payoff function~\(f\), quantitative thresholds~\(v_i\) (one per dimension), and probability thresholds~\(\alpha_{i}\), we show how to compute a single strategy that enforces that for all dimension~\(i\), the probability that an outcome~\(\rho\) satisfies \(f_{i}(\rho) \geq v_{i}\) is at least~\(\alpha_{i}\). We study this problem for the classical quantitative payoffs studied in the literature (sup, inf, lim sup, lim inf, mean-payoff, truncated sum, discounted sum). So our work can be seen as an extension to the quantitative case of the multi-objective model checking problem on MDPs studied by Etessami et al. in unweighted MDPs.} }

@inproceedings{HK-icalp15, address = {Kyoto, Japan}, month = jul, year = 2015, volume = {9135}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Halld{\'o}rsson, Magnus M. and Iwama, Kazuo and Kobayashi, Naoki and Speckmann, Bettina}, acronym = {{ICALP}'15}, booktitle = {{P}roceedings of the 42nd {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'15)~-- {P}art~{II}}, author = {Haase, Christoph and Kiefer, Stefan}, title = {The Odds of Staying on Budget}, pages = {234-246}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/HK-icalp15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HK-icalp15.pdf}, doi = {10.1007/978-3-662-47666-6_19}, abstract = {Given Markov chains and Markov decision processes (MDPs) whose transitions are labelled with non-negative integer costs, we study the computational complexity of deciding whether the probability of paths whose accumulated cost satisfies a Boolean combination of inequalities exceeds a given threshold. For acyclic Markov chains, we show that this problem is PP-complete, whereas it is hard for the POSSLP problem and in PS PACE for general Markov chains. Moreover, for acyclic and general MDPs, we prove PSPACE- and EXP-completeness, respectively. Our results have direct implications on the complexity of computing reward quantiles in succinctly represented stochastic systems.} }

@inproceedings{DGGL-icalp15, address = {Kyoto, Japan}, month = jul, year = 2015, volume = {9135}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Halld{\'o}rsson, Magnus M. and Iwama, Kazuo and Kobayashi, Naoki and Speckmann, Bettina}, acronym = {{ICALP}'15}, booktitle = {{P}roceedings of the 42nd {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'15)~-- {P}art~{II}}, author = {Dubut, J{\'e}r{\'e}my and Goubault, {\'E}ric and Goubault{-}Larrecq, Jean}, title = {Natural Homology}, pages = {171-183}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DGGL-icalp15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DGGL-icalp15.pdf}, doi = {10.1007/978-3-662-47666-6_14}, abstract = {We propose a notion of homology for directed algebraic topology, based on so-called natural systems of abelian groups, and which we call natural homology. Contrarily to previous proposals, and as we show, natural homology has many desirable properties: it~is invariant under isomorphisms of directed spaces, it is invariant under refinement (subdivision), and it is computable on cubical complexes.} }

@inproceedings{LS-lics15, address = {Kyoto, Japan}, month = jul, year = 2015, publisher = {{IEEE} Press}, acronym = {{LICS}'15}, booktitle = {{P}roceedings of the 30th {A}nnual {ACM\slash IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'15)}, author = {Leroux, J{\'e}r{\^o}me and Schmitz, Sylvain}, title = {Demystifying Reachability in Vector Addition Systems}, pages = {56-67}, url = {http://arxiv.org/abs/1503.00745}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-arxiv15.pdf}, doi = {10.1109/LICS.2015.1}, abstract = {More than 30 years after their inception, the decidability proofs for reachability in vector addition systems (VAS) still retain much of their mystery. These proofs rely crucially on a decomposition of runs successively refined by Mayr, Kosaraju, and Lambert, which appears rather magical, and for which no complexity upper bound is known.\par We first offer a justification for this decomposition technique, by showing that it emerges naturally in the study of the ideals of a well quasi ordering of VAS runs. In a second part, we apply recent results on the complexity of termination thanks to well quasi orders and well orders to obtain fast-growing complexity upper bounds for the decomposition algorithms, thus providing the first known upper bounds for general VAS reachability.} }

@inproceedings{BFGHM-lics15, address = {Kyoto, Japan}, month = jul, year = 2015, publisher = {{IEEE} Press}, acronym = {{LICS}'15}, booktitle = {{P}roceedings of the 30th {A}nnual {ACM\slash IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'15)}, author = {Blondin, Michael and Finkel, Alain and G{\"o}ller, Stefan and Haase, Christoph and McKenzie, Pierre}, title = {Reachability in Two-Dimensional Vector Addition Systems with States is {PSPACE}-Complete}, pages = {32-43}, url = {http://arxiv.org/abs/1412.4259}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFGHM-lics15-long.pdf}, doi = {10.1109/LICS.2015.14}, abstract = {Determining the complexity of the reachability problem for vector addition systems with states (VASS) is a long-standing open problem in computer science. Long known to be decidable, the problem to this day lacks any complexity upper bound whatsoever. In this paper, reachability for two-dimensional VASS is shown PSPACE-complete. This improves on a previously known doubly exponential time bound established by Howell, Rosier, Huynh and Yen in~1986. The coverability and boundedness problems are also noted to be PSPACE-complete. In addition, some complexity results are given for the reachability problem in two-dimensional VASS and in integer VASS when numbers are encoded in unary.} }

@inproceedings{ACR-acsd15, address = {Brussels, Belgium}, month = jun, year = 2015, publisher = {{IEEE} Computer Society Press}, editor = {Haar, Stefan and Meyer, Roland}, acronym = {{ACSD}'15}, booktitle = {{P}roceedings of the 15th {I}nternational {C}onference on {A}pplication of {C}oncurrency to {S}ystem {D}esign ({ACSD}'15)}, author = {Andr{\'e}, {\'E}tienne and Chatain, {\relax Th}omas and Rodr{\'\i}guez, C{\'e}sar}, title = {Preserving Partial Order Runs in Parametric Time {P}etri Nets}, pages = {120-129}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ACR-acsd15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ACR-acsd15.pdf}, doi = {10.1109/ACSD.2015.16}, abstract = {Parameter synthesis for timed systems aims at deriving parameter valuations satisfying a given property. In this paper we target concurrent systems; it is well known that concurrency is a source of state-space explosion, and partial order techniques were defined to cope with this problem. Here we use partial order semantics for parametric time Petri nets as a way to significantly enhance the result of an existing synthesis algorithm. Given a reference parameter valuation, our approach synthesizes other valuations preserving, up to interleaving, the behavior of the reference parameter valuation. We show the applicability of our approach using acyclic asynchronous circuits.} }

@inproceedings{CHKS-pn15, address = {Brussels, Belgium}, month = jun, year = 2015, volume = {9115}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Devillers, Raymond and Valmari, Antti}, acronym = {{PETRI~NETS}'15}, booktitle = {{P}roceedings of the 36th {I}nternational {C}onference on {A}pplications and {T}heory of {P}etri {N}ets ({PETRI~NETS}'15)}, author = {Chatain, {\relax Th}omas and Haar, Stefan and Koutny, Maciej and Schwoon, Stefan}, title = {Non-Atomic Transition Firing in Contextual Nets}, pages = {117-136}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CHKS-pn15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CHKS-pn15.pdf}, doi = {10.1007/978-3-319-19488-2_6}, abstract = {The firing rule for Petri nets assumes instantaneous and simultaneous consumption and creation of tokens. In the context of ordinary Petri nets, this poses no particular problem because of the system's asynchronicity, even if token creation occurs later than token consumption in the firing. With read arcs, the situation changes, and several different choices of semantics are possible. The step semantics introduced by Janicki and Koutny can be seen as imposing a two-phase firing scheme: first, the presence of the required tokens is checked, then consumption and production of tokens happens. Pursuing this approach further, we develop a more general framework based on explicitly splitting the phases of firing, allowing to synthesize coherent steps. This turns out to define a more general non-atomic semantics, which has important potential for safety as it allows to detect errors that were missed by the previous semantics. Then we study the characterization of partial-order processes feasible under one or the other semantics.} }

@incollection{BH-im15, year = 2015, publisher = {CNRS \'Editions}, editor = {Ollinger, Nicolas}, booktitle = {Informatique Math{\'e}matique. Une~photographie en~2015}, author = {Bertrand, Nathalie and Haddad, Serge}, title = {Contr{\^o}le, probabilit{\'e}s et observation partielle}, chapter = 5, pages = {177-227}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BH-im15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BH-im15.pdf} }

@article{DDS-ic15, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Demri, St{\'e}phane and Dhar, Amit Kumar and Sangnier, Arnaud}, title = {Taming Past {LTL} and Flat Counter Systems}, volume = {242}, month = jun, year = 2015, pages = {306-339}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-ic15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-ic15.pdf}, doi = {10.1016/j.ic.2015.03.007}, abstract = {Reachability and LTL model-checking problems for flat counter systems are known to be decidable but whereas the reachability problem can be shown in NP, the best known complexity upper bound for the latter problem is made of a tower of several exponentials. Herein, we show that this problem is only NP-complete even if LTL admits past-time operators and arithmetical constraints on counters. As far as past-time operators are concerned, their addition to LTL immediately leads to complications and hence an NP upper bound cannot be deduced by translating formulae into LTL and studying the problem only for this latter logic. Actually, the NP upper bound is shown by adequately combining a new stuttering theorem for Past LTL and the property of small integer solutions for quantifier-free Presburger formulae. This latter complexity bound extends known and recent results on model-checking weak Kripke structures with LTL formulae as well as reachability problems for flat counter systems. We also provide other complexity results obtained by restricting further the class of flat counter systems.} }

@article{BBDHP-peva15, publisher = {Elsevier Science Publishers}, journal = {Performance Evaluation}, author = {Ballarini, Paolo and Barbot, Beno{\^\i}t and Duflot, Marie and Haddad, Serge and Pekergin, Nihal}, title = {{HASL}: A~New Approach for Performance Evaluation and Model Checking from Concepts to Experimentation}, year = {2015}, month = aug, volume = 90, pages = {53-77}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2015-04.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2015-04.pdf}, doi = {10.1016/j.peva.2015.04.003}, abstract = {We introduce the Hybrid Automata Stochastic Language (HASL), a new temporal logic formalism for the verification of Discrete Event Stochastic Processes (DESP). HASL employs a Linear Hybrid Automaton (LHA) to select prefixes of relevant execution paths of a DESP. LHA allows rather elaborate information to be collected \emph{on-the-fly} during path selection, providing the user with powerful means to express sophisticated measures. A~formula of HASL consists of an LHA and an expression~\(Z\) referring to moments of \emph{path random variables}. A~simulation-based statistical engine is employed to obtain a confidence interval estimate of the expected value of~\(Z\). In~essence, HASL~provides a unifying verification framework where temporal reasoning is naturally blended with elaborate reward-based analysis. Moreover, we have implemented a tool, named COSMOS, for performing analysis of HASL formula for DESP modelled by Petri nets. Using this tool we have developed two detailed case studies: a flexible manufacturing system and a genetic oscillator.} }

@article{LS-tocl15, publisher = {ACM Press}, journal = {ACM Transactions on Computational Logic}, author = {Lazi{\'c}, Ranko and Schmitz, Sylvain}, title = {Non-Elementary Complexities for Branching~{VASS}, {MELL}, and Extensions}, volume = {16}, number = {3:20}, nopages = {}, month = jul, year = 2015, url = {http://arxiv.org/abs/1401.6785}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-tocl15.pdf}, doi = {10.1145/2733375}, abstract = {We study the complexity of reachability problems on branching extensions of vector addition systems, which allows us to derive new non-elementary complexity bounds for fragments and variants of propositional linear logic. We show that provability in the multiplicative exponential fragment is Tower-hard already in the affine case---and hence non-elementary. We match this lower bound for the full propositional affine linear logic, proving its Tower-completeness. We also show that provability in propositional contractive linear logic is Ackermann-complete.} }

@inproceedings{FKM-syncop15, address = {London, UK}, volume = 44, series = {Open Access Series in Informatics}, month = apr, year = 2015, editor = {Andr{\'e}, {\'E}tienne and Frehse, Goran}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, acronym = {{SYNCOP}'15}, booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop on {S}ynthesis of {C}ontinuous {P}arameters ({SYNCOP}'15)}, author = {Fribourg, Laurent and K{\"u}hne, Ulrich and Markey, Nicolas}, title = {Game-based Synthesis of Distributed Controllers for Sampled Switched Systems}, pages = {47-61}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FKM-syncop15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FKM-syncop15.pdf}, doi = {10.4230/OASIcs.SynCoP.2015.47}, abstract = {Switched systems are a convenient formalism for modeling physical processes interacting with a digital controller. Unfortunately, the formalism does not capture the distributed nature encountered e.g. in cyber-physical systems, which are organized as networks of elements interacting with each other and with local controllers. Most current methods for control synthesis can only produce a centralized controller, which is assumed to have complete knowledge of all the component states and can interact with all of them. In~this paper, we~consider a controller synthesis method based on state space decomposition, and propose a game-based approach in order to extend it within a distributed framework.} }

@inproceedings{LDRCF-syncop15, address = {London, UK}, volume = 44, series = {Open Access Series in Informatics}, month = apr, year = 2015, editor = {Andr{\'e}, {\'E}tienne and Frehse, Goran}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, acronym = {{SYNCOP}'15}, booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop on {S}ynthesis of {C}ontinuous {P}arameters ({SYNCOP}'15)}, author = {Le{~}Co{\"e}nt, Adrien and De{~}Vuyst, Florian and Rey, {\relax Ch}ristian and Chamoin, Ludovic and Fribourg, Laurent}, title = {Guaranteed control of switched control systems using model order reduction and state-space bisection}, pages = {32-46}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LDCRF-syncop15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LDCRF-syncop15.pdf}, doi = {10.4230/OASIcs.SynCoP.2015.32}, abstract = {This paper considers discrete-time linear systems controlled by a quantized law, i.e., a piecewise constant time function taking a finite set of values. We show how to generate the control by, first, applying model reduction to the original system, then using a {"}state-space bisection{"} method for synthesizing a control at the reduced-order level, and finally computing an upper bound to the deviations between the controlled output trajectories of the reduced-order model and those of the original model. The effectiveness of our approach is illustrated on several examples of the literature.} }

@inproceedings{ACD-post15, address = {London, UK}, month = apr, year = 2015, volume = {9036}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Focardi, Riccardo and Myers, Andrew}, acronym = {{POST}'15}, booktitle = {{P}roceedings of the 4th {I}nternational {C}onference on {P}rinciples of {S}ecurity and {T}rust ({POST}'15)}, author = {Arapinis, Myrto and Cheval, Vincent and Delaune, St{\'e}phanie}, title = {Composing security protocols: from confidentiality to privacy}, pages = {324-343}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ACD-post15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ACD-post15.pdf}, doi = {10.1007/978-3-662-46666-7_17}, abstract = {Security protocols are used in many of our daily-life applications, and our privacy largely depends on their design. Formal verification techniques have proved their usefulness to analyse these protocols, but they become so complex that modular techniques have to be developed. We propose several results to safely compose security protocols. We consider arbitrary primitives modeled using an equational theory, and a rich process algebra close to the applied pi calculus.\par Relying on these composition results, we derive some security properties on a protocol from the security analysis performed on each of its sub-protocols individually. We consider parallel composition and the case of key-exchange protocols. Our results apply to deal with confidentiality but also privacy-type properties (e.g. anonymity) expressed using a notion of equivalence. We illustrate the usefulness of our composition results on protocols from the 3G phone application and electronic passport.} }

@phdthesis{scerri-phd15, author = {Scerri, Guillaume}, title = {Proofs of security protocols revisited}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2015, month = jan, url = {http://www.lsv.fr/Publis/PAPERS/PDF/scerri-phd15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/scerri-phd15.pdf} }

@article{DD-jancl15, publisher = {Taylor \& Francis}, journal = {Journal of Applied Non-Classical Logics}, author = {Demri, St{\'e}phane and Deters, Morgan}, title = {Separation Logics and Modalities: A~Survey}, volume = 25, number = 1, pages = {50-99}, year = 2015, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-jancl15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-jancl15.pdf}, doi = {10.1080/11663081.2015.1018801}, abstract = {Like modal logic, temporal logic, or description logic, separation logic has become a popular class of logical formalisms in computer science, conceived as assertion languages for Hoare-style proof systems with the goal to perform automatic program analysis. In a broad sense, separation logic is often understood as a programming language, an assertion language and a family of rules involving Hoare triples. In this survey, we present similarities between separation logic as an assertion language and modal and temporal logics. Moreover, we propose a selection of landmark results about decidability, complexity and expressive power.} }

@article{DD-tocl15, publisher = {ACM Press}, journal = {ACM Transactions on Computational Logic}, author = {Demri, St{\'e}phane and Deters, Morgan}, title = {Two-variable separation logic and its inner circle}, volume = 16, number = {2:15}, nopages = {}, month = mar, year = 2015, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-tocl15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-tocl15.pdf}, doi = {10.1145/2724711}, abstract = {Separation logic is a well-known assertion language for Hoare-style proof systems. We show that first-order separation logic with a unique record field restricted to two quantified variables and no program variables is undecidable. This is among the smallest fragments of separation logic known to be undecidable, and this contrasts with decidability of two-variable first-order logic. We also investigate its restriction by dropping the magic wand connective, known to be decidable with non-elementary complexity, and we show that the satisfiability problem with only two quantified variables is not yet elementary recursive. Furthermore, we establish insightful and concrete relationships between two-variable separation logic and propositional in- terval temporal logic (PITL), data logics, and modal logics, providing an inner circle of closely-related logics.} }

@inproceedings{KV-icdt15, address = {Brussels, Belgium}, month = mar, year = 2015, volume = 31, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Arenas, Marcelo}, acronym = {{ICDT}'15}, booktitle = {{P}roceedings of the 18th {I}nternational {C}onference on {D}atabase {T}heory ({ICDT}'15)}, author = {Koutsos, Adrien and Vianu, Victor}, title = {Process-Centric Views of Data-Driven Business Artifacts}, pages = {247-264}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/KV-icdt15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KV-icdt15.pdf}, doi = {10.4230/LIPIcs.ICDT.2015.247}, abstract = {Declarative, data-aware workflow models are becoming increasingly pervasive. While these have numerous benefits, classical process-centric specifications retain certain advantages. Workflow designers are used to development tools such as BPMN or UML diagrams, that focus on control flow. Views describing valid sequences of tasks are also useful to provide stake-holders with high-level descriptions of the workflow, stripped of the accompanying data. In this paper we study the problem of recovering process-centric views from declarative, data-aware workflow specifications in a variant of IBM's business artifact model. We focus on the simplest and most natural process-centric views, specified by finite-state transition systems, and describing regular languages. The results characterize when process-centric views of artifact systems are regular, using both linear and branching-time semantics. We also study the impact of data dependencies on regularity of the views.} }

@inproceedings{NF-icdt15, address = {Brussels, Belgium}, month = mar, year = 2015, volume = 31, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Arenas, Marcelo}, acronym = {{ICDT}'15}, booktitle = {{P}roceedings of the 18th {I}nternational {C}onference on {D}atabase {T}heory ({ICDT}'15)}, author = {Francis, Nadime}, title = {Asymptotic Determinacy of Path Queries using Union-of-Paths Views}, pages = {44-59}, note = {Best student paper award}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/NF-icdt15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/NF-icdt15.pdf}, doi = {10.4230/LIPIcs.ICDT.2015.44}, abstract = {We consider the view determinacy problem over graph databases for queries defined as (possibly infinite) unions of path queries. These queries select pairs of nodes in a graph that are connected through a path whose length falls in a given set. A~view specification is a set of such queries. We~say that a view specification~\(\textbf{V}\) determines a query~\(Q\) if, for all databases~\(D\), the answers to~\(\textbf{V}\) on~\(D\) contain enough information to answer~\(Q\).\par Our main result states that, given a view~\(\textbf{V}\), there exists an explicit bound that depends on~\(\textbf{V}\) such that we can decide the determinacy problem for all queries that ask for a path longer than this bound, and provide first-order rewritings for the queries that are determined. We call this notion asymptotic determinacy. As a corollary, we can also compute the set of almost all path queries that are determined by~\(\textbf{V}\).} }

@inproceedings{RRS-vmcai15, address = {Mumbai, India}, month = jan, year = 2015, volume = 8931, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {D'Souza, Deepak and Lal, Akash and Larsen, Kim Guldstrand}, acronym = {{VMCAI}'15}, booktitle = {{P}roceedings of the 16th {I}nternational {C}onference on {V}erification, {M}odel {C}hecking and {A}bstract {I}nterpretation ({VMCAI}'15)}, author = {Randour, Mickael and Raskin, Jean-Fran{\c{c}}ois and Sankur, Ocan}, title = {Variations on the Stochastic Shortest Path Problem}, pages = {1-18}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/RRS-vmcai15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RRS-vmcai15.pdf}, doi = {10.1007/978-3-662-46081-8_1}, abstract = {In this invited contribution, we revisit the stochastic shortest path problem, and show how recent results allow one to improve over the classical solutions: we present algorithms to synthesize strategies with multiple guarantees on the distribution of the length of paths reaching a given target, rather than simply minimizing its expected value. The concepts and algorithms that we propose here are applications of more general results that have been obtained recently for Markov decision processes and that are described in a series of recent papers.} }

@article{VCDHRR-icomp15, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Velner, Yaron and Chatterjee, Krishnendu and Doyen, Laurent and Henzinger, Thomas A. and Rabinovich, Alexander Moshe and Raskin, Jean-Fran{\c{c}}ois}, title = {The complexity of multi-mean-payoff and multi-energy games}, year = 2015, month = apr, volume = 241, pages = {177-196}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDRR-icomp15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDRR-icomp15.pdf}, doi = {10.1016/j.ic.2015.03.001}, abstract = {In mean-payoff games, the objective of the protagonist is to ensure that the limit average of an infinite sequence of numeric weights is nonnegative. In energy games, the objective is to ensure that the running sum of weights is always nonnegative. Multi-mean-payoff and multi-energy games replace individual weights by tuples, and the limit average (resp., running sum) of each coordinate must be (resp.,~remain) nonnegative. We prove finite-memory determinacy of multi-energy games and show inter-reducibility of multi-mean-payoff and multi-energy games for finite-memory strategies. We improve the computational complexity for solving both classes with finite-memory strategies: we prove coNP-completeness improving the previous known \textsf{EXPSPACE} bound. For memoryless strategies, we show that deciding the existence of a winning strategy for the protagonist is NP-complete. We present the first solution of multi-mean-payoff games with infinite-memory strategies: we show that mean-payoff-sup objectives can be decided in \textsf{NP}{{\(\cap\)}}\textsf{coNP}, whereas mean-payoff-inf objectives are coNP-complete.} }

@article{CDRR-icomp15, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, 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}, year = 2015, month = jun, volume = 242, pages = {25-52}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDRR-icomp15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDRR-icomp15.pdf}, doi = {10.1016/j.ic.2015.03.010}, 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 \(\textsf{NP}\cap\textsf{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.} }

@article{GJL-tocl15, publisher = {ACM Press}, journal = {ACM Transactions on Computational Logic}, author = {G{\"o}ller, Stefan and Jung, Jean Christoph and Lohrey, Markus}, title = {The Complexity of Decomposing Modal and First-Order Theories}, volume = 16, number = {1:9}, nopages = {}, month = mar, year = 2015, url = {http://www.lsv.fr/Publis/PAPERS/PDF/GJL-tocl15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GJL-tocl15.pdf}, doi = {10.1145/2699918}, abstract = {We study the satisfiability problem of the logic \(\textbf{K}^{2}=\textbf{K}\times\textbf{K}\), i.e., the two-dimensional variant of unimodal logic, where models are restricted to asynchronous products of two Kripke frames. Gabbay and Shehtman proved in 1998 that this problem is decidable in a tower of exponentials. So far the best known lower bound is NEXP-hardness shown by Marx and Mikul\'as in~2001.\par Our first main result closes this complexity gap: We show that satisfiability in~\(\textbf{K}^{2}\) is nonelementary. More precisely, we prove that it is \(k\)-NEXP-complete, where \(k\) is the switching depth (the~minimal modal rank among the two dimensions) of the input formula, hereby solving a conjecture of Marx and Mikul\'as. Using our lower-bound technique allows us to derive also nonelementary lower bounds for the two-dimensional modal logics \(\textbf{K}^{4}\times\textbf{K}\) and \(\textbf{S5}_{2}\times\textbf{K}\) for which only elementary lower bounds were previously known.\par Moreover, we apply our technique to prove nonelementary lower bounds for the sizes of Feferman-Vaught decompositions with respect to product for any decomposable logic that is at least as expressive as unimodal\(\textbf{K}\), generalizing a recent result by the first author and~Lin. For the three-variable fragment \(\textsf{FO}^3\) of first-order logic, we obtain the following immediate corollaries: (i)~the~size of Feferman-Vaught decompositions with respect to disjoint sum are inherently nonelementary and (ii)~equivalent formulas in Gaifman normal form are inherently nonelementary.\par Our second main result consists in providing effective elementary (more precisely, doubly exponential) upper bounds for the two-variable fragment \(\textsf{FO}^2\) of first-order logic both for Feferman-Vaught decompositions and for equivalent formulas in Gaifman normal form.} }

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

@techreport{CHH-arxiv16, author = {Chistikov, Dmitry and Haase, Christoph and Halfon, Simon}, title = {Context-Free Commutative Grammars with Integer Counters and Resets}, institution = {Computing Research Repository}, number = {1511-04893}, year = {2015}, month = nov, type = {Research Report}, url = {http://arxiv.org/abs/1511.04893}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CHH-arxiv16.pdf}, note = {31~pages}, abstract = {We study the computational complexity of reachability, coverability and inclusion for extensions of context-free commutative grammars with integer counters and reset operations on them. Those grammars can alternatively be viewed as an extension of communication-free Petri nets. Our main results are that reachability and coverability are inter-reducible and both NP-complete. In particular, this class of commutative grammars enjoys semi-linear reachability sets. We also show that the inclusion problem is, in general, coNEXP-complete and already \(\Pi^{P}_{2}\)-complete for grammars with only one non-terminal symbol. Showing the lower bound for the latter result requires us to develop a novel \(\Pi^{P}_{2}\)-complete variant of the classic subset sum problem.} }

@misc{vip-D32, author = {Baelde, David and Delaune, St{\'e}phanie and Kremer, Steve}, title = {Decision procedures for equivalence based properties (part~{II})}, howpublished = {Deliverable VIP~3.2 (ANR-11-JS02-0006)}, month = sep, year = {2015}, note = {9~pages}, type = {Contract Report}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/vip-d32.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/vip-d32.pdf} }

@misc{vip-D41, author = {Delaune, St{\'e}phanie and Kremer, Steve}, title = {Composition results for equivalence-based security properties}, howpublished = {Deliverable VIP~3.1 (ANR-11-JS02-0006)}, month = sep, year = {2015}, note = {6~pages}, type = {Contract Report}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/vip-d41.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/vip-d41.pdf} }

@article{LS-sigmodrec15, publisher = {ACM Press}, journal = {SIGMOD Records}, author = {Segoufin, Luc}, title = {Constant Delay Enumeration for Conjunctive Queries}, year = 2015, volume = {44}, number = {1}, pages = {10-17}, month = mar, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-sigmodrec15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-sigmodrec15.pdf}, doi = {10.1145/2783888.2783894}, abstract = {We survey some of the recent results about enumerating the answers to queries over a database. We focus on the case where the enumeration is performed with a constant delay between any two consecutive solutions, after a linear time preprocessing.\par This cannot be always achieved. It requires restricting either the class of queries or the class of databases.\par We consider conjunctive queries and describe several scenarios when this is possible.} }

@article{PS-lmcs15, journal = {Logical Methods in Computer Science}, author = {Place, {\relax Th}omas and Segoufin, Luc}, title = {Deciding definability in {{\(\textrm{FO}^{2}(<_{\textbf{h}},<_{\textbf{v}})\)}} on trees}, year = 2015, volume = {11}, number = {3:5}, nopages = {}, month = sep, url = {http://www.lsv.fr/Publis/PAPERS/PDF/PS-lmcs15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PS-lmcs15.pdf}, doi = {10.2168/LMCS-11(3:5)2015}, abstract = {We provide a decidable characterization of regular forest languages definable in \(\textrm{FO}^{2}(<_{\textbf{h}},<_{\textbf{v}})\). By~\(\textrm{FO}^{2}(<_{\textbf{h}},<_{\textbf{v}})\) we refer to the two variable fragment of first order logic built from the descendant relation and the following sibling relation. In terms of expressive power it corresponds to a fragment of the navigational core of XPath that contains modalities for going up to some ancestor, down to some descendant, left to some preceding sibling, and right to some following sibling.\par We also show that our techniques can be applied to other two variable first-order logics having exactly the same vertical modalities as \(\textrm{FO}^{2}(<_{\textbf{h}},<_{\textbf{v}})\) but having different horizontal modalities.} }

@article{FSS-lmcs15, journal = {Logical Methods in Computer Science}, author = {Francis, Nadime and Segoufin, Luc and Sirangelo, Cristina}, title = {Datalog Rewritings of Regular Path Queries using Views}, year = 2015, volume = {11}, number = {4:14}, nopages = {}, month = dec, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FSS-lmcs15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FSS-lmcs15.pdf}, doi = {10.2168/LMCS-11(4:14)2015}, abstract = {We consider query answering using views on graph databases, i.e. databases structured as edge-labeled graphs. We mainly consider views and queries specified by Regular Path Queries~(RPQ). These are queries selecting pairs of nodes in a graph database that are connected via a path whose sequence of edge labels belongs to some regular language. We say that a view~\(\textbf{V}\) determines a query~\(Q\) if for all graph databases~\(D\), the~view image~\(\textbf{V}(D)\) always contains enough information to answer~\(Q\) on~\(D\). In~other words, there is a well defined function from~\(\textbf{V}(D)\) to~\(Q(D)\).\par Our main result shows that when this function is monotone, there exists a rewriting of~\(Q\) as a Datalog query over the view instance~\(\textbf{V}(D)\). In particular the rewriting query can be evaluated in time polynomial in the size of~\(\textbf{V}(D)\). Moreover this implies that it is decidable whether an RPQ query can be rewritten in Datalog using RPQ views.} }

@article{BCS-jacm15, publisher = {ACM Press}, journal = {Journal of the~{ACM}}, author = {B{\'a}r{\'a}ny, Vince and ten Cate, Balder and Segoufin, Luc}, title = {Guarded nagation}, year = 2015, volume = {62}, number = {3:22}, nopages = {}, month = jun, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCS-jacm15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCS-jacm15.pdf}, doi = {10.1145/2701414}, abstract = { We consider restrictions of first-order logic and of fixpoint logic in which all occurrences of negation are required to be guarded by an atomic predicate. In terms of expressive power, the logics in question, called GNFO and GNFP, extend the guarded fragment of first-order logic and the guarded least fixpoint logic, respectively. They also extend the recently introduced unary negation fragments of first-order logic and of least fixpoint logic.\par We show that the satisfiability problem for GNFO and for GNFP is 2ExpTime-complete, both on arbitrary structures and on finite structures. We also study the complexity of the associated model checking problems. Finally, we show that GNFO and GNFP are not only computationally well behaved, but also model theoretically: we~show that GNFO and GNFP have the tree-like model property and that GNFO has the finite model property, and we characterize the expressive power of GNFO in terms of invariance for an appropriate notion of bisimulation.\par Our complexity upper bounds for GNFO and GNFP hold true even for their {"}clique-guarded{"} extensions CGNFO and CGNFP, in which clique guards are allowed in the place of guards.} }

@inproceedings{DS-flc2, noaddress = {Berlin, Germany}, month = sep, year = 2015, volume = 9300, series = {Lecture Notes in Computer Science}, publisher = {Springer}, noacronym = {}, booktitle = {Fields of Logic and Computation~{II}~-- Essays Dedicated to {Y}uri {G}urevich on the Occasion of His 75th Birthday}, editor = { Beklemishev, Lev D. and Blass, Andreas and Dershowitz, Nachum and Finkbeiner, Bernd and Schulte, Wolfram}, author = {Dawar, Anuj and Segoufin, Luc}, title = {Capturing {MSO} with one quantifier}, pages = {142-152}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DS-flc2.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DS-flc2.pdf}, doi = {10.1007/978-3-319-23534-9_8}, abstract = {We construct a single Lindstr{\"o}m quantifier~\(Q\) such that \(\textrm{FO} (Q)\), the extension of first-order logic with~\(Q\) has the same expressive power as monadic second-order logic on the class of binary trees (with distinct left and right successors) and also on unranked trees with a sibling order. This resolves a conjecture by ten~Cate and Segoufin. The quantifier~\(Q\) is a variation of a quantifier expressing the Boolean satisfiability problem.} }

@inproceedings{SA-adbis15, address = {Poitiers, France}, month = sep, year = 2015, nmnote = {post-proceedings published by LNCS, to appear}, editor = {Bellatreche, Ladjel}, acronym = {{ADBIS}'15}, booktitle = {{P}roceedings of the 19th {E}ast-{E}uropean {C}onference on {A}dvances in {D}atabases and {I}nformation {S}ystems ({ADBIS}'15)}, author = {Abiteboul, Serge}, title = {The Story of Webdamlog}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/SA-adbis15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SA-adbis15.pdf}, abstract = {We~summarize in this paper works about the management of data in a distributed manner based on Webdamlog, a datalog-extension. We~point to relevant articles on these works. More references may be found there.} }

@proceedings{HM-acsd2015, editor = {Haar, Stefan and Meyer, Roland}, title = {{P}roceedings of the 15th {I}nternational {C}onference on {A}pplication of {C}oncurrency to {S}ystem {D}esign ({ACSD}'15)}, booktitle = {{P}roceedings of the 15th {I}nternational {C}onference on {A}pplication of {C}oncurrency to {S}ystem {D}esign ({ACSD}'15)}, acronym = {{ACSD}'15}, publisher = {{IEEE} Computer Society Press}, year = 2015, month = jun, address = {Brussels, Belgium}, url = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=7352411} }

@inproceedings{ADESWSS-webdb15, address = {Melbourne, Australia}, month = may, year = 2015, publisher = {ACM Press}, editor = {Stoyanovich, Julia and Suchanek, Fabian M}, acronym = {({W}eb{DB}'15)}, booktitle = {{P}roceedings of the 18th {I}nternational {W}orkshop on the {W}eb and {D}atabases ({W}eb{DB}'15)}, author = {Abiteboul, Serge and Dong, Xin Luna and Etzioni, Oren and Srivastava, Divesh and Weikum, Gerhard and Stoyanovich, Julia and Suchanek, Fabian M.}, title = {The elephant in the room: getting value from Big Data}, pages = {1-5}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ADESWSS-webdb15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ADESWSS-webdb15.pdf}, doi = {10.1145/2767109.2770014} }

@inproceedings{MSAM-sigmod15, address = {Melbourne, Australia}, month = may # {-} # jun, year = 2015, publisher = {ACM Press}, editor = {Sellis, Timos K. and Davidson, Susan B. and Ives,Zachary G.}, acronym = {{SIGMOD}'15}, booktitle = {{P}roceedings of the {ACM} {SIGMOD} {I}nternaitonal {C}onference on {M}anagement of {D}ata ({SIGMOD}'15)}, author = {Moffitt, Vera Zaychik and Stoyanovich, Julia and Abiteboul, Serge and Miklau, Gerome}, title = {Collaborative Access Control in {W}ebdam{L}og}, pages = {197-211}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/MSAM-sigmod15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/MSAM-sigmod15.pdf}, doi = {10.1109/DSAA.2015.7344775}, abstract = {The management of Web users' personal information is increasingly distributed across a broad array of applications and systems, including online social networks and cloud-based services. Users wish to share data using these systems, but avoiding the risks of unintended disclosures or unauthorized access by applications has become a major challenge.\par We propose a novel access control model that operates within a distributed data management framework based on datalog. Using this model, users can control access to data they own and control applications they run. They can conveniently specify access control policies providing flexible tuple-level control derived using provenance information. We present a formal specification of the model, an implementation built using an open-source distributed datalog engine, and an extensive experimental evaluation showing that the computational cost of access control is modest.} }

@article{cacm15-AAK, publisher = {ACM Press}, journal = {Communications of the~{ACM}}, author = {Abiteboul, Serge and Andr{\'e}, Benjamin and Kaplan, Daniel}, title = {Managing your digital life}, volume = {58}, number = {5}, pages = {32-35}, year = 2015, month = may, url = {http://www.lsv.fr/Publis/PAPERS/PDF/cacm15-AAK.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/cacm15-AAK.pdf}, doi = {10.1145/2670528}, abstract = {Everyone should be able to manage their personal data with a personal information management system.} }

@inproceedings{APS-tap15, address = {L'Aquila, Italy}, month = jul, year = 2015, volume = 9154, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = { Blanchette, Jasmin Christian and Kosmatov, Nikolai}, acronym = {{TAP}'15}, booktitle = {{P}roceedings of the 9th {I}nternational {C}onference on {T}ests and {P}roofs ({TAP}'15)}, author = {Athanasiou, Konstantinos and Ponce{ }de{~}Le{\'o}n, Hern\'an and Schwoon, Stefan}, title = {Test Case Generation for Concurrent Systems Using Event Structures}, pages = {19-37}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/APS-tap15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/APS-tap15.pdf}, doi = {10.1007/978-3-319-21215-9_2}, abstract = {This paper deals with the test-case generation problem for concurrent systems that are specified by true-concurrency models such as Petri nets. We show that using true-concurrency models reduces both the size and the number of test cases needed for achieving certain coverage criteria. We present a test-case generation algorithm based on Petri net unfoldings and a SAT encoding for solving controllability problems in test cases. Finally, we evaluate our algorithm against traditional test-case generation methods under interleaving semantics.} }

@misc{mcc:2015, author = {F. Kordon and H. Garavel and L. M. Hillah and Hulin{-}Hubard, Francis and A. Linard and M. Beccuti and A. Hamez and E. Lopez-Bobeda and L. Jezequel and J. Meijer and E. Paviot-Adet and C. Rodriguez and C. Rohr and J. Srba and Y. Thierry-Mieg and K. Wolf}, month = jun, title = {{Complete Results for the 2015 Edition of the Model Checking Contest}}, year = {2015}, url = {http://mcc.lip6.fr/2015/results.php} }

@misc{JGL:dom15, author = {Goubault{-}Larrecq, Jean}, howpublished = {Invited talk, Domains XII workshop, Cork, Ireland}, month = aug, title = {Formal balls}, year = {2015} }

@misc{GSM:dga-inria15, author = {Goubault-Larrecq, Jean and Sentucq, Pierre-Arnaud and Majorczyk, Fr{\'e}d{\'e}ric}, howpublished = {Rapport interm{\'e}diaire du contrat DGA-INRIA Orchids}, month = may, title = {Etat d'avancement interm{\'e}diaire des travaux engag{\'e}s sur {OrchIDS}}, year = {2015} }

@mastersthesis{m2-Gonzalez, author = {Gonz{\'a}lez, Mauricio}, title = {{Constructions d'Information Parfaite pour certains Jeux {\`a} Information Imparfaite. Quelques Algorithmes.}}, school = {Universit{\'e} Pierre et Marie Curie, Paris, France}, type = {Rapport de {M}aster}, year = {2015}, month = dec }

@mastersthesis{m2-Fortin, author = {Fortin, Marie}, title = {{Verification of distributed systems with parameterized network topology}}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2015}, month = sep }

*This file was generated by
bibtex2html 1.98.*