Automated deduction of finite-state control programs for reactive systems
Malik, R. (1998). Automated deduction of finite-state control programs for reactive systems. In Proceedings of 15th International Conference on Automated Deduction Lindau, Germany, July 5–10, 1998(pp. 302- 316). Berlin: Springer.
Permanent Research Commons link: https://hdl.handle.net/10289/1702
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 a 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 ∪ C ≒ α.