@inproceedings{ltc-GardentPPS11, address = {Pozna\'n, Poland}, month = nov, year = 2014, volume = {8387}, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, editor = {Vetulani, Zygmunt and Mariani, Joseph}, acronym = {{LTC}'11}, booktitle = {{P}roceedings of the 5th {L}anguage {\&} {T}echnology {C}onference ({LTC}'11)}, author = {Gardent, Claire and Perrier, Guy and Parmentier, Yannick and Schmitz, Sylvain}, title = {Lexical Disambiguation in {LTAG} using Left Context}, nopages = {}, url = {http://hal.archives-ouvertes.fr/hal-00629902/}, abstract = {In this paper, we present an automaton-based lexical disambiguation process for Lexicalized Tree-Adjoining Grammar (LTAG). This process builds on previous work of Bonfante \textit{et~al.}~(2004), and extends it by computing a polarity-based abstraction, which contains information about left context. This extension allows for a faster lexical disambiguation by reducing the filtering automaton.} }

@inproceedings{ABGGP-vstte13, address = {Atherton, California, USA}, year = 2014, volume = 8164, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Cohen, Ernie and Rybalchenko, Andrey}, acronym = {{VSTTE}'13}, booktitle = {{R}evised {S}elected {P}apers of the 5th {IFIP} {TC2}\slash{WG2.3} {C}onference {V}erified {S}oftware---{T}heories, {T}ools, and {E}xperiments ({VSTTE}'13)}, author = {Adj{\'e}, Assal{\'e} and Bouissou, Olivier and Goubault{-}Larrecq, Jean and Goubault, {\'E}ric and Putot, Sylvie}, title = {Static Analysis of Programs with Imprecise Probabilistic Inputs}, pages = {22-47}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGGP-vstte13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGGP-vstte13.pdf}, doi = {10.1007/978-3-642-54108-7}, abstract = {Having a precise yet sound abstraction of the inputs of numerical programs is important to analyze their behavior. For many programs, these inputs are probabilistic, but the actual distribution used is only partially known. We present a static analysis framework for reasoning about programs with inputs given as imprecise probabilities: we define a collecting semantics based on the notion of previsions and an abstract semantics based on an extension of Dempster-Shafer structures. We prove the correctness of our approach and show on some realistic examples the kind of invariants we are able to infer.} }

@mastersthesis{m2-lefaucheux, author = {Lefaucheux, Engel}, title = {D{\'e}tection de fautes dans les syst{\`e}mes probabilistes}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2014}, month = sep, url = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-lefaucheux.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-lefaucheux.pdf}, note = {35~pages} }

@mastersthesis{m2-dubut, author = {Dubut, J{\'e}r{\'e}my}, title = {{H}omologie dirig{\'e}e}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2014}, month = sep, url = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-dubut.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-dubut.pdf}, note = {35~pages} }

@mastersthesis{m2-halfon, author = {Halfon, Simon}, title = {Non Primitive Recursive Complexity Classes}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2014}, month = sep, url = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-halfon.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-halfon.pdf}, note = {21~pages} }

@inproceedings{FFLRS-fsfma14, address = {Singapore}, month = may, year = 2014, volume = 156, series = {Electronic Proceedings in Theoretical Computer Science}, editor = {Lin, Shang{-}Wei and Petrucci, Laure}, acronym = {{FSFMA}'14}, booktitle = {{P}roceedings of the 2nd {F}rench-{S}ingaporean {W}orkshop on {F}ormal {M}ethods and {A}pplications ({FSFMA}'14)}, author = {Feld, Gilles and Fribourg, Laurent and Labrousse, Denis and Revol, Bertrand and Soulat, Romain}, title = {Correct-by-design Control Synthesis for Multilevel Converters using State Space Decomposition}, pages = {5-16}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FFLRS-fsfma14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FFLRS-fsfma14.pdf}, doi = {10.4204/EPTCS.156.5}, abstract = {High-power converters based on elementary switching cells are more and more used in the industry of power electronics owing to various advantages such as lower voltage stress and reduced power loss. However, the complexity of controlling such converters is a major challenge that the power manufacturing industry has to face with. The synthesis of industrial switching controllers relies today on heuristic rules and empiric simulation. The state of the system is not guaranteed to stay within the limits that are admissible for its correct electrical behavior. We show here how to apply a formal method in order to synthesize a correct-by-design control that guarantees that the power converter will always stay within a predefined safe zone of variations for its input parameters. The method is applied in order to synthesize a correct-by-design control for 5-level and 7-level power converters with a flying capacitor topology. We check the validity of our approach by numerical simulations for 5 and 7 levels. We also perform physical experimentations using a prototype built by SATIE laboratory for 5 levels} }

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

@misc{cassting-D62, author = {Markey, Nicolas and Valette, Sophie}, title = {Annual report for Year~1}, howpublished = {Cassting deliverable~D6.2 (FP7-ICT-601148)}, month = may, year = {2014}, note = {38~pages}, type = {Contract Report} }

@misc{cassting-D31, author = {Markey, Nicolas and Brihaye, {\relax Th}omas and Larsen, Kim G.}, title = {Robustness of collective adaptive systems}, howpublished = {Cassting deliverable~D3.1 (FP7-ICT-601148)}, month = mar, year = {2014}, note = {17~pages}, type = {Contract Report}, url = {http://www.cassting-project.eu/wp-content/uploads/2014/05/deliv-31.pdf}, pdf = {http://www.cassting-project.eu/wp-content/uploads/2014/05/deliv-31.pdf} }

@misc{cassting-D24, author = {Markey, Nicolas and Chaturvedi, Namit and Geeraerts, Gilles and Srba, Ji{\v{r}}{\'\i}}, title = {Efficient strategy synthesis for complex objectives}, howpublished = {Cassting deliverable~D2.4 (FP7-ICT-601148)}, month = oct, year = {2014}, note = {20~pages}, type = {Contract Report}, url = {http://www.cassting-project.eu/wp-content/uploads/2014/10/deliv-24.pdf}, pdf = {http://www.cassting-project.eu/wp-content/uploads/2014/10/deliv-24.pdf} }

@misc{cassting-D14, author = {Brihaye, {\relax Th}omas and Markey, Nicolas}, title = {Solution concepts for collective adaptive systems}, howpublished = {Cassting deliverable~D1.4 (FP7-ICT-601148)}, month = mar, year = {2014}, note = {13~pages}, type = {Contract Report}, url = {http://www.cassting-project.eu/wp-content/uploads/2014/05/deliv-14.pdf}, pdf = {http://www.cassting-project.eu/wp-content/uploads/2014/05/deliv-14.pdf} }

@article{BFCH-compj14, publisher = {Oxford University Press}, journal = {The Computer Journal}, author = {Beccuti, Marco and Franceschinis, Giuliana and Codetta{-}Raiteri, Daniele and Haddad, Serge}, title = {Computing Optimal Repair Strategies by Means of NdRFT Modeling and Analysis}, volume = 57, number = 12, month = dec, year = 2014, pages = {1870-1892}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFCH-compj14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFCH-compj14.pdf}, doi = {10.1093/comjnl/bxt134}, abstract = {In this paper, the \emph{Non-deterministic Repairable Fault Tree}~(NdRFT) formalism is proposed: it allows the modeling of failures of complex systems in addition to their repair processes. Its originality with respect to other Fault Tree extensions allows us to address repair strategy optimization problems: in an NdRFT model, the decision as to whether to start or not a given repair action is non-deterministic, so that all the possibilities are left open. The formalism is rather powerful, it allows: the specification of self-revealing events, the representation of components degradation, the choice among local repair, global repair, preventive maintenance, and the specification of the resources needed to start a repair action. The optimal repair strategy with respect to some relevant system state function, e.g. system unavailability, can then be computed by solving an optimization problem on a Markov Decision Process derived from the NdRFT. Such derivation is obtained by converting the NdRFT model into an intermediate formalism called Markov Decision Petri Net~(MDPN). In the paper, the NdRFT syntax and semantics are formally described, together with the conversion rules to derive from the NdRFT the corresponding MDPN model. The application of NdRFT is illustrated through examples.} }

@article{GLS-tods14, publisher = {ACM Press}, journal = {ACM Transactions on Database Systems}, author = {Gheerbrant, Am{\'e}lie and Libkin, Leonid and Sirangelo, Cristina}, title = {Na{\"\i}ve Evaluation of Queries over Incomplete Databases}, volume = {39}, number = {4:31}, nopages = {}, month = dec, year = {2014}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/GLS-tods14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLS-tods14.pdf}, doi = {10.1145/2691190.2691194}, abstract = {The term na{\"\i}ve evaluation refers to evaluating queries over incomplete databases as if nulls were usual data values, i.e., to using the standard database query evaluation engine. Since the semantics of query answering over incomplete databases is that of certain answers, we would like to know when na{\"\i}ve evaluation computes them: i.e., when certain answers can be found without inventing new specialized algorithms. For relational databases it is well known that unions of conjunctive queries possess this desirable property, and results on preservation of formulae under homomorphisms tell us that within relational calculus, this class cannot be extended under the open-world assumption.\par Our goal here is twofold. First, we develop a general framework that allows us to determine, for a given semantics of incompleteness, classes of queries for which na{\"\i}ve evaluation computes certain answers. Second, we apply this approach to a variety of semantics, showing that for many classes of queries beyond unions of conjunctive queries, na{\"\i}ve evaluation makes perfect sense under assumptions different from open-world. Our key observations are: (1)~na{\"\i}ve evaluation is equivalent to monotonicity of queries with respect to a semantics-induced ordering, and (2)~for most reasonable semantics of incompleteness, such monotonicity is captured by preservation under various types of homomorphisms. Using these results we find classes of queries for which na{\"\i}ve evaluation works, e.g., positive first-order formulae for the closed-world semantics. Even more, we introduce a general relation-based framework for defining semantics of incompleteness, show how it can be used to capture many known semantics and to introduce new ones, and describe classes of first-order queries for which na{\"\i}ve evaluation works under such semantics.} }

@inproceedings{BC-ccs14, address = {Scottsdale, Arizona, USA}, month = nov, year = 2014, publisher = {ACM Press}, editor = {Ahn, Gail-Joon and Yung, Moti and Li, Ninghui}, acronym = {{CCS}'14}, booktitle = {{P}roceedings of the 21st {ACM} {C}onference on {C}omputer and {C}ommunications {S}ecurity ({CCS}'14)}, author = {Bana, Gergei and Comon{-}Lundh, Hubert}, title = {A~Computationally Complete Symbolic Attacker for Equivalence Properties}, pages = {609-620}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BC-ccs14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BC-ccs14.pdf}, doi = {10.1145/2660267.2660276}, abstract = {We consider the problem of computational indistinguishability of protocols. We design a symbolic model, amenable to automated deduction, such that a successful inconsistency proof implies computational indistinguishability. Conversely, symbolic models of distinguishability provide clues for likely computational attacks. We follow the idea we introduced earlier for reachability properties, axiomatizing what an attacker cannot violate. This results a computationally complete symbolic attacker, and ensures unconditional computational soundness for the symbolic analysis. We present a small library of computationally sound, modular axioms, and test our technique on an example protocol. Despite additional difficulties stemming from the equivalence properties, the models and the soundness proofs turn out to be simpler than they were for reachability properties.} }

@phdthesis{ponce-phd2014, author = {Ponce{ }de{~}Le{\'o}n, Hern{\'a}n}, title = {Testing Concurrent Systems Through Event Structures}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2014, month = nov, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ponce-phd14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ponce-phd14.pdf} }

@phdthesis{barbot-phd2014, author = {Barbot, Beno{\^\i}t}, title = {Acceleration for Statistical Model Checking}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2014, month = nov, url = {http://www.lsv.fr/Publis/PAPERS/PDF/barbot-phd14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/barbot-phd14.pdf} }

@phdthesis{sirangelo-HDR14, author = {Sirangelo, Cristina}, title = {Representing and querying incomplete information: a~data interoperability perspective}, year = 2014, month = dec, type = {M{\'e}moire d'habilitation}, school = {{\'E}cole Normale Sup{\'e}rieure de Cachan, France}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/hdr-CS14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/hdr-CS14.pdf} }

@article{LLV-tcs14, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {Lange, Martin and Lozes, {\'E}tienne and Vargas{ }Guzm{\'a}n, Manuel}, title = {Model-checking process equivalences}, volume = {560}, number = {3}, year = {2014}, month = dec, pages = {326-347}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LLV-tcs14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LLV-tcs14.pdf}, doi = {10.1016/j.tcs.2014.08.020}, abstract = {Process equivalences are formal methods that relate programs and systems which, informally, behave in the same way. Since there is no unique notion of what it means for two dynamic systems to display the same behaviour there are a multitude of formal process equivalences, ranging from bisimulation to trace equivalence, categorised in the linear-time branching-time spectrum.\par We present a logical framework based on an expressive modal fixpoint logic which is capable of defining many process equivalence relations: for each such equivalence there is a fixed formula which is satisfied by a pair of processes if and only if they are equivalent with respect to this relation.\par We explain how to do model checking for this logic in EXPTIME. This allows model checking technology to be used for process equivalence checking. We introduce two fragments of the logic for which it is possible to do model-checking in PTIME and PSPACE respectively, and show that the formulas that define the process equivalences we consider are in one of these fragments. This yields a generic proof technique for establishing the complexities of these process equivalences.\par Finally, we show how partial evaluation can be used to obtain decision procedures for process equivalences from the generic model checking scheme.} }

@article{BHLM-lmcs14, journal = {Logical Methods in Computer Science}, author = {Bollig, Benedikt and Habermehl, Peter and Leucker, Martin and Monmege, Benjamin}, title = {A~Robust Class of Data Languages and an Application to Learning}, year = {2014}, month = dec, volume = 10, number = {4:19}, nopages = {}, url = {http://arxiv.org/abs/1411.6646}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHLM-lmcs14.pdf}, doi = {10.2168/LMCS-10(4:19)2014}, abstract = {We~introduce session automata, an automata model to process data words, i.e., words over an infinite alphabet. Session automata support the notion of fresh data values, which are well suited for modeling protocols in which sessions using fresh values are of major interest, like in security protocols or ad-hoc networks. Session automata have an expressiveness partly extending, partly reducing that of classical register automata. We~show that, unlike register automata and their various extensions, session automata are robust: They (i)~are closed under intersection, union, and (resource-sensitive) complementation, (ii)~admit a symbolic regular representation, (iii)~have a decidable inclusion problem (unlike register automata), and (iv)~enjoy logical characterizations. Using these results, we establish a learning algorithm to infer session automata through membership and equivalence queries.} }

@article{HSS-lmcs14, journal = {Logical Methods in Computer Science}, author = {Haase, Christoph and Schmitz, Sylvain and Schnoebelen, {\relax Ph}ilippe}, title = {The Power of Priority Channel Systems}, year = {2014}, month = dec, volume = 10, number = {4:4}, nopages = {}, url = {http://arxiv.org/abs/1301.5500}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HSS-lmcs14.pdf}, doi = {10.2168/LMCS-10(4:4)2014}, abstract = {We introduce Priority Channel Systems, a new class of channel systems where messages carry a numeric priority and where higher-priority messages can supersede lower-priority messages preceding them in the fifo communication buffers. The decidability of safety and inevitability properties is shown via the introduction of a priority embedding, a well-quasi-ordering that has not previously been used in well-structured systems. We then show how Priority Channel Systems can compute Fast-Growing functions and prove that the aforementioned verification problems are \(\mathbf{F}_{\epsilon_{0}}\)-complete.} }

@inproceedings{DSS-pods14, address = {Snowbird, Utah, USA}, month = jun, year = 2014, publisher = {ACM Press}, editor = {Hull, Richard and Grohe, Martin}, acronym = {{PODS}'14}, booktitle = {{P}roceedings of the 33rd {A}nnual {ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium on {P}rinciples of {D}atabase {S}ystems ({PODS}'14)}, author = {Durand, Arnaud and Schweikardt, Nicole and Segoufin, Luc}, title = {Enumerating answers to first-order queries over databases of low degree}, pages = {121-131}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DSS-pods14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DSS-pods14.pdf}, doi = {10.1145/2594538.2594539}, abstract = {A~class of relational databases has low degree if for all~\(\delta\), all but finitely many databases in the class have degree at most~\(n^{\delta}\), where \(n\) is the size of the database. Typical examples are databases of bounded degree or of degree bounded by \(\textrm{log} n\).\par It is known that over a class of databases having low degree, first-order boolean queries can be checked in pseudo-linear time, i.e. in time bounded by \(n^{1+\epsilon}\), for all~\(\epsilon\). We~generalise this result by considering query evaluation.\par We show that counting the number of answers to a query can be done in pseudo-linear time and that enumerating the answers to a query can be done with constant delay after a pseudo-linear time preprocessing.} }

@inproceedings{segoufin-stacs14, address = {Lyon, France}, month = mar, year = 2014, volume = 25, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Mayr, Ernst W. and Portier, Natacha}, acronym = {{STACS}'14}, booktitle = {{P}roceedings of the 31st {A}nnual {S}ymposium on {T}heoretical {A}spects of {C}omputer {S}cience ({STACS}'14)}, author = {Segoufin, Luc}, title = {A~glimpse on constant delay enumeration}, pages = {13-27}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/segoufin-stacs14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/segoufin-stacs14.pdf}, doi = {10.4230/LIPIcs.STACS.2014.13}, 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. This cannot be always achieved. It requires restricting either the class of queries or the class of databases. We describe here several scenarios when this is possible.} }

@inproceedings{ADV-icdt14, address = {Athens, Greece}, month = mar, year = 2014, editor = {Schweikardt, Nicole and Christophides, Vassilis and Leroy, Vincent}, acronym = {{ICDT}'14}, booktitle = {{P}roceedings of the 17th {I}nternational {C}onference on {D}atabase {T}heory ({ICDT}'14)}, author = {Abiteboul, Serge and Deutch, Daniel and Vianu, Victor}, title = {Deduction with Contradictions in Datalog}, pages = {143-154}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ADV-icdt14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ADV-icdt14.pdf}, doi = {10.5441/002/icdt.2014.17}, abstract = {We study deduction in the presence of inconsistencies. Following previous works, we capture deduction via datalog programs and inconsistencies through violations of functional dependencies (FDs). We study and compare two semantics for datalog with FDs: the first, of a logical nature, is based on inferring facts one at a time, while never violating the FDs; the second, of an operational nature, consists in a fixpoint computation in which maximal sets of facts consistent with the FDs are inferred at each stage.\par Both semantics are nondeterministic, yielding sets of possible worlds. We introduce a PTIME (in the size of the extensional data) algorithm, that given a datalog program, a set of FDs and an input instance, produces a c-table representation of the set of possible worlds. Then, we propose to quantify nondeterminism with probabilities, by means of a probabilistic semantics. We consider the problem of capturing possible worlds along with their probabilities via probabilistic c-tables.\par We then study classical computational problems in this novel context. We consider the problems of computing the probabilities of answers, of identifying most likely supports for answers, and of determining the extensional facts that are most influential for deriving a particular fact. We show that the interplay of recursion and FDs leads to novel technical challenges in the context of these problems.} }

@inproceedings{JLMX-mfps30, address = {Ithaca, New~York, USA}, month = jun, year = 2014, volume = 308, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier Science Publishers}, editor = {Jacobs, Bart and Silva, Alexandra and Staton, Sam}, acronym = {{MFPS}'14}, booktitle = {{P}roceedings of the 30th {C}onference on {M}athematical {F}oundations of {P}rogramming {S}emantics ({MFPS}'14)}, author = {Jaziri, Samy and Larsen, Kim G. and Mardare, Radu and Xue, Bingtian}, title = {Adequacy and Complete Axiomatization for Timed Modal Logic}, pages = {183-210}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/JLMX-mfps14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JLMX-mfps14.pdf}, doi = {10.1016/j.entcs.2014.10.011}, abstract = {In this paper we develop the metatheory for Timed Modal Logic~(TML), which is the modal logic used for the analysis of timed transition systems~(TTSs). We solve a series of long-standing open problems related to~TML. Firstly, we prove that TML enjoys the Hennessy-Milner property and solve one of the open questions in the field. Secondly, we prove that the set of validities are not recursively enumerable. Nevertheless, we develop a strongly-complete proof system for~TML. Since the logic is not compact, the proof system contains infinitary rules, but only with countable sets of instances. Thus, we~can involve topological results regarding Stone spaces, such as the Rasiowa-Sikorski lemma, to complete the proofs.} }

@inproceedings{GLJ-mfps30, address = {Ithaca, New~York, USA}, month = jun, year = 2014, volume = 308, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier Science Publishers}, editor = {Jacobs, Bart and Silva, Alexandra and Staton, Sam}, acronym = {{MFPS}'14}, booktitle = {{P}roceedings of the 30th {C}onference on {M}athematical {F}oundations of {P}rogramming {S}emantics ({MFPS}'14)}, author = {Goubault{-}Larrecq, Jean and Jung, Achim}, title = {{QRB}, {QFS}, and the Probabilistic Powerdomain}, pages = {167-182}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/GLJ-mfps14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLJ-mfps14.pdf}, doi = {10.1016/j.entcs.2014.10.010}, abstract = {We show that the first author's QRB-domains coincide with Li and Xu's QFS-domains, and also with Lawson-compact quasi-continuous dcpos, with stably-compact locally finitary compact spaces, with sober QFS-spaces, and with sober QRB-spaces. The first three coincidences were discovered independently by Lawson and~Xi. The equivalence with sober QFS-spaces is then applied to give a novel, direct proof that the probabilistic powerdomain of a QRB-domain is a QRB-domain. This improves upon a previous, similar result, which was limited to pointed, second-countable QRB-domains.} }

@inproceedings{AG-fsttcs14, address = {New~Dehli, India}, month = dec, year = 2014, volume = {29}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Raman, Venkatesh and Suresh, S.~P.}, acronym = {{FSTTCS}'14}, booktitle = {{P}roceedings of the 34th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'14)}, author = {Aiswarya, C. and Gastin, Paul}, title = {Reasoning about distributed systems: {WYSIWYG}}, pages = {11-30}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AG-fsttcs14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AG-fsttcs14.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2014.11}, abstract = {There are two schools of thought on reasoning about distributed systems: one~following interleaving based semantics, and one following partial-order{{\slash}}graph based semantics. This paper compares these two approaches and argues in favour of the latter. An~introductory treatment of the split-width technique is also provided.} }

@article{BFHP-fi14, publisher = {{IOS} Press}, journal = {Fundamenta Informaticae}, author = {Bernardinello, Luca and Ferigato, Carlo and Haar, Stefan and Pomello, Lucia}, title = {Closed Sets in Occurrence Nets with Conflicts}, volume = 133, number = 4, year = 2014, pages = {323-344}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHP-fi14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHP-fi14.pdf}, doi = {10.3233/FI-2014-1079}, abstract = {The semantics of concurrent processes can be defined in terms of partially ordered sets. Occurrence nets, which belong to the family of Petri nets, model concurrent processes as partially ordered sets of occurrences of local states and local events. On the basis of the associated concurrency relation, a closure operator can be defined, giving rise to a lattice of closed sets. Extending previous results along this line, the present paper studies occurrence nets with forward conflicts, modelling families of processes. It is shown that the lattice of closed sets is orthomodular, and the relations between closed sets and some particular substructures of an occurrence net are studied. In particular, the paper deals with runs, modelling concurrent histories, and trails, corresponding to possible histories of sequential components. A~second closure operator is then defined by means of an iterative procedure. The~corresponding closed sets, here called 'dynamically closed', are shown to form a complete lattice, which in general is not orthocomplemented. Finally, it is shown that, if an occurrence net satisfies a property called B-density, which essentially says that any antichain meets any trail, then the two notions of closed set coincide, and they form a complete, algebraic orthomodular lattice.} }

@inproceedings{BHL-fsttcs14, address = {New~Dehli, India}, month = dec, year = 2014, volume = {29}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Raman, Venkatesh and Suresh, S.~P.}, acronym = {{FSTTCS}'14}, booktitle = {{P}roceedings of the 34th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'14)}, author = {Bertrand, Nathalie and Haddad, Serge and Lefaucheux, Engel}, title = {Foundation of Diagnosis and Predictability in Probabilistic Systems}, pages = {417-429}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHL-fsttcs14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHL-fsttcs14.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2014.417}, abstract = {In discrete event systems prone to unobservable faults, a diagnoser must eventually detect fault occurrences. The diagnosability problem consists in deciding whether such a diagnoser exists. Here we investigate diagnosis for probabilistic systems modelled by partially observed Markov chains also called probabilistic labeled transition systems (pLTS). First we study different specifications of diagnosability and establish their relations both in finite and infinite pLTS. Then we analyze the complexity of the diagnosability problem for finite pLTS: we show that the polynomial time procedure earlier proposed is erroneous and that in fact for all considered specifications, the problem is PSPACE-complete. We also establish tight bounds for the size of diagnosers. Afterwards we consider the dual notion of predictability which consists in predicting that in a safe run, a fault will eventually occur. Predictability is an easier problem than diagnosability: it is NLOGSPACE-complete. Yet the predictor synthesis is as hard as the diagnoser synthesis. Finally we introduce and study the more flexible notion of prediagnosability that generalizes predictability and diagnosability.} }

@inproceedings{BGK-fsttcs14, address = {New~Dehli, India}, month = dec, year = 2014, volume = {29}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Raman, Venkatesh and Suresh, S.~P.}, acronym = {{FSTTCS}'14}, booktitle = {{P}roceedings of the 34th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'14)}, author = {Bollig, Benedikt and Gastin, Paul and Kumar, Akshay}, title = {Parameterized Communicating Automata: Complementation and Model Checking}, pages = {625-637}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGK-fsttcs14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGK-fsttcs14.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2014.625}, abstract = {We study the language-theoretical aspects of parameterized communicating automata (PCAs), in which processes communicate via rendez-vous. A given PCA can be run on any topology of bounded degree such as pipelines, rings, ranked trees, and grids. We show that, under a context bound, which restricts the local behavior of each process, PCAs are effectively complementable. Complementability is considered a key aspect of robust automata models and can, in particular, be exploited for verification. In this paper, we use it to obtain a characterization of context-bounded PCAs in terms of monadic second-order (MSO) logic. As the emptiness problem for context-bounded PCAs is decidable for the classes of pipelines, rings, and trees, their model-checking problem wrt. MSO properties also becomes decidable. While previous work on model checking parameterized systems typically uses temporal logics without next operator, our MSO logic allows one to express several natural next modalities.} }

@inproceedings{CMS-fsttcs14, address = {New~Dehli, India}, month = dec, year = 2014, volume = {29}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Raman, Venkatesh and Suresh, S.~P.}, acronym = {{FSTTCS}'14}, booktitle = {{P}roceedings of the 34th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'14)}, author = {Chadha, Rohit and Mathur, Umang and Schwoon, Stefan}, title = {Computing Information Flow Using Symbolic Model-Checking}, pages = {505-516}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CMS-fsttcs14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CMS-fsttcs14.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2014.505}, abstract = {Several measures have been proposed in literature for quantifying the information leaked by the public outputs of a program with secret inputs. We consider the problem of computing information leaked by a deterministic or probabilistic program when the measure of information is based on (a)~min-entropy and (b)~Shannon entropy. The key challenge in computing these measures is that we need the total number of possible outputs and, for each possible output, the number of inputs that lead to it. A direct computation of these quantities is infeasible because of the state-explosion problem. We therefore propose symbolic algorithms based on binary decision diagrams (BDDs). The advantage of our approach is that these symbolic algorithms can be easily implemented in any BDD-based model-checking tool that checks for reachability in deterministic non-recursive programs by computing program summaries. We demonstrate the validity of our approach by implementing these algorithms in a tool Moped-QLeak, which is built upon Moped, a model checker for Boolean programs. Finally, we show how this symbolic approach extends to probabilistic programs.} }

@inproceedings{DFM-fsttcs14, address = {New~Dehli, India}, month = dec, year = 2014, volume = {29}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Raman, Venkatesh and Suresh, S.~P.}, acronym = {{FSTTCS}'14}, booktitle = {{P}roceedings of the 34th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'14)}, author = {David, Claire and Francis, Nadime and Murlak, Filip}, title = {Consistency of injective tree patterns}, pages = {279-290}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DFM-fsttcs14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DFM-fsttcs14.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2014.279}, abstract = {Testing if an incomplete description of an XML document is consistent, that is, if it describes a real document conforming to the imposed schema, amounts to deciding if a given tree pattern can be matched injectively into a tree accepted by a fixed automaton. This problem can be solved in polynomial time for patterns that use the child relation and the sibling order, but do not use the descendant relation. For general patterns the problem is in NP, but no lower bound has been known so far. We show that the problem is NP-complete already for patterns using only child and descendant relations. The source of hardness turns out to be the interplay between these relations: for patterns using only descendant we give a polynomial algorithm. We also show that the algorithm can be adapted to patterns using descendant and following-sibling, but combining descendant and next-sibling leads to intractability.} }

@inproceedings{DJLMS-fsttcs14, address = {New~Dehli, India}, month = dec, year = 2014, volume = {29}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Raman, Venkatesh and Suresh, S.~P.}, acronym = {{FSTTCS}'14}, booktitle = {{P}roceedings of the 34th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'14)}, author = {Doyen, Laurent and Juhl, Line and Larsen, Kim G. and Markey, Nicolas and Shirmohammadi, Mahsa}, title = {Synchronizing words for weighted and timed automata}, pages = {121-132}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DJLMS-fsttcs14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DJLMS-fsttcs14.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2014.121}, abstract = {The problem of synchronizing automata is concerned with the existence of a word that sends all states of the automaton to one and the same state. This problem has classically been studied for complete deterministic finite automata, with the existence problem being NLOGSPACE-complete.\par In this paper we consider synchronizing-word problems for weighted and timed automata. We consider the synchronization problem in several variants and combinations of these, including deterministic and non-deterministic timed and weighted automata, synchronization to unique location with possibly different clock valuations or accumulated weights, as well as synchronization with a safety condition forbidding the automaton to visit states outside a safety-set during synchronization (e.g. energy constraints). For deterministic weighted automata, the synchronization problem is proven PSPACE-complete under energy constraints, and in 3-EXPSPACE under general safety constraints. For timed automata the synchronization problems are shown to be PSPACE-complete in the deterministic case, and undecidable in the non-deterministic case.} }

@inproceedings{BMS-fsttcs14, address = {New~Dehli, India}, month = dec, year = 2014, volume = {29}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Raman, Venkatesh and Suresh, S.~P.}, acronym = {{FSTTCS}'14}, booktitle = {{P}roceedings of the 34th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'14)}, author = {Bouyer, Patricia and Markey, Nicolas and Stan, Daniel}, title = {Mixed {N}ash Equilibria in Concurrent Games}, pages = {351-363}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-fsttcs14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-fsttcs14.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2014.351}, abstract = {We study mixed-strategy Nash equilibria in multiplayer deterministic concurrent games played on graphs, with terminal-reward payoffs (that is, absorbing states with a value for each player). We show undecidability of the existence of a constrained Nash equilibrium (the constraint requiring that one player should have maximal payoff), with only three players and 0/1-rewards (i.e., reachability objectives). This has to be compared with the undecidability result by Ummels and Wojtczak for turn-based games which requires 14 players and general rewards. Our proof has various interesting consequences: (i)~the~undecidability of the existence of a Nash equilibrium with a constraint on the social welfare; (ii)~the~undecidability of the existence of an (unconstrained) Nash equilibrium in concurrent games with terminal-reward payoffs.} }

@article{BBBMBGJ-lmcs14, journal = {Logical Methods in Computer Science}, author = {Bertrand, Nathalie and Bouyer, Patricia and Brihaye, {\relax Th}omas and Menet, Quentin and Baier, Christel and Gr{\"o}{\ss}er, Marcus and Jurdzi{\'n}ski, Marcin}, title = {Stochastic Timed Automata}, volume = 10, number = {4:6}, nopages = {}, month = dec, year = 2014, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBBMBGJ-mfcs14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBBMBGJ-mfcs14.pdf}, doi = {10.2168/LMCS-10(4:6)2014}, abstract = {A~stochastic timed automaton is a purely stochastic process defined on a timed automaton, in which both delays and discrete choices are made randomly. We study the almost-sure model-checking problem for this model, that is, given a stochastic timed automaton~\(\mathcal{A}\) and a property~\(\varphi\), we want to decide whether \(\mathcal{A}\) satisfies~\(\varphi\) with probability~\(1\). In this paper, we identify several classes of automata and of properties for which this can be decided. The proof relies on the construction of a finite abstraction, called the thick graph, that we interpret as a finite Markov chain, and for which we can decide the almost-sure model-checking problem. Correctness of the abstraction holds when automata are almost-surely fair, which we show, is the case for two large classes of systems, single-clock automata and so-called weak-reactive automata. Techniques employed in this article gather tools from real-time verification and probabilistic verification, as well as topological games played on timed automata.} }

@article{BCGZ-jal14, publisher = {Elsevier Science Publishers}, journal = {Journal of Applied Logic}, author = {Bollig, Benedikt and Cyriac, Aiswarya and Gastin, Paul and Zeitoun, Marc}, title = {Temporal logics for concurrent recursive programs: Satisfiability and model checking}, volume = 12, number = 4, pages = {395-416}, month = dec, year = 2014, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGZ-jal14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGZ-jal14.pdf}, doi = {10.1016/j.jal.2014.05.001}, abstract = {We develop a general framework for the design of temporal logics for concurrent recursive programs. A program execution is modeled as a partial order with multiple nesting relations. To specify properties of executions, we consider any temporal logic whose modalities are definable in monadic second-order logic and which, in addition, allows PDL-like path expressions. This captures, in a unifying framework, a wide range of logics defined for ranked and unranked trees, nested words, and Mazurkiewicz traces that have been studied separately. We show that satisfiability and model checking are decidable in EXPTIME and 2EXPTIME, depending on the precise path modalities.} }

@proceedings{KHY-topnoc2014, editor = {Koutny, Maciej and Haddad, Serge and Yakovlev, Alex}, title = {Transactions on {P}etri Nets and Other Models of Concurrency~{IX}}, booktitle = {Transactions on {P}etri Nets and Other Models of Concurrency~{IX}}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = 8910, year = {2014}, noaddress = {}, url = {http://www.springer.com/978-3-662-45729-0} }

@incollection{topnoc14-CH, year = 2014, volume = {8910}, series = {Lecture Notes in Computer Science}, editor = {Koutny, Maciej and Haddad, Serge and Yakovlev, Alex}, publisher = {Springer}, booktitle = {Transactions on {P}etri Nets and Other Models of Concurrency~{IX}}, author = {Chatain, {\relax Th}omas and Haar, Stefan}, title = {A Canonical Contraction for Safe {P}etri Nets}, pages = {83-98}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/topnoc14-CH.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/topnoc14-CH.pdf}, doi = {10.1007/978-3-662-45730-6_5}, abstract = {Under maximal semantics, the occurrence of an event~\(a\) in a concurrent run of an occurrence net may imply the occurrence of other events, not causally related to~\(a\), in the same run. In recent works, we have formalized this phenomenon as the reveals relation, and used it to obtain a contraction of sets of events called facets in the context of occurrence nets. Here, we extend this idea to propose a canonical contraction of general safe Petri nets into pieces of partial-order behaviour which can be seen as {"}macro-transitions{"} since all their events must occur together in maximal semantics. On occurrence nets, our construction coincides with the facets abstraction. Our contraction preserves the maximal semantics in the sense that the maximal processes of the contracted net are in bijection with those of the original net.} }

@inproceedings{CHJPS-cmsb14, address = {Manchester, UK}, month = nov, year = 2014, volume = {8859}, series = {Lecture Notes in Bioinformatics}, publisher = {Springer-Verlag}, editor = {Mendes, Pedro}, acronym = {{CMSB}'14}, booktitle = {{P}roceedings of the 12th {C}onference on {C}omputational {M}ethods in {S}ystem {B}iology ({CMSB}'14)}, author = {Chatain, {\relax Th}omas and Haar, Stefan and Jezequel, Lo{\"\i}g and Paulev{\'e}, Lo{\"\i}c and Schwoon, Stefan}, title = {Characterization of Reachable Attractors Using {P}etri Net Unfoldings}, pages = {129-142}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CHJPS-cmsb14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CHJPS-cmsb14.pdf}, doi = {10.1007/978-3-319-12982-2_10}, abstract = {Attractors of network dynamics represent the long-term behaviours of the modelled system. Their characterization is therefore crucial for understanding the response and differentiation capabilities of a dynamical system. In the scope of qualitative models of interaction networks, the computation of attractors reachable from a given state of the network faces combinatorial issues due to the state space explosion. In this paper, we present a new algorithm that exploits the concurrency between transitions of parallel acting components in order to reduce the search space. The algorithm relies on Petri net unfoldings that can be used to compute a compact representation of the dynamics. We illustrate the applicability of the algorithm with Petri net models of cell signalling and regulation networks, Boolean and multi-valued. The proposed approach aims at being complementary to existing methods for deriving the attractors of Boolean models, while being generic since they apply to any safe Petri net.} }

@inproceedings{BHHP-simul14, address = {Nice, France}, month = oct, year = 2014, publisher = {XPS}, editor = {Arisha, Amr and Bobashev, Georgiy}, acronym = {{SIMUL}'14}, booktitle = {{P}roceedings of the 6th {I}nternational {C}onference on {A}dvances in {S}ystem {S}imulation ({SIMUL}'14)}, author = {Barbot, Beno{\^\i}t and Haddad, Serge and Heiner, Monika and Picaronny, Claudine}, title = {Rare Event Handling in Signalling Cascades}, pages = {126-131}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHHP-simul14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHHP-simul14.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{DDS-rp14, address = {Oxford, UK}, month = sep, year = 2014, volume = {8762}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Ouaknine, Jo{\"e}l and Potapov, Igor and Worrell, James}, acronym = {{RP}'14}, booktitle = {{P}roceedings of the 8th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'14)}, author = {Demri, St{\'e}phane and Dhar, Amit Kumar and Sangnier, Arnaud}, title = {Equivalence Between Model-Checking Flat Counter Systems and {P}resburger Arithmetic}, pages = {85-97}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-rp14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-rp14.pdf}, doi = {10.1007/978-3-319-11439-2_7}, abstract = {We show that model-checking flat counter systems over CTL\textsuperscript{*} (with arithmetical constraints on counter values) has the same complexity as the satisfiability problem for Presburger arithmetic. The lower bound already holds with the temporal operator EF only, no~arithmetical constraints in the logical language and with guards on transitions made of simple linear constraints. This complements our understanding of model-checking flat counter systems with linear-time temporal logics, such as LTL for which the problem is already known to be (only) NP-complete with guards restricted to the linear fragment.} }

@proceedings{DKW-ijcar2014, editor = {Demri, St{\'e}phane and Kapur, Deepak and Weidenbach, Christoph}, title = {{P}roceedings of the 7th {I}nternational {J}oint {C}onference on {A}utomated {R}easoning ({IJCAR}'14)}, booktitle = {{P}roceedings of the 7th {I}nternational {J}oint {C}onference on {A}utomated {R}easoning ({IJCAR}'14)}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = 8562, year = {2014}, month = jul, address = {Vienna, Austria}, url = {http://www.springer.com/978-3-319-08586-9} }

@article{CD-interstices14, publisher = {INRIA}, journal = {Interstices}, author = {Chr{\'e}tien, R{\'e}my and Delaune, St{\'e}phanie}, title = {Le~bitcoin, une monnaie \(100\%\) num{\'e}rique}, month = sep, year = {2014}, url = {https://interstices.info/jcms/ni_78681/le-bitcoin-une-monnaie-100-numerique}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-interstices14.pdf} }

@inproceedings{CDR-tgc14, address = {Rome, Italy}, month = dec, year = 2014, volume = {8902}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Maffei, Matteo and Tuosto, Emilio}, acronym = {{TGC}'14}, booktitle = {{R}evised {S}elected {P}apers of the 9th {S}ymposium on {T}rustworthy {G}lobal {C}omputing ({TGC}'14)}, author = {Cheval, Vincent and Delaune, St{\'e}phanie and Ryan, Mark D.}, title = {Tests for establishing security properties}, pages = {82-96}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDR-tgc14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDR-tgc14.pdf}, doi = {10.1007/978-3-662-45917-1_6}, abstract = {Ensuring strong security properties in some cases requires participants to carry out tests during the execution of a protocol. A~classical example is electronic voting: participants are required to verify the presence of their ballots on a bulletin board, and to verify the computation of the election outcome. The notion of certificate transparency is another example, in which participants in the protocol are required to perform tests to verify the integrity of a certificate log.\par We present a framework for modelling systems with such `testable properties', using the applied pi calculus. We model the tests that are made by participants in order to obtain the security properties. Underlying our work is an attacker model called {"}malicious but cautious{"}, which lies in between the Dolev-Yao model and the {"}honest but curious{"} model. The malicious-but-cautious model is appropriate for cloud computing providers that are potentially malicious but are assumed to be cautious about launching attacks that might cause user tests to fail.} }

@inproceedings{schmitz-rp14, address = {Oxford, UK}, month = sep, year = 2014, volume = {8762}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Ouaknine, Jo{\"e}l and Potapov, Igor and Worrell, James}, acronym = {{RP}'14}, booktitle = {{P}roceedings of the 8th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'14)}, author = {Schmitz, Sylvain}, title = {Complexity Bounds for Ordinal-Based Termination}, pages = {1-19}, url = {http://arxiv.org/abs/1407.5896}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/schmitz-rp14.pdf}, doi = {10.1007/978-3-319-11439-2_1}, abstract = {`What more than its truth do we know if we have a proof of a theorem in a given formal system?' We examine Kreisel's question in the particular context of program termination proofs, with an eye to deriving complexity bounds on program running times.\par Our main tool for this are length function theorems, which provide complexity bounds on the use of well quasi orders. We illustrate how to prove such theorems in the simple yet until now untreated case of ordinals. We show how to apply this new theorem to derive complexity bounds on programs when they are proven to terminate thanks to a ranking function into some ordinal.} }

@inproceedings{GLS-pp14, year = 2014, volume = 8464, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {van Breugel, Franck and Kashefi, Elham and Palamidessi, Catuscia and Rutten, Jan}, booktitle = {Horizons of the Mind. A~Tribute to Prakash Panangaden}, author = {Goubault{-}Larrecq, Jean and Segala, Roberto}, title = {Random Measurable Selections}, pages = {343-362}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/GLS-pp14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLS-pp14.pdf}, doi = {10.1007/978-3-319-06880-0_18}, abstract = {We make the first steps towards showing a general {"}randomness for free{"} theorem for stochastic automata. The goal of such theorems is to replace randomized schedulers by averages of pure schedulers. Here, we explore the case of measurable multifunctions and their measurable selections. This involves constructing probability measures on the measurable space of measurable selections of a given measurable multifunction, which seems to be a fairly novel problem. We then extend this to the case of IT automata, namely, non-deterministic (infinite) automata with a history-dependent transition relation. Throughout, we strive to make our assumptions minimal.} }

@inproceedings{BGS-rp14, address = {Oxford, UK}, month = sep, year = 2014, volume = {8762}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Ouaknine, Jo{\"e}l and Potapov, Igor and Worrell, James}, acronym = {{RP}'14}, booktitle = {{P}roceedings of the 8th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'14)}, author = {Bollig, Benedikt and Gastin, Paul and Schubert, Jana}, title = {Parameterized Verification of Communicating Automata under Context Bounds}, pages = {45-57}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGS-rp14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGS-rp14.pdf}, doi = {10.1007/978-3-319-11439-2_4}, abstract = {We study the verification problem for parameterized communicating automata~(PCA), in which processes synchronize via message passing. A~given PCA can be run on any topology of bounded degree (such as pipelines, rings, or ranked trees), and communication may take place between any two processes that are adjacent in the topology. Parameterized verification asks if there is a topology from a given topology class that allows for an accepting run of the given PCA. In general, this problem is undecidable even for synchronous communication and simple pipeline topologies. We therefore consider context-bounded verification, which restricts the behavior of each single process. For several variants of context bounds, we show that parameterized verification over pipelines, rings, and ranked trees is decidable. Our approach is automata-theoretic and uniform. We introduce a notion of graph acceptor that identifies those topologies allowing for an accepting run. Depending on the given topology class, the topology acceptor can then be restricted, or adjusted, so that the verification problem reduces to checking emptiness of finite automata or tree automata.} }

@inproceedings{HM-rp14, address = {Oxford, UK}, month = sep, year = 2014, volume = {8762}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Ouaknine, Jo{\"e}l and Potapov, Igor and Worrell, James}, acronym = {{RP}'14}, booktitle = {{P}roceedings of the 8th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'14)}, author = {Haddad, Serge and Monmege, Benjamin}, title = {Reachability in {MDP}s: Refining Convergence of Value Iteration}, pages = {125-137}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2014-07.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2014-07.pdf}, doi = {10.1007/978-3-319-11439-2_10}, abstract = {Markov Decision Processes (MDP) are a widely used model including both non-deterministic and probabilistic choices. Minimal and maximal probabilities to reach a target set of states, with respect to a policy resolving non-determinism, may be computed by several methods including value iteration. This algorithm, easy to implement and efficient in terms of space complexity, consists in iteratively finding the probabilities of paths of increasing length. However, it raises three issues: (1)~defining a stopping criterion ensuring a bound on the approximation, (2)~analyzing the rate of convergence, and (3)~specifying an additional procedure to obtain the exact values once a sufficient number of iterations has been performed. The first two issues are still open and for the third one a {"}crude{"} upper bound on the number of iterations has been proposed. Based on a graph analysis and transformation of MDPs, we address these problems. First we introduce an interval iteration algorithm, for which the stopping criterion is straightforward. Then we exhibit convergence rate. Finally we significantly improve the bound on the number of iterations required to get the exact values.} }

@inproceedings{LS-rp14, address = {Oxford, UK}, month = sep, year = 2014, volume = {8762}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Ouaknine, Jo{\"e}l and Potapov, Igor and Worrell, James}, acronym = {{RP}'14}, booktitle = {{P}roceedings of the 8th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'14)}, author = {Leroux, J{\'e}r{\^o}me and Schnoebelen, {\relax Ph}ilippe}, title = {On Functions Weakly Computable by {P}etri Nets and Vector Addition Systems}, pages = {190-202}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-rp14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-rp14.pdf}, doi = { 10.1007/978-3-319-11439-2_15}, abstract = {We show that any unbounded function weakly computable by a Petri net or a VASS cannot be sublinear. This answers a long-standing folklore conjecture about weakly computing the inverses of some fast-growing functions. The proof relies on a pumping lemma for sets of runs in Petri nets or VASSes.} }

@inproceedings{HH-rp14, address = {Oxford, UK}, month = sep, year = 2014, volume = {8762}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Ouaknine, Jo{\"e}l and Potapov, Igor and Worrell, James}, acronym = {{RP}'14}, booktitle = {{P}roceedings of the 8th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'14)}, author = {Haase, Christoph and Halfon, Simon}, title = {Integer Vector Addition Systems with States}, pages = {112-124}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/HH-rp14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HH-rp14.pdf}, doi = {10.1007/978-3-319-11439-2_9}, abstract = {This paper studies reachability, coverability and inclusion problems for Integer Vector Addition Systems with States (\(\mathbb{Z}\)-VASS) and extensions and restrictions thereof. A~\(\mathbb{Z}\)-VASS comprises a finite-state controller with a finite number of counters ranging over the integers. Although it is folklore that reachability in \(\mathbb{Z}\)-VASS is NP-complete, it turns out that despite their naturalness, from a complexity point of view this class has received little attention in the literature. We fill this gap by providing an in-depth analysis of the computational complexity of the aforementioned decision problems. Most interestingly, it turns out that while the addition of reset operations to ordinary VASS leads to undecidability and Ackermann-hardness of reachability and coverability, respectively, they can be added to \(\mathbb{Z}\)-VASS while retaining NP-completeness of both coverability and reachability.} }

@article{PHL-stvr14, publisher = {John Wiley \& Sons, Ltd.}, journal = {Software Testing, Verification and Reliability}, author = {Ponce{ }de{~}Le{\'o}n, Hern{\'a}n and Haar, Stefan and Longuet, Delphine}, title = {Model-Based Testing for Concurrent Systems with Labeled Event Structures}, volume = 24, number = 7, year = {2014}, month = nov, pages = {558-590}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-stvr14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-stvr14.pdf}, doi = {10.1002/stvr.1543}, abstract = {We propose a theoretical testing framework and a test generation algorithm for concurrent systems specified with true concurrency models, such as Petri nets or networks of automata. The semantic model of computation of such formalisms are labeled event structures, which allow to represent concurrency explicitly. We introduce the notions of strong and weak concurrency: strongly concurrent events must be concurrent in the implementation, while weakly concurrent ones may eventually be ordered. The ioco type conformance relations for sequential systems rely on the observation of sequences of actions and blockings, thus they are not capable of capturing and exploiting concurrency of non sequential behaviors. We propose an extension of \textbf{ioco} for labeled event structures, named \textbf{co-ioco}, allowing to deal with strong and weak concurrency. We~extend the notions of test cases and test execution to labeled event structures, and give a test generation algorithm building a complete test suite for \textbf{co-ioco}.} }

@inproceedings{BMP-dx14, address = {Graz, Austria}, month = sep, year = 2014, editor = {Abreu, Rui and Pill, Ingo and Wotawa, Franz}, acronym = {{DX}'14}, booktitle = {{P}roceedings of the 25th {I}nternational {W}orkshop on {P}rinciples of {D}iagnosis ({DX}'14)}, author = {Brand{\'a}n{ }Briones, Laura and Madalinski, Agnes and Ponce{ }de{~}Le{\'o}n, Hern{\'a}n}, title = {Distributed Diagnosability Analysis with {P}etri Nets}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMP-dx14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMP-dx14.pdf}, abstract = {We propose a framework to distributed diagnosability analysis of concurrent systems modeled with Petri nets as a collection of components synchronizing on common observable transitions, where faults can occur in several components. The diagnosability analysis of the entire system is done in parallel by verifying the interaction of each component with the fault free versions of the other components. Furthermore, we use existing efficient methods and tools, in particular parallel LTL-X model checking based on unfoldings, for diagnosability verification.} }

@article{EM-integers14, journal = {INTEGERS -- Electronic Journal of Combinatorial Number Theory}, author = {Elias, Yara and McKenzie, Pierre}, title = {On Generalized Addition Chains}, volume = 14, number = {A16}, nopages = {}, year = 2014, month = mar, url = {http://www.lsv.fr/Publis/PAPERS/PDF/EM-integers14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/EM-integers14.pdf}, abstract = {Given integers \(d \geq 1\), and \(g \geq 2\), a~\(g\)-addition chain for~\(d\) is a sequence of integers \(a_0 = 1\), \(a_1\), \(a_2\), ... , \(a_{r-1}\), \(a_r = d\) where \(a_i = a_{j_{1}} + a_{j_{2}} + \cdots + a_{j_{k}}\), with \(2 \leq k \leq g\), and \(0 \leq j_1 \leq j_2 \cdots j_k \leq i-1\). The length of a \(g\)-addition chain is~\(r\), the number of terms following~\(1\) in the sequence. We denote by~\(l_{g}(d)\) the length of a shortest addition chain for~\(d\). Many results have been established in the case \(g = 2\). Our aim is to establish the same sort of results for arbitrary fixed~\(g\). In~particular, we adapt methods for constructing \(g\)-addition chains when \(g = 2\) to the case \(g > 2\) and we study the asymptotic behavior of~\(l_g\).} }

@inproceedings{CKM-ncma14, address = {Kassel, Germany}, month = jul, year = 2014, volume = 304, series = {books@ocg.at}, publisher = {Austrian Computer Society}, editor = {Bensch, Suna and Freund, Rudolf and Otto, Friedrich}, acronym = {{NCMA}'14}, booktitle = {{P}roceedings of the 6th {W}orkshop on {N}on-{C}lassical {M}odels of {A}utomata and {A}pplications ({NCMA}'14)}, author = {Cadilhac, Micha{\"e}l and Krebs, Andreas and McKenzie, Pierre}, title = {Extremely uniform branching programs}, pages = {73-83}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CKM-ncma14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CKM-ncma14.pdf}, abstract = {We propose a new descriptive complexity notion of uniformity for branching programs solving problems defined on structured data. We observe that FO[=]-uniform (\(n\)-way) branching programs are unable to solve the tree evaluation problem studied by Cook, McKenzie, Wehr, Braverman and Santhanam because such programs possess a variant of their thriftiness property. Similarly, FO[=]-uniform (\(n\)-way) branching programs are unable to solve the P-complete GEN problem because such programs possess the incremental property studied by G{\'a}l, Kouck{\'y} and McKenzie.} }

@inproceedings{AGN-atva14, address = {Sydney, Australia}, month = nov, year = {2014}, volume = 8837, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Cassez, Franck and Raskin, Jean-Fran{\c{c}}ois}, acronym = {{ATVA}'14}, booktitle = {{P}roceedings of the 12th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'14)}, author = {Aiswarya, C. and Gastin, Paul and Narayan Kumar, K.}, title = {Verifying Communicating Multi-pushdown Systems via Split-width}, pages = {1-17}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AGN-atva14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGN-atva14.pdf}, doi = {10.1007/978-3-319-11936-6_1}, abstract = {Communicating multi-pushdown systems model networks of multi-threaded recursive programs communicating via reliable FIFO channels. We extend the notion of split-width to this setting, improving and simplifying the earlier definition. Split-width, while having the same power of clique-{{\slash}}tree-width, gives a divide-and-conquer technique to prove the bound of a class, thanks to the two basic operations, shuffle and merge, of the split-width algebra. We illustrate this technique on examples. We also obtain simple, uniform and optimal decision procedures for various verification problems parametrised by split-width.} }

@article{FKS-fmsd14, publisher = {Springer}, journal = {Formal Methods in System Design}, author = {Fribourg, Laurent and K{\"u}hne, Ulrich and Soulat, Romain}, title = {Finite Controlled Invariants for Sampled Switched Systems}, year = 2014, month = dec, volume = 45, number = 3, pages = {303-329}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FKS-fmsd14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FKS-fmsd14.pdf}, doi = {10.1007/s10703-014-0211-2}, abstract = {We consider in this paper switched systems, a class of hybrid systems recently used with success in various domains such as automotive industry and power electronics. We propose a state-dependent control strategy which makes the trajectories of the analyzed system converge to finite cyclic sequences of points. Our method relies on a technique of decomposition of the state space into local regions where the control is uniform. We have implemented the procedure using zonotopes, and applied it successfully to several examples of the literature and industrial case studies in power electronics.} }

@inproceedings{SLAF-syncop14, address = {Grenoble, France}, volume = 145, series = {Electronic Proceedings in Theoretical Computer Science}, month = apr, year = 2014, editor = {Andr{\'e}, {\'E}tienne and Frehse, Goran}, acronym = {{SYNCOP}'14}, booktitle = {{P}roceedings of the 1st {I}nternational {W}orkshop on {S}ynthesis of {C}ontinuous {P}arameters ({SYNCOP}'14)}, author = {Sun, Youcheng and Lipari, Giuseppe and Andr{\'e}, {\'E}tienne and Fribourg, Laurent}, title = {Toward Parametric Timed Interfaces for Real-Time Components}, pages = {49-64}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/SLAF-syncop14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SLAF-syncop14.pdf}, doi = {10.4204/EPTCS.145.6}, abstract = {We propose here a framework to model real-time components consisting of concurrent real-time tasks running on a single processor, using parametric timed automata. Our framework is generic and modular, so as to be easily adapted to different schedulers and more complex task models. We first perform a parametric schedulability analysis of the components using the inverse method. We show that the method unfortunately does not provide satisfactory results when the task periods are considered as parameters. After identifying and explaining the problem, we present a solution adapting the model by making use of the worst-case scenario in schedulability analysis. We show that the analysis with the inverse method always converges on the modified model when the system load is strictly less than~\(100\%\). Finally, we show how to use our parametric analysis for the generation of timed interfaces in compositional system design.} }

@inproceedings{BGM-atva14, address = {Sydney, Australia}, month = nov, year = {2014}, volume = 8837, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Cassez, Franck and Raskin, Jean-Fran{\c{c}}ois}, acronym = {{ATVA}'14}, booktitle = {{P}roceedings of the 12th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'14)}, author = {Bouyer, Patricia and Gardy, Patrick and Markey, Nicolas}, title = {Quantitative verification of weighted {K}ripke structures}, pages = {64-80}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-atva14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-atva14.pdf}, doi = {10.1007/978-3-319-11936-6_6}, abstract = {Extending formal verification techniques to handle quantitative aspects, both for the models and for the properties to be checked, has become a central research topic over the last twenty years. Following several recent works, we study model checking for (one-dimensional) weighted Kripke structures with positive and negative weights, and temporal logics constraining the total and/or average weight. We prove decidability when only accumulated weight is constrained, while allowing average-weight constraints alone already is undecidable.} }

@inproceedings{MV-atva14, address = {Sydney, Australia}, month = nov, year = {2014}, volume = 8837, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Cassez, Franck and Raskin, Jean-Fran{\c{c}}ois}, acronym = {{ATVA}'14}, booktitle = {{P}roceedings of the 12th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'14)}, author = {Markey, Nicolas and Vester, Steen}, title = {Symmetry Reduction in Infinite Games with Finite Branching}, pages = {281-296}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/MV-atva14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/MV-atva14.pdf}, doi = {10.1007/978-3-319-11936-6_21}, abstract = {Symmetry reductions have been applied extensively for the verification of finite-state concurrent systems and hardware designs using model-checking of temporal logics such as LTL, CTL and CTL\textsuperscript{*}, as well as real-time and probabilistic-system model-checking. In this paper we extend the technique to handle infinite-state games on graphs with finite branching where the objectives of the players can be very general. As particular applications, it is shown that the technique can be applied to reduce the state space in parity games as well as when doing model-checking of the temporal logic ATL\textsuperscript{*}.} }

@article{ADK-lmcs14, journal = {Logical Methods in Computer Science}, author = {Arapinis, Myrto and Delaune, St{\'e}phanie and Kremer, Steve}, title = {Dynamic Tags for Security Protocols}, volume = 10, number = {2:11}, nopages = {}, month = jun, year = 2014, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ADK-lmcs14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ADK-lmcs14.pdf}, doi = {10.2168/LMCS-10(2:11)2014}, abstract = {The design and verification of cryptographic protocols is a notoriously difficult task, even in symbolic models which take an abstract view of cryptography. This is mainly due to the fact that protocols may interact with an arbitrary attacker which yields a verification problem that has several sources of unboundedness (size of messages, number of sessions, etc. In this paper, we characterize a class of protocols for which deciding security for an unbounded number of sessions is decidable. More precisely, we present a simple transformation which maps a protocol that is secure for a bounded number of protocol sessions (a~decidable problem) to a protocol that is secure for an unbounded number of sessions. The precise number of sessions that need to be considered is a function of the security property and we show that for several classical security properties a single session is sufficient. Therefore, in many cases our results yields a design strategy for security protocols: (i)~design a protocol intended to be secure for a {single session}; and (ii)~apply our transformation to obtain a protocol which is secure for an unbounded number of sessions.} }

@article{FL-is14, publisher = {Springer}, journal = {Informatik Spektrum}, author = {Finkel, Alain and Leroux, J{\'e}r{\^o}me}, title = {Neue, einfache {A}lgorithmen f{\"u}r {P}etrinetze}, volume = 37, number = {3}, month = jun, year = 2014, pages = {229-236}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FL-is14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FL-is14.pdf}, doi = {10.1007/s00287-013-0753-5}, abstract = {Wir zeigen, wie die Entscheidungsprobleme der {\"U}berdeckung, der Beschr{\"a}nktheit und der Erreichbarkeit mithilfe induktiver Invarianten einfacher l{\"o}sbar sind als mit herk{\"o}mmlichen Methoden} }

@article{CD-tocl14, publisher = {ACM Press}, journal = {ACM Transactions on Computational Logic}, author = {Chatterjee, Krishnendu and Doyen, Laurent}, title = {Partial-Observation Stochastic Games: How to Win when Belief Fails}, volume = 15, number = {2:16}, month = apr, year = 2014, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-tocl14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-tocl14.pdf}, doi = {10.1145/2579819}, abstract = {In two-player finite-state stochastic games of partial observation on graphs, in every state of the graph, the players simultaneously choose an action, and their joint actions determine a probability distribution over the successor states. The game is played for infinitely many rounds and thus the players construct an infinite path in the graph. We consider reachability objectives where the first player tries to ensure a target state to be visited almost-surely (i.e., with probability~1) or positively (i.e., with positive probability), no matter the strategy of the second player.\par We classify such games according to the information and to the power of randomization available to the players. On the basis of information, the game can be one-sided with either (a)~player~1, or (b)~player 2 having partial observation (and the other player has perfect observation), or two-sided with (c)~both players having partial observation. On the basis of randomization, (a)~the players may not be allowed to use randomization (pure strategies), or (b)~they may choose a probability distribution over actions but the actual random choice is external and not visible to the player (actions invisible), or (c)~they may use full randomization.\par Our main results for pure strategies are as follows: (1)~For one-sided games with player~2 having perfect observation we show that (in contrast to full randomized strategies) belief-based (subset-construction based) strategies are not sufficient, and we present an exponential upper bound on memory both for almost-sure and positive winning strategies; we show that the problem of deciding the existence of almost-sure and positive winning strategies for player~1 is EXPTIME-complete and present symbolic algorithms that avoid the explicit exponential construction. (2)~For one-sided games with player~1 having perfect observation we show that non-elementary memory is both necessary and sufficient for both almost-sure and positive win- ning strategies. (3)~We~show that for the general (two-sided) case finite-memory strategies are sufficient for both positive and almost-sure winning, and at least non-elementary memory is required. We establish the equivalence of the almost-sure winning problems for pure strategies and for randomized strategies with actions invisible. Our equivalence result exhibit serious flaws in previous results of the literature: we show a non-elementary memory lower bound for almost-sure winning whereas an exponential upper bound was previously claimed.} }

@inproceedings{CS-mfcs14, address = {Budapest, Hungary}, month = aug, year = 2014, volume = {8634}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {{\'E}sik, Zolt{\'a}n and Csuhaj{-}Varj{\'u}, Erzs{\'e}bet and Dietzfelbinger, Martin}, acronym = {{MFCS}'14}, booktitle = {{P}roceedings of the 39th {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'14)~-- {P}art~{I}}, author = {Courtois, Jean-Baptiste and Schmitz, Sylvain}, title = {Alternating Vector Addition Systems with States}, pages = {220-231}, url = {http://hal.inria.fr/hal-00980878}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-mfcs14.pdf}, doi = {10.1007/978-3-662-44522-8_19}, abstract = {Alternating vector addition systems are obtained by equipping vector addition systems with states (VASS) with 'fork' rules, and provide a natural setting for infinite-arena games played over a VASS. Initially introduced in the study of propositional linear logic, they have more recently gathered attention in the guise of \emph{multi-dimensional energy} games for quantitative verification and synthesis.\par We show that establishing who is the winner in such a game with a state reachability objective is 2-ExpTime-complete. As a further application, we show that the same complexity result applies to the problem of whether a VASS is simulated by a finite-state system.} }

@inproceedings{CGK-concur14, address = {Rome, Italy}, month = sep, year = 2014, volume = 8704, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Baldan, Paolo and Gorla, Daniele}, acronym = {{CONCUR}'14}, booktitle = {{P}roceedings of the 25th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'14)}, author = {Cyriac, Aiswarya and Gastin, Paul and Narayan Kumar, K.}, title = {Controllers for the Verification of Communicating Multi-Pushdown Systems}, pages = {297-311}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CGK-concur14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CGK-concur14.pdf}, doi = {10.1007/978-3-662-44584-6_21}, abstract = {Multi-pushdowns communicating via queues are formal models of multi-threaded programs communicating via channels. They are turing powerful and much of the work on their verification has focussed on under-approximation techniques. Any error detected in the under-approximation implies an error in the system. However the successful verification of the under-approximation is not as useful if the system exhibits unverified behaviours. Our aim is to design controllers that observe/restrict the system so that it stays within the verified under-approximation. We identify some important properties that a good controller should satisfy. We consider an extensive under-approximation class, construct a distributed controller with the desired properties and also establish the decidability of verification problems for this class.} }

@inproceedings{CCD-concur14, address = {Rome, Italy}, month = sep, year = 2014, volume = 8704, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Baldan, Paolo and Gorla, Daniele}, acronym = {{CONCUR}'14}, booktitle = {{P}roceedings of the 25th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'14)}, author = {Chr{\'e}tien, R{\'e}my and Cortier, V{\'e}ronique and Delaune, St{\'e}phanie}, title = {Typing messages for free in security protocols: the~case of equivalence properties}, pages = {372-386}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-concur14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-concur14.pdf}, doi = {10.1007/978-3-662-44584-6_26}, abstract = {Privacy properties such as untraceability, vote secrecy, or anonymity are typically expressed as behavioural equivalence in a process algebra that models security protocols. In this paper, we study how to decide one particular relation, namely trace equivalence, for an unbounded number of sessions.\par Our first main contribution is to reduce the search space for attacks. Specifically, we show that if there is an attack then there is one that is well-typed. Our result holds for a large class of typing systems and a large class of determinate security protocols. Assuming finitely many nonces and keys, we can derive from this result that trace equivalence is decidable for an unbounded number of sessions for a class of tagged protocols, yielding one of the first decidability results for the unbounded case. As an intermediate result, we also provide a novel decision procedure in the case of a bounded number of sessions.} }

@inproceedings{DMS-concur14, address = {Rome, Italy}, month = sep, year = 2014, volume = 8704, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Baldan, Paolo and Gorla, Daniele}, acronym = {{CONCUR}'14}, booktitle = {{P}roceedings of the 25th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'14)}, author = {Doyen, Laurent and Massart, {\relax Th}ierry and Shirmohammadi, Mahsa}, title = {Robust Synchronization in {M}arkov Decision Processes}, pages = {234-248}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DMS-concur14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DMS-concur14.pdf}, doi = {10.1007/978-3-662-44584-6_17}, abstract = {We consider synchronizing properties of Markov decision processes (MDP), viewed as generators of sequences of probability distributions over states. A~probability distribution is \(p\)-synchronizing if the probability mass is at least~\(p\) in some state, and a sequence of probability distributions is weakly \(p\)-synchronizing, or strongly \(p\)-synchronizing if respectively infinitely many, or all but finitely many distributions in the sequence are \(p\)-synchronizing.\par For each synchronizing mode, an MDP can be \textit{(i)}~sure winning if there is a strategy that produces a \(1\)-synchronizing sequence; \textit{(ii)}~almost-sure winning if there is a strategy that produces a sequence that is, for all \(\epsilon>0\), a \((1-\epsilon)\)-synchronizing sequence; \textit{(iii)}~limit-sure winning if for all \(\epsilon>0\), there is a strategy that produces a \((1-\epsilon)\)-synchronizing sequence.\par For each synchronizing and winning mode, we consider the problem of deciding whether an MDP is winning, and we establish matching upper and lower complexity bounds of the problems, as well as the optimal memory requirement for winning strategies: \textit{(a)}~for all winning modes, we show that the problems are PSPACE-complete for weakly synchronizing, and PTIME-complete for strongly synchronizing; \textit{(b)}~we~show that for weakly synchronizing, exponential memory is sufficient and may be necessary for sure winning, and infinite memory is necessary for almost-sure winning; for strongly synchronizing, linear-size memory is sufficient and may be necessary in all modes; \textit{(c)}~we~show a robustness result that the almost-sure and limit-sure winning modes coincide for both weakly and strongly synchronizing.} }

@inproceedings{BMM-concur14, address = {Rome, Italy}, month = sep, year = 2014, volume = 8704, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Baldan, Paolo and Gorla, Daniele}, acronym = {{CONCUR}'14}, booktitle = {{P}roceedings of the 25th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'14)}, author = {Bouyer, Patricia and Markey, Nicolas and Matteplackel, Raj~Mohan}, title = {Averaging in~{LTL}}, pages = {266-280}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMM-concur14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMM-concur14.pdf}, doi = {10.1007/978-3-662-44584-6_19}, abstract = {For the accurate analysis of computerized systems, powerful quantitative formalisms have been designed, together with efficient verification algorithms. However, verification has mostly remained boolean---either a property is~true, or it~is false. We~believe that this is too crude in a context where quantitative information and constraints are crucial: correctness should be quantified!\par In a recent line of works, several authors have proposed quantitative semantics for temporal logics, using e.g. \emph{discounting} modalities (which give less importance to distant events). In~the present paper, we define and study a quantitative semantics of~LTL with \emph{averaging} modalities, either on the long run or within an until modality. This, in a way, relaxes the classical Boolean semantics of~LTL, and provides a measure of certain properties of a model. We~prove that computing and even approximating the value of a formula in this logic is undecidable.} }

@inproceedings{PHL-ictac14, address = {Bucharest, Romania}, month = sep, year = 2014, volume = 8687, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Ciobanu, Gabriel and M{\'e}ry, Dominique}, acronym = {{ICTAC}'14}, booktitle = {{P}roceedings of the 11th {I}nternational {C}olloquium on {T}heoretical {A}spects of {C}omputing ({ICTAC}'14)}, author = {Ponce{ }de{~}Le{\'o}n, Hern{\'a}n and Haar, Stefan and Longuet, Delphine}, title = {Distributed testing of concurrent systems: vector clocks to the rescue}, pages = {369-387}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-ictac14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-ictac14.pdf}, doi = {10.1007/978-3-319-10882-7_22}, abstract = {The ioco relation has become a standard in model-based conformance testing. The co-ioco conformance relation is an extension of this relation to concurrent systems specified with true-concurrency models. This relation assumes a global control and observation of the system under test, which is not usually realistic in the case of physically distributed systems. Such systems can be partially observed at each of their points of control and observation by the sequences of inputs and outputs exchanged with their environment. Unfortunately, in general, global observation cannot be reconstructed from local ones, so global conformance cannot be decided with local tests. We propose to append time stamps to the observable actions of the system under test in order to regain global conformance from local testing.} }

@inproceedings{KS-dcfs2014, address = {Turku, Finland}, month = aug, year = 2014, volume = {8614}, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, editor = {J{\"u}rgensen, Helmut and Karhum{\"a}ki, Juhani and Okhotin, Alexander}, acronym = {{DCFS}'14}, booktitle = {{P}roceedings of the 16th {W}orkshop on {D}escriptional {C}omplexity of {F}ormal {S}ystems ({DCFS}'14)}, author = {Karandikar, Prateek and Schnoebelen, {\relax Ph}ilippe}, title = {On the state complexity of closures and interiors of regular languages with subwords}, pages = {234-245}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-dcfs2014.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-dcfs2014.pdf}, doi = {10.1007/978-3-319-09704-6_21}, abstract = {We study the state complexity of the set of subwords and superwords of regular languages, and provide new lower bounds in the case of languages over a two-letter alphabet. We also consider the dual interior sets, for which the nondeterministic state complexity has a doubly-exponential upper bound. We prove a matching doubly-exponential lower bound for downward interiors in the case of an unbounded alphabet.} }

@inproceedings{KH-acsd14, address = {Tunis, Tunisia}, month = jun, year = 2014, publisher = {{IEEE} Computer Society Press}, acronym = {{ACSD}'14}, booktitle = {{P}roceedings of the 14th {I}nternational {C}onference on {A}pplication of {C}oncurrency to {S}ystem {D}esign ({ACSD}'14)}, author = {Kordon, Fabrice and Hulin{-}Hubard, Francis}, title = {BenchKit, a Tool for Massive Concurrent Benchmarking}, pages = {159-165}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/KH-acsd14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KH-acsd14.pdf}, doi = {10.1109/ACSD.2014.12}, abstract = {Benchmarking numerous programs in a reasonable time requires the use of several (potentially multicore) computers. We experimented such a situation in the context of the MCC (Model Checking Contest @ Petri net) where we had to operate more than 52000 runs for the 2013 edition. This paper presents BenchKit, a tool to operate programs on sets of potentially parallel machines and to gather monitoring information like CPU or memory usage. It also samples such data over the execution time. BenchKit has been elaborated in the context of the MCC and will be used for the 2014 edition.} }

@inproceedings{GHKS-acsd14, address = {Tunis, Tunisia}, month = jun, year = 2014, publisher = {{IEEE} Computer Society Press}, acronym = {{ACSD}'14}, booktitle = {{P}roceedings of the 14th {I}nternational {C}onference on {A}pplication of {C}oncurrency to {S}ystem {D}esign ({ACSD}'14)}, author = {Germanos, Vasileios and Haar, Stefan and Khomenko, Victor and Schwoon, Stefan}, title = {Diagnosability under Weak Fairness}, pages = {132-141}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/GHKS-acsd14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GHKS-acsd14.pdf}, doi = {10.1109/ACSD.2014.9}, 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{SLSFM-rtcsa14, address = {Chongqing, China}, month = aug, year = 2014, publisher = {{IEEE} Computer Society Press}, acronym = {{RTCSA}'14}, booktitle = {{P}roceedings of the 20th {IEEE} {I}nternational {C}onference on {E}mbedded and {R}eal-{T}ime {C}omputing {S}ystems and {A}pplications ({RTCSA}'14)}, author = {Sun, Youcheng and Lipari, Giuseppe and Soulat, Romain and Fribourg, Laurent and Markey, Nicolas}, title = {Component-Based Analysis of Hierarchical Scheduling using Linear Hybrid Automata}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/SLSFM-rtcsa14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SLSFM-rtcsa14.pdf}, doi = {10.1109/RTCSA.2014.6910502}, abstract = {Formal methods (e.g. Timed Automata or Linear Hybrid Automata) can be used to analyse a real-time system by performing a reachability analysis on the model. The advantage of using formal methods is that they are more expressive than classical analytic models used in schedulability analysis. For example, it is possible to express state-dependent behaviour, arbitrary activation patterns,~etc.\par In this paper we use the formalism of Linear Hybrid Automata to encode a hierarchical scheduling system. In particular, we model a dynamic server algorithm and the tasks contained within, abstracting away the rest of the system, thus enabling component-based scheduling analysis. We prove the correctness of the model and the decidability of the reachability analysis for the case of periodic tasks. Then, we compare the results of our model against classical schedulability analysis techniques, showing that our analysis performs better than analytic methods in terms of resource utilisation. We further present two case studies: a~component with state-dependent tasks, and a simplified model of a real avionics system. Finally, through extensive tests with various configurations, we demonstrate that this approach is usable for medium size components.} }

@article{BFSP-tcs14, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {Bouchy, Florent and Finkel, Alain and San{ }Pietro, Pierluigi}, title = {Dense-choice Counter Machines Revisited}, volume = {542}, month = jul, year = 2014, pages = {17-31}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFSP-tcs14.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFSP-tcs14.pdf}, doi = {10.1016/j.tcs.2014.04.029}, abstract = {This paper clarifies the picture about Dense-choice Counter Machines (DCM), a less studied version of Counter Machines where counters range on a dense, rather than discrete, domain. The definition of DCM is revisited to make it extend (discrete) Counter Machines, and new undecidability and decidability results are proved. Using the first-order additive mixed theory of reals and integers, the paper presents a logical characterization of the sets of configurations reachable by reversal-bounded DCM. We also relate the DCM model to more common models of systems.} }

@techreport{rr-lsv-14-06, author = {Sun, Youcheng and Lipari, Giuseppe}, title = {A Weak Simulation Relation for Real-Time Schedulability Analysis of Global Fixed Priority Scheduling Using Linear Hybrid Automata}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2014}, month = apr, type = {Research Report}, number = {LSV-14-06}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2014-06.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2014-06.pdf}, versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2014-06-v1.pdf, 20140428}, note = {17~pages}, abstract = {In this paper we present an exact schedulability test for sporadic real-time tasks scheduled by the Global Fixed Priority Fully Preemptive Scheduler on a multiprocessor system. The analysis consists in modelling the system as a Linear Hybrid Automaton, and in performing a reachability analysis for states representing deadline miss conditions. To mitigate the problem of state space explosion, we propose a partial order relationship over the symbolic states of the model and we prove that this is a weak simulation relation. We then present an implementation of the analysis in a software tool, and we show that the use of the proposed model permits to analyse larger systems than other exact algorithms in the literature.} }

@inproceedings{CD-icalp14, address = {Copenhagen, Denmark}, month = jul, year = 2014, volume = 8573, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Esparza, Javier and Fraigniaud, Pierre and Koutsoupias, Elias}, acronym = {{ICALP}'14}, booktitle = {{P}roceedings of the 41st {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'14)~-- {P}art~{II}}, author = {Chatterjee, Krishnendu and Doyen, Laurent}, title = {Games with a Weak Adversary}, pages = {110-121}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-icalp14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-icalp14.pdf}, doi = {10.1007/978-3-662-43951-7_10}, abstract = {We consider multi-player graph games with partial-observation and parity objective. While the decision problem for three-player games with a coalition of the first and second players against the third player is undecidable in general, we present a decidability result for partial-observation games where the first and third player are in a coalition against the second player, thus where the second player is adversarial but weaker due to partial-observation. We establish tight complexity bounds in the case where player~1 is less informed than player~2, namely 2-EXPTIME-completeness for parity objectives. The symmetric case of player~1 more informed than player~2 is much more complicated, and we show that already in the case where player~1 has perfect observation, memory of size non-elementary is necessary in general for reachability objectives, and the problem is decidable for safety and reachability objectives. Our results have tight connections with partial-observation stochastic games for which we derive new complexity results.} }

@inproceedings{BFM-icalp14, address = {Copenhagen, Denmark}, month = jul, year = 2014, volume = 8573, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Esparza, Javier and Fraigniaud, Pierre and Koutsoupias, Elias}, acronym = {{ICALP}'14}, booktitle = {{P}roceedings of the 41st {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'14)~-- {P}art~{II}}, author = {Blondin, Michael and Finkel, Alain and McKenzie, Pierre}, title = {Handling Infinitely Branching {WSTS}}, pages = {13-25}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFM-icalp14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFM-icalp14.pdf}, doi = {10.1007/978-3-662-43951-7_2}, abstract = {Most decidability results concerning well-structured transition systems apply to the \emph{finitely branching} variant. Yet some models (inserting automata, \(\omega\)-Petri nets,~...) are naturally infinitely branching. Here we develop tools to handle infinitely branching WSTS by exploiting the crucial property that in the (ideal) completion of a well-quasi-ordered set, downward-closed sets are finite unions of ideals. Then, using these tools, we derive decidability results and we delineate the undecidability frontier in the case of the termination, the control-state maintainability and the coverability problems. Coverability and boundedness under new effectivity conditions are shown decidable.} }

@inproceedings{DD-aiml14, address = {Groningen, The Netherlands}, month = aug, year = 2014, publisher = {College Publications}, editor = {Gor{\'e}, Rajeev and Kooi, Barteld P. and Kurucz, Agi}, acronym = {{AiML}'14}, booktitle = {{P}roceedings of the 10th {C}onference on {A}dvances in {M}odal {L}ogics ({AiML}'14)}, author = {Demri, St{\'e}phane and Deters, Morgan}, title = {The effects of modalities in separation logics (extended abstract)}, pages = {134-138}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-aiml14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-aiml14.pdf}, 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. We present similarities with modal and temporal logics, and we present landmark results about decidability, complexity and expressive power.} }

@inproceedings{DD-csllics14, address = {Vienna, Austria}, month = jul, year = 2014, publisher = {ACM Press}, acronym = {{CSL\slash LICS}'14}, booktitle = {{P}roceedings of the Joint Meeting of the 23rd {EACSL} {A}nnual {C}onference on {C}omputer {S}cience {L}ogic and the 29th {A}nnual {ACM\slash IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({CSL\slash LICS}'14)}, author = {Demri, St{\'e}phane and Deters, Morgan}, title = {Expressive Completeness of Separation Logic With Two Variables and No Separating Conjunction}, nopages = {}, chapter = {37}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-csllics14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-csllics14.pdf}, doi = {10.1145/2603088.2603142}, abstract = {We show that first-order separation logic with one record field restricted to two variables and the separating implication (no separating conjunction) is as expressive as weak second-order logic, substantially sharpening a previous result. Capturing weak second-order logic with such a restricted form of separation logic requires substantial updates to known proof techniques. We develop these, and as a by-product identify the smallest fragment of separation logic known to be undecidable: first-order separation logic with one record field, two variables, and no separating conjunction.} }

@inproceedings{BGMZ-csllics14, address = {Vienna, Austria}, month = jul, year = 2014, publisher = {ACM Press}, acronym = {{CSL\slash LICS}'14}, booktitle = {{P}roceedings of the Joint Meeting of the 23rd {EACSL} {A}nnual {C}onference on {C}omputer {S}cience {L}ogic and the 29th {A}nnual {ACM\slash IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({CSL\slash LICS}'14)}, author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin and Zeitoun, Marc}, title = {Logical Characterization of Weighted Pebble Walking Automata}, nopages = {}, chapter = 19, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-csllics14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-csllics14.pdf}, doi = {10.1145/2603088.2603118}, abstract = {Weighted automata are a conservative quantitative extension of finite automata that enjoys applications, e.g., in language processing and speech recognition. Their expressive power, however, appears to be limited, especially when they are applied to more general structures than words, such as graphs. To address this drawback, weighted automata have recently been generalized to weighted pebble walking automata, which proved useful as a tool for the specification and evaluation of quantitative properties over words and nested words. In this paper, we establish the expressive power of weighted pebble walking automata in terms of transitive closure logic, lifting a similar result by Engelfriet and Hoogeboom from the Boolean case to a quantitative setting. This result applies to general classes of graphs, including all the aforementioned classes.} }

@inproceedings{Haase-csllics14, address = {Vienna, Austria}, month = jul, year = 2014, publisher = {ACM Press}, acronym = {{CSL\slash LICS}'14}, booktitle = {{P}roceedings of the Joint Meeting of the 23rd {EACSL} {A}nnual {C}onference on {C}omputer {S}cience {L}ogic and the 29th {A}nnual {ACM\slash IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({CSL\slash LICS}'14)}, author = {Haase, Christoph}, title = {Subclasses of {P}resburger Arithmetic and the Weak {EXP} Hierarchy}, nopages = {}, chapter = 47, url = {http://arxiv.org/abs/1401.5266}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Haase-csllics14.pdf}, doi = {10.1145/2603088.2603092}, abstract = {It is shown that for any fixed \(i>0\), the \(\Sigma_{i+1}\)-fragment of Presburger arithmetic, i.e., its restriction to \(i+1\) quantifier alternations beginning with an existential quantifier, is complete for \(\Sigma^{\textsc{EXP}}_{i}\), the \(i\)-th level of the weak EXP hierarchy, an~analogue to the polynomial-time hierarchy residing between \textsc{NEXP} and \textsc{EXPSPACE}. This result completes the computational complexity landscape for Presburger arithmetic, a~line of research which dates back to the seminal work by Fischer~\& Rabin in~1974. Moreover, we~apply some of the techniques developed in the proof of the lower bound in order to establish bounds on sets of naturals definable in the \(\Sigma_1\)-fragment of Presburger arithmetic: given a \(\Sigma_1\)-formula \(\Phi(x)\), it~is shown that the set of non-negative solutions is an ultimately periodic set whose period is at most doubly-exponentially and that this bound is tight.} }

@inproceedings{BB-csllics14, address = {Vienna, Austria}, month = jul, year = 2014, publisher = {ACM Press}, acronym = {{CSL\slash LICS}'14}, booktitle = {{P}roceedings of the Joint Meeting of the 23rd {EACSL} {A}nnual {C}onference on {C}omputer {S}cience {L}ogic and the 29th {A}nnual {ACM\slash IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({CSL\slash LICS}'14)}, author = {Bollig, Benedikt}, title = {Logic for Communicating Automata with Parameterized Topology}, nopages = {}, chapter = 18, exturl = {http://hal.inria.fr/hal-00872807/}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BB-csllics14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BB-csllics14.pdf}, doi = {10.1145/2603088.2603093}, abstract = {We introduce parameterized communicating automata~(PCA) as a model of systems where finite-state processes communicate through FIFO channels. Unlike classical communicating automata, a given PCA can be run on any network topology of bounded degree. The topology is thus a parameter of the system. We provide various B{\"u}chi-Elgot-Trakhtenbrot theorems for~PCA, which roughly read as follows: Given a logical specification~\(\phi\) and a class of topologies~\(T\), there is a~PCA that is equivalent to~\(\phi\) on all topologies from~\(T\). We~give uniform constructions which allow us to instantiate~\(T\) with concrete classes such as pipelines, ranked trees, grids, rings,~etc. The proofs build on a locality theorem for first-order logic due to Schwentick and Barthelmann, and they exploit concepts from the non-parameterized case, notably a result by Genest, Kuske, and Muscholl.} }

@inproceedings{CDNV-fossacs14, address = {Grenoble, France}, month = apr, year = 2014, volume = {8412}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Muscholl, Anca}, acronym = {{FoSSaCS}'14}, booktitle = {{P}roceedings of the 17th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'14)}, author = {Chatterjee, Krishnendu and Doyen, Laurent and Nain, Sumit and Vardi, Moshe Y.}, title = {The Complexity of Partial-Observation Stochastic Parity Games with Finite-Memory Strategies}, pages = {242-257}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDNV-fossacs14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDNV-fossacs14.pdf}, doi = {10.1007/978-3-642-54830-7_16}, abstract = { We consider two-player partial-observation stochastic games on finite-state graphs where player~1 has partial observation and player~2 has perfect observation. The winning condition we study are \(\omega\)-regular conditions specified as parity objectives. The qualitative-analysis problem given a partial-observation stochastic game and a parity objective asks whether there is a strategy to ensure that the objective is satisfied with probability~1 (resp.~positive probability). These qualitative-analysis problems are known to be undecidable. However in many applications the relevant question is the existence of finite-memory strategies, and the qualitative-analysis problems under finite-memory strategies was recently shown to be decidable in 2EXPTIME. We improve the complexity and show that the qualitative-analysis problems for partial-observation stochastic parity games under finite-memory strategies are EXPTIME-complete; and also establish optimal (exponential) memory bounds for finite-memory strategies required for qualitative analysis. } }

@inproceedings{CDGO-fossacs14, address = {Grenoble, France}, month = apr, year = 2014, volume = {8412}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Muscholl, Anca}, acronym = {{FoSSaCS}'14}, booktitle = {{P}roceedings of the 17th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'14)}, author = {Chatterjee, Krishnendu and Doyen, Laurent and Gimbert, Hugo and Oualhadj, Youssouf}, title = {Perfect-Information Stochastic Mean-Payoff Parity Games}, pages = {210-225}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDGO-fossacs14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDGO-fossacs14.pdf}, doi = {10.1007/978-3-642-54830-7_4}, abstract = {The theory of graph games is the foundation for modeling and synthesizing reactive processes. In the synthesis of stochastic processes, we use \(2\frac{1}{2}\)-player games where some transitions of the game graph are controlled by two adversarial players, the System and the Environment, and the other transitions are determined probabilistically. We consider \(2\frac{1}{2}\)-player games where the objective of the System is the conjunction of a qualitative objective (specified as a parity condition) and a quantitative objective (specified as a mean-payoff condition). We establish that the problem of deciding whether the System can ensure that the probability to satisfy the mean-payoff parity objective is at least a given threshold is in \(\textsf{NP}\cap\textsf{coNP}\), matching the best known bound in the special case of 2-player games (where all transitions are deterministic) with only parity objectives, or with only mean-payoff objectives. We present an algorithm running in time~\(O(d \cdot n^{2d} \cdot \textsf{MeanGame}) to compute the set of almost-sure winning states from which the objective can be ensured with probability~1, where n is the number of states of the game, d the number of priorities of the parity objective, and MeanGame is the complexity to compute the set of almost-sure winning states in \(2\frac{1}{2}\)-player mean-payoff games. Our results are useful in the synthesis of stochastic reactive systems with both functional requirement (given as a qualitative objective) and performance requirement (given as a quantitative objective).} }

@inproceedings{DMS-fossacs14, address = {Grenoble, France}, month = apr, year = 2014, volume = {8412}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Muscholl, Anca}, acronym = {{FoSSaCS}'14}, booktitle = {{P}roceedings of the 17th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'14)}, author = {Doyen, Laurent and Massart, {\relax Th}ierry and Shirmohammadi, Mahsa}, title = {Limit Synchronization in Markov Decision Processes}, pages = {58-72}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DMS-fossacs14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DMS-fossacs14.pdf}, doi = {10.1007/978-3-642-54830-7_4}, abstract = {Markov decision processes (MDP) are finite-state systems with both strategic and probabilistic choices. After fixing a strategy, an MDP produces a sequence of probability distributions over states. The sequence is eventually synchronizing if the probability mass accumulates in a single state, possibly in the limit. Precisely, for \(0 \leq p \leq 1\) the sequence is \(p\)-synchronizing if a probability distribution in the sequence assigns probability at least~\(p\) to some state, and we distinguish three synchronization modes: \textit{(i)}~sure winning if there exists a strategy that produces a 1-synchronizing sequence; \textit{(ii)}~almost-sure winning if there exists a strategy that produces a sequence that is, for all \(\varepsilon>0\), a \((1-\varepsilon)\)-synchronizing sequence; \textit{(iii)}~limit-sure winning if for all \(\varepsilon>0\), there exists a strategy that produces a \((1-\varepsilon)\)-synchronizing sequence. We~consider the problem of deciding whether an MDP is sure, almost-sure, or limit-sure winning, and we establish the decidability and optimal complexity for all modes, as well as the memory requirements for winning strategies. Our main contributions are as follows: \textit{(a)}~for~each winning modes we~present characterizations that give a PSPACE complexity for the decision problems, and we establish matching PSPACE lower bounds; \textit{(b)}~we~show that for sure winning strategies, exponential memory is sufficient and may be necessary, and that in general infinite memory is necessary for almost-sure winning, and unbounded memory is necessary for limit-sure winning; \textit{(c)}~along with our results, we establish new complexity results for alternating finite automata over a one-letter alphabet.} }

@inproceedings{FSS-icdt14, address = {Athens, Greece}, month = mar, year = 2014, editor = {Schweikardt, Nicole and Christophides, Vassilis and Leroy, Vincent}, acronym = {{ICDT}'14}, booktitle = {{P}roceedings of the 17th {I}nternational {C}onference on {D}atabase {T}heory ({ICDT}'14)}, author = {Francis, Nadime and Segoufin, Luc and Sirangelo, Cristina}, title = {Datalog Rewritings of Regular Path Queries using Views}, pages = {107-118}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FSS-icdt14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FSS-icdt14.pdf}, doi = {10.5441/002/icdt.2014.14}, abstract = {We consider query answering using views on graph databases, i.e. databases structured as edge-labeled graphs. We consider views and queries specified by Regular Path Queries. 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.\par A~view~\(\mathbf{V}\) determines a query~\(Q\) if for all graph databases~\(D\), the view image~\(\mathbf{V}(D)\) always contains enough information to answer~\(Q\) on~\(D\). In other words, there is a well defined function from~\(\mathbf{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~\(\mathbf{V}(D)\). In~particular the query can be evaluated in time polynomial in the size of~\(\mathbf{V}(D)\).\par As a side result we also prove that it is decidable whether an RPQ query can be rewritten in Datalog using RPQ views.} }

@techreport{BB-arxiv14, author = {Brault{-}Baron, Johann}, title = {Hypergraph Acyclicity Revisited}, institution = {Computing Research Repository}, number = {1403.7076}, year = {2014}, month = feb, type = {Research Report}, url = {http://arxiv.org/abs/1403.7076}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BB-arxiv14.pdf}, note = {32~pages}, abstract = {The notion of graph acyclicity has been extended to several different notions of hypergraph acyclicity, in increasing order of generality: \emph{gamma} acyclicity, \emph{beta} acyclicity, and \emph{alpha} acyclicity, that have met a great interest in many fields. \parWe prove the equivalence between the numerous characterizations of each notion with a new, simpler proof, in a self-contained manner. For that purpose, we introduce new notions of alpha, beta and gamma leaf that allow to define new {"}rule-based{"} characterizations of each notion.\par The~combined presentation of the notions is completed with a study of their respective closure properties. New closure results are established, and alpha, beta and gamma acyclicity are proved optimal w.r.t. their closure properties.} }

@article{LM-lmcs14, journal = {Logical Methods in Computer Science}, author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas}, title = {Quantified {CTL}: Expressiveness and Complexity}, volume = 10, number = {4:17}, nopages = {}, month = dec, year = 2014, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LM-lmcs14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LM-lmcs14.pdf}, doi = {10.2168/LMCS-10(4:17)2014}, abstract = {While it was defined long ago, the extension of CTL with quantification over atomic propositions has never been studied extensively. Considering two different semantics (depending whether propositional quantification refers to the Kripke structure or to its unwinding tree), we~study its expressiveness (showing in particular that QCTL coincides with Monadic Second-Order Logic for both semantics) and characterise the complexity of its model-checking and satisfiability problems, depending on the number of nested propositional quantifiers (showing that the structure semantics populates the polynomial hierarchy while the tree semantics populates the exponential hierarchy).} }

@article{NM-ercim14, publisher = {European Research Consortium for Informatics and Mathematics}, journal = {ERCIM News}, author = {Markey, Nicolas}, title = {Cassting: Synthesizing Complex Systems Using Non-Zero-Sum Games}, volume = 97, pages = {25-26}, year = 2014, month = apr, url = {http://ercim-news.ercim.eu/en97/special/cassting-synthesizing-complex-systems-using-non-zero-sum-games}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/NM-ercim14.pdf} }

@inproceedings{DGLM-csr14, address = {Moscow, Russia}, month = jun, year = 2014, volume = {8476}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Pin, Jean-{\'E}ric}, acronym = {{CSR}'14}, booktitle = {{P}roceedings of the 9th {I}nternational {C}omputer {S}cience {S}ymposium in {R}ussia ({CSR}'14)}, author = {Demri, St{\'e}phane and Galmiche, Didier and Larchey-Wendling, Dominique and M{\'e}ry, Daniel}, title = {Separation Logic with One Quantified Variable}, pages = {125-138}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DGLM-csr14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DGLM-csr14.pdf}, doi = {10.1007/978-3-319-06686-8_10}, abstract = {We investigate first-order separation logic with one record field restricted to a unique quantified variable (1SL1). Undecidability is known when the number of quantified variables is unbounded and the satisfiability problem is PSPACE-complete for the propositional fragment. We show that the satisfiability problem for 1SL1 is PSPACE-complete and we characterize its expressive power by showing that every formula is equivalent to a Boolean combination of atomic properties. This contributes to our understanding of fragments of first-order separation logic that can specify properties about the memory heap of programs with singly-linked lists. When the number of program variables is fixed, the complexity drops to polynomial time. All the fragments we consider contain the magic wand operator and first-order quantification over a single variable.} }

@phdthesis{mahsa-phd2014, author = {Shirmohammadi, Mahsa}, title = {Qualitative Analysis of Synchronizing Probabilistic Systems}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France and Universit\'e Libre de Bruxelles, Belgium}, type = {Th{\`e}se de doctorat}, year = 2014, month = dec, url = {http://www.lsv.fr/Publis/PAPERS/PDF/mahsa-phd14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/mahsa-phd14.pdf} }

@phdthesis{soulat-phd2014, author = {Soulat, Romain}, title = {Synthesis of Correct-by-Design Schedulers for Hybrid Systems}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2014, month = feb, url = {http://www.lsv.fr/Publis/PAPERS/PDF/soulat-phd14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/soulat-phd14.pdf} }

@techreport{rr-lsv-14-03, author = {Fribourg, Laurent and Goubault, {\'E}ric and Mohamed, Sameh and Putot, Sylvie and Soulat, Romain}, title = {Synthesis of robust boundary control for systems governed by semi-discrete differential equations}, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, year = {2014}, month = feb, type = {Research Report}, number = {LSV-14-03}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2014-03.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2014-03.pdf}, versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2014-03-v1.pdf, 20140228}, note = {8~pages}, abstract = {The topic of boundary control of PDEs has been the subject of a considerable literature since the seminal works of J.-L. Lions in the 90s. In this paper, we consider the boundary control of systems represented by spatial discretizations of~PDEs (i.e.,~semi-discrete equations). We~focus on control laws which are sampled and piecewise constant: periodically, at every sampling time, a fixed control amplitude is applied to the system until the next sampling instant. We show that, under some conditions, sampled piecewise-constant boundary control allows to achieve {"}approximate controllability{"}: Given a time \(T>0\), the controlled system evolves to a neighborhood of a given final state. The result is illustrated on the boundary control of the semi-discrete version of the heat equation.} }

@inproceedings{CDFR-vmcai14, address = {San~Diego, California, USA}, month = jan, year = 2014, volume = 8318, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {McMillan, Kenneth and Rival, Xavier}, acronym = {{VMCAI}'14}, booktitle = {{P}roceedings of the 15th {I}nternational {C}onference on {V}erification, {M}odel {C}hecking and {A}bstract {I}nterpretation ({VMCAI}'14)}, author = {Chatterjee, Krishnendu and Doyen, Laurent and Filiot, Emmanuel and Raskin, Jean-Fran{\c{c}}ois}, title = {Doomsday Equilibria for Omega-Regular Games}, pages = {78-97}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDFR-vmcai14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDFR-vmcai14.pdf}, doi = {10.1007/978-3-642-54013-4_5}, abstract = {Two-player games on graphs provide the theoretical framework for many important problems such as reactive synthesis. While the traditional study of two-player zero-sum games has been extended to multi-player games with several notions of equilibria, they are decidable only for perfect-information games, whereas several applications require imperfect-information games.\par In this paper we propose a new notion of equilibria, called doomsday equilibria, which is a strategy profile such that all players satisfy their own objective, and if any coalition of players deviates and violates even one of the players objective, then the objective of every player is violated.\par We present algorithms and complexity results for deciding the existence of doomsday equilibria for various classes of \(\omega\)-regular objectives, both for imperfect-information games, and for perfect-information games.We provide optimal complexity bounds for imperfect-information games, and in most cases for perfect-information games.} }

@inproceedings{Schmitz-rta14, address = {Vienna, Austria}, month = jul, year = 2014, volume = {8560}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Dowek, Gilles}, acronym = {{RTA\slash TLCA}'14}, booktitle = {{P}roceedings of the {J}oint 25th {I}nternational {C}onference on {R}ewriting {T}echniques and {A}pplications and 12th {I}nternational {C}onference on {T}yped {L}ambda-{C}alculi and {A}pplications ({RTA\slash TLCA}'14)}, author = {Schmitz, Sylvain}, title = {Implicational Relevance Logic is 2-{E}xp{T}ime-Complete}, pages = {395-409}, url = {http://arxiv.org/abs/1402.0705}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Schmitz-rta14.pdf}, doi = {10.1007/978-3-319-08918-8_27}, abstract = {We show that provability in the implicational fragment of relevance logic is complete for doubly exponential time, using reductions to and from coverability in branching vector addition systems.} }

@inproceedings{LS-csllics14, address = {Vienna, Austria}, month = jul, year = 2014, publisher = {ACM Press}, acronym = {{CSL\slash LICS}'14}, booktitle = {{P}roceedings of the Joint Meeting of the 23rd {EACSL} {A}nnual {C}onference on {C}omputer {S}cience {L}ogic and the 29th {A}nnual {ACM\slash IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({CSL\slash LICS}'14)}, author = {Lazi{\'c}, Ranko and Schmitz, Sylvain}, title = {Non-Elementary Complexities for Branching {VASS}, {MELL}, and Extensions}, nopages = {}, chapter = 61, url = {http://arxiv.org/abs/1401.6785}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-csllics14.pdf}, doi = {10.1145/2603088.2603129}, 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{BDH-post14, address = {Grenoble, France}, month = apr, year = 2014, volume = {8414}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Abadi, Mart{\'\i}n and Kremer, Steve}, acronym = {{POST}'14}, booktitle = {{P}roceedings of the 3rd {I}nternational {C}onference on {P}rinciples of {S}ecurity and {T}rust ({POST}'14)}, author = {Baelde, David and Delaune, St{\'e}phanie and Hirschi, Lucca}, title = {A~reduced semantics for deciding trace equivalence using constraint systems}, pages = {1-21}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDH-post14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDH-post14.pdf}, doi = {10.1007/978-3-642-54792-8_1}, abstract = {Many privacy-type properties of security protocols can be modelled using trace equivalence properties in suitable process algebras. It has been shown that such properties can be decided for interesting classes of finite processes (i.e.,~without replication) by means of symbolic execution and constraint solving. However, this does not suffice to obtain practical tools. Current prototypes suffer from a classical combinatorial explosion problem caused by the exploration of many interleavings in the behaviour of processes. Modersheim et~al. have tackled this problem for reachability properties using partial order reduction techniques. We revisit their work, generalize it and adapt it for equivalence checking. We obtain an optimization in the form of a reduced symbolic semantics that eliminates redundant interleavings on the fly.} }

@inproceedings{BM-sr14, address = {Grenoble, France}, month = apr, year = 2014, volume = 146, series = {Electronic Proceedings in Theoretical Computer Science}, editor = {Mogavero, Fabio and Murano, Aniello}, acronym = {{SR}'14}, booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop on {S}trategic {R}easoning ({SR}'14)}, author = {Berwanger, Dietmar and Mathew, Anup Basil}, title = {Games with Recurring Certainty}, pages = {91-96}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BM-sr14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BM-sr14.pdf}, doi = {10.4204/EPTCS.146.12}, abstract = {Infinite games where several players seek to coordinate under imperfect information are known to be intractable, unless the information flow is severely restricted. Examples of undecidable cases typically feature a situation where players become uncertain about the current state of the game, and this uncertainty lasts forever.\par Here we consider games where the players attain certainty about the current state over and over again along any play. For finite-state games, we note that this kind of \emph{recurring} certainty implies a stronger condition of \emph{periodic} certainty, that is, the events of state certainty ultimately occur at uniform, regular intervals. We show that it is decidable whether a given game presents recurring certainty, and that, if so, the problem of synthesising coordination strategies under \(\omega\)-regular winning conditions is solvable.} }

@inproceedings{CDFR-sr14, address = {Grenoble, France}, month = apr, year = 2014, volume = 146, series = {Electronic Proceedings in Theoretical Computer Science}, editor = {Mogavero, Fabio and Murano, Aniello}, acronym = {{SR}'14}, booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop on {S}trategic {R}easoning ({SR}'14)}, author = {Chatterjee, Krishnendu and Doyen, Laurent and Filiot, Emmanuel and Raskin, Jean-Fran{\c{c}}ois}, title = {Doomsday Equilibria for Omega-Regular Games}, pages = {43-48}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDFR-sr14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDFR-sr14.pdf}, doi = {10.4204/EPTCS.146.6}, abstract = {Two-player games on graphs provide the theoretical framework for many important problems such as reactive synthesis. While the traditional study of two-player zero-sum games has been extended to multi-player games with several notions of equilibria, they are decidable only for perfect-information games, whereas several applications require imperfect-information games.\par In this paper we propose a new notion of equilibria, called doomsday equilibria, which is a strategy profile such that all players satisfy their own objective, and if any coalition of players deviates and violates even one of the players objective, then the objective of every player is violated.\par We present algorithms and complexity results for deciding the existence of doomsday equilibria for various classes of \(\omega\)-regular objectives, both for imperfect-information games, and for perfect-information games. We provide optimal complexity bounds for imperfect-information games, and in most cases for perfect-information games.} }

@inproceedings{BMV-sr14, address = {Grenoble, France}, month = apr, year = 2014, volume = 146, series = {Electronic Proceedings in Theoretical Computer Science}, editor = {Mogavero, Fabio and Murano, Aniello}, acronym = {{SR}'14}, booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop on {S}trategic {R}easoning ({SR}'14)}, author = {Bouyer, Patricia and Markey, Nicolas and Vester, Steen}, title = {Nash Equilibria in Symmetric Games with Partial Observation}, pages = {49-55}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMV-sr14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMV-sr14.pdf}, doi = {10.4204/EPTCS.146.7}, abstract = {We investigate a model for representing large multiplayer games, which satisfy strong symmetry properties. This model is made of multiple copies of an arena; each player plays in his own arena, and can partially observe what the other players do. Therefore, this game has partial information and symmetry constraints, which make the computation of Nash equilibria difficult. We show several undecidability results, and for bounded-memory strategies, we precisely characterize the complexity of computing pure Nash equilibria (for qualitative objectives) in this game model.} }

@phdthesis{cyriac-phd2014, author = {Cyriac, Aiswarya}, title = {Verification of Communicating Recursive Programs via Split-width}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2014, month = jan, url = {http://www.lsv.fr/Publis/PAPERS/PDF/cyriac-phd14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/cyriac-phd14.pdf} }

@inproceedings{AGHKO-fossacs14, address = {Grenoble, France}, month = apr, year = 2014, volume = {8412}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Muscholl, Anca}, acronym = {{FoSSaCS}'14}, booktitle = {{P}roceedings of the 17th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'14)}, author = {Antonopoulos, Timos and Gorogiannis, Nikos and Haase, Christoph and Kanovich, Max and Ouaknine, Jo{\"e}l}, title = {Foundations for Decision Problems in Separation Logic with General Inductive Predicates}, pages = {411-425}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AGHKO-fossacs14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGHKO-fossacs14.pdf}, doi = {10.1007/978-3-642-54830-7_27}, abstract = {We establish foundational results on the computational complexity of deciding entailment in Separation Logic with general inductive predicates whose underlying base language allows for pure formulas, pointers and existentially quantified variables. We show that entailment is in general undecidable, and \textsc{ExpTime}-hard in a fragment recently shown to be decidable by Iosif~\emph{et~al.} Moreover, entailment in the base language is \(\Pi_2^{\text{P}}\)-complete, the upper bound even holds in the presence of list predicates. We additionally show that entailment in essentially any fragment of Separation Logic allowing for general inductive predicates is intractable even when strong syntactic restrictions are imposed.} }

@inproceedings{BFHHH-fossacs14, address = {Grenoble, France}, month = apr, year = 2014, volume = {8412}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Muscholl, Anca}, acronym = {{FoSSaCS}'14}, booktitle = {{P}roceedings of the 17th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'14)}, author = {Bertrand, Nathalie and Fabre, {\'E}ric and Haar, Stefan and Haddad, Serge and H{\'e}lou{\"e}t, Lo{\"\i}c}, title = {Active diagnosis for probabilistic systems}, pages = {29-42}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHHH-fossacs14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHHH-fossacs14.pdf}, doi = {10.1007/978-3-642-54830-7_4}, abstract = {The diagnosis problem amounts to deciding whether some specific {"}fault{"} event occurred or not in a system, given the observations collected on a run of this system. This system is then diagnosable if the fault can always be detected, and the active diagnosis problem consists in controlling the system in order to ensure its diagnosability. We consider here a stochastic framework for this problem: once a control is selected, the system becomes a stochastic process. In this setting, the active diagnosis problem consists in deciding whether there exists some observation-based strategy that makes the system diagnosable with probability one. We prove that this problem is EXPTIME-complete, and that the active diagnosis strategies are belief-based. The safe active diagnosis problem is similar, but aims at enforcing diagnosability while preserving a positive probability to non faulty runs, i.e. without enforcing the occurrence of a fault. We prove that this problem requires non belief-based strategies, and that it is undecidable. However, it belongs to NEXPTIME when restricted to belief-based strategies. Our work also refines the decidability/undecidability frontier for verification problems on partially observed Markov decision processes.} }

@article{ABGMN-fi13, publisher = {{IOS} Press}, journal = {Fundamenta Informaticae}, author = {Akshay, S. and Bollig, Benedikt and Gastin, Paul and Mukund, Madhavan and Narayan Kumar, K.}, title = {Distributed Timed Automata with Independently Evolving Clocks}, volume = {130}, number = {4}, month = apr, year = 2014, pages = {377-407}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGMN-fi13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGMN-fi13.pdf}, doi = {10.3233/FI-2014-996}, abstract = {We propose a model of distributed timed systems where each component is a timed automaton with a set of local clocks that evolve at a rate independent of the clocks of the other components. A~clock can be read by any component in the system, but it can only be reset by the automaton it belongs~to.\par There are two natural semantics for such systems. The \emph{universal} semantics captures behaviors that hold under any choice of clock rates for the individual components. This is a natural choice when checking that a system always satisfies a positive specification. To check if a system avoids a negative specification, it is better to use the \emph{existential} semantics—the set of behaviors that the system can possibly exhibit under some choice of clock rates.\par We show that the existential semantics always describes a regular set of behaviors. However, in the case of universal semantics, checking emptiness or universality turns out to be undecidable. As an alternative to the universal semantics, we propose a \emph{reactive} semantics that allows us to check positive specifications and yet describes a regular set of behaviors.} }

@article{BGMZ-tocl13, publisher = {ACM Press}, journal = {ACM Transactions on Computational Logic}, author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin and Zeitoun, Marc}, title = {Pebble Weighted Automata and Weighted Logics}, volume = 15, number = {2:15}, month = apr, year = 2014, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-tocl13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-tocl13.pdf}, doi = {10.1145/2579819}, abstract = {We introduce new classes of weighted automata on words. Equipped with pebbles, they go beyond the class of recognizable formal power series: they capture weighted first-order logic enriched with a quantitative version of transitive closure. In contrast to previous work, this calculus allows for unrestricted use of existential and universal quantifications over positions of the input word. We actually consider both two-way and one-way pebble weighted automata. The latter class constrains the head of the automaton to walk left-to-right, resetting it each time a pebble is dropped. Such automata have already been considered in the Boolean setting, in the context of data words. Our main result states that two-way pebble weighted automata, one-way pebble weighted automata, and our weighted logic are expressively equivalent. We also give new logical characterizations of standard recognizable series.} }

@article{SBM-ic14, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Sankur, Ocan and Bouyer, Patricia and Markey, Nicolas}, title = {Shrinking Timed Automata}, volume = 234, month = feb, year = 2014, pages = {107-132}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/SBM-ic14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SBM-ic14.pdf}, doi = {10.1016/j.ic.2014.01.002}, abstract = {We define and study a new approach to the implementability of timed automata, where the semantics is perturbed by imprecisions and finite frequency of the hardware. In order to circumvent these effects, we introduce \emph{parametric shrinking} of clock constraints, which corresponds to tightening the guards. We propose symbolic procedures to decide the existence of (and then compute) parameters under which the shrunk version of a given timed automaton is non-blocking and can time-abstract simulate the exact semantics. We then define an implementation semantics for timed automata with a digital clock and positive reaction times, and show that for shrinkable timed automata, non-blockingness and time-abstract simulation are preserved in implementation.} }

@article{GM-tcs14, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {Gastin, Paul and Monmege, Benjamin}, title = {Adding Pebbles to Weighted Automata~-- Easy Specification {\&} Efficient Evaluation}, volume = {534}, month = may, year = 2014, pages = {24-44}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/GM-tcs14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GM-tcs14.pdf}, doi = {10.1016/j.tcs.2014.02.034}, abstract = {We extend weighted automata and weighted rational expressions with 2-way moves and reusable pebbles. We show with examples from natural language modeling and quantitative model-checking that weighted expressions and automata with pebbles are more expressive and allow much more natural and intuitive specifications than classical ones. We extend Kleene-Sch{\"u}tzenberger theorem showing that weighted expressions and automata with pebbles have the same expressive power. We focus on an efficient translation from expressions to automata. We also prove that the evaluation problem for weighted automata can be done very efficiently if the number of reusable pebbles is low.} }

@article{BLM-peva13, publisher = {Elsevier Science Publishers}, journal = {Performance Evaluation}, author = {Bouyer, Patricia and Larsen, Kim G. and Markey, Nicolas}, title = {Lower-Bound Constrained Runs in Weighted Timed Automata}, volume = 73, month = mar, year = 2014, pages = {91-109}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BLM-peva13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BLM-peva13.pdf}, doi = { 10.1016/j.peva.2013.11.002}, abstract = {We investigate a number of problems related to infinite runs of weighted timed automata (with a single weight variable), subject to lower-bound constraints on the accumulated weight. Closing an open problem from an earlier paper, we show that the existence of an infinite lower-bound-constrained run is--for us somewhat unexpectedly--undecidable for weighted timed automata with four or more clocks.\par This undecidability result assumes a fixed and known initial credit. We show that the related problem of existence of an initial credit for which there exists a feasible run is decidable in PSPACE. We also investigate the variant of these problems where only bounded-duration runs are considered, showing that this restriction makes our original problem decidable in NEXPTIME. We prove that the universal versions of all those problems (i.e, checking that all the considered runs satisfy the lower-bound constraint) are decidable in PSPACE.\par Finally, we extend this study to multi-weighted timed automata: the existence of a feasible run becomes undecidable even for bounded duration, but the existence of initial credits remains decidable (in~PSPACE).} }

@inproceedings{KL-pdp14, address = {Turin, Italy}, month = feb, year = 2014, publisher = {{IEEE} Computer Society Press}, editor = {Aldinucci, Marco and D'Agostino, Daniele and Kilpatrick, Peter}, acronym = {{PDP}'14}, booktitle = {{P}roceedings of the 22nd {E}uromicro {I}nternational {C}onference on {P}arallel, {D}istributed, and {N}etwork-{B}ased {P}rocessing ({PDP}'14)}, author = {Kumar, Sunil and Lipari, Giuseppe}, title = {Latency Analysis of Network-On-Chip-based Many-Core Processors}, pages = {432-439}, doi = {10.1109/PDP.2014.107}, abstract = {The next generation of processor will contain an increasing number of cores, connected to the main memory and to each other using fast Network-on-Chip (NoC) organised in complex mesh structures. In order to analyse real-time programs running on such architectures, it is necessary to estimate the communication latency between processes running on different cores. The goal of this paper is to propose an analytic model for bounding the communication latency on NoC for many-core architectures. In particular, we introduce a new approach to analyse the communication latency on NoC with wormhole switching and credit-based virtual channel flow control. The proposed model is evaluated by comparing the results predicted by the model with real measurements obtained running a set of experiments on an Intel SCC platform.} }

@article{ACD-icomp13, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Arnaud, Mathilde and Cortier, V{\'e}ronique and Delaune, St{\'e}phanie}, title = {Modeling and Verifying Ad~Hoc Routing Protocols}, volume = 238, pages = {30-67}, month = nov, year = 2014, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ACD-icomp13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ACD-icomp13.pdf}, doi = {10.1016/j.ic.2014.07.004}, abstract = {Mobile ad hoc networks consist of mobile wireless devices which autonomously organize their infrastructure. In such networks, a central issue, ensured by routing protocols, is to find a route from one device to another. Those protocols use cryptographic mechanisms in order to prevent malicious nodes from compromising the discovered route.\par Our contribution is twofold. We first propose a calculus for modeling and reasoning about security protocols, including in particular secured routing protocols. Our calculus extends standard symbolic models to take into account the characteristics of routing protocols and to model wireless communication in a more accurate way. Our second main contribution is a decision procedure for analyzing routing protocols for any network topology. By using constraint solving techniques, we show that it is possible to automatically discover (in~NPTIME) whether there exists a network topology that would allow malicious nodes to mount an attack against the protocol, for a bounded number of sessions. We also provide a decision procedure for detecting attacks in case the network topology is given a priori. We demonstrate the usage and usefulness of our approach by analyzing protocols of the literature, such as SRP applied to DSR and SDMSR.} }

@inproceedings{HHM-tgc13, address = {Buenos Aires, Argentina}, month = mar, year = 2014, volume = {8358}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Abadi, Mart{\'\i}n and Lluch{ }Lafuente, Alberto}, acronym = {{TGC}'13}, booktitle = {{R}evised {S}elected {P}apers of the 8th {S}ymposium on {T}rustworthy {G}lobal {C}omputing ({TGC}'13)}, author = {Haddad, Serge and Hennicker, Rolf and M{\o}ller, Mikael H.}, title = {Specification of Asynchronous Component Systems with Modal {I}{{\slash}}{O}-{P}etri Nets}, pages = {219-234}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/HHM-tgc13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HHM-tgc13.pdf}, doi = {10.1007/978-3-319-05119-2_13}, abstract = {We consider Petri nets with distinguished labels for inputs, outputs, internal communications and silent actions and with {"}must{"} and {"}may{"} modalities for transitions. The input\slash output labels show the interaction capabilities of a net to the outside used to build larger nets by asynchronous composition via communication channels. The modalities express constraints for Petri net refinement taking into account observational abstraction from silent transitions. Modal I\slash O-Petri nets are equipped with a modal transition system semantics. We show that refinement is preserved by asynchronous composition and by hiding of communication channels. We study conformance properties which express communication requirements for composed systems and we show that those properties are preserved by refinement. On this basis we propose a methodology for the specification of distributed systems in terms of modal I\slash O-Petri nets which supports incremental design, encapsulation of components and stepwise refinement. Finally we show that our communication properties are decidable.} }

@article{GL-acs13, publisher = {Springer}, journal = {Applied Categorical Structures}, author = {Goubault{-}Larrecq, Jean}, title = {Exponentiable streams and prestreams}, volume = {22}, number = {3}, year = 2014, month = jun, pages = {515-549}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/GL-acs13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GL-acs13.pdf}, corrigendumpdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GL-acs13-erratum.pdf}, doi = { 10.1007/s10485-013-9315-x}, note = {Errata 1: \url{http://www.lsv.fr/Publis/PAPERS/PDF/GL-acs13-erratum.pdf}; Errata 2: \url{http://www.lsv.fr/Publis/PAPERS/PDF/GL-acs13-erratum2.pdf}}, abstract = {Inspired by a construction of Escard{\'o}, Lawson, and Simpson, we give a general construction of \(\mathcal C\)-generated objects in a topological construct. When \(\mathcal C\) consists of exponentiable objects, the resulting category is Cartesian-closed. This generalizes the familiar construction of compactly-generated spaces, and we apply this to Krishnan's categories of streams and prestreams, as well as to Haucourt streams. For that, we need to identify the exponentiable objects in these categories: for prestreams, we show that these are the preordered core-compact topological spaces, and for streams, these are the core-compact streams.} }

@article{BCD-icomp13, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Bursuc, Sergiu and Comon{-}Lundh, Hubert and Delaune, St{\'e}phanie}, title = {Deducibility constraints and blind signatures}, year = {2014}, month = nov, volume = 238, pages = {106-127}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCD-icomp13.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCD-icomp13.pdf}, nonote = {32~pages}, doi = {10.1016/j.ic.2014.07.006}, abstract = {Deducibility constraints represent in a symbolic way the infinite set of possible executions of a finite protocol. Solving a deducibility constraint amounts to finding all possible ways of filling the gaps in a proof. For finite local inference systems, there is an algorithm that reduces any deducibility constraint to a finite set of solved forms. This allows one to decide any trace security property of cryptographic protocols.\par We investigate here the case of infinite local inference systems, through the case study of blind signatures. We show that, in this case again, any deducibility constraint can be reduced to finitely many solved forms (hence we can decide trace security properties). We sketch also another example to which the same method can be applied.} }

@article{BCGMNTW-jfr14, publisher = {University of Bologna}, journal = {Journal of Formalized Reasoning}, author = {Baelde, David and Chaudhuri, Kaustuv and Gacek, Andrew and Miller, Dale and Nadathur, Gopalan and Tiu, Alwen and Wang, Yuting}, title = {Abella: A~System for Reasoning about Relational Specifications}, volume = {7}, number = {2}, year = {2014}, pages = {1-89}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGMNTW-jfr14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGMNTW-jfr14.pdf}, doi = {10.6092/issn.1972-5787/4650}, abstract = {The Abella interactive theorem prover is based on an intuitionistic logic that allows for inductive and co-inductive reasoning over relations. Abella supports the \(\lambda\)-tree approach to treating syntax containing binders: it~allows simply typed \(\lambda\)-terms to be used to represent such syntax and it provides higher-order (pattern) unification, the \(\nabla\) quantifier, and nominal constants for reasoning about these representations. As such, it is a suitable vehicle for formalizing the meta-theory of formal systems such as logics and programming languages. This tutorial exposes Abella incrementally, starting with its capabilities at a first-order logic level and gradually presenting more sophisticated features, ending with the support it offers to the \emph{two-level logic approach} to meta-theoretic reasoning. Along the way, we show how Abella can be used prove theorems involving natural numbers, lists, and automata, as well as involving typed and untyped \(\lambda\)-calculi and the \(\pi\)-calculus.} }

@techreport{KNS-arxiv14, author = {Karandikar, Prateek and Niewerth, Matthias and Schnoebelen, {\relax Ph}ilippe}, title = {On the state complexity of closures and interiors of regular languages with subwords}, institution = {Computing Research Repository}, number = {1406.0690}, year = {2014}, month = nov, type = {Research Report}, url = {http://arxiv.org/abs/1406.0690}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KNS-arxiv14.pdf}, note = {24~pages}, abstract = {We study the state complexity of the set of subwords and superwords of regular languages, and provide new lower bounds in the case of languages over a two-letter alphabet. We also consider the dual interior sets, for which the nondeterministic state complexity has a doubly-exponential upper bound. We prove a matching doubly-exponential lower bound for downward interiors in the case of an unbounded alphabet.} }

@article{AFG-sif15, publisher = {SIF}, journal = {1024~-- Bulletin de la soci{\'e}t{\'e} informatique de France}, author = {Abiteboul, Serge and Fribourg, Laurent and Goubault{-}Larrecq, Jean}, title = {{G}{\'e}rard {B}erry~: un~informaticien m{\'e}daille d'or du {CNRS}~2014}, volume = 4, pages = {139-142}, month = oct, year = 2014, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AFG-sif15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AFG-sif15.pdf}, abstract = {C'est un chercheur en informatique qui vient de recevoir la m{\'e}daille d'or du CNRS, la plus haute distinction scientifique fran{\c c}aise toutes disciplines confondues. Les informaticiens sont rares {\`a} avoir {\'e}t{\'e} ainsi honor{\'e}s : ce n'est que la seconde fois apr{\`e}s Jacques Stern en~2006.} }

@inproceedings{MA-bda14, address = {Autrans, France}, month = oct, year = 2014, editor = {Gross-Amblard, David and Collet, {\relax Ch}ristine and Bobineau, {\relax Ch}ristophe and Jouanot, Fabrice}, acronym = {{BDA}'14}, booktitle = {{A}ctes de la 30{\`e}me {C}onf{\'e}rence sur la {G}estion de {D}onn{\'e}es~-- {P}rincipes, {T}echnologies et {A}pplications ({BDA}'14)}, author = {Montoya, David and Abiteboul, Serge}, title = {Inf{\'e}rence d'itin{\'e}raires multimodaux {\`a}~partir de donn{\'e}es smartphone}, pages = {38-42}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/MA-bda14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/MA-bda14.pdf}, abstract = {We designed a system to infer the multimodal itineraries traveled by a user from a combination of smartphone sensor data (e.g., GPS, Wi-Fi, inertial sensors), personal information, and knowledge of the transport network topology (e.g., maps, transportation timetables). The system operates with a Multimodal Transport Network that captures the set of admissible multimodal itineraries, i.e., paths of this network with weights providing the statistics (expected time and variance) of the paths. The network takes into account public transportation schedules. Our Multimodal Transport Network is constructed from publicly available transport data of Paris and its neighbourhoods published by different transport agencies and map organizations. The system models sensor uncertainty with probabilities, and the likelihood that a multimodal itinerary was taken by the user is captured in a Dynamic Bayesian Network. For this demonstration, we captured data from users travelling over the Paris region who were asked to record data for different trips via an Android application. After uploading their data into our system, a set of most likely itineraries is computed for each trip. For each trip, the system displays recognized multimodal itineraries and their estimated likelihood over an interactive map.} }

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

@misc{mcc:2014, author = {F. Kordon and H. Garavel and L.-M. Hillah and Hulin{-}Hubard, Francis and A. Linard and M. Beccuti and S. Evangelista and A. Hamez and N. Lohmann and E. Lopez and E. Paviot-Adet and C. Rodriguez and C. Rohr and J. Srba}, month = jun, title = {{Results for the MCC @ Petri Nets 2014}}, year = {2014}, url = {http://mcc.lip6.fr/2014} }

@mastersthesis{m2-doumane, author = {Doumane, Amina}, title = {{\'E}tudes des automates en ludique}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2014}, month = sep }

@misc{JGL:lls14, author = {Goubault{-}Larrecq, Jean}, howpublished = {Matinale de l'innovation Logiciels Libres et S{\'e}curit{\'e}, Paris, France}, month = dec, title = {D{\'e}tection d'intrusions avec {OrchIDS}}, year = {2014} }

@misc{JGL:ccc14, author = {Goubault{-}Larrecq, Jean}, howpublished = {Invited talk, Continuity, Computability, Constructivity workshop (CCC), Ljubljana, Slovenia}, month = sep, title = {Noetherian spaces}, year = {2014} }

@misc{JGL:cps14, author = {Goubault{-}Larrecq, Jean}, howpublished = {CPS Summer School, Grenoble, France}, month = jul, title = {{OrchIDS}: on the value of rigor in intrusion detection}, year = {2014} }

@misc{GSM:dga-inria-2-14, author = {Goubault-Larrecq, Jean and Sentucq, Pierre-Arnaud and Majorczyk, Fr{\'e}d{\'e}ric}, howpublished = {Fourniture 2 du contrat DGA-INRIA Orchids}, month = may, title = {Techniques et m{\'e}thodes de g{\'e}n{\'e}ration de signatures pour la d{\'e}tection d'intrusions}, year = {2014} }

@misc{GSM:dga-inria-1-14, author = {Goubault-Larrecq, Jean and Sentucq, Pierre-Arnaud and Majorczyk, Fr{\'e}d{\'e}ric}, howpublished = {Fourniture 1 du contrat DGA-INRIA Orchids}, month = may, title = {Politiques de s{\'e}curit{\'e} syst{\`e}me}, year = {2014} }

@mastersthesis{m2-Jaziri, author = {Jaziri, Samy}, title = {{Robustness issues in priced timed automata}}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2014}, month = sep }

*This file was generated by
bibtex2html 1.98.*