<p>I assume that you are asking for the construction of the probability space for a given LMP. Although, I do not have a particular reference for this construction, there are a few closely related constructions that might help you. </p>

<p>The usual way (in my oppinion) would be to construct the probability spaces via Borel $\sigma$-algebras. The following book is a good reference for such probability spaces: Robert B. Ash and Catherine A. Doleans-Dade. Probability &amp; Measure Theory.
Elsevier Science, 2000. </p>

<p>If that should not suffice, e.g. if you need a construction providing Lebesgue measurability, you could take a look at this paper, which is on a related system model (Continuous-time markov decision processes): <a href="http://link.springer.com/article/10.1007%2Fs00236-011-0140-0" rel="nofollow">http://link.springer.com/article/10.1007%2Fs00236-011-0140-0</a></p>

CC BY-SA 3.0
2013-03-28T15:25:34.813Z
I should have mentioned, that I am familiar with general probability theory and related measure-theoretical concepts. I cannot see though, how does your answer provide any insight into my question. In particular, Lebesgue measure seem to be of help in the linked paper *only* due to the fact that a continuous-time model is considered.
SBF
CC BY-SA 3.0
2013-03-28T19:47:33.943Z
From the question and a quick look at the linked paper, I got the impression that the difference of LMPs and PAs is that the state spaces might be infinite, and even continuous. Instead of considering CTMDPs as automata with a set of discrete states $S$ and a continuous time domain, you can look at them as automata with discrete steps on a continuous state space ($S\times\mathbb{R}^{\geq 0}$).
Markus
CC BY-SA 3.0
2013-03-29T09:07:36.110Z
That makes two problems closer, agree - you mean, the discrete steps are counters of transitions, whereas the state is the original state and the inter transition time? However, even if we can adopt the behavioural semantics of ctMDP to LMP, that may not be the intended one. I rather wonder about sources that discuss explicitly the behavior of LMP.
SBF
CC BY-SA 3.0
2013-03-29T16:27:18.873Z
Yes, that was what I wanted to say. Now I also see a little bit better what you mean by the asking for the "intended" behvioural semantics of LMPs. However, as you noted in your comment on Vijay's answer, I see no way around defining traces and their probability densities first.
Markus
CC BY-SA 3.0
2013-03-29T16:38:13.777Z
Ok, actually the way through trace distributions is natural for me (I have a background in stochastic processes), but since I'm not familiar with many TCS concepts, I thought that people from that area may think about a different concept of behavior.
SBF
CC BY-SA 3.0
2013-03-26T18:13:08.437Z
2013-03-26T18:21:33.930Z
2013-03-26T18:21:33.930Z
Markus
<p>[Comment space was too short]</p>

<p>I think it depends on what you mean by behaviour. Probabilistic automata follow in the tradition of finite automata, so their behaviour is defined in terms of their language or traces. Labelled Markov Processes follow in the tradition of process algebra, where it is known that processes can be compared using a variety of preorders typically starting with bisimulation. You do have notions of bisimulation defined for LMPs and in that paper. Bisimulation is stronger than trace equivalence, as you may know, so the behaviour you are interested in is the tree unfolding rooted at a given state. Definition 3.1 of the paper you have linked gives approximations of this tree. </p>

CC BY-SA 3.0
2013-03-28T15:40:15.630Z
That's indeed an interesting point to think about bisimulations as a hint for a possible definition of an LMP. However, to say that *Bisimulation is stronger than trace equivalence* for LMP, don't we have to define the trace equivalence for LMP first? Otherwise, we seem to discuss the equivalence of models (as tuples, using bisimulation) without saying what do these models mean exactly.
SBF
CC BY-SA 3.0
2013-04-01T08:42:50.160Z
I am confused. Doesn't the definition of trace equivalence follow the same construction as for probabilistic automata?
Vijay D
CC BY-SA 3.0
2013-04-01T10:09:14.760Z
That's exactly my question. I think, it would be natural to define the trace equivalence of LMP in an equivalent way as it is done for PA (we can't really say *in the same way* since some measurability issues have to be addressed). However, as I mentioned in my comment to @Markus, I am not sure whether this is an intended way to define traces of LMP. That's why in my question I said that I am interested in a *source* that explicitly defines the behavior of LMP.
SBF
CC BY-SA 3.0
2013-03-26T16:53:06.317Z
2013-03-26T16:53:06.317Z
Vijay D
<p><a href="http://www.cs.mcgill.ca/~prakash/Pubs/fullmetric.pdf" rel="nofollow">Labelled Markov Processes</a> (LMP) seem to be a generalization of <a href="http://www.cs.mcgill.ca/~prakash/Pubs/fullmetric.pdf" rel="nofollow">Probabilistic Automata</a> (PA) studied by Segala to the case of the general state space. Namely, any LMP is given by a be a finite set of labels $A$, a measurable state space $(X,\mathscr B(X))$ and substochastic kernels
$$
  \forall a\in A,\;\tau_a:X\times \mathscr B(X)\to [0,1].
$$
In case $X$ is finite and $\mathscr B(X) = 2^X$, we obtain simply a PA.</p>

<p>The behavior of the PA is clear to me: it is given by trace distributions over the sequences of labels - e.g. in Section 3 <a href="http://www.cs.mcgill.ca/~prakash/Pubs/fullmetric.pdf" rel="nofollow">here</a>. I would expect the very same definition of the behavior for LMP, but I have never seen it defined formally anywhere. I would appreciate if you can hint upon a source describing the behaviour of a LMP.</p>

<p><strong>Updated:</strong> after a short discussion, I have to clarify some details. I am familiar with measure-theoretical approach to probability and stochastic processes, and I think that behavioral semantics of PA extends directly to LMP modulo dealing with Borel or universally measurable transition kernels to characterize an adversary. However, I am not sure whether this is a possible way to define a behavior of LMP, or it is the intended one. For example, it may perhaps be described in the PhD thesis of J. Desharnais (which I do not have an access to).</p>

CC BY-SA 3.0
2013-03-26T11:32:51.577Z
There is a book on [Labelled Markov Processes](http://www.worldscientific.com/worldscibooks/10.1142/p595).
Dave Clarke
CC BY-SA 3.0
2013-03-26T11:35:21.020Z
@DaveClarke: Thanks, I have it in my office, there the LMP is defined just as a tuple, and no probability space construction/other definition of the behavior is given (unless I miss it).
SBF
<reference-request><pr.probability><markov-chains><probabilistic-automata>
Behaviour of Labelled Markov Processes
SBF
# Behaviour of Labelled Markov Processes

(Asked by: username_0 on 2013-03-26)

[Labelled Markov Processes](http://www.cs.mcgill.ca/~prakash/Pubs/fullmetric.pdf) (LMP) seem to be a generalization of [Probabilistic Automata](http://www.cs.mcgill.ca/~prakash/Pubs/fullmetric.pdf) (PA) studied by Segala to the case of the general state space. Namely, any LMP is given by a be a finite set of labels $A$, a measurable state space $(X,\mathscr B(X))$ and substochastic kernels
$$
\forall a\in A,\;\tau\_a:X\times \mathscr B(X)\to [0,1].
$$
In case $X$ is finite and $\mathscr B(X) = 2^X$, we obtain simply a PA.

The behavior of the PA is clear to me: it is given by trace distributions over the sequences of labels - e.g. in Section 3 [here](http://www.cs.mcgill.ca/~prakash/Pubs/fullmetric.pdf). I would expect the very same definition of the behavior for LMP, but I have never seen it defined formally anywhere. I would appreciate if you can hint upon a source describing the behaviour of a LMP.

**Updated:** after a short discussion, I have to clarify some details. I am familiar with measure-theoretical approach to probability and stochastic processes, and I think that behavioral semantics of PA extends directly to LMP modulo dealing with Borel or universally measurable transition kernels to characterize an adversary. However, I am not sure whether this is a possible way to define a behavior of LMP, or it is the intended one. For example, it may perhaps be described in the PhD thesis of J. Desharnais (which I do not have an access to).

**Tags:** reference-request, pr.probability, markov-chains, probabilistic-automata

> **Comments:**
> **username_1**: There is a book on [Labelled Markov Processes](http://www.worldscientific.com/worldscibooks/10.1142/p595).  
> **username_0**: @DaveClarke: Thanks, I have it in my office, there the LMP is defined just as a tuple, and no probability space construction/other definition of the behavior is given (unless I miss it).  

---

## 2 answers

### Answer by username_2 on 2013-03-26. Score: 2

I assume that you are asking for the construction of the probability space for a given LMP. Although, I do not have a particular reference for this construction, there are a few closely related constructions that might help you.

The usual way (in my oppinion) would be to construct the probability spaces via Borel $\sigma$-algebras. The following book is a good reference for such probability spaces: Robert B. Ash and Catherine A. Doleans-Dade. Probability & Measure Theory.
Elsevier Science, 2000.

If that should not suffice, e.g. if you need a construction providing Lebesgue measurability, you could take a look at this paper, which is on a related system model (Continuous-time markov decision processes): <http://link.springer.com/article/10.1007%2Fs00236-011-0140-0>

> **Comments:**
> **username_0**: I should have mentioned, that I am familiar with general probability theory and related measure-theoretical concepts. I cannot see though, how does your answer provide any insight into my question. In particular, Lebesgue measure seem to be of help in the linked paper *only* due to the fact that a continuous-time model is considered.  
> **username_2**: From the question and a quick look at the linked paper, I got the impression that the difference of LMPs and PAs is that the state spaces might be infinite, and even continuous. Instead of considering CTMDPs as automata with a set of discrete states $S$ and a continuous time domain, you can look at them as automata with discrete steps on a continuous state space ($S\times\mathbb{R}^{\geq 0}$).  
> **username_0**: That makes two problems closer, agree - you mean, the discrete steps are counters of transitions, whereas the state is the original state and the inter transition time? However, even if we can adopt the behavioural semantics of ctMDP to LMP, that may not be the intended one. I rather wonder about sources that discuss explicitly the behavior of LMP.  
> **username_2**: Yes, that was what I wanted to say. Now I also see a little bit better what you mean by the asking for the "intended" behvioural semantics of LMPs. However, as you noted in your comment on Vijay's answer, I see no way around defining traces and their probability densities first.  
> **username_0**: Ok, actually the way through trace distributions is natural for me (I have a background in stochastic processes), but since I'm not familiar with many TCS concepts, I thought that people from that area may think about a different concept of behavior.  

---

### Answer by username_3 on 2013-03-26. Score: 2

[Comment space was too short]

I think it depends on what you mean by behaviour. Probabilistic automata follow in the tradition of finite automata, so their behaviour is defined in terms of their language or traces. Labelled Markov Processes follow in the tradition of process algebra, where it is known that processes can be compared using a variety of preorders typically starting with bisimulation. You do have notions of bisimulation defined for LMPs and in that paper. Bisimulation is stronger than trace equivalence, as you may know, so the behaviour you are interested in is the tree unfolding rooted at a given state. Definition 3.1 of the paper you have linked gives approximations of this tree.

> **Comments:**
> **username_0**: That's indeed an interesting point to think about bisimulations as a hint for a possible definition of an LMP. However, to say that *Bisimulation is stronger than trace equivalence* for LMP, don't we have to define the trace equivalence for LMP first? Otherwise, we seem to discuss the equivalence of models (as tuples, using bisimulation) without saying what do these models mean exactly.  
> **username_3**: I am confused. Doesn't the definition of trace equivalence follow the same construction as for probabilistic automata?  
> **username_0**: That's exactly my question. I think, it would be natural to define the trace equivalence of LMP in an equivalent way as it is done for PA (we can't really say *in the same way* since some measurability issues have to be addressed). However, as I mentioned in my comment to @username_2, I am not sure whether this is an intended way to define traces of LMP. That's why in my question I said that I am interested in a *source* that explicitly defines the behavior of LMP.  

---

