Reactive synthesis (or temporal synthesis) is the field of
computer science
Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to Applied science, practical discipli ...
that studies automatic generation of state machines (e.g.
Moore machine
In the theory of computation, a Moore machine is a finite-state machine whose current output values are determined only by its current state. This is in contrast to a Mealy machine, whose output values are determined both by its current state and ...
s) from high-level specifications (e.g. formulas in
linear temporal logic In logic, linear temporal logic or linear-time temporal logic (LTL) is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths, e.g., a condition will eventually be true, a condition will ...
). "Reactivity" highlights the fact that the synthesized machine interacts with the user, reading an input and producing an output, and never stops its operation.
The synthesis problem was introduced by
Alonzo Church
Alonzo Church (June 14, 1903 – August 11, 1995) was an American mathematician, computer scientist, logician, philosopher, professor and editor who made major contributions to mathematical logic and the foundations of theoretical computer scienc ...
in 1962,
with specifications being formulas in
monadic second-order logic In mathematical logic, monadic second-order logic (MSO) is the fragment of second-order logic where the second-order quantification is limited to quantification over sets. It is particularly important in the logic of graphs, because of Courcelle's t ...
and state machines in the form of digital circuits.
See also
*
Program synthesis In computer science, program synthesis is the task to construct a program that provably satisfies a given high-level formal specification. In contrast to program verification, the program is to be constructed rather than given; however, both fields ...
*
Model checking
In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software systems ...
References
{{reflist
Computer science
Logic