@article{BKM-cc14, publisher = {Birkh{\"a}user}, journal = {Computational Complexity}, author = {Blondin, Michael and Krebs, Andreas and McKenzie, Pierre}, title = {The Complexity of Intersecting Finite Automata Having Few Final States}, volume = {25}, number = {4}, pages = {775-814}, month = dec, year = 2016, note = {To appear}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BKM-cc14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BKM-cc14.pdf}, doi = {10.1007/s00037-014-0089-9}, abstract = {The problem of determining whether several finite automata accept a word in common is closely related to the well-studied membership problem in transformation monoids. We raise the issue of limiting the number of final states in the automata intersection problem. For automata with two final states, we show the problem to be \(\oplus{L}\)-complete or NP-complete according to whether a nontrivial monoid other than a direct product of cyclic groups of order~2 is allowed in the automata. We further consider idempotent commutative automata and (Abelian, mainly) group automata with one, two, or three final states over a singleton or larger alphabet, elucidating (under the usual hypotheses on complexity classes) the complexity of the intersection nonemptiness and related problems in each case.} }

@article{PHL-sttt14, publisher = {Springer}, journal = {International Journal on Software Tools for Technology Transfer}, author = {Ponce{ }de{~}Le{\'o}n, Hern{\'a}n and Haar, Stefan and Longuet, Delphine}, title = {Model-based Testing for Concurrent Systems: Unfolding-based Test Selection}, volume = {18}, number = 3, year = {2016}, month = jun, pages = {305-318}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-sttt14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-sttt14.pdf}, doi = {10.1007/s10009-014-0353-y}, abstract = {Model-based testing has mainly focused on models where concurrency is interpreted as interleaving (like the ioco theory for labeled transition systems), which may be too coarse when one wants concurrency to be preserved in the implementation. In order to test such concurrent systems, we choose to use Petri nets as specifications and define a concurrent conformance relation named co-ioco. We present a test generation algorithm based on Petri net unfolding able to build a complete test suite w.r.t our co-ioco conformance relation. In addition we propose several coverage criteria that allow to select finite prefixes of an unfolding in order to build manageable test suites.} }

@article{haar-mvlsc15, publisher = {Old City Publishing}, journal = {Journal of Multiple-Valued Logic and Soft Computing}, author = {Haar, Stefan}, title = {Cyclic Ordering through Partial Orders}, volume = {27}, number = {2-3}, year = 2016, month = sep, pages = {209-228}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/haar-mvlsc16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/haar-mvlsc16.pdf}, abstract = {The orientation problem for ternary cyclic order relations has been attacked in the literature from combinatorial perspectives, through rotations, and by connection with Petri nets. We propose here a two-fold characterization of orientable cyclic orders in terms of symmetries of partial orders as well as in terms of separating sets (cuts). The results are inspired by properties of non-sequential discrete processeses, but also apply to dense structures of any cardinality.} }

@article{KNS-tcs2015, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, 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 and superwords}, volume = {610}, number = {A}, pages = { 91-107}, year = {2016}, month = jan, url = {http://www.lsv.fr/Publis/PAPERS/PDF/KNS-tcs15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KNS-tcs15.pdf}, doi = {10.1016/j.tcs.2015.09.028}, abstract = {The downward and upward closures of a regular language~\(L\) are obtained by collecting all the subwords and superwords of its elements, respectively. The downward and upward interiors of~\(L\) are obtained dually by collecting words having all their subwords and superwords in~\(L\), respectively.\par We provide lower and upper bounds on the size of the smallest automata recognizing these closures and interiors. We also consider the computational complexity of decision problems for closures of regular languages.} }

@article{BHJL-fi15, publisher = {{IOS} Press}, journal = {Fundamenta Informaticae}, author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge and Jovanovi{\'c}, Aleksandra and Lime, Didier}, title = {Interrupt Timed Automata with Auxiliary Clocks and Parameters}, volume = {143}, number = {3-4}, pages = {235-259}, month = mar, year = 2016, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHJL-fi15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHJL-fi15.pdf}, doi = {10.3233/FI-2016-1313}, abstract = {Interrupt Timed Automata (ITA) are an expressive timed model, introduced to take into account interruptions according to levels. Due to this feature, this formalism is incomparable with Timed Automata.\par However several decidability results related to reachability and model checking have been obtained. We add auxiliary clocks to ITA, thereby extending its expressive power while preserving decidability of reachability. Moreover, we define a parametrized version of ITA, with polynomials of parameters appearing in guards and updates. While parametric reasoning is particularly relevant for timed models, it very often leads to undecidability results. We prove that various reachability problems, including robust reachability, are decidable for this model, and we give complexity upper bounds for a fixed or variable number of clocks, levels and parameters.} }

@article{BGM-ipl15, publisher = {Elsevier Science Publishers}, journal = {Information Processing Letters}, author = {Bouyer, Patricia and Gardy, Patrick and Markey, Nicolas}, title = {On~the semantics of Strategy Logic}, volume = {116}, number = {2}, pages = {75-79}, month = feb, year = {2016}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-ipl15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-ipl15.pdf}, doi = {10.1016/j.ipl.2015.10.004}, abstract = {We define and study a slight variation on the semantics of Strategy Logic: while in the classical semantics, all strategies are shifted during the evaluation of temporal modalities, we propose to only shift the strategies that have been assigned to a player, thus matching the intuition that we can assign the very same strategy to the players at different points in time. We prove that surprisingly, this renders the model-checking problem undecidable.} }

@article{HK-ipl15, publisher = {Elsevier Science Publishers}, journal = {Information Processing Letters}, author = {Haase, Christoph and Kiefer, Stefan}, title = {The Complexity of the \(K\)th Largest Subset Problem and Related Problems}, volume = {116}, number = {2}, pages = {111-115}, month = feb, year = {2016}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/HK-ipl15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HK-ipl15.pdf}, doi = {10.1016/j.ipl.2015.09.015}, abstract = {We show that the \textsc{\(K\)th largest subset} problem and the \textsc{\(K\)th largest \(m\)-tuple} problem are in PP and hard for PP under polynomial-time Turing reductions. Several problems from the literature were previously shown NP-hard via reductions from those two problems, and by our main result they become PP-hard as well. We also provide complementary PP-upper bounds for some of them.} }

@article{DD-jlc15, publisher = {Oxford University Press}, journal = {Journal of Logic and Computation}, author = {Demri, St{\'e}phane and Deters, Morgan}, title = {Temporal Logics on Strings with Prefix Relation}, year = 2016, volume = {26}, number = {3}, pages = {989-1017}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-jlc15-v2.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-jlc15-v2.pdf}, doi = {10.1093/logcom/exv028}, abstract = {We show that linear-time temporal logic over concrete domains made of finite strings and the prefix relation admits a PSpace-complete satisfiability problem. Actually, we extend a known result with the concrete domain made of the set of natural numbers and the greater than relation (corresponding to the singleton alphabet case) and we solve an open problem mentioned in several publications. Since the prefix relation is not a total ordering, it~is not possible to take advantage of existing techniques dedicated to temporal logics with concrete domains that are essentially linearly ordered structures. Instead, we introduce an adequate encoding of string constraints into length constraints that allows us to reduce the problem on strings to the problem on natural numbers. To~do~so, we~also propose an extended version of the logic on strings that is able to compare lengths of longest common prefixes and for which the satisfiability problem is shown in PSpace. Finally, we show how to lift the result for the branching-time case in order to get decidability when the underlying temporal logic is~CTL\textsuperscript*.} }

@article{Schmitz-jsl15, publisher = {Association for Symbolic Logic}, journal = {Journal of Symbolic Logic}, author = {Schmitz, Sylvain}, title = {Implicational Relevance Logic is \(2\)-{ExpTime}-Complete}, volume = {81}, number = {2}, pages = {641-661}, month = jun, year = 2016, url = {http://arxiv.org/abs/1402.0705}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Schmitz-jsl15.pdf}, doi = {10.1017/jsl.2015.7}, 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.} }

@misc{qcover16, author = {Blondin, Michael and Finkel, Alain and Haase, Christoph and Haddad, Serge}, title = {{QCover: an efficient coverability verifier for discrete and continuous Petri nets}}, url = {https://github.com/blondimi/qcover}, year = {2016} }

@phdthesis{theissing-PhD16, author = {Theissing, Simon}, title = {Supervision in Multi-Modal Transportation System}, school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France}, type = {Th{\`e}se de doctorat}, year = {2016}, month = dec, url = {https://tel.archives-ouvertes.fr/tel-01419126}, pdf = {https://hal.inria.fr/tel-01419126v3/document} }

@article{BCEZ-dmtcs2016, journal = {Discrete Mathematics \& Theoretical Computer Science}, author = {Brough, Tara and Ciobanu, Laura and Elder, Murray and Zetzsche, Georg}, title = {{Permutations of context-free, ET0L and indexed languages}}, volume = {17}, number = {3}, year = {2016}, month = may, pages = {167-178}, url = {https://dmtcs.episciences.org/2164}, pdf = {https://arxiv.org/pdf/1604.05431.pdf} }

@inproceedings{DLV-pods16, acronym = {{PODS}'16}, publisher = {ACM Press}, month = jun, booktitle = {{P}roceedings of the 35th {ACM} {SIGMOD-SIGACT-SIGAI} {S}ymposium on {P}rinciples of {D}atabase {S}ystems ({PODS}'16)}, title = {{P}roceedings of the 35th {ACM} {SIGMOD-SIGACT-SIGAI} {S}ymposium on {P}rinciples of {D}atabase {S}ystems ({PODS}'16)}, address = {San Francisco, California, USA}, abstract = {Data-driven workflows, of which IBM's Business Artifacts are a prime exponent, have been successfully deployed in practice, adopted in industrial standards, and have spawned a rich body of research in academia, focused primarily on static analysis. The present work represents a significant advance on the problem of artifact verification, by considering a much richer and more realistic model than in previous work, incorporating core elements of IBM's successful Guard-Stage-Milestone model. In particular, the model features task hierarchy, concurrency, and richer artifact data. It also allows database key and foreign key dependencies, as well as arithmetic constraints. The results show decidability of verification and establish its complexity, making use of novel techniques including a hierarchy of Vector Addition Systems and a variant of quantifier elimination tailored to our context.}, author = {Deutsch, Alin and Li, Yuliang and Vianu, Victor}, pages = {179-194}, doi = {10.1145/2902251.2902275}, year = {2016} }

@phdthesis{mvdb-phd2016, author = {Van{ }den{ }Bogaard, Marie}, title = {Motifs de Flot d'Information dans les Jeux {\`a} Information Imparfaite}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2016, month = nov, url = {http://www.lsv.fr/Publis/PAPERS/PDF/mvdb-phd16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/mvdb-phd16.pdf} }

@mastersthesis{m2-jacomme, author = {Jacomme, Charlie}, title = {Automated applications of Cryptographic Assumptions}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2016}, month = sep, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-jacomme.pdf} }

@mastersthesis{m2-lehaut, author = {Lehaut, Mathieu}, title = {PDL on infinite alphabet}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2016}, month = aug, url = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-lehaut.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-lehaut.pdf}, note = {19~pages} }

@article{DH-jlamp16, publisher = {Elsevier Science Publishers}, journal = {Journal of Logic and Algebraic Methods in Programming}, author = {Delaune, St{\'e}phanie and Hirschi, Lucca}, title = {A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols}, volume = {87}, year = {2016}, pages = {127-144}, url = {http://www.sciencedirect.com/science/article/pii/S235222081630133X}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DH-jlamp16.pdf}, doi = {10.1016/j.jlamp.2016.10.005}, note = {To~appear}, abstract = {Cryptographic protocols aim at securing communications over insecure networks such as the Internet, where dishonest users may listen to communications and interfere with them. A secure communication has a different meaning depending on the underlying application. It ranges from the confidentiality of a data to e.g. verifiability in electronic voting systems. Another example of a security notion is privacy. Formal symbolic models have proved their usefulness for analysing the security of protocols. Until quite recently, most results focused on trace properties like confidentiality or authentication. There are however several security properties, which cannot be defined (or cannot be naturally defined) as trace properties and require a notion of behavioural equivalence. Typical examples are anonymity, and privacy related properties. During the last decade, several results and verification tools have been developed to analyse equivalence-based security properties. We propose here a synthesis of decidability and undecidability results for equivalence-based security properties. Moreover, we give an overview of existing verification tools that may be used to verify equivalence-based security properties.} }

@techreport{BGMS-arxiv16, author = {Beame, Paul and Grosshans, Nathan and McKenzie, Pierre and Segoufin, Luc}, title = {Nondeterminism and an abstract formulation of {N}eciporuk's lower bound method}, institution = {Computing Research Repository}, number = {1608.01932}, year = {2016}, url = {http://arxiv.org/abs/1608.01932}, pdf = {http://arxiv.org/abs/1608.01932}, month = aug, type = {Research Report}, note = {34~pages} }

@inproceedings{MPAS-cikm16, address = {Indianapolis, Indiana, USA}, month = oct, publisher = {ACM}, acronym = {{CIKM}'16}, booktitle = {{P}roceedings of the 25th {ACM} {I}nternational {C}onference on {I}nformation and {K}nowledge {M}anagement ({CIKM}'16)}, author = {Montoya, David and Pellissier Tanon, Thomas and Abiteboul, Serge and Suchanek, Fabian}, title = {{T}hymeflow, {A} {P}ersonal {K}nowledge {B}ase with {S}patio-temporal {D}ata}, pages = {2477-2480}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/MPAS-cikm16.pdf}, year = {2016}, doi = {10.1145/2983323.2983337}, abstract = {The typical Internet user has data spread over several devices and across several online systems. We demonstrate an open-source system for integrating user's data from dierent sources into a single Knowledge Base. Our system integrates data of dierent kinds into a coherent whole, starting with email messages, calendar, contacts, and location history. It is able to detect event periods in the user's location data and align them with calendar events. We will demonstrate how to query the system within and across dierent dimensions, and perform analytics over emails, events, and locations.} }

@mastersthesis{m2-lick, author = {Lick, Anthony}, title = {Syst{\`e}mes de preuves pour logiques modales}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2016}, month = aug, url = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-lick.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-lick.pdf}, note = {20~pages} }

@phdthesis{blondin-phd2016, author = {Blondin, Michael}, title = {Algorithmique et complexit{\'e} des syst{\`e}mes {\`a} compteurs}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France and Universit{\'e} de Montr{\'e}al}, type = {Th{\`e}se de doctorat}, year = {2016}, month = jun, url = {https://tel.archives-ouvertes.fr/tel-01359000/} }

@phdthesis{mohamed-PhD16, author = {Mohamed, Sameh}, title = {Une m{\'e}thode topologique pour la recherche d'ensembles invariants de syst{\`e}mes continus et {\`a} commutation}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = {2016}, month = oct, url = {http://www.lsv.fr/Publis/PAPERS/PDF/mohamed-phd16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/mohamed-phd16.pdf} }

@phdthesis{C-phd2016, author = {Cauderlier, Rapha{\"e}l}, title = {{Object-Oriented Mechanisms for Interoperability between Proof Systems}}, school = {{Conservatoire National Des Arts et M{\'e}tiers, Paris}}, type = {Th{\`e}se de doctorat}, year = 2016, month = oct, url = {https://hal.inria.fr/tel-01415945/}, pdf = {https://hal.inria.fr/tel-01415945/file/main.pdf} }

@book{DGL-cup2016, author = {Demri, St{\'e}phane and Goranko, Valentin and Lange, Martin}, title = {{T}emporal {L}ogics in {C}omputer {S}cience}, publisher = {Cambridge University Press}, series = {Cambridge Tracts in Theoretical Computer Science}, volume = {58}, year = {2016}, month = oct, url = {http://www.cambridge.org/9781107028364}, isbn = {9781107028364} }

@inproceedings{HHKLL-syncop16, address = {Eindhoven, The Netherlands}, month = apr, year = 2016, volume = 220, series = {Electronic Proceedings in Theoretical Computer Science}, acronym = {{C}assting/{SYNCOP}'16}, booktitle = {{P}roceedings of the {C}assting {W}orkshop on {G}ames for the {S}ynthesis of {C}omplex {S}ystems and 3rd {I}nternational {W}orkshop on {S}ynthesis of {C}omplex {P}arameters ({C}assting/{SYNCOP}'16)}, author = {Hutagalung, Milka and Hundeshagen, Norbert and Kuske, Dietrich and Lange, Martin and Lozes, {\'{E}}tienne}, title = {Two-Buffer Simulation Games}, pages = {213-227}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/HHKLL-syncop16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HHKLL-syncop16.pdf}, doi = {10.4204/EPTCS.220.3}, abstract = {We consider simulation games played between Spoiler and Duplicator on two B{\"u}chi automata in which the choices made by Spoiler can be buffered by Duplicator in two different buffers before she executes them on her structure. Previous work on such games using a single buffer has shown that they are useful to approximate language inclusion problems. We study the decidability and complex- ity and show that games with two buffers can be used to approximate corresponding problems on finite transducers, i.e. the inclusion problem for rational relations over infinite words.} }

@inproceedings{HHKLL-gandalf16, address = {Catania, Italy}, month = sep, year = 2016, volume = {226}, series = {Electronic Proceedings in Theoretical Computer Science}, editor = {Cantone, Domenico and Delzanno, Giorgio}, acronym = {{GandALF}'16}, booktitle = {{P}roceedings of the 7th {I}nternational {S}ymposium on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification ({GandALF}'16)}, author = {Hutagalung, Milka and Hundeshagen, Norbert and Kuske, Dietrich and Lange, Martin and Lozes, {\'{E}}tienne}, title = {Multi-Buffer Simulations for Trace Language Inclusion}, pages = {213-227}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/HHKLL-gandalf16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HHKLL-gandalf16.pdf}, doi = {10.4204/EPTCS.226.15}, abstract = {We consider simulation games played between Spoiler and Duplicator on two B{\"u}chi automata in which the choices made by Spoiler can be buffered by Duplicator in several buers before she executes them on her structure. We show that the simulation games are useful to approximate the inclusion of trace closures of languages accepted by finite-state automata, which is known to be undecidable. We study the decidability and complexity and show that the game with bounded buffers can be decided in polynomial time, whereas the game with one unbounded and one bounded buffer is highly undecidable. We also show some sufficient conditions on the automata for Duplicator to win the game (with unbounded buffers).} }

@inproceedings{Halmagrand-ictac16, address = {Taipei, Taiwan}, month = oct, volume = 9965, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Alves Sampaio, Cesar and Wang, Farn}, acronym = {{ICTAC}'16}, booktitle = {{P}roceedings of the 13th {I}nternational {C}olloquium on {T}heoretical {A}spects of {C}omputing ({ICTAC}'16)}, author = {Halmagrand, Pierre}, title = {{{Soundly Proving B Method Formulae Using Typed Sequent Calculus}}}, pages = {196-213}, year = {2016}, doi = {10.1007/978-3-319-46750-4_12}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Halmagrand-ictac2016.pdf}, url = {https://hal.archives-ouvertes.fr/hal-01342849}, abstract = {The B Method is a formal method mainly used in the railway industry to specify and develop safety-critical software. To guarantee the consistency of a B project, one decisive challenge is to show correct a large amount of proof obligations, which are mathematical formulae expressed in a classical set theory extended with a specific type system. To improve automated theorem proving in the B Method, we propose to use a first-order sequent calculus extended with a polymorphic type system, which is in particular the output proof-format of the tableau-based automated theorem prover Zenon. After stating some modifications of the B syntax and defining a sound elimination of comprehension sets, we propose a translation of B formulae into a polymorphic first-order logic format. Then, we introduce the typed sequent calculus used by Zenon, and show that Zenon proofs can be translated to proofs of the initial B formulae in the B proof system.} }

@techreport{PS-arxiv16, author = {Place, Thomas and Segoufin, Luc}, title = {Decidable Characterization of FO2(<, +1) and locality of {DA}}, institution = {Computing Research Repository}, number = {1606.03217}, year = {2016}, url = {http://arxiv.org/abs/1606.03217}, pdf = {http://arxiv.org/abs/1606.03217}, month = jun, type = {Research Report}, note = {8~pages} }

@article{JSD-lmcs16, journal = {Logical Methods in Computer Science}, author = {Jacquemard, Florent and Segoufin, Luc and Dimino, Jer{\'{e}}mie}, title = {FO2(<, +1,{\textasciitilde}) on data trees, data tree automata and branching vector addition systems}, volume = {12}, number = {2}, pages = {1-28}, year = {2016}, url = {http://www.lmcs-online.org/ojs/viewarticle.php?id=1789&layout=abstract}, doi = {10.2168/LMCS-12(2:3)2016}, pdf = {https://arxiv.org/pdf/1601.01579.pdf}, abstract = {} }

@techreport{arxiv16-BFMK, author = {Blondin, Michael and Finkel, Alain and McKenzie, Pierre}, title = {Well Behaved Transition Systems}, institution = {Computing Research Repository}, number = {1608.02636}, year = {2016}, month = aug, type = {Research Report}, url = {http://arxiv.org/abs/1608.02636}, pdf = {http://arxiv.org/abs/1608.02636}, note = {18~pages}, abstract = {The well-quasi-ordering (i.e., a well-founded quasi-ordering such that all antichains are finite) that defines well-structured transition systems (WSTS) is shown not to be the weakest hypothesis that implies decidability of the coverability problem. We show coverability decidable for monotone transition systems that only require the absence of infinite antichains and call well behaved transitions systems (WBTS) the new strict superclass of the class of WSTS that arises. By contrast, we confirm that boundedness and termination are undecidable for WBTS under the usual hypotheses, and show that stronger monotonicity conditions can enforce decidability. Proofs are similar or even identical to existing proofs but the surprising message is that a hypothesis implicitely assumed minimal for twenty years in the theory of WSTS can meaningfully be relaxed, allowing more orderings to be handled in an abstract way.} }

@inproceedings{vDCC-EMISA16, address = {Vienna, Austria}, month = oct, publisher = {{CEUR-WS.org}}, volume = {1701}, series = {{CEUR} Workshop Proceedings}, editor = {Rinderle-Ma, Stefanie and Mendling, Jan}, acronym = {{EMISA}'16}, booktitle = {{P}roceedings of the 7th {I}nt. {W}orkshop on {E}nterprise {M}odelling and {I}nformation {S}ystems {A}rchitectures ({EMISA}'16)}, author = {van Dongen, Boudewijn and Carmona, Josep and Chatain, {\relax Th}omas}, title = {{Alignment-based Quality Metrics in Conformance Checking}}, pages = {87-90}, year = {2016}, doi = {}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/vanDongen-EMISA16.pdf}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/vanDongen-EMISA16.pdf}, abstract = {The holy grail in process mining is a process discovery algorithm that, given an event log, produces fitting, precise, properly generalizing and simple process models. Within the field of process mining, conformance checking is considered to be anything where observed behaviour, e.g., in the form of event logs or event streams, needs to be related to already modelled behaviour. In the conformance checking domain, the relation between an event log and a model is typically quantified using fitness, precision and generalization. In this paper, we present metrics for fitness, precision and generalization, based on alignments and the newer concept named anti-alignments.} }

@article{GLSSW-dagrep16, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, journal = {Dagstuhl Reports}, author = {Goubault{-}Larrecq, Jean and Seisenberger, Monika and Selivanov, Victor and Weiermann, Andreas}, title = {Well {Q}uasi-{O}rders in {C}omputer {S}cience ({D}agstuhl {S}eminar 16031)}, year = 2016, month = jan, volume = {6}, number = {1}, pages = {69-98}, url = {http://dx.doi.org/10.4230/DagRep.6.1.69}, pdf = {http://dx.doi.org/10.4230/DagRep.6.1.69}, doi = {10.4230/DagRep.6.1.69}, abstract = {This report documents the program and the outcomes of Dagstuhl Seminar 16031 {"}Well Quasi{-}Orders in Computer Science{"}, the first seminar devoted to the multiple and deep interactions between the theory of Well quasi{-}orders (known as the Wqo{-}Theory) and several fields of Computer Science (Verification and Termination of Infinite-State Systems, Automata and Formal Languages, Term Rewriting and Proof Theory, topological complexity of computational problems on continuous functions). Wqo{-}Theory is a highly developed part of Combinatorics with ever-growing number of applications in Mathematics and Computer Science, and Well quasi-orders are going to become an important unifying concept of Theoretical Computer Science. In this seminar, we brought together several communities from Computer Science and Mathematics in order to facilitate the knowledge transfer between Mathematicians and Computer Scientists as well as between established and younger researchers and thus to push forward the interaction between Wqo{-}Theory and Computer Science.} }

@inproceedings{MHP-HSB16, address = {Grenoble France}, month = oct, optvolume = 9957, series = {Lecture Notes in Computer Science}, publisher = {Springer}, opteditor = {Cinquemani, Eugenio and Donz{\'{e}, Alexandre}}, acronym = {{HSB}'16}, booktitle = {{P}roceedings of the 5th {I}nternational {W}orkshop on {H}ybrid {S}ystems {B}iology}, author = {Mandon, Hugues and Haar, Stefan and Paulev{\'e}, Lo{\"i}c}, title = {{Relationship between the Reprogramming Determinants of Boolean Networks and their Interaction Graph}}, pages = {113-127}, year = {2016}, doi = {10.1007/978-3-319-47151-8_8}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/MHP-HSB16.pdf}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/MHP-HSB16.pdf}, abstract = {In this paper, we address the formal characterization of tar- gets triggering cellular trans-differentiation in the scope of Boolean net- works with asynchronous dynamics. Given two fixed points of a Boolean network, we are interested in all the combinations of mutations which allow to switch from one fixed point to the other, either possibly, or in- evitably. In the case of existential reachability, we prove that the set of nodes to (permanently) flip are only and necessarily in certain connected components of the interaction graph. In the case of inevitable reachabil- ity, we provide an algorithm to identify a subset of possible solutions.} }

@inproceedings{GLL-rv16, address = {Madrid, Spain}, volume = 10012, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Madrid, Spain}, acronym = {{RV}'16}, booktitle = {{P}roceedings of the 16th {C}onference on {R}untime {V}erification ({RV}'16)}, author = {Goubault{-}Larrecq, Jean and Lachance, Jean{-}Philippe}, title = {On the {C}omplexity of {M}onitoring {O}rchids {S}ignatures}, year = 2016, month = sep, pages = {169-164}, opturl = {http://link.springer.com/chapter/10.1007%2F978-3-319-46982-9_11}, optpdf = {http://link.springer.com/chapter/10.1007%2F978-3-319-46982-9_11}, doi = {10.1007/978-3-319-46982-9_11}, abstract = {Modern monitoring tools such as our intrusion detection tool Orchids work by firing new monitor instances dynamically. Given an Orchids signature (a.k.a. a rule, a specification), what is the complexity of checking that specification, that signature? In other words, let f(n) be the maximum number of monitor instances that can be fired on a sequence of n events: we design an algorithm that decides whether f(n) is asymptotically exponential or polynomial, and in the latter case returns an exponent d such that f(n)=Theta(n^d) . Ultimately, the problem reduces to the following mathematical question, which may have other uses in other domains: given a system of recurrence equations described using the operators + and max, and defining integer sequences u_n, what is the asymptotic behavior of u_n as n tends to infinity? We show that, under simple assumptions, u_n is either exponential or polynomial, and that this can be decided, and the exponent computed, using a simple modification of Tarjanâ€™s strongly connected components algorithm, in linear time.} }

@inproceedings{KSHP-sasb16, address = {Edinburgh, UK}, month = sep, missingnumber = {2}, missingvolume = {}, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier Science Publishers}, acronym = {{SASB}'16}, booktitle = {{P}roceedings of {T}he {S}eventh {I}nternational {W}orkshop on {S}tatic {A}nalysis and {S}ystems {B}iology (SASB 2016)}, title = {{Unfolding of Parametric Logical Regulatory Networks}}, author = {Kolc{\'a}k, Juraj and {\v S}afr{\'a}nek, David and Haar, Stefan and Paulev{\'e}, Lo{\"i}c}, year = {2016}, note = {To appear}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KSHP-SASB16.pdf}, url = {https://hal.archives-ouvertes.fr/hal-01354109}, abstract = {In systems biology, models of cellular regulatory processes such as gene regulatory networks or signalling pathways are crucial to understanding the behaviour of living cells. Available biological data are however often insufficient for full model specification. In this paper, we focus on partially specified models where the missing information is abstracted in the form of parameters. We introduce a novel approach to analysis of parametric logical regulatory networks addressing both sources of combinatoric explosion native to the model. First, we introduce a new compact representation of admissible parameters using Boolean lattices. Then, we define the unfolding of parametric regulatory networks. The resulting structure provides a partial- order reduction of concurrent transitions, and factorises the common transitions among the concrete models. A comparison is performed against state-of-the-art approaches to parametric model analysis.} }

@article{KGHPAJRHH-tpnomc2016, publisher = {Springer}, journal = {Transactions on Petri Nets and Other Models of Concurrency}, author = {Kordon, Fabrice and Garavel, Hubert and Hillah, Lom{-}Messan and Paviot{-}Adet, Emmanuel and Jezequel, Lo{\"{\i}}g and Rodr{\'{\i}}guez, C{\'{e}}sar and Hulin{-}Hubard, Francis }, title = {{MCC}'2015 - {T}he {F}ifth {M}odel {C}hecking {C}ontest}, volume = {11}, pages = {262-273}, year = {2016}, url = {http://dx.doi.org/10.1007/978-3-662-53401-4_12}, doi = {10.1007/978-3-662-53401-4_12}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KGHPAJRHH-tpnomc2016.pdf} }

@article{ADFLP-fi2016, publisher = {{IOS} Press}, journal = {Fundamenta Informaticae}, author = {Abdulla, Parosh Aziz and Demri, St{\'e}phane and Finkel, Alain and Leroux, J{\'e}r{\^o}me and Potapov, Igor}, editor = {Abdulla, Parosh Aziz and Demri, St{\'e}phane and Finkel, Alain and Leroux, J{\'e}r{\^o}me and Potapov, Igor}, number = {3--4}, title = {Selected papers of Reachability Problems Workshop 2012 (Bordeaux) and 2013 (Uppsala)}, url = {http://content.iospress.com/journals/fundamenta-informaticae/143/3-4}, volume = {143}, year = {2016} }

@proceedings{BDM-aiml16, title = {{P}roceedings of the 11th {C}onference on {A}dvances in {M}odal {L}ogic ({AiML}'16)}, booktitle = {{P}roceedings of the 11th {C}onference on {A}dvances in {M}odal {L}ogic ({AiML}'16)}, acronym = {{AiML}'16}, editor = {Beklemishev, Lev and Demri, St{\'e}phane and Mat{\'e}, Andr{\'a}s}, publisher = {College Publications}, year = 2016, month = sep, address = {Budapest, Hungary}, url = {http://www.collegepublications.co.uk/aiml/?00008} }

@inproceedings{Bollig-fsttcs16, address = {Chennai, India}, month = dec, year = 2016, volume = {65}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {S. Akshay and Akash Lal and Saket Saurabh and Sandeep Sen}, acronym = {{FSTTCS}'16}, booktitle = {{P}roceedings of the 36th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'16)}, author = {Bollig, Benedikt}, title = {One-Counter Automata with Counter Observability}, pages = {20:1-20:14}, url = {http://drops.dagstuhl.de/opus/volltexte/2016/6855/}, doi = {10.4230/LIPIcs.FSTTCS.2016.20}, abstract = {In a one-counter automaton (OCA), one can produce a letter from some finite alphabet, increment and decrement the counter by one, or compare it with constants up to some threshold. It is well-known that universality and language inclusion for OCAs are undecidable. In this paper, we consider OCAs with counter observability: 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 PSPACE-complete, thus no harder than the corresponding problems for finite automata. In fact, by establishing a link with visibly one-counter automata, we show that OCAs with counter observability are effectively determinizable and closed under all boolean operations. Moreover, it turns out that they are expressively equivalent to strong automata, in which transitions are guarded by MSO formulas over the natural numbers with successor.} }

@proceedings{FM-formats16, title = {{P}roceedings of the 14th {I}nternational {C}onference on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'16)}, booktitle = {{P}roceedings of the 14th {I}nternational {C}onference on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'16)}, acronym = {{FORMATS}'16}, editor = {Fr{\"a}nzle, Martin and Markey, Nicolas}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {9884}, doi = {10.1007/978-3-319-44878-7}, url = {http://link.springer.com/book/10.1007/978-3-319-44878-7}, year = 2016, month = aug, address = {Qu\'ebec City, Canada} }

@proceedings{BDJMS-casstingsyncop16, title = {{P}roceedings of the {C}assting Workshop on {G}ames for the {S}ynthesis of {C}omplex {S}ystems ({C}assting'16) and of the 3rd {I}nternational {W}orkshop on {S}ynthesis of {C}omplex {P}arameters ({S}yn{C}o{P}'16)}, booktitle = {{P}roceedings of the {C}assting Workshop on {G}ames for the {S}ynthesis of {C}omplex {S}ystems ({C}assting'16) and of the 3rd {I}nternational {W}orkshop on {S}ynthesis of {C}omplex {P}arameters ({S}yn{C}o{P}'16)}, acronym = {{C}assting{{\slash}}{S}yn{C}o{P}'16}, editor = {Brihaye, {\relax Th}omas and Delahaye, Beno{\^\i}t and Jezequel, Lo{\"\i}g and Markey, Nicolas and Srba, Ji{\v{r}}{\'i}}, doi = {10.4204/EPTCS.220}, url = {http://eptcs.web.cse.unsw.edu.au/content.cgi?CASSTINGSynCoP2016}, series = {Electronic Proceedings in Theoretical Computer Science}, volume = 220, year = 2016, month = jul, address = {Eindhoven, The~Netherlands} }

@inproceedings{BMS-gandalf16, address = {Catania, Italy}, month = sep, year = 2016, volume = {226}, series = {Electronic Proceedings in Theoretical Computer Science}, editor = {Cantone, Domenico and Delzanno, Giorgio}, acronym = {{GandALF}'16}, booktitle = {{P}roceedings of the 7th {I}nternational {S}ymposium on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification ({GandALF}'16)}, author = {Bouyer, Patricia and Markey, Nicolas and Stan, Daniel}, title = {Stochastic Equilibria under Imprecise Deviations in Terminal-Reward Concurrent Games}, pages = {61-75}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-gandalf16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-gandalf16.pdf}, doi = {10.4204/EPTCS.226.5}, abstract = {We study the existence of mixed-strategy equilibria in concurrent games played on graphs. While existence is guaranteed with safety objectives for each player, Nash equilibria need not exist when players are given arbitrary terminal-reward objectives, and their existence is undecidable with qualitative reachability objectives (and~only three players). However, these results rely on the fact that the players can enforce infinite plays while trying to improve their payoffs. In this paper, we introduce a relaxed notion of equilibria, where deviations are imprecise. We prove that contrary to Nash equilibria, such (stationary) equilibria always exist, and we develop a PSPACE algorithm to compute one.} }

@inproceedings{Finkel-rp16, address = {Aalborg, Denmark}, month = sep, year = 2016, volume = {9899}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Larsen, Kim G. and Srba, Ji{\v{r}}{\'\i}}, acronym = {{RP}'16}, booktitle = {{P}roceedings of the 10th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'16)}, author = {Finkel, Alain}, title = {The Ideal Theory for {WSTS}}, pages = {1-22}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/Finkel-rp16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Finkel-rp16.pdf}, doi = {10.1007/978-3-319-45994-3_1}, abstract = {We begin with a survey on well structured transition systems and, in particular, we present the ideal framework [FG09a, BFM14] which was recently used to obtain new deep results on Petri nets and extensions. We argue that the theory of ideals prompts a renewal of the theory of WSTS by providing a way to define a new class of monotonic systems, the so-called Well Behaved Transition Systems, which properly contains WSTS, and for which coverability is still decidable by a forward algorithm. We then recall the completion of WSTS which leads to defining a conceptual Karp-Miller procedure that terminates in more cases than the generalized Karp-Miller procedure on extensions of Petri nets.} }

@inproceedings{ABDL-rp16, address = {Aalborg, Denmark}, month = sep, year = 2016, volume = {9899}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Larsen, Kim G. and Srba, Ji{\v{r}}{\'\i}}, acronym = {{RP}'16}, booktitle = {{P}roceedings of the 10th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'16)}, author = {Alechina, Natasha and Bulling, Nils and Demri, St{\'e}phane and Logan, Brian}, title = {On the Complexity of Resource-Bounded Logics}, pages = {36-50}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABDL-rp16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABDL-rp16.pdf}, doi = {10.1007/978-3-319-45994-3_3}, abstract = {We revisit decidability results for resource-bounded logics and use decision problems on VASS to establish complexity characterisation of (decidable) model-checking problems. We show that the model-checking problem for the logic RB\(\pm\)ATL is 2EXPTIME-complete by using recent results on alternating VASS. Moreover, we establish that the model-checking problem for RBTL is EXPSPACE-complete and that the problem is decidable and of the same complexity for RBTL\textsuperscript{*}, proving a new decidability result as a by-product of the approach. We establish that the model-checking problem for RB\(\pm\)ATL\textsuperscript{*}, the extension of RB\(\pm\)ATL with arbitrary path formulae is decidable by a reduction into parity games. We are also able to synthesise values for resource parameters. Hence, the paper establishes formal correspondences between model-checking problems and decision problems on alternating VASS, paving the way to more applications.} }

@inproceedings{LFS-rp16, address = {Aalborg, Denmark}, month = sep, year = 2016, volume = {9899}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Larsen, Kim G. and Srba, Ji{\v{r}}{\'\i}}, acronym = {{RP}'16}, booktitle = {{P}roceedings of the 10th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'16)}, author = {Le{~}Co{\"e}nt, Adrien and Fribourg, Laurent and Soulat, Romain}, title = {Compositional analysis of Boolean networks using local fixed-point iterations}, pages = {134-147}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LFS-rp16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LFS-rp16.pdf}, doi = {10.1007/978-3-319-45994-3_10}, abstract = {We present a compositional method which allows to over-approximate the set of attractors and under-approximate the set of basins of attraction of a Boolean network~(BN). This merely consists in replacing a global fixed-point computation by a composition of local fixed-point computations. Once these approximations have been computed, it~becomes much more tractable to generate the exact sets of attractors and basins of attraction. We illustrate the interest of our approach on several examples, among which is a BN modeling a railway interlocking system with 50 nodes and millions of attractors.} }

@inproceedings{LFMDC-rp16, address = {Aalborg, Denmark}, month = sep, year = 2016, volume = {9899}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Larsen, Kim G. and Srba, Ji{\v{r}}{\'\i}}, acronym = {{RP}'16}, booktitle = {{P}roceedings of the 10th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'16)}, author = {Le{~}Co{\"e}nt, Adrien and Fribourg, Laurent and Markey, Nicolas and De{~}Vuyst, Florian and Chamoin, Ludovic}, title = {Distributed Synthesis of State-Dependent Switching Control}, pages = {119-133}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LFMDC-rp16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LFMDC-rp16.pdf}, doi = {10.1007/978-3-319-45994-3_9}, abstract = {We present a correct-by-design method of state-dependent control synthesis for linear discrete-time switching systems. Given an objective region~\(R\) of the state space, the method builds a capture set~\(S\) and a control which steers any element of~\(S\) into~\(R\). The method works by iterated backward reachability from~\(R\). More precisely, \(S\)~is given as a parametric extension of~\(R\), and the maximum value of the parameter is solved by linear programming. The method can also be used to synthesize a stability control which maintains indefinitely within~\(R\) all the states starting at~\(R\). We~explain how the synthesis method can be performed in a distributed manner. The method has been implemented and successfully applied to the synthesis of a distributed control of a concrete floor heating system with 11 rooms and \(2^11 = 2048\) switching modes.} }

@inproceedings{HT-pasm16, address = {M{\"u}nster, Germany}, month = apr, year = 2016, volume = {327}, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier Science Publishers}, editor = {Haverkort, Boudewijn and Knottenbelt, William and Remke, Anne and Thomas, Nigel}, booktitle = {{P}roceedings of the 8th {I}nternational {W}orkshop on {P}ractical {A}pplications of {S}tochastic {M}odelling ({PASM}'16)}, author = {Haar, Stefan and Theissing, Simon}, title = {Forecasting Passenger Loads in Transportation Networks}, pages = {49-69}, url = {https://hal.inria.fr/hal-01259585}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HT-pasm16.pdf}, doi = {10.1016/j.entcs.2016.09.023}, abstract = {This work is part of an ongoing effort to understand the dynamics of passenger loads in modern, multimodal transportation networks (TNs) and to mitigate the impact of perturbations. The challenge is that the percentage of passengers at any given point of the TN that have a certain destination, i.e. their distribution over different trip profiles, is unknown. We introduce a stochastic hybrid automaton model for multimodal TNs that allows to compute how such probabilistic load vectors are propagated through the TN, and develop a computation strategy for forecasting the network's load a certain time into the future.} }

@misc{vip-D42, author = {Delaune, St{\'e}phanie and Gazeau, Ivan}, howpublished = {Deliverable VIP~4.2 (ANR-11-JS02-0006)}, month = jun, note = {5~pages}, type = {Contract Report}, title = {Combination issues}, year = {2016}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/vip-d42.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/vip-d42.pdf} }

@misc{vip-D22, author = {Delaune, St{\'e}phanie and Gazeau, Ivan}, howpublished = {Deliverable VIP~2.2 (ANR-11-JS02-0006)}, month = jun, note = {8~pages}, type = {Contract Report}, title = {Results on the case studies}, year = {2016}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/vip-d22.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/vip-d22.pdf} }

@techreport{HT-hal16, author = {Haar, Stefan and Theissing, Simon}, title = {A~Passenger-centric Multi-agent System Model for Multimodal Public Transportation}, institution = {HAL-inria}, number = {hal-01322956}, month = may, year = {2016}, type = {Research Report}, url = {https://hal.inria.fr/hal-01322956}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HT-hal16.pdf}, note = {12~pages}, abstract = {If we want to understand how perturbations spread across a multi-modal public transportation system, we have to include passenger flows into the model and the analysis. Indeed, in general no two different lines in such a system are physically connected directly, or share tracks or other resources. Rather, they are connected by passengers changing lines and thus transmit perturbations from one line or mode to another. We present a formal passenger-centric multi-agent system model that can capture (i)~individual and possibly multi-modal trip profiles with branches resulting from different decision outcomes, (ii)~the~movement of fixed-route operated transportation means, and (iii)~in-vehicle and in-station capacity constraints. The model is based on a nets-within-nets approach with Petri nets as the basic building entities. Thus, it has a convenient graphical representation, and the possibility of execution.} }

@inproceedings{HT-qest16, address = {Qu{\'e}bec City, Canada}, month = aug, year = 2016, volume = {9826}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Agha, Gul and Van{~}Houdt, Benny}, acronym = {{QEST}'16}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {Q}uantitative {E}valuation of {S}ystems ({QEST}'16)}, author = {Haar, Stefan and Theissing, Simon}, title = {Decoupling Passenger Flows for Improved Load Prediction}, pages = {364-379}, url = {https://hal.inria.fr/hal-01330136}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HT-qest16.pdf}, doi = {10.1007/978-3-319-43425-4_24}, abstract = {This paper continues our work on perturbation analysis of multimodal transportation networks~(TNs) by means of a stochastic hybrid automaton~(SHA) model. We focus here on the approximate computation , in particular on the major bottleneck consisting in the high dimensionality of systems of stochastic differential balance equations (SDEs) that define the continuous passenger-flow dynamics in the different modes of the SHA model. In fact, for every pair of a mode and a station, one system of coupled SDEs relates the passenger loads of all discrete points such as platforms considered in this station, and all vehicles docked to it, to the passenger flows in between. In general, such an SDE system has many dimensions, which makes its numerical computation and thus the approximate computation of the SHA model intractable. We show how these systems can be canonically replaced by lower-dimensional ones, by decoupling the passenger flows inside every mode from one another. We prove that the resulting approximating passenger-flow dynamics converges to the original one, if the replacing set of balance equations set up for all decoupled passenger flows communicate their results among each other in vanishing time intervals.} }

@inproceedings{HT-acc16, address = {Boston, Massachusetts, USA}, month = jul, year = 2016, publisher = {{IEEE} Control System Society}, acronym = {{ACC}'16}, booktitle = {{P}roceedings of the 35th {A}merican {C}ontrol {C}onference ({ACC}'16)}, author = {Haar, Stefan and Theissing, Simon}, title = {Predicting Traffic Load in Public Transportation Networks}, pages = {821-826}, url = {https://hal.inria.fr/hal-01329632}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HT-acc16.pdf}, doi = {10.1109/ACC.2016.7525015}, abstract = {This work is part of an ongoing effort to understand the dynamics of passenger loads in modern, multimodal transportation networks (TNs) and to mitigate the impact of perturbations, under the restrictions that the precise number of passengers in some point of the TN that intend to reach a certain destination (i.e. their distribution over different trip profiles) is unknown. We introduce an approach based on a stochastic hybrid automaton model for a TN that allows to compute how such probabilistic load vectors are propagated through the TN, and develop a computation strategy for forecasting the network's load a certain time in the future.} }

@inproceedings{FHLM-wodes16, address = {Xi'an, China}, month = may # {-} # jun, year = 2016, publisher = {{IEEE} Control System Society}, editor = {Cassandras, Christos G. and Giua, Alessandro}, acronym = {{WODES}'16}, booktitle = {{P}roceedings of the 13th {W}orkshop on {D}iscrete {E}vent {S}ystems ({WODES}'16)}, author = {Fabre, {\'E}ric and H{\'e}lou{\"e}t, Lo{\"i}c and Lefaucheux, Engel and Marchand, Herv{\'e}}, title = {Diagnosability of Repairable Faults}, pages = {230-236}, url = {https://hal.inria.fr/hal-01302562}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FHLM-wodes16.pdf}, doi = {10.1109/WODES.2016.7497853}, abstract = {The diagnosis problem for discrete event systems consists in deciding whether some fault event occurred or not in the system, given partial observations on the run of that system. Diagnosability checks whether a correct diagnosis can be issued in bounded time after a fault, for all faulty runs of that system. This problem appeared two decades ago and numerous facets of it have been explored, mostly for permanent faults. It is known for example that diagnosability of a system can be checked in polynomial time, while the construction of a diagnoser is exponential. The present paper examines the case of transient faults, that can appear and be repaired. Diagnosability in this setting means that the occurrence of a fault should always be detected in bounded time, but also before the fault is repaired. Checking this notion of diagnosability is proved to be PSPACE-complete. It is also shown that faults can be reliably counted provided the system is diagnosable for faults and for repairs.} }

@inproceedings{vDCC-bpm16, address = {Rio de Janeiro, Brazil}, month = sep, year = 2016, volume = {9850}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {La{~}Rosa, Marcello and Loos, Peter and Pastor, Oscar}, acronym = {{BPM}'16}, booktitle = {{P}roceedings of the 14th {I}nternational {C}onference on {B}usiness {P}rocess {M}anagement ({BPM}'16)}, author = {van Dongen, Boudewijn F. and Carmona, Josep and Chatain, {\relax Th}omas}, title = {A Unified Approach for Measuring Precision and Generalization Based on Anti-Alignments}, pages = {39-56}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/vDCC-bpm16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/vDCC-bpm16.pdf}, doi = {10.1007/978-3-319-45348-4_3}, abstract = {The holy grail in process mining is an algorithm that, given an event log, produces fitting, precise, properly generalizing and simple process models. While there is consensus on the existence of solid metrics for fitness and simplicity, current metrics for precision and generalization have important flaws, which hamper their applicability in a general setting. In this paper, a novel approach to measure precision and generalization is presented, which relies on the notion of anti-alignments. An anti-alignment describes highly deviating model traces with respect to observed behavior. We propose metrics for precision and generalization that resemble the leave-one-out cross-validation techniques, where individual traces of the log are removed and the computed anti-alignment assess the model's capability to describe precisely or generalize the observed behavior.} }

@inproceedings{KS-csl16, address = {Marseille, France}, month = sep, year = 2016, volume = {62}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Regnier, Laurent and Talbot, Jean-Marc}, acronym = {{CSL}'16}, booktitle = {{P}roceedings of the 25th {A}nnual {EACSL} {C}onference on {C}omputer {S}cience {L}ogic ({CSL}'16)}, author = {Prateek Karandikar and Schnoebelen, {\relax Ph}ilippe}, title = {The height of piecewise-testable languages with applications in logical complexity}, pages = {37:1-37:22}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-csl16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-csl16.pdf}, doi = {10.4230/LIPIcs.CSL.2016.37}, abstract = {The height of a piecewise-testable language~\(L\) is the maximum length of the words needed to define~\(L\) by excluding and requiring given subwords. The height of~\(L\) is an important descriptive complexity measure that has not yet been investigated in a systematic way. This paper develops a series of new techniques for bounding the height of finite languages and of languages obtained by taking closures by subwords, superwords and related operations.\par As an application of these results, we show that \({\textsf{FO}}^2(A^*,\sqsubseteq)\), the two-variable fragment of the first-order logic of sequences with the subword ordering, can only express piecewise-testable properties and has elementary complexity.} }

@inproceedings{GGL-csl16, address = {Marseille, France}, month = sep, year = 2016, volume = {62}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Regnier, Laurent and Talbot, Jean-Marc}, acronym = {{CSL}'16}, booktitle = {{P}roceedings of the 25th {A}nnual {EACSL} {C}onference on {C}omputer {S}cience {L}ogic ({CSL}'16)}, author = {Ganardi, Moses and G{\"o}ller, Stefan and Lohrey, Markus}, title = {On the Parallel Complexity of Bisimulation over Finite Systems}, pages = {12:1-12:17}, doi = {10.4230/LIPIcs.CSL.2016.12}, abstract = {In this paper the computational complexity of the (bi)simulation problem over restricted graph classes is studied. For trees given as pointer structures or terms the (bi)simulation problem is complete for logarithmic space or NC\(^1\), respectively. This solves an open problem from Balc{\'a}zar, Gabarr{\'o}, and S{\'a}ntha. We also show that the simulation problem is P-complete even for graphs of bounded path-width.} }

@inproceedings{DGGL-csl16, address = {Marseille, France}, month = sep, year = 2016, volume = {62}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Regnier, Laurent and Talbot, Jean-Marc}, acronym = {{CSL}'16}, booktitle = {{P}roceedings of the 25th {A}nnual {EACSL} {C}onference on {C}omputer {S}cience {L}ogic ({CSL}'16)}, author = {Dubut, J{\'e}r{\'e}my and Goubault, {\'E}ric and Goubault{-}Larrecq, Jean}, title = {The Directed Homotopy Hypothesis}, pages = {9:1-9:16}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DBS-csl16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DBS-csl16.pdf}, doi = {10.4230/LIPIcs.CSL.2016.9}, abstract = {The homotopy hypothesis was originally stated by Grothendieck: topological spaces should be {"}equivalent{"} to (weak) infinite-groupoids, which give algebraic representatives of homotopy types. Much later, several authors developed geometrizations of computational models, e.g., for rewriting, distributed systems, (homotopy) type theory etc. But an essential feature in the work set up in concurrency theory, is that time should be considered irreversible, giving rise to the field of directed algebraic topology. Following the path proposed by Porter, we state here a directed homotopy hypothesis: Grandis' directed topological spaces should be {"}equivalent{"} to a weak form of topologically enriched categories, still very close to (infinite,1)-categories. We develop, as in ordinary algebraic topology, a directed homotopy equivalence and a weak equivalence, and show invariance of a form of directed homology.} }

@inproceedings{DBS-csl16, address = {Marseille, France}, month = sep, year = 2016, volume = {62}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Regnier, Laurent and Talbot, Jean-Marc}, acronym = {{CSL}'16}, booktitle = {{P}roceedings of the 25th {A}nnual {EACSL} {C}onference on {C}omputer {S}cience {L}ogic ({CSL}'16)}, author = {Amina Doumane and David Baelde and Alexis Saurin}, title = {Infinitary proof theory: the multiplicative additive case}, pages = {42:1-42:17}, doi = {10.4230/LIPIcs.CSL.2016.42}, abstract = {Infinitary and regular proofs are commonly used in fixed point logics. Being natural intermediate devices between semantics and traditional finitary proof systems, they are commonly found in completeness arguments, automated deduction, verification, etc. However, their proof theory is surprisingly underdeveloped. In particular, very little is known about the computational behavior of such proofs through cut elimination. Taking such aspects into account has unlocked rich developments at the intersection of proof theory and programming language theory. One would hope that extending this to infinitary calculi would lead, e.g., to a better understanding of recursion and corecursion in programming languages. Structural proof theory is notably based on two fundamental properties of a proof system: cut elimination and focalization. The first one is only known to hold for restricted (purely additive) infinitary calculi, thanks to the work of Santocanale and Fortier; the second one has never been studied in infinitary systems. In this paper, we consider the infinitary proof system muMALLi for multiplicative and additive linear logic extended with least and greatest fixed points, and prove these two key results. We thus establish muMALLi as a satisfying computational proof system in itself, rather than just an intermediate device in the study of finitary proof systems.} }

@inproceedings{BLS-hal15, address = {Marseille, France}, month = sep, year = 2016, volume = {62}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Regnier, Laurent and Talbot, Jean-Marc}, acronym = {{CSL}'16}, booktitle = {{P}roceedings of the 25th {A}nnual {EACSL} {C}onference on {C}omputer {S}cience {L}ogic ({CSL}'16)}, author = {Baelde, David and Lunel, Simon and Schmitz, Sylvain}, title = {A~Sequent Calculus for a Modal Logic on Finite Data Trees}, pages = {32:1-32:16}, url = {https://hal.inria.fr/hal-01191172}, doi = {10.4230/LIPIcs.CSL.2016.32}, abstract = {We investigate the proof theory of a modal fragment of XPath equipped with data (in)equality tests over finite data trees, i.e. over finite unranked trees where nodes are labelled with both a symbol from a finite alphabet and a single data value from an infinite domain. We present a sound and complete sequent calculus for this logic, which yields the optimal PSPACE complexity bound for its validity problem.} }

@inproceedings{Bouyer-mfcs16, address = {Krakow, Poland}, month = aug, year = 2016, volume = {58}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf}, acronym = {{MFCS}'16}, booktitle = {{P}roceedings of the 41st {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'16)}, author = {Bouyer, Patricia}, title = {Optimal Reachability in Weighted Timed Automata and Games}, pages = {3:1-3:3}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/bouyer-mfcs16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bouyer-mfcs16.pdf}, doi = {10.4230/LIPIcs.MFCS.2016.3}, abstract = {This is an overview of the invited talk delivered at the 41st International Symposium on Math- ematical Foundations of Computer Science (MFCS-2016).} }

@inproceedings{ABKMT-mfcs16, address = {Krakow, Poland}, month = aug, year = 2016, volume = {58}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf}, acronym = {{MFCS}'16}, booktitle = {{P}roceedings of the 41st {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'16)}, author = {Akshay, S. and Bouyer, Patricia and Krishna, Shankara Narayanan and Manasa, Lakshmi and Trivedi, Ashutosh }, title = {Stochastic Timed Games Revisited}, pages = {8:1-8:14}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABKMT-mfcs16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABKMT-mfcs16.pdf}, doi = {10.4230/LIPIcs.MFCS.2016.8}, abstract = {Stochastic timed games (STGs), introduced by Bouyer and Forejt, naturally generalize both continuous-time Markov chains and timed automata by providing a partition of the locations between those controlled by two players (Player Box and Player Diamond) with competing objectives and those governed by stochastic laws. Depending on the number of players---2,~1, or~0---subclasses of stochastic timed games are often classified as \(2\frac{1}{2}\)-player, \(1\frac{1}{2}\)-player, and \(\frac{1}{2}\)-player games where the \(\frac{1}{2}\) symbolizes the presence of the stochastic {"}nature{"} player. For STGs with reachability objectives it is known that \(1\frac{1}{2}\)-player one-clock STGs are decidable for qualitative objectives, and that \(2\frac{1}{2}\)-player three-clock STGs are undecidable for quantitative reachability objectives. This paper further refines the gap in this decidability spectrum. We show that quantitative reachability objectives are already undecidable for \(1\frac{1}{2}\)-player four-clock STGs, and even under the time-bounded restriction for \(2\frac{1}{2}\)-player five-clock~STGs. We~also obtain a class of \(1\frac{1}{2}\), \(2\frac{1}{2}\)-player STGs for which the quantitative reachability problem is decidable.} }

@inproceedings{NPR-mfcs16, address = {Krakow, Poland}, month = aug, year = 2016, volume = {58}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf}, acronym = {{MFCS}'16}, booktitle = {{P}roceedings of the 41st {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'16)}, author = {Reino Niskanen and Igor Potapov and Julien Reichert}, title = {Undecidability of Two-dimensional Robot Games}, pages = {73:1-73:13}, url = {http://arxiv.org/abs/1604.08779}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/NPR-mfcs16.pdf}, doi = {10.4230/LIPIcs.MFCS.2016.73}, abstract = {Robot game is a two-player vector addition game played on the integer lattice \(\mathbb{Z}^n\). Both players have sets of vectors and in each turn the vector chosen by a player is added to the current configuration vector of the game. One of the players, called Eve, tries to play the game from the initial configuration to the origin while the other player, Adam, tries to avoid the origin. The problem is to decide whether or not Eve has a winning strategy. In this paper we prove undecidability of the robot game in dimension two answering the question formulated by Doyen and Rabinovich in 2011 and closing the gap between undecidable and decidable cases.} }

@inproceedings{DGGL-concur16, address = {Qu{\'e}bec City, Canada}, month = aug, year = 2016, volume = {59}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Desharnais, Jos{\'e}e and Jagadeesan, Radha}, acronym = {{CONCUR}'16}, booktitle = {{P}roceedings of the 27th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'16)}, author = {Dubut, J{\'e}r{\'e}my and Goubault, {\'E}ric and Goubault{-}Larrecq, Jean}, title = {Bisimulations and unfolding in {{\(\mathcal{P}\)}}-accessible categorical models}, pages = {25:1-25:14}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DGGL-concur16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DGGL-concur16.pdf}, doi = {10.4230/LIPIcs.CONCUR.2016.25}, abstract = {We propose a categorical framework for bisimulations and unfoldings that unifies the classical approach from Joyal \emph{et~al.} via open maps and unfoldings. This is based on a notion of categories accessible with respect to a subcategory of path shapes, i.e., for which one can define a nice notion of trees as glueings of paths. We show that transition systems and presheaf models are instances of our framework. We also prove that in our framework, several notions of bisimulation coincide, in particular an {"}operational~one{"} akin to the standard definition in transition systems. Also, our notion of accessibility is preserved by coreflections. This also leads us to a notion of unfolding that behaves well in the accessible case: it~is a right adjoint and is a universal covering, i.e., it is initial among the morphisms that have the unique lifting property with respect to path shapes. As an application, we prove that the universal covering of a groupoid, a standard construction in algebraic topology, is an unfolding, when the category of path shapes is well chosen.} }

@inproceedings{AGS-concur16, address = {Qu{\'e}bec City, Canada}, month = aug, year = 2016, volume = {59}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Desharnais, Jos{\'e}e and Jagadeesan, Radha}, acronym = {{CONCUR}'16}, booktitle = {{P}roceedings of the 27th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'16)}, author = {Akshay, S. and Paul Gastin and Krishna, Shankara Narayanan}, title = {Analyzing Timed Systems Using Tree Automata}, pages = {27:1-27:14}, url = {http://arxiv.org/abs/1604.08443}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGS-concur16.pdf}, doi = {10.4230/LIPIcs.CONCUR.2016.27}, abstract = {Timed systems, such as timed automata, are usually analyzed using their operational semantics on timed words. The classical region abstraction for timed automata reduces them to (untimed) finite state automata with the same time-abstract properties, such as state reachability. We propose a new technique to analyze such timed systems using finite tree automata instead of finite word automata. The main idea is to consider timed behaviors as graphs with matching edges capturing timing constraints. Such graphs can be interpreted in trees opening the way to tree automata based techniques which are more powerful than analysis based on word automata. The technique is quite general and applies to many timed systems. In this paper, as an example, we develop the technique on timed pushdown systems, which have recently received considerable attention. Further, we also demonstrate how we can use it on timed automata and timed multi-stack pushdown systems (with boundedness restrictions).} }

@inproceedings{BHL-concur16, address = {Qu{\'e}bec City, Canada}, month = aug, year = 2016, volume = {59}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Desharnais, Jos{\'e}e and Jagadeesan, Radha}, acronym = {{CONCUR}'16}, booktitle = {{P}roceedings of the 27th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'16)}, author = {Nathalie Bertrand and Serge Haddad and Engel Lefaucheux}, title = {Diagnosis in Infinite-State Probabilistic Systems}, pages = {37:1-37:15}, url = {https://hal.inria.fr/hal-01334218}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHL-concur16.pdf}, doi = {10.4230/LIPIcs.CONCUR.2016.37}, abstract = {In a recent work, we introduced four variants of diagnosability (\textsf{FA}, \textsf{IA}, \textsf{FF},~\textsf{IF}) in (finite) probabilistic systems (pLTS) depending whether one considers (1)~finite or infinite runs and (2)~faulty or all runs. We studied their relationship and established that the corresponding decision problems are PSPACE-complete. A~key ingredient of the decision procedures was a characterisation of diagnosability by the fact that a random run almost surely lies in an open set whose specification only depends on the qualitative behaviour of the pLTS. Here we investigate similar issues for infinite pLTS. We~first show that this characterisation still holds for \textsf{FF}-diagnosability but with a~\(G_{\delta}\) set instead of an open set and also for \textsf{IF}-and \textsf{IA}-diagnosability when pLTS are finitely branching. We also prove that surprisingly \textsf{FA}-diagnosability cannot be characterised in this way even in the finitely branching case. Then we apply our characterisations for a partially observable probabilistic extension of visibly pushdown automata (POpVPA), yielding EXPSPACE procedures for solving diagnosability problems. In~addition, we~establish some computational lower bounds and show that slight extensions of POpVPA lead to undecidability.} }

@inproceedings{DLM-concur16, address = {Qu{\'e}bec City, Canada}, month = aug, year = 2016, volume = {59}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Desharnais, Jos{\'e}e and Jagadeesan, Radha}, acronym = {{CONCUR}'16}, booktitle = {{P}roceedings of the 27th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'16)}, author = {David, Am{\'e}lie and Laroussinie, Fran{\c{c}}ois and Markey, Nicolas}, title = {On~the expressiveness of~{QCTL}}, pages = {28:1-28:15}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DLM-concur16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DLM-concur16.pdf}, doi = {10.4230/LIPIcs.CONCUR.2016.28}, abstract = {QCTL extends the temporal logic CTL with quantification over atomic propositions. While the algorithmic questions for QCTL and its fragments with limited quantification depth are well-understood (e.g. satisfiability of QCTL\textsuperscript{\(k\)}, with at most \(k\) nested blocks of quantifiers, is \(k+1\)-EXPTIME-complete), very few results are known about the expressiveness of this logic. We~address such expressiveness questions in this paper. We first consider the \emph{distinguishing power} of these logics (i.e.,~their ability to separate models), their relationship with behavioural equivalences, and their ability to capture the behaviours of finite Kripke structures with so-called characteristic formulas. We then consider their \emph{expressive power} (i.e.,~their ability to express a property), showing that in terms of expressiveness the hierarchy QCTL\textsuperscript{\(k\)} collapses at level~2 (in~other terms, any~QCTL formula can be expressed using at most two nested blocks of quantifiers).} }

@inproceedings{GR-langonto16, address = {Portoro{\v{z}}, Slovenia}, editor = {Grci{\'c} Simeunovi, Larisa and Vintar, {\u{S}}pela and Khan, Fahad and Le{\'o}n Ara{\'u}z, Pilar and Faber, Pamela and Fontini, Francesca and Parvisi, Artemis and Unger, Christina}, acronym = {{LangOnto+TermiKS}'16}, booktitle = {{P}roceedings of the {J}oint 2nd {W}orkshop on {L}anguage and {O}ntology~\& {T}erminology and {K}nowledge {S}tructures ({LangOnto+TermiKS}'16)}, author = {Grefenstette, Gregory and Rafes, Karima}, title = {Transforming {W}ikipedia into an Ontology-based Information Retrieval Search Engine for Local Experts using a Third-Party Taxonomy}, year = 2016, month = may, url = {http://www.lsv.fr/Publis/PAPERS/PDF/GR-langonto16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GR-langonto16.pdf}, note = {To appear}, abstract = {Wikipedia is widely used for finding general information about a wide variety of topics. Its vocation is not to provide local information. For~example, it~provides plot, cast, and production information about a given movie, but not showing times in your local movie theatre. Here we describe how we can connect local information to Wikipedia, without altering its content. The~case study we present involves finding local scientific experts. Using a third-party taxonomy, independent from Wikipedia's category hierarchy, we index information connected to our local experts, present in their activity reports, and we re-index Wikipedia content using the same taxonomy. The connections between Wikipedia pages and local expert reports are stored in a relational database, accessible through as public SPARQL endpoint. A~Wikipedia gadget (or plugin) activated by the interested user, accesses the endpoint as each Wikipedia page is accessed. An~additional tab on the Wikipedia page allows the user to open up a list of teams of local experts associated with the subject matter in the Wikipedia page. The technique, though presented here as a way to identify local experts, is generic, in that any third party taxonomy, can be used in this to connect Wikipedia to any non-Wikipedia data source.} }

@article{LDRCF-ijdc16, publisher = {Springer}, journal = {International Journal of Dynamics and Control}, author = {Le{~}Co{\"e}nt, Adrien and De{~}Vuyst, Florian and Rey, Christian and Chamoin, Ludovic and Fribourg, Laurent}, title = {Control of mechanical systems using set-based methods}, pages = {1-17}, year = 2016, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LDRCF-ijdc16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LDRCF-ijdc16.pdf}, doi = {10.1007/s40435-016-0245-y}, abstract = {This paper considers large discrete-time linear systems obtained from discretized partial differential equations, and controlled by a \emph{quantized} law, i.e., a piecewise constant time function taking a finite set of values. We show how to generate the control by, first, applying \emph{model reduction} to the original system, then using a {"}state-space bisection{"} method for synthesizing a control at the reduced-order level, and finally computing an upper bound on the deviations between the controlled output trajectories of the reduced-order model and those of the original model. The effectiveness of our approach is illustrated on several examples of the literature.} }

@inproceedings{LACF-snr16, address = {Vienna, Austria}, month = apr, year = 2016, publisher = {{IEEE} Computer Society Press}, acronym = {{SNR}'16}, booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop on {S}ymbolic and {N}umerical {M}ethods for {R}eachability {A}nalysis ({SNR}'16)}, author = {Le{~}Co{\"e}nt, Adrien and Alexandre{ }dit{ }Sandretto, Julien and Chapoutot, Alexandre and Fribourg, Laurent}, title = {Control of Nonlinear Switched Systems Based on Validated Simulation}, pages = {1-6}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LACF-snr16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LACF-snr16.pdf}, abstract = {We present an algorithm of control synthesis for nonlinear switched systems, based on an existing procedure of state-space bisection and made available for nonlinear systems with the help of validated simulation. The use of validated simulation also permits to take bounded perturbations and varying parameters into account. The whole approach is entirely guaranteed and the induced controllers are correct-by-design.} }

@article{DFP-lmcs16, journal = {Logical Methods in Computer Science}, author = {Demri, St{\'e}phane and Figueira, Diego and Praveen, M}, title = {Reasoning about Data Repetitions with Counter Systems}, year = 2016, volume = {12}, number = {3}, month = aug, pages = {1:1-1:55}, url = {http://arxiv.org/abs/1604.02887}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DFP-lmcs16.pdf}, doi = {10.2168/LMCS-12(3:1)2016}, abstract = {We study linear-time temporal logics interpreted over data words with multiple attributes. We restrict the atomic formulas to equalities of attribute values in successive positions and to repetitions of attribute values in the future or past. We demonstrate correspondences between satisfiability problems for logics and reachability-like decision problems for counter systems. We show that allowing\slash disallowing atomic formulas expressing repetitions of values in the past corresponds to the reachability\slash coverability problem in Petri nets. This gives us 2EXPSPACE upper bounds for several satisfiability problems. We prove matching lower bounds by reduction from a reachability problem for a newly introduced class of counter systems. This new class is a succinct version of vector addition systems with states in which counters are accessed via pointers, apotentially useful feature in other contexts. We strengthen further the correspondences between data logics and counter systems by characterizing the complexity of fragments, extensions and variants of the logic. For instance, we precisely characterize the relationship between the number of attributes allowed in the logic and the number of counters needed in the counter system.} }

@inproceedings{BBCM-csr16, address = {St~Petersburg, Russia}, month = jun, year = 2016, volume = {9691}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Gerhard J. Woeginger}, acronym = {{CSR}'16}, booktitle = {{P}roceedings of the 11th {I}nternational {C}omputer {S}cience {S}ymposium in {R}ussia ({CSR}'16)}, author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and Carlier, Pierre and Menet, Quentin}, title = {Compositional Design of Stochastic Timed Automata}, pages = {117-130}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBCM-csr16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBCM-csr16.pdf}, doi = {10.1007/978-3-319-34171-2_9}, abstract = {In this paper, we study the model of stochastic timed automata and we target the definition of adequate composition operators that will allow a compositional approach to the design of stochastic systems with hard real-time constraints. This paper achieves the first step towards that goal. Firstly, we define a parallel composition operator that (we~prove) corresponds to the interleaving semantics for that model; we give conditions over probability distributions, which ensure that the operator is well-defined; and we exhibit problematic behaviours when this condition is not satisfied. We furthermore identify a large and natural subclass which is closed under parallel composition. Secondly, we define a bisimulation notion which naturally extends that for continuous-time Markov chains. Finally, we importantly show that the defined bisimulation is a congruence w.r.t. the parallel composition, which is an expected property for a proper modular approach to system design.} }

@inproceedings{BBBC-icalp16, address = {Rome, Italy}, month = jul, year = 2016, volume = {55}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide}, acronym = {{ICALP}'16}, booktitle = {{P}roceedings of the 43rd {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'16)}, author = {Bertrand, Nathalie and Bouyer, Patricia and Brihaye, {\relax Th}omas and Carlier, Pierre}, title = {Analysing Decisive Stochastic Processes}, pages = {101:1-101:14}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBBC-icalp16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBBC-icalp16.pdf}, doi = {10.4230/LIPIcs.ICALP.2016.101}, abstract = {In~2007, Abdulla \textit{et~al.} introduced the elegant concept of decisive Markov chain. Intuitively, decisiveness allows one to lift the good properties of finite Markov chains to infinite Markov chains. For instance, the approximate quantitative reachability problem can be solved for decisive Markov chains (enjoying reasonable effectiveness assumptions) including probabilistic lossy channel systems and probabilistic vector addition systems with states. In this paper, we extend the concept of decisiveness to more general stochastic processes. This extension is non trivial as we consider stochastic processes with a potentially continuous set of states and uncountable branching (common features of real-time stochastic processes). This allows us to obtain decidability results for both qualitative and quantitative verification problems on some classes of real-time stochastic processes, including generalized semi-Markov processes and stochastic timed automata.} }

@inproceedings{CH-icalp16, address = {Rome, Italy}, month = jul, year = 2016, volume = {55}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide}, acronym = {{ICALP}'16}, booktitle = {{P}roceedings of the 43rd {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'16)}, author = {Dmitry Chistikov and Christoph Haase}, title = {The Taming of the Semi-Linear Set}, pages = {128:1-128:14}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CH-icalp16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CH-icalp16.pdf}, doi = {10.4230/LIPIcs.ICALP.2016.128}, abstract = {Semi-linear sets, which are finitely generated subsets of the monoid \((\mathbb{Z}^d, +)\), have numerous applications in theoretical computer science. Although semi-linear sets are usually given implicitly, by formulas in Presburger arithmetic or by other means, the effect of Boolean operations on semi-linear sets in terms of the size of generators has primarily been studied for explicit representations. In this paper, we develop a framework suitable for implicitly presented semi-linear sets, in which the size of a semi-linear set is characterized by its norm---the maximal magnitude of a generator.\par We put together a {"}toolbox{"} of operations and decompositions for semi-linear sets which give bounds in terms of the norm (as opposed to just the bit-size of the description), a unified presentation, and simplified proofs. This toolbox, in particular, provides exponentially better bounds for the complement and set-theoretic difference. We also obtain bounds on unambiguous decompositions and, as an application of the toolbox, settle the complexity of the equivalence problem for exponent-sensitive commutative grammars.} }

@inproceedings{Zetzche-icalp16, address = {Rome, Italy}, month = jul, year = 2016, volume = {55}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide}, acronym = {{ICALP}'16}, booktitle = {{P}roceedings of the 43rd {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'16)}, author = {Georg Zetzsche}, title = {The complexity of downward closure comparisons}, pages = {123:1-123:14}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/Zetzche-icalp16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Zetzche-icalp16.pdf}, doi = {10.4230/LIPIcs.ICALP.2016.123}, abstract = {The downward closure of a language is the set of all (not necessarily contiguous) subwords of its members. It is well-known that the downward closure of every language is regular. Moreover, recent results show that downward closures are computable for quite powerful system models.\par One advantage of abstracting a language by its downward closure is that then, equivalence and inclusion become decidable. In~this work, we study the complexity of these two problems. More precisely, we consider the following decision problems: Given languages~\(K\) and~\(L\) from classes~\(\mathcal{C}\) and~\(\mathcal{D}\), respectively, does the downward closure of~\(K\) include (equal) that of~\(L\)?\par These problems are investigated for finite automata, one-counter automata, context-free grammars, and reversal-bounded counter automata. For each combination, we prove a completeness result either for fixed or for arbitrary alphabets. Moreover, for Petri net languages, we show that both problems are Ackermann-hard and for higher-order pushdown automata of order~\(k\), we prove hardness for complements of nondeterministic \(k\)-fold exponential time.} }

@inproceedings{CD-icalp16, address = {Rome, Italy}, month = jul, year = 2016, volume = {55}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide}, acronym = {{ICALP}'16}, booktitle = {{P}roceedings of the 43rd {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'16)}, author = {Chatterjee, Krishnendu and Doyen, Laurent}, title = {Computation Tree Logic for Synchronization Properties}, pages = {98:1-98:14}, url = {http://arxiv.org/abs/1604.06384}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-icalp16.pdf}, doi = {10.4230/LIPIcs.ICALP.2016.98}, abstract = {We present a logic that extends CTL (Computation Tree Logic) with operators that express synchronization properties. A property is synchronized in a system if it holds in all paths of a certain length. The new logic is obtained by using the same path quantifiers and temporal operators as in CTL, but allowing a different order of the quantifiers. This small syntactic variation induces a logic that can express non-regular properties for which known extensions of MSO with equality of path length are undecidable. We show that our variant of CTL is decidable and that the model-checking problem is in \(\Delta_3^P = P^{NP^NP}\), and is DP-hard. We analogously consider quantifier exchange in extensions of CTL, and we present operators defined using basic operators of CTL* that express the occurrence of infinitely many synchronization points. We show that the model-checking problem remains in \(\Delta_3^P\). The distinguishing power of CTL and of our new logic coincide if the Next operator is allowed in the logics, thus the classical bisimulation quotient can be used for state-space reduction before model checking.} }

@inproceedings{GLS-icalp16, address = {Rome, Italy}, month = jul, year = 2016, volume = {55}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide}, acronym = {{ICALP}'16}, booktitle = {{P}roceedings of the 43rd {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'16)}, author = {Goubault{-}Larrecq, Jean and Schmitz, Sylvain}, title = {Deciding Piecewise Testable Separability for Regular Tree Languages}, pages = {97:1-97:15}, url = {https://hal.inria.fr/hal-01276119/}, optpdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLS-icalp16.pdf}, doi = {10.4230/LIPIcs.ICALP.2016.97}, abstract = {The piecewise testable separability problem asks, given two input languages, whether there exists a piecewise testable language that contains the first input language and is disjoint from the second. We prove a general characterisation of piecewise testable separability on languages in a well-quasi-order, in terms of ideals of the ordering. This subsumes the known characterisations in the case of finite words. In the case of finite ranked trees ordered by homeomorphic embedding, we show using effective representations for tree ideals that it entails the decidability of piecewise testable separability when the input languages are regular. A~final byproduct is a new proof of the decidability of whether an input regular language of ranked trees is piecewise testable, which was first shown in the unranked case by Boja{\'n}czyk, Segoufin, and Straubing (Log.~Meth. in Comput.~Sci.,~8(3:26), 2012).} }

@inproceedings{GHLT-icalp16, address = {Rome, Italy}, month = jul, year = 2016, volume = {55}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide}, acronym = {{ICALP}'16}, booktitle = {{P}roceedings of the 43rd {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'16)}, author = {Stefan G{\"o}ller and Christoph Haase and Ranko Lazi{\'c} and Patrick Totzke}, title = {A Polynomial-Time Algorithm for Reachability in Branching {VASS} in Dimension One}, pages = {105:1-105:13}, url = {http://arxiv.org/abs/1602.05547}, pfd = {http://www.lsv.fr/Publis/PAPERS/PDF/GHLT-icalp16.pdf}, doi = {10.4230/LIPIcs.ICALP.2016.105}, abstract = {Branching VASS (BVASS) generalise vector addition systems with states by allowing for special branching transitions that can non-deterministically distribute a counter value between two control states. A~run of a BVASS consequently becomes a tree, and reachability is to decide whether a given configuration is the root of a reachability tree. This paper shows P-completeness of reachability in BVASS in dimension one, the first decidability result for reachability in a subclass of BVASS known so~far. Moreover, we~show that coverability and boundedness in BVASS in dimension one are P-complete as~well.} }

@inproceedings{BCM-cav16, address = {Toronto, Canada}, month = jul, year = 2016, volume = 9779, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Chaudhuri, Swarat and Farzan, Azadeh}, acronym = {{CAV}'16}, booktitle = {{P}roceedings of the 28th {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV}'16)~-- {P}art~{I}}, author = {Bouyer, Patricia and Colange, Maximilien and Markey, Nicolas}, title = {Symbolic Optimal Reachability in Weighted Timed Automata}, pages = {513-530}, url = {http://arxiv.org/abs/1602.00481}, doi = {10.1007/978-3-319-41528-4_28}, abstract = {Weighted timed automata have been defined in the early 2000's for modelling resource-consumption or -allocation problems in real-time systems. Optimal reachability is decidable in weighted timed automata, and a symbolic forward algorithm has been developed to solve that problem. This algorithm uses so-called priced zones, an extension of standard zones with cost functions. In order to ensure termination, the algorithm requires clocks to be bounded. For unpriced timed automata, much work has been done to develop sound abstractions adapted to the forward exploration of timed automata, ensuring termination of the model-checking algorithm without bounding the clocks. In this paper, we take advantage of recent developments on abstractions for timed automata, and propose an algorithm allowing for symbolic analysis of all weighted timed automata, without requiring bounded clocks.} }

@inproceedings{BMRSS-icalp16, address = {Rome, Italy}, month = jul, year = 2016, volume = {55}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide}, acronym = {{ICALP}'16}, booktitle = {{P}roceedings of the 43rd {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'16)}, author = {Bouyer, Patricia and Markey, Nicolas and Randour, Mickael and Sangnier, Arnaud and Stan, Daniel}, title = {Reachability in Networks of Register Protocols under Stochastic Schedulers}, pages = {106:1-106:14}, url = {http://arxiv.org/abs/1602.05928}, doi = {10.4230/LIPIcs.ICALP.2016.106}, abstract = {We study the almost-sure reachability problem in a distributed system obtained as the asynchronous composition of~\(N\) copies (called \emph{processes}) of the same automaton (called \emph{protocol}), that can communicate via a shared register with finite domain. The automaton has two types of transitions: write-transitions update the value of the register, while read-transitions move to a new state depending on the content of the register. Non-determinism is resolved by a stochastic scheduler. Given a protocol, we focus on almost-sure reachability of a target state by one of the processes. The answer to this problem naturally depends on the number~\(N\) of processes. However, we prove that our setting has a cut-off property : the answer to the almost-sure reachability problem is constant when \(N\) is large enough; we~then develop an EXPSPACE algorithm deciding whether this constant answer is positive or negative.} }

@inproceedings{LS-lics16, address = {New York City, USA}, month = jul, year = 2016, publisher = {ACM Press}, editor = {Grohe, Martin and Koskinen, Eric and Shankar, Natarajan}, acronym = {{LICS}'16}, booktitle = {{P}roceedings of the 31st {A}nnual {ACM\slash IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'16)}, author = {Ranko Lazi{\'c} and Sylvain Schmitz}, title = {The Complexity of Coverability in {{\(\nu\)}}-{P}etri Nets}, pages = {467-476}, url = {https://hal.inria.fr/hal-01265302}, doi = {10.1145/2933575.2933593}, abstract = {We show that the coverability problem in nu-Petri nets is complete for `double Ackermann' time, thus closing an open complexity gap between an Ackermann lower bound and a hyper-Ackermann upper bound. The coverability problem captures the verification of safety properties in this nominal extension of Petri nets with name management and fresh name creation. Our completeness result establishes nu-Petri nets as a model of intermediate power among the formalisms of nets enriched with data, and relies on new algorithmic insights brought by the use of well-quasi-order ideals.} }

@inproceedings{DBHS-lics16, address = {New York City, USA}, month = jul, year = 2016, publisher = {ACM Press}, editor = {Grohe, Martin and Koskinen, Eric and Shankar, Natarajan}, acronym = {{LICS}'16}, booktitle = {{P}roceedings of the 31st {A}nnual {ACM\slash IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'16)}, author = {Amina Doumane and David Baelde and Lucca Hirschi and Alexis Saurin}, title = {Towards Completeness via Proof Search in the Linear Time {{\(\mu\)}}-calculus}, pages = {377-386}, url = {https://hal.archives-ouvertes.fr/hal-01275289/}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DBHS-lics16.pdf}, doi = {10.1145/2933575.2933598}, abstract = {Modal \(\mu\)-calculus is one of the central languages of logic and verification, whose study involves notoriously complex objects: automata over infinite structures on the model-theoretical side; infinite proofs and proofs by (co)induction on the proof-theoretical side. Nevertheless, axiomatizations have been given for both linear and branching time \(\mu\)-calculi, with quite involved completeness arguments. We come back to this central problem, considering it from a proof search viewpoint, and provide some new completeness arguments in the linear time \(\mu\)-calculus. Our results only deal with restricted classes of formulas that closely correspond to (non-alternating) \(\omega\)-automata but, compared to earlier proofs, our completeness arguments are direct and constructive. We first consider a natural circular proof system based on sequent calculus, and show that it is complete for inclusions of parity automata directly expressed as formulas, making use of Safra's construction directly in proof search. We then consider the corresponding finitary proof system, featuring (co)induction rules, and provide a partial translation result from circular to finitary proofs. This yields completeness of the finitary proof system for inclusions of sufficiently deterministic parity automata, and finally for arbitrary B{\"u}chi automata.} }

@inproceedings{CG-lics16, address = {New York City, USA}, month = jul, year = 2016, publisher = {ACM Press}, editor = {Grohe, Martin and Koskinen, Eric and Shankar, Natarajan}, acronym = {{LICS}'16}, booktitle = {{P}roceedings of the 31st {A}nnual {ACM\slash IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'16)}, author = {{\relax Th}omas Colcombet and Stefan G{\"o}ller}, title = {Games with bound guess actions}, pages = {257-266}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CG-lics16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CG-lics16.pdf}, doi = {10.1145/2933575.2934502}, abstract = {We introduce games with (bound) guess actions. These are games in which the players may be asked along the play to provide num- bers that need to satisfy some bounding constraints. These are nat- ural extensions of domination games occurring in the regular cost function theory. In this paper we consider more specifically the case where the constraints to be bounded are regular cost functions, and the long term goal is an ?-regular winning condition. We show that such games are decidable on finite arenas.} }

@inproceedings{CD-lics16, address = {New York City, USA}, month = jul, year = 2016, publisher = {ACM Press}, editor = {Grohe, Martin and Koskinen, Eric and Shankar, Natarajan}, acronym = {{LICS}'16}, booktitle = {{P}roceedings of the 31st {A}nnual {ACM\slash IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'16)}, author = {Chatterjee, Krishnendu and Doyen, Laurent}, title = {Perfect-information Stochastic Games with Generalized Mean-Payoff Objectives}, pages = {247-256}, url = {http://arxiv.org/abs/1604.06376}, doi = {10.1145/2933575.2934513}, abstract = {Graph games provide the foundation for modeling and synthesizing reactive processes. In the synthesis of stochastic reactive processes, the traditional model is perfect-information stochastic games, where some transitions of the game graph are controlled by two adversarial players, and the other transitions are executed probabilistically. We consider such games where the objective is the conjunction of several quantitative objectives (specified as mean-payoff conditions), which we refer to as generalized mean-payoff objectives. The basic decision problem asks for the existence of a finite-memory strategy for a player that ensures the generalized mean-payoff objective be satisfied with a desired probability against all strategies of the opponent. A special case of the decision problem is the almost-sure problem where the desired probability is~1. Previous results presented a semi-decision procedure for epsilon-approximations of the almost-sure problem. In this work, we show that both the almost-sure problem as well as the general basic decision problem are coNP-complete, significantly improving the previous results. Moreover, we show that in the case of 1-player stochastic games, randomized memoryless strategies are sufficient and the problem can be solved in polynomial time. In contrast, in two-player stochastic games, we show that even with randomized strategies exponential memory is required in general, and present a matching exponential upper bound. We also study the basic decision problem with infinite-memory strategies and present computational complexity results for the problem. Our results are relevant in the synthesis of stochastic reactive systems with multiple quantitative requirements. } }

@inproceedings{DOMZ-lics16, address = {New York City, USA}, month = jul, year = 2016, publisher = {ACM Press}, editor = {Grohe, Martin and Koskinen, Eric and Shankar, Natarajan}, acronym = {{LICS}'16}, booktitle = {{P}roceedings of the 31st {A}nnual {ACM\slash IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'16)}, author = {D'Osualdo, Emanuele and Roland Meyer and Georg Zetzsche}, title = {First-order logic with reachability for infinite-state systems}, pages = {457-466}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DOMZ-lics16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DOMZ-lics16.pdf}, doi = {10.1145/2933575.2934552}, abstract = {First-order logic with the reachability predicate (FO(R)) is an important means of specification in system analysis. Its decidability status is known for some individual types of infinite-state systems such as pushdown (decidable) and vector addition systems (undecidable). \par This work aims at a general understanding of which types of systems admit decidability. As a unifying model, we employ valence systems over graph monoids, which feature a finite-state control and are parameterized by a monoid to represent their storage mechanism. As special cases, this includes pushdown systems, various types of counter systems (such as vector addition systems) and combinations thereof. Our main result is a complete characterization of those graph monoids where FO(R) is decidable for the resulting transition systems.} }

@inproceedings{ACHKSZ-lics16, address = {New York City, USA}, month = jul, year = 2016, publisher = {ACM Press}, editor = {Grohe, Martin and Koskinen, Eric and Shankar, Natarajan}, acronym = {{LICS}'16}, booktitle = {{P}roceedings of the 31st {A}nnual {ACM\slash IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'16)}, author = {Atig, Mohamed Faouzi and Dmitry Chistikov and Piotr Hofman and Kumar, K. Narayan and Prakash Saivasan and Georg Zetzsche}, title = {Complexity of regular abstractions of one-counter languages}, pages = {207-216}, url = {http://arxiv.org/abs/1602.03419}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ACHKSZ-lics16.pdf}, doi = {10.1145/2933575.2934561}, abstract = {We study the computational and descriptional complexity of the following transformation: Given a one-counter automaton~(OCA)~\(A\), construct a nondeterministic finite automaton~(NFA)~\(B\) that recognizes an abstraction of the language~\(L(A)\): its~(1)~downward closure, (2)~upward closure, or (3)~Parikh image. For the Parikh image over a fixed alphabet and for the upward and downward closures, we find polynomial-time algorithms that compute such an NFA. For the Parikh image with the alphabet as part of the input, we find a quasi-polynomial time algorithm and prove a completeness result: we construct a sequence of OCA that admits a polynomial-time algorithm iff there is one for all OCA. For all three abstractions, it was previously unknown if appropriate NFA of sub-exponential size exist.} }

@inproceedings{HBD-sp16, address = {San Jose, California, USA}, month = may, year = 2016, publisher = {IEEECSP}, editor = {Locasto, Michael and Shmatikov, Vitaly and Erlingsson, {\'U}lfar}, acronym = {{S\&P}'16}, booktitle = {{P}roceedings of the 37th {IEEE} {S}ymposium on {S}ecurity and {P}rivacy ({S\&P}'16)}, author = {Hirschi, Lucca and Baelde, David and Delaune, St{\'e}phanie}, title = {A~method for verifying privacy-type properties: the~unbounded case}, pages = {564-581}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/HBD-sp16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HBD-sp16.pdf}, doi = {10.1109/SP.2016.40}, abstract = {In~this paper, we~consider the problem of verifying anonymity and unlinkability in the symbolic model, where protocols are represented as processes in a variant of the applied pi calculus notably used in the Proverif tool. Existing tools and techniques do not allow one to verify directly these properties, expressed as behavioral equivalences. We propose a different approach: we design two conditions on protocols which are sufficient to ensure anonymity and unlinkability, and which can then be effectively checked automatically using Proverif. Our two conditions correspond to two broad classes of attacks on unlinkability, corresponding to data and control-flow leaks.\par This theoretical result is general enough to apply to a wide class of protocols. In particular, we apply our techniques to provide the first formal security proof of the BAC protocol (e-passport). Our work has also lead to the discovery of new attacks, including one on the LAK protocol (RFID authentication) which was previously claimed to be unlinkable (in~a weak sense) and one on the PACE protocol (e-passport).} }

@inproceedings{CC-pn16, address = {Tor{\'u}n, Poland}, month = jun, year = 2016, volume = {9698}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Kordon, Fabrice and Moldt, Daniel}, acronym = {{PETRI~NETS}'16}, booktitle = {{P}roceedings of the 37th {I}nternational {C}onference on {A}pplications and {T}heory of {P}etri {N}ets ({PETRI~NETS}'16)}, author = {Carmona, Josep and Chatain, {\relax Th}omas}, title = {Anti-Alignments in Conformance Checking~-- The~Dark Side of Process Models}, pages = {240-258}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CC-pn16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CC-pn16.pdf}, doi = {10.1007/978-3-319-39086-4_15}, abstract = {Conformance checking techniques asses the suitability of a process model in representing an underlying process, observed through a collection of real executions. These techniques suffer from the well-known state space explosion problem, hence handling process models exhibiting large or even infinite state spaces remains a challenge. One important metric in conformance checking is to asses the precision of the model with respect to the observed executions, i.e., characterize the ability of the model to produce behavior unrelated to the one observed. By~avoiding the computation of the full state space of a model, current techniques only provide estimations of the precision metric, which in some situations tend to be very optimistic, thus hiding real problems a process model may have. In this paper we present the notion of anti-alignment as a concept to help unveiling traces in the model that may deviate significantly from the observed behavior. Using anti-alignments, current estimations can be improved, e.g., in precision checking. We show how to express the problem of finding anti-alignments as the satisfiability of a Boolean formula, and provide a tool which can deal with large models efficiently.} }

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

@techreport{DD-arxiv16, author = {D{\'i}az{-}Caro, Alejandro and Dowek, Gilles}, title = {Quantum superpositions and projective measurement in the lambda calculus}, institution = {Computing Research Repository}, number = {1601.04294}, year = {2016}, month = jan, type = {Research Report}, url = {http://arxiv.org/abs/1601.04294}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-arxiv16.pdf}, note = {22~pages}, abstract = {We propose an extension of simply typed lambda-calculus to handle some properties of quantum computing. The equiprobable quantum superposition is taken as a commutative pair and the quantum measurement as a non-deterministic projection over it. Destructive interferences are achieved by introducing an inverse symbol with respect to pairs. The no-cloning property is ensured by using a combination of syntactic linearity with linear logic. Indeed, the syntactic linearity is enough for unitary gates, while a function measuring its argument needs to enforce that the argument is used only once.} }

@inproceedings{FGMP-hscc16, address = {Vienna, Austria}, month = apr, year = 2016, publisher = {ACM Press}, editor = {Abate, Alessandro and Fainekos, Georgios}, acronym = {{HSCC}'16}, booktitle = {{P}roceedings of the 19th {ACM} {I}nternational {C}onference on {H}ybrid {S}ystems: {C}omputation and {C}ontrol ({HSCC}'16)}, author = {Fribourg, Laurent and Goubault, {\'E}ric and Mohamed, Sameh and Putot, Sylvie}, title = {A~Topological Method for Finding Invariant Sets of Switched Systems}, pages = {61-70}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FGMP-hscc16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FGMP-hscc16.pdf}, doi = {10.1145/2883817.2883822}, abstract = {We~revisit the problem of finding controlled invariants sets (viability), for a class of differential inclusions, using topological methods based on Wazewski property. In~many ways, this generalizes the Viability Theorem approach, which is itself a generalization of the Lyapunov function approach for systems described by ordinary differential equations. We give a computable criterion based on SoS methods for a class of differential inclusions to have a non-empty viability kernel within some given region. We use this method to prove the existence of (controlled) invariant sets of switched systems inside a region described by a polynomial template, both with time-dependent switching and with state-based switching through a finite set of hypersurfaces. A~Matlab implementation allows us to demonstrate its use.} }

@phdthesis{rc-phd2016, author = {Chr{\'e}tien, R{\'e}my}, title = {Analyse automatique de propri{\'e}t{\'e}s d'{\'e}quivalence pour les protocoles cryptographiques}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2016, month = jan, url = {http://www.lsv.fr/Publis/PAPERS/PDF/rc-phd16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/rc-phd16.pdf} }

@inproceedings{LS-stacs16, address = {Orl{\'e}ans, France}, month = feb, year = 2016, volume = {47}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Ollinger, Nicolas and Vollmer, Heribert}, acronym = {{STACS}'16}, booktitle = {{P}roceedings of the 33rd {A}nnual {S}ymposium on {T}heoretical {A}spects of {C}omputer {S}cience ({STACS}'16)}, author = {Leroux, J{\'e}r{\^o}me and Schmitz, Sylvain}, title = {Ideal Decompositions for Vector Addition Systems}, pages = {1:1-1:13}, url = {http://drops.dagstuhl.de/opus/volltexte/2016/5702}, doi = {10.4230/LIPIcs.STACS.2016.1}, abstract = {Vector addition systems, or equivalently Petri nets, are one of the most popular formal models for the representation and the analysis of parallel processes. Many problems for vector addition systems are known to be decidable thanks to the theory of well-structured transition systems. Indeed, vector addition systems with configurations equipped with the classical point-wise ordering are well-structured transition systems. Based on this observation, problems like coverability or termination can be proven decidable.\par However, the theory of well-structured transition systems does not explain the decidability of the reachability problem. In this presentation, we show that runs of vector addition systems can also be equipped with a well quasi-order. This observation provides a unified understanding of the data structures involved in solving many problems for vector addition systems, including the central reachability problem.} }

@article{siglog16-Schmitz, publisher = {ACM Press}, journal = {SIGLOG News}, author = {Schmitz, Sylvain}, title = {Automata column: The~complexity of reachability in vector addition systems}, volume = 3, number = 1, pages = {3-21}, year = 2016, month = jan, url = {https://hal.inria.fr/hal-01275972}, doi = {10.1145/2893582.2893585}, annote = {Invited column}, abstract = {The program of the 30th Symposium on Logic in Computer Science held in 2015 in Kyoto included two contributions on the computational complexity of the reachability problem for vector addition systems: Blondin, Finkel, G{\"o}ller, Haase, and McKenzie~[2015] attacked the problem by providing the first tight complexity bounds in the case of dimension-2 systems with states, while Leroux and Schmitz~[2015] proved the first complexity upper bound in the general case. The purpose of this column is to present the main ideas behind these two results, and more generally survey the current state of affairs.} }

@article{CFS-tcs16, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {Chambart, Pierre and Finkel, Alain and Schmitz, Sylvain}, title = {Forward Analysis and Model Checking for Trace Bounded~{WSTS}}, year = 2016, volume = {637}, pages = {1-29}, month = jul, url = {http://arxiv.org/abs/1004.2802}, doi = {10.1016/j.tcs.2016.04.020}, abstract = {We investigate a subclass of well-structured transition systems~(WSTS), the bounded---in the sense of Ginsburg and Spanier (Trans.~AMS, 1964)---complete deterministic ones, which we claim provide an adequate basis for the study of forward analyses as developed by Finkel and Goubault-Larrecq (ICALP~2009). Indeed, we prove that, unlike other conditions considered previously for the termination of forward analysis, boundedness is decidable. Boundedness turns out to be a valuable restriction for WSTS verification, as we show that it further allows to decide all {{\(\omega\)}}-regular properties on the set of infinite traces of the system.} }

@article{toct-Schmitz13, publisher = {ACM Press}, journal = {ACM Transactions on Computation Theory}, author = {Schmitz, Sylvain}, title = {Complexity Hierarchies Beyond {E}lementary}, volume = {8}, number = {1:3}, nopages = {}, year = 2016, month = feb, url = {http://arxiv.org/abs/1312.5686}, doi = {10.1145/2858784}, abstract = {We introduce a hierarchy of fast-growing complexity classes and show its suitability for completeness statements of many non elementary problems. This hierarchy allows the classification of many decision problems with a non-elementary complexity, which occur naturally in logic, combinatorics, formal languages, verification, etc., with complexities ranging from simple towers of exponentials to Ackermannian and beyond.} }

@inproceedings{CCHPW-fossacs16, address = {Eindhoven, The~Netherlands}, month = apr, year = 2016, volume = {9634}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Jacobs, Bart and L{\"o}ding, Christof}, acronym = {{FoSSaCS}'16}, booktitle = {{P}roceedings of the 19th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'16)}, author = {Chistikov, Dmitry and Czerwi{\'n}ski, Wojciech and Hofman, Piotr and Pilipczuk, Micha{\l} and Wehar, Michael}, title = {Shortest paths in one-counter systems}, pages = {462-478}, url = {http://arxiv.org/abs/1510.05460}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCHPW-fossacs16.pdf}, doi = {10.1007/978-3-662-49630-5_27}, abstract = {We show that any one-counter automaton with \(n\) states, if its language is non-empty, accepts some word of length at most~\(O(n^2)\). This closes the gap between the previously known upper bound of~\(O(n^3)\) and lower bound of~\(\Omega(n^2)\). More generally, we prove a tight upper bound on the length of shortest paths between arbitrary configurations in one-counter transition systems. Weaker bounds have previously appeared in the literature, and our result offers an improvement.} }

@inproceedings{HLLLST-fossacs16, address = {Eindhoven, The~Netherlands}, month = apr, year = 2016, volume = {9634}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Jacobs, Bart and L{\"o}ding, Christof}, acronym = {{FoSSaCS}'16}, booktitle = {{P}roceedings of the 19th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'16)}, author = {Hofman, Piotr and Lasota, S{\l}awomir and Lazi{\'c}, Ranko and Leroux, J{\'e}r{\^o}me and Schmitz, Sylvain and Totzke, Patrick}, title = {Coverability Trees for {P}etri Nets with Unordered Data}, pages = {445-461}, url = {https://hal.inria.fr/hal-01252674}, doi = {10.1007/978-3-662-49630-5_26}, abstract = {We study an extension of classical Petri nets where tokens carry values from a countable data domain, that can be tested for equality upon firing transitions. These Unordered Data Petri Nets (UDPN) are well-structured and therefore allow generic decision procedures for several verification problems including coverability and boundedness. We show how to construct a finite representation of the coverability set in terms of its ideal decomposition. This not only provides an alternative method to decide coverability and boundedness, but is also an important step towards deciding the reachability problem. This also allows to answer more precise questions about the reachability set, for instance whether there is a bound on the number of tokens on a given place (place boundedness), or if such a bound exists for the number of different data values carried by tokens (place width boundedness). We provide matching Hyper-Ackermann bounds on the size of cover-ability trees and on the running time of the induced decision procedures.} }

@inproceedings{FG-fossacs16, address = {Eindhoven, The~Netherlands}, month = apr, year = 2016, volume = {9634}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Jacobs, Bart and L{\"o}ding, Christof}, acronym = {{FoSSaCS}'16}, booktitle = {{P}roceedings of the 19th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'16)}, author = {Fortin, Marie and Gastin, Paul}, title = {Verification of parameterized communicating automata via split-width}, pages = {197-213}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FG-fossacs16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FG-fossacs16.pdf}, doi = {10.1007/978-3-662-49630-5_12}, abstract = {We~study verification problems for distributed systems communicating via unbounded FIFO channels. The number of processes of the system as well as the communication topology are not fixed a~priori. Systems are given by parameterized communicating automata (PCAs) which can be run on any communication topology of bounded degree, with arbitrarily many processes. Such systems are Turing powerful so we concentrate on under-approximate verification. We extend the notion of split-width to behaviors of PCAs. We show that emptiness, reachability and model-checking problems of PCAs are decidable when restricted to behaviors of bounded split-width. Reachability and emptiness are EXPTIME-complete, but only polynomial in the size of the PCA. We also describe several concrete classes of bounded split-width, for which we prove similar results.} }

@inproceedings{CDD-post16, address = {Eindhoven, The~Netherlands}, month = apr, year = 2016, volume = { 9635}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Piessens, Frank and Vigan{\'o}, Luca}, acronym = {{POST}'16}, booktitle = {{P}roceedings of the 5th {I}nternational {C}onference on {P}rinciples of {S}ecurity and {T}rust ({POST}'16)}, author = {Cortier, V{\'e}ronique and Dallon, Antoine and Delaune, St{\'e}phanie}, title = {Bounding the number of agents, for equivalence~too}, pages = {211-232}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDD-post16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDD-post16.pdf}, doi = {10.1007/978-3-662-49635-0_11}, abstract = {Bounding the number of agents is a current practice when modeling a protocol. In~2003, it has been shown that one honest agent and one dishonest agent are indeed sufficient to find all possible attacks, for secrecy properties. This is no longer the case for equivalence properties, crucial to express many properties such as vote privacy or untraceability.\par In this paper, we show that it is sufficient to consider two honest agents and two dishonest agents for equivalence properties, for deterministic processes with standard primitives and without else branches. More generally, we show how to bound the number of agents for arbitrary constructor theories and for protocols with simple else branches. We show that our hypotheses are tight, providing counter-examples for non actiondeterministic processes, non constructor theories, or protocols with complex else branches.} }

@inproceedings{tacas16-BFHH, address = {Eindhoven, The Netherlands}, month = apr, year = 2016, volume = {9636}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Chechik, Marsha and Raskin, Jean-Fran{\c{c}}ois}, acronym = {{TACAS}'16}, booktitle = {{P}roceedings of the 22th {I}nternational {C}onference on {T}ools and {A}lgorithms for {C}onstruction and {A}nalysis of {S}ystems ({TACAS}'16)}, author = {Blondin, Michael and Finkel, Alain and Haase, Christoph and Haddad, Serge}, title = {Approaching the Coverability Problem Continuously}, pages = {480-496}, url = {http://arxiv.org/abs/1510.05724}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/arxiv15-BFHH.pdf}, doi = {10.1007/978-3-662-49674-9_28}, abstract = {The coverability problem for Petri nets plays a central role in the verification of concurrent shared-memory programs. However, its high EXPSPACE-complete complexity poses a challenge when encountered in real-world instances. In this paper, we develop a new approach to this problem which is primarily based on applying forward coverability in continuous Petri nets as a pruning criterion inside a backward coverability framework. A cornerstone of our approach is the efficient encoding of a recently developed polynomial-time algorithm for reachability in continuous Petri nets into SMT. We demonstrate the effectiveness of our approach on standard benchmarks from the literature, which shows that our approach decides significantly more instances than any existing tool and is in addition often much faster, in particular on large instances.} }

@inproceedings{HH-stacs16, address = {Orl{\'e}ans, France}, month = feb, year = 2016, volume = {47}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Ollinger, Nicolas and Vollmer, Heribert}, acronym = {{STACS}'16}, booktitle = {{P}roceedings of the 33rd {A}nnual {S}ymposium on {T}heoretical {A}spects of {C}omputer {S}cience ({STACS}'16)}, author = {Haase, Christoph and Hofman, Piotr}, title = {Tightening the Complexity of Equivalence Problems for Commutative Grammars}, pages = {41:1-14}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/HH-stacs16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HH-stacs16.pdf}, doi = {10.4230/LIPIcs.STACS.2016.41}, abstract = {Given two finite-state automata, are the Parikh images of the languages they generate equivalent? This problem was shown decidable in coNEXP by Huynh in 1985 within the more general setting of context-free commutative grammars. Huynh conjectured that a~\(\Pi_{2}^{P}\) upper bound might be possible, and Kopczy{\'n}ski and To established in 2010 such an upper bound when the size of the alphabet is fixed. The contribution of this paper is to show that the language equivalence problem for regular and context-free commutative grammars is actually coNEXP-complete. In addition, our lower bound immediately yields further coNEXP-completeness results for equivalence problems for regular commutative expressions, reversal-bounded counter automata and communication-free Petri nets. Finally, we improve both lower and upper bounds for language equivalence for exponent-sensitive commutative grammars.} }

@inproceedings{BHL-lata16, address = {Prague, Czech Republic}, month = mar, year = 2016, volume = {9618}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Mart{\'\i}n-Vide, Carlos}, acronym = {{LATA}'16}, booktitle = {{P}roceedings of the 10th {I}nternational {C}onference on {L}anguage and {A}utomata {T}heory and {A}pplications ({LATA}'16)}, author = {Bertrand, Nathalie and Haddad, Serge and Lefaucheux, Engel}, title = {Accurate Approximate Diagnosability of Stochastic Systems}, pages = {549-561}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHL-lata16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHL-lata16.pdf}, doi = {10.1007/978-3-319-30000-9_42}, abstract = {Diagnosis of partially observable stochastic systems prone to faults was introduced in the late nineties. Diagnosability, i.e. the existence of a diagnoser, may be specified in different ways: (1)~exact diagnosability (called A-diagnosability) requires that almost surely a fault is detected and that no fault is erroneously claimed while (2)~approximate diagnosability (called \(\varepsilon\)-diagnosability) allows a small probability of error when claiming a fault and (3)~accurate approximate diagnosability (called AA-diagnosability) requires that this error threshold may be chosen arbitrarily small. Here we mainly focus on approximate diagnoses. We first refine the almost sure requirement about finite delay introducing a uniform version and showing that while it does not discriminate between the two versions of exact diagnosability this is no more the case in approximate diagnosis. Then we establish a complete picture for the decidability status of the diagnosability problems: (uniform) \(\varepsilon\)-diagnosability and uniform AA-diagnosability are undecidable while AA-diagnosability is decidable in PTIME, answering a longstanding open question.} }

@article{DD-tocl15b, publisher = {ACM Press}, journal = {ACM Transactions on Computational Logic}, author = {Demri, St{\'e}phane and Deters, Morgan}, title = {Expressive Completeness of Separation Logic With Two Variables and No Separating Conjunction}, volume = {17}, number = {2}, pages = {12:1-12:44}, month = mar, year = 2016, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-tocl15b.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-tocl15b.pdf}, doi = {10.1145/2835490}, abstract = {Separation logic is used as an assertion language for Hoare-style proof systems about programs with pointers, and there is an ongoing quest for understanding its complexity and expressive power. Herein, 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. Because we forbid ourselves the use of many syntactic resources, this underscores even further the power of separating implication on concrete heaps.} }

@article{HOW-fi15, publisher = {{IOS} Press}, journal = {Fundamenta Informaticae}, author = {Haase, Christoph and Ouaknine, Jo{\"e}l and Worrell, James}, title = {Relating Reachability Problems in Timed and Counter Automata}, volume = {143}, number = {3-4}, pages = {317-338}, year = 2016, month = jan, url = {http://www.lsv.fr/Publis/PAPERS/PDF/HOW-fi15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HOW-fi15.pdf}, doi = {10.3233/FI-2016-1316}, abstract = {We establish a relationship between reachability problems in timed automata and space-bounded counter automata. We show that reachability in timed automata with three or more clocks is logarithmic-space inter-reducible with reachability in space-bounded counter automata with two counters. We moreover show the logarithmic-space equivalence of reachability in two-clock timed automata and space-bounded one-counter automata. This last reduction has recently been employed by Fearnley and Jurdzi{\'n}ski to settle the computational complexity of reachability in two-clock timed automata.} }

@techreport{BJM-arxiv16, author = {Bouyer, Patricia and Markey, Nicolas and Jug{\'e}, Vincent}, title = {Dynamic Complexity of Parity Games with Bounded Tree-Width}, institution = {Computing Research Repository}, number = {1610.00571}, year = {2016}, url = {https://arxiv.org/abs/1610.00571}, pdf = {https://arxiv.org/abs/1610.00571}, month = oct, type = {Research Report}, note = {33~pages} }

@misc{mcc:2016, author = {F. Kordon and H. Garavel and L. M. Hillah and Hulin{-}Hubard, Francis and G. Chiardo and A. Hamez and L. Jezequel and A. Miner and J. Meijer and E. Paviot-Adet and D. Racordon and C. Rodriguez and C. Rohr and J. Srba and Y. Thierry-Mieg and G. Tr{\d i}nh and K. Wolf}, month = jun, title = {{Complete Results for the 2016 Edition of the Model Checking Contest}}, year = {2016}, url = {http://mcc.lip6.fr/2016/results.php} }

@misc{JGL:pls16, author = {Goubault{-}Larrecq, Jean}, howpublished = {Encart dans l'article ''S'adapter {\`a} la cyberguerre'', de Karen Elazari, Pour La Science 459}, month = jan, title = {Les m{\'e}thodes formelles: l'autre arme de la cybers{\'e}curit{\'e}}, year = {2016}, pages = {50-55} }

@misc{JGL:stc16, author = {Goubault{-}Larrecq, Jean}, howpublished = {Invited talk (plenary speaker), Summer Topology Conference, Leicester, UK}, month = aug, title = {A few things on Noetherian spaces}, year = {2016} }

@misc{JGL:gs16, author = {Goubault{-}Larrecq, Jean}, howpublished = {Invited talk, Galway Symposium, Leicester, UK}, month = aug, title = {An introduction to asymmetric topology and domain theory: why, what, and how}, year = {2016} }

@misc{JGL:dm16, author = {Goubault{-}Larrecq, Jean}, howpublished = {Invited talk, Dale Miller Festschrift, Paris Diderot University, Paris}, month = dec, title = {A semantics for {{\(\nabla\)}}}, year = {2016} }

@misc{GSHM:dga-inria16, author = {Goubault-Larrecq, Jean and Sentucq, Pierre-Arnaud and Hulin-Hubard, Francis and Majorczyk, Fr{\'e}d{\'e}ric}, howpublished = {Rapport final et fourniture 4 du contrat DGA-INRIA Orchids}, month = may, title = {Etat final des travaux engag{\'e}s sur {Orchids}}, year = {2016} }

@misc{GM:dga-inria16, author = {Goubault-Larrecq, Jean and Majorczyk, Fr{\'e}d{\'e}ric}, howpublished = {Fourniture 3 du contrat DGA-INRIA Orchids}, month = may, title = {G{\'e}n{\'e}ration de signatures pour le suivi de flux d'informations}, year = {2016} }

@inproceedings{AMP-lfmtp16, address = {Porto, Portugal}, month = jun, publisher = {ACM Press}, editor = {Dowek, Gilles and Licata, Daniel R. and Alves, Sandra}, acronym = {{LFMTP}'16}, booktitle = {Proceedings of the 11th {I}nternational {W}orkshop on {L}ogical {F}rameworks and {M}eta-{L}anguages: {T}heory and {P}ractice ({LFMTP}'16)}, author = {Cauderlier, Rapha{\"e}l}, title = {{{A Rewrite System for Proof Constructivization}}}, pages = {2:1-2:7}, year = {2016}, doi = {10.1007/978-3-319-40578-0\_5}, url = {https://hal.inria.fr/hal-01420634/}, pdf = {https://hal.inria.fr/hal-01420634/file/LFMTP_2016.pdf}, abstract = {Proof constructivization is the problem of automatically extracting constructive proofs out of classical proofs. This process is required when classical theorem provers are integrated in intuitionistic proof assistants. We use the ability of rewrite systems to represent partial functions to implement heuristics for proof constructivization in Dedukti, a logical framework based on rewriting in which proofs are first-class objects which can be the subject of computation. We benchmark these heuristics on the proofs output by the automated theorem prover Zenon on the TPTP library of problems.} }

@inproceedings{AMP-rc16, address = {Bologna, Italy}, month = jul, volume = 9720, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Lanese, Ivan and Devitt, Simon}, acronym = {{RC}'16}, booktitle = {8th Conference on Reversible Computation (RC'16)}, author = {Arrighi, Pablo and Martiel, Simon and Perdrix, Simon}, title = {{{Reversible Causal Graph Dynamics}}}, pages = {73-88}, year = {2016}, doi = {10.1007/978-3-319-40578-0\_5}, url = {https://hal.archives-ouvertes.fr/hal-01361427}, abstract = {Causal Graph Dynamics extend Cellular Automata to arbitrary , bounded-degree, time-varying graphs. The whole graph evolves in discrete time steps, and this global evolution is required to have a number of physics-like symmetries: shift-invariance (it acts everywhere the same) and causality (information has a bounded speed of propagation). We add a further physics-like symmetry, namely reversibility.} }

@inproceedings{ADJL-hatt2016, author = {Assaf, Ali and Dowek, Gilles and Jouannaud, Jean-Pierre and Liu, Jiaxiang}, title = {{{Encoding Proofs in Dedukti: the case of Coq proofs}}}, nopages = {}, booktitle = {Preliminary Proceedings of the 1st International Workshop on Hammers for Type Theories (HaTT'16)}, year = {2016}, address = {Coimbra, Portugal}, url = {https://hal.inria.fr/hal-01330980}, pdf = {https://hal.inria.fr/hal-01330980/file/HaTT_2016_paper_3.pdf}, abstract = {A main ambition of the Inria project Dedukti is to serve as a common language for representing and type checking proof objects originating from other proof systems. Encoding these proof objects makes heavy use of the rewriting capabilities of LambdaPiModulo, the formal system on which Dedukti is based. So far, the proofs generated by two automatic proof systems, Zenon and iProver, have been encoded, and can therefore be read and checked by Dedukti. But Dedukti goes far beyond this so-called hammering technique of sending goals to automated provers. Proofs from HOL and Matita can be encoded as well. Some Coq?s proofs can be encoded already, when they do not use universe polymorphism. Our ambition here is to close this remaining gap. To this end, we describe a rewrite-based encoding in LambdaPiModulo of the Calculus of Constructions with a cumulative hierarchy of predicative universes above Prop, which is confluent on open terms.} }

@inproceedings{ADJL-hor2016, author = {Assaf, Ali and Dowek, Gilles and Jouannaud, Jean-Pierre and Liu, Jiaxiang}, title = {{{Untyped Confluence in Dependent Type Theories}}}, nopages = {}, booktitle = {Proceedings of the 8th International Workshop on Higher-Order Rewriting (HOR'16)}, year = {2016}, address = {Porto, Portugal}, url = {https://hal.inria.fr/hal-01330955}, pdf = {https://hal.inria.fr/hal-01330955/file/HOR_2016_paper.pdf}, abstract = {We investigate techniques based on van Oostrom's decreasing diagrams that reduce confluence proofs to the checking of critical pairs in the absence of termination properties, which are useful in dependent type calculi to prove confluence on untyped terms. These techniques are applied to a complex example originating from practice: a faithful encoding, in an extension of LF with rewrite rules on objects and types, of a subset of the calculus of inductive constructions with a cumulative hierarchy of predicative universes above Prop. The rules may be first-order or higher-order, plain or modulo, non-linear on the right or on the left. Variables which occur non-linearly in lefthand sides of rules must take their values in confined types: in our example, the natural numbers. The first-order rules are assumed to be terminating and confluent modulo some theory: in our example, associativity, commutativity and identity. Critical pairs involving higher-order rules must satisfy van Oostrom's decreasing diagram condition wrt their indexes taken as labels.} }

@inproceedings{A-types2016, address = {Novi Sad, Serbia}, volume = {97}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Ghilezan, Silvia and Ivetic, Jelena}, acronym = {{TYPES}'16}, booktitle = {{P}roceedings of the 22nd {I}nternational {C}onference on {T}ypes for {P}roofs and {P}rograms ({TYPES}'16)}, author = {Assaf, Ali and Burel, Guillaume and Cauderlier, Rapha{\"e}l and Delahaye, David and Dowek, Gilles and Dubois, Catherine and Gilbert, Fr{\'e}d{\'e}ric and Halmagrand, Pierre and Hermant, Olivier and Saillard, Ronan}, title = {{{Expressing theories in the {{\(\lambda\Pi\)}}-calculus modulo theory and in the Dedukti system}}}, year = {2016}, note = {To appear} }

@unpublished{D-preprint2016, title = {{Rules and derivations in an elementary logic course}}, author = {Dowek, Gilles}, note = {preprint}, year = {2016}, month = jan, url = {https://hal.inria.fr/hal-01252124/}, pdf = {https://hal.inria.fr/hal-01252124/file/ttl.pdf}, abstract = {When teaching an elementary logic course to students who have a general scientific background but have never been exposed to logic, we have to face the problem that the notions of deduction rule and of derivation are completely new to them, and are related to nothing they already know, unlike, for instance, the notion of model, that can be seen as a generalization of the notion of algebraic structure. In this note, we defend the idea that one strategy to introduce these notions is to start with the notion of inductive definition [1]. Then, the notion of derivation comes naturally. We also defend the idea that derivations are pervasive in logic and that defining precisely this notion at an early stage is a good investment to later define other notions in proof theory, computability theory, automata theory, ... Finally, we defend the idea that to define the notion of derivation precisely, we need to distinguish two notions of derivation: labeled with elements and labeled with rule names. This approach has been taken in [2].} }

@unpublished{AD-preprint2016, title = {{What is the Planck constant the magnitude of?}}, author = {Arrighi, Pablo and Dowek, Gilles}, note = {preprint}, year = {2016}, month = dec, url = {https://hal.inria.fr/hal-01421711}, pdf = {https://hal.inria.fr/hal-01421711/file/planck.pdf}, abstract = {The Planck constant is the minimal area of one bit.} }

@inproceedings{CD-ictac16, address = {Taipei, Taiwan}, month = oct, volume = 9965, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Alves Sampaio, Cesar and Wang, Farn}, acronym = {{ICTAC}'16}, booktitle = {{P}roceedings of the 13th {I}nternational {C}olloquium on {T}heoretical {A}spects of {C}omputing ({ICTAC}'16)}, author = {Cauderlier, Rapha{\"e}l and Dubois, Catherine}, title = {{{ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti}}}, pages = {459-468}, year = {2016}, pdf = {https://hal.inria.fr/hal-01420638/file/ICTAC_2016.pdf}, url = {https://hal.inria.fr/hal-01420638/}, abstract = {The programming environment FoCaLiZe allows the user to specify, implement, and prove programs with the help of the theorem prover Zenon. In the actual version, those proofs are verified by Coq. In this paper we propose to extend the FoCaLiZe compiler by a backend to the Dedukti language in order to benefit from Zenon Modulo, an extension of Zenon for Deduction modulo. By doing so, FoCaLiZe can benefit from a technique for finding and verifying proofs more quickly. The paper focuses mainly on the process that overcomes the lack of local pattern-matching and recursive definitions in Dedukti.} }

@mastersthesis{m2-thire, author = {Thir{\'e}, Fran{\c{c}}ois}, title = {Reverse engineering on arithmetic proofs}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2016}, month = aug, url = {https://hal.inria.fr/hal-01424816}, pdf = {https://hal.inria.fr/hal-01424816/file/main.pdf}, note = {26~pages} }

@phdthesis{ph-phd2016, author = {Halmagrand, Pierre}, title = {{Automated Deduction and Proof Certification for the B Method}}, school = {{Conservatoire National Des Arts et M{\'e}tiers, Paris}}, type = {Th{\`e}se de doctorat}, year = 2016, month = dec, url = {https://hal.inria.fr/tel-01420460/} }

@inproceedings{AD-dcm15, address = {Cali, Colombia}, month = mar, volume = 204, series = {Electronic Proceedings in Theoretical Computer Science}, editor = {Mu\~noz, C\'esar A. and P\'erez, Jorge A.}, acronym = {{DCM}'15}, booktitle = {{P}roceedings of the 11th {I}nternational {W}orkshop on {D}evelopments in {C}omputational {M}odels ({DCM}'15)}, author = {Arrighi, Pablo and Dowek, Gilles}, doi = {10.4204/EPTCS.204.1}, pages = {1-10}, title = {Free fall and cellular automata}, url = {https://hal.inria.fr/hal-01421712}, year = {2016}, abstract = {Three reasonable hypotheses lead to the thesis that physical phenomena can be described and simulated with cellular automata. In this work, we attempt to describe the motion of a particle upon which a constant force is applied, with a cellular automaton, in Newtonian physics, in Special Relativity, and in General Relativity. The results are very different for these three theories.} }

@article{BGMS-toct16, publisher = {ACM Press}, journal = {ACM Transactions on Computation Theory}, author = {Beame, Paul and Grosshans, Nathan and McKenzie, Pierre and Segoufin, Luc}, title = {Nondeterminism and An Abstract Formulation of {Ne\v{c}iporuk}'s Lower Bound Method}, volume = {9}, number = {1}, year = {2016}, pages = {5:1-5:34}, doi = {10.1145/3013516}, month = dec }

@inproceedings{DLM-pnse16, address = {Torun, Poland}, month = jun, year = 2016, volume = 1591, series = {CEUR Workshop Proceedings}, publisher = {CEUR-WS.org}, editor = {Lawrence Cabac and Lars Michael Kristensen and Heiko R{\"o}lke:}, acronym = {{PNSE}'16}, booktitle = {{P}roceedings of the 10th {I}nternational {W}orkshop on {P}etri {N}ets and {S}oftware {E}ngineering ({PNSE}'16)}, author = {Alban Linard and Beno{\^{\i}}t Barbot and Didier Buchs and Maximilien Colange and Cl{\'{e}}ment D{\'{e}}moulins and Lom{-}Messan Hillah and Alexis Martin}, title = {Layered Data: {A} Modular Formal Definition without Formalisms}, pages = {287-306}, url = {http://ceur-ws.org/Vol-1591/}, pdf = {http://ceur-ws.org/Vol-1591/paper19.pdf}, abstract = {Defining formalisms and models in a modular way is a painful task. Metamodeling tools and languages have usually not been created with this goal in mind. This article proposes a data structure, called layered data, that allows defining easily modular abstract syntax for for- malisms and models. It also shows its use through an exhaustive example. As a side effect, this article discusses the notion of formalism, and asserts that they do not exist as standalone objects, but rather as relations between models.} }

*This file was generated by
bibtex2html 1.98.*