12 Search Results for "Lefaucheux, Engel"

Document
DOI: 10.4230/LIPIcs.CONCUR.2022.10
Parameter Synthesis for Parametric Probabilistic Dynamical Systems and Prefix-Independent Specifications

Authors: Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Markus A. Whiteland, and James Worrell

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
We consider the model-checking problem for parametric probabilistic dynamical systems, formalised as Markov chains with parametric transition functions, analysed under the distribution-transformer semantics (in which a Markov chain induces a sequence of distributions over states). We examine the problem of synthesising the set of parameter valuations of a parametric Markov chain such that the orbits of induced state distributions satisfy a prefix-independent ω-regular property. Our main result establishes that in all non-degenerate instances, the feasible set of parameters is (up to a null set) semialgebraic, and can moreover be computed (in polynomial time assuming that the ambient dimension, corresponding to the number of states of the Markov chain, is fixed).
Cite as

Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Markus A. Whiteland, and James Worrell. Parameter Synthesis for Parametric Probabilistic Dynamical Systems and Prefix-Independent Specifications. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{baier_et_al:LIPIcs.CONCUR.2022.10,
  author =	{Baier, Christel and Funke, Florian and Jantsch, Simon and Karimov, Toghrul and Lefaucheux, Engel and Ouaknine, Jo\"{e}l and Purser, David and Whiteland, Markus A. and Worrell, James},
  title =	{{Parameter Synthesis for Parametric Probabilistic Dynamical Systems and Prefix-Independent Specifications}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{10:1--10:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.10},
  URN =		{urn:nbn:de:0030-drops-170732},
  doi =		{10.4230/LIPIcs.CONCUR.2022.10},
  annote =	{Keywords: Model checking, parametric Markov chains, distribution transformer semantics}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2022.39
Bounding the Escape Time of a Linear Dynamical System over a Compact Semialgebraic Set

Authors: Julian D'Costa, Engel Lefaucheux, Eike Neumann, Joël Ouaknine, and James Worrell

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
We study the Escape Problem for discrete-time linear dynamical systems over compact semialgebraic sets. We establish a uniform upper bound on the number of iterations it takes for every orbit of a rational matrix to escape a compact semialgebraic set defined over rational data. Our bound is doubly exponential in the ambient dimension, singly exponential in the degrees of the polynomials used to define the semialgebraic set, and singly exponential in the bitsize of the coefficients of these polynomials and the bitsize of the matrix entries. We show that our bound is tight by providing a matching lower bound.
Cite as

Julian D'Costa, Engel Lefaucheux, Eike Neumann, Joël Ouaknine, and James Worrell. Bounding the Escape Time of a Linear Dynamical System over a Compact Semialgebraic Set. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 39:1-39:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{dcosta_et_al:LIPIcs.MFCS.2022.39,
  author =	{D'Costa, Julian and Lefaucheux, Engel and Neumann, Eike and Ouaknine, Jo\"{e}l and Worrell, James},
  title =	{{Bounding the Escape Time of a Linear Dynamical System over a Compact Semialgebraic Set}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{39:1--39:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.39},
  URN =		{urn:nbn:de:0030-drops-168374},
  doi =		{10.4230/LIPIcs.MFCS.2022.39},
  annote =	{Keywords: Discrete linear dynamical systems, Program termination, Compact semialgebraic sets, Uniform termination bounds}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2021.33
On the Complexity of the Escape Problem for Linear Dynamical Systems over Compact Semialgebraic Sets

Authors: Julian D'Costa, Engel Lefaucheux, Eike Neumann, Joël Ouaknine, and James Worrell

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
We study the computational complexity of the Escape Problem for discrete-time linear dynamical systems over compact semialgebraic sets, or equivalently the Termination Problem for affine loops with compact semialgebraic guard sets. Consider the fragment of the theory of the reals consisting of negation-free ∃ ∀-sentences without strict inequalities. We derive several equivalent characterisations of the associated complexity class which demonstrate its robustness and illustrate its expressive power. We show that the Compact Escape Problem is complete for this class.
Cite as

Julian D'Costa, Engel Lefaucheux, Eike Neumann, Joël Ouaknine, and James Worrell. On the Complexity of the Escape Problem for Linear Dynamical Systems over Compact Semialgebraic Sets. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 33:1-33:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{dcosta_et_al:LIPIcs.MFCS.2021.33,
  author =	{D'Costa, Julian and Lefaucheux, Engel and Neumann, Eike and Ouaknine, Jo\"{e}l and Worrell, James},
  title =	{{On the Complexity of the Escape Problem for Linear Dynamical Systems over Compact Semialgebraic Sets}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{33:1--33:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.33},
  URN =		{urn:nbn:de:0030-drops-144734},
  doi =		{10.4230/LIPIcs.MFCS.2021.33},
  annote =	{Keywords: Discrete linear dynamical systems, Program termination, Compact semialgebraic sets, Theory of the reals}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2021.67
On Positivity and Minimality for Second-Order Holonomic Sequences

Authors: George Kenison, Oleksiy Klurman, Engel Lefaucheux, Florian Luca, Pieter Moree, Joël Ouaknine, Markus A. Whiteland, and James Worrell

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
An infinite sequence ⟨u_n⟩_n of real numbers is holonomic (also known as P-recursive or P-finite) if it satisfies a linear recurrence relation with polynomial coefficients. Such a sequence is said to be positive if each u_n ≥ 0, and minimal if, given any other linearly independent sequence ⟨v_n⟩_n satisfying the same recurrence relation, the ratio u_n/v_n → 0 as n → ∞. In this paper we give a Turing reduction of the problem of deciding positivity of second-order holonomic sequences to that of deciding minimality of such sequences. More specifically, we give a procedure for determining positivity of second-order holonomic sequences that terminates in all but an exceptional number of cases, and we show that in these exceptional cases positivity can be determined using an oracle for deciding minimality.
Cite as

George Kenison, Oleksiy Klurman, Engel Lefaucheux, Florian Luca, Pieter Moree, Joël Ouaknine, Markus A. Whiteland, and James Worrell. On Positivity and Minimality for Second-Order Holonomic Sequences. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 67:1-67:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{kenison_et_al:LIPIcs.MFCS.2021.67,
  author =	{Kenison, George and Klurman, Oleksiy and Lefaucheux, Engel and Luca, Florian and Moree, Pieter and Ouaknine, Jo\"{e}l and Whiteland, Markus A. and Worrell, James},
  title =	{{On Positivity and Minimality for Second-Order Holonomic Sequences}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{67:1--67:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.67},
  URN =		{urn:nbn:de:0030-drops-145071},
  doi =		{10.4230/LIPIcs.MFCS.2021.67},
  annote =	{Keywords: Holonomic sequences, Minimal solutions, Positivity Problem}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2021.28
The Orbit Problem for Parametric Linear Dynamical Systems

Authors: Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Florian Luca, Joël Ouaknine, David Purser, Markus A. Whiteland, and James Worrell

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

Abstract
We study a parametric version of the Kannan-Lipton Orbit Problem for linear dynamical systems. We show decidability in the case of one parameter and Skolem-hardness with two or more parameters. More precisely, consider a d-dimensional square matrix M whose entries are algebraic functions in one or more real variables. Given initial and target vectors u,v ∈ ℚ^d, the parametric point-to-point orbit problem asks whether there exist values of the parameters giving rise to a concrete matrix N ∈ ℝ^{d× d}, and a positive integer n ∈ ℕ, such that N^{n} u = v. We show decidability for the case in which M depends only upon a single parameter, and we exhibit a reduction from the well-known Skolem Problem for linear recurrence sequences, suggesting intractability in the case of two or more parameters.
Cite as

Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Florian Luca, Joël Ouaknine, David Purser, Markus A. Whiteland, and James Worrell. The Orbit Problem for Parametric Linear Dynamical Systems. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 28:1-28:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{baier_et_al:LIPIcs.CONCUR.2021.28,
  author =	{Baier, Christel and Funke, Florian and Jantsch, Simon and Karimov, Toghrul and Lefaucheux, Engel and Luca, Florian and Ouaknine, Jo\"{e}l and Purser, David and Whiteland, Markus A. and Worrell, James},
  title =	{{The Orbit Problem for Parametric Linear Dynamical Systems}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{28:1--28:17},
  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.28},
  URN =		{urn:nbn:de:0030-drops-144053},
  doi =		{10.4230/LIPIcs.CONCUR.2021.28},
  annote =	{Keywords: Orbit problem, parametric, linear dynamical systems}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2020.36
Reachability in Dynamical Systems with Rounding

Authors: Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, Amaury Pouly, David Purser, and Markus A. Whiteland

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

Abstract
We consider reachability in dynamical systems with discrete linear updates, but with fixed digital precision, i.e., such that values of the system are rounded at each step. Given a matrix M ∈ ℚ^{d × d}, an initial vector x ∈ ℚ^{d}, a granularity g ∈ ℚ_+ and a rounding operation [⋅] projecting a vector of ℚ^{d} onto another vector whose every entry is a multiple of g, we are interested in the behaviour of the orbit 𝒪 = ⟨[x], [M[x]],[M[M[x]]],… ⟩, i.e., the trajectory of a linear dynamical system in which the state is rounded after each step. For arbitrary rounding functions with bounded effect, we show that the complexity of deciding point-to-point reachability - whether a given target y ∈ ℚ^{d} belongs to 𝒪 - is PSPACE-complete for hyperbolic systems (when no eigenvalue of M has modulus one). We also establish decidability without any restrictions on eigenvalues for several natural classes of rounding functions.
Cite as

Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, Amaury Pouly, David Purser, and Markus A. Whiteland. Reachability in Dynamical Systems with Rounding. 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. 36:1-36:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{baier_et_al:LIPIcs.FSTTCS.2020.36,
  author =	{Baier, Christel and Funke, Florian and Jantsch, Simon and Karimov, Toghrul and Lefaucheux, Engel and Ouaknine, Jo\"{e}l and Pouly, Amaury and Purser, David and Whiteland, Markus A.},
  title =	{{Reachability in Dynamical Systems with Rounding}},
  booktitle =	{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  pages =	{36:1--36:17},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.36},
  URN =		{urn:nbn:de:0030-drops-132778},
  doi =		{10.4230/LIPIcs.FSTTCS.2020.36},
  annote =	{Keywords: dynamical systems, rounding, reachability}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.41
The Big-O Problem for Labelled Markov Chains and Weighted Automata

Authors: Dmitry Chistikov, Stefan Kiefer, Andrzej S. Murawski, and David Purser

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
Given two weighted automata, we consider the problem of whether one is big-O of the other, i.e., if the weight of every finite word in the first is not greater than some constant multiple of the weight in the second. We show that the problem is undecidable, even for the instantiation of weighted automata as labelled Markov chains. Moreover, even when it is known that one weighted automaton is big-O of another, the problem of finding or approximating the associated constant is also undecidable. Our positive results show that the big-O problem is polynomial-time solvable for unambiguous automata, coNP-complete for unlabelled weighted automata (i.e., when the alphabet is a single character) and decidable, subject to Schanuel’s conjecture, when the language is bounded (i.e., a subset of w_1^* … w_m^* for some finite words w_1,… ,w_m). On labelled Markov chains, the problem can be restated as a ratio total variation distance, which, instead of finding the maximum difference between the probabilities of any two events, finds the maximum ratio between the probabilities of any two events. The problem is related to ε-differential privacy, for which the optimal constant of the big-O notation is exactly exp(ε).
Cite as

Dmitry Chistikov, Stefan Kiefer, Andrzej S. Murawski, and David Purser. The Big-O Problem for Labelled Markov Chains and Weighted Automata. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 41:1-41:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{chistikov_et_al:LIPIcs.CONCUR.2020.41,
  author =	{Chistikov, Dmitry and Kiefer, Stefan and Murawski, Andrzej S. and Purser, David},
  title =	{{The Big-O Problem for Labelled Markov Chains and Weighted Automata}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{41:1--41:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.41},
  URN =		{urn:nbn:de:0030-drops-128534},
  doi =		{10.4230/LIPIcs.CONCUR.2020.41},
  annote =	{Keywords: weighted automata, labelled Markov chains, probabilistic systems}
}
Document
DOI: 10.4230/LIPIcs.STACS.2020.49
How Fast Can You Escape a Compact Polytope?

Authors: Julian D'Costa, Engel Lefaucheux, Joël Ouaknine, and James Worrell

Published in: LIPIcs, Volume 154, 37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020)

Abstract
The Continuous Polytope Escape Problem (CPEP) asks whether every trajectory of a linear differential equation initialised within a convex polytope eventually escapes the polytope. We provide a polynomial-time algorithm to decide CPEP for compact polytopes. We also establish a quantitative uniform upper bound on the time required for every trajectory to escape the given polytope. In addition, we establish iteration bounds for termination of discrete linear loops via reduction to the continuous case.
Cite as

Julian D'Costa, Engel Lefaucheux, Joël Ouaknine, and James Worrell. How Fast Can You Escape a Compact Polytope?. In 37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 154, pp. 49:1-49:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{dcosta_et_al:LIPIcs.STACS.2020.49,
  author =	{D'Costa, Julian and Lefaucheux, Engel and Ouaknine, Jo\"{e}l and Worrell, James},
  title =	{{How Fast Can You Escape a Compact Polytope?}},
  booktitle =	{37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020)},
  pages =	{49:1--49:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-140-5},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{154},
  editor =	{Paul, Christophe and Bl\"{a}ser, Markus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2020.49},
  URN =		{urn:nbn:de:0030-drops-119105},
  doi =		{10.4230/LIPIcs.STACS.2020.49},
  annote =	{Keywords: Continuous linear dynamical systems, termination}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2017.13
Probabilistic Disclosure: Maximisation vs. Minimisation

Authors: Béatrice Bérard, Serge Haddad, and Engel Lefaucheux

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

Abstract
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.
Cite as

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-dev.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
DOI: 10.4230/LIPIcs.CONCUR.2016.37
Diagnosis in Infinite-State Probabilistic Systems

Authors: Nathalie Bertrand, Serge Haddad, and Engel Lefaucheux

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

Abstract
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.
Cite as

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-dev.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
DOI: 10.4230/LIPIcs.FSTTCS.2015.278
Simple Priced Timed Games are not That Simple

Authors: Thomas Brihaye, Gilles Geeraerts, Axel Haddad, Engel Lefaucheux, and Benjamin Monmege

Published in: LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

Abstract
Priced timed games are two-player zero-sum games played on priced timed automata (whose locations and transitions are labeled by weights modeling the costs of spending time in a state and executing an action, respectively). The goals of the players are to minimise and maximise the cost to reach a target location, respectively. We consider priced timed games with one clock and arbitrary (positive and negative) weights and show that, for an important subclass of theirs (the so-called simple priced timed games), one can compute, in exponential time, the optimal values that the players can achieve, with their associated optimal strategies. As side results, we also show that one-clock priced timed games are determined and that we can use our result on simple priced timed games to solve the more general class of so-called reset-acyclic priced timed games (with arbitrary weights and one-clock).
Cite as

Thomas Brihaye, Gilles Geeraerts, Axel Haddad, Engel Lefaucheux, and Benjamin Monmege. Simple Priced Timed Games are not That Simple. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 278-292, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{brihaye_et_al:LIPIcs.FSTTCS.2015.278,
  author =	{Brihaye, Thomas and Geeraerts, Gilles and Haddad, Axel and Lefaucheux, Engel and Monmege, Benjamin},
  title =	{{Simple Priced Timed Games are not That Simple}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{278--292},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-97-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{45},
  editor =	{Harsha, Prahladh and Ramalingam, G.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.278},
  URN =		{urn:nbn:de:0030-drops-56235},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.278},
  annote =	{Keywords: Priced timed games, real-time systems, game theory}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.417
Foundation of Diagnosis and Predictability in Probabilistic Systems

Authors: Nathalie Bertrand, Serge Haddad, and Engel Lefaucheux

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

Abstract
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.
Cite as

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-dev.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}
}
  • Refine by Author
  • 11 Lefaucheux, Engel
  • 7 Ouaknine, Joël
  • 6 Worrell, James
  • 4 Purser, David
  • 4 Whiteland, Markus A.
  • Show More...

  • Refine by Classification
  • 5 Theory of computation → Logic and verification
  • 1 Theory of computation
  • 1 Theory of computation → Probabilistic computation
  • 1 Theory of computation → Timed and hybrid models

  • Refine by Keyword
  • 2 Compact semialgebraic sets
  • 2 Discrete linear dynamical systems
  • 2 Partially observed systems
  • 2 Program termination
  • 2 probabilistic systems
  • Show More...

  • Refine by Type
  • 12 document

  • Refine by Publication Year
  • 3 2020
  • 3 2021
  • 2 2022
  • 1 2014
  • 1 2015
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact