@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{RBH-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 = {Bouillard, Anne and Haar, Stefan and Rosario, Sidney},
  title = {Critical paths in the Partial Order Unfolding of a
                 Stochastic {P}etri Net},
  pages = {43-57},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-formats09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-formats09.pdf},
  doi = {10.1007/978-3-642-04368-0_6},
  abstract = {In concurrent real-time processes, the speed of individual
                  components has a double impact: on the one hand, the overall
                  latency of a compound process is affected by the latency of
                  its components. But, if the composition has race conditions,
                  the very outcome of the process will also depend on the
                  latency of component processes. Using stochastic Petri nets,
                  we investigate the probability of a transition occurrence
                  being critical for the entire process, i.e. such that a
                  small increase or decrease of the duration of the occurrence
                  entails an increase or decrease of the total duration of the
                  process. The first stage of the analysis focuses on
                  occurrence nets, as obtained by partial order unfoldings, to
                  determine criticality of events; we then lift to workflow
                  nets to investigate criticality of transitions inside a
                  workflow.}
}
@article{RBHJ-tsc08,
  publisher = {{IEEE} Computer Society Press},
  journal = {IEEE Transactions on Services Computing},
  author = {Rosario, Sidney and Benveniste, Albert and Haar, Stefan and
                  Jard, Claude},
  title = {Probabilistic {Q}o{S} and Soft Contracts for
                  Transaction-Based Web Services Orchestrations},
  pages = {187-200},
  volume = 1,
  number = 4,
  month = oct # {-} # dec,
  year = 2008,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/RBHJ-tsc08.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/RBHJ-tsc08.pdf},
  doi = {10.1109/TSC.2008.17},
  abstract = {Service level agreements (SLAs), or contracts, have an
                  important role in web services. They define the obligations
                  and rights between the provider of a web service and its
                  client, about the function and the Quality of the service
                  (QoS). For composite services like orchestrations, contracts
                  are deduced by a process called QoS contract composition,
                  based on contracts established between the orchestration and
                  the called web services. Contracts are typically stated as
                  hard guarantees (e.g., response time always less than 5
                  msec). Using hard bounds is not realistic, however, and more
                  statistical approaches are needed. In this paper we propose
                  using soft probabilistic contracts instead, which consist of
                  a probability distribution for the considered QoS
                  parameter---in this paper, we focus on timing. We show how to
                  compose such contracts, to yield a global probabilistic
                  contract for the orchestration. Our approach is implemented
                  by the TOrQuE tool. Experiments on TOrQuE show that overly
                  pessimistic contracts can be avoided and significant room
                  for safe overbooking exists. An essential component of SLA
                  management is then the continuous monitoring of the
                  performance of called web services, to check for violations
                  of the SLA. We propose a statistical technique for run-time
                  monitoring of soft contracts.}
}
@inproceedings{BRBH-atpn09,
  address = {Paris, France},
  month = jun,
  year = 2009,
  volume = 5606,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Franceschinis, Giuliana and Wolf, Karsten},
  acronym = {{PETRI~NETS}'09},
  booktitle = {{P}roceedings of the 30th
               {I}nternational {C}onference on
               {A}pplications and {T}heory of {P}etri {N}ets
               ({PETRI~NETS}'09)},
  author = {Bouillard, Anne and Rosario, Sidney and
		 Benveniste, Albert and Haar, Stefan},
  title = {Monotonicity in Service Orchestrations},
  pages = {263-282},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BRBH-atpn09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BRBH-atpn09.pdf},
  doi = {10.1007/978-3-642-02424-5_16},
  abstract = {Web Service orchestrations are compositions of different Web
    Services to form a new service. The services called during the orchestration
    guarantee a given performance to the orchestrater, usually in the form of
    contracts.\par
    These contracts can be used by the orchestrater to deduce the contract it
    can offer to its own clients, by performing contract composition. An
    implicit assumption in contract based QoS management is: {"}the better the
    component services perform, the better the orchestration's performance
    will~be{"}. Thus, contract based QoS management for Web services
    orchestrations implicitly assumes monotony.\par
    In some orchestrations, however, monotony can be violated, i.e., the
    performance of the orchestration improves when the performance of a
    component service degrades. This is highly undesirable since it can render
    the process of contract composition inconsistent.\par
    In this paper we define monotony for orchestrations modelled by Colored
    Occurrence Nets (CO-nets) and we characterize the classes of monotonic
    orchestrations. We show that few orchestrations are indeed monotonic,
    mostly since latency can be traded for quality of data. We also propose a
    sound refinement of monotony, called \emph{conditional monotony}, which
    forbids this kind of cheating and show that conditional monotony is widely
    satisfied by orchestrations. This finding leads to reconsidering the way
    SLAs should be formulated.}
}
@phdthesis{haar-hab2009,
  author = {Haar, Stefan},
  title = {Law and Partial Order~-- Nonsequential Behaviour and
                  Probability in Asynchronous Systems},
  school = {Universit{\'e} Rennes~1, Rennes, France},
  type = {M{\'e}moire d'habilitation},
  year = 2008,
  month = oct,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SH-hdr09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SH-hdr09.pdf}
}
@phdthesis{haar-these97,
  author = {Haar, Stefan},
  title = {Kausalit{\"a}t, Nebenl{\"a}ufigkeit und Konflikt. Elementare
                  Netzsysteme  aus topologisch-relationaler Sicht},
  year = 1997,
  type = {Th{\`e}se de doctorat},
  school = {Hamburg University, Germany}
}
@article{PH-at08,
  publisher = {Springer},
  journal = {Annals of Telecomunications},
  author = {Pouyllau, H{\'e}lia and Haar, Stefan},
  title = {Distributed {B}usacker-{G}owen algorithm for end-to-end {Q}o{S} pipe
                  negotiation in {X}-domain networks},
  volume = 63,
  number = {11-12},
  pages = {621-630},
  month = dec,
  year = 2008,
  doi = {10.1007/s12243-008-0055-0},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/PH-at08.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PH-at08.pdf},
  abstract = {Multimedia services and other critical multisite services
                  (e.g., VPN) are becoming mainstream, and they require a
                  guaranteed quality of service~(QoS). Services need to be
                  established across several autonomous systems~(ASes), often
                  to connect end-users. Thus, provisioning and control of
                  \emph{end-to-end} QoS requirements arise as one of the main
                  challenges in inter-AS management. The \emph{contractual approach},
                  consisting in using service-level agreements~(SLAs) defined
                  by each crossed~AS, allows to negotiate contract chains that
                  satisfy end-to-end requirements. However, establishing such
                  chains by on-demand negotiations does not scale up for large
                  numbers of requests. Hence, we propose a negotiation process
                  to occur before users' requests to establish service are
                  received. The proposed negotiation process results in the
                  selection of aggregated contract chains, called pipes, and a
                  distribution between them. Such a distribution would
                  indicate, for each chain of a pipe, the connection flow it
                  may accept. In this paper, we address the pipe negotiation
                  problem as a network flow problem. We also propose a
                  distributed adaptation of an algorithm for network flow
                  problems.}
}
@article{FBJH-deds05,
  publisher = {Springer},
  journal = {Discrete Event Dynamic Systems: Theory and Applications},
  author = {Fabre, {\'E}ric and Benveniste, Albert and 
                  Haar, Stefan and Jard, Claude},
  title = {Distributed monitoring of concurrent and asynchronous systems},
  volume = 15,
  number = {1},
  pages = {33-84},
  month = mar,
  year = 2005,
  doi = {10.1007/s10626-005-5238-5},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FBJH-deds05.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FBJH-deds05.pdf},
  abstract = {In this paper we study the diagnosis of distributed
                  asynchronous systems with concurrency. Diagnosis is
                  performed by a peer-to-peer distributed architecture of
                  supervisors. Our approach relies on Petri net unfoldings and
                  event structures, as means to manipulate trajectories of
                  systems with concurrency. This article is an extended
                  version of the paper with same title, which appeared as a
                  plenary address in the \textit{Proceedings of CONCUR'2003}.}
}
@article{BFH-tac03,
  publisher = {{IEEE} Computer Society Press},
  journal = {IEEE Transactions on Automatic Control},
  author = {Benveniste, Albert and Fabre, {\'E}ric and Haar, Stefan},
  title = {{M}arkov Nets: Probabilistic Models for Distributed and
                  Concurrent Systems},
  pages = {1936-1950},
  volume = 48,
  number = 11,
  month = nov,
  year = 2003,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFH-tac03.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFH-tac03.pdf},
  doi = {10.1109/TAC.2003.819076},
  abstract = {For distributed systems, i.e., large complex networked
                  systems, there is a drastic difference between a local view
                  and knowledge of the system, and its global view.
                  Distributed systems have local state and time, but do not
                  possess global state and time in the usual sense. In this
                  paper, motivated by the monitoring of distributed systems
                  and in particular of telecommunications networks, we develop
                  a generalization of Markov chains and hidden Markov models
                  for distributed and concurrent systems. By a concurrent
                  system, we mean a system in which components may evolve
                  independently, with sparse synchronizations. We follow a
                  so-called true concurrency approach, in which neither global
                  state nor global time are available. Instead, we use only
                  local states in combination with a partial order model of
                  time. Our basic mathematical tool is that of Petri net
                  unfoldings.}
}
@article{GHM-jcss03,
  publisher = {Elsevier Science Publishers},
  journal = {Journal of Computer and System Sciences},
  author = {Gaujal, Bruno and Haar, Stefan and Mairesse, Jean},
  title = {Blocking a Transition in a Free Choice Net, and What it Tells
                  About its Throughput},
  volume = 66,
  number = 3,
  pages = {515-548},
  month = may,
  year = 2003,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GHM-jcss03.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GHM-jcss03.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GHM-jcss03.ps},
  doi = {10.1016/S0022-0000(03)00039-4},
  abstract = {In a live and bounded free choice Petri net, pick a
                  non-conflicting transition. Then there exists a unique
                  reachable marking in which no transition is enabled except
                  the selected one. For a routed live and bounded free choice
                  net, this property is true for any transition of the net.
                  Consider now a live and bounded stochastic routed free
                  choice net, and assume that the routings and the firing
                  times are independent and identically distributed. Using the
                  above results, we prove the existence of asymptotic firing
                  throughputs for all transitions in the net. Furthermore, the
                  vector of the throughputs at the different transitions is
                  explicitly computable up to a multiplicative constant.}
}
@article{BFHJ-tac03,
  publisher = {{IEEE} Computer Society Press},
  journal = {IEEE Transactions on Automatic Control},
  author = {Benveniste, Albert and Fabre, {\'E}ric and Haar, Stefan and
                  Jard, Claude},
  title = {Diagnosis of Asynchronous Discrete Event Systems: A~Net Unfolding Approach},
  pages = {714-727},
  volume = 48,
  number = 5,
  month = may,
  year = 2003,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFHJ-tac03.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFHJ-tac03.pdf},
  doi = {10.1109/TAC.2003.811249},
  abstract = {In this paper, we consider the diagnosis of asynchronous
                  discrete event systems. We follow a so-called true
                  concurrency approach, in which no global state and no global
                  time is available. Instead, we use only local states in
                  combination with a partial order model of time. Our basic
                  mathematical tool is that of net unfoldings originating from
                  the Petri net research area. This study was motivated by the
                  problem of event correlation in telecommunications network
                  management.}
}
@article{Haar-fi02,
  publisher = {{IOS} Press},
  journal = {Fundamenta Informaticae},
  author = {Haar, Stefan},
  title = {Probabilistic Cluster Unfoldings},
  pages = {281-314},
  volume = 53,
  number = {3-4},
  month = dec,
  year = 2002,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Haar-fi02.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Haar-fi02.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Haar-fi02.ps},
  abstract = {This article introduces \emph{probabilistic cluster branching
    processes}, a probabilistic unfolding semantics for untimed Petri nets,
    with no structural or safety assumptions, giving probability measures for
    concurrent runs. The unfolding is constructed by local choices on each
    cluster (conflict closed subnet), while the authorization for cluster
    actions is governed by a stochastic trace, the \emph{policy}, that
    authorizes cluster actions. We introduce and characterize stopping times
    for these models, and prove a strong Markov property. Particularly
    adaquate probability measures for the choice of step in a cluster, as well
    as for the policy, are obtained by constructing Markov Fields from
    suitable marking-dependent Gibbs potentials.}
}
@article{Haar-fi01,
  publisher = {{IOS} Press},
  journal = {Fundamenta Informaticae},
  author = {Haar, Stefan},
  title = {Clusters, Confusion and Unfoldings},
  pages = {259-270},
  volume = 47,
  number = {3-4},
  month = sep # {-} # oct,
  year = 2001,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/Haar-fi01.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Haar-fi01.pdf},
  abstract = {We study \emph{independence} of events in the unfoldings of
    Petri nets, in particular indirect influences between concurrent events:
    \emph{Confusion} in the sense of E. Smith and \emph{weak interference}.
    The role of structural \emph{(conflict) clusters} is investigated, and a
    new unfolding semantics based on clusters motivated and introduced.}
}
@article{Haar-fi00,
  publisher = {{IOS} Press},
  journal = {Fundamenta Informaticae},
  author = {Haar, Stefan},
  title = {Occurrence Net Logics},
  pages = {105-127},
  volume = 43,
  number = {1-4},
  month = jul # {-} # aug,
  year = 2000
}
@inproceedings{BHJJ-testcom08,
  address = {Tokyo, Japan},
  month = jun,
  year = 2008,
  volume = 5047,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Suzuki, Kenji and Higashino, Teruo and Ulrich, Andreas and
                  Hasegawa, Toru},
  acronym = {{T}est{C}om/{FATES}'08},
  booktitle = {{P}roceedings of the 20th {IFIP} {TC 6/WG 6.1} {I}nternational {C}onference
	  on {T}esting of {S}oftware and {C}ommunicating {S}ystems
                  ({T}est{C}om'08) and 
	  8th {I}nternational {W}orkshop on {F}ormal {A}pproaches to {T}esting
                  of {S}oftware ({FATES}'08)},
  author = {von Bochmann, Gregor and Haar, Stefan and Jard, Claude and
                  Jourdan, Guy-Vincent},
  title = {Testing Systems Specified as Partial Order
                  Input{\slash}Output Automata},
  pages = {169-183},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHJJ-testcom08.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHJJ-testcom08.pdf},
  doi = {10.1007/978-3-540-68524-1_13},
  abstract = {An Input{\slash}Output Automaton is an automaton with a finite number
                  of states where each transition is associated with a single
                  inpuf or output interaction. In [1], we introduced a new
                  formalism, in which each transition is associated with a
                  bipartite partially ordered set made of concurrent inputs
                  followed by concurrent outputs. In this paper, we generalize
                  this model to Partial Order Input/Output Automata (POIOA),
                  in which each transition is associated with an almost
                  arbitrary partially ordered set of inputs and outputs. This
                  formalism can be seen as High-Level Messages Sequence Charts
                  with inputs and outputs and allows for the specification of
                  concurrency between inputs and outputs in a very general,
                  direct and concise way. We give a formal definition of this
                  framework, and define several conformance relations for
                  comparing system specifications expressed in this formalism.
                  Then we show how to derive a test suite that guarantees to
                  detect faults defined by a POIOA-specific fault model:
                  missing output faults, unspecified output faults, weaker
                  precondition faults, stronger precondition faults and
                  transfer faults.}
}
@inproceedings{HJJ-testcom07,
  address = {Tallinn, Estonia},
  month = jun,
  year = 2007,
  volume = 4581,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Petrenko, Alexandre and Veanes, Margus and Tretmans, Jan and
                  Grieskamp, Wolfgang},
  acronym = {{T}est{C}om/{FATES}'07},
  booktitle = {{P}roceedings of the 19th {IFIP} {TC 6/WG 6.1} {I}nternational {C}onference
	  on {T}esting of {S}oftware and {C}ommunicating {S}ystems
                  ({T}est{C}om'07) and 
	  7th {I}nternational {W}orkshop on {F}ormal {A}pproaches to {T}esting
                  of {S}oftware ({FATES}'07)},
  author = {Haar, Stefan and Jard, Claude and
                  Jourdan, Guy-Vincent},
  title = {Testing Input{\slash}Output Partial Order Automata},
  pages = {171-185},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HJJ-testcom07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HJJ-testcom07.pdf},
  doi = {10.1007/978-3-540-73066-8_12},
  abstract = {We propose an extension of the Finite State Machine framework in
                  distributed systems, using \emph{input{\slash}output partial
                  order automata} (IOPOA). In this model, transitions can be
                  executed non-atomically, reacting to asynchronous inputs on
                  several ports, and producing asynchronous output on those
                  ports. We develop the formal framework for distributed
                  testing in this architecture and compare with the
                  synchronous I{\slash}O automaton setting. The advantage of the
                  compact modelling by IOPOA combines with low complexity:
                  the number of tests required for concurrent input in our
                  model is polynomial in the number of inputs.}
}
@inproceedings{RBHJ-icws07,
  address = {Salt Lake City, Utah, USA},
  month = jul,
  year = 2007,
  publisher = {{IEEE} Computer Society Press},
  noeditor = {},
  acronym = {{ICWS}'07},
  booktitle = {{P}roceedings of the 6th {I}nternational {C}onference on {W}eb {S}ervices
                  ({ICWS}'07)},
  author = {Rosario, Sidney and Benveniste, Albert and Haar, Stefan and
                  Jard, Claude},
  title = {Probabilistic {Q}o{S} and soft contracts for transaction
                  based web services},
  pages = {126-133},
  doi = {10.1109/ICWS.2007.144},
  abstract = {Web services orchestrations and choreographies require
                  establishing Quality of Service (QoS) contracts with the
                  user. This is achieved by performing QoS composition, based
                  on contracts established between the orchestration and the
                  called Web services. These contracts are typically stated in
                  the form of hard guarantees (e.g., response time always less
                  than 5~msec). In this paper we propose using soft contracts
                  instead. Soft contracts are characterized by means of
                  probability distributions for QoS parameters. We show how to
                  compose such contracts, to yield a global contract
                  (probabilistic) for the orchestration. Our approach is
                  implemented by the TOrQuE tool. Experiments on TOrQuE show
                  that overly pessimistic contracts can be avoided and
                  significant room for safe overbooking exists.}
}
@inproceedings{PH-icws07,
  address = {Salt Lake City, Utah, USA},
  month = jul,
  year = 2007,
  publisher = {{IEEE} Computer Society Press},
  noeditor = {},
  acronym = {{ICWS}'07},
  booktitle = {{P}roceedings of the 6th {I}nternational {C}onference on {W}eb {S}ervices
                  ({ICWS}'07)},
  author = {Pouyllau, H{\'e}lia and Haar, Stefan},
  title = {A~protocol for {Q}o{S} contract negotiation and its implementation using web Services},
  pages = {168-175},
  doi = {10.1109/ICWS.2007.14},
  abstract = {The way Internet is used changes: demand grows for critical
                  services that cross several provider networks; guaranteeing
                  a required end-to-end Quality of Service (QoS) across
                  several networks becomes a challenge. Some critical services
                  (e.g. video-conference, VPN etc.) can not be satisfied in a
                  best effort fashion. The use of QoS contracts (Service Level
                  Agreements, SLAs) is effective for management of such
                  services. However, the problem of meeting end-to-end QoS
                  requirement remains: no centralized entity can compute
                  overall QoS for chains of contracts, and a fortiori, such
                  contract chains can not be optimized centrally. Thus, the
                  following problem has to be solved: given an end-to-end QoS
                  request and collections of available SLAs on each
                  participating domain, establish an end-to-end contract
                  committing a chain of providers and giving optimal service
                  under most reliable guarantees available.}
}
@inproceedings{PH-aims07,
  address = {Oslo, Norway},
  month = jun,
  year = 2007,
  volume = 4543,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Bandara, Arosha K. and Burgess, Mark},
  acronym = {{AIMS}'07},
  booktitle = {{P}roceedings of the 1st {I}nternational {C}onference on
                  {A}utonomous {I}nfrastructure, 
                  {M}anagement and {S}ecurity ({AIMS}'07)},
  author = {Pouyllau, H{\'e}lia and Haar, Stefan},
  title = {Distributed End-to-End QoS Contract Negotiation},
  pages = {180-183},
  doi = {10.1007/978-3-540-72986-0_20}
}
@inproceedings{RKBCHJ-wsfm07,
  address = {Brisbane, Australia},
  year = 2008,
  volume = 4937,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Dumas, Marlon and Heckel, Reiko},
  acronym = {{WS-FM}'07},
  booktitle = {{P}roceedings of the 4th {I}nternational {W}orkshop on {W}eb
                  {S}ervices and {F}ormal {M}ethods ({WS}-{FM}'07)},
  author = {Rosario, Sidney and Kitchin, David and Benveniste, Albert and
                  Cook, William R. and Haar, Stefan and Jard, Claude},
  title = {Event Structure Semantics of Orc},
  pages = {154-168},
  doi = {10.1007/978-3-540-79230-7_11},
  abstract = {Developing wide-area distributed applications requires jointly
    analyzing functional and Quality of Service (QoS) aspects, such as timing
    properties. Labelled transition systems and sequential trace
    semantics---the common semantic domains---do not facilitate this kind of
    analysis because they do not precisely express the causal relationships
    between events. Asymmetric Event Structures (AES) provide an explicit
    representation of the causal dependencies between events in the execution
    of a system and allow for an elegant coding of preemption. Event
    structures are, however, difficult to construct compositionally, because
    they cannot easily represent fragments of a computation. The heaps we
    develop here allow for such a representation, and easily generate AES. In
    this paper, we develop a partial-order semantics in terms of heaps, for
    Orc, an orchestration language used to describe distributed computations
    over the internet. We briefly show how Orc, and this new semantics, are
    used for QoS studies of wide area orchestrations.}
}
@inproceedings{PACH-aict06,
  address = {Guadeloupe, French Caribbean},
  month = feb,
  year = 2006,
  publisher = {{IEEE} Computer Society Press},
  noeditor = {},
  acronym = {{AICT}/{ICIW}'06},
  booktitle = {{P}roceedings of the {A}dvanced {I}nternational {C}onference on
                  {T}elecommunications and {I}nternational                
                  {C}onference on {I}nternet and {W}eb {A}pplications and
                  {S}ervices ({AICT}/{ICIW}'06)},
  author = {Pouyllau, H{\'e}lia and Aghasaryan, Armen and Ciarletta,
                  Laurent and Haar, Stefan},
  title = {X-domain {Q}o{S} budget negotiation using Dynamic
                  Programming},
  pages = {35}
}
@inproceedings{BHK-fossacs06,
  address = {Vienna, Austria},
  month = mar,
  year = 2006,
  volume = 3921,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Aceto, Luca and Ing{\'o}lfsd{\'o}ttir, Anna},
  acronym = {{FoSSaCS}'06},
  booktitle = {{P}roceedings of the 9th {I}nternational
               {C}onference on {F}oundations of {S}oftware {S}cience
               and {C}omputation {S}tructures
               ({FoSSaCS}'06)},
  author = {Baldan, Paolo and Haar, Stefan and K{\"o}nig, Barbara},
  title = {Distributed Unfolding of {P}etri Nets},
  pages = {126-141},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHK-fossacs06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHK-fossacs06.pdf},
  doi = {10.1007/11690634_9},
  abstract = {Some recent Petri net-based approaches to fault diagnosis of
                  distributed systems suggest to factor the problem into local
                  diagnoses based on the unfoldings of local views of the
                  system, which are then correlated with diagnoses from
                  neighbouring supervisors. In this paper we propose a notion
                  of system factorisation expressed in terms of pullback
                  decomposition. To ensure coherence of the local views and
                  completeness of the diagnosis, data exchange among the
                  unfolders needs to be specified with care. We introduce
                  interleaving structures as a format for data exchange
                  between unfolders and we propose a distributed algorithm for
                  computing local views of the unfolding for each system
                  component. The theory of interleaving structures is
                  developed to prove correctness of the distributed unfolding
                  algorithm.}
}
@inproceedings{AAHM-pods05,
  address = {Baltimore, Maryland, USA},
  month = jun,
  year = 2005,
  publisher = {ACM Press},
  editor = {Li, Chen},
  acronym = {{PODS}'05},
  booktitle = {{P}roceedings of the 24th {A}nnual 
	  {ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium 
	  on {P}rinciples of {D}atabase {S}ystems
	  ({PODS}'05)},
  author = {Abiteboul, Serge and Abrams, Zo{\"e} and Haar, Stefan and
                  Milo, Tova},
  title = {Diagnosis of asynchronous discrete event systems: datalog to the rescue!},
  pages = {358-367},
  doi = {10.1145/1065167.1065214},
  abstract = {We consider query optimization techniques for data intensive P2P
                  applications. We show how to adapt an old technique from
                  deductive databases, namely Query-Sub-Query~(QSQ), to~a
                  setting where autonomous and distributed peers share large
                  volumes of interelated data.We illustrate the technique with
                  an important telecommunication problem, the diagnosis of
                  distributed telecom systems. We show that (i)~the~problem
                  can be modeled using Datalog programs, and (ii)~it~can
                  benefit from the large battery of optimization techniques
                  developed for Datalog. In particular, we show that a simple
                  generic use of the extension of QSQ achieves an optimization
                  as good as that previously provided by dedicated diagnosis
                  algorithms. Furthermore, we show that it allows solving
                  efficiently a much larger class of system analysis problems.}
}
@inproceedings{FBHJA-ict04,
  address = {Fortaleza, Brazil},
  month = aug,
  year = 2004,
  volume = 3124,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {de Souza, Jos{\'e} Neuman and Dini, Petre and Lorenz, Pascal},
  acronym = {{ICT}'04},
  booktitle = {{P}roceedings of the 11th {I}nternational {C}onference on
                  {T}elecommunications  ({ICT}'04)},
  author = {Fabre, {\'E}ric and Benveniste, Albert and Haar, Stefan and
                  Jard, Stefan and Aghasaryan, Armen},
  title = {Algorithms for Distributed Fault Management in
                  Telecommunications Networks},
  pages = {820-825},
  abstract = {Distributed architectures for network management have been the
                  subject of a large research effort, but distributed
                  algorithms that implement the corresponding functions have
                  been much less investigated. In this paper we describe novel
                  algorithms for model-based distributed fault diagnosis.}
}
@inproceedings{BHFJ-concur03,
  address = {Marseilles, France},
  month = aug,
  year = 2003,
  volume = 2761,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Amadio, Roberto M. and Lugiez, Denis},
  acronym = {{CONCUR}'03},
  booktitle = {{P}roceedings of the 14th 
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'03)},
  author = {Benveniste, Albert and Haar, Stefan and Fabre, {\'E}ric and
                  Jard, Claude},
  title = {Distributed Monitoring of Concurrent and Asynchronous
                  Systems},
  pages = {1-26},
  abstract = {Developing applications over a distributed and asynchronous
     architecture without the need for synchronization services is going to
     become a central track for distributed computing. This research track
     will be central for the domain of autonomic computing and
     self-management. Distributed constraint solving, distributed observation,
     and distributed optimization, are instances of such applications. This
     paper is about distributed observation: we investigate the problem of
     distributed monitoring of concurrent and asynchronous systems, with
     application to distributed fault management in telecommunications
     networks.\par
     Our approach combines two techniques: compositional unfoldings to handle
     concurrency properly, and a variant of graphical algorithms and belief
     propagation, originating from statistics and information theory.}
}
@inproceedings{haar-papm2002,
  address = {Copenhagen, Denmark},
  month = jul,
  year = 2002,
  volume = 2399,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Hermanns, Holger and Segala, Roberto},
  acronym = {{PAPM-PROBMIV}'02},
  booktitle = {{P}roceedings of the 2nd Joint Interbational Workshop on Process
                  Algebra and Probabilistic Methods, Performance Modeling and
                  Verification ({PAPM-PROBMIV}'02)},
  author = {Haar, Stefan},
  title = {Probabilistic Unfoldings and Partial Order Fairness in
                  {P}etri Nets},
  pages = {95-114},
  doi = {10.1007/3-540-45605-8_7},
  abstract = {The article investigates fairness and conspiracy in a
                  probabilistic framework, based on unfoldings of Petri nets.
                  Here, the unfolding semantics uses a new, cluster-based view
                  of local \emph{choice}. The algorithmic construction of the
                  unfolding proceeds on two levels, choice of steps inside
                  conflict clusters, where the choice may be fair or unfair,
                  and the \emph{policy} controlling the order in which clusters may
                  act; this policy may or may not conspire, e.g., against a
                  transition. In the context of an example where conspiracy
                  can hide in the partial order behavior of a life and 1-safe
                  Petri net, we show that, under non-degenerate i.i.d.
                  randomization on both levels, both conspiracy and unfair
                  behavior have probability~0. The probabilistic model, using
                  special Gibbs potentials, is presented here in the context
                  of 1-safe nets, but extends to any Petri net.}
}
@inproceedings{HBFJ-ifac05,
  address = {Prague, Czech Republic},
  month = jul,
  year = 2005,
  publisher = {IFAC},
  editor = {Hor{\'a}cek, Petr and {\v{S}}imandl, Miroslav and
                  Z{\'\i}tek, Pavel},
  acronym = {{IFAC}'05},
  booktitle = {{P}roceedings of the 16th {IFAC} {W}orld {C}ongress
               ({IFAC}'05)},
  author = {Haar, Stefan and Benveniste, Albert and Fabre, {\'E}ric and
                  Jard, Claude},
  title = {Fault Diagnosis for Distributed Asynchronous Dynamically Reconfigured Discrete
                  Event Systems},
  nopages = {},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HBFJ-ifac05.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HBFJ-ifac05.pdf},
  abstract = {Diagnosis of concurrent and asynchronous systems, such as large
    telecommunication or information systems, requires powerful mathematical
    models. The use of Petri net unfoldings allows to formalize diagnosis
    using partial order semantics, a generalization from the global state
    model imposed by the use of automata. If, in addition to asynchronicity
    and distribution, the network topology itself is subject to dynamic
    changes, all static models, including Petri nets, reach their limits.
    Then, graph grammars can be used, encoding in the current local states not
    only the current values of state variables but also the current topology
    of the network connections; the fact that unfolding semantics is available
    allows to carry over the diagnosis algorithms to this setting. }
}
@inproceedings{HBFJ-cdc03,
  address = {Hawaii, USA},
  month = dec,
  year = 2003,
  volume = 4,
  publisher = {{IEEE} Control System Society},
  acronym = {{CDC}'03},
  booktitle = {{P}roceedings of the 42nd {IEEE} {C}onference on Decision 
		and Control ({CDC}'03)},
  author = {Haar, Stefan and Benveniste, Albert and Fabre, {\'E}ric and
                  Jard, Claude},
  title = {Partial Order Diagnosability of Discrete Event Systems Using
                  {P}etri Net Unfoldings},
  pages = {3748-3753},
  doi = {10.1109/CDC.2003.1271732},
  abstract = {In truly asynchronous, distributed systems, neither global state
                  nor global time are available. The diagnosis approach with
                  Petri net unfoldings, motivated by the problem of event
                  correlation in telecommunications network management and
                  proposed, uses only local states in combination with a
                  partial order model of time. Here, we give a definition of
                  weak and strong diagnosability in terms of partially ordered
                  executions, and characterize diagnosable systems; the
                  characterizing property can be effectively verified using a
                  finite complete prefix of the net unfolding.}
}
@inproceedings{haar-cdc07,
  address = {New Orleans, Louisiana, USA},
  month = dec,
  year = 2007,
  publisher = {{IEEE} Control System Society},
  acronym = {{CDC}'07},
  booktitle = {{P}roceedings of the 46th {IEEE} {C}onference on Decision 
		and Control ({CDC}'07)},
  author = {Haar, Stefan},
  title = {Unfold and Cover: Qualitative Diagnosability for {P}etri
                  Nets},
  pages = {1886-1891},
  doi = {10.1109/CDC.2007.4434691},
  abstract = {In recent years, classical discrete event fault diagnosis
                  techniques have been extended to Petri net system models
                  under partial order semantics. We propose here to take
                  further advantage of the partial order representation of
                  concurrent processes; we explore the relational structure of
                  occurrence nets to derive a covering relation. It indicates
                  that occurrence of some event~\(a\) inevitable leads to
                  occurrence of some event~\(b\), before~\(a\), after~\(a\), or
                  concurrently. Covering defines a decomposition of occurrence
                  nets into facets; we introduce the facet-based concept of
                  \(q\)-diagnosability ---for qualitative diagnosability as opposed
                  to quantitative criteria--- which is specific to partial
                  order semantics. All objects considered can be computed from
                  a finite unfolding prefix of bounded length.}
}
@inproceedings{BHFJ-cdc03,
  address = {Hawaii, USA},
  month = dec,
  year = 2003,
  volume = 4,
  publisher = {{IEEE} Control System Society},
  acronym = {{CDC}'03},
  booktitle = {{P}roceedings of the 42nd {IEEE} {C}onference on Decision 
		and Control ({CDC}'03)},
  author = {Benveniste, Albert and Haar, Stefan and Fabre, {\'E}ric and
                  Jard, Claude},
  title = {Distributed unfoldings: a tool to address distributed discrete event
                  systems diagnosis},
  pages = {3742-3747},
  doi = {10.1109/CDC.2003.1271731},
  abstract = {This paper deals with distributed and asynchronous discrete
                  event systems diagnosis. This paper has proposed an
                  unfolding approach to the distributed diagnosis of
                  concurrent and asynchronous discrete event dynamical
                  systems. This presentation was informal, based on a toy
                  illustrative examples. Fault diagnosis for distributed
                  discrete event systems with asychronous communication is
                  analyzed.}
}
@inproceedings{haar-pnpm03,
  address = {Urbana, Illinois, USA},
  month = sep,
  year = 2003,
  publisher = {{IEEE} Computer Society Press},
  noeditor = {},
  acronym = {{PNPM}'03},
  booktitle = {{P}roceedings of the 10th {I}nternational {W}orkshop on {P}etri
                  {N}ets and {P}erformance {M}odels ({PNPM}'03)},
  author = {Haar, Stefan},
  title = {Distributed Semi-{M}arkov Processes in Stochastic {T}-Timed
                  {P}etri Nets},
  pages = {114-123}
}
@inproceedings{haar-csp02,
  address = {Berlin, Germany},
  month = oct,
  year = 2002,
  volume = 161,
  series = {Informatik Bericht},
  publisher = {Humboldt Universit{\"a}t zu Berlin},
  editor = {Burkhard, Hans-Dieter and Czaja, Ludwik and Lindemann, Gabriela
                  and Skowron, Andrzej and Starke, Peter H.},
  acronym = {{CS\&P}'02},
  booktitle = {{P}roceedings of the 11th {C}oncurrency, {S}pecification \&
                  {P}rogramming {W}orkshop ({CS\&P}'02)},
  author = {Haar, Stefan},
  title = {Probabilizing Parallelism in Cluster Unfoldings}
}
@inproceedings{BFJH-wodes02,
  address = {Zaragoza, Spain},
  month = oct,
  year = 2002,
  acronym = {{WODES}'02},
  booktitle = {{P}roceedings of the 6th {W}orkshop on {D}iscrete {E}vent {S}ystems
	   ({WODES}'02)},
  author = {Benveniste, Albert and Fabre, {\'E}ric and
                  Jard, Claude and Haar, Stefan},
  title = {Diagnosis of Asynchronous Discrete Event Systems, A~Net
                  Unfolding Approach},
  pages = {182-190}
}
@inproceedings{HSKT-wodes02,
  address = {Zaragoza, Spain},
  month = oct,
  year = 2002,
  acronym = {{WODES}'02},
  booktitle = {{P}roceedings of the 6th {W}orkshop on {D}iscrete {E}vent {S}ystems
	   ({WODES}'02)},
  author = {Haar, Stefan and Simonot-Lion, Fran{\c{c}}oise and Kaiser,
                  Laurent and Toussaint, Jo{\"e}l},
  title = {Equivalence of Timed State Machines and Safe Time {P}etri
                  Nets},
  pages = {119-126}
}
@inproceedings{BFH-allerton01,
  address = {Monticello, Illinois, USA},
  month = oct,
  year = 2001,
  editor = {Jones, Douglas L. and Voulgaris, Petros G.},
  booktitle = {{P}roceedings of the 39th {A}nnual {A}llerton {C}onference on
		{C}ommunication, {C}ontrol, and {C}omputing},
  author = {Benveniste, Albert and Fabre, {\'E}ric and Haar, Stefan},
  title = {Probabilistic {P}etri Net Unfoldings in Network Fault
                  Diagnosis}
}
@inproceedings{BFH-pmccs5,
  address = {Erlangen, Germany},
  month = sep,
  year = 2001,
  editor = {L{\"u}thi, Johannes and Telek, Mikl{\'o}s},
  acronym = {{PMCCS}-5},
  booktitle = {{P}roceedings of the 5th {I}nternational {W}orkshop on
                  {P}erformability {M}odeling of {C}omputer and
                  {C}ommunication {S}ystems ({PMCCS-5})},
  author = {Benveniste, Albert and Fabre, {\'E}ric and Haar, Stefan},
  title = {Probabilistic Branching Processes for Fault Diagnosis in
                  Concurrent Systems}
}
@inproceedings{HBF-wcdc01,
  address = {Newcastle upon Tyne, UK},
  month = jun,
  year = 2001,
  editor = {Ezhilchelvan, Paul and Romanovsky, Alexander},
  booktitle = {{P}roceedings of the {W}orkshop on {C}oncurrency in {D}ependable
                  {C}omputing},
  author = {Haar, Stefan and Benveniste, Albert and Fabre, {\'E}ric},
  title = {{M}arkov Nets: A~New Probabilistic Model
                  for Fault Diagnosis in Concurrent Systems},
  nopages = {}
}
@inproceedings{BH-sssc01,
  address = {Prague, Czech Republic},
  month = aug,
  year = 2001,
  editor = {Gaubert, St{\'e}phane},
  booktitle = {{P}roceedings of the {W}orkshop on {M}ax-{P}lus {A}lgebras},
  author = {Baccelli, Fran{\c{c}}ois and Haar, Stefan},
  title = {Counter Equations for Timed Competition Nets}
}
@inproceedings{haar-getco01,
  address = {Aalborg, Denmark},
  month = aug,
  year = 2001,
  noeditor = {},
  acronym = {{GETCO}'01},
  booktitle = {{P}reliminary {P}roceedings of the 3rd {W}orkshop on {G}eometric and
		{T}opological {M}ethods in {C}oncurrency ({GETCO}'01)},
  author = {Haar, Stefan},
  title = {Cyclic and Partial Order Models for Concurrency},
  nmnote = {Did not appear in post proceedings},
  nopages = {}
}
@inproceedings{GH-wodes00,
  address = {Ghent, Belgium},
  month = aug,
  year = 2000,
  publisher = {Kluwer Academic Publishers},
  editor = {Boel, Ren{\'e} and Stremersch, Geert},
  acronym = {{WODES}'00},
  booktitle = {{P}roceedings of the 5th {W}orkshop on {D}iscrete {E}vent {S}ystems
	   ({WODES}'00)},
  author = {Gaujal, Bruno and Haar, Stefan},
  title = {A~Limit Semantics for Timed {P}etri Nets},
  pages = {219-228}
}
@inproceedings{haar-mfcs98wc,
  address = {Brno, Czech Republic},
  month = aug,
  year = 1998,
  volume = 18,
  series = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier Science Publishers},
  editor = {Jan{\v c}ar, Petr and K{\v{r}}et{\'i}nsk{\'y}, Mojm{\'i}r},
  booktitle = {{P}roceedings of the {MFCS'98} {W}orkshop on {C}oncurrency},
  author = {Haar, Stefan},
  title = {Branching Processes of General {S/T}-Systems and their
                  Properties},
  pages = {65-74},
  doi = {10.1016/S1571-0661(05)80250-6 }
}
@inproceedings{haar-wodes10,
  address = {Berlin, Germany},
  month = aug # {-} # sep,
  year = 2010,
  publisher = {IFAC},
  editor = {Raisch, J{\"o}rg and Giua, Alessandro and Lafortune,
                  St{\'e}phane and Moor, Thomas},
  acronym = {{WODES}'10},
  booktitle = {{P}roceedings of the 10th {W}orkshop on {D}iscrete {E}vent {S}ystems
	   ({WODES}'10)},
  author = {Haar, Stefan},
  title = {What Topology Tells us about Diagnosability in Partial Order Semantics},
  pages = {221-226},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/SH-wodes10.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SH-wodes10.pdf},
  abstract = {From a partial observation of the behaviour of a labeled
    Discrete Event System, fault Diagnosis strives to determine whether or not
    a given {"}invisible{"} fault event has occurred. The diagnosability problem
    can be stated as follows: does the labeling allow for an outside observer
    to determine the occurrence of the fault, no later than a bounded number
    of events after that unobservable occurrence? In concurrent systems,
    partial order semantics adds to the difficulty of the problem, but also
    provides a richer and more complex picture of observation and diagnosis.
    In particular, it is crucial to clarify the intuitive notion of {"}time
    after fault occurrence{"}. To this end, we will use a unifying metric
    framework for event structures, providing a general topological
    description of diagnosability in both sequential and nonsequential
    semantics for Petri nets.}
}
@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.}
}
@article{Haar-tac10,
  publisher = {{IEEE} Computer Society Press},
  journal = {IEEE Transactions on Automatic Control},
  author = {Haar, Stefan},
  title = {Types of Asynchronous Diagnosability and
		the {\emph{Reveals}}-Relation in Occurrence Nets},
  volume = 55,
  number = 10,
  month = oct,
  year = 2010,
  pages = {2310-2320},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/haar-tac10.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/haar-tac10.pdf},
  doi = {10.1109/TAC.2010.2063490},
  abstract = {We consider asynchronous diagnosis in (safe) Petri net models of
    distributed systems, using the partial order semantics of occurrence net
    unfoldings. Both the observability and diagnosability properties will
    appear in two different forms, depending on the semantics chosen:
    \emph{strong} observability and diagnosability are the classical notions
    from the state machine model and correspond to interleaving semantics in
    Petri nets. By contrast, the \emph{weak} form is linked to characteristics
    of nonsequential processes, and requires an asynchronous \emph{progress}
    assumption on those processes. We give algebraic characterizations for
    both types, and give verification methods. The study of weak
    diagnosability leads us to the analysis of a relation in occurrence nets,
    first presented in~[S.~Haar~(2007): \textit{Unfold and Cover: Qualitative
    Diagnosability for Petri Nets.}]: given the occurrence of some event~\(a\)
    that \emph{reveals}~\(b\), the occurrence of~\(b\) is inevitable. Then
    \(b\) may already have occurred, be concurrent to, or even in the future
    of~\(a\). We show that the \emph{reveals}-relation can be effectively
    computed recursively---for each pair, a suitable finite prefix of bounded
    depth is sufficient---and show its use in asynchronous diagnosis. Based on
    this relation, a~decomposition of the Petri net unfolding into
    \emph{facets} is defined, yielding an abstraction technique that preserves
    and reflects maximal partially ordered runs.}
}
@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{haar-cdcccc09,
  address = {Shanghai, China},
  month = dec,
  year = 2009,
  publisher = {{IEEE} Control System Society},
  acronym = {{CDC/CCC}'09},
  booktitle = {{P}roceedings of the Joint 48th {IEEE} {C}onference on {D}ecision 
		and {C}ontrol ({CDC}'09) and 28th {C}hinese {C}ontrol {C}onference ({CCC}'09)},
  author = {Haar, Stefan},
  title = {Qualitative Diagnosability of Labeled {P}etri Nets Revisited},
  pages = {1248-1253},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/haar-cdc09.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/haar-cdc09.pdf},
  doi = {10.1109/CDC.2009.5400917},
  abstract = {In recent years, classical discrete event fault diagnosis
    techniques have been extended to Petri Net system models under partial
    order semantics. In~a recent paper, we showed how to take further
    advantage of the partial order representation of concurrent processes, by
    decomposing the unfolding into 'facets', formed by subnets whose events
    either all occur eventually, or none of them occurs. A~notion of
    \emph{q(ualitative)}-diagnosability was proposed based on this
    decomposition. The present paper corrects the definition of
    q-diagnosability and develops its properties. Sufficient and necessary
    criteria, on the transition labeling, for q-diagnosability are shown; for
    their verification, and diagnosis itself, compact data structures are
    sufficient.}
}
@article{haar-deds11,
  publisher = {Springer},
  journal = {Discrete Event Dynamic Systems: Theory and Applications},
  author = {Haar, Stefan},
  title = {What topology tells us about diagnosability in partial order semantics},
  pages = {383-402},
  volume = 22,
  number = 4,
  year = {2012},
  month = dec,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/haar-deds11.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/haar-deds11.pdf},
  doi = {10.1007/s10626-011-0121-z},
  abstract = {From a partial observation of the behaviour of a labeled
    Discrete Event System, \emph{fault diagnosis} strives to determine whether
    or not a given {"}invisible{"} fault event has occurred. The
    \emph{diagnosability problem} can be stated as follows: does the labeling
    allow for an outside observer to determine the occurrence of the fault, no
    later than a bounded number of events after that unobservable occurrence?
    When this problem is investigated in the context of concurrent systems,
    partial order semantics adds to the difficulty of the problem, but also
    provides a richer and more complex picture of observation and diagnosis.
    In particular, it is crucial to clarify the intuitive notion of
    {"}\emph{time after fault occurrence}{"}. To this end, we will use a
    unifying metric framework for event structures, providing a general
    topological description of diagnosability in both sequential and
    nonsequential semantics for Petri nets.}
}
@inproceedings{HKS-gandalf11,
  address = {Minori, Italy},
  month = jun,
  year = 2011,
  volume = 54,
  series = {Electronic Proceedings in Theoretical Computer Science},
  editor = {D'Agostino, Giovanna and La{~}Torre, Salvatore},
  acronym = {{GandALF}'11},
  booktitle = {{P}roceedings of the 2nd {I}nternational {S}ymposium
                on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification
                  ({GandALF}'11)},
  author = {Haar, Stefan and Kern, Christian and Schwoon, Stefan},
  title = {Computing the Reveals Relation in Occurrence Nets},
  pages = {31-44},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/HKS-gandalf11.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HKS-gandalf11.pdf},
  doi = {10.4204/EPTCS.54.3},
  abstract = {Petri net unfoldings are a useful tool to tackle state-space
    explosion in verification and related tasks. Moreover, their structure
    allows to access directly the relations of causal precedence, concurrency,
    and conflict between events. Here, we explore the data structure further,
    to determine the following relation: event~\(a\) is said to reveal
    event~\(b\) iff the occurrence of~\(a\) implies that~\(b\) inevitably
    occurs, too, be it before, after, or concurrently with~\(a\). Knowledge of
    reveals facilitates in particular the analysis of partially observable
    systems, in the context of diagnosis, testing, or verification; it can
    also be used to generate more concise representations of behaviours via
    abstractions. The reveals relation was previously introduced in the
    context of fault diagnosis, where it was shown that the reveals relation
    was decidable: for a given pair~\(a,b\) in the unfolding~\(U\) of a safe
    Petri net~\(N\), a finite prefix~\(P\) of~\(U\) is sufficient to decide
    whether or not \(a\) reveals~\(b\). In this paper, we first considerably
    improve the bound on~\(|P|\). We then show that there exists an efficient
    algorithm for computing the relation on a given prefix. We have
    implemented the algorithm and report on experiments.}
}
@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}
}
@misc{impro-D2.1,
  author = {Akshay, S. and B{\'e}rard, B{\'e}atrice and Bouyer, Patricia
                  and Haar, Stefan and Haddad, Serge and Jard, Claude and
		  Lime, Didier and Markey, Nicolas and Reynier, Pierre-Alain
                  and Sankur, Ocan and Thierry-Mieg, Yann},
  title = {Overview of Robustness in Timed Systems},
  howpublished = {Deliverable ImpRo D~2.1 (ANR-2010-BLAN-0317)},
  year = 2012,
  month = jan,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d21.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d21.pdf}
}
@incollection{HM-lncis433,
  author = {Haar, Stefan and Masopust, Tom{\'a}{\v{s}}},
  title = {Languages, Decidability, and Complexity},
  booktitle = {Control of Discrete-Event Systems~-- Automata and {P}etri Net Perspectives},
  editor = {Seatzu, Carla and Silva, Manuel and van Schuppen, Jan H.},
  year = {2013},
  pages = {23-43},
  publisher = {Springer},
  series = {Lecture Notes in Control and Information Sciences},
  volume = 433,
  doi = {10.1007/978-1-4471-4276-8_2},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/HM-lncis433.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HM-lncis433.pdf}
}
@incollection{HS-lncis433,
  author = {Haar, Stefan and Fabre, {\'E}ric},
  title = {Diagnosis with {P}etri Net Unfoldings},
  booktitle = {Control of Discrete-Event Systems~-- Automata and {P}etri Net Perspectives},
  editor = {Seatzu, Carla and Silva, Manuel and van Schuppen, Jan H.},
  year = {2013},
  pages = {301-318},
  publisher = {Springer},
  series = {Lecture Notes in Control and Information Sciences},
  volume = 433,
  doi = {10.1007/978-1-4471-4276-8_15},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/HS-lncis433.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HS-lncis433.pdf}
}
@inproceedings{PHL-tap12,
  address = {Prague, Czech Republic},
  month = may # {-} # jun,
  year = 2012,
  volume = 7305,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Brucker, Achim D. and Julliand, Jacques},
  acronym = {{TAP}'12},
  booktitle = {{P}roceedings of the 6th {I}nternational {C}onference
                  on {T}ests and {P}roofs ({TAP}'12)},
  author = {Ponce{ }de{~}Le{\'o}n, Hern{\'a}n and Haar, Stefan and Longuet, Delphine},
  title = {Conformance Relations for Labeled Event Structures},
  pages = {83-98},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-tap12.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-tap12.pdf},
  doi = {10.1007/978-3-642-30473-6_8},
  abstract = {We propose a theoretical framework for testing concurrent
    systems from true concurrency models like Petri nets or networks of
    automata. The underlying model of computation of such formalisms are
    labeled event structures, which allow to represent concurrency explicitly.
    The activity of testing relies on the definition of a conformance relation
    that depends on the observable behaviors on the system under test, which
    is given for sequential systems by ioco type relations. However, these
    relations are not capable of capturing and exploiting concurrency of non
    sequential behavior. We~study different conformance relations for labeled
    event structures, relying on different notions of observation, and
    investigate their properties and connections.}
}
@inproceedings{AMH-safep12,
  address = {Mexico City, Mexico},
  month = aug,
  year = 2012,
  publisher = {IFAC},
  acronym = {{SAFEPROCESS}'12},
  booktitle = {{P}roceedings of the 8th {IFAC} {S}ymposium on {F}ault {D}etection, 
  	   {S}upervision and {S}afety for {T}echnical {P}rocesses ({SAFEPROCESS}'12)},
  author = {Agarwal, Anoopam and Madalinski, Agnes and Haar, Stefan},
  title = {Effective Verification of Weak Diagnosability},
  nopages = {},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/AMH-safep12.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AMH-safep12.pdf},
  doi = {10.3182/20120829-3-MX-2028.00083},
  abstract = {The \emph{diagnosability} problem can be stated as follows: does
    a given labeled Discrete Event System allow for an outside observer to
    determine the occurrence of the {"}invisible{"} fault, no later than a
    bounded number of events after that unobservable occurrence, and based on
    the partial observation of the behaviour? When this problem is
    investigated in the context of concurrent systems, partial order semantics
    induces a separation between classical or strong diagnosability on the one
    hand, and \emph{weak diagnosability} on the other hand. The present paper
    presents the first solution for checking weak diagnosability, via a
    \emph{verifier} construction.}
}
@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.}
}
@misc{impro-D51,
  author = {Bouyer, Patricia and Faucou, S{\'e}bastien and Haar, Stefan and 
  	    Jovanivi{\'c}, Aleksandra and Lime, Didier and Markey, Nicolas and
	    Roux, Olivier H. and Sankur, Ocan},
  title = {Control tasks for Timed System; Robustness issues},
  howpublished = {Deliverable ImpRo~5.1, (ANR-10-BLAN-0317)},
  month = jan,
  year = {2013},
  note = {34~pages},
  type = {Contract Report},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d51.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d51.pdf}
}
@inproceedings{HHMS-fsttcs13,
  address = {Guwahati, India},
  month = dec,
  year = 2013,
  volume = {24},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Seth, Anil and Vishnoi, Nisheeth},
  acronym = {{FSTTCS}'13},
  booktitle = {{P}roceedings of the 33rd {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'13)},
  author = {Haar, Stefan and Haddad, Serge and Melliti, Tarek and Schwoon,
                  Stefan},
  title = {Optimal Constructions for Active Diagnosis},
  pages = {527-539},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/HHMS13-fsttcs.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HHMS13-fsttcs.pdf},
  doi = {10.4230/LIPIcs.FSTTCS.2013.527},
  abstract = {The task of diagnosis consists in detecting, without ambiguity,
    occurrence of faults in a partially observed system. Depending on the
    degree of observability, a discrete event system may be diagnosable or
    not. Active diagnosis aims at controlling the system in order to make it
    diagnosable. Solutions have already been proposed for the active diagnosis
    problem, but their complexity remains to be improved. We solve here the
    active diagnosability decision problem and the active diagnoser synthesis
    problem, proving that (1)~our procedures are optimal w.r.t. to
    computational complexity, and (2)~the memory required for the active
    diagnoser produced by the synthesis is minimal. Furthermore, focusing on
    the minimal delay before detection, we establish that the memory required
    for any active diagnoser achieving this delay may be highly greater than
    the previous one. So we refine our construction to build with the same
    complexity and memory requirement an active diagnoser that realizes a
    delay bounded by twice the minimal delay.}
}
@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{PHL-ictss13,
  address = {Istanbul, Turkey},
  month = nov,
  year = 2013,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Yenig{\"u}n, H{\"u}sn{\"u} and Yilmaz, Cemal and Ulrich, Andreas},
  acronym = {{ICTSS}'13},
  booktitle = {{P}roceedings of the 25th {IFIP} {I}nternational {C}onference on
                  {T}esting {S}oftware and {S}ystems ({ICTSS}'13)},
  author = {Ponce{ }de{~}Le{\'o}n, Hern{\'a}n and Haar, Stefan and
                  Longuet, Delphine},
  title = {Unfolding-based Test Selection for Concurrent Conformance},
  pages = {98-113},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-ictss13.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-ictss13.pdf},
  doi = {10.1007/978-3-642-41707-8_7},
  abstract = {Model-based testing has mainly focused on models where currency
    is interpreted as interleaving (like the ioco theory for labeled
    transition systems), which may be too coarse when one wants concurrency to
    be preserved in the implementation. In order to test such concurrent
    systems, we choose to use Petri nets as specifications and define a
    concurrent conformance relation named co-ioco. We propose a test
    generation algorithm based on Petri net unfolding able to build a complete
    test suite w.r.t our co-ioco conformance relation. In addition we propose
    a coverage criterion based on a dedicated notion of complete prefixes that
    selects a manageable test suite.}
}
@inproceedings{HRS-acsd13,
  address = {Barcelona, Spain},
  month = jul,
  year = 2013,
  publisher = {{IEEE} Computer Society Press},
  editor = {Pietkiewicz{-}Koutny, Marta and Lazarescu, Mihai Teodor},
  acronym = {{ACSD}'13},
  booktitle = {{P}roceedings of the 13th {I}nternational
               {C}onference on {A}pplication of {C}oncurrency
               to {S}ystem {D}esign
               ({ACSD}'13)},
  author = {Haar, Stefan and Rodr{\'\i}guez, C{\'e}sar and Schwoon, Stefan},
  title = {Reveal Your Faults: It's Only Fair!},
  pages = {120-129},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/HRS-acsd13.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HRS-acsd13.pdf},
  doi = {10.1109/ACSD.2013.15},
  abstract = {We present a methodology for fault diagnosis in
    concurrent, partially observable systems with additional fairness
    constraints. In this weak diagnosis, one asks whether a concurrent
    chronicle of observed events allows to determine that a
    non-observable fault will inevitably occur, sooner or later, on
    any maximal system run compatible with the observation. The
    approach builds on strengths and techniques of unfoldings of safe
    Petri nets, striving to compute a compact prefix of the unfolding
    that carries sufficient information for the diagnosis
    algorithm. Our work extends and generalizes the unfolding-based
    diagnosis approaches by Benveniste \textit{et~al.} as well as
    Esparza and Kern. Both of these focused mostly on the use of
    sequential observations, in particular did not exploit the
    capacity of unfoldings to reveal inevitable occurrences of
    concurrent or future events studied by Balaguer
    \textit{et~al.}. Our diagnosis method captures such indirect,
    revealed dependencies. We~develop theoretical foundations and an
    algorithmic solution to the diagnosis problem, and present a SAT
    solving method for practical diagnosis with our approach.}
}
@article{HKS-tcs13,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Haar, Stefan and Kern, Christian and Schwoon, Stefan},
  title = {Computing the Reveals Relation in Occurrence Nets},
  year = 2013,
  month = jul,
  volume = 493,
  pages = {66-79},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/HKS-tcs13.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HKS-tcs13.pdf},
  doi = {10.1016/j.tcs.2013.04.028},
  abstract = {Petri net unfoldings are a useful tool to tackle state-space
    explosion in verification and related tasks. Moreover, their structure
    allows to access directly the relations of causal precedence, concurrency,
    and conflict between events. Here, we explore the data structure further,
    to determine the following relation: event~\(a\) is said to reveal
    event~\(b\) iff the occurrence of~\(a\) implies that~\(b\) inevitably
    occurs, too, be it before, after, or concurrently with~\(a\). Knowledge of
    reveals facilitates in particular the analysis of partially observable
    systems, in the context of diagnosis, testing, or verification; it can
    also be used to generate more concise representations of behaviours via
    abstractions. The reveals relation was previously introduced in the
    context of fault diagnosis, where it was shown that the reveals relation
    was decidable: for a given pair~\(a,b\) in the unfolding~\(U\) of a safe
    Petri net~\(N\), a finite prefix~\(P\) of~\(U\) is sufficient to decide
    whether or not \(a\) reveals~\(b\). In this paper, we first considerably
    improve the bound on~\(|P|\). We then show that there exists an efficient
    algorithm for computing the relation on a given prefix. We have
    implemented the algorithm and report on experiments.}
}
@article{PHL-sttt14,
  publisher = {Springer},
  journal = {International Journal on Software Tools 
             for Technology Transfer},
  author = {Ponce{ }de{~}Le{\'o}n, Hern{\'a}n and Haar, Stefan and
                  Longuet, Delphine},
  title = {Model-based Testing for Concurrent Systems: Unfolding-based Test Selection},
  volume = {18},
  number = 3,
  year = {2016},
  month = jun,
  pages = {305-318},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-sttt14.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-sttt14.pdf},
  doi = {10.1007/s10009-014-0353-y},
  abstract = {Model-based testing has mainly focused on models where
    concurrency is interpreted as interleaving (like the ioco theory for
    labeled transition systems), which may be too coarse when one wants
    concurrency to be preserved in the implementation. In order to test such
    concurrent systems, we choose to use Petri nets as specifications and
    define a concurrent conformance relation named co-ioco. We present a test
    generation algorithm based on Petri net unfolding able to build a complete
    test suite w.r.t our co-ioco conformance relation. In addition we propose
    several coverage criteria that allow to select finite prefixes of an
    unfolding in order to build manageable test suites.}
}
@article{haar-mvlsc15,
  publisher = {Old City Publishing},
  journal = {Journal of Multiple-Valued Logic and Soft Computing},
  author = {Haar, Stefan},
  title = {Cyclic Ordering through Partial Orders},
  volume = {27},
  number = {2-3},
  year = 2016,
  month = sep,
  pages = {209-228},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/haar-mvlsc16.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/haar-mvlsc16.pdf},
  abstract = {The orientation problem for ternary cyclic order relations has
    been attacked in the literature from combinatorial perspectives, through
    rotations, and by connection with Petri nets. We propose here a two-fold
    characterization of orientable cyclic orders in terms of symmetries of
    partial orders as well as in terms of separating sets (cuts). The results
    are inspired by properties of non-sequential discrete processeses, but
    also apply to dense structures of any cardinality.}
}
@article{BFHP-fi14,
  publisher = {{IOS} Press},
  journal = {Fundamenta Informaticae},
  author = {Bernardinello, Luca and Ferigato, Carlo and
  	 	     Haar, Stefan and Pomello, Lucia},
  title = {Closed Sets in Occurrence Nets with Conflicts},
  volume = 133,
  number = 4,
  year = 2014,
  pages = {323-344},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHP-fi14.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHP-fi14.pdf},
  doi = {10.3233/FI-2014-1079},
  abstract = {The semantics of concurrent processes can be defined in terms of
    partially ordered sets. Occurrence nets, which belong to the family of
    Petri nets, model concurrent processes as partially ordered sets of
    occurrences of local states and local events. On the basis of the
    associated concurrency relation, a closure operator can be defined, giving
    rise to a lattice of closed sets. Extending previous results along this
    line, the present paper studies occurrence nets with forward conflicts,
    modelling families of processes. It is shown that the lattice of closed
    sets is orthomodular, and the relations between closed sets and some
    particular substructures of an occurrence net are studied. In particular,
    the paper deals with runs, modelling concurrent histories, and trails,
    corresponding to possible histories of sequential components. A~second
    closure operator is then defined by means of an iterative procedure.
    The~corresponding closed sets, here called 'dynamically closed', are shown
    to form a complete lattice, which in general is not orthocomplemented.
    Finally, it is shown that, if an occurrence net satisfies a property
    called B-density, which essentially says that any antichain meets any
    trail, then the two notions of closed set coincide, and they form a
    complete, algebraic orthomodular lattice.}
}
@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.}
}
@article{PHL-stvr14,
  publisher = {John Wiley \& Sons, Ltd.},
  journal = {Software Testing, Verification and Reliability},
  author = {Ponce{ }de{~}Le{\'o}n, Hern{\'a}n and Haar, Stefan and
                  Longuet, Delphine},
  title = {Model-Based Testing for Concurrent Systems with Labeled Event
                  Structures},
  volume = 24,
  number = 7,
  year = {2014},
  month = nov,
  pages = {558-590},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-stvr14.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-stvr14.pdf},
  doi = {10.1002/stvr.1543},
  abstract = {We propose a theoretical testing framework and a test generation
    algorithm for concurrent systems specified with true concurrency models,
    such as Petri nets or networks of automata. The semantic model of
    computation of such formalisms are labeled event structures, which allow
    to represent concurrency explicitly. We introduce the notions of strong
    and weak concurrency: strongly concurrent events must be concurrent in the
    implementation, while weakly concurrent ones may eventually be ordered.
    The ioco type conformance relations for sequential systems rely on the
    observation of sequences of actions and blockings, thus they are not
    capable of capturing and exploiting concurrency of non sequential
    behaviors. We propose an extension of \textbf{ioco} for labeled event
    structures, named \textbf{co-ioco}, allowing to deal with strong and weak
    concurrency. We~extend the notions of test cases and test execution to
    labeled event structures, and give a test generation algorithm building a
    complete test suite for \textbf{co-ioco}.}
}
@inproceedings{PHL-ictac14,
  address = {Bucharest, Romania},
  month = sep,
  year = 2014,
  volume = 8687,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Ciobanu, Gabriel and M{\'e}ry, Dominique},
  acronym = {{ICTAC}'14},
  booktitle = {{P}roceedings of the 11th {I}nternational {C}olloquium on
	{T}heoretical {A}spects of {C}omputing ({ICTAC}'14)},
  author = {Ponce{ }de{~}Le{\'o}n, Hern{\'a}n and Haar, Stefan and
                  Longuet, Delphine},
  title = {Distributed testing of concurrent systems: vector clocks to
                  the rescue},
  pages = {369-387},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-ictac14.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PHL-ictac14.pdf},
  doi = {10.1007/978-3-319-10882-7_22},
  abstract = {The ioco relation has become a standard in model-based
    conformance testing. The co-ioco conformance relation is an extension of
    this relation to concurrent systems specified with true-concurrency
    models. This relation assumes a global control and observation of the
    system under test, which is not usually realistic in the case of
    physically distributed systems. Such systems can be partially observed at
    each of their points of control and observation by the sequences of inputs
    and outputs exchanged with their environment. Unfortunately, in general,
    global observation cannot be reconstructed from local ones, so global
    conformance cannot be decided with local tests. We propose to append time
    stamps to the observable actions of the system under test in order to
    regain global conformance from local testing.}
}
@inproceedings{GHKS-acsd14,
  address = {Tunis, Tunisia},
  month = jun,
  year = 2014,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{ACSD}'14},
  booktitle = {{P}roceedings of the 14th {I}nternational
               {C}onference on {A}pplication of {C}oncurrency
               to {S}ystem {D}esign
               ({ACSD}'14)},
  author = {Germanos, Vasileios and Haar, Stefan
                and Khomenko, Victor and Schwoon, Stefan},
  title = {Diagnosability under Weak Fairness},
  pages = {132-141},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/GHKS-acsd14.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GHKS-acsd14.pdf},
  doi = {10.1109/ACSD.2014.9},
  abstract = {In partially observed Petri nets, diagnosis is the
                task of detecting whether or not the given sequence of
                observed labels indicates that some unobservable fault
                has occurred. Diagnosability is an associated property of
                the Petri net, stating that in any possible execution an
                occurrence of a fault can eventually be diagnosed.\par In this
                paper we consider diagnosability under the weak fairness (WF)
                assumption, which intuitively states that no transition from
                a given set can stay enabled forever---it~must eventually
                either fire or be disabled. We show that a previous approach
                to WF-diagnosability in the literature has a major flaw, and
                present a corrected notion. Moreover, we present an efficient
                method for verifying WF-diagnosability based on a reduction
                to LTL-X model checking. An important advantage of this
                method is that the LTL-X formula is fixed---in~particular,
                the WF assumption does not have to be expressed as a part of
                it (which would make the formula length proportional to the
                size of the specification), but rather the ability of existing
                model checkers to handle weak fairness directly is exploited.}
}
@inproceedings{BFHHH-fossacs14,
  address = {Grenoble, France},
  month = apr,
  year = 2014,
  volume = {8412},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Muscholl, Anca},
  acronym = {{FoSSaCS}'14},
  booktitle = {{P}roceedings of the 17th {I}nternational
               {C}onference on {F}oundations of {S}oftware {S}cience
               and {C}omputation {S}tructures
               ({FoSSaCS}'14)},
  author = {Bertrand, Nathalie and Fabre, {\'E}ric and Haar, Stefan and
                  Haddad, Serge and H{\'e}lou{\"e}t, Lo{\"\i}c},
  title = {Active diagnosis for probabilistic systems},
  pages = {29-42},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHHH-fossacs14.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFHHH-fossacs14.pdf},
  doi = {10.1007/978-3-642-54830-7_4},
  abstract = {The diagnosis problem amounts to deciding whether some specific
    {"}fault{"} event occurred or not in a system, given the observations
    collected on a run of this system. This system is then diagnosable if the
    fault can always be detected, and the active diagnosis problem consists in
    controlling the system in order to ensure its diagnosability. We consider
    here a stochastic framework for this problem: once a control is selected,
    the system becomes a stochastic process. In this setting, the active
    diagnosis problem consists in deciding whether there exists some
    observation-based strategy that makes the system diagnosable with
    probability one. We prove that this problem is EXPTIME-complete, and that
    the active diagnosis strategies are belief-based. The safe active
    diagnosis problem is similar, but aims at enforcing diagnosability while
    preserving a positive probability to non faulty runs, i.e. without
    enforcing the occurrence of a fault. We prove that this problem requires
    non belief-based strategies, and that it is undecidable. However, it
    belongs to NEXPTIME when restricted to belief-based strategies. Our work
    also refines the decidability/undecidability frontier for verification
    problems on partially observed Markov decision processes.}
}
@article{GHKS-tecs15,
  publisher = {ACM Press},
  journal = {ACM Transactions in Embedded Computing Systems},
  author = {Germanos, Vasileios and Haar, Stefan
                and Khomenko, Victor and Schwoon, Stefan},
  title = {Diagnosability under Weak Fairness},
  volume = 14,
  number = {4:69},
  nopages = {},
  month = dec,
  year = 2015,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/GHKS-tecs15.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GHKS-tecs15.pdf},
  doi = {10.1145/2832910},
  abstract = {In partially observed Petri nets, diagnosis is the task of
    detecting whether or not the given sequence of observed labels indicates
    that some unobservable fault has occurred. Diagnosability is an associated
    property of the Petri net, stating that in any possible execution an
    occurrence of a fault can eventually be diagnosed.\par
    In this paper we consider diagnosability under the weak fairness (WF)
    assumption, which intuitively states that no transition from a given set
    can stay enabled forever---it~must eventually either fire or be disabled.
    We show that a previous approach to WF-diagnosability in the literature
    has a major flaw, and present a corrected notion. Moreover, we present an
    efficient method for verifying WF-diagnosability based on a reduction to
    LTL-X model checking. An~important advantage of this method is that the
    LTL-X formula is fixed---in~particular, the WF assumption does not have to
    be expressed as a part of it (which would make the formula length
    proportional to the size of the specification), but rather the ability of
    existing model checkers to handle weak fairness directly is exploited.}
}
@inproceedings{BHHHS-cdc15,
  address = {Osaka, Japan},
  month = dec,
  year = 2015,
  publisher = {{IEEE} Control System Society},
  noeditor = {},
  acronym = {{CDC}'15},
  booktitle = {{P}roceedings of the 54th {IEEE} {C}onference on
                  {D}ecision and {C}ontrol ({CDC}'15)},
  author = {B{\"o}hm, Stanislav and Haar, Stefan and Haddad, Serge and
                  Hofman, Piotr and Schwoon, Stefan},
  title = {Active Diagnosis with Observable Quiescence},
  pages = {1663-1668},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHHHS-cdc15.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHHHS-cdc15.pdf},
  doi = {10.1109/CDC.2015.7402449},
  abstract = {Active diagnosis of a discrete-event system consists in
    controlling the system such that faults can be detected. Here we extend
    the framework of active diagnosis by introducing modalities for actions
    and states and a new capability for the controller, namely observing that
    the system is quiescent. We design a game-based construction for both the
    decision and the synthesis problems that is computationally optimal.
    Furthermore we prove that the size and the delay provided by the active
    diagnoser (when it exists) are almost optimal.}
}
@inproceedings{adhs15-HT,
  address = {Atlanta, Georgia, USA},
  month = oct,
  year = 2015,
  number = 27,
  volume = 48,
  series = {IFAC-PapersOnLine},
  publisher = {Elsevier Science Publishers},
  editor = {Lennartson, Bengt and Tabuada, Paulo},
  acronym = {{ADHS}'15},
  booktitle = {{P}roceedings of the 5th {IFAC} {C}onference on {A}nalysis and
                  {D}esign of {H}ybrid {S}ystems ({ADHS}'15)},
  author = {Haar, Stefan and Theissing, Simon},
  title = {A~Hybrid-Dynamical Model for Passenger-flow in Transportation
                   Systems},
  pages = {236-241},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/adhs15-HT.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/adhs15-HT.pdf},
  doi = {10.1016/j.ifacol.2015.11.181},
  abstract = {In a network with different transportation modes, or multimodal
    public transportation system (MPTS), modes are linked among one another
    not by resources or infrastructure elements---which are not shared, e.g.,
    between different metro lines---but by the flow of passengers between
    them. Now, the movements of passengers are steered by the destinations
    that individual passengers have, and by which they can be grouped into
    trip profiles. To use the strength of fluid dynamics, we therefore
    introduce a multiphase hybrid Petri net model, in which the vehicle
    dynamics is rendered by individual tokens moving in an infrastructure net,
    while passenger quantities are given as vectors---whose components
    correspond to trip profiles---and evolve at stations according to fluid
    dynamics. This model is intended as a building block for obtaining
    supervisory control, via transport operator actions, to mitigate
    congestion.}
}
@inproceedings{PRCHH-atva15,
  address = {Shanghai, China},
  month = oct,
  year = {2015},
  volume = {9364},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Finkbeiner, Bernd and Pu, Geguang and Zhang, Lijun},
  acronym = {{ATVA}'15},
  booktitle = {{P}roceedings of the 13th {I}nternational
               {S}ymposium on {A}utomated {T}echnology
               for {V}erification and {A}nalysis
               ({ATVA}'15)},
  author = {Ponce{ }de{~}Le{\'o}n, Hern{\'a}n and Rodr{\'\i}guez,
                  C{\'e}sar and Carmona, Josep and Heljanko, Keijo and Haar, Stefan},
  title = {Unfolding-Based Process Discovery},
  pages = {},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/PRCHH-atva15.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/PRCHH-atva15.pdf},
  doi = {10.1007/978-3-319-24953-7_4},
  abstract = {This paper presents a novel technique for process discovery. In
    contrast to the current trend, which only considers an event log for
    discovering a process model, we assume two additional inputs: an
    independence relation on the set of logged activities, and a collection of
    negative traces. After deriving an intermediate net unfolding from them,
    we perform a controlled folding giving rise to a Petri net which contains
    both the input log and all independence-equivalent traces arising from~it.
    Remarkably, the derived Petri net cannot execute any trace from the
    negative collection. The entire chain of transformations is fully
    automated. A tool has been developed and experimental results are provided
    that witness the significance of the contribution of this paper.}
}
@inproceedings{HPRV-ppdp15,
  address = {Siena, Italy},
  month = jul,
  year = 2015,
  publisher = {ACM Press},
  editor = {Albert, Elvira},
  acronym = {{PPDP}'15},
  booktitle = {{P}roceedings of the 17th {I}nternational
  	   {C}onference on {P}rinciples and {P}ractice of {D}eclarative 
	   {P}rogramming ({PPDP}'15)},
  author = {Haar, Stefan and Perchy, Salim and Rueda, Camilo and
                  Valencia, Franck},
  title = {An Algebraic View of Space{{\slash}}Belief and
                  Extrusion{{\slash}}Utterance for
                  Concurrency{{\slash}}Epistemic Logic},
  pages = {161-172},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/HPRV-ppdp15.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HPRV-ppdp15.pdf},
  doi = {10.1007/978-3-319-19488-2_6},
  abstract = {We enrich spatial constraint systems with operators to specify
    information and processes moving from a space to another. We shall refer
    to these news structures as spatial constraint systems with extrusion. We
    shall investigate the properties of this new family of constraint systems
    and illustrate their applications. From a computational point of view the
    new operators provide for process\slash information extrusion, a central
    concept in formalisms for mobile communication. From an epistemic point of
    view extrusion corresponds to a notion we shall call utterance; a~piece of
    information that an agent communicates to others but that may be
    inconsistent with the agent's beliefs. Utterances can then be used to
    express instances of epistemic notions, which are common place in social
    media, such as hoaxes or intentional lies. Spatial constraint systems with
    extrusion can be seen as complete Heyting algebras equipped with maps to
    account for spatial and epistemic specifications.}
}
@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.}
}
@article{HHMS-jcss16,
  publisher = {Elsevier Science Publishers},
  journal = {Journal of Computer and System Sciences},
  author = {Stefan Haar and
               Serge Haddad and
               Tarek Melliti and
               Stefan Schwoon},
  title = {Optimal constructions for active diagnosis},
  pages = {101-120},
  volume = {83},
  number = {1},
  year = {2017},
  doi = {10.1016/j.jcss.2016.04.007},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HHMS-jcss16.pdf},
  abstract = {Diagnosis is the task of detecting fault occurrences in a partially observed sys- tem. Depending on the possible observations, a discrete-event system may be diagnosable or not. Active diagnosis aims at controlling the system to render it diagnosable. Past research has proposed solutions for this problem, but their complexity remains to be improved. Here, we solve the decision and synthesis problems for active diagnosability, proving that (1) our procedures are optimal with respect to computational complexity, and (2) the memory required for our diagnoser is minimal. We then study the delay between a fault occurrence and its detection by the diagnoser. We construct a memory-optimal diagnoser whose delay is at most twice the minimal delay, whereas the memory required to achieve optimal delay may be highly greater. We also provide a solution for parametrized active diagnosis, where we automatically construct the most permissive controller respecting a given delay.}
}
@inproceedings{MHP-HSB16,
  address = {Grenoble France},
  month = oct,
  optvolume = 9957,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  opteditor = {Cinquemani, Eugenio and
               Donz{\'{e}, Alexandre}},
  acronym = {{HSB}'16},
  booktitle = {{P}roceedings of the 5th
           {I}nternational {W}orkshop on 
           {H}ybrid {S}ystems {B}iology},
  author = {Mandon, Hugues and Haar, Stefan and Paulev{\'e}, Lo{\"i}c},
  title = {{Relationship between the Reprogramming Determinants of Boolean Networks and their Interaction Graph}},
  pages = {113-127},
  year = {2016},
  doi = {10.1007/978-3-319-47151-8_8},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/MHP-HSB16.pdf},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/MHP-HSB16.pdf},
  abstract = {In this paper, we address the formal characterization of tar- gets triggering cellular trans-differentiation in the scope of Boolean net- works with asynchronous dynamics. Given two fixed points of a Boolean network, we are interested in all the combinations of mutations which allow to switch from one fixed point to the other, either possibly, or in- evitably. In the case of existential reachability, we prove that the set of nodes to (permanently) flip are only and necessarily in certain connected components of the interaction graph. In the case of inevitable reachabil- ity, we provide an algorithm to identify a subset of possible solutions.}
}
@inproceedings{KSHP-sasb16,
  address = {Edinburgh, UK},
  month = sep,
  missingnumber = {2},
  missingvolume = {},
  series = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier Science Publishers},
  acronym = {{SASB}'16},
  booktitle = {{P}roceedings of {T}he {S}eventh {I}nternational {W}orkshop on {S}tatic {A}nalysis and {S}ystems {B}iology (SASB 2016)},
  title = {{Unfolding of Parametric Logical Regulatory Networks}},
  author = {Kolc{\'a}k, Juraj and {\v S}afr{\'a}nek, David and Haar, Stefan and Paulev{\'e}, Lo{\"i}c},
  year = {2016},
  note = {To appear},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KSHP-SASB16.pdf},
  url = {https://hal.archives-ouvertes.fr/hal-01354109},
  abstract = {In systems biology, models of cellular regulatory processes such as gene regulatory networks or signalling pathways are crucial to understanding the behaviour of living cells. Available biological data are however often insufficient for full model specification. In this paper, we focus on partially specified models where the missing information is abstracted in the form of parameters. We introduce a novel approach to analysis of parametric logical regulatory networks addressing both sources of combinatoric explosion native to the model. First, we introduce a new compact representation of admissible parameters using Boolean lattices. Then, we define the unfolding of parametric regulatory networks. The resulting structure provides a partial- order reduction of concurrent transitions, and factorises the common transitions among the concrete models. A comparison is performed against state-of-the-art approaches to parametric model analysis.}
}
@inproceedings{HT-pasm16,
  address = {M{\"u}nster, Germany},
  month = apr,
  year = 2016,
  volume = {327},
  series = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier Science Publishers},
  editor = {Haverkort, Boudewijn and Knottenbelt, William and Remke, Anne and Thomas, Nigel},
  booktitle = {{P}roceedings of the 8th {I}nternational {W}orkshop on {P}ractical
                  {A}pplications of {S}tochastic {M}odelling ({PASM}'16)},
  author = {Haar, Stefan and Theissing, Simon},
  title = {Forecasting Passenger Loads in Transportation Networks},
  pages = {49-69},
  url = {https://hal.inria.fr/hal-01259585},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HT-pasm16.pdf},
  doi = {10.1016/j.entcs.2016.09.023},
  abstract = {This work is part of an ongoing effort to understand the
    dynamics of passenger loads in modern, multimodal transportation
    networks (TNs) and to mitigate the impact of perturbations. The
    challenge is that the percentage of passengers at any given point of
    the TN that have a certain destination, i.e. their distribution over
    different trip profiles, is unknown. We introduce a stochastic
    hybrid automaton model for multimodal TNs that allows to compute how
    such probabilistic load vectors are propagated through the TN, and
    develop a computation strategy for forecasting the network's load a
    certain time into the future.}
}
@techreport{HT-hal16,
  author = {Haar, Stefan and Theissing, Simon},
  title = {A~Passenger-centric Multi-agent System Model for
                  Multimodal Public Transportation},
  institution = {HAL-inria},
  number = {hal-01322956},
  month = may,
  year = {2016},
  type = {Research Report},
  url = {https://hal.inria.fr/hal-01322956},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HT-hal16.pdf},
  note = {12~pages},
  abstract = {If we want to understand how perturbations spread across a
    multi-modal public transportation system, we have to include
    passenger flows into the model and the analysis. Indeed, in general
    no two different lines in such a system are physically connected
    directly, or share tracks or other resources. Rather, they are
    connected by passengers changing lines and thus transmit
    perturbations from one line or mode to another. We present a formal
    passenger-centric multi-agent system model that can capture
    (i)~individual and possibly multi-modal trip profiles with branches
    resulting from different decision outcomes, (ii)~the~movement of
    fixed-route operated transportation means, and (iii)~in-vehicle and
    in-station capacity constraints. The model is based on a
    nets-within-nets approach with Petri nets as the basic building
    entities. Thus, it has a convenient graphical representation, and
    the possibility of execution.}
}
@inproceedings{HT-qest16,
  address = {Qu{\'e}bec City, Canada},
  month = aug,
  year = 2016,
  volume = {9826},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Agha, Gul and Van{~}Houdt, Benny},
  acronym = {{QEST}'16},
  booktitle = {{P}roceedings of the 13th {I}nternational
               {C}onference on {Q}uantitative 
               {E}valuation of {S}ystems
               ({QEST}'16)},
  author = {Haar, Stefan and Theissing, Simon},
  title = {Decoupling Passenger Flows for Improved Load Prediction},
  pages = {364-379},
  url = {https://hal.inria.fr/hal-01330136},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HT-qest16.pdf},
  doi = {10.1007/978-3-319-43425-4_24},
  abstract = {This paper continues our work on perturbation analysis of
    multimodal transportation networks~(TNs) by means of a stochastic
    hybrid automaton~(SHA) model. We focus here on the approximate
    computation , in particular on the major bottleneck consisting in
    the high dimensionality of systems of stochastic differential
    balance equations (SDEs) that define the continuous passenger-flow
    dynamics in the different modes of the SHA model. In fact, for every
    pair of a mode and a station, one system of coupled SDEs relates the
    passenger loads of all discrete points such as platforms considered
    in this station, and all vehicles docked to it, to the passenger
    flows in between. In general, such an SDE system has many
    dimensions, which makes its numerical computation and thus the
    approximate computation of the SHA model intractable. We show how
    these systems can be canonically replaced by lower-dimensional ones,
    by decoupling the passenger flows inside every mode from one
    another. We prove that the resulting approximating passenger-flow
    dynamics converges to the original one, if the replacing set of
    balance equations set up for all decoupled passenger flows
    communicate their results among each other in vanishing time
    intervals.}
}
@inproceedings{HT-acc16,
  address = {Boston, Massachusetts, USA},
  month = jul,
  year = 2016,
  publisher = {{IEEE} Control System Society},
  acronym = {{ACC}'16},
  booktitle = {{P}roceedings of the 35th {A}merican {C}ontrol 
	       {C}onference ({ACC}'16)},
  author = {Haar, Stefan and Theissing, Simon},
  title = {Predicting Traffic Load in Public Transportation Networks},
  pages = {821-826},
  url = {https://hal.inria.fr/hal-01329632},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HT-acc16.pdf},
  doi = {10.1109/ACC.2016.7525015},
  abstract = {This work is part of an ongoing effort to understand the
    dynamics of passenger loads in modern, multimodal transportation
    networks (TNs) and to mitigate the impact of perturbations, under
    the restrictions that the precise number of passengers in some point
    of the TN that intend to reach a certain destination (i.e. their
    distribution over different trip profiles) is unknown. We introduce
    an approach based on a stochastic hybrid automaton model for a TN
    that allows to compute how such probabilistic load vectors are
    propagated through the TN, and develop a computation strategy for
    forecasting the network's load a certain time in the future.}
}
@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{MHP-cmsb17,
  address = {Darmstadt, Germany},
  month = sep,
  year = 2017,
  volume = {10545},
  series = {Lecture Notes in Bioinformatics},
  publisher = {Springer-Verlag},
  editor = {Feret, J{\'e}r{\^o}me and Koeppl, Heinz},
  acronym = {{CMSB}'17},
  booktitle = {{P}roceedings of the 15th
           {C}onference on
           {C}omputational {M}ethods in {S}ystem {B}iology
	   ({CMSB}'17)},
  author = {Mandon, Hugues and Haar, Stefan and Paulev{\'e}, Lo{\"i}c},
  title = {{Temporal Reprogramming of Boolean Networks}},
  pages = {179-195},
  pdf = {https://hal.inria.fr/hal-01589251/document},
  doi = {10.1007/978-3-319-67471-1\_11},
  abstract = {Cellular reprogramming, a technique that opens huge opportunities in modern and regenerative medicine, heavily relies on identifying key genes to perturb. Most of computational methods focus on finding mutations to apply to the initial state in order to control which attractor the cell will reach. However, it has been shown, and is proved in this article, that waiting between the perturbations and using the transient dynamics of the system allow new reprogramming strategies. To identify these temporal perturbations, we consider a qualitative model of regulatory networks, and rely on Petri nets to model their dynamics and the putative perturbations. Our method establishes a complete characterization of temporal perturbations, whether permanent (mutations) or only temporary, to achieve the existential or inevitable reachability of an arbitrary state of the system. We apply a prototype implementation on small models from the literature and show that we are able to derive temporal perturbations to achieve trans-differentiation.}
}
@inproceedings{HPV-icsc17,
  address = {San Diego, CA, USA},
  month = jan,
  volume = 11,
  series = {IEEE ICSC},
  publisher = {{IEEE} Press},
  todoeditor = {D?Auria, Daniela and Liu, Jianquan and Pilato, Giovanni},
  acronym = {{ICSC}'17},
  booktitle = {{P}roceedings of the 11th International Conference on Semantic Computing	({ICSC}'17)},
  author = {Haar, Stefan and Perchy, Salim and Valencia, Frank},
  title = {{D-SPACES: Implementing Declarative Semantics for Spatially Structured Information}},
  pages = {227-233},
  year = {2017},
  doi = {10.1109/ICSC.2017.34},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HPV-icsc17.pdf},
  url = {https://hal.inria.fr/hal-01328189},
  abstract = {We introduce in this paper D-SPACES, an implementation of constraint systems with space and extrusion operators. Constraint systems are algebraic models that allow for a semantic language-like representation of information in systems where the concept of space is a primary structural feature. We give this information mainly an epistemic interpretation and consider various agents as entities acting upon it. D-SPACES is coded as a c++11 library providing implementations for constraint systems, space functions and extrusion functions. The interfaces to access each implementation are minimal and thoroughly documented. D-SPACES also provides property-checking methods as well as an implementation of a specific type of constraint systems (a boolean algebra). This last implementation serves as an entry point for quick access and proof of concept when using these models. Furthermore, we offer an illustrative example in the form of a small social network where users post their beliefs and utter their opinions.}
}
@article{GHPRV-jlamp17,
  publisher = {Elsevier Science Publishers},
  journal = {Journal of Logic and Algebraic Methods in Programming},
  author = {Guzm{\'a}n, Michell and Haar, Stefan and Perchy, Salim and Rueda, Camilo and Valencia, Frank},
  title = {{Belief, Knowledge, Lies and Other Utterances in an Algebra for Space and Extrusion}},
  volume = {86},
  number = {1},
  year = {2017},
  pages = {107-133},
  doi = {10.1016/j.jlamp.2016.09.001},
  month = jan,
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GHPRV-jlamp17.pdf},
  url = {https://hal.inria.fr/hal-01257113},
  abstract = {The notion of constraint system (cs) is central to declarative formalisms from concurrency theory such as process calculi for concurrent constraint programming (ccp). Constraint systems are often represented as lattices: their elements, called constraints, represent partial information and their order corresponds to entailment. Recently a notion of n-agent spatial cs was introduced to represent information in concurrent constraint programs for spatially distributed multi-agent systems. From a computational point of view a spatial constraint system can be used to specify partial information holding in a given agent's space (local information). From an epistemic point of view a spatial cs can be used to specify information that a given agent considers true (beliefs). Spatial constraint systems, however, do not provide a mechanism for specifying the mobility of information/processes from one space to another. Information mobility is a fundamental aspect of concurrent systems. In this article we develop the theory of spatial constraint systems with operators to specify information and processes moving from a space to another. We shall investigate the properties of this new family of constraint systems and illustrate their applications. From a computational point of view the new operators provide for process/information extrusion, a central concept in formalisms for mobile communication. From an epistemic point of view extrusion corresponds I to a notion we shall call utterance; a piece of information that an agent communicate to others but that may be inconsistent with the agent's beliefs. Utterances can then be used to express instances of epistemic notions such as hoaxes or intentional lies which are common place in social media. Spatial constraint system can express the epistemic notion of belief by means of space functions that specify local information. We shall also show that spatial constraint can also express the epistemic notion of knowledge by means of a derived spatial operator that specifies global information.}
}
@inproceedings{BHSS-pn17,
  address = {Zaragoza, Spain},
  month = jun,
  volume = {10258},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {van der Aalst, Wifred and Best, Eike},
  acronym = {{PETRI~NETS}'17},
  booktitle = {{P}roceedings of the 38th
               {I}nternational {C}onference on
               {A}pplications and {T}heory of {P}etri {N}ets
               ({PETRI~NETS}'17)},
  author = {B{\'e}rard, B{\'e}atrice and Haar, Stefan and
                  Schmitz, Sylvain and Schwoon, Stefan},
  title = {The Complexity of Diagnosability and Opacity
                  Verification for {P}etri Nets},
  pages = {200-220},
  year = {2017},
  doi = {10.1007/978-3-319-57861-3_13},
  url = {https://hal.inria.fr/hal-01484476},
  abstract = {Diagnosability and opacity are two well-studied problems in discrete-event systems.  We revisit these two problems with respect to expressiveness and complexity issues.  We first relate different notions of diagnosability and opacity.  We consider in particular fairness issues and extend the definition of Germanos et al. [ACM TECS, 2015] of weakly fair diagnosability for safe Petri nets to general Petri nets and to opacity questions.  Second, we provide a global picture of complexity results for the verification of diagnosability and opacity.  We show that diagnosability is NL-complete for finite state systems, PSPACE-complete for safe Petri nets (even with fairness), and EXPSPACE-complete for general Petri nets without fairness, while non diagnosability is inter-reducible with reachability when fault events are not weakly fair.  Opacity is ESPACE-complete for safe Petri nets (even with fairness) and undecidable for general Petri nets already without fairness.}
}
@inproceedings{HKP-vmcai2019,
  address = {Cascais/Lisbon, Portugal},
  month = jan,
  year = 2019,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Enea, Constantin and Piskac, Ruzica},
  acronym = {{VMCAI}'19},
  booktitle = {{P}roceedings of the 20th {I}nternational {C}onference on
   	       {V}erification, {M}odel {C}hecking and {A}bstract {I}nterpretation
	       ({VMCAI}'19)},
  author = {Haar, Stefan and Kolc{\'a}k, Juraj and Paulev{\'e}, Lo{\"i}c},
  title = {{Combining Refinement of Parametric Models with Goal-Oriented Reduction of Dynamics}},
  pages = {555-576},
  url = {https://hal.archives-ouvertes.fr/hal-01940174/},
  pdf = {https://hal.archives-ouvertes.fr/hal-01940174/file/manuscript.pdf},
  abstract = {Parametric models abstract part of the specification of dynamical models by integral parameters. They are for example used in computational systems biology, notably with parametric regulatory networks, which specify the global architecture (interactions) of the networks, while parameterising the precise rules for drawing the possible temporal evolutions of the states of the components. A key challenge is then to identify the discrete parameters corresponding to concrete models with desired dynamical properties. This paper addresses the restriction of the abstract execution of parametric regulatory (discrete) networks by the means of static analysis of reachability properties (goal states). Initially defined at the level of concrete parameterised models, the goal-oriented reduction of dynamics is lifted to parametric networks, and is proven to preserve all the minimal traces to the specified goal states. It results that one can jointly perform the refinement of parametric networks (restriction of domain of parameters) while reducing the necessary transitions to explore and preserving reachability properties of interest.}
}
@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.}
}
@inproceedings{BHL-fsttcs18,
  address = {Ahmedabad, India},
  month = dec,
  year = 2018,
  volume = {122},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Sumit Ganguly and Paritosh Pandya},
  acronym = {{FSTTCS}'18},
  booktitle = {{P}roceedings of the 38th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'18)},
  author = {B{\'e}atrice B{\'e}rard and Stefan Haar and Lo{\"i}c H{\'e}lou{\"e}t},
  title = {Hyper Partial Order Logic},
  pages = {20:1-20:21},
  url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9919},
  pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/9919/pdf/LIPIcs-FSTTCS-2018-20.pdf},
  doi = {10.4230/LIPIcs.FSTTCS.2018.20},
  abstract = {We define HyPOL, a local hyper logic for partial order models, expressing properties of sets of runs. These properties depict shapes of causal dependencies in sets of partially ordered executions, with similarity relations defined as isomorphisms of past observations. Unsurprisingly, since comparison of projections are included, satisfiability of this logic is undecidable. We then address model checking of HyPOL and show that, already for safe Petri nets, the problem is undecidable. Fortunately, sensible restrictions of observations and nets allow us to bring back model checking of HyPOL to a decidable problem, namely model checking of MSO on graphs of bounded treewidth.}
}
@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.}
}
@article{KSHP-tcs19,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Kolc{\'a}k, Juraj and {\v S}afr{\'a}nek, David and Haar, Stefan and Paulev{\'e}, Lo{\"i}c},
  title = {{Parameter Space Abstraction and Unfolding Semantics of Discrete Regulatory Networks}},
  volume = {765},
  year = {2019},
  pages = {120-144},
  doi = {10.1016/j.tcs.2018.03.009},
  pdf = {https://hal.archives-ouvertes.fr/hal-01734805/document},
  url = {https://hal.archives-ouvertes.fr/hal-01734805/},
  abstract = {The modelling of discrete regulatory networks combines a graph specifying the pairwise influences between the variables of the system, and a parametrisation from which can be derived a discrete transition system. Given the influence graph only, the exploration of admissible parametrisations and the behaviours they enable is computationally demanding due to the combinatorial explosions of both parametrisation and reachable state space. This article introduces an abstraction of the parametrisation space and its refinement to account for the existence of given transitions, and for constraints on the sign and observability of influences. The abstraction uses a convex sub-lattice containing the concrete parametrisation space specified by its infimum and supremum parametrisations. It is shown that the computed abstractions are optimal, i.e., no smaller convex sublattice exists. Although the abstraction may introduce over-approximation, it has been proven to be conservative with respect to reachability of states. Then, an unfolding semantics for Parametric Regulatory Networks is defined, taking advantage of concurrency between transitions to provide a compact representation of reachable transitions. A prototype implementation is provided: it has been applied to several examples of Boolean and multi-valued networks, showing its tractability for networks with numerous components.}
}
@article{BHSS-fi18,
  publisher = {{IOS} Press},
  journal = {Fundamenta Informaticae},
  author = {B{\'e}atrice B{\'e}rard and Stefan Haar and Sylvain Schmitz and Stefan Schwoon},
  title = {{The Complexity of Diagnosability and Opacity Verification for Petri Nets}},
  volume = 161,
  number = 4,
  year = 2018,
  pages = {317-349},
  doi = {10.3233/FI-2018-1706},
  url = {https://hal.inria.fr/hal-01852119},
  abstract = {Diagnosability and opacity are two well-studied problems in discrete-event systems. We revisit these two problems with respect to expressiveness and complexity issues.
\par
We first relate different notions of diagnosability and opacity. We consider in particular fairness issues and extend the definition of Germanos et al. [ACM TECS, 2015] of weakly fair diagnosability for safe Petri nets to general Petri nets and to opacity questions.
\par
Second, we provide a global picture of complexity results for the verification of diagnosability and opacity. We show that diagnosability is NL-complete for finite state systems, PSPACE-complete for safe convergent Petri nets (even with fairness), and EXPSPACE-complete for general Petri nets without fairness, while non diagnosability is inter-reducible with reachability when fault events are not weakly fair. Opacity is ESPACE-complete for safe Petri nets (even with fairness) and undecidable for general Petri nets already without fairness.}
}
@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{MSHPP-cmsb19,
  address = {Trieste, Italy},
  month = sep,
  volume = {11773},
  series = {Lecture Notes in Bioinformatics},
  publisher = {Springer-Verlag},
  editor = {Luca Bortolussi and Guido Sanguinetti},
  acronym = {{CMSB}'19},
  booktitle = {{P}roceedings of the 17th
           {C}onference on
           {C}omputational {M}ethods in {S}ystem {B}iology
	   ({CMSB}'19)},
  author = {Mandon, Hugues and Su, Cui and Haar, Stefan and Pang, Jun and Paulev{\'e}, Lo{\"i}c},
  title = {Sequential Reprogramming of Boolean Networks Made Practical},
  pages = {3-19},
  doi = {10.1007/978-3-030-31304-3_1},
  year = 2019,
  abstract = {We address the sequential reprogramming of gene regulatory networks modelled as Boolean networks. We develop an attractor-based sequential reprogramming method to compute all sequential reprogramming paths from a source attractor to a target attractor, where only attractors of the network are used as intermediates. Our method is more practical than existing reprogramming methods as it incorporates several practical constraints: (1) only biologically observable states, viz. attractors, can act as intermediates; (2) certain attractors, such as apoptosis, can be avoided as intermediates; (3) certain nodes can be avoided to perturb as they may be essential for cell survival or difficult to perturb with biomolecular techniques; and (4) given a threshold \(k\), all sequential reprogramming paths with no more than \(k\) perturbations are computed. We compare our method with the minimal one-step reprogramming and the minimal sequential reprogramming on a variety of biological networks. The results show that our method can greatly reduce the number of perturbations compared to the one-step reprogramming, while having comparable results with the minimal sequential reprogramming. Moreover, our implementation is scalable for networks of more than 60 nodes.}
}
@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.}
}
@article{MSPPHP-ipl19,
  publisher = {ACM Press},
  journal = {IEEE/ACM Transaction on Computational Biology and Bioinformatics},
  author = {Mandon, Hugues and Su, Cui and Pang, Jun and Paul, Soumya and Haar, Stefan and Paulev{\'e}, Lo{\"i}c},
  title = {Algorithms for the Sequential Reprogramming of Boolean Networks},
  volume = {16},
  number = {5},
  pages = {1610--1619},
  year = 2019,
  pdf = {https://hal.archives-ouvertes.fr/hal-02113864/file/main.pdf},
  url = {https://hal.archives-ouvertes.fr/hal-02113864}
}
@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{HPS-cmsb20,
  address = {held online},
  month = sep,
  volume = {12314},
  series = {Lecture Notes in Bioinformatics},
  publisher = {Springer-Verlag},
  editor = {Alessandro Abate and Tatjana Petrov and Verena Wolf},
  acronym = {{CMSB}'20},
  booktitle = {{P}roceedings of the 18th
           {C}onference on
           {C}omputational {M}ethods in {S}ystem {B}iology
	   ({CMSB}'20)},
  author = {Stefan Haar and Lo{\"i}c Paulev{\'e} and Stefan Schwoon},
  title = {{Drawing the Line: Basin Boundaries in Safe Petri Nets}},
  pages = {321-336},
  year = {2020},
  doi = {10.1007/978-3-030-60327-4\_17}
}
@inproceedings{HHSY-fsttcs20,
  address = {Goa, India},
  month = dec,
  volume = {182},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Nitin Saxena and Sunil Simon},
  acronym = {{FSTTCS}'20},
  booktitle = {{P}roceedings of the 40th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'20)},
  author = {Stefan Haar and Serge Haddad and Stefan Schwoon and Lina Ye},
  title = {Active Prediction for Discrete Event Systems},
  pages = {48:1--48:16},
  year = {2020},
  doi = {https://doi.org/10.4230/LIPIcs.FSTTCS.2020.48},
  pdf = {https://drops.dagstuhl.de/opus/volltexte/2020/13289/pdf/LIPIcs-FSTTCS-2020-48.pdf},
  url = {https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=13289}
}
@proceedings{DH-pn2019,
  author = {Susanna Donatelli and Stefan Haar},
  editor = {Susanna Donatelli and Stefan Haar},
  title = {Proceedings of the 40th International Conference on Application and Theory of Petri Nets and Concurrency ({PETRI NETS}'19)},
  booktitle = {Proceedings of the 40th International Conference on Application and Theory of Petri Nets and Concurrency ({Petri Nets}'19)},
  month = jun,
  series = {Lecture Notes in Computer Science},
  volume = {11522},
  publisher = {Springer},
  year = {2019},
  address = {Aachen, Germany},
  url = {https://doi.org/10.1007/978-3-030-21571-2},
  doi = {10.1007/978-3-030-21571-2}
}

This file was generated by bibtex2html 1.98.