Efficient Coalgebraic Partition Refinement
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2017
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866909993518759936 |
|---|---|
| author | Dorsch, Ulrich Milius, Stefan Schröder, Lutz Wißmann, Thorsten |
| author_facet | Dorsch, Ulrich Milius, Stefan Schröder, Lutz Wißmann, Thorsten |
| contents | We present a generic partition refinement algorithm that quotients coalgebraic systems by behavioural equivalence, an important task in reactive verification; coalgebraic generality implies in particular that we cover not only classical relational systems but also various forms of weighted systems. Under assumptions on the type functor that allow representing its finite coalgebras in terms of nodes and edges, our algorithm runs in time $\mathcal{O}(m\cdot \log n)$ where $n$ and $m$ are the numbers of nodes and edges, respectively. Instances of our generic algorithm thus match the runtime of the best known algorithms for unlabelled transition systems, Markov chains, and deterministic automata (with fixed alphabets), and improve the best known algorithms for Segala systems. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_1705_08362 |
| institution | arXiv |
| publishDate | 2017 |
| record_format | arxiv |
| spellingShingle | Efficient Coalgebraic Partition Refinement Dorsch, Ulrich Milius, Stefan Schröder, Lutz Wißmann, Thorsten Data Structures and Algorithms Logic in Computer Science We present a generic partition refinement algorithm that quotients coalgebraic systems by behavioural equivalence, an important task in reactive verification; coalgebraic generality implies in particular that we cover not only classical relational systems but also various forms of weighted systems. Under assumptions on the type functor that allow representing its finite coalgebras in terms of nodes and edges, our algorithm runs in time $\mathcal{O}(m\cdot \log n)$ where $n$ and $m$ are the numbers of nodes and edges, respectively. Instances of our generic algorithm thus match the runtime of the best known algorithms for unlabelled transition systems, Markov chains, and deterministic automata (with fixed alphabets), and improve the best known algorithms for Segala systems. |
| title | Efficient Coalgebraic Partition Refinement |
| topic | Data Structures and Algorithms Logic in Computer Science |
| url | https://arxiv.org/abs/1705.08362 |