Document

**Published in:** LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Decisiveness of infinite Markov chains with respect to some (finite or infinite) target set of states is a key property that allows to compute the reachability probability of this set up to an arbitrary precision. Most of the existing works assume constant weights for defining the probability of a transition in the considered models. However numerous probabilistic modelings require the (dynamic) weight to also depend on the current state. So we introduce a dynamic probabilistic version of counter machine (pCM). After establishing that decisiveness is undecidable for pCMs even with constant weights, we study the decidability of decisiveness for subclasses of pCM. We show that, without restrictions on dynamic weights, decisiveness is undecidable with a single state and single counter pCM. On the contrary with polynomial weights, decisiveness becomes decidable for single counter pCMs under mild conditions. Then we show that decisiveness of probabilistic Petri nets (pPNs) with polynomial weights is undecidable even when the target set is upward-closed unlike the case of constant weights. Finally we prove that the standard subclass of pPNs with a regular language is decisive with respect to a finite set whatever the kind of weights.

Alain Finkel, Serge Haddad, and Lina Ye. About Decisiveness of Dynamic Probabilistic Models. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{finkel_et_al:LIPIcs.CONCUR.2023.14, author = {Finkel, Alain and Haddad, Serge and Ye, Lina}, title = {{About Decisiveness of Dynamic Probabilistic Models}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {14:1--14:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.14}, URN = {urn:nbn:de:0030-drops-190089}, doi = {10.4230/LIPIcs.CONCUR.2023.14}, annote = {Keywords: infinite Markov chain, reachability probability, decisiveness} }

Document

Complete Volume

**Published in:** LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

LIPIcs, Volume 203, CONCUR 2021, Complete Volume

32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 1-672, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@Proceedings{haddad_et_al:LIPIcs.CONCUR.2021, title = {{LIPIcs, Volume 203, CONCUR 2021, Complete Volume}}, booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)}, pages = {1--672}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-203-7}, ISSN = {1868-8969}, year = {2021}, volume = {203}, editor = {Haddad, Serge and Varacca, Daniele}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021}, URN = {urn:nbn:de:0030-drops-143766}, doi = {10.4230/LIPIcs.CONCUR.2021}, annote = {Keywords: LIPIcs, Volume 203, CONCUR 2021, Complete Volume} }

Document

Front Matter

**Published in:** LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Front Matter, Table of Contents, Preface, Conference Organization

32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{haddad_et_al:LIPIcs.CONCUR.2021.0, author = {Haddad, Serge and Varacca, Daniele}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)}, pages = {0:i--0:xiv}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-203-7}, ISSN = {1868-8969}, year = {2021}, volume = {203}, editor = {Haddad, Serge and Varacca, Daniele}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.0}, URN = {urn:nbn:de:0030-drops-143779}, doi = {10.4230/LIPIcs.CONCUR.2021.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} }

Document

**Published in:** LIPIcs, Volume 182, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)

A central task in partially observed controllable system is to detect or prevent the occurrence of certain events called faults. Systems for which one can design a controller avoiding the faults are called actively safe. Otherwise, one may require that a fault is eventually detected, which is the task of diagnosis. Systems for which one can design a controller detecting the faults are called actively diagnosable. An intermediate requirement is prediction, which consists in determining that a fault will occur whatever the future behaviour of the system. When a system is not predictable, one may be interested in designing a controller to make it so. Here we study the latter problem, called active prediction, and its associated property, active predictability. In other words, we investigate how to determine whether or not a system enjoys the active predictability property, i.e., there exists an active predictor for the system.
Our contributions are threefold. From a semantical point of view, we refine the notion of predictability by adding two quantitative requirements: the minimal and maximal delay before the occurence of the fault, and we characterize the requirements fulfilled by a controller that performs predictions. Then we show that active predictability is EXPTIME-complete where the upper bound is obtained via a game-based approach. Finally we establish that active predictability is equivalent to active safety when the maximal delay is beyond a threshold depending on the size of the system, and we show that this threshold is accurate by exhibiting a family of systems fulfilling active predictability but not active safety.

Stefan Haar, Serge Haddad, Stefan Schwoon, and Lina Ye. Active Prediction for Discrete Event Systems. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 48:1-48:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{haar_et_al:LIPIcs.FSTTCS.2020.48, author = {Haar, Stefan and Haddad, Serge and Schwoon, Stefan and Ye, Lina}, title = {{Active Prediction for Discrete Event Systems}}, booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)}, pages = {48:1--48:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-174-0}, ISSN = {1868-8969}, year = {2020}, volume = {182}, editor = {Saxena, Nitin and Simon, Sunil}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.48}, URN = {urn:nbn:de:0030-drops-132898}, doi = {10.4230/LIPIcs.FSTTCS.2020.48}, annote = {Keywords: Automata Theory, Partially observed systems, Diagnosability, Predictability} }

Document

**Published in:** LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)

We consider opacity questions where an observation function provides
to an external attacker a view of the states along executions and
secret executions are those visiting some state from a fixed
subset. Disclosure occurs when the observer can deduce from a finite
observation that the execution is secret, the epsilon-disclosure
variant corresponding to the execution being secret with probability
greater than 1 - epsilon. In a probabilistic and non deterministic
setting, where an internal agent can choose between actions, there
are two points of view, depending on the status of this agent: the
successive choices can either help the attacker trying to disclose
the secret, if the system has been corrupted, or they can prevent
disclosure as much as possible if these choices are part of the
system design. In the former situation, corresponding to a worst
case, the disclosure value is the supremum over the strategies of
the probability to disclose the secret (maximisation), whereas in
the latter case, the disclosure is the infimum (minimisation). We
address quantitative problems (comparing the optimal value with a
threshold) and qualitative ones (when the threshold is zero or one)
related to both forms of disclosure for a fixed or finite
horizon. For all problems, we characterise their decidability status
and their complexity. We discover a surprising asymmetry: on the one
hand optimal strategies may be chosen among deterministic ones in
maximisation problems, while it is not the case for minimisation. On
the other hand, for the questions addressed here, more minimisation
problems than maximisation ones are decidable.

Béatrice Bérard, Serge Haddad, and Engel Lefaucheux. Probabilistic Disclosure: Maximisation vs. Minimisation. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 13:1-13:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{berard_et_al:LIPIcs.FSTTCS.2017.13, author = {B\'{e}rard, B\'{e}atrice and Haddad, Serge and Lefaucheux, Engel}, title = {{Probabilistic Disclosure: Maximisation vs. Minimisation}}, booktitle = {37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)}, pages = {13:1--13:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-055-2}, ISSN = {1868-8969}, year = {2018}, volume = {93}, editor = {Lokam, Satya and Ramanujam, R.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.13}, URN = {urn:nbn:de:0030-drops-83844}, doi = {10.4230/LIPIcs.FSTTCS.2017.13}, annote = {Keywords: Partially observed systems, Opacity, Markov chain, Markov decision process} }

Document

**Published in:** LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Computing steady-state distributions in infinite-state stochastic systems is in general a very difficult task. Product-form Petri nets are those Petri nets for which the steady-state distribution can be described as a natural product corresponding, up to a normalising constant, to an exponentiation of the markings. However, even though some classes of nets are known to have a product-form distribution, computing the normalising constant can be hard. The class of (closed) \Pi^3-nets has been proposed in an earlier work, for which it is shown that one can compute the steady-state distribution efficiently. However these nets are bounded. In this paper, we generalise queuing Markovian networks and closed \Pi^3-nets to obtain the class of open \Pi^3-nets, that generate infinite-state systems. We show interesting properties of these nets: (1) we prove that liveness can be decided in polynomial time, and that reachability in live \Pi^3-nets can be decided in polynomial time; (2) we show that we can decide ergodicity of such nets in polynomial time as well; (3) we provide a pseudo-polynomial time algorithm to compute the normalising constant.

Patricia Bouyer, Serge Haddad, and Vincent Jugé. Unbounded Product-Form Petri Nets. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 31:1-31:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bouyer_et_al:LIPIcs.CONCUR.2017.31, author = {Bouyer, Patricia and Haddad, Serge and Jug\'{e}, Vincent}, title = {{Unbounded Product-Form Petri Nets}}, booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)}, pages = {31:1--31:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-048-4}, ISSN = {1868-8969}, year = {2017}, volume = {85}, editor = {Meyer, Roland and Nestmann, Uwe}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.31}, URN = {urn:nbn:de:0030-drops-77957}, doi = {10.4230/LIPIcs.CONCUR.2017.31}, annote = {Keywords: Performance evaluation, infinite-state systems, Petri nets, steady-state distribution} }

Document

**Published in:** LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

In a recent work, we introduced four variants of diagnosability
(FA, IA, FF, IF) in (finite) probabilistic
systems (pLTS) depending whether one considers (1) finite or
infinite runs and (2) faulty or all runs. We studied their
relationship and established that the corresponding decision
problems are PSPACE-complete. A key ingredient of the decision
procedures was a characterisation of diagnosability by the fact that
a random run almost surely lies in an open set whose specification
only depends on the qualitative behaviour of the pLTS. Here we
investigate similar issues for infinite pLTS. We first show that
this characterisation still holds for FF-diagnosability but
with a G-delta set instead of an open set and also for IF-
and IA-diagnosability when pLTS are finitely branching. We also
prove that surprisingly FA-diagnosability cannot be
characterised in this way even in the finitely branching case. Then
we apply our characterisations for a partially observable
probabilistic extension of visibly pushdown automata (POpVPA),
yielding EXPSPACE procedures for solving diagnosability problems.
In addition, we establish some computational lower bounds and show
that slight extensions of POpVPA lead to undecidability.

Nathalie Bertrand, Serge Haddad, and Engel Lefaucheux. Diagnosis in Infinite-State Probabilistic Systems. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 37:1-37:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.CONCUR.2016.37, author = {Bertrand, Nathalie and Haddad, Serge and Lefaucheux, Engel}, title = {{Diagnosis in Infinite-State Probabilistic Systems}}, booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)}, pages = {37:1--37:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-017-0}, ISSN = {1868-8969}, year = {2016}, volume = {59}, editor = {Desharnais, Jos\'{e}e and Jagadeesan, Radha}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.37}, URN = {urn:nbn:de:0030-drops-61597}, doi = {10.4230/LIPIcs.CONCUR.2016.37}, annote = {Keywords: probabilistic systems, infinite-state systems, pushdown automata, diagnosis, partial observation} }

Document

**Published in:** LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

In discrete event systems prone to unobservable faults, a diagnoser must eventually detect fault occurrences. The diagnosability problem consists in deciding whether such a diagnoser exists. Here we investigate diagnosis for probabilistic systems modelled by partially observed Markov chains also called probabilistic labeled transition systems (pLTS). First we study different specifications of diagnosability and establish their relations both in finite and infinite pLTS. Then we analyze the complexity of the diagnosability problem for finite pLTS: we show that the polynomial time procedure earlier proposed is erroneous and that in fact for all considered specifications, the problem is PSPACE-complete. We also establish tight bounds for the size of diagnosers. Afterwards we consider the dual notion of predictability which consists in predicting that in a safe run, a fault will eventually occur. Predictability is an easier problem than diagnosability: it is NLOGSPACE-complete. Yet the predictor synthesis is as hard as the diagnoser synthesis. Finally we introduce and study the more flexible notion of prediagnosability that generalizes predictability and diagnosability.

Nathalie Bertrand, Serge Haddad, and Engel Lefaucheux. Foundation of Diagnosis and Predictability in Probabilistic Systems. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 417-429, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.FSTTCS.2014.417, author = {Bertrand, Nathalie and Haddad, Serge and Lefaucheux, Engel}, title = {{Foundation of Diagnosis and Predictability in Probabilistic Systems}}, booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)}, pages = {417--429}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-77-4}, ISSN = {1868-8969}, year = {2014}, volume = {29}, editor = {Raman, Venkatesh and Suresh, S. P.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.417}, URN = {urn:nbn:de:0030-drops-48605}, doi = {10.4230/LIPIcs.FSTTCS.2014.417}, annote = {Keywords: Partially observed systems, Diagnosis, Markov chains} }

Document

**Published in:** LIPIcs, Volume 24, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)

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. We then focus on the delay between the occurrence of a fault 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 for a diagnoser with optimal delay may be highly greater.

Stefan Haar, Serge Haddad, Tarek Melliti, and Stefan Schwoon. Optimal Constructions for Active Diagnosis. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 24, pp. 527-539, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{haar_et_al:LIPIcs.FSTTCS.2013.527, author = {Haar, Stefan and Haddad, Serge and Melliti, Tarek and Schwoon, Stefan}, title = {{Optimal Constructions for Active Diagnosis}}, booktitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)}, pages = {527--539}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-64-4}, ISSN = {1868-8969}, year = {2013}, volume = {24}, editor = {Seth, Anil and Vishnoi, Nisheeth K.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2013.527}, URN = {urn:nbn:de:0030-drops-43981}, doi = {10.4230/LIPIcs.FSTTCS.2013.527}, annote = {Keywords: Diagnosis, Control theory, Automata theory, Games.} }

X

Feedback for Dagstuhl Publishing

Feedback submitted

Please try again later or send an E-mail