Qais

T3: Computational Layer: algorithms

Language equivalences of finite DAs and bisimilarity of finite LTSs can be respectively computed via the Myhill-Nerode algorithm and the partition refinement algorithm. These two are just well-known instances of an abstract coalgebraic algorithm, that has inspired the definition of new algorithms for more peculiar equivalences [BM] and, recently, for approximating behavioural metrics [vBW]. In our opinion, the latter represents an evident proof of the effectiveness of the coalgebraic treatment of metrics. Indeed, the resulting algorithm is both the most elegant and the most efficient, amongst those introduced so far.

In this task we propose to obtain:

• Generalized Algorithm. We would like to give an abstract definition of the algorithm of [vBW] in order to have algorithms for computing all the behavioural metrics characterized in T1. Another interesting line of research for approximating metrics of linear systems consists in extending [Rut07].

• Metric Quotient. Given a system of a certain type, we can quotient its state space w.r.t. behavioural equivalence and obtain a new system that is equivalent to the original one (the new system is usually the minimal system of the equivalence class). We would like to investigate the possibility of a metric quotient that allows to merge those states whose distance is smaller than a certain ε. We conjecture that the distance between the original system and the merged one should be bounded by kε for a certain constant k.

• On-the-fly checking. Another approach for computing behavioural equivalences is the on-the-fly checking method [FM]. The underlying principle is to incrementally build a bisimulation relating the systems that we want to prove equivalent. Whenever these are modeled in a formal language, the method allows also to prove equivalences amongst systems with an infinite state space [Hir]. Analogously, we could automatically check if the distance of two systems is smaller than a certain ε by incrementally computing a metric bisimulation (as defined in T2) that assigns distance ε to these systems. This method could be effective for automatically over-approximating the distances of systems with continuous state space.

• Prototype tool. In order to test the effectiveness of the algorithms developed in the above points, we willl implemente a prototype tool encoding all of them. This prototype tool will be developed in a functional programming language, such as Haskell, and will be linked to the coinductive theorem prover CIRC.

Research team: 2 x BI 12 M, Luís Soares Barbosa; José Nuno Oliveira; Jorge Sousa Pinto (?)

Deliverables: We envisage the publication of three research articles in mainstream conferences (such as TACAS, FASE or CAV), one in a workshop and one journal paper (such as SCP or FAC), plus the development of prototype tool, which will be made publicly available.