A Single Complete Relational Rule for Coalgebraic Refinement
| Autor: | Luís Soares Barbosa, César J. Rodrigues, José Nuno Oliveira |
|---|---|
| Přispěvatelé: | Universidade do Minho |
| Rok vydání: | 2009 |
| Předmět: |
Pure mathematics
General Computer Science Coalgebra Monotonic function 0102 computer and information sciences 02 engineering and technology 01 natural sciences Transition systems Theoretical Computer Science Morphism Computer Science::Logic in Computer Science Mathematics::Category Theory 0202 electrical engineering electronic engineering information engineering Mathematics Discrete mathematics Science & Technology Functor Binary relation coalgebraic refinement 020207 software engineering Refinement Relational operator Relational calculus 010201 computation theory & mathematics Transition system Computer Science(all) |
| Zdroj: | Repositório Científico de Acesso Aberto de Portugal Repositório Científico de Acesso Aberto de Portugal (RCAAP) instacron:RCAAP |
| ISSN: | 1571-0661 |
| DOI: | 10.1016/j.entcs.2009.12.014 |
| Popis: | A transition system can be presented either as a binary relation or as a coalgebra for the powerset functor, each representation being obtained from the other by transposition. More generally, a coalgebra for a functor F generalises transition systems in the sense that a shape for transitions is determined by F, typically encoding a signature of methods and observers. This paper explores such a duality to frame in purely relational terms coalgebraic refinement, showing that relational (data) refinement of transition relations, in its two variants, downward and upward (functional) simulations, is equivalent to coalgebraic refinement based on backward and forward morphisms, respectively. Going deeper, it is also shown that downward simulation provides a complete relational rule to prove coalgebraic refinement. With such a single rule the paper defines a pre-ordered calculus for refinement of coalgebras, with bisimilarity as the induced equivalence. The calculus is monotonic with respect to the main relational operators and arbitrary relator F, therefore providing a framework for structural reasoning about refinement. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect