9 citations · 30 across the 11 of their papers we have counts for
12 papers
Distributed Synthesis in Continuous Time
Holger Hermanns, Jan Krčál, Steen Vester
We introduce a formalism modelling communication of distributed agents strictly in continuous-time. Within this framework, we study the problem of synthesising local strategies for…
Controller synthesis for MDPs and Frequency LTLGU
Vojtěch Forejt, Jan Krčál, Jan Křetínský
Quantitative extensions of temporal logics have recently attracted significant attention. In this work, we study frequency LTL (fLTL), an extension of LTL which allows to speak abo…
Optimal Continuous Time Markov Decisions
Yuliya Butkova, Hassan Hatefi, Holger Hermanns +1
In the context of Markov decision processes running in continuous time, one of the most intriguing challenges is the efficient approximation of finite horizon reachability objectiv…
Recharging Probably Keeps Batteries Alive
Holger Hermanns, Jan Krčál, Gilles Nies
The kinetic battery model is a popular model of the dynamic behavior of a conventional battery, useful to predict or optimize the time until battery depletion. The model however la…
On Frequency LTL in Probabilistic Systems
Vojtěch Forejt, Jan Krčál
We study frequency linear-time temporal logic (fLTL) which extends the linear-time temporal logic (LTL) with a path operator expressing that on a path, certain formula holds…
Optimizing Performance of Continuous-Time Stochastic Systems using Timeout Synthesis
Tomáš Brázdil, Ľuboš Korenčiak, Jan Krčál +2
We consider parametric version of fixed-delay continuous-time Markov chains (or equivalently deterministic and stochastic Petri nets, DSPN) where fixed-delay transitions are specif…
Dealing with Zero Density Using Piecewise Phase-type Approximation
Ľuboš Korenčiak, Jan Krčál, Vojtěch Řehák
Every probability distribution can be approximated up to a given precision by a phase-type distribution, i.e. a distribution encoded by a continuous time Markov chain (CTMC). Howev…
Probabilistic Bisimulation: Naturally on Distributions
Holger Hermanns, Jan Krčál, Jan Křetínský
In contrast to the usual understanding of probabilistic systems as stochastic processes, recently these systems have also been regarded as transformers of probabilities. In this pa…
Probabilistic Bisimulations for PCTL Model Checking of Interval MDPs
Vahid Hashemi, Hassan Hatefi, Jan Krčál
Verification of PCTL properties of MDPs with convex uncertainties has been investigated recently by Puggelli et al. However, model checking algorithms typically suffer from state s…
Compositional Verification and Optimization of Interactive Markov Chains
Holger Hermanns, Jan Krčál, Jan Křetínský
Interactive Markov chains (IMC) are compositional behavioural models extending labelled transition systems and continuous-time Markov chains. We provide a framework and algorithms…
Fixed-delay Events in Generalized Semi-Markov Processes Revisited
Tomáš Brázdil, Jan Krčál, Jan Křetínský +1
We study long run average behavior of generalized semi-Markov processes with both fixed-delay events as well as variable-delay events. We show that allowing two fixed-delay events…
Measuring Performance of Continuous-Time Stochastic Processes using Timed Automata
Tomáš Brázdil, Jan Krčál, Jan Křetínský +2
We propose deterministic timed automata (DTA) as a model-independent language for specifying performance and dependability measures over continuous-time stochastic processes. Techn…