Search Results

Documents authored by Krcal, Jan

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},
  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.184
On Frequency LTL in Probabilistic Systems

Authors: Vojtech Forejt and Jan Krcal

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

Abstract
We study frequency linear-time temporal logic (fLTL) which extends the linear-time temporal logic (LTL) with a path operator G^p expressing that on a path, certain formula holds with at least a given frequency p, thus relaxing the semantics of the usual G operator of LTL. Such logic is particularly useful in probabilistic systems, where some undesirable events such as random failures may occur and are acceptable if they are rare enough. Frequency-related extensions of LTL have been previously studied by several authors, where mostly the logic is equipped with an extended "until" and "globally" operator, leading to undecidability of most interesting problems. For the variant we study, we are able to establish fundamental decidability results. We show that for Markov chains, the problem of computing the probability with which a given fLTL formula holds has the same complexity as the analogous problem for LTL. We also show that for Markov decision processes the problem becomes more delicate, but when restricting the frequency bound p to be 1 and negations not to be outside any G^p operator, we can compute the maximum probability of satisfying the fLTL formula. This can be again performed with the same time complexity as for the ordinary LTL formulas.
Cite as

Vojtech Forejt and Jan Krcal. On Frequency LTL in Probabilistic Systems. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 184-197, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{forejt_et_al:LIPIcs.CONCUR.2015.184,
  author =	{Forejt, Vojtech and Krcal, Jan},
  title =	{{On Frequency LTL in Probabilistic Systems}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{184--197},
  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.184},
  URN =		{urn:nbn:de:0030-drops-53789},
  doi =		{10.4230/LIPIcs.CONCUR.2015.184},
  annote =	{Keywords: Markov chains, Markov decision processes, LTL, controller synthesis}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2012.474
Verification of Open Interactive Markov Chains

Authors: Tomas Brazdil, Holger Hermanns, Jan Krcal, Jan Kretinsky, and Vojtech Rehak

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

Abstract
Interactive Markov chains (IMC) are compositional behavioral models extending both labeled transition systems and continuous-time Markov chains. IMC pair modeling convenience - owed to compositionality properties - with effective verification algorithms and tools - owed to Markov properties. Thus far however, IMC verification did not consider compositionality properties, but considered closed systems. This paper discusses the evaluation of IMC in an open and thus compositional interpretation. For this we embed the IMC into a game that is played with the environment. We devise algorithms that enable us to derive bounds on reachability probabilities that are assured to hold in any composition context.
Cite as

Tomas Brazdil, Holger Hermanns, Jan Krcal, Jan Kretinsky, and Vojtech Rehak. Verification of Open Interactive Markov Chains. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 474-485, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{brazdil_et_al:LIPIcs.FSTTCS.2012.474,
  author =	{Brazdil, Tomas and Hermanns, Holger and Krcal, Jan and Kretinsky, Jan and Rehak, Vojtech},
  title =	{{Verification of Open Interactive Markov Chains}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{474--485},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.474},
  URN =		{urn:nbn:de:0030-drops-38826},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.474},
  annote =	{Keywords: IMC, compositional verification, synthesis, time bounded reachability, discretization}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2009.2307
Continuous-Time Stochastic Games with Time-Bounded Reachability

Authors: Tomas Brazdil, Vojtech Forejt, Jan Krcal, Jan Kretinsky, and Antonin Kucera

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

Abstract
We study continuous-time stochastic games with time-bounded reachability objectives. We show that each vertex in such a game has a \emph{value} (i.e., an equilibrium probability), and we classify the conditions under which optimal strategies exist. Finally, we show how to compute optimal strategies in finite uniform games, and how to compute $\varepsilon$-optimal strategies in finitely-branching games with bounded rates (for finite games, we provide detailed complexity estimations).
Cite as

Tomas Brazdil, Vojtech Forejt, Jan Krcal, Jan Kretinsky, and Antonin Kucera. Continuous-Time Stochastic Games with Time-Bounded Reachability. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 61-72, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{brazdil_et_al:LIPIcs.FSTTCS.2009.2307,
  author =	{Brazdil, Tomas and Forejt, Vojtech and Krcal, Jan and Kretinsky, Jan and Kucera, Antonin},
  title =	{{Continuous-Time Stochastic Games with Time-Bounded Reachability}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{61--72},
  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.2307},
  URN =		{urn:nbn:de:0030-drops-23077},
  doi =		{10.4230/LIPIcs.FSTTCS.2009.2307},
  annote =	{Keywords: Continuous time stochastic systems, time bounded reachability, stochastic games}
}
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