## T1 - Uniform metric derivation for quantitative models of computation

In order to study services from a quantitative perspective, there is a need to shift from classical models of computation, such as labelled transition systems, to more elaborate ones, such as weighted or probabilistic automata, where quantities can easily be modelled.

Many probabilistic systems have been studied in the literature. A coalgebraic treatment of probabilistic systems appeared in [BSdV], where different types of systems and their
behavioural equivalence are coalgebraically characterized via several functors on
the category of sets. In [vBW] a notion of metric was introduced for one type of probabilistic system, the so-called probabilistic reactive systems.

It is the main goal of this task to uniformly define notions of metrics for all the systems considered in [BSdV].
In order to do that, we will study how to ``lift'' all the functors considered from the category of sets to metric spaces.

The approach in [vBW], from which we will certainly draw inspiration, strongly relies on the existence of a final coalgebra. For the functor of reactive systems, this follows by a theorem in [TR], but for many important functors
(e.g., not-contractive functors allowing to define the so called metrics without discount) this theorem does not apply. Thus, another important issue consists in studying the conditions guaranteeing the existence of final coalgebras for the class of functors we will study.

There was work in the nineties trying to address this problem [ABBR,BvBR]. We will use this work as basis of our study. In [BvBR] the authors consider generalized metric spaces, which could be useful for defining metrics for linear-systems, which we see as an interesting application for the general theory.

Main contributions:

- A notion of metric, defined uniformly, for a large class of probabilistic systems
- Conditions on the existence of final coalgebras for the functors we will consider to model probabilistic systems
- Instantiation of the the general framework considered in the two points above to linear systems.

**Research team**: (BI) Bolseiro de Investigação (Mestrado) 1; Luís Soares Barbosa; Luís Monteiro; Alexandra Silva

**Deliverables**: Given its foundational character, the main deliverables of this task will be a number of research papers. We envisage 5 papers, two of which in mainstream conferences (such as LICS, Fossacs or ICALP), two in a workshop (such as CMCS or WADT) and the other in a journal (TCS, Information & Computation).