Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | https://arxiv.org/abs/2510.24204 |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866918175438798848 |
|---|---|
| author | Neves, Renato |
| author_facet | Neves, Renato |
| contents | We present an adequacy theorem for a concurrent extension of probabilistic GCL. The underlying denotational semantics is based on the so-called mixed powerdomains, which combine non-determinism with probabilistic behaviour. The theorem itself is formulated via M. Smyth's idea of treating observable properties as open sets of a topological space. The proof hinges on a 'topological generalisation' of König's lemma in the setting of probabilistic programming (a result that is proved in the paper as well). One application of the theorem is that it entails semi-decidability w.r.t. whether a concurrent program satisfies an observable property (written in a certain form). This is related to M. Escardo's conjecture about semi-decidability w.r.t. may and must probabilistic testing. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_24204 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | An Adequacy Theorem Between Mixed Powerdomains and Probabilistic Concurrency Neves, Renato Logic in Computer Science F.3.2 We present an adequacy theorem for a concurrent extension of probabilistic GCL. The underlying denotational semantics is based on the so-called mixed powerdomains, which combine non-determinism with probabilistic behaviour. The theorem itself is formulated via M. Smyth's idea of treating observable properties as open sets of a topological space. The proof hinges on a 'topological generalisation' of König's lemma in the setting of probabilistic programming (a result that is proved in the paper as well). One application of the theorem is that it entails semi-decidability w.r.t. whether a concurrent program satisfies an observable property (written in a certain form). This is related to M. Escardo's conjecture about semi-decidability w.r.t. may and must probabilistic testing. |
| title | An Adequacy Theorem Between Mixed Powerdomains and Probabilistic Concurrency |
| topic | Logic in Computer Science F.3.2 |
| url | https://arxiv.org/abs/2510.24204 |