{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:35:13Z","timestamp":1750307713132,"version":"3.41.0"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCR-0092724"],"award-info":[{"award-number":["CCR-0092724"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Auton. Adapt. Syst."],"published-print":{"date-parts":[[2009,1]]},"abstract":"<jats:p>We concentrate on automatic revision of untimed and real-time programs with respect to UNITY properties. The main focus of this article is to identify instances where addition of UNITY properties can be achieved efficiently (in polynomial time) and where the problem of adding UNITY properties is difficult (NP-complete). Regarding efficient revision, we present a sound and complete algorithm that adds a single<jats:italic>leads-to<\/jats:italic>property (respectively,<jats:italic>bounded-time leads-to<\/jats:italic>property) and a conjunction of<jats:italic>unless, stable<\/jats:italic>, and<jats:italic>invariant<\/jats:italic>properties (respectively,<jats:italic>bounded-time unless<\/jats:italic>and<jats:italic>stable<\/jats:italic>) to an existing untimed (respectively, real-time) UNITY program in polynomial-time in the state space (respectively, region graph) of the given program. Regarding hardness results, we show that (1) while one<jats:italic>leads-to<\/jats:italic>(respectively,<jats:italic>ensures<\/jats:italic>) property can be added in polynomial-time, the problem of adding two such properties (or any combination of<jats:italic>leads-to<\/jats:italic>and<jats:italic>ensures<\/jats:italic>) is NP-complete, (2) if maximum non-determinism is desired then the problem of adding even a single<jats:italic>leads-to<\/jats:italic>property is NP-complete, and (3) the problem of providing maximum non-determinism while adding a single<jats:italic>bounded-time leads-to<\/jats:italic>property to a real-time program is NP-complete (in the size of the program's region graph) even if the original program satisfies the corresponding<jats:italic>unbounded leads-to<\/jats:italic>property.<\/jats:p>","DOI":"10.1145\/1462187.1462192","type":"journal-article","created":{"date-parts":[[2009,2,10]],"date-time":"2009-02-10T16:42:19Z","timestamp":1234284139000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Complexity results in revising UNITY programs"],"prefix":"10.1145","volume":"4","author":[{"given":"Borzoo","family":"Bonakdarpour","sequence":"first","affiliation":[{"name":"Michigan State University,"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ali","family":"Ebnenasir","sequence":"additional","affiliation":[{"name":"Michigan Technological University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sandeep S.","family":"Kulkarni","sequence":"additional","affiliation":[{"name":"Michigan State University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2009,2,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/227595.227602"},{"volume-title":"Proceedings of the Conference on Hybrid Systems: Computation and Control (HSCC). 19--30","author":"Asarin E.","key":"e_1_2_1_3_1"},{"volume-title":"Proceedings of the IFAC Symposium on System Structure and Control. 469--474","author":"Asarin E.","key":"e_1_2_1_4_1"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/383043.383044"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/646734.701461"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/963778.963782"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-3886-0"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70952-7_17"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-49823-0_9"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDCS.2007.109"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_16"},{"volume-title":"Proceedings of the International Conference on Computer Aided Verification (CAV). 180--192","author":"Bouyer P.","key":"e_1_2_1_13_1"},{"key":"e_1_2_1_14_1","unstructured":"Carruth A. 1994. Real-time UNITY. Tech. rep. CS-TR-94-10 University of Texas at Austin. Carruth A. 1994. Real-time UNITY. Tech. rep. CS-TR-94-10 University of Texas at Austin."},{"key":"e_1_2_1_15_1","unstructured":"Chandy K. M. and Misra J. 1988. Parallel Program Design: A Foundation. Addison-Wesley Longman Publishing Co. Inc. Boston MA. Chandy K. M. and Misra J. 1988. Parallel Program Design: A Foundation. Addison-Wesley Longman Publishing Co. Inc. Boston MA."},{"volume-title":"Proceedings of the International Conference on Computer-Aided Verificaion (CAV). 399--409","author":"Courcoubetis C.","key":"e_1_2_1_16_1"},{"volume-title":"Proceedings of the International Conference on Concurrency Theory (CONCUR).","author":"de Alfaro L.","key":"e_1_2_1_17_1"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/361179.361202"},{"key":"e_1_2_1_19_1","unstructured":"Dijkstra E. W. 1990. A Discipline of Programming. Prentice-Hall Englewood Cliffs NJ. Dijkstra E. W. 1990. A Discipline of Programming. Prentice-Hall Englewood Cliffs NJ."},{"volume-title":"Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS). 571--582","author":"D'Souza D.","key":"e_1_2_1_20_1"},{"volume-title":"Proceedings of the Conference on Principles of Distributed Systems (OPODIS). 275--290","author":"Ebnenasir A.","key":"e_1_2_1_21_1"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(83)90017-5"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539795290477"},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Faella M. LaTorre S. and Murano A. 2002. Dense real-time games. In Logic in Computer Science (LICS). 167--176. Faella M. LaTorre S. and Murano A. 2002. Dense real-time games. In Logic in Computer Science (LICS). 167--176.","DOI":"10.1109\/LICS.2002.1029826"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"volume-title":"Proceedings of the Conference on Computer Aided Verification (CAV). 226--238","author":"Jobstmann B.","key":"e_1_2_1_26_1"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-2001-2_9"},{"volume-title":"Proceedings of the Symposium on Reliable Distributed Systems (SRDS). 130--140","author":"Kulkarni S. S.","key":"e_1_2_1_28_1"},{"key":"e_1_2_1_29_1","doi-asserted-by":"crossref","unstructured":"Kulkarni S. S. Arora A. and Ebnenasir A. 2007. Software Engineering and Fault-Tolerance. World Scientific Publishing Co. Pte. Ltd (Chapter: Adding Fault-Tolerance to State Machine-Based Designs). Kulkarni S. S. Arora A. and Ebnenasir A. 2007. Software Engineering and Fault-Tolerance. World Scientific Publishing Co. Pte. Ltd (Chapter: Adding Fault-Tolerance to State Machine-Based Designs).","DOI":"10.1142\/9789812778864_0003"},{"volume-title":"Proceedings of the International Conference on Distributed Computing Systems (ICDCS). 337--344","author":"Kulkarni S. S.","key":"e_1_2_1_30_1"},{"volume-title":"Proceedings of the International Conference on Distributed Computing Systems (ICDCS).","author":"Kulkarni S. S.","key":"e_1_2_1_31_1"},{"volume-title":"Proceedings of the International Conference on Dependable Systems and Networks (DSN). 209--219","author":"Kulkarni S. S.","key":"e_1_2_1_32_1"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01797143"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/9.61009"},{"volume-title":"Proceedings of the Conference on Formal Modeling and Analysis of Timed Systems (FORMATS). 274--289","author":"Maler O.","key":"e_1_2_1_35_1"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/357233.357237"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.312117"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054198000301"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"volume-title":"Proceedings of the International Colloqium on Automata, Languages, and Programming (ICALP). 652--671","author":"Pnueli A.","key":"e_1_2_1_40_1"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.21072"},{"key":"e_1_2_1_42_1","unstructured":"Rohloff K. R. 2004. Computations on distributed discrete-event systems. Ph.D. thesis University of Michigan. Rohloff K. R. 2004. Computations on distributed discrete-event systems. Ph.D. thesis University of Michigan."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2003.812780"},{"volume-title":"Proceedings of the International Conference on Computer Aided Verification (CAV). 58--64","year":"2002","author":"Thomas W.","key":"e_1_2_1_44_1"},{"volume-title":"Proceedings of the Conference on Implementation and Application of Automata (CIAA). 11--22","author":"Wallmeier N.","key":"e_1_2_1_45_1"}],"container-title":["ACM Transactions on Autonomous and Adaptive Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1462187.1462192","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1462187.1462192","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:30:15Z","timestamp":1750253415000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1462187.1462192"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,1]]},"references-count":45,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2009,1]]}},"alternative-id":["10.1145\/1462187.1462192"],"URL":"https:\/\/doi.org\/10.1145\/1462187.1462192","relation":{},"ISSN":["1556-4665","1556-4703"],"issn-type":[{"type":"print","value":"1556-4665"},{"type":"electronic","value":"1556-4703"}],"subject":[],"published":{"date-parts":[[2009,1]]},"assertion":[{"value":"2007-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-02-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}