This paper surveys the analysis of parametric Markov models whose transitions are labelled
with functions over a finite set of parameters. These models are symbolic representations of …

Dependency on the correct operation of embedded systems is rapidly growing, mainly due
to their wide range of applications. Their structures are becoming more complex and …

We consider the problem of synthesising rate parameters for stochastic biochemical
networks so that a given time-bounded CSL property is guaranteed to hold, or, in the case of …

Formal verification is used to establish the compliance of software and hardware systems
with important classes of requirements. System compliance with functional requirements is …

We describe a tool-supported method for the efficient synthesis of parametric continuous-
time Markov chains (pCTMC) that correspond to robust designs of a system under …

Markov chain analysis is a key technique in formal verification. A practical obstacle is that all
probabilities in Markov models need to be known. However, system quantities such as …

We employ uncertain parametric CTMCs with parametric transition rates and a prior on the
parameter values. The prior encodes uncertainty about the actual transition rates, while the …

Parameterized verification of temporal properties is an active research area, being extremely
relevant for model-based design of complex systems. In this paper, we focus on parameter …

We consider the problem of predictive monitoring (PM), ie, predicting at runtime the
satisfaction of a desired property from the current system's state. Due to its relevance for …

We consider the problem of predictive monitoring (PM), ie, predicting at runtime future
violations of a system from the current state. We work under the most realistic settings where …