{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:58:26Z","timestamp":1750309106840,"version":"3.41.0"},"reference-count":22,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2004,10,1]],"date-time":"2004-10-01T00:00:00Z","timestamp":1096588800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2004,10]]},"abstract":"<jats:p>A temporal logic is presented for reasoning about the correctness of timed concurrent constraint programs. The logic is based on modalities which allow one to specify what a process produces as a reaction to what its environment inputs. These modalities provide an assumption\/commitment style of specification which allows a sound and complete compositional axiomatization of the reactive behavior of timed concurrent constraint programs.<\/jats:p>","DOI":"10.1145\/1024922.1024926","type":"journal-article","created":{"date-parts":[[2004,10,7]],"date-time":"2004-10-07T17:38:56Z","timestamp":1097170736000},"page":"706-731","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Proving correctness of timed concurrent constraint programs"],"prefix":"10.1145","volume":"5","author":[{"given":"Frank S.","family":"De Boer","sequence":"first","affiliation":[{"name":"CWI and Universiteit Utrecht, Amsterdam, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maurizio","family":"Gabbrielli","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Bologna, Bologna, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maria Chiara","family":"Meo","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Chieti-Pescara, Pescara, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2004,10]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(92)90005-V"},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of 8th Annual IEEE Symposium on Logic In Computer Science, M. Y. Vardi, Ed. IEEE Computer Society Press","author":"Brookes S.","year":"1993","unstructured":"Brookes , S. 1993 . A fully abstract semantics of a shared variable parallel language . In Proceedings of 8th Annual IEEE Symposium on Logic In Computer Science, M. Y. Vardi, Ed. IEEE Computer Society Press , Los Alamitos, CA, 98--109. Brookes, S. 1993. A fully abstract semantics of a shared variable parallel language. In Proceedings of 8th Annual IEEE Symposium on Logic In Computer Science, M. Y. Vardi, Ed. IEEE Computer Society Press, Los Alamitos, CA, 98--109."},{"volume-title":"Proc. IEEE (Special Issue on Another Look at Real-Time Systems). 79","author":"Caspi P.","key":"e_1_2_1_3_1","unstructured":"Caspi , P. , Halbwachs , N. , Pilaud , D. , and Raymond , P . 1991. The synchronous dataflow programming language lustre . Proc. IEEE (Special Issue on Another Look at Real-Time Systems). 79 , 9, 1305--1319. Caspi, P., Halbwachs, N., Pilaud, D., and Raymond, P. 1991. The synchronous dataflow programming language lustre. Proc. IEEE (Special Issue on Another Look at Real-Time Systems). 79, 9, 1305--1319."},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1137\/0207005","article-title":"Soundness and completeness of an axiom system for program verification","volume":"7","author":"Cook S.","year":"1978","unstructured":"Cook , S. 1978 . Soundness and completeness of an axiom system for program verification . SIAM J. Computat. 7 , 1, 70 -- 90 . Cook, S. 1978. Soundness and completeness of an axiom system for program verification. SIAM J. Computat. 7, 1, 70--90.","journal-title":"SIAM J. Computat."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/265943.265954"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2879"},{"volume-title":"Proceedings of TIME 01","author":"de Boer F. S.","key":"e_1_2_1_7_1","unstructured":"de Boer , F. S. , Gabbrielli , M. , and Meo , M. C . 2001. A temporal logic for reasoning about timed concurrent constraint programs . In Proceedings of TIME 01 , C. Bettini and A. Montanari, Eds. IEEE Press, Los Alamitos, CA, 227--233. de Boer, F. S., Gabbrielli, M., and Meo, M. C. 2001. A temporal logic for reasoning about timed concurrent constraint programs. In Proceedings of TIME 01, C. Bettini and A. Montanari, Eds. IEEE Press, Los Alamitos, CA, 227--233."},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of FoSSaCS","volume":"2303","author":"de Boer F. S.","year":"2002","unstructured":"de Boer , F. S. , Gabbrielli , M. , and Meo , M. C . 2002. Proving correctness of timed concurrent constraint programs . In Proceedings of FoSSaCS 2002 , M. Nielsen and U. Engberg, Eds. Lecture Notes in Computer Science , vol. 2303 . Springer-Verlag, Berlin, Germany, 37--51. de Boer, F. S., Gabbrielli, M., and Meo, M. C. 2002. Proving correctness of timed concurrent constraint programs. In Proceedings of FoSSaCS 2002, M. Nielsen and U. Engberg, Eds. Lecture Notes in Computer Science, vol. 2303. Springer-Verlag, Berlin, Germany, 37--51."},{"key":"e_1_2_1_9_1","volume-title":"M","author":"de Boer F. S.","year":"1991","unstructured":"de Boer , F. S. , Kok , J. N. , Palamidessi , C. , and Rutten , J. J. M . M . 1991 . The failure of failures in a paradigm for asynchronous communication. In Proceedings of CONCUR'91, J. C. M. Baeten and J. F. Groote, Eds. Lecture Notes in Computer Science, vol. 527 . Springer-Verlag , Berlin, Germany, 111--126. de Boer, F. S., Kok, J. N., Palamidessi, C., and Rutten, J. J. M. M. 1991. The failure of failures in a paradigm for asynchronous communication. In Proceedings of CONCUR'91, J. C. M. Baeten and J. F. Groote, Eds. Lecture Notes in Computer Science, vol. 527. Springer-Verlag, Berlin, Germany, 111--126."},{"key":"e_1_2_1_10_1","volume-title":"M","author":"de Boer F. S.","year":"1992","unstructured":"de Boer , F. S. , Kok , J. N. , Palamidessi , C. , and Rutten , J. J. M . M . 1992 . On blocks: Locality and asynchronous communication. In Proceedings of the REX Workshop on Semantics : Foundations and Applications, J. W. de Bakker, W. P. de Roever, and G. Rozenberg, Eds. Lecture Notes in Computer Science, vol. 666 . Springer-Verlag , Berlin, Germany, 73--90. de Boer, F. S., Kok, J. N., Palamidessi, C., and Rutten, J. J. M. M. 1992. On blocks: Locality and asynchronous communication. In Proceedings of the REX Workshop on Semantics: Foundations and Applications, J. W. de Bakker, W. P. de Roever, and G. Rozenberg, Eds. Lecture Notes in Computer Science, vol. 666. Springer-Verlag, Berlin, Germany, 73--90."},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of TAPSOFT\/CAAP, S. Abramsky and T. S. E. Maibaum, Eds. Lecture Notes in Computer Science","volume":"493","author":"de Boer F. S.","unstructured":"de Boer , F. S. and Palamidessi , C . 1991. A fully abstract model for concurrent constraint programming . In Proceedings of TAPSOFT\/CAAP, S. Abramsky and T. S. E. Maibaum, Eds. Lecture Notes in Computer Science , vol. 493 . Springer-Verlag, Berlin, Germany, 296--319. de Boer, F. S. and Palamidessi, C. 1991. A fully abstract model for concurrent constraint programming. In Proceedings of TAPSOFT\/CAAP, S. Abramsky and T. S. E. Maibaum, Eds. Lecture Notes in Computer Science, vol. 493. Springer-Verlag, Berlin, Germany, 296--319."},{"key":"e_1_2_1_12_1","volume-title":"Eds. Electronic Notes in Theoretical Computer Science","volume":"48","author":"Falaschi M.","unstructured":"Falaschi , M. , Policriti , A. , and Villanueva , A . 2001. Modeling concurrent systems specified in a temporal concurrent constraint language. In Declarative Programming---Selected Papers from AGP 2000, A. Dovier, M. C. Meo, and A. Omicini , Eds. Electronic Notes in Theoretical Computer Science , vol. 48 . Elsevier Science Publishers, Amsterdam, The Netherlands. Falaschi, M., Policriti, A., and Villanueva, A. 2001. Modeling concurrent systems specified in a temporal concurrent constraint language. In Declarative Programming---Selected Papers from AGP 2000, A. Dovier, M. C. Meo, and A. Omicini, Eds. Electronic Notes in Theoretical Computer Science, vol. 48. Elsevier Science Publishers, Amsterdam, The Netherlands."},{"volume-title":"Proc. IEEE (Special Issue on Another Look at Real-Time Systems). 79","author":"Guernic P. L.","key":"e_1_2_1_13_1","unstructured":"Guernic , P. L. , Borgue , M. L. , Gauthier , T. , and Marie , C. L . 1991. Programming real time applications with signal . Proc. IEEE (Special Issue on Another Look at Real-Time Systems). 79 , 9, 1321--1336. Guernic, P. L., Borgue, M. L., Gauthier, T., and Marie, C. L. 1991. Programming real time applications with signal. Proc. IEEE (Special Issue on Another Look at Real-Time Systems). 79, 9, 1321--1336."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"e_1_2_1_15_1","unstructured":"Henkin L. Monk J. D. and Tarski A. 1971. Cylindric Algebras (Part I). North-Holland Amsterdam The Netherlands.  Henkin L. Monk J. D. and Tarski A. 1971. Cylindric Algebras (Part I). North-Holland Amsterdam The Netherlands."},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the 4th ACM Symposium on Principles of Distributed Computing. ACM Press","author":"Jonsson B.","year":"1985","unstructured":"Jonsson , B. 1985 . A model and a proof system for asynchronous processes . In Proceedings of the 4th ACM Symposium on Principles of Distributed Computing. ACM Press , New York, NY, 49--58. 10.1145\/323596.323601 Jonsson, B. 1985. A model and a proof system for asynchronous processes. In Proceedings of the 4th ACM Symposium on Principles of Distributed Computing. ACM Press, New York, NY, 49--58. 10.1145\/323596.323601"},{"key":"e_1_2_1_17_1","first-page":"298","article-title":"Temporal Concurrent Constraint Programming: Applications and Behavior. Lecture Notes in Computer Science, vol. 2300. Springer-Verlag, Berlin, Germany","volume":"4","author":"Nielsen M.","year":"2002","unstructured":"Nielsen , M. and Valencia , F. 2002 . Temporal Concurrent Constraint Programming: Applications and Behavior. Lecture Notes in Computer Science, vol. 2300. Springer-Verlag, Berlin, Germany , Chapter 4 , 298 -- 324 . Nielsen, M. and Valencia, F. 2002. Temporal Concurrent Constraint Programming: Applications and Behavior. Lecture Notes in Computer Science, vol. 2300. Springer-Verlag, Berlin, Germany, Chapter 4, 298--324.","journal-title":"Chapter"},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of CP","volume":"2239","author":"Palamidessi C.","year":"2001","unstructured":"Palamidessi , C. and Valencia , F. D . 2001. A temporal concurrent constraint programming calculus . In Proceedings of CP 2001 , T. Walsh, Ed. Lecture Notes in Computer Science , vol. 2239 . Springer-Verlag, Berlin, Germany, 302--316. Palamidessi, C. and Valencia, F. D. 2001. A temporal concurrent constraint programming calculus. In Proceedings of CP 2001, T. Walsh, Ed. Lecture Notes in Computer Science, vol. 2239. Springer-Verlag, Berlin, Germany, 302--316."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1996.0064"},{"volume-title":"Proceedings of 17th POPL. ACM Press","author":"Saraswat V. A.","key":"e_1_2_1_21_1","unstructured":"Saraswat , V. A. and Rinard , M . 1990. Concurrent constraint programming . In Proceedings of 17th POPL. ACM Press , New York, NY, 232--245. 10.1145\/96709.96733 Saraswat, V. A. and Rinard, M. 1990. Concurrent constraint programming. In Proceedings of 17th POPL. ACM Press, New York, NY, 232--245. 10.1145\/96709.96733"},{"volume-title":"Proceedings of 18th POPL. ACM Press","author":"Saraswat V. A.","key":"e_1_2_1_22_1","unstructured":"Saraswat , V. A. , Rinard , M. , and Panangaden , P . 1991. Semantics foundations of concurrent constraint programming . In Proceedings of 18th POPL. ACM Press , New York, NY, 333--352. 10.1145\/99583.99627 Saraswat, V. A., Rinard, M., and Panangaden, P. 1991. Semantics foundations of concurrent constraint programming. In Proceedings of 18th POPL. ACM Press, New York, NY, 333--352. 10.1145\/99583.99627"},{"volume-title":"Reactive constraint programming. Tech. rep","author":"Valencia F. D.","key":"e_1_2_1_23_1","unstructured":"Valencia , F. D. 2000. Reactive constraint programming. Tech. rep ., Centre for Basic Research in Computer Science (Brics), Denmark. Valencia, F. D. 2000. Reactive constraint programming. Tech. rep., Centre for Basic Research in Computer Science (Brics), Denmark."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1024922.1024926","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1024922.1024926","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:48:46Z","timestamp":1750286926000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1024922.1024926"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,10]]},"references-count":22,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2004,10]]}},"alternative-id":["10.1145\/1024922.1024926"],"URL":"https:\/\/doi.org\/10.1145\/1024922.1024926","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2004,10]]},"assertion":[{"value":"2004-10-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}