4 results
Patricia Bouyer ; Kim G. Larsen ; Nicolas Markey.
We consider the model of priced (a.k.a. weighted) timed automata, an extension of timed automata with cost information on both locations and transitions, and we study various model-checking problems for that model based on extensions of classical temporal logics with cost constraints on modalities. […]
Published on June 20, 2008
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.
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