@inproceedings{ABGR-datalog10,
address = {Oxford, UK},
month = mar,
year = 2011,
volume = 6702,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {de Moor, Oege and Gottlob, Georg and Furche, Tim and
Sellers, Andrew Jon},
acronym = {{D}atalog'10},
booktitle = {{R}evised {S}elected {P}apers of the 1st {I}nternational {W}orkshop
{D}atalog {R}eloaded ({D}atalog'10)},
author = {Abiteboul, Serge and Bienvenu, Meghyn and Galland, Alban
and Rousset, Marie-{\relax Ch}ristine},
title = {Distributed {D}atalog Revisited},
pages = {252-261},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGR-datalog10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGR-datalog10.pdf},
doi = {10.1007/978-3-642-24206-9_15}
}
@article{bbdfh-pe10,
publisher = {Elsevier Science Publishers},
journal = {Performance Evaluation},
author = {Baarir, Souheib and Beccuti, Marco and Dutheillet, Claude and
Franceschinis, Giuliana and Haddad, Serge},
title = {Lumping partially symmetrical stochastic models},
volume = 76,
nunmber = 1,
month = jan,
pages = {21-44},
year = 2011,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/bbdfh-pe10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bbdfh-pe10.pdf},
doi = {10.1016/j.peva.2010.09.002},
abstract = {The performance and dependability evaluation of complex systems
by means of dynamic stochastic models (e.g. Markov chains) may be impaired
by the combinatorial explosion of their state space. Among the possible
methods to cope with this problem, symmetry-based ones can be applied to
systems including several similar components. Often however these systems
are only partially symmetric: their behavior is in general symmetric
except for some local situation when the similar components need to be
differentiated.\par
In this paper two methods to efficiently analyze partially symmetrical
models are presented in a general setting and the requirements for their
efficient implementation are discussed. Some case studies are presented to
show the methods' effectiveness and their applicative interest.}
}
@article{JKV-icomp10,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Jacquemard, Florent and Klay, Francis and Vacher, Camille},
title = {Rigid Tree Automata},
volume = {209},
number = 3,
pages = {486-512},
year = 2011,
month = mar,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JKV-icomp11.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JKV-icomp11.pdf},
doi = {10.1016/j.ic.2010.11.015},
abstract = {We introduce the class of Rigid Tree Automata (RTA), an
extension of standard bottom-up automata on ranked trees with
distinguished states called rigid. Rigid states define a restriction on
the computation of RTA on trees: RTA can test for equality in subtrees
reaching the same rigid state. RTA are able to perform local and global
tests of equality between subtrees, non-linear tree pattern matching, and
restricted disequality tests as well. Properties like determinism, pumping
lemma, boolean closure, and several decision problems are studied in
detail. In particular, the emptiness problem is shown decidable in linear
time for RTA whereas membership of a given tree to the language of a given
RTA is NP-complete. Our main result is the decidability of whether a given
tree belongs to the rewrite closure of a RTA language under a restricted
family of term rewriting systems, whereas this closure is not a RTA
language. This result, one of the first on rewrite closure of languages of
tree automata with constraints, is enabling the extension of model
checking procedures based on finite tree automata techniques. Finally, a
comparison of RTA with several classes of tree automata with local and
global equality tests, and with dag automata is also provided.}
}
@article{AFFM-rsl10,
publisher = {Cambridge University Press},
journal = {Review of Symbolic Logic},
author = {Areces, Carlos and Figueira, Diego and Figueira, Santiago and
Mera, Sergio},
title = {The Expressive Power of Memory Logics},
year = {2011},
month = jun,
volume = 4,
number = 2,
pages = {290 - 318 },
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AFFM-rsl10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AFFM-rsl10.pdf},
doi = {10.1017/S1755020310000389},
abstract = {We investigate the expressive power of \emph{memory logics}.
These are modal logics extended with the possibility to store (or remove)
the current node of evaluation in (or from) a \emph{memory}, and to
perform membership tests on the current memory. From this perspective, the
hybrid logic \(\mathcal{HL}(\downarrow)\), for example, can be thought of
as a particular case of a memory logic where the memory is an indexed list
of elements of the domain.\par
This work focuses in the case where the memory is a set, and we can test
whether the current node belongs to the set or not. We prove that, in
terms of expressive power, the memory logics we discuss here lie between
the basic modal logic \(\mathcal{K}\) and \(\mathcal{HL}(\downarrow)\). We
show that the satisfiability problem of most of the logics we cover is
undecidable. The only logic with a decidable satisfiability problem is
obtained by imposing strong constraints on which elements can be
memorized.}
}
@inproceedings{CSV-vmcai11,
address = {Austin, Texas, USA},
month = jan,
year = 2011,
volume = 6538,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Jhala, Ranjit and Schmidt, David},
acronym = {{VMCAI}'11},
booktitle = {{P}roceedings of the 12th {I}nternational {C}onference on
{V}erification, {M}odel {C}hecking and {A}bstract {I}nterpretation
({VMCAI}'11)},
author = {Chadha, Rohit and Sistla, A. Prasad and Viswanathan, Mahesh},
title = {Probabilistic {B}{\"u}chi automata with non-extremal acceptance
thresholds},
pages = {103-117},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CSV-vmcai11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CSV-vmcai11.pdf},
doi = {10.1007/978-3-642-18275-4_9},
abstract = {This paper investigates the power of Probabilistic
B{\"u}chi Automata~(PBA) when the threshold probability of acceptance is
non-extremal, i.e., is a value strictly between 0 and 1. Many practical
randomized algorithms are designed to work under non-extremal threshold
probabilities and thus it is important to study power of PBAs for such
cases.\par
The paper presents a number of surprising expressiveness and decidability
results for PBAs when the threshold probability is non-extremal. Some of
these results sharply contrast with the results for extremal threshold
probabilities. The paper also presents results for Hierarchical PBAs and
for an interesting subclass of them called simple PBAs.}
}
@incollection{DR-lgtcs10,
month = jan,
year = 2011,
publisher = {Cambridge University Press},
booktitle = {Lectures in Game Theory for Computer Scientists},
editor = {Apt, Krzysztof R. and Gr{\"a}del, Erich},
author = {Doyen, Laurent and Raskin, Jean-Fran{\c{c}}ois},
title = {Games with Imperfect Information: Theory and Algorithms},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DR-lgtcs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DR-lgtcs10.pdf},
ps = {DR-lgtcs10.ps}
}
@article{GLK-mscs10,
publisher = {Cambridge University Press},
journal = {Mathematical Structures in Computer Science},
author = {Goubault{-}Larrecq, Jean and Keimel, Klaus},
title = {{C}hoquet-{K}endall-{M}atheron Theorems for Non-{H}ausdorff
Spaces},
volume = 21,
number = 3,
pages = {511-561},
month = jun,
year = 2011,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GLK-mscs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLK-mscs10.pdf},
doi = {10.1017/S0960129510000617},
abstract = {We establish Choquet-Kendall-Matheron theorems on non-Hausdorff
topological spaces. This typical result of random set theory is profitably
recast in purely topological terms, using intuitions and tools from domain
theory. We obtain three variants of the theorem, each one characterizing
distributions, in the form of continuous valuations, over relevant
powerdomains of demonic, resp. angelic, resp. erratic non-determinism.}
}
@article{BCL-jlli10,
publisher = {Kluwer Academic Publishers},
journal = {Journal of Logic, Language and Information},
author = {Bouyer, Patricia and Cassez, Franck and Laroussinie,
Fran{\c{c}}ois},
title = {Timed Modal Logics for Real-Time Systems: Specification,
Verification and Control},
volume = 20,
number = 2,
pages = {169-203},
year = 2011,
month = apr,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCL-jlli10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCL-jlli10.pdf},
doi = {10.1007/s10849-010-9127-4},
abstract = {In this paper, a timed modal logic~\(L_{c}\) is presented for
the specification and verification of real-time systems.
Several important results for~\(L_{c}\) are discussed. First
we address the model checking problem and we show that it is
an EXPTIME-complete problem. Secondly we consider
expressiveness and we explain how to express strong timed
bisimilarity and how to build characteristic formulas for
timed automata. We also propose a compositional algorithm
for~\(L_{c}\) model checking. Finally we consider several
control problems for which \(L_{c}\) can be used to check
controllability.}
}
@article{AGM-jcss11,
publisher = {Elsevier Science Publishers},
journal = {Journal of Computer and System Sciences},
author = {Abiteboul, Serge and Gottlob, Georg and Manna, Marco},
title = {Distributed {XML} design},
volume = 77,
number = 6,
pages = {936-964},
month = nov,
year = 2011,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AGM-jcss11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGM-jcss11.pdf},
doi = {10.1016/j.jcss.2011.02.003},
abstract = {A distributed XML document is an XML document that spans several
machines. We assume that a distribution design of the document tree is
given, consisting of an \emph{XML kernel-document}
\(T_{[\mathbf{f}_{1},...,\mathbf{f}_{n}]}\) where some leaves are
{"}docking points{"} for external resources providing XML subtrees
(\(\mathbf{f}_{1},...,\mathbf{f}_{n}\) standing, e.g., for Web services or
peers at remote locations). The top-down design problem consists in, given
a \emph{type} (a~schema document that may vary from a DTD to a tree
automaton) for the distributed document, {"}propagating{"} locally this
type into a collection of types, that we call \emph{typing}, while
preserving desirable properties. We also consider the bottom-up design
which consists in, given a type for each external resource, exhibiting a
global type that is enforced by the local types, again with natural
desirable properties. In the article, we lay out the fundamentals of a
theory of distributed XML design, analyze problems concerning typing
issues in this setting, and study their complexity.}
}
@article{ACKNS-tods11,
publisher = {ACM Press},
journal = {ACM Transactions on Database Systems},
author = {Abiteboul, Serge and Chan, T.-H. Hubert and Kharlamov, Evgeny
and Nutt, Werner and Senellart, Pierre},
title = {Capturing continuous data and answering aggregate
queries in probabilistic~{XML}},
volume = {36},
number = {4:25},
month = dec,
year = 2011,
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ACKNS-tods11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ACKNS-tods11.pdf},
doi = {10.1145/2043652.2043658},
abstract = {Sources of data uncertainty and imprecision are numerous. A way
to handle this uncertainty is to associate probabilistic annotations to
data. Many such probabilistic database models have been proposed, both in
the relational and in the semi-structured setting. The latter is
particularly well adapted to the management of uncertain data coming from
a variety of automatic processes. An important problem, in the context of
probabilistic XML databases, is that of answering aggregate queries
(count, sum, avg, etc.), which has received limited attention so~far. In a
model unifying the various (discrete) semi-structured probabilistic models
studied up to now, we present algorithms to compute the distribution of
the aggregation values (exploiting some regularity properties of the
aggregate functions) and probabilistic moments (especially expectation and
variance) of this distribution. We also prove the intractability of some
of these problems and investigate approximation techniques. We finally
extend the discrete model to a continuous one, in order to take into
account continuous data values, such as measurements from sensor networks,
and extend our algorithms and complexity results to the continuous case.}
}
@inproceedings{SGA-iswc11,
address = {Bonn, Germany},
month = oct,
year = 2011,
volume = 7031,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Aroyo, Lora and Welty, Chris and Alani, Harith and Taylor, Jamie
and Bernstein, Abraham and Kagal, Lalana and
Fridman{ }Noy,Natasha and Blomqvist, Eva},
acronym = {{ISWC}'11},
booktitle = {{P}roceedings of the 10th {I}nternational {S}emantic {W}eb {C}onference
({ISWC}'11)},
author = {Suchanek, Fabian M. and Gross{-}Amblard, David and
Abiteboul, Serge},
title = {Watermarking for Ontologies},
pages = {697-713},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SGA-iswc11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SGA-iswc11.pdf},
doi = {10.1007/978-3-642-25073-6_44},
abstract = {In this paper, we study watermarking methods to prove the
ownership of an ontology. Different from existing approaches, we propose
to watermark not by altering existing statements, but by removing them.
Thereby, our approach does not introduce false statements into the
ontology. We show how ownership of ontologies can be established with
provably tight probability bounds, even if only parts of the ontology are
being re-used. We finally demonstrate the viability of our approach on
real-world ontologies.}
}
@inproceedings{AGP-webdb11,
address = {Athens, Greece},
month = jun,
year = 2011,
editor = {Marian, Am{\'e}lie and Vassalos, Vasilis},
acronym = {({W}eb{DB}'11)},
booktitle = {{P}roceedings of the 14th {I}nternational {W}orkshop on the
{W}eb and {D}atabases ({W}eb{DB}'11)},
author = {Abiteboul, Serge and Galland, Alban and Polyzotis, Neoklis},
title = {Web information management with access control},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AGP-webdb11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGP-webdb11.pdf},
abstract = {We investigate the problem of sharing private information on the
Web, where the information is hosted on different machines that may use
different access control and distribution schemes. We introduce a
distributed knowledge-base model, termed WebdamExchange, that comprises
logical statements for specifying data, access control, distribution and
knowledge about other peers. The statements can be communicated,
replicated, queried, and updated, while keeping track of time and
provenance. This unified base allows applications to reason declaratively
about what data is accessible, where it resides, and how to retrieve it
securely.}
}
@inproceedings{ABKT-icde11,
editor = {Abiteboul, Serge and B{\"o}hm, Klemens and Koch, Christoph and
Tan, Kian-Lee},
author = {Abiteboul, Serge and B{\"o}hm, Klemens and Koch, Christoph and
Tan, Kian-Lee},
title = {{P}roceedings of the 27th {I}nternational {C}onference on
{D}ata {E}ngineering ({ICDE}'11)},
booktitle = {{P}roceedings of the 27th {I}nternational {C}onference on
{D}ata {E}ngineering ({ICDE}'11)},
year = 2011,
month = apr,
publisher = {{IEEE} Computer Society Press},
address = {Hannover, Germany},
doi = {10.1109/ICDE.2011.5767975},
url = {http://ieeexplore.ieee.org/xpl/tocresult.jsp?punumber=5765035}
}
@inproceedings{ACK-icdt11,
address = {Uppsala, Sweden},
month = mar,
year = 2011,
publisher = {ACM Press},
editor = {Milo, Tova},
acronym = {{ICDT}'11},
booktitle = {{P}roceedings of the 14th {I}nternational {C}onference on
{D}atabase {T}heory ({ICDT}'11)},
author = {Abiteboul, Serge and ten~Cate, Balder and Katsis, Yannis},
title = {On the equivalence of distributed systems with queries and communication},
pages = {126-137},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ACK-icdt11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ACK-icdt11.pdf},
doi = {10.1145/1938551.1938570},
abstract = {Distributed data management systems consist of peers
that store, exchange and process data in order to collaboratively
achieve a common goal, such as evaluate 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{ABV-icdt11,
address = {Uppsala, Sweden},
month = mar,
year = 2011,
publisher = {ACM Press},
editor = {Milo, Tova},
acronym = {{ICDT}'11},
booktitle = {{P}roceedings of the 14th {I}nternational {C}onference on
{D}atabase {T}heory ({ICDT}'11)},
author = {Abiteboul, Serge and Bourhis, Pierre and Vianu, Victor},
title = {Comparing workflow specification languages: a~matter of views},
pages = {78-89},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABV-icdt11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABV-icdt11.pdf},
doi = {10.1145/1938551.1938564},
abstract = {We address the problem of comparing the expressiveness
of workflow specification formalisms using a notion of view of a
workflow. Views allow to compare widely different workflow systems
by mapping them to a common representation capturing the
observables relevant to the comparison. Using this framework, we
compare the expressiveness of several workflow specification
mechanisms, including automata, temporal constraints, and
pre-and-post conditions, with XML and relational databases as
underlying data models. One surprising result shows the
considerable power of static constraints to simulate apparently
much richer workflow control mechanisms.}
}
@inproceedings{DMS-iwigp11,
address = {Saarbr{\"u}cken, Germany},
month = mar,
year = 2011,
volume = 50,
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Reich, Johannes and Finkbeiner, Bernd},
acronym = {{iWIGP}'11},
booktitle = {{P}roceedings of the {I}nternational
{W}orkshop on {I}nteractions, {G}ames and {P}rotocols ({iWIGP}'11)},
author = {Doyen, Laurent and Massart, {\relax Th}ierry and Shirmohammadi, Mahsa},
title = {Synchronizing Objectives for {M}arkov Decision Processes},
pages = {61-75},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DMS-iwigp11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DMS-iwigp11.pdf}
}
@inproceedings{CD-memics11,
address = {Lednice, Czech Republic },
month = oct,
year = 2011,
volume = 7119,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Bouda, Jan and {\v{C}}ern{\'a}, Ivana and Sekanina, Luk{\'a}{\v{s}}
and Vojnar, Tom{\'a}{\v{s}}},
acronym = {{MEMICS}'11},
booktitle = {{P}roceedings of the 7th {A}nnual {D}octoral {W}orkshop on {M}athematical
and {E}ngineering {M}ethods in {C}omputer {S}cience
({MEMICS}'11)},
author = {Chatterjee, Krishnendu and Doyen, Laurent},
title = {Games and Markov Decision Processes with Mean-payoff
Parity and Energy Parity Objectives},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-memics11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-memics11.pdf},
abstract = {The analysis of games and probabilistic systems with
quantitative objectives (such as mean-payoff and energy objectives) and
\(\omega\)-regular objectives (such as parity objectives) provide the
mathematical foundation for performance analysis and verification of
various classes of systems. In this talk, we will present a survey of both
classical results and recent results about mean-payoff, energy, and parity
objectives. We will discuss about how to solve their combinations, their
inter-relationship, and mention interesting open problems.}
}
@inproceedings{BBDDR-atva11,
address = {Taipei, Taiwan},
month = oct,
year = {2011},
volume = 6996,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Bultan, Tevfik and Hsiung, Pao-Ann},
acronym = {{ATVA}'11},
booktitle = {{P}roceedings of the 9th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'11)},
author = {Brihaye, {\relax Th}omas and Bruy{\`e}re, V{\'e}ronique and
Doyen, Laurent and Ducobu, Marc and Raskin, Jean-Fran{\c{c}}ois},
title = {Antichain-based {QBF} Solving},
pages = {183-197},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBDDR-atva11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBDDR-atva11.pdf},
doi = {10.1007/978-3-642-24372-1_14}
}
@article{BCDGR-fmsd2011,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Brim, Lubos and Chaloupka, Jakub and Doyen, Laurent and
Gentilini, Raffaella and Raskin, Jean-Fran{\c{c}}ois},
title = {Faster algorithms for mean-payoff games},
year = {2011},
month = apr,
volume = {38},
number = {2},
pages = {97-118},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCDGR-fmsd2011.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCDGR-fmsd2011.pdf},
doi = {10.1007/s10703-010-0105-x}
}
@misc{JGL-tacl11,
author = {Jean Goubault{-}Larrecq},
title = {A Few Pearls in the Theory of Quasi-Metric Spaces},
year = {2011},
month = jul,
howpublished = {Invited talk, Fifth International Conference on Topology,
Algebra, and Categories in Logic (TACL'11), Marseilles,
France, July~2011}
}
@article{BDMSS-tocl11,
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
author = {Boja{\'n}czyk, Miko{\l}aj and David, Claire and Muscholl,
Anca and Schwentick, {\relax Th}omas and Segoufin, Luc},
title = {Two-variable logic on data words},
volume = 12,
number = {4:27},
nopages = {},
year = 2011,
month = jul,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDMSS-tocl11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDMSS-tocl11.pdf},
doi = {10.1145/1970398.1970403}
}
@article{KS-lmcs11,
journal = {Logical Methods in Computer Science},
author = {Kazana, Wojciech and Segoufin, Luc},
title = {First-order query evaluation on structures of
bounded degree},
volume = 7,
number = {2:20},
year = 2011,
month = jun,
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-lmcs11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-lmcs11.pdf},
doi = {10.2168/LMCS-7(2:20)2011}
}
@article{PS-lmcs11,
journal = {Logical Methods in Computer Science},
author = {Place, {\relax Th}omas and Segoufin, Luc},
title = {A decidable characterization of locally testable
tree languages},
volume = 7,
number = {4:03},
year = 2011,
month = nov,
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/PS-lmcs11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PS-lmcs11.pdf},
doi = {10.2168/LMCS-7(4:3)2011}
}
@inproceedings{AGLMP-icde11,
address = {Hannover, Germany},
month = apr,
year = 2011,
publisher = {{IEEE} Computer Society Press},
editor = {Abiteboul, Serge and B{\"o}hm, Klemens and Koch, Christoph and Tan, Kian-Lee},
acronym = {{ICDE}'11},
booktitle = {{P}roceedings of the 27th {I}nternational {C}onference on
{D}ata {E}ngineering ({ICDE}'11)},
author = {Antoine, {\'E}milien and Galland, Alban and
Lyngbaek, Kristian and Marian, Am{\'e}lie and
Polyzotis, Neoklis},
title = {Social networking on top of the WebdamExchange system},
pages = {1300-1303},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AGLMP-icde11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGLMP-icde11.pdf},
doi = {10.1109/ICDE.2011.5767939},
abstract = {The demonstration presents the WebdamExchange system,
\emph{a~distributed knowledge base management system with access rights,
localization and provenance}. This system is based on the exchange of
logical statements that describe documents, collections, access rights,
keys and localization information and updates of this data.\par We
illustrate how the model can be used in a social-network context to help
users keep control on their data on the web. In particular, we show how
users within very different schemes of data-distribution (centralized,
dht, unstructured P2P,~etc.) can still transparently collaborate while
keeping a good control over their own data.}
}
@inproceedings{ABGA-pods11,
address = {Athens, Greece},
month = jun,
year = 2011,
publisher = {ACM Press},
editor = {Lenzerini, Maurizio and Schwentick, {\relax Th}omas},
acronym = {{PODS}'11},
booktitle = {{P}roceedings of the 30th {A}nnual
{ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium
on {P}rinciples of {D}atabase {S}ystems
({PODS}'11)},
author = {Abiteboul, Serge and Bienvenu, Meghyn and
Galland, Alban and Antoine, {\'E}milien},
title = {A rule-based language for Web data management},
pages = {293-304},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGA-pods11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGA-pods11.pdf},
doi = {10.1145/1989284.1989320},
abstract = {There is a new trend to use Datalog-style rule-based languages
to specify modern distributed applications, notably on the Web. We
introduce here such a language for a distributed data model where peers
exchange messages (i.e.,~logical facts) as well as rules. The model is
formally defined and its interest for distributed data management is
illustrated through a variety of examples. A~contribution of our work is a
study of the impact on expressiveness of {"}delegations{"} (the
installation of rules by a peer in some other peer) and explicit
timestamps. We also validate the semantics of our model by showing that
under certain natural conditions, our semantics converges to the same
semantics as the centralized system with the same rules. Indeed, we show
this is even true when updates are considered.}
}
@techreport{LSV-11-24,
author = {Arnaud, Mathilde and Cortier, V{\'e}ronique and Delaune, St{\'e}phanie},
title = {Modeling and Verifying Ad~Hoc Routing Protocols},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2011},
month = dec,
type = {Research Report},
number = {LSV-11-24},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2011-24.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2011-24.pdf},
versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2011-24-v1.pdf, 20111220},
note = {66~pages},
abstract = {Mobile ad hoc networks consist of mobile wireless devices which
autonomously organize their infrastructure. In such networks, a central
issue, ensured by routing protocols, is to find a route from one device to
another. Those protocols use cryptographic mechanisms in order to prevent
malicious nodes from compromising the discovered route.\par
Our contribution is twofold. We first propose a calculus for modeling and
reasoning about security protocols, including in particular secured
routing protocols. Our calculus extends standard symbolic models to take
into account the characteristics of routing protocols and to model
wireless communication in a more accurate way. Our second main
contribution is a decision procedure for analyzing routing protocols for
any network topology. By using constraint solving techniques, we show that
it is possible to automatically discover (in~NPTIME) whether there exists
a network topology that would allow malicious nodes to mount an attack
against the protocol, for a bounded number of sessions. We also provide a
decision procedure for detecting attacks in case the network topology is
given a priori. We demonstrate the usage and usefulness of our approach by
analyzing protocols of the literature, such as SRP applied to DSR and
SDMSR.}
}
@phdthesis{bourhis-phd2011,
author = {Bourhis, Pierre},
title = {On the dynamics of active documents for distributed data management},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2011,
month = feb,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/bourhis-these.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bourhis-these.pdf}
}
@phdthesis{arnaud-phd2011,
author = {Arnaud, Mathilde},
title = {Formal verification of secured routing protocols},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2011,
month = dec,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/arnaud-these11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/arnaud-these11.pdf}
}
@phdthesis{ciobaca-phd2011,
author = {Ciob{\^a}c{\u{a}}, {\c{S}}tefan},
title = {Automated Verification of Security Protocols
with Appplications to Electronic Voting},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2011,
month = dec,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ciobaca-these11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ciobaca-these11.pdf}
}
@techreport{lsv-11-23,
author = {Lozes, {\'E}tienne and Villard, Jules},
title = {Sharing Contract-Obedient Endpoints},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2011},
month = dec,
type = {Research Report},
number = {LSV-11-23},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2011-23.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2011-23.pdf},
versions = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2011-23-v1.pdf, 20111207},
note = {42~pages},
abstract = {Most of the existing verification techniques for programs based
on message passing suppose either that channel endpoints are used in a
linear fashion, where at most one thread can be considered as the owner of
an endpoint at any given time, or that endpoints may be used arbitrarily
by any number of threads. The former approach forbids the sharing of
channels, while the latter limits what is provable about programs, since
no constraint is put on the usage of channels. In this paper, we propose a
midpoint between these techniques by extending a previously published
proof system based on separation logic to allow the sharing of endpoints.
We identify two independent mechanisms for supporting sharing: the
standard technique based on reasoning with permissions, and a new
technique based on what we call ownership on demand. We formalize these
two techniques in a proof system, illustrate them on several examples, and
we extend Villard's semantics and soundness proofs to support sharing.}
}
@article{BCJST-ijis11,
publisher = {Springer},
journal = {International Journal on Information Security},
author = {Backes, Michael and Cervesato, Iliano and Jaggard, Aaron and
Scedrov, Andre and Tsay, Joe-Kai},
title = {Cryptographically sound security proofs for basic and public-key
{K}erberos},
pages = {107-134},
volume = {10},
number = {2},
year = {2011},
month = jun,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCJST-ijis11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCJST-ijis11.pdf},
doi = {10.1007/s10207-011-0125-6}
}
@inproceedings{ILV-imacc11,
address = {Oxford, UK},
month = dec,
year = 2011,
volume = {7089},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Chen, Liqun},
acronym = {{IMACC}'11},
booktitle = {{P}roceedings of the 13th {IMA} {I}nternational {C}onference
on {C}ryptography and {C}oding
({IMACC}'11)},
author = {Izabach{\`e}ne, Malika and Libert, Beno{\^\i}t and
Vergnaud, Damien},
title = {Block-wise {P}-Signatures and Non-Interactive Anonymous
Credentials with Efficient Attributes},
pages = {431-450},
doi = {10.1007/978-3-642-25516-8_26},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ILV-imacc11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ILV-imacc11.pdf},
abstract = {Anonymous credentials are protocols in which users obtain
certificates from organizations and subsequently demonstrate their
possession in such a way that transactions carried out by the same user
cannot be linked. We present an anonymous credential scheme with
non-interactive proofs of credential possession where credentials are
associated with a number of attributes. Following recent results of
Camenisch and Gro\ss{} (CCS~2008), the proof simultaneously convinces the
verifier that certified attributes satisfy a certain predicate. Our
construction relies on a new kind of P-signature, termed \emph{block-wise
P-signature}, that allows a user to obtain a signature on a committed
vector of messages and makes it possible to generate a short witness that
serves as a proof that the signed vector satisfies the predicate.
A~non-interactive anonymous credential is obtained by combining our
\emph{block-wise} P-signature scheme with the Groth-Sahai proof system. It
allows efficiently proving possession of a credential while simultaneously
demonstrating that underlying attributes satisfy a predicate corresponding
to the evaluation of inner products (and therefore disjunctions or
polynomial evaluations). The security of our scheme is proved in the
standard model under non-interactive assumptions.}
}
@book{LPS-book11,
author = {Luccio, Fabrizio and Pagli, Linda and Steel, Graham},
title = {Mathematical and Algorithmic Foundations of the Internet},
publisher = {CRC Press},
year = 2011,
month = jul,
url = {https://www.crcpress.com/9781439831380}
}
@incollection{steel-crypt2011,
author = {Steel, Graham},
title = {Formal Analysis of Security~{API}s},
booktitle = {Encyclopedia of Cryptography and Security},
edition = {2nd},
editor = {van Tilborg, Henk C. A. and Jajodia, Sushil},
year = {2011},
pages = {492-494},
publisher = {Springer},
doi = {10.1007/978-1-4419-5906-5_873}
}
@inproceedings{JKS-frocos11,
address = {Saarbr{\"u}cken, Germany},
month = oct,
year = 2011,
volume = 6989,
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
editor = {Tinelli, Cesare and Sofronie-Stokkermans, Viorica},
acronym = {{FroCoS}'11},
booktitle = {{P}roceedings of the 8th {I}nternational {S}ymposium on {F}rontiers of
{C}ombining {S}ystems ({FroCoS}'11)},
author = {Jacquemard, Florent and Kojima, Yoshiharu and Sakai, Masahiko},
title = {Controlled Term Rewriting},
pages = {179-194},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/JKS-frocos11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JKS-frocos11.pdf},
doi = {},
abstract = {Motivated by the problem of verification of imperative tree
transformation programs, we study the combination, called controlled term
rewriting systems~(CTRS), of term rewriting rules with constraints
selecting the possible rewrite positions. These constraints are specified,
for each rewrite rule, by a selection automaton which defines a set of
positions in a term based on tree automata computations.\par
We show that reachability is PSPACE-complete for so-called monotonic CTRS,
such that the size of every left-hand-side of every rewrite rule is larger
or equal to the size of the corresponding right-hand-side, and also for
the class of context-free non-collapsing CTRS, which transform CF tree
language into CF tree languages.\par
When allowing size-reducing rules, reachability becomes undecidable, even
for flat CTRS (both sides of rewrite rules are of depth at most one) when
restricting to words (i.e. function symbols have arity at most one), and
for ground CTRS (rewrite rules have no variables).\par
We also consider a restricted version of the control such that a position
is selected if the sequence of symbols on the path from that position to
the root of the tree belongs to a given regular language. This restriction
enables decision results in the above cases.}
}
@phdthesis{jacquemard-HDR11,
author = {Jacquemard, Florent},
title = {Extended Tree Automata for the Verification of Infinite State Systems},
year = 2011,
month = nov,
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-fj11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/hdr-fj11.pdf}
}
@article{CSV-lmcs11,
journal = {Logical Methods in Computer Science},
author = {Chadha, Rohit and Sistla, A. Prasad and Viswanathan, Mahesh},
title = {Power of Randomization in Automata on Infinite Strings},
year = {2011},
month = sep,
volume = {7},
number = {3:22},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CSV-lmcs11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CSV-lmcs11.pdf},
doi = {10.2168/LMCS-7(3:22)2011},
abstract = {Probabilistic B{\"u}chi Automata~(PBA) are randomized,
finite state automata that process input strings of
infinite length. Based on the threshold chosen for
the acceptance probability, different classes of
languages can be defined. In this paper, we present
a number of results that clarify the power of such
machines and properties of the languages they
define. The broad themes we focus on are as
follows. We present results on the decidability and
precise complexity of the emptiness, universality
and language containment problems for such machines,
thus answering questions central to the use of these
models in formal verification. Next, we characterize
the languages recognized by PBAs topologically,
demonstrating that though general PBAs can recognize
languages that are not regular, topologically the
languages are as simple as \(\omega\)-regular
languages. Finally, we introduce Hierarchical PBAs,
which are syntactically restricted forms of PBAs
that are tractable and capture exactly the class of
\(\omega\)-regular languages.}
}
@inproceedings{FRS-infinity11,
address = {Taipei, Taiwan},
month = oct,
year = 2011,
volume = 73,
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Chen, Yu-Fang and Wang, Chao},
acronym = {{INFINITY}'11},
booktitle = {{P}roceedings of the 13th {I}nternational
{W}orkshops on {V}erification of {I}nfinite
{S}tate {S}ystems
({INFINITY}'11)},
author = {Fribourg, Laurent and Revol, Bertrand and Soulat, Romain},
title = {Synthesis of Switching Rules for Ensuring Reachability
Properties of Sampled Linear Systems},
pages = {35-48},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FRS-infinity11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FRS-infinity11.pdf},
doi = {10.4204/EPTCS.73.6},
abstract = {We consider here systems with piecewise linear dynamics that are
periodically sampled with a given period~\(\tau\). At each sampling time,
the mode of the system, i.e., the parameters of the linear dynamics, can
be switched, according to a switching rule. Such systems can be modelled
as a special form of hybrid automata, called {"}switched systems{"}, that
are automata with an \emph{infinite} real state space. The problem is to
find a switching rule that guarantees the system to still be in a given
area~\(V\) at the next sampling time, and so on indefinitely. In this
paper, we will consider two approaches: the~\emph{indirect} one that
abstracts the system under the form of a finite discrete event system, and
the \emph{direct} one that works on the continuous state space.\par
Our methods rely on previous works, but we specialize them to a simplified
context (linearity, periodic switching instants, absence of control
input), which is motivated by the features of a focused case study:
a~DC-DC boost converter built by electronics laboratory SATIE
(ENS~Cachan). Our enhanced methods allow us to treat successfully this
real-life example.}
}
@mastersthesis{kumardhar-master,
author = {Kumar Dhar, Amit},
title = {Counter Systems with {P}resburger-definable Reachability Sets:
Decidability and Complexity},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2011},
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/akd11-m2.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/akd11-m2.pdf}
}
@inproceedings{BD-frocos11,
address = {Saarbr{\"u}cken, Germany},
month = oct,
year = 2011,
volume = 6989,
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
editor = {Tinelli, Cesare and Sofronie-Stokkermans, Viorica},
acronym = {{FroCoS}'11},
booktitle = {{P}roceedings of the 8th {I}nternational {S}ymposium on {F}rontiers of
{C}ombining {S}ystems ({FroCoS}'11)},
author = {Bersani, Marcello and Demri, St{\'e}phane},
title = {The complexity of reversal-bounded model-checking},
pages = {71-86},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BD-frocos11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BD-frocos11.pdf},
doi = {10.1007/978-3-642-24364-6_6},
abstract = {We study model-checking problems on counter systems when guards
are quantifier-free Presburger formulae, the specification
languages are LTL-like dialects with arithmetical
constraints and the runs are restricted to reversal-bounded
ones. We introduce a generalization of reversal-boundedness
and we show the NExpTime-completeness of the
reversal-bounded model-checking problem as well as for
related reversalbounded reachability problems. As a
by-product, we show the effective Presburger definability
for sets of configurations for which there is a
reversal-bounded run verifying a given temporal formula. Our
results generalize existing results about reversal-bounded
counter automata and provides a uniform and more general
framework.}
}
@phdthesis{chambart-phd2011,
author = {Chambart, Pierre},
title = {Du Probl{\`e}me de sous-mot de {P}ost et de la complexit{\'e} des canaux non
fiables},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2011,
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/chambart-these11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/chambart-these11.pdf}
}
@phdthesis{galland-phd2011,
author = {Galland, Alban},
title = {Distributed Data Management with Access Control},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2011,
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/galland-these11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/galland-these11.pdf}
}
@book{webdam2011,
author = {Abiteboul, Serge and Manolescu, Ioana and
Rigaux, {\relax Ph}ilippe and Rousset, Marie-{\relax Ch}ristine
and Senellart, Pierre},
title = {Web Data Management},
year = 2011,
publisher = {Cambridge University Press},
url = {http://webdam.inria.fr/Jorge/}
}
@article{UW-lmcs11,
journal = {Logical Methods in Computer Science},
author = {Ummels, Michael and Wojtczak, Dominik},
title = {The Complexity of {N}ash Equilibria in Stochastic Multiplayer Games},
year = {2011},
month = sep,
volume = {7},
number = {3:20},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/UW-lmcs11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/UW-lmcs11.pdf},
doi = {10.2168/LMCS-7(3:20)2011},
abstract = {We analyse the computational complexity of finding Nash
equilibria in turn-based stochastic multiplayer games with omega-regular
objectives. We show that restricting the search space to equilibria whose
payoffs fall into a certain interval may lead to undecidability. In
particular, we prove that the following problem is undecidable: Given a
game~\(G\), does there exist a Nash equilibrium of~\(G\) where
Player~\(0\) wins with probability~\(1\)? Moreover, this problem remains
undecidable when restricted to pure strategies or (pure) strategies with
finite memory. One way to obtain a decidable variant of the problem is to
restrict the strategies to be positional or stationary. For the complexity
of these two problems, we obtain a common lower bound of NP and upper
bounds of NP and PSPACE respectively. Finally, we single out a special
case of the general problem that, in many cases, admits an efficient
solution. In particular, we prove that deciding the existence of an
equilibrium in which each player either wins or loses with
probability~\(1\) can be done in polynomial time for games where the
objective of each player is given by a parity condition with a bounded
number of priorities.}
}
@techreport{lsv-11-20,
author = {Berwanger, Dietmar and Kaiser, {\L}ukasz and Le{\ss}enich, Simon},
title = {Imperfect Recall and Counter Games},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2011},
month = oct,
type = {Research Report},
number = {LSV-11-20},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2011-20.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2011-20.pdf},
note = {21~pages},
abstract = {We study a class of omega-regular games with imperfect
information and imperfect recall, and present a
solution method which relies on the
MSO-compatibility of graph unfoldings. Furthermore,
we show a reduction from a large class of counter
parity games to such games with imperfect recall.
By combining the two results, we obtain the first
elementary algorithm for solving counter parity
games, which provides substantially improved
complexity bounds for several problems in
computational logic.}
}
@phdthesis{dacosta-phd2011,
author = {Da{~}Costa, Arnaud},
title = {Propri{\'e}t{\'e}s de jeux multi-agents},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2011,
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/dacosta-these11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/dacosta-these11.pdf}
}
@mastersthesis{pasaila-master,
author = {Pasail{\u{a}}, Daniel},
title = {Verifying equivalence properties of security protocols},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2011},
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/dp11-m2.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/dp11-m2.pdf}
}
@mastersthesis{degriek-master,
author = {Degrieck, Jan},
title = {R{\'e}duction de graphes pour l'analyse de protocoles de routage
s{\'e}curis{\'e}s},
school = {{M}aster {P}arisien de {R}echerche en
{I}nformatique, Paris, France},
type = {Rapport de {M}aster},
year = {2011},
month = sep,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/jd11-m2.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/jd11-m2.pdf}
}
@inproceedings{CFM-ncma11,
address = {Milano, Italy},
month = jul,
year = 2011,
volume = 282,
series = {books@ocg.at},
publisher = {Austrian Computer Society},
editor = {Freund, Rudolf and Holzer, Markus and Mereghetti, Carlo
and Otto, Friedrich and Palano, Beatrice},
acronym = {{NCMA}'11},
booktitle = {{P}roceedings of the 3rd {W}orkshop on {N}on-{C}lassical {M}odels
of {A}utomata and {A}pplications ({NCMA}'11)},
author = {Cadilhac, Micha{\"e}l and Finkel, Alain and McKenzie, Pierre},
title = {On the Expressiveness of {P}arikh Automata and Related Models},
pages = {103-119},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-ncma11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-ncma11.pdf},
doi = {}
}
@inproceedings{CFM-words11,
address = {Prague, Czech Republic},
month = sep,
year = 2011,
volume = {63},
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Ambro{\v{z}}, Petr and Holub, {\v{S}}t{\v{e}}p{\'a}n and
Mas{\'a}kov{\'a}, Zuzana},
acronym = {{WORDS}'11},
booktitle = {{P}roceedings of the 8th {I}nternational {C}onference {WORDS} ({WORDS}'11)},
author = {Cadilhac, Micha{\"e}l and Finkel, Alain and McKenzie, Pierre},
title = {Bounded {P}arikh Automata},
pages = {93-102},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-words11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CFM-words11.pdf},
doi = {10.4204/EPTCS.63.13}
}
@inproceedings{SR-dcfs11,
address = {Limburg, Germany},
month = jul,
year = 2011,
volume = {6808},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Holzer, Markus and Kutrib, Martin and Pighizzini, Giovanni},
acronym = {{DCFS}'11},
booktitle = {{P}roceedings of the 13th {I}nternational {W}orkshop on
{D}escriptional {C}omplexity of {F}ormal {S}ystems ({DCFS}'11)},
author = {Schwoon, Stefan and Rodr{\'\i}guez, C{\'e}sar},
title = {Construction and {SAT}-based verification
of Contextual Unfoldings},
pages = {34-42},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SR-dcfs11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SR-dcfs11.pdf},
doi = {10.1007/978-3-642-22600-7_3},
nonote = {Invited paper},
abstract = {Unfoldings succinctly represent the set of reachable markings of
a Petri net. Here, we shall consider the case of contextual nets, which
extend Petri nets with read arcs, and which are more suitable to represent
the case of concurrent read access. We discuss the problem of
(efficiently) constructing unfoldings of such nets. On the basis of these
unfoldings, various verification problems can be encoded as satisfiability
problems in propositional logic.}
}
@inproceedings{HKS-gandalf11,
address = {Minori, Italy},
month = jun,
year = 2011,
volume = 54,
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {D'Agostino, Giovanna and La{~}Torre, Salvatore},
acronym = {{GandALF}'11},
booktitle = {{P}roceedings of the 2nd {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification
({GandALF}'11)},
author = {Haar, Stefan and Kern, Christian and Schwoon, Stefan},
title = {Computing the Reveals Relation in Occurrence Nets},
pages = {31-44},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HKS-gandalf11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HKS-gandalf11.pdf},
doi = {10.4204/EPTCS.54.3},
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{CDS-fct11,
address = {Oslo, Norway},
month = aug,
year = 2011,
volume = 6914,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Owe, Olaf and Steffen, Martin and Telle, Jan Arne},
acronym = {{FCT}'11},
booktitle = {{P}roceedings of the 18th {I}nternational {S}ymposium
on {F}undamentals of {C}omputation {T}heory
({FCT}'11)},
author = {Chatterjee, Krishnendu and Doyen, Laurent and Singh, Rohit},
title = {On Memoryless Quantitative Objectives},
pages = {148-159},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDS-fct11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDS-fct11.pdf},
doi = {10.1007/978-3-642-22953-4_13},
abstract = {In two-player games on graph, the players construct an infinite
path through the game graph and get a reward computed by a payoff function
over infinite paths. Over weighted graphs, the typical and most studied
payoff functions compute the limit-average or the discounted sum of the
rewards along the path. Besides their simple definition, these two payoff
functions enjoy the property that memoryless optimal strategies always
exist.\par
In an attempt to construct other simple payoff functions, we define a
class of payoff functions which compute an (infinite) weighted average of
the rewards. This new class contains both the limit-average and the
discounted sum functions, and we show that they are the only members of
this class which induce memoryless optimal strategies, showing that there
is essentially no other simple payoff functions.}
}
@inproceedings{DDMM-fsttcs11,
address = {Mumbai, India},
month = dec,
year = 2011,
volume = 13,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Chakraborty, Supratik and Kumar, Amit},
acronym = {{FSTTCS}'11},
booktitle = {{P}roceedings of the 31st {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'11)},
author = {Darondeau, {\relax Ph}ilippe and Demri, St{\'e}phane and
Meyer, Roland and Morvan, {\relax Ch}ristophe},
title = {{P}etri Net Reachability Graphs: Decidability Status of {FO}
Properties},
pages = {140-151},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DDMM-fsttcs11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DDMM-fsttcs11.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2011.140},
abstract = {We investigate the decidability and complexity status of
model-checking problems on unlabelled reachability graphs of Petri nets by
considering first-order, modal and pattern-based languages without labels
on transitions or atomic propositions on markings. We consider several
parameters to separate decidable problems from undecidable ones. Not only
are we able to provide precise borders and a systematic analysis, but we
also demonstrate the robustness of our proof techniques.}
}
@inproceedings{SBM-fsttcs11,
address = {Mumbai, India},
month = dec,
year = 2011,
volume = 13,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Chakraborty, Supratik and Kumar, Amit},
acronym = {{FSTTCS}'11},
booktitle = {{P}roceedings of the 31st {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'11)},
author = {Sankur, Ocan and Bouyer, Patricia and Markey, Nicolas},
title = {Shrinking Timed Automata},
pages = {90-102},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SBM-fsttcs11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SBM-fsttcs11.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2011.90},
abstract = {We define and study a new approach to the implementability
of timed automata, where the semantics is perturbed by imprecisions and
finite frequency of the hardware. In order to circumvent these effects, we
introduce \emph{parametric shrinking} of clock constraints, which
corresponds to tightening the guards. We propose symbolic procedures to
decide the existence of (and then compute) parameters under which the
shrunk version of a given timed automaton is non-blocking and can
time-abstract simulate the exact semantics. We then define an
implementation semantics for timed automata with a digital clock and
positive reaction times, and show that for shrinkable timed automata both
properties are preserved in implementation.}
}
@inproceedings{CDK-fsttcs11,
address = {Mumbai, India},
month = dec,
year = 2011,
volume = 13,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Chakraborty, Supratik and Kumar, Amit},
acronym = {{FSTTCS}'11},
booktitle = {{P}roceedings of the 31st {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'11)},
author = {Chevalier, C{\'e}line and Delaune, St{\'e}phanie and Kremer, Steve},
title = {Transforming Password Protocols to Compose},
pages = {204-216},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDK-fsttcs11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDK-fsttcs11.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2011.204},
abstract = {Formal, symbolic techniques are extremely useful for modelling
and analysing security protocols. They improved our understanding of
security protocols, allowed to discover flaws, and 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.}
}
@inproceedings{BBMU-fsttcs11,
address = {Mumbai, India},
month = dec,
year = 2011,
volume = 13,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Chakraborty, Supratik and Kumar, Amit},
acronym = {{FSTTCS}'11},
booktitle = {{P}roceedings of the 31st {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'11)},
author = {Bouyer, Patricia and Brenguier, Romain and Markey, Nicolas
and Ummels, Michael},
title = {{N}ash Equilibria in Concurrent Games with {B}{\"u}chi Objectives},
pages = {375-386},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBMU-fsttcs11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBMU-fsttcs11.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2011.375},
abstract = {We study the problem of the existence (and computation) of Nash
equilibria in multi-player concurrent games with B{\"u}chi-definable
objectives. First, when the objectives are B{\"u}chi conditions on the
game, we prove that the existence problem can be solved in polynomial
time. In a second part, we extend our technique to objectives defined by
deterministic B{\"u}chi automata, and prove that the problem then becomes
EXPTIME-complete. We prove PSPACE-completeness for the case where the
B{\"u}chi automata are 1-weak.}
}
@inproceedings{BLP-fsttcs11,
address = {Mumbai, India},
month = dec,
year = 2011,
volume = 13,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Chakraborty, Supratik and Kumar, Amit},
acronym = {{FSTTCS}'11},
booktitle = {{P}roceedings of the 31st {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'11)},
author = {Berwanger, Dietmar and Kaiser, {\L}ukasz and Puchala, Bernd},
title = {Perfect-Information Construction for Coordination in Games},
pages = {387-398},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BLP-fsttcs11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BLP-fsttcs11.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2011.387},
abstract = {We present a general construction for eliminating imperfect
information from games with several players who coordinate against nature,
and to transform them into two-player games with perfect information while
preserving winning strategy profiles. The construction yields an infinite
game tree with epistemic models associated to nodes. To obtain a more
succinct representation, we define an abstraction based on homomorphic
equivalence, which we prove to be sound for games with observable winning
conditions. The abstraction generates finite game graphs in several
relevant cases, and leads to a new semi-decision procedure for
multi-player games with imperfect information.}
}
@incollection{FLS-fosad11,
noaddress = {},
month = sep,
year = 2011,
volume = 6858,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Aldini, Alessandro and Gorrieri, Roberto},
acronym = {{FOSAD}'{VI}},
booktitle = {{F}oundations of {S}ecurity {A}nalysis and {D}esign~-- {FOSAD}
{T}utorial {L}ectures ({FOSAD}'{VI})},
author = {Focardi, Riccardo and Luccio, Flaminia L. and Steel, Graham},
title = {An Introduction to Security {API} Analysis},
pages = {35-65},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FLS-fosad11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FLS-fosad11.pdf},
doi = {10.1007/978-3-642-23082-0_2},
abstract = {A~security API is an Application Program Interface that allows
untrusted code to access sensitive resources in a secure way. Examples of
security APIs include the interface between the tamper-resistant chip on a
smartcard (trusted) and the card reader (untrusted), the~interface between
a~cryptographic Hardware Security Module, or~HSM (trusted) and the client
machine (untrusted), and the Google maps API (an~interface between a
server, trusted by Google, and the rest of the Internet).}
}
@inproceedings{CCD-ccs11,
address = {Chicago, Illinois, USA},
month = oct,
year = 2011,
publisher = {ACM Press},
editor = {Chen, Yan and Danezis, George and Shmatikov, Vitaly},
acronym = {{CCS}'11},
booktitle = {{P}roceedings of the 18th {ACM} {C}onference
on {C}omputer and {C}ommunications {S}ecurity
({CCS}'11)},
author = {Cheval, Vincent and Comon{-}Lundh, Hubert and
Delaune, St{\'e}phanie},
title = {Trace Equivalence Decision: Negative Tests and Non-determinism},
pages = {321-330},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-ccs11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCD-ccs11.pdf},
doi = {10.1145/2046707.2046744},
abstract = {We consider security properties of cryptographic protocols that
can be modeled using the notion of trace equivalence. The notion of
equivalence is crucial when specifying privacy-type properties, like
anonymity, vote-privacy, and unlinkability.\par
In this paper, we give a calculus that is close to the applied pi calculus
and that allows one to capture most existing protocols that rely on
classical cryptographic primitives. First, we propose a symbolic semantics
for our calculus relying on constraint systems to represent infinite sets
of possible traces, and we reduce the decidability of trace equivalence to
deciding a notion of symbolic equivalence between sets of constraint
systems. Second, we develop an algorithm allowing us to decide whether two
sets of constraint systems are in symbolic equivalence or not. Altogether,
this yields the first decidability result of trace equivalence for a
general class of processes that may involve else branches and\slash or private
channels (for a bounded number of sessions).}
}
@incollection{haddad-DS11b,
author = {Haddad, Serge},
title = {Introduction to Verification},
booktitle = {Models and Analysis in Distributed Systems},
editor = {Haddad, Serge and Kordon, Fabrice and Pautet, Laurent and
Petrucci, Laure},
publisher = {John Wiley \& Sons, Ltd.},
chapter = 6,
pages = {137-154},
year = 2011
}
@incollection{DP-DS11b,
author = {Demri, St{\'e}phane and Poitrenaud, Denis},
title = {Verification of Infinite-State Systems},
booktitle = {Models and Analysis in Distributed Systems},
editor = {Haddad, Serge and Kordon, Fabrice and Pautet, Laurent and
Petrucci, Laure},
publisher = {John Wiley \& Sons, Ltd.},
chapter = 8,
pages = {221-269},
year = 2011,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DP-DS11b.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DP-DS11b.pdf}
}
@book{HKPP-DS11a,
editor = {Haddad, Serge and Kordon, Fabrice and Pautet, Laurent and
Petrucci, Laure},
title = {Distributed Systems Design and Algorithms},
publisher = {John Wiley \& Sons, Ltd.},
year = {2011},
url = {http://www.iste.co.uk/index.php?f=a&ACTION=View&id=415}
}
@book{HKPP-DS11b,
editor = {Haddad, Serge and Kordon, Fabrice and Pautet, Laurent and
Petrucci, Laure},
title = {Models and Analysis in Distributed Systems},
publisher = {John Wiley \& Sons, Ltd.},
year = {2011},
url = {http://www.iste.co.uk/index.php?f=a&ACTION=View&id=416}
}
@inproceedings{ECGJ-msr11,
address = {Lille, France},
month = nov,
year = 2011,
number = {1-3},
volume = {45},
series = {Journal Europ{\'e}en des Syst{\`e}mes Automatis{\'e}s},
publisher = {Herm{\`e}s},
editor = {Craye, {\'E}tienne and Gamati{\'e}, Abdoulaye},
acronym = {{MSR}'11},
booktitle = {{A}ctes du 8{\`e}me {C}olloque sur la
{M}od{\'e}lisation des {S}yst{\`e}mes
{R}{\'e}actifs
({MSR}'11)},
author = {Echeveste, Jod{\'e} and Cont, Arshia and Giavitto,
Jean-Louis and Jacquemard, Florent},
title = {Formalisation des relations temporelles entre une partition et une
performance musicale dans un contexte d'accompagnement automatique},
pages = {109-124},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ECGJ-msr11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ECGJ-msr11.pdf},
doi = {10.3166/jesa.45.109-124},
abstract = {We sketch the real-time features required by automatic musical
accompaniment seen as a reactive system. We formalize the datation of
musical event taking into account the various temporal scales used in
music. Various strategies for the handling of synchronization constraints
and the handling of errors are presented.}
}
@inproceedings{BHP-msr11,
address = {Lille, France},
month = nov,
year = 2011,
number = {1-3},
volume = {45},
series = {Journal Europ{\'e}en des Syst{\`e}mes Automatis{\'e}s},
publisher = {Herm{\`e}s},
editor = {Craye, {\'E}tienne and Gamati{\'e}, Abdoulaye},
acronym = {{MSR}'11},
booktitle = {{A}ctes du 8{\`e}me {C}olloque sur la
{M}od{\'e}lisation des {S}yst{\`e}mes
{R}{\'e}actifs
({MSR}'11)},
author = {Barbot, Beno{\^\i}t and Haddad, Serge and Picaronny, Claudine},
title = {{\'E}chantillonnage pr{\'e}f{\'e}rentiel pour le model checking statistique},
pages = {237-252},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-msr11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-msr11.pdf},
doi = {10.3166/jesa.45.237-252},
abstract = {The statistical model checking can be usefully substituted for
numerical model checking when the models to be studied are huge. However
the statistical approach cannot evaluate too small probabilities. In order
to solve the problem, we develop here a new approach based on importance
sampling. While most of the techniques related to importance sampling are
based on heuristics, we establish theoretical results under some
hypotheses. These results ensure a reduction of the variance during
application of importance sampling. We also characterize situations that
fulfill the hypotheses and we extend our approach for handling other
situations but then without theoretical guarantee. We have implemented
this approach with the tool \textsc{Cosmos} after some extensions. At~last
we have evaluated this approach for two examples and analysed the
experimentations.}
}
@inproceedings{BMS-formats11,
address = {Aalborg, Denmark},
month = sep,
year = 2011,
volume = 6919,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Fahrenberg, Uli and Tripakis, Stavros},
acronym = {{FORMATS}'11},
booktitle = {{P}roceedings of the 9th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'11)},
author = {Bouyer, Patricia and Markey, Nicolas and Sankur, Ocan},
title = {Robust Model-Checking of Timed Automata via Pumping in
Channel Machines},
pages = {97-112},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-formats11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-formats11.pdf},
doi = {10.1007/978-3-642-24310-3_8},
abstract = {Timed automata are governed by a mathematical semantics which
assumes perfectly continuous and precise clocks. This requirement is not
satised by digital hardware on which the models are implemented. In~fact,
it~was shown that the presence of imprecisions, however small they may be,
may yield extra behaviours. Therefore correctness proven on the formal
model does not imply correctness of the real system.\par
The problem of robust model-checking was then dened to circumvent this
inconsistency. It consists in computing a bound on the imprecision under
which the system will be correct.\par
In this work, we show that robust model-checking against
\(\omega\)-regular properties for timed automata can be reduced to
standard model-checking of timed automata, by computing an adequate bound
on the imprecision. This yields a new algorithm for robust model-checking
of \(\omega\)-regular properties, which is both optimal and valid for
general timed automata.}
}
@inproceedings{bonnet-RP11,
address = {Genova, Italy},
month = sep,
year = 2011,
volume = {6945},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Delzanno, Giorgio and Potapov, Igor},
acronym = {{RP}'11},
booktitle = {{P}roceedings of the 5th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'11)},
author = {Bonnet, R{\'e}mi},
title = {Decidability of {LTL} Model Checking for Vector Addition
Systems with one Zero-test},
pages = {85-95},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/bonnet-RP11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bonnet-RP11.pdf},
doi = {10.1007/978-3-642-24288-5_9},
abstract = {We consider the class of Vector Addition Systems with one
zero-test and we show that the model-checking problem for LTL is decidable
thanks to a reduction to the computability of the cover and the
decidability of reachability. Our proof uses the notion of increasing
loop, that we refine to fit the non-standard monotony of our system.}
}
@inproceedings{FK-RP11,
address = {Genova, Italy},
month = sep,
year = 2011,
volume = {6945},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Delzanno, Giorgio and Potapov, Igor},
acronym = {{RP}'11},
booktitle = {{P}roceedings of the 5th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'11)},
author = {Fribourg, Laurent and K{\"u}hne, Ulrich},
title = {Parametric Verification and Test Coverage for Hybrid Automata
Using the Inverse Method},
pages = {191-204},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FK-RP11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FK-RP11.pdf},
doi = {10.1007/978-3-642-24288-5_17},
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{AS-RP11,
address = {Genova, Italy},
month = sep,
year = 2011,
volume = {6945},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Delzanno, Giorgio and Potapov, Igor},
acronym = {{RP}'11},
booktitle = {{P}roceedings of the 5th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'11)},
author = {Andr{\'e}, {\'E}tienne and Soulat, Romain},
title = {Synthesis of Timing Parameters Satisfying Safety Properties},
pages = {31-44},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AS-RP11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AS-RP11.pdf},
doi = {10.1007/978-3-642-24288-5_5},
abstract = {Safety properties are crucial when verifying real-time
concurrent systems. When reasoning parametrically, i.e., with unknown
constants, it is of high interest to infer a set of parameter valuations
consistent with such safety properties. We present here algorithms based
on the inverse method for parametric timed automata: given a reference
parameter valuation, it infers a constraint such that, for any valuation
satisfying this constraint, the discrete behavior of the system is the
same as under the reference valuation in terms of traces, i.e.,
alternating sequences of locations and actions. These algorithms do not
guarantee the equality of the trace sets, but are significantly quicker,
synthesize larger sets of parameter valuations than the original method,
and still preserve various properties including safety (i.e.,
non-reachability) properties. Those algorithms have been implemented in
Imitator~II and applied to various examples of asynchronous circuits and
communication protocols. }
}
@techreport{lsv-11-18,
author = {Florentin, {\'E}ric and Fribourg, Laurent and K{\"u}hne, Ulrich and
Lefebvre, St{\'e}phane and Rey, {\relax Ch}ristian},
title = {{COUPLET}: Coupled Electrothermal Simulation},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2011},
month = jun,
type = {Research Report},
number = {LSV-11-18},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2011-18.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2011-18.pdf},
note = {32~pages},
abstract = {The~aim of the project COUPLET (supported by Institut
Farman) is to study the electrothermal effects of
the degradation of the metallisation layer of power
semiconductor dies. In this first technical report
of the project, we describe our work of modeling and
simulation of the behavior of a power
transistor. The die is represented by four
elementary transistors driven by a distributed gate
signal. A~simplified electrical model is used to
simulate the transistor behavior at turn-off. The
thermal model is realized by finite elements methods
and allows to estimate the maximum temperature on
each elementary transistor. By~coupling the thermal
model with the electric simulation, it is possible
to take into account silicon and metallisation
heating in the electrical model.}
}
@inproceedings{SC-unif11,
address = {Wroc{\l}aw, Poland},
month = jul,
year = 2011,
editor = {Baader, Franz},
acronym = {{UNIF}'11},
booktitle = {{P}roceedings of the 25th {I}nternational
{W}orkshop on {U}nification
({UNIF}'11)},
author = {Ciob{\^a}c{\u{a}}, {\c{S}}tefan},
title = {Computing finite variants for subterm convergent rewrite systems},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SC-unif11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SC-unif11.pdf},
abstract = {Driven by an application in the verification of security
protocols, we introduce the strong finite variant property, an extention
of the finite variant property, and we show that subterm convergent
rewrite systems enjoy the strong finite variant property modulo the empty
equational theory.\par
We argue that the strong finite variant property is more natural and more
useful in practice than the finite variant property. We also compare the
two properties and we provide a prototype implementation of an algorithm
that computes a finite strongly complete set of variants for any term t
with respect to a subterm convergent rewrite system.}
}
@inproceedings{BMOU-atva11,
address = {Taipei, Taiwan},
month = oct,
year = {2011},
volume = 6996,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Bultan, Tevfik and Hsiung, Pao-Ann},
acronym = {{ATVA}'11},
booktitle = {{P}roceedings of the 9th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'11)},
author = {Bouyer, Patricia and Markey, Nicolas and Olschewski, J{\"o}rg
and Ummels, Michael},
title = {Measuring Permissiveness in Parity Games: Mean-Payoff
Parity Games Revisited},
pages = {135-149},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMOU-atva11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMOU-atva11.pdf},
doi = {10.1007/978-3-642-24372-1_11},
abstract = {We study nondeterministic strategies in parity games with the
aim of computing a most permissive winning strategy. Following earlier
work, we measure permissiveness in terms of the average
number{\slash}weight of transitions blocked by a strategy. Using a
translation into mean-payoff parity games, we prove that deciding (the
permissiveness~of) a~most permissive winning strategy is in
\(\textsf{NP}\cap\textsf{coNP}\). Along the way, we~provide a new study of
mean-payoff parity games. In particular, we give a new algorithm for
solving these games, which beats all previously known algorithms for this
problem.}
}
@inproceedings{CKVAK-qest11,
address = {Aachen, Germany},
month = sep,
year = 2011,
publisher = {{IEEE} Computer Society Press},
acronym = {{QEST}'11},
booktitle = {{P}roceedings of the 8th {I}nternational
{C}onference on {Q}uantitative
{E}valuation of {S}ystems
({QEST}'11)},
author = {Chadha, Rohit and Korthikranthi, Vijay and Viswanathan,
Mahesh and Agha, Gul and Kwon, Youngmin},
title = {Model Checking {MDP}s with a Unique Compact Invariant Set of
Distributions},
pages = {121-130},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CKVAK-qest11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CKVAK-qest11.pdf},
doi = {10.1109/QEST.2011.22},
abstract = {The semantics of Markov Decision Processes (MDPs), when viewed
as transformers of probability distributions, can described as a labeled
transition system over the probability distributions over the states of
the MDP. The MDP can be seen as defining a set of executions, where each
execution is a sequence of probability distributions. Reasoning about
sequences of distributions allows one to express properties not
expressible in logics like PCTL; examples include expressing bounds on
transient rewards and expected values of random variables, as well as
comparing the probability of being in one set of states at a given time
with another set of states. With respect to such a semantics, the problem
of checking that the MDP never reaches a bad distribution is undecidable.
In this paper, we identify a special class of MDPs called
\emph{semi-regular} MDPs that have a unique non-empty, compact, invariant
set of distributions, for which we show that checking any
\(\omega\)-regular property is decidable. Our decidability result also
implies that for semi-regular probabilistic finite automata with isolated
cut-points, the emptiness problem is decidable.}
}
@inproceedings{CD-mfcs11,
address = {Warsaw, Poland},
month = aug,
year = 2011,
volume = 6907,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Murlak, Filip and Sankowski, Piotr},
acronym = {{MFCS}'11},
booktitle = {{P}roceedings of the 36th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'11)},
author = {Chatterjee, Krishnendu and Doyen, Laurent},
title = {Energy and Mean-Payoff Parity {M}arkov
Decision Processes},
pages = {206-218},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-mfcs11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-mfcs11.pdf},
doi = {10.1007/978-3-642-22993-0_21},
abstract = {We consider Markov Decision Processes (MDPs) with mean-payoff
parity and energy parity objectives. In system design, the parity
objective is used to encode \(\omega\)-regular specifications, while the
mean-payoff and energy objectives can be used to model quantitative
resource constraints. The energy condition requires that the resource
level never drops below~\(0\), and the mean-payoff condition requires that
the limit-average value of the resource consumption is within a threshold.
While these two (energy and mean-payoff) classical conditions are
equivalent for two-player games, we~show that they differ for MDPs. We
show that the problem of deciding whether a state is almost-sure winning
(i.e., winning with probability~\(1\)) in energy parity MDPs is in
\(\textsf{NP}\cap\textsf{coNP}\), while for mean-payoff parity MDPs, the
problem is solvable in polynomial time.}
}
@inproceedings{DMS-mfcs11,
address = {Warsaw, Poland},
month = aug,
year = 2011,
volume = 6907,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Murlak, Filip and Sankowski, Piotr},
acronym = {{MFCS}'11},
booktitle = {{P}roceedings of the 36th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'11)},
author = {Doyen, Laurent and Massart, {\relax Th}ierry and
Shirmohammadi, Mahsa},
title = {Infinite Synchronizing Words for Probabilistic Automata},
pages = {278-289},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DMS-mfcs11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DMS-mfcs11.pdf},
doi = {10.1007/978-3-642-22993-0_27},
abstract = {Probabilistic automata are finite-state automata where the
transitions are chosen according to fixed probability distributions. We
consider a semantics where on an input word the automaton produces a
sequence of probability distributions over states. An~infinite word is
accepted if the produced sequence is synchronizing, i.e. the sequence of
the highest probability in the distributions tends to~\(1\). We show that
this semantics generalizes the classical notion of synchronizing words for
deterministic automata. We consider the emptiness problem, which asks
whether some word is accepted by a given probabilistic automaton, and the
universality problem, which asks whether all words are accepted. We
provide reductions to establish the PSPACE-completeness of the two
problems.}
}
@inproceedings{BCGZ-mfcs11,
address = {Warsaw, Poland},
month = aug,
year = 2011,
volume = 6907,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Murlak, Filip and Sankowski, Piotr},
acronym = {{MFCS}'11},
booktitle = {{P}roceedings of the 36th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'11)},
author = {Bollig, Benedikt and Cyriac, Aiswarya and Gastin, Paul and Zeitoun, Marc},
title = {Temporal Logics for Concurrent Recursive Programs: Satisfiability
and Model Checking},
pages = {132-144},
url = {http://hal.archives-ouvertes.fr/hal-00591139/en/},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGZ-mfcs11.pdf},
doi = {10.1007/978-3-642-22993-0_15},
abstract = {We develop a general framework for the design of temporal logics
for concurrent recursive programs. A program execution is modeled as a
partial order with multiple nesting relations. To specify properties of
executions, we consider any temporal logic whose modalities are definable
in monadic second-order logic and that, in addition, allows PDL-like path
expressions. This captures, in a unifying framework, a wide range of
logics defined for trees, nested words, and Mazurkiewicz traces that have
been studied separately. We show that satisfiability and model checking
are decidable in EXPTIME and 2EXPTIME, depending on the precise path
modalities.}
}
@inproceedings{Schmitz-fsmnlp11,
address = {Blois, France},
month = jul,
year = 2011,
publisher = {ACL Press},
editor = {Maletti, Andreas},
acronym = {{FSMNLP}'11},
booktitle = {{P}roceedings of the 9th {I}nternational {W}orkshop on
{F}inite-{S}tate {M}ethods and {N}atural {L}anguage
{P}rocessing ({FSMNLP}'11)},
author = {Sylvain Schmitz},
title = {A~Note on Sequential Rule-Based {POS} Tagging},
pages = {83-87},
url = {http://hal.archives-ouvertes.fr/hal-00600260/},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Schmitz-fsmnlp11.pdf},
abstract = {Brill's part-of-speech tagger is defined through a cascade of
leftmost rewrite rules. We revisit the compilation of such rules into a
single sequential transducer given by Roche and Schabes (\textit{Comput.
Ling.}~1995) and provide a direct construction of the minimal sequential
transducer for each individual rule.}
}
@inproceedings{BS-mfcs11,
address = {Warsaw, Poland},
month = aug,
year = 2011,
volume = 6907,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Murlak, Filip and Sankowski, Piotr},
acronym = {{MFCS}'11},
booktitle = {{P}roceedings of the 36th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'11)},
author = {Blockelet, Michel and Schmitz, Sylvain},
title = {Model-Checking Coverability Graphs of Vector Addition Systems},
pages = {108-119},
url = {http://hal.archives-ouvertes.fr/hal-00600077/},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-mfcs11.pdf},
doi = {10.1007/978-3-642-22993-0_13},
abstract = {A large number of properties of a vector addition system---for
instance coverability, boundedness, or regularity---can be decided using its
coverability graph, by looking for some characteristic pattern. We propose
to unify the known exponential-space upper bounds on the complexity of
such problems on vector addition systems, by seeing them as instances of
the model-checking problem for a suitable extension of computation tree
logic, which allows to check for the existence of these patterns. This
provides new insights into what constitutes a {"}coverability-like{"}
property.}
}
@inproceedings{Sankur-mfcs11,
address = {Warsaw, Poland},
month = aug,
year = 2011,
volume = 6907,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Murlak, Filip and Sankowski, Piotr},
acronym = {{MFCS}'11},
booktitle = {{P}roceedings of the 36th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'11)},
author = {Sankur, Ocan},
title = {Untimed Language Preservation in Timed Systems},
pages = {556-567},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/OS-mfcs11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/OS-mfcs11.pdf},
corrigendumpdf = {http://www.lsv.fr/Publis/PAPERS/PDF/OS-mfcs11-erratum.pdf},
doi = {10.1007/978-3-642-22993-0_50},
abstract = {Timed automata are a model that is extensively used in formal
verification of real-time systems. However, their mathematical semantics
is an idealization which assumes perfectly precise clocks, but does not
correspond to real hardware. In fact, it is known that imprecisions,
however small they may be, may yield extra behaviours. Several works
concentrated on a relaxation of the semantics of timed automata to model
the imprecisions of the clocks. Algorithms were given, first for safety,
then for richer linear-time properties, to decide the robustness of timed
systems, that is, the existence of a bound on the imprecisions under which
the system satisfies a given property. In this work, we study a stronger
notion of robustness: we show how to decide whether the untimed language
of a timed automaton is preserved under small enough imprecisions, and
provide a bound on the imprecision parameter.}
}
@inproceedings{Bonnet-mfcs11,
address = {Warsaw, Poland},
month = aug,
year = 2011,
volume = 6907,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Murlak, Filip and Sankowski, Piotr},
acronym = {{MFCS}'11},
booktitle = {{P}roceedings of the 36th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'11)},
author = {Bonnet, R{\'e}mi},
title = {The reachability problem for Vector Addition Systems with one zero-test},
pages = {145-157},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/RB-mfcs11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RB-mfcs11.pdf},
doi = {10.1007/978-3-642-22993-0_16},
abstract = {We consider here a variation of Vector Addition Systems where
one counter can be tested for zero. We extend the reachability proof for
Vector Addition System recently published by Leroux to this model. This
provides an alternate, more conceptual proof of the reachability problem
that was originally proved by Reinhardt.}
}
@inproceedings{NM-sies11,
address = {V{\"a}ster{\aa}s, Sweden},
month = jun,
year = 2011,
publisher = {{IEEE} Computer Society Press},
noeditor = {},
acronym = {{SIES}'11},
booktitle = {{P}roceedings of the 6th {IEEE} {I}nternational {S}ymposium
on {I}ndustrial {E}mbedded {S}ystems ({SIES}'11)},
author = {Markey, Nicolas},
title = {Robustness in Real-time Systems},
pages = {28-34},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/NM-sies11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/NM-sies11.pdf},
doi = {10.1109/SIES.2011.5953652},
abstract = {We~review several aspects of robustness of real-time systems,
and present recent results on the robust verification of timed automata.}
}
@inproceedings{BDDHP-case11,
address = {Trieste, Italy},
month = aug,
year = 2011,
publisher = {{IEEE} Robotics \& Automation Society},
noeditor = {},
acronym = {{CASE}'11},
booktitle = {{P}roceedings of the 7th {IEEE} {C}onference on {A}utomation
{S}cience and {E}ngineering ({CASE}'11)},
author = {Ballarini, Paolo and Djafri, Hilal and Duflot, Marie and
Haddad, Serge and Pekergin, Nihal},
title = {{P}etri Nets Compositional Modeling and Verification
of Flexible Manufacturing Systems},
pages = {588-593},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDDHP-case11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDDHP-case11.pdf},
doi = {10.1109/CASE.2011.6042488},
abstract = {Flexible Manufacturing Systems (FMS) are amongst the
most studied types of systems, however due to their
increasing complexity, there is still room for
improvement in their modeling and analysis. In this
paper we consider the design and the analysis of
stochastic models of FMS in two complementary
respects. First we describe a (stochastic) Petri
Nets based compositional framework which enables to
model an FMS by combination of an arbitrary number
of basic components. Second we demonstrate how
classical transient-analysis of manufacturing
systems, including reliability and performability
analysis, can be enriched by application of a novel,
sophisticated stochastic logic, namely the Hybrid
Automata Stochastic Logic (HASL). We demonstrate the
proposed methodology on an FMS example.}
}
@inproceedings{BDDHP-qest11,
address = {Aachen, Germany},
month = sep,
year = 2011,
publisher = {{IEEE} Computer Society Press},
acronym = {{QEST}'11},
booktitle = {{P}roceedings of the 8th {I}nternational
{C}onference on {Q}uantitative
{E}valuation of {S}ystems
({QEST}'11)},
author = {Ballarini, Paolo and Djafri, Hilal and Duflot, Marie and
Haddad, Serge and Pekergin, Nihal},
title = {{COSMOS}: a~Statistical Model Checker for the
Hybrid Automata Stochastic Logic},
pages = {143-144},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDDHP-qest11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDDHP-qest11.pdf},
doi = {10.1109/QEST.2011.24},
abstract = {This tool paper introduces COSMOS, a statistical model
checker for the Hybrid Automata Stochastic Logic
(HASL). HASL employs Linear Hybrid Automata (LHA), a
generalization of Deterministic Timed Automata
(DTA), to describe accepting execution paths of a
Discrete Event Stochastic Process (DESP), a class of
stochastic models which includes, but is not limited
to, Markov chains. As a result HASL verification
turns out to be a unifying framework where
sophisticated temporal reasoning is naturally
blended with elaborate reward-based analysis. COSMOS
takes as input a DESP (described in terms of a
Generalized Stochastic Petri Net), an LHA and an
expression~\(Z\) representing the quantity to be
estimated. It returns a confidence interval
estimation of~\(Z\). COSMOS is written in C++ and is
freely available to the research community.}
}
@article{BFH-ijpe11,
publisher = {RAMS Consultants},
journal = {International Journal of Performability Engineering},
author = {Beccuti, Marco and Franceschinis, Giuliana and Haddad, Serge},
title = {{MDWN}solver: A~Framework to Design and Solve {M}arkov Decision {P}etri Nets},
year = {2011},
month = sep,
volume = 7,
number = 5,
pages = {417-428},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFH-ijpe11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFH-ijpe11.pdf},
abstract = {MDWNsolver is a framework for system modeling and optimization
of performability measures based on Markov Decision Petri Net (MDPN) and
Markov Decision Well-formed Net (MDWN) formalisms, two Petri Net
extensions for high level specification of Markov Decision Processes
(MDP). It is integrated in the GreatSPN suite which provides a GUI to
design MDPN/MDWN models. From the analysis point of view, MDWNsolver uses
efficient algorithms that take advantage of system symmetries, thus
reducing the analysis complexity. In this paper the MDWNsolver framework
features and architecture are presented, and some application examples are
discussed.}
}
@inproceedings{UW-concur11,
address = {Aachen, Germany},
month = sep,
year = 2011,
volume = 6901,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Katoen, Joost-Pieter and K{\"o}nig, Barbara},
acronym = {{CONCUR}'11},
booktitle = {{P}roceedings of the 22nd
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'11)},
author = {Ummels, Michael and Wojtczak, Dominik},
title = {The Complexity of {N}ash Equilibria in Limit-Average Games},
pages = {482-496},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/UW-concur11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/UW-concur11.pdf},
doi = {10.1007/978-3-642-23217-6_32},
abstract = {We study the computational complexity of Nash equilibria in
concurrent games with limit-average objectives. In particular, we prove
that the existence of a Nash equilibrium in randomised strategies is
undecidable, while the existence of a Nash equilibrium in pure strategies
is decidable, even if we put a constraint on the payoff of the
equilibrium. Our undecidability result holds even for a restricted class
of concurrent games, where nonzero rewards occur only on terminal states.
Moreover, we show that the constrained existence problem is undecidable
not only for concurrent games but for turn-based games with the same
restriction on rewards. Finally, we prove that the constrained existence
problem for Nash equilibria in (pure or randomised) stationary strategies
is decidable and analyse its complexity.}
}
@inproceedings{Bol-concur11,
address = {Aachen, Germany},
month = sep,
year = 2011,
volume = 6901,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Katoen, Joost-Pieter and K{\"o}nig, Barbara},
acronym = {{CONCUR}'11},
booktitle = {{P}roceedings of the 22nd
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'11)},
author = {Bollig, Benedikt},
title = {An automaton over data words that captures {EMSO} logic},
pages = {171-186},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/B-concur11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/B-concur11.pdf},
doi = {10.1007/978-3-642-23217-6_12},
abstract = {We develop a general framework for the specification and
implementation of systems whose executions are words, or partial orders,
over an infinite alphabet. As a model of an implementation, we introduce
class register automata, a one-way automata model over words with multiple
data values. Our model combines register automata and class memory
automata. It has natural interpretations. In particular, it captures
communicating automata with an unbounded number of processes, whose
semantics can be described as a set of (dynamic) message sequence charts.
On the specification side, we provide a local existential monadic
second-order logic that does not impose any restriction on the number of
variables. We study the realizability problem and show that every formula
from that logic can be effectively, and in elementary time, translated
into an equivalent class register automaton.}
}
@inproceedings{RSB-concur11,
address = {Aachen, Germany},
month = sep,
year = 2011,
volume = 6901,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Katoen, Joost-Pieter and K{\"o}nig, Barbara},
acronym = {{CONCUR}'11},
booktitle = {{P}roceedings of the 22nd
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'11)},
author = {Rodr{\'\i}guez, C{\'e}sar and Schwoon, Stefan and Baldan, Paolo},
title = {Efficient contextual unfolding},
pages = {342-357},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/RSB-concur11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RSB-concur11.pdf},
doi = {10.1007/978-3-642-23217-6_23},
abstract = {A~contextual net is a Petri net extended with read arcs, which
allow transitions to check for tokens without consuming them. Contextual
nets allow for better modelling of concurrent read access than Petri nets,
and their unfoldings can be exponentially more compact than those of a
corresponding Petri net. A~constructive but abstract procedure for
generating those unfoldings was proposed in earlier work; however, no
concrete implementation existed. Here, we~close this gap providing two
concrete methods for computing contextual unfoldings, with a view to
efficiency. We report on experiments carried out on a number of
benchmarks. These show that not only are contextual unfoldings more
compact than Petri net unfoldings, but they can be computed with the same
or better efficiency, in~particular with respect to the place-replication
encoding of contextual nets into Petri nets.}
}
@inproceedings{BLMST-concur11,
address = {Aachen, Germany},
month = sep,
year = 2011,
volume = 6901,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Katoen, Joost-Pieter and K{\"o}nig, Barbara},
acronym = {{CONCUR}'11},
booktitle = {{P}roceedings of the 22nd
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'11)},
author = {Bouyer, Patricia and Larsen, Kim~G. and Markey, Nicolas and
Sankur, Ocan and Thrane, Claus},
title = {Timed automata can always be made implementable},
pages = {76-91},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BLMST-concur11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BLMST-concur11.pdf},
doi = {10.1007/978-3-642-23217-6_6},
abstract = {Timed automata follow a mathematical semantics, which
assumes perfect precision and synchrony of
clocks. Since this hypothesis does not hold in
digital systems, properties proven formally on a
timed automaton may be lost at implementation. In
order to ensure implementability, several approaches
have been considered, corresponding to different
hypotheses on the implementation platform. We
address two of these: a~timed automaton is samplable
if its semantics is preserved under a discretization
of time; it is robust if its semantics is preserved
when all timing constraints are relaxed by some
small positive parameter. We propose a construction
which makes timed automata implementable in the
above sense: From any timed automaton~\(\mathcal{A}\),
we build a timed automaton~\(\mathcal{A}'\) that
exhibits the same behaviour as~\(\mathcal{A}\), and
moreover is both robust and samplable by
construction.}
}
@inproceedings{BBBS-icalp11,
address = {Z{\"u}rich, Switzerland},
month = jul,
year = 2011,
volume = 6756,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Aceto, Luca and Henzinger, Monika and Sgall, Jir{\'\i}},
acronym = {{ICALP}'11},
booktitle = {{P}roceedings of the 38th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'11)~-- {P}art~{II}},
author = {Bertrand, Nathalie and Bouyer, Patricia and Brihaye, {\relax
Th}omas and Stainer, Am{\'e}lie},
title = {Emptiness and Universality Problems in Timed Automata with Positive Frequency},
pages = {246-257},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBBS-icalp11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBBS-icalp11.pdf},
doi = {10.1007/978-3-642-22012-8_19},
abstract = {The languages of infinite timed words accepted by timed automata
are traditionally dened using B{\"u}chi-like conditions. These acceptance
conditions focus on the set of locations visited infinitely often along a
run, but completely ignore quantitative timing aspects. In this paper we
propose a natural quantitative semantics for timed automata based on the
so-called frequency, which measures the proportion of time spent in the
accepting locations. We study various properties of timed languages
accepted with positive frequency, and in particular the emptiness and
universality problems.}
}
@inproceedings{BDGORW-icalp11,
address = {Z{\"u}rich, Switzerland},
month = jul,
year = 2011,
volume = 6756,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Aceto, Luca and Henzinger, Monika and Sgall, Jir{\'\i}},
acronym = {{ICALP}'11},
booktitle = {{P}roceedings of the 38th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'11)~-- {P}art~{II}},
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 = {On~Reachability for Hybrid Automata over Bounded Time},
pages = {416-427},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDGORW-icalp11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDGORW-icalp11.pdf},
doi = {10.1007/978-3-642-22012-8_33},
abstract = {This paper investigates the time-bounded version of the
reachability problem for hybrid automata. This problem asks whether a
given hybrid automaton can reach a given target location
within~\(\mathbf{T}\) time units, where \(\mathbf{T}\) is a constant
rational value. We show that, in contrast to the classical (unbounded)
reachability problem, the timed-bounded version is decidable for
rectangular hybrid automata provided only non-negative rates are allowed.
This class of systems is of practical interest and subsumes, among others,
the class of stopwatch automata. We also show that the problem becomes
undecidable if either diagonal constraints or both negative and positive
rates are allowed.}
}
@inproceedings{BCS-icalp11,
address = {Z{\"u}rich, Switzerland},
month = jul,
year = 2011,
volume = 6756,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Aceto, Luca and Henzinger, Monika and Sgall, Jir{\'\i}},
acronym = {{ICALP}'11},
booktitle = {{P}roceedings of the 38th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'11)~-- {P}art~{II}},
author = {B{\'a}r{\'a}ny, Vince and ten~Cate, Balder and Segoufin, Luc},
title = {Guarded negation},
pages = {356-367},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCS-icalp11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCS-icalp11.pdf},
doi = {10.1007/978-3-642-22012-8_28},
abstract = {We consider restrictions of first-order logic and of fixpoint
logic in which all occurrences of negation are required to be guarded by
an atomic predicate. In terms of expressive power, the logics in
question, called GNFO and GNFP, extend the guarded fragment of first-order
logic and guarded least fixpoint logic, respectively. They also extend the
recently introduced unary negation fragments of first-order logic and of
least fixpoint logic.\par
We show that the satisfiability problem for GNFO and for GNFP is
2ExpTime-complete, both on arbitrary structures and on finite structures.
We also study the complexity of the associated model checking problems.
Finally, we show that GNFO and GNFP are not only computationally well
behaved, but also model theoretically: we show that GNFO and GNFP have the
tree-like model property and that GNFO has the finite model property, and
we characterize the expressive power of GNFO in terms of invariance for an
appropriate notion of bisimulation.}
}
@inproceedings{SS-icalp11,
address = {Z{\"u}rich, Switzerland},
month = jul,
year = 2011,
volume = 6756,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Aceto, Luca and Henzinger, Monika and Sgall, Jir{\'\i}},
acronym = {{ICALP}'11},
booktitle = {{P}roceedings of the 38th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'11)~-- {P}art~{II}},
author = {Schmitz, Sylvain and Schnoebelen, {\relax Ph}ilippe},
title = {Multiply-Recursive Upper Bounds with {H}igman's Lemma},
pages = {441-452},
url = {http://arxiv.org/abs/1103.4399},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SS-icalp11.pdf},
doi = {10.1007/978-3-642-22012-8_35},
abstract = {We develop a new analysis for the length of controlled
bad sequences in well-quasi-orderings based on
Higman's Lemma. This leads to tight
multiply-recursive upper bounds that readily apply
to several verification algorithms for
well-structured systems.}
}
@inproceedings{AMSS-icalp11,
address = {Z{\"u}rich, Switzerland},
month = jul,
year = 2011,
volume = 6756,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Aceto, Luca and Henzinger, Monika and Sgall, Jir{\'\i}},
acronym = {{ICALP}'11},
booktitle = {{P}roceedings of the 38th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'11)~-- {P}art~{II}},
author = {Anderson, Matthew and van~Melkebeek, Dieter and Schweikardt,
Nicole and Segoufin, Luc},
title = {Locality of queries definable in invariant first-order logic
with arbitrary built-in predicates},
pages = {368-379},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AMSS-icalp11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AMSS-icalp11.pdf},
doi = {10.1007/978-3-642-22012-8_29},
abstract = {We consider first-order formulas over relational structures
which may use arbitrary numerical predicates. We require that the validity
of the formula is independent of the particular interpretation of the
numerical predicates and refer to such formulas as Arb-invariant
first-order.\par
Our main result shows a Gaifman locality theorem: two tuples of a
structure with n elements, having the same neighborhood up to distance
\((\log n)^{\omega(1)}\), cannot be distinguished by Arb-invariant
first-order formulas. When restricting attention to word structures, we
can achieve the same quantitative strength for Hanf locality. In both
cases we show that our bounds are tight.\par
Our proof exploits the close connection between Arb-invariant first-order
formulas and the complexity class \(\textsf{AC}^{0}\), and hinges on the
tight lower bounds for parity on constant-depth circuits.}
}
@techreport{rr-lsv-11-08,
author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin and
Zeitoun, Marc},
title = {Weighted Expressions and {DFS} Tree Automata},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2011},
month = apr,
type = {Research Report},
number = {LSV-11-08},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2011-08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2011-08.pdf},
note = {32~pages},
abstract = {We introduce weighted expressions, a~calculus to express
quantitative properties over unranked trees. They involve products and
sums from a semiring as well as classical boolean formulas. We~show that
weighted expressions are expressively equivalent to a new class of
weighted tree-walking automata. This new automata model is equipped with
pebbles, and follows a depth-first-search policy in the tree.}
}
@inproceedings{benzina-iccans11,
address = {Republic of Maldives},
month = may,
year = 2011,
noeditor = {},
acronym = {{ICCANS}'11},
booktitle = {{P}roceedings of the {I}nternational {C}onference on {C}omputer {A}pplications
and {N}etwork {S}ecurity ({ICCANS}'11)},
author = {Benzina, Hedi},
title = {Logic in Virtualized Systems},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/benzina-iccans11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/benzina-iccans11.pdf},
abstract = {As virtualized systems grow in complexity, they are
increasingly vulnerable to denial-of-service (DoS)
attacks involving resource exhaustion. A malicious
driver downloaded and installed by the system
administrator can trigger high-complexity behavior
exhausting CPU time or stack space and making the
whole system unavailable. Virtualized systems such
as Xen or VirtualBox have been proposed to increase
the level of security on computers. On the other
hand, such virtualized systems are now targets for
attacks. The weak spot of such systems is domain
zero administration, which is left entirely under
the administrator's responsibility, and is in
particular vulnerable to attacks. \par
We propose to let
the administrator write and deploy security policies
and rely on RuleGen, a policy compiler, and Orchids'
fast, real-time monitoring engine to raise alerts in
case any policy violation, expressed in a fragment
of linear temporal logic, is detected. This approach
has shown its efficiency against real DoS exploits.
}
}
@phdthesis{markey-HDR11,
author = {Markey, Nicolas},
title = {Verification of Embedded Systems -- Algorithms and Complexity},
year = 2011,
month = apr,
type = {M{\'e}moire d'habilitation},
school = {{\'E}cole Normale Sup{\'e}rieure de Cachan, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hdr-nm.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hdr-nm.pdf}
}
@incollection{CDM-fmtasp11,
author = {Comon{-}Lundh, Hubert and Delaune, St{\'e}phanie and Millen, Jonathan K.},
title = {Constraint solving techniques and enriching the model with
equational theories},
booktitle = {Formal Models and Techniques for Analyzing Security Protocols},
editor = {Cortier, V{\'e}ronique and Kremer, Steve},
series = {Cryptology and Information Security Series},
volume = 5,
publisher = {{IOS} Press},
nochapter = {},
pages = {35-61},
year = 2011,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDM-fmtasp11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDM-fmtasp11.pdf},
abstract = {Derivability constraints represent in a symbolic way the
infinite set of possible executions of a finite protocol, in presence of
an arbitrary active attacker. Solving a derivability constraint consists
in computing a simplified representation of such executions, which is
amenable to the verification of any (trace) security property. Our goal is
to explain this method on a non-trivial combination of primitives.\par
In this chapter we explain how to model the protocol executions using
derivability constraints, and how such constraints are interpreted,
depending on the cryptographic primitives and the assumed attacker
capabilities. Such capabilities are represented as a deduction system that
has some specific properties. We choose as an example the combination of
exclusive-or, symmetric encryption{\slash}decryption and pairing{\slash}unpairing. We
explain the properties of the deduction system in this case and give a
complete and terminating set of rules that solves derivability
constraints. A similar set of rules has been already published for the
classical Dolev-Yao attacker, but it is a new result for the combination
of primitives that we consider. This allows to decide trace security
properties for this combination of primitives and arbitrary finite
protocols.}
}
@inproceedings{ACD-cade11,
address = {Wroc{\l}aw, Poland},
month = jul,
year = 2011,
volume = {6803},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Bj{\o}rner, Nikolaj and Sofronie-Stokkermans, Viorica},
acronym = {{CADE}'11},
booktitle = {{P}roceedings of the 23rd {I}nternational
{C}onference on {A}utomated {D}eduction
({CADE}'11)},
author = {Arnaud, Mathilde and Cortier, V{\'e}ronique and Delaune,
St{\'e}phanie},
title = {Deciding security for protocols with recursive tests},
pages = {49-63},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ACD-cade11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ACD-cade11.pdf},
doi = {10.1007/978-3-642-22438-6_6},
abstract = {Security protocols aim at securing communications over public
networks. Their design is notoriously dicult and error-prone. Formal
methods have shown their usefulness for providing a careful security
analysis in the case of standard authentication and condentiality
protocols. However, most current techniques do not apply to protocols that
perform recursive computation e.g. on a list of messages received from the
network.\par
While considering general recursive input{\slash}output actions very quickly
yields undecidability, we focus on protocols that perform recursive tests
on received messages but output messages that depend on the inputs in a
standard way. This is in particular the case of secured routing protocols,
distributed right delegation or PKI certication paths. We provide NPTIME
decision procedures for protocols with recursive tests and for a bounded
number of sessions. We also revisit constraint system solving, providing a
complete symbolic representation of the attacker knowledge.}
}
@inproceedings{KSW-csf11,
address = {Cernay-la-Ville, France},
month = jun,
year = 2011,
publisher = {{IEEE} Computer Society Press},
acronym = {{CSF}'11},
booktitle = {{P}roceedings of the
24th {IEEE} {C}omputer {S}ecurity {F}oundations
{S}ymposium ({CSF}'11)},
author = {Kremer, Steve and Steel, Graham and Warinschi, Bogdan},
title = {Security for Key Management Interfaces},
pages = {266-280},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/KSW-csf11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KSW-csf11.pdf},
nolongps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2011-07.ps},
nolongpsgz = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PSGZ/
rr-lsv-2011-07.ps.gz},
doi = {10.1109/CSF.2011.25},
abstract = {We propose a much-needed formal definition of security
for cryptographic key management APIs. The
advantages of our definition are that it is general,
intuitive, and applicable to security proofs in both
symbolic and computational models of
cryptography. Our definition relies on an idealized
API which allows only the most essential functions
for generating, exporting and importing keys, and
takes into account dynamic corruption of keys.
Based on this we can define the security of more
expressive APIs which support richer
functionality. We illustrate our approach by showing
the security of APIs both in symbolic and
computational models.}
}
@inproceedings{DKRS-csf11,
address = {Cernay-la-Ville, France},
month = jun,
year = 2011,
publisher = {{IEEE} Computer Society Press},
acronym = {{CSF}'11},
booktitle = {{P}roceedings of the
24th {IEEE} {C}omputer {S}ecurity {F}oundations
{S}ymposium ({CSF}'11)},
author = {Delaune, St{\'e}phanie and Kremer, Steve and Ryan, Mark D. and
Steel, Graham},
title = {Formal analysis of protocols based on {TPM} state registers},
pages = {66-82},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DKRS-csf11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DKRS-csf11.pdf},
doi = {10.1109/CSF.2011.12},
abstract = {We~present a Horn-clause-based framework for analysing security
protocols that use platform configuration registers~(PCRs), which are
registers for maintaining state inside the Trusted Platform Module~(TPM).
In~our model, the~PCR state space is unbounded, and our experience shows
that a na{\"i}ve analysis using ProVerif or SPASS does not terminate. To
address this, we extract a set of instances of the Horn clauses of our
model, for which ProVerif does terminate on our examples. We~prove the
soundness of this extraction process: no~attacks are lost, that~is, any
query derivable in the more general set of clauses is also derivable from
the extracted instances. The~effectiveness of our framework is
demonstrated in two case studies: a~simplified version of Microsoft
Bitlocker, and a digital envelope protocol that allows a user to choose
whether to perform a decryption, or to verifiably renounce the ability to
perform the decryption.}
}
@techreport{rr-lsv-11-04,
author = {Fribourg, Laurent and K{\"u}hne, Ulrich},
title = {Parametric Verification of Hybrid Automata Using the Inverse Method},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2011},
month = mar,
type = {Research Report},
number = {LSV-11-04},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2011-04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2011-04.pdf},
note = {25~pages},
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 subset of parameters
which guarantee a certain behavior of a system. Recently, a method has
been presented for attacking this problem for Timed Automata. In this
report, we show the extension of this methodology for hybrid automata with
linear and affine dynamics. The method is demonstrated with a distributed
temperature control system and several other hybrid system benchmarks from
the literature.}
}
@inproceedings{CLC-stacs11,
address = {Dortmund, Germany},
month = mar,
year = 2011,
volume = 9,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {D{\"u}rr, Christoph and Schwentick, {\relax Th}omas},
acronym = {{STACS}'11},
booktitle = {{P}roceedings of the 28th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'11)},
author = {Comon{-}Lundh, Hubert and Cortier, V{\'e}ronique},
title = {How to prove security of communication protocols?
A~discussion on the soundness of formal models w.r.t. computational ones},
pages = {29-44},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CLC-stacs11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CLC-stacs11.pdf},
doi = {10.4230/LIPIcs.STACS.2011.29},
abstract = {Security protocols are short programs that aim at
securing communication over a public network. Their
design is known to be error-prone with flaws found
years later. That is why they deserve a careful
security analysis, with rigorous proofs. Two main
lines of research have been (independently)
developed to analyse the security of protocols. On
the one hand, formal methods provide with symbolic
models and often automatic proofs. On the other
hand, cryptographic models propose a tighter
modeling but proofs are more difficult to write and
to check. An approach developed during the last
decade consists in bridging the two approaches,
showing that symbolic models are sound
w.r.t. symbolic ones, yielding strong security
guarantees using automatic tools. These results have
been developed for several cryptographic primitives
(e.g. symmetric and asymmetric encryption,
signatures, hash) and security properties. While
proving soundness of symbolic models is a very
promising approach, several technical details are
often not satisfactory. Focusing on symmetric
encryption, we describe the difficulties and
limitations of the available results.}
}
@inproceedings{CS-stacs11,
address = {Dortmund, Germany},
month = mar,
year = 2011,
volume = 9,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {D{\"u}rr, Christoph and Schwentick, {\relax Th}omas},
acronym = {{STACS}'11},
booktitle = {{P}roceedings of the 28th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'11)},
author = {ten~Cate, Balder and Segoufin, Luc},
title = {Unary negation},
pages = {344-355},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-stacs11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-stacs11.pdf},
doi = {10.4230/LIPIcs.STACS.2011.344},
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 Beth property.}
}
@inproceedings{ST-stacs11,
address = {Dortmund, Germany},
month = mar,
year = 2011,
volume = 9,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {D{\"u}rr, Christoph and Schwentick, {\relax Th}omas},
acronym = {{STACS}'11},
booktitle = {{P}roceedings of the 28th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'11)},
author = {Segoufin, Luc and Toru{\'n}czyk, Szymon},
title = {Automata based verification over linearly ordered data domains},
pages = {81-92},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ST-stacs11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ST-stacs11.pdf},
doi = {10.4230/LIPIcs.STACS.2011.81},
abstract = {In this paper we work over linearly ordered data domains
equipped with finitely many unary predicates and constants. We consider
nondeterministic automata processing words and storing finitely many
variables ranging over the domain. During a transition, these automata can
compare the data values of the current configuration with those of the
previous configuration using the linear order, the unary predicates and
the constants.\par
We show that emptiness for such automata is decidable, both over finite
and infinite words, under reasonable computability assumptions on the
linear order.\par
Finally, we show how our automata model can be used for verifying
properties of workflow specifications in the presence of an underlying
database.}
}
@article{LS-jcss11,
publisher = {Elsevier Science Publishers},
journal = {Journal of Computer and System Sciences},
author = {Libkin, Leonid and Sirangelo, Cristina},
title = {Data exchange and schema mappings in open and closed worlds},
year = {2011},
month = may,
volume = {77},
number = {3},
pages = {542-571},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-jcss11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-jcss11.pdf},
doi = {10.1016/j.jcss.2010.04.010}
}
@phdthesis{kremer-HDR11,
author = {Kremer, Steve},
title = {Modelling and analyzing security protocols in cryptographic process calculi},
year = 2011,
month = mar,
type = {M{\'e}moire d'habilitation},
school = {{\'E}cole Normale Sup{\'e}rieure de Cachan, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hdr-SK.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hdr-SK.pdf},
noslides = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/SLIDES/}
}
@phdthesis{steel-HDR11,
author = {Steel, Graham},
title = {Formal Analysis of Security {API}s},
year = 2011,
month = mar,
type = {M{\'e}moire d'habilitation},
school = {{\'E}cole Normale Sup{\'e}rieure de Cachan, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hdr-GS.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hdr-GS.pdf},
noslides = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/SLIDES/}
}
@phdthesis{delaune-HDR11,
author = {Delaune, St{\'e}phanie},
title = {Verification of security protocols: from confidentiality to privacy},
year = 2011,
month = mar,
type = {M{\'e}moire d'habilitation},
school = {{\'E}cole Normale Sup{\'e}rieure de Cachan, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hdr-SD.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hdr-SD.pdf},
abstract = {Security is a very old concern, which until quite recently was
mostly of interest for military purposes. The deployment of electronic
commerce changes this drastically. The security of exchanges is ensured by
cryptographic protocols which are notoriously error prone. The formal
verification of cryptographic protocols is a difficult problem that can be
seen as a particular model-checking problem in an hostile environment.
Many results and tools have been developed to automatically verify
cryptographic protocols.\par
Recently, new type of applications have emerged, in order to face new
technological and societal challenges, e.g. electronic voting protocols,
secure routing protocols for mobile ad hoc networks,~... These
applications involve some features that are not taken into account by the
existing verification tools, e.g. complex cryptographic primitives,
privacy-type security properties,~... This prevents us from modelling
these protocols in an accurate way. Moreover, protocols are often analysed
in isolation and this is well-known to be not sufficient. In this thesis,
we use formal methods to study these aspects concerning the verification
of cryptographic protocols.}
}
@inproceedings{pas-icdt11,
address = {Uppsala, Sweden},
month = mar,
year = 2011,
publisher = {ACM Press},
editor = {Milo, Tova},
acronym = {{ICDT}'11},
booktitle = {{P}roceedings of the 14th {I}nternational {C}onference on
{D}atabase {T}heory ({ICDT}'11)},
author = {Pasail{\u{a}}, Daniel},
title = {Conjunctive queries determinacy and rewriting},
pages = {220-231},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/pasaila-icdt11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/pasaila-icdt11.pdf},
doi = {10.1145/1938551.1938580}
}
@inproceedings{BCH-acsd11,
address = {Newcastle upon Tyne, UK},
month = jun,
year = 2011,
publisher = {{IEEE} Computer Society Press},
editor = {Caillaud, Beno{\^\i}t and Carmona, Josep},
acronym = {{ACSD}'11},
booktitle = {{P}roceedings of the 11th {I}nternational
{C}onference on {A}pplication of {C}oncurrency
to {S}ystem {D}esign
({ACSD}'11)},
author = {Balaguer, Sandie and Chatain, {\relax Th}omas and Haar, Stefan},
title = {Building Tight Occurrence Nets from Reveals Relations},
pages = {44-53},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCH-acsd11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCH-acsd11.pdf},
doi = {10.1109/ACSD.2011.16},
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 in~[Haar, IEEE TAC 55(10):2310-2320, 2010] 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}\)?}
}
@inproceedings{HMN-atpn11,
address = {Newcastle upon Tyne, UK},
month = jun,
year = 2011,
volume = {6709},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Kristensen, Lars M. and Petrucci, Laure},
acronym = {{PETRI~NETS}'11},
booktitle = {{P}roceedings of the 32nd
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({PETRI~NETS}'11)},
author = {Haddad, Serge and Mairesse, Jean and Nguyen, Hoang-Thach},
title = {Synthesis and Analysis of Product-form {P}etri Nets},
pages = {288-307},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HMN-atpn11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HMN-atpn11.pdf},
doi = {10.1007/978-3-642-21834-7_16},
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{CFS-atpn2011,
address = {Newcastle upon Tyne, UK},
month = jun,
year = 2011,
volume = {6709},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Kristensen, Lars M. and Petrucci, Laure},
acronym = {{PETRI~NETS}'11},
booktitle = {{P}roceedings of the 32nd
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({PETRI~NETS}'11)},
author = {Chambart, Pierre and Finkel, Alain and Schmitz, Sylvain},
title = {Forward Analysis and Model Checking for Trace Bounded {WSTS}},
nopages = {49-68},
url = {http://arxiv.org/abs/1004.2802},
doi = {10.1007/978-3-642-21834-7_4},
abstract = {We investigate a subclass of well-structured transition
systems~(WSTS), the bounded---in the sense of Ginsburg and Spanier (Trans.
AMS 1964)---complete deterministic ones, which we claim provide an
adequate basis for the study of forward analyses as developed by Finkel
and Goubault-Larrecq (ICALP~2009). Indeed, we prove that, unlike other
conditions considered previously for the termination of forward analysis,
boundedness is decidable. Boundedness turns out to be a valuable
restriction for WSTS verification, as we show that it further allows to
decide all \(\omega\)-regular properties on the set of infinite traces of
the system.}
}
@inproceedings{ACGP-rsa11,
address = {San Francisco, California, USA},
month = feb,
year = 2011,
volume = 6558,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Kiayias, Aggelos},
acronym = {{CT-RSA}'11},
booktitle = {{P}roceedings of the {C}ryptographers' {T}rack at the {RSA}
{C}onference 2011 ({CT-RSA}'11)},
author = {Abdalla, Michel and Chevalier, C{\'e}line and Granboulan, Louis and
Pointcheval, David},
title = {Contributory Password-Authenticated Group Key Exchange with
Join Capability},
pages = {142-160},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ACGP-rsa11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ACGP-rsa11.pdf},
doi = {10.1007/978-3-642-19074-2_11},
abstract = {Password-based authenticated group key exchange allows any group
of users in possession of a low-entropy secret key to establish a common
session key even in the presence of adversaries. In this paper, we propose
a new generic construction of password-authenticated group key exchange
protocol from any two-party password-authenticated key exchange with
explicit authentication. Our new construction has several advantages when
compared to existing solutions. First, our construction only assumes a
common reference string and does not rely on any idealized models. Second,
our scheme enjoys a simple and intuitive security proof in the universally
composable framework and is optimal in the sense that it allows at most
one password test per user instance. Third, our scheme also achieves a
strong notion of security against insiders in that the adversary cannot
bias the distribution of the session key as long as one of the players
involved in the protocol is honest. Finally, we show how to easily extend
our protocol to the dynamic case in a way that the costs of establishing a
common key between two existing groups is significantly smaller than
computing a common key from scratch.}
}
@inproceedings{FFSS-lics2011,
address = {Toronto, Canada},
month = jun,
year = 2011,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'11},
booktitle = {{P}roceedings of the 26th
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'11)},
author = {Figueira, Diego and Figueira, Santiago and Schmitz, Sylvain and
Schnoebelen, {\relax Ph}ilippe},
title = {{A}ckermannian and Primitive-Recursive Bounds with {D}ickson's Lemma},
pages = {269-278},
url = {http://arxiv.org/abs/1007.2989},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FFSS-lics11.pdf},
doi = {10.1109/LICS.2011.39},
abstract = {Dickson's Lemma is a simple yet powerful tool widely used in
decidability proofs, especially when dealing with counters or related data
structures in algorithmics, verification and model-checking, constraint
solving, logic, etc. While Dickson's Lemma is well-known, most computer
scientists are not aware of the complexity upper bounds that are entailed
by its use. This is mainly because, on this issue, the existing literature
is not very accessible.\par
We propose a new analysis of the length of bad sequences over
\((\mathbb{N}^{k},\leq)\), improving on earlier results and providing
upper bounds that are essentially tight. This analysis is complemented by
a {"}user guide{"} explaining through practical examples how to easily
derive complexity upper bounds from Dickson's Lemma.}
}
@inproceedings{GLV-lics2011,
address = {Toronto, Canada},
month = jun,
year = 2011,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'11},
booktitle = {{P}roceedings of the 26th
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'11)},
author = {Goubault{-}Larrecq, Jean and Varacca, Daniele},
title = {Continuous Random Variables},
pages = {97-106},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GLV-lics2011.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLV-lics2011.pdf},
corrigendumpdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLV-lics2011-errata.pdf},
doi = {10.1109/LICS.2011.23},
abstract = {We introduce the domain of continuous random variables (CRV)
over a domain, as an alternative to Jones and Plotkin's probabilistic
powerdomain. While no known Cartesian-closed category is stable under the
latter, we show that the so-called thin (uniform) CRVs define a strong
monad on the Cartesian-closed category of bc-domains. We also characterize
their inequational theory, as (fair-)coin algebras. We apply this to solve
a recent problem posed by M. Escard{\'o}: testing is semi-decidable for
EPCF terms. CRVs arose from the study of the second author's (layered)
Hoare indexed valuations, and we also make the connection apparent.}
}
@inproceedings{Fig-lics2011,
address = {Toronto, Canada},
month = jun,
year = 2011,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'11},
booktitle = {{P}roceedings of the 26th
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'11)},
author = {Figueira, Diego},
title = {A decidable two-way logic on data words},
pages = {365-374},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/Fig-lics2011.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Fig-lics2011.pdf},
doi = {10.1109/LICS.2011.18},
abstract = {We study the satisfiability problem for a logic on data words.
A~data word is a finite word where every position carries a label from a
finite alphabet and a data value from an infinite domain. The logic we
consider is two-way, contains \emph{future} and \emph{past} modalities,
which are considered as reflexive and transitive relations, and data
equality and inequality tests. This logic corresponds to the fragment of
XPath with the 'followingsibling- or-self' and 'preceding-sibling-or-self'
axes over data words. We show that this problem is decidable,
EXPSPACE-complete. This is surprising considering that with the strict
(non-reflexive) navigation relations the satisfiability problem is
undecidable. To~prove this, we~first reduce the problem to a derivation
problem for an infinite transition system, and then we show how to
abstract this problem into a reachability problem of a finite transition
system.}
}
@phdthesis{villard-phd2010,
author = {Villard, Jules},
title = {Heaps and Hops},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
type = {Th{\`e}se de doctorat},
year = 2011,
month = feb,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/villard-phd.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/villard-phd.pdf},
abstract = {This thesis is about the specification and verification of
copyless message-passing programs, a particular kind of concurrent
programs that communicate by message passing. Instead of copying messages
over channels, processes exchange pointers into a shared memory where the
actual contents of messages are stored. Channels are themselves objects in
the heap that can be communicated, thus achieving full mobility. This
flexible and efficient programming paradigm must be used carefully: every
pointer that is communicated becomes shared between its sender and its
recipient, which may introduce races. To err on the side of caution, the
sender process should not attempt to access the area of storage
circumscribed by a message once it has been sent. Indeed, this right is
now reserved to the recipient, who may already have modified it or even
disposed of it. In other words, the ownership of pieces of heap hops from
process to process following the flow of messages.\par
Copyless message passing combines two features of programs that make
formal verification challenging: explicit memory management and
concurrency. To tackle these difficulties, we base our approach on two
recent developments. On the one hand, concurrent separation logic produces
concise proofs of pointer-manipulating programs by keeping track only of
those portions of storage owned by the program. We use such local
reasoning techniques to analyse the fluxes of ownership in programs, and
ensure in particular that no dangling pointer will be dereferenced or
freed at runtime. On the other hand, channel contracts, a form of session
types introduced by the Sing\# programming language, provide an abstraction
of the exchanges of messages that can be used to statically verify that
programs never face unexpected message receptions and that all messages
are delivered before a channel is closed.\par
The contributions contained in this thesis fall into three categories.
First, we give a semantics to copyless message-passing programs, the
ownership transfers they induce and contracts, and link the three
together. In doing so, we provide the first formal model of a
theoretically significant subset of the Sing\# programming language. In
particular, we show that some properties of their contracts rub off on
programs, which justifies their use as protocol specifications. Second, we
introduce the first proof system for copyless message passing, based on
separation logic and contracts. The proof system discharges parts of the
verification of programs on the verification of their contracts. The
marriage of these two techniques allows one to prove that programs are
free from memory faults, race conditions and message-passing errors such
as unspecified receptions and undelivered messages. Moreover, we show how
the logic and contracts cooperate to prove the absence of memory leaks.
Third, we give an implementation of our analysis, Heap-Hop, that takes
annotated programs as input and automatically checks the given
specifications and deduces which of the properties above are enjoyed by
the program. The only annotations needed by Heap-Hop are pre and
postconditions of each function, loop invariants, and the contracts
followed by the communications.}
}
@book{CK-ios2011,
editor = {Cortier, V{\'e}ronique and Kremer, Steve},
title = {Formal Models and Techniques for Analyzing Security Protocols},
publisher = {{IOS} Press},
year = {2011},
series = {Cryptology and Information Security Series},
volume = 5,
url = {http://www.iospress.nl/loadtop/load.php?isbn=9781607507130}
}
@inproceedings{BDDHP-valuetools11,
address = {Cachan, France},
month = may,
year = 2011,
acronym = {{VALUETOOLS}'11},
booktitle = {{P}roceedings of the 5th {I}nternational {C}onference
on {P}erformance {E}valuation {M}ethodologies and {T}ools
({VALUETOOLS}'11)},
author = {Ballarini, Paolo and Djafri, Hilal and Duflot, Marie and
Haddad, Serge and Pekergin, Nihal},
title = {{HASL}: An~Expressive Language for Statistical Verification
of Stochastic Models},
pages = {306-315},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDDHP-valuetools11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDDHP-valuetools11.pdf},
abstract = {We introduce the Hybrid Automata Stochastic Logic (HASL), a new
temporal logic formalism for the verification of discrete event stochastic
processes (DESP). HASL employs Linear Hybrid Automata (LHA) as machineries
to select prefixes of relevant execution paths of a DESP~\(\mathcal{D}\).
The advantage with LHA is that rather elaborate information can be
collected \emph{on-the-fly} during path selection, providing the user with
a powerful means to express sophisticated measures. A formula of HASL
consists of an LHA~\(\mathcal{A}\) and an expression~\(Z\) referring to
moments of \emph{path random variables}. A~simulation-based statistical
engine is employed to obtained a confidence-interval estimate of the
expected value of~\(Z\). In essence HASL provide a unifying verification
framework where sophisticated temporal reasoning is naturally blended with
elabo- rate reward-based analysis. We illustrate the HASL approach by
means of some examples and a discussion about its expressivity. We also
provide empirical evidence obtained through COSMOS, a prototype software
tool for HASL verification.}
}
@article{BFLM-cacm11,
publisher = {ACM Press},
journal = {Communications of the~{ACM}},
author = {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim~G. and
Markey, Nicolas},
title = {Quantitative analysis of real-time systems
using priced timed automata},
volume = 54,
number = 9,
month = sep,
pages = {78-87},
year = 2011,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLM-cacm11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLM-cacm11.pdf},
doi = {10.1145/1995376.1995396},
abstract = {The problems of time-dependent behavior in general, and dynamic
resource allocation in particular, pervade many aspects of modern life.
Prominent examples range from reliability and efficient use of
communication resources in a telecommunication network to the allocation
of tracks in a continental railway network, from scheduling the usage of
computational resources on a chip for durations of nano-seconds to the
weekly, monthly, or longer-range reactive planning in a factory or a
supply chain.}
}
@inproceedings{BFHR-fossacs11,
address = {Saarbr{\"u}cken, Germany},
month = mar # {-} # apr,
year = 2011,
volume = {6604},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Hofmann, Martin},
acronym = {{FoSSaCS}'11},
booktitle = {{P}roceedings of the 14th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'11)},
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},
pages = {153-167},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHR-fossacs11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHR-fossacs11.pdf},
doi = {10.1007/978-3-642-19805-2_11}
}
@inproceedings{FS-stacs11,
address = {Dortmund, Germany},
month = mar,
year = 2011,
volume = 9,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {D{\"u}rr, Christoph and Schwentick, {\relax Th}omas},
acronym = {{STACS}'11},
booktitle = {{P}roceedings of the 28th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'11)},
author = {Figueira, Diego and Segoufin, Luc},
title = {Bottom-up automata on data trees and vertical {XP}ath},
pages = {93-104},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FS-stacs11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FS-stacs11.pdf},
doi = {10.4230/LIPIcs.STACS.2011.93},
abstract = {A data tree is a tree whose every node carries a label from a
finite alphabet and a datum from some infinite domain. We introduce a new
model of automata over unranked data trees with a decidable emptiness
problem. It is essentially a bottom-up alternating automaton with one
register, enriched with epsilon-transitions that perform tests on the data
values of the subtree. We show that it captures the expressive power of
the vertical fragment of XPath --containing the child, descendant, parent
and ancestor axes-- obtaining thus a decision procedure for its
satisfiability problem.}
}
@inproceedings{BKKL-ceeset2008,
address = {Brno, Czech Republic},
year = 2011,
volume = {4980},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Huzar, Zbigniew and Koc{\'\i}, Radek and Meyer, Bertrand and
Walter, Bartosz and Zendulka, Jaroslav},
acronym = {{CEE-SET}'08},
booktitle = {{R}evised {S}elected {P}apars of the 3rd {IFIP} {TC2} {C}entral and
{E}ast {E}uropean {C}onference on {S}oftware {E}ngineering
{T}echniques ({CEE-SET}'08)},
author = {Bollig, Benedikt and Katoen, Joost-Pieter and Kern,
Carsten and Leucker, Martin},
title = {{SMA}---The {S}myle Modeling Approach},
pages = {103-117},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-ceeset2008.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKKL-ceeset2008.pdf},
doi = {10.1007/978-3-642-22386-0_8},
abstract = {This paper introduces the model-based software development
methodology SMA---the Smyle Modeling Approach---which is centered around
Smyle, a dedicated learning procedure to support engineers to
interactively obtain design models from requirements, characterized as
either being desired (positive) or unwanted (negative) system behavior.
The learning approach is complemented by scenario patterns where the
engineer can specify clearly desired or unwanted behavior. This~way, user
interaction is reduced to the interesting scenarios limiting the design
effort considerably. In~SMA, the learning phase is complemented by an
effective analysis phase that allows for detecting design flaws at an
early design stage. This paper describes the approach and reports on first
practical experiences.}
}
@article{JGL-jyg10,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Goubault{-}Larrecq, Jean},
title = {Musings Around the Geometry of Interaction, and Coherence},
volume = 412,
number = 20,
pages = {1998-2014},
year = 2011,
month = apr,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/jgl-jyg10.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/jgl-jyg10.pdf},
doi = {10.1016/j.tcs.2010.12.023},
abstract = {We introduce the Danos-R{\'e}gnier category \(\mathcal{DR}(M)\)
of a linear inverse monoid~\(M\), as~a categorical description of
geometries of interaction~(GOI) inspired from the weight algebra. The
natural setting for GOI is that of a so-called weakly Cantorian linear
inverse monoid, in which case \(\mathcal{DR}(M)\) is a kind of symmetrized
version of the classical Abramsky-Haghverdi-Scott construction of a weak
linear category from a GOI situation. It is well-known that GOI is
perfectly suited to describe the multiplicative fragment of linear logic,
and indeed \(\mathcal{DR}(M)\) will be a \(\star\)-autonomous category in
this case. It is also well-known that the categorical interpretation of
the other linear connectives conflicts with GOI interpretations. We make
this precise, and show that \(\mathcal{DR}(M)\) has no terminal object, no
cartesian product of any two objects, and no exponential---whatever
\(M\)~is, unless \(M\)~is trivial. However, a form of coherence completion
of \(\mathcal{DR}(M)\) \textit{{\`a} la} Hu-Joyal (which for additives
resembles a layered approach \textit{{\`a} la} Hughes-van Glabbeek),
provides a model of full classical linear logic, as soon as \(M\) is
weakly Cantorian. One finally notes that Girard's notion of \emph{coherence} is
pervasive, and instrumental in every aspect of this work.}
}
@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.",
}}
This file was generated by bibtex2html 1.98.