IEEE Transactions on Automatic Control · 2014 · 11 citations · 22 references
ComputingComputer ScienceComputer SystemsAlgorithmsFormal MethodsSystems ModelingAutomata TheoryDiscrete-event System ModelingFinite AutomataFinite State Machine ModelingFinite-state MachinesModel CheckingAutomata In Formal VerificationComplexityDiscrete-event ModelingFinite State Machine VerificationFinite-state VerificationNondeterministic Finite AutomataSystem ObservabilityTimed Automata
The observer property is an important condition to be satisfied by abstractions of Discrete Event System (DES) models. This technical note presents a new algorithm that tests if an abstraction of a DES obtained through natural projection has the observer property. The procedure, called OP-Verifier, can be applied to (potentially nondeterministic) automata, with no restriction on the existence of cycles of “non-relevant” events. This procedure has quadratic complexity in the number of states. The performance of the algorithm is illustrated by a set of experiments.
22
Depth-First Search and Linear Graph Algorithms
Robert E. Tarjan · SIAM Journal on Computing · 1972 · 6K citations