@TECHREPORT{01-2002-Gardi,
AUTHOR = {Frederic Gardi},
TITLE = {{On the Partition of an Interval Graph into Proper
Interval Subgraphs}},
INSTITUTION = {{LIF}},
ADDRESS = {Marseille, France},
TYPE = {Research report},
NUMBER = {01-2002},
MONTH = {April},
YEAR = 2002,
URL =
{http://www.lim.univ-mrs.fr/Rapports/01-2002-Gardi.html},
ABSTRACT = {In this paper the problem of the partition of an
interval graph into proper interval subgraphs is
considered. It arises in a study about the problem
of working schedules planning. Here we give some
upper bounds on the minimum size of such a partition
as well as some efficient algorithms to compute
it. In particular, we prove that every K1,t-free
interval graph, t >= 3, is partitionnable into t/2
proper interval subgraphs. The proof of this
proposition yields a linear or quasi-linear time
algorithm to compute such a partition. Moreover, we
give a linear-time algorithm to compute the minimum
t such that an interval graph is K1,t-free. Next, we
show that each n-vertex interval graph can be
partitionned into O(log n) proper interval subgraphs
always in linear or quasi-linear time. Finally, we
construct interval graphs for which this bound is
sharp.},
tasks = {1.4},
funding = {partially by AMETIST}
}
@TECHREPORT{02-2002-Gardi,
AUTHOR = {Frederic Gardi},
TITLE = {{The Mutual Exclusion Scheduling Problem for Proper
Interval Graphs}},
INSTITUTION = {{LIF}},
ADDRESS = {Marseille, France},
TYPE = {Research report},
NUMBER = {02-2002},
MONTH = {April},
YEAR = 2002,
URL =
{http://www.lim.univ-mrs.fr/Rapports/02-2002-Gardi.html},
ABSTRACT = {In this paper, the mutual exclusion scheduling (MES)
problem for proper interval graphs is
considered. Given an undirected graph G and a
non-negative integer k, the problem is to find a
minimum coloring of G, such that each colour is used
at most k times. The complexity of this problem is
known to be NP-complete for interval graphs. We
prove that MES can be solved in linear time for
proper interval graphs thanks to a greedy
algorithm. As a byproduct of the proof of this
result, we also obtain a linear-time algorithm to
solve MES for interval graphs under certain
conditions. Finally, this study yields some results
about the complexity of finding an uniform coloring
of proper interval graphs.},
tasks = {1.4},
funding = {partially funded by AMETIST}
}
@TECHREPORT{07-2002-Gardi,
AUTHOR = {Frederic Gardi},
TITLE = {{An efficient algorithm for maximum disjoint
matchings in a set of intervals and related
problems}},
INSTITUTION = {{LIF}},
ADDRESS = {Marseille, France},
TYPE = {Research report},
NUMBER = {07-2002},
MONTH = {May},
YEAR = {2002},
URL =
{http://www.lim.univ-mrs.fr/Rapports/07-2002-Gardi.html},
ABSTRACT = {In this paper we consider the problem of determining
a maximum matching in a set of intervals (two
intervals can be matched if they are disjoint). We
propose an incremental algorithm to compute such a
maximum disjoint matching. We show that this
algorithm runs in O(n) time if the list of sorted
endpoints of the set of intervals is given in
input. This result is applied to solve efficiently
particular cases of two scheduling problems: working
schedules planning and mutual exclusion scheduling
for interval graphs.},
tasks = {1.4},
funding = {partially funded by AMETIST}
}
@TECHREPORT{11-2003-Gardi,
AUTHOR = {Frederic Gardi},
TITLE = {{A note on the Roberts characterization of proper
and unit interval graphs}},
INSTITUTION = {{LIF}},
ADDRESS = {Marseille, France},
TYPE = {Research report},
NUMBER = {11-2003},
MONTH = {January},
YEAR = {2003},
URL =
{http://www.lim.univ-mrs.fr/Rapports/11-2003-Gardi.html},
ABSTRACT = {In this note, a constructive proof is given that the
classes of proper interval graphs and unit interval
graphs coincide, a result originally established by
F.S. Roberts.},
tasks = {1.4},
funding = {partially funded by AMETIST}
}
@TECHREPORT{12-2003-Gardi,
AUTHOR = {Frederic Gardi},
TITLE = {{Mutual exclusion scheduling with interval graphs
and related classes}},
INSTITUTION = {{LIF}},
ADDRESS = {Marseille, France},
TYPE = {Research report},
NUMBER = {12-2003},
MONTH = {May},
YEAR = {2003},
URL =
{http://www.lim.univ-mrs.fr/Rapports/12-2003-Gardi.html},
ABSTRACT = {In this note, the mutual exclusion scheduling
problem is considered. Given an undirected graph G
and an integer k, the problem is to find a minimum
coloring of G such that each color is used at most k
times. The cardinality of such a coloring is denoted
with chi(G,k). For intervals graphs, the problem is
known to be NP-complete even for fixed k >= 4. We
prove that if an interval graph or more generally a
circular-arc graph G with n vertices admits a
coloring such that each colour is used at least k
times, then chi(G,k) equals the lower bound
ceil(n/k). The proof yields a linear-time algorithm
to solve the problem in this case which finds
applications in schedules planning. Then, the
assertion is extended to the class of triangulated
graphs for k <= 3 and disproved for bounded
tolerance graphs and co-comparability graphs.},
tasks = {1.4},
funding = {partially funded by AMETIST}
}
@InProceedings{BMNZ02,
author = {S. Bornot and R. Morin and P. Niebert and S. Zennou},
title = {Black Box Unfolding with Local First Search},
booktitle = {TACAS'2002},
pages = {386 ff.},
year = 2002,
volume = 2280,
series = {LNCS},
ABSTRACT = {McMillan s unfolding approach to the reachability
problem in 1-safe Petri nets and its later
improvements by Esparza-Romer-Vogler have proven in
practice as a very eective method to avoid
state-explosion. This method computes a complete
finite prefix of the infinite branching process of a
net. On the other hand, the Local First Search
approach (LFS) was recently introduced as a new
partial order reduction technique which
characterizes a restricted subset of configurations
that need to be explored to check local
properties. In this paper we amalgamate the two
approaches: We combine the reduction criterion of
LFS with the notions of an adequate order and cuto
events essential to the unfolding approach. As a
result, our new LFS method computes a reduced
transition system without the problem of state
duplication (present in the original LFS). Since it
works for any transition system with an independence
relation, this black box partial unfolding remains
more general than the unfolding of Petri
nets. Experiments show that the combination gives
improved reductions compared to the original LFS.},
url = {http://www.cmi.univ-mrs.fr/~niebert/docs/tacas02.pdf},
tasks = {2.3.a},
funding = {pre AMETIST funding}
}
@InProceedings{LNZ02,
author = {D. Lugiez and P. Niebert and S. Zennou},
title = {Dynamic Bounds and Transition Merging for Local
First Search},
booktitle = {Model Checking Software},
pages = {221--229},
year = 2002,
volume = 2318,
series = {LNCS},
ABSTRACT = {Local First Search (LFS) was recently introduced as
a new partial order reduction approach. It is based
on the observation that local properties can be
found searching on paths with a low degree
(LFSnumber) of concurrent progress. It has shown its
potential to find sequences to local states fast. In
this paper, we explore several improvements of LFS:
On the one hand, we propose a replacement of the
static bound on LFS-numbers by a dynamic criterion
to detect exhaustion of reachable local properties
faster. On the other hand, we explore the
possibilities of combining LFS with other partial
order reduction methods. It turns out that the
combination with transition merging is possible and
rewarding, while the sleep-set method is
incompatible with LFS.},
url = {http://www.cmi.univ-mrs.fr/~niebert/docs/sw02.pdf},
tasks = {2.3.a},
funding = {pre AMETIST funding}
}
@Article{Nie03,
author = {Peter Niebert},
title = {Petri Nets An Intuitive Formalism for Concurrency, 2
parts (in German)},
journal = {Automatisierungs Technik},
year = 2003,
month = 3,
ABSTRACT = {This two part article is part of a series 'Theory
for the professional' in this well known German
journal of control engineering. It is aimed to
proliferation of knowledge. In the second part, we
also introduce Time Petri nets.},
url =
{http://www.cmi.univ-mrs.fr/~niebert/docs/at0303304.pdf},
tasks = {4.3},
funding = {purely funded by AMETIST}
}
@TechReport{albert02,
author = {Sarah Albert},
title = {CYBERNETIX Case Study -- Informal description},
institution = {Cybern{\'e}tix - LIF},
year = {2002},
URL = {http;//www.cmi.univ-mrs.fr/~niebert/docs/cyx.pdf},
ABSTRACT = {This paper is a basic presentation of the first case
study proposed by Cyberntix. The aim is to give a
first idea of the system, presenting the objectives,
the characteristics of the system and the
constraints and to present the questions concerning
this case study and the challenges to the different
partners.},
TASKS = {3.1.1},
funding = {purely funded by AMETIST}
}
@TechReport{albert02designcpn,
author = {S. Albert},
title = {{Design/CPN model of Cybernetix Case Study}},
institution = {Cybern{\'e}tix - LIF},
year = 2002,
ABSTRACT = {Colored Petri Net model of the case study. The basic
idea for the choice of colored Petri nets for
modelling the case study is to represent cards as
value carrying tokens. To read and execute this
model, a (free) licence of Design/CPN, to be
obtained from http://www.daimi.au.dk/designCPN/, is
required.},
url =
{http://www.cmi.univ-mrs.fr/~niebert/docs/cybernetix-cpn.tgz},
tasks = {3.1.2}
}
@TechReport{albertniebert02a,
author = {Sarah Albert and Peter Niebert},
title = {Cybern{\'e}tix Case Study -- Performance Analysis --
Optimality of the SuperSingle mode},
institution = {Cybern{\'e}tix -LIF},
year = 2002,
ABSTRACT = {We do a performance analysis of continuous
production with the Batch Mode and the Super Single
mode for the Cybern{\'e}tix case study. With a refined
upper bound we explain the use of holes on the
conveyor belt and show that the performance of the
Super Single is extremely close to an upper bound
for the average throughput. The proof technique for
the upper bound of the throughput may have interest
beyond this application.},
url =
{http://www.cmi.univ-mrs.fr/~niebert/docs/cybernetix-optimality.pdf},
tasks = {3.1.2}
}
@Misc{d.03:_clock_mazur_traces_partial_order,
author = {D. Lugiez, P. Niebert, S. Zennou},
title = {Clocked Mazurkiewicz Traces for Partial Order
Reductions of Timed Automata},
year = 2003,
ABSTRACT = { Our work a new approach on the question of partial
order reductions of timed automata. As a formal
framework, we first we develop a theory of clocked
and timed Mazur\-kie\-wicz traces to represent
executions of networks of timed automata with timing
constraints. Then, based on a language theoretic
framework, we construct finite symbolic automata for
the reachability problem in two steps: Event zones
are used to represent abstractly possible extensions
of a given clocked trace. This construction yields
automata with desired commutation properties, but --
as shown by an examply -- which are unavoidably
infinite. In the second step, we use a finite index
equivalence -- which is not a right congruence --
for cutting paths in the infinite automaton without
losing reachable states. As a result, we obtain an
automaton avoiding the state splitting due to
interleaving but without restrictions of prior
approaches.},
url =
{http://www.cmi.univ-mrs.fr/~niebert/docs/clockedmazu.pdf},
tasks = {2.3.a},
funding = {purely funded by AMETIST}
}
@Misc{else02,
author = {Sarah Zennou and Manuel Yguel and Peter Niebert},
title = {ELSE: A new symbolic state generator for timed
automata},
year = 2003,
ABSTRACT = {We present ELSE, a new state generator for timed
automata. ELSE is based on VERIMAG s IF-2.0
specification language and is designed to be used
with state exploration tools like CADP. In
particular, it compiles IF-2.0 specifications to C
programs that link with CADP. It thus concentrates
on the generation of comparatively small state
spaces and integrates into existing tool chains. The
emphasis of the ELSE development is on fundamentally
di{\textregistered}erent data structures and algorithms, notably on
the level of zones. Rather than representing
possible values of clocks at a given symbolic state,
event zones represent in an abstract way the timing
constraints of past and future events. This approach
is useful for certain partial order reduction
approaches.},
url = {http://www.cmi.univ-mrs.fr/~niebert/docs/else.pdf},
tasks = {2.3.a,2.5},
funding = {purely funded by AMETIST}
}