Name
Abstract | ||
|---|---|---|
Observability concepts allow to focus on the observable behaviour of a system while abstracting internal details of implementation. In this context, formal verification techniques use behavioural equivalence notions formalizing the idea of indistinguishability of system states. In this paper, we investigate the relation between two behavioural equivalences: the algebraic observational equivalence in the framework of observational algebras with many hidden sorts and automata bisimulation. For that purpose, we propose a transformation of an observational algebra into an infinite deterministic automaton. Consequently, we obtain a subclass of deterministic automata, equivalent to (infinite) Mealy automata, which we call Observational Algebra Automata (OAA). We use a categorical setting to show the equivalence between bisimulation on OAA and algebraic observational equivalence. Therefore we extend the hidden algebras result concerning observational equivalence and bisimulation coincidence to the non-monadic case. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-642-14455-4_9 | Developments in Language Theory |
Keywords | Field | DocType |
behavioural equivalence notion,behavioural equivalence,algebraic observational equivalence,deterministic automaton,observational equivalence,hidden sort,hidden algebra,bisimulation coincidence,automata bisimulation,observational algebra,formal verification | Discrete mathematics,Combinatorics,Observability,Algebraic number,Deterministic automaton,Observational equivalence,Computer science,Automaton,Equivalence (measure theory),Bisimulation,Formal verification | Conference |
Volume | ISSN | ISBN |
6224 | 0302-9743 | 3-642-14454-3 |
Citations | PageRank | References |
0 | 0.34 | 18 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mouhebeddine Berrima | 1 | 3 | 1.07 |
| Narjes Ben Rajeb | 2 | 29 | 3.77 |