Author name cluster

Josée Desharnais

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

9 papers

2 author rows

CSL Conference 2026 Conference Paper

ε-Distance via Lévy-Prokhorov Lifting

Josée Desharnais
Ana Sokolova

The most studied and accepted pseudometric for probabilistic processes is one based on the Kantorovich distance between distributions. It comes with many theoretical and motivating results, in particular it is the fixpoint of a given functional and defines a functor on (complete) pseudometric spaces. It is also the foundation for a categorical lifting of pseudometrics. Other notions of behavioural pseudometrics have also been proposed, one of them (ε-distance) based on ε-bisimulation. ε-Distance has the advantages that it is intuitively easy to understand, it relates systems that are conceptually close (for example, an imperfect implementation is close to its specification), and it comes equipped with a natural notion of ε-coupling. Finally, this distance is easy to compute. We show that ε-distance is also the greatest fixpoint of a functional and provides a functor. The latter is obtained by replacing the Kantorovich distance in the lifting functor with the Lévy-Prokhorov distance. In addition, we show that ε-couplings and ε-bisimulations have an appealing coalgebraic characterization.

Details

TCS Journal 2021 Journal Article

General Cops and Robbers games with randomness

Frédéric Simard
Josée Desharnais
François Laviolette

Cops and Robbers games have been studied for the last few decades in computer science and mathematics. As in general pursuit evasion games, pursuers (cops) seek to capture evaders (robbers); however, players move in turn and are constrained to move on a discrete structure, usually a graph, and know the exact location of their opponent. In 2017, Bonato and MacGillivray [2] presented a general characterization of Cops and Robbers games in order for them to be globally studied. However, their model doesn't cover cases where stochastic events may occur, such as the robbers moving in a random fashion. In this paper we present a novel model with stochastic elements that we call a Generalized Probabilistic Cops and Robbers game (GPCR). A typical such game is one where the robber moves according to a probabilistic distribution, either because she is rather lost or drunk than evading, or because she is a robot. We present results to solve GPCR games, thus enabling one to study properties relating to the optimal strategies in large classes of Cops and Robbers games. Some classic Cops and Robbers games properties are also extended.

Details DOI

I&C Journal 2013 Journal Article

Testing probabilistic equivalence through Reinforcement Learning

Josée Desharnais
François Laviolette
Sami Zhioua

Checking if a given system implementation respects its specification is often done by proving that the two are “equivalent”. The equivalence is chosen, in particular, for its computability and of course for its meaning, that is, for its adequacy with what is observable from the two systems (implementation and specification). Trace equivalence is easily testable (decidable from interaction), but often considered too weak; in contrast, bisimulation is accepted as the canonical equivalence for interaction, but it is not testable. Richer than an equivalence is a form of distance: it is zero between equivalent systems, and it provides an estimation of their difference if the systems are not equivalent. Our main contribution is to define such a distance in a context where (1) the two systems to be compared have a stochastic behavior; (2) the model of one of them (e. g. , the implementation) is unknown, hence our only knowledge is obtained by interacting with it; (3) consequently the target equivalence (observed when distance is zero) must be testable. To overcome the problem that the model is unknown, we use a Reinforcement Learning approach that provides powerful stochastic algorithms that only need to interact with the model. Our second main contribution is a new family of testable equivalences, called K-moment. The weakest of them, 1-moment equivalence, is trace equivalence; as K grows, K-moment equivalences become finer, all remaining, as well as their limit, weaker than bisimulation. We propose a framework to define (and test) a bigger class of testable equivalences: Test-Observation-Equivalences (TOEs), and we show how they can be made coarser or not, by tuning some parameters.

Details DOI

I&C Journal 2011 Journal Article

A logical duality for underspecified probabilistic systems

Josée Desharnais
François Laviolette
Amélie Turgeon

This paper establishes a Stone-type duality between specifications and infLMPs. An infLMP is a probabilistic process whose transitions satisfy super-additivity instead of additivity. Interestingly, its simple structure can encode a mix of probabilistic and non-deterministic behavior, which, as we show, is strongly related to another well-known such model: probabilistic automata. Our duality puts in relation the category of infLMPs and a category of abstract representations of them based on properties only. We exhibit a Galois connection between these categories and show that we have an adjunct pair of functors when restricted to LMPs only. Our duality also shows that an infLMP can be considered as a demonic representative of a system’s information. Moreover, it carries forward a view where states are less important, and events, or properties, become the main characters, as it should be in probability theory. Along the way, we show that bisimulation and simulation are naturally interpreted in this setting, and we exhibit the interesting relationship between infLMPs and the usual probabilistic modal logics. This paper is an extended version of a Concur ’09 paper [13]; in particular, the comparison of infLMPs with probabilistic automata and the Galois connection are new.

Details DOI

I&C Journal 2010 Journal Article

Weak bisimulation is sound and complete for pCTL ∗

Josée Desharnais
Vineet Gupta
Radha Jagadeesan
Prakash Panangaden

We investigate weak bisimulation of probabilistic systems in the presence of nondeterminism, i. e. labelled concurrent Markov chains (LCMC) with silent transitions. We develop an approach based on allowing convex combinations of computations, similar to Segala and Lynch’s use of randomized schedulers. The definition of weak bisimulation destroys the additivity property of the probability distributions, yielding instead capacities. The mathematics behind capacities naturally captures the intuition that when we deal with nondeterminism we must work with bounds on the possible probabilities rather than with their exact values. Our analysis leads to three new developments: • We identify a characterization of “image finiteness” for countable-state systems and present a new definition of weak bisimulation for these LCMCs. We prove that our definition coincides with that of Philippou, Lee and Sokolsky for finite state systems. • We show that bisimilar states have matching computations. The notion of matching involves convex combinations of transitions. • We study a minor variant of the probabilistic logic pCTL ∗ – the variation arises from an extra path formula to address action labels. We show that bisimulation is sound and complete for this variant of pCTL ∗. This is an extended complete version of a paper that was presented at CONCUR 2002.

Details DOI

I&C Journal 2006 Journal Article

Bisimulation and cocongruence for probabilistic systems

Vincent Danos
Josée Desharnais
François Laviolette
Prakash Panangaden

We introduce a new notion of bisimulation, called event bisimulation on labelled Markov processes (LMPs) and compare it with the, now standard, notion of probabilistic bisimulation, originally due to Larsen and Skou. Event bisimulation uses a sub σ-algebra as the basic carrier of information rather than an equivalence relation. The resulting notion is thus based on measurable subsets rather than on points: hence the name. Event bisimulation applies smoothly for general measure spaces; bisimulation, on the other hand, is known only to work satisfactorily for analytic spaces. We prove the logical characterization theorem for event bisimulation without having to invoke any of the subtle aspects of analytic spaces that feature prominently in the corresponding proof for ordinary bisimulation. These complexities only arise when we show that on analytic spaces the two concepts coincide. We show that the concept of event bisimulation arises naturally from taking the co-congruence point of view for probabilistic systems. We show that the theory can be given a pleasing categorical treatment in line with general coalgebraic principles. As an easy application of these ideas we develop a notion of “almost sure” bisimulation; the theory comes almost “for free” once we modify Giry’s monad appropriately.

Details DOI

TCS Journal 2004 Journal Article

Metrics for labelled Markov processes

Josée Desharnais
Vineet Gupta
Radha Jagadeesan
Prakash Panangaden

The notion of process equivalence of probabilistic processes is sensitive to the exact probabilities of transitions. Thus, a slight change in the transition probabilities will result in two equivalent processes being deemed no longer equivalent. This instability is due to the quantitative nature of probabilistic processes. In a situation where the process behavior has a quantitative aspect there should be a more robust approach to process equivalence. This paper studies a metric between labelled Markov processes. This metric has the property that processes are at zero distance if and only if they are bisimilar. The metric is inspired by earlier work on logics for characterizing bisimulation and is related, in spirit, to the Hutchinson metric.

Details DOI

I&C Journal 2003 Journal Article

Approximating labelled Markov processes

Josée Desharnais
Vineet Gupta
Radha Jagadeesan
Prakash Panangaden

Labelled Markov processes are probabilistic versions of labelled transition systems. In general, the state space of a labelled Markov process may be a continuum. In this paper, we study approximation techniques for continuous-state labelled Markov processes. We show that the collection of labelled Markov processes carries a Polish-space structure with a countable basis given by finite-state Markov chains with rational probabilities; thus permitting the approximation of quantitative observations (e. g. , an integral of a continuous function) of a continuous-state labelled Markov process by the observations on finite-state Markov chains. The primary technical tools that we develop to reach these results are • A variant of a finite-model theorem for the modal logic used to characterize bisimulation, and • an isomorphism between the poset of Markov processes (ordered by simulation) with the ω-continuous dcpo Proc (defined as the solution of the recursive domain equation Proc=∏ L P Pr (Proc)). The isomorphism between labelled Markov processes and Proc can be independently viewed as a full-abstraction result relating an operational (labelled Markov process) and a denotational (Proc) model and yields a logic complete for reasoning about simulation for continuous-state processes.

Details DOI

I&C Journal 2002 Journal Article

Bisimulation for Labelled Markov Processes

Josée Desharnais
Abbas Edalat
Prakash Panangaden

In this paper we introduce a new class of labelled transition systems—labelled Markov processes— and define bisimulation for them. Labelled Markov processes are probabilistic labelled transition systems where the state space is not necessarily discrete. We assume that the state space is a certain type of common metric space called an analytic space. We show that our definition of probabilistic bisimulation generalizes the Larsen–Skou definition given for discrete systems. The formalism and mathematics is substantially different from the usual treatment of probabilistic process algebra. The main technical contribution of the paper is a logical characterization of probabilistic bisimulation. This study revealed some unexpected results, even for discrete probabilistic systems. • Bisimulation can be characterized by a very weak modal logic. The most striking feature is that one has no negation or any kind of negative proposition. • We do not need any finite branching assumption, yet there is no need of infinitary conjunction. We also show how to construct the maximal autobisimulation on a system. In the finite state case, this is just a state minimization construction. The proofs that we give are of an entirely different character than the typical proofs of these results. They use quite subtle facts about analytic spaces and appear, at first sight, to be entirely nonconstructive. Yet one can give an algorithm for deciding bisimilarity of finite state systems which constructs a formula that witnesses the failure of bisimulation.

Details DOI