Document

**Published in:** LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

Entropic risk (ERisk) is an established risk measure in finance, quantifying risk by an exponential re-weighting of rewards. We study ERisk for the first time in the context of turn-based stochastic games with the total reward objective. This gives rise to an objective function that demands the control of systems in a risk-averse manner. We show that the resulting games are determined and, in particular, admit optimal memoryless deterministic strategies. This contrasts risk measures that previously have been considered in the special case of Markov decision processes and that require randomization and/or memory. We provide several results on the decidability and the computational complexity of the threshold problem, i.e. whether the optimal value of ERisk exceeds a given threshold. In the most general case, the problem is decidable subject to Shanuel’s conjecture. If all inputs are rational, the resulting threshold problem can be solved using algebraic numbers, leading to decidability via a polynomial-time reduction to the existential theory of the reals. Further restrictions on the encoding of the input allow the solution of the threshold problem in NP∩coNP. Finally, an approximation algorithm for the optimal value of ERisk is provided.

Christel Baier, Krishnendu Chatterjee, Tobias Meggendorfer, and Jakob Piribauer. Entropic Risk for Turn-Based Stochastic Games. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{baier_et_al:LIPIcs.MFCS.2023.15, author = {Baier, Christel and Chatterjee, Krishnendu and Meggendorfer, Tobias and Piribauer, Jakob}, title = {{Entropic Risk for Turn-Based Stochastic Games}}, booktitle = {48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)}, pages = {15:1--15:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-292-1}, ISSN = {1868-8969}, year = {2023}, volume = {272}, editor = {Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.15}, URN = {urn:nbn:de:0030-drops-185491}, doi = {10.4230/LIPIcs.MFCS.2023.15}, annote = {Keywords: Stochastic games, risk-aware verification} }

Document

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

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).

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

Track B: Automata, Logic, Semantics, and Theory of Programming

**Published in:** LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)

The stochastic shortest path problem (SSPP) asks to resolve the non-deterministic choices in a Markov decision process (MDP) such that the expected accumulated weight before reaching a target state is maximized. This paper addresses the optimization of the variance-penalized expectation (VPE) of the accumulated weight, which is a variant of the SSPP in which a multiple of the variance of accumulated weights is incurred as a penalty. It is shown that the optimal VPE in MDPs with non-negative weights as well as an optimal deterministic finite-memory scheduler can be computed in exponential space. The threshold problem whether the maximal VPE exceeds a given rational is shown to be EXPTIME-hard and to lie in NEXPTIME. Furthermore, a result of interest in its own right obtained on the way is that a variance-minimal scheduler among all expectation-optimal schedulers can be computed in polynomial time.

Jakob Piribauer, Ocan Sankur, and Christel Baier. The Variance-Penalized Stochastic Shortest Path Problem. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 129:1-129:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{piribauer_et_al:LIPIcs.ICALP.2022.129, author = {Piribauer, Jakob and Sankur, Ocan and Baier, Christel}, title = {{The Variance-Penalized Stochastic Shortest Path Problem}}, booktitle = {49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)}, pages = {129:1--129:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-235-8}, ISSN = {1868-8969}, year = {2022}, volume = {229}, editor = {Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.129}, URN = {urn:nbn:de:0030-drops-164705}, doi = {10.4230/LIPIcs.ICALP.2022.129}, annote = {Keywords: Markov decision process, variance, stochastic shortest path problem} }

Document

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

Quantified linear temporal logic (QLTL) is an ω-regular extension of LTL allowing quantification over propositional variables. We study the model checking problem of QLTL-formulas over Markov chains and Markov decision processes (MDPs) with respect to the number of quantifier alternations of formulas in prenex normal form. For formulas with k{-}1 quantifier alternations, we prove that all qualitative and quantitative model checking problems are k-EXPSPACE-complete over Markov chains and k{+}1-EXPTIME-complete over MDPs.
As an application of these results, we generalize vacuity checking for LTL specifications from the non-probabilistic to the probabilistic setting. We show how to check whether an LTL-formula is affected by a subformula, and also study inherent vacuity for probabilistic systems.

Jakob Piribauer, Christel Baier, Nathalie Bertrand, and Ocan Sankur. Quantified Linear Temporal Logic over Probabilistic Systems with an Application to Vacuity Checking. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{piribauer_et_al:LIPIcs.CONCUR.2021.7, author = {Piribauer, Jakob and Baier, Christel and Bertrand, Nathalie and Sankur, Ocan}, title = {{Quantified Linear Temporal Logic over Probabilistic Systems with an Application to Vacuity Checking}}, booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)}, pages = {7:1--7:18}, 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.7}, URN = {urn:nbn:de:0030-drops-143842}, doi = {10.4230/LIPIcs.CONCUR.2021.7}, annote = {Keywords: Quantified linear temporal logic, Markov chain, Markov decision process, vacuity} }

Document

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

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.

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

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

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.

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

Complete Volume

**Published in:** LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

LIPIcs, Volume 183, CSL 2021, Complete Volume

29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 1-734, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@Proceedings{baier_et_al:LIPIcs.CSL.2021, title = {{LIPIcs, Volume 183, CSL 2021, Complete Volume}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {1--734}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021}, URN = {urn:nbn:de:0030-drops-134339}, doi = {10.4230/LIPIcs.CSL.2021}, annote = {Keywords: LIPIcs, Volume 183, CSL 2021, Complete Volume} }

Document

Front Matter

**Published in:** LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Front Matter, Table of Contents, Preface, Conference Organization

29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 0:i-0:xx, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{baier_et_al:LIPIcs.CSL.2021.0, author = {Baier, Christel and Goubault-Larrecq, Jean}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)}, pages = {0:i--0:xx}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-175-7}, ISSN = {1868-8969}, year = {2021}, volume = {183}, editor = {Baier, Christel and Goubault-Larrecq, Jean}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.0}, URN = {urn:nbn:de:0030-drops-134348}, doi = {10.4230/LIPIcs.CSL.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)

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.

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} }

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

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

The Skolem problem and the related Positivity problem for linear recurrence sequences are outstanding number-theoretic problems whose decidability has been open for many decades. In this paper, the inherent mathematical difficulty of a series of optimization problems on Markov decision processes (MDPs) is shown by a reduction from the Positivity problem to the associated decision problems which establishes that the problems are also at least as hard as the Skolem problem as an immediate consequence. The optimization problems under consideration are two non-classical variants of the stochastic shortest path problem (SSPP) in terms of expected partial or conditional accumulated weights, the optimization of the conditional value-at-risk for accumulated weights, and two problems addressing the long-run satisfaction of path properties, namely the optimization of long-run probabilities of regular co-safety properties and the model-checking problem of the logic frequency-LTL. To prove the Positivity- and hence Skolem-hardness for the latter two problems, a new auxiliary path measure, called weighted long-run frequency, is introduced and the Positivity-hardness of the corresponding decision problem is shown as an intermediate step. For the partial and conditional SSPP on MDPs with non-negative weights and for the optimization of long-run probabilities of constrained reachability properties (aU b), solutions are known that rely on the identification of a bound on the accumulated weight or the number of consecutive visits to certain sates, called a saturation point, from which on optimal schedulers behave memorylessly. In this paper, it is shown that also the optimization of the conditional value-at-risk for the classical SSPP and of weighted long-run frequencies on MDPs with non-negative weights can be solved in pseudo-polynomial time exploiting the existence of a saturation point. As a consequence, one obtains the decidability of the qualitative model-checking problem of a frequency-LTL formula that is not included in the fragments with known solutions.

Jakob Piribauer and Christel Baier. On Skolem-Hardness and Saturation Points in Markov Decision Processes. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 138:1-138:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{piribauer_et_al:LIPIcs.ICALP.2020.138, author = {Piribauer, Jakob and Baier, Christel}, title = {{On Skolem-Hardness and Saturation Points in Markov Decision Processes}}, booktitle = {47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)}, pages = {138:1--138:17}, 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.138}, URN = {urn:nbn:de:0030-drops-125455}, doi = {10.4230/LIPIcs.ICALP.2020.138}, annote = {Keywords: Markov decision process, Skolem problem, stochastic shortest path, conditional expectation, conditional value-at-risk, model checking, frequency-LTL} }

Document

Complete Volume

**Published in:** LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

LIPIcs, Volume 132, ICALP'19, Complete Volume

46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Proceedings{baier_et_al:LIPIcs.ICALP.2019, title = {{LIPIcs, Volume 132, ICALP'19, Complete Volume}}, booktitle = {46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-109-2}, ISSN = {1868-8969}, year = {2019}, volume = {132}, editor = {Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019}, URN = {urn:nbn:de:0030-drops-108644}, doi = {10.4230/LIPIcs.ICALP.2019}, annote = {Keywords: Theory of computation} }

Document

Front Matter

**Published in:** LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Front Matter, Table of Contents, Preface, Conference Organization

46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 0:i-0:xxxviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{baier_et_al:LIPIcs.ICALP.2019.0, author = {Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)}, pages = {0:i--0:xxxviii}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-109-2}, ISSN = {1868-8969}, year = {2019}, volume = {132}, editor = {Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.0}, URN = {urn:nbn:de:0030-drops-105765}, doi = {10.4230/LIPIcs.ICALP.2019.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} }

Document

**Published in:** LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Conventional approaches for parallel composition of stochastic systems relate probability measures of the individual components in terms of product measures. Such approaches rely on the assumption that components interact stochastically independent, which might be too rigid for modeling real world systems. In this paper, we introduce a parallel-composition operator for stochastic transition systems that is based on couplings of probability measures and does not impose any stochastic assumptions. When composing systems within our framework, the intended dependencies between components can be determined by providing so-called spans and span couplings. We present a congruence result for our operator with respect to a standard notion of bisimilarity and develop a general theory for spans, exploiting deep results from descriptive set theory. As an application of our general approach, we propose a model for stochastic hybrid systems called stochastic hybrid motion automata.

Daniel Gburek, Christel Baier, and Sascha Klüppelholz. Composition of Stochastic Transition Systems Based on Spans and Couplings. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 102:1-102:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{gburek_et_al:LIPIcs.ICALP.2016.102, author = {Gburek, Daniel and Baier, Christel and Kl\"{u}ppelholz, Sascha}, title = {{Composition of Stochastic Transition Systems Based on Spans and Couplings}}, booktitle = {43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)}, pages = {102:1--102:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-013-2}, ISSN = {1868-8969}, year = {2016}, volume = {55}, editor = {Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.102}, URN = {urn:nbn:de:0030-drops-62379}, doi = {10.4230/LIPIcs.ICALP.2016.102}, annote = {Keywords: Stochastic Transition System, Composition, Stochastic Hybrid Motion Automata, Stochastically Independent, Coupling, Span, Bisimulation, Congruence, Po} }

Document

**Published in:** Dagstuhl Seminar Proceedings, Volume 10031, Quantitative Models: Expressiveness and Analysis (2010)

From Jan 18 to Jan 22, 2010, the Dagstuhl Seminar 10031 ``Quantitative Models: Expressiveness and Analysis '' was held in Schloss Dagstuhl~--~Leibniz Center for Informatics. During the seminar, several participants presented their current
research, and ongoing work and open problems were discussed. Abstracts of
the presentations given during the seminar as well as abstracts of
seminar results and ideas are put together in this paper. The first section
describes the seminar topics and goals in general.
Links to extended abstracts or full papers are provided, if available.

Christel Baier, Manfred Droste, Paul Gastin, and Kim Guldstrand Larsen. 10031 Abstracts Collection – Quantitative Models: Expressiveness and Analysis. In Quantitative Models: Expressiveness and Analysis. Dagstuhl Seminar Proceedings, Volume 10031, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{baier_et_al:DagSemProc.10031.1, author = {Baier, Christel and Droste, Manfred and Gastin, Paul and Larsen, Kim Guldstrand}, title = {{10031 Abstracts Collection – Quantitative Models: Expressiveness and Analysis}}, booktitle = {Quantitative Models: Expressiveness and Analysis}, pages = {1--15}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2010}, volume = {10031}, editor = {Christel Baier and Manfred Droste and Paul Gastin and Kim Guldstrand Larsen}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10031.1}, URN = {urn:nbn:de:0030-drops-26839}, doi = {10.4230/DagSemProc.10031.1}, annote = {Keywords: Quantitative models, quantitative analysis, timed and hybrid systems, probabilistic systems, weighted automata} }

Document

**Published in:** Dagstuhl Seminar Proceedings, Volume 10031, Quantitative Models: Expressiveness and Analysis (2010)

Quantitative models and quantitative analysis in Computer Science
are currently intensively studied, resulting in a revision of the
foundation of Computer Science where classical yes/no answers are
replaced by quantitative analyses. The potential application areas
are huge, e.g., performance analysis, operational research or
embedded systems.
The aim of the seminar was to address three fundamental topics
which are closely related: quantitative analysis of real-time and hybrid
systems; probabilistic analysis and stochastic automata; weighted
automata. These three areas of research have mainly evolved
independently so far and the relationship between them has emerged
only recently. The seminar brought together leading researchers
of the three areas, with the goal of future highly productive
cross-fertilizations.

Christel Baier, Manfred Droste, Paul Gastin, and Kim Guldstrand Larsen. 10031 Executive Summary – Quantitative Models: Expressiveness and Analysis. In Quantitative Models: Expressiveness and Analysis. Dagstuhl Seminar Proceedings, Volume 10031, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{baier_et_al:DagSemProc.10031.2, author = {Baier, Christel and Droste, Manfred and Gastin, Paul and Larsen, Kim Guldstrand}, title = {{10031 Executive Summary – Quantitative Models: Expressiveness and Analysis}}, booktitle = {Quantitative Models: Expressiveness and Analysis}, pages = {1--2}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2010}, volume = {10031}, editor = {Christel Baier and Manfred Droste and Paul Gastin and Kim Guldstrand Larsen}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10031.2}, URN = {urn:nbn:de:0030-drops-26824}, doi = {10.4230/DagSemProc.10031.2}, annote = {Keywords: Quantitative models, quantitative analysis, timed and hybrid systems, probabilistic systems, weighted automata} }

Document

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

In a context of $\omega$-regular specifications for infinite execution
sequences, the classical B\"uchi condition, or repeated liveness
condition, asks that an accepting state is visited infinitely often. In
this paper, we show that in a probabilistic context it is relevant to
strengthen this infinitely often condition. An execution path is now
accepting if the \emph{proportion} of time spent on an accepting state
does not go to zero as the length of the path goes to infinity. We
introduce associated notions of recurrence and transience for
non-homogeneous finite Markov chains and study the computational
complexity of the associated problems. As Probabilistic B\"uchi Automata
(PBA) have been an attempt to generalize B\"uchi automata to a
probabilistic context, we define a class of Constrained Probabilistic
Automata with our new accepting condition on runs. The accepted language
is defined by the requirement that the measure of the set of accepting
runs is positive (probable semantics) or equals 1 (almost-sure
semantics). In contrast to the PBA case, we prove that
the emptiness problem for the language of a constrained probabilistic
B\"uchi automaton with the probable semantics is decidable.

Mathieu Tracol, Christel Baier, and Marcus Grösser. Recurrence and Transience for Probabilistic Automata. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 395-406, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{tracol_et_al:LIPIcs.FSTTCS.2009.2335, author = {Tracol, Mathieu and Baier, Christel and Gr\"{o}sser, Marcus}, title = {{Recurrence and Transience for Probabilistic Automata}}, booktitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science}, pages = {395--406}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-13-2}, ISSN = {1868-8969}, year = {2009}, volume = {4}, editor = {Kannan, Ravi and Narayan Kumar, K.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2335}, URN = {urn:nbn:de:0030-drops-23357}, doi = {10.4230/LIPIcs.FSTTCS.2009.2335}, annote = {Keywords: Markov Chains, Probabilistic Automata, Buchi Automata, Recurrence, Omega-Regular Properties} }