Polynomial-time verification of the observer property in abstractions

Abstract

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.