@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.