@comment{{This file has been generated by bib2bib 1.93}}
@comment{{Command line: bib2bib -oc cites -ob tmp.bib -c 'not $type = "PROCEEDINGS"' paul.bib peter_hongyang.bib luigi.bib remi_nicolas.bib emmanuel.bib}}
@inproceedings{maieli:_inter,
author = {Maieli, Roberto and Ruet, Paul},
title = {Interactive correctness criterion for
multiplicative-additive proof-nets},
note = {LICS 2006 short paper},
abstract = {Proof-nets are special graphs (proof-structures)
representing de-sequentialised proofs of the linear
logic (LL) sequent calculus. Each proof-net stands
for a class of sequent proofs which are equivalent
modulo irrelevant permutations of logical rules. In
our work we present an interactive characterisation
of those cut-free proof-structures coming from
proofs of the multiplicative-additive fragment of
linear logic (MALL). This work is intended to extend
to MALL proof-nets an original proposal by Girard
for an interactive correction criterion for
proof-nets of the multiplicative fragment of linear
logic (MLL). Its natural consequence we will be the
study of the question of ``modularity'' for additive
proof-nets. },
month = jun,
year = 2006
}
@article{DBLP:journals/entcs/IlleR08,
author = {Pierre Ille and
Paul Ruet},
title = {Cyclic Extensions of Order Varieties},
journal = {Electr. Notes Theor. Comput. Sci.},
volume = {212},
year = {2008},
pages = {119-132},
ee = {http://dx.doi.org/10.1016/j.entcs.2008.04.057},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/tacas/NiebertP06,
author = {Peter Niebert and
Doron Peled},
title = {Efficient Model Checking for LTL with Partial Order Snapshots.},
booktitle = {TACAS},
year = {2006},
pages = {272-286},
ee = {http://dx.doi.org/10.1007/11691372_18},
crossref = {DBLP:conf/tacas/2006},
bibsource = {DBLP, http://dblp.uni-trier.de},
abstract = { Certain behavioral properties of distributed
systems are difficult to express in interleaving
semantics, whereas they are naturally expressed in
terms of partial orders of events or, equivalently,
Mazurkiewicz traces. Examples of such properties are
serializability of a database or {\em
snapshots}. Recently, a modest extension for LTL by
an operator that expresses snapshots has been
proposed. It combines the ease of linear
(interleaving) specification with this useful
partial order concept. The new construct allows one
to assert that a global snapshot (also called a {\em
slice} or a {\em cut}) was passed, perhaps not in
the observed (interleaved) execution sequence, but
possibly in a (trace) equivalent one. A model
checking algorithm was suggested for a subset of
this logic, with PSPACE complexity in the size of
the system and the checked formula. For the whole
logic, a solution that is in EXSPACE in the size of
the system (PSPACE in the number of its global
states) was given. In this paper, we provide a model
checking algorithm in PSPACE in the size of a system
of communicating sequential processes when
restricting snapshots to boolean combinations of
local properties of each process. Concerning size of
the formula, it is PSPACE for the case of snapshot
properties expressed in DNF, and EXPSPACE where a
translation to DNF is necessary. }
}
@proceedings{DBLP:conf/tacas/2006,
editor = {Holger Hermanns and Jens Palsberg},
title = {Tools and Algorithms for the Construction and
Analysis of Systems, 12th International Conference,
TACAS 2006 Held as Part of the Joint European
Conferences on Theory and Practice of Software,
ETAPS 2006, Vienna, Austria, March 25 - April 2,
2006, Proceedings},
booktitle = {TACAS},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {3920},
month = apr,
year = {2006},
isbn = {3-540-33056-9},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{POEM,
author = {Peter Niebert and
Hongyang Qu},
title = {The Implementation of Mazurkiewicz Traces in POEM.},
booktitle = {ATVA},
year = {2006},
pages = {508-522},
ee = {http://dx.doi.org/10.1007/11901914_37},
crossref = {DBLP:conf/atva/2006},
bibsource = {DBLP, http://dblp.uni-trier.de},
abstract = {We present the implementation of the trace theory in
a new model checking tool framework, POEM, that has
a strong emphasis on Partial Order Methods. A tree
structure is used to store trace systems, which
allows sharing common prefixes among traces and
therefore, re- duces memory cost. This structure is
easy to extend to incorporate ad- ditional
features. Two applications are shown in the paper:
An extended structure to support an adequate order
for Local First Search, and an acceleration of event
zone based state space search for timed automata. },
pdf = {pdfs/poem.pdf}
}
@proceedings{DBLP:conf/atva/2006,
editor = {Susanne Graf and Wenhui Zhang},
title = {Automated Technology for Verification and Analysis,
4th International Symposium, ATVA 2006, Beijing,
China, October 23-26, 2006.},
booktitle = {ATVA},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {4218},
month = oct,
year = {2006},
isbn = {3-540-47237-1},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/forte/ElkindGPQ06,
author = {Edith Elkind and Blaise Genest and Doron Peled and
Hongyang Qu},
title = {Grey-Box Checking.},
booktitle = {FORTE},
year = {2006},
pages = {420-435},
ee = {http://dx.doi.org/10.1007/11888116_30},
crossref = {DBLP:conf/forte/2006},
bibsource = {DBLP, http://dblp.uni-trier.de},
abstract = {There are many cases where we want to verify a
system that does not have a usable formal model: the
model may be missing, out of date, or simply too big
to be used. A possible method is to analyze the
system while learning the model (black box
checking). However, learning may be an expensive
task, thus it needs to be guided, e.g., using the
checked property or an inaccurate model (adaptive
model checking). In this paper, we consider the case
where some of the system components are completely
specified (white boxes), while others are unknown
(black boxes), giving rise to a grey box system.We
provide algorithms and lower bounds, as well as
experimental results for this model. },
pdf = {pdfs/greybox6.pdf}
}
@proceedings{DBLP:conf/forte/2006,
editor = {Elie Najm and Jean-Fran\c{c}ois Pradat-Peyre and
V{\'e}ronique Donzeau-Gouge},
title = {Formal Techniques for Networked and Distributed
Systems - FORTE 2006, 26th IFIP WG 6.1 International
Conference, Paris, France, September 26-29, 2006.},
booktitle = {FORTE},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {4229},
month = sep,
year = {2006},
isbn = {3-540-46219-8},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/ictac/KurbanNQV06,
author = {Marcos E. Kurb{\'a}n and
Peter Niebert and
Hongyang Qu and
Walter Vogler},
title = {Stronger Reduction Criteria for Local First Search.},
booktitle = {ICTAC},
year = 2006,
pages = {108-122},
ee = {http://dx.doi.org/10.1007/11921240_8},
crossref = {DBLP:conf/ictac/2006},
bibsource = {DBLP, http://dblp.uni-trier.de},
abstract = {Local First Search (LFS) is a partial order
technique for reducing the number of states to be
explored when trying to decide reachability of a
local (component) property in a parallel system; it
is based on an analysis of the structure of the
partial orders of executions in such
systems. Intuitively, LFS is based on a criterion
that allows to guide the search for such local
properties by limiting the Èconcurrent progressÉ of
components. In this paper, we elaborate the analysis
of the partial orders in ques- tion and obtain
related but significantly stronger criteria for
reductions, show their relation to the previously
established criterion, and discuss the algorithmics
of the proposed improvement. Our contribution is
both fundamental in providing better insights into
LFS and practical in pro- viding an improvement of
high potential. },
pdf = {pdfs/strongerlfs.pdf}
}
@proceedings{DBLP:conf/ictac/2006,
editor = {Kamel Barkaoui and Ana Cavalcanti and Antonio
Cerone},
title = {Theoretical Aspects of Computing - ICTAC 2006, Third
International Colloquium, Tunis, Tunisia, November
20-24, 2006, Proceedings},
booktitle = {ICTAC},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {4281},
month = nov,
year = {2006},
isbn = {3-540-48815-4},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/formats/NiebertQ06,
author = {Peter Niebert and Hongyang Qu},
title = {Adding Invariants to Event Zone Automata.},
booktitle = {FORMATS},
year = {2006},
pages = {290-305},
ee = {http://dx.doi.org/10.1007/11867340_21},
crossref = {DBLP:conf/formats/2006},
bibsource = {DBLP, http://dblp.uni-trier.de},
abstract = {Recently, a new approach to the symbolic model
checking of timed automata based on a partial order
semantics was introduced, which relies on event
zones that use vectors of event occurrences instead
of clock zones that use vectors of clock values
grouped in polyhedral clock constraints. A key
property of that approach is that the exchange of
independent actions in a sequence preserves the
event zones, whereas the clock zone may change. As a
result, symbolic state exploration with event zones
rather than clock zones can result in significant
reductions in the number of symbolic states
explored. Moreover, the formal development allowed
for the class of timed automata proposed by
Alur-Dill, except for state invariants. In this
work, we show how to extend the event zone approach
to net- works of automata with local state
invariants, an important feature for modeling
complex timed systems. We give a formalization of
local in- variants that avoids the burden of formal
specialization to a particular kind of model: Rather
than formalizing local states, we attach to each
transition an urgency constraint that relates to the
global state invariant like a local invariant, thus
allowing straight a forward application of the
current work to networks of timed
automata. Surprisingly, under highly reasonable
assumptions, the independence relation as previously
formalised without invariants, is preserved. We give
a Èrelaxed seman- ticsÉ of runs in the presence of
these local invariants and show that it is
consistent with non-relaxed semantics. We have
integrated the extension into a prototype tool with
event zones and can report very promissing
experimental results. },
pdf = {pdfs/invariantsforeventzones.pdf}
}
@proceedings{DBLP:conf/formats/2006,
editor = {Eugene Asarin and Patricia Bouyer},
title = {Formal Modeling and Analysis of Timed Systems, 4th
International Conference, FORMATS 2006, Paris,
France, September 25-27, 2006, Proceedings},
booktitle = {FORMATS},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {4202},
month = sep,
year = {2006},
isbn = {3-540-45026-2},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{ORDER-24-3,
author = {Santocanale, Luigi},
title = {On the join depenency relation in multinomial
lattices},
journal = {Order},
volume = 24,
number = 3,
pages = {155--179},
month = aug,
year = 2007,
month = aug,
note = {@Springer},
arxiv = {http://arxiv.org/math.CO/0510098},
hal = {http://hal.archives-ouvertes.fr/hal-00142355},
abstract = {We study the congruence lattices of the multinomial
lattices $L(v)$ introduced by Bennett and
Birkhoff. Our main motivation is to investigate
Parikh equivalence relations that model concurrent
computation. We accomplish this goal by providing an
explicit description of the join dependency relation
between two join irreducible elements and of its
reflexive transitive closure. The explicit
description emphasizes several properties and makes
it possible to separate the equational theories of
multinomial lattices by their dimensions. In their
covering of non modular varieties Jipsen and Rose
define a sequence of equations $SD_{n}(\land)$, for
$n \geq 0$. Our main result sounds as follows:
\emph{if $v = (v_{1},\ldots ,v_{n}) \in N^{n}$ and
$v_{i} > 0$ for $i = 1,\ldots ,n$, then the
multinomial lattice $L(v)$ satisfies
$SD_{n-1}(\land)$ and fails $SD_{n-2}(\land)$}.}
}
@unpublished{santocanale:DSL,
author = {Luigi Santocanale},
title = {Derived Semidistributive Lattices},
month = jan,
year = 2007,
pdf = {pdfs/DSD.pdf},
note = {Accepted for presention at the conference OAL 2007,
Nashville, USA, june 12 2007}
}
@inproceedings{CONCUR2007,
author = {Santocanale, Luigi},
title = {A Nice Labelling for Tree-Like Event Structures of
Degree 3},
booktitle = {CONCUR 2007},
pages = {151--165},
year = 2007,
month = sep,
editor = {L. Caires and V.T. Vasconcelos},
volume = 4703,
series = {\href{http://www.springer.de/comp/lncs/index.html}{Lecture Notes in Computer Science}},
address = {Berlin Heidelberg},
publisher = {Springer-Verlag},
note = {@Springer-Verlag},
hal = {http://hal.archives-ouvertes.fr/hal-00142349},
arxiv = {http://arxiv.org/abs/0704.2355},
abstract = {We address the problem of finding nice labellings
for event structures of degree $3$. We develop a
minimum theory by which we prove that the labelling
number of an event structure of degree $3$ is
bounded by a linear function of the height. The main
theorem we present in this paper states that event
structures of degree $3$ whose causality order is a
tree have a nice labelling with $3$ colors. Finally,
we exemplify how to use this theorem to construct
upper bounds for the labelling number of other event
structures of degree $3$.}
}
@unpublished{DSDL,
author = {Santocanale, Luigi},
title = {Derived Semidistributive Lattices},
hal = {http://hal.archives-ouvertes.fr/hal-00165699/},
arxiv = {http://arxiv.org/abs/0708.1695},
note = {Accepted for publication in the journal Algebra Universalis},
month = jul,
year = 2007,
abstract = {For $L$ a finite lattice, let $\mathcal{C}(L)$
denote the set of pairs $\gamma =
(\gamma_{0},\gamma_{1})$ such that $\gamma_{0}$ is a
lower cover of $\gamma_{1}$ and order it as follows:
$\gamma \leq \delta$ iff $\gamma_{0} \leq
\delta_{0}$, $\gamma_{1} \leq \delta_{1}$, but
$\gamma_{1} \leq \delta_{0}$ does not hold. Let
$\mathcal{C}(L,\gamma)$ denote the connected
component of $\gamma$ in this poset. Our main result
states that $\mathcal{C}(L,\gamma)$ is a
semidistributive lattice if $L$ is semidistributive,
and that $\mathcal{C}(L,\gamma)$ is a bounded
lattice if $L$ is bounded. Let $\mathcal{S}_{n}$ be
the permutohedron on $n$ letters and
$\mathcal{T}_{n}$ be the associahedron on $n+1$
letters. Explicit computations show that
$\mathcal{C}(\mathcal{S}_{n},\alpha) =
\mathcal{S}_{n-1}$ and
$\mathcal{C}(\mathcal{T}_{n},\alpha) =
\mathcal{T}_{n-1}$, up to isomorphism, whenever
$\alpha$ is an atom. These results are consequences
of new characterizations of finite join
semidistributive and finite lower bounded lattices:
(i) a finite lattice is join semidistributive if and
only if the projection sending $\gamma \in
\mathcal{C}(L)$ to $\gamma_{0} \in L$ creates
pullbacks, (ii) a finite join semidistributive
lattice is lower bounded if and only if it has a
strict facet labelling. Strict facet labellings, as
defined here, are generalization of the tools used
by Barbut et al. to prove that lattices of Coxeter
groups are bounded.}
}
@inproceedings{entanglement2,
author = {Belkhir, Walid and Santocanale, Luigi},
title = {Undirected Graphs of Entanglement 2},
note = {@Springer-Verlag},
booktitle = {FSTTCS 2007},
pages = {508--519},
volume = {4855},
year = 2007,
editor = {Arvind, V. and Prasad, S.},
series = {\href{http://www.springer.de/comp/lncs/index.html}{Lecture Notes in Computer Science}},
month = dec,
publisher = {Springer-Verlag},
hal = {http://hal.archives-ouvertes.fr/hal-00144355},
arxiv = {http://fr.arxiv.org/abs/0705.0419},
abstract = {Entanglement is a complexity measure of directed
graphs that origins in fixed point theory. This
measure has shown its use in designing efficient
algorithms to verify logical properties of
transition systems. We are interested in the problem
of deciding whether a graph has entanglement at most
$k$. As this measure is defined by means of games,
game theoretic ideas naturally lead to design
polynomial algorithms that, for fixed $k$, decide
the problem. Known characterizations of directed
graphs of entanglement at most $1$ lead, for $k =
1$, to design even faster algorithms. In this paper
we present an explicit characterization of
\emph{undirected} graphs of entanglement at most
$2$. With such a characterization at hand, we devise
a linear time algorithm to decide whether an
undirected graph has this property.}
}
@inproceedings{LPAR2007,
author = {Venema, Yde and Santocanale, Luigi},
title = {Completeness for flat modal fixpoint logics},
booktitle = {LPAR 2007},
pages = {499--513},
year = 2007,
editor = {Dershowitz, Nachum and Voronkov, Andrei},
series = {\href{http://www.springer.de/comp/lnai/index.html}{Lecture Notes in Artificial Intelligence}},
volume = {4790},
month = oct,
publisher = {Springer-Verlag},
note = {@Springer-Verlag},
pdf = {http://www.cmi.univ-mrs.fr/~lsantoca/papers/lpar07.pdf},
abstract = { Given a set $\Gamma$ of modal formulas of the form
$\gamma(x,\vec{p})$, where $x$ occurs positively in
$\gamma$, the language $\mathcal{L}_{\#}(\Gamma)$ is
obtained by adding to the language of polymodal
logic $K$ connectives $\#_{\gamma}$, $\gamma \in
\Gamma$. Each term $\#_{\gamma}$ is meant to be
interpreted as the least fixed point of the
functional interpretation of the term
$\gamma(x)$. Given such a $\Gamma$, we construct
an axiom system $\mathcal{K}_{\#}(\Gamma)$ which is
sound and complete w.r.t. the concrete
interpretation of the language $\mathcal{L}_{\#}(\Gamma)$
on Kripke frames. If $\Gamma$ is finite, then
$\mathcal{K}_{\#}(\Gamma)$ is a finite set of axioms
and inference rules. }
}
@inproceedings{LPAR08,
author = {Belkhir, Walid and Santocanale, Luigi},
title = {The variable hierarchy for the lattice
$\mu$-calculus},
pdf = {papers/LPAR08.pdf},
hal = {http://hal.archives-ouvertes.fr/hal-00178806/},
arxiv = {http://fr.arxiv.org/abs/0710.2419},
month = nov,
year = 2008,
pages = {605-620},
abstract = {Parity games are combinatorial representations of
closed Boolean $\mu$-terms. By adding to them draw
positions, they have been organized by Arnold and
one of the authors into a $\mu$-calculus. As done by
Berwanger et al. for the propositional modal
$\mu$-calculus, it is possible to classify parity
games into levels of hierarchy according to the
number of fixed-point variables. We ask whether this
hierarchy collapses w.r.t. the standard
interpretation of the games $\mu$-calculus into the
class of all complete lattices. We answer this
question negatively by providing, for each $n \geq
1$, a parity game $G_n$ with these properties: it
unravels to a $\mu$-term built up with $n$
fixed-point variables, it is semantically equivalent
to no game with strictly less than $n-2$ fixed-point
variables.},
crossref = {PROCSLPAR2008},
notefr = {nil}
}
@proceedings{PROCSLPAR2008,
editor = {Iliano Cervesato and Helmut Veith and Andrei
Voronkov},
booktitle = {LPAR 2008},
note = {Proceedings of the 15th International Conference on
Logic for Programming, Artificial Intelligence, and
Reasoning, Doha, Qatar, November 22-27, 2008. },
publisher = {Springer},
series = {\href{http://www.springer.de/comp/lncs/index.html}{Lecture Notes in Computer Science}},
volume = {5330},
year = {2008},
isbn = {978-3-540-89438-4},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{ROGICS08,
author = {Santocanale, Luigi},
title = {Combinatorics from Concurrency: the Nice Labelling
Problem for Event Structures},
pages = {411-419},
crossref = {PROCSROGICS08},
pdf = {papers/rogics08.pdf},
year = 2008,
abstract = {An event structures is a mathematical model of a
concurrent process. It consists of a set of local
events ordered by a causality relation and separated
by a conflict relation. A global state, or
configuration, is an order ideal whose elements are
pairwise not in conflict. Configurations, ordered by
subset inclusion, form a poset whose Hasse diagram
codes the state-transition graph of the process. By
labelling edges, the state-transition graph can be
enriched with the structure of a deterministic
concurrent automaton on some alphabet. The
\emph{nice labelling problem} asks to minimize the
cardinality of the alphabet. In this talk we shall
first introduce the nice labelling problem and show
how it translates to a graph coloring problem. We
shall then survey on the problem and present the
results that are available to us nowadays. Thus we
shall The survey will also be the occasion to point
out new perspectives, open problems, and research
paths. },
notefr = {nil}
}
@proceedings{PROCSROGICS08,
booktitle = {ROGICS'08},
note = {Proceedings of the International Conference on
Relations, Orders and Graphs : Interaction with
Computer Science. 12-17 May, 2008, Mahdia, Tunisia},
editor = {Boudabbous, Youssef and Zaguia, Nejib},
month = may,
year = 2008,
notecucu = {Proceedings of the International Conference on
Relations, Orders and Graphs : Interaction with
Computer Science. 12-17 May, 2008, Mahdia, Tunisia },
notefrcucu = {Proceedings of the International Conference on
Relations, Orders and Graphs : Interaction with
Computer Science. 12-17 May, 2008, Mahdia, Tunisia },
mylabel = {BZ}
}
@unpublished{variablehierarchy,
author = {Belkhir, Walid and Santocanale, Luigi},
title = {The variable hierarchy for the games $\mu$-calculus},
note = {Accepted for publication in the journal Annals of Pure and Applied Logic},
hal = {http://hal.archives-ouvertes.fr/hal-00178806/},
arxiv = {http://fr.arxiv.org/abs/0710.2419},
month = oct,
year = 2007,
abstract = {Parity games are combinatorial representations of
closed Boolean $\mu$-terms. By adding to them draw
positions, they have been organized by Arnold and
one of the authors into a $\mu$-calculus. As done by
Berwanger et al. for the propositional modal
$\mu$-calculus, it is possible to classify parity
games into levels of hierarchy according to the
number of fixed-point variables. We ask whether this
hierarchy collapses w.r.t. the standard
interpretation of the games $\mu$-calculus into the
class of all complete lattices. We answer this
question negatively by providing, for each $n \geq
1$, a parity game $G_n$ with these properties: it
unravels to a $\mu$-term built up with $n$
fixed-point variables, it is semantically equivalent
to no game with strictly less than $n-2$ fixed-point
variables.}
}
@unpublished{CONCUR2007IEC,
author = {Santocanale, Luigi},
title = {A Nice Labelling for Tree-Like Event Structures of
Degree 3},
month = may,
year = 2008,
note = {Accepted for publication in a special issue of the journal Information
and Computation dedicated to conference CONCUR 2007},
hal = {http://hal.archives-ouvertes.fr/hal-00369451/fr/},
arxiv = {http://fr.arxiv.org/abs/0903.3462}
}
@unpublished{SP_preprint,
author = {Cockett, Robin and Santocanale, Luigi},
title = {On the word problem for ${\Sigma}{\Pi}$-categories, and
the properties of two-way communication},
note = {Submitted},
month = apr,
year = 2009,
hal = {http://hal.archives-ouvertes.fr/hal-00374654/fr/},
arxiv = {http://fr.arxiv.org/abs/0904.1529},
abstract = {The word problem for categories with free products
and coproducts (sums), SP-categories, is directly
related to the problem of determining the
equivalence of certain processes. Indeed, the maps
in these categories may be directly interpreted as
processes which communicate by two-way channels. The
maps of an SP-category may also be viewed as a proof
theory for a simple logic with a game theoretic
intepretation. The cut-elimination procedure for
this logic determines equality only up to certain
permuting conversions. As the equality classes under
these permuting conversions are finite, it is easy
to see that equality between cut-free terms (even in
the presence of the additive units) is
decidable. Unfortunately, this does not yield a
tractable decision algorithm as these equivalence
classes can contain exponentially many
terms. However, the rather special properties of
these free categories -- and, thus, of two-way
communication -- allow one to devise a tractable
algorithm for equality. We show that, restricted to
cut-free terms s,t : X --> A, the decision procedure
runs in time polynomial on |X||A|, the product of
the sizes of the domain and codomain type.}
}
@booklet{hdr,
author = {Santocanale, Luigi},
title = {Structures alg\'ebriques et d'ordre en logique et
concurrence},
school = {Universit{\'e} de Provence},
year = 2008,
month = dec,
abstract = {Nous souhaitons illustrer comment la notion de
structure, alg\'ebrique et d'ordre, peut \^etre un
guide fructuex dans l'\'etude de sujets importants
de l'informatique tels que les processus concurrents
et les logiques modales et temporales pour la
v\'erification des syst\`emes informatiques.},
note = {{H}abiltation \`a Diriger les Recherches,
Universit{\'e} de Provence},
notefr = {Date de soutenance: le 9 d\'ecembre 2008. Composition
du jury~: Composition du jury: M Andr\'e Arnold
(Bordeaux), M Yves Lafont (Marseille), M R\'emi Morin
(Marseille), M Yde Venema (Amsterdam), M Friedrich
Wehrung (Caen), M Denis Lugiez (Marseille,
rapporteur), M Maurice Pouzet (Lyon, Calgary,
rapporteur), M Igor Walukiewicz (Bordeaux,
rapporteur).},
tel = {http://tel.archives-ouvertes.fr/tel-00369583/fr/}
}
@article{ENTCS230,
author = {Luigi Santocanale},
title = {Topological Properties of Event Structures},
journal = {Electr. Notes Theor. Comput. Sci.},
volume = {230},
year = {2009},
pages = {149-160},
ee = {http://dx.doi.org/10.1016/j.entcs.2009.02.023},
bibsource = {DBLP, http://dblp.uni-trier.de},
pdf = {http://www.cmi.univ-mrs.fr/~lsantoca/papers/GETCO06.pdf},
abstract = {Motivated by the nice labeling problem for event
structures, we study the topological properties of
the associated graphs. For each $n \geq 0$, we
exhibit a graph $G_{n}$ that cannot occur on an
antichain as a subgraph of the graph of an event
structure of degree $n$. The clique complexes of the
graphs $G_{n}$ are disks ($n$ even) and spheres ($n$
odd) in increasing dimensions. We strengthen the
result for event structure of degree $3$: cycles of
length greater than $3$ do not occur on antichains
as subgraphs. This amount to saying that the clique
complex of the graph of an event structure of degree
$3$ is acyclic.},
note = {{G}ETCO 2006, Geometrical and Topological Methods in
Concurrency, Bonn, August 26 2006.}
}
@phdthesis{Belkhir,
author = {Belkhir, Walid},
title = {Algebra and Combinatorics of Parity Games},
school = {Université de Provence},
year = 2008,
month = dec
}
@unpublished{TACL09,
author = {Luigi Santocanale},
title = {A duality for finite lattices},
month = jan,
year = 2009,
pdf = {papers/TACL09.pdf},
note = {To be presented at the conference TACL 2009,
Amsterdam, Holland, july 7-11 2009}
}
@inproceedings{DBLP:conf/csr/BaudruM06,
author = {Nicolas Baudru and
R{\'e}mi Morin},
title = {Unfolding Synthesis of Asynchronous Automata.},
booktitle = {CSR},
year = {2006},
pages = {46-57},
ee = {http://dx.doi.org/10.1007/11753728_8},
crossref = {DBLP:conf/csr/2006},
bibsource = {DBLP, http://dblp.uni-trier.de},
pdf = {pdfs/CSR06_org_LNCS_3967.pdf},
abstract = {Zielonka's theorem shows that each regular set of
Mazurkiewicz traces can be implemented as a system
of synchronized processes provided with some
distributed control structure called an asynchronous
automaton. This paper gives a new algorithm for the
synthesis of a non-deterministic asynchronous
automaton from a regular Mazurkiewicz trace
language. Our approach is based on an unfolding
procedure that improves the complexity of Zielonka's
and Pighizzini's techniques: Our construction is
polynomial in terms of the number of states but
still double-exponential in the size of the
alphabet. As opposed to Métivier's work, our
algorithm does not restrict to acyclic dependence
alphabets. }
}
@proceedings{DBLP:conf/csr/2006,
editor = {Dima Grigoriev and John Harrison and Edward
A. Hirsch},
title = {Computer Science - Theory and Applications, First
International Computer Science Symposium in Russia,
CSR 2006, St. Petersburg, Russia, June 8-12, 2006,
Proceedings},
booktitle = {CSR},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {3967},
month = jun,
year = {2006},
isbn = {3-540-34166-8},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/apn/BaudruM06,
author = {Nicolas Baudru and
R{\'e}mi Morin},
title = {The Synthesis Problem of Netcharts.},
booktitle = {ICATPN},
year = {2006},
pages = {84-104},
ee = {http://dx.doi.org/10.1007/11767589_6},
crossref = {DBLP:conf/apn/2006},
bibsource = {DBLP, http://dblp.uni-trier.de},
pdf = {pdfs/LNCS_4024_ICATPN_06_Baudru_Morin.pdf},
abstract = {A netchart is basically a Petri net whose places are
located at some process and whose transitions are
labeled by message sequence charts (MSCs). Two
recent papers showed independently that any
globally-cooperative high-level MSC corresponds to
the behaviors of some communicating finite-state
machine -- or equivalently a netchart. These
difficult results rely either on ThomasÇ graph
acceptors or ZielonkaÇs construction of asynchronous
automata. In this paper we give a direct and
self-contained synthesis of netcharts from
globally-cooperative high-level MSCs by means of a
simpler unfolding procedure.}
}
@proceedings{DBLP:conf/apn/2006,
editor = {Susanna Donatelli and P. S. Thiagarajan},
title = {Petri Nets and Other Models of Concurrency - ICATPN
2006, 27th International Conference on Applications
and Theory of Petri Nets and Other Models of
Concurrency, Turku, Finland, June 26-30, 2006,
Proceedings},
booktitle = {ICATPN},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {4024},
month = jun,
year = {2006},
isbn = {3-540-34699-6},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/fsttcs/BaudruM07,
author = {Nicolas Baudru and
R{\'e}mi Morin},
title = {Synthesis of Safe Message-Passing Systems},
booktitle = {FSTTCS},
year = {2007},
pages = {277-289},
ee = {http://dx.doi.org/10.1007/978-3-540-77050-3_23},
crossref = {DBLP:conf/fsttcs/2007},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/fsttcs/2007,
editor = {Vikraman Arvind and
Sanjiva Prasad},
title = {FSTTCS 2007: Foundations of Software Technology and Theoretical
Computer Science, 27th International Conference, New Delhi,
India, December 12-14, 2007, Proceedings},
booktitle = {FSTTCS},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {4855},
year = {2007},
isbn = {978-3-540-77049-7},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/concur/Morin08,
author = {R{\'e}mi Morin},
title = {Semantics of Deterministic Shared-Memory Systems},
booktitle = {CONCUR},
year = {2008},
pages = {36-51},
ee = {http://dx.doi.org/10.1007/978-3-540-85361-9_7},
crossref = {DBLP:conf/concur/2008},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/concur/2008,
editor = {Franck van Breugel and
Marsha Chechik},
title = {CONCUR 2008 - Concurrency Theory, 19th International Conference,
CONCUR 2008, Toronto, Canada, August 19-22, 2008. Proceedings},
booktitle = {CONCUR},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {5201},
year = {2008},
isbn = {978-3-540-85360-2},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/dlt/Morin08,
author = {R{\'e}mi Morin},
title = {MSO Logic for Unambiguous Shared-Memory Systems},
booktitle = {Developments in Language Theory},
year = {2008},
pages = {516-528},
ee = {http://dx.doi.org/10.1007/978-3-540-85780-8_41},
crossref = {DBLP:conf/dlt/2008},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/dlt/2008,
editor = {Masami Ito and
Masafumi Toyama},
title = {Developments in Language Theory, 12th International Conference,
DLT 2008, Kyoto, Japan, September 16-19, 2008. Proceedings},
booktitle = {Developments in Language Theory},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {5257},
year = {2008},
isbn = {978-3-540-85779-2},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@unpublished{EPndsms,
author = {Morin, R{\'e}mi},
title = {Expressive power of non-deterministic shared-memory
systems},
note = {submitted},
month = sep,
year = {2008}
}
@inproceedings{DBLP:conf/wdag/ChalopinGM08,
author = {J{\'e}r{\'e}mie Chalopin and
Emmanuel Godard and
Yves M{\'e}tivier},
title = {Local Terminations and Distributed Computability in Anonymous
Networks},
booktitle = {DISC},
year = {2008},
pages = {47-62},
ee = {http://dx.doi.org/10.1007/978-3-540-87779-0_4},
crossref = {DBLP:conf/wdag/2008},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/wdag/2008,
editor = {Gadi Taubenfeld},
title = {Distributed Computing, 22nd International Symposium, DISC
2008, Arcachon, France, September 22-24, 2008. Proceedings},
booktitle = {DISC},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {5218},
year = {2008},
isbn = {978-3-540-87778-3},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
This file was generated by bibtex2html 1.93.