franck-control.bib
@COMMENT{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{Command line: bib2bib -q -c category="control" -oc franck-control.cite -ob franck-control.bib mabib.bib}}
@COMMENT{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{Command line: bib2bib -s $date -s lex bib/mabib.bib}}
@COMMENT{{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{{Command line: bib2bib -s lex -s $date bib/mabib.bib}}
@COMMENT{{{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{{{Command line: bib2bib -s lex -s $date bib/mabib.bib}}
@COMMENT{{{{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{{{{Command line: bib2bib -s lex -s $date bib/mabib.bib}}
@TECHREPORT{cassez-wcet-2010,
AUTHOR = {Franck Cassez},
CATEGORY = {control},
LEX = {Da},
TITLE = {{Timed Games for Computing Worst-Case Execution-Times}},
INSTITUTION = {National ICT Australia},
YEAR = 2010,
TYPE = {Research Report},
MONTH = JUN,
PDF = {http://arxiv.org/pdf/1006.1951v1},
NOTE = {31 pages, arXiv:1006.1951v1 [cs.SE]},
ARXIV = {http://arxiv.org/abs/1006.1951},
ABSTRACT = { In this paper we introduce a framework for computing upper bounds yet
accurate WCET for hardware platforms with caches and pipelines. The methodology
we propose consists of 3 steps: 1) given a program to analyse, compute an
equivalent (WCET-wise) abstract program; 2) build a timed game by composing
this abstract program with a network of timed automata modeling the
architecture; and 3) compute the WCET as the optimal time to reach a winning
state in this game. We demonstrate the applicability of our framework on
standard benchmarks for an ARM9 processor with instruction and data caches, and
compute the WCET with UPPAAL-TiGA. We also show that this framework can easily
be extended to take into account dynamic changes in the speed of the processor
during program execution. }
}
@INPROCEEDINGS{cassez-hscc-09,
ABSTRACT = { In this paper, we show how to apply recent tools for the automatic
synthesis of robust and near-optimal controllers for a real
industrial case study. We show how to use three different classes of
models and their supporting existing tools, TiGA for
synthesis, PHAVer for verification, and {\sc Simulink} for
simulation, in a complementary way. We believe that this case study
shows that our tools have reached a level of maturity that allows us
to tackle interesting and relevant industrial control problems.},
AUTHOR = {Cassez, Franck and Jessen, Jan J. and Larsen, Kim Guldstrand and Raskin, Jean-Fran\c{c}ois and Reynier, Pierre-Alain},
BOOKTITLE = {Proc. of the 12th International Conference on Hybrid Systems: Computation and Control (HSCC'09)},
CLASS = {internatconference},
MONTH = APR,
CATEGORY = {control},
LEX = {B},
VOLUME = {5469},
RATE = {"45\%"},
ADDRESS = {San Francisco, CA, USA},
NUMIRCYN = {C},
PAGES = {90--104},
PDF = {./ps-pdf-files/hscc-09.pdf},
OSLIDES = {../other-files/slides-hscc-09.pdf},
PUBLISHER = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
SERIES = {\begin{rawhtml}Lecture Notes in Computer Science\end{rawhtml}},
TITLE = {{Automatic Synthesis of Robust and Optimal Controllers -- An
Industrial Case Study}},
YEAR = {2009}
}
@INPROCEEDINGS{cassez-formats-07,
AUTHOR = {Cassez, Franck},
TITLE = {Efficient On-the-Fly Algorithms for Partially
Observable Timed Games},
BOOKTITLE = {Proc. of the 5th Int. Conf. on Formal Modeling and Analysis of Timed Systems (FORMATS'07)},
CLASS = {invited-book},
NOTE = {Invited Paper},
PUBLISHER = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
LEX = {B},
YEAR = {2007},
OPTKEY = {},
VOLUME = {4763},
OPTNUMBER = {},
CATEGORY = {control},
SLIDES = {./ps-pdf-files/formats-07-slides.pdf},
SERIES = {\begin{rawhtml}Lecture Notes in Computer Science\end{rawhtml}},
OPTTYPE = {},
OPTEDITION = {},
XXMONTH = OCT,
PDF = {./ps-pdf-files/formats-07.pdf},
PAGES = {5--24},
ABSTRACT = { In this paper, we review some recent results on the efficient
synthesis of controllers for timed systems. We first recall the basics of
controller synthesis for timed games and then present an efficient
on-the-fly algorithm for reachability games and its extension to partially
observable timed games.
},
OPTANNOTE = {}
}
@INPROCEEDINGS{cassez-atva-07,
ABSTRACT = {In this paper we consider the problem of
controller synthesis for timed games under imperfect
information. Novel to our approach is the
requirements to strategies: they should be based on
a finite collection of observations and must be
stuttering invariant in the sense that repeated
identical observations will not change the
strategy. We provide a constructive transformation
to equivalent finite games with perfect information,
giving decidability as well as allowing for an
efficient on-the-fly forward algorithm. We report on
application of an initial experimental
implementation. },
AUTHOR = {Cassez, Franck and David, Alexandre and Larsen, Kim G. and Lime, Didier and Raskin, Jean-Fran\c{c}ois},
LEX = {B},
BOOKTITLE = {5th Int. Symp. on Automated Technology for Verification and Analysis (ATVA'07)},
CLASS = {internatconference},
CATEGORY = {control},
MONTH = OCT,
PDF = {./ps-pdf-files/atva-07.pdf},
PUBLISHER = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
READ = {No},
PAGES = {307--321},
SERIES = {\begin{rawhtml}Lecture Notes in Computer Science\end{rawhtml}},
TITLE = {Timed Control with Observation Based and Stuttering Invariant
Strategies},
VOLUME = {4762},
PDF = {./ps-pdf-files/atva-07.pdf},
SLIDES = {./ps-pdf-files/slides-atva-07.pdf},
RATE = {"25\%"},
NOTE = {},
YEAR = {2007}
}
@INPROCEEDINGS{CDFLL-concur-05,
ABSTRACT = { In this paper, we propose a first efficient on-the-fly algorithm for
solving games based on timed game automata with respect to
reachability and safety properties.
The algorithm we propose is a symbolic extension of the on-the-fly
algorithm suggested by Liu \& Smolka \cite{LS98} for linear-time
model-checking of finite-state systems. Being on-the-fly, the
symbolic algorithm may terminate long before having explored the
entire state-space. Also the individual steps of the algorithm are
carried out efficiently by the use of so-called zones as the
underlying data structure.
Various optimizations of the basic symbolic algorithm are proposed
as well as methods for obtaining time-optimal winning strategies
(for reachability games). Extensive evaluation of an experimental
implementation of the algorithm yields very encouraging performance
results.},
ADRESS = {San Francisco, CA, USA},
AUTHOR = {Cassez, Franck and David, Alexandre and Fleury, Emmanuel and Larsen, Kim G. and Lime, Didier},
BOOKTITLE = {{P}roc. of the 16th {I}nt. {C}onf. on {C}oncurrency {T}heory ({CONCUR}'05)},
CATEGORY = {control},
CLASS = {internatconference},
MONTH = AUG,
LEX = {B},
PAGES = {66--80},
PDF = {./ps-pdf-files/efficient-control-concur05.pdf},
OSLIDES = {./ps-pdf-files/efficient-control-concur05-slides.pdf},
PUBLISHER = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
SERIES = {\begin{rawhtml}Lecture Notes in Computer Science\end{rawhtml}},
TITLE = {Efficient On-The-Fly Algorithms for the Analysis of Timed Games},
RATE = {"38\%"},
VOLUME = 3653,
YEAR = {2005}
}
@INPROCEEDINGS{bouyer-fsttcs-04,
ABSTRACT = { Priced timed (game) automata extend timed (game) automata with costs
on both locations and transitions. In this paper we focus on
reachability priced timed game automata and prove that the
optimal cost for winning such a game is computable under conditions
concerning the non-zenoness of cost.
Under stronger conditions (strictness of constraints) we prove that in
case an optimal strategy exists, we can compute a state-based winning
optimal strategy.},
AUTHOR = {Bouyer, Patricia and Cassez, Franck and Fleury, Emmanuel and Larsen, Kim G.},
CATEGORY = {control},
BOOKTITLE = {Proc. of the 24th Int. Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'04)},
CLASS = {internatconference},
DATE-MODIFIED = {2006-10-09 06:11:04 +0200},
MONTH = DEC,
LEX = {B},
PAGES = {148--160},
PDF = {./ps-pdf-files/fsttcs04.pdf},
OSLIDES = {http://www.lsv.ens-cachan.fr/~bouyer/files/fsttcs04.pdf},
PUBLISHER = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
SERIES = {\begin{rawhtml}Lecture Notes in Computer Science\end{rawhtml}},
TITLE = {Optimal Strategies in Priced Timed Game Automata},
RATE = {"24\%"},
VOLUME = 3328,
YEAR = 2004
}
@INPROCEEDINGS{bouyer-gdv-04,
ABSTRACT = {Priced timed (game) automata extend timed (game) automata with
costs on both locations and transitions. The problem of synthesizing an optimal
winning strategy for a priced timed game under some hypotheses has been shown
decidable in [6]. In this paper, we present an algorithm for computing the optimal
cost and for synthesizing an optimal strategy in case there exists one. We also
describe the implementation of this algorithm with the tool HyTech and present
an example.},
AUTHOR = {Bouyer, Patricia and Cassez, Franck and Fleury, Emmanuel and Larsen, Kim G.},
CATEGORY = {control},
BOOKTITLE = {Proc. of the {W}orkshop on {G}ames in {D}esign and {V}erification ({GDV'04})},
CLASS = {internatconference},
MONTH = FEB,
NUMBER = {1},
PAGES = {11--31},
PDF = {./ps-pdf-files/gdv04.pdf},
PUBLISHER = {Copyright \begin{rawhtml}Elsevier\end{rawhtml}},
SERIES = {Elec. Notes in Theo. Comp. Science},
TITLE = {Synthesis of Optimal Strategies Using {HyTech}},
SLIDES = {./ps-pdf-files/slides-gdv-04.pdf},
LEX = {B},
VOLUME = {119},
YEAR = {2005}
}
@INPROCEEDINGS{cassez-hscc-02,
ABSTRACT = {In the literature, we find several formulations of the
control problem for
timed and hybrid systems. We argue that formulations where a
controller can cause an action at any point in dense (rational or
real) time are problematic, by presenting an example where the
controller must act faster and faster, yet causes no Zeno effects
(say, the control actions are at times
$0,\frac{1}{2},1,1\frac{1}{4},2,2\frac{1}{8},3,3\frac{1}{16},\ldots$).
Such a controller is, of course, not implementable in software. Such
controllers are avoided by formulations where the controller can cause
actions only at discrete (integer) points in time. While the
resulting control problem is well-understood if the time unit, or
``sampling rate'' of the controller, is fixed a priori, we define a
novel, stronger formulation: the {\em discrete-time control problem
with unknown sampling rate\/} asks if a sampling controller exists for
{\em some\/} sampling rate. We prove that this problem is undecidable
even in the special case of timed automata.},
AUTHOR = {Cassez, Franck and Henzinger, Thomas A. and Raskin, Jean-Fran\c{c}ois},
BOOKTITLE = {Proc. of the Workshop on Hybrid Systems: Computation and Control (HSCC'02)},
CATEGORY = {control},
CLASS = {internatconference},
MONTH = MAR,
LEX = {B},
NUMBER = {2289},
RATE = {"45\%"},
NUMIRCYN = {C},
PAGES = {134--148},
PS = {./ps-pdf-files/hscc-02-control.ps.gz},
PUBLISHER = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
SERIES = {\begin{rawhtml}Lecture Notes in Computer Science\end{rawhtml}},
TITLE = {{ A Comparison of Control Problems for Timed and Hybrid Systems}},
YEAR = {2002}
}
@ARTICLE{Cortos-MSR05-control-journal,
LEX = {Bb},
AUTHOR = {Altisen, Karine and Bouyer, Patricia and Cachat, Thierry and Cassez, Franck and Gardey, Guillaume},
JOURNAL = {\begin{rawhtml}European Journal of Automation\end{rawhtml}},
CLASS = {natjournal},
XXMONTH = OCT,
XXNOTE = {This paper is the same as~\cite{Cortos-MSR05-control}},
PAGES = {367-380},
VOLUME = {39},
NUMBER = {1-2-3},
PDF = {./ps-pdf-files/intro-control-msr05.pdf},
CATEGORY = {control},
PUBLISHER = {Herm{\`e}s},
TITLE = {Introduction au contr{\^o}le des syst{\`e}mes temps-r{\'e}el},
URL = {http://www.lsv.ens-cachan.fr/aci-cortos},
YEAR = {2005}
}
@INBOOK{cassez-control-iste-2009,
AUTHOR = {Cassez, Franck and Markey, Nicolas},
TITLE = {Communicating Embedded Systems -- Software and Design},
EDITOR = {Jard, Claude and Roux, Olivier H.},
MONTH = OCT,
PAGES = {83--120},
PUBLISHER = {\begin{rawhtml}ISTE Publishing Ltd. -- John Wiley & Sons, Ltd.\end{rawhtml}},
CHAPTER = {Control of Timed Systems},
CLASS = {ed-book},
CATEGORY = {control},
LEX = {C},
URL = {http://www.iste.co.uk/index.php?f=a&ACTION=View&id=288},
YEAR = {2009},
PDF = {./ps-pdf-files/iste-wiley-book-control.pdf},
ABSTRACT = {In this book Chapter we address the problem of controller synthesis for timed systems. By
timed systems we refer to systems which are subject to quantitative (hard) real-time
constraints. We assume the reader is familiar with the basics of Timed Automata
theory, or has read Chapter 1 and Chapter 2 in this book. },
NOTE = {ISBN:978-1-8482-1143-8. Draft version may differ from published one.}
}
@INBOOK{cassez-control-afsec-08,
AUTHOR = {Cassez, Franck and Markey, Nicolas},
EDITOR = {Jard, Claude and Roux, Olivier H.},
TITLE = {Syst\`emes embarqu\'es -- Approches formelles},
CHAPTER = {Contr\^ole des syst\`emes temporis\'es},
CATEGORY = {control},
PUBLISHER = {\begin{rawhtml}Hermès Science\end{rawhtml}},
YEAR = {2008},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
LEX = {C},
URL = {http://www.lavoisier.fr/notice/fr335499.html},
SERIES = {Trait\'e IC2},
XXXTYPE = {{I}nvited Chapter.},
EDITION = {},
MONTH = OCT,
CLASS = {ed-book},
PAGES = {105--144},
PDF = {./ps-pdf-files/afsec-book-control.pdf},
NOTE = {In french},
ABSTRACT = {Ce chapitre traite de la synth\`ese de contr\^oleurs
pour les syst\`emes temporis\'es. Par syst\`emes
temporisés nous entendons les syst\`emes dans lesquels
des contraintes de temps quantitatives sont
sp\'ecif\'ees. Les notions de base que nous utilisons
dans ce chapitre s'appuient sur les concepts
introduits dans les chapitre 3 et chapitre 4 ; la
lecture de ces chapitres est donc recommand\'ee au
lecteur qui ne connaitrait pas les fondements des
automates temporis\'es. }
}
@PHDTHESIS{cassez-hdr-07,
CATEGORY = {control},
AUTHOR = {Cassez, Franck},
TITLE = {Control of Timed Systems},
SCHOOL = {Ecole Polytechnique de l'Universit\'e de Nantes, France},
TYPE = {Habilitation à Diriger les Recherches},
YEAR = {2007},
LEX = {D},
MONTH = SEP,
CLASS = {other},
OPTNOTE = {Draft version in French},
FR-PDF = {./ps-pdf-files/hdr-fr-cassez.pdf},
EN-PDF = {./ps-pdf-files/hdr-en-cassez.pdf},
SLIDES = {./ps-pdf-files/slides-hdr-cassez.pdf}
}
@MISC{cassez-etr-07,
AUTHOR = {Cassez, Franck and Markey, Nicolas},
CLASS = {invited-book},
HOWPUBLISHED = {Actes de l'\'ecole d'\'et\'e ETR'07},
XXMONTH = SEP,
NOTE = {Nantes},
LEX = {D},
PDF = {./ps-pdf-files/etr-07.pdf},
TITLE = {{Contr{\^o}le des syst\`emes temporis\'es}},
CATEGORY = {control},
ABSTRACT = {Cet article est une introduction au contrôle des systèmes
modélisés par des automates temporisés. Nous
définissons les notions de base du contrôle vu comme
un jeu: stratégie, objectif de contrôle, états
gagnants. On s'intéresse ensuite aux opérateurs de
base permettant de résoudre les jeux
temporisés. Nous considérons le cas des jeux de
sûreté pour lesquels nous donnons un exemple complet
de calcul de contrôleur. Nous abordons ensuite la
notion importante d'implémentabilité des
contrôleurs. Deux points de vue sont proposés:
l'un syntaxique, qui consiste à décrire la
plate-forme cible pour l'implémentation par des
automates temporisés; l'autre sémantique, qui
considère une sémantique implémentable des automates
temporisés. },
SLIDES = {./ps-pdf-files/slides-etr-07.pdf},
YEAR = {2007}
}
@TECHREPORT{bouyer-brics-04,
ABSTRACT = { Priced timed (game) automata extends timed (game) automata with costs on both locations and transitions. In this paper we focus on
reachability games for priced timed game automata and prove that the
optimal cost for winning such a game is computable under conditions
concerning the
non-zenoness of cost. Under stronger conditions (strictness of
constraints) we prove in addition that it is decidable whether there
is an optimal strategy in which case an optimal strategy can be
computed. Our results extend previous decidability result which
requires the underlying game automata to be acyclic. Finally, our
results are encoded in a first prototype in {\em HyTech} which is applied
on a small case-study.},
AUTHOR = {Bouyer, Patricia and Cassez, Franck and Fleury, Emmanuel and Larsen, Kim Guldstrand},
INSTITUTION = {BRICS, Denmark},
LEX = {Da},
XXMONTH = FEB,
NOTE = {ISSN 0909-0878},
CATEGORY = {control},
NUMBER = {RS-04-0},
TITLE = {{Optimal Strategies in Priced Timed Game Automata}},
TYPE = {BRICS Reports Series},
URL = {http://www.brics.dk/RS/04/4/},
YEAR = {2004}
}
@BOOK{cassez-num-spec-tsi-06,
TITLE = {{Contrôle des applications temps-r\'eel: modèles temporis\'es et hybrides}},
PUBLISHER = {\begin{rawhtml}Hermès Science\end{rawhtml}},
CATEGORY = {control},
YEAR = {2006},
EDITOR = {Cassez, Franck and Laroussinie, Fran\c{c}ois},
OPTKEY = {},
LEX = {D},
VOLUME = {25},
NUMBER = {3},
SERIES = {\begin{rawhtml}Technique et Science Informatiques\end{rawhtml}},
OPTEDITION = {},
OPTXXMONTH = {},
CLASS = {ed-book},
XXNOTE = {Special Issue},
OPTANNOTE = {}
}
franck-hs.bib
@COMMENT{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{Command line: bib2bib -q -c category="hs" -oc franck-hs.cite -ob franck-hs.bib mabib.bib}}
@COMMENT{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{Command line: bib2bib -s $date -s lex bib/mabib.bib}}
@COMMENT{{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{{Command line: bib2bib -s lex -s $date bib/mabib.bib}}
@COMMENT{{{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{{{Command line: bib2bib -s lex -s $date bib/mabib.bib}}
@COMMENT{{{{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{{{{Command line: bib2bib -s lex -s $date bib/mabib.bib}}
@INPROCEEDINGS{cassez-atva-06,
ABSTRACT = {In this paper we give a symbolic concurrent semantics for network of
timed automata (NTA) in terms of extended symbolic nets. Extended symbolic
nets are standard occurrence nets extended with read arcs and symbolic constraints on places and transitions. We prove that there is a complete finite prefix
for any NTA that contains at least the information of the simulation graph of the
NTA but keep explicit the notions of concurrency and causality of the network.
},
AUTHOR = {Cassez, Franck and Chatain, Thomas and Jard, Claude},
BOOKTITLE = {4th Int. Symp. on Automated Technology for Verification and Analysis (ATVA'06)},
CLASS = {internatconference},
DATE-ADDED = {2006-10-09 06:16:38 +0200},
DATE-MODIFIED = {2006-10-09 07:21:12 +0200},
CATEGORY = {hs},
MONTH = OCT,
PDF = {./ps-pdf-files/atva-06.pdf},
SLIDES = {./ps-pdf-files/slides-atva-06.pdf},
LEX = {B},
PUBLISHER = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
READ = {No},
PAGES = {307--321},
SERIES = {\begin{rawhtml}Lecture Notes in Computer Science\end{rawhtml}},
TITLE = {{Symbolic Unfoldings for Networks of Timed Automata}},
VOLUME = {4218},
RATE = {"25\%"},
YEAR = {2006}
}
@INPROCEEDINGS{cassez-concur-00,
ABSTRACT = { In this paper we define and study the class of {\em
stopwatch automata} which are timed automata
augmented with {\em stopwatches} and {\em
unobservable behaviour}. In particular, we
investigate the expressive power of this class of
automata, and show as a main result that any finite
or infinite {\em timed language} accepted by a
\emph{linear hybrid automaton} is also acceptable by
a stopwatch automaton. The consequences of this
result are two-fold: firstly, it shows that the
seemingly minor upgrade from timed automata to
stopwatch automata immediately yields the full
expressive power of linear hybrid
automata. Secondly, reachability analysis of linear
hybrid automata may effectively be reduced to
reachability analysis of stopwatch automata. This,
in turn, may be carried out using an easy
(over-approximating) extension of the efficient
reachability analysis for timed automata to
stopwatch automata. We report on preliminary
experiments on analyzing translations of linear
hybrid automata using a stopwatch-extension of the
real-time verification tool \sf {UPPAAL}. },
AUTHOR = {Cassez, Franck and Larsen, Kim Guldstrand},
BOOKTITLE = {Proc. of the 11th Int. Conf. on Concurrency Theory, (CONCUR'00)},
CLASS = {internatconference},
CATEGORY = {hs},
MONTH = JUL,
LEX = {B},
VOLUME = {1877},
NUMIRCYN = {C},
PAGES = {138--152},
PS = {./ps-pdf-files/concur2k.ps},
RATE = {"36\%"},
PUBLISHER = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
SERIES = {\begin{rawhtml}Lecture Notes in Computer Science\end{rawhtml}},
TITLE = {{The Impressive Power of Stopwatches}},
YEAR = {2000}
}
@INPROCEEDINGS{Cortos-MSR05-control,
AUTHOR = {Altisen, Karine and Bouyer, Patricia and Cachat, Thierry and Cassez, Franck and Gardey, Guillaume},
LEX = {Bbb},
BOOKTITLE = {{A}ctes du 5{\`e}me {C}olloque sur la {M}od{\'e}lisation des {S}yst{\`e}mes {R}{\'e}actifs ({MSR}'05)},
CLASS = {invited-book},
XXMONTH = OCT,
CATEGORY = {hs},
NOTE = {Invited Paper. Also appeared as~\cite{Cortos-MSR05-control-journal}},
PAGES = {367-380},
PDF = {./ps-pdf-files/intro-control-msr05.pdf},
SLIDES = {./ps-pdf-files/slides-msr05.pdf},
PUBLISHER = {\begin{rawhtml}Hermès Science\end{rawhtml}},
TITLE = {Introduction au contr{\^o}le des syst{\`e}mes temps-r{\'e}el},
URL = {http://www.lsv.ens-cachan.fr/aci-cortos},
YEAR = {2005}
}
@TECHREPORT{cassez-rr-unfolding-06,
ABSTRACT = {
In this paper we give a symbolic concurrent semantics for network of
timed automata (NTA) in terms of \emph{extended symbolic
nets}. Symbolic nets are standard occurrence nets extended with
\emph{read arcs} and \emph{symbolic constraints} on places and
transitions.
We prove that there is a \emph{complete finite prefix} for any NTA
that contains at least the information of the simulation graph of
the NTA but keep explicit the notions of concurrency and causality
of the network.
},
LEX = {Da},
CATEGORY = {hs},
AUTHOR = {Cassez, Franck and Chatain, Thomas and Jard, Claude},
INSTITUTION = {IRCCyN/CNRS, Nantes},
XXMONTH = MAY,
NUMBER = {RI-2006-4},
NUMIRCCYN = {I},
PDF = {./ps-pdf-files/unfolding-rr-06.pdf},
TITLE = {{Symbolic Unfoldings for Networks of Timed Automata}},
YEAR = {2006}
}
franck-logics.bib
@COMMENT{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{Command line: bib2bib -q -c category="logics" -oc franck-logics.cite -ob franck-logics.bib mabib.bib}}
@COMMENT{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{Command line: bib2bib -s $date -s lex bib/mabib.bib}}
@COMMENT{{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{{Command line: bib2bib -s lex -s $date bib/mabib.bib}}
@COMMENT{{{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{{{Command line: bib2bib -s lex -s $date bib/mabib.bib}}
@COMMENT{{{{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{{{{Command line: bib2bib -s lex -s $date bib/mabib.bib}}
@ARTICLE{bouyer-jlli-2010,
AUTHOR = {Bouyer, Patricia and Cassez, Franck and Laroussinie, Fran\c{c}ois},
TITLE = {{Timed Modal Logics for Real-Time Systems -- Specification, Verification and Control}},
JOURNAL = {\begin{rawhtml}Journal of Logic, Language and Computation\end{rawhtml}},
YEAR = {2010},
LEX = {A},
CATEGORY = {logics},
CLASS = {internatjournal},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
OPTMONTH = {},
NOTE = {Forthcoming},
PDF = {./ps-pdf-files/jlli-2010.pdf},
OPTANNOTE = {},
PUBLISHER = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
ABSTRACT = {
In this paper, a timed modal logic Lc is presented for the specification
and verification of real-time systems. Several important results for Lc 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 Lc model checking. Finally
we consider several control problems for which Lc can be used to check controllability.
}
}
@INPROCEEDINGS{BCL-concur2005,
ABSTRACT = {In this paper we use the timed modal logic $L_\nu$ to specify control
objectives for timed plants. We show that the control problem for a
large class of objectives can be reduced to a model-checking problem for
an extension ($L^c$) of the logic Lnu with a new modality.
More precisely we define a fragment of $L_\nu$, namely $L_\nu^d$, such that any
control objective of $L_\nu^d$ can be translated into a $L^c$ formula that
holds for the plant if and only if there is a controller that can
enforce the control objective.
We also show that the new modality of $L^c$ strictly increases the
expressive power of $L_\nu$ while model-checking of Lc remains
EXPTIME-complete.},
ADRESS = {San Francisco, CA, USA},
AUTHOR = {Bouyer, Patricia and Cassez, Franck and Laroussinie, Fran\c{c}ois},
BOOKTITLE = {{P}roc. of the 16th {I}nt. {C}onf. on {C}oncurrency {T}heory ({CONCUR}'05)},
CATEGORY = {logics},
CLASS = {internatconference},
MONTH = AUG,
LEX = {B},
PAGES = {81--94},
PDF = {./ps-pdf-files/modal-control-concur05.pdf},
SLIDES = {./ps-pdf-files/slides-concur-05.pdf},
PUBLISHER = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
RATE = {"38\%"},
SERIES = {\begin{rawhtml}Lecture Notes in Computer Science\end{rawhtml}},
TITLE = {Modal Logics for Timed Control},
VOLUME = 3653,
YEAR = {2005}
}
@TECHREPORT{bouyer-modal-control-05,
ABSTRACT = {In this paper we use the timed modal logic $L_\nu$ to specify control
objectives for timed plants. We show that the control problem for a
large class of objectives can be reduced to a model-checking problem for
an extension ($L^c$) of the logic Lnu with a new modality.
More precisely we define a fragment of $L_\nu$, namely $L_\nu^d$, such that any
control objective of $L_\nu^d$ can be translated into a $L^c$ formula that
holds for the plant if and only if there is a controller that can
enforce the control objective.
We also show that the new modality of $L^c$ strictly increases the
expressive power of $L_\nu$ while model-checking of Lc remains
EXPTIME-complete.},
AUTHOR = {Bouyer, Patricia and Cassez, Franck and Laroussinie, Fran\c{c}ois},
INSTITUTION = {IRCCyN/CNRS, Nantes},
CATEGORY = {logics},
LEX = {Da},
MONTH = MAR,
NUMBER = {RI-2005-2},
PDF = {./ps-pdf-files/modal-control-rr.pdf},
TITLE = {{Modal Logics for Timed Control}},
URL = {http://www.lsv.ens-cachan.fr/~fl/cmcweb.html},
YEAR = {2005}
}
@INPROCEEDINGS{cassez-cav-00,
ABSTRACT = { In this paper we present a semi-algorithm to do
compositional model-checking for hybrid systems. We
first define a modal logic $L_\nu$ which is
expressively complete for linear hybrid automata. We
then show that it is possible to extend the result
on compositional model-checking for parallel
compositions of finite automata and networks of
timed automata to linear hybrid automata. Finally we
present some results obtained with an extension of
the tool {\sf CMC} to handle a subclass of hybrid
automata (the stopwatch automata). },
AUTHOR = {Cassez, Franck and Laroussinie, Fran\c{c}ois},
BOOKTITLE = {Proc. of the Int. Conf. on Computer Aided Verification, (CAV'00)},
CLASS = {internatconference},
CATEGORY = {logics},
MONTH = JUN,
LEX = {B},
NUMIRCYN = {C},
PAGES = {373--388},
PS = {./ps-pdf-files/cav-00.ps},
PUBLISHER = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
SERIES = {\begin{rawhtml}Lecture Notes in Computer Science\end{rawhtml}},
TITLE = {{Model-Checking of Hybrid Automata by Quotienting and Constraints Solving}},
RATE = {"38\%"},
VOLUME = {1855},
YEAR = {2000}
}
@MISC{cassez-etr-03,
AUTHOR = {Cassez, Franck},
CLASS = {invited-book},
HOWPUBLISHED = {Actes de l'\'ecole d'\'et\'e ETR'03},
XXMONTH = SEP,
NOTE = {Toulouse},
LEX = {D},
PDF = {./ps-pdf-files/verif-qualit-etr-03.pdf},
SLIDES = {./ps-pdf-files/slides-etr-03.pdf},
CATEGORY = {logics},
TITLE = {{V\'erification qualitative -- {Model-Checking} et Logiques Temporelles}},
YEAR = {2003}
}
franck-faultdiag.bib
@COMMENT{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{Command line: bib2bib -q -c category="faultdiag" -oc franck-faultdiag.cite -ob franck-faultdiag.bib mabib.bib}}
@COMMENT{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{Command line: bib2bib -s $date -s lex bib/mabib.bib}}
@COMMENT{{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{{Command line: bib2bib -s lex -s $date bib/mabib.bib}}
@COMMENT{{{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{{{Command line: bib2bib -s lex -s $date bib/mabib.bib}}
@COMMENT{{{{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{{{{Command line: bib2bib -s lex -s $date bib/mabib.bib}}
@TECHREPORT{cassez-dyn-diag-ts-2010,
AUTHOR = {Franck Cassez},
CATEGORY = {faultdiag},
LEX = {Da},
TITLE = {{Dynamic Observers for Fault Diagnosis of Timed Systems}},
INSTITUTION = {National ICT Australia},
YEAR = 2010,
TYPE = {Research Report},
MONTH = MAR,
PDF = {http://arxiv.org/pdf/1006.4681v1},
NOTE = {8 pages, arXiv:1006.4681 [cs.FL]},
ARXIV = {http://arxiv.org/abs/1006.4681},
ABSTRACT = { In this paper we extend the work on dynamic observers for
fault diagnosis to timed automata. We
study sensor minimization problems with static observers and
then address the problem of computing the most permissive
dynamic observer for a system given by a timed automaton.
}
}
@INPROCEEDINGS{cassez-atva-10,
ABSTRACT = {In this paper we study the fault codiagnosis problem for discrete
event systems given by finite automata (FA) and timed systems
gi\-ven by timed automata (TA). We provide a uniform
characterization of codiagnosability for FA and TA which extends the
necessary and sufficient condition that characterizes
diagnosability. We also settle the complexity of the
codiagnosability problems both for FA and TA and show that
codiagnosability is PSPACE-complete in both cases. For FA this
improves on the previously known bound (EXPTIME) and for TA it is a
new result. Finally we address the codiagnosis problem for TA under
bounded resources and show it is 2EXPTIME-complete.},
AUTHOR = {Cassez, Franck},
BOOKTITLE = {8th Int. Symp. on Automated Technology for Verification and Analysis (ATVA'10)},
CLASS = {internatconference},
CATEGORY = {faultdiag},
LEX = {B},
MONTH = SEP,
NOTE = {Extended~version in~\cite{cassez-codiag-2010}},
OPTVOLUME = 5799,
SERIES = {\begin{rawhtml}Lecture Notes in Computer Science\end{rawhtml}},
RATE = {"41\%"},
NUMIRCYN = {C},
ADDRESS = {Singapore},
OPTPAGES = {352--367},
PUBLISHER = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
OPTSLIDES = {./ps-pdf-files/slides-atva-09.pdf},
PDF = {./ps-pdf-files/atva-10.pdf},
TITLE = {{The Complexity of Codiagnosability for Discrete Event and Timed Systems}},
YEAR = {2010}
}
@TECHREPORT{cassez-codiag-2010,
AUTHOR = {Franck Cassez},
CATEGORY = {faultdiag},
LEX = {Da},
TITLE = {The Complexity of Codiagnosability for Discrete Event and Timed Systems},
INSTITUTION = {National ICT Australia},
YEAR = 2010,
TYPE = {Research Report},
MONTH = APR,
PDF = {http://arxiv.org/pdf/1004.2550v1},
PS = {http://arxiv.org/ps/1004.2550v1},
NOTE = {24 pages, arXiv:1004.2550v1 [cs.FL]},
ARXIV = {http://arxiv.org/abs/1004.2550},
ABSTRACT = {In this paper we study the fault codiagnosis problem for discrete
event systems given by finite automata (FA) and timed systems
gi\-ven by timed automata (TA). We provide a uniform
characterization of codiagnosability for FA and TA which extends the
necessary and sufficient condition that characterizes
diagnosability. We also settle the complexity of the
codiagnosability problems both for FA and TA and show that
codiagnosability is PSPACE-complete in both cases. For FA this
improves on the previously known bound (EXPTIME) and for TA it is a
new result. Finally we address the codiagnosis problem for TA under
bounded resources and show it is 2EXPTIME-complete.}
}
@ARTICLE{cassez-fi-08,
AUTHOR = {Cassez, Franck and Tripakis, Stavros},
TITLE = {Fault Diagnosis with Static and Dynamic Diagnosers},
JOURNAL = {\begin{rawhtml}Fundamenta Informaticae\end{rawhtml}},
YEAR = {2008},
OPTKEY = {},
VOLUME = {88},
NUMBER = {4},
LEX = {A},
PAGES = {497--540},
CATEGORY = {faultdiag},
MONTH = NOV,
ABSTRACT = {We study sensor minimization problems in the context of
fault diagnosis. Fault diagnosis consists in
synthesizing a diagnoser that observes a given plant
and identifies faults in the plant as soon as
possible after their occurrence. Existing literature
on this problem has considered the case of fixed
static observers, where the set of observable events
is fixed and does not change during execution of the
system. In this paper, we consider static observers
where the set of observable events is not fixed, but
needs to be optimized (e.g., minimized in size). We
also consider dynamic observers, where the observer
can ``switch'' sensors on or off, thus dynamically
changing the set of events it wishes to observe. It
is known that checking diagnosability (i.e., whether
a given observer is capable of identifying faults)
can be solved in polynomial time for static
observers, and we show that the same is true for
dynamic ones. On the other hand, minimizing the
number of (static) observable events required to
achieve diagnosability is NP-complete. We show that
this is true also in the case of mask-based
observation, where some events are observable but
not distinguishable. For dynamic observers'
synthesis, we prove that a most permissive
finite-state observer can be computed in doubly
exponential time, using a game-theoretic
approach. We further investigate optimization
problems for dynamic observers and define a notion of
cost of an observer. We show how to compute an
optimal observer using results on mean-payoff games
by Zwick and Paterson. },
CLASS = {internatjournal},
NOTE = {},
PDF = {./ps-pdf-files/diag-fi-08.pdf},
OPTANNOTE = {}
}
@INPROCEEDINGS{cassez-cdc-09,
AUTHOR = {Cassez, Franck},
TITLE = {{A Note on Fault Diagnosis Algorithms}},
OPTCROSSREF = {},
OPTKEY = {},
BOOKTITLE = {48th IEEE Conference on Decision and Control and 28th Chinese Control Conference},
OPTPAGES = {},
YEAR = {2009},
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
ARXIV = {http://arxiv.org/abs/1004.2764},
ADDRESS = {Shanghai, P.R. China},
MONTH = DEC,
OPTORGANIZATION = {},
PUBLISHER = {IEEE Computer Society},
NOTE = {Extended Version. Forthcoming},
CATEGORY = {faultdiag},
CLASS = {internatconference},
PDF = {http://arxiv.org/pdf/1004.2764v1},
OPTANNOTE = {},
SLIDES = {./ps-pdf-files/slides-cdc-09.pdf},
ABSTRACT = { In this paper we review algorithms for checking diagnosability of
discrete-event systems and timed automata. We point out that the
diagnosability problems in both cases reduce to the emptiness
problem for (timed) B\"uchi automata. Moreover, it is known that,
checking whether a discrete-event system is diagnosable, can also be
reduced to checking bounded diagnosability. We establish a similar
result for timed automata. We also provide a synthesis of the
complexity results for the different fault diagnosis problems.}
}
@INPROCEEDINGS{cassez-wodes-08,
CLASS = {invited-book},
AUTHOR = {Cassez, Franck and Tripakis, Stavros},
TITLE = {Fault Diagnosis with Dynamic Diagnosers},
OPTCROSSREF = {},
OPTKEY = {},
BOOKTITLE = {Proc. of the $9^{th}$ Workshop on Discrete Event Systems (WODES'08)},
PAGES = {212--217},
YEAR = {2008},
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {Proc. of the $9^{th}$ Workshop on Discrete Event Systems (WODES'08)},
OPTADDRESS = {},
ARXIV = {http://arxiv.org/abs/1004.2810},
LEX = {B},
MONTH = MAY,
OPTORGANIZATION = {},
CATEGORY = {faultdiag},
PUBLISHER = {IEEE Computer Society},
NOTE = {},
PDF = {http://arxiv.org/pdf/1004.2810v1},
SLIDES = {./ps-pdf-files/slides-wodes-08.pdf},
OPTANNOTE = {},
ABSTRACT = { In this paper, we review some recent results about the use
of dynamic observers for fault diagnosis of discrete
event systems. Dynamic observers can switch sensors
on or off, thus dynamically changing the set of
events they wish to observe. We study the dynamic
diagnoser synthesis problem and some related
optimization problems. }
}
@INPROCEEDINGS{cassez-acsd-07,
AUTHOR = {Cassez, Franck and Tripakis, Stavros and Altisen, Karine},
TITLE = {Sensor Minimization Problems with Static or Dynamic Observers for Fault Diagnosis},
OPTCROSSREF = {},
OPTKEY = {},
CLASS = {internatconference},
BOOKTITLE = {7th Int. Conf. on Application of Concurrency to System Design (ACSD'07)},
PAGES = {90--99},
YEAR = {2007},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
LEX = {B},
CATEGORY = {faultdiag},
MONTH = JUL,
OPTORGANIZATION = {},
PDF = {./ps-pdf-files/acsd-07.pdf},
SLIDES = {./ps-pdf-files/slides-acsd-07.pdf},
PUBLISHER = {IEEE Computer Society},
OPTANNOTE = {},
ABSTRACT = {We study sensor minimization problems in the context of
fault diagnosis. Fault diagnosis consists of synthesizing a
diagnoser that observes a given plant and identifies faults
in the plant as soon as possible after their occurrence.
Existing literature on this problem has considered the case of
static observers, where the set of observable events does
not change during execution of the system. In this paper, we
consider static as well as dynamic observers, where the
observer can switch sensors on or off, thus dynamically
changing the set of events it wishes to observe.
}
}
@INPROCEEDINGS{cassez-tase-07,
AUTHOR = {Cassez, Franck and Tripakis, Stavros and Altisen, Karine},
TITLE = {Synthesis Of Optimal Dynamic Observers for Fault Diagnosis of Discrete-Event Systems},
OPTCROSSREF = {},
OPTKEY = {},
CLASS = {internatconference},
BOOKTITLE = {1st IEEE \& IFIP Int. Symp. on Theoretical Aspects of Soft. Engineering (TASE'07)},
PAGES = {316--325},
YEAR = {2007},
CATEGORY = {faultdiag},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
MONTH = JUN,
OPTORGANIZATION = {},
PDF = {./ps-pdf-files/tase-07.pdf},
LEX = {B},
SLIDES = {./ps-pdf-files/slides-tase-07.pdf},
AVIVIDEO = {../other-files/tase-07.avi},
RATE = {21\%},
PUBLISHER = {IEEE Computer Society},
OPTANNOTE = {},
ABSTRACT = {Fault diagnosis consists in synthesizing a diagnoser that
observes a given plant through a set of observable events,
and identifies faults which are not observable as soon as
possible after their occurrence. Existing literature on this
problem has considered the case of static observers, where
the set of observable events does not change during exe-
cution of the system. In this paper, we consider dynamic
observers, where the observer can switch sensors on or off,
thus dynamically changing the set of events it wishes to
observe. We define a notion of cost for such dynamic observers
and show that (i) the cost of a given dynamic observer can
be computed and (ii) an optimal dynamic observer can be
synthesized.
}
}
@INPROCEEDINGS{altisen-acsd-06,
ABSTRACT = {We study the monitoring and fault-diagnosis problems
for dense-time real-time systems, where observers (monitors and diagnosers) have access to digital rather than analog clocks. Analog clocks are infinitely-precise, thus, not
implementable. We show how, given a specification modeled as a timed automaton and a timed automaton model
of the digital clock, a sound and optimal (i.e., as precise
as possible) digital-clock monitor can be synthesized. We
also show how, given plant and digital clock modeled as
timed automata, we can check existence of a digital-clock
diagnoser and, if one exists, how to synthesize it. Finally,
we consider the problem of existence of digital-clock diag-
nosers where the digital clock is unknown. We show that
there are cases where a digital clock, no matter how precise, does not exist, even though the system is diagnosable
with analog clocks. Finally, we provide a sufficient condition for digital-clock diagnosability.
check whether the observed behavior satisfies the specification. This is the objective of the observer, which in this
case is called a monitor. Our goal is to synthesize a monitor
automatically from the specification.
In the fault-diagnosis problem, we have a model of the
system, for instance, in the form of an (untimed or timed)
automaton. We also know that the system may produce
some faults. However, these faults are not directly observable, thus, their occurrence must be deduced from other
observations (this can be seen as a grey-box setting). The
objective of the observer, which in this case is called a diagnoser, is to detect whether a fault occurred or not, and
this as soon as possible after the fault happened. In this
case, before we attempt to synthesize a diagnoser, we must
first check existence of a diagnoser, called diagnosability.
Indeed, a diagnoser may not exist in cases where the system
},
AUTHOR = {Altisen, Karine and Cassez, Franck and Tripakis, Stavros},
BOOKTITLE = {6th Int. Conf. on Application of Concurrency to System Design (ACSD'06)},
CLASS = {internatconference},
DATE-MODIFIED = {2006-10-09 07:07:40 +0200},
CATEGORY = {faultdiag},
MONTH = JUN,
OPTNOTE = {Forthcoming},
PDF = {./ps-pdf-files/acsd-06.pdf},
SLIDES = {./ps-pdf-files/slides-acsd-06.pdf},
PUBLISHER = {IEEE Computer Society},
RATE = {"51\%"},
LEX = {B},
TITLE = {Monitoring and Fault-Diagnosis with Digital Clocks},
YEAR = {2006}
}
@INBOOK{cassez-diag-iste-2009,
AUTHOR = {Cassez, Franck and Tripakis, Stavros},
TITLE = {Communicating Embedded Systems -- Software and Design},
EDITOR = {Jard, Claude and Roux, Olivier H.},
MONTH = OCT,
PAGES = {120--151},
PUBLISHER = {\begin{rawhtml}ISTE Publishing Ltd. -- John Wiley & Sons, Ltd.\end{rawhtml}},
CHAPTER = {Fault Diagnosis of Timed Systems},
CATEGORY = {faultdiag},
CLASS = {ed-book},
LEX = {C},
URL = {http://www.iste.co.uk/index.php?f=a&ACTION=View&id=288},
YEAR = {2009},
PDF = {./ps-pdf-files/iste-wiley-book-diag.pdf},
ABSTRACT = {In this book Chapter, we review the main results pertaining
to the problem of fault diagnosis of timed
automata. Timed automata are introduced in Chapter 1
and Chapter 2 in this book, and the reader not
familiar with this model is invited to read them
first.},
NOTE = {ISBN:978-1-8482-1143-8. Draft version may differ from published one.}
}
@INBOOK{cassez-diag-afsec-08,
AUTHOR = {Cassez, Franck and Tripakis, Stavros},
EDITOR = {Jard, Claude and Roux, Olivier H.},
TITLE = {Syst\`emes embarqu\'es -- Approches formelles},
CHAPTER = {Diagnostic des syst\`emes temporis\'es},
PUBLISHER = {\begin{rawhtml}Hermès Science\end{rawhtml}},
YEAR = {2008},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
SERIES = {Trait\'e IC2},
XXXTYPE = {{I}nvited Chapter.},
EDITION = {},
URL = {http://www.lavoisier.fr/notice/fr335499.html},
MONTH = OCT,
LEX = {C},
CLASS = {ed-book},
PAGES = {145--176},
CATEGORY = {faultdiag},
PDF = {./ps-pdf-files/afsec-book-diag.pdf},
NOTE = {In french},
ABSTRACT = {Dans ce chapitre nous donnons les principaux
r\'esultats concernant le diagnostic de fautes dans
les systèmes temporis\'es. Le mod\`ele de syst\`emes
temporis\'es que nous prenons est celui des automates
temporis\'es introduits dans les chapitre 3 et
chapitre 4. Nous invitons le lecteur qui n'est pas
familier avec ce mod\`ele \`a consulter ces chapitres
pr\'ealablement \`a la lecture de celui-ci. }
}
@TECHREPORT{sensor-rr-07,
ABSTRACT = {
We study sensor minimization problems in the context of fault
diagnosis. Fault diagnosis consists in synthesizing a diagnoser
that observes a given plant and identifies faults in the plant as
soon as possible after their occurrence. Existing literature on this
problem has considered the case of static observers, where the set
of observable events does not change during execution of the system.
In this paper, we consider static as well as {dynamic} observers,
where the observer can ``switch'' sensors on or off, thus
dynamically changing the set of events it wishes to observe. It is
known that checking diagnosability (whether an observer capable of
identifying faults exists) can be solved in polynomial time for
static observers, and we show that the same is true for dynamic
ones. On the other hand, minimizing the number of (static)
observable events required to achieve diagnosability is
NP-complete. We show that this is true also in the case of
mask-based observation, where some events are observable but not
distinguishable. For dynamic observers, we prove that a most
permissive observer can be computed in doubly exponential time,
using a game-theoretic approach. We further investigate
optimization problems for dynamic observers and define a notion of
cost of an observer. Finally we show how to compute an optimal
observer.
},
AUTHOR = {Cassez, Franck and Tripakis, Stavros and Altisen, Karine},
INSTITUTION = {IRCCyN/CNRS, Nantes},
CATEGORY = {faultdiag},
LEX = {Da},
MONTH = JAN,
NUMBER = {RI-2007-1},
NUMIRCCYN = {I},
PDF = {./ps-pdf-files/rr-2007-01.pdf},
TITLE = {{Sensor Minimization Problems with Static or Dynamic Observers
for Fault Diagnosis}},
YEAR = {2007}
}
franck-security.bib
@COMMENT{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{Command line: bib2bib -q -c category="security" -oc franck-security.cite -ob franck-security.bib mabib.bib}}
@COMMENT{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{Command line: bib2bib -s $date -s lex bib/mabib.bib}}
@COMMENT{{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{{Command line: bib2bib -s lex -s $date bib/mabib.bib}}
@COMMENT{{{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{{{Command line: bib2bib -s lex -s $date bib/mabib.bib}}
@COMMENT{{{{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{{{{Command line: bib2bib -s lex -s $date bib/mabib.bib}}
@INPROCEEDINGS{cassez-fossacs-2010,
ABSTRACT = { The paper considers the complexity of verifying that a finite state system
satisfies a number of definitions of information flow security.
The systems model considered is one in which agents operate
synchronously with awareness of the global clock. This enables timing
based attacks to be captured, whereas previous work on this topic
has dealt primarily with asynchronous systems.
Versions of the notions of
nondeducibility on inputs, nondeducibility on strategies, and
an unwinding based notion are formulated for this model.
All three notions are shown to be decidable, and their computational
complexity is characterised.},
AUTHOR = {Cassez, Franck and {van der Meyden}, Ron and Zhang, Chenyi},
BOOKTITLE = {13th International Conference on Foundations of Software Science and Computation Structures},
CLASS = {internatconference},
CATEGORY = {security},
LEX = {B},
MONTH = MAR,
NOTE = {},
VOLUME = 6014,
SERIES = {\begin{rawhtml}Lecture Notes in Computer Science\end{rawhtml}},
RATE = {"??\%"},
NUMIRCYN = {C},
ADDRESS = {Paphos, Cyprus},
PAGES = {282--296},
PUBLISHER = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
XXSLIDES = {},
YEAR = {2010},
PDF = {./ps-pdf-files/fossacs-2010.pdf},
TITLE = {{The Complexity of Synchronous Notions of Information Flow Security}}
}
@INPROCEEDINGS{benattar-formats-09,
ABSTRACT = { In this paper, we focus on the synthesis of secure timed systems
which are given by timed automata.
The security property that the system must satisfy is a
\emph{non-interference} property.
Various notions of non-interference have been defined in the
literature, and in this paper we focus on \emph{Strong
Non-deterministic Non-Interference} (SNNI)
and we study the two following problems: ($1$) check whether it is
possible to enforce a system to be SNNI; if yes ($2$) compute a
sub-system which is SNNI.},
AUTHOR = {Benattar, Gilles and Cassez, Franck and Lime, Didier and Roux, Olivier H.},
BOOKTITLE = {Proc. of the 7th Int. Conf. on Formal Modeling and Analysis of Timed Systems (FORMATS'09)},
CLASS = {internatconference},
CATEGORY = {security},
LEX = {B},
MONTH = SEP,
NOTE = {},
PAGES = {28-42},
EE = {http://dx.doi.org/10.1007/978-3-642-04368-0_5},
VOLUME = {5813},
SERIES = {\begin{rawhtml}Lecture Notes in Computer Science\end{rawhtml}},
RATE = {"41\%"},
NUMIRCYN = {C},
ADDRESS = {Budapest, Hungary},
PUBLISHER = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
OSLIDES = {./ps-pdf-files/slides-formats-09.pdf},
PDF = {./ps-pdf-files/formats-09.pdf},
TITLE = {{Synthesis of Non-Interferent Timed Systems}},
YEAR = {2009}
}
@INPROCEEDINGS{cassez-atva-09,
ABSTRACT = { In this paper, we address the problem of synthesizing \emph{opaque}
systems by selecting the set of observable
events.
We first investigate the case of \emph{static} observability
where the set of observable events
is fixed a priori. In this context, we show that checking whether a
system is opaque and computing an optimal static observer ensuring
opacity are both PSPACE-complete problems.
Next, we introduce \emph{dynamic} partial observability where the
set of observable events
can
change over time.
We show how to check that a system is opaque \wrt a dynamic observer
and also address the corresponding synthesis problem: given a system
$G$ and secret states $S$, compute the set of dynamic observers
under which $S$ is opaque. Our main result is that the synthesis
problem can be solved in EXPTIME.},
AUTHOR = {Cassez, Franck and Dubreil, J\'er\'emy and Marchand, Herv\'e},
BOOKTITLE = {7th Int. Symp. on Automated Technology for Verification and Analysis (ATVA'09)},
CLASS = {internatconference},
CATEGORY = {security},
LEX = {B},
MONTH = OCT,
NOTE = {Extended~version in~\cite{cassez-rr-09}},
VOLUME = 5799,
SERIES = {\begin{rawhtml}Lecture Notes in Computer Science\end{rawhtml}},
RATE = {"41\%"},
NUMIRCYN = {C},
ADDRESS = {Macau SAR, China},
PAGES = {352--367},
PUBLISHER = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
SLIDES = {./ps-pdf-files/slides-atva-09.pdf},
PDF = {./ps-pdf-files/atva-09.pdf},
TITLE = {{Dynamic Observers for the Synthesis of Opaque Systems}},
YEAR = {2009}
}
@INPROCEEDINGS{cassez-isa-09,
ABSTRACT = { In this paper we extend the notion of opacity, defined for
discrete-event systems, to dense-time systems. We define the timed
opacity problem for timed automata and study its algorithmic status.
We show that for the very restrictive class of Event Recording Timed
Automata, the opacity problem is already undecidable leaving no hope
for an algorithmic solution to the opacity problem in dense-time.},
AUTHOR = {Cassez, Franck},
BOOKTITLE = {Proc. of the 3rd International Conference on Information Security and Assurance (ISA'09)},
CLASS = {internatconference},
CATEGORY = {security},
LEX = {B},
MONTH = JUN,
NOTE = {},
VOLUME = 5576,
SERIES = {\begin{rawhtml}Lecture Notes in Computer Science\end{rawhtml}},
RATE = {"30\%"},
NUMIRCYN = {C},
ADDRESS = {Seoul, Korea},
PAGES = {21--30},
PUBLISHER = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
SLIDES = {./ps-pdf-files/slides-isa-09.pdf},
PDF = {./ps-pdf-files/isa-09.pdf},
TITLE = {{The Dark Side of Timed Opacity}},
YEAR = {2009}
}
@INPROCEEDINGS{cassez-mmm-07,
ABSTRACT = {In this paper, we focus on distributed systems sub
ject to security issues. Such systems are usually
composed of two entities: a high level user and a
low level user that can both do some actions. The
security properties we consider are non-interference
properties. A system is non-interferent if the low
level user cannot deduce any information by playing
its low level actions. Various notions of
non-interference have been defined in the
literature, and in this paper we focus on two of
them: one trace-based property (SNNI) and another
bisimulation-based property (BSNNI). For these
properties we study the problems of synthesis of a
high level user so that the system is
non-interferent. We prove that a most permissive
high level user can be computed when one exists. },
AUTHOR = {Cassez, Franck and Mullins, John and Roux, Olivier H.},
BOOKTITLE = {4th Int. Conf. on Mathematical Methods, Models and Architectures for Computer Network Security (MMM-ACNS'07)},
CLASS = {internatconference},
CATEGORY = {security},
MONTH = SEP,
PDF = {./ps-pdf-files/mmm-07.pdf},
PUBLISHER = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
LEX = {B},
READ = {No},
PAGES = {159--170},
SLIDES = {./ps-pdf-files/mmm-07-slides.pdf},
SERIES = {\begin{rawhtml}Lecture Notes in Computer Science\end{rawhtml} Series: Communications in Computer and Inform. Science},
TITLE = {Synthesis of Non-Interferent Distributed Systems},
VOLUME = 1,
RATE = {"25\%"},
XXNOTE = {},
ABSTRACT = {In this paper, we focus on distributed systems sub ject to
security issues. Such systems are usually composed of two entities: a
high level user and a low level user that can both do some actions. The
security properties we consider are non-interference properties. A system
is non-interferent if the low level user cannot deduce any information by
playing its low level actions. Various notions of non-interference have
been defined in the literature, and in this paper we focus on two of
them: one trace-based property (SNNI) and another bisimulation-based
property (BSNNI).
For these properties we study the problems of synthesis of a high level
user so that the system is non-interferent. We prove that a most permissive high level user can be computed when one exists.
},
YEAR = {2007}
}
@TECHREPORT{benattar-rr-08,
AUTHOR = {Benattar, Gilles and Cassez, Franck and Lime, Didier
and Roux, Olivier H.},
TITLE = {Controller Synthesis for Non-Interference
Properties},
INSTITUTION = {IRCCyN},
YEAR = {2008},
CATEGORY = {security},
OPTKEY = {},
OPTTYPE = {},
NUMBER = {RI-2008-01},
ADDRESS = {1 rue de la No\"e, BP 92101, 44321 Nantes
Cedex, France},
LEX = {Da},
MONTH = APR,
PDF = {./ps-pdf-files/snni-tech-rr-08.pdf},
OPTNOTE = {},
OPTANNOTE = {},
ABSTRACT = {
In this paper, we focus on the synthesis of secure systems. We
assume the system is composed of two users, the low level and the
high level users. The security property the system must satisfy is a
\emph{non-interference} property.
A system is \emph{non-interferent} if the low level user cannot
deduce any information about the system by playing its low level
actions. Various notions of non-interference have been defined in
the literature, and in this paper we consider the most popular ones:
trace-based non-interference (SNNI) and (bi)simulation-based
non-interference (CSNNI and BSNNI).
For each of these notions, we study the corresponding synthesis
problem, \ie build a controller \st the controlled system is
non-interferent.}
}
@TECHREPORT{cassez-rr-09,
AUTHOR = {Cassez, Franck and Dubreil, J\'er\'emy and Marchand, Herv\'e},
TITLE = {{Dynamic Observers for the Synthesis of Opaque
Systems}},
INSTITUTION = {IRISA},
YEAR = {2009},
CATEGORY = {security},
OPTKEY = {},
OPTTYPE = {},
NUMBER = {1930},
ADDRESS = {Campus de Beaulieu -- 35042 Rennes Cedex -- France},
LEX = {Da},
MONTH = MAY,
PDF = {./ps-pdf-files/dynamic-opacity-rr-09.pdf},
NOTE = {22 pages},
OPTANNOTE = {},
ABSTRACT = {In this paper, we address the problem of synthesizing \emph{opaque}
systems. A secret predicate $S$ over the runs of a system $G$ is
\emph{opaque} to an external user having partial observability over
$G$, if s/he can never infer from the observation of a run of $G$
that the run belongs to $S$. We first investigate the case of
\emph{static} partial observability where the set of events the user
can observe is fixed a priori. In this context, we show that
checking whether a system is opaque is PSPACE-complete, which
implies that computing an optimal static observer ensuring opacity
is also a PSPACE-complete problem.
%
Next, we introduce \emph{dynamic} partial observability where the
set of events the user can observe changes over time.
%
We show how to check that a system is opaque \wrt to a dynamic
observer and also address the corresponding synthesis problem: given
a system $G$ and secret states $S$, compute the set of dynamic
observers under which $S$ is opaque. Our main result is that the set
of such observers can be finitely represented and can be computed in
EXPTIME.
}
}
franck-tpn.bib
@COMMENT{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{Command line: bib2bib -q -c category="tpn" -oc franck-tpn.cite -ob franck-tpn.bib mabib.bib}}
@COMMENT{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{Command line: bib2bib -s $date -s lex bib/mabib.bib}}
@COMMENT{{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{{Command line: bib2bib -s lex -s $date bib/mabib.bib}}
@COMMENT{{{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{{{Command line: bib2bib -s lex -s $date bib/mabib.bib}}
@COMMENT{{{{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{{{{Command line: bib2bib -s lex -s $date bib/mabib.bib}}
@ARTICLE{BCHLR08-tcs,
CLASS = {internatjournal},
AUTHOR = {B{\'e}rard, B{\'e}atrice and Cassez, Franck and Haddad, Serge and Lime, Didier and Roux, Olivier~H.},
LEX = {A},
CATEGORY = {tpn},
JOURNAL = {\begin{rawhtml}Theoretical Computer Science\end{rawhtml}},
NOTE = {},
PUBLISHER = {Copyright \begin{rawhtml}Elsevier\end{rawhtml}},
VOLUME = 403,
NUMBER = {2--3},
PAGES = {202--220},
TITLE = {When are Timed Automata Weakly Timed Bisimilar to Time {P}etri Nets?},
YEAR = {2008},
ABSTRACT = {
In this paper, we compare Timed Automata (TA) and Time
Petri Nets (TPN) with respect to weak timed bisimilarity. It is already
known that the class of bounded TPNs is strictly included in the class
of TA. It is thus natural to try and identify the subclass TAwtb of TA
equivalent to some TPN for the weak timed bisimulation relation. We
give a characterization of this subclass and we show that the membership
problem and the reachability problem for TAwtb are PSPACE-complete.
Furthermore we show that for a TA in TAwtb with integer
constants, an equivalent TPN can be built with integer bounds but with
a size exponential w.r.t. the original model. Surprisingly, using rational
bounds yields a TPN whose size is linear.
},
PDF = {./ps-pdf-files/tcs-2008.pdf}
}
@ARTICLE{cassez-jss-06,
ABSTRACT = {In this paper, we consider Time Petri Nets (TPN)
where time is associated with transitions. We give a
formal semantics for TPNs in terms of Timed
Transition Systems. Then, we propose a translation
from TPNs to Timed Automata (TA) that preserves the
behavioral semantics (timed bisimilarity) of the
TPNs. For the theory of TPNs this result is
two-fold: i) reachability problems and more
generally TCTL model-checking are decidable for
bounded TPNs; ii) allowing strict time constraints
on transitions for TPNs preserves the results
described in i). The practical appli- cations of the
translation are: i) one can specify a system using
both TPNs and Timed Automata and a precise semantics
is given to the composition; ii) one can use
existing tools for analyzing timed automata (like
Kronos, Uppaal or Cmc) to analyze TPNs. In this
paper we describe the new feature of the tool Romeo
that implements our translation of TPNs in the
Uppaal input format. We also report on experiments
carried out on various examples and compare the
result of our method to state-of-the-art tool for
analyzing TPNs. },
AUTHOR = {Cassez, Franck and Roux, Olivier H.},
LEX = {A},
DATE-MODIFIED = {2006-10-09 06:54:57 +0200},
JOURNAL = {\begin{rawhtml}Journal of Software and Systems\end{rawhtml}},
PAGES = {1456--1468},
PDF = {./ps-pdf-files/jss-06.pdf},
CATEGORY = {tpn},
TITLE = {Structural Translation from Time Petri Nets to Timed Automata},
VOLUME = {79},
CLASS = {internatjournal},
NUMBER = {10},
MONTH = OCT,
PUBLISHER = {Copyright \begin{rawhtml}Elsevier\end{rawhtml}},
YEAR = {2006}
}
@INPROCEEDINGS{BCHLR-formats2005,
ABSTRACT = {
In this paper we consider the model of Time Petri Nets
(TPN) where time is associated with transitions. We also consider Timed
Automata (TA) as defined by Alur \& Dill, and compare the expressive-
ness of the two models w.r.t. timed language acceptance and (weak)
timed bisimilarity. We first prove that there exists a TA A s.t. there is
no TPN (even unbounded) that is (weakly) timed bisimilar to A. We
then propose a structural translation from TA to (1-safe) TPNs preserv-
ing timed language acceptance. Further on, we prove that the previous
(slightly extended) translation also preserves weak timed bisimilarity for
a syntactical subclass $T_{Asyn}(\leq,\geq)$ of TA. For the theory of TPNs, the
consequences are: 1) TA, bounded TPNs and 1-safe TPNs are equally
expressive w.r.t. timed language acceptance; 2) TA are strictly more expressive than bounded TPNs w.r.t. timed bisimilarity; 3) The subclass
$T_{Asyn}(\leq,\geq)$, bounded and 1-safe TPNs ''`a la Merlin'' are equally ex-
pressive w.r.t. timed bisimilarity.
},
AUTHOR = {B\'erard, B\'eatrice and Cassez, Franck and Haddad, Serge and Roux, Olivier H. and Lime, Didier},
LEX = {B},
CATEGORY = {tpn},
BOOKTITLE = {Proc. of the 3rd Int. Conf. on Formal Modeling and Analysis of Timed Systems (FORMATS'05)},
CLASS = {internatconference},
MONTH = SEP,
PAGES = {211--225},
PDF = {./ps-pdf-files/petri-nets-formats05.pdf},
SLIDES = {./ps-pdf-files/slides-formats-05.pdf},
PUBLISHER = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
SERIES = {\begin{rawhtml}Lecture Notes in Computer Science\end{rawhtml}},
TITLE = {{Comparison of the Expressiveness of Timed Automata and Time Petri Nets}},
VOLUME = 3829,
RATE = {"44\%"},
YEAR = {2005}
}
@INPROCEEDINGS{BCHLR-fsttcs2005,
ABSTRACT = {
In this paper, we compare Timed Automata (TA) with Time Petri Nets
(TPN) with respect to weak timed bisimilarity. It is already
known that the class of bounded TPNs is included in the class
of TA. It is thus natural to try and identify the (strict) subclass
$\taminus$ of TA that is equivalent to TPN for the weak time
bisimulation relation. We give a characterisation of this subclass
and we show that the membership problem and the reachability problem
for $\taminus$ are $PSPACE$-complete. Furthermore we show that
for a TA in $\taminus$ with integer constants,
an equivalent TPN can be built with
integer bounds but with a size exponential w.r.t. the original model.
Surprisingly, using rational bounds yields a TPN whose size is
linear.
},
AUTHOR = {B\'erard, B\'eatrice and Cassez, Franck and Haddad, Serge and Roux, Olivier H. and Lime, Didier},
CATEGORY = {tpn},
LEX = {B},
BOOKTITLE = {Proc. of the 25th Int. Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'05)},
CLASS = {internatconference},
DATE-MODIFIED = {2006-10-09 07:05:49 +0200},
XXMONTH = DEC,
PAGES = {276--284},
PDF = {./ps-pdf-files/petri-nets-fsttcs05.pdf},
PUBLISHER = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
SERIES = {\begin{rawhtml}Lecture Notes in Computer Science\end{rawhtml}},
TITLE = {{When are Timed Automata weakly timed bisimilar to Time Petri Nets ?}},
VOLUME = 3821,
RATE = {"23\%"},
YEAR = {2005}
}
@INPROCEEDINGS{BCHLR-atva2005,
ABSTRACT = {
In this paper we study the model of Time Petri Nets (TPNs)
where a time interval is associated with the firing of a
transition, but we extend it by considering general intervals rather than
closed ones. A key feature of timed models is the memory policy,
i.e. which timing informations are kept when a transition is fired.
The original model selects an \emph{intermediate} semantics where
the transitions disabled after consuming the tokens, as well as the firing
transition, are reinitialised. However this semantics is not appropriate
for some applications. So we consider here two alternative semantics:
the \emph{atomic} and the \emph{persistent atomic} ones.
First we present relevant patterns of discrete event systems
which show the interest of these semantics.
Then we compare the expressiveness of the three semantics w.r.t.
the weak time bisimilarity establishing inclusion results in the
general case. Furthermore we show that some inclusions are strict with
unrestricted intervals even when nets are bounded.
Then we focus on bounded TPNs
with upper-closed intervals and we prove that the semantics are
equivalent. Finally taking into account both the practical and the
theoretical issues, we conclude that persistent atomic semantics
should be preferred.
},
AUTHOR = {B\'erard, B\'eatrice and Cassez, Franck and Haddad, Serge and Roux, Olivier H. and Lime, Didier},
CATEGORY = {tpn},
LEX = {B},
BOOKTITLE = {3rd Int. Symp. on Automated Technology for Verification and Analysis (ATVA'05)},
CLASS = {internatconference},
DATE-MODIFIED = {2006-10-09 07:11:24 +0200},
XXMONTH = OCT,
PAGES = {293--307},
PDF = {./ps-pdf-files/petri-nets-atva05.pdf},
PUBLISHER = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
SERIES = {\begin{rawhtml}Lecture Notes in Computer Science\end{rawhtml}},
TITLE = {{Comparison of Different Semantics for Time Petri Nets}},
VOLUME = 3707,
RATE = {"35\%"},
YEAR = {2005}
}
@INPROCEEDINGS{cassez-avocs-04,
ABSTRACT = {In this paper, we consider Time Petri Nets (TPN) where time is associated with
transitions. We give a formal semantics for TPNs in terms of Timed Transition Systems. Then,
we propose a translation from TPNs to Timed Automata (TA) that preserves the behavioural
semantics (timed bisimilarity) of the TPNs. For the theory of TPNs this result
is two-fold: i) reachability problems and more generally TCTL model-checking are
decidable for bounded TPNs; ii) allowing strict time constraints on transitions
for TPNs preserves the results described in i). The practical applications of
the translation are: i) one can specify a system using both TPNs and Timed
Automata and a precise semantics is given to the composition; ii) one can
use existing tools for analysing timed automata (like KRONOS or UPPAAL or CMC)
to analyse TPNs.},
LEX = {B},
AUTHOR = {Cassez, Franck and Roux, Olivier H.},
BOOKTITLE = {Proceedings of the {W}orkshop on {A}utomated {V}erification {o}f {C}ritical {S}ystems (AVoCS'04)},
CLASS = {internatconference},
CATEGORY = {tpn},
MONTH = JUN,
NOTE = {Updated English version of~\cite{cassez-msr-03}},
NUMBER = {6},
PAGES = {145--160},
PDF = {./ps-pdf-files/avocs04.pdf},
SLIDES = {./ps-pdf-files/slides-avocs-04.pdf},
PUBLISHER = {Copyright \begin{rawhtml}Elsevier\end{rawhtml}},
SERIES = {Elec. Notes in Theo. Comp. Science},
TITLE = {{Structural Translation of Time Petri Nets into Timed Automata}},
VOLUME = {128},
YEAR = {2005}
}
@INBOOK{ars-petri-nets,
AUTHOR = {Cassez, Franck and Roux, Olivier H.},
EDITOR = {Kordic, Vedran},
TITLE = {Petri Nets -- Theory and Applications},
CHAPTER = {From Time Petri Nets to Timed Automata},
PUBLISHER = {Advanced Robotic Systems, Vienna, Austria},
YEAR = {2008},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
SERIES = {{I}-Tech {E}ducation {O}nline},
XXXTYPE = {{I}nvited Chapter.},
EDITION = {},
LEX = {C},
MONTH = FEB,
CATEGORY = {tpn},
CLASS = {ed-book},
URL = {http://intechweb.org/books.php},
PAGES = {225--252},
PDF = {./ps-pdf-files/tpn-book-08.pdf},
ISBN = {ISBN 978-3-902613-12-7},
NOTE = {Free download from \url{http://intechweb.org/books.php}.},
ABSTRACT = {In this chapter we introduce a formalism, \emph{Time
Petri Nets (TPNs)}, to model real-time systems. We
compare it with another well-known formalism,
\emph{Timed Automata (TA)}, used for specifying
timed systems. We precisely define the semantics of
TPNs and TA and compare them according to two
criteria: the \emph{languages} (or set of
behaviours) then can generate, and the \emph{trees}
(or branching behaviours) they can generate. We
show that every TPN can be translated into an
equivalent TA. Then, we introduce a real-time logic
to specify properties of real-time systems. We show
how to check that a given TPN satisfies a property
written in this logic. For this we use our
translation\footnote{This translation preserves the
properties of this logic.} from TPNs to TA and check
the property on the equivalent TA. Finally we
briefly report on experiments for checking real-time
properties of TPNs using this framework. }
}
@INPROCEEDINGS{cassez-msr-03,
ABSTRACT = {Dans cet article, nous consid{\'e}rons les r{\'e}seaux de Petri
t-temporels (RdPT) c'est {\`a} dire pour lesquels le
temps est associ{\'e} aux transitions sous la forme d'un
interval. Nous en donnons une s{\'e}mantique formelle en
terme de syst{\`e}mes de transitions temporis{\'e}s. Nous
proposons ensuite une traduction structurelle des
RdPTs en un produit synchronis{\'e} d'automates
temporis{\'e}s (ATs) qui pr{\'e}serve la s{\'e}mantique
comportementale (bisimilarit{\'e} temporelle) des
RdPTs. Les cons{\'e}quences th{\'e}oriques de ce r{\'e}sultat
sont: i) les probl{\'e}mes d'accessibilit{\'e} et plus
g{\'e}n{\'e}ralement de model-checking de TCTL sont
d{\'e}cidables pour les RdPTs born{\'e}s; ii) il est
possible d'{\'e}tendre les RdPTs en consid{\'e}rant des
contraintes temporelles strictes sur les transitions
en pr{\'e}servant les r{\'e}sultats d{\'e}crits plus haut en
i). D'un point de vue pratique, les cons{\'e}quences
sont doubles: i) on peut sp{\'e}cifier un syst{\`e}me {\`a}
l'aide de RdPTs et d'automates temporis{\'e}s et en
donner une s{\'e}mantique facilement; ii) les outils
disponibles pour l'analyse des automates temporis{\'e}s
(comme \textsf{KRONOS} ou \textsf{UPPAAL} ou
\textsf{CMC}) peuvent {\^e}tre utilis{\'e}s pour la
v{\'e}rification de RdPTs.},
AUTHOR = {Cassez, Franck and Roux, Olivier Henri},
BOOKTITLE = {4$\textit{\`eme}$ Colloque Francophone sur la Mod{\'e}lisation des Syst{\`e}mes R{\'e}actifs, (MSR'03)},
LEX = {Cb},
CLASS = {natconference},
CATEGORY = {tpn},
MONTH = OCT,
NUMIRCYN = {C},
PDF = {./ps-pdf-files/tpn-ta-03.pdf},
TITLE = {{Traduction structurelle des R{\'e}seaux de {Petri} Temporels en Automates Temporis{\'e}s}},
YEAR = {2003}
}
@TECHREPORT{berard-ta2tpn-05,
ABSTRACT = {In this paper we consider the model of Time Petri Nets (TPN) ``\`a la
Merlin'' where time is associated with transitions, but we extend it
with open intervals to specify the firing intervals of the
transitions. We also consider Timed Automata (TA) as defined by Alur
\& Dill, and compare the expressiveness of the two models w.r.t.
timed language acceptance and (weak) timed bisimilarity. We first
prove the following results: 1) bounded TPNs and TA are equally
expressive w.r.t. timed language acceptance; 2) there exists a TA
${\cal A}$ s.t. there is no TPN (even unbounded) that is (weakly)
timed bisimilar to ${\cal A}$. Because of 2) above, it is
natural to try and identify the (strict) subclass of TA that is
equivalent to TPN w.r.t. weak timed bisimilarity. Thus we give some
further results: 1) we characterize the subclass TA$^-$ of TA that
is equivalent to the original model of TPN as defined by Merlin,
\ie restricted to closed intervals, 2) we show that the associated
membership problem for TA$^-$ is $PSPACE$-complete and 3) we prove
that the reachability problem for TA$^-$ is also $PSPACE$-complete.
},
AUTHOR = {B\'erard, B\'eatrice and Cassez, Franck and Haddad, Serge and Lime, Didier and Roux, Olivier Henri},
INSTITUTION = {IRCCyN/CNRS, Nantes},
LEX = {Da},
MONTH = APR,
NUMBER = {RI-2005-3},
CATEGORY = {tpn},
PDF = {./ps-pdf-files/ta2tpn.pdf},
TITLE = {{Comparison of the Expressiveness of Timed Automata and Time Petri Nets}},
YEAR = {2005}
}
@TECHREPORT{cassez-ri-msr-03,
ABSTRACT = {
In this paper, we consider Time Petri Nets (TPN) where time is
associated with transitions. We give a formal semantics for TPNs in
terms of Timed Transition Systems. Then, we propose a translation
from TPNs to Timed Automata (TA) that preserves the behavioural
semantics (timed bisimilarity) of the TPNs. For the theory of TPNs
this result is two-fold: i) reachability problems and more generally
TCTL model-checking are decidable for bounded TPNs; ii) allowing
strict time constraints on transitions for TPNs preserves the
results described in i). The practical applications of the
translation are: i) one can specify a system using both TPNs and
Timed Automata and a precise semantics is given to the composition;
ii) one can use existing tools for analysing timed automata (like
KRONOS or UPPAAL or CMC) to analyse TPNs.
},
LEX = {Da},
CATEGORY = {tpn},
AUTHOR = {Cassez, Franck and Roux, Olivier H.},
INSTITUTION = {IRCCyN/CNRS},
NOTE = {English version of~\cite{cassez-msr-03}},
NUMBER = {1496, RI-2003-4},
PDF = {./ps-pdf-files/ri-msr-03.pdf},
TITLE = {{From Time Petri Nets to Timed Automata}},
YEAR = {2003}
}
franck-bio.bib
@COMMENT{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{Command line: bib2bib -q -c category="bio" -oc franck-bio.cite -ob franck-bio.bib mabib.bib}}
@COMMENT{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{Command line: bib2bib -s $date -s lex bib/mabib.bib}}
@COMMENT{{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{{Command line: bib2bib -s lex -s $date bib/mabib.bib}}
@COMMENT{{{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{{{Command line: bib2bib -s lex -s $date bib/mabib.bib}}
@COMMENT{{{{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{{{{Command line: bib2bib -s lex -s $date bib/mabib.bib}}
@INPROCEEDINGS{bernot-bioconcur-2003,
ABSTRACT = { The aim of the paper is to revisit the model of Biological
Regulatory Networks (BRN) which was proposed by Ren\'e Thomas to
model the interactions between a set of genes. We give a formal
semantics for BRN in terms of transition systems which formalizes
the evolution rules given by Ren\'e Thomas. Then we show how to use
this model to find interesting properties of a BRN like the set of
stable states, cycles etc using tools for analyzing transition
systems.
},
CATEGORY = {bio},
AUTHOR = {Bernot, Gilles and Cassez, Franck and Comet, Jean-Paul and Delaplace, Franck and M\"uller, C\'eline and Roux, Olivier F. and Roux, Olivier H.},
LEX = {Bb},
BOOKTITLE = {Proc. of the Workshop on Concurrent Models in Molecular Biology (BioConcur'03)},
CLASS = {internatconference},
XXMONTH = SEP,
CATEGORY = {bio},
XXNOTE = {Forthcoming},
PDF = {./ps-pdf-files/bioconcur-entcs-07.pdf},
PUBLISHER = {Copyright \begin{rawhtml}Elsevier\end{rawhtml}},
SERIES = {Elec. Notes in Theo. Comp. Science},
VOLUME = 180,
NUMBER = 3,
TITLE = {{Semantics of {Biological Regulatory Networks}}},
YEAR = {2007}
}
franck-languages.bib
@COMMENT{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{Command line: bib2bib -q -c category="langrt" -oc franck-languages.cite -ob franck-languages.bib mabib.bib}}
@COMMENT{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{Command line: bib2bib -s $date -s lex bib/mabib.bib}}
@COMMENT{{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{{Command line: bib2bib -s lex -s $date bib/mabib.bib}}
@COMMENT{{{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{{{Command line: bib2bib -s lex -s $date bib/mabib.bib}}
@COMMENT{{{{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{{{{Command line: bib2bib -s lex -s $date bib/mabib.bib}}
@ARTICLE{cassez-fi-2004,
ABSTRACT = { In this paper we present a \emph{timed} extension of the AltaRica
formalism. Following previous works, we first extend the semantics of
AltaRica with time and define \emph{timed components} and \emph{timed nodes}.
Moreover we lift the \emph{priority features} of AltaRica to the timed
case. We obtain a timed version of AltaRica, called Timed AltaRica. Finally we give
a translation of a Timed AltaRica specification into a usual timed automaton.
These are the semantic foundations of a high-level hierarchical
language for the specification of timed systems.
},
AUTHOR = {Cassez, Franck and Pagetti, Claire and Roux, Olivier F.},
JOURNAL = {\begin{rawhtml}Fundamenta Informaticae\end{rawhtml}},
LEX = {A},
MONTH = AUG,
NUMBER = {3--4},
CATEGORY = {langrt},
PAGES = {291--332},
PDF = {./ps-pdf-files/fi-timed-altarica.pdf},
TITLE = {{A timed extension for \textsf{AltaRica}}},
CLASS = {internatjournal},
VOLUME = {62},
YEAR = {2004}
}
@ARTICLE{herbreteau-jrts-01,
ABSTRACT = {We are concerned in this paper with the verification of
reactive systems with event memorization. The
reactive systems are specified with an asynchronous
reactive language {\sf Electre} the main feature of
which is the capability of memorizing occurrences of
events in order to process them later. This memory
capability is quite interesting for specifying
reactive systems but leads to a verification model
with a dramatically large number of states (due to
the stored occurrences of events). In this paper, we
show that {\em partial-order} methods can be applied
successfuly for verification purposes on our model
of reactive programs with event memorization. The
main points of our work are two-fold: (1) we show
that the \emph{independance relation} which is a key
point for applying partial-order methods can be
extracted automatically from an {\sf Electre}
program; (2) the partial-order technique turns out
to be very efficient and may lead to a drastic
reduction in the number of states of the model as
demonstrated by a real-life industrial case study. },
AUTHOR = {Herbreteau, Fr\'ed\'eric and Cassez, Franck and Roux, Olivier},
CATEGORY = {langrt},
JOURNAL = {\begin{rawhtml}Journal of Real-Time Systems\end{rawhtml}},
MONTH = MAY,
PUBLISHER = {Copyright \begin{rawhtml}Kluwer\end{rawhtml}},
CLASS = {internatjournal},
LEX = {A},
NUMBER = {3},
NUMIRCYN = {A},
PAGES = {287-316},
PDF = {./ps-pdf-files/jrts-01.pdf},
PS = {./ps-pdf-files/jrts-01.ps.gz},
TITLE = {{Application of Partial-Order Methods to Reactive Systems with Event Memorization}},
VOLUME = {20},
YEAR = {2001}
}
@ARTICLE{roux-jfac-99,
ABSTRACT = {We present in this paper some new language features and constructs,
that allow the joint synchronous/asynchronous programming of reactive
applications, as well as their formal verification. We show that
reactive applications may be dealt with from two points of view.
First, from the {\em chronological} point of view, i.e., when
reactions are instantaneous, generated by event occurrences in
discrete time. Second, from the {\em chronometrical} point of view,
when reactions have durations in dense time. This duality must be
expressible in languages that allow a consistent programming of both
{\em synchronous} and {\em asynchronous} features. The objective of
mixing these dual approaches leads to model reactive systems by using
{\em hybrid systems}, to deal simultaneously with both discrete and
continuous phenomena. Furthermore, this must be followed by some
verification of the application's properties, with respect to its
behavioural and quantitative features. We analyze several existing
frameworks that meet these requirements, and propose our own approach
based on the language {\sf Electre}.},
AUTHOR = {Roux, Olivier and Rusu, Vlad and Cassez, Franck},
JOURNAL = {\begin{rawhtml}Formal Aspects of Computing\end{rawhtml}},
MONTH = DEC,
PUBLISHER = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
CLASS = {internatjournal},
LEX = {A},
NUMBER = {4},
NUMIRCYN = {A},
PAGES = {448--471},
PS = {./ps-pdf-files/fac-99.ps.gz},
CATEGORY = {langrt},
TITLE = {{Hybrid Verification of Reactive Systems}},
VOLUME = {11},
YEAR = {1999}
}
@ARTICLE{cassez-jesa-97,
ABSTRACT = {{\it GRAFCET} is a graphical formalism derived from Petri
Nets and widely used to program automation
applications. So far, this formalism has not been
equipped with a formal semantics: interpretation
algorithms give the meaning of a GRAFCET
description. Our purpose is to take advantage of the
work carried out for reactive languages: these
languages are given a precise behavioural semantics
by means of finite-state machines; the behavioural
model can then be checked for various
properties. The work presented hereafter consists in
equipping GRAFCET with a formal semantics to obtain
a behavioural model (namely a timed automaton) that
captures the metric aspect of time. },
AUTHOR = {Cassez, Franck},
CATEGORY = {langrt},
LEX = {A},
DATE-MODIFIED = {2006-10-09 07:22:12 +0200},
JOURNAL = {\begin{rawhtml}European Journal of Automation\end{rawhtml}},
KEYWORDS = {semantics,reactive language},
CLASS = {internatjournal},
NUMBER = {3},
PUBLISHER = {\begin{rawhtml}Hermès Science\end{rawhtml}},
NUMIRCYN = {A},
PAGES = {581--603},
PS = {./ps-pdf-files/jesa-97.ps.gz},
TITLE = {{Formal Semantics for Reactive {GRAFCET}}},
VOLUME = {31},
YEAR = {1997}
}
@ARTICLE{cassez-tcs-95,
ABSTRACT = {We present in this paper an operational semantics for the
{\sf ELECTRE} reactive language (Roux et al.,
1992). This language is based on an asynchronous
approach to real-time systems. First basic concepts
and intuitive semantics are introduced. Then we give
rules to model dynamic semantics of {\sf ELECTRE}
programs: this constitutes an operational semantics
for the {\sf ELECTRE} language. This operational
semantics is used to define a model of execution for
{\sf ELECTRE} programs: transition system. In
addition, we prove, using structural induction on
the operational semantics, that this transition
system is a finite state transition
system. Eventually, we extend the previous
transition system so as to handle multiple-storage
events: it is important since the asynchronous {\sf
ELECTRE} language deals with multiple memorized
occurrences of the events. This result gives a means
of compiling the {\sf ELECTRE} language into a
finite-state machine. },
AUTHOR = {Cassez, Franck and Roux, Olivier},
JOURNAL = {\begin{rawhtml}Theoretical Computer Science\end{rawhtml}},
LEX = {A},
KEYWORDS = {Informatique th\'eorique},
CATEGORY = {langrt},
MONTH = JUL,
CLASS = {internatjournal},
NUMBER = {1--2},
NUMIRCYN = {A},
PAGES = {109--143},
TITLE = {{Compilation of the {Electre} Reactive Language into Finite Transition Systems}},
URL = {http://www.sciencedirect.com},
VOLUME = {146},
PUBLISHER = {Copyright \begin{rawhtml}Elsevier\end{rawhtml}},
YEAR = {1995}
}
@ARTICLE{tsi-92,
AUTHOR = {Roux, Olivier and Creusot, Denis and Cassez, Franck and Elloy, {Jean-Pierre}},
TITLE = {Le langage r\'eactif asynchrone {ELECTRE}},
JOURNAL = {\begin{rawhtml}Technique et Science Informatiques\end{rawhtml}},
YEAR = {1992},
LEX = {B},
OPTKEY = {},
CATEGORY = {langrt},
VOLUME = {11},
NUMBER = {5},
PAGES = {35--66},
CLASS = {natjournal},
OPTXXMONTH = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@INPROCEEDINGS{herbreteau-latin-02,
ABSTRACT = { Reactive Fiffo Systems (RFS)
are used to model reactive systems which are able to memorize the
events that cannot be processed when they occur. In this paper we
investigate the decidability of verification problems for Embedded
RFS which are RFS running under some environmental constraints. We
show that almost all the usual verification problems are undecidable
for the class of Periodically Embedded RFS with two memorizing
events, whereas they become decidable for Regularly Embedded RFS
with a single memorizing event. We then focus on Embedded Lossy RFS
and we show in particular that for Regularly Embedded Lossy RFS the
set of predecessors $\textit{Pred}^*$ is upward closed and
effectively computable.
},
AUTHOR = {Herbreteau, Fr{\'e}d{\'e}ric and Cassez, Franck and Finkel, Alain and Roux, Olivier F. and Sutre, Gr\'egoire},
BOOKTITLE = {Proc. of the Latin American Symp. on Theoretical Informatics (LATIN'02)},
LEX = {B},
CLASS = {internatconference},
KEY = {latin-02},
KEYWORDS = {FIFFO-automata, model-checking, recognizability},
MONTH = MAR,
NUMIRCYN = {C},
PAGES = {400--414},
PDF = {./ps-pdf-files/latin-02.pdf},
PS = {./ps-pdf-files/latin-02.ps.gz},
PUBLISHER = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
SERIES = {\begin{rawhtml}Lecture Notes in Computer Science\end{rawhtml}},
CATEGORY = {langrt},
TITLE = {{Verification of Embedded Reactive {FIFFO} Systems}},
RATE = {"42\%"},
VOLUME = {2286},
YEAR = {2002}
}
@INPROCEEDINGS{prigent-spin-02,
ABSTRACT = { This paper tackles the problem of model-checking SDL
programs that use the save operator. Previous work on model-checking
SDL programs with SPIN consisted in translating SDL into IF (using
sdl2if) and finally IF to Promela (if2pml). However, the save
operator of SDL is not handled by the (final) translator if2pml . We
propose an extension of the if2pml tool that translates IF into
Promela programs with save operators. We also add an abstraction
method on buffer messages to if2pml allowing the user to gather some
buffer messages into one abstract value. We use our extended version
of if2pml to validate an Unmanned Underwater Vehicle (UUV) subsystem
specified with SDL.},
AUTHOR = {Prigent, Armelle and Cassez, Franck and Dhaussy, Philippe and Roux, Olivier F.},
BOOKTITLE = {Proc. of the 9th International SPIN Workshop on Model Checking of Software (SPIN'02)},
CLASS = {internatconference},
KEYWORDS = {SDL formalism, save operator, model-checking, data abstraction},
MONTH = MAR,
CATEGORY = {langrt},
LEX = {B},
NUMIRCYN = {C},
PAGES = {400--414},
PDF = {./ps-pdf-files/spin-02.pdf},
PS = {./ps-pdf-files/spin-02.ps.gz},
PUBLISHER = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
SERIES = {\begin{rawhtml}Lecture Notes in Computer Science\end{rawhtml}},
RATE = {"50\%"},
TITLE = {{Extending the Translation from {SDL} to {Promela}}},
VOLUME = {2318},
YEAR = {2002}
}
@INPROCEEDINGS{sutre-amast-98,
ABSTRACT = {Our work intends to verify reactive systems with event
memorization specified with the reactive language
{\sf Electre}. For this, we define a particular
behavioral model for {\sf Electre} programs,
reactive FIFFO Automata (RFAs), which is close to
Fifo Automata. Intuitively, a RFA is the model of a
reactive system which may store event occurrences
that must not be immediately taken into account. We
show that, contrarily to lossy systems where the
reachability set is rec ognizable but not
effectively computable, (1) the reachability set of
a RFA is recognizable, and (2) it is effectively
computable. Moreover, we also study the
relationships between RFAs and Finite Automata and
we prove that (3) from a trace language point of
view, inclusions between RFAs and Finite Automata
are undecidable and (4) the linear temporal logic
$\LTL$ on states without the temporal operator next
is decidable for RFAs, while $\LTL$ on transitions
is undecidable. },
AUTHOR = {Sutre, Gr\'egoire and Finkel, Alain and Roux, Olivier F. and Cassez, Franck},
BOOKTITLE = {Proc. of the 7th Int. Conf. on Algebraic Methodology and Software Technology (AMAST'98)},
CLASS = {internatconference},
KEYWORDS = {FIFFO-automata, model-checking, recognizability},
MONTH = JAN,
CATEGORY = {langrt},
LEX = {B},
NUMIRCYN = {C},
PAGES = {106--123},
PS = {./ps-pdf-files/amast-98.ps.gz},
PUBLISHER = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
SERIES = {\begin{rawhtml}Lecture Notes in Computer Science\end{rawhtml}},
TITLE = {{Effective recognizability and model-checking of reactive {FIFFO} automata}},
VOLUME = {1548},
YEAR = {1999}
}
@INPROCEEDINGS{pagetti-facs-2003,
ABSTRACT = { In this paper we present a timed extension of the AltaRica language,
Timed AltaRica, and describe the architecture of a compiler from Timed AltaRica to timed
automata. We present the features of the language, namely
modularity, hierarchical modeling and reuse of components during the
specification phase, on an avionics example. Then, we use the
compiler from Timed AltaRica to Timed Automata to check some safety properties
on the system.},
LEX = {Ca},
AUTHOR = {Pagetti, Claire and Cassez, Franck and Roux, Olivier F.},
BOOKTITLE = {Workshop on Formal Aspects of Component Software (FACS'03)},
CLASS = {other},
CATEGORY = {langrt},
MONTH = SEP,
NOTE = {Pisa, Italy, September 8--9, 2003},
PAGES = {63--80},
PDF = {./ps-pdf-files/facs-03.pdf},
PUBLISHER = {UNU/IIST, Macau},
TITLE = {{Hierarchical Modeling and Verification of Timed Systems in Timed {AltaRica}}},
URL = {http://www.iist.unu.edu/newrh/III/1/docs/techreports/report284.html},
YEAR = {2003}
}
@INPROCEEDINGS{cassez-msr-96,
AUTHOR = {Cassez, Franck},
TITLE = {S\'emantique pour le {GRAFCET} r\'eactif},
OPTCROSSREF = {},
OPTKEY = {},
BOOKTITLE = {{A}ctes du $1^{er}$ {C}olloque sur la {M}od{\'e}lisation des {S}yst{\`e}mes {R}{\'e}actifs ({MSR}'96)},
LEX = {D},
OPTPAGES = {},
YEAR = {1996},
CLASS = {natconference},
CATEGORY = {langrt},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {},
OPTXXMONTH = {},
OPTORGANIZATION = {},
OPTPUBLISHER = {},
OPTNOTE = {},
OPTANNOTE = {}
}
@INPROCEEDINGS{cassez-cari-00,
AUTHOR = {Cassez, Franck and Herbreteau, Fr\'ed\'eric and Roux, Olivier F.},
BOOKTITLE = {Conf{\'e}rence Africaine de Recherche en Informatique, CARI'2000},
CLASS = {natconference},
KEYWORDS = {FIFFO automaton},
MONTH = OCT,
NOTE = {Conf{\'e}rence francophone},
NUMIRCYN = {D},
CATEGORY = {langrt},
LEX = {D},
PAGES = {291--298},
PS = {./ps-pdf-files/cari2000.ps},
PUBLISHER = {INRIA},
TITLE = {{Reactive Systems with Unbounded Event Memorization}},
YEAR = {2000}
}
@TECHREPORT{cassez-altarica-02,
ABSTRACT = {In this work we present a \emph{timed} extension of the
AltaRica formalism. We extend the semantics of
AltaRica to \emph{timed components} and \emph{timed
nodes}. Moreover we also extend the \emph{priority
mechanism} of AltaRica to the timed case. Finally we
give a translation of a Timed AltaRica specification
into a usual timed automaton that can then be
analysed by existing tools for checking properties
of timed systems.},
CATEGORY = {langrt},
LEX = {Da},
AUTHOR = {Cassez, Franck and Pagetti, Claire and Roux, Olivier F.},
INSTITUTION = {IRCCyN/CNRS, Nantes},
MONTH = DEC,
NUMBER = 13,
PDF = {./ps-pdf-files/timed-altarica.pdf},
TITLE = {{A timed extension for \textsf{AltaRica}}},
URL = {http://altarica.labri.fr/},
YEAR = {2002}
}
franck-misc.bib
@COMMENT{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{Command line: bib2bib -q -c category="misc" -oc franck-misc.cite -ob franck-misc.bib mabib.bib}}
@COMMENT{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{Command line: bib2bib -s $date -s lex bib/mabib.bib}}
@COMMENT{{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{{Command line: bib2bib -s lex -s $date bib/mabib.bib}}
@COMMENT{{{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{{{Command line: bib2bib -s lex -s $date bib/mabib.bib}}
@COMMENT{{{{{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{{{{{Command line: bib2bib -s lex -s $date bib/mabib.bib}}
@MISC{cassez-compile-phaver-09,
AUTHOR = {Cassez, Franck},
CLASS = {other},
CATEGORY = {misc},
HOWPUBLISHED = {Short Note, NICTA, Sydney, Australia},
KEYWORDS = {PHAVer, OS X},
MONTH = MAR,
NUMIRCYN = {D},
LEX = {D},
TITLE = {{How to Install PHAVer on Mac OS X}},
PDF = {./ps-pdf-files/install-phaver-09.pdf},
YEAR = {2009},
URL = {http://www-verimag.imag.fr/~frehse/phaver_web/index.html},
ABSTRACT = {This short note explains how to install PHAVer (and the
needed libraries) for a single user on Mac OS X
running Leopard (10.5.6). It might also work for
earlier versions (you can report to me in case of a
successful install on earlier version).}
}
@MISC{cassez-notes-auto-09,
AUTHOR = {Cassez, Franck},
CLASS = {other},
CATEGORY = {misc},
HOWPUBLISHED = {Short Note, NICTA, Sydney, Australia},
KEYWORDS = {automate, langage, régulier},
MONTH = JUL,
NUMIRCYN = {D},
LEX = {D},
TITLE = {{Langages Réguliers et Automates Finis}},
PDF = {./ps-pdf-files/notes-auto-09.pdf},
YEAR = {2009},
NOTE = {Old version from 2006 updated},
ABSTRACT = {Petite introduction aux automates finis et langages
réguliers.}
}
@BOOK{cassez-movep-01,
ABSTRACT = {This LNCS Tutorials volume gathers the contributions of speakers
who gave talks at the summer school MOVEP'00, held in Nantes, France in
june 2000.},
EDITOR = {Cassez, Franck and Jard, Claude and Rozoy, Brigitte and Ryan, Mark D.},
CLASS = {ed-book},
CATEGORY = {misc},
MONTH = JUN,
LEX = {D},
NUMIRCYN = {B},
PUBLISHER = {Copyright \begin{rawhtml}Springer\end{rawhtml}},
SERIES = {Lecture Notes in Computer Science Tutorials},
TITLE = {{Proc. of the Int. Summer School on Modelling and Verification of Parallel Processes (MOVEP'2k)}},
URL = {http://link.springer.de/link/service/series/0558/tocs/t2067.htm},
VOLUME = {2067},
YEAR = {2001}
}
@INPROCEEDINGS{cassez-fireworks-00,
AUTHOR = {Cassez, Franck and Ryan, Mark D. and Schobbens, Pierre-Yves},
BOOKTITLE = {3rd {FIREworks} Workshop -- Language Constructs for Describing Features},
CLASS = {other},
XXMONTH = MAY,
LEX = {D},
NUMIRCYN = {C},
PAGES = {85--104},
PS = {./ps-pdf-files/book-feature-atl.ps},
CATEGORY = {misc},
PUBLISHER = {Springer Verlag, London},
TITLE = {{Proving Feature non-interaction with Alternating Time Temporal logic.}},
YEAR = {2000}
}
@BOOK{cassez-movep-02,
CLASS = {ed-book},
EDITOR = {Cassez, Franck and Jard, Claude and Laroussinie, Fran\c{c}ois and Ryan, Mark D.},
KEYWORDS = {Informatique, v{\'e}rification, sp{\'e}cification},
MONTH = JUN,
NOTE = {450 pages, in English},
NUMIRCYN = {B},
LEX = {D},
PUBLISHER = {Ecole Centrale de Nantes},
CATEGORY = {misc},
TITLE = {{Proceedings of the Summer School MOVEP'2002}},
URL = {http://www.cs.bham.ac.uk/~mdr/movep},
YEAR = {2002}
}
@BOOK{cassez-movep-06,
ADDRESS = {Bordeaux, France},
CLASS = {ed-book},
EDITOR = {Cassez, Franck and J\'eron, Therry and Laroussinie,
Fran\c{c}ois and Raskin, Jean-Fran\c{c}ois and Ryan,
Mark D.},
LEX = {D},
CATEGORY = {misc},
KEYWORDS = {Informatique, v{\'e}rification, sp{\'e}cification},
MONTH = DEC,
NOTE = {400 pages, in English},
NUMIRCYN = {B},
PUBLISHER = {LaBRI, Bordeaux, France},
TITLE = {{Proceedings of the Summer School MOVEP'2006}},
URL = {http://www.cs.bham.ac.uk/~mdr/movep},
YEAR = {2006}
}
@BOOK{cassez-movep-04,
ADDRESS = {Bruxelles, Belgium},
CLASS = {ed-book},
EDITOR = {Cassez, Franck and J\'eron, Therry and Laroussinie,
Fran\c{c}ois and Raskin, Jean-Fran\c{c}ois and Ryan,
Mark D.},
LEX = {D},
KEYWORDS = {Informatique, v{\'e}rification, sp{\'e}cification},
MONTH = DEC,
CATEGORY = {misc},
NOTE = {400 pages, in English},
NUMIRCYN = {B},
PUBLISHER = {Universit\'e Libre de Bruxelles, Belgique},
TITLE = {{Proceedings of the Winter School MOVEP'2004}},
URL = {http://www.cs.bham.ac.uk/~mdr/movep},
YEAR = {2004}
}
@BOOK{cassez-movep-00,
CLASS = {ed-book},
EDITOR = {Cassez, Franck and Jard, Claude and Rozoy, Brigitte and Ryan, Mark D.},
KEYWORDS = {Informatique, v{\'e}rification, sp{\'e}cification},
MONTH = JUN,
LEX = {D},
NOTE = {300 pages, in English},
CATEGORY = {misc},
NUMIRCYN = {B},
PUBLISHER = {Ecole Centrale de Nantes},
TITLE = {{Proceedings of the Summer School MOVEP'2000}},
YEAR = {2000}
}
@BOOK{cassez-movep-98,
CLASS = {ed-book},
EDITOR = {Cassez, Franck and Jard, Claude and Roux, Olivier F. and Rozoy, Brigitte},
KEYWORDS = {Informatique, v{\'e}rification, sp{\'e}cification},
MONTH = JUN,
LEX = {D},
NOTE = {280 pages, in french},
CATEGORY = {misc},
NUMIRCYN = {B},
PUBLISHER = {Ecole Centrale de Nantes},
TITLE = {{Actes de l'\'ecole d'\'et\'e MOVEP'98}},
YEAR = {1998}
}
@MISC{bouabdallah-brest-98,
AUTHOR = {Bouabdallah, Ahmed and Cassez, Franck and Champeau, Jo\"el and Dhaussy, Philippe and Lorillard, Fran\c{c}ois and Roux, Olivier F;},
CLASS = {other},
HOWPUBLISHED = {7$^{\mbox{\em i\`eme}}$ journ\'ees th\'ematiques {\em Informatique et \'electronique embarqu\'ees}, Brest},
KEYWORDS = {verification, temps-reel},
MONTH = OCT,
LEX = {E},
CATEGORY = {misc},
NUMIRCYN = {D},
TITLE = {V\'erification d'un logiciel temps-r\'eel distribu\'e: \'etude comparative des environnements {B, SDT et SPIN}},
YEAR = {1998}
}