5 results
Radu Mardare ; Luca Cardelli ; Kim G. Larsen.
Continuous Markovian Logic (CML) is a multimodal logic that expresses quantitative and qualitative properties of continuous-time labelled Markov processes with arbitrary (analytic) state-spaces, henceforth called continuous Markov processes (CMPs). The modalities of CML evaluate the rates of the […]
Published on November 29, 2012
Benoît Delahaye ; Uli Fahrenberg ; Kim G. Larsen ; Axel Legay.
This paper studies a difference operator for stochastic systems whose specifications are represented by Abstract Probabilistic Automata (APAs). In the case refinement fails between two specifications, the target of this operator is to produce a specification APA that represents all witness PAs of […]
Published on August 26, 2014
Giorgio Bacci ; Giovanni Bacci ; Kim G. Larsen ; Radu Mardare.
We propose a distance between continuous-time Markov chains (CTMCs) and study the problem of computing it by comparing three different algorithmic methodologies: iterative, linear program, and on-the-fly. In a work presented at FoSSaCS'12, Chen et al. characterized the bisimilarity distance of […]
Published on June 30, 2017
Giorgio Bacci ; Giovanni Bacci ; Kim G. Larsen ; Radu Mardare.
In this paper we propose a complete axiomatization of the bisimilarity distance of Desharnais et al. for the class of finite labelled Markov chains. Our axiomatization is given in the style of a quantitative extension of equational logic recently proposed by Mardare, Panangaden, and Plotkin (LICS […]
Published on November 16, 2018
Daniel Gebler ; Kim G. Larsen ; Simone Tini.
We study which standard operators of probabilistic process calculi allow for compositional reasoning with respect to bisimulation metric semantics. We argue that uniform continuity (generalizing the earlier proposed property of non-expansiveness) captures the essential nature of compositional […]
Published on April 27, 2017