@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.",
}}
@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},
pages = {409-424},
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\)).}
}
@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}},
pages = {555-576},
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.}
}
@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{BHL-icomp19,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Nathalie Bertrand and Serge Haddad and Engel Lefaucheux},
title = {{A Tale of Two Diagnoses in Probabilistic Systems}},
volume = {269},
year = {2019},
month = dec,
doi = {10.1016/j.ic.2019.104441},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHL-icomp18.pdf},
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: exact diagnosability requires that almost surely a fault is detected and that no fault is erroneously claimed; approximate diagnosability tolerates a small error probability when claiming a fault; last, accurate approximate diagnosability guarantees that the error probability can be chosen arbitrarily small. In this article, we first refine the specification of diagnosability by identifying three criteria: (1) detecting faulty runs or providing information
for all runs (2) considering finite or infinite runs, and (3) requiring or not a uniform detection delay. We then give a complete picture of relations between the different diagnosability specifications for probabilistic systems and establish characterisations for most of them in the finite-state case. Based on these characterisations, we develop decision procedures, study their complexity and prove their optimality. We also design synthesis algorithms to construct diagnosers
and we analyse their memory requirements. Finally we establish undecidability of the diagnosability problems for which we provided no characterisation.}
}
@article{JGL-mscs18,
publisher = {Cambridge University Press},
journal = {Mathematical Structures in Computer Science},
author = {Goubault{-}Larrecq, Jean},
title = {A semantics for nabla},
volume = {29},
pages = {1250--1274},
year = {2019},
doi = {10.1017/S0960129518000063},
url = {https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/article/semantics-for-nabla/A3337AB54DC58CBDDEC78116F4390777}
}
@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{Genestier-hor19,
address = {Dortmund, Germany},
month = jun,
novolume = {??},
noseries = {??},
noeditor = {},
acronym = {{HOR}'19},
booktitle = {{P}roceedings of the 10th {I}nternational {W}orkshop on {H}igher-{O}rder {R}ewriting
({HOR}'19)},
author = {Genestier, Guillaume},
title = {{S}ize{C}hange{T}ool: {A} {T}ermination {C}hecker for {R}ewriting {D}ependent {T}ypes},
pages = {14--19},
year = 2019,
pdf = {https://hal.archives-ouvertes.fr/hal-02442465/file/presentationSCT.pdf}
}
@inproceedings{EBB-pxtp19,
address = {Natal, Brazil},
month = aug,
volume = {301},
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Giselle Reis and Haniel Barbosa},
acronym = {{PxTP}'19},
booktitle = {{P}roceedings of the 6th {W}orkshop on {P}roof e{X}change for {T}heorem {P}roving
({PxTP}'19)},
author = {El Haddad, Mohamed and Burel, Guillaume and Blanqui, Fr{\'e}d{\'e}ric},
title = {{E}kstrakto: {A} tool to reconstruct {D}edukti proofs from {TSTP} files (extended abstract)},
pages = {27--35},
year = 2019,
pdf = {https://hal.inria.fr/hal-02200548/file/main.pdf},
url = {http://eptcs.web.cse.unsw.edu.au/paper.cgi?PxTP2019.5}
}
@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
}
@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},
pages = {41:1-41:15},
year = 2019,
doi = {10.4230/LIPIcs.FSTTCS.2019.41},
pdf = {https://drops.dagstuhl.de/opus/volltexte/2019/11603/pdf/LIPIcs-FSTTCS-2019-41.pdf},
url = {https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11603},
abstract = {We introduce the well structured problem as the question of whether a model (here a counter machine) is well structured (here for the usual ordering on integers). We show that it is undecidable for most of the (Presburger-defined) counter machines except for Affine VASS of dimension one. However, the strong well structured problem is decidable for all Presburger counter machines. While Affine VASS of dimension one are not, in general, well structured, we give an algorithm that computes the set of predecessors of a configuration; as a consequence this allows to decide the well structured problem for 1-Affine VASS.}
}
@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},
pages = {31:1-31:15},
year = 2019,
doi = {10.4230/LIPIcs.FSTTCS.2019.31},
pdf = {https://drops.dagstuhl.de/opus/volltexte/2019/11593/pdf/LIPIcs-FSTTCS-2019-31.pdf},
url = {https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11593},
abstract = {Traditional concurrent games on graphs involve a fixed number of players, who take decisions simultaneously, determining the next state of the game. In this paper, we introduce a parameterized variant of concurrent games on graphs, where the parameter is precisely the number of players. Parameterized concurrent games are described by finite graphs, in which the transitions bear regular languages to describe the possible move combinations that lead from one vertex to another. We consider the problem of determining whether the first player, say Eve, has a strategy to ensure a reachability objective against any strategy profile of her opponents as a coalition. In particular Eve's strategy should be independent of the number of opponents she actually has. Technically, this paper focuses on an a priori simpler setting where the languages labeling transitions only constrain the number of opponents (but not their precise action choices). These constraints are described as semilinear sets, finite unions of intervals, or intervals. We establish the precise complexities of the parameterized reachability game problem, ranging from PTIME-complete to PSPACE-complete, in a variety of situations depending on the contraints (semilinear predicates, unions of intervals, or intervals) and on the presence or not of non-determinism.}
}
@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},
volume = {29},
number = {8},
pages = {1139--1184},
year = 2019,
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DF-jlc19.pdf}
}
@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},
note = {Invited talk},
year = 2019,
pdf = {https://arxiv.org/abs/1908.01137},
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.}
}
@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
32nd {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},
volume = {263},
pages = {372--391},
year = 2019,
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},
pdf = {https://arxiv.org/pdf/1904.08590.pdf},
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}
}
@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},
volume = {16},
number = {5},
pages = {1610--1619},
year = 2019,
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
32nd {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.}
}
@article{DDR-biosys19,
publisher = {Elsevier Science Publishers},
journal = {Biosystems},
author = {D{\'{\i}}az{-}Caro, Alejandro and Dowek, Gilles and Rinaldi, Juan Pablo},
title = {Two linearities for quantum computing in the lambda calculus},
volume = {186},
doi = {10.1016/j.biosystems.2019.104012},
year = {2019},
url = {10.1016/j.biosystems.2019.104012}
}
@mastersthesis{m2-Doueneau,
author = {Ga{\"e}tan Dou{\'e}neau-Tabot},
title = {{Register Models for Pebble Transducers and Applications to Optimization}},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2019},
month = sep
}
@mastersthesis{m2-Grienenberger,
author = {Emilie Grienenberger},
title = {{Concept alignment in Logipedia - Alignement of logical connectives between HOL Light and Dedukti}},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2019},
month = sep
}
@mastersthesis{m2-Lopez,
author = {Aliaume Lopez},
title = {Th{\'e}or{\`e}mes de pr{\'e}servation},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2019},
month = sep
}
@mastersthesis{m2-Suresh,
author = {Amrita Suresh},
title = {{Termination, boundedness and reachability for input-bounded FIFO Machines}},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2019},
month = sep
}
@phdthesis{jaziri-phd2019,
author = {Samy Jaziri},
title = {{Automata on Timed Structures}},
school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France},
type = {Th{\`e}se de doctorat},
year = 2019,
month = sep,
url = {https://tel.archives-ouvertes.fr/tel-02384274},
pdf = {https://tel.archives-ouvertes.fr/tel-02384274/document}
}
@phdthesis{bury-phd2019,
author = {Guillaume Bury},
title = {{Integrating rewriting, tableau and superposition into SMT}},
school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France},
type = {Th{\`e}se de doctorat},
year = 2019,
month = may,
url = {https://tel.archives-ouvertes.fr/tel-02612985},
pdf = {https://tel.archives-ouvertes.fr/tel-02612985/document}
}
@phdthesis{mandon-phd2019,
author = {Hugues Mandon},
title = {{Algorithms for Cell Reprogramming Strategies in Boolean Networks}},
school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France},
type = {Th{\`e}se de doctorat},
year = 2019,
month = dec,
url = {https://tel.archives-ouvertes.fr/tel-02412717},
pdf = {https://hal.archives-ouvertes.fr/tel-02412717/document}
}
@phdthesis{lick-phd2019,
author = {Anthony Lick},
title = {{XPath-like Query Logics: Proof Systems and Real-World Applicability}},
school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France},
type = {Th{\`e}se de doctorat},
year = 2019,
month = jul,
url = {https://tel.archives-ouvertes.fr/tel-02276423},
pdf = {https://tel.archives-ouvertes.fr/tel-02276423/document}
}
@phdthesis{saoud-phd2019,
author = {Adnane Saoud},
title = {{Compositional and Efficient Controller Synthesis for Cyber-Physical Systems}},
school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France},
type = {Th{\`e}se de doctorat},
year = 2019,
month = oct,
url = {https://tel.archives-ouvertes.fr/tel-02317723},
pdf = {https://tel.archives-ouvertes.fr/tel-02317723/document}
}
@phdthesis{koutsos-phd2019,
author = {Adrien Koutsos},
title = {Preuves symboliques de propri{\'e}t{\'e}s d'indistinguabilit{\'e} calculatoire},
school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France},
type = {Th{\`e}se de doctorat},
year = 2019,
month = sep,
url = {https://tel.archives-ouvertes.fr/tel-02317745},
pdf = {https://tel.archives-ouvertes.fr/tel-02317745/document}
}
@phdthesis{gonzalez-phd2019,
author = {Gonz{\'a}lez, Mauricio},
title = {{Stochastic Games on Graphs with Applications to Smart-Grids Optimization}},
school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France},
type = {Th{\`e}se de doctorat},
year = 2019,
month = nov,
url = {http://www.theses.fr/2019SACLN064},
pdf = {http://www.lsv.fr/~gonzalez/phd/Thesis_Gonzalez_V2_2.pdf}
}
@inproceedings{ZSGF-ecc19,
address = {Naples, Italy},
month = jun,
publisher = {{IEEE} Press},
acronym = {{ECC}'19},
booktitle = {{P}roceedings of the 18th {E}uropean {C}ontrol {C}onference ({ECC}'19)},
author = {Daniele Zonetti and Adnane Saoud and Antoine Girard and Laurent Fribourg},
title = {A symbolic approach to voltage stability and power sharing in time-varying{DC} microgrids},
pages = {903-909},
year = {2019},
doi = {10.23919/ECC.2019.8796095},
url = {https://doi.org/10.23919/ECC.2019.8796095}
}
@inproceedings{CF-cyphy19,
address = {New York City, NY, USA},
month = oct,
editor = {Roger D. Chamberlain and Martin Grimheden and Walid Taha},
volume = {11971},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
noeditor = {},
acronym = {{CyPhy/WESE}'19},
booktitle = {9th International Workshop on Cyber Physical Systems ({CyPhy}'19) and 15th International Workshop on Model-Based Design ({WESE}'19), Revised Selected Papers},
author = {Adrien {Le Co{\"{e}}nt} and Laurent Fribourg},
title = {Guaranteed Optimal Reachability Control of Reaction-Diffusion Equations Using One-Sided Lipschitz Constants and Model Reduction},
pages = {181-202},
year = {2019},
doi = {10.1007/978-3-030-41131-2_9},
url = {https://doi.org/10.1007/978-3-030-41131-2_9}
}
@inproceedings{DFKN-dsd19,
address = {Kallithea, Greece},
month = aug,
publisher = {{IEEE} Press},
noeditor = {},
acronym = {{DSD}'19},
booktitle = {{P}roceedings of the 22nd {E}uromicro {C}onference on {D}igital {S}ystem {D}esign ({DSD}'19)},
author = {Jean{-}Luc Danger and Laurent Fribourg and Ulrich K{\"u}hne and Maha Naceur},
title = {LAOCO{\"O}N: {A} Run-Time Monitoring and Verification Approach for Hardware Trojan Detection},
pages = {269-276},
year = {2019},
doi = {10.1109/DSD.2019.00047},
url = {https://doi.org/10.1109/DSD.2019.00047}
}
@inproceedings{CF-cdc19,
address = {Nice, France},
month = dec,
publisher = {{IEEE} Control System Society},
noeditor = {},
acronym = {{CDC}'19},
booktitle = {{P}roceedings of the 58th {IEEE} {C}onference on
{D}ecision and {C}ontrol ({CDC}'19)},
author = {Adrien {Le Co{\"e}nt} and Laurent Fribourg},
title = {Guaranteed Control of Sampled Switched Systems using Semi-Lagrangian Schemes and One-Sided Lipschitz Constants},
pages = {599-604},
year = {2019},
doi = {10.1109/CDC40024.2019.9029376},
pdf = {https://arxiv.org/pdf/1903.05882.pdf},
url = {https://doi.org/10.1109/CDC40024.2019.9029376}
}
@inproceedings{ACFJL-acsd19,
address = {Aachen, Germany},
month = jun,
publisher = {{IEEE} Computer Society Press},
editor = {J{\"o}rg Keller and Wojciech Penczek},
acronym = {{ACSD}'19},
booktitle = {{P}roceedings of the 19th {I}nternational
{C}onference on {A}pplication of {C}oncurrency
to {S}ystem {D}esign
({ACSD}'19)},
author = {{\'E}tienne Andr{\'e} and Emmanuel Coquard and Laurent Fribourg and Jawher Jerray and David Lesens},
title = {Parametric Schedulability Analysis of a Launcher Flight Control System Under Reactivity Constraints},
pages = {13-22},
year = {2019},
doi = {10.1109/ACSD.2019.00006},
url = {https://doi.org/10.1109/ACSD.2019.00006}
}
@proceedings{CG-fsttcs2019,
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)},
title = {{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 = {Arkadev Chattopadhyay and Paul Gastin},
year = {2019},
url = {http://www.dagstuhl.de/dagpub/978-3-95977-131-3}
}
@inproceedings{BCC-bpm19,
address = {Vienna, Austria},
month = sep,
volume = 362,
series = {Lecture Notes in Business Information Processing},
publisher = {Springer},
editor = {Chiara Di Francescomarino and Remco M. Dijkman and Uwe Zdun},
acronym = {{BPM}'19},
booktitle = {{B}usiness {P}rocess {M}anagement {W}orkshops ({BPM}'19), Revised Selected Papers},
author = {Mathilde Boltenhagen and Thomas Chatain and Josep Carmona},
title = {Encoding Conformance Checking Artefacts in {SAT}},
pages = {160-171},
year = {2019},
doi = {10.1007/978-3-030-37453-2_14},
pdf = {https://hal.inria.fr/hal-02419980/document},
url = {https://doi.org/10.1007/978-3-030-37453-2_14}
}
@article{ACCD-tpnomc19,
publisher = {Springer},
journal = {Transactions on Petri Nets and Other Models of Concurrency},
author = {Wil M. P. van der Aalst and
Josep Carmona and
Thomas Chatain and
Boudewijn F. van Dongen},
title = {A Tour in Process Mining: From Practice to Algorithmic Challenges},
pages = {1-35},
year = {2019},
volume = {14},
doi = {10.1007/978-3-662-60651-3_1},
url = {https://doi.org/10.1007/978-3-662-60651-3_1}
}
@proceedings{DH-pn2019,
author = {Susanna Donatelli and Stefan Haar},
editor = {Susanna Donatelli and Stefan Haar},
title = {Proceedings of the 40th International Conference on Application and Theory of Petri Nets and Concurrency ({PETRI NETS}'19)},
booktitle = {Proceedings of the 40th International Conference on Application and Theory of Petri Nets and Concurrency ({Petri Nets}'19)},
month = jun,
series = {Lecture Notes in Computer Science},
volume = {11522},
publisher = {Springer},
year = {2019},
address = {Aachen, Germany},
url = {https://doi.org/10.1007/978-3-030-21571-2},
doi = {10.1007/978-3-030-21571-2}
}
@inproceedings{OMFS-patmos19,
address = {Rhodes, Greece},
month = jul,
publisher = {{IEEE} Press},
acronym = {{PATMOS}'19},
booktitle = {{P}roceedings of the 29th {I}nternational {S}ymposium on {P}ower and {T}iming {M}odeling, {O}ptimization
and {S}imulation ({PATMOS}'19)},
author = {Daniel {\"O}hlinger and J{\"u}rgen Maier and Matthias F{\"u}gger and Ulrich Schmid},
title = {The Involution Tool for Accurate Digital Timingand Power Analysis},
pages = {1-8},
year = {2019},
doi = {10.1109/PATMOS.2019.8862165},
url = {https://doi.org/10.1109/PATMOS.2019.8862165}
}
@article{FNNS-tcad19,
publisher = {{IEEE} Circuits and Systems Society},
journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits
and Systems},
author = {Matthias F{\"u}gger and Robert Najvirt and Thomas Nowak and Ulrich Schmid},
title = {A faithful binary circuit model},
doi = {10.1109/TCAD.2019.2937748},
year = {2019},
url = {https://ieeexplore.ieee.org/document/8818370}
}
@inproceedings{B-atva19,
address = {Taipei, Taiwan},
month = oct,
volume = {11781},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Yu{-}Fang Chen and Chih{-}Hong Cheng and Javier Esparza},
acronym = {{ATVA}'19},
booktitle = {{P}roceedings of the 17th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'19)},
author = {Patricia Bouyer},
title = {{A Note on Game Theory and Verification (Invited Talk)}},
pages = {3-22},
doi = {10.1007/978-3-030-31784-3_1},
year = 2019
}
@inproceedings{B-time19,
address = {M{\'{a}}laga, Spain},
month = oct,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Johann Gamper and Sophie Pinchinat and Guido Sciavicco},
acronym = {{TIME}'19},
booktitle = {{P}roceedings of the 26th {I}nternational {S}ymposium on
{T}emporal {R}epresentation and {R}easoning
({TIME}'19)},
author = {Patricia Bouyer},
title = {{On the Computation of Nash Equilibria in Games on Graphs (Invited Talk)}},
pages = {3:1-3:3},
doi = {10.4230/LIPIcs.TIME.2019.3},
year = 2019
}
@article{LPSS-lmcs2020,
journal = {Logical Methods in Computer Science},
author = {J{\'e}r{\^o}me Leroux and M. Praveen and Gr{\'e}goire Sutre and Schnoebelen, {\relax Ph}ilippe},
title = {On Functions Weakly Computable by Pushdown {Petri} Nets and Related Systems},
volume = {15},
number = {4},
year = 2019,
doi = {10.23638/LMCS-15(4:15)2019},
pdf = {https://arxiv.org/pdf/1904.04090.pdf}
}
@inproceedings{FHK-msr2019,
address = {Angers, France},
month = nov,
futureseries = {Journal Europ{\'e}en des Syst{\`e}mes Automatis{\'e}s},
publisher = {HAL},
editor = {Beno{\^i}t Delahaye and S{\'e}bastien Lahaye and Mehdi Lhommeau},
acronym = {{MSR}'19},
booktitle = {{A}ctes du 12{\`e}me {C}olloque sur la
{M}od{\'e}lisation des {S}yst{\`e}mes
{R}{\'e}actifs
({MSR}'19)},
author = {Alain Finkel and Serge Haddad and Igor Khmelnitsky},
title = {{R{\'e}ification des acc{\'e}l{\'e}rations pour la construction de Karp et Miller}},
year = 2019,
pdf = {https://hal.archives-ouvertes.fr/hal-02431913/file/MSR19_paper_17.pdf},
url = {https://hal.archives-ouvertes.fr/hal-02431913}
}
This file was generated by bibtex2html 1.98.