CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Diagnosability Verification Using Compositional Branching Bisimulation

Mona Noori Hosseini (Institutionen för signaler och system, Automation) ; Bengt Lennartson (Institutionen för signaler och system, Automation)
Göteborg : Chalmers University of Technology, 2016. - 8 s.

This paper presents an efficient diagnosability verification technique, based on a general abstraction approach. More specifically, branching bisimulation including state labels with explicit divergence (BBSD) is defined. This bisimulation preserves the temporal logic property that verifies diagnosability. Based on a proposed BBSD algorithm, compositional abstraction for modular diagnosability verification is shown to offer a significant state space reduction in comparison to state-of-the-art techniques. This is illustrated by verifying non-diagnosability analytically for a set of synchronized components, where the abstracted solution is independent of the number of components and the number of observable events.

Denna post skapades 2016-04-13. Senast ändrad 2016-04-13.
CPL Pubid: 234619


Läs direkt!

Lokal fulltext (fritt tillgänglig)

Institutioner (Chalmers)

Institutionen för signaler och system, Automation


Elektroteknik och elektronik

Chalmers infrastruktur