Synthesizing Concurrent Programs Using Answer Set Programming

• Autorzy: De Angelis E. , Pettorossi A. , Proietti M.
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

answer set programming; concurrent programs; synthesis

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2012
• Tom: Vol. 120, nr 3/4
• Strony: 205--229
• Opis fizyczny: Bibliogr. 28 poz., tab.

Twórcy

autor

De Angelis E.

autor

Pettorossi A.

autor

Proietti M.

• Department of Science University of Chieti-Pescara G. d’Annunzio Viale Pindaro 42, 65127 Pescara, Italy,

Bibliografia

• [1] K. R. Apt and R. N. Bol. Logic programming and negation: A survey. Journal of Logic Programming, 19, 20:9-71, 1994.
• [2] P. C. Attie and E. A. Emerson. Synthesis of concurrent systems with many similar processes. ACM Transactions on Programming Languages and Systems, 20:51-115, January 1998.
• [3] P. C. Attie and E. A. Emerson. Synthesis of concurrent programs for an atomic read/write model of computation. ACM Transactions on Programming Languages and Systems, 23:187-242, 2001.
• [4] C. Baral. Knowledge representation, reasoning and declarative problem solving. Cambridge University Press, 2003.
• [5] P. Bonatti, F. Calimeri, N. Leone, and F. Ricca. Answer Set Programming. In A. Dovier and E. Pontelli, editors, A 25-Year Perspective on Logic Programming, Lecture Notes in Computer Science 6125. Springer, Berlin, 2010.
• [6] S. Brass and J. Dix. Characterizations of the Stable Semantics by Partial Evaluation. In Logic Programming and Nonmonotonic Reasoning, Lecture Notes in Computer Science 928, pages 85-98. Springer, 1995.
• [7] E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In D. Kozen, editor, Logics of Programs, Lecture Notes in Computer Science 131, pages 52-71. Springer, Berlin, 1982.
• [8] E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
• [9] E. M. Clarke, D. E. Long, and K. L. McMillan. Compositional model checking. In Logic in Computer Science, LICS '89, Proceedings, pages 353-362. IEEE Computer Society, 1989.
• [10] E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, Englewod Cliffs, N.J., 1976.
• [11] C. Drescher, M. Gebser, T. Grote, B. Kaufmann, A. König, M. Ostrowski, and T. Schaub. Conflict-driven disjunctive answer set solving. In G. Brewka and J. Lang, editors, Proc. 11th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR '08), pages 422-432. AAAI Press, 2008.
• [12] T. Eiter, G. Gottlob, and H. Mannila. Disjunctive datalog. ACM Transactions on Database Systems, 22:364-418, 1997.
• [13] E. A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 997-1072. Elsevier, 1990.
• [14] E. A. Emerson and A. P. Sistla. Symmetry and model checking. Formal Methods in System Design, 9:105-131, 1996.
• [15] M. Gebser, J. Lee, and Y. Lierler. Head-elementary-set-free logic programs. In C. Baral, G. Brewka, and J. S. Schlipf, editors, Proceedings of the 9th International Conference on Logic Programming and Nonmotonic Reasoning (LPNMR 2007), Lecture Notes in Computer Science 4483, pages 149-161. Springer, Berlin, 2007.
• [16] M. Gelfond. Answer sets. In F. van Harmelen, V. Lifschitz, and B. Porter, editors, Handbook of Knowledge Representation, chapter 7, pages 285-316. Elsevier, 2007.
• [17] M. Gelfond and V. Lifschitz. Classical negation in logic programs and disjunctive databases. New Generation Computing, 9:365-385, 1991.
• [18] S. Heymans, D. Van Nieuwenborgh, and D. Vermeir. Synthesis from temporal specifications using preferred answer set programming. In M. Coppo, E. Lodi, and G. Pinna, editors, Proceedings of the 9th Italian Conference on Theoretical Computer Science, Lecture Notes in Computer Science 3701, pages 280-294. Springer, Berlin, 2005.
• [19] T. Janhunen and I. Niemelä. GNT - A Solver for Disjunctive Logic Programs. In Logic Programming and Nonmonotonic Reasoning, Lecture Notes in Computer Science 2923, pages 331-335. Springer, 2004.
• [20] O. Kupferman and M. Y. Vardi. Synthesis with incomplete information. In D. M. Gabbay, editor, Applied Logic #16: Advances in Temporal Logic, pages 109-127. Kluwer Academic Publishers, 2000.
• [21] N. Leone, G. Pfeifer,W. Faber, T. Eiter, G. Gottlob, S. Perri, and F. Scarcello. The DLV system for knowledge representation and reasoning. ACM Transaction on Computational Logic, 7:499-562, 2006.
• [22] Z. Manna and P. Wolper. Synthesis of communicating processes from temporal logic specifications. ACM Transactions on Programming Languages and Systems, 6(1):68-93, 1984.
• [23] U. Nilsson and J. Lübcke. Constraint logic programming for local and symbolic model-checking. In J. W. Lloyd, editor, Proceedings of the First International Conference on Computational Logic (CL 2000), London, UK, 24-28 July, Lecture Notes in Artificial Intelligence 1861, pages 384-398. Springer-Verlag, 2000.
• [24] G. L. Peterson. Myths about the mutual exclusion problem. Information Processing Letters, 12(3):115-116, 1981.
• [25] A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proceedings of the 16th ACM SIGPLANSIGACT Symposium on Principles of programming languages (POPL '89), pages 179-190, New York, NY, USA, 1989.
• [26] J. S. Schlipf. Complexity and undecidability results for logic programming. Annals of Mathematics and Artificial Intelligence, 15:257-288, 1995.
• [27] T. Syrjänen. Lparse 1.0 user's manual. http://www.tcs.hut.fi/Software/smodels/, 2002.
• [28] M. Truszczyński. Logic programming for knowledge representation. In V. Dahl and I. Niemelä, editors, Proceedings of the 23rd International Conference on Logic Programming (ICLP '07), Lecture Notes in Computer Science 4670, pages 76-88. Springer, 2007.