A deductive database support to the specification of concurrent system

We present an approach to the specification of concurrent systems, by means of a deductive database management system. The approach is based on the synthesis of logic formulas: starting from a temporal logic formula, that represents the requirements of a system, a general model for such formula, is derived. From this model, all the concurrent systems satisfying the formula can be generated. A graphical representation of the model is given through a deductive database management system GEDBLOG. Moreover, we show that this model can be used to verify when a given system, obtained elsewhere, is in agreement with its requirements expressed by logical specifications.