{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:42:33Z","timestamp":1750308153965,"version":"3.41.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2005,7,1]],"date-time":"2005-07-01T00:00:00Z","timestamp":1120176000000},"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. Des. Autom. Electron. Syst."],"published-print":{"date-parts":[[2005,7]]},"abstract":"<jats:p>Assume-guarantee style verification of modules relies on the appropriate modeling of the interaction of the module with its environment. Popular temporal logics such as Computation Tree Logic (CTL) and Linear Temporal Logic (LTL) that were originally defined for closed systems (Kripke structures) do not make any syntactic discrimination between input and output variables. As a result, these logics and their recent derivatives (such as System Verilog, Sugar, Forspec, etc) permit the specification of properties that have some semantic problems when interpreted over open systems or modules. These semantic problems are quite common in practice, but are computationally hard to detect within a given specification. In this article, we propose a new style for writing temporal specifications of open systems that helps the designer to avoid most of these problems. In the proposed style, the basic temporal operators (such as<jats:italic>next<\/jats:italic>and<jats:italic>until<\/jats:italic>) are annotated with<jats:italic>assume<\/jats:italic>constraints over the input variables. We formalize this style through an extension of LTL, namely Open-LTL and an extension of CTL with fairness, called Open-CTL. We show that this simple syntactic separation between the<jats:italic>assume<\/jats:italic>and the<jats:italic>guarantee<\/jats:italic>achieves the desired results. We show that the proposed style can be integrated with traditional symbolic model-checking techniques and present a complete tool for the verification of Verilog RTL modules in isolation.<\/jats:p>","DOI":"10.1145\/1080334.1080337","type":"journal-article","created":{"date-parts":[[2005,11,7]],"date-time":"2005-11-07T16:00:45Z","timestamp":1131379245000},"page":"492-522","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["The open family of temporal logics"],"prefix":"10.1145","volume":"10","author":[{"given":"Ansuman","family":"Banerjee","sequence":"first","affiliation":[{"name":"Indian Institute of Technology, Kharagpur, Kharagpur, WB"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pallab","family":"Dasgupta","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology, Kharagpur, Kharagpur, WB"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2005,7]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/203095.201069"},{"volume-title":"Proceedings of the International Conference on Computer Aided Verification (CAV'01)","author":"Amla N.","key":"e_1_2_1_2_1","unstructured":"Amla , N. , Emerson , E. A. , Kurshan , R. P. , and Namjoshi , K. S . 2001. RTDT: A front-end for efficient model checking of synchronous timing diagrams . In Proceedings of the International Conference on Computer Aided Verification (CAV'01) . 387--390.]] Amla, N., Emerson, E. A., Kurshan, R. P., and Namjoshi, K. S. 2001. RTDT: A front-end for efficient model checking of synchronous timing diagrams. In Proceedings of the International Conference on Computer Aided Verification (CAV'01). 387--390.]]"},{"volume-title":"Proceedings of the International Conference on Correct Hardware Design and Verification Methods (CHARME'99)","author":"Amla N.","key":"e_1_2_1_3_1","unstructured":"Amla , N. , Emerson , E. A. , and Namjoshi , K. S . 1999. Efficient decompositional model checking for regular timing diagrams . In Proceedings of the International Conference on Correct Hardware Design and Verification Methods (CHARME'99) . 67--81.]] Amla, N., Emerson, E. A., and Namjoshi, K. S. 1999. Efficient decompositional model checking for regular timing diagrams. In Proceedings of the International Conference on Correct Hardware Design and Verification Methods (CHARME'99). 67--81.]]"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'01)","volume":"2031","author":"Amla N.","unstructured":"Amla , N. , Emerson , E. A. , Namjoshi , K. S. , and Trefler , R . 2001. Assume-guarantee based compositional reasoning for synchronous timing diagrams . In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'01) . Lecture Notes in Computer Science , vol. 2031 , 465--479.]] Amla, N., Emerson, E. A., Namjoshi, K. S., and Trefler, R. 2001. Assume-guarantee based compositional reasoning for synchronous timing diagrams. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'01). Lecture Notes in Computer Science, vol. 2031, 465--479.]]"},{"volume-title":"Proceedings of the International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'02)","author":"Amla N.","key":"e_1_2_1_5_1","unstructured":"Amla , N. , Emerson , E. A. , Namjoshi , K. S. , and Trefler , R . 2002. Visual specifications for modular reasoning about asynchronous systems . In Proceedings of the International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'02) . 226--242.]] Amla, N., Emerson, E. A., Namjoshi, K. S., and Trefler, R. 2002. Visual specifications for modular reasoning about asynchronous systems. In Proceedings of the International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'02). 226--242.]]"},{"volume-title":"Proceedings of the International Conference on Concurrency Theory (CONCUR'03)","author":"Amla N.","key":"e_1_2_1_6_1","unstructured":"Amla , N. , Emerson , E. A. , Namjoshi , K. S. , and Trefler , R . 2003. Abstract patterns of compositional reasoning . In Proceedings of the International Conference on Concurrency Theory (CONCUR'03) . 423--438.]] Amla, N., Emerson, E. A., Namjoshi, K. S., and Trefler, R. 2003. Abstract patterns of compositional reasoning. In Proceedings of the International Conference on Concurrency Theory (CONCUR'03). 423--438.]]"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'02)","volume":"2280","author":"Armoni R.","unstructured":"Armoni , R. , Fix , L. , Gerth , R. , Ginsburg , B. , Kanza , T. , Lantrer , A. , Modor-Haim , S. , Tiemeyer , A. , Singerman , E. , and Vardi , M. Y . 2002. The ForSpec temporal logic: A new property-specification language . In Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'02) . Lecture Notes in Computer Science , vol. 2280 , Springer Verlag. 296--311.]] Armoni, R., Fix, L., Gerth, R., Ginsburg, B., Kanza, T., Lantrer, A., Modor-Haim, S., Tiemeyer, A., Singerman, E., and Vardi, M. Y. 2002. The ForSpec temporal logic: A new property-specification language. In Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'02). Lecture Notes in Computer Science, vol. 2280, Springer Verlag. 296--311.]]"},{"volume-title":"Proceedings of the International Conference on VLSI Design (VLSI'04)","author":"Banerjee A.","key":"e_1_2_1_8_1","unstructured":"Banerjee , A. , Dasgupta , P. and Chakrabarti , P. P . 2004. Formal verification of modules under real time environment constraints . In Proceedings of the International Conference on VLSI Design (VLSI'04) . 103--108.]] Banerjee, A., Dasgupta, P. and Chakrabarti, P. P. 2004. Formal verification of modules under real time environment constraints. In Proceedings of the International Conference on VLSI Design (VLSI'04). 103--108.]]"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/513918.513954"},{"key":"e_1_2_1_10_1","first-page":"417","article-title":"Proofs of networks of processes","volume":"7","author":"Chandy K. M.","year":"1981","unstructured":"Chandy , K. M. and Misra , J. 1981 . Proofs of networks of processes . IEEE Trans. Softw. Eng. 7 , 4, 417 -- 426 .]] Chandy, K. M. and Misra, J. 1981. Proofs of networks of processes. IEEE Trans. Softw. Eng. 7, 4, 417--426.]]","journal-title":"IEEE Trans. Softw. Eng."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_2_1_12_1","unstructured":"Clarke E. M. Grumberg O. and Peled D. A. 2000. Model Checking MIT Press Cambridge MA.]] Clarke E. M. Grumberg O. and Peled D. A. 2000. Model Checking MIT Press Cambridge MA.]]"},{"volume-title":"Proceedings of the IEEE Asia South Pacific Design Automation Conference (ASPDAC'02)","author":"Dasgupta P.","key":"e_1_2_1_13_1","unstructured":"Dasgupta , P. , Chakrabarti , A. , and Chakrabarti , P. P . 2002. Open computation tree logic for formal verification of modules . In Proceedings of the IEEE Asia South Pacific Design Automation Conference (ASPDAC'02) . 735--740.]] Dasgupta, P., Chakrabarti, A., and Chakrabarti, P. P. 2002. Open computation tree logic for formal verification of modules. In Proceedings of the IEEE Asia South Pacific Design Automation Conference (ASPDAC'02). 735--740.]]"},{"key":"e_1_2_1_14_1","volume-title":"Languages and Programming. Lecture Notes in Computer Science","volume":"85","author":"Emerson E. A.","unstructured":"Emerson , E. A. and Clarke , E. M . 1980. Characterizing correctness properties of parallel programs using fixpoints. Automata , Languages and Programming. Lecture Notes in Computer Science , vol. 85 , Springer-Verlag. 169--181.]] Emerson, E. A. and Clarke, E. M. 1980. Characterizing correctness properties of parallel programs using fixpoints. Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 85, Springer-Verlag. 169--181.]]"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/318593.318620"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/647759.735030"},{"volume-title":"Proceedings of the 7th International Joint Conference on Theory and Practice of Software Development (TAPSOFT'97)","author":"Emerson E. A.","key":"e_1_2_1_17_1","unstructured":"Emerson , E. A. and Trefler , R. J . 1997. Generalized Quantitative temporal reasoning: An automata theoretic-approach . In Proceedings of the 7th International Joint Conference on Theory and Practice of Software Development (TAPSOFT'97) . 189--200.]] Emerson, E. A. and Trefler, R. J. 1997. Generalized Quantitative temporal reasoning: An automata theoretic-approach. In Proceedings of the 7th International Joint Conference on Theory and Practice of Software Development (TAPSOFT'97). 189--200.]]"},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Emerson E. A. and Trefler R. J. 1999. Parametric quantitative temporal reasoning: In Logic in Computer Science. 336--343.]] Emerson E. A. and Trefler R. J. 1999. Parametric quantitative temporal reasoning: In Logic in Computer Science. 336--343.]]","DOI":"10.1109\/LICS.1999.782628"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177725"},{"volume-title":"Proceedings of the International Conference on Computer-Aided Design (ICCAD'00)","author":"Henzinger T.","key":"e_1_2_1_20_1","unstructured":"Henzinger , T. , Qadeer , S. , and Rajamani , S . 2000. Decomposing refinement proofs using assume-guarantee reasoning . In Proceedings of the International Conference on Computer-Aided Design (ICCAD'00) . IEEE Computer Society Press, 245--252.]] Henzinger, T., Qadeer, S., and Rajamani, S. 2000. Decomposing refinement proofs using assume-guarantee reasoning. In Proceedings of the International Conference on Computer-Aided Design (ICCAD'00). IEEE Computer Society Press, 245--252.]]"},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the International Conference of International Federation for Information Processing (IFIP'83)","author":"Jones C. B.","year":"1983","unstructured":"Jones , C. B. 1983 . Specification and design of parallel programs . In Proceedings of the International Conference of International Federation for Information Processing (IFIP'83) . North Holland, 321--332.]] Jones, C. B. 1983. Specification and design of parallel programs. In Proceedings of the International Conference of International Federation for Information Processing (IFIP'83). North Holland, 321--332.]]"},{"volume-title":"Proceedings of the Temporal Logic in Specification Lecture Notes in Computer Science","author":"Josko B.","key":"e_1_2_1_22_1","unstructured":"Josko , B. 1987. MCTL---An extension of CTL for modular verification of concurrent systems . In Proceedings of the Temporal Logic in Specification Lecture Notes in Computer Science , vol. 398 , Springer Verlag . 165--187.]] Josko, B. 1987. MCTL---An extension of CTL for modular verification of concurrent systems. In Proceedings of the Temporal Logic in Specification Lecture Notes in Computer Science, vol. 398, Springer Verlag. 165--187.]]"},{"key":"e_1_2_1_23_1","series-title":"Lecture Notes in Computer Science","volume-title":"Verifying the correctness of AADL Modules using model checking","author":"Josko B.","unstructured":"Josko , B. 1999. Verifying the correctness of AADL Modules using model checking . Lecture Notes in Computer Science , vol. 430 , Springer-Verlag . 386--400.]] Josko, B. 1999. Verifying the correctness of AADL Modules using model checking. Lecture Notes in Computer Science, vol. 430, Springer-Verlag. 386--400.]]"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/647765.735861"},{"volume-title":"Computer Aided Verification of Coordinating Processes: The Automata Theoretic Approach","author":"Kurshan R. P.","key":"e_1_2_1_25_1","unstructured":"Kurshan , R. P. 1994. Computer Aided Verification of Coordinating Processes: The Automata Theoretic Approach . Princeton University Press , Princeton, NJ .]] Kurshan, R. P. 1994. Computer Aided Verification of Coordinating Processes: The Automata Theoretic Approach. Princeton University Press, Princeton, NJ.]]"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/646704.701881"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.734103"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02311231"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Pnueli A. 1984. In transition for global to modular temporal reasoning about programs. In Logics and Models of Concurrent Systems K. R. Apt Ed. Springer-Verlag. 123--144.]] Pnueli A. 1984. In transition for global to modular temporal reasoning about programs. In Logics and Models of Concurrent Systems K. R. Apt Ed. Springer-Verlag. 123--144.]]","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"key":"e_1_2_1_32_1","volume-title":"the International Symposium on Compositionality: The Significant Difference (COMPOS'97)","volume":"1536","author":"Roever W.-P.","year":"1997","unstructured":"Roever , W.-P. 1997 . The need for Compositional Proof Systems. A Survey . In the International Symposium on Compositionality: The Significant Difference (COMPOS'97) . Lecture Notes in Computer Science , vol. 1536 , 1--22.]] Roever, W.-P. 1997. The need for Compositional Proof Systems. A Survey. In the International Symposium on Compositionality: The Significant Difference (COMPOS'97). Lecture Notes in Computer Science, vol. 1536, 1--22.]]"},{"key":"e_1_2_1_34_1","volume-title":"CUDD: CU Decision Diagram Package, Release 2.3.0, User's Manual. Department of Electrical and Computer Engineering","author":"Somenzi F.","year":"1998","unstructured":"Somenzi , F. 1998 . CUDD: CU Decision Diagram Package, Release 2.3.0, User's Manual. Department of Electrical and Computer Engineering , University of Colorado , Boulder, CO .]] Somenzi, F. 1998. CUDD: CU Decision Diagram Package, Release 2.3.0, User's Manual. Department of Electrical and Computer Engineering, University of Colorado, Boulder, CO.]]"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/646823.706907"},{"key":"e_1_2_1_36_1","first-page":"1","article-title":"Dynamic linear time temporal logic","volume":"96","author":"Thiagarajan J.","year":"1999","unstructured":"Thiagarajan , J. and Henriksen , P. S. 1999 . Dynamic linear time temporal logic . Annals Pure Applied Logic 96 , 1 -- 3 , 187--207.]] Thiagarajan, J. and Henriksen, P. S. 1999. Dynamic linear time temporal logic. Annals Pure Applied Logic 96, 1--3, 187--207.]]","journal-title":"Annals Pure Applied Logic"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/646835.759693"}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1080334.1080337","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1080334.1080337","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:18:51Z","timestamp":1750263531000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1080334.1080337"}},"subtitle":["Annotating temporal operators with input constraints"],"short-title":[],"issued":{"date-parts":[[2005,7]]},"references-count":36,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2005,7]]}},"alternative-id":["10.1145\/1080334.1080337"],"URL":"https:\/\/doi.org\/10.1145\/1080334.1080337","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2005,7]]},"assertion":[{"value":"2005-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}