@inproceedings{CB-post13,
address = {Rome, Italy},
month = mar,
year = 2013,
volume = {7796},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Basin, David and Mitchell, John},
acronym = {{POST}'13},
booktitle = {{P}roceedings of the 2nd {I}nternational {C}onference on
{P}rinciples of {S}ecurity and {T}rust
({POST}'13)},
author = {Cheval, Vincent and Blanchet, Bruno},
title = {Proving More Observational Equivalences with ProVerif},
pages = {226-246},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CB-post13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CB-post13.pdf},
doi = {10.1007/978-3-642-36830-1_12},
abstract = {This paper presents an extension of the automatic protocol
verifier ProVerif in order to prove more observational
equivalences. ProVerif can prove observational equivalence
between processes that have the same structure but differ by
the messages they contain. In order to extend the class of
equivalences that ProVerif handles, we extend the language
of terms by defining more functions (destructors) by rewrite
rules. In particular, we allow rewrite rules with
inequalities as side-conditions, so that we can express
tests {"}if then else{"} inside terms. Finally,
we provide an automatic procedure that translates a process
into an equivalent process that performs as many actions as
possible inside terms, to allow ProVerif to prove the
desired equivalence. These extensions have been implemented
in ProVerif and allow us to automatically prove anonymity in
the private authentication protocol by Abadi and Fournet.}
}
@inproceedings{CD-post13,
address = {Rome, Italy},
month = mar,
year = 2013,
volume = {7796},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Basin, David and Mitchell, John},
acronym = {{POST}'13},
booktitle = {{P}roceedings of the 2nd {I}nternational {C}onference on
{P}rinciples of {S}ecurity and {T}rust
({POST}'13)},
author = {Chr{\'e}tien, R{\'e}my and Delaune, St{\'e}phanie},
title = {Formal analysis of privacy for routing protocols in mobile ad~hoc networks},
pages = {1-20},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-post13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-post13.pdf},
doi = {10.1007/978-3-642-36830-1_1},
abstract = {Routing protocols aim at establishing a route between
distant nodes in ad hoc networks. Secured versions
of routing protocols have been proposed to provide
more guarantees on the resulting routes, and some of
them have been designed to protect the privacy of
the users. In this paper, we propose a framework for
analysing privacy-type properties for routing
protocols. We use a variant of the applied-pi
calculus as our basic modelling formalism. More
precisely, using the notion of equivalence between
traces, we formalise three security properties
related to privacy, namely indistinguishability,
unlinkability, and anonymity. We study the
relationship between these definitions and we
illustrate them using two versions of the ANODR
routing protocol.}
}
@article{BFHR-icomp13,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Bonnet, R{\'e}mi and Finkel, Alain and Haddad, Serge and
Rosa{-}Velardo, Fernando},
title = {Ordinal Theory for Expressiveness of Well-Structured
Transition Systems},
year = 2013,
month = mar,
volume = 224,
pages = {1-22},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHR-icomp12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHR-icomp12.pdf},
doi = {10.1016/j.ic.2012.11.003},
abstract = {We characterize the importance of resources (like counters,
channels, or alphabets) when measuring the expressiveness of
Well-Structured Transition Systems~(WSTS). We establish, for usual classes
of well partial orders, the equivalence between the existence of order
reflections (non-monotonic order embeddings) and the simulations with
respect to coverability languages. We show that the non-existence of order
reflections can be proved by the computation of order types. This allows
us to extend the current classification of WSTS, in particular solving
some open problems, and to unify the existing proofs.}
}
@article{BCHLR-tcs13,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {B{\'e}rard, B{\'e}atrice and Cassez, Franck and Haddad, Serge
and Lime, Didier and Roux, Olivier~H.},
title = {The Expressive Power of Time {P}etri Nets},
year = 2013,
month = feb,
volume = 474,
ftturenumber = {},
pages = {1-20},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCHLR-tcs12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCHLR-tcs12.pdf},
doi = {10.1016/j.tcs.2012.12.005},
abstract = {We investigate expressiveness questions for time Petri nets
(TPNs) and some their most usefull extensions. We first introduce
generalised time Petri nets (GTPNs) as an abstract model that encompasses
variants of TPNs such as self modifications and read, reset and inhibitor
arcs.\par
We give a syntactical translation from bounded GTPNs to timed automata
(TA) that generates isomorphic transition systems. We prove that the class
of bounded GTPNs is stricly less expressive than TA w.r.t. weak timed
bisimilarity. We prove that bounded GTPNs, bounded TPNs and TA are equally
expressive w.r.t. timed language acceptance. Finally, we characterise a
syntactical subclass of TA that is equally expressive to bounded GTPNs
{"}\`a~la Merlin{"} w.r.t. weak timed bisimilarity. These results provide
a unified comparison of the expressiveness of many variants of timed
models often used in practice. It leads to new important results for TPNs.
Among them are: 1-safe TPNs and bounded-TPNs are equally expressive;
\(\epsilon\)-transitions strictly increase the expressive power of TPNs;
self modifying nets as well as read, inhibitor and reset arcs do not add
expressiveness to bounded TPNs.}
}
@article{ABG-fmsd12,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Akshay, S. and Bollig, Benedikt and Gastin, Paul},
title = {Event-clock Message Passing Automata: A~Logical
Characterization and an Emptiness-Checking Algorithm},
year = 2013,
month = jun,
volume = 42,
number = {3},
pages = {262-300},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABG-fmsd12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABG-fmsd12.pdf},
doi = {10.1007/s10703-012-0179-8},
abstract = {We are interested in modeling behaviors and verifying
properties of systems in which time and concurrency play a crucial
role. We introduce a model of distributed automata which are
equipped with event clocks as in [Alur, Fix,
Henzinger. Event-clock automata: A~determinizable class of timed
automata. TCS 211(1-2):253-273, 1999.], which we call Event Clock
Message Passing Automata (ECMPA). To describe the behaviors of
such systems we use timed partial orders (modeled as message
sequence charts with timing).\par
Our first goal is to extend the classical
B{\"u}chi-Elgot-Trakhtenbrot equivalence to the timed and
distributed setting, by showing an equivalence between ECMPA and a
timed extension of monadic second-order (MSO) logic. We obtain
such a constructive equivalence in two different ways:
(1)~by~restricting the semantics by bounding the set of timed
partial orders (2)~by~restricting the timed MSO logic to its
existential fragment. We next consider the emptiness problem for
ECMPA, which asks if a given ECMPA has some valid timed
execution. In general this problem is undecidable and we show that
by considering only bounded timed executions, we can obtain
decidability. We do this by constructing a timed automaton which
accepts all bounded timed executions of the ECMPA and checking
emptiness of this timed automaton.}
}
@article{BCH-fi12,
publisher = {{IOS} Press},
journal = {Fundamenta Informaticae},
author = {Balaguer, Sandie and Chatain, {\relax Th}omas and Haar, Stefan},
title = {Building Occurrence Nets from Reveals Relations},
year = 2013,
month = may,
volume = 123,
number = 3,
pages = {245-272},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCH-fi12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCH-fi12.pdf},
doi = {10.3233/FI-2013-809},
abstract = {Occurrence nets are a well known partial order model for the
concurrent behavior of Petri nets. The causality and conflict relations
between events, which are explicitly represented in occurrence nets,
induce logical dependencies between event occurrences: the occurrence of
an event~\(e\) in a run implies that all its causal predecessors also
occur, and that no event in conflict with~\(e\) occurs. But these
structural relations do not express all the logical dependencies between
event occurrences in maximal runs: in particular, the occurrence of~\(e\)
in any maximal run may imply the occurrence of another event that is not a
causal predecessor of~\(e\), in that run. The \emph{reveals} relation has
been introduced to express this dependency between two events. Here we
generalize the reveals relation to express more general dependencies,
involving more than two events, and we introduce ERL logic to express them
as boolean formulas. Finally we answer the synthesis problem that arises:
given an ERL formula~\(\varphi\), is there an occurrence
net~\(\mathcal{N}\) such that \(\varphi\)~describes exactly the
dependencies between the events of~\(\mathcal{N}\)?}
}
@article{GS-tocl12,
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
author = {Gastin, Paul and Sznajder, Nathalie},
title = {Fair Synthesis for Asynchronous Distributed Systems},
nopages = {},
volume = 14,
number = {2:9},
month = jun,
year = 2013,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GS-tocl12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GS-tocl12.pdf},
doi = {10.1145/2480759.2480761},
abstract = {We study the synthesis problem in an asynchronous distributed
setting: a finite set of processes interact locally with an uncontrollable
environment and communicate with each other by sending signals---actions
controlled by a sender process and that are immediately received by the
target process. The fair synthesis problem is to come up with a local
strategy for each process such that the resulting fair behaviors of the
system meet a given specification. We consider external specifications
satisfying some natural closure properties related to the architecture. We
present this new setting for studying the fair synthesis problem for
distributed systems, and give decidability results for the subclass of
networks where communications happen through a strongly connected graph.
We claim that this framework for distributed synthesis is natural,
convenient and avoids most of the usual sources of undecidability for the
synthesis problem. Hence, it may open the way to a decidable theory of
distributed synthesis.}
}
@article{BS-fmsd2012,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Bertrand, Nathalie and Schnoebelen, {\relax Ph}ilippe},
title = {Computable fixpoints in well-structured symbolic model
checking},
pages = {233-267},
volume = 43,
number = 2,
month = oct,
year = 2013,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-fmsd12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-fmsd12.pdf},
doi = {10.1007/s10703-012-0168-y},
abstract = {We prove a general finite-time convergence theorem for fixpoint
expressions over a well-quasi-ordered set. This has immediate applications
for the verification of well-structured systems, where a main issue is the
computability of fixpoint expressions, and in particular for
game-theoretical properties and probabilistic systems where nesting and
alternation of least and greatest fixpoints are common.}
}
@incollection{HM-lncis433,
author = {Haar, Stefan and Masopust, Tom{\'a}{\v{s}}},
title = {Languages, Decidability, and Complexity},
booktitle = {Control of Discrete-Event Systems~-- Automata and {P}etri Net Perspectives},
editor = {Seatzu, Carla and Silva, Manuel and van Schuppen, Jan H.},
year = {2013},
pages = {23-43},
publisher = {Springer},
series = {Lecture Notes in Control and Information Sciences},
volume = 433,
doi = {10.1007/978-1-4471-4276-8_2},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HM-lncis433.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HM-lncis433.pdf}
}
@incollection{HS-lncis433,
author = {Haar, Stefan and Fabre, {\'E}ric},
title = {Diagnosis with {P}etri Net Unfoldings},
booktitle = {Control of Discrete-Event Systems~-- Automata and {P}etri Net Perspectives},
editor = {Seatzu, Carla and Silva, Manuel and van Schuppen, Jan H.},
year = {2013},
pages = {301-318},
publisher = {Springer},
series = {Lecture Notes in Control and Information Sciences},
volume = 433,
doi = {10.1007/978-1-4471-4276-8_15},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HS-lncis433.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HS-lncis433.pdf}
}
@article{AFS-fmsd12,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Andr{\'e}, {\'E}tienne and Fribourg, Laurent and Sproston,
Jeremy},
title = {An~Extension of the Inverse Method to Probabilistic Timed
Automata},
year = 2013,
month = apr,
volume = 42,
number = 2,
pages = {119-145},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AFS-fmsd12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AFS-fmsd12.pdf},
doi = {10.1007/s10703-012-0169-x},
abstract = {Probabilistic timed automata can be used to model systems in
which probabilistic and timing behaviour coexist. Verification of
probabilistic timed automata models is generally performed with regard to
a single reference valuation pi0 of the timing parameters. Given such a
parameter valuation, we present a method for obtaining automatically a
constraint~\(K_0\) on timing parameters for which the reachability
probabilities (1)~remain invariant and (2)~are equal to the reachability
probabilities for the reference valuation. The method relies on parametric
analysis of a non-probabilistic version of the probabilistic timed
automata model using the {"}inverse method{"}. The method presents the
following advantages. First, since \(K_0\) corresponds to a dense domain
around pi0 on which the system behaves uniformly, it gives us a measure of
robustness of the system. Second, it allows us to obtain a valuation
satisfying \(K_0\) which is as small as possible while preserving
reachability probabilities, thus making the probabilistic analysis of the
system easier and faster in practice. We provide examples of the
application of our technique to models of randomized protocols, and
introduce an extension of the method allowing the generation of a
{"}probabilistic cartography{"} of a system.}
}
@article{BCD-tocl12,
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
author = {Baudet, Mathieu and Cortier, V{\'e}ronique and Delaune, St{\'e}phanie},
title = {{YAPA}: A~generic tool for computing intruder knowledge},
year = 2013,
month = feb,
nopages = {},
number = {1:4},
volume = 14,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCD-tocl12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCD-tocl12.pdf},
doi = {10.1145/2422085.2422089},
abstract = {Reasoning about the knowledge of an attacker is a
necessary step in many formal analyses of security
protocols. In the framework of the applied pi
calculus, as in similar languages based on
equational logics, knowledge is typically expressed
by two relations: deducibility and static
equivalence. Several decision procedures have been
proposed for these relations under a variety of
equational theories. However, each theory has its
particular algorithm, and none has been implemented
so far. \par We provide a generic procedure for
deducibility and static equivalence that takes as
input any convergent rewrite system. We show that
our algorithm covers most of the existing decision
procedures for convergent theories. We also provide
an efficient implementation, and compare it briefly
with the tools ProVerif and KiSs.}
}
@book{JGL-topology,
author = {Goubault{-}Larrecq, Jean},
title = {Non-{H}ausdorff Topology and Domain Theory---Selected Topics
in Point-Set Topology},
publisher = {Cambridge University Press},
series = {New Mathematical Monographs},
volume = {22},
year = {2013},
month = mar,
url = {http://www.cambridge.org/9781107034136},
isbn = {9781107034136}
}
@inproceedings{GLS-rr13,
address = {Mannheim, Germany},
month = jul,
year = 2013,
volume = 7994,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Faber, Wolfgang and Lembo, Domenico},
acronym = {{WRRS}'13},
booktitle = {{P}roceedings of the 7th {I}nternational {C}onference on
{W}eb {R}easoning and {R}ule {S}ystems ({WRRS}'13)},
author = {Gheerbrant, Am{\'e}lie and Libkin, Leonid and Sirangelo,
Cristina},
affiliaton = {Scotland, University of Edinburgh, School of Informatics and Scotland, University of Edinburgh, School of Informatics and France, ENS Cachan \& CNRS \& INRIA, LSV[Dahu]},
title = {Reasoning About Pattern-Based {XML} Queries},
pages = {4-18},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GLS-rr13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLS-rr13.pdf},
doi = {10.1007/978-3-642-39666-3_2},
abstract = {We survey results about static analysis of pattern-based queries
over XML documents. These queries are analogs of conjunctive queries,
their unions and Boolean combinations, in which tree patterns play the
role of atomic formulae. As in the relational case, they can be viewed as
both queries and incomplete documents, and thus static analysis problems
can also be viewed as finding certain answers of queries over such
documents. We look at satisfiability of patterns under schemas,
containment of queries for various features of XML used in queries,
finding certain answers, and applications of pattern-based queries in
reasoning about schema mappings for data exchange.}
}
@incollection{AV-buneman13,
noaddress = {},
month = sep,
year = 2013,
volume = 8000,
series = {Lecture Notes in Computer Science},
editor = {Tannen, Val and Wong, Limsoon and Libkin, Leonid and
Fan, Wenfei and Tan, Wang-Chiew and Fourman, Michael},
publisher = {Springer},
booktitle = {{I}n~{S}earch of {E}legance in the {T}heory and {P}ractice of
{C}omputation~-- {E}ssays {D}edicated to {P}eter~{B}uneman},
author = {Abiteboul, Serge and Vianu, Victor},
title = {Models for Data-Centric Workflows},
pages = {1-12},
doi = {10.1007/978-3-642-41660-6_1},
abstract = {We present two models for data-centric workflows: the first
based on business artifacts and the second on Active XML. We then compare
the two models and argue that Active XML is strictly more expressive,
based on a natural semantics and choice of observables. Finally, we
mention several verification results for the two models.}
}
@inproceedings{AAMST-sigmod13,
address = {New~York, New~York, USA},
month = jun,
year = 2013,
publisher = {ACM Press},
editor = {Ross, Kenneth A. and Srivastava, Divesh and Papadias, Dimitris},
acronym = {{SIGMOD}'13},
booktitle = {{P}roceedings of the {ACM} {SIGMOD} {I}nternaitonal
{C}onference on {M}anagement of {D}ata ({SIGMOD}'13)},
author = {Abiteboul, Serge and Antoine, {\'E}milien and Miklau,
Gerome and Stoyanovich, Julia and Testard, Jules},
title = {Rule-based application development using Webdamlog},
pages = {965-968},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AAMST-sigmod13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AAMST-sigmod13.pdf},
doi = {10.1145/2463676.2465251},
abstract = {We present the WebdamLog system for managing distributed data on
the Web in a peer-to-peer manner. We demonstrate the main features of the
system through an application called Wepic for sharing pictures between
attendees of the sigmod conference. Using Wepic, the attendees will be
able to share, download, rate and annotate pictures in a highly
decentralized manner. We show how WebdamLog handles heterogeneity of the
devices and services used to share data in such a Web setting. We exhibit
the simple rules that define the Wepic application and show how to easily
modify the Wepic application.}
}
@inproceedings{BD-csr13,
address = {Ekaterinburg, Russia},
month = jun,
year = 2013,
volume = {7913},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Bulatov, Andrei A. and Shur, Arseny M.},
acronym = {{CSR}'13},
booktitle = {{P}roceedings of the 8th {I}nternational {C}omputer {S}cience
{S}ymposium in {R}ussia ({CSR}'13)},
author = {Bansal, Kshitij and Demri, St{\'e}phane},
title = {Model-checking bounded multi-pushdown systems},
pages = {405-417},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BD-csr13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BD-csr13.pdf},
doi = {10.1007/978-3-642-38536-0_35},
abstract = {We provide complexity characterizations of model checking
multi-pushdown systems. We consider three standard notions for
boundedness: context boundedness, phase boundedness and stack ordering.
The logical formalism is a linear-time temporal logic extending well-known
logic \texttt{CaRet} but dedicated to multi-pushdown systems in which abstract
operators are parameterized by stacks. We show that the problem is
ExpTime-complete for context-bounded runs and unary encoding of the number
of context switches; we also prove that the problem is 2ExpTime-complete
for phase-bounded runs and unary encoding of the number of phase switches.
In both cases, the value~\(k\) is given as an input, which makes a
substantial difference in the complexity.}
}
@misc{cassting-D41,
author = {Markey, Nicolas and Larsen, Kim G. and Skou, Arne and Lux, Daniel
and Rozenkilde, Jesper and Pedersen, Keld L. and
S{\o}rensen, Susanne M.},
title = {Description of case studies},
howpublished = {Cassting deliverable~D4.1 (FP7-ICT-601148)},
month = oct,
year = {2013},
note = {19~pages},
type = {Contract Report},
nourlnote = {confidentiel}
}
@misc{cassting-D51,
author = {Valette, Sophie and Markey, Nicolas},
title = {Cassting website},
howpublished = {Cassting deliverable~D6.1 (FP7-ICT-601148)},
month = jun,
year = {2013},
note = {10~pages},
type = {Contract Report},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/cassting-d51.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/cassting-d51.pdf}
}
@misc{cassting-D61,
author = {Valette, Sophie and Markey, Nicolas},
title = {Minutes of the Kick-Off Meeting},
howpublished = {Cassting deliverable~D6.1 (FP7-ICT-601148)},
month = apr,
year = {2013},
note = {9~pages},
type = {Contract Report},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/cassting-d61.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/cassting-d61.pdf}
}
@phdthesis{chatain-HDR13,
author = {Chatain, {\relax Th}omas},
title = {Concurrency in Real-Time Distributed Systems, from Unfoldings
to Implementability},
year = 2013,
month = dec,
type = {M{\'e}moire d'habilitation},
school = {{\'E}cole Normale Sup{\'e}rieure de Cachan, France},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/hdr-chatain13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/hdr-chatain13.pdf}
}
@phdthesis{crodriguez-phd2013,
author = {Rodr{\'\i}guez, C{\'e}sar},
title = {Verification Based on Unfoldings of {P}etri Nets with Read Arcs},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2013,
month = dec,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/cr-phd13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/cr-phd13.pdf}
}
@misc{impro-D31,
author = {B{\'e}rard, B{\'e}atrice and Bouyer, Patricia and Larsen, Kim G. and
Markey, Nicolas and Mullins, John and Sankur, Ocan and Sassolas,
Mathieu and Thrane, Claus},
title = {Measuring the robustness},
howpublished = {Deliverable ImpRo~3.1, (ANR-10-BLAN-0317)},
month = jan,
year = {2013},
note = {59~pages},
type = {Contract Report},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d31.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d31.pdf}
}
@misc{impro-D51,
author = {Bouyer, Patricia and Faucou, S{\'e}bastien and Haar, Stefan and
Jovanivi{\'c}, Aleksandra and Lime, Didier and Markey, Nicolas and
Roux, Olivier H. and Sankur, Ocan},
title = {Control tasks for Timed System; Robustness issues},
howpublished = {Deliverable ImpRo~5.1, (ANR-10-BLAN-0317)},
month = jan,
year = {2013},
note = {34~pages},
type = {Contract Report},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d51.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d51.pdf}
}
@phdthesis{schwoon-HDR13,
author = {Schwoon, Stefan},
title = {Efficient verification of sequential and concurrent systems},
year = 2013,
month = dec,
type = {M{\'e}moire d'habilitation},
school = {{\'E}cole Normale Sup{\'e}rieure de Cachan, France},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/hdr-schwoon13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/hdr-schwoon13.pdf}
}
@phdthesis{eantoine-phd2013,
author = {Antoine, {\'E}milien},
title = {Distributed data management with a declarative rule-based language: \emph{Webdamlog}},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2013,
month = dec,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/eantoine-phd13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/eantoine-phd13.pdf}
}
@article{CS-lmcs13,
journal = {Logical Methods in Computer Science},
author = {ten~Cate, Balder and Segoufin, Luc},
title = {Unary negation},
volume = 9,
number = {3:25},
month = sep,
year = 2013,
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-lmcs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-lmcs13.pdf},
doi = {10.2168/LMCS-9(3:25)2013},
abstract = {We study fragments of first-order logic and of least fixed point
logic that allow only unary negation: negation of formulas with at most
one free variable. These logics generalize many interesting known
formalisms, including modal logic and the \(\mu\)-calculus, as well as
conjunctive queries and monadic Datalog. We show that satisfiability and
finite satisfiability are decidable for both fragments, and we pinpoint
the complexity of satisfiability, finite satisfiability, and model
checking. We also show that the unary negation fragment of first-order
logic is model-theoretically very well behaved. In particular, it enjoys
Craig Interpolation and the Projective Beth Property.}
}
@inproceedings{BC-fossacs13,
address = {Rome, Italy},
month = mar,
year = 2013,
volume = {7794},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Pfenning, Frank},
acronym = {{FoSSaCS}'13},
booktitle = {{P}roceedings of the 16th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'13)},
author = {Bonnet, R{\'e}mi and Chadha, Rohit},
title = {Bounded Context-Switching and Reentrant Locking},
pages = {65-80},
doi = {10.1007/978-3-642-37075-5_5},
abstract = {Reentrant locking is a \emph{recursive locking} mechanism which allows
a thread in a multi-threaded program to acquire the reentrant lock
multiple times. The thread must release this lock an equal number of times
before another thread can acquire this lock. We consider the control state
reachability problem for recursive multi-threaded programs synchronizing
via a finite number of reentrant locks. Such programs can be abstracted as
multi-pushdown systems with a finite number of counters. The pushdown
stacks model the call stacks of the threads and the counters model the
reentrant locks. The control state reachability problem is already
undecidable for non-reentrant locks. As a consequence, for non-reentrant
locks, under-approximation techniques which restrict the search space have
gained traction. One popular technique is to limit the number of context
switches. Our main result is that the problem of checking whether a
control state is reachable within a bounded number of context switches is
decidable for recursive multi-threaded programs synchronizing via a finite
number of reentrant locks if we restrict the lock-usage to contextual
locking: a release of an instance of reentrant lock can only occur if the
instance was acquired before in the same procedure and each instance of a
reentrant lock acquired in a procedure call must be released before the
procedure returns. The decidability is obtained by a reduction to the
reachability problem of Vector Addition Systems with States~(VASS).}
}
@article{BCMV-lmcs13,
journal = {Logical Methods in Computer Science},
author = {Bonnet, R{\'e}mi and Chadha, Rohit and Madhusudan, P. and
Viswanathan, Mahesh},
title = {Reachability under contextual locking},
volume = 9,
number = {3:21},
month = sep,
year = 2013,
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCMV-lmcs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCMV-lmcs13.pdf},
doi = {10.2168/LMCS-9(3:21)2013},
abstract = {The pairwise reachability problem for a multi-threaded program
asks, given control locations in two threads, whether they can be
simultaneously reached in an execution of the program. The problem is
important for static analysis and is used to detect statements that are
concurrently enabled. This problem is in general undecidable even when
data is abstracted and when the threads (with recursion) synchronize only
using a finite set of locks. Popular programming paradigms that limit the
lock usage patterns have been identified under which the pairwise
reachability problem becomes decidable. In this paper, we consider a new
natural programming paradigm, called contextual locking, which ties the
lock usage to calling patterns in each thread: we assume that locks are
released in the same context that they were acquired and that every lock
acquired by a thread in a procedure call is released before the procedure
returns. Our main result is that the pairwise reachability problem is
polynomial-time decidable for this new programming paradigm as well. The
problem becomes undecidable if the locks are reentrant; reentrant locking
is a recursive locking mechanism which allows a thread in a multi-threaded
program to acquire the reentrant lock multiple times.}
}
@proceedings{BF-formats2013,
title = {{P}roceedings of the 11th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'13)},
booktitle = {{P}roceedings of the 11th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'13)},
acronym = {{FORMATS}'13},
editor = {Braberman, V{\'\i}ctor and Fribourg, Laurent},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 8053,
url = {http://link.springer.com/978-3-642-40228-9},
year = 2013,
month = aug,
address = {Buenos Aires, Argentina}
}
@article{BC-lmcs13,
journal = {Logical Methods in Computer Science},
author = {Balaguer, Sandie and Chatain, {\relax Th}omas},
title = {Avoiding Shared Clocks in Networks of Timed Automata},
volume = 9,
number = {4:13},
nopages = {},
year = 2013,
month = nov,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BC-lmcs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BC-lmcs13.pdf},
doi = {10.2168/LMCS-9(4:13)2013},
abstract = {Networks of timed automata~(NTA) are widely used to model
distributed real-time systems. Quite often in the literature, the automata
are allowed to share clocks. This is a problem when one considers
implementing such model in a distributed architecture, since reading
clocks a priori requires communications which are not explicitly described
in the model. We focus on the following question: given a NTA \(A_{1}
\parallel A_{2}\) where \(A_{2}\) reads some clocks reset by~\(A_{1}\),
does there exist a NTA \(A'_{1} \parallel A'_{2}\) without shared clocks
with the same behavior as the initial NTA? For this, we allow the automata
to exchange information during synchronizations only. We discuss a
formalization of the problem and give a criterion using the notion of
contextual timed transition system, which represents the behavior
of~\(A_{2}\) when in parallel with~\(A_{1}\). Finally, we effectively
build \(A'_{1} \parallel A'_{2}\) when it exists.}
}
@article{CD-pourlascience13,
publisher = {Belin},
journal = {Pour La Science},
author = {Chr{\'e}tien, R{\'e}my and Delaune, St{\'e}phanie},
title = {La protection des informations sensibles},
volume = {433},
month = nov,
year = 2013,
pages = {70-77},
url = {http://www.pourlascience.fr/ewb_pages/a/article-la-protection-des-informations-sensibles-32228.php}
}
@phdthesis{monmege-phd2013,
author = {Monmege, Benjamin},
title = {Sp{\'e}cification et v{\'e}rification de propri{\'e}t{\'e}s
quantitatives~: expressions, logiques, et automates},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2013,
month = oct,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/monmege-phd13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/monmege-phd13.pdf}
}
@book{FS-book13,
author = {Fribourg, Laurent and Soulat, Romain},
title = {Control of Switching Systems by Invariance Analysis: Application to Power Electronics},
publisher = {Wiley-ISTE},
year = 2013,
month = jul,
isbn = {9781848216068},
note = {144~pages},
url = {http://www.iste.co.uk/index.php?f=a&ACTION=View&id=684},
abstract = {This book presents correct-by-design control techniques for
switching systems, using different methods of stability analysis.
Switching systems are increasingly used in the electronics and mechanical
industries; in power electronics and the automotive industry, for example.
This is due to their flexibility and simplicity in accurately controlling
industrial mechanisms. By adopting appropriate control rules, we can steer
a switching system to a region centered at a desired equilibrium point,
while avoiding {"}unsafe{"} regions of parameter saturation.\par
The authors explain various correct-by-design methods for control
synthesis, using different methods of stability and invariance analysis.
They also provide several applications of these methods to industrial
examples of power electronics.}
}
@inproceedings{BL-ewili13,
address = {Toulouse, France},
month = aug,
year = 2013,
noeditor = {},
acronym = {{EW}i{L}i'13},
booktitle = {{P}roceedings of the 3rd {E}mbedded {O}perating {S}ystems
{W}orkshop ({EW}i{L}i'13)},
author = {Benedetto, Salvatore and Lipari, Giuseppe},
title = {{{ADOK}: A~Minimal Object Oriented Real-Time Operating System in~{C++}}},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BL-ewili13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BL-ewili13.pdf},
abstract = {Most embedded software is currently developed using the C
programming language, even though its low level of abstraction requires a
lot of effort to the programmer. The C++ language is a better choice
because: it raises the level of abstraction; it is strongly typed, so it
prevents many common programming mistakes; it can be made as efficient as
C through fine-grained customisation of memory mechanisms; it can be
easily adapted to domain-specific needs. In addition, recent compilers
have grown in maturity and performance, and the new standard
considerably improves the language by introducing new concepts and an
easier syntax.\par
In this paper we present ADOK, a minimal Real-Time Operating System
entirely written in C++ with the exception of a few lines of assembler
code. It directly offers a C++ interface to the developer, and it provides
a flexible scheduling framework which allows the developer to customise
the scheduling to its needs. In particular, we implement a two-level
scheduler based on Earliest Deadline First, the Stack Resource Policy
protocol for sharing resources and support for mode changes. We
demonstrate through examples and a small case-study that ADOK can
substantially improve productivity without sacrificing on performance.}
}
@inproceedings{BLBL-iceac13,
address = {Istanbul, Turkey},
month = dec,
year = 2013,
publisher = {{IEEE} Circuits and Systems Society},
noeditor = {},
acronym = {{ICEAC}'13},
booktitle = {{P}roceedings of the 4th {I}nternational {C}onference on
{E}nergy-{A}ware {C}omputing {S}ystems and {A}pplications ({ICEAC}'14),},
author = {Bambagini, Mario and Lelli, Juri and Buttazzo, Giorgio and Lipari, Giuseppe},
title = {On the Energy-Aware Partitioning of Real-Time Tasks on Homogeneous
Multi-Processor Systems},
pages = {69-74},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BLBL-iceac13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BLBL-iceac13.pdf},
doi = {10.1109/ICEAC.2013.6737640},
abstract = {In high-performance computing systems, efficient energy
management is a key feature for keeping energy bills low and avoiding
thermal dissipation problems, as well as for controlling the application
performance. This paper considers the problem of partitioning and
scheduling a set of real-time tasks on a realistic hardware platform
consisting of a number of homogeneous processors. Several well-known
heuristics are compared to identify the approach that better reduces the
overall energy consumption of the entire system. Despite the actual state
of art, the approach which minimizes the number of active cores is the
most energy efficient.}
}
@inproceedings{PLML-rtlws2013,
address = {Lugano-Manno, Switzerland},
month = oct,
year = 2013,
publisher = {Open Source Automation Development Lab (OSADL)},
noeditor = {},
acronym = {{RTLWS}'13},
booktitle = {{P}roceedings of the 15th {R}eal-{T}ime {L}inux {W}orkshop ({RTLWS}'13)},
author = {Parri, Andrea and Lelli, Juri and Marinoni, Mauro and Lipari,
Giuseppe},
title = {Design and Implementation of the Multiprocessor Bandwidth
Inheritance Protocol on {L}inux},
oldtitle = {An~implementation of the Bandwidth Inheritance Protocol in the {L}inux Kernel},
pages = {41-54},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/PLML-rtlws13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PLML-rtlws13.pdf},
abstract = {The Resource Reservation (RR) framework has been proven very
effective in the joint scheduling of hard real time and soft real time
application in Open Systems. A fundamental problem in this context
concerns the extension of the Resource Reservation approach to systems
where tasks interact through shared resources.\par
The Bandwidth Inheritance (BWI) protocol was first proposed in
[Lamastra~G., Lipari~G., Abeni~L.~(2001). A~bandwidth inheritance
algorithm for real-time task synchronization in open systems. In:~Proc.
22nd IEEE Real-Time Systems Symposium] to preserve Bandwidth Isolation
between independent groups of tasks, and to enable a schedulability
analysis for hard real time tasks.\par
In this paper, we present the first implementation of the BWI protocol
within the Linux kernel. We describe the protocol, the way it has been
implemented in Linux, and we report some early experiments to measure its
overhead. Our work is based on the SCHED\_DEADLINE patch, a scheduling
class for the Linux kernel that provides Resource Reservation using the
Constant Bandwidth Server algorithm. The BWI implementation extends
Linux's current implementation of the Priority Inheritance protocol,
without affecting past design decisions. Our implementation is neutral to
the underlying scheduling scheme and can be adopted in global, clustered
and partitioned scheduling.\par
Results show agreement with theoretical analysis, and
performance{\slash}overheads comparable with the current implementation of
Priority Inheritance in Linux.\par
The work presented here has practical implications for applications
running on Linux with SCHED\_DEADLINE scheduling policy and share resources
through mutex semaphores. In fact, the protocol guarantees temporal
isolation between non-interacting threads, hence real-time guarantees are
possible even where no a-priori information about tasks' scheduling
parameters are available.}
}
@inproceedings{LGBB-burns13,
address = {York, UK},
month = mar,
year = 2013,
editor = {Audsley, Neil and Baruah, Sanjoy},
publisher = {CreateSpace Independent Publishing Platform},
booktitle = {Real-Time Sytems: the past, the present, and the future~--
{P}roceedings of a conference organized in celebration of
{P}rofessor {A}lan~{B}urns' sixtieth birthday},
author = {Lipari, Giuseppe and George, Laurent and Bini, Enrico and
Bertogna, Marko},
title = {On the Average Complexity of the Processor Demand Analysis for
Earliest Deadline Scheduling},
pages = {75-86},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LGBB-burns13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LGBB-burns13.pdf},
abstract = {Schedulability analysis of a set of sporadic tasks scheduled by
EDF on a single processor system is a well known and solved problem: the
Processor Demand Analysis is a necessary and sufficient test for EDF with
pseudo-polynomial complexity. Over the years, many researchers have tried
to find efficient methods for reducing the average-case running time of
this test. The problem becomes relevant when doing sensitivity analysis of
the worst-case execution times of the tasks: the number of constraints to
check is directly linked to the complexity of the analysis. In this paper
we describe the problem and present some known facts, with the aim of
summarising the state of the art and stimulate research in this
direction.}
}
@inproceedings{LB-burns13,
address = {York, UK},
month = mar,
year = 2013,
editor = {Audsley, Neil and Baruah, Sanjoy},
publisher = {CreateSpace Independent Publishing Platform},
booktitle = {Real-Time Sytems: the past, the present, and the future~--
{P}roceedings of a conference organized in celebration of
{P}rofessor {A}lan~{B}urns' sixtieth birthday},
author = {Lipari, Giuseppe and Buttazzo, Giorgio},
title = {{Resource reservation for Mixed Criticality Systems}},
pages = {60-74},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LB-burns13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LB-burns13.pdf},
abstract = {This paper presents a reservation-based approach to schedule
mixed criticality systems in a way that guarantees the schedulability of
high-criticality tasks independently of the behaviour of low-criticality
tasks. Two key ideas are presented: first, to reduce the system
uncertainty and advance the time at which a high-criticality task reveals
its actual execution time, the initial portion of its code is handled by a
dedicated server with a bandwidth reserved for the worst-case, but with a
shorter deadline; second, to avoid the pessimism related to off-line
budget allocation, an efficient reclaiming mechanism, namely the GRUB
algorithm, is used to exploit the budget left by high-criticality tasks in
favor of those low-criticality tasks that can still complete within their
deadline.}
}
@inproceedings{SSLAF-ftscs13,
address = {Queenstown, New Zealand},
month = oct,
year = 2013,
editor = {Artho, Cyrille and {\"O}lveczky, Peter Csaba},
acronym = {{FTSCS}'13},
booktitle = {{P}reproceedings of the 2nd {I}nternational {W}orkshop on
{F}ormal {T}echniques for {S}afety-{C}ritical {S}ystems ({FTSCS}'13)},
author = {Sun, Youcheng and Soulat, Romain and Lipari, Giuseppe and
Andr{\'e}, {\'E}tienne and Fribourg, Laurent},
title = {Parametric Schedulability Analysis of Fixed Priority Real-Time
Distributed Systems},
pages = {179-194},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SSLAF-ftscs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SSLAF-ftscs13.pdf},
abstract = {In this paper, we address the problem of parametric
schedulability analysis of distributed real-time systems scheduled by
fixed priority. We propose two different approaches to parametric
analysis. The first one is a novel analytic technique that extends
single-processor sensitivity analysis to the case of distributed systems.
The second approach is based on model checking of Parametric Stopwatch
Automata~(PSA): we~generate a PSA model from a high-level description of
the system, and then we apply the Inverse Method to obtain all possible
behaviours of the system. Both techniques have been implemented in two
software tools, and they have been compared with classical holistic
analysis on two meaningful test cases. The results show that the analytic
method provides results similar to classical holistic analysis in a very
efficient way, whereas the PSA approach is slower but covers the entire
space of solutions.}
}
@inproceedings{BL-etfa13,
address = {Cagliari, Italy},
month = sep,
year = 2013,
publisher = {{IEEE} Industrial Electronics Society},
noeditor = {},
acronym = {{ETFA}'13},
booktitle = {{P}roceedings of the 18th {IEEE} {I}nternational
{C}onference on {E}merging {T}echnologies and {F}actory
{A}utomation ({ETFA}'13)},
author = {Buttazzo, Giorgio and Lipari, Giuseppe},
title = {Ptask: An~Educational {C}~Library for Programming Real-Time Systems on Linux},
nopages = {},
doi = {10.1109/ETFA.2013.6648001},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BL-etfa13.pdf},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BL-etfa13.pdf},
abstract = {When learning real-time programming, the novice is faced with
many technical difficulties due to low-level C libraries that require
considerable programming effort even for implementing a simple periodic
task. For example, the POSIX Real-Time standard only provides a low level
notion of thread, hence programmers usually build higher level code on top
of the POSIX API, every time re-inventing the wheel.\par
In this paper we present a simple C library that simplifies real-time
programming in Linux by hiding low-level details of task creation,
allocation and synchronization, and provides utilities for more high-level
functionalities, like support for mode-change and adaptive systems. The
library is released as open-source and it is currently being employed to
teach real-time programming in university courses in embedded systems.}
}
@phdthesis{brochenin-phd2013,
author = {Brochenin, R{\'e}mi},
title = {Separation Logic: Expressiveness, Complexity, Temporal Extension},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2013,
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/brochenin-phd13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/brochenin-phd13.pdf}
}
@phdthesis{kazana-phd2013,
author = {Kazana, Wojciech},
title = {Query Evaluation with Constant Delay},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2013,
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/kazana-phd13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/kazana-phd13.pdf}
}
@inproceedings{HHMS-fsttcs13,
address = {Guwahati, India},
month = dec,
year = 2013,
volume = {24},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Seth, Anil and Vishnoi, Nisheeth},
acronym = {{FSTTCS}'13},
booktitle = {{P}roceedings of the 33rd {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'13)},
author = {Haar, Stefan and Haddad, Serge and Melliti, Tarek and Schwoon,
Stefan},
title = {Optimal Constructions for Active Diagnosis},
pages = {527-539},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HHMS13-fsttcs.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HHMS13-fsttcs.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2013.527},
abstract = {The task of diagnosis consists in detecting, without ambiguity,
occurrence of faults in a partially observed system. Depending on the
degree of observability, a discrete event system may be diagnosable or
not. Active diagnosis aims at controlling the system in order to make it
diagnosable. Solutions have already been proposed for the active diagnosis
problem, but their complexity remains to be improved. We solve here the
active diagnosability decision problem and the active diagnoser synthesis
problem, proving that (1)~our procedures are optimal w.r.t. to
computational complexity, and (2)~the memory required for the active
diagnoser produced by the synthesis is minimal. Furthermore, focusing on
the minimal delay before detection, we establish that the memory required
for any active diagnoser achieving this delay may be highly greater than
the previous one. So we refine our construction to build with the same
complexity and memory requirement an active diagnoser that realizes a
delay bounded by twice the minimal delay.}
}
@inproceedings{EJS-fsttcs13,
address = {Guwahati, India},
month = dec,
year = 2013,
volume = {24},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Seth, Anil and Vishnoi, Nisheeth},
acronym = {{FSTTCS}'13},
booktitle = {{P}roceedings of the 33rd {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'13)},
author = {Esparza, Javier and Jezequel, Lo{\"\i}g and Schwoon, Stefan},
title = {Computation of summaries using net unfoldings},
pages = {225-236},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/EJS-fsttcs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/EJS-fsttcs13.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2013.225},
abstract = {We study the following summarization problem: given a parallel
composition \(A = A_1\Vert\cdots\Vert A_n\) of labelled transition systems
communicating with the environment through a distinguished component
\(A_i\), efficiently compute a summary~\(S_i\) such that \(E\Vert A\) and
\(E\Vert S_i\) are trace-equivalent for every environment~\(E\). While \(S_i\)
can be computed using elementary automata theory, the resulting algorithm
suffers from the state-explosion problem. We present a new, simple but
subtle algorithm based on net unfoldings, a partial-order semantics, give
some experimental results using an implementation on top of Mole, and show
that our algorithm can handle divergences and compute weighted summaries
with minor modifications.}
}
@inproceedings{RS-fsfma13,
address = {Singapore},
month = jul,
year = 2013,
volume = 31,
series = {Open Access Series in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Choppy, {\relax Ch}ristine and Sun, Jun},
acronym = {{FSFMA}'13},
booktitle = {{P}roceedings of the 1st {F}rench-{S}ingaporean {W}orkshop
on {F}ormal {M}ethods and {A}pplications ({FSFMA}'13)},
author = {Rodr{\'\i}guez, C{\'e}sar and Schwoon, Stefan},
title = {An Improved Construction of {P}etri Net Unfoldings},
pages = {47-52},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/RS-fsfma13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RS-fsfma13.pdf},
doi = {10.4230/OASIcs.FSFMA.2013.47},
abstract = {Petri nets are a well-known model language for concurrent
systems. The unfolding of a Petri net is an acyclic net bisimilar to the
original one. Because it is acyclic, it admits simpler decision problems
though it is in general larger than the net. In this paper, we revisit the
problem of efficiently constructing an unfolding. We propose a new method
that avoids computing the concurrency relation and therefore uses less
memory than some other methods but still represents a good time-space
tradeoff. We implemented the approach and report on experiments.}
}
@article{HMY-jocs13,
publisher = {Elsevier Science Publishers},
journal = {Journal of Computational Science},
author = {Haddad, Serge and Mokdad, Lynda and Youcef, Samir},
title = {Bounding models families for performance evaluation in composite
Web services},
volume = {4},
number = {4},
year = {2013},
pages = {232-241},
month = jul,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HMY-jocs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HMY-jocs13.pdf},
doi = {10.1016/j.jocs.2011.11.003},
abstract = {One challenge of composite Web service architectures is the
guarantee of the Quality of Service~(QoS). Performance evaluation of these
architectures is essential but complex due to synchronizations inside the
orchestration of services. We propose methods to automatically derive from
the original model a family of bounding models for the composite Web
response time. These models allow to find the appropriate trade-off
between accuracy of the bounds and the computational complexity. The
numerical results show the interest of our approach w.r.t. complexity and
accuracy of the response time bounds.}
}
@techreport{rr-lsv-13-13,
author = {Hirschi, Lucca},
title = {R{\'e}duction d'entrelacements pour l'{\'e}quivalence de traces},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2013},
month = sep,
type = {Research Report},
number = {LSV-13-13},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2013-13.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2013-13.pdf},
versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2013-13-v1.pdf, 20130910},
note = {22~pages},
abstract = {La trace \'equivalence permet notamment de mod\'eliser l'anonymat de
protocoles cryptographiques. Cette propri\'et\'e est d\'ecidable pour de
nombreuses classes de protocoles et quelques outils permettent de la
prouver automatiquement. Mais malheureusement, tous ces outils sont tr\`es
lents et peu de protocoles r\'eellement int\'eressants peuvent \^etre analys\'es
dans un temps raisonnable. Ces outils doivent r\'ealiser un parcours
exhaustif des traces (symboliques) possibles. Mais le parall\`ele introduit
de nombreux entrelacements dont un grand nombre sont peu pertinents. Cette
explosion combinatoire est une des causes de cette inefficacit\'e.\par
Une optimisation dont l'id\'ee est emprunt\'ee \`a la POR (Partial Order
Reduction) permet de r\'eduire significativement l'espace de recherche en
reconnaissant certaines redondances entre les traces. Elle a \'et\'e
d\'evelopp\'ee dans le cas des propri\'et\'es d'accessibilit\'e.
L'objectif est de l'adapter au cas de l'\'equivalence, de l'automatiser,
d'augmenter son champ d'action et de l'introduire dans un outil
existant.}
}
@inproceedings{BMS-rp13,
address = {Uppsala, Sweden},
month = sep,
year = 2013,
volume = {8169},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abdulla, Parosh Aziz and Potapov, Igor},
acronym = {{RP}'13},
booktitle = {{P}roceedings of the 7th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'13)},
author = {Bouyer, Patricia and Markey, Nicolas and Sankur, Ocan},
title = {Robustness in timed automata},
pages = {1-18},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-rp13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-rp13.pdf},
doi = {10.1007/978-3-642-41036-9_1},
abstract = {In this paper we survey several approaches to the robustness of
timed automata, that~is, the ability of a system to resist to slight
perturbations or errors. We will concentrate on robustness against timing
errors which can be due to measuring errors, imprecise clocks, and
unexpected runtime behaviors such as execution times that are longer or
shorter than expected.\par
We consider the perturbation model of guard enlargement and formulate
several robust verification problems that have been studied recently,
including robustness analysis, robust implementation, and robust control.}
}
@inproceedings{CH-pnse13,
address = {Milano, Italy},
month = jun,
year = 2013,
volume = 969,
series = {CEUR Workshop Proceedings},
publisher = {RWTH Aachen, Germany},
editor = {Moldt, Daniel and R{\"o}lke, Heiko},
acronym = {{PNSE}'13},
booktitle = {{P}roceedings of the 7th {I}nternational {W}orkshop on {P}etri
{N}ets and {S}oftware {E}ngineering ({PNSE}'13)},
author = {Chatain, {\relax Th}omas and Haar, Stefan},
title = {A~Canonical Contraction for Safe {P}etri Nets},
pages = {25-39},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CH-pnse13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CH-pnse13.pdf},
abstract = {Under maximal semantics, the occurrence of an event~\(a\) in a
concurrent run of an occurrence net may imply the occurrence of other
events, not causally related to~\(a\), in the same run. In recent works, we
have formalized this phenomenon as the \emph{reveals} relation, and used
it to obtain a contraction of sets of events called \emph{facets} in the
context of occurrence nets. Here, we extend this idea to propose a
canonical contraction of general safe Petri nets into pieces of
partial-order behaviour which can be seen as {"}macro-transitions{"} since
all their events must occur together in maximal semantics. On occurrence
nets, our construction coincides with the facets abstraction. Our
contraction preserves the maximal semantics in the sense that the maximal
processes of the contracted net are in bijection with those of the
original net.}
}
@inproceedings{PHL-ictss13,
address = {Istanbul, Turkey},
month = nov,
year = 2013,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Yenig{\"u}n, H{\"u}sn{\"u} and Yilmaz, Cemal and Ulrich, Andreas},
acronym = {{ICTSS}'13},
booktitle = {{P}roceedings of the 25th {IFIP} {I}nternational {C}onference on
{T}esting {S}oftware and {S}ystems ({ICTSS}'13)},
author = {Ponce{ }de{~}Le{\'o}n, Hern{\'a}n and Haar, Stefan and
Longuet, Delphine},
title = {Unfolding-based Test Selection for Concurrent Conformance},
pages = {98-113},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-ictss13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-ictss13.pdf},
doi = {10.1007/978-3-642-41707-8_7},
abstract = {Model-based testing has mainly focused on models where currency
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 propose 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
a coverage criterion based on a dedicated notion of complete prefixes that
selects a manageable test suite.}
}
@inproceedings{PBB-dx13,
address = {Jerusalem, Israel},
month = oct,
year = 2013,
editor = {Kalech, Meir and Feldman, Alexander and Provan, Gregory},
acronym = {{DX}'13},
booktitle = {{P}roceedings of the 24th {I}nternational {W}orkshop on
{P}rinciples of {D}iagnosis ({DX}'13)},
author = {Ponce{ }de{~}Le{\'o}n, Hern{\'a}n and Bonigo, Gonzalo and
Brand{\'a}n{ }Briones, Laura},
title = {Distributed Analysis of Diagnosability in Concurrent Systems},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/PBB-dx13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PBB-dx13.pdf},
abstract = {Complex systems often exhibit unexpected faults that are
difficult to handle. Such systems are desirable to be diagnosable, i.e.
faults can be automatically detected as they occur (or shortly
afterwards), enabling the system to handle the fault or recover. A system
is diagnosable if it is possible to detect every fault, in a finite time
after they occurred, by only observing the available information from the
system. Complex systems are usually built from simpler components running
concurrently. We study how to infer the diagnosability property of a
complex system (distributed and with multiple faults) from a parallelized
analysis of the diagnosability of each of its components synchronizing
with fault free versions of the others. In this paper we make the
following contributions: (1)~we~address the diagnosability problem of
concurrent systems with arbitrary faults occurring freely in each
component. (2)~We~distribute the diagnosability analysis and illustrate
our approach with examples. Moreover, (3)~we~present a prototype tool that
implements our techniques showing promising results.}
}
@inproceedings{reichert-rp13,
address = {Uppsala, Sweden},
month = sep,
year = 2013,
volume = {8169},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abdulla, Parosh Aziz and Potapov, Igor},
acronym = {{RP}'13},
booktitle = {{P}roceedings of the 7th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'13)},
author = {Reichert, Julien},
title = {On The Complexity of Counter Reachability Games},
pages = {196-208},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/JR-rp13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JR-rp13.pdf},
doi = {10.1007/978-3-642-41036-9_18},
abstract = {Counter reachability games are played by two players on a graph
with labelled edges. Each move consists in picking an edge from the
current location and adding its label to a counter vector. The objective
is to reach a given counter value in a given location. We distinguish
three semantics for counter reachability games, according to what happens
when a counter value would become negative: the edge is either disabled,
or enabled but the counter value becomes zero, or enabled. We consider the
problem of deciding the winner in counter reachability games and show
that, in most cases, it has the same complexity under all semantics.
Surprisingly, under one semantics, the complexity in dimension one depends
on whether the objective value is zero or any other integer.}
}
@inproceedings{BHJL-rp13,
address = {Uppsala, Sweden},
month = sep,
year = 2013,
volume = {8169},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abdulla, Parosh Aziz and Potapov, Igor},
acronym = {{RP}'13},
booktitle = {{P}roceedings of the 7th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'13)},
author = {B{\'e}rard, B{\'e}atrice and Haddad, Serge and
Jovanovic, Aleksandra and Lime, Didier},
title = {Parametric Interrupt Timed Automata},
pages = {59-69},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHJL-rp13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHJL-rp13.pdf},
doi = {10.1007/978-3-642-41036-9_7},
abstract = {Parametric reasoning is particularly relevant for timed models,
but very often leads to undecidability of reachability problems. We
propose a parametrised version of Interrupt Timed Automata (an~expressive
model incomparable to Timed Automata), where polynomials of parameters can
occur in guards and updates. We prove that different reachability
problems, including robust reachability, are decidable for this model, and
we give complexity upper bounds for a fixed or variable number of clocks
and parameters.}
}
@inproceedings{FS-rp13,
address = {Uppsala, Sweden},
month = sep,
year = 2013,
volume = {8169},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abdulla, Parosh Aziz and Potapov, Igor},
acronym = {{RP}'13},
booktitle = {{P}roceedings of the 7th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'13)},
author = {Fribourg, Laurent and Soulat, Romain},
title = {Stability Controllers for Sampled Switched Systems},
pages = {135-145},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FS-rp13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FS-rp13.pdf},
doi = {10.1007/978-3-642-41036-9_13},
abstract = {We consider in this paper switched systems, a class of hybrid
systems recently used with success in various domains such as automotive
industry and power electonics. We propose a state-dependent control
strategy which makes the trajectories of the analyzed system converge to
finite cyclic sequences of points. Our method relies on a technique of
decomposition of the state space into local regions where the control is
uniform. We have implemented the procedure using zonotopes, and applied it
successfully to several examples of the literature.}
}
@incollection{DKNPPPS-book13,
author = {Duflot, Marie and Kwiatkowska, Marta and
Norman, Gethin and Parker, David and
Peyronnet, Sylvain and Picaronny, Claudine and
Sproston, Jeremy},
title = {Practical Applications of Probabilistic Model
Checking to Communication Protocols},
booktitle = {Formal Methods for Industrial Critical Systems: A Survey of Applications},
editor = {Gnesi, Stefania and Margaria, Tiziana},
publisher = {John Wiley \& Sons, Ltd. and {IEEE} Computer Society Press},
year = 2013,
chapter = 7,
pages = {133-150},
month = mar,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DKNPPPS-book13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DKNPPPS-book13.pdf},
doi = {10.1002/9781118459898.ch7}
}
@inproceedings{DDS-icalp13,
address = {Riga, Latvia},
month = jul,
year = 2013,
volume = {7966},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Fomin, Fedor V. and Freivalds, R{\=u}si{\c{n}}{\v{s}}
and Kwiatkowska, Marta and Peleg, David},
acronym = {{ICALP}'13},
booktitle = {{P}roceedings of the 40th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'13)~-- {P}art~{II}},
author = {Demri, St{\'e}phane and Dhar, Amit Kumar and Sangnier, Arnaud},
title = {On the Complexity of Verifying Regular Properties on Flat Counter Systems},
pages = {162-173},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-icalp13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDS-icalp13.pdf},
doi = {10.1007/978-3-642-39212-2_17},
abstract = {Among the approximation methods for the verification of counter
systems, one of them consists in model-checking their flat unfoldings.
Unfortunately, the complexity characterization of model-checking problems
for such operational models is not always well studied except for
reachability queries or for Past LTL. In this paper, we characterize the
complexity of model-checking problems on flat counter systems for the
specification languages including first-order logic, linear mu-calculus,
infinite automata, and related formalisms. Our results span different
complexity classes (mainly from PTime to PSpace) and they apply to
languages in which arithmetical constraints on counter values are
systematically allowed. As far as the proof techniques are concerned, we
provide a uniform approach that focuses on the main issues.}
}
@inproceedings{JGL-mfcs13,
address = {Klosterneuburg, Austria},
month = aug,
year = 2013,
volume = {8087},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Chatterjee, Krishnendu and Sgall, Ji{\v{r}}{\'\i}},
acronym = {{MFCS}'13},
booktitle = {{P}roceedings of the 38th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'13)},
author = {Goubault{-}Larrecq, Jean},
title = {A Constructive Proof of the Topological {K}ruskal Theorem},
pages = {22-41},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-mfcs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-mfcs13.pdf},
doi = {10.1007/978-3-642-40313-2_3},
abstract = {We give a constructive proof of Kruskal's Tree
Theorem---precisely, of a topological extension of~it. The proof is in the
style of a constructive proof of Higman's Lemma due to Murthy and
Russell~(1990), and illuminates the role of regular expressions there. In
the process, we discover an extension of Dershowitz' recursive path
ordering to a form of cyclic terms which we call \(\mu\)-terms. This all came
from recent research on Noetherian spaces, and serves as a teaser for
their theory.}
}
@inproceedings{Fribourg-fsfma13,
address = {Singapore},
month = jul,
year = 2013,
volume = 31,
series = {Open Access Series in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Choppy, {\relax Ch}ristine and Sun, Jun},
acronym = {{FSFMA}'13},
booktitle = {{P}roceedings of the 1st {F}rench-{S}ingaporean {W}orkshop
on {F}ormal {M}ethods and {A}pplications ({FSFMA}'13)},
author = {Fribourg, Laurent},
title = {Control of Switching Systems by Invariance Analysis (Invited~Talk)},
pages = {1},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/F-fsfma13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/F-fsfma13.pdf},
doi = {10.4230/OASIcs.FSFMA.2013.1},
abstract = {Switched systems are embedded devices widespread in industrial
applications such as power electronics and automotive
control. They consist of continuous-time dynamical
subsystems and a rule that controls the switching between
them. Under a suitable control rule, the system can improve
its steady-state performance and meet essential properties
such as safety and stability in desirable operating zones.
We explain that such controller synthesis problems are
related to the construction of appropriate invariants of the
state space, which approximate the limit sets of the system
trajectories. We present a new approach of invariant
construction based on a technique of state space
decomposition interleaved with forward fixed point
computation. The method is illustrated in a case study taken
from the field of power electronics.}
}
@inproceedings{FKS-fsfma13,
address = {Singapore},
month = jul,
year = 2013,
volume = 31,
series = {Open Access Series in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Choppy, {\relax Ch}ristine and Sun, Jun},
acronym = {{FSFMA}'13},
booktitle = {{P}roceedings of the 1st {F}rench-{S}ingaporean {W}orkshop
on {F}ormal {M}ethods and {A}pplications ({FSFMA}'13)},
author = {Fribourg, Laurent and K{\"u}hne, Ulrich and Soulat, Romain},
title = {Constructing Attractors of Nonlinear Dynamical Systems by
State Space Decomposition},
pages = {53-60},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FKS-fsfma13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FKS-fsfma13.pdf},
doi = {10.4230/OASIcs.FSFMA.2013.53},
abstract = {In a previous work, we have shown how to generate attractor sets
of affine hybrid systems using a method of state space decomposition. We
show here how to adapt the method to polynomial dynamics systems by
approximating them as switched affine systems. We show the practical
interest of the method on standard examples of the literature.}
}
@inproceedings{GHPR-pn13,
address = {Milano, Italy},
month = jun,
year = 2013,
volume = {7927},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Colom, Jos{\'e}-Manuel and Desel, J{\"o}rg},
acronym = {{PETRI~NETS}'13},
booktitle = {{P}roceedings of the 34th
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({PETRI~NETS}'13)},
author = {Geeraerts, Gilles and Heu{\ss}ner, Alexander and Praveen, M.
and Raskin, Jean-Fran{\c{c}}ois},
title = {{{\(\omega\)}}-{P}etri nets},
pages = {49-69},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GHPR-atpn13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GHPR-atpn13.pdf},
doi = {10.1007/978-3-642-38697-8_4},
abstract = {We introduce \(\omega\)-Petri nets (\(\omega\)PN), an extension
of plain Petri nets with \(\omega\)-labeled input and output arcs, that is
well-suited to analyse parametric concurrent systems with dynamic thread
creation. Most techniques (such as the Karp and Miller tree or the Rackoff
technique) that have been proposed in the setting of plain Petri nets do
not apply directly to \(\omega\)PN because \(\omega\)PN define transition systems
that have infinite branching. This motivates a thorough analysis of the
computational aspects of~\(\omega\)PN. We show that an \(\omega\)PN can be turned
into a plain Petri net that allows to recover the reachability set of the
\(\omega\)PN, but that does not preserve termination. This yields complexity
bounds for the reachability, (place) boundedness and coverability problems
on \(\omega\)PN. We provide a practical algorithm to compute a coverability
set of the \(\omega\)PN and to decide termination by adapting the classical
Karp and Miller tree construction. We also adapt the Rackoff technique to
\(\omega\)PN, to obtain the exact complexity of the termination problem.
Finally, we consider the extension of \(\omega\)PN with reset and transfer
arcs, and show how this extension impacts the decidability and complexity
of the aforementioned problems.}
}
@article{KS-tocl13,
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
author = {Kazana, Wojciech and Segoufin, Luc},
title = {Enumeration of monadic second-order queries on trees},
volume = 14,
number = {4},
year = 2013,
month = nov,
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-tocl13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-tocl13.pdf},
doi = {10.1145/2528928},
abstract = {We consider the enumeration problem of monadic second-order
(MSO) queries with first-order free variables over trees. In [Bagan 2006]
it was shown that this problem is in
\textsc{Constant-Delay}\(_{\text{lin}}\). An enumeration problem belongs
to \textsc{Constant-Delay}\(_{\text{lin}}\) if for an input structure of
size~\(n\) it can be solved by:
\begin{itemize}
\item an \(O(n)\) precomputation phase building an index structure,
\item followed by a phase enumerating the answers with no repetition and a
constant delay between two consecutive outputs.
\end{itemize}
In this article we give a different proof of this result based on the
deterministic factorization forest decomposition theorem of Colcombet
[Colcombet~2007].}
}
@inproceedings{BST-pods13,
address = {New~York, New~York, USA},
month = jun,
year = 2013,
publisher = {ACM Press},
editor = {Fan, Wenfei},
acronym = {{PODS}'13},
booktitle = {{P}roceedings of the 32nd {A}nnual
{ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium
on {P}rinciples of {D}atabase {S}ystems
({PODS}'13)},
author = {Boja{\'n}czyk, Miko{\l}aj and Segoufin, Luc and Toru{\'n}czyk, Szymon},
title = {Verification of Database-driven Systems via Amalgamation},
pages = {63-74},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BST-pods13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BST-pods13.pdf},
doi = {10.1145/2463664.2465228},
abstract = {We describe a general framework for static verification of
systems that base their decisions upon queries to databases. The database
is specified using constraints, typically a schema, and is not modified
during a run of the system. The system is equipped with a finite number of
registers for storing intermediate information from the database and the
specification consists of a transition table described using
quantifier-free formulas that can query either the database or the
registers.\par
Our main result concerns systems querying XML databases---modeled as data
trees---using quantifier-free formulas with predicates such as the
descendant axis or comparison of data values. In this scenario we show an
ExpSpace algorithm for deciding reachability.\par
Our technique is based on the notion of amalgamation and is quite general.
For instance it also applies to relational databases (with an optimal
\textsc{PSpace} algorithm).\par
We also show that minor extensions of the model lead to undecidability.}
}
@inproceedings{GLS-pods13,
address = {New~York, New~York, USA},
month = jun,
year = 2013,
publisher = {ACM Press},
editor = {Fan, Wenfei},
acronym = {{PODS}'13},
booktitle = {{P}roceedings of the 32nd {A}nnual
{ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium
on {P}rinciples of {D}atabase {S}ystems
({PODS}'13)},
author = {Gheerbrant, Am{\'e}lie and Libkin, Leonid and Sirangelo, Cristina},
title = {When is Na{\"\i}ve Evaluation Possible?},
pages = {75-86},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GLS-pods13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLS-pods13.pdf},
doi = {10.1145/2463664.2463674},
abstract = {The term na{\"\i}ve evaluation refers to evaluating queries over
incomplete databases as if nulls were usual data values, i.e., to using
the standard database query evaluation engine. Since the semantics of
query answering over incomplete databases is that of certain answers, we
would like to know when na{\"\i}ve evaluation computes them: i.e., when
certain answers can be found without inventing new specialized algorithms.
For relational databases it is well known that unions of conjunctive
queries possess this desirable property, and results on preservation of
formulae under homomorphisms tell us that within relational calculus, this
class cannot be extended under the open-world assumption.\par
Our goal here is twofold. First, we develop a general framework that
allows us to determine, for a given semantics of incompleteness, classes
of queries for which na{\"\i}ve evaluation computes certain answers.
Second, we apply this approach to a variety of semantics, showing that for
many classes of queries beyond unions of conjunctive queries, na{\"\i}ve
evaluation makes perfect sense under assumptions different from
open-world. Our key observations are: (1)~na{\"\i}ve evaluation is
equivalent to monotonicity of queries with respect to a semantics-induced
ordering, and (2)~for most reasonable semantics, such monotonicity is
captured by preservation under various types of homomorphisms. Using these
results we find classes of queries for which na{\"\i}ve evaluation works,
e.g., positive first-order formulae for the closed-world semantics. Even
more, we introduce a general relation-based framework for defining
semantics of incompleteness, show how it can be used to capture many known
semantics and to introduce new ones, and describe classes of first-order
queries for which na{\"\i}ve evaluation works under such semantics.}
}
@inproceedings{AV-pods13,
address = {New~York, New~York, USA},
month = jun,
year = 2013,
publisher = {ACM Press},
editor = {Fan, Wenfei},
acronym = {{PODS}'13},
booktitle = {{P}roceedings of the 32nd {A}nnual
{ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium
on {P}rinciples of {D}atabase {S}ystems
({PODS}'13)},
author = {Abiteboul, Serge and Vianu, Victor},
title = {Collaborative Data-Driven Workflows: Think Global, Act Local},
pages = {91-102},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AV-pods13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AV-pods13.pdf},
doi = {10.1145/2463664.2463672},
abstract = {We introduce and study a model of collaborative data-driven
workflows. In a local-as-view style, each peer has a partial view of a
global instance that remains purely virtual. Local updates have side
effects on other peers' data, defined via the global instance. We also
assume that the peers provide (an abstraction of) their specifications, so
that each peer can actually see and reason on the specification of the
entire system. We study the ability of a peer to carry out runtime
reasoning about the global run of the system, and in particular about
actions of other peers, based on its own local observations. A main
contribution is to show that, under a reasonable restriction (namely,
key-visibility ), one can construct a finite symbolic representation of
the infinite set of global runs consistent with given local observations.
Using the symbolic representation, we show that we can evaluate in pspace
a large class of properties over global runs, expressed in an extension of
first-order logic with past linear-time temporal operators, PLTL-FO. We
also provide a variant of the algorithm allowing to incrementally monitor
a statically defined property, and then develop an extension allowing to
monitor an infinite class of properties sharing the same temporal
structure, defined dynamically as the run unfolds. Finally, we consider an
extension of the language, augmeting workflow control with PLTL-FO
formulas. We prove that this does not increase the power of the workflow
specification language, thereby showing that the language is closed under
such introspective reasoning.}
}
@inproceedings{KS-pods13,
address = {New~York, New~York, USA},
month = jun,
year = 2013,
publisher = {ACM Press},
editor = {Fan, Wenfei},
acronym = {{PODS}'13},
booktitle = {{P}roceedings of the 32nd {A}nnual
{ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium
on {P}rinciples of {D}atabase {S}ystems
({PODS}'13)},
author = {Kazana, Wojciech and Segoufin, Luc},
title = {Enumeration of First-Order Queries on Classes of Structures With Bounded Expansion},
pages = {297-308},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-pods13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-pods13.pdf},
doi = {10.1145/2463664.2463667},
abstract = {We consider the evaluation of first-order queries over classes
of databases with bounded expansion. The notion of bounded expansion is
fairly broad and generalizes bounded degree, bounded treewidth and
exclusion of at least one minor. It was known that over a class of
databases with bounded expansion, first-order sentences could be evaluated
in time linear in the size of the database. We first give a different
proof of this result. Moreover, we show that answers to first-order
queries can be enumerated with constant delay after a linear time
preprocessing. We also show that counting the number of answers to a query
can be done in time linear in the size of the database.}
}
@inproceedings{SHLRFLF-epe13,
address = {Lille, France},
month = sep,
year = 2013,
publisher = {{IEEE} Power Electronics Society},
editor = {Lataire, {\relax Ph}ilippe},
booktitle = {{P}roceedings of the 15th {E}uropean {C}onference
on {P}ower {E}lectronics and {A}pplications ({EPE}'13)},
author = {Soulat, Romain and H{\'e}rault, Guillaume and Labrousse,
Denis and Revol, Bertrand and Feld, Gilles and Lefebvre,
St{\'e}phane and Fribourg, Laurent},
title = {Use of a full wave correct-by-design command to control a
multilevel modular converter},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SHLRFLF-epe13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SHLRFLF-epe13.pdf},
doi = {10.1109/EPE.2013.6634448},
abstract = {This paper proposes a method to synthesize a full wave control
applied to a multilevel modular converter~(MMC). This method guarantees
the output waveform and the balancing of the capacitors. Numerical
simulations and experiments are used to check the validity of the
approach.}
}
@inproceedings{ABDHHKLP-icfem13,
address = {Queenstown, New~Zealand},
month = oct # {-} # nov,
year = 2013,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Groves, Lindsay and Sub, Jing},
acronym = {{ICFEM}'13},
booktitle = {{P}roceedings of the 15th {I}nternational
{C}onference on {F}ormal {E}ngineering
{M}ethods
({ICFEM}'13)},
author = {Andr{\'e}, {\'E}tienne and Barbot, Beno{\^\i}t and
D{\'e}moulins, Cl{\'e}ment and Hillah, Lom Messan and
Hulin{-}Hubard, Francis and Kordon, Fabrice and Linard, Alban
and Petrucci, Laure},
title = {A Modular Approach for Reusing Formalisms in Verification
Tools of Concurrent Systems},
pages = {199-214},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABDHHKLP-icfem13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABDHHKLP-icfem13.pdf},
doi = {10.1007/978-3-642-41202-8_14},
abstract = {Over the past two decades, numerous verification tools have been
successfully used for verifying complex concurrent systems, modelled using
various formalisms. However, it is still hard to coordinate these tools
since they rely on such a large number of formalisms. Having a proper
syntactical mechanism to interrelate them through variability would
increase the capability of effective integrated formal methods. In this
paper, we propose a modular approach for defining new formalisms by
reusing existing ones and adding new features and/or constraints. Our
approach relies on standard XML technologies; their use provides the
capability of rapidly and automatically obtaining tools for representing
and validating models. It thus enables fast iterations in developing and
testing complex formalisms. As a case study, we applied our modular
definition approach on families of Petri nets and timed automata.}
}
@inproceedings{AHHKLLP-iceccs13,
address = {Singapore},
month = jul,
year = 2013,
publisher = {{IEEE} Computer Society Press},
editor = {Liu, Yang and Martin, Andrew},
acronym = {{ICECCS}'13},
booktitle = {{P}roceedings of the 18th {IEEE} {I}nternational {C}onference on {E}ngineering of
{C}omplex {C}omputer {S}ystems ({ICECCS}'13)},
author = {Andr{\'e}, {\'E}tienne and Hillah, Lom Messan and Hulin{-}Hubard,
Francis and Kordon, Fabrice and Lembachar, Yousra and Linard, Alban
and Petrucci, Laure},
title = {{C}osy{V}erif: An~Open Source Extensible Verification
Environment},
pages = {33-36},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AHHKLLP-iceccs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AHHKLLP-iceccs13.pdf},
doi = {10.1109/ICECCS.2013.15},
abstract = {CosyVerif aims at gathering within a common framework various
existing tools for specification and verification. It has been designed in
order to 1)~support different formalisms with the ability to easily create
new ones, 2)~provide a graphical user interface for every formalism,
3)~include verification tools called via the graphical interface or via an
API as a Web service, and 4)~offer the possibility for a developer to
integrate his/her own tool without much effort, also allowing it to
interact with the other tools. Several tools have already been integrated
for the formal verification of (extensions~of) Petri nets and timed
automata.}
}
@inproceedings{LM-gandalf13,
address = {Borca di Cadore, Italy},
month = aug,
year = 2013,
volume = {119},
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Puppis, Gabriele and Villa, Tiziano},
acronym = {{GandALF}'13},
booktitle = {{P}roceedings of the 4th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification
({GandALF}'13)},
author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas},
title = {Satisfiability of {ATL} with strategy contexts},
pages = {208-223},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LM-gandalf13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LM-gandalf13.pdf},
doi = {10.4204/EPTCS.119.18},
abstract = {Various extensions of the temporal logic ATL have recently been
introduced to express rich properties of multi-agent systems. Among these,
ATLsc extends ATL with \emph{strategy contexts}, while Strategy Logic has
\emph{first-order quantification} over strategies. There is a price to pay
for the rich expressiveness of these logics: model-checking is
non-elementary, and satisfiability is undecidable.\par
We prove in this paper that satisfiability is decidable in several special
cases. The most important one is when restricting to \emph{turn-based}
games. We~prove that decidability also holds for concurrent games if the
number of moves available to the agents is bounded. Finally, we~prove that
restricting strategy quantification to memoryless strategies brings back
undecidability.}
}
@inproceedings{BDGORW-atva13,
address = {Hanoi, Vietnam},
month = oct,
year = {2013},
volume = {8172},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Dang{-}Van, Hung and Ogawa, Mizuhito},
acronym = {{ATVA}'13},
booktitle = {{P}roceedings of the 11th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'13)},
author = {Brihaye, {\relax Th}omas and Doyen, Laurent and Geeraerts, Gilles and
Ouaknine, Jo{\"e}l and Raskin, Jean-Fran{\c{c}}ois
and Worrell, James},
title = {Time-Bounded Reachability for Monotonic Hybrid Automata: Complexity and Fixed
Points},
pages = {55-70},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDGORW-atva13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDGORW-atva13.pdf},
doi = {10.1007/978-3-319-02444-8_6},
abstract = {We study the \emph{time-bounded reachability problem} for \emph{monotonic
hybrid automata} (MHA), i.e., rectangular hybrid automata for which the
rate of each variable is either always non-negative or always
non-positive. In this paper, we revisit the decidability results presented
in [Brihaye et~al., \textit{On reachability for hybrid automata over
bounded time}, ICALP~2011] and show that the problem is NExpTime-complete.
We also show that we can effectively compute fixed points that
characterise the sets of states that are reachable (resp. co-reachable)
within \(T\) time units from a given state.}
}
@inproceedings{CDRR-atva13,
address = {Hanoi, Vietnam},
month = oct,
year = {2013},
volume = {8172},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Dang{-}Van, Hung and Ogawa, Mizuhito},
acronym = {{ATVA}'13},
booktitle = {{P}roceedings of the 11th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'13)},
author = {Chatterjee, Krishnendu and Doyen, Laurent and Randour, Mickael and
Raskin, Jean-Fran{\c{c}}ois},
title = {Looking at Mean-Payoff and Total-Payoff through Windows},
pages = {118-132},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDRR-atva13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDRR-atva13.pdf},
doi = {10.1007/978-3-319-02444-8_10},
abstract = {We consider two-player games played on weighted directed graphs
with mean-payoff and total-payoff objectives, two classical quantitative
objectives. While for single-dimensional games the complexity and memory
bounds for both objectives coincide, we show that in contrast to
multi-dimensional mean-payoff games that are known to be coNP-complete,
multi-dimensional total-payoff games are undecidable. We introduce
conservative approximations of these objectives, where the payoff is
considered over a local finite window sliding along a play, instead of the
whole play. For single dimension, we show that (i)~if the window size is
polynomial, deciding the winner takes polynomial time, and (ii)~the
existence of a bounded window can be decided in NP coNP, and is at least
as hard as solving mean-payoff games. For multiple dimensions, we show
that (i)~the problem with fixed window size is EXPTIME-complete, and
(ii)~there is no primitive-recursive algorithm to decide the existence of
a bounded window.}
}
@inproceedings{RS-atva13,
address = {Hanoi, Vietnam},
month = oct,
year = {2013},
volume = {8172},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Dang{-}Van, Hung and Ogawa, Mizuhito},
acronym = {{ATVA}'13},
booktitle = {{P}roceedings of the 11th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'13)},
author = {Rodr{\'\i}guez, C{\'e}sar and Schwoon, Stefan},
title = {Cunf: A~Tool for Unfolding and Verifying Petri Nets with Read
Arcs},
pages = {492-495},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/RS-atva13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RS-atva13.pdf},
doi = {10.1007/978-3-319-02444-8_42},
abstract = {Cunf is a tool for building and analyzing unfoldings of Petri
nets with read arcs. An unfolding represents the behaviour of a net by a
partial order, effectively coping with the state-explosion problem
stemming from the interleaving of concurrent actions. C-net unfoldings can
be up to exponentially smaller than Petri net unfoldings, and recent work
proposed algorithms for their construction and verification. Cunf is the
first implementation of these techniques, it has been carefully engineered
and optimized to ensure that the theoretical gains are put into
practice.}
}
@inproceedings{AFS-atva13,
address = {Hanoi, Vietnam},
month = oct,
year = {2013},
volume = {8172},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Dang{-}Van, Hung and Ogawa, Mizuhito},
acronym = {{ATVA}'13},
booktitle = {{P}roceedings of the 11th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'13)},
author = {Andr{\'e}, {\'E}tienne and Fribourg, Laurent and Soulat, Romain},
title = {Merge and Conquer: State Merging in Parametric Timed Automata},
pages = {381-396},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AFS-atva13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AFS-atva13.pdf},
doi = {10.1007/978-3-319-02444-8_27},
abstract = {Parameter synthesis for real-time systems aims at synthesizing
dense sets of valuations for the timing requirements, guaranteeing a good
behavior. A popular formalism for modeling parameterized realtime systems
is parametric timed automata (PTAs). Compacting the state space of PTAs as
much as possible is fundamental. We present here a state merging reduction
based on convex union, that reduces the state space, but yields an
over-approximation of the executable paths. However, we show that it
preserves the sets of reachable locations and executable actions. We also
show that our merging technique associated with the inverse method, an
algorithm for parameter synthesis, preserves locations as well, and
outputs larger sets of parameter valuations.}
}
@article{CCD-tcs13,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Cheval, Vincent and Cortier, V{\'e}ronique and Delaune, St{\'e}phanie},
title = {Deciding equivalence-based properties using constraint solving},
year = {2013},
month = jun,
volume = {492},
pages = {1-39},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-tcs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-tcs13.pdf},
doi = {10.1016/j.tcs.2013.04.016},
abstract = {Formal methods have proved their usefulness for analyzing the
security of protocols. Most existing results focus on trace properties
like secrecy 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, privacy related properties or statements closer to
security properties used in cryptography.\par
In this paper, we consider three notions of equivalence defined in the
applied pi calculus: observational equivalence, may-testing equivalence,
and trace equivalence. First, we study the relationship between these
three notions. We show that for determinate processes, observational
equivalence actually coincides with trace equivalence, a notion simpler to
reason with. We exhibit a large class of determinate processes, called
simple processes, that capture most existing protocols and cryptographic
primitives. While trace equivalence and may-testing equivalence seem very
similar, we show that may-testing equivalence is actually strictly
stronger than trace equivalence. We prove that the two notions coincide
for image-finite processes, such as processes without replication.\par
Second, we reduce the decidability of trace equivalence (for finite
processes) to deciding symbolic equivalence between sets of constraint
systems. For simple processes without replication and with trivial else
branches, it turns out that it is actually sufficient to decide symbolic
equivalence between pairs of positive constraint systems. Thanks to this
reduction and relying on a result first proved by M. Baudet, this yields
the first decidability result of observational equivalence for a general
class of equational theories (for processes without else branch nor
replication). Moreover, based on another decidability result for deciding
equivalence between sets of constraint systems, we get decidability of
trace equivalence for processes with else branch for standard
primitives.}
}
@inproceedings{SS-concur13,
address = {Buenos Aires, Argentina},
month = aug,
year = 2013,
volume = 8052,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {D'Argenio, Pedro R. and Melgratti, Hern{\'a}n)},
acronym = {{CONCUR}'13},
booktitle = {{P}roceedings of the 24th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'13)},
author = {Schmitz, Sylvain and Schnoebelen, {\relax Ph}ilippe},
title = {The Power of Well-Structured Systems},
pages = {5-24},
url = {http://arxiv.org/abs/1402.2908},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SS-concur13.pdf},
doi = {10.1007/978-3-642-40184-8_2},
abstract = {Well-structured systems, aka WSTS, are computational models
where the set of possible configurations is equipped with a
well-quasi-ordering which is compatible with the transition relation
between configurations. This structure supports generic decidability
results that are important in verification and several other fields. This
paper recalls the basic theory underlying well-structured systems and
shows how two classic decision algorithms can be formulated as an
exhaustive search for some {"}bad{"} sequences. This lets us describe new
powerful techniques for the complexity analysis of WSTS algorithms.
Recently, these techniques have been successful in precisely
characterizing the power, in a complexity-theoretical sense, of several
important WSTS models like unreliable channel systems, monotonic counter
machines, or networks of timed systems.}
}
@inproceedings{CCS-cade2013,
address = {Lake Placid, New~York, USA},
month = jun,
year = 2013,
volume = 7898,
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
editor = {Bonacina, Maria Paola},
acronym = {{CADE}'13},
booktitle = {{P}roceedings of the 24th {I}nternational
{C}onference on {A}utomated {D}eduction
({CADE}'13)},
author = {Comon{-}Lundh, Hubert and Cortier, V{\'e}ronique and
Scerri, Guillaume},
title = {Tractable inference systems: an extension with a
deducibility predicate},
pages = {91-108},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCS-cade2013.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCS-cade2013.pdf},
doi = {10.1007/978-3-642-38574-2_6},
abstract = {The main contribution of the paper is a PTIME decision procedure
for the satisfiability problem in a class of first-order Horn clauses. Our
result is an extension of the tractable classes of Horn clauses of Basin &
Ganzinger in several respects. For instance, our clauses may contain
atomic formulas \(S \vdash t\) where \(\vdash\) is a predicate symbol and
\(S\) is a finite set of terms instead of a term. \(\vdash\)~is used to
represent any possible computation of an attacker, given a set of
messages~\(S\). The class of clauses that we consider encompasses the
clauses designed by Bana~\& Comon-Lundh for security proofs of protocols
in a computational model. \par
Because of the (variadic) \(\vdash\) predicate symbol, we cannot use
ordered resolution strategies only, as in Basin~\& Ganzinger: given \(S
\vdash t\), we must avoid computing \(S' \vdash t\) for all subsets \(S'\)
of~\(S\). Instead, we design PTIME entailment procedures for increasingly
expressive fragments, such procedures being used as oracles for the next
fragment. \par
Finally, we obtain a PTIME procedure for arbitrary ground clauses and
saturated Horn clauses (as in Basin~\& Ganzinger), together with a
particular class of (non saturated) Horn clauses with the \(\vdash\)
predicate and constraints (which are necessary to cover the
application).}
}
@inproceedings{HRS-acsd13,
address = {Barcelona, Spain},
month = jul,
year = 2013,
publisher = {{IEEE} Computer Society Press},
editor = {Pietkiewicz{-}Koutny, Marta and Lazarescu, Mihai Teodor},
acronym = {{ACSD}'13},
booktitle = {{P}roceedings of the 13th {I}nternational
{C}onference on {A}pplication of {C}oncurrency
to {S}ystem {D}esign
({ACSD}'13)},
author = {Haar, Stefan and Rodr{\'\i}guez, C{\'e}sar and Schwoon, Stefan},
title = {Reveal Your Faults: It's Only Fair!},
pages = {120-129},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HRS-acsd13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HRS-acsd13.pdf},
doi = {10.1109/ACSD.2013.15},
abstract = {We present a methodology for fault diagnosis in
concurrent, partially observable systems with additional fairness
constraints. In this weak diagnosis, one asks whether a concurrent
chronicle of observed events allows to determine that a
non-observable fault will inevitably occur, sooner or later, on
any maximal system run compatible with the observation. The
approach builds on strengths and techniques of unfoldings of safe
Petri nets, striving to compute a compact prefix of the unfolding
that carries sufficient information for the diagnosis
algorithm. Our work extends and generalizes the unfolding-based
diagnosis approaches by Benveniste \textit{et~al.} as well as
Esparza and Kern. Both of these focused mostly on the use of
sequential observations, in particular did not exploit the
capacity of unfoldings to reveal inevitable occurrences of
concurrent or future events studied by Balaguer
\textit{et~al.}. Our diagnosis method captures such indirect,
revealed dependencies. We~develop theoretical foundations and an
algorithmic solution to the diagnosis problem, and present a SAT
solving method for practical diagnosis with our approach.}
}
@article{HKS-tcs13,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Haar, Stefan and Kern, Christian and Schwoon, Stefan},
title = {Computing the Reveals Relation in Occurrence Nets},
year = 2013,
month = jul,
volume = 493,
pages = {66-79},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HKS-tcs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HKS-tcs13.pdf},
doi = {10.1016/j.tcs.2013.04.028},
abstract = {Petri net unfoldings are a useful tool to tackle state-space
explosion in verification and related tasks. Moreover, their structure
allows to access directly the relations of causal precedence, concurrency,
and conflict between events. Here, we explore the data structure further,
to determine the following relation: event~\(a\) is said to reveal
event~\(b\) iff the occurrence of~\(a\) implies that~\(b\) inevitably
occurs, too, be it before, after, or concurrently with~\(a\). Knowledge of
reveals facilitates in particular the analysis of partially observable
systems, in the context of diagnosis, testing, or verification; it can
also be used to generate more concise representations of behaviours via
abstractions. The reveals relation was previously introduced in the
context of fault diagnosis, where it was shown that the reveals relation
was decidable: for a given pair~\(a,b\) in the unfolding~\(U\) of a safe
Petri net~\(N\), a finite prefix~\(P\) of~\(U\) is sufficient to decide
whether or not \(a\) reveals~\(b\). In this paper, we first considerably
improve the bound on~\(|P|\). We then show that there exists an efficient
algorithm for computing the relation on a given prefix. We have
implemented the algorithm and report on experiments.}
}
@inproceedings{FS-ncmip13,
address = {Cachan, France},
month = may,
year = 2013,
number = {012007},
volume = 464,
series = {Journal of Physics: Conference Series},
publisher = {{IOS} Press},
editor = {Blanc{-}F{\'e}raud, Laure and Joubert, Pierre-Yves},
acronym = {{NCMIP}'13},
booktitle = {{P}roceedings of the 3rd {I}nternational {W}orkshop on {N}ew
{C}omputational {M}ethods for {I}nverse {P}roblems ({NCMIP}'13)},
author = {Fribourg, Laurent and Soulat, Romain},
title = {Limit Cycles of Controlled Switched Systems: Existence,
Stability, Sensitivity},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FS-ncmip13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FS-ncmip13.pdf},
doi = {10.1088/1742-6596/464/1/012007},
abstract = {We present a control method which makes the trajectories
of a switched system converge to a stable limit cycle lying in a
desired region of equilibrium. The method is illustrated on the
boost DC-DC converter example. We also point out in this example
the sensitivity of limit cycles to parameter variations by showing
how the limit cycle evolves in presence of small perturbations of
some system parameters. This suggests that limit cycles are good
candidates for reliable estimations of the physical parameters of
switched systems, using an appropriate inverse approach.}
}
@inproceedings{ABHH-qest13,
address = {Buenos Aires, Argentina},
month = aug,
year = 2013,
publisher = {{IEEE} Computer Society Press},
acronym = {{QEST}'13},
booktitle = {{P}roceedings of the 10th {I}nternational
{C}onference on {Q}uantitative
{E}valuation of {S}ystems
({QEST}'13)},
author = {Akshay, S. and Bertrand, Nathalie and Haddad, Serge and
H{\'e}lou{\"e}t, Lo{\"\i}c},
title = {The steady-state control problem for Markov decision processes},
pages = {290-304},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABHH-qest13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABHH-qest13.pdf},
doi = {10.1007/978-3-642-40196-1_26},
abstract = {This paper addresses a control problem for probabilistic models
in the setting of Markov decision processes~(MDP). We~are interested in
the steady-state control problem which asks, given an ergodic MDP~\(M\)
and a distribution~\(\delta_{\text{goal}}\), whether there exists a
(history-dependent randomized) policy \(\pi\) ensuring that the
steady-state distribution of~\(M\) under~\(\pi\) is
exactly~\(\delta_{\text{goal}}\). We~first show that stationary randomized
policies suffice to achieve a given steady-state distribution. Then we
infer that the steady-state control problem is decidable for~MDP, and can
be represented as a linear program which is solvable in PTIME. This
decidability result extends to labeled MDP (LMDP) where the objective is a
steady-state distribution on labels carried by the states, and we provide
a PSPACE algorithm. We also show that a related steady-state language
inclusion problem is decidable in EXPTIME for LMDP. Finally, we prove that
if we consider MDP under partial observation (POMDP), the steady-state
control problem becomes undecidable.}
}
@inproceedings{KKS-esorics13,
address = {Egham, U.K.},
month = sep,
year = 2013,
volume = {8134},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Crampton, Jason and Jajodia, Sushil and Mayes, Keith},
acronym = {{ESORICS}'13},
booktitle = {{P}roceedings of the 18th {E}uropean {S}ymposium on
{R}esearch in {C}omputer {S}ecurity ({ESORICS}'13)},
author = {Kremer, Steve and K{\"u}nnemann, Robert and Steel, Graham},
title = {Universally Composable Key-Management},
pages = {327-344},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/KKS-esorics13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KKS-esorics13.pdf},
doi = {10.1007/978-3-642-40203-6_19},
abstract = {We present the first universally composable key-management
functionality, formalized in the GNUC framework by Hofheinz and Shoup. It
allows the enforcement of a wide range of security policies and can be
extended by diverse key usage operations with no need to repeat the
security proof. We illustrate its use by proving an implementation of a
security token secure with respect to arbitrary key-usage operations and
explore a proof technique that allows the storage of cryptographic keys
externally, a novel development in simulation-based security frameworks.}
}
@phdthesis{sankur-phd2013,
author = {Sankur, Ocan},
title = {Robustness in Timed Automata: Analysis, Synthesis, Implementation},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2013,
month = may,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/sankur-phd13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/sankur-phd13.pdf}
}
@article{FK-ijfcs13,
publisher = {World Scientific},
journal = {International Journal of Foundations of Computer Science},
author = {Fribourg, Laurent and K{\"u}hne, Ulrich},
title = {Parametric Verification and Test Coverage for Hybrid Automata
using the Inverse Method},
year = 2013,
month = feb,
volume = 24,
number = 2,
pages = {233-249},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FK-ijfcs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FK-ijfcs13.pdf},
doi = {10.1142/S0129054113400091},
abstract = {Hybrid systems combine continuous and discrete behavior. Hybrid
Automata are a powerful formalism for the modeling and verification of
such systems. A~common problem in hybrid system verification is the good
parameters problem, which consists in identifying a set of parameter
valuations which guarantee a certain behavior of a system. Recently, a
method has been presented for attacking this problem for Timed Automata.
In this paper, we show the extension of this methodology for hybrid
automata with linear and affine dynamics. The method is demonstrated with
a hybrid system benchmark from the literature.}
}
@inproceedings{CJ-formats13,
address = {Buenos Aires, Argentina},
month = aug,
year = 2013,
volume = 8053,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Braberman, V{\'\i}ctor and Fribourg, Laurent},
acronym = {{FORMATS}'13},
booktitle = {{P}roceedings of the 11th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'13)},
author = {Chatain, {\relax Th}omas and Jard, Claude},
title = {Back in Time {P}etri Nets},
pages = {91-105},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CJ-formats13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CJ-formats13.pdf},
doi = {10.1007/978-3-642-40229-6_7},
abstract = {The time progress assumption is at the core of the semantics of
real-time formalisms. It is also the major obstacle to the development of
partial-order techniques for real-time distributed systems since the
events are ordered both by causality and by their occurrence in time.
Anyway, extended free choice safe time Petri nets (TPNs) were already
identified as a class where partial order semantics behaves well. We show
that, for this class, the time progress assumption can even be dropped
(time may go back in case of concurrency), which establishes a nice
relation between partial-order semantics and time progress assumption.}
}
@inproceedings{BMS-formats13,
address = {Buenos Aires, Argentina},
month = aug,
year = 2013,
volume = 8053,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Braberman, V{\'\i}ctor and Fribourg, Laurent},
acronym = {{FORMATS}'13},
booktitle = {{P}roceedings of the 11th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'13)},
author = {Bouyer, Patricia and Markey, Nicolas and Sankur, Ocan},
title = {Robust Weighted Timed Automata and Games},
pages = {31-46},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-formats13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-formats13.pdf},
doi = {10.1007/978-3-642-40229-6_3},
abstract = {Weighted timed automata extend timed automata with cost
variables that can be used to model the evolution of various quantities.
Although cost-optimal reachability is decidable (in polynomial space) on
this model, it becomes undecidable on weighted timed games. This paper
studies cost-optimal reachability problems on weighted timed automata and
games under robust semantics. More precisely, we consider two perturbation
game semantics that introduce imprecisions in the standard semantics, and
bring robustness properties w.r.t. timing imprecisions to controllers. We
give a polynomial-space algorithm for weighted timed automata, and prove
the undecidability of cost-optimal reachability on weighted timed games,
showing that the problem is robustly undecidable.}
}
@inproceedings{HSS-concur13,
address = {Buenos Aires, Argentina},
month = aug,
year = 2013,
volume = 8052,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {D'Argenio, Pedro R. and Melgratti, Hern{\'a}n)},
acronym = {{CONCUR}'13},
booktitle = {{P}roceedings of the 24th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'13)},
author = {Haase, Christoph and Schmitz, Sylvain and Schnoebelen,
{\relax Ph}ilippe},
title = {The Power of Priority Channel Systems},
pages = {319-333},
url = {http://arxiv.org/abs/1301.5500},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HSS-corr13.pdf},
arxivpdf = {http://arxiv.org/pdf/1301.5500},
doi = {10.1007/978-3-642-40184-8_23},
abstract = {We introduce Priority Channel Systems, a new natural class of
channel systems where messages carry a numeric priority and where
higher-priority messages can supersede lower-priority messages preceding
them in the fifo communication buffers. The decidability of safety and
inevitability properties is shown via the introduction of a \emph{priority
embedding}, a~well-quasi-ordering that has not previously been used in
well-structured systems. We then show how Priority Channel Systems can
compute Fast-Growing functions and prove that the aforementioned
verification problems are \(F_{\epsilon_{0}}\)-complete.}
}
@inproceedings{SBMR-concur13,
address = {Buenos Aires, Argentina},
month = aug,
year = 2013,
volume = 8052,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {D'Argenio, Pedro R. and Melgratti, Hern{\'a}n)},
acronym = {{CONCUR}'13},
booktitle = {{P}roceedings of the 24th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'13)},
author = {Sankur, Ocan and Bouyer, Patricia and Markey, Nicolas and
Reynier, Pierre-Alain},
title = {Robust Controller Synthesis in Timed Automata},
pages = {546-560},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SBMR-concur13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SBMR-concur13.pdf},
doi = {10.1007/978-3-642-40184-8_38},
abstract = {We consider the fundamental problem of B{\"u}chi acceptance in
timed automata in a robust setting. The problem is formalised in terms of
controller synthesis: timed automata are equipped with a parametrised
game-based semantics that models the possible perturbations of the
decisions taken by the controller. We characterise timed automata that are
robustly controllable for some parameter, with a simple graph theoretic
condition, by showing the equivalence with the existence of an aperiodic
lasso that satisfies the winning condition (aperiodicity was defined and
used earlier in different contexts to characterise convergence phenomena
in timed automata). We then show decidability and PSPACE-completeness of
our problem.}
}
@inproceedings{FGH-mfcs13,
address = {Klosterneuburg, Austria},
month = aug,
year = 2013,
volume = {8087},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Chatterjee, Krishnendu and Sgall, Ji{\v{r}}{\'\i}},
acronym = {{MFCS}'13},
booktitle = {{P}roceedings of the 38th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'13)},
author = {Finkel, Alain and G{\"o}ller, Stefan and Haase, Christoph},
title = {Reachability in Register Machines with Polynomial Updates},
pages = {409-420},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FGH-mfcs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FGH-mfcs13.pdf},
ps = {FGH-mfcs13.ps},
doi = {10.1007/978-3-642-40313-2_37},
abstract = {This paper introduces a class of register machines whose
registers can be updated by polynomial functions when a transition is
taken, and the domain of the registers can be constrained by linear
constraints. This model strictly generalises a variety of known formalisms
such as various classes of Vector Addition Systems with States. Our main
result is that reachability in our class is PSPACE-complete when
restricted to one register. We moreover give a classification of the
complexity of reachability according to the type of polynomials allowed
and the geometry induced by the range-constraining formula.}
}
@article{ACK-jcss13,
publisher = {Elsevier Science Publishers},
journal = {Journal of Computer and System Sciences},
author = {Abiteboul, Serge and ten~Cate, Balder and
Katsis, Yannis},
title = {On the equivalence of distributed systems with queries and
communication},
volume = 79,
number = 6,
pages = {739-762},
year = 2013,
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ACK-jcss13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ACK-jcss13.pdf},
doi = {10.1016/j.jcss.2013.01.001},
abstract = {Distributed data management systems consist of peers that store,
exchange and process data in order to collaboratively achieve a common
goal, such as evaluating some query. We study the equivalence of such
systems. We model a distributed system by a collection of Active XML
documents, i.e., trees augmented with function calls for performing tasks
such as sending, receiving and querying data. As our model is quite
general, the equivalence problem turns out to be undecidable. However, we
exhibit several restrictions of the model, for which equivalence can be
effectively decided. We also study the computational complexity of the
equivalence problem, and present an axiomatization of equivalence, in the
form of a set of equivalence-preserving rewrite rules allowing us to
optimize a system by rewriting it into an equivalent, but possibly more
efficient system.}
}
@inproceedings{McK-dcfs13,
address = {London, Ontario, Canada},
month = jul,
year = 2013,
volume = {8031},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
acronym = {{DCFS}'13},
booktitle = {{P}roceedings of the 15th {W}orkshop on {D}escriptional
{C}omplexity of {F}ormal {S}ystems ({DCFS}'13)},
author = {McKenzie, Pierre},
title = {Can chimps go it alone?},
pages = {17},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/McK-dcfs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/McK-dcfs13.pdf},
doi = {10.1007/978-3-642-39310-5_3}
}
@inproceedings{CCD-icalp13,
address = {Riga, Latvia},
month = jul,
year = 2013,
volume = {7966},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Fomin, Fedor V. and Freivalds, R{\=u}si{\c{n}}{\v{s}}
and Kwiatkowska, Marta and Peleg, David},
acronym = {{ICALP}'13},
booktitle = {{P}roceedings of the 40th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'13)~-- {P}art~{II}},
author = {Chr{\'e}tien, R{\'e}my and Cortier, V{\'e}ronique and Delaune, St{\'e}phanie},
title = {From security protocols to pushdown automata},
pages = {137-149},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-icalp13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-icalp13.pdf},
doi = {10.1007/978-3-642-39212-2_15},
abstract = {Formal methods have been very successful in analyzing
security protocols for reachability properties such as secrecy or
authentication. In contrast, there are very few results for
equivalence-based properties, crucial for studying
e.g. privacy-like properties such as anonymity or vote
secrecy.\par
We study the problem of checking equivalence of security protocols
for an unbounded number of sessions. Since replication leads very
quickly to undecidability (even in the simple case of secrecy), we
focus on a limited fragment of protocols (standard primitives but
pairs, one variable per protocol's rules) for which the secrecy
preservation problem is known to be decidable. Surprisingly, this
fragment turns out to be undecidable for equivalence. Then,
restricting our attention to deterministic protocols, we propose
the first decidability result for checking equivalence of
protocols for an unbounded number of sessions. This result is
obtained through a characterization of equivalence of protocols in
terms of equality of languages of (generalized, real-time)
deterministic pushdown automata.}
}
@inproceedings{ABMW-icdt13,
address = {Genoa, Italy},
month = mar,
year = 2013,
publisher = {ACM Press},
editor = {Tan, Wang-Chiew and Guerrini, Giovanna and Catania, Barbara and
Gounaris, Anastasios},
acronym = {{ICDT}'13},
booktitle = {{P}roceedings of the 16th {I}nternational {C}onference on
{D}atabase {T}heory ({ICDT}'13)},
author = {Abiteboul, Serge and Bourhis, Pierre and Muscholl, Anca and Wu, Zhilin},
title = {Recursive queries on trees and data trees},
pages = {93-104},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABMW-icdt13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABMW-icdt13.pdf},
doi = {10.1145/2448496.2448509},
abstract = {The analysis of datalog programs over relational
structures has been studied in depth, most notably the problem of
containment. The analysis problems that have been considered were
shown to be undecidable with the exception of (i)~containment of
arbitrary programs in nonrecursive ones, (ii)~containment of
monadic programs, and (iii)~emptiness. In~this paper, we are
concerned with a much less studied problem, the analysis of
datalog programs over data trees. We show that the analysis of
datalog programs is more complex for data trees than for arbitrary
structures. In particular we prove that the three aforementioned
problems are undecidable for data trees. But in practice, data
trees (e.g., XML trees) are often of bounded depth. We prove that
all three problems are decidable over bounded depth data trees.
Another contribution of the paper is the study of a new form of
automata called pattern automata, that are essentially equivalent
to linear datalog programs. We use pattern automata to show that
the emptiness problem for linear monadic datalog programs with
data value inequalities is decidable over arbitrary data trees.}
}
@article{BCGJV-lmcs13,
journal = {Logical Methods in Computer Science},
author = {Bargu{\~n}{\'o}, Luis and Creus, Carles and Godoy, Guillem
and Jacquemard, Florent and Vacher, Camille},
title = {Decidable Classes of Tree Automata Mixing Local and Global
Constraints Modulo Flat Theories},
volume = 9,
number = 2,
nopages = {},
month = apr,
year = 2013,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGJV-lmcs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGJV-lmcs13.pdf},
doi = {10.2168/LMCS-9(2:1)2013},
abstract = {We define a class of ranked tree automata TABG generalizing both
the tree automata with local tests between brothers of Bogaert and Tison
(1992) and with global equality and disequality constraints (TAGED) of
Filiot et al. (2007). TABG can test for equality and disequality modulo a
given flat equational theory between brother subterms and between subterms
whose positions are defined by the states reached during a computation. In
particular, TABG can check that all the subterms reaching a given state
are distinct. This constraint is related to monadic key constraints for
XML documents, meaning that every two distinct positions of a given type
have different values. We prove decidability of the emptiness problem for
TABG. This solves, in particular, the open question of the decidability of
emptiness for TAGED. We further extend our result by allowing global
arithmetic constraints for counting the number of occurrences of some
state or the number of different equivalence classes of subterms (modulo a
given flat equational theory) reaching some state during a computation. We
also adapt the model to unranked ordered terms. As a consequence of our
results for TABG, we prove the decidability of a fragment of the monadic
second order logic on trees extended with predicates for equality and
disequality between subtrees, and cardinality.}
}
@inproceedings{BKM-lics13,
address = {New-Orleans, Louisiana, USA},
month = jun,
year = 2013,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'13},
booktitle = {{P}roceedings of the 28th
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'13)},
author = {Bollig, Benedikt and Kuske, Dietrich and Mennicke, Roy},
title = {The Complexity of Model Checking Multi-Stack Systems},
pages = {163-170},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BKM-lics13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BKM-lics13.pdf},
doi = {10.1109/LICS.2013.22},
abstract = {We consider the linear-time model-checking problem for boolean
concurrent programs with recursive procedure calls. While sequential
recursive programs are usually modeled as pushdown automata, concurrent
recursive programs involve several processes and can be naturally
abstracted as pushdown automata with multiple stacks. Their behavior can
be understood as words with multiple nesting relations, each relation
connecting a procedure call with its corresponding return. To reason about
multiply nested words, we consider the class of all temporal logics as
defined in the book by Gabbay, Hodkinson, and Reynolds~(1994). The
unifying feature of these temporal logics is that their modalities are
defined in monadic second-order~(MSO) logic. In particular, this captures
numerous temporal logics over concurrent and/or recursive programs that
have been defined so far. Since the general model checking problem is
undecidable, we restrict attention to phase bounded executions as proposed
by La~Torre, Madhusudan, and Parlato (LICS~2007). While the MSO model
checking problem in this case is non-elementary, our main result states
that the model checking (and satisfiability) problem for all MSO-definable
temporal logics is decidable in elementary time. More precisely, it is
solvable in \((n+2)\)-EXPTIME where \(n\) is the maximal level of the MSO
modalities in the monadic quantifier alternation hierarchy. We complement
this result and provide, for each level~\(n\), a~temporal logic whose
model checking problem is \(n\)-EXPSPACE-hard.}
}
@inproceedings{DFP-lics13,
address = {New-Orleans, Louisiana, USA},
month = jun,
year = 2013,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'13},
booktitle = {{P}roceedings of the 28th
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'13)},
author = {Demri, St{\'e}phane and Figueira, Diego and Praveen, M.},
title = {Reasoning about Data Repetitions with Counter Systems},
pages = {33-42},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DFP-lics13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DFP-lics13.pdf},
doi = {10.1109/LICS.2013.8},
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/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, a potentially 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{BS-lics13,
address = {New-Orleans, Louisiana, USA},
month = jun,
year = 2013,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'13},
booktitle = {{P}roceedings of the 28th
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'13)},
author = {Boral, Anudhyan and Schmitz, Sylvain},
title = {Model Checking Parse Trees},
pages = {153-162},
url = {http://arxiv.org/abs/1211.5256},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-lics13.pdf},
arxivpdf = {http://arxiv.org/pdf/1211.5256},
doi = {10.1109/LICS.2013.21},
abstract = {Parse trees are fundamental syntactic structures in both
computational linguistics and compilers construction. We argue in this
paper that, in both fields, there are good incentives for model-checking
sets of parse trees for some word according to a context-free grammar. We
put forward the adequacy of propositional dynamic logic (PDL) on trees in
these applications, and study as a sanity check the complexity of the
corresponding model-checking problem: although complete for exponential
time in the general case, we find natural restrictions on grammars for our
applications and establish complexities ranging from nondeterministic
polynomial time to polynomial space in the relevant cases.}
}
@inproceedings{ABBDF-pads13,
address = {Montreal, Canada},
month = may,
year = 2013,
publisher = {ACM Press},
editor = {Wainer, Gabriel A.},
acronym = {{PADS}'13},
booktitle = {{P}roceedings of the 1st {ACM} {SIGSIM} {C}onference on {P}rinciples of
{A}dvanced {D}iscrete {S}imulation ({PADS}'13)},
author = {Amparore, Elvio Gilberto and Barbot, Beno{\^\i}t and Beccuti,
Marco and Donatelli, Susanna and Franceschinis, Giuliana},
title = {Simulation-based Verification of Hybrid Automata Stochastic
Logic Formulas for Stochastic Symmetric Nets},
pages = {253-264},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABBDF-pads13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABBDF-pads13.pdf},
doi = {10.1145/2486092.2486124},
abstract = {The Hybrid Automata Stochastic Logic (HASL) has been recently
defined as a flexible way to express classical performance measures as well
as more complex, path-based ones (generically called {"}HASL formulas{"}).
The considered paths are executions of Generalized Stochastic Petri Nets
(GSPN), which are an extension of the basic Petri net formalism to define
discrete event stochastic processes. The computation of the HASL formulas
for a GSPN model is demanded to the COSMOS tool, that applies simulation
techniques to the formula computation. Stochastic Symmetric Nets (SSN) are
an high level Petri net formalism, of the \emph{colored} type, in which tokens can
have an identity, and it is well known that colored Petri nets allow one to
describe systems in a more compact and parametric form than basic
(uncolored) Petri nets. In this paper we propose to extend HASL and COSMOS
to support colors, so that performance formulas for SSN can be easily
defined and evaluated. This requires a new definition of the logic, to
ensure that colors are taken into account in a correct and useful manner,
and a significant extension of the COSMOS tool.}
}
@inproceedings{BHLM-dlt13,
address = {Marne-la-Vall{\'e}e, France},
month = jun,
year = 2013,
volume = {7907},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {B{\'e}al, Marie-Pierre and Carton, Olivier},
acronym = {{DLT}'13},
booktitle = {{P}roceedings of the 17th {I}nternational
{C}onference on {D}evelopments in {L}anguage {T}heory
({DLT}'13)},
author = {Bollig, Benedikt and Habermehl, Peter and Leucker, Martin and
Monmege, Benjamin},
title = {A~Fresh Approach to Learning Register Automata},
pages = {118-130},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHLM-dlt13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHLM-dlt13.pdf},
doi = {10.1007/978-3-642-38771-5_12},
abstract = {This paper provides an Angluin-style learning algorithm for a
class of register automata supporting the notion of \emph{fresh} data values.
More specifically, we introduce \emph{session automata} which are well suited for
modeling protocols in which sessions using fresh values are of major
interest, like in security protocols or ad-hoc networks. We show that
session automata (i)~have an expressiveness partly extending, partly
reducing that of register automata, (ii)~admit a symbolic regular
representation, and (iii)~have a decidable equivalence and model-checking
problem (unlike register automata). Using these results, we establish a
learning algorithm to infer session automata through membership and
equivalence queries. Finally, we strengthen the robustness of our
automaton by its characterization in monadic second-order logic.}
}
@inproceedings{BCHKS-lata13,
address = {Bilbao, Spain},
month = apr,
year = 2013,
volume = {7810},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Dediu, Adrian Horia and Mart{\'\i}n-Vide, Carlos and Truthe, Bianca},
acronym = {{LATA}'13},
booktitle = {{P}roceedings of the 7th {I}nternational {C}onference on {L}anguage
and {A}utomata {T}heory and {A}pplications ({LATA}'13)},
author = {Bollig, Benedikt and Cyriac, Aiswarya and H{\'e}lou{\"e}t,
Lo{\"\i}c and Kara, Ahmet and Schwentick, {\relax Th}omas},
title = {Dynamic Communicating Automata and Branching High-Level {MSC}s},
pages = {177-189},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCHKS-lata13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCHKS-lata13.pdf},
doi = {10.1109/REVET.2012.6195253},
abstract = {We study dynamic communicating automata~(DCA), an~extension of
classical communicating finite-state machines that allows for dynamic
creation of processes. The behavior of a DCA can be described as a set of
message sequence charts~(MSCs). While DCA serve as a model of an
implementation, we propose branching high-level MSCs~(bHMSCs) on the
specification side. Our focus is on the implementability problem: given a
bHMSC, can one construct an equivalent DCA? As this problem is
undecidable, we introduce the notion of executability, a decidable
necessary criterion for implementability. We show that executability of
bHMSCs is EXPTIME-complete. We~then identify a class of bHMSCs for which
executability effectively implies implementability.}
}
@inproceedings{CCP-cav13,
address = {Saint Petersburg, Russia},
month = jul,
year = 2013,
volume = {8044},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Sharygina, Natasha and Veith, Helmut},
acronym = {{CAV}'13},
booktitle = {{P}roceedings of the 25th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'13)},
author = {Cheval, Vincent and Cortier, V{\'e}ronique and Plet, Antoine},
title = {Lengths may break privacy~---or~how to check for
equivalences with length},
pages = {708-723},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCP-cav13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCP-cav13.pdf},
doi = {10.1007/978-3-642-39799-8_50},
abstract = {Security protocols have been successfully analyzed using
symbolic models, where messages are represented by terms and protocols by
processes. Privacy properties like anonymity or untraceability are
typically expressed as equivalence between processes. While some decision
procedures have been proposed for automatically deciding process
equivalence, all existing approaches abstract away the information an
attacker may get when observing the length of messages.\par In this paper, we
study process equivalence with length tests. We first show that, in the
static case, almost all existing decidability results (for static
equivalence) can be extended to cope with length tests. In the active
case, we prove decidability of trace equivalence with length tests, for a
bounded number of sessions and for standard primitives. Our result relies
on a previous decidability result from Cheval~\emph{et~al.} (without
length tests). Our procedure has been implemented and we have discovered a
new flaw against privacy in the biometric passport protocol.}
}
@inproceedings{HIOP-cav13,
address = {Saint Petersburg, Russia},
month = jul,
year = 2013,
volume = {8044},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Sharygina, Natasha and Veith, Helmut},
acronym = {{CAV}'13},
booktitle = {{P}roceedings of the 25th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'13)},
author = {Haase, Christoph and Ishtiaq, Samin and Ouaknine, Jo{\"e}l and Parkinson, Matthew},
title = {SeLoger: A~Tool for Graph-Based Reasoning in Separation
Logic},
pages = {790-795},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HIOP-cav13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HIOP-cav13.pdf},
doi = {10.1007/978-3-642-39799-8_55},
abstract = {This paper introduces the tool SeLoger, which is a reasoner for
satisfiability and entailment in a fragment of separation logic with
pointers and linked lists. SeLoger builds upon and extends graph-based
algorithms that have recently been introduced in order to settle both
decision problems in polynomial time. Running SeLoger on standard
benchmarks shows that the tool outperforms current state-of-the-art tools
by orders of magnitude.}
}
@inproceedings{OS-cav13,
address = {Saint Petersburg, Russia},
month = jul,
year = 2013,
volume = {8044},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Sharygina, Natasha and Veith, Helmut},
acronym = {{CAV}'13},
booktitle = {{P}roceedings of the 25th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'13)},
author = {Sankur, Ocan},
title = {Shrinktech: A~Tool for the Robustness Analysis of Timed Automata},
pages = {1006-1012},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/OS-cav13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/OS-cav13.pdf},
doi = {10.1007/978-3-642-39799-8_72},
abstract = {We present a tool for the robustness analysis of timed automata,
that can check whether a given time-abstract behaviour of a timed
automaton is still present when the guards are perturbed. The perturbation
model we consider is shrinking, which corresponds to increasing lower
bounds and decreasing upper bounds in the clock guards by parameters. The
tool synthesizes these parameters for which the given behaviour is
preserved in the new automaton if possible, and generates a
counter-example otherwise. This can be used for 1)~robustness analysis,
and for 2)~deriving implementations under imprecisions.}
}
@inproceedings{RB-cav13,
address = {Saint Petersburg, Russia},
month = jul,
year = 2013,
volume = {8044},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Sharygina, Natasha and Veith, Helmut},
acronym = {{CAV}'13},
booktitle = {{P}roceedings of the 25th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'13)},
author = {Brenguier, Romain},
title = {{PRALINE}: A~Tool for Computing Nash Equilibria in Concurrent
Games},
pages = { 890-895},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/RB-cav13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RB-cav13.pdf},
doi = {10.1007/978-3-642-39799-8_63},
abstract = {We present PRALINE, which is the first tool to compute Nash
equilibria in games played over graphs. We consider concurrent games: at
each step, players choose their actions independently. There can be an
arbitrary number of players. The preferences of the players are given by
payoff functions that map states to integers, the goal for a player is
then to maximize the limit superior of her payoff; this can be seen as a
generalization of B{\"u}chi objectives. PRALINE looks for pure Nash equilibria
in these games. It can construct the strategies of the equilibrium and
users can play against it to test the equilibrium. We give the idea behind
its implementation and present examples of its practical use.}
}
@inproceedings{RSK-pn13,
address = {Milano, Italy},
month = jun,
year = 2013,
volume = {7927},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Colom, Jos{\'e}-Manuel and Desel, J{\"o}rg},
acronym = {{PETRI~NETS}'13},
booktitle = {{P}roceedings of the 34th
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({PETRI~NETS}'13)},
author = {Rodr{\'\i}guez, C{\'e}sar and Schwoon, Stefan and Khomenko,
Victor},
title = {Contextual Merged Processes},
pages = {29-48},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/RSK-atpn13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RSK-atpn13.pdf},
doi = {10.1007/978-3-642-38697-8_3},
abstract = {We integrate two compact data structures for
representing state spaces of Petri nets: merged processes and
contextual prefixes. The resulting data structure, called
contextual merged processes (CMP), combines the advantages of the
original ones and copes with several important sources of state
space explosion: concurrency, sequences of choices, and concurrent
read accesses to shared resources. In particular, we demonstrate
on a number of benchmarks that CMPs are more compact than either
of the original data structures. Moreover, we sketch a polynomial
(in the CMP size) encoding into SAT of the model-checking problem
for reachability properties.}
}
@inproceedings{FH-pn13,
address = {Milano, Italy},
month = jun,
year = 2013,
volume = {7927},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Colom, Jos{\'e}-Manuel and Desel, J{\"o}rg},
acronym = {{PETRI~NETS}'13},
booktitle = {{P}roceedings of the 34th
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({PETRI~NETS}'13)},
author = {Fraca, Est{\'\i}baliz and Haddad, Serge},
title = { Complexity Analysis of Continuous {P}etri Nets},
pages = {170-189},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FH-pn13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FH-pn13.pdf},
doi = {10.1007/978-3-642-38697-8_10},
abstract = {At the end of the eighties, continuous Petri nets were
introduced for: (1)~alleviating the combinatory explosion triggered by
discrete Petri nets and, (2)~modelling the behaviour of physical systems
whose state is composed of continuous variables. Since then several works
have established that the computational complexity of deciding some
standard behavioural properties of Petri nets is reduced in this
framework. Here we first establish the decidability of additional
properties like boundedness and reachability set inclusion. We also design
new decision procedures for the reachability and lim-reachability problems
with a better computational complexity. Finally we provide lower bounds
characterising the exact complexity class of the boundedness, the
reachability, the deadlock freeness and the liveness problems.}
}
@inproceedings{HHM-pn13,
address = {Milano, Italy},
month = jun,
year = 2013,
volume = {7927},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Colom, Jos{\'e}-Manuel and Desel, J{\"o}rg},
acronym = {{PETRI~NETS}'13},
booktitle = {{P}roceedings of the 34th
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({PETRI~NETS}'13)},
author = {Haddad, Serge and Hennicker, Rolf and M{\o}ller, Mikael H.},
title = {Channel Properties of Asynchronously Composed {P}etri~Nets},
pages = {369-388},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HHM-pn13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HHM-pn13.pdf},
doi = {10.1007/978-3-642-38697-8_20},
abstract = {We consider asynchronously composed I/O-Petri nets (AIOPNs) with
built-in communication channels. They are equipped with a compositional
semantics in terms of asynchronous I/O-transition systems (AIOTSs)
admitting infinite state spaces. We study various channel properties that
deal with the production and consumption of messages exchanged via the
communication channels and establish useful relationships between them. In
order to support incremental design we show that the channel properties
considered in this work are preserved by asynchronous composition, i.e.
they are compositional. As a crucial result we prove that the channel
properties are decidable for AIOPNs.}
}
@inproceedings{AR-qapl2013,
address = {Rome, Italy},
volume = {117},
series = {Electronic Proceedings in Theoretical Computer Science},
month = jun,
year = 2013,
editor = {Bortolussi, Luca and Wiklicky, Herbert},
acronym = {{QAPL}'13},
booktitle = {{P}roceedings of the 11th {I}nternational
{W}orkshop on {Q}uantitative {A}spects of
{P}rogramming {L}anguages ({QAPl}'13)},
author = {Arul, Arjun and Reichert, Julien},
title = {The Complexity of Robot Games on the Integer Line},
pages = {132-148},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AR-qapl13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AR-qapl13.pdf},
doi = {10.4204/EPTCS.117.9},
abstract = {In robot games on~\(\mathbb{Z}\), two players add integers to a
counter. Each player has a finite set from which he picks the integer to
add, and the objective of the first player is to let the counter reach~\(0\).
We present an exponential-time algorithm for deciding the winner of a
robot game given the initial counter value, and prove a matching lower
bound.}
}
@inproceedings{BS-qapl2013,
address = {Rome, Italy},
volume = {117},
series = {Electronic Proceedings in Theoretical Computer Science},
month = jun,
year = 2013,
editor = {Bortolussi, Luca and Wiklicky, Herbert},
acronym = {{QAPL}'13},
booktitle = {{P}roceedings of the 11th {I}nternational
{W}orkshop on {Q}uantitative {A}spects of
{P}rogramming {L}anguages ({QAPl}'13)},
author = {Bertrand, Nathalie and Schnoebelen, {\relax Ph}ilippe},
title = {Solving stochastic B{\"u}chi games on infinite arenas with a
finite attractor},
pages = {116-131},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-qapl2013.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-qapl2013.pdf},
doi = {10.4204/EPTCS.117.8},
abstract = {We consider games played on an infinite probabilistic arena
where the first player aims at satisfying generalized B{\"u}chi objectives
almost surely, i.e., with probability one. We provide a fixpoint
characterization of the winning sets and associated winning strategies in
the case where the arena satisfies the finite-attractor property. From
this we directly deduce the decidability of these games on probabilistic
lossy channel systems.}
}
@book{AS-book13,
author = {Andr{\'e}, {\'E}tienne and Soulat, Romain},
title = {The~Inverse Method},
publisher = {Wiley-ISTE},
year = 2013,
month = jan,
isbn = {9781848214477},
note = {176~pages},
url = {http://www.iste.co.uk/index.php?f=a&ACTION=View&id=546},
abstract = {This book introduces state-of-the-art verification techniques
for real-time embedded systems, based on the inverse method for parametric
timed automata. It reviews popular formalisms for the specification and
verification of timed concurrent systems and, in particular, timed
automata as well as several extensions such as timed automata equipped
with stopwatches, linear hybrid automata and affine hybrid automata.\par
The inverse method is introduced, and its benefits for guaranteeing
robustness in real-time systems are shown. Then, it is shown how an
iteration of the inverse method can solve the good parameters problem for
parametric timed automata by computing a behavioral cartography of the
system. Different extensions are proposed particularly for hybrid systems
and applications to scheduling problems using timed automata with
stopwatches. Various examples, both from the literature and industry,
illustrate the techniques throughout the book.\par
Various parametric verifications are performed, in particular of
abstractions of a memory circuit sold by the chipset manufacturer
ST-Microelectronics, as well as of the prospective flight control system
of the next generation of spacecraft designed by ASTRIUM Space
Transportation.}
}
@article{CDH-fmsd13,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Chatterjee, Krishnendu and Doyen, Laurent and Henzinger, {\relax Th}omas A.},
title = {A~survey of partial-observation stochastic parity games},
volume = 43,
number = 2,
pages = {268-284},
month = oct,
year = 2013,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDH-fmsd13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDH-fmsd13.pdf},
doi = {10.1007/s10703-012-0164-2},
abstract = {We consider two-player zero-sum stochastic games on
graphs with \(\omega\)-regular winning conditions specified as
parity objectives. These games have applications in the design and
control of reactive systems. We survey the complexity results for
the problem of deciding the winner in such games, and in classes
of interest obtained as special cases, based on the information
and the power of randomization available to the players, on the
class of objectives and on the winning mode.\par
On the basis of information, these games can be classified as
follows: (a)~partial-observation (both players have partial view
of the game); (b)~one-sided partial-observation (one player has
partial-observation and the other player has
complete-observation); and (c)~complete-observation (both players
have complete view of the game). The one-sided partial-observation
games have two important subclasses: the one-player games, known
as partial-observation Markov decision processes~(POMDPs), and the
blind one-player games, known as probabilistic automata.\par
On the basis of randomization, (a)~the players may not be allowed
to use randomization (pure strategies), or (b)~they may choose a
probability distribution over actions but the actual random choice
is external and not visible to the player (actions invisible), or
(c)~they may use full randomization.\par
Finally, various classes of games are obtained by restricting the
parity objective to a reachability, safety, B{\"u}chi, or
coB{\"u}chi condition. We also consider several winning modes,
such as sure-winning (i.e., all outcomes of a strategy have to
satisfy the winning condition), almost-sure winning (i.e., winning
with probability~\(1\)), limit-sure winning (i.e., winning with
probability arbitrarily close to~\(1\)), and value-threshold
winning (i.e., winning with probability at least~\(v\), where
\(v\) is a given rational).}
}
@article{CDKR-fmsd13,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Chevalier, C{\'e}line and Delaune, St{\'e}phanie and
Kremer, Steve and Ryan, Mark D.},
title = {Composition of Password-based Protocols},
volume = {43},
number = {3},
pages = {369-413},
month = dec,
year = 2013,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDKR-fmsd13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDKR-fmsd13.pdf},
doi = {10.1007/s10703-013-0184-6},
abstract = {Formal and symbolic techniques are extremely useful for
modelling and analysing security protocols. They have helped to improve
our understanding of such protocols, allowed us to discover flaws, and
they also provide support for protocol design. However, such analyses
usually consider that the protocol is executed in isolation or assume a
bounded number of protocol sessions. Hence, no security guarantee is
provided when the protocol is executed in a more complex environment.\par
In this paper, we study whether password protocols can be safely composed,
even when a same password is reused. More precisely, we present a
transformation which maps a password protocol that is secure for a single
protocol session (a~decidable problem) to a protocol that is secure for an
unbounded number of sessions. Our result provides an effective strategy to
design secure password protocols: (i)~design a protocol intended to be
secure for one protocol session; (ii)~apply our transformation and obtain
a protocol which is secure for an unbounded number of sessions. Our
technique also applies to compose different password protocols allowing us
to obtain both inter-protocol and inter-session composition.}
}
@article{HMN-fi13,
publisher = {{IOS} Press},
journal = {Fundamenta Informaticae},
author = {Haddad, Serge and Mairesse, Jean and Nguyen, Hoang-Thach},
title = {Synthesis and Analysis of Product-form {P}etri Nets},
year = {2013},
volume = {122},
number = {1-2},
pages = {147-172},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HMN-fi13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HMN-fi13.pdf},
doi = {10.3233/FI-2013-786},
abstract = {For a large Markovian model, a {"}product form{"} is an explicit
description of the steady-state behaviour which is otherwise generally
untractable. Being first introduced in queueing networks, it has been
adapted to Markovian Petri nets. Here we address three relevant issues for
product-form Petri nets which were left fully or partially open:
(1)~we~provide a sound and complete set of rules for the synthesis;
(2)~we~characterise the exact complexity of classical problems like
reachability; (3)~we~introduce a new subclass for which the normalising
constant (a~crucial value for product-form expression) can be efficiently
computed.}
}
@inproceedings{BGM-fossacs13,
address = {Rome, Italy},
month = mar,
year = 2013,
volume = {7794},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Pfenning, Frank},
acronym = {{FoSSaCS}'13},
booktitle = {{P}roceedings of the 16th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'13)},
author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin},
title = {Weighted Specifications over Nested Words},
pages = {385-400},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-fossacs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-fossacs13.pdf},
doi = {10.1007/978-3-642-37075-5_25},
abstract = {This paper studies several formalisms to specify quantitative
properties of finite nested words (or~equivalently finite unranked trees).
These can be used for XML documents or recursive programs: for~instance,
counting how often a given entry occurs in an XML document, or~computing
the memory required for a recursive program execution. Our main interest
is to translate these properties, as efficiently as possible, into an
automaton, and to use this computational device to decide problems related
to the properties (e.g.,~emptiness, model checking, simulation) or to
compute the value of a quantitative specification over a given nested
word. The specification formalisms are weighted regular expressions (with
forward and backward moves following linear edges or call-return edges),
weighted first-order logic, and weighted temporal logics. We~introduce
weighted automata walking in nested words, possibly dropping\slash lifting
(reusable) pebbles during the traversal. We prove that the evaluation
problem for such automata can be done very efficiently if the number of
pebble names is small, and we also consider the emptiness problem.}
}
@article{demri-jcss13,
publisher = {Elsevier Science Publishers},
journal = {Journal of Computer and System Sciences},
author = {Demri, St{\'e}phane},
title = {On selective unboundedness of~{VASS}},
year = {2013},
volume = {79},
number = {5},
pages = {689-713},
month = aug,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/demri-jcss13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/demri-jcss13.pdf},
doi = {10.1016/j.jcss.2013.01.014},
abstract = {Numerous properties of vector addition systems with states
amount to checking the (un)boundedness of some selective feature (e.g.,
number of reversals, counter values, run lengths). Some of these features
can be checked in exponential space by using Rackoff's proof or its
variants, combined with Savitch's Theorem. However, the question is still
open for many others, e.g., regularity detection problem and
reversal-boundedness detection problem. In the paper, we introduce the
class of generalized unboundedness properties that can be verified in
exponential space by extending Rackoff's technique, sometimes in an
unorthodox way. We obtain new optimal upper bounds, for example for place
boundedness problem, reversal-boundedness detection (several variants are
present in the paper), strong promptness detection problem and regularity
detection. Our analysis is sufficiently refined so as to obtain a
polynomial-space bound when the dimension is fixed.}
}
@incollection{GLJ-hg13,
noaddress = {},
month = jan,
year = 2013,
volume = 7797,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
noacronym = {},
booktitle = {Programming Logics~-- Essays in Memory of {H}arald {G}anzinger},
editor = {Voronkov, Andrei and Weidenbach, Christoph},
author = {Goubault{-}Larrecq, Jean and Jouannaud, Jean-Pierre},
title = {The Blossom of Finite Semantic Trees},
pages = {90-122},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GLJ-hg13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLJ-hg13.pdf}
}
@phdthesis{bonnet-phd2013,
author = {Bonnet, R{\'e}mi},
title = {Theory of Well-Structured Transition Systems and Extended Vector-Addition Systems},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2013,
month = jan,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/bonnet-phd13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bonnet-phd13.pdf}
}
@techreport{rr-lsv-13-02,
author = {Doyen, Laurent and Rabinovich, Alexander},
title = {Robot games},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2013},
month = jan,
type = {Research Report},
number = {LSV-13-02},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2013-02.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2013-02.pdf},
versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2013-02-v1.pdf, 20130124},
note = {2~pages},
abstract = {We introduce robot games, and we give the simplest definition
for which decidability is open.}
}
@inproceedings{BNS-cc13,
address = {Rome, Italy},
month = mar,
year = 2013,
volume = {7791},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {De{~}Bosschere, Koen and Jhala, Ranjit},
acronym = {{CC}'13},
booktitle = {{P}roceedings of the 22nd {I}nternational {C}onference on {C}ompiler
{C}onstruction ({CC}'13)},
author = {Eberhard Bertsch and Mark-Jan Nederhof and Sylvain
Schmitz},
title = {On {LR} Parsing with Selective Delays},
pages = {244-263},
url = {http://hal.archives-ouvertes.fr/hal-00769668},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BNS-cc13.pdf},
doi = {10.1007/978-3-642-37051-9_13},
abstract = {The paper investigates an extension of LR parsing that allows
the delay of parsing decisions until a sufficient amount
of context has been processed. We provide two
characterizations for the resulting class of grammars, one
based on grammar transformations, the other on the direct
construction of a parser. We also report on experiments with
a grammar collection.}
}
@inproceedings{KS-fossacs13,
address = {Rome, Italy},
month = mar,
year = 2013,
volume = {7794},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Pfenning, Frank},
acronym = {{FoSSaCS}'13},
booktitle = {{P}roceedings of the 16th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'13)},
author = {Karandikar, Prateek and Schmitz, Sylvain},
title = {The Parametric Ordinal-Recursive Complexity of {P}ost
Embedding Problems},
pages = {273-288},
url = {http://arxiv.org/abs/1211.5259},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-fossacs13.pdf},
doi = {10.1007/978-3-642-37075-5_18},
abstract = {Post Embedding Problems are a family of decision problems based
on the interaction of a rational relation with the subword embedding
ordering, and are used in the literature to prove non multiply-recursive
complexity lower bounds. We refine the construction of Chambart and
Schnoebelen (LICS~2008) and prove parametric lower bounds depending on the
size of the alphabet.}
}
@misc{reachard-18,
author = {Finkel, Alain},
title = {REACHARD~-- Compte-rendu interm{\'e}diaire},
month = mar,
year = {2013},
note = {9~pages},
type = {Contract Report},
howpublished = {Deliverable~D2 Reachard (ANR-11-BS02-001)}
}
@article{CFM-ijfcs13,
publisher = {World Scientific},
journal = {International Journal of Foundations of Computer Science},
author = {Cadilhac, Micha{\"e}l and Finkel, Alain and McKenzie, Pierre},
title = {Unambiguous Contrained Automata},
volume = 24,
number = 7,
month = nov,
year = 2013,
pages = {1099-1116},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-ijfcs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-ijfcs13.pdf},
doi = {10.1142/S0129054113400339},
abstract = {The class of languages captured by Constrained Automata~(CA)
that are unambiguous is shown to possess more closure properties than the
provably weaker class captured by deterministic~CA. Problems decidable for
deterministic CA are nonetheless shown to remain decidable for
unambiguous~CA, and testing for regularity is added to this set of
decidable problems. Unambiguous CA~are then shown incomparable with
deterministic reversal-bounded machines in terms of expressivity, and a
deterministic model equivalent to unambiguous~CA is identified.}
}
@inproceedings{BDD-frocos13,
address = {Nancy, France},
month = sep,
year = 2013,
volume = 8152,
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
editor = {Fontaine, Pascal and Ringeissen, Christophe and Schmidt, Renate A.},
acronym = {{FroCoS}'13},
booktitle = {{P}roceedings of the 9th {I}nternational {S}ymposium on {F}rontiers of
{C}ombining {S}ystems ({FroCoS}'13)},
author = {Barrett, Clark and Demri, St{\'e}phane and Deters, Morgan},
title = {Witness runs for counter machines},
pages = {120-150},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDD-frocos13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDD-frocos13.pdf},
doi = {10.1007/978-3-642-40885-4_9},
abstract = {In this paper, we present recent results about the verification
of counter machines by using decision procedures for Presburger
arithmetic. We recall several known classes of counter machines for which
the reachability sets are Presburger-definable as well as temporal logics
with arithmetical constraints. We discuss issues related to flat counter
machines, path schema enumeration, and the use of SMT solvers.}
}
@mastersthesis{m2-stan13,
author = {Stan, Daniel},
title = {{\'E}quilibres mixtes dans les jeux concurrents},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2013},
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-stan13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/m2-stan13.pdf},
note = {29~pages}
}
@article{BS13-TSI-games,
publisher = {Herm{\`e}s},
journal = {Technique et Science Informatiques},
author = {Berwanger, Dietmar and Serre, Olivier},
editor = {Berwanger, Dietmar and Serre, Olivier},
title = {Th{\'e}orie des jeux en informatique},
booktitle = {Th{\'e}orie des jeux en informatique},
volume = 32,
number = {9-10},
year = 2013,
month = dec,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BS13-TSI-games.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BS13-TSI-games.pdf}
}
@inproceedings{GLO-fps13,
address = {La Rochelle, France},
month = oct,
year = 2013,
volume = 8352,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Danger, Jean-Luc and Debbabi, Mourad and Marion, Jean-Yves and
Garcia{-}Alfaro, Joaquin and Zincir{-}Heywood,Nur},
acronym = {{FPS}'13},
booktitle = {{R}evised {S}elected {P}apers of the 6th {I}nternational {S}ymposium on
{F}oundations and {P}ractice of {S}ecurity ({FPS}'13)},
author = {Goubault{-}Larrecq, Jean and Olivain, Julien},
title = {On~the Efficiency of Mathematics in Intrusion
Detection: The NetEntropy Case.},
pages = {3-16},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GLO-fps13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLO-fps13.pdf},
doi = {10.1007/978-3-319-05302-8_1},
abstract = {NetEntropy is a plugin to the Orchids intrusion detection tool
that is originally meant to detect some subtle attacks on implementations
of cryptographic protocols such as {SSL\slash TLS}. NetEntropy compares
the sample entropy of a data stream to a known profile, and flags any
significant variation. Our point is to stress the \emph{mathematics} behind
NetEntropy: the reason of the rather incredible precision of NetEntropy is
to be found in theorems due to Paninski and Moddemeijer.}
}
@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.",
}}
@mastersthesis{m2-hirschi,
author = {Hirschi, Lucca},
title = {Reduction of interleavings for trace equivalence checking of security protocols},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2013},
month = aug
}
@misc{JGL:stc13,
author = {Goubault{-}Larrecq, Jean},
howpublished = {Invited talk (semi-plenary speaker), Summer Topology Conference, North Bay, Ontario, CA},
month = jul,
title = {A few pearls in the theory of quasi-metric spaces},
year = {2013}
}
@misc{JGL:dga13,
author = {Goubault{-}Larrecq, Jean},
howpublished = {S{\'e}minaire DGA Innosciences. DGA, Bagneux},
month = jun,
title = {{OrchIDS}, ou : de l'importance de la s{\'e}mantique},
year = {2013}
}
@misc{JGL:at13,
author = {Goubault{-}Larrecq, Jean},
howpublished = {Invited talk, Workshop on Asymmetric Topology, Summer Topology Conference, North Bay, Ontario, CA},
month = jul,
title = {A short proof of the {Schr{\"o}der-Simpson} theorem},
year = {2013}
}
@mastersthesis{m2-Fang,
author = {Fang, Erwin},
title = {{Permissive multi-strategies in timed games}},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2013},
month = aug
}
This file was generated by bibtex2html 1.98.