Giovanni Bacci

Model Checking Reward Markov Models with Uncertainties

Giovanni Bacci, Mikkel Hansen, and Kim G. Larsen.

We consider the problem of analysing Markov reward models (MRMs) in the presence of imprecise or uncertain rewards. Properties of interests for their analysis are (i) probabilistic bisimilarity, and (ii) specifications expressed as probabilistic reward CTL formulae (PRCTL). We consider two extensions of the notion of MRM, namely (a) constrained Markov reward models, i.e., MRMs with rewards parametric on a set variables subject to some constraints, and (b) stochastic Markov reward models, i.e., MRMs with rewards modelled as real-valued random variables as opposed to precise rewards. Our approach is based on quantifier elimination for linear real arithmetic which is used for computing a symbolic representation of the set or parameter valuations satisfying a given property in the form of a quantifier-free first-order formula in the linear theory of the reals. Our work finds applications in model repair, where parameters need to be tuned so as to satisfy the desired specification, as well as in robustness analysis in the presence of stochastic perturbations.

On the Verification of Weighted Kripke Structures Under Uncertainty

Giovanni Bacci, Mikkel Hansen, and Kim G. Larsen.

We considered the problem of checking weighted CTL properties for weighted Kripke structures in presence of imprecise weights. We consider two extensions of the notion of weighted Kripke structures, namely (i) parametric weighted Kripke structures, having transitions weights modelled as affine maps over a set of parameters and, (ii) weight-uncertain Kripke structures, having transition labelled by real-valued random variables as opposed to precise real valued weights.

Optimal and Robust Controller Synthesis using Energy Timed Automata with Uncertainty

Giovanni Bacci, Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, Nicolas Markey Pierre-Alain Reynier.

This is a Mathematica package that implements the algorithm for solving the energy-constrained infinite-run problem for flat segmented energy timed Automata. The package requires one to install Mjollnir for performing quantifier elimination. The source code includes a real industrial example of a hydraulic oil pump provided by the German company HYDAC within the European project Quasimodo

Metric-based State Space Reduction for Markov Chains

Giovanni Bacci, Giorgio Bacci, Kim G. Larsen, and Radu Mardare.

This is a Mathematica package that implements an Expectation Maximization algorithm that iteratively better and better approximant of a given Markov chain. The output of this iterative procedure is a sub-optimal approximant of the original Markov chain with respect to the bisimilarity distance of Desharnais, Gupta, Jagadeesan, and Panangaden [TCS'04]

On-the-fly Computation of Bisimilarity Distances

Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare.

This is a Mathematica package that provides different methods for computing the (lambda-discounted) bisimilarity distances between Continuous-Time Markov Chains (CTMCs). Our bisimilarity distance allows one to provide an ad-hoc distance between state-labels that is meant to represent the distance over static behaviors.

The package implements three alternative methods:

• Iterative method
• Linear Program Method
• On-the-fly method

In particular the last method allows one to compute the bisimilarity distance between a specific pairs of states avoiding the entire exploration of the state space of the CTMC.

Computing Behavioral Distances, Compositionally

Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare.

This is a prototype written in Mathematica that implements a method for computing the behavioral distance of Ferns et al. for Markov Decisions Processes with rewards (MDPs). This method exactly computes the distance between a given set of states without exploring the entire set of states of the MDP. Moreover, for MDPs built using safe (non-extensive) operators, this method is able to exploit the structure of the system, further reducing the computation time.

The BisimDist Library: Efficient Computation of Bisimilarity Distances for Markovian Models

Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare.

The BisimDist library consists of two Mathematica packages, namely the MCDist and MDPDist packages, that implement an on-the-fly method for computing the behavioral distance respectively for Markov Chains (MCs) and Markov Decision Processes with rewards (MDPs). The on-the-fly strategy allows one to compute the distance between a given set of states avoiding an entire exploration of state space of the system. The MCDist package computes the distance of Desharnais et al. for MCs whereas, the MDPDist implements the computation of the distance of Ferns et al. for MDPs.