Models, Algorithms, Logics and Tools
Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday
Page
%P
-
Article
On decidability of recursive weighted logics
In this paper, we develop and study two recursive weighted logics (RWLs) \(\mathcal {L}^w\) ...
-
Chapter and Conference Paper
Timed Comparisons of Semi-Markov Processes
Semi-Markov processes are Markovian processes in which the firing time of transitions is modelled by probabilistic distributions over positive reals interpreted as the probability of firing a transition at a c...
-
Chapter and Conference Paper
A Hemimetric Extension of Simulation for Semi-Markov Decision Processes
Semi-Markov decision processes (SMDPs) are continuous-time Markov decision processes where the residence-time on states is governed by generic distributions on the positive real line.
-
Chapter and Conference Paper
Weighted Branching Systems: Behavioural Equivalence, Behavioural Distance, and Their Logical Characterisations
In this work, we extend the notion of branching bisimulation to weighted systems. We abstract away from singular transitions and allow for bisimilar systems to match each other using finite paths of similar be...
-
Book
-
Chapter and Conference Paper
A Complete Approximation Theory for Weighted Transition Systems
We propose a way of reasoning about minimal and maximal values of the weights of transitions in a weighted transition system (WTS). This perspective induces a notion of bisimulation that is coarser than the cl...
-
Chapter and Conference Paper
On the Total Variation Distance of Semi-Markov Chains
Semi-Markov chains (SMCs) are continuous-time probabilistic transition systems where the residence time on states is governed by generic distributions on the positive real line.
-
Chapter and Conference Paper
Converging from Branching to Linear Metrics on Markov Chains
We study the strong and strutter trace distances on Markov chains (MCs). Our interest in these metrics is motivated by their relation to the probabilistic
-
Chapter and Conference Paper
Decidability and Expressiveness of Recursive Weighted Logic
Labelled weighted transition systems (LWSs) are transition systems labelled with actions and real numbers. The numbers represent the costs of the corresponding actions in terms of resources. Recursive Weighted...
-
Chapter and Conference Paper
A Decidable Recursive Logic for Weighted Transition Systems
In this paper we develop and study the Recursive Weighted Logic (RWL), a multi-modal logic that expresses qualitative and quantitative properties of labelled weighted transition systems (LWSs). LWSs are transi...
-
Chapter
Bisimulation on Markov Processes over Arbitrary Measurable Spaces
We introduce a notion of bisimulation on labelled Markov Processes over generic measurable spaces in terms of arbitrary binary relations. Our notion of bisimulation is proven to coincide with the coalgebraic d...
-
Chapter and Conference Paper
Continuity Properties of Distances for Markov Processes
In this paper we investigate distance functions on finite state Markov processes that measure the behavioural similarity of non-bisimilar processes. We consider both probabilistic bisimilarity metrics, and tra...
-
Chapter and Conference Paper
Strong Completeness for Markovian Logics
In this paper we present Hilbert-style axiomatizations for three logics for reasoning about continuous-space Markov processes (MPs): (i) a logic for MPs defined for probability distributions on measurable stat...
-
Chapter and Conference Paper
The BisimDist Library: Efficient Computation of Bisimilarity Distances for Markovian Models
This paper presents a library for exactly computing the bisimilarity Kantorovich-based pseudometrics between Markov chains and between Markov decision processes. These are distances that measure the behavioral...
-
Chapter and Conference Paper
Computing Behavioral Distances, Compositionally
We propose a general definition of composition operator on Markov Decision Processes with rewards (MDPs) and identify a well behaved class of operators, called safe, that are guaranteed to be non-extensive w.r.t....
-
Chapter and Conference Paper
Stochastic Pi-calculus Revisited
We develop a version of stochastic Pi-calculus with a semantics based on measure theory. We define the behaviour of a process in a rate environment using measures over the measurable space of processes induced...
-
Chapter and Conference Paper
On-the-Fly Exact Computation of Bisimilarity Distances
This paper proposes an algorithm for exact computation of bisimilarity distances between discrete-time Markov chains introduced by Desharnais et. al. Our work is inspired by the theoretical results presented b...
-
Chapter and Conference Paper
Taking It to the Limit: Approximate Reasoning for Markov Processes
We develop a fusion of logical and metrical principles for reasoning about Markov processes. More precisely, we lift metrics from processes to sets of processes satisfying a formula and explore how the satisfa...
-
Chapter
Combining Epistemic Logic and Hennessy-Milner Logic
We define an epistemic logic for labelled transition systems by introducing equivalence relations for the agents on the states of the labelled transition system. The idea is that agents observe the dynamics of...
-
Chapter and Conference Paper
Decidability of Modular Logics for Concurrency
The modular logics we approach in this paper are logics for concurrent systems that reflect both behavioral and structural properties of systems. They combine dynamic modalities that express behavioural proper...
