@article{BKM-cc14,
publisher = {Birkh{\"a}user},
journal = {Computational Complexity},
author = {Blondin, Michael and Krebs, Andreas and McKenzie, Pierre},
title = {The Complexity of Intersecting Finite Automata Having Few
Final States},
volume = {25},
number = {4},
pages = {775-814},
month = dec,
year = 2016,
note = {To appear},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BKM-cc14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BKM-cc14.pdf},
doi = {10.1007/s00037-014-0089-9},
abstract = {The problem of determining whether several finite automata
accept a word in common is closely related to the well-studied membership
problem in transformation monoids. We raise the issue of limiting the
number of final states in the automata intersection problem. For automata
with two final states, we show the problem to be \(\oplus{L}\)-complete
or NP-complete according to whether a nontrivial monoid other than a
direct product of cyclic groups of order~2 is allowed in the automata. We
further consider idempotent commutative automata and (Abelian, mainly)
group automata with one, two, or three final states over a singleton or
larger alphabet, elucidating (under the usual hypotheses on complexity
classes) the complexity of the intersection nonemptiness and related
problems in each case.}
}
@article{PHL-sttt14,
publisher = {Springer},
journal = {International Journal on Software Tools
for Technology Transfer},
author = {Ponce{ }de{~}Le{\'o}n, Hern{\'a}n and Haar, Stefan and
Longuet, Delphine},
title = {Model-based Testing for Concurrent Systems: Unfolding-based Test Selection},
volume = {18},
number = 3,
year = {2016},
month = jun,
pages = {305-318},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-sttt14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-sttt14.pdf},
doi = {10.1007/s10009-014-0353-y},
abstract = {Model-based testing has mainly focused on models where
concurrency is interpreted as interleaving (like the ioco theory for
labeled transition systems), which may be too coarse when one wants
concurrency to be preserved in the implementation. In order to test such
concurrent systems, we choose to use Petri nets as specifications and
define a concurrent conformance relation named co-ioco. We present a test
generation algorithm based on Petri net unfolding able to build a complete
test suite w.r.t our co-ioco conformance relation. In addition we propose
several coverage criteria that allow to select finite prefixes of an
unfolding in order to build manageable test suites.}
}
@article{haar-mvlsc15,
publisher = {Old City Publishing},
journal = {Journal of Multiple-Valued Logic and Soft Computing},
author = {Haar, Stefan},
title = {Cyclic Ordering through Partial Orders},
volume = {27},
number = {2-3},
year = 2016,
month = sep,
pages = {209-228},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/haar-mvlsc16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/haar-mvlsc16.pdf},
abstract = {The orientation problem for ternary cyclic order relations has
been attacked in the literature from combinatorial perspectives, through
rotations, and by connection with Petri nets. We propose here a two-fold
characterization of orientable cyclic orders in terms of symmetries of
partial orders as well as in terms of separating sets (cuts). The results
are inspired by properties of non-sequential discrete processeses, but
also apply to dense structures of any cardinality.}
}
@article{KNS-tcs2015,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Karandikar, Prateek and Niewerth, Matthias and Schnoebelen,
{\relax Ph}ilippe},
title = {On the state complexity of closures and interiors of regular
languages with subwords and superwords},
volume = {610},
number = {A},
pages = { 91-107},
year = {2016},
month = jan,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/KNS-tcs15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KNS-tcs15.pdf},
doi = {10.1016/j.tcs.2015.09.028},
abstract = {The downward and upward closures of a regular language~\(L\) are
obtained by collecting all the subwords and superwords of its elements,
respectively. The downward and upward interiors of~\(L\) are obtained dually
by collecting words having all their subwords and superwords in~\(L\),
respectively.\par
We provide lower and upper bounds on the size of the smallest automata
recognizing these closures and interiors. We also consider the
computational complexity of decision problems for closures of regular
languages.}
}
@article{BHJL-fi15,
publisher = {{IOS} Press},
journal = {Fundamenta Informaticae},
author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge and Jovanovi{\'c},
Aleksandra and Lime, Didier},
title = {Interrupt Timed Automata with Auxiliary Clocks and Parameters},
volume = {143},
number = {3-4},
pages = {235-259},
month = mar,
year = 2016,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHJL-fi15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHJL-fi15.pdf},
doi = {10.3233/FI-2016-1313},
abstract = {Interrupt Timed Automata (ITA) are an expressive timed model,
introduced to take into account interruptions according to levels. Due to
this feature, this formalism is incomparable with Timed Automata.\par
However several decidability results related to reachability and model
checking have been obtained. We add auxiliary clocks to ITA, thereby
extending its expressive power while preserving decidability of
reachability. Moreover, we define a parametrized version of ITA, with
polynomials of parameters appearing in guards and updates. While
parametric reasoning is particularly relevant for timed models, it very
often leads to undecidability results. We prove that various reachability
problems, including robust reachability, are decidable for this model, and
we give complexity upper bounds for a fixed or variable number of clocks,
levels and parameters.}
}
@article{BGM-ipl15,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Bouyer, Patricia and Gardy, Patrick and Markey, Nicolas},
title = {On~the semantics of Strategy Logic},
volume = {116},
number = {2},
pages = {75-79},
month = feb,
year = {2016},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-ipl15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-ipl15.pdf},
doi = {10.1016/j.ipl.2015.10.004},
abstract = {We define and study a slight variation on the semantics of
Strategy Logic: while in the classical semantics, all strategies are
shifted during the evaluation of temporal modalities, we propose to only
shift the strategies that have been assigned to a player, thus matching
the intuition that we can assign the very same strategy to the players at
different points in time. We prove that surprisingly, this renders the
model-checking problem undecidable.}
}
@article{HK-ipl15,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Haase, Christoph and Kiefer, Stefan},
title = {The Complexity of the \(K\)th Largest Subset Problem and Related Problems},
volume = {116},
number = {2},
pages = {111-115},
month = feb,
year = {2016},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HK-ipl15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HK-ipl15.pdf},
doi = {10.1016/j.ipl.2015.09.015},
abstract = {We show that the \textsc{\(K\)th largest subset} problem and the
\textsc{\(K\)th largest \(m\)-tuple} problem are in PP and hard for PP
under polynomial-time Turing reductions. Several problems from the
literature were previously shown NP-hard via reductions from those two
problems, and by our main result they become PP-hard as well. We also
provide complementary PP-upper bounds for some of them.}
}
@article{DD-jlc15,
publisher = {Oxford University Press},
journal = {Journal of Logic and Computation},
author = {Demri, St{\'e}phane and Deters, Morgan},
title = {Temporal Logics on Strings with Prefix Relation},
year = 2016,
volume = {26},
number = {3},
pages = {989-1017},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-jlc15-v2.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-jlc15-v2.pdf},
doi = {10.1093/logcom/exv028},
abstract = {We show that linear-time temporal logic over concrete domains
made of finite strings and the prefix relation admits a PSpace-complete
satisfiability problem. Actually, we extend a known result with the
concrete domain made of the set of natural numbers and the greater than
relation (corresponding to the singleton alphabet case) and we solve an
open problem mentioned in several publications. Since the prefix relation
is not a total ordering, it~is not possible to take advantage of existing
techniques dedicated to temporal logics with concrete domains that are
essentially linearly ordered structures. Instead, we introduce an adequate
encoding of string constraints into length constraints that allows us to
reduce the problem on strings to the problem on natural numbers. To~do~so,
we~also propose an extended version of the logic on strings that is able
to compare lengths of longest common prefixes and for which the
satisfiability problem is shown in PSpace. Finally, we show how to lift
the result for the branching-time case in order to get decidability when
the underlying temporal logic is~CTL\textsuperscript*.}
}
@article{Schmitz-jsl15,
publisher = {Association for Symbolic Logic},
journal = {Journal of Symbolic Logic},
author = {Schmitz, Sylvain},
title = {Implicational Relevance Logic is \(2\)-{ExpTime}-Complete},
volume = {81},
number = {2},
pages = {641-661},
month = jun,
year = 2016,
url = {http://arxiv.org/abs/1402.0705},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Schmitz-jsl15.pdf},
doi = {10.1017/jsl.2015.7},
abstract = {We show that provability in the implicational fragment of
relevance logic is complete for doubly exponential time, using reductions
to and from coverability in branching vector addition systems.}
}
@misc{qcover16,
author = {Blondin, Michael and Finkel, Alain and Haase, Christoph and Haddad, Serge},
title = {{QCover: an efficient coverability verifier for discrete and continuous Petri nets}},
url = {https://github.com/blondimi/qcover},
year = {2016}
}
@phdthesis{theissing-PhD16,
author = {Theissing, Simon},
title = {Supervision in Multi-Modal Transportation System},
school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France},
type = {Th{\`e}se de doctorat},
year = {2016},
month = dec,
url = {https://tel.archives-ouvertes.fr/tel-01419126},
pdf = {https://hal.inria.fr/tel-01419126v3/document}
}
@article{BCEZ-dmtcs2016,
journal = {Discrete Mathematics \& Theoretical Computer Science},
author = {Brough, Tara and Ciobanu, Laura and Elder, Murray and Zetzsche, Georg},
title = {{Permutations of context-free, ET0L and indexed languages}},
volume = {17},
number = {3},
year = {2016},
month = may,
pages = {167-178},
url = {https://dmtcs.episciences.org/2164},
pdf = {https://arxiv.org/pdf/1604.05431.pdf}
}
@inproceedings{DLV-pods16,
acronym = {{PODS}'16},
publisher = {ACM Press},
month = jun,
booktitle = {{P}roceedings of the 35th {ACM} {SIGMOD-SIGACT-SIGAI} {S}ymposium on {P}rinciples of {D}atabase {S}ystems ({PODS}'16)},
title = {{P}roceedings of the 35th {ACM} {SIGMOD-SIGACT-SIGAI} {S}ymposium on {P}rinciples of {D}atabase {S}ystems ({PODS}'16)},
address = {San Francisco, California, USA},
abstract = {Data-driven workflows, of which IBM's Business
Artifacts are a prime exponent, have been
successfully deployed in practice, adopted in
industrial standards, and have spawned a rich body
of research in academia, focused primarily on static
analysis. The present work represents a significant
advance on the problem of artifact verification, by
considering a much richer and more realistic model
than in previous work, incorporating core elements
of IBM's successful Guard-Stage-Milestone model. In
particular, the model features task hierarchy,
concurrency, and richer artifact data. It also
allows database key and foreign key dependencies, as
well as arithmetic constraints. The results show
decidability of verification and establish its
complexity, making use of novel techniques including
a hierarchy of Vector Addition Systems and a variant
of quantifier elimination tailored to our context.},
author = {Deutsch, Alin and Li, Yuliang and Vianu, Victor},
pages = {179-194},
doi = {10.1145/2902251.2902275},
year = {2016}
}
@phdthesis{mvdb-phd2016,
author = {Van{ }den{ }Bogaard, Marie},
title = {Motifs de Flot d'Information dans les Jeux {\`a} Information Imparfaite},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2016,
month = nov,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/mvdb-phd16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/mvdb-phd16.pdf}
}
@mastersthesis{m2-jacomme,
author = {Jacomme, Charlie},
title = {Automated applications of Cryptographic Assumptions},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2016},
month = sep,
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-jacomme.pdf}
}
@mastersthesis{m2-lehaut,
author = {Lehaut, Mathieu},
title = {PDL on infinite alphabet},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2016},
month = aug,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-lehaut.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-lehaut.pdf},
note = {19~pages}
}
@article{DH-jlamp16,
publisher = {Elsevier Science Publishers},
journal = {Journal of Logic and Algebraic Methods in Programming},
author = {Delaune, St{\'e}phanie and Hirschi, Lucca},
title = {A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols},
volume = {87},
year = {2016},
pages = {127-144},
url = {http://www.sciencedirect.com/science/article/pii/S235222081630133X},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DH-jlamp16.pdf},
doi = {10.1016/j.jlamp.2016.10.005},
note = {To~appear},
abstract = {Cryptographic protocols aim at securing communications over insecure networks such as the Internet, where dishonest users may listen to communications and interfere with them. A secure communication has a different meaning depending on the underlying application. It ranges from the confidentiality of a data to e.g. verifiability in electronic voting systems. Another example of a security notion is privacy. Formal symbolic models have proved their usefulness for analysing the security of protocols. Until quite recently, most results focused on trace properties like confidentiality or authentication. There are however several security properties, which cannot be defined (or cannot be naturally defined) as trace properties and require a notion of behavioural equivalence. Typical examples are anonymity, and privacy related properties. During the last decade, several results and verification tools have been developed to analyse equivalence-based security properties. We propose here a synthesis of decidability and undecidability results for equivalence-based security properties. Moreover, we give an overview of existing verification tools that may be used to verify equivalence-based security properties.}
}
@techreport{BGMS-arxiv16,
author = {Beame, Paul and
Grosshans, Nathan and
McKenzie, Pierre and
Segoufin, Luc},
title = {Nondeterminism and an abstract formulation of {N}eciporuk's lower
bound method},
institution = {Computing Research Repository},
number = {1608.01932},
year = {2016},
url = {http://arxiv.org/abs/1608.01932},
pdf = {http://arxiv.org/abs/1608.01932},
month = aug,
type = {Research Report},
note = {34~pages}
}
@inproceedings{MPAS-cikm16,
address = {Indianapolis, Indiana, USA},
month = oct,
publisher = {ACM},
acronym = {{CIKM}'16},
booktitle = {{P}roceedings of the 25th {ACM} {I}nternational {C}onference on {I}nformation and {K}nowledge {M}anagement ({CIKM}'16)},
author = {Montoya, David and
Pellissier Tanon, Thomas and
Abiteboul, Serge and
Suchanek, Fabian},
title = {{T}hymeflow, {A} {P}ersonal {K}nowledge {B}ase with {S}patio-temporal {D}ata},
pages = {2477-2480},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/MPAS-cikm16.pdf},
year = {2016},
doi = {10.1145/2983323.2983337},
abstract = {The typical Internet user has data spread over several devices
and across several online systems. We demonstrate an
open-source system for integrating user's data from di erent
sources into a single Knowledge Base. Our system integrates
data of di erent kinds into a coherent whole, starting with
email messages, calendar, contacts, and location history. It
is able to detect event periods in the user's location data and
align them with calendar events. We will demonstrate how
to query the system within and across di erent dimensions,
and perform analytics over emails, events, and locations.}
}
@mastersthesis{m2-lick,
author = {Lick, Anthony},
title = {Syst{\`e}mes de preuves pour logiques modales},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2016},
month = aug,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-lick.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-lick.pdf},
note = {20~pages}
}
@phdthesis{blondin-phd2016,
author = {Blondin, Michael},
title = {Algorithmique et complexit{\'e} des syst{\`e}mes {\`a}
compteurs},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France and Universit{\'e} de Montr{\'e}al},
type = {Th{\`e}se de doctorat},
year = {2016},
month = jun,
url = {https://tel.archives-ouvertes.fr/tel-01359000/}
}
@phdthesis{mohamed-PhD16,
author = {Mohamed, Sameh},
title = {Une m{\'e}thode topologique pour la recherche d'ensembles invariants de syst{\`e}mes
continus et {\`a} commutation},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = {2016},
month = oct,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/mohamed-phd16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/mohamed-phd16.pdf}
}
@phdthesis{C-phd2016,
author = {Cauderlier, Rapha{\"e}l},
title = {{Object-Oriented Mechanisms for Interoperability between Proof Systems}},
school = {{Conservatoire National Des Arts et M{\'e}tiers, Paris}},
type = {Th{\`e}se de doctorat},
year = 2016,
month = oct,
url = {https://hal.inria.fr/tel-01415945/},
pdf = {https://hal.inria.fr/tel-01415945/file/main.pdf}
}
@book{DGL-cup2016,
author = {Demri, St{\'e}phane and Goranko, Valentin and Lange, Martin},
title = {{T}emporal {L}ogics in {C}omputer {S}cience},
publisher = {Cambridge University Press},
series = {Cambridge Tracts in Theoretical Computer Science},
volume = {58},
year = {2016},
month = oct,
url = {http://www.cambridge.org/9781107028364},
isbn = {9781107028364}
}
@inproceedings{HHKLL-syncop16,
address = {Eindhoven, The Netherlands},
month = apr,
year = 2016,
volume = 220,
series = {Electronic Proceedings in Theoretical Computer Science},
acronym = {{C}assting/{SYNCOP}'16},
booktitle = {{P}roceedings of the {C}assting {W}orkshop on {G}ames for the {S}ynthesis of {C}omplex
{S}ystems and 3rd {I}nternational {W}orkshop on {S}ynthesis of {C}omplex {P}arameters
({C}assting/{SYNCOP}'16)},
author = {Hutagalung, Milka and
Hundeshagen, Norbert and
Kuske, Dietrich and
Lange, Martin and
Lozes, {\'{E}}tienne},
title = {Two-Buffer Simulation Games},
pages = {213-227},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HHKLL-syncop16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HHKLL-syncop16.pdf},
doi = {10.4204/EPTCS.220.3},
abstract = {We consider simulation games played between Spoiler and Duplicator on two B{\"u}chi
automata in which the choices made by Spoiler can be buffered by Duplicator in two different buffers
before she executes them on her structure. Previous work on such games using a single buffer has
shown that they are useful to approximate language inclusion problems. We study the decidability and
complex- ity and show that games with two buffers can be used to approximate corresponding problems on
finite transducers, i.e. the inclusion problem for rational relations over infinite words.}
}
@inproceedings{HHKLL-gandalf16,
address = {Catania, Italy},
month = sep,
year = 2016,
volume = {226},
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Cantone, Domenico and Delzanno, Giorgio},
acronym = {{GandALF}'16},
booktitle = {{P}roceedings of the 7th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification
({GandALF}'16)},
author = {Hutagalung, Milka and
Hundeshagen, Norbert and
Kuske, Dietrich and
Lange, Martin and
Lozes, {\'{E}}tienne},
title = {Multi-Buffer Simulations for Trace Language Inclusion},
pages = {213-227},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HHKLL-gandalf16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HHKLL-gandalf16.pdf},
doi = {10.4204/EPTCS.226.15},
abstract = {We consider simulation games played between Spoiler and Duplicator on two B{\"u}chi automata in
which the choices made by Spoiler can be buffered by Duplicator in several bu ers before she executes
them on her structure. We show that the simulation games are useful to approximate the
inclusion of trace closures of languages accepted by finite-state automata, which is known to be undecidable.
We study the decidability and complexity and show that the game with bounded buffers
can be decided in polynomial time, whereas the game with one unbounded and one bounded buffer is
highly undecidable. We also show some sufficient conditions on the automata for Duplicator to win
the game (with unbounded buffers).}
}
@inproceedings{Halmagrand-ictac16,
address = {Taipei, Taiwan},
month = oct,
volume = 9965,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Alves Sampaio, Cesar and Wang, Farn},
acronym = {{ICTAC}'16},
booktitle = {{P}roceedings of the 13th {I}nternational {C}olloquium on
{T}heoretical {A}spects of {C}omputing ({ICTAC}'16)},
author = {Halmagrand, Pierre},
title = {{{Soundly Proving B Method Formulae Using Typed Sequent Calculus}}},
pages = {196-213},
year = {2016},
doi = {10.1007/978-3-319-46750-4_12},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Halmagrand-ictac2016.pdf},
url = {https://hal.archives-ouvertes.fr/hal-01342849},
abstract = {The B Method is a formal method mainly used in the railway industry to specify and develop safety-critical software.
To guarantee the consistency of a B project, one decisive challenge is to show correct a large amount of proof obligations, which are mathematical formulae
expressed in a classical set theory extended with a specific type system. To improve automated theorem proving in the B Method, we propose to use a
first-order sequent calculus extended with a polymorphic type system, which is in particular the output proof-format of the tableau-based automated
theorem prover Zenon. After stating some modifications of the B syntax and defining a sound elimination of comprehension sets, we propose a
translation of B formulae into a polymorphic first-order logic format. Then, we introduce the typed sequent calculus used by Zenon, and show
that Zenon proofs can be translated to proofs of the initial B formulae in the B proof system.}
}
@techreport{PS-arxiv16,
author = {Place, Thomas and
Segoufin, Luc},
title = {Decidable Characterization of FO2(<, +1) and locality of
{DA}},
institution = {Computing Research Repository},
number = {1606.03217},
year = {2016},
url = {http://arxiv.org/abs/1606.03217},
pdf = {http://arxiv.org/abs/1606.03217},
month = jun,
type = {Research Report},
note = {8~pages}
}
@article{JSD-lmcs16,
journal = {Logical Methods in Computer Science},
author = {Jacquemard, Florent and
Segoufin, Luc and
Dimino, Jer{\'{e}}mie},
title = {FO2(<, +1,{\textasciitilde}) on data trees, data tree automata
and branching vector addition systems},
volume = {12},
number = {2},
pages = {1-28},
year = {2016},
url = {http://www.lmcs-online.org/ojs/viewarticle.php?id=1789&layout=abstract},
doi = {10.2168/LMCS-12(2:3)2016},
pdf = {https://arxiv.org/pdf/1601.01579.pdf},
abstract = {}
}
@techreport{arxiv16-BFMK,
author = {Blondin, Michael and Finkel, Alain and McKenzie, Pierre},
title = {Well Behaved Transition Systems},
institution = {Computing Research Repository},
number = {1608.02636},
year = {2016},
month = aug,
type = {Research Report},
url = {http://arxiv.org/abs/1608.02636},
pdf = {http://arxiv.org/abs/1608.02636},
note = {18~pages},
abstract = {The well-quasi-ordering (i.e., a well-founded quasi-ordering such that all antichains are finite) that defines well-structured transition systems (WSTS) is shown not to be the weakest hypothesis that implies decidability of the coverability problem. We show coverability decidable for monotone transition systems that only require the absence of infinite antichains and call well behaved transitions systems (WBTS) the new strict superclass of the class of WSTS that arises. By contrast, we confirm that boundedness and termination are undecidable for WBTS under the usual hypotheses, and show that stronger monotonicity conditions can enforce decidability. Proofs are similar or even identical to existing proofs but the surprising message is that a hypothesis implicitely assumed minimal for twenty years in the theory of WSTS can meaningfully be relaxed, allowing more orderings to be handled in an abstract way.}
}
@inproceedings{vDCC-EMISA16,
address = {Vienna, Austria},
month = oct,
publisher = {{CEUR-WS.org}},
volume = {1701},
series = {{CEUR} Workshop Proceedings},
editor = {Rinderle-Ma, Stefanie and Mendling, Jan},
acronym = {{EMISA}'16},
booktitle = {{P}roceedings of the 7th {I}nt. {W}orkshop on {E}nterprise {M}odelling and {I}nformation {S}ystems {A}rchitectures
({EMISA}'16)},
author = {van Dongen, Boudewijn and Carmona, Josep and Chatain, {\relax Th}omas},
title = {{Alignment-based Quality Metrics in Conformance Checking}},
pages = {87-90},
year = {2016},
doi = {},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/vanDongen-EMISA16.pdf},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/vanDongen-EMISA16.pdf},
abstract = {The holy grail in process mining is a process discovery algorithm that, given an event
log, produces fitting, precise, properly generalizing and simple process models. Within the field of
process mining, conformance checking is considered to be anything where observed behaviour, e.g.,
in the form of event logs or event streams, needs to be related to already modelled behaviour.
In the conformance checking domain, the relation between an event log and a model is typically
quantified using fitness, precision and generalization. In this paper, we present metrics for fitness,
precision and generalization, based on alignments and the newer concept named anti-alignments.}
}
@article{GLSSW-dagrep16,
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
journal = {Dagstuhl Reports},
author = {Goubault{-}Larrecq, Jean and Seisenberger, Monika and Selivanov, Victor and Weiermann, Andreas},
title = {Well {Q}uasi-{O}rders in {C}omputer {S}cience ({D}agstuhl {S}eminar
16031)},
year = 2016,
month = jan,
volume = {6},
number = {1},
pages = {69-98},
url = {http://dx.doi.org/10.4230/DagRep.6.1.69},
pdf = {http://dx.doi.org/10.4230/DagRep.6.1.69},
doi = {10.4230/DagRep.6.1.69},
abstract = {This report documents the program and the outcomes of Dagstuhl Seminar 16031 {"}Well Quasi{-}Orders in Computer
Science{"}, the first seminar devoted to the multiple and deep interactions between the theory of Well quasi{-}orders
(known as the Wqo{-}Theory) and several fields of Computer Science (Verification and Termination of Infinite-State Systems,
Automata and Formal Languages, Term Rewriting and Proof Theory, topological complexity of computational problems on continuous
functions). Wqo{-}Theory is a highly developed part of Combinatorics with ever-growing number of applications in Mathematics and
Computer Science, and Well quasi-orders are going to become an important unifying concept of Theoretical Computer Science.
In this seminar, we brought together several communities from Computer Science and Mathematics in order to facilitate the
knowledge transfer between Mathematicians and Computer Scientists as well as between established and younger researchers and thus
to push forward the interaction between Wqo{-}Theory and Computer Science.}
}
@inproceedings{MHP-HSB16,
address = {Grenoble France},
month = oct,
optvolume = 9957,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
opteditor = {Cinquemani, Eugenio and
Donz{\'{e}, Alexandre}},
acronym = {{HSB}'16},
booktitle = {{P}roceedings of the 5th
{I}nternational {W}orkshop on
{H}ybrid {S}ystems {B}iology},
author = {Mandon, Hugues and Haar, Stefan and Paulev{\'e}, Lo{\"i}c},
title = {{Relationship between the Reprogramming Determinants of Boolean Networks and their Interaction Graph}},
pages = {113-127},
year = {2016},
doi = {10.1007/978-3-319-47151-8_8},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/MHP-HSB16.pdf},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/MHP-HSB16.pdf},
abstract = {In this paper, we address the formal characterization of tar- gets triggering cellular trans-differentiation in the scope of Boolean net- works with asynchronous dynamics. Given two fixed points of a Boolean network, we are interested in all the combinations of mutations which allow to switch from one fixed point to the other, either possibly, or in- evitably. In the case of existential reachability, we prove that the set of nodes to (permanently) flip are only and necessarily in certain connected components of the interaction graph. In the case of inevitable reachabil- ity, we provide an algorithm to identify a subset of possible solutions.}
}
@inproceedings{GLL-rv16,
address = {Madrid, Spain},
volume = 10012,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Madrid, Spain},
acronym = {{RV}'16},
booktitle = {{P}roceedings of the 16th {C}onference on {R}untime {V}erification ({RV}'16)},
author = {Goubault{-}Larrecq, Jean and Lachance, Jean{-}Philippe},
title = {On the {C}omplexity of {M}onitoring {O}rchids {S}ignatures},
year = 2016,
month = sep,
pages = {169-164},
opturl = {http://link.springer.com/chapter/10.1007%2F978-3-319-46982-9_11},
optpdf = {http://link.springer.com/chapter/10.1007%2F978-3-319-46982-9_11},
doi = {10.1007/978-3-319-46982-9_11},
abstract = {Modern monitoring tools such as our intrusion detection tool Orchids work by firing new monitor instances dynamically. Given an Orchids signature (a.k.a. a rule, a specification), what is the complexity of checking that specification, that signature? In other words, let f(n) be the maximum number of monitor instances that can be fired on a sequence of n events: we design an algorithm that decides whether f(n) is asymptotically exponential or polynomial, and in the latter case returns an exponent d such that f(n)=Theta(n^d) . Ultimately, the problem reduces to the following mathematical question, which may have other uses in other domains: given a system of recurrence equations described using the operators + and max, and defining integer sequences u_n, what is the asymptotic behavior of u_n as n tends to infinity? We show that, under simple assumptions, u_n is either exponential or polynomial, and that this can be decided, and the exponent computed, using a simple modification of Tarjan’s strongly connected components algorithm, in linear time.}
}
@inproceedings{KSHP-sasb16,
address = {Edinburgh, UK},
month = sep,
missingnumber = {2},
missingvolume = {},
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
acronym = {{SASB}'16},
booktitle = {{P}roceedings of {T}he {S}eventh {I}nternational {W}orkshop on {S}tatic {A}nalysis and {S}ystems {B}iology (SASB 2016)},
title = {{Unfolding of Parametric Logical Regulatory Networks}},
author = {Kolc{\'a}k, Juraj and {\v S}afr{\'a}nek, David and Haar, Stefan and Paulev{\'e}, Lo{\"i}c},
year = {2016},
note = {To appear},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KSHP-SASB16.pdf},
url = {https://hal.archives-ouvertes.fr/hal-01354109},
abstract = {In systems biology, models of cellular regulatory processes such as gene regulatory networks or signalling pathways are crucial to understanding the behaviour of living cells. Available biological data are however often insufficient for full model specification. In this paper, we focus on partially specified models where the missing information is abstracted in the form of parameters. We introduce a novel approach to analysis of parametric logical regulatory networks addressing both sources of combinatoric explosion native to the model. First, we introduce a new compact representation of admissible parameters using Boolean lattices. Then, we define the unfolding of parametric regulatory networks. The resulting structure provides a partial- order reduction of concurrent transitions, and factorises the common transitions among the concrete models. A comparison is performed against state-of-the-art approaches to parametric model analysis.}
}
@article{KGHPAJRHH-tpnomc2016,
publisher = {Springer},
journal = {Transactions on Petri Nets and Other Models of Concurrency},
author = {Kordon, Fabrice and
Garavel, Hubert and
Hillah, Lom{-}Messan and
Paviot{-}Adet, Emmanuel and
Jezequel, Lo{\"{\i}}g and
Rodr{\'{\i}}guez, C{\'{e}}sar and
Hulin{-}Hubard, Francis },
title = {{MCC}'2015 - {T}he {F}ifth {M}odel {C}hecking {C}ontest},
volume = {11},
pages = {262-273},
year = {2016},
url = {http://dx.doi.org/10.1007/978-3-662-53401-4_12},
doi = {10.1007/978-3-662-53401-4_12},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KGHPAJRHH-tpnomc2016.pdf}
}
@article{ADFLP-fi2016,
publisher = {{IOS} Press},
journal = {Fundamenta Informaticae},
author = {Abdulla, Parosh Aziz and Demri, St{\'e}phane and Finkel, Alain and Leroux, J{\'e}r{\^o}me and Potapov, Igor},
editor = {Abdulla, Parosh Aziz and Demri, St{\'e}phane and Finkel, Alain and Leroux, J{\'e}r{\^o}me and Potapov, Igor},
number = {3--4},
title = {Selected papers of Reachability Problems Workshop 2012 (Bordeaux) and 2013 (Uppsala)},
url = {http://content.iospress.com/journals/fundamenta-informaticae/143/3-4},
volume = {143},
year = {2016}
}
@proceedings{BDM-aiml16,
title = {{P}roceedings of the 11th {C}onference on {A}dvances in {M}odal {L}ogic ({AiML}'16)},
booktitle = {{P}roceedings of the 11th {C}onference on {A}dvances in {M}odal {L}ogic ({AiML}'16)},
acronym = {{AiML}'16},
editor = {Beklemishev, Lev and Demri, St{\'e}phane and Mat{\'e}, Andr{\'a}s},
publisher = {College Publications},
year = 2016,
month = sep,
address = {Budapest, Hungary},
url = {http://www.collegepublications.co.uk/aiml/?00008}
}
@inproceedings{Bollig-fsttcs16,
address = {Chennai, India},
month = dec,
year = 2016,
volume = {65},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {S. Akshay and Akash Lal and Saket Saurabh and Sandeep Sen},
acronym = {{FSTTCS}'16},
booktitle = {{P}roceedings of the 36th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'16)},
author = {Bollig, Benedikt},
title = {One-Counter Automata with Counter Observability},
pages = {20:1-20:14},
url = {http://drops.dagstuhl.de/opus/volltexte/2016/6855/},
doi = {10.4230/LIPIcs.FSTTCS.2016.20},
abstract = {In a one-counter automaton (OCA), one can produce a letter from some finite alphabet, increment and decrement the counter by one, or compare it with constants up to some threshold. It is well-known that universality and language inclusion for OCAs are undecidable. In this paper, we consider OCAs with counter observability: Whenever the automaton produces a letter, it outputs the current counter value along with it. Hence, its language is now a set of words over an infinite alphabet. We show that universality and inclusion for that model are PSPACE-complete, thus no harder than the corresponding problems for finite automata. In fact, by establishing a link with visibly one-counter automata, we show that OCAs with counter observability are effectively determinizable and closed under all boolean operations. Moreover, it turns out that they are expressively equivalent to strong automata, in which transitions are guarded by MSO formulas over the natural numbers with successor.}
}
@proceedings{FM-formats16,
title = {{P}roceedings of the 14th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'16)},
booktitle = {{P}roceedings of the 14th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'16)},
acronym = {{FORMATS}'16},
editor = {Fr{\"a}nzle, Martin and Markey, Nicolas},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {9884},
doi = {10.1007/978-3-319-44878-7},
url = {http://link.springer.com/book/10.1007/978-3-319-44878-7},
year = 2016,
month = aug,
address = {Qu\'ebec City, Canada}
}
@proceedings{BDJMS-casstingsyncop16,
title = {{P}roceedings of the {C}assting Workshop on
{G}ames for the {S}ynthesis of {C}omplex {S}ystems ({C}assting'16)
and of the 3rd {I}nternational {W}orkshop on
{S}ynthesis of {C}omplex {P}arameters ({S}yn{C}o{P}'16)},
booktitle = {{P}roceedings of the {C}assting Workshop on
{G}ames for the {S}ynthesis of {C}omplex {S}ystems ({C}assting'16)
and of the 3rd {I}nternational {W}orkshop on
{S}ynthesis of {C}omplex {P}arameters ({S}yn{C}o{P}'16)},
acronym = {{C}assting{{\slash}}{S}yn{C}o{P}'16},
editor = {Brihaye, {\relax Th}omas and Delahaye, Beno{\^\i}t and Jezequel,
Lo{\"\i}g and Markey, Nicolas and Srba, Ji{\v{r}}{\'i}},
doi = {10.4204/EPTCS.220},
url = {http://eptcs.web.cse.unsw.edu.au/content.cgi?CASSTINGSynCoP2016},
series = {Electronic Proceedings in Theoretical Computer Science},
volume = 220,
year = 2016,
month = jul,
address = {Eindhoven, The~Netherlands}
}
@inproceedings{BMS-gandalf16,
address = {Catania, Italy},
month = sep,
year = 2016,
volume = {226},
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Cantone, Domenico and Delzanno, Giorgio},
acronym = {{GandALF}'16},
booktitle = {{P}roceedings of the 7th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification
({GandALF}'16)},
author = {Bouyer, Patricia and Markey, Nicolas and Stan, Daniel},
title = {Stochastic Equilibria under Imprecise Deviations in
Terminal-Reward Concurrent Games},
pages = {61-75},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-gandalf16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-gandalf16.pdf},
doi = {10.4204/EPTCS.226.5},
abstract = {We study the existence of mixed-strategy equilibria in
concurrent games played on graphs. While existence is guaranteed
with safety objectives for each player, Nash equilibria need not
exist when players are given arbitrary terminal-reward objectives,
and their existence is undecidable with qualitative reachability
objectives (and~only three players). However, these results rely on
the fact that the players can enforce infinite plays while trying to
improve their payoffs. In this paper, we introduce a relaxed notion
of equilibria, where deviations are imprecise. We prove that
contrary to Nash equilibria, such (stationary) equilibria always
exist, and we develop a PSPACE algorithm to compute one.}
}
@inproceedings{Finkel-rp16,
address = {Aalborg, Denmark},
month = sep,
year = 2016,
volume = {9899},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Larsen, Kim G. and Srba, Ji{\v{r}}{\'\i}},
acronym = {{RP}'16},
booktitle = {{P}roceedings of the 10th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'16)},
author = {Finkel, Alain},
title = {The Ideal Theory for {WSTS}},
pages = {1-22},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/Finkel-rp16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Finkel-rp16.pdf},
doi = {10.1007/978-3-319-45994-3_1},
abstract = {We begin with a survey on well structured transition systems and, in particular, we present the ideal framework [FG09a, BFM14] which was recently used to obtain new deep results on Petri nets and extensions. We argue that the theory of ideals prompts a renewal of the theory of WSTS by providing a way to define a new class of monotonic systems, the so-called Well Behaved Transition Systems, which properly contains WSTS, and for which coverability is still decidable by a forward algorithm. We then recall the completion of WSTS which leads to defining a conceptual Karp-Miller procedure that terminates in more cases than the generalized Karp-Miller procedure on extensions of Petri nets.}
}
@inproceedings{ABDL-rp16,
address = {Aalborg, Denmark},
month = sep,
year = 2016,
volume = {9899},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Larsen, Kim G. and Srba, Ji{\v{r}}{\'\i}},
acronym = {{RP}'16},
booktitle = {{P}roceedings of the 10th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'16)},
author = {Alechina, Natasha and Bulling, Nils and Demri,
St{\'e}phane and Logan, Brian},
title = {On the Complexity of Resource-Bounded Logics},
pages = {36-50},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABDL-rp16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABDL-rp16.pdf},
doi = {10.1007/978-3-319-45994-3_3},
abstract = {We revisit decidability results for resource-bounded
logics and use decision problems on VASS to establish complexity
characterisation of (decidable) model-checking problems. We show
that the model-checking problem for the logic RB\(\pm\)ATL is
2EXPTIME-complete by using recent results on alternating VASS.
Moreover, we establish that the model-checking problem for RBTL is
EXPSPACE-complete and that the problem is decidable and of the same
complexity for RBTL\textsuperscript{*}, proving a new decidability
result as a by-product of the approach. We establish that the
model-checking problem for RB\(\pm\)ATL\textsuperscript{*}, the
extension of RB\(\pm\)ATL with arbitrary path formulae is decidable
by a reduction into parity games. We are also able to synthesise
values for resource parameters. Hence, the paper establishes formal
correspondences between model-checking problems and decision
problems on alternating VASS, paving the way to more applications.}
}
@inproceedings{LFS-rp16,
address = {Aalborg, Denmark},
month = sep,
year = 2016,
volume = {9899},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Larsen, Kim G. and Srba, Ji{\v{r}}{\'\i}},
acronym = {{RP}'16},
booktitle = {{P}roceedings of the 10th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'16)},
author = {Le{~}Co{\"e}nt, Adrien and Fribourg, Laurent and
Soulat, Romain},
title = {Compositional analysis of Boolean networks using local fixed-point
iterations},
pages = {134-147},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LFS-rp16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LFS-rp16.pdf},
doi = {10.1007/978-3-319-45994-3_10},
abstract = {We present a compositional method which allows to
over-approximate the set of attractors and under-approximate the set
of basins of attraction of a Boolean network~(BN). This merely
consists in replacing a global fixed-point computation by a
composition of local fixed-point computations. Once these
approximations have been computed, it~becomes much more tractable to
generate the exact sets of attractors and basins of attraction. We
illustrate the interest of our approach on several examples, among
which is a BN modeling a railway interlocking system with 50 nodes
and millions of attractors.}
}
@inproceedings{LFMDC-rp16,
address = {Aalborg, Denmark},
month = sep,
year = 2016,
volume = {9899},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Larsen, Kim G. and Srba, Ji{\v{r}}{\'\i}},
acronym = {{RP}'16},
booktitle = {{P}roceedings of the 10th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'16)},
author = {Le{~}Co{\"e}nt, Adrien and Fribourg, Laurent and
Markey, Nicolas and De{~}Vuyst, Florian and Chamoin, Ludovic},
title = {Distributed Synthesis of State-Dependent Switching Control},
pages = {119-133},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LFMDC-rp16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LFMDC-rp16.pdf},
doi = {10.1007/978-3-319-45994-3_9},
abstract = {We present a correct-by-design method of state-dependent
control synthesis for linear discrete-time switching systems. Given
an objective region~\(R\) of the state space, the method builds a
capture set~\(S\) and a control which steers any element of~\(S\)
into~\(R\). The method works by iterated backward reachability
from~\(R\). More precisely, \(S\)~is given as a parametric extension
of~\(R\), and the maximum value of the parameter is solved by linear
programming. The method can also be used to synthesize a stability
control which maintains indefinitely within~\(R\) all the states
starting at~\(R\). We~explain how the synthesis method can be
performed in a distributed manner. The method has been implemented
and successfully applied to the synthesis of a distributed control
of a concrete floor heating system with 11 rooms and \(2^11 = 2048\)
switching modes.}
}
@inproceedings{HT-pasm16,
address = {M{\"u}nster, Germany},
month = apr,
year = 2016,
volume = {327},
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Haverkort, Boudewijn and Knottenbelt, William and Remke, Anne and Thomas, Nigel},
booktitle = {{P}roceedings of the 8th {I}nternational {W}orkshop on {P}ractical
{A}pplications of {S}tochastic {M}odelling ({PASM}'16)},
author = {Haar, Stefan and Theissing, Simon},
title = {Forecasting Passenger Loads in Transportation Networks},
pages = {49-69},
url = {https://hal.inria.fr/hal-01259585},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HT-pasm16.pdf},
doi = {10.1016/j.entcs.2016.09.023},
abstract = {This work is part of an ongoing effort to understand the
dynamics of passenger loads in modern, multimodal transportation
networks (TNs) and to mitigate the impact of perturbations. The
challenge is that the percentage of passengers at any given point of
the TN that have a certain destination, i.e. their distribution over
different trip profiles, is unknown. We introduce a stochastic
hybrid automaton model for multimodal TNs that allows to compute how
such probabilistic load vectors are propagated through the TN, and
develop a computation strategy for forecasting the network's load a
certain time into the future.}
}
@misc{vip-D42,
author = {Delaune, St{\'e}phanie and Gazeau, Ivan},
howpublished = {Deliverable VIP~4.2 (ANR-11-JS02-0006)},
month = jun,
note = {5~pages},
type = {Contract Report},
title = {Combination issues},
year = {2016},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/vip-d42.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/vip-d42.pdf}
}
@misc{vip-D22,
author = {Delaune, St{\'e}phanie and Gazeau, Ivan},
howpublished = {Deliverable VIP~2.2 (ANR-11-JS02-0006)},
month = jun,
note = {8~pages},
type = {Contract Report},
title = {Results on the case studies},
year = {2016},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/vip-d22.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/vip-d22.pdf}
}
@techreport{HT-hal16,
author = {Haar, Stefan and Theissing, Simon},
title = {A~Passenger-centric Multi-agent System Model for
Multimodal Public Transportation},
institution = {HAL-inria},
number = {hal-01322956},
month = may,
year = {2016},
type = {Research Report},
url = {https://hal.inria.fr/hal-01322956},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HT-hal16.pdf},
note = {12~pages},
abstract = {If we want to understand how perturbations spread across a
multi-modal public transportation system, we have to include
passenger flows into the model and the analysis. Indeed, in general
no two different lines in such a system are physically connected
directly, or share tracks or other resources. Rather, they are
connected by passengers changing lines and thus transmit
perturbations from one line or mode to another. We present a formal
passenger-centric multi-agent system model that can capture
(i)~individual and possibly multi-modal trip profiles with branches
resulting from different decision outcomes, (ii)~the~movement of
fixed-route operated transportation means, and (iii)~in-vehicle and
in-station capacity constraints. The model is based on a
nets-within-nets approach with Petri nets as the basic building
entities. Thus, it has a convenient graphical representation, and
the possibility of execution.}
}
@inproceedings{HT-qest16,
address = {Qu{\'e}bec City, Canada},
month = aug,
year = 2016,
volume = {9826},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Agha, Gul and Van{~}Houdt, Benny},
acronym = {{QEST}'16},
booktitle = {{P}roceedings of the 13th {I}nternational
{C}onference on {Q}uantitative
{E}valuation of {S}ystems
({QEST}'16)},
author = {Haar, Stefan and Theissing, Simon},
title = {Decoupling Passenger Flows for Improved Load Prediction},
pages = {364-379},
url = {https://hal.inria.fr/hal-01330136},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HT-qest16.pdf},
doi = {10.1007/978-3-319-43425-4_24},
abstract = {This paper continues our work on perturbation analysis of
multimodal transportation networks~(TNs) by means of a stochastic
hybrid automaton~(SHA) model. We focus here on the approximate
computation , in particular on the major bottleneck consisting in
the high dimensionality of systems of stochastic differential
balance equations (SDEs) that define the continuous passenger-flow
dynamics in the different modes of the SHA model. In fact, for every
pair of a mode and a station, one system of coupled SDEs relates the
passenger loads of all discrete points such as platforms considered
in this station, and all vehicles docked to it, to the passenger
flows in between. In general, such an SDE system has many
dimensions, which makes its numerical computation and thus the
approximate computation of the SHA model intractable. We show how
these systems can be canonically replaced by lower-dimensional ones,
by decoupling the passenger flows inside every mode from one
another. We prove that the resulting approximating passenger-flow
dynamics converges to the original one, if the replacing set of
balance equations set up for all decoupled passenger flows
communicate their results among each other in vanishing time
intervals.}
}
@inproceedings{HT-acc16,
address = {Boston, Massachusetts, USA},
month = jul,
year = 2016,
publisher = {{IEEE} Control System Society},
acronym = {{ACC}'16},
booktitle = {{P}roceedings of the 35th {A}merican {C}ontrol
{C}onference ({ACC}'16)},
author = {Haar, Stefan and Theissing, Simon},
title = {Predicting Traffic Load in Public Transportation Networks},
pages = {821-826},
url = {https://hal.inria.fr/hal-01329632},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HT-acc16.pdf},
doi = {10.1109/ACC.2016.7525015},
abstract = {This work is part of an ongoing effort to understand the
dynamics of passenger loads in modern, multimodal transportation
networks (TNs) and to mitigate the impact of perturbations, under
the restrictions that the precise number of passengers in some point
of the TN that intend to reach a certain destination (i.e. their
distribution over different trip profiles) is unknown. We introduce
an approach based on a stochastic hybrid automaton model for a TN
that allows to compute how such probabilistic load vectors are
propagated through the TN, and develop a computation strategy for
forecasting the network's load a certain time in the future.}
}
@inproceedings{FHLM-wodes16,
address = {Xi'an, China},
month = may # {-} # jun,
year = 2016,
publisher = {{IEEE} Control System Society},
editor = {Cassandras, Christos G. and Giua, Alessandro},
acronym = {{WODES}'16},
booktitle = {{P}roceedings of the 13th {W}orkshop on {D}iscrete {E}vent {S}ystems
({WODES}'16)},
author = {Fabre, {\'E}ric and H{\'e}lou{\"e}t, Lo{\"i}c and
Lefaucheux, Engel and Marchand, Herv{\'e}},
title = {Diagnosability of Repairable Faults},
pages = {230-236},
url = {https://hal.inria.fr/hal-01302562},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FHLM-wodes16.pdf},
doi = {10.1109/WODES.2016.7497853},
abstract = {The diagnosis problem for discrete event systems consists
in deciding whether some fault event occurred or not in the system,
given partial observations on the run of that system. Diagnosability
checks whether a correct diagnosis can be issued in bounded time
after a fault, for all faulty runs of that system. This problem
appeared two decades ago and numerous facets of it have been
explored, mostly for permanent faults. It is known for example that
diagnosability of a system can be checked in polynomial time, while
the construction of a diagnoser is exponential. The present paper
examines the case of transient faults, that can appear and be
repaired. Diagnosability in this setting means that the occurrence
of a fault should always be detected in bounded time, but also
before the fault is repaired. Checking this notion of diagnosability
is proved to be PSPACE-complete. It is also shown that faults can be
reliably counted provided the system is diagnosable for faults and
for repairs.}
}
@inproceedings{vDCC-bpm16,
address = {Rio de Janeiro, Brazil},
month = sep,
year = 2016,
volume = {9850},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {La{~}Rosa, Marcello and Loos, Peter and Pastor, Oscar},
acronym = {{BPM}'16},
booktitle = {{P}roceedings of the 14th {I}nternational {C}onference on
{B}usiness {P}rocess {M}anagement ({BPM}'16)},
author = {van Dongen, Boudewijn F. and Carmona, Josep and Chatain,
{\relax Th}omas},
title = {A Unified Approach for Measuring Precision and
Generalization Based on Anti-Alignments},
pages = {39-56},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/vDCC-bpm16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/vDCC-bpm16.pdf},
doi = {10.1007/978-3-319-45348-4_3},
abstract = {The holy grail in process mining is an algorithm that, given an
event log, produces fitting, precise, properly generalizing and simple
process models. While there is consensus on the existence of solid metrics
for fitness and simplicity, current metrics for precision and
generalization have important flaws, which hamper their applicability in a
general setting. In this paper, a novel approach to measure precision and
generalization is presented, which relies on the notion of
anti-alignments. An anti-alignment describes highly deviating model traces
with respect to observed behavior. We propose metrics for precision and
generalization that resemble the leave-one-out cross-validation
techniques, where individual traces of the log are removed and the
computed anti-alignment assess the model's capability to describe
precisely or generalize the observed behavior.}
}
@inproceedings{KS-csl16,
address = {Marseille, France},
month = sep,
year = 2016,
volume = {62},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Regnier, Laurent and Talbot, Jean-Marc},
acronym = {{CSL}'16},
booktitle = {{P}roceedings of the 25th {A}nnual {EACSL} {C}onference on
{C}omputer {S}cience {L}ogic ({CSL}'16)},
author = {Prateek Karandikar and Schnoebelen,
{\relax Ph}ilippe},
title = {The height of piecewise-testable languages with applications in
logical complexity},
pages = {37:1-37:22},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-csl16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-csl16.pdf},
doi = {10.4230/LIPIcs.CSL.2016.37},
abstract = {The height of a piecewise-testable language~\(L\) is the maximum
length of the words needed to define~\(L\) by excluding and requiring given
subwords. The height of~\(L\) is an important descriptive complexity measure
that has not yet been investigated in a systematic way. This paper
develops a series of new techniques for bounding the height of finite
languages and of languages obtained by taking closures by subwords,
superwords and related operations.\par
As an application of these results, we show that
\({\textsf{FO}}^2(A^*,\sqsubseteq)\), the two-variable fragment of the
first-order logic of sequences with the subword ordering, can only express
piecewise-testable properties and has elementary complexity.}
}
@inproceedings{GGL-csl16,
address = {Marseille, France},
month = sep,
year = 2016,
volume = {62},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Regnier, Laurent and Talbot, Jean-Marc},
acronym = {{CSL}'16},
booktitle = {{P}roceedings of the 25th {A}nnual {EACSL} {C}onference on
{C}omputer {S}cience {L}ogic ({CSL}'16)},
author = {Ganardi, Moses and G{\"o}ller, Stefan and Lohrey, Markus},
title = {On the Parallel Complexity of Bisimulation over Finite Systems},
pages = {12:1-12:17},
doi = {10.4230/LIPIcs.CSL.2016.12},
abstract = {In this paper the computational complexity of the (bi)simulation problem over restricted graph classes is studied. For trees given as pointer structures or terms the (bi)simulation problem is complete for logarithmic space or NC\(^1\), respectively. This solves an open problem from Balc{\'a}zar, Gabarr{\'o}, and S{\'a}ntha. We also show that the simulation problem is P-complete even for graphs of bounded path-width.}
}
@inproceedings{DGGL-csl16,
address = {Marseille, France},
month = sep,
year = 2016,
volume = {62},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Regnier, Laurent and Talbot, Jean-Marc},
acronym = {{CSL}'16},
booktitle = {{P}roceedings of the 25th {A}nnual {EACSL} {C}onference on
{C}omputer {S}cience {L}ogic ({CSL}'16)},
author = {Dubut, J{\'e}r{\'e}my and Goubault, {\'E}ric and
Goubault{-}Larrecq, Jean},
title = {The Directed Homotopy Hypothesis},
pages = {9:1-9:16},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DBS-csl16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DBS-csl16.pdf},
doi = {10.4230/LIPIcs.CSL.2016.9},
abstract = {The homotopy hypothesis was originally stated by Grothendieck: topological spaces should be {"}equivalent{"} to (weak) infinite-groupoids, which give algebraic representatives of homotopy types. Much later, several authors developed geometrizations of computational models, e.g., for rewriting, distributed systems, (homotopy) type theory etc. But an essential feature in the work set up in concurrency theory, is that time should be considered irreversible, giving rise to the field of directed algebraic topology. Following the path proposed by Porter, we state here a directed homotopy hypothesis: Grandis' directed topological spaces should be {"}equivalent{"} to a weak form of topologically enriched categories, still very close to (infinite,1)-categories. We develop, as in ordinary algebraic topology, a directed homotopy equivalence and a weak equivalence, and show invariance of a form of directed homology.}
}
@inproceedings{DBS-csl16,
address = {Marseille, France},
month = sep,
year = 2016,
volume = {62},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Regnier, Laurent and Talbot, Jean-Marc},
acronym = {{CSL}'16},
booktitle = {{P}roceedings of the 25th {A}nnual {EACSL} {C}onference on
{C}omputer {S}cience {L}ogic ({CSL}'16)},
author = {Amina Doumane and David Baelde and Alexis Saurin},
title = {Infinitary proof theory: the multiplicative additive case},
pages = {42:1-42:17},
doi = {10.4230/LIPIcs.CSL.2016.42},
abstract = {Infinitary and regular proofs are commonly used in fixed point logics. Being natural intermediate devices between semantics and traditional finitary proof systems, they are commonly found in completeness arguments, automated deduction, verification, etc. However, their proof theory is surprisingly underdeveloped. In particular, very little is known about the computational behavior of such proofs through cut elimination. Taking such aspects into account has unlocked rich developments at the intersection of proof theory and programming language theory. One would hope that extending this to infinitary calculi would lead, e.g., to a better understanding of recursion and corecursion in programming languages. Structural proof theory is notably based on two fundamental properties of a proof system: cut elimination and focalization. The first one is only known to hold for restricted (purely additive) infinitary calculi, thanks to the work of Santocanale and Fortier; the second one has never been studied in infinitary systems. In this paper, we consider the infinitary proof system muMALLi for multiplicative and additive linear logic extended with least and greatest fixed points, and prove these two key results. We thus establish muMALLi as a satisfying computational proof system in itself, rather than just an intermediate device in the study of finitary proof systems.}
}
@inproceedings{BLS-hal15,
address = {Marseille, France},
month = sep,
year = 2016,
volume = {62},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Regnier, Laurent and Talbot, Jean-Marc},
acronym = {{CSL}'16},
booktitle = {{P}roceedings of the 25th {A}nnual {EACSL} {C}onference on
{C}omputer {S}cience {L}ogic ({CSL}'16)},
author = {Baelde, David and Lunel, Simon and Schmitz, Sylvain},
title = {A~Sequent Calculus for a Modal Logic on Finite Data
Trees},
pages = {32:1-32:16},
url = {https://hal.inria.fr/hal-01191172},
doi = {10.4230/LIPIcs.CSL.2016.32},
abstract = {We investigate the proof theory of a modal fragment of XPath
equipped with data (in)equality tests over finite data
trees, i.e. over finite unranked trees where nodes are
labelled with both a symbol from a finite alphabet and a
single data value from an infinite domain. We present a
sound and complete sequent calculus for this logic, which
yields the optimal PSPACE complexity bound for its validity
problem.}
}
@inproceedings{Bouyer-mfcs16,
address = {Krakow, Poland},
month = aug,
year = 2016,
volume = {58},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf},
acronym = {{MFCS}'16},
booktitle = {{P}roceedings of the 41st
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'16)},
author = {Bouyer, Patricia},
title = {Optimal Reachability in Weighted Timed Automata and Games},
pages = {3:1-3:3},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/bouyer-mfcs16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bouyer-mfcs16.pdf},
doi = {10.4230/LIPIcs.MFCS.2016.3},
abstract = {This is an overview of the invited talk delivered at the 41st International Symposium on Math- ematical Foundations of Computer Science (MFCS-2016).}
}
@inproceedings{ABKMT-mfcs16,
address = {Krakow, Poland},
month = aug,
year = 2016,
volume = {58},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf},
acronym = {{MFCS}'16},
booktitle = {{P}roceedings of the 41st
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'16)},
author = {Akshay, S. and Bouyer, Patricia and Krishna, Shankara Narayanan and
Manasa, Lakshmi and Trivedi, Ashutosh },
title = {Stochastic Timed Games Revisited},
pages = {8:1-8:14},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABKMT-mfcs16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABKMT-mfcs16.pdf},
doi = {10.4230/LIPIcs.MFCS.2016.8},
abstract = {Stochastic timed games (STGs), introduced by Bouyer and Forejt,
naturally generalize both continuous-time Markov chains and timed automata
by providing a partition of the locations between those controlled by two
players (Player Box and Player Diamond) with competing objectives and
those governed by stochastic laws. Depending on the number of
players---2,~1, or~0---subclasses of stochastic timed games are often
classified as \(2\frac{1}{2}\)-player, \(1\frac{1}{2}\)-player, and
\(\frac{1}{2}\)-player games where the \(\frac{1}{2}\) symbolizes the
presence of the stochastic {"}nature{"} player. For STGs with reachability
objectives it is known that \(1\frac{1}{2}\)-player one-clock STGs are
decidable for qualitative objectives, and that \(2\frac{1}{2}\)-player
three-clock STGs are undecidable for quantitative reachability objectives.
This paper further refines the gap in this decidability spectrum. We show
that quantitative reachability objectives are already undecidable for
\(1\frac{1}{2}\)-player four-clock STGs, and even under the time-bounded
restriction for \(2\frac{1}{2}\)-player five-clock~STGs. We~also obtain a
class of \(1\frac{1}{2}\), \(2\frac{1}{2}\)-player STGs for which the
quantitative reachability problem is decidable.}
}
@inproceedings{NPR-mfcs16,
address = {Krakow, Poland},
month = aug,
year = 2016,
volume = {58},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf},
acronym = {{MFCS}'16},
booktitle = {{P}roceedings of the 41st
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'16)},
author = {Reino Niskanen and Igor Potapov and Julien Reichert},
title = {Undecidability of Two-dimensional Robot Games},
pages = {73:1-73:13},
url = {http://arxiv.org/abs/1604.08779},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/NPR-mfcs16.pdf},
doi = {10.4230/LIPIcs.MFCS.2016.73},
abstract = {Robot game is a two-player vector addition game played on the integer lattice \(\mathbb{Z}^n\). Both players have sets of vectors and in each turn the vector chosen by a player is added to the current configuration vector of the game. One of the players, called Eve, tries to play the game from the initial configuration to the origin while the other player, Adam, tries to avoid the origin. The problem is to decide whether or not Eve has a winning strategy. In this paper we prove undecidability of the robot game in dimension two answering the question formulated by Doyen and Rabinovich in 2011 and closing the gap between undecidable and decidable cases.}
}
@inproceedings{DGGL-concur16,
address = {Qu{\'e}bec City, Canada},
month = aug,
year = 2016,
volume = {59},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Desharnais, Jos{\'e}e and Jagadeesan, Radha},
acronym = {{CONCUR}'16},
booktitle = {{P}roceedings of the 27th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'16)},
author = {Dubut, J{\'e}r{\'e}my and Goubault, {\'E}ric and Goubault{-}Larrecq, Jean},
title = {Bisimulations and unfolding in {{\(\mathcal{P}\)}}-accessible categorical models},
pages = {25:1-25:14},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DGGL-concur16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DGGL-concur16.pdf},
doi = {10.4230/LIPIcs.CONCUR.2016.25},
abstract = {We propose a categorical framework for bisimulations and
unfoldings that unifies the classical approach from Joyal
\emph{et~al.} via open maps and unfoldings. This is based on a
notion of categories accessible with respect to a subcategory of
path shapes, i.e., for which one can define a nice notion of trees
as glueings of paths. We show that transition systems and presheaf
models are instances of our framework. We also prove that in our
framework, several notions of bisimulation coincide, in particular
an {"}operational~one{"} akin to the standard definition in
transition systems. Also, our notion of accessibility is preserved
by coreflections. This also leads us to a notion of unfolding that
behaves well in the accessible case: it~is a right adjoint and is a
universal covering, i.e., it is initial among the morphisms that
have the unique lifting property with respect to path shapes. As an
application, we prove that the universal covering of a groupoid, a
standard construction in algebraic topology, is an unfolding, when
the category of path shapes is well chosen.}
}
@inproceedings{AGS-concur16,
address = {Qu{\'e}bec City, Canada},
month = aug,
year = 2016,
volume = {59},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Desharnais, Jos{\'e}e and Jagadeesan, Radha},
acronym = {{CONCUR}'16},
booktitle = {{P}roceedings of the 27th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'16)},
author = {Akshay, S. and Paul Gastin and Krishna, Shankara Narayanan},
title = {Analyzing Timed Systems Using Tree Automata},
pages = {27:1-27:14},
url = {http://arxiv.org/abs/1604.08443},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGS-concur16.pdf},
doi = {10.4230/LIPIcs.CONCUR.2016.27},
abstract = {Timed systems, such as timed automata, are usually analyzed
using their operational semantics on timed words. The classical region
abstraction for timed automata reduces them to (untimed) finite state
automata with the same time-abstract properties, such as state
reachability. We propose a new technique to analyze such timed systems
using finite tree automata instead of finite word automata. The main idea
is to consider timed behaviors as graphs with matching edges capturing
timing constraints. Such graphs can be interpreted in trees opening the
way to tree automata based techniques which are more powerful than
analysis based on word automata. The technique is quite general and
applies to many timed systems. In this paper, as an example, we develop
the technique on timed pushdown systems, which have recently received
considerable attention. Further, we also demonstrate how we can use it on
timed automata and timed multi-stack pushdown systems (with boundedness
restrictions).}
}
@inproceedings{BHL-concur16,
address = {Qu{\'e}bec City, Canada},
month = aug,
year = 2016,
volume = {59},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Desharnais, Jos{\'e}e and Jagadeesan, Radha},
acronym = {{CONCUR}'16},
booktitle = {{P}roceedings of the 27th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'16)},
author = {Nathalie Bertrand and Serge Haddad and Engel Lefaucheux},
title = {Diagnosis in Infinite-State Probabilistic Systems},
pages = {37:1-37:15},
url = {https://hal.inria.fr/hal-01334218},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHL-concur16.pdf},
doi = {10.4230/LIPIcs.CONCUR.2016.37},
abstract = {In a recent work, we introduced four variants of
diagnosability (\textsf{FA}, \textsf{IA}, \textsf{FF},~\textsf{IF})
in (finite) probabilistic systems (pLTS) depending whether one
considers (1)~finite or infinite runs and (2)~faulty or all runs. We
studied their relationship and established that the corresponding
decision problems are PSPACE-complete. A~key ingredient of the
decision procedures was a characterisation of diagnosability by the
fact that a random run almost surely lies in an open set whose
specification only depends on the qualitative behaviour of the pLTS.
Here we investigate similar issues for infinite pLTS. We~first show
that this characterisation still holds for
\textsf{FF}-diagnosability but with a~\(G_{\delta}\) set instead of
an open set and also for \textsf{IF}-and \textsf{IA}-diagnosability
when pLTS are finitely branching. We also prove that surprisingly
\textsf{FA}-diagnosability cannot be characterised in this way even
in the finitely branching case. Then we apply our characterisations
for a partially observable probabilistic extension of visibly
pushdown automata (POpVPA), yielding EXPSPACE procedures for solving
diagnosability problems. In~addition, we~establish some
computational lower bounds and show that slight extensions of POpVPA
lead to undecidability.}
}
@inproceedings{DLM-concur16,
address = {Qu{\'e}bec City, Canada},
month = aug,
year = 2016,
volume = {59},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Desharnais, Jos{\'e}e and Jagadeesan, Radha},
acronym = {{CONCUR}'16},
booktitle = {{P}roceedings of the 27th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'16)},
author = {David, Am{\'e}lie and Laroussinie, Fran{\c{c}}ois and
Markey, Nicolas},
title = {On~the expressiveness of~{QCTL}},
pages = {28:1-28:15},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DLM-concur16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DLM-concur16.pdf},
doi = {10.4230/LIPIcs.CONCUR.2016.28},
abstract = {QCTL extends the temporal logic CTL with quantification
over atomic propositions. While the algorithmic questions for QCTL
and its fragments with limited quantification depth are
well-understood (e.g. satisfiability of QCTL\textsuperscript{\(k\)},
with at most \(k\) nested blocks of quantifiers, is
\(k+1\)-EXPTIME-complete), very few results are known about the
expressiveness of this logic. We~address such expressiveness
questions in this paper. We first consider the \emph{distinguishing
power} of these logics (i.e.,~their ability to separate models),
their relationship with behavioural equivalences, and their ability
to capture the behaviours of finite Kripke structures with so-called
characteristic formulas. We then consider their \emph{expressive
power} (i.e.,~their ability to express a property), showing that in
terms of expressiveness the hierarchy QCTL\textsuperscript{\(k\)}
collapses at level~2 (in~other terms, any~QCTL formula can be
expressed using at most two nested blocks of quantifiers).}
}
@inproceedings{GR-langonto16,
address = {Portoro{\v{z}}, Slovenia},
editor = {Grci{\'c} Simeunovi, Larisa and Vintar,
{\u{S}}pela and Khan, Fahad and Le{\'o}n Ara{\'u}z,
Pilar and Faber, Pamela and Fontini, Francesca and
Parvisi, Artemis and Unger, Christina},
acronym = {{LangOnto+TermiKS}'16},
booktitle = {{P}roceedings of the {J}oint 2nd {W}orkshop on {L}anguage and
{O}ntology~\& {T}erminology and {K}nowledge
{S}tructures ({LangOnto+TermiKS}'16)},
author = {Grefenstette, Gregory and Rafes, Karima},
title = {Transforming {W}ikipedia into an Ontology-based
Information Retrieval Search Engine for Local Experts
using a Third-Party Taxonomy},
year = 2016,
month = may,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GR-langonto16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GR-langonto16.pdf},
note = {To appear},
abstract = {Wikipedia is widely used for finding general information
about a wide variety of topics. Its vocation is not to provide
local information. For~example, it~provides plot, cast, and
production information about a given movie, but not showing times in
your local movie theatre. Here we describe how we can connect local
information to Wikipedia, without altering its content. The~case
study we present involves finding local scientific experts. Using a
third-party taxonomy, independent from Wikipedia's category
hierarchy, we index information connected to our local experts,
present in their activity reports, and we re-index Wikipedia content
using the same taxonomy. The connections between Wikipedia pages and
local expert reports are stored in a relational database, accessible
through as public SPARQL endpoint. A~Wikipedia gadget (or plugin)
activated by the interested user, accesses the endpoint as each
Wikipedia page is accessed. An~additional tab on the Wikipedia page
allows the user to open up a list of teams of local experts
associated with the subject matter in the Wikipedia page. The
technique, though presented here as a way to identify local experts,
is generic, in that any third party taxonomy, can be used in this to
connect Wikipedia to any non-Wikipedia data source.}
}
@article{LDRCF-ijdc16,
publisher = {Springer},
journal = {International Journal of Dynamics and Control},
author = {Le{~}Co{\"e}nt, Adrien and De{~}Vuyst, Florian and Rey,
Christian and Chamoin, Ludovic and Fribourg, Laurent},
title = {Control of mechanical systems using set-based methods},
pages = {1-17},
year = 2016,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LDRCF-ijdc16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LDRCF-ijdc16.pdf},
doi = {10.1007/s40435-016-0245-y},
abstract = {This paper considers large discrete-time linear systems obtained
from discretized partial differential equations, and controlled by a
\emph{quantized} law, i.e., a piecewise constant time function taking a
finite set of values. We show how to generate the control by, first,
applying \emph{model reduction} to the original system, then using a
{"}state-space bisection{"} method for synthesizing a control at the
reduced-order level, and finally computing an upper bound on the
deviations between the controlled output trajectories of the reduced-order
model and those of the original model. The effectiveness of our approach
is illustrated on several examples of the literature.}
}
@inproceedings{LACF-snr16,
address = {Vienna, Austria},
month = apr,
year = 2016,
publisher = {{IEEE} Computer Society Press},
acronym = {{SNR}'16},
booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop
on {S}ymbolic and {N}umerical {M}ethods for
{R}eachability {A}nalysis ({SNR}'16)},
author = {Le{~}Co{\"e}nt, Adrien and Alexandre{ }dit{ }Sandretto,
Julien and Chapoutot, Alexandre and Fribourg,
Laurent},
title = {Control of Nonlinear Switched Systems Based on
Validated Simulation},
pages = {1-6},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LACF-snr16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LACF-snr16.pdf},
abstract = {We present an algorithm of control synthesis for nonlinear
switched systems, based on an existing procedure of state-space
bisection and made available for nonlinear systems with the help of
validated simulation. The use of validated simulation also permits
to take bounded perturbations and varying parameters into account.
The whole approach is entirely guaranteed and the induced
controllers are correct-by-design.}
}
@article{DFP-lmcs16,
journal = {Logical Methods in Computer Science},
author = {Demri, St{\'e}phane and Figueira, Diego and Praveen, M},
title = {Reasoning about Data Repetitions with Counter Systems},
year = 2016,
volume = {12},
number = {3},
month = aug,
pages = {1:1-1:55},
url = {http://arxiv.org/abs/1604.02887},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DFP-lmcs16.pdf},
doi = {10.2168/LMCS-12(3:1)2016},
abstract = {We study linear-time temporal logics interpreted over data words
with multiple attributes. We restrict the atomic formulas to equalities
of attribute values in successive positions and to repetitions of
attribute values in the future or past. We demonstrate correspondences
between satisfiability problems for logics and reachability-like decision
problems for counter systems. We show that allowing\slash disallowing
atomic formulas expressing repetitions of values in the past corresponds
to the reachability\slash coverability problem in Petri nets. This gives
us 2EXPSPACE upper bounds for several satisfiability problems. We prove
matching lower bounds by reduction from a reachability problem for a
newly introduced class of counter systems. This new class is a succinct
version of vector addition systems with states in which counters are
accessed via pointers, apotentially useful feature in other contexts. We
strengthen further the correspondences between data logics and counter
systems by characterizing the complexity of fragments, extensions and
variants of the logic. For instance, we precisely characterize the
relationship between the number of attributes allowed in the logic and
the number of counters needed in the counter system.}
}
@inproceedings{BBCM-csr16,
address = {St~Petersburg, Russia},
month = jun,
year = 2016,
volume = {9691},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Gerhard J. Woeginger},
acronym = {{CSR}'16},
booktitle = {{P}roceedings of the 11th {I}nternational {C}omputer {S}cience
{S}ymposium in {R}ussia ({CSR}'16)},
author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and Carlier,
Pierre
and Menet, Quentin},
title = {Compositional Design of Stochastic Timed Automata},
pages = {117-130},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBCM-csr16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBCM-csr16.pdf},
doi = {10.1007/978-3-319-34171-2_9},
abstract = {In this paper, we study the model of stochastic timed automata
and we target the definition of adequate composition operators that will
allow a compositional approach to the design of stochastic systems with
hard real-time constraints. This paper achieves the first step towards
that goal. Firstly, we define a parallel composition operator that
(we~prove) corresponds to the interleaving semantics for that model; we
give conditions over probability distributions, which ensure that the
operator is well-defined; and we exhibit problematic behaviours when this
condition is not satisfied. We furthermore identify a large and natural
subclass which is closed under parallel composition. Secondly, we define
a bisimulation notion which naturally extends that for continuous-time
Markov chains. Finally, we importantly show that the defined bisimulation
is a congruence w.r.t. the parallel composition, which is an expected
property for a proper modular approach to system design.}
}
@inproceedings{BBBC-icalp16,
address = {Rome, Italy},
month = jul,
year = 2016,
volume = {55},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Chatzigiannakis, Ioannis and Mitzenmacher,
Michael and Rabani, Yuval and Sangiorgi, Davide},
acronym = {{ICALP}'16},
booktitle = {{P}roceedings of the 43rd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'16)},
author = {Bertrand, Nathalie and Bouyer, Patricia and Brihaye,
{\relax Th}omas
and Carlier, Pierre},
title = {Analysing Decisive Stochastic Processes},
pages = {101:1-101:14},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBBC-icalp16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBBC-icalp16.pdf},
doi = {10.4230/LIPIcs.ICALP.2016.101},
abstract = {In~2007, Abdulla \textit{et~al.} introduced the elegant concept
of decisive Markov chain. Intuitively, decisiveness allows one to lift the
good properties of finite Markov chains to infinite Markov chains. For
instance, the approximate quantitative reachability problem can be solved
for decisive Markov chains (enjoying reasonable effectiveness assumptions)
including probabilistic lossy channel systems and probabilistic vector
addition systems with states. In this paper, we extend the concept of
decisiveness to more general stochastic processes. This extension is non
trivial as we consider stochastic processes with a potentially continuous
set of states and uncountable branching (common features of real-time
stochastic processes). This allows us to obtain decidability results for
both qualitative and quantitative verification problems on some classes of
real-time stochastic processes, including generalized semi-Markov
processes and stochastic timed automata.}
}
@inproceedings{CH-icalp16,
address = {Rome, Italy},
month = jul,
year = 2016,
volume = {55},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Chatzigiannakis, Ioannis and Mitzenmacher,
Michael and Rabani, Yuval and Sangiorgi, Davide},
acronym = {{ICALP}'16},
booktitle = {{P}roceedings of the 43rd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'16)},
author = {Dmitry Chistikov and Christoph Haase},
title = {The Taming of the Semi-Linear Set},
pages = {128:1-128:14},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CH-icalp16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CH-icalp16.pdf},
doi = {10.4230/LIPIcs.ICALP.2016.128},
abstract = {Semi-linear sets, which are finitely generated subsets of
the monoid \((\mathbb{Z}^d, +)\), have numerous applications in theoretical
computer science. Although semi-linear sets are usually given
implicitly, by formulas in Presburger arithmetic or by other means,
the effect of Boolean operations on semi-linear sets in terms of the
size of generators has primarily been studied for explicit
representations. In this paper, we develop a framework suitable for
implicitly presented semi-linear sets, in which the size of a
semi-linear set is characterized by its norm---the maximal magnitude
of a generator.\par
We put together a {"}toolbox{"} of operations and decompositions for
semi-linear sets which give bounds in terms of the norm (as opposed
to just the bit-size of the description), a unified presentation,
and simplified proofs. This toolbox, in particular, provides
exponentially better bounds for the complement and set-theoretic
difference. We also obtain bounds on unambiguous decompositions and,
as an application of the toolbox, settle the complexity of the
equivalence problem for exponent-sensitive commutative grammars.}
}
@inproceedings{Zetzche-icalp16,
address = {Rome, Italy},
month = jul,
year = 2016,
volume = {55},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Chatzigiannakis, Ioannis and Mitzenmacher,
Michael and Rabani, Yuval and Sangiorgi, Davide},
acronym = {{ICALP}'16},
booktitle = {{P}roceedings of the 43rd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'16)},
author = {Georg Zetzsche},
title = {The complexity of downward closure comparisons},
pages = {123:1-123:14},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/Zetzche-icalp16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Zetzche-icalp16.pdf},
doi = {10.4230/LIPIcs.ICALP.2016.123},
abstract = {The downward closure of a language is the set of all (not
necessarily contiguous) subwords of its members. It is well-known
that the downward closure of every language is regular. Moreover,
recent results show that downward closures are computable for quite
powerful system models.\par
One advantage of abstracting a language by its downward closure is
that then, equivalence and inclusion become decidable. In~this work,
we study the complexity of these two problems. More precisely, we
consider the following decision problems: Given languages~\(K\)
and~\(L\) from classes~\(\mathcal{C}\) and~\(\mathcal{D}\),
respectively, does the downward closure of~\(K\) include (equal)
that of~\(L\)?\par
These problems are investigated for finite automata, one-counter
automata, context-free grammars, and reversal-bounded counter
automata. For each combination, we prove a completeness result
either for fixed or for arbitrary alphabets. Moreover, for Petri net
languages, we show that both problems are Ackermann-hard and for
higher-order pushdown automata of order~\(k\), we prove hardness for
complements of nondeterministic \(k\)-fold exponential time.}
}
@inproceedings{CD-icalp16,
address = {Rome, Italy},
month = jul,
year = 2016,
volume = {55},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Chatzigiannakis, Ioannis and Mitzenmacher,
Michael and Rabani, Yuval and Sangiorgi, Davide},
acronym = {{ICALP}'16},
booktitle = {{P}roceedings of the 43rd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'16)},
author = {Chatterjee, Krishnendu and Doyen, Laurent},
title = {Computation Tree Logic for Synchronization Properties},
pages = {98:1-98:14},
url = {http://arxiv.org/abs/1604.06384},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-icalp16.pdf},
doi = {10.4230/LIPIcs.ICALP.2016.98},
abstract = {We present a logic that extends CTL (Computation Tree Logic)
with operators that express synchronization properties. A property is
synchronized in a system if it holds in all paths of a certain length. The
new logic is obtained by using the same path quantifiers and temporal
operators as in CTL, but allowing a different order of the quantifiers.
This small syntactic variation induces a logic that can express
non-regular properties for which known extensions of MSO with equality of
path length are undecidable. We show that our variant of CTL is decidable
and that the model-checking problem is in \(\Delta_3^P = P^{NP^NP}\), and
is DP-hard. We analogously consider quantifier exchange in extensions of
CTL, and we present operators defined using basic operators of CTL* that
express the occurrence of infinitely many synchronization points. We show
that the model-checking problem remains in \(\Delta_3^P\). The
distinguishing power of CTL and of our new logic coincide if the Next
operator is allowed in the logics, thus the classical bisimulation
quotient can be used for state-space reduction before model checking.}
}
@inproceedings{GLS-icalp16,
address = {Rome, Italy},
month = jul,
year = 2016,
volume = {55},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Chatzigiannakis, Ioannis and Mitzenmacher,
Michael and Rabani, Yuval and Sangiorgi, Davide},
acronym = {{ICALP}'16},
booktitle = {{P}roceedings of the 43rd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'16)},
author = {Goubault{-}Larrecq, Jean and Schmitz, Sylvain},
title = {Deciding Piecewise Testable Separability for Regular
Tree Languages},
pages = {97:1-97:15},
url = {https://hal.inria.fr/hal-01276119/},
optpdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLS-icalp16.pdf},
doi = {10.4230/LIPIcs.ICALP.2016.97},
abstract = {The piecewise testable separability problem asks, given
two input languages, whether there exists a piecewise testable
language that contains the first input language and is disjoint from
the second. We prove a general characterisation of piecewise
testable separability on languages in a well-quasi-order, in terms
of ideals of the ordering. This subsumes the known characterisations
in the case of finite words. In the case of finite ranked trees
ordered by homeomorphic embedding, we show using effective
representations for tree ideals that it entails the decidability of
piecewise testable separability when the input languages are
regular. A~final byproduct is a new proof of the decidability of
whether an input regular language of ranked trees is piecewise
testable, which was first shown in the unranked case by Boja{\'n}czyk,
Segoufin, and Straubing (Log.~Meth. in Comput.~Sci.,~8(3:26),
2012).}
}
@inproceedings{GHLT-icalp16,
address = {Rome, Italy},
month = jul,
year = 2016,
volume = {55},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Chatzigiannakis, Ioannis and Mitzenmacher,
Michael and Rabani, Yuval and Sangiorgi, Davide},
acronym = {{ICALP}'16},
booktitle = {{P}roceedings of the 43rd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'16)},
author = {Stefan G{\"o}ller and Christoph Haase and Ranko
Lazi{\'c} and Patrick Totzke},
title = {A Polynomial-Time Algorithm for Reachability in
Branching {VASS} in Dimension One},
pages = {105:1-105:13},
url = {http://arxiv.org/abs/1602.05547},
pfd = {http://www.lsv.fr/Publis/PAPERS/PDF/GHLT-icalp16.pdf},
doi = {10.4230/LIPIcs.ICALP.2016.105},
abstract = {Branching VASS (BVASS) generalise vector addition systems
with states by allowing for special branching transitions that can
non-deterministically distribute a counter value between two control
states. A~run of a BVASS consequently becomes a tree, and
reachability is to decide whether a given configuration is the root
of a reachability tree. This paper shows P-completeness of
reachability in BVASS in dimension one, the first decidability
result for reachability in a subclass of BVASS known so~far.
Moreover, we~show that coverability and boundedness in BVASS in
dimension one are P-complete as~well.}
}
@inproceedings{BCM-cav16,
address = {Toronto, Canada},
month = jul,
year = 2016,
volume = 9779,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Chaudhuri, Swarat and Farzan, Azadeh},
acronym = {{CAV}'16},
booktitle = {{P}roceedings of the 28th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'16)~-- {P}art~{I}},
author = {Bouyer, Patricia and Colange, Maximilien and Markey, Nicolas},
title = {Symbolic Optimal Reachability in Weighted Timed Automata},
pages = {513-530},
url = {http://arxiv.org/abs/1602.00481},
doi = {10.1007/978-3-319-41528-4_28},
abstract = {Weighted timed automata have been defined in the early 2000's
for modelling resource-consumption or -allocation problems in real-time
systems. Optimal reachability is decidable in weighted timed automata, and
a symbolic forward algorithm has been developed to solve that problem. This
algorithm uses so-called priced zones, an extension of standard zones with
cost functions. In order to ensure termination, the algorithm requires
clocks to be bounded. For unpriced timed automata, much work has been done
to develop sound abstractions adapted to the forward exploration of timed
automata, ensuring termination of the model-checking algorithm without
bounding the clocks. In this paper, we take advantage of recent
developments on abstractions for timed automata, and propose an algorithm
allowing for symbolic analysis of all weighted timed automata, without
requiring bounded clocks.}
}
@inproceedings{BMRSS-icalp16,
address = {Rome, Italy},
month = jul,
year = 2016,
volume = {55},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Chatzigiannakis, Ioannis and Mitzenmacher,
Michael and Rabani, Yuval and Sangiorgi, Davide},
acronym = {{ICALP}'16},
booktitle = {{P}roceedings of the 43rd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'16)},
author = {Bouyer, Patricia and Markey, Nicolas and Randour,
Mickael and Sangnier, Arnaud and Stan, Daniel},
title = {Reachability in Networks of Register Protocols under
Stochastic Schedulers},
pages = {106:1-106:14},
url = {http://arxiv.org/abs/1602.05928},
doi = {10.4230/LIPIcs.ICALP.2016.106},
abstract = {We study the almost-sure reachability problem in a distributed
system obtained as the asynchronous composition of~\(N\) copies (called
\emph{processes}) of the same automaton (called \emph{protocol}), that can
communicate via a shared register with finite domain. The automaton has
two types of transitions: write-transitions update the value of the
register, while read-transitions move to a new state depending on the
content of the register. Non-determinism is resolved by a stochastic
scheduler. Given a protocol, we focus on almost-sure reachability of a
target state by one of the processes. The answer to this problem naturally
depends on the number~\(N\) of processes. However, we prove that our
setting has a cut-off property : the answer to the almost-sure
reachability problem is constant when \(N\) is large enough; we~then
develop an EXPSPACE algorithm deciding whether this constant answer is
positive or negative.}
}
@inproceedings{LS-lics16,
address = {New York City, USA},
month = jul,
year = 2016,
publisher = {ACM Press},
editor = {Grohe, Martin and Koskinen, Eric and Shankar, Natarajan},
acronym = {{LICS}'16},
booktitle = {{P}roceedings of the 31st {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'16)},
author = {Ranko Lazi{\'c} and Sylvain Schmitz},
title = {The Complexity of Coverability in {{\(\nu\)}}-{P}etri Nets},
pages = {467-476},
url = {https://hal.inria.fr/hal-01265302},
doi = {10.1145/2933575.2933593},
abstract = {We show that the coverability problem in nu-Petri
nets is complete for `double Ackermann' time, thus
closing an open complexity gap between an Ackermann
lower bound and a hyper-Ackermann upper bound. The
coverability problem captures the verification of
safety properties in this nominal extension of Petri
nets with name management and fresh name
creation. Our completeness result establishes
nu-Petri nets as a model of intermediate power among
the formalisms of nets enriched with data, and
relies on new algorithmic insights brought by the
use of well-quasi-order ideals.}
}
@inproceedings{DBHS-lics16,
address = {New York City, USA},
month = jul,
year = 2016,
publisher = {ACM Press},
editor = {Grohe, Martin and Koskinen, Eric and Shankar, Natarajan},
acronym = {{LICS}'16},
booktitle = {{P}roceedings of the 31st {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'16)},
author = {Amina Doumane and David Baelde and Lucca Hirschi
and Alexis Saurin},
title = {Towards Completeness via Proof Search in the Linear
Time {{\(\mu\)}}-calculus},
pages = {377-386},
url = {https://hal.archives-ouvertes.fr/hal-01275289/},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DBHS-lics16.pdf},
doi = {10.1145/2933575.2933598},
abstract = {Modal \(\mu\)-calculus is one of the central
languages of logic and verification, whose study
involves notoriously complex objects: automata over
infinite structures on the model-theoretical side;
infinite proofs and proofs by (co)induction on the
proof-theoretical side. Nevertheless,
axiomatizations have been given for both linear and
branching time \(\mu\)-calculi, with quite involved
completeness arguments. We come back to this
central problem, considering it from a proof search
viewpoint, and provide some new completeness
arguments in the linear time \(\mu\)-calculus. Our
results only deal with restricted classes of
formulas that closely correspond to
(non-alternating) \(\omega\)-automata but, compared
to earlier proofs, our completeness arguments are
direct and constructive. We first consider a
natural circular proof system based on sequent
calculus, and show that it is complete for
inclusions of parity automata directly expressed as
formulas, making use of Safra's construction
directly in proof search. We then consider the
corresponding finitary proof system, featuring
(co)induction rules, and provide a partial
translation result from circular to finitary
proofs. This yields completeness of the finitary
proof system for inclusions of sufficiently
deterministic parity automata, and finally for
arbitrary B{\"u}chi automata.}
}
@inproceedings{CG-lics16,
address = {New York City, USA},
month = jul,
year = 2016,
publisher = {ACM Press},
editor = {Grohe, Martin and Koskinen, Eric and Shankar, Natarajan},
acronym = {{LICS}'16},
booktitle = {{P}roceedings of the 31st {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'16)},
author = {{\relax Th}omas Colcombet and Stefan G{\"o}ller},
title = {Games with bound guess actions},
pages = {257-266},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CG-lics16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CG-lics16.pdf},
doi = {10.1145/2933575.2934502},
abstract = {We introduce games with (bound) guess actions. These are games in which the players may be asked along the play to provide num- bers that need to satisfy some bounding constraints. These are nat- ural extensions of domination games occurring in the regular cost function theory. In this paper we consider more specifically the case where the constraints to be bounded are regular cost functions, and the long term goal is an ?-regular winning condition. We show that such games are decidable on finite arenas.}
}
@inproceedings{CD-lics16,
address = {New York City, USA},
month = jul,
year = 2016,
publisher = {ACM Press},
editor = {Grohe, Martin and Koskinen, Eric and Shankar, Natarajan},
acronym = {{LICS}'16},
booktitle = {{P}roceedings of the 31st {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'16)},
author = {Chatterjee, Krishnendu and Doyen, Laurent},
title = {Perfect-information Stochastic Games with
Generalized Mean-Payoff Objectives},
pages = {247-256},
url = {http://arxiv.org/abs/1604.06376},
doi = {10.1145/2933575.2934513},
abstract = {Graph games provide the foundation for modeling and synthesizing reactive processes. In the synthesis of stochastic reactive processes, the traditional model is perfect-information stochastic games, where some transitions of the game graph are controlled by two adversarial players, and the other transitions are executed probabilistically. We consider such games where the objective is the conjunction of several quantitative objectives (specified as mean-payoff conditions), which we refer to as generalized mean-payoff objectives. The basic decision problem asks for the existence of a finite-memory strategy for a player that ensures the generalized mean-payoff objective be satisfied with a desired probability against all strategies of the opponent. A special case of the decision problem is the almost-sure problem where the desired probability is~1. Previous results presented a semi-decision procedure for epsilon-approximations of the almost-sure problem. In this work, we show that both the almost-sure problem as well as the general basic decision problem are coNP-complete, significantly improving the previous results. Moreover, we show that in the case of 1-player stochastic games, randomized memoryless strategies are sufficient and the problem can be solved in polynomial time. In contrast, in two-player stochastic games, we show that even with randomized strategies exponential memory is required in general, and present a matching exponential upper bound. We also study the basic decision problem with infinite-memory strategies and present computational complexity results for the problem. Our results are relevant in the synthesis of stochastic reactive systems with multiple quantitative requirements. }
}
@inproceedings{DOMZ-lics16,
address = {New York City, USA},
month = jul,
year = 2016,
publisher = {ACM Press},
editor = {Grohe, Martin and Koskinen, Eric and Shankar, Natarajan},
acronym = {{LICS}'16},
booktitle = {{P}roceedings of the 31st {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'16)},
author = {D'Osualdo, Emanuele and Roland Meyer and Georg Zetzsche},
title = {First-order logic with reachability for infinite-state systems},
pages = {457-466},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DOMZ-lics16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DOMZ-lics16.pdf},
doi = {10.1145/2933575.2934552},
abstract = {First-order logic with the reachability predicate
(FO(R)) is an important means of specification in
system analysis. Its decidability status is known
for some individual types of infinite-state systems
such as pushdown (decidable) and vector addition
systems (undecidable). \par This work aims at a
general understanding of which types of systems
admit decidability. As a unifying model, we employ
valence systems over graph monoids, which feature a
finite-state control and are parameterized by a
monoid to represent their storage mechanism. As
special cases, this includes pushdown systems,
various types of counter systems (such as vector
addition systems) and combinations thereof. Our
main result is a complete characterization of those
graph monoids where FO(R) is decidable for the
resulting transition systems.}
}
@inproceedings{ACHKSZ-lics16,
address = {New York City, USA},
month = jul,
year = 2016,
publisher = {ACM Press},
editor = {Grohe, Martin and Koskinen, Eric and Shankar, Natarajan},
acronym = {{LICS}'16},
booktitle = {{P}roceedings of the 31st {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'16)},
author = {Atig, Mohamed Faouzi and Dmitry Chistikov and Piotr
Hofman and Kumar, K. Narayan and Prakash Saivasan and
Georg Zetzsche},
title = {Complexity of regular abstractions of one-counter languages},
pages = {207-216},
url = {http://arxiv.org/abs/1602.03419},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ACHKSZ-lics16.pdf},
doi = {10.1145/2933575.2934561},
abstract = {We study the computational and descriptional complexity of
the following transformation: Given a one-counter
automaton~(OCA)~\(A\), construct a nondeterministic
finite automaton~(NFA)~\(B\) that recognizes an
abstraction of the language~\(L(A)\): its~(1)~downward
closure, (2)~upward closure, or (3)~Parikh image. For
the Parikh image over a fixed alphabet and for the
upward and downward closures, we find polynomial-time
algorithms that compute such an NFA. For the Parikh
image with the alphabet as part of the input, we find
a quasi-polynomial time algorithm and prove a
completeness result: we construct a sequence of OCA
that admits a polynomial-time algorithm iff there is
one for all OCA. For all three abstractions, it was
previously unknown if appropriate NFA of
sub-exponential size exist.}
}
@inproceedings{HBD-sp16,
address = {San Jose, California, USA},
month = may,
year = 2016,
publisher = {IEEECSP},
editor = {Locasto, Michael and Shmatikov, Vitaly and Erlingsson, {\'U}lfar},
acronym = {{S\&P}'16},
booktitle = {{P}roceedings of the 37th {IEEE} {S}ymposium
on {S}ecurity and {P}rivacy ({S\&P}'16)},
author = {Hirschi, Lucca and Baelde, David and Delaune, St{\'e}phanie},
title = {A~method for verifying privacy-type properties:
the~unbounded case},
pages = {564-581},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HBD-sp16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HBD-sp16.pdf},
doi = {10.1109/SP.2016.40},
abstract = {In~this paper, we~consider the problem of verifying
anonymity and unlinkability in the symbolic model, where protocols
are represented as processes in a variant of the applied pi calculus
notably used in the Proverif tool. Existing tools and techniques do
not allow one to verify directly these properties, expressed as
behavioral equivalences. We propose a different approach: we design
two conditions on protocols which are sufficient to ensure anonymity
and unlinkability, and which can then be effectively checked
automatically using Proverif. Our two conditions correspond to two
broad classes of attacks on unlinkability, corresponding to data and
control-flow leaks.\par
This theoretical result is general enough to apply to a wide class
of protocols. In particular, we apply our techniques to provide the
first formal security proof of the BAC protocol (e-passport). Our
work has also lead to the discovery of new attacks, including one on
the LAK protocol (RFID authentication) which was previously claimed
to be unlinkable (in~a weak sense) and one on the PACE protocol
(e-passport).}
}
@inproceedings{CC-pn16,
address = {Tor{\'u}n, Poland},
month = jun,
year = 2016,
volume = {9698},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Kordon, Fabrice and Moldt, Daniel},
acronym = {{PETRI~NETS}'16},
booktitle = {{P}roceedings of the 37th
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({PETRI~NETS}'16)},
author = {Carmona, Josep and Chatain, {\relax Th}omas},
title = {Anti-Alignments in Conformance Checking~-- The~Dark Side of Process Models},
pages = {240-258},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CC-pn16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CC-pn16.pdf},
doi = {10.1007/978-3-319-39086-4_15},
abstract = {Conformance checking techniques asses the suitability of a
process model in representing an underlying process, observed
through a collection of real executions. These techniques suffer
from the well-known state space explosion problem, hence handling
process models exhibiting large or even infinite state spaces
remains a challenge. One important metric in conformance checking is
to asses the precision of the model with respect to the observed
executions, i.e., characterize the ability of the model to produce
behavior unrelated to the one observed. By~avoiding the computation
of the full state space of a model, current techniques only provide
estimations of the precision metric, which in some situations tend
to be very optimistic, thus hiding real problems a process model may
have. In this paper we present the notion of anti-alignment as a
concept to help unveiling traces in the model that may deviate
significantly from the observed behavior. Using anti-alignments,
current estimations can be improved, e.g., in precision checking. We
show how to express the problem of finding anti-alignments as the
satisfiability of a Boolean formula, and provide a tool which can
deal with large models efficiently.}
}
@comment{{B-arxiv16,
author = Bollig, Benedikt,
affiliation = aff-LSVmexico,
title = One-Counter Automata with Counter Visibility,
institution = Computing Research Repository,
number = 1602.05940,
month = feb,
nmonth = 2,
year = 2016,
type = RR,
axeLSV = mexico,
NOcontrat = "",
url = http://arxiv.org/abs/1602.05940,
PDF = "http://www.lsv.fr/Publis/PAPERS/PDF/B-arxiv16.pdf",
lsvdate-new = 20160222,
lsvdate-upd = 20160222,
lsvdate-pub = 20160222,
lsv-category = "rapl",
wwwpublic = "public and ccsb",
note = 18~pages,
abstract = "In a one-counter automaton (OCA), one can read a letter
from some finite alphabet, increment and decrement the counter by
one, or test it for zero. It is well-known that universality and
language inclusion for OCAs are undecidable. We consider here OCAs
with counter visibility: Whenever the automaton produces a letter,
it outputs the current counter value along with~it. Hence, its
language is now a set of words over an infinite alphabet. We show
that universality and inclusion for that model are in PSPACE, thus
no harder than the corresponding problems for finite automata, which
can actually be considered as a special case. In fact, we show that
OCAs with counter visibility are effectively determinizable and
closed under all boolean operations. As~a~strict generalization, we
subsequently extend our model by registers. The general nonemptiness
problem being undecidable, we impose a bound on the number of
register comparisons and show that the corresponding nonemptiness
problem is NP-complete.",
}}
@techreport{DD-arxiv16,
author = {D{\'i}az{-}Caro, Alejandro and Dowek, Gilles},
title = {Quantum superpositions and projective measurement in
the lambda calculus},
institution = {Computing Research Repository},
number = {1601.04294},
year = {2016},
month = jan,
type = {Research Report},
url = {http://arxiv.org/abs/1601.04294},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-arxiv16.pdf},
note = {22~pages},
abstract = {We propose an extension of simply typed lambda-calculus to
handle some properties of quantum computing. The equiprobable quantum
superposition is taken as a commutative pair and the quantum measurement
as a non-deterministic projection over it. Destructive interferences are
achieved by introducing an inverse symbol with respect to pairs. The
no-cloning property is ensured by using a combination of syntactic
linearity with linear logic. Indeed, the syntactic linearity is enough for
unitary gates, while a function measuring its argument needs to enforce
that the argument is used only once.}
}
@inproceedings{FGMP-hscc16,
address = {Vienna, Austria},
month = apr,
year = 2016,
publisher = {ACM Press},
editor = {Abate, Alessandro and Fainekos, Georgios},
acronym = {{HSCC}'16},
booktitle = {{P}roceedings of the 19th {ACM} {I}nternational {C}onference
on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
({HSCC}'16)},
author = {Fribourg, Laurent and Goubault, {\'E}ric and Mohamed, Sameh
and Putot, Sylvie},
title = {A~Topological Method for Finding Invariant Sets of Switched Systems},
pages = {61-70},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FGMP-hscc16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FGMP-hscc16.pdf},
doi = {10.1145/2883817.2883822},
abstract = {We~revisit the problem of finding controlled invariants sets
(viability), for a class of differential inclusions, using topological
methods based on Wazewski property. In~many ways, this generalizes the
Viability Theorem approach, which is itself a generalization of the
Lyapunov function approach for systems described by ordinary differential
equations. We give a computable criterion based on SoS methods for a class
of differential inclusions to have a non-empty viability kernel within
some given region. We use this method to prove the existence of
(controlled) invariant sets of switched systems inside a region described
by a polynomial template, both with time-dependent switching and with
state-based switching through a finite set of hypersurfaces. A~Matlab
implementation allows us to demonstrate its use.}
}
@phdthesis{rc-phd2016,
author = {Chr{\'e}tien, R{\'e}my},
title = {Analyse automatique de propri{\'e}t{\'e}s d'{\'e}quivalence pour
les protocoles cryptographiques},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2016,
month = jan,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/rc-phd16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/rc-phd16.pdf}
}
@inproceedings{LS-stacs16,
address = {Orl{\'e}ans, France},
month = feb,
year = 2016,
volume = {47},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Ollinger, Nicolas and Vollmer, Heribert},
acronym = {{STACS}'16},
booktitle = {{P}roceedings of the 33rd {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'16)},
author = {Leroux, J{\'e}r{\^o}me and Schmitz, Sylvain},
title = {Ideal Decompositions for Vector Addition Systems},
pages = {1:1-1:13},
url = {http://drops.dagstuhl.de/opus/volltexte/2016/5702},
doi = {10.4230/LIPIcs.STACS.2016.1},
abstract = {Vector addition systems, or equivalently Petri nets, are one of
the most popular formal models for the representation and the analysis of
parallel processes. Many problems for vector addition systems are known to
be decidable thanks to the theory of well-structured transition systems.
Indeed, vector addition systems with configurations equipped with the
classical point-wise ordering are well-structured transition systems.
Based on this observation, problems like coverability or termination can
be proven decidable.\par
However, the theory of well-structured transition systems does not explain
the decidability of the reachability problem. In this presentation, we
show that runs of vector addition systems can also be equipped with a well
quasi-order. This observation provides a unified understanding of the data
structures involved in solving many problems for vector addition systems,
including the central reachability problem.}
}
@article{siglog16-Schmitz,
publisher = {ACM Press},
journal = {SIGLOG News},
author = {Schmitz, Sylvain},
title = {Automata column: The~complexity of reachability in
vector addition systems},
volume = 3,
number = 1,
pages = {3-21},
year = 2016,
month = jan,
url = {https://hal.inria.fr/hal-01275972},
doi = {10.1145/2893582.2893585},
annote = {Invited column},
abstract = {The program of the 30th Symposium on Logic in Computer Science
held in 2015 in Kyoto included two contributions on the computational
complexity of the reachability problem for vector addition systems:
Blondin, Finkel, G{\"o}ller, Haase, and McKenzie~[2015] attacked the
problem by providing the first tight complexity bounds in the case of
dimension-2 systems with states, while Leroux and Schmitz~[2015] proved
the first complexity upper bound in the general case. The purpose of this
column is to present the main ideas behind these two results, and more
generally survey the current state of affairs.}
}
@article{CFS-tcs16,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Chambart, Pierre and Finkel, Alain and Schmitz, Sylvain},
title = {Forward Analysis and Model Checking for Trace
Bounded~{WSTS}},
year = 2016,
volume = {637},
pages = {1-29},
month = jul,
url = {http://arxiv.org/abs/1004.2802},
doi = {10.1016/j.tcs.2016.04.020},
abstract = {We investigate a subclass of well-structured transition
systems~(WSTS), the bounded---in the sense of Ginsburg and Spanier
(Trans.~AMS, 1964)---complete deterministic ones, which we claim provide
an adequate basis for the study of forward analyses as developed by
Finkel and Goubault-Larrecq (ICALP~2009). Indeed, we prove that, unlike
other conditions considered previously for the termination of forward
analysis, boundedness is decidable. Boundedness turns out to be a
valuable restriction for WSTS verification, as we show that it further
allows to decide all {{\(\omega\)}}-regular properties on the set of infinite
traces of the system.}
}
@article{toct-Schmitz13,
publisher = {ACM Press},
journal = {ACM Transactions on Computation Theory},
author = {Schmitz, Sylvain},
title = {Complexity Hierarchies Beyond {E}lementary},
volume = {8},
number = {1:3},
nopages = {},
year = 2016,
month = feb,
url = {http://arxiv.org/abs/1312.5686},
doi = {10.1145/2858784},
abstract = {We introduce a hierarchy of fast-growing complexity classes and
show its suitability for completeness statements of many non elementary
problems. This hierarchy allows the classification of many decision
problems with a non-elementary complexity, which occur naturally in
logic, combinatorics, formal languages, verification, etc., with
complexities ranging from simple towers of exponentials to Ackermannian
and beyond.}
}
@inproceedings{CCHPW-fossacs16,
address = {Eindhoven, The~Netherlands},
month = apr,
year = 2016,
volume = {9634},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Jacobs, Bart and L{\"o}ding, Christof},
acronym = {{FoSSaCS}'16},
booktitle = {{P}roceedings of the 19th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'16)},
author = {Chistikov, Dmitry and Czerwi{\'n}ski, Wojciech and Hofman,
Piotr and Pilipczuk, Micha{\l} and Wehar, Michael},
title = {Shortest paths in one-counter systems},
pages = {462-478},
url = {http://arxiv.org/abs/1510.05460},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCHPW-fossacs16.pdf},
doi = {10.1007/978-3-662-49630-5_27},
abstract = {We show that any one-counter automaton with \(n\) states, if its
language is non-empty, accepts some word of length at most~\(O(n^2)\).
This closes the gap between the previously known upper bound of~\(O(n^3)\)
and lower bound of~\(\Omega(n^2)\). More generally, we prove a tight upper
bound on the length of shortest paths between arbitrary configurations in
one-counter transition systems. Weaker bounds have previously appeared in
the literature, and our result offers an improvement.}
}
@inproceedings{HLLLST-fossacs16,
address = {Eindhoven, The~Netherlands},
month = apr,
year = 2016,
volume = {9634},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Jacobs, Bart and L{\"o}ding, Christof},
acronym = {{FoSSaCS}'16},
booktitle = {{P}roceedings of the 19th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'16)},
author = {Hofman, Piotr and Lasota, S{\l}awomir and Lazi{\'c}, Ranko and
Leroux, J{\'e}r{\^o}me and Schmitz, Sylvain and Totzke, Patrick},
title = {Coverability Trees for {P}etri Nets with Unordered Data},
pages = {445-461},
url = {https://hal.inria.fr/hal-01252674},
doi = {10.1007/978-3-662-49630-5_26},
abstract = {We study an extension of classical Petri nets where tokens carry
values from a countable data domain, that can be tested for equality upon
firing transitions. These Unordered Data Petri Nets (UDPN) are
well-structured and therefore allow generic decision procedures for
several verification problems including coverability and boundedness. We
show how to construct a finite representation of the coverability set in
terms of its ideal decomposition. This not only provides an alternative
method to decide coverability and boundedness, but is also an important
step towards deciding the reachability problem. This also allows to answer
more precise questions about the reachability set, for instance whether
there is a bound on the number of tokens on a given place (place
boundedness), or if such a bound exists for the number of different data
values carried by tokens (place width boundedness). We provide matching
Hyper-Ackermann bounds on the size of cover-ability trees and on the
running time of the induced decision procedures.}
}
@inproceedings{FG-fossacs16,
address = {Eindhoven, The~Netherlands},
month = apr,
year = 2016,
volume = {9634},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Jacobs, Bart and L{\"o}ding, Christof},
acronym = {{FoSSaCS}'16},
booktitle = {{P}roceedings of the 19th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'16)},
author = {Fortin, Marie and Gastin, Paul},
title = {Verification of parameterized communicating automata via split-width},
pages = {197-213},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FG-fossacs16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FG-fossacs16.pdf},
doi = {10.1007/978-3-662-49630-5_12},
abstract = {We~study verification problems for distributed systems
communicating via unbounded FIFO channels. The number of processes
of the system as well as the communication topology are not fixed
a~priori. Systems are given by parameterized communicating automata
(PCAs) which can be run on any communication topology of bounded
degree, with arbitrarily many processes. Such systems are Turing
powerful so we concentrate on under-approximate verification. We
extend the notion of split-width to behaviors of PCAs. We show that
emptiness, reachability and model-checking problems of PCAs are
decidable when restricted to behaviors of bounded split-width.
Reachability and emptiness are EXPTIME-complete, but only polynomial
in the size of the PCA. We also describe several concrete classes of
bounded split-width, for which we prove similar results.}
}
@inproceedings{CDD-post16,
address = {Eindhoven, The~Netherlands},
month = apr,
year = 2016,
volume = { 9635},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Piessens, Frank and Vigan{\'o}, Luca},
acronym = {{POST}'16},
booktitle = {{P}roceedings of the 5th {I}nternational {C}onference on
{P}rinciples of {S}ecurity and {T}rust
({POST}'16)},
author = {Cortier, V{\'e}ronique and Dallon, Antoine and
Delaune, St{\'e}phanie},
title = {Bounding the number of agents, for equivalence~too},
pages = {211-232},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDD-post16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDD-post16.pdf},
doi = {10.1007/978-3-662-49635-0_11},
abstract = {Bounding the number of agents is a current practice when
modeling a protocol. In~2003, it has been shown that one honest agent and
one dishonest agent are indeed sufficient to find all possible attacks,
for secrecy properties. This is no longer the case for equivalence
properties, crucial to express many properties such as vote privacy or
untraceability.\par
In this paper, we show that it is sufficient to consider two honest agents
and two dishonest agents for equivalence properties, for deterministic
processes with standard primitives and without else branches. More
generally, we show how to bound the number of agents for arbitrary
constructor theories and for protocols with simple else branches. We show
that our hypotheses are tight, providing counter-examples for non
actiondeterministic processes, non constructor theories, or protocols with
complex else branches.}
}
@inproceedings{tacas16-BFHH,
address = {Eindhoven, The Netherlands},
month = apr,
year = 2016,
volume = {9636},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Chechik, Marsha and Raskin, Jean-Fran{\c{c}}ois},
acronym = {{TACAS}'16},
booktitle = {{P}roceedings of the 22th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'16)},
author = {Blondin, Michael and Finkel, Alain and Haase, Christoph and
Haddad, Serge},
title = {Approaching the Coverability Problem Continuously},
pages = {480-496},
url = {http://arxiv.org/abs/1510.05724},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/arxiv15-BFHH.pdf},
doi = {10.1007/978-3-662-49674-9_28},
abstract = {The coverability problem for Petri nets plays a central role in
the verification of concurrent shared-memory programs. However, its high
EXPSPACE-complete complexity poses a challenge when encountered in
real-world instances. In this paper, we develop a new approach to this
problem which is primarily based on applying forward coverability in
continuous Petri nets as a pruning criterion inside a backward
coverability framework. A cornerstone of our approach is the efficient
encoding of a recently developed polynomial-time algorithm for
reachability in continuous Petri nets into SMT. We demonstrate the
effectiveness of our approach on standard benchmarks from the literature,
which shows that our approach decides significantly more instances than
any existing tool and is in addition often much faster, in particular on
large instances.}
}
@inproceedings{HH-stacs16,
address = {Orl{\'e}ans, France},
month = feb,
year = 2016,
volume = {47},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Ollinger, Nicolas and Vollmer, Heribert},
acronym = {{STACS}'16},
booktitle = {{P}roceedings of the 33rd {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'16)},
author = {Haase, Christoph and Hofman, Piotr},
title = {Tightening the Complexity of Equivalence Problems for
Commutative Grammars},
pages = {41:1-14},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HH-stacs16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HH-stacs16.pdf},
doi = {10.4230/LIPIcs.STACS.2016.41},
abstract = {Given two finite-state automata, are the Parikh images of the
languages they generate equivalent? This problem was shown decidable in
coNEXP by Huynh in 1985 within the more general setting of context-free
commutative grammars. Huynh conjectured that a~\(\Pi_{2}^{P}\) upper bound
might be possible, and Kopczy{\'n}ski and To established in 2010 such an
upper bound when the size of the alphabet is fixed. The contribution of
this paper is to show that the language equivalence problem for regular
and context-free commutative grammars is actually coNEXP-complete. In
addition, our lower bound immediately yields further coNEXP-completeness
results for equivalence problems for regular commutative expressions,
reversal-bounded counter automata and communication-free Petri nets.
Finally, we improve both lower and upper bounds for language equivalence
for exponent-sensitive commutative grammars.}
}
@inproceedings{BHL-lata16,
address = {Prague, Czech Republic},
month = mar,
year = 2016,
volume = {9618},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Mart{\'\i}n-Vide, Carlos},
acronym = {{LATA}'16},
booktitle = {{P}roceedings of the 10th {I}nternational {C}onference on {L}anguage
and {A}utomata {T}heory and {A}pplications ({LATA}'16)},
author = {Bertrand, Nathalie and Haddad, Serge and Lefaucheux, Engel},
title = {Accurate Approximate Diagnosability of Stochastic Systems},
pages = {549-561},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHL-lata16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHL-lata16.pdf},
doi = {10.1007/978-3-319-30000-9_42},
abstract = {Diagnosis of partially observable stochastic systems prone to
faults was introduced in the late nineties. Diagnosability, i.e. the
existence of a diagnoser, may be specified in different ways: (1)~exact
diagnosability (called A-diagnosability) requires that almost surely a
fault is detected and that no fault is erroneously claimed while
(2)~approximate diagnosability (called \(\varepsilon\)-diagnosability)
allows a small probability of error when claiming a fault and (3)~accurate
approximate diagnosability (called AA-diagnosability) requires that this
error threshold may be chosen arbitrarily small. Here we mainly focus on
approximate diagnoses. We first refine the almost sure requirement about
finite delay introducing a uniform version and showing that while it does
not discriminate between the two versions of exact diagnosability this is
no more the case in approximate diagnosis. Then we establish a complete
picture for the decidability status of the diagnosability problems:
(uniform) \(\varepsilon\)-diagnosability and uniform AA-diagnosability are
undecidable while AA-diagnosability is decidable in PTIME, answering a
longstanding open question.}
}
@article{DD-tocl15b,
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
author = {Demri, St{\'e}phane and Deters, Morgan},
title = {Expressive Completeness of Separation Logic With Two Variables and
No Separating Conjunction},
volume = {17},
number = {2},
pages = {12:1-12:44},
month = mar,
year = 2016,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-tocl15b.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DD-tocl15b.pdf},
doi = {10.1145/2835490},
abstract = {Separation logic is used as an assertion language for
Hoare-style proof systems about programs with pointers, and there is an
ongoing quest for understanding its complexity and expressive power.
Herein, we show that first-order separation logic with one record field
restricted to two variables and the separating implication (no~separating
conjunction) is as expressive as weak second-order logic, substantially
sharpening a previous result. Capturing weak second-order logic with such
a restricted form of separation logic requires substantial updates to
known proof techniques. We develop these, and as a by-product identify the
smallest fragment of separation logic known to be undecidable: first-order
separation logic with one record field, two variables, and no separating
conjunction. Because we forbid ourselves the use of many syntactic
resources, this underscores even further the power of separating
implication on concrete heaps.}
}
@article{HOW-fi15,
publisher = {{IOS} Press},
journal = {Fundamenta Informaticae},
author = {Haase, Christoph and Ouaknine, Jo{\"e}l and Worrell, James},
title = {Relating Reachability Problems in Timed and Counter Automata},
volume = {143},
number = {3-4},
pages = {317-338},
year = 2016,
month = jan,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HOW-fi15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HOW-fi15.pdf},
doi = {10.3233/FI-2016-1316},
abstract = {We establish a relationship between reachability problems in
timed automata and space-bounded counter automata. We show that
reachability in timed automata with three or more clocks is
logarithmic-space inter-reducible with reachability in space-bounded
counter automata with two counters. We moreover show the logarithmic-space
equivalence of reachability in two-clock timed automata and space-bounded
one-counter automata. This last reduction has recently been employed by
Fearnley and Jurdzi{\'n}ski to settle the computational complexity of
reachability in two-clock timed automata.}
}
@techreport{BJM-arxiv16,
author = {Bouyer, Patricia and Markey, Nicolas and Jug{\'e}, Vincent},
title = {Dynamic Complexity of Parity Games with Bounded Tree-Width},
institution = {Computing Research Repository},
number = {1610.00571},
year = {2016},
url = {https://arxiv.org/abs/1610.00571},
pdf = {https://arxiv.org/abs/1610.00571},
month = oct,
type = {Research Report},
note = {33~pages}
}
@misc{mcc:2016,
author = {F. Kordon and H. Garavel and L. M. Hillah and Hulin{-}Hubard, Francis
and G. Chiardo and A. Hamez and L. Jezequel and A. Miner and J. Meijer
and E. Paviot-Adet and D. Racordon and C. Rodriguez and C. Rohr and J.
Srba and Y. Thierry-Mieg and G. Tr{\d i}nh and K. Wolf},
month = jun,
title = {{Complete Results for the 2016 Edition of the Model Checking Contest}},
year = {2016},
url = {http://mcc.lip6.fr/2016/results.php}
}
@misc{JGL:pls16,
author = {Goubault{-}Larrecq, Jean},
howpublished = {Encart dans l'article ''S'adapter {\`a} la cyberguerre'', de Karen Elazari, Pour La Science 459},
month = jan,
title = {Les m{\'e}thodes formelles: l'autre arme de la cybers{\'e}curit{\'e}},
year = {2016},
pages = {50-55}
}
@misc{JGL:stc16,
author = {Goubault{-}Larrecq, Jean},
howpublished = {Invited talk (plenary speaker), Summer Topology Conference, Leicester, UK},
month = aug,
title = {A few things on Noetherian spaces},
year = {2016}
}
@misc{JGL:gs16,
author = {Goubault{-}Larrecq, Jean},
howpublished = {Invited talk, Galway Symposium, Leicester, UK},
month = aug,
title = {An introduction to asymmetric topology and domain theory: why, what, and how},
year = {2016}
}
@misc{JGL:dm16,
author = {Goubault{-}Larrecq, Jean},
howpublished = {Invited talk, Dale Miller Festschrift, Paris Diderot University, Paris},
month = dec,
title = {A semantics for {{\(\nabla\)}}},
year = {2016}
}
@misc{GSHM:dga-inria16,
author = {Goubault-Larrecq, Jean and Sentucq, Pierre-Arnaud and Hulin-Hubard, Francis and Majorczyk, Fr{\'e}d{\'e}ric},
howpublished = {Rapport final et fourniture 4 du contrat DGA-INRIA Orchids},
month = may,
title = {Etat final des travaux engag{\'e}s sur {Orchids}},
year = {2016}
}
@misc{GM:dga-inria16,
author = {Goubault-Larrecq, Jean and Majorczyk, Fr{\'e}d{\'e}ric},
howpublished = {Fourniture 3 du contrat DGA-INRIA Orchids},
month = may,
title = {G{\'e}n{\'e}ration de signatures pour le suivi de flux d'informations},
year = {2016}
}
@inproceedings{AMP-lfmtp16,
address = {Porto, Portugal},
month = jun,
publisher = {ACM Press},
editor = {Dowek, Gilles and Licata, Daniel R. and Alves, Sandra},
acronym = {{LFMTP}'16},
booktitle = {Proceedings of the 11th {I}nternational {W}orkshop on {L}ogical {F}rameworks and
{M}eta-{L}anguages: {T}heory and {P}ractice ({LFMTP}'16)},
author = {Cauderlier, Rapha{\"e}l},
title = {{{A Rewrite System for Proof Constructivization}}},
pages = {2:1-2:7},
year = {2016},
doi = {10.1007/978-3-319-40578-0\_5},
url = {https://hal.inria.fr/hal-01420634/},
pdf = {https://hal.inria.fr/hal-01420634/file/LFMTP_2016.pdf},
abstract = {Proof constructivization is the problem of automatically extracting constructive proofs out of classical proofs. This process is required when classical theorem provers are integrated in intuitionistic proof assistants. We use the ability of rewrite systems to represent partial functions to implement heuristics for proof constructivization in Dedukti, a logical framework based on rewriting in which proofs are first-class objects which can be the subject of computation. We benchmark these heuristics on the proofs output by the automated theorem prover Zenon on the TPTP library of problems.}
}
@inproceedings{AMP-rc16,
address = {Bologna, Italy},
month = jul,
volume = 9720,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Lanese, Ivan and Devitt, Simon},
acronym = {{RC}'16},
booktitle = {8th Conference on Reversible Computation (RC'16)},
author = {Arrighi, Pablo and Martiel, Simon and Perdrix, Simon},
title = {{{Reversible Causal Graph Dynamics}}},
pages = {73-88},
year = {2016},
doi = {10.1007/978-3-319-40578-0\_5},
url = {https://hal.archives-ouvertes.fr/hal-01361427},
abstract = {Causal Graph Dynamics extend Cellular Automata to arbitrary , bounded-degree, time-varying graphs. The whole graph evolves in discrete time steps, and this global evolution is required to have a number of physics-like symmetries: shift-invariance (it acts everywhere the same) and causality (information has a bounded speed of propagation). We add a further physics-like symmetry, namely reversibility.}
}
@inproceedings{ADJL-hatt2016,
author = {Assaf, Ali and Dowek, Gilles and Jouannaud, Jean-Pierre and Liu, Jiaxiang},
title = {{{Encoding Proofs in Dedukti: the case of Coq proofs}}},
nopages = {},
booktitle = {Preliminary Proceedings of the 1st International Workshop on Hammers for Type Theories (HaTT'16)},
year = {2016},
address = {Coimbra, Portugal},
url = {https://hal.inria.fr/hal-01330980},
pdf = {https://hal.inria.fr/hal-01330980/file/HaTT_2016_paper_3.pdf},
abstract = {A main ambition of the Inria project Dedukti is to serve as a common language for representing and type checking proof objects originating from other proof systems. Encoding these proof objects makes heavy use of the rewriting capabilities of LambdaPiModulo, the formal system on which Dedukti is based. So far, the proofs generated by two automatic proof systems, Zenon and iProver, have been encoded, and can therefore be read and checked by Dedukti. But Dedukti goes far beyond this so-called hammering technique of sending goals to automated provers. Proofs from HOL and Matita can be encoded as well. Some Coq?s proofs can be encoded already, when they do not use universe polymorphism. Our ambition here is to close this remaining gap. To this end, we describe a rewrite-based encoding in LambdaPiModulo of the Calculus of Constructions with a cumulative hierarchy of predicative universes above Prop, which is confluent on open terms.}
}
@inproceedings{ADJL-hor2016,
author = {Assaf, Ali and Dowek, Gilles and Jouannaud, Jean-Pierre and Liu, Jiaxiang},
title = {{{Untyped Confluence in Dependent Type Theories}}},
nopages = {},
booktitle = {Proceedings of the 8th International Workshop on Higher-Order Rewriting (HOR'16)},
year = {2016},
address = {Porto, Portugal},
url = {https://hal.inria.fr/hal-01330955},
pdf = {https://hal.inria.fr/hal-01330955/file/HOR_2016_paper.pdf},
abstract = {We investigate techniques based on van Oostrom's decreasing diagrams that reduce confluence proofs to the checking of critical pairs in the absence of termination properties, which are useful in dependent type calculi to prove confluence on untyped terms. These techniques are applied to a complex example originating from practice: a faithful encoding, in an extension of LF with rewrite rules on objects and types, of a subset of the calculus of inductive constructions with a cumulative hierarchy of predicative universes above Prop. The rules may be first-order or higher-order, plain or modulo, non-linear on the right or on the left. Variables which occur non-linearly in lefthand sides of rules must take their values in confined types: in our example, the natural numbers. The first-order rules are assumed to be terminating and confluent modulo some theory: in our example, associativity, commutativity and identity. Critical pairs involving higher-order rules must satisfy van Oostrom's decreasing diagram condition wrt their indexes taken as labels.}
}
@inproceedings{A-types2016,
address = {Novi Sad, Serbia},
volume = {97},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Ghilezan, Silvia and Ivetic, Jelena},
acronym = {{TYPES}'16},
booktitle = {{P}roceedings of the 22nd {I}nternational {C}onference on {T}ypes for {P}roofs and {P}rograms
({TYPES}'16)},
author = {Assaf, Ali and Burel, Guillaume and Cauderlier, Rapha{\"e}l and Delahaye, David and Dowek, Gilles and Dubois, Catherine and Gilbert, Fr{\'e}d{\'e}ric and Halmagrand, Pierre and Hermant, Olivier and Saillard, Ronan},
title = {{{Expressing theories in the {{\(\lambda\Pi\)}}-calculus modulo theory and in the Dedukti system}}},
year = {2016},
note = {To appear}
}
@unpublished{D-preprint2016,
title = {{Rules and derivations in an elementary logic course}},
author = {Dowek, Gilles},
note = {preprint},
year = {2016},
month = jan,
url = {https://hal.inria.fr/hal-01252124/},
pdf = {https://hal.inria.fr/hal-01252124/file/ttl.pdf},
abstract = {When teaching an elementary logic course to students who have a general scientific background but have never been exposed to logic, we have to face the problem that the notions of deduction rule and of derivation are completely new to them, and are related to nothing they already know, unlike, for instance, the notion of model, that can be seen as a generalization of the notion of algebraic structure. In this note, we defend the idea that one strategy to introduce these notions is to start with the notion of inductive definition [1]. Then, the notion of derivation comes naturally. We also defend the idea that derivations are pervasive in logic and that defining precisely this notion at an early stage is a good investment to later define other notions in proof theory, computability theory, automata theory, ... Finally, we defend the idea that to define the notion of derivation precisely, we need to distinguish two notions of derivation: labeled with elements and labeled with rule names. This approach has been taken in [2].}
}
@unpublished{AD-preprint2016,
title = {{What is the Planck constant the magnitude of?}},
author = {Arrighi, Pablo and Dowek, Gilles},
note = {preprint},
year = {2016},
month = dec,
url = {https://hal.inria.fr/hal-01421711},
pdf = {https://hal.inria.fr/hal-01421711/file/planck.pdf},
abstract = {The Planck constant is the minimal area of one bit.}
}
@inproceedings{CD-ictac16,
address = {Taipei, Taiwan},
month = oct,
volume = 9965,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Alves Sampaio, Cesar and Wang, Farn},
acronym = {{ICTAC}'16},
booktitle = {{P}roceedings of the 13th {I}nternational {C}olloquium on
{T}heoretical {A}spects of {C}omputing ({ICTAC}'16)},
author = {Cauderlier, Rapha{\"e}l and Dubois, Catherine},
title = {{{ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti}}},
pages = {459-468},
year = {2016},
pdf = {https://hal.inria.fr/hal-01420638/file/ICTAC_2016.pdf},
url = {https://hal.inria.fr/hal-01420638/},
abstract = {The programming environment FoCaLiZe allows the user to specify, implement, and prove programs with the help of the theorem prover Zenon. In the actual version, those proofs are verified by Coq. In this paper we propose to extend the FoCaLiZe compiler by a backend to the Dedukti language in order to benefit from Zenon Modulo, an extension of Zenon for Deduction modulo. By doing so, FoCaLiZe can benefit from a technique for finding and verifying proofs more quickly. The paper focuses mainly on the process that overcomes the lack of local pattern-matching and recursive definitions in Dedukti.}
}
@mastersthesis{m2-thire,
author = {Thir{\'e}, Fran{\c{c}}ois},
title = {Reverse engineering on arithmetic proofs},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2016},
month = aug,
url = {https://hal.inria.fr/hal-01424816},
pdf = {https://hal.inria.fr/hal-01424816/file/main.pdf},
note = {26~pages}
}
@phdthesis{ph-phd2016,
author = {Halmagrand, Pierre},
title = {{Automated Deduction and Proof Certification for the B Method}},
school = {{Conservatoire National Des Arts et M{\'e}tiers, Paris}},
type = {Th{\`e}se de doctorat},
year = 2016,
month = dec,
url = {https://hal.inria.fr/tel-01420460/}
}
@inproceedings{AD-dcm15,
address = {Cali, Colombia},
month = mar,
volume = 204,
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Mu\~noz, C\'esar A. and P\'erez, Jorge A.},
acronym = {{DCM}'15},
booktitle = {{P}roceedings of the 11th {I}nternational {W}orkshop on
{D}evelopments in {C}omputational {M}odels ({DCM}'15)},
author = {Arrighi, Pablo and Dowek, Gilles},
doi = {10.4204/EPTCS.204.1},
pages = {1-10},
title = {Free fall and cellular automata},
url = {https://hal.inria.fr/hal-01421712},
year = {2016},
abstract = {Three reasonable hypotheses lead to the thesis that physical phenomena can be described and simulated with cellular automata. In this work, we attempt to describe the motion of a particle upon which a constant force is applied, with a cellular automaton, in Newtonian physics, in Special Relativity, and in General Relativity. The results are very different for these three theories.}
}
@article{BGMS-toct16,
publisher = {ACM Press},
journal = {ACM Transactions on Computation Theory},
author = {Beame, Paul and Grosshans, Nathan and McKenzie, Pierre and Segoufin, Luc},
title = {Nondeterminism and An Abstract Formulation of {Ne\v{c}iporuk}'s Lower Bound Method},
volume = {9},
number = {1},
year = {2016},
pages = {5:1-5:34},
doi = {10.1145/3013516},
month = dec
}
@inproceedings{DLM-pnse16,
address = {Torun, Poland},
month = jun,
year = 2016,
volume = 1591,
series = {CEUR Workshop Proceedings},
publisher = {CEUR-WS.org},
editor = {Lawrence Cabac and Lars Michael Kristensen and Heiko R{\"o}lke:},
acronym = {{PNSE}'16},
booktitle = {{P}roceedings of the 10th {I}nternational {W}orkshop on {P}etri
{N}ets and {S}oftware {E}ngineering ({PNSE}'16)},
author = {Alban Linard and
Beno{\^{\i}}t Barbot and
Didier Buchs and
Maximilien Colange and
Cl{\'{e}}ment D{\'{e}}moulins and
Lom{-}Messan Hillah and
Alexis Martin},
title = {Layered Data: {A} Modular Formal Definition without Formalisms},
pages = {287-306},
url = {http://ceur-ws.org/Vol-1591/},
pdf = {http://ceur-ws.org/Vol-1591/paper19.pdf},
abstract = {Defining formalisms and models in a modular way is a painful task. Metamodeling tools and languages have usually not been created with this goal in mind. This article proposes a data structure, called layered data, that allows defining easily modular abstract syntax for for- malisms and models. It also shows its use through an exhaustive example. As a side effect, this article discusses the notion of formalism, and asserts that they do not exist as standalone objects, but rather as relations between models.}
}
This file was generated by bibtex2html 1.98.