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)
13th International Workshop on Discrete Event Systems, Xi'an, China, May 30 - June 1, 2016 (1550-5227). p. 245-250. (2016)
[Konferensbidrag, refereegranskat]

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 nondiagnosability 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-06-09. Senast ändrad 2016-10-14.
CPL Pubid: 237496


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för signaler och system, Automation



Chalmers infrastruktur