Systematic construction of design models from temporal logic based descriptions

This paper presents an approach which allows one to synthesise manufacturing system design models from temporal logic based descriptions. The aim of the approach is to obtain a functional abstraction of the actual system. This functional abstraction realises the external functional behaviour of the modelled system without replicating the actual mechanism. It involves less places and transitions than the accurately modelled system, thus allowing to ease the verification task effort. The approach is illustrated when used to synthesise a machining station. A formal proof of the logical correctness of the obtained model is also presented