Abstract
This paper is concerned with the refinement and control of a certain class of labelled transition systems, called plant automata, via bisimulation quotients.
Refinement means that arbitrary transitions may be removed whereas control allows only removing edges with the same edge label.
The goal is to ensure given LTL properties in the resulting plant automaton.
We give a hardness result for refinement and control and investigate, in particular, the question whether refineability and controllability can be decided by looking at bisimulation quotients.