Origins and metamorphoses of the Trinity: logic, nets, automata
Boris A. Trakhtenbrot · 2002
Synthesis and verification of systems with finite state space are well established problems in logic and computer science and have a long history. Precise formulations are based on preliminary formalization of two languages: SPEC (for specifications), IMP (for implementations) and a (satisfaction) relation, sat, included in IMP x SPEC. Clearly, one can consider different languages which may reflect a variety of abstraction levels. It may well happen that an object at a given level may serve as implementation for a higher level and also as specification for a lower level. From this perspective the three level paradigm is instructive and there is a proliferation of its versions. Though many of them are relevant to the subject, in this lecture the author singles out only one to which he refers to as The Trinity, namely: at the highest level-specifications expressed as formulas based on second order monadic logic (SOML); at the intermediate level-formalization of transducers (i.e. transformers of input signals into output signals) via finite sequential automata; at the lower level-formalization of discrete synchronous hardware via logical nets.