Search

• < Previous
• 1
• Next >

---

Model Checking One-clock Priced Timed Automata

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.&nbsp;[&hellip;]

---

Continuous Markovian Logics - Axiomatization and Quantified Metatheory

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&nbsp;[&hellip;]

---

Refinement and Difference for Probabilistic Automata

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&nbsp;[&hellip;]

---

Compositional bisimulation metric reasoning with Probabilistic Process Calculi

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&nbsp;[&hellip;]

---

A Complete Quantitative Deduction System for the Bisimilarity Distance on Markov Chains

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&nbsp;[&hellip;]

---

On-the-Fly Computation of Bisimilarity Distances

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&nbsp;[&hellip;]

---

Computing Probabilistic Bisimilarity Distances for Probabilistic Automata

Giorgio Bacci ; Giovanni Bacci ; Kim G. Larsen ; Radu Mardare ; Qiyi Tang ; Franck van Breugel.

The probabilistic bisimilarity distance of Deng et al. has been proposed as a robust quantitative generalization of Segala and Lynch's probabilistic bisimilarity for probabilistic automata. In this paper, we present a characterization of the bisimilarity distance as the solution of a simple&nbsp;[&hellip;]

---