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

@incollection{DSS-wqo17, author = {D{\v z}amonja, Mirna and Schmitz, Sylvain and Schnoebelen, {\relax Ph}ilippe}, title = {On ordinal invariants in well quasi orders and finite antichain orders}, booktitle = {Well-quasi orders in computation, logic, language and reasoning}, editor = {Peter Schuster and Monika Seisenberer and Andreas Weiermann}, publisher = {Springer}, series = {Trends in Logic}, url = {https://arxiv.org/abs/1711.00428}, pdf = {https://arxiv.org/pdf/1711.00428}, year = {2019}, optnmonth = {}, abstract = {We investigate the ordinal invariants height, length, and width of well quasi orders (WQO), with particular emphasis on width, an invariant of interest for the larger class of orders with finite antichain condition (FAC). We show that the width in the class of FAC orders is completely determined by the width in the class of WQOs, in the sense that if we know how to calculate the width of any WQO then we have a procedure to calculate the width of any given FAC order. We show how the width of WQO orders obtained via some classical constructions can sometimes be computed in a compositional way. In particular, this allows proving that every ordinal \(\alpha\) can be obtained as the width of some WQO poset. One of the difficult questions is to give a complete formula for the width of Cartesian products of WQOs. Even the width of the product of two ordinals is only known through a complex recursive formula. Although we have not given a complete answer to this question we have advanced the state of knowledge by considering some more complex special cases and in particular by calculating the width of certain products containing three factors. In the course of writing the paper we have discovered that some of the relevant literature was written on cross-purposes and some of the notions rediscovered several times. Therefore we also use the occasion to give a unified presentation of the known results.}, note = {To appear} }

@inproceedings{CLS-jfla19, address = {Lamoura, France}, month = jan, year = 2019, editor = {Nicolas Magaud and Zaynah Dargaye}, acronym = {{JFLA}'19}, booktitle = {{A}ctes des 30{\`e}mes {J}ourn{\'e}es {F}rancophones sur les {L}angages {A}pplicatifs ({JFLA}'19)}, author = {Simon Colin and Rodolphe Lepigre and Gabriel Scherer}, title = {{Unboxing Mutually Recursive Type Definitions}}, pdf = {https://lepigre.fr/files/publications/CLS2019.pdf}, abstract = {In modern OCaml, single-argument datatype declarations (variants with a single constructor, records with a single immutable field) can sometimes be ''unboxed''. This means that their memory representation is the same as their single argument, omitting an indirection through the variant or record constructor, thus achieving better memory efficiency. However, in the case of generalized/guarded algebraic datatypes (GADTs), unboxing is not always possible due to a subtle assumption about the runtime representation of OCaml values. The current correctness check is incomplete, rejecting many valid definitions, in particular those involving mutually-recursive datatype declarations. In this paper, we explain the notion of separability as a semantic for the unboxing criterion, and propose a set of inference rules to check separability. From these inference rules, we derive a new implementation of the unboxing check that properly supports mutually-recursive definitions.}, note = {To appear} }

@inproceedings{AFMS-vmcai2019, address = {Cascais/Lisbon, Portugal}, month = jan, year = 2019, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Enea, Constantin and Piskac, Ruzica}, acronym = {{VMCAI}'19}, booktitle = {{P}roceedings of the 20th {I}nternational {C}onference on {V}erification, {M}odel {C}hecking and {A}bstract {I}nterpretation ({VMCAI}'19)}, author = {Andr{\'e}, {\'E}tienne and Fribourg, Laurent and Mota, Jean-Marc and Soulat, Romain}, title = {Verification of an industrial asynchronous leader election algorithm using abstractions and parametric model checking}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AFMS-vmcai19.pdf}, abstract = {The election of a leader in a network is a challenging task, especially when the processes are asynchronous, i.e., execute an algorithm with time-varying periods. Thales developed an industrial election algorithm with an arbitrary number of processes, that can possibly fail. In this work, we prove the correctness of a variant of this industrial algorithm. We use a method combining abstraction, the SafeProver solver, and a parametric timed model-checker. This allows us to prove the correctness of the algorithm for a large number \(p\) of processes (\(p = 5000\)).}, note = {To appear} }

@inproceedings{HKP-vmcai2019, address = {Cascais/Lisbon, Portugal}, month = jan, year = 2019, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Enea, Constantin and Piskac, Ruzica}, acronym = {{VMCAI}'19}, booktitle = {{P}roceedings of the 20th {I}nternational {C}onference on {V}erification, {M}odel {C}hecking and {A}bstract {I}nterpretation ({VMCAI}'19)}, author = {Haar, Stefan and Kolc{\'a}k, Juraj and Paulev{\'e}, Lo{\"i}c}, title = {{Combining Refinement of Parametric Models with Goal-Oriented Reduction of Dynamics}}, url = {https://hal.archives-ouvertes.fr/hal-01940174/}, pdf = {https://hal.archives-ouvertes.fr/hal-01940174/file/manuscript.pdf}, abstract = {Parametric models abstract part of the specification of dynamical models by integral parameters. They are for example used in computational systems biology, notably with parametric regulatory networks, which specify the global architecture (interactions) of the networks, while parameterising the precise rules for drawing the possible temporal evolutions of the states of the components. A key challenge is then to identify the discrete parameters corresponding to concrete models with desired dynamical properties. This paper addresses the restriction of the abstract execution of parametric regulatory (discrete) networks by the means of static analysis of reachability properties (goal states). Initially defined at the level of concrete parameterised models, the goal-oriented reduction of dynamics is lifted to parametric networks, and is proven to preserve all the minimal traces to the specified goal states. It results that one can jointly perform the refinement of parametric networks (restriction of domain of parameters) while reducing the necessary transitions to explore and preserving reachability properties of interest.}, note = {To appear} }

@article{KS-lmcs19, journal = {Logical Methods in Computer Science}, author = {P. Karandikar and Schnoebelen, {\relax Ph}ilippe}, title = {The height of piecewise-testable languages and the complexity of the logic of subwords}, volume = {15}, number = {2}, pages = {6:1-6:27}, year = {2019}, month = apr, pdf = {https://lmcs.episciences.org/5409/pdf}, url = {https://lmcs.episciences.org/5409}, 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. As an application of these results, we show that \(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{BLS-pods19, address = {Amsterdam, Netherlands}, month = jun # {-} # jul, publisher = {ACM Press}, editor = {Christoph Koch}, acronym = {{PODS}'19}, booktitle = {{P}roceedings of the 38th {A}nnual {ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium on {P}rinciples of {D}atabase {S}ystems ({PODS}'19)}, author = {Baelde, David and Lick, Anthony and Schmitz, Sylvain}, title = {Decidable {XP}ath Fragments in the Real World}, pages = {285-302}, year = 2019, doi = {10.1145/3294052.3319685}, url = {https://hal.inria.fr/hal-01852475}, abstract = {XPath is arguably the most popular query language for selecting elements in XML documents. Besides query evaluation, query satisfiability and containment are the main computational problems for XPath; they are useful, for instance, to detect dead code or validate query optimisations. These problems are undecidable in general, but several fragments have been identified over time for which satisfiability (or query containment) is decidable: CoreXPath 1.0 and 2.0 without so-called data joins, fragments with data joins but limited navigation, etc. However, these fragments are often given in a simplified syntax, and sometimes wrt. a simplified XPath semantics. Moreover, they have been studied mostly with theoretical motivations, with little consideration for the practically relevant features of XPath. To investigate the practical impact of these theoretical fragments, we design a benchmark compiling thousands of real-world XPath queries extracted from open-source projects. These queries are then matched against syntactic fragments from the literature. We investigate how to extend these fragments with seldom-considered features such as free variables, data tests, data joins, and the last() and id() functions, for which we provide both undecidability and decidability results. We analyse the coverage of the original and extended fragments, and further provide a glimpse at which other practically-motivated features might be worth investigating in the future.} }

@article{KSHP-tcs19, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {Kolc{\'a}k, Juraj and {\v S}afr{\'a}nek, David and Haar, Stefan and Paulev{\'e}, Lo{\"i}c}, title = {{Parameter Space Abstraction and Unfolding Semantics of Discrete Regulatory Networks}}, volume = {765}, year = {2019}, pages = {120-144}, doi = {10.1016/j.tcs.2018.03.009}, pdf = {https://hal.archives-ouvertes.fr/hal-01734805/document}, url = {https://hal.archives-ouvertes.fr/hal-01734805/}, abstract = {The modelling of discrete regulatory networks combines a graph specifying the pairwise influences between the variables of the system, and a parametrisation from which can be derived a discrete transition system. Given the influence graph only, the exploration of admissible parametrisations and the behaviours they enable is computationally demanding due to the combinatorial explosions of both parametrisation and reachable state space. This article introduces an abstraction of the parametrisation space and its refinement to account for the existence of given transitions, and for constraints on the sign and observability of influences. The abstraction uses a convex sub-lattice containing the concrete parametrisation space specified by its infimum and supremum parametrisations. It is shown that the computed abstractions are optimal, i.e., no smaller convex sublattice exists. Although the abstraction may introduce over-approximation, it has been proven to be conservative with respect to reachability of states. Then, an unfolding semantics for Parametric Regulatory Networks is defined, taking advantage of concurrency between transitions to provide a compact representation of reachable transitions. A prototype implementation is provided: it has been applied to several examples of Boolean and multi-valued networks, showing its tractability for networks with numerous components.} }

@inproceedings{JGL-lncs11760, volume = 11760, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {M{\'a}rio S. Alvim and Kostas Chatzikokolakis and Carlos Olarte and Franck Valencia}, acronym = {{The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy}}, booktitle = {The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy---Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday}, author = {Goubault{-}Larrecq, Jean}, title = {Fooling the Parallel or Tester with Probability $8/27$}, pages = {313--328}, year = 2019, note = {Updated version on arXiv:1903.12653}, url = {https://arxiv.org/abs/1903.12653}, abstract = {It is well-known that the higher-order language PCF is not fully abstract: there is a program - the so-called parallel or tester, meant to test whether its input behaves as a parallel or - which never terminates on any input, operationally, but is denotationally non-trivial. We explore a probabilistic variant of PCF, and ask whether the parallel or tester exhibits a similar behavior there. The answer is no: operationally, one can feed the parallel or tester an input that will fool it into thinking it is a parallel or. We show that the largest probability of success of such would-be parallel ors is exactly 8/27. The bound is reached by a very simple probabilistic program. The difficult part is to show that that bound cannot be exceeded.} }

@inproceedings{MSHPP-cmsb19, address = {Trieste, Italy}, month = sep, volume = {11773}, series = {Lecture Notes in Bioinformatics}, publisher = {Springer-Verlag}, editor = {Luca Bortolussi and Guido Sanguinetti}, acronym = {{CMSB}'19}, booktitle = {{P}roceedings of the 17th {C}onference on {C}omputational {M}ethods in {S}ystem {B}iology ({CMSB}'19)}, author = {Mandon, Hugues and Su, Cui and Haar, Stefan and Pang, Jun and Paulev{\'e}, Lo{\"i}c}, title = {Sequential Reprogramming of Boolean Networks Made Practical}, pages = {3-19}, doi = {10.1007/978-3-030-31304-3_1}, year = 2019, abstract = {We address the sequential reprogramming of gene regulatory networks modelled as Boolean networks. We develop an attractor-based sequential reprogramming method to compute all sequential reprogramming paths from a source attractor to a target attractor, where only attractors of the network are used as intermediates. Our method is more practical than existing reprogramming methods as it incorporates several practical constraints: (1) only biologically observable states, viz. attractors, can act as intermediates; (2) certain attractors, such as apoptosis, can be avoided as intermediates; (3) certain nodes can be avoided to perturb as they may be essential for cell survival or difficult to perturb with biomolecular techniques; and (4) given a threshold \(k\), all sequential reprogramming paths with no more than \(k\) perturbations are computed. We compare our method with the minimal one-step reprogramming and the minimal sequential reprogramming on a variety of biological networks. The results show that our method can greatly reduce the number of perturbations compared to the one-step reprogramming, while having comparable results with the minimal sequential reprogramming. Moreover, our implementation is scalable for networks of more than 60 nodes.} }

@inproceedings{DGJL-isdt19, address = {Yangzhou, China}, month = jun, volume = 345, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier Science Publishers}, editor = {Jung, Achim and Li, Qingguo and Xu, Luoshan and Zhang, Guo-Qiang}, acronym = {{ISDT}'19}, booktitle = {{P}roceedings of the {I}nternational {S}ymposium on {D}omain {T}heory ({ISDT}'19)}, author = {de Brecht, Matthew and Goubault{-}Larrecq, Jean and Jia, Xiaodong and Lyu, Zhenchao}, title = {Domain-complete and LCS-complete Spaces}, pages = {3-35}, doi = {10.1016/j.entcs.2019.07.014}, year = 2019 }

@inproceedings{GJ-isdt19, address = {Yangzhou, China}, month = jun, volume = 345, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier Science Publishers}, editor = {Jung, Achim and Li, Qingguo and Xu, Luoshan and Zhang, Guo-Qiang}, acronym = {{ISDT}'19}, booktitle = {{P}roceedings of the {I}nternational {S}ymposium on {D}omain {T}heory ({ISDT}'19)}, author = {Goubault{-}Larrecq, Jean and Jia, Xiaodong}, title = {Algebras of the Extended Probabilistic Powerdomain Monad}, pages = {37-61}, doi = {10.1016/j.entcs.2019.07.015}, year = 2019 }

@article{GM-hjm19, publisher = {University of Houston}, journal = {Houston Journal of Mathematics}, author = {Goubault{-}Larrecq, Jean and Mynard, Fr{\'e}d{\'e}ric}, title = {Convergence without Points}, year = 2019, note = {To appear} }

@techreport{DH-hal19, author = {Donatelli, Susanna and Haddad, Serge}, institution = {HAL}, month = oct, note = {23~pages}, number = {hal-02306021}, type = {Research Report}, title = {{Autonomous Transitions Enhance CSLTA Expressiveness and Conciseness}}, year = {2019}, url = {https://hal.inria.fr/hal-02306021}, pdf = {https://hal.inria.fr/hal-02306021/document}, abstract = {CSLTA is a stochastic temporal logic for continuous-time Markov chains (CTMC) where formulas similarly to those of CTL* are inductively defined by nesting of timed path formulas and state formulas. In particular a timed path formula of CSLTA is specified by a single-clock Deterministic Timed Automaton (DTA). Such a DTA features two kinds of transitions: synchronizing transitions triggered by CTMC transitions and autonomous transitions triggered by time elapsing that change the location of the DTA when the clock reaches a given threshold. It has already been shown that CSLTA strictly includes stochastic logics like CSL and asCSL. An interesting variant of CSLTA consists in equipping transitions rather than locations by boolean formulas. Here we answer the following question: do autonomous transitions and/or boolean guards on transitions enhance expressiveness and/or conciseness of DTAs? We show that this is indeed the case. In establishing our main results we also identify an accurate syntactical characterization of DTAs for which the autonomous transitions do not add expressive power but lead to exponentially more concise DTAs.} }

@inproceedings{GF-fsttcs19, address = {Bombay, India}, month = dec, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Arkadev Chattopadhyay and Paul Gastin}, acronym = {{FSTTCS}'19}, booktitle = {{P}roceedings of the 39th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'19)}, author = {Ekanshdeep Gupta and Alain Finkel}, title = {The well structured problem for Presburger counter machines}, note = {To appear}, year = 2019 }

@inproceedings{BBM-fsttcs19, address = {Bombay, India}, month = dec, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Arkadev Chattopadhyay and Paul Gastin}, acronym = {{FSTTCS}'19}, booktitle = {{P}roceedings of the 39th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'19)}, author = {Nathalie Bertrand and Patricia Bouyer and Anirban Majumdar}, title = {Concurrent parameterized games}, note = {To appear}, year = 2019 }

@article{BQS-lmcs19, journal = {Logical Methods in Computer Science}, author = {Bollig, Benedikt and Quaas, Karin and Sangnier, Arnaud}, title = {The Complexity of Flat Freeze LTL}, volume = {15}, number = {3}, pages = {32:1-32:26}, year = 2019, doi = {10.23638/LMCS-15(3:32)2019}, pdf = {https://lmcs.episciences.org/5795/pdf}, url = {https://arxiv.org/abs/1609.06124}, abstract = {We consider the model-checking problem for freeze LTL on one-counter automata (OCA). Freeze LTL extends LTL with the freeze quantifier, which allows one to store different counter values of a run in registers so that they can be compared with one another. As the model-checking problem is undecidable in general, we focus on the flat fragment of freeze LTL, in which the usage of the freeze quantifier is restricted. In a previous work, Lechner et al. showed that model checking for flat freeze LTL on OCA with binary encoding of counter updates is decidable and in 2NEXPTIME. In this paper, we prove that the problem is, in fact, NEXPTIME-complete no matter whether counter updates are encoded in unary or binary. Like Lechner et al., we rely on a reduction to the reachability problem in OCA with parameterized tests (OCA(P)). The new aspect is that we simulate OCA(P) by alternating two-way automata over words. This implies an exponential upper bound on the parameter values that we exploit towards an NP algorithm for reachability in OCA(P) with unary updates. We obtain our main result as a corollary. As another application, relying on a reduction by Bundala and Ouaknine, one obtains an alternative proof of the known fact that reachability in closed parametric timed automata with one parametric clock is in NEXPTIME.} }

@article{DF-jlc19, publisher = {Oxford University Press}, journal = {Journal of Logic and Computation}, author = {Demri, St{\'e}phane and Fervari, Raul}, title = {The power of modal separation logics}, year = 2019, note = {To appear} }

@inproceedings{SZ-rp19, address = {Brussels, Belgium}, month = sep, volume = {11674}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Rapha{\"e}l Jungers and Emmanuel Fillot and Igor Potapov}, acronym = {{RP}'19}, booktitle = {{P}roceedings of the 13th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'19)}, author = {Sylvain Schmitz and Georg Zetzsche}, title = {Coverability Is Undecidable in One-Dimensional Pushdown Vector Addition Systems with Resets}, year = 2019, pages = {193-201}, pdf = {https://arxiv.org/pdf/1906.07069.pdf}, url = {https://arxiv.org/abs/1906.07069}, doi = {10.1007/978-3-030-30806-3_15}, abstract = {We consider the model of pushdown vector addition systems with resets. These consist of vector addition systems that have access to a pushdown stack and have instructions to reset counters. For this model, we study the coverability problem. In the absence of resets, this problem is known to be decidable for one-dimensional pushdown vector addition systems, but decidability is open for general pushdown vector addition systems. Moreover, coverability is known to be decidable for reset vector addition systems without a pushdown stack. We show in this note that the problem is undecidable for one-dimensional pushdown vector addition systems with resets.} }

@inproceedings{BGH-fscd19, address = {Dortmund, Germany}, month = jun, volume = {131}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Herman Geuvers}, acronym = {{FSCD}'19}, booktitle = {{P}roceedings of the 4th International Conference on Formal Structures for Computation and Deduction ({FSCD}'19)}, author = {Fr{\'e}d{\'e}ric Blanqui and Guillaume Genestier and Olivier Hermant}, title = {Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting}, pages = {9:1-9:21}, doi = {10.4230/LIPIcs.FSCD.2019.9}, year = 2019, pdf = {http://drops.dagstuhl.de/opus/volltexte/2019/10516/pdf/LIPIcs-FSCD-2019-9.pdf}, url = {http://drops.dagstuhl.de/opus/volltexte/2019/10516/}, abstract = {Dependency pairs are a key concept at the core of modern automated termination provers for first-order term rewriting systems. In this paper, we introduce an extension of this technique for a large class of dependently-typed higher-order rewriting systems. This extends previous results by Wahlstedt on the one hand and the first author on the other hand to strong normalization and non-orthogonal rewriting systems. This new criterion is implemented in the type-checker Dedukti.} }

@inproceedings{DD-fscd19, address = {Dortmund, Germany}, month = jun, volume = {131}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Herman Geuvers}, acronym = {{FSCD}'19}, booktitle = {{P}roceedings of the 4th International Conference on Formal Structures for Computation and Deduction ({FSCD}'19)}, author = {Alejandro {D{\'i}az-Caro} and Gilles Dowek}, title = {Proof Normalisation in a Logic Identifying Isomorphic Propositions}, pages = {14:1-14:23}, doi = {10.4230/LIPIcs.FSCD.2019.14}, year = 2019, pdf = {http://drops.dagstuhl.de/opus/volltexte/2019/10521/pdf/LIPIcs-FSCD-2019-14.pdf}, url = {http://drops.dagstuhl.de/opus/volltexte/2019/10521/}, abstract = {We define a fragment of propositional logic where isomorphic propositions, such as A wedge B and B wedge A, or A ==> (B wedge C) and (A ==> B) wedge (A ==> C) are identified. We define System I, a proof language for this logic, and prove its normalisation and consistency.} }

@inproceedings{GMG-dlt19, address = {Warsaw, Poland}, month = aug, volume = {11647}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Piotrek Hofman and Micha\l Skrzypczak}, acronym = {{DLT}'19}, booktitle = {{P}roceedings of the 23th {I}nternational {C}onference on {D}evelopments in {L}anguage {T}heory ({DLT}'19)}, author = {Paul Gastin and Amaldev Manuel and R. Govind}, title = {Logics for Reversible Regular Languages and Semigroups with Involution}, pages = {182-191}, doi = {10.1007/978-3-030-24886-4_13}, year = 2019, pdf = {https://arxiv.org/pdf/1907.01214.pdf}, url = {https://arxiv.org/abs/1907.01214}, abstract = {We present MSO and FO logics with predicates ``between'' and ``neighbour'' that characterise various fragments of the class of regular languages that are closed under the reverse operation. The standard connections that exist between MSO and FO logics and varieties of finite semigroups extend to this setting with semigroups extended with an involution. The case is different for FO with neighbour relation where we show that one needs additional equations to characterise the class.} }

@inproceedings{Gastin-cai19, address = {Ni{\u s}, Serbia}, month = jun, volume = 11545, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Miroslav {\'C}iri{\'c} and Manfred Droste and Jean-{\'E}ric Pin}, acronym = {{CAI}'19}, booktitle = {{P}roceedings of the 8th {I}nternational {C}onference on {A}lgebraic {I}nformatics ({CAI}'19)}, author = {Gastin, Paul}, title = {Modular Descriptions of Regular Functions}, pages = {3-9}, doi = {}, note = {Invited talk}, year = 2019, doi = {10.1007/978-3-030-21363-3_1}, abstract = {We discuss various formalisms to describe string-to-string transformations. Many are based on automata and can be seen as operational descriptions, allowing direct implementations when the input scanner is deterministic. Alternatively, one may use more human friendly descriptions based on some simple basic transformations (e.g., copy, duplicate, erase, reverse) and various combinators such as function com- position or extensions of regular operations.} }

@article{CHKPT-nc19, publisher = {Springer}, journal = {Natural Computing}, author = {Chatain, {\relax Th}omas and Haar, Stefan and Kolc{\'a}k, Juraj and Paulev{\'e}, Lo{\"i}c and Thakkar, Aalok}, title = {Concurrency in {Boolean} networks}, year = 2019, note = {To appear}, pdf = {https://hal.inria.fr/hal-01893106v2/document}, url = {https://link.springer.com/article/10.1007/s11047-019-09748-4}, abstract = {Boolean networks (BNs) are widely used to model the qualitative dynamics of biological systems. Besides the logical rules determining the evolution of each component with respect to the state of its regulators, the scheduling of component updates can have a dramatic impact on the predicted behaviours. In this paper, we explore the use of Read (contextual) Petri Nets (RPNs) to study dynamics of BNs from a concurrency theory perspective. After showing bi-directional translations between RPNs and BNs and analogies between results on synchronism sensitivity, we illustrate that usual updating modes for BNs can miss plausible behaviours, i.e., incorrectly conclude on the absence/impossibility of reaching specific configurations. We propose an encoding of BNs capitalizing on the RPN semantics enabling more behaviour than the generalized asynchronous updating mode. The proposed encoding ensures a correct abstraction of any multivalued refinement, as one may expect to achieve when modelling biological systems with no assumption on its time features.} }

@inproceedings{K-csf19, address = {Hoboken, NJ, USA}, month = jul, publisher = {{IEEE} Computer Society Press}, editor = {Delaune, St{\'e}phanie and Jia, Limin}, acronym = {{CSF}'19}, booktitle = {{P}roceedings of the 31st {IEEE} {C}omputer {S}ecurity {F}oundations {S}ymposium ({CSF}'19)}, author = {Adrien Koutsos}, title = {Decidability of a Sound Set of Inference Rules for Computational Indistinguishability}, pages = {48-61}, year = 2019, doi = {10.1109/CSF.2019.00011}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/K-csf19.pdf}, abstract = {Computational indistinguishability is a key property in cryptography and verification of security protocols. Current tools for proving it rely on cryptographic game transformations. We follow Bana and Comon's approach, axiomatizing what an adversary cannot distinguish. We prove the decidability of a set of first-order axioms which are computationally sound, though incomplete, for protocols with a bounded number of sessions whose security is based on an IND-CCA_2 encryption scheme. Alternatively, our result can be viewed as the decidability of a family of cryptographic game transformations. Our proof relies on term rewriting and automated deduction techniques.} }

@inproceedings{K-eurosp19, address = {Stockholm, Sweden}, month = jun, publisher = {{IEEE} Press}, editor = {Frank Piessens and Frank Stajano}, acronym = {{EuroS\&P}'19}, booktitle = {{P}roceedings of the 4th IEEE European Symposium on Security and Privacy ({EuroS\&P}'19)}, author = {Adrien Koutsos}, title = {The {5G-AKA} Authentication Protocol Privacy}, pages = {464-479}, year = 2019, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/K-eurosp19.pdf}, doi = {10.1109/EuroSP.2019.00041}, abstract = {We study the 5G-AKA authentication protocol described in the 5G mobile communication standards. This version of AKA tries to achieve a better privacy than the 3G and 4G versions through the use of asymmetric randomized encryption. Nonetheless, we show that except for the IMSI-catcher attack, all known attacks against 5G-AKA privacy still apply. Next, we modify the 5G-AKA protocol to prevent these attacks, while satisfying 5G-AKA efficiency constraints as much as possible. We then formally prove that our protocol is sigma-unlinkable. This is a new security notion, which allows for a fine-grained quantification of a protocol privacy. Our security proof is carried out in the Bana-Comon indistinguishability logic. We also prove mutual authentication as a secondary result.} }

@article{JGL-topa19, publisher = {Elsevier Science Publishers}, journal = {Topology and its Applications}, author = {Goubault{-}Larrecq, Jean}, title = {Formal Ball Monads}, year = 2019, note = {To appear}, doi = {10.1016/j.topol.2019.06.044}, url = {http://www.sciencedirect.com/science/article/pii/S0166864119302160}, abstract = {The formal ball construction B is a central tool of quasi-metric space theory. We show that it induces monads on certain natural categories of quasi-metric spaces, with 1-Lipschitz maps as morphisms, or with 1-Lipschitz continuous maps as morphisms. Those are left Kock-Zöberlein monads, and that allows us to characterize their algebras exactly. As an application, we study so-called Lipschitz regular spaces, a natural class of spaces that contain all standard algebraic quasi-metric spaces with relatively compact balls, in particular all metric spaces whose closed balls are compact. There are other Lipschitz regular spaces, as we show, and notably all B-algebras. That includes all spaces of formal balls, with their d+-Scott topology. The value of Lipschitz regularity is that, for a Lipschitz regular standard quasi-metric space X,d, the space LX of lower semicontinuous maps from X to the extended non-negative reals, with the Scott topology, retracts onto each of the spaces L_alpha(X,d) of alpha-Lipschitz continuous maps, and that the subspace topology on the latter coincides with the Scott topology.} }

@inproceedings{GMS-cav19, address = {New York, USA}, month = jul, volume = {11561}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Isil Dillig and Serdar Tasiran}, acronym = {{CAV}'19}, booktitle = {{P}roceedings of the 31st {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV}'19)}, author = {Paul Gastin and Sayan Mukherjee and B. Srivathsan}, title = {Fast algorithms for handling diagonal constraints in timed automata}, pages = {41-59}, year = 2019, doi = {10.1007/978-3-030-25540-4_3}, url = {https://arxiv.org/abs/1904.08590} }

@inproceedings{BCC-atpn19, address = {Aachen, Germany}, month = jun, year = 2019, volume = {11522}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Susanna Donatelli and Stefan Haar}, acronym = {{PETRI~NETS}'19}, booktitle = {{P}roceedings of the 40th {I}nternational {C}onference on {A}pplications and {T}heory of {P}etri {N}ets ({PETRI~NETS}'19)}, author = {Mathilde Boltenhagen and Thomas Chatain and Josep Carmona}, title = {Generalized Alignment-Based Trace Clustering of Process Behavior}, pages = {237-257}, url = {https://link.springer.com/chapter/10.1007/978-3-030-21571-2_14}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCC-atpn19.pdf}, doi = {10.1007/978-3-030-21571-2_14}, abstract = {Process mining techniques use event logs containing real process executions in order to mine, align and extend process models. The partition of an event log into trace variants facilitates the understanding and analysis of traces, so it is a common pre-processing in process mining environments. Trace clustering automates this partition; traditionally it has been applied without taking into consideration the availability of a process model. In this paper we extend our previous work on process model based trace clustering, by allowing cluster centroids to have a complex structure, that can range from a partial order, down to a subnet of the initial process model. This way, the new clustering framework presented in this paper is able to cluster together traces that are distant only due to concurrency or loop constructs in process models. We show the complexity analysis of the different instantiations of the trace clustering framework, and have implemented it in a prototype tool that has been tested on different datasets.} }

@inproceedings{BBM-mfcs19, address = {Aachen, Germany}, month = aug, volume = {138}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Pinar Heggernes and Joost-Pieter Katoen and Peter Rossmanith}, acronym = {{MFCS}'19}, booktitle = {{P}roceedings of the 42nd {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'19)}, author = {Manfred Droste and Paul Gastin}, title = {Aperiodic Weighted Automata and Weighted First-Order Logic}, pages = {76:1-76:15}, year = 2019, doi = {10.4230/LIPIcs.MFCS.2019.76}, pdf = {http://drops.dagstuhl.de/opus/volltexte/2019/11020/pdf/LIPIcs-MFCS-2019-76.pdf}, url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11020} }

@inproceedings{BT-mfcs19, address = {Aachen, Germany}, month = aug, volume = {138}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Pinar Heggernes and Joost-Pieter Katoen and Peter Rossmanith}, acronym = {{MFCS}'19}, booktitle = {{P}roceedings of the 42nd {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'19)}, author = {Patricia Bouyer and Nathan Thomasset}, title = {Nash equilibria in games over graphs equipped with a communication mechanism}, pages = {9:1-9:14}, year = 2019, doi = {10.4230/LIPIcs.MFCS.2019.9}, pdf = {http://drops.dagstuhl.de/opus/volltexte/2019/10953/pdf/LIPIcs-MFCS-2019-9.pdf}, url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=10953} }

@inproceedings{BBM-concur19, address = {Amsterdam, The Netherlands}, month = aug, volume = {140}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Wan Fokkink and Rob {van Glabbeek}}, acronym = {{CONCUR}'19}, booktitle = {{P}roceedings of the 30th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'19)}, author = {Nathalie Bertrand and Patricia Bouyer and Anirban Majumdar}, title = {Reconfiguration and message losses in parameterized broadcast networks}, pages = {32:1-32:15}, year = 2019, doi = {10.4230/LIPIcs.CONCUR.2019.32}, pdf = {http://drops.dagstuhl.de/opus/volltexte/2019/10934/pdf/LIPIcs-CONCUR-2019-32.pdf}, url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=10934} }

@inproceedings{FP-concur19, address = {Amsterdam, The Netherlands}, month = aug, volume = {140}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Wan Fokkink and Rob {van Glabbeek}}, acronym = {{CONCUR}'19}, booktitle = {{P}roceedings of the 30th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'19)}, author = {Alain Finkel and M. Praveen}, title = {Verification of Flat FIFO Systems}, pages = {12:1-12:17}, year = 2019, doi = {10.4230/LIPIcs.CONCUR.2019.12}, pdf = {http://drops.dagstuhl.de/opus/volltexte/2019/10914/pdf/LIPIcs-CONCUR-2019-12.pdf}, url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=10914}, abstract = {The decidability and complexity of reachability problems and model-checking for flat counter systems have been explored in detail. However, only few results are known for flat FIFO systems, only in some particular cases (a single loop or a single bounded expression). We prove, by establishing reductions between properties, and by reducing SAT to a subset of these properties that many verification problems like reachability, non-termination, unboundedness are NP-complete for flat FIFO systems, generalizing similar existing results for flat counter systems. We construct a trace-flattable counter system that is bisimilar to a given flat FIFO system, which allows to model-check the original flat FIFO system. Our results lay the theoretical foundations and open the way to build a verification tool for (general) FIFO systems based on analysis of flat subsystems.} }

@article{HBD-jcs19, publisher = {{IOS} Press}, journal = {Journal of Computer Security}, author = {Hirschi, Lucca and Baelde, David and Delaune, St{\'e}phanie}, title = {A method for unbounded verification of privacy-type properties}, volume = {27}, number = {3}, pages = {277-342}, year = 2019, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HBD-jcs19.pdf}, doi = {10.3233/JCS-171070}, url = {https://content.iospress.com/articles/journal-of-computer-security/jcs171070} }

@article{GBM-tocsys19, publisher = {Springer}, journal = {Theory of Computing Systems}, author = {Gardy, Patrick and Bouyer, Patricia and Markey, Nicolas}, title = {Dependences in Strategy Logic}, year = 2019, note = {To appear}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GBM-tocsys19.pdf}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GBM-tocsys19.pdf} }

@inproceedings{BKMMMP-ijcai19, futureaddress = {}, month = jul, publisher = {IJCAI organization}, editor = {Kraus, Sarit}, acronym = {{IJCAI}'19}, booktitle = {{P}roceedings of the 28th {I}nternational {J}oint {C}onference on {A}rtificial {I}ntelligence ({IJCAI}'19)}, author = {Bouyer, Patricia and Kupferman, Orna and Markey, Nicolas and Maubert, Bastien and Murano, Aniello and Perelli, Giuseppe}, title = {Reasoning about Quality and Fuzziness of Strategic Behaviours}, pages = {1588-1594}, year = 2019, doi = {10.24963/ijcai.2019/220}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKMMMP-ijcai19.pdf}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKMMMP-ijcai19.pdf} }

@inproceedings{BD-aamas19, address = {Montreal, Canada}, month = jun, publisher = {ACM Press}, acronym = {{AAMAS}'19}, booktitle = {{P}roceedings of the 18th {I}nternational {J}oint {C}onference on {A}utonomous {A}gents and {M}ulti-{A}gent {S}ystems ({AAMAS}'19)}, author = {Belardinelli, Francesco and Demri, St{\'e}phane}, title = {Resource-bounded ATL: the Quest for Tractable Fragments}, pages = {206--214}, year = 2019, pdf = {http://www.ifaamas.org/Proceedings/aamas2019/pdfs/p206.pdf}, url = {http://www.ifaamas.org/Proceedings/aamas2019/forms/contents.htm#3F} }

@article{MSPPHP-ipl19, publisher = {ACM Press}, journal = {IEEE/ACM Transaction on Computational Biology and Bioinformatics}, author = {Mandon, Hugues and Su, Cui and Pang, Jun and Paul, Soumya and Haar, Stefan and Paulev{\'e}, Lo{\"i}c}, title = {Algorithms for the Sequential Reprogramming of Boolean Networks}, year = 2019, note = {To appear}, pdf = {https://hal.archives-ouvertes.fr/hal-02113864/file/main.pdf}, url = {https://hal.archives-ouvertes.fr/hal-02113864} }

@inproceedings{Schmitz-icalp19, address = {Patras, Greece}, month = jul, volume = {132}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Chatzigiannakis, Ioannis and Merelli, Emanuela}, acronym = {{ICALP}'19}, booktitle = {{P}roceedings of the 46th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'19)}, author = {Schmitz, Sylvain}, title = {The Parametric Complexity of Lossy Counter Machines}, year = 2019, pages = {129:1-129:15}, doi = {10.4230/LIPIcs.ICALP.2019.129}, pdf = {https://hal.archives-ouvertes.fr/hal-02020728v2/document}, url = {http://drops.dagstuhl.de/opus/volltexte/2019/10705/}, abstract = {The reachability problem in lossy counter machines is the best-known ACKERMANN-complete problem and has been used to establish most of the ACKERMANN-hardness statements in the literature. This hides however a complexity gap when the number of counters is fixed. We close this gap and prove F_d-completeness for machines with d counters, which provides the first known uncontrived problems complete for the fast-growing complexity classes at levels 3 < d < omega. We develop for this an approach through antichain factorisations of bad sequences and analysing the length of controlled antichains.} }

@inproceedings{Fortin-icalp19, address = {Patras, Greece}, month = jul, volume = {132}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Chatzigiannakis, Ioannis and Merelli, Emanuela}, acronym = {{ICALP}'19}, booktitle = {{P}roceedings of the 46th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'19)}, author = {Fortin, Marie}, title = {FO = FO3 for linear orders with monotone binary relations}, year = 2019, pages = {116:1-116:13}, doi = {10.4230/LIPIcs.ICALP.2019.116}, pdf = {http://drops.dagstuhl.de/opus/volltexte/2019/10692/pdf/LIPIcs-ICALP-2019-116.pdf}, url = {http://drops.dagstuhl.de/opus/volltexte/2019/10692/}, abstract = {We show that over the class of linear orders with additional binary relations satisfying some monotonicity conditions, monadic first-order logic has the three-variable property. This generalizes (and gives a new proof of) several known results, including the fact that monadic first-order logic has the three-variable property over linear orders, as well as over (R, <, +1), and answers some open questions mentioned in a paper from Antonopoulos, Hunter, Raza and Worrell [FoSSaCS 2015]. Our proof is based on a translation of monadic first-order logic formulas into formulas of a star-free variant of Propositional Dynamic Logic, which are in turn easily expressible in monadic first-order logic with three variables.} }

@inproceedings{DFM-jelia19, address = {Rende, Italy}, month = jun, year = 2019, volume = 11468, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, editor = {Calimeri, Francesco and Leone, Nicola and Manna, Marco}, acronym = {{JELIA}'19}, booktitle = {{P}roceedings of the 16th {E}uropean {C}onference on {L}ogics in {A}rtificial {I}ntelligence ({JELIA}'19)}, author = {Demri, St{\'e}phane and Fervari, Raul and Mansutti, Alessio}, title = {Axiomatising logics with separating conjunctions and modalities}, pages = {692-708}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DFM-jelia19.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DFM-jelia19.pdf}, doi = {10.1007/978-3-030-19570-0_45} }

@article{HS-ipl19, publisher = {Elsevier Science Publishers}, journal = {Information Processing Letters}, author = {Halfon, Simon and Schnoebelen, {\relax Ph}ilippe}, title = {On shuffle products, acyclic automata and piecewise-testable languages}, volume = {145}, pages = {68-73}, year = 2019, doi = {10.1016/j.ipl.2019.01.012}, abstract = {We show that the shuffle $L\unicode{x29E2} F$ of a piecewise-testable language $L$ and a finite language $F$ is piecewise-testable. The proof relies on a classic but little-used automata-theoretic characterization of piecewise-testable languages. We also discuss some mild generalizations of the main result, and provide bounds on the piecewise complexity of $L\unicode{x29E2} F$.} }

@inproceedings{BGJKS-csf19, address = {Hoboken, NJ, USA}, month = jul, publisher = {{IEEE} Computer Society Press}, editor = {Delaune, St{\'e}phanie and Jia, Limin}, acronym = {{CSF}'19}, booktitle = {{P}roceedings of the 31st {IEEE} {C}omputer {S}ecurity {F}oundations {S}ymposium ({CSF}'19)}, author = {Barthe, Gilles and Gr{\'e}goire, Benjamin and Jacomme, Charlie and Kremer, Steve and Strub, Pierre-Yves}, title = {Symbolic methods in computational cryptography proofs}, pages = {136-151}, year = 2019, doi = {10.1109/CSF.2019.00017}, pdf = {https://hal.inria.fr/hal-02117794/document}, url = {https://hal.inria.fr/hal-02117794}, abstract = {Code-based game-playing is a popular methodology for proving security of cryptographic constructions and side-channel countermeasures. This methodology relies on treating cryptographic proofs as an instance of relational program verification (between probabilistic programs), and decomposing the latter into a series of elementary relational program verification steps. In this paper, we develop principled methods for proving such elementary steps for probabilistic programs that operate over finite fields and related algebraic structures. We focus on three essential properties: program equivalence, information flow, and uniformity. We give characterizations of these properties based on deducibility and other notions from symbolic cryptography. We use (sometimes improve) tools from symbolic cryptography to obtain decision procedures or sound proof methods for program equivalence, information flow, and uniformity. Finally, we evaluate our approach using examples drawn from provable security and from side-channel analysis-for the latter, we focus on the masking countermeasure against differential power analysis. A partial implementation of our approach is integrated in EASYCRYPT, a proof assistant for provable security, and in MASKVERIF, a fully automated prover for masked implementations.} }

@inproceedings{FHK-atpn19, address = {Aachen, Germany}, month = jun, year = 2019, volume = {11522}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Susanna Donatelli and Stefan Haar}, acronym = {{PETRI~NETS}'19}, booktitle = {{P}roceedings of the 40th {I}nternational {C}onference on {A}pplications and {T}heory of {P}etri {N}ets ({PETRI~NETS}'19)}, author = {Finkel, Alain and Haddad, Serge and Khmelnitsky, Igor}, title = {Coverability and Termination in Recursive Petri Nets}, pages = { 429-448}, url = {https://hal.inria.fr/hal-02081019}, pdf = {https://hal.inria.fr/hal-02081019/document}, doi = {10.1007/978-3-030-21571-2_23}, abstract = {In the early two-thousands, Recursive Petri nets have been introduced in order to model distributed planning of multi-agent systems for which counters and recursivity were necessary. Although Recursive Petri nets strictly extend Petri nets and stack automata, most of the usual property problems are solvable but using non primitive recursive algorithms, even for coverability and termination. For almost all other extended Petri nets models containing a stack the complexity of coverability and termination are unknown or strictly larger than EXPSPACE. In contrast, we establish here that for Recursive Petri nets, the coverability and termination problems are EXPSPACE-complete as for Petri nets. From an expressiveness point of view, we show that coverability languages of Recursive Petri nets strictly include the union of coverability languages of Petri nets and context-free languages. Thus we get for free a more powerful model than Petri net.} }

@inproceedings{JGL-lics19, address = {Vancouver, Canada}, month = jun, publisher = {{IEEE} Press}, editor = {Bouyer, Patricia}, acronym = {{LICS}'19}, booktitle = {{P}roceedings of the 34th {A}nnual {ACM\slash IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'19)}, author = {Goubault{-}Larrecq, Jean}, title = {A Probabilistic and Non-Deterministic Call-by-Push-Value Language}, pages = {1-13}, year = 2019, doi = {10.1109/LICS.2019.8785809}, abstract = {There is no known way of giving a domain-theoretic semantics to higher-order probabilistic languages, in such a way that the involved domains are continuous or quasi-continuous. We argue that the problem naturally disappears for languages with two kinds of types, where one kind is interpreted in a Cartesian-closed category of continuous dcpos, and the other is interpreted in a category that is closed under the probabilistic powerdomain functor. Such a setting is provided by Paul B. Levy's call-by-push-value paradigm. Following this insight, we define a call-by-push-value language, with probabilistic choice sitting inside the value types, and where conversion from a value type to a computation type involves demonic non-determinism. We give both a domain-theoretic semantics and an operational semantics for the resulting language, and we show that they are sound and adequate. With the addition of statistical termination testers and parallel if, we show that the language is even fully abstract-and those two primitives are required for that.} }

@inproceedings{AGJK-lics19, address = {Vancouver, Canada}, month = jun, publisher = {{IEEE} Press}, editor = {Bouyer, Patricia}, acronym = {{LICS}'19}, booktitle = {{P}roceedings of the 34th {A}nnual {ACM\slash IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'19)}, author = {Akshay, S. and Gastin, Paul and Jug{\'e}, Vincent and Krishna, Shankara Narayanan}, title = {Timed systems through the lens of logic}, pages = {1-13}, year = 2019, doi = {10.1109/LICS.2019.8785684}, pdf = {https://arxiv.org/pdf/1903.03773.pdf}, url = {https://arxiv.org/abs/1903.03773}, abstract = {In this paper, we analyze timed systems with data structures, using a rich interplay of logic and properties of graphs. We start by describing behaviors of timed systems using graphs with timing constraints. Such a graph is called realizable if we can assign time-stamps to nodes or events so that they are consistent with the timing constraints. The logical definability of several graph properties has been a challenging problem, and we show, using a highly non-trivial argument, that the realizability property for collections of graphs with strict timing constraints is logically definable in a class of propositional dynamic logic (EQ-ICPDL), which is strictly contained in MSO. Using this result, we propose a novel, algorithmically efficient and uniform proof technique for the analysis of timed systems enriched with auxiliary data structures, like stacks and queues. Our technique unravels new results (for emptiness checking as well as model checking) for timed systems with richer features than considered so far, while also recovering existing results.} }

@inproceedings{BD-lics19, address = {Vancouver, Canada}, month = jun, publisher = {{IEEE} Press}, editor = {Bouyer, Patricia}, acronym = {{LICS}'19}, booktitle = {{P}roceedings of the 34th {A}nnual {ACM\slash IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'19)}, author = {Bednarczyk, Bartosz and Demri, St{\'e}phane}, title = {Why propositional quantification makes modal logics on trees robustly hard ?}, pages = {1-13}, year = 2019, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BD-lics2019.pdf}, doi = {10.1109/LICS.2019.8785656} }

@inproceedings{CD-lics19, address = {Vancouver, Canada}, month = jun, publisher = {{IEEE} Press}, editor = {Bouyer, Patricia}, acronym = {{LICS}'19}, booktitle = {{P}roceedings of the 34th {A}nnual {ACM\slash IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'19)}, author = {Chatterjee, Krishnendu and Doyen, Laurent}, title = {Graph Planning with Expected Finite Horizon}, pages = {1-13}, year = 2019, doi = {10.1109/LICS.2019.8785706}, abstract = {Graph planning gives rise to fundamental algorithmic questions such as shortest path, traveling salesman problem, etc. A classical problem in discrete planning is to consider a weighted graph and construct a path that maximizes the sum of weights for a given time horizon T. However, in many scenarios, the time horizon is not fixed, but the stopping time is chosen according to some distribution such that the expected stopping time is T. If the stopping time distribution is not known, then to ensure robustness, the distribution is chosen by an adversary, to represent the worst-case scenario. A stationary plan for every vertex always chooses the same outgoing edge. For fixed horizon or fixed stopping-time distribution, stationary plans are not sufficient for optimality. Quite surprisingly we show that when an adversary chooses the stopping-time distribution with expected stopping time T, then stationary plans are sufficient. While computing optimal stationary plans for fixed horizon is NP-complete, we show that computing optimal stationary plans under adversarial stopping-time distribution can be achieved in polynomial time. Consequently, our polynomial-time algorithm for adversarial stopping time also computes an optimal plan among all possible plans.} }

@inproceedings{LS-lics19, address = {Vancouver, Canada}, month = jun, publisher = {{IEEE} Press}, editor = {Bouyer, Patricia}, acronym = {{LICS}'19}, booktitle = {{P}roceedings of the 34th {A}nnual {ACM\slash IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'19)}, author = {J{\'e}r{\^o}me Leroux and Schmitz, Sylvain}, title = {Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension}, pages = {1-13}, year = 2019, doi = {10.1109/LICS.2019.8785796}, url = {https://arxiv.org/abs/1903.08575}, abstract = {The reachability problem in vector addition systems is a central question, not only for the static verification of these systems, but also for many inter-reducible decision problems occurring in various fields. The currently best known upper bound on this problem is not primitive-recursive, even when considering systems of fixed dimension. We provide significant refinements to the classical decomposition algorithm of Mayr, Kosaraju, and Lambert and to its termination proof, which yield an ACKERMANN upper bound in the general case, and primitive-recursive upper bounds in fixed dimension. While this does not match the currently best known TOWER lower bound for reachability, it is optimal for related problems.} }

@article{LS-icomp19, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Ranko Lazi\'c and Sylvain Schmitz}, title = {The Ideal View on {R}ackoff's Coverability Technique}, url = {https://hal.inria.fr/hal-01176755}, year = 2019, note = {To appear}, abstract = {Well-structured transition systems form a large class of infinite-state systems, for which safety verification is decidable thanks to a generic backward coverability algorithm. However, for several classes of systems, the generic upper bounds one can extract from the algorithm are far from optimal. In particular, in the case of vector addition systems (VAS) and several of their extensions, the known tight upper bounds were rather derived thanks to ad-hoc arguments based on Rackoff's small witness property. We show how to derive the same bounds directly on the computations of the VAS instantiation of the generic backward coverability algorithm. This relies on a dual view of the algorithm using ideal decompositions of downwards-closed sets, which exhibits a key structural invariant in the VAS case. This reasoning offers a uniform setting for all well-structured transition systems, including branching ones, and we further apply it to several VAS extensions: we derive optimal upper bounds for coverability in branching and alternating VAS, matching the previously known results from the literature.} }

@inproceedings{MFNS-async19, address = {Hirosaki, Japan}, month = may, publisher = {{IEEE} Computer Society}, editor = {Marly Roncken and Andrey Mokhov}, acronym = {{ASYNC}'19}, booktitle = {{P}roceedings of the 25th {IEEE} {I}nternational {S}ymposium on {A}synchronous {C}ircuits and {S}ystems ({ASYNC}'19)}, author = {J{\"u}rgen Maier and Matthias F{\"u}gger and Thomas Nowak and Ulrich Schmid}, title = {Transistor-Level Analysis of Dynamic Delay Models}, pages = {76-85}, year = {2019}, doi = {10.1109/ASYNC.2019.00019}, abstract = {Delay estimation is a crucial task in digital circuit design as it provides the possibility to assure the desired functionality, but also prevents undesired behavior very early. For this purpose elaborate delay models like the Degradation Delay Model (DDM) and the Involution Delay Model (IDM) have been proposed in the past, which facilitate accurate dynamic timing analysis: Both use delay functions that determine the delay of the current input transition based on the time difference T to the previous output one. Currently, however, extensive analog simulations are necessary to determine the (parameters of the) delay function, which is a very time-consuming and cumbersome task and thus limits the applicability of these models. In this paper, we therefore thoroughly investigate the characterization procedures of a CMOS inverter on the transistor level in order to derive analytical expressions for the delay functions. Based on reasonably simple transistor models we identify three operation regions, each described by a different estimation function. Using simulations with two independent technologies, we show that our predictions are not only accurate but also reasonably robust w.r.t. variations. Our results furthermore indicate that the exponential fitting proposed for DDM is actually only partially valid, while our analytic approach can be applied on the whole range. Even the more complex IDM is predicted reasonably accurate.} }

@inproceedings{BBR-fossacs19, address = {Prague, Czech Republic}, month = apr, year = 2019, volume = {11425}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Boja{\'n}czyk, Mikolaj and Simpson, Alex}, acronym = {{FoSSaCS}'19}, booktitle = {{P}roceedings of the 22nd {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'19)}, author = {Benedikt Bollig and Patricia Bouyer and Fabian Reiter}, title = {Identifiers in Registers - Describing Network Algorithms with Logic}, pages = {115-132}, url = {https://arxiv.org/abs/1811.08197}, pdf = {https://arxiv.org/pdf/1811.08197.pdf}, doi = {10.1007/978-3-030-17127-8}, abstract = {We propose a formal model of distributed computing based on register automata that captures a broad class of synchronous network algorithms. The local memory of each process is represented by a finite-state controller and a fixed number of registers, each of which can store the unique identifier of some process in the network. To underline the naturalness of our model, we show that it has the same expressive power as a certain extension of first-order logic on graphs whose nodes are equipped with a total order. Said extension lets us define new functions on the set of nodes by means of a so-called partial fixpoint operator. In spirit, our result bears close resemblance to a classical theorem of descriptive complexity theory that characterizes the complexity class PSPACE in terms of partial fixpoint logic (a proper superclass of the logic we consider here).} }

@inproceedings{JS-lics19, address = {Vancouver, Canada}, month = jun, publisher = {{IEEE} Press}, editor = {Bouyer, Patricia}, acronym = {{LICS}'19}, booktitle = {{P}roceedings of the 34th {A}nnual {ACM\slash IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'19)}, author = {Jan{\v c}ar, Petr and Schmitz, Sylvain}, title = {Bisimulation Equivalence of First-Order Grammars is {ACKERMANN}-Complete}, pages = {1-12}, year = 2019, doi = {10.1109/LICS.2019.8785848}, url = {https://arxiv.org/abs/1901.07170}, abstract = {Checking whether two pushdown automata with restricted silent actions are weakly bisimilar was shown decidable by S{\'e}nizergues (1998, 2005). We provide the first known complexity upper bound for this famous problem, in the equivalent setting of first-order grammars. This ACKERMANN upper bound is optimal, and we also show that strong bisimilarity is primitive-recursive when the number of states of the automata is fixed.} }

*This file was generated by
bibtex2html 1.98.*