@inproceedings{Chatain-Jard_FORTE04,
address = {Madrid, Spain},
month = sep,
year = 2004,
volume = 3235,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {de Frutos-Escrig, David and N{\'U}{\~n}ez, Manuel},
acronym = {{FORTE}'04},
booktitle = {{P}roceedings of 24th {IFIP} {WG6.1}
{I}nternational {C}onference on {F}ormal
{T}echniques for {N}etworked and {D}istributed {S}ystems
({FORTE}'04)},
author = {Chatain, {\relax Th}omas and Jard, Claude},
title = {Symbolic Diagnosis of Partially Observable Concurrent Systems},
pages = {326-342},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Chatain-Jard_FORTE04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Chatain-Jard_FORTE04.pdf},
abstract = {Monitoring large distributed concurrent systems is a challenging
task. In this paper we formulate (model-based) diagnosis by means of hidden
state history reconstruction, from event (e.g.~alarm) observations. We follow
a so-called true concurrency approach: the model defines explicitly the causal
and concurrency relations between the observable events, produced by the
system under supervision on different points of observation. The problem is to
compute on-the-fly the different partial order histories, which are the
possible explanations of the observable events. In this paper we extend our
first method based on Petri nets unfolding to high-level parameterized Petri
nets. This allows the designer to model data aspects (even on infinite
domains) and non deterministic actions. The observation of such an action
gives only partial information and the supervisor has to introduce parameters
to represent the hidden aspects of the reached state. This supposes that the
possible values for the parameters are symbolically computed and refined
during supervision. In practice, non deterministic actions can also be used as
an approximation to deal with incomplete information about the system. In this
case the refinement of the parameters during supervision improves the
knowledge of the model. }
}
@inproceedings{Chatain-Jard_FORMATS05,
address = {Uppsala, Sweden},
month = nov,
year = 2005,
volume = 3829,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Pettersson, Paul and Yi, Wang},
acronym = {{FORMATS}'05},
booktitle = {{P}roceedings of the 3rd {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'05)},
author = {Chatain, {\relax Th}omas and Jard, Claude},
title = {Time Supervision of Concurrent Systems Using Symbolic Unfoldings of
Time {P}etri Nets},
pages = {196-210},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/RR5706-CJ05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/RR5706-CJ05.pdf},
doi = {10.1007/11603009_16},
abstract = {Monitoring real-time concurrent systems is a challenging task.
In~this paper we formulate (model-based) supervision by means of hidden state
history reconstruction, from event (e.g.~alarm) observations. We~follow a
so-called true concurrency approach using time Petri nets: the model defines
explicitly the causal and concurrency relations between the observable events,
produced by the system under supervision on different points of observation,
and constrained by time aspects. The~problem is to compute on-the-fly the
different partial order histories, which are the possible explanations of the
observable events. We~do~not impose that time is observable: the aim of
supervision is to infer the partial ordering of the events and their possible
firing dates. This is achieved by considering a model of the system under
supervision, given as a time Petri net, and the on-the-fly construction of an
unfolding, guided by the observations. Using a symbolic representation, this
paper presents a new definition of the unfolding of time Petri nets with dense
time. }
}
@inproceedings{Chatain-Helouet-Jard_FORTE05,
address = {Taipei, Taiwan},
month = oct,
year = 2005,
volume = 3731,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Wang, Farn},
acronym = {{FORTE}'05},
booktitle = {{P}roceedings of 25th {IFIP} {WG6.1}
{I}nternational {C}onference on {F}ormal
{T}echniques for {N}etworked and {D}istributed {S}ystems
({FORTE}'05)},
author = {Chatain, {\relax Th}omas and H{\'e}lou{\"e}t, Lo{\"\i}c and Jard, Claude},
title = {From Automata Networks to~{HMSC}s: A Reverse Model Engineering Perspective},
pages = {489-502},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Chatain-Helouet-Jard_FORTE05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Chatain-Helouet-Jard_FORTE05.pdf},
doi = {10.1007/11562436_35},
abstract = {
This paper considers the problem of automatic abstraction, from a low-level model given
in term of network of interacting automata to a high-level message sequence chart.
This allows the designer to play in a coherent way with the local and global views
of a system, and opens new perspectives in reverse model engineering. Our technique
is based on a partial order semantics of synchronous parallel automata and the
construction of a complete finite prefix of an event-structure coding all the
behaviors. We present the models and algorithms. The examples presented in the
paper have been processed by a small software prototype we have implemented.}
}
@inproceedings{Chatain-Jard_SAPIR05,
address = {Lisbon, Portugal},
month = jul,
year = 2005,
optaddress = {},
publisher = {{IEEE} Computer Society Press},
noeditor = {},
acronym = {{AICT}\slash {SAPIR}\slash {ELETE} 2005},
booktitle = {Telecommunications~2005: Advanced Industrial Conference on
Telecommunications~-- Service Assurance with Partial and
Intermittent Resources Conference~-- E-Learning on
Telecommunications Workshop ({AICT}\slash {SAPIR}\slash {ELETE} 2005)},
author = {Chatain, {\relax Th}omas and Jard, Claude},
title = {Models for the Supervision of Web Services Orchestration with Dynamic Changes},
pages = {446-451},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Chatain-Jard_SAPIR05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Chatain-Jard_SAPIR05.pdf},
doi = {10.1109/AICT.2005.60},
abstract = {Programming on the Web enlights some classical problems encountered on large
distributed applications with a particular emphasis on dynamic changes. In~that
context, we are interested in the questions of supervision and diagnosis.
Our~approach is based on true-concurrency models and consists in building an
unfolding of a model of the supervised system, that selects the histories that
explain the observed alarms. In~this paper we extend the notion of unfolding of
high-level Petri nets to a model of dynamic systems that we define. This model
is close to high-level Petri nets and allows us to model dynamicity. Finally we
explain how to use unfoldings of dynamic nets for the diagnosis application.}
}
@inproceedings{Jard-Chatain-Bourhis_MSR05,
address = {Autrans, France},
month = oct,
year = 2005,
publisher = {Herm{\`e}s},
editor = {Alla, Hassane and Rutten, {\'E}ric},
acronym = {{MSR}'05},
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)},
author = {Jard, Claude and Chatain, {\relax Th}omas and Bourhis, Pierre},
title = {Diagnostic temporel dans les syst{\`e}mes r{\'e}partis {\`a}
l'aide de d{\'e}pliages de r{\'e}seaux de {P}etri temporels},
pages = {351-365},
abstract = {La supervision et le diagnostic dans les syst\`emes r\'epartis
temps-r\'eel est une question d'une grande actualit\'e. Dans cet article, nous
pr\'esentons le probl\`eme de la supervision comme la reconstruction des histoires
cach\'ees d'un mod\`ele temporel, \`a partir de l'observation r\'epartie d'\'ev\'enements.
Nous utilisons une approche fond\'ee sur une s\'emantique d'ordre partiel des
r\'eseaux de Petri temporels.}
}
@inproceedings{Chatain_CFIP05,
address = {Bordeaux, France},
month = apr,
year = 2005,
publisher = {Herm{\`e}s},
editor = {Castanet, Richard},
booktitle = {{A}ctes du 11{\`e}me {C}olloque {F}rancophone
sur l'{I}ng{\'e}nierie des {P}rotocoles},
author = {Chatain, {\relax Th}omas},
title = {Diagnostic pour les syst{\`e}mes distribu{\'e}s dynamiques partiellement observables},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Chatain_CFIP05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Chatain_CFIP05.pdf},
abstract = {De plus en plus de composants des syst\`emes distribu\'es \'emettent
des alarmes ou des messages d'erreur lorsqu'une situation particuli\`ere se
produit. Or la masse d'alarmes enregistr\'ees oblige \`a construire des outils
automatiques qui se basent sur un mod\`ele du syst\`eme pour remonter aux causes
premi\`eres des anomalies. Nous nous int\'eressons au probl\`eme du diagnostic bas\'e
sur des mod\`eles de vraie concurrence. Notre approche consiste \`a construire un
d\'epliage d'un mod\`ele du syst\`eme supervis\'e en s\'electionnant les histoires qui
expliquent les alarmes observ\'ees. Dans cet article nous \'etendons la notion de
d\'epliage symbolique de r\'eseaux de Petri de haut niveau \`a un mod\`ele de r\'eseaux
dynamiques que nous d\'efinissons. Ce mod\`ele se rapproche des r\'eseaux de Petri
de haut niveau mais permet en plus de mod\'eliser des syst\`emes dynamiques. Enfin
nous montrons comment utiliser les d\'epliages symboliques des r\'eseaux
dynamiques dans le cadre du diagnostic.}
}
@phdthesis{Chatain-PhD,
author = {Chatain, {\relax Th}omas},
title = {D{\'e}pliages symboliques de r{\'e}seaux de {P}etri de haut niveau
et application {\`a} la supervision des syst{\`e}mes r{\'e}partis},
month = nov,
year = 2006,
type = {Th{\`e}se de doctorat},
school = {Universit{\'e} Rennes~1, Rennes, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PhD-chatain.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PhD-chatain.pdf},
abstract = {Many components of distributed systems are now designed so that
they emit alarms when some particular conditions are met. Nevertheless
inferring the causes of the failures remains a challenging problem which
sometimes requires to reconstruct a part of the history of the system. We
propose to compute the explanations of an observation, according to a model of
the net. For this we use the notion of unfoldings of Petri nets. Unfoldings
provide an efficient way to represent the executions and to emphasize the
causality and concurrency relations between the events. This allows to find
easily the causes of the failures. But in order to model real systems,
high-level extensions of Petri nets are often required. We define symbolic
unfoldings of colored Petri nets, dynamic nets and time Petri nets. In
symbolic unfoldings the histories are grouped into families of parameterized
executions.}
}
@inproceedings{Cassez-Chatain-Jard_ATVA06,
address = {Beijing, China},
month = oct,
year = {2006},
volume = 4218,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Graf, Susanne and Zhang, Wenhui},
acronym = {{ATVA}'06},
booktitle = {{P}roceedings of the 4th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'06)},
author = {Cassez, Franck and Chatain, {\relax Th}omas and Jard, Claude},
title = {Symbolic Unfoldings For Networks of Timed Automata},
pages = {307-321},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Cassez-Chatain-Jard_RI-IRCCyN-2006-4.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Cassez-Chatain-Jard_RI-IRCCyN-2006-4.pdf},
doi = {10.1007/11901914_24},
abstract = {In this paper we give a symbolic concurrent semantics for network of timed
automata~(NTA) in terms of extended symbolic nets. 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.}
}
@inproceedings{Chatain-Jard_ICATPN06,
address = {Turku, Finland},
month = jun,
year = 2006,
volume = 4024,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Donatelli, Susanna and Thiagarajan, P. S.},
acronym = {{ICATPN}'06},
booktitle = {{P}roceedings of the 27th
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({ICATPN}'06)},
author = {Chatain, {\relax Th}omas and Jard, Claude},
title = {Complete Finite Prefixes of Symbolic Unfoldings of Safe Time {P}etri Nets},
pages = {125-145},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Chatain-Jard_ICATPN06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Chatain-Jard_ICATPN06.pdf},
doi = {10.1007/11767589_8},
abstract = {Time Petri nets have proved their interest in modeling real-time concurrent
systems. Their usual semantics is defined in term of firing sequences, which can
be coded in a (symbolic and global) state graph, computable from a bounded net.
An~alternative is to consider a {"}partial order{"} semantics given in
term of
processes, which keep explicit the notions of causality and concurrency without
computing arbitrary interleavings. In ordinary place/transition bounded nets, it
has been shown for many years that the whole set of processes can be finitely
represented by a prefix of what is called the {"}unfolding{"}. This paper
defines
such a prefix for safe time Petri nets. It is based on a symbolic unfolding of
the net, using a notion of {"}partial state{"}.}
}
@article{Chatain-Khomenko_IPL07,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Chatain, {\relax Th}omas and Khomenko, Victor},
title = {On the Well-Foundedness of Adequate Orders Used for
Construction of Complete Unfolding Prefixes},
year = 2007,
month = nov,
volume = 104,
number = 4,
pages = {129-136},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Chatain-Khomenko_IPL07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Chatain-Khomenko_IPL07.pdf},
doi = {10.1016/j.ipl.2007.06.002},
abstract = {Petri net unfolding prefixes are an important technique for formal
verification and synthesis of concurrent systems. In~this paper we show that
the requirement that the adequate order used for truncating a Petri net
unfolding must be well-founded is superfluous in many important cases, i.e.,
it logically follows from other requirements. We~give a complete analysis
when this is the case. These results concern the very `core' of the
unfolding theory.}
}
@misc{dots-3.1,
author = {Bollig, Benedikt and Bouyer, Patricia and Cassez, Franck and
Chatain, {\relax Th}omas and Gastin, Paul and Haddad, Serge
and Jard, Claude},
title = {Model for distributed timed systems},
howpublished = {Deliverable DOTS~3.1 (ANR-06-SETI-003)},
year = 2008,
month = sep
}
@inproceedings{ACEF-rp08,
address = {Liverpool, UK},
month = dec,
year = 2008,
volume = 223,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Halava, Vesa and Potapov, Igor},
acronym = {{RP}'08},
booktitle = {{P}roceedings of the 2nd {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'08)},
author = {Andr{\'e}, {\'E}tienne and Chatain, {\relax Th}omas and
Encrenaz, Emmanuelle and Fribourg, Laurent},
title = {An Inverse Method for Parametric Timed Automata},
pages = {29-46},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACEF-rp08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACEF-rp08.pdf},
doi = {10.1016/j.entcs.2008.12.029},
abstract = {Given a timed automaton with parametric timings, our objective
is to describe a procedure for deriving constraints on the parametric
timings in order to ensure that, for~each value of parameters satisfying
these constraints, the behaviors of the timed automata are time-abstract
equivalent. We~will exploit a reference valuation of the parameters that
is supposed to capture a characteristic proper behavior of the system.
The~method has been implemented and is illustrated on various examples of
asynchronous circuits.}
}
@inproceedings{BCHK-concur08,
address = {Toronto, Canada},
month = aug,
year = 2008,
volume = 5201,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {van Breugel, Franck and Chechik, Marsha},
acronym = {{CONCUR}'08},
booktitle = {{P}roceedings of the 19th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'08)},
author = {Baldan, Paolo and Chatain, {\relax Th}omas and Haar, Stefan and K{\"o}nig,
Barbara},
title = {Unfolding-based Diagnosis of Systems with an Evolving Topology},
pages = {203-217},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCHK-concur08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCHK-concur08.pdf},
doi = {10.1007/978-3-540-85361-9_19},
abstract = {We propose a framework for model-based diagnosis of systems with
mobility and variable topologies, modelled as graph transformation
systems. Generally speaking, model-based diagnosis is aimed at
constructing explanations of observed faulty behaviours on the basis of a
given model of the system. Since the number of possible explanations may
be huge we exploit the unfolding as a compact data structure to store
them, along the lines of previous work dealing with Petri net models.
Given a model of a system and an observation, the explanations can be
constructed by unfolding the model constrained by the observation, and
then removing incomplete explanations in a pruning phase. The theory is
formalised in a general categorical setting: constraining the system by
the observation corresponds to taking a product in the chosen category of
graph grammars, so that the correctness of the procedure can be proved by
using the fact that the unfolding is a right adjoint and thus it preserves
products. The theory thus should be easily applicable to a wide class of
system models, including graph grammars and Petri nets.}
}
@inproceedings{ACDFR-msr09,
address = {Nantes, France},
month = nov,
year = 2009,
number = {7-9},
volume = {43},
series = {Journal Europ{\'e}en des Syst{\`e}mes Automatis{\'e}s},
publisher = {Herm{\`e}s},
editor = {Lime, Didier and Roux, Olivier H.},
acronym = {{MSR}'09},
booktitle = {{A}ctes du 7{\`e}me {C}olloque sur la
{M}od{\'e}lisation des {S}yst{\`e}mes
{R}{\'e}actifs
({MSR}'09)},
author = {Andr{\'e}, {\'E}tienne and Chatain, {\relax Th}omas and
De{ }Smet, Olivier and Fribourg, Laurent and Ruel, Silvain},
title = {Synth{\`e}se de contraintes temporis{\'e}es pour
une architecture d'automatisation en r{\'e}seau},
pages = {1049-1064},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACDFR-msr09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACDFR-msr09.pdf},
abstract = {We deal with the problem of synthesis of timing constraints for
concurrent systems. Such systems are modeled by networks of timed automata
where some constants, represented as parameters, can be tuned. A suitable
value of these parameters is assumed to be known from a preliminarily
simulation process. We present a method which infers a zone of suitable
points around this reference functioning point. This zone is defined by a
system of linear inequalities over the parameters. This method is applied
to the case study of a networked automation system.}
}
@inproceedings{CDL-adhs09,
address = {Zaragoza, Spain},
month = sep,
year = 2009,
editor = {Giua, Alessandro and Silva, Manuel and Zaytoon, Janan},
acronym = {{ADHS}'09},
booktitle = {{P}roceedings of the 3rd {IFAC} {C}onference on {A}nalysis and
{D}esign of {H}ybrid {S}ystems ({ADHS}'09)},
author = {Chatain, {\relax Th}omas and David, Alexandre and Larsen, Kim
G.},
title = {Playing Games with Timed Games},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDL-adhs09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDL-adhs09.pdf},
abstract = {In this paper we focus on property-preserving preorders between
timed game automata and their application to control of partially
observable systems. Following the example of timed simulation between
timed automata, we define timed alternating simulation as a preorder
between timed game automata, which preserves controllability. We define a
method to reduce the timed alternating simulation problem to a safety
game. We show how timed alternating simulation can be used to control
efficiently a partially observable system. This method is illustrated by a
generic case study.}
}
@inproceedings{BCDL-formats09,
address = {Budapest, Hungary},
month = sep,
year = 2009,
volume = 5813,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ouaknine, Jo{\"e}l and Vaandrager, Frits},
acronym = {{FORMATS}'09},
booktitle = {{P}roceedings of the 7th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'09)},
author = {Bulychev, Peter and Chatain, {\relax Th}omas and David,
Alexandre and Larsen, Kim G.},
title = {Checking simulation relation between timed game automata},
pages = {73-87},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCDL-formats09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCDL-formats09.pdf},
doi = {10.1007/978-3-642-04368-0_8},
abstract = {In this paper we focus on property-preserving preorders between
timed game automata and their application to control of
partially observable systems. We define timed weak
alternating simulation as a preorder between timed game
automata, which preserves controllability. We define the
rules of building a symbolic turn-based two-player game such
that the existence of a winning strategy is equivalent to
the simulation being satisfied. We also propose an
on-the-fly algorithm for solving this game. This simulation
checking method can be applied to the case of
non-alternating or strong simulations as well. We illustrate
our algorithm by a case study and report on results.}
}
@article{ACEF-ijfcs09,
publisher = {World Scientific},
journal = {International Journal of Foundations of Computer Science},
author = {Andr{\'e}, {\'E}tienne and Chatain, {\relax Th}omas and
Encrenaz, Emmanuelle and Fribourg, Laurent},
title = {An Inverse Method for Parametric Timed Automata},
volume = 20,
number = 5,
pages = {819-836},
month = oct,
year = 2009,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACEF-ijfcs09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACEF-ijfcs09.pdf},
doi = {10.1142/S0129054109006905},
abstract = {We consider in this paper systems modeled by timed automata. The
timing bounds involved in the action guards and location invariants of our
timed automata are not constants, but parameters. Those parametric timed
automata allow the modelling of various kinds of timed systems,
\textit{e.g.} communication protocols or asynchronous circuits. We will
also assume that we are given an initial tuple~\(\pi_0\) of values for the
parameters, which corresponds to values for which the system is known to
behave properly. Our goal is to compute a constraint~\(K_0\) on the
parameters, satisfied by~\(\pi_0\), guaranteeing that, under any parameter
valuation satisfying~\(K_0\), the system behaves in the same manner: for any
two parameter valuations satisfying~\(K_0\), the behaviors of the timed
automata are (time-abstract) equivalent, \textit{i.e.}, the traces of execution
viewed as alternating sequences of actions and locations are identical. We
present an algorithm \texttt{InverseMethod} that terminates in the case of acyclic
models, and discuss how to extend it in the cyclic case. We also explain
how to combine our method with classical synthesis methods which are based
on the avoidance of a given set of bad states. A prototype implementation
has been done, and various experiments are described.}
}
@misc{dots-2.2,
author = {Chatain, {\relax Th}omas and Gastin, Paul and Muscholl, Anca
and Sznajder, Nathalie and Walukiewicz, Igor and
Zeitoun, Marc},
title = {Distributed control for restricted specifications},
howpublished = {Deliverable DOTS~2.2 (ANR-06-SETI-003)},
year = 2009,
month = mar
}
@inproceedings{CGS-sofsem09,
address = {\v{S}pindler\r{u}v Ml\'{y}n, Czech Republic},
month = jan,
year = 2009,
volume = 5404,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Nielsen, Mogens and Ku{\v c}era, Anton{\'\i}n and Bro
Miltersen, Peter and Palamidessi, Catuscia and T{\r{u}}ma,
Petr and Valencia, Franck},
acronym = {{SOFSEM}'09},
booktitle = {{P}roceedings of the 35th International Conference on
Current Trends in Theory and Practice of
Computer Science ({SOFSEM}'09)},
author = {Chatain, {\relax Th}omas and Gastin, Paul and Sznajder, Nathalie},
title = {Natural Specifications Yield Decidability for Distributed
Synthesis of Asynchronous Systems},
pages = {141-152},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CGS-sofsem09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CGS-sofsem09.pdf},
doi = {10.1007/978-3-540-95891-8_16},
abstract = {We study the synthesis problem in an asynchronous distributed
setting: a finite set of processes interact locally with an uncontrollable
environment and communicate with each other by sending signals---actions
that are immediately received by the target process. The synthesis problem
is to come up with a local strategy for each process such that the
resulting behaviours of the system meet a given specification. We consider
external specifications over partial orders. External means that
specifications only relate input and output actions from and to the
environment and not signals exchanged by processes. We also ask for some
closure properties of the specification. We present this new setting for
studying the distributed synthesis problem, and give decidability results:
the non-distributed case, and the subclass of networks where communication
happens through a strongly connected graph. We believe that this framework
for distributed synthesis yields decidability results for many more
architectures.}
}
@inproceedings{CJ-notere10,
address = {Tozeur, Tunisia},
month = may # {-} # jun,
year = 2010,
publisher = {{IEEE} Computer Society Press},
noeditor = {},
acronym = {{NOTERE}'10},
booktitle = {{A}ctes de la 10{\`e}me {C}onf{\'e}rence {I}nternationale sur les
{NO}uvelles {TE}chnologies de la {R\'E}partition ({NOTERE}'10)},
author = {Chatain, {\relax Th}omas and Jard, Claude},
title = {S{\'e}mantique concurrente symbolique des r{\'e}seaux
de {P}etri saufs et d{\'e}pliages finis des r{\'e}seaux
temporels},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CJ-notere10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CJ-notere10.pdf},
abstract = {On consid\`ere des r\'eseaux de Petri color\'es, \`a contraintes
lin\'eaires et pouvant poss\'eder des arcs de lecture. Sur cette classe,
on d\'efinit une s\'emantique concurrente en termes de processus d'ordre
partiel permettant de garder explicite l'ind\'ependance entre des tirs de
transitions. L'ensemble des processus peut \^etre repr\'esent\'e en
utilisant la notion de d\'epliage symbolique. Nous montrons alors comment
les r\'eseaux de Petri temporels peuvent \^etre cod\'es dans ce mod\`ele
\`a l'aide d'une transformation syntaxique pr\'eservant la concurrence.
Cette transformation permet de d\'efinir la notion de d\'epliage de
r\'eseaux de Petri temporels et d'en donner une repr\'esentation par
pr\'efixe fini.}
}
@inproceedings{BCH-time10,
address = {Paris, France},
month = sep,
year = 2010,
publisher = {{IEEE} Computer Society Press},
editor = {Markey, Nicolas and Wijsen, Jef},
acronym = {{TIME}'10},
booktitle = {{P}roceedings of the 17th {I}nternational {S}ymposium on
{T}emporal {R}epresentation and {R}easoning
({TIME}'10)},
author = {Balaguer, Sandie and Chatain, {\relax Th}omas and Haar, Stefan},
title = {A~Concurrency-Preserving Translation from Time {P}etri Nets to Networks of Timed
Automata},
pages = {77-84},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCH-time10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCH-time10.pdf},
doi = {10.1109/TIME.2010.12},
abstract = {Real-time distributed systems may be modeled in different
formalisms such as time Petri nets~(TPN) and networks of timed
automata~(NTA). This paper focuses on translating a \(1\)-bounded TPN into
an NTA and considers an equivalence which takes the distribution of
actions into account. This translation is extensible to bounded~TPNs.
We~first use \(S\)-invariants to decompose the net into components that
give the structure of the automata, then we add clocks to provide the
timing information. Although we have to use an extended syntax in the
timed automata, this is a novel approach since the other transformations
and comparisons of these models did not consider the preservation of
concurrency.}
}
@inproceedings{CF-pn10,
address = {Braga, Portugal},
month = jun,
year = 2010,
volume = 6128,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Lilius, Johan and Penczek, Wojciech},
acronym = {{PETRI~NETS}'10},
booktitle = {{P}roceedings of the 31st
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({PETRI~NETS}'10)},
author = {Chatain, {\relax Th}omas and Fabre, {\'E}ric},
title = {Factorization Properties of Symbolic Unfoldings of Colored
{P}etri Nets},
pages = {165-184},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CF-pn10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CF-pn10.pdf},
doi = {10.1007/978-3-642-13675-7_11},
abstract = {The unfolding technique is an efficient tool to explore the runs
of a Petri net in a true concurrency semantics, \textit{i.e.}, without
constructing all the interleavings of concurrent actions. But even small
real systems are never modeled directly as ordinary Petri nets: they use
many high-level features that were designed as extensions of Petri nets.
We focus here on two such features: colors and compositionality. We show
that the symbolic unfolding of a product of colored Petri nets can be
expressed as the product of the symbolic unfoldings of these nets. This is
a necessary result in view of distributed computations based on symbolic
unfoldings, as they have been developed already for standard unfoldings,
to design modular verification techniques, or modular diagnosis
procedures, for example. The factorization property of symbolic unfoldings
is valid for several classes of colored or high-level nets. We derive it
here for a class of (high-level) open nets, for which the composition is
performed by connecting places rather than transitions.}
}
@incollection{DBBetal-CES09,
author = {David, Alexandre and Behrmann, Gerd and Bulychev, Peter and
Byg, Joakin and Chatain, {\relax Th}omas and Larsen, Kim G.
and
Pettersson, Paul and Rasmussen, Jacob Illum and
Srba, Ji{\v{r}}{\'\i} and
Yi, Wang and Joergensen, Kenneth Y. and Lime, Didier and
Magnin, Morgan and Roux, Olivier H. and Traonouez, Louis-Marie},
title = {Tools for Model-Checking Timed Systems},
booktitle = {Communicating Embedded Systems~-- Software and Design},
editor = {Jard, Claude and Roux, Olivier H.},
publisher = {Wiley-ISTE},
year = 2009,
month = oct,
pages = {165-225},
chapter = 6,
url = {http://www.iste.co.uk/index.php?f=x&ACTION=View&id=288},
nops = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/.ps},
nopsgz = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PSGZ/.ps.gz},
isbn = {9781848211438}
}
@article{BCHK-icomp10,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Baldan, Paolo and Chatain, {\relax Th}omas and Haar, Stefan and
K{\"o}nig, Barbara},
title = {Unfolding-based Diagnosis of Systems with an Evolving Topology},
volume = 208,
number = 10,
pages = {1169-1192},
year = 2010,
month = oct,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCHK-icomp10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCHK-icomp10.pdf},
doi = {10.1016/j.ic.2009.11.009},
abstract = {We propose a framework for model-based diagnosis of systems with
mobility and variable topologies, modelled as graph transformation
systems. Generally speaking, model-based diagnosis is aimed at
constructing explanations of observed faulty behaviours on the basis of a
given model of the system. Since the number of possible explanations may
be huge, we exploit the unfolding as a compact data structure to store
them, along the lines of previous work dealing with Petri net models.
Given a model of a system and an observation, the explanations can be
constructed by unfolding the model constrained by the observation, and
then removing incomplete explanations in a pruning phase. The theory is
formalised in a general categorical setting: constraining the system by
the observation corresponds to taking a product in the chosen category of
graph grammars, so that the correctness of the procedure can be proved by
using the fact that the unfolding is a right adjoint and thus it preserves
products. The theory should hence be easily applicable to a wide class of
system models, including graph grammars and Petri nets.}
}
@inproceedings{BCH-acsd11,
address = {Newcastle upon Tyne, UK},
month = jun,
year = 2011,
publisher = {{IEEE} Computer Society Press},
editor = {Caillaud, Beno{\^\i}t and Carmona, Josep},
acronym = {{ACSD}'11},
booktitle = {{P}roceedings of the 11th {I}nternational
{C}onference on {A}pplication of {C}oncurrency
to {S}ystem {D}esign
({ACSD}'11)},
author = {Balaguer, Sandie and Chatain, {\relax Th}omas and Haar, Stefan},
title = {Building Tight Occurrence Nets from Reveals Relations},
pages = {44-53},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCH-acsd11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCH-acsd11.pdf},
doi = {10.1109/ACSD.2011.16},
abstract = {Occurrence nets are a well known partial order model for the
concurrent behavior of Petri nets. The causality and conflict relations
between events, which are explicitly represented in occurrence nets,
induce logical dependencies between event occurrences: the occurrence of
an event~\(e\) in a run implies that all its causal predecessors also
occur, and that no event in conflict with \(e\) occurs. But these
structural relations do not express all the logical dependencies between
event occurrences in maximal runs: in particular, the occurrence of~\(e\)
in any maximal run may imply the occurrence of another event that is not a
causal predecessor of~\(e\), in that run. The \emph{reveals} relation has
been introduced in~[Haar, IEEE TAC 55(10):2310-2320, 2010] to express this
dependency between two events. Here we generalize the reveals relation to
express more general dependencies, involving more than two events, and we
introduce ERL logic to express them as boolean formulas. Finally we answer
the synthesis problem that arises: given an ERL formula~\(\varphi\), is
there an occurrence net~\(\mathcal{N}\) such that \(\varphi\) describes
exactly the dependencies between the events of~\(\mathcal{N}\)?}
}
@article{BCH-fi12,
publisher = {{IOS} Press},
journal = {Fundamenta Informaticae},
author = {Balaguer, Sandie and Chatain, {\relax Th}omas and Haar, Stefan},
title = {Building Occurrence Nets from Reveals Relations},
year = 2013,
month = may,
volume = 123,
number = 3,
pages = {245-272},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCH-fi12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCH-fi12.pdf},
doi = {10.3233/FI-2013-809},
abstract = {Occurrence nets are a well known partial order model for the
concurrent behavior of Petri nets. The causality and conflict relations
between events, which are explicitly represented in occurrence nets,
induce logical dependencies between event occurrences: the occurrence of
an event~\(e\) in a run implies that all its causal predecessors also
occur, and that no event in conflict with~\(e\) occurs. But these
structural relations do not express all the logical dependencies between
event occurrences in maximal runs: in particular, the occurrence of~\(e\)
in any maximal run may imply the occurrence of another event that is not a
causal predecessor of~\(e\), in that run. The \emph{reveals} relation has
been introduced to express this dependency between two events. Here we
generalize the reveals relation to express more general dependencies,
involving more than two events, and we introduce ERL logic to express them
as boolean formulas. Finally we answer the synthesis problem that arises:
given an ERL formula~\(\varphi\), is there an occurrence
net~\(\mathcal{N}\) such that \(\varphi\)~describes exactly the
dependencies between the events of~\(\mathcal{N}\)?}
}
@misc{impro-D4.1,
author = {Balaguer, Sandie and Chatain, {\relax Th}omas and Haar, Stefan},
title = {Concurrent semantics for timed distributed systems},
howpublished = {Deliverable ImpRo D~4.1 (ANR-2010-BLAN-0317)},
year = 2012,
month = mar,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d41.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d41.pdf}
}
@inproceedings{BC-concur12,
address = {Newcastle, UK},
month = sep,
year = 2012,
volume = 7454,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Koutny, Maciej and Ulidowski, Irek},
acronym = {{CONCUR}'12},
booktitle = {{P}roceedings of the 23rd
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'12)},
author = {Balaguer, Sandie and Chatain, {\relax Th}omas},
title = {Avoiding Shared Clocks in Networks of Timed Automata},
pages = {100-114},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BC-concur12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BC-concur12.pdf},
doi = {10.1007/978-3-642-32940-1_9},
abstract = {Networks of timed automata~(NTA) are widely used to model
distributed real-time systems. Quite often in the literature, the automata
are allowed to share clocks. This is a problem when one considers
implementing such model in a distributed architecture, since reading
clocks a priori requires communications which are not explicitly described
in the model. We focus on the following question: given a NTA \(A_{1}
\parallel A_{2}\) where \(A_{2}\) reads some clocks reset by~\(A_{1}\),
does there exist a NTA \(A'_{1} \parallel A'_{2}\) without shared clocks
with the same behavior as the initial NTA? For this, we allow the automata
to exchange information during synchronizations only. We discuss a
formalization of the problem and give a criterion using the notion of
contextual timed transition system, which represents the behavior
of~\(A_{2}\) when in parallel with~\(A_{1}\). Finally, we effectively
build \(A'_{1} \parallel A'_{2}\) when it exists.}
}
@article{BCH-fmsd12,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Balaguer, Sandie and Chatain, {\relax Th}omas and Haar,
Stefan},
title = {A~Concurrency-Preserving Translation from Time {P}etri Nets to
Networks of Timed Automata},
year = 2012,
month = jun,
volume = 40,
number = 3,
pages = {330-355},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCH-fmsd12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCH-fmsd12.pdf},
doi = {10.1007/s10703-012-0146-4},
abstract = {Several formalisms to model distributed real-time systems
coexist in the literature. This naturally induces a need to compare their
expressiveness and to translate models from one formalism to another when
possible. The first formal comparisons of the expressiveness of these
models focused on the preservation of the sequential behavior of the
models, using notions like timed language equivalence or timed
bisimilarity. They do not consider preservation of concurrency. In~this
paper we define timed traces as a partial order representation of
executions of our models for real-time distributed systems. Timed traces
provide an alternative to timed words, and take the distribution of
actions into account. We propose a translation between two popular
formalisms that describe timed concurrent systems: \(1\)-bounded time Petri
nets~(TPN) and networks of timed automata~(NTA). Our translation preserves
the distribution of actions, that is we require that if the TPN represents
the product of several components (called processes), then each process
should have its counterpart as one timed automaton in the resulting~NTA.}
}
@phdthesis{chatain-HDR13,
author = {Chatain, {\relax Th}omas},
title = {Concurrency in Real-Time Distributed Systems, from Unfoldings
to Implementability},
year = 2013,
month = dec,
type = {M{\'e}moire d'habilitation},
school = {{\'E}cole Normale Sup{\'e}rieure de Cachan, France},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/hdr-chatain13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/hdr-chatain13.pdf}
}
@article{BC-lmcs13,
journal = {Logical Methods in Computer Science},
author = {Balaguer, Sandie and Chatain, {\relax Th}omas},
title = {Avoiding Shared Clocks in Networks of Timed Automata},
volume = 9,
number = {4:13},
nopages = {},
year = 2013,
month = nov,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BC-lmcs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BC-lmcs13.pdf},
doi = {10.2168/LMCS-9(4:13)2013},
abstract = {Networks of timed automata~(NTA) are widely used to model
distributed real-time systems. Quite often in the literature, the automata
are allowed to share clocks. This is a problem when one considers
implementing such model in a distributed architecture, since reading
clocks a priori requires communications which are not explicitly described
in the model. We focus on the following question: given a NTA \(A_{1}
\parallel A_{2}\) where \(A_{2}\) reads some clocks reset by~\(A_{1}\),
does there exist a NTA \(A'_{1} \parallel A'_{2}\) without shared clocks
with the same behavior as the initial NTA? For this, we allow the automata
to exchange information during synchronizations only. We discuss a
formalization of the problem and give a criterion using the notion of
contextual timed transition system, which represents the behavior
of~\(A_{2}\) when in parallel with~\(A_{1}\). Finally, we effectively
build \(A'_{1} \parallel A'_{2}\) when it exists.}
}
@inproceedings{CH-pnse13,
address = {Milano, Italy},
month = jun,
year = 2013,
volume = 969,
series = {CEUR Workshop Proceedings},
publisher = {RWTH Aachen, Germany},
editor = {Moldt, Daniel and R{\"o}lke, Heiko},
acronym = {{PNSE}'13},
booktitle = {{P}roceedings of the 7th {I}nternational {W}orkshop on {P}etri
{N}ets and {S}oftware {E}ngineering ({PNSE}'13)},
author = {Chatain, {\relax Th}omas and Haar, Stefan},
title = {A~Canonical Contraction for Safe {P}etri Nets},
pages = {25-39},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CH-pnse13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CH-pnse13.pdf},
abstract = {Under maximal semantics, the occurrence of an event~\(a\) in a
concurrent run of an occurrence net may imply the occurrence of other
events, not causally related to~\(a\), in the same run. In recent works, we
have formalized this phenomenon as the \emph{reveals} relation, and used
it to obtain a contraction of sets of events called \emph{facets} in the
context of occurrence nets. Here, we extend this idea to propose a
canonical contraction of general safe Petri nets into pieces of
partial-order behaviour which can be seen as {"}macro-transitions{"} since
all their events must occur together in maximal semantics. On occurrence
nets, our construction coincides with the facets abstraction. Our
contraction preserves the maximal semantics in the sense that the maximal
processes of the contracted net are in bijection with those of the
original net.}
}
@inproceedings{CJ-formats13,
address = {Buenos Aires, Argentina},
month = aug,
year = 2013,
volume = 8053,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Braberman, V{\'\i}ctor and Fribourg, Laurent},
acronym = {{FORMATS}'13},
booktitle = {{P}roceedings of the 11th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'13)},
author = {Chatain, {\relax Th}omas and Jard, Claude},
title = {Back in Time {P}etri Nets},
pages = {91-105},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CJ-formats13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CJ-formats13.pdf},
doi = {10.1007/978-3-642-40229-6_7},
abstract = {The time progress assumption is at the core of the semantics of
real-time formalisms. It is also the major obstacle to the development of
partial-order techniques for real-time distributed systems since the
events are ordered both by causality and by their occurrence in time.
Anyway, extended free choice safe time Petri nets (TPNs) were already
identified as a class where partial order semantics behaves well. We show
that, for this class, the time progress assumption can even be dropped
(time may go back in case of concurrency), which establishes a nice
relation between partial-order semantics and time progress assumption.}
}
@incollection{topnoc14-CH,
year = 2014,
volume = {8910},
series = {Lecture Notes in Computer Science},
editor = {Koutny, Maciej and Haddad, Serge and Yakovlev, Alex},
publisher = {Springer},
booktitle = {Transactions on {P}etri Nets and Other Models of Concurrency~{IX}},
author = {Chatain, {\relax Th}omas and Haar, Stefan},
title = {A Canonical Contraction for Safe {P}etri Nets},
pages = {83-98},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/topnoc14-CH.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/topnoc14-CH.pdf},
doi = {10.1007/978-3-662-45730-6_5},
abstract = {Under maximal semantics, the occurrence of an event~\(a\) in a
concurrent run of an occurrence net may imply the occurrence of other
events, not causally related to~\(a\), in the same run. In recent works,
we have formalized this phenomenon as the reveals relation, and used it to
obtain a contraction of sets of events called facets in the context of
occurrence nets. Here, we extend this idea to propose a canonical
contraction of general safe Petri nets into pieces of partial-order
behaviour which can be seen as {"}macro-transitions{"} since all their
events must occur together in maximal semantics. On occurrence nets, our
construction coincides with the facets abstraction. Our contraction
preserves the maximal semantics in the sense that the maximal processes of
the contracted net are in bijection with those of the original net.}
}
@inproceedings{CHJPS-cmsb14,
address = {Manchester, UK},
month = nov,
year = 2014,
volume = {8859},
series = {Lecture Notes in Bioinformatics},
publisher = {Springer-Verlag},
editor = {Mendes, Pedro},
acronym = {{CMSB}'14},
booktitle = {{P}roceedings of the 12th
{C}onference on
{C}omputational {M}ethods in {S}ystem {B}iology
({CMSB}'14)},
author = {Chatain, {\relax Th}omas and Haar, Stefan and Jezequel,
Lo{\"\i}g and Paulev{\'e}, Lo{\"\i}c and Schwoon, Stefan},
title = {Characterization of Reachable Attractors Using {P}etri Net
Unfoldings},
pages = {129-142},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CHJPS-cmsb14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CHJPS-cmsb14.pdf},
doi = {10.1007/978-3-319-12982-2_10},
abstract = {Attractors of network dynamics represent the long-term
behaviours of the modelled system. Their characterization is therefore
crucial for understanding the response and differentiation capabilities of
a dynamical system. In the scope of qualitative models of interaction
networks, the computation of attractors reachable from a given state of
the network faces combinatorial issues due to the state space explosion.
In this paper, we present a new algorithm that exploits the concurrency
between transitions of parallel acting components in order to reduce the
search space. The algorithm relies on Petri net unfoldings that can be
used to compute a compact representation of the dynamics. We illustrate
the applicability of the algorithm with Petri net models of cell
signalling and regulation networks, Boolean and multi-valued. The proposed
approach aims at being complementary to existing methods for deriving the
attractors of Boolean models, while being generic since they apply to any
safe Petri net.}
}
@inproceedings{ACR-acsd15,
address = {Brussels, Belgium},
month = jun,
year = 2015,
publisher = {{IEEE} Computer Society Press},
editor = {Haar, Stefan and Meyer, Roland},
acronym = {{ACSD}'15},
booktitle = {{P}roceedings of the 15th {I}nternational
{C}onference on {A}pplication of {C}oncurrency
to {S}ystem {D}esign
({ACSD}'15)},
author = {Andr{\'e}, {\'E}tienne and Chatain, {\relax Th}omas and
Rodr{\'\i}guez, C{\'e}sar},
title = {Preserving Partial Order Runs in Parametric Time {P}etri Nets},
pages = {120-129},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ACR-acsd15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ACR-acsd15.pdf},
doi = {10.1109/ACSD.2015.16},
abstract = {Parameter synthesis for timed systems aims at deriving parameter
valuations satisfying a given property. In this paper we target concurrent
systems; it is well known that concurrency is a source of state-space
explosion, and partial order techniques were defined to cope with this
problem. Here we use partial order semantics for parametric time Petri
nets as a way to significantly enhance the result of an existing synthesis
algorithm. Given a reference parameter valuation, our approach synthesizes
other valuations preserving, up to interleaving, the behavior of the
reference parameter valuation. We show the applicability of our approach
using acyclic asynchronous circuits.}
}
@inproceedings{CHKS-pn15,
address = {Brussels, Belgium},
month = jun,
year = 2015,
volume = {9115},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Devillers, Raymond and Valmari, Antti},
acronym = {{PETRI~NETS}'15},
booktitle = {{P}roceedings of the 36th
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({PETRI~NETS}'15)},
author = {Chatain, {\relax Th}omas and Haar, Stefan and Koutny,
Maciej and Schwoon, Stefan},
title = {Non-Atomic Transition Firing in Contextual Nets},
pages = {117-136},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CHKS-pn15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CHKS-pn15.pdf},
doi = {10.1007/978-3-319-19488-2_6},
abstract = {The firing rule for Petri nets assumes instantaneous and
simultaneous consumption and creation of tokens. In the context of
ordinary Petri nets, this poses no particular problem because of the
system's asynchronicity, even if token creation occurs later than token
consumption in the firing. With read arcs, the situation changes, and
several different choices of semantics are possible. The step semantics
introduced by Janicki and Koutny can be seen as imposing a two-phase
firing scheme: first, the presence of the required tokens is checked, then
consumption and production of tokens happens. Pursuing this approach
further, we develop a more general framework based on explicitly splitting
the phases of firing, allowing to synthesize coherent steps. This turns
out to define a more general non-atomic semantics, which has important
potential for safety as it allows to detect errors that were missed by the
previous semantics. Then we study the characterization of partial-order
processes feasible under one or the other semantics.}
}
@inproceedings{vDCC-EMISA16,
address = {Vienna, Austria},
month = oct,
publisher = {{CEUR-WS.org}},
volume = {1701},
series = {{CEUR} Workshop Proceedings},
editor = {Rinderle-Ma, Stefanie and Mendling, Jan},
acronym = {{EMISA}'16},
booktitle = {{P}roceedings of the 7th {I}nt. {W}orkshop on {E}nterprise {M}odelling and {I}nformation {S}ystems {A}rchitectures
({EMISA}'16)},
author = {van Dongen, Boudewijn and Carmona, Josep and Chatain, {\relax Th}omas},
title = {{Alignment-based Quality Metrics in Conformance Checking}},
pages = {87-90},
year = {2016},
doi = {},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/vanDongen-EMISA16.pdf},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/vanDongen-EMISA16.pdf},
abstract = {The holy grail in process mining is a process discovery algorithm that, given an event
log, produces fitting, precise, properly generalizing and simple process models. Within the field of
process mining, conformance checking is considered to be anything where observed behaviour, e.g.,
in the form of event logs or event streams, needs to be related to already modelled behaviour.
In the conformance checking domain, the relation between an event log and a model is typically
quantified using fitness, precision and generalization. In this paper, we present metrics for fitness,
precision and generalization, based on alignments and the newer concept named anti-alignments.}
}
@inproceedings{CC-pn16,
address = {Tor{\'u}n, Poland},
month = jun,
year = 2016,
volume = {9698},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Kordon, Fabrice and Moldt, Daniel},
acronym = {{PETRI~NETS}'16},
booktitle = {{P}roceedings of the 37th
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({PETRI~NETS}'16)},
author = {Carmona, Josep and Chatain, {\relax Th}omas},
title = {Anti-Alignments in Conformance Checking~-- The~Dark Side of Process Models},
pages = {240-258},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CC-pn16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CC-pn16.pdf},
doi = {10.1007/978-3-319-39086-4_15},
abstract = {Conformance checking techniques asses the suitability of a
process model in representing an underlying process, observed
through a collection of real executions. These techniques suffer
from the well-known state space explosion problem, hence handling
process models exhibiting large or even infinite state spaces
remains a challenge. One important metric in conformance checking is
to asses the precision of the model with respect to the observed
executions, i.e., characterize the ability of the model to produce
behavior unrelated to the one observed. By~avoiding the computation
of the full state space of a model, current techniques only provide
estimations of the precision metric, which in some situations tend
to be very optimistic, thus hiding real problems a process model may
have. In this paper we present the notion of anti-alignment as a
concept to help unveiling traces in the model that may deviate
significantly from the observed behavior. Using anti-alignments,
current estimations can be improved, e.g., in precision checking. We
show how to express the problem of finding anti-alignments as the
satisfiability of a Boolean formula, and provide a tool which can
deal with large models efficiently.}
}
@comment{{B-arxiv16,
author = Bollig, Benedikt,
affiliation = aff-LSVmexico,
title = One-Counter Automata with Counter Visibility,
institution = Computing Research Repository,
number = 1602.05940,
month = feb,
nmonth = 2,
year = 2016,
type = RR,
axeLSV = mexico,
NOcontrat = "",
url = http://arxiv.org/abs/1602.05940,
PDF = "http://www.lsv.fr/Publis/PAPERS/PDF/B-arxiv16.pdf",
lsvdate-new = 20160222,
lsvdate-upd = 20160222,
lsvdate-pub = 20160222,
lsv-category = "rapl",
wwwpublic = "public and ccsb",
note = 18~pages,
abstract = "In a one-counter automaton (OCA), one can read a letter
from some finite alphabet, increment and decrement the counter by
one, or test it for zero. It is well-known that universality and
language inclusion for OCAs are undecidable. We consider here OCAs
with counter visibility: Whenever the automaton produces a letter,
it outputs the current counter value along with~it. Hence, its
language is now a set of words over an infinite alphabet. We show
that universality and inclusion for that model are in PSPACE, thus
no harder than the corresponding problems for finite automata, which
can actually be considered as a special case. In fact, we show that
OCAs with counter visibility are effectively determinizable and
closed under all boolean operations. As~a~strict generalization, we
subsequently extend our model by registers. The general nonemptiness
problem being undecidable, we impose a bound on the number of
register comparisons and show that the corresponding nonemptiness
problem is NP-complete.",
}}
@inproceedings{CCV-er17,
address = {Valencia, Spain},
month = nov,
volume = 10650,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Mayr, Heinrich C. and Guizzardi, Giancarlo and Ma, Hui and Pastor, Oscar},
booktitle = {{P}roceedings of the 36th {I}nternational {C}onference on {C}onceptual {M}odeling ({ER}'17)},
author = {Chatain, {\relax Th}omas and Carmona, Josep and van Dongen, Boudewijn},
title = {Alignment-Based Trace Clustering},
pages = {295-308},
year = {2017},
doi = {10.1007/978-3-319-69904-2_24},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CCV-er17.pdf},
url = {https://doi.org/10.1007/978-3-319-69904-2_24},
abstract = {A novel method to cluster event log traces is presented in this paper. In contrast to the approaches in the literature, the clustering approach of this paper assumes an additional input: a process model that describes the current process. The core idea of the algorithm is to use model traces as centroids of the clusters detected, computed from a generalization of the notion of alignment. This way, model explanations of observed behavior are the driving force to compute the clusters, instead of current model agnostic approaches, e.g., which group log traces merely on their vector-space similarity. We believe alignment-based trace clustering provides results more useful for stakeholders. Moreover, in case of log incompleteness, noisy logs or concept drift, they can be more robust for dealing with highly deviating traces. The technique of this paper can be combined with any clustering technique to provide model explanations to the clusters computed. The proposed technique relies on encoding the individual alignment problems into the (pseudo-)Boolean domain, and has been implemented in our tool DarkSider that uses an open-source solver.},
note = {To appear}
}
@inproceedings{CP-concur17,
address = {Berlin, Germany},
month = sep,
year = 2017,
volume = {85},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Meyer, Roland and Nestmann, Uwe},
acronym = {{CONCUR}'17},
booktitle = {{P}roceedings of the 28th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'17)},
author = {Chatain, {\relax Th}omas and Paulev{\'e}, Lo{\"i}c},
title = {Goal-Driven Unfolding of {P}etri Nets},
pages = {18:1-18:16},
url = {http://drops.dagstuhl.de/opus/volltexte/2017/7773},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2017/7773/pdf/LIPIcs-CONCUR-2017-18.pdf},
doi = {10.4230/LIPIcs.CONCUR.2017.18},
abstract = {Unfoldings provide an efficient way to avoid the state-space explosion due to interleavings of concurrent transitions when exploring the runs of a Petri net. The theory of adequate orders allows one to define finite prefixes of unfoldings which contain all the reachable markings. In this paper we are interested in reachability of a single given marking, called the goal. We propose an algorithm for computing a finite prefix of the unfolding of a 1-safe Petri net that preserves all minimal configurations reaching this goal. Our algorithm combines the unfolding technique with on-the-fly model reduction by static analysis aiming at avoiding the exploration of branches which are not needed for reaching the goal. We present some experimental results.}
}
@inproceedings{VCCT-caise17,
address = {Essen, Germany},
month = jun,
volume = 10253,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Dubois, Eric and Pohl, Klaus},
acronym = {{CAiSE}'17},
booktitle = {{P}roceedings of the 29th {I}nternational {C}onference on {A}dvanced {I}nformation {S}ystems {E}ngineering ({CAiSE}'17)},
author = {{van Dongen}, Boudewijn and Carmona, Josep and Chatain, {\relax Th}omas and Taymouri, Farbod},
title = {Aligning Modeled and Observed Behavior: A Compromise Between Complexity and Quality},
pages = {94-109},
year = {2017},
doi = {10.1007/978-3-319-59536-8_7},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/VCCT-caise17.pdf},
abstract = {Certifying that a process model is aligned with the real process executions is perhaps the most desired feature a process model may have: aligned process models are crucial for organizations, since strategic decisions can be made easier on models instead of on plain data. In spite of its importance, the current algorithmic support for computing alignments is limited: either techniques that explicitly explore the model behavior (which may be worst-case exponential with respect to the model size), or heuristic approaches that cannot guarantee a solution, are the only alternatives. In this paper we propose a solution that sits right in the middle in the complexity spectrum of alignment techniques; it can always guarantee a solution, whose quality depends on the exploration depth used and local decisions taken at each step. We use linear algebraic techniques in combination with an iterative search which focuses on progressing towards a solution. The experiments show a clear reduction in the time required for reaching a solution, without sacrificing significantly the quality of the alignment obtained.}
}
@article{ACR-tecs17,
publisher = {ACM Press},
journal = {ACM Transactions in Embedded Computing Systems},
author = {Andr{\'e}, {\'E}tienne and Chatain, {\relax Th}omas and Rodr{\'\i}guez, C{\'e}sar},
title = {Preserving Partial-Order Runs in Parametric Time {P}etri Nets},
volume = {16},
number = {2},
year = {2017},
pages = {43:1-43:26},
doi = {10.1145/3012283},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ACR-tecs17.pdf},
abstract = {Parameter synthesis for timed systems aims at deriving parameter valuations satisfying a given property. In this article, we target concurrent systems. We use partial-order semantics for parametric time Petri nets as a way to both cope with the well-known state-space explosion due to concurrency and significantly enhance the result of an existing synthesis algorithm. Given a reference parameter valuation, our approach synthesizes other valuations preserving the partial-order executions of the reference parameter valuation. We show the applicability of our approach using a tool applied to asynchronous circuits.}
}
@techreport{CHKTP-hal18,
author = {Chatain, {\relax Th}omas and Haar, Stefan and Kolc{\'a}k, Juraj and Thakkar, Aalok and Paulev{\'e}, Lo{\"i}c},
institution = {HAL},
month = oct,
note = {33~pages},
number = {hal-01893106},
type = {Research Report},
title = {{Concurrency in Boolean networks}},
year = {2018},
url = {https://hal.inria.fr/hal-01893106},
pdf = {https://hal.inria.fr/hal-01893106/document},
abstract = {Boolean networks (BNs) are widely used to model the qualitative dynamics of biological systems. Besides the logical rules determining the evolution of each component with respect to the state of its regulators, the scheduling of components updates can have a dramatic impact on the predicted behaviours. In this paper, we explore the use of Contextual Petri Nets (CPNs) to study dynamics of BNs with a concurrency theory perspective. After showing bi-directional translations between CPNs and BNs and analogies between results on synchronism sensitivies, we illustrate that usual updating modes for BNs can miss plausible behaviours, i.e., incorrectly conclude on the absence/impossibility of reaching specific configurations. Taking advantage of CPN semantics enabling more behaviour than the generalized asynchronous updating mode, we propose an encoding of BNs ensuring a correct abstraction of any multivalued refinement, as one may expect to achieve when modelling biological systems with no assumption on its time features.}
}
@techreport{CHP-arxiv18,
author = {Chatain, {\relax Th}omas and Haar, Stefan and Paulev{\'e}, Lo{\"i}c},
institution = {Computing Research Repository},
month = aug,
note = {15~pages},
number = {1808.10240},
type = {Research Report},
title = {Most Permissive Semantics of Boolean Networks},
year = {2018},
url = {https://arxiv.org/abs/1808.10240},
pdf = {https://arxiv.org/pdf/1808.10240v1.pdf},
abstract = {As shown in [3], the usual update modes of
Boolean networks (BNs), including synchronous and (generalized)
asynchronous, fail to capture behaviours introduced by multivalued
refinements. Thus, update modes do not allow a correct abstract
reasoning on dynamics of biological systems, as they may lead to reject
valid BN models.\par
We introduce a new semantics for interpreting BNs which meets with a
correct abstraction of any multivalued refinements, with any update
mode. This semantics subsumes all the usual updating modes, while
enabling new behaviours achievable by more concrete models. Moreover, it
appears that classical dynamical analyses of reachability and
attractors have a simpler computational complexity:
\begin{itemize}
\item reachability can be assessed in a polynomial number of iterations
(instead of being PSPACE-complete with update modes);
\item attractors are hypercubes, and deciding the existence of attractors
with a given upper-bounded dimension is in NP (instead of
PSPACE-complete with update modes).
\end{itemize}
The computation of iterations is in NP in the very general case, and is
linear when local functions are monotonic, or with some usual
representations of functions of BNs (binary decision diagrams, Petri
nets, automata networks, etc.).\par
In brief, the most permissive semantics of BNs enables a correct
abstract reasoning on dynamics of BNs, with a greater tractability than
previously introduced update modes.\par
This technical report lists the main
definitions and properties of the most permissive semantics of BNs, and
draw some remaining open questions.}
}
@inproceedings{CHP-automata18,
address = {Ghent, Belgium},
month = jun,
year = 2018,
volume = 10875,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Jan Baetens and Martin Kutrib},
acronym = {{AUTOMATA}'18},
booktitle = {{P}roceedings of the 24th Annual International Workshop on Cellular Automata and Discrete Complex Systems ({AUTOMATA}'18)},
author = {Chatain, {\relax Th}omas and Haar, Stefan and Paulev{\'e}, Lo{\"i}c},
title = {{Boolean Networks: Beyond Generalized Asynchronicity}},
pages = {29-42},
url = {https://hal.inria.fr/hal-01768359v2},
doi = {10.1007/978-3-319-92675-9\_3},
abstract = {Boolean networks are commonly used in systems biology to model dynamics of biochemical networks by abstracting away many (and often unknown) parameters related to speed and species activity thresholds. It is then expected that Boolean networks produce an over-approximation of behaviours (reachable configurations), and that subsequent refinements would only prune some impossible transitions. However, we show that even generalized asynchronous updating of Boolean networks, which subsumes the usual updating modes including synchronous and fully asynchronous, does not capture all transitions doable in a multi-valued or timed refinement. We define a structural model transformation which takes a Boolean network as input and outputs a new Boolean network whose asynchronous updating simulates both synchronous and asynchronous updating of the original network, and exhibits even more behaviours than the generalized asynchronous updating. We argue that these new behaviours should not be ignored when analyzing Boolean networks, unless some knowledge about the characteristics of the system explicitly allows one to restrict its behaviour.}
}
@inproceedings{CCDJR-lata18,
address = {Bar-Ilan, Israel},
month = apr,
year = 2018,
volume = {10792},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Mart{\'\i}n-Vide, Carlos},
acronym = {{LATA}'18},
booktitle = {{P}roceedings of the 12th {I}nternational {C}onference on {L}anguage
and {A}utomata {T}heory and {A}pplications ({LATA}'18)},
author = {Chatain, {\relax Th}omas and Comlan, Maurice and Delfieu, David and Jezequel, Lo{\"i}g and Roux, Olivier H.},
title = {Pomsets and Unfolding of Reset Petri Nets},
pages = {258-270},
url = {https://doi.org/10.1007/978-3-319-77313-1_20},
doi = {10.1007/978-3-319-77313-1_20},
abstract = {Reset Petri nets are a particular class of Petri nets where transition firings can remove all tokens from a place without checking if this place actually holds tokens or not. In this paper we look at partial order semantics of such nets. In particular, we propose a pomset bisimulation for comparing their concurrent behaviours. Building on this pomset bisimulation we then propose a generalization of the standard finite complete prefixes of unfolding to the class of safe reset Petri nets.}
}
@article{CHKPT-nc19,
publisher = {Springer},
journal = {Natural Computing},
author = {Chatain, {\relax Th}omas and Haar, Stefan and Kolc{\'a}k, Juraj and Paulev{\'e}, Lo{\"i}c and Thakkar, Aalok},
title = {Concurrency in {Boolean} networks},
volume = {19},
pages = {91--109},
year = 2020,
pdf = {https://hal.inria.fr/hal-01893106v2/document},
url = {https://link.springer.com/article/10.1007/s11047-019-09748-4},
abstract = {Boolean networks (BNs) are widely used to model the qualitative dynamics
of biological systems. Besides the logical rules determining the evolution of each
component with respect to the state of its regulators, the scheduling of component
updates can have a dramatic impact on the predicted behaviours. In this paper, we
explore the use of Read (contextual) Petri Nets (RPNs) to study dynamics of BNs from
a concurrency theory perspective. After showing bi-directional translations between
RPNs and BNs and analogies between results on synchronism sensitivity, we illustrate
that usual updating modes for BNs can miss plausible behaviours, i.e., incorrectly
conclude on the absence/impossibility of reaching specific configurations. We propose
an encoding of BNs capitalizing on the RPN semantics enabling more behaviour than the
generalized asynchronous updating mode. The proposed encoding ensures a correct
abstraction of any multivalued refinement, as one may expect to achieve when modelling
biological systems with no assumption on its time features.}
}
@inproceedings{BCC-atpn19,
address = {Aachen, Germany},
month = jun,
year = 2019,
volume = {11522},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Susanna Donatelli and Stefan Haar},
acronym = {{PETRI~NETS}'19},
booktitle = {{P}roceedings of the 40th
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({PETRI~NETS}'19)},
author = {Mathilde Boltenhagen and Thomas Chatain and Josep Carmona},
title = {Generalized Alignment-Based Trace Clustering of Process Behavior},
pages = {237-257},
url = {https://link.springer.com/chapter/10.1007/978-3-030-21571-2_14},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCC-atpn19.pdf},
doi = {10.1007/978-3-030-21571-2_14},
abstract = {Process mining techniques use event logs containing real process executions in order to mine, align and extend process models. The partition of an event log into trace variants facilitates the understanding and analysis of traces, so it is a common pre-processing in process mining environments. Trace clustering automates this partition; traditionally it has been applied without taking into consideration the availability of a process model. In this paper we extend our previous work on process model based trace clustering, by allowing cluster centroids to have a complex structure, that can range from a partial order, down to a subnet of the initial process model. This way, the new clustering framework presented in this paper is able to cluster together traces that are distant only due to concurrency or loop constructs in process models. We show the complexity analysis of the different instantiations of the trace clustering framework, and have implemented it in a prototype tool that has been tested on different datasets.}
}
@article{BCC-is20,
publisher = {Elsevier Science Publishers},
journal = {Information Systems},
author = {Mathilde Boltenhagen and Thomas Chatain and Josep Carmona},
title = {Model-based trace variant analysis of event logs},
year = 2020,
doi = {https://doi.org/10.1016/j.is.2020.101675},
url = {https://www.sciencedirect.com/science/article/abs/pii/S0306437920301307?via%3Dihub},
note = {To appear}
}
@article{BCC-comp21,
publisher = {Springer},
journal = {Computing},
author = {Mathilde Boltenhagen and Thomas Chatain and Josep Carmona},
title = {Optimized {SAT} encoding of conformance checking artefacts},
volume = {103},
number = {1},
pages = {29-50},
year = 2021,
doi = {10.1007/s00607-020-00831-8},
url = {https://doi.org/10.1007/s00607-020-00831-8}
}
@article{BCC-is21,
publisher = {Elsevier Science Publishers},
journal = {Information Systems},
author = {Mathilde Boltenhagen and Thomas Chatain and Josep Carmona},
title = {Anti-alignments—Measuring the precision of process models and event logs},
volume = {98},
year = 2021,
doi = {https://doi.org/10.1016/j.is.2020.101708},
url = {https://doi.org/10.1016/j.is.2020.101708},
note = {To appear}
}
@article{PKCH-natcommun20,
publisher = {Nature Research},
journal = {Nature Communications},
author = {Lo{\"i}c Paulev{\'e} and Juraj Kolc{\'a}k and Thomas Chatain and Stefan Haar},
title = {Reconciling qualitative, abstract, and scalable modeling of biological networks},
volume = {11},
number = {4256},
month = aug,
doi = {10.1038/s41467-020-18112-5},
year = {2020},
url = {https://www.nature.com/articles/s41467-020-18112-5}
}
@inproceedings{BCC-bpm19,
address = {Vienna, Austria},
month = sep,
volume = 362,
series = {Lecture Notes in Business Information Processing},
publisher = {Springer},
editor = {Chiara Di Francescomarino and Remco M. Dijkman and Uwe Zdun},
acronym = {{BPM}'19},
booktitle = {{B}usiness {P}rocess {M}anagement {W}orkshops ({BPM}'19), Revised Selected Papers},
author = {Mathilde Boltenhagen and Thomas Chatain and Josep Carmona},
title = {Encoding Conformance Checking Artefacts in {SAT}},
pages = {160-171},
year = {2019},
doi = {10.1007/978-3-030-37453-2_14},
pdf = {https://hal.inria.fr/hal-02419980/document},
url = {https://doi.org/10.1007/978-3-030-37453-2_14}
}
@article{ACCD-tpnomc19,
publisher = {Springer},
journal = {Transactions on Petri Nets and Other Models of Concurrency},
author = {Wil M. P. van der Aalst and
Josep Carmona and
Thomas Chatain and
Boudewijn F. van Dongen},
title = {A Tour in Process Mining: From Practice to Algorithmic Challenges},
pages = {1-35},
year = {2019},
volume = {14},
doi = {10.1007/978-3-662-60651-3_1},
url = {https://doi.org/10.1007/978-3-662-60651-3_1}
}
This file was generated by bibtex2html 1.98.