Automated deduction of finite-state control programs for reactive systems

摘要

We propose an approach towards the automatic synthesis of finite-state reactive control programs from purely declarative, logic specifications of their requirements. More precisely, if P is a set of propositional temporal logic formulas, representing the environment of a reactive system, and if #alpha# is a propositional formula, representing a safety requirement, then we point out how to deduce a most general set C of formulas, representing a control program, such that P union C |=#alpha#.