10 Search Results for "Soudjani, Sadegh"

Document
DOI: 10.4230/LIPIcs.MFCS.2025.79
Deciding Robust Instances of an Escape Problem for Dynamical Systems in Euclidean Space

Authors: Eike Neumann

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
We study the problem of deciding whether a point escapes a closed subset of ℝ^d under the iteration of a continuous map f : ℝ^d → ℝ^d in the bit-model of real computation. We give a sound partial decision method for this problem which is complete in the sense that its halting set contains the halting set of all sound partial decision methods for the problem. Equivalently, our decision method terminates on all problem instances whose answer is robust under all sufficiently small perturbations of the function. We further show that the halting set of our algorithm is dense in the set of all problem instances. While our algorithm applies to general continuous functions, we demonstrate that it also yields complete decision methods for much more rigid function families: affine linear systems and quadratic complex polynomials. In the latter case, completeness is subject to the density of hyperbolicity conjecture in complex dynamics. This in particular yields an alternative proof of Hertling’s (2004) conditional answer to a question raised by Penrose (1989) regarding the computability of the Mandelbrot set.
Cite as

Eike Neumann. Deciding Robust Instances of an Escape Problem for Dynamical Systems in Euclidean Space. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 79:1-79:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{neumann:LIPIcs.MFCS.2025.79,
  author =	{Neumann, Eike},
  title =	{{Deciding Robust Instances of an Escape Problem for Dynamical Systems in Euclidean Space}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{79:1--79:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.79},
  URN =		{urn:nbn:de:0030-drops-241866},
  doi =		{10.4230/LIPIcs.MFCS.2025.79},
  annote =	{Keywords: Dynamical Systems, Computability in Analysis, Non-Linear Functions}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.36
Explainability is a Game for Probabilistic Bisimilarity Distances

Authors: Emily Vlasman, Anto Nanah Ji, James Worrell, and Franck van Breugel

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
We revisit a game from the literature that characterizes the probabilistic bisimilarity distances of a labelled Markov chain. We illustrate how an optimal policy of the game can explain these distances. Like the games that characterize bisimilarity and probabilistic bisimilarity, the game is played on pairs of states and matches transitions of those states. To obtain more convincing and interpretable explanations than those provided by generic optimal policies, we restrict to optimal policies that delay reaching observably inequivalent state pairs for as long as possible (called 1-maximal) while quickly reaching equivalent ones (called 0-minimal). We present iterative algorithms that compute 1-maximal and 0-minimal policies and prove an exponential lower bound for the number of iterations of the algorithm that computes 1-maximal policies.
Cite as

Emily Vlasman, Anto Nanah Ji, James Worrell, and Franck van Breugel. Explainability is a Game for Probabilistic Bisimilarity Distances. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 36:1-36:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vlasman_et_al:LIPIcs.CONCUR.2025.36,
  author =	{Vlasman, Emily and Nanah Ji, Anto and Worrell, James and van Breugel, Franck},
  title =	{{Explainability is a Game for Probabilistic Bisimilarity Distances}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{36:1--36:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.36},
  URN =		{urn:nbn:de:0030-drops-239861},
  doi =		{10.4230/LIPIcs.CONCUR.2025.36},
  annote =	{Keywords: probabilistic bisimilarity distance, labelled Markov chain, game, policy, explainability}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.9
A Direct Reduction from Stochastic Parity Games to Simple Stochastic Games

Authors: Raphaël Berthon, Joost-Pieter Katoen, and Zihan Zhou

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
Significant progress has been recently achieved in developing efficient solutions for simple stochastic games (SSGs), focusing on reachability objectives. While reductions from stochastic parity games (SPGs) to SSGs have been presented in the literature through the use of multiple intermediate game models, a direct and simple reduction has been notably absent. This paper introduces a novel and direct polynomial-time reduction from quantitative SPGs to quantitative SSGs. By leveraging a gadget-based transformation that effectively removes the priority function, we construct an SSG that simulates the behavior of a given SPG. We formally establish the correctness of our direct reduction. Furthermore, we demonstrate that under binary encoding this reduction is polynomial, thereby directly corroborating the known NP ∩ coNP complexity of SPGs and providing new understanding in the relationship between parity and reachability objectives in turn-based stochastic games.
Cite as

Raphaël Berthon, Joost-Pieter Katoen, and Zihan Zhou. A Direct Reduction from Stochastic Parity Games to Simple Stochastic Games. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 9:1-9:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{berthon_et_al:LIPIcs.CONCUR.2025.9,
  author =	{Berthon, Rapha\"{e}l and Katoen, Joost-Pieter and Zhou, Zihan},
  title =	{{A Direct Reduction from Stochastic Parity Games to Simple Stochastic Games}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{9:1--9:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.9},
  URN =		{urn:nbn:de:0030-drops-239595},
  doi =		{10.4230/LIPIcs.CONCUR.2025.9},
  annote =	{Keywords: stochastic games, parity, reduction}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.163
Verification of Linear Dynamical Systems via O-Minimality of the Real Numbers

Authors: Toghrul Karimov

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
A discrete-time linear dynamical system (LDS) is given by an update matrix M ∈ ℝ^{d× d}, and has the trajectories ⟨s, Ms, M²s, …⟩ for s ∈ ℝ^d. Reachability-type decision problems of linear dynamical systems, most notably the Skolem Problem, lie at the forefront of decidability: typically, sound and complete algorithms are known only in low dimensions, and these rely on sophisticated tools from number theory and Diophantine approximation. Recently, however, o-minimality has emerged as a counterpoint to these number-theoretic tools that allows us to decide certain modifications of the classical problems of LDS without any dimension restrictions. In this paper, we first introduce the Decomposition Method, a framework that captures all applications of o-minimality to decision problems of LDS that are currently known to us. We then use the Decomposition Method to show decidability of the Robust Safety Problem (restricted to bounded initial sets) in arbitrary dimension: given a matrix M, a bounded semialgebraic set S of initial points, and a semialgebraic set T of unsafe points, it is decidable whether there exists ε > 0 such that all orbits that begin in the ε-ball around S avoid T.
Cite as

Toghrul Karimov. Verification of Linear Dynamical Systems via O-Minimality of the Real Numbers. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 163:1-163:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{karimov:LIPIcs.ICALP.2025.163,
  author =	{Karimov, Toghrul},
  title =	{{Verification of Linear Dynamical Systems via O-Minimality of the Real Numbers}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{163:1--163:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.163},
  URN =		{urn:nbn:de:0030-drops-235401},
  doi =		{10.4230/LIPIcs.ICALP.2025.163},
  annote =	{Keywords: Linear dynamical systems, reachability problems, o-minimality}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.157
Bayesian Inference in Quantum Programs

Authors: Christina Gehnen, Dominique Unruh, and Joost-Pieter Katoen

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
Conditioning is a key feature in probabilistic programming to enable modeling the influence of data (also known as observations) to the probability distribution described by such programs. Determining the posterior distribution is also known as Bayesian inference. This paper equips a quantum while-language with conditioning, defines its denotational and operational semantics over infinite-dimensional Hilbert spaces, and shows their equivalence. We provide sufficient conditions for the existence of weakest (liberal) precondition-transformers and derive inductive characterizations of these transformers. It is shown how w(l)p-transformers can be used to assess the effect of Bayesian inference on (possibly diverging) quantum programs.
Cite as

Christina Gehnen, Dominique Unruh, and Joost-Pieter Katoen. Bayesian Inference in Quantum Programs. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 157:1-157:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{gehnen_et_al:LIPIcs.ICALP.2025.157,
  author =	{Gehnen, Christina and Unruh, Dominique and Katoen, Joost-Pieter},
  title =	{{Bayesian Inference in Quantum Programs}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{157:1--157:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.157},
  URN =		{urn:nbn:de:0030-drops-235345},
  doi =		{10.4230/LIPIcs.ICALP.2025.157},
  annote =	{Keywords: Quantum Program Logics, Weakest Preconditions, Bayesian Inference, Program Semantics}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2021.34
The Pseudo-Skolem Problem is Decidable

Authors: Julian D'Costa, Toghrul Karimov, Rupak Majumdar, Joël Ouaknine, Mahmoud Salamati, Sadegh Soudjani, and James Worrell

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

Abstract
We study fundamental decision problems on linear dynamical systems in discrete time. We focus on pseudo-orbits, the collection of trajectories of the dynamical system for which there is an arbitrarily small perturbation at each step. Pseudo-orbits are generalizations of orbits in the topological theory of dynamical systems. We study the pseudo-orbit problem, whether a state belongs to the pseudo-orbit of another state, and the pseudo-Skolem problem, whether a hyperplane is reachable by an ε-pseudo-orbit for every ε. These problems are analogous to the well-studied orbit problem and Skolem problem on unperturbed dynamical systems. Our main results show that the pseudo-orbit problem is decidable in polynomial time and the Skolem problem on pseudo-orbits is decidable. The former extends the seminal result of Kannan and Lipton from orbits to pseudo-orbits. The latter is in contrast to the Skolem problem for linear dynamical systems, which remains open for proper orbits.
Cite as

Julian D'Costa, Toghrul Karimov, Rupak Majumdar, Joël Ouaknine, Mahmoud Salamati, Sadegh Soudjani, and James Worrell. The Pseudo-Skolem Problem is Decidable. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 34:1-34:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{dcosta_et_al:LIPIcs.MFCS.2021.34,
  author =	{D'Costa, Julian and Karimov, Toghrul and Majumdar, Rupak and Ouaknine, Jo\"{e}l and Salamati, Mahmoud and Soudjani, Sadegh and Worrell, James},
  title =	{{The Pseudo-Skolem Problem is Decidable}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{34:1--34: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.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.34},
  URN =		{urn:nbn:de:0030-drops-144742},
  doi =		{10.4230/LIPIcs.MFCS.2021.34},
  annote =	{Keywords: Pseudo-orbits, Orbit problem, Skolem problem, linear dynamical systems}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2020.133
On Decidability of Time-Bounded Reachability in CTMDPs

Authors: Rupak Majumdar, Mahmoud Salamati, and Sadegh Soudjani

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)

Abstract
We consider the time-bounded reachability problem for continuous-time Markov decision processes. We show that the problem is decidable subject to Schanuel’s conjecture. Our decision procedure relies on the structure of optimal policies and the conditional decidability (under Schanuel’s conjecture) of the theory of reals extended with exponential and trigonometric functions over bounded domains. We further show that any unconditional decidability result would imply unconditional decidability of the bounded continuous Skolem problem, or equivalently, the problem of checking if an exponential polynomial has a non-tangential zero in a bounded interval. We note that the latter problems are also decidable subject to Schanuel’s conjecture but finding unconditional decision procedures remain longstanding open problems.
Cite as

Rupak Majumdar, Mahmoud Salamati, and Sadegh Soudjani. On Decidability of Time-Bounded Reachability in CTMDPs. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 133:1-133:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{majumdar_et_al:LIPIcs.ICALP.2020.133,
  author =	{Majumdar, Rupak and Salamati, Mahmoud and Soudjani, Sadegh},
  title =	{{On Decidability of Time-Bounded Reachability in CTMDPs}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{133:1--133:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.133},
  URN =		{urn:nbn:de:0030-drops-125408},
  doi =		{10.4230/LIPIcs.ICALP.2020.133},
  annote =	{Keywords: CTMDP, Time bounded reachability, Continuous Skolem Problem, Schanuel’s Conjecture}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.13
The Robot Routing Problem for Collecting Aggregate Stochastic Rewards

Authors: Rayna Dimitrova, Ivan Gavran, Rupak Majumdar, Vinayak S. Prabhu, and Sadegh Esmaeil Zadeh Soudjani

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

Abstract
We propose a new model for formalizing reward collection problems on graphs with dynamically generated rewards which may appear and disappear based on a stochastic model. The robot routing problem is modeled as a graph whose nodes are stochastic processes generating potential rewards over discrete time. The rewards are generated according to the stochastic process, but at each step, an existing reward disappears with a given probability. The edges in the graph encode the (unit-distance) paths between the rewards' locations. On visiting a node, the robot collects the accumulated reward at the node at that time, but traveling between the nodes takes time. The optimization question asks to compute an optimal (or epsilon-optimal) path that maximizes the expected collected rewards. We consider the finite and infinite-horizon robot routing problems. For finite-horizon, the goal is to maximize the total expected reward, while for infinite horizon we consider limit-average objectives. We study the computational and strategy complexity of these problems, establish NP-lower bounds and show that optimal strategies require memory in general. We also provide an algorithm for computing epsilon-optimal infinite paths for arbitrary epsilon > 0.
Cite as

Rayna Dimitrova, Ivan Gavran, Rupak Majumdar, Vinayak S. Prabhu, and Sadegh Esmaeil Zadeh Soudjani. The Robot Routing Problem for Collecting Aggregate Stochastic Rewards. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{dimitrova_et_al:LIPIcs.CONCUR.2017.13,
  author =	{Dimitrova, Rayna and Gavran, Ivan and Majumdar, Rupak and Prabhu, Vinayak S. and Soudjani, Sadegh Esmaeil Zadeh},
  title =	{{The Robot Routing Problem for Collecting Aggregate Stochastic Rewards}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{13:1--13:17},
  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.13},
  URN =		{urn:nbn:de:0030-drops-77920},
  doi =		{10.4230/LIPIcs.CONCUR.2017.13},
  annote =	{Keywords: Path Planning, Graph Games, Quantitative Objectives, Discounting}
}
Document
DOI: 10.4230/LITES-v004-i001-a004
How Is Your Satellite Doing? Battery Kinetics with Recharging and Uncertainty

Authors: Holger Hermanns, Jan Krčál, and Gilles Nies

Published in: LITES, Volume 4, Issue 1 (2017). Leibniz Transactions on Embedded Systems, Volume 4, Issue 1

Abstract
The kinetic battery model is a popular model of the dynamic behaviour of a conventional battery, useful to predict or optimize the time until battery depletion. The model however lacks certain obvious aspects of batteries in-the-wild, especially with respect to the effects of random influences and the behaviour when charging up to capacity limits.This paper considers the kinetic battery model with limited capacity in the context of piecewise constant yet random charging and discharging. We provide exact representations of the battery behaviour wherever possible, and otherwise develop safe approximations that bound the probability distribution of the battery state from above and below. The resulting model enables the time-dependent evaluation of the risk of battery depletion. This is demonstrated in an extensive dependability study of a nano satellite currently orbiting the earth.
Cite as

Holger Hermanns, Jan Krčál, and Gilles Nies. How Is Your Satellite Doing? Battery Kinetics with Recharging and Uncertainty. In LITES, Volume 4, Issue 1 (2017). Leibniz Transactions on Embedded Systems, Volume 4, Issue 1, pp. 04:1-04:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{hermanns_et_al:LITES-v004-i001-a004,
  author =	{Hermanns, Holger and Kr\v{c}\'{a}l, Jan and Nies, Gilles},
  title =	{{How Is Your Satellite Doing? Battery Kinetics with Recharging and Uncertainty}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{04:1--04:28},
  ISSN =	{2199-2002},
  year =	{2017},
  volume =	{4},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v004-i001-a004},
  URN =		{urn:nbn:de:0030-drops-192655},
  doi =		{10.4230/LITES-v004-i001-a004},
  annote =	{Keywords: Battery Power, Depletion Risk, Bounded Charging and Discharging, Stochastic Load, Distribution Bounds}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.169
Dynamic Bayesian Networks as Formal Abstractions of Structured Stochastic Processes

Authors: Sadegh Esmaeil Zadeh Soudjani, Alessandro Abate, and Rupak Majumdar

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
We study the problem of finite-horizon probabilistic invariance for discrete-time Markov processes over general (uncountable) state spaces. We compute discrete-time, finite-state Markov chains as formal abstractions of general Markov processes. Our abstraction differs from existing approaches in two ways. First, we exploit the structure of the underlying Markov process to compute the abstraction separately for each dimension. Second, we employ dynamic Bayesian networks (DBN) as compact representations of the abstraction. In contrast, existing approaches represent and store the (exponentially large) Markov chain explicitly, which leads to heavy memory requirements limiting the application to models of dimension less than half, according to our experiments. We show how to construct a DBN abstraction of a Markov process satisfying an independence assumption on the driving process noise. We compute a guaranteed bound on the error in the abstraction w.r.t. the probabilistic invariance property; the dimension-dependent abstraction makes the error bounds more precise than existing approaches. Additionally, we show how factor graphs and the sum-product algorithm for DBNs can be used to solve the finite-horizon probabilistic invariance problem. Together, DBN-based representations and algorithms can be significantly more efficient than explicit representations of Markov chains for abstracting and model checking structured Markov processes.
Cite as

Sadegh Esmaeil Zadeh Soudjani, Alessandro Abate, and Rupak Majumdar. Dynamic Bayesian Networks as Formal Abstractions of Structured Stochastic Processes. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 169-183, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{esmaeilzadehsoudjani_et_al:LIPIcs.CONCUR.2015.169,
  author =	{Esmaeil Zadeh Soudjani, Sadegh and Abate, Alessandro and Majumdar, Rupak},
  title =	{{Dynamic Bayesian Networks as Formal Abstractions of Structured Stochastic Processes}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{169--183},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.169},
  URN =		{urn:nbn:de:0030-drops-53693},
  doi =		{10.4230/LIPIcs.CONCUR.2015.169},
  annote =	{Keywords: Structured stochastic systems, general space Markov processes, formal verification, dynamic Bayesian networks, Markov chain abstraction}
}
  • Refine by Type
  • 10 Document/PDF
  • 5 Document/HTML

  • Refine by Publication Year
  • 5 2025
  • 1 2021
  • 1 2020
  • 2 2017
  • 1 2015

  • Refine by Author
  • 4 Majumdar, Rupak
  • 2 Karimov, Toghrul
  • 2 Katoen, Joost-Pieter
  • 2 Salamati, Mahmoud
  • 2 Soudjani, Sadegh
  • Show More...

  • Refine by Series/Journal
  • 9 LIPIcs
  • 1 LITES

  • Refine by Classification
  • 2 Theory of computation → Logic and verification
  • 1 Computer systems organization → Reliability
  • 1 Hardware → Batteries
  • 1 Mathematics of computing → Markov processes
  • 1 Mathematics of computing → Probability and statistics
  • Show More...

  • Refine by Keyword
  • 1 Battery Power
  • 1 Bayesian Inference
  • 1 Bounded Charging and Discharging
  • 1 CTMDP
  • 1 Computability in Analysis
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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