Modular finite-state machine analysis
Simon Ware, Robi Malik · 2007
Physical systems can be modelled as a system of finite state automata running in parallel. When a system is represented in this way it can be verified whether or not the given system conforms to given specifications by composing the synchronous product of the system[17]. However composing the synchronous product requires time and memory which is exponential in the number of automata in the system thus making it impractical for more complicated system. One of the methods for getting around this is the modular technique of controllability checking[3], but unfortunately this is also subject to in the worst case requiring time and memory which is exponential in the number of automata in the system. This project has developed new techniques for checking the controllability of systems which have even made it possible to check the controllability of a