Affiliations: Department of Science, University of Chieti-Pescara G. d'Annunzio, Viale Pindaro 42, 65127 Pescara, Italy, deangelis@sci.unich.it | Department of Informatics, Systems, and Production, University of Rome Tor Vergata, Via del Politecnico 1, 00133 Rome, Italy, pettorossi@disp.uniroma2.it | IASI-CNR, Viale Manzoni 30, 00185 Rome, Italy, maurizio.proietti@iasi.cnr.it
Note: [] Address for correspondence: Department of Science, University of Chieti-Pescara G. d'Annunzio, Viale Pindaro 42, 65127 Pescara, Italy
Abstract: We address the problem of the automatic synthesis of concurrent programs within a framework based on Answer Set Programming (ASP). Every concurrent program to be synthesized is specified by providing both the behavioural and the structural properties it should satisfy. Behavioural properties, such as safety and liveness properties, are specified by using formulas of the Computation Tree Logic, which are encoded as a logic program. Structural properties, such as the symmetry of processes, are also encoded as a logic program. Then, the program which is the union of these two encoding programs, is given as input to an ASP system which returns as output a set of answer sets. Finally, each answer set is decoded into a synthesized program that, by construction, satisfies the desired behavioural and structural properties.
