Search Results

Documents authored by Jantsch, Simon

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.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.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
Invited Talk
DOI: 10.4230/LIPIcs.ICALP.2021.1
From Verification to Causality-Based Explications (Invited Talk)

Authors: Christel Baier, Clemens Dubslaff, Florian Funke, Simon Jantsch, Rupak Majumdar, Jakob Piribauer, and Robin Ziemek

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

Abstract
In view of the growing complexity of modern software architectures, formal models are increasingly used to understand why a system works the way it does, opposed to simply verifying that it behaves as intended. This paper surveys approaches to formally explicate the observable behavior of reactive systems. We describe how Halpern and Pearl’s notion of actual causation inspired verification-oriented studies of cause-effect relationships in the evolution of a system. A second focus lies on applications of the Shapley value to responsibility ascriptions, aimed to measure the influence of an event on an observable effect. Finally, formal approaches to probabilistic causation are collected and connected, and their relevance to the understanding of probabilistic systems is discussed.
Cite as

Christel Baier, Clemens Dubslaff, Florian Funke, Simon Jantsch, Rupak Majumdar, Jakob Piribauer, and Robin Ziemek. From Verification to Causality-Based Explications (Invited Talk). In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 1:1-1:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{baier_et_al:LIPIcs.ICALP.2021.1,
  author =	{Baier, Christel and Dubslaff, Clemens and Funke, Florian and Jantsch, Simon and Majumdar, Rupak and Piribauer, Jakob and Ziemek, Robin},
  title =	{{From Verification to Causality-Based Explications}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{1:1--1:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.1},
  URN =		{urn:nbn:de:0030-drops-140709},
  doi =		{10.4230/LIPIcs.ICALP.2021.1},
  annote =	{Keywords: Model Checking, Causality, Responsibility, Counterfactuals, Shapley value}
}
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.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}
}
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