We examine the determinization of monitors for HML with recursion. We demonstrate that every monitor is equivalent to a deterministic one, which is at most doubly exponential in size with respect to the original monitor. When monitors are described as CCS-like processes, this doubly exponential bound is optimal. When (deterministic) monitors are described as finite automata (or as their labeled transition systems), then they can be exponentially more succinct than their CCS process form.
Determinizing monitors for HML with recursion
Luca Aceto
;
2020-01-01
Abstract
We examine the determinization of monitors for HML with recursion. We demonstrate that every monitor is equivalent to a deterministic one, which is at most doubly exponential in size with respect to the original monitor. When monitors are described as CCS-like processes, this doubly exponential bound is optimal. When (deterministic) monitors are described as finite automata (or as their labeled transition systems), then they can be exponentially more succinct than their CCS process form.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
2020_JLogAlgebraicMethodsProgram_111_Aceto.pdf
non disponibili
Tipologia:
Versione Editoriale (PDF)
Licenza:
Non pubblico
Dimensione
921.58 kB
Formato
Adobe PDF
|
921.58 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
