Details

Autor(en) / Beteiligte

• Pena, P.N.
• Cury, J.E.R.
• Lafortune, S.

Titel

Polynomial-time verification of the observer property in abstractions

Ist Teil von

• 2008 American Control Conference, 2008, p.465-470

Ort / Verlag

IEEE

Erscheinungsjahr

2008

Quelle

IEEE Electronic Library Online

Beschreibungen/Notizen

• This paper presents an algorithm to test if an abstraction obtained through natural projection has the observer property, without having to compute the abstraction. The original automaton and the set of events to be kept by the projection are inputs to the algorithm. An automaton, the verifier, is built such that the verification of the property becomes a verification of reachability of a special state. The complexity of the algorithm is polynomial in the size of the state space of the automaton. Two examples are presented to illustrate the algorithm.