A Framework for Coalgebraic Reward-Sensitive Bisimulation (Extended Version)

1. Problema e Contesto

Il lavoro si concentra sull'estensione delle nozioni classiche di bisimulazione (usate per verificare l'equivalenza comportamentale tra stati di sistemi transizionali) per includere aspetti quantitativi, in particolare le ricompense (rewards) o i costi associati alle transizioni.

• Limitazione delle approcci esistenti: Le bisimulazioni tradizionali sono efficaci per proprietà qualitative (es. "due stati accettano lo stesso linguaggio"), ma non riescono a gestire differenze quantitative come distanze metriche o costi relativi accumulati.
• La sfida: Esistono già nozioni di bisimulazione "gradate" (graded), come le amortised bisimulations, che tracciano differenze di ricompensa entro un certo limite. Tuttavia, manca un'astrazione comune e una teoria categoriale/coalgebraica unificata che spieghi formalmente come le nozioni gradate (che tengono conto delle ricompense) si relazionino e raffinino le nozioni non gradate (qualitative). Non è chiaro come queste due visioni possano essere integrate coerentemente in un unico modello.

2. Metodologia

Gli autori adottano un approccio basato sulla teoria delle categorie e sulla teoria delle coalghe, estendendo il lavoro pionieristico di Hermida e Jacobs sulle fibrazioni.

• Fibrations e Lifting: Utilizzano il framework delle fibrazioni (in particolare CLat⊓-fibrations) per modellare le relazioni di simulazione. Una coalgebra $c: S \to FS$ modella il sistema, mentre un "lifting" del funtore $F$ alla fibrazione permette di definire le simulazioni come coalgebre nella categoria totale.
• Categorical Gluing (Incollaggio Categoriale): Il cuore della metodologia è l'applicazione della tecnica dell'incollaggio categoriale (categorical gluing), mutuata dalla logica categoriale. Questa tecnica permette di combinare due diverse nozioni di coalgebra (una graduata e una non graduata) lungo un morfismo ben comportato.
• Dottrina di Incollaggio Adjoint (Adjoint Gluing Doctrine): Viene introdotta una struttura assiomatica basata su un'aggiunzione fibrata tra due categorie di relazioni:
  1. Una categoria di relazioni non gradate ($E$).
  2. Una categoria di relazioni gradate ($E_g$), dove l'indice della gradazione rappresenta la tolleranza sulla differenza di ricompensa.
     L'aggiunzione coinvolge un funtore di unione ($\exists_g$) che mappa le relazioni gradate in quelle non gradate, e un funtore di inclusione ($\Delta$) che mappa le relazioni non gradate in quelle gradate (come relazioni costanti).

3. Contributi Chiave

1. Framework Unificato per Bisimulazioni Sensibili alle Ricompense:
   Gli autori propongono un modello formale che unifica le simulazioni qualitative e quelle quantitative. Il modello permette di definire una "simulazione incollata" (glued simulation) che contiene sia la struttura relazionale classica sia i vincoli quantitativi sulle ricompense.

2. Costruzione di Coalghe Incollate:
   Viene dimostrata la possibilità di costruire una nuova coalgebra su una categoria incollata (comma category) che proietta coerentemente sia sulla coalgebra graduata che su quella non graduata. Questo fornisce un modo puramente formale per collegare le strutture delle due nozioni di bisimulazione.

3. Teorema di Correttezza Astratta (Soundness Theorem):
   Viene provato un teorema fondamentale (Teorema 3) che stabilisce che se esiste una simulazione graduata (che rispetta i vincoli di ricompensa), allora la sua unione (tramite il funtore $\exists_g$) è necessariamente una simulazione non graduata valida. Questo formalizza l'idea che la nozione graduata è un raffinamento di quella non graduata.

4. Caratterizzazione della Coalgebra Finale:
   Gli autori caratterizzano la coalgebra finale nel modello incollato. Dimostrano che il supporto (carrier) della coalgebra finale è composto dalle coalghe finali delle componenti graduata e non graduata, fornendo principi di ragionamento co-induttivo per i sistemi incollati.

5. Generalità e Applicabilità:
   Il framework è dimostrato essere sufficientemente generale da includere diversi casi d'uso esistenti e nuovi:

   • Automati Deterministici con Ricompense (DAwR): Una nuova nozione di simulazione che limita la differenza di ricompensa accumulata.
   • Amortised Bisimulations: Per sistemi di transizione etichettati (LTS) con costi.
   • Simulazioni su Processi Decisionali di Markov (MDP): Varianti sensibili alle ricompense per sistemi probabilistici.
   • Bisimulazioni Metriche e Relazionali: Per processi di Markov etichettati (LMP), mostrando come le bisimulazioni basate su pseudometriche (es. metrica di Lévy-Prokhorov) si relazionino con quelle basate su relazioni gradate.

4. Risultati Principali

• Teorema 3 (Correttezza): Conferma che la proiezione di una simulazione graduata su una non graduata preserva la validità della simulazione.
• Teorema 4: Dimostra che le coalghe incollate formano una coppia sezione-retrazione rispetto alle coalghe gradate e non gradate, caratterizzando strutturalmente la relazione tra i due livelli.
• Teoremi 7 e 8: Stabiliscono una corrispondenza precisa tra bisimulazioni metriche e relazionali per i processi di Markov, mostrando che sotto certe condizioni (spazio degli stati finito), le due nozioni sono equivalenti tramite l'aggiunzione definita nel framework.
• Proposizione 2 e 3: Forniscono la base semantica per gli automati con ricompense, dimostrando che la "somiglianza graduata" cattura l'inclusione del linguaggio con vincoli di ricompensa, e che la sua unione è una simulazione classica.

5. Significato e Impatto

Questo lavoro è significativo perché:

• Ponte tra Qualitativo e Quantitativo: Offre la prima teoria coalgebraica che spiega sistematicamente come le nozioni di bisimulazione "gradate" (che gestiscono tolleranze e costi) siano un raffinamento naturale delle nozioni classiche.
• Unificazione Concettuale: Sostituisce approcci frammentati con un unico framework basato su fibrazioni e incollaggio categoriale, capace di trattare sistemi deterministici, probabilistici e metrici sotto lo stesso cappello teorico.
• Fondamento per l'Analisi: Fornisce gli strumenti matematici (come la coalgebra finale nel modello incollato) per sviluppare strumenti di verifica formale che devono ragionare simultaneamente sulla correttezza logica e sull'efficienza economica (costi/ricompense) dei sistemi.
• Nuove Direzioni di Ricerca: Introduce nuove nozioni (come le simulazioni su DAwR) e apre la strada all'applicazione di tecniche di logica categoriale (come le relazioni logiche) all'analisi di sistemi quantitativi complessi.

In sintesi, il paper presenta un avanzamento teorico fondamentale che rende possibile trattare le differenze quantitative nelle simulazioni non come un'aggiunta ad hoc, ma come una struttura intrinseca e coerente all'interno della teoria delle coalghe.