{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,2]],"date-time":"2023-02-02T13:10:27Z","timestamp":1675343427663},"reference-count":74,"publisher":"Association for Computing Machinery (ACM)","issue":"2","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2000,3]]},"abstract":"\n Translating linear temporal logic formulas to automata has proven to be an effective approach for implementing linear-time model-checking, and for obtaining many extensions and improvements to this verification method. On the other hand, for branching temporal logic, automata-theoretic techniques have long been thought to introduce an exponential penalty, making them essentially useless for model-checking. Recently, Bernholtz and Grumberg [1993] have shown that this exponential penalty can be avoided, though they did not match the linear complexity of non-automata-theoretic algorithms. In this paper, we show that\n alternating tree automata<\/jats:italic>\n are the key to a comprehensive automata-theoretic framework for branching temporal logics. Not only can they be used to obtain optimal decision procedures, as was shown by Muller et al., but, as we show here, they also make it possible to derive optimal model-checking algorithms. Moreover, the simple combinatorial structure that emerges from the automata-theoretic approach opens up new possibilities for the implementation of branching-time model checking and has enabled us to derive improved space complexity bounds for this long-standing problem.\n <\/jats:p>","DOI":"10.1145\/333979.333987","type":"journal-article","created":{"date-parts":[[2002,7,27]],"date-time":"2002-07-27T11:26:13Z","timestamp":1027769173000},"page":"312-360","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":295,"title":["An automata-theoretic approach to branching-time model checking"],"prefix":"10.1145","volume":"47","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[{"name":"Hebrew Univ., Jerusalem, Israel"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[{"name":"Rice Univ, Houston, TX"}]},{"given":"Pierre","family":"Wolper","sequence":"additional","affiliation":[{"name":"Univ. de Li\u00e8ge, Li\u00e8ge Sart-Tilman, Belgium"}]}],"member":"320","published-online":{"date-parts":[[2000,3]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"100","volume-title":"Proceedings of the 38th IEEE Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos, Calif.","author":"ALUR R.","year":"1997","unstructured":"ALUR , R. , HENZINGER , T. A. , AND KUPFERMAN , 0. 1997 . Alternating-time temporal logic . In Proceedings of the 38th IEEE Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos, Calif. , pp. 100 - 109 .]] ALUR, R., HENZINGER, T. A., AND KUPFERMAN, 0. 1997. Alternating-time temporal logic. In Proceedings of the 38th IEEE Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., pp. 100-109.]]"},{"key":"e_1_2_1_2_1","series-title":"Lecture Notes in Computer Science","first-page":"142","volume-title":"Computer Aided Verification, Proceedings of the 7th International Conference (Liege, Belgium, July)","author":"ANDERSEN H. R.","unstructured":"ANDERSEN , H. R. , AND VERGAUWEN , B. 1995. Efficient checking of behavioural relations and modal assertions using fixed-point inversion . In Computer Aided Verification, Proceedings of the 7th International Conference (Liege, Belgium, July) . Lecture Notes in Computer Science , vol. 939 . Springer-Verlag , New York , pp. 142 - 154 .]] ANDERSEN, H. R., AND VERGAUWEN, B. 1995. Efficient checking of behavioural relations and modal assertions using fixed-point inversion. In Computer Aided Verification, Proceedings of the 7th International Conference (Liege, Belgium, July). Lecture Notes in Computer Science, vol. 939. Springer-Verlag, New York, pp. 142-154.]]"},{"key":"e_1_2_1_3_1","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Proceedings of the European Symposium on Programming (ESOP)","author":"ANDERSON H. R.","unstructured":"ANDERSON , H. R. 1992. Model checking and boolean graphs . In Proceedings of the European Symposium on Programming (ESOP) . Lecture Notes in Computer Science , vol. 582 . Springer- Verlag , New York , pp. 1 - 19 .]] ANDERSON, H. R. 1992. Model checking and boolean graphs. In Proceedings of the European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 582. Springer- Verlag, New York, pp. 1-19.]]"},{"key":"e_1_2_1_4_1","first-page":"62","volume-title":"Temporal Logic in Specification","author":"BANIEQBAL B.","unstructured":"BANIEQBAL , B. , AND BARRINGER , H. 1987. Temporal logic with fixed points . In Temporal Logic in Specification , B. Banieqbal, H. Barringer, and A. Pnueli, Eds. Lecture Notes in Computer Science, vol. 398 . Springer-Verlag , New York, pp. 62 - 74 .]] BANIEQBAL, B., AND BARRINGER, H. 1987. Temporal logic with fixed points. In Temporal Logic in Specification, B. Banieqbal, H. Barringer, and A. Pnueli, Eds. Lecture Notes in Computer Science, vol. 398. Springer-Verlag, New York, pp. 62-74.]]"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/320613.320614"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/320064.320066"},{"key":"e_1_2_1_7_1","series-title":"Lecture Notes in Computer Science","first-page":"262","volume-title":"Proceedings of the 4th Conference on Concurrency Theory (Hildesheim, Aug.)","author":"BERNHOLTZ","unstructured":"BERNHOLTZ , 0., AND GRUMBERG , 0. 1993. Branching time temporal logic and amorphous tree automata . In Proceedings of the 4th Conference on Concurrency Theory (Hildesheim, Aug.) . Lecture Notes in Computer Science , vol. 715 . Springer-Verlag , New York , pp. 262 - 277 .]] BERNHOLTZ, 0., AND GRUMBERG, 0. 1993. Branching time temporal logic and amorphous tree automata. In Proceedings of the 4th Conference on Concurrency Theory (Hildesheim, Aug.). Lecture Notes in Computer Science, vol. 715. Springer-Verlag, New York, pp. 262-277.]]"},{"key":"e_1_2_1_8_1","series-title":"Lecture Notes on Computer Science","volume-title":"Proceedings of the 1996 Workshop on Tools and Algorithms for the Construction and Analysis of Systems","author":"BHAT G.","unstructured":"BHAT , G. , AND CLEAVELAND , R. 1996a. Efficient local model-checking for fragments of the modal \/x-calculus . In Proceedings of the 1996 Workshop on Tools and Algorithms for the Construction and Analysis of Systems . Lecture Notes on Computer Science , vol. 1055 . Springer-Verlag , Berlin, Germany .]] BHAT, G., AND CLEAVELAND, R. 1996a. Efficient local model-checking for fragments of the modal \/x-calculus. In Proceedings of the 1996 Workshop on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes on Computer Science, vol. 1055. Springer-Verlag, Berlin, Germany.]]"},{"key":"e_1_2_1_9_1","first-page":"304","volume-title":"Proceedings of the llth IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif.","author":"BHAT G.","year":"1996","unstructured":"BHAT , G. , AND CLEAVELAND , R. 1996 b. Efficient model checking via the equational\/x-calculus . In Proceedings of the llth IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif. , pp. 304 - 312 .]] BHAT, G., AND CLEAVELAND, R. 1996b. Efficient model checking via the equational\/x-calculus. In Proceedings of the llth IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., pp. 304-312.]]"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/322234.322243"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_2_1_12_1","first-page":"124","volume-title":"Eds. Lecture Notes in Computer Science","volume":"803","author":"CLARKE E. M.","year":"1993","unstructured":"CLARKE , E. M. , GRUMBERG , 0., AND LONG , D. 1993 . Verification tools for finite-state concurrent systems. In Decade of Concurrency--Reflections and Perspectives (Proceedings of REX School) J. W. de Bakker, W.-P. de Roever, and G. Rozenberg , Eds. Lecture Notes in Computer Science , vol. 803 . Springer-Verlag, New York , pp. 124 - 175 .]] CLARKE, E. M., GRUMBERG, 0., AND LONG, D. 1993. Verification tools for finite-state concurrent systems. In Decade of Concurrency--Reflections and Perspectives (Proceedings of REX School) J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, Eds. Lecture Notes in Computer Science, vol. 803. Springer-Verlag, New York, pp. 124-175.]]"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01383878"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00121128"},{"issue":"3","key":"e_1_2_1_15_1","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","article-title":"Linear-time algorithms for testing the satisfiability of propositional horn formulae","volume":"1","author":"DOWLING W. F.","year":"1984","unstructured":"DOWLING , W. F. , AND GALLIER , J.H. 1984 . Linear-time algorithms for testing the satisfiability of propositional horn formulae . J. Logic Prog. 1 , 3 , 267 - 284 .]] DOWLING, W. F., AND GALLIER, J.H. 1984. Linear-time algorithms for testing the satisfiability of propositional horn formulae. J. Logic Prog. 1, 3, 267-284.]]","journal-title":"J. Logic Prog."},{"key":"e_1_2_1_16_1","series-title":"Lecture Notes in Computer Science","first-page":"79","volume-title":"Proceedings of the Workshop on Logic of Programs","author":"EMERSON E.A.","unstructured":"EMERSON , E.A. 1985. Automata, tableaux, and temporal logics . In Proceedings of the Workshop on Logic of Programs . Lecture Notes in Computer Science , vol. 193 . Springer-Verlag , New York , pp. 79 - 87 .]] EMERSON, E.A. 1985. Automata, tableaux, and temporal logics. In Proceedings of the Workshop on Logic of Programs. Lecture Notes in Computer Science, vol. 193. Springer-Verlag, New York, pp. 79-87.]]"},{"key":"e_1_2_1_17_1","series-title":"Lecture Notes in Computer Science","first-page":"41","volume-title":"Proceedings of the VIII-th BANFF Higher Order Workshop","author":"EMERSON E.A.","unstructured":"EMERSON , E.A. 1996. Automated temporal reasoning about reactive systems . In Proceedings of the VIII-th BANFF Higher Order Workshop . Lecture Notes in Computer Science , vol. 1043 . Springer- Verlag , New York , pp. 41 - 101 .]] EMERSON, E.A. 1996. Automated temporal reasoning about reactive systems. In Proceedings of the VIII-th BANFF Higher Order Workshop. Lecture Notes in Computer Science, vol. 1043. Springer- Verlag, New York, pp. 41-101.]]"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4999"},{"key":"e_1_2_1_19_1","first-page":"328","volume-title":"Proceedings of the 29th IEEE Symposium on Foundations of Computer Science (White Plains, N.Y., Oct.) IEEE Computer Society Press, Los Alamitos, Calif.","author":"EMERSON E. A.","year":"1988","unstructured":"EMERSON , E. A. , AND JUTLA , C. 1988 . The complexity of tree automata and logics of programs . In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science (White Plains, N.Y., Oct.) IEEE Computer Society Press, Los Alamitos, Calif. , pp. 328 - 337 .]] EMERSON, E. A., AND JUTLA, C. 1988. The complexity of tree automata and logics of programs. In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science (White Plains, N.Y., Oct.) IEEE Computer Society Press, Los Alamitos, Calif., pp. 328-337.]]"},{"key":"e_1_2_1_20_1","first-page":"368","volume-title":"Proceedings of the 32nd IEEE Symposium on Foundations of Computer Science (San Juan, P.R., Oct.). IEEE Computer Society Press, Los Alamitos, Calif.","author":"EMERSON E. A.","year":"1991","unstructured":"EMERSON , E. A. , AND JUTLA , C. 1991 . Tree automata, Mu-calculus and determinacy . In Proceedings of the 32nd IEEE Symposium on Foundations of Computer Science (San Juan, P.R., Oct.). IEEE Computer Society Press, Los Alamitos, Calif. , pp. 368 - 377 .]] 10.1109\/SFCS.1991.185392 EMERSON, E. A., AND JUTLA, C. 1991. Tree automata, Mu-calculus and determinacy. In Proceedings of the 32nd IEEE Symposium on Foundations of Computer Science (San Juan, P.R., Oct.). IEEE Computer Society Press, Los Alamitos, Calif., pp. 368-377.]] 10.1109\/SFCS.1991.185392"},{"key":"e_1_2_1_21_1","series-title":"Lecture Notes in Computer Science","first-page":"385","volume-title":"Computer Aided Verification, Proceedings of the 5th International Conference (Elounda, Crete, June)","author":"EMERSON E. A.","unstructured":"EMERSON , E. A. , JUTLA , C. , AND SISTLA , A. P. 1993. On model-checking for fragments of \/x-calculus . In Computer Aided Verification, Proceedings of the 5th International Conference (Elounda, Crete, June) . Lecture Notes in Computer Science , vol. 697 . Springer-Verlag , New York , pp. 385 - 396 .]] EMERSON, E. A., JUTLA, C., AND SISTLA, A. P. 1993. On model-checking for fragments of \/x-calculus. In Computer Aided Verification, Proceedings of the 5th International Conference (Elounda, Crete, June). Lecture Notes in Computer Science, vol. 697. Springer-Verlag, New York, pp. 385-396.]]"},{"key":"e_1_2_1_22_1","first-page":"267","volume-title":"Proceedings of the 1st Symposium on Logic in Computer Science","author":"EMERSON E. A.","year":"1986","unstructured":"EMERSON , E. A. , AND LEI , C.-L. 1986 . Efficient model checking in fragments of the propositional \/x-calculus . In Proceedings of the 1st Symposium on Logic in Computer Science ( Cambridge, Mass., June). pp. 267 - 278 .]] EMERSON, E. A., AND LEI, C.-L. 1986. Efficient model checking in fragments of the propositional \/x-calculus. In Proceedings of the 1st Symposium on Logic in Computer Science (Cambridge, Mass., June). pp. 267-278.]]"},{"key":"e_1_2_1_23_1","first-page":"14","volume-title":"Proceedings of the 16th Annual ACM Symposium on Theory of Computing (Washington, D.C., Apr. 30-May 2). ACM","author":"EMERSON E. A.","year":"1984","unstructured":"EMERSON , E. A. , AND SISTLA , A.P. 1984 . Deciding branching time logic . In Proceedings of the 16th Annual ACM Symposium on Theory of Computing (Washington, D.C., Apr. 30-May 2). ACM , New York , pp. 14 - 24 .]] 10.1145\/800057.808661 EMERSON, E. A., AND SISTLA, A.P. 1984. Deciding branching time logic. In Proceedings of the 16th Annual ACM Symposium on Theory of Computing (Washington, D.C., Apr. 30-May 2). ACM, New York, pp. 14-24.]] 10.1145\/800057.808661"},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","article-title":"Propositional dynamic logic of regular programs","volume":"18","author":"FISCHER M. J.","year":"1979","unstructured":"FISCHER , M. J. , AND LADNER , R. E. 1979 . Propositional dynamic logic of regular programs . J. Comput. Syst. Sci. 18 , 194 - 211 .]] FISCHER, M. J., AND LADNER, R. E. 1979. Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18, 194-211.]]","journal-title":"J. Comput. Syst. Sci."},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the 14th Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif.]]","author":"GRAEDEL E.","year":"1999","unstructured":"GRAEDEL , E. , AND WALUKIEWICZ , I. 1999 . Guarded fixed point logic . In Proceedings of the 14th Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif.]] GRAEDEL, E., AND WALUKIEWICZ, I. 1999. Guarded fixed point logic. In Proceedings of the 14th Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif.]]"},{"key":"e_1_2_1_26_1","volume-title":"Limits of parallel computation","author":"GREENLAW R.","unstructured":"GREENLAW , R. , HOOVER , H. J. , AND RUZZO , W.L. 1995. Limits of parallel computation . Oxford University Press , Oxford, England .]] GREENLAW, R., HOOVER, H. J., AND RUZZO, W.L. 1995. Limits of parallel computation. Oxford University Press, Oxford, England.]]"},{"key":"e_1_2_1_27_1","series-title":"Lecture Notes in Computer Science","first-page":"514","volume-title":"Proceedings of the 7th Conference on Concurrency Theory (Pisa, Italy, Aug.)","author":"HENZINGER T. A.","unstructured":"HENZINGER , T. A. , KUPFERMAN , 0., AND VARDI , M.Y. 1996. A space-efficient on-the-fly algorithm for real-time model checking . In Proceedings of the 7th Conference on Concurrency Theory (Pisa, Italy, Aug.) . Lecture Notes in Computer Science , vol. 1119 . Springer-Verlag , New York , pp. 514 - 529 .]] HENZINGER, T. A., KUPFERMAN, 0., AND VARDI, M.Y. 1996. A space-efficient on-the-fly algorithm for real-time model checking. In Proceedings of the 7th Conference on Concurrency Theory (Pisa, Italy, Aug.). Lecture Notes in Computer Science, vol. 1119. Springer-Verlag, New York, pp. 514-529.]]"},{"issue":"3","key":"e_1_2_1_28_1","doi-asserted-by":"crossref","first-page":"384","DOI":"10.1016\/0022-0000(81)90039-8","article-title":"Number of quantifiers is better than number of tape cells","volume":"22","author":"IMMERMAN N.","year":"1981","unstructured":"IMMERMAN , N. 1981 . Number of quantifiers is better than number of tape cells . J. Comput. Syst. Sci. 22 , 3 , 384 - 406 .]] IMMERMAN, N. 1981. Number of quantifiers is better than number of tape cells. J. Comput. Syst. Sci. 22, 3, 384-406.]]","journal-title":"J. Comput. Syst. Sci."},{"key":"e_1_2_1_29_1","series-title":"Lecture Notes in Computer Science","first-page":"189","volume-title":"Automatic Verification Methods for Finite State Systems, Proceedings of the International Workshop (Grenoble, Switzerland, June)","author":"JARD C.","unstructured":"JARD , C. , AND JERON , T. 1989. On-line model-checking for finite linear temporal logic specifications . In Automatic Verification Methods for Finite State Systems, Proceedings of the International Workshop (Grenoble, Switzerland, June) . Lecture Notes in Computer Science , vol. 407 . Springer- Verlag , New York , pp. 189 - 196 .]] JARD, C., AND JERON, T. 1989. On-line model-checking for finite linear temporal logic specifications. In Automatic Verification Methods for Finite State Systems, Proceedings of the International Workshop (Grenoble, Switzerland, June). Lecture Notes in Computer Science, vol. 407. Springer- Verlag, New York, pp. 189-196.]]"},{"key":"e_1_2_1_30_1","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1016\/S0022-0000(75)80050-X","article-title":"Space-bounded reducibility among combinatorial problems","volume":"11","author":"JONES N. D.","year":"1975","unstructured":"JONES , N. D. 1975 . Space-bounded reducibility among combinatorial problems . J. Comput. Syst. Sci. 11 , 68 - 75 .]] JONES, N. D. 1975. Space-bounded reducibility among combinatorial problems. J. Comput. Syst. Sci. 11, 68-75.]]","journal-title":"J. Comput. Syst. Sci."},{"key":"e_1_2_1_32_1","first-page":"254","volume-title":"Proceedings of the 18th IEEE Symposium on Foundation of Computer Science. IEEE Computer Science Press, Los Alamitos, Calif.","author":"KOZEN D.","year":"1977","unstructured":"KOZEN , D. 1977 . Lower bounds for natural proof systems . In Proceedings of the 18th IEEE Symposium on Foundation of Computer Science. IEEE Computer Science Press, Los Alamitos, Calif. , pp. 254 - 266 .]] KOZEN, D. 1977. Lower bounds for natural proof systems. In Proceedings of the 18th IEEE Symposium on Foundation of Computer Science. IEEE Computer Science Press, Los Alamitos, Calif., pp. 254-266.]]"},{"key":"e_1_2_1_33_1","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","article-title":"Results on the propositional\/x-calculus","volume":"27","author":"KOZEN D.","year":"1983","unstructured":"KOZEN , D. 1983 . Results on the propositional\/x-calculus . Theoret. Comput. Sci. 27 , 333 - 354 .]] KOZEN, D. 1983. Results on the propositional\/x-calculus. Theoret. Comput. Sci. 27, 333-354.]]","journal-title":"Theoret. Comput. Sci."},{"key":"e_1_2_1_34_1","series-title":"Lecture Notes in Computer Science","first-page":"408","volume-title":"Proceedings of the 6th Conference on Concurrency Theory (Philadelphia, Pa., Aug.)","author":"KUPFERMAN","unstructured":"KUPFERMAN , 0., AND VARDI , M. Y. 1995. On the complexity of branching modular model checking . In Proceedings of the 6th Conference on Concurrency Theory (Philadelphia, Pa., Aug.) . Lecture Notes in Computer Science , vol. 962 . Springer-Verlag , New York , pp. 408 - 422 .]] KUPFERMAN, 0., AND VARDI, M. Y. 1995. On the complexity of branching modular model checking. In Proceedings of the 6th Conference on Concurrency Theory (Philadelphia, Pa., Aug.). Lecture Notes in Computer Science, vol. 962. Springer-Verlag, New York, pp. 408-422.]]"},{"key":"e_1_2_1_35_1","series-title":"Lecture Notes in Computer Science","first-page":"75","volume-title":"Computer Aided Verification, Proceedings of the 8th International Conference","author":"KUPFERMAN","unstructured":"KUPFERMAN , 0., AND VARDI , M. Y. 1996. Module checking . In Computer Aided Verification, Proceedings of the 8th International Conference . Lecture Notes in Computer Science , vol. 1102 . Springer-Verlag , New York , pp. 75 - 86 .]] KUPFERMAN, 0., AND VARDI, M. Y. 1996. Module checking. In Computer Aided Verification, Proceedings of the 8th International Conference. Lecture Notes in Computer Science, vol. 1102. Springer-Verlag, New York, pp. 75-86.]]"},{"key":"e_1_2_1_36_1","series-title":"Lecture Notes in Computer Science","first-page":"36","volume-title":"Computer Aided Verification, Proceedings of the 9th International Conference","author":"KUPFERMAN","unstructured":"KUPFERMAN , 0., AND VARDI , M.Y. 1997. Module checking revisited . In Computer Aided Verification, Proceedings of the 9th International Conference . Lecture Notes in Computer Science , vol. 1254 . Springer-Verlag , New York , pp. 36 - 47 .]] KUPFERMAN, 0., AND VARDI, M.Y. 1997. Module checking revisited. In Computer Aided Verification, Proceedings of the 9th International Conference. Lecture Notes in Computer Science, vol. 1254. Springer-Verlag, New York, pp. 36-47.]]"},{"key":"e_1_2_1_37_1","first-page":"81","volume-title":"Proceedings of the 13th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif.","author":"KUPFERMAN","year":"1998","unstructured":"KUPFERMAN , 0., AND VARDI , M.Y. 1998 a. Freedom, weakness, and determinism: From lineartime to branching-time . In Proceedings of the 13th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif. , pp. 81 - 92 .]] KUPFERMAN, 0., AND VARDI, M.Y. 1998a. Freedom, weakness, and determinism: From lineartime to branching-time. In Proceedings of the 13th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., pp. 81-92.]]"},{"key":"e_1_2_1_38_1","series-title":"Lecture Notes in Computer Science","first-page":"381","volume-title":"Proceedings of the Compositionality Workshop","author":"KUPFERMAN","unstructured":"KUPFERMAN , 0., AND VARDI , M. Y. 1998b. Modular model checking . In Proceedings of the Compositionality Workshop . Lecture Notes in Computer Science , vol. 1536 . Springer-Verlag , New York , pp. 381 - 401 .]] KUPFERMAN, 0., AND VARDI, M. Y. 1998b. Modular model checking. In Proceedings of the Compositionality Workshop. Lecture Notes in Computer Science, vol. 1536. Springer-Verlag, New York, pp. 381-401.]]"},{"key":"e_1_2_1_39_1","first-page":"224","volume-title":"Proceedings of the 30th Annual ACM Symposium on Theory of Computing (Dallas, Tex., May 23-26)","author":"KUPFERMAN","year":"1998","unstructured":"KUPFERMAN , 0., AND VARDI , M. Y. 1998 c. Weak alternating automata and tree automata emptiness . In Proceedings of the 30th Annual ACM Symposium on Theory of Computing (Dallas, Tex., May 23-26) . ACM, New York , pp. 224 - 233 .]] 10.1145\/276698.276748 KUPFERMAN, 0., AND VARDI, M. Y. 1998c. Weak alternating automata and tree automata emptiness. In Proceedings of the 30th Annual ACM Symposium on Theory of Computing (Dallas, Tex., May 23-26). ACM, New York, pp. 224-233.]] 10.1145\/276698.276748"},{"issue":"2","key":"e_1_2_1_40_1","doi-asserted-by":"crossref","first-page":"245","DOI":"10.2307\/421091","article-title":"Church's problem revisited","volume":"5","author":"KUPFERMAN","year":"1999","unstructured":"KUPFERMAN , 0., AND VARDI , M. Y. 1999 a. Church's problem revisited . Bull. Symb. Logic 5 , 2 , 245 - 263 .]] KUPFERMAN, 0., AND VARDI, M. Y. 1999a. Church's problem revisited. Bull. Symb. Logic 5, 2, 245-263.]]","journal-title":"Bull. Symb. Logic"},{"key":"e_1_2_1_41_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the lOth Conference on Concurrency Theory","author":"KUPFERMAN","unstructured":"KUPFERMAN , 0., AND VARDI , M. Y. 1999b. Robust satisfaction . In Proceedings of the lOth Conference on Concurrency Theory . Lecture Notes in Computer Science . Springer-Verlag , New York .]] KUPFERMAN, 0., AND VARDI, M. Y. 1999b. Robust satisfaction. In Proceedings of the lOth Conference on Concurrency Theory. Lecture Notes in Computer Science. Springer-Verlag, New York.]]"},{"key":"e_1_2_1_42_1","unstructured":"KUPFERMAN 0. VARDI M. Y. AND WOLPER P. 1997. Module checking. Inf. Comput. to appear.]] KUPFERMAN 0. VARDI M. Y. AND WOLPER P. 1997. Module checking. Inf. Comput. to appear.]]"},{"key":"e_1_2_1_43_1","first-page":"174","volume-title":"Proceedings of the 7th Annual ACM Symposium on Principles of Programming Languages, ACM","author":"LAMPORT L.","year":"1980","unstructured":"LAMPORT , L. 1980 . Sometimes is sometimes \"not never\"--On the temporal logic of programs . In Proceedings of the 7th Annual ACM Symposium on Principles of Programming Languages, ACM , New York , pp. 174 - 185 .]] 10.1145\/567446.567463 LAMPORT, L. 1980. Sometimes is sometimes \"not never\"--On the temporal logic of programs. In Proceedings of the 7th Annual ACM Symposium on Principles of Programming Languages, ACM, New York, pp. 174-185.]] 10.1145\/567446.567463"},{"key":"e_1_2_1_44_1","series-title":"Lecture Notes in Computer Science","first-page":"30","volume-title":"Proceedings of the 4th Conference on Computer Aided Verification (Montreal, Que., Canada, June)","author":"LARSEN K.G.","unstructured":"LARSEN , K.G. 1992. Efficient local correctness checking . In Proceedings of the 4th Conference on Computer Aided Verification (Montreal, Que., Canada, June) . Lecture Notes in Computer Science , Springer-Verlag , New York , pp. 30 - 43 .]] LARSEN, K.G. 1992. Efficient local correctness checking. In Proceedings of the 4th Conference on Computer Aided Verification (Montreal, Que., Canada, June). Lecture Notes in Computer Science, Springer-Verlag, New York, pp. 30-43.]]"},{"key":"e_1_2_1_45_1","first-page":"97","volume-title":"Proceedings of the 12th Annual ACM Symposium on Principles of Programming Languages (New Orleans, La., Jan.) ACM","author":"LICHTENSTEIN","year":"1985","unstructured":"LICHTENSTEIN , 0., AND PNUELI , A. 1985 . Checking that finite state concurrent programs satisfy their linear specification . In Proceedings of the 12th Annual ACM Symposium on Principles of Programming Languages (New Orleans, La., Jan.) ACM , New York , pp. 97 - 107 .]] 10.1145\/318593.318622 LICHTENSTEIN, 0., AND PNUELI, A. 1985. Checking that finite state concurrent programs satisfy their linear specification. In Proceedings of the 12th Annual ACM Symposium on Principles of Programming Languages (New Orleans, La., Jan.) ACM, New York, pp. 97-107.]] 10.1145\/318593.318622"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/322033.322037"},{"key":"e_1_2_1_47_1","series-title":"Lecture Notes in Computer Science","first-page":"132","volume-title":"Proceedings of the 5th Annual Conference on Computer Aided Verification (Stanford, Calif., June)","author":"MIHAIL M.","unstructured":"MIHAIL , M. , AND PAPADEMITRIOU , C.H. 1994. On the random walk method for protocol testing . In Proceedings of the 5th Annual Conference on Computer Aided Verification (Stanford, Calif., June) . Lecture Notes in Computer Science , vol. 818 . Springer-Verlag , New York , pp. 132 - 141 .]] MIHAIL, M., AND PAPADEMITRIOU, C.H. 1994. On the random walk method for protocol testing. In Proceedings of the 5th Annual Conference on Computer Aided Verification (Stanford, Calif., June). Lecture Notes in Computer Science, vol. 818. Springer-Verlag, New York, pp. 132-141.]]"},{"key":"e_1_2_1_48_1","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1016\/0304-3975(84)90049-5","article-title":"Alternating finite automata on ~0-words","volume":"32","author":"MIYANO S.","year":"1984","unstructured":"MIYANO , S. , AND HAYASHI , T. 1984 . Alternating finite automata on ~0-words . Theoret. Comput. Sci. 32 , 321 - 330 .]] MIYANO, S., AND HAYASHI, T. 1984. Alternating finite automata on ~0-words. Theoret. Comput. Sci. 32, 321-330.]]","journal-title":"Theoret. Comput. Sci."},{"key":"e_1_2_1_49_1","volume-title":"Proceedings of the 13th International Colloquium on Automata, Languages and Programming. Springer-Verlag","author":"MULLER D. E.","year":"1986","unstructured":"MULLER , D. E. , SAOUDI , A. , AND SCHUPP , P.E. 1986 . Alternating automata, the weak monadic theory of the tree and its complexity . In Proceedings of the 13th International Colloquium on Automata, Languages and Programming. Springer-Verlag , New York.]] MULLER, D. E., SAOUDI, A., AND SCHUPP, P.E. 1986. Alternating automata, the weak monadic theory of the tree and its complexity. In Proceedings of the 13th International Colloquium on Automata, Languages and Programming. Springer-Verlag, New York.]]"},{"key":"e_1_2_1_50_1","first-page":"422","volume-title":"Proceedings of the 3rd IEEE Symposium on Logic in Computer Science","author":"MULLER D. E.","year":"1988","unstructured":"MULLER , D. E. , SAOUDI , A. , AND SCHUPP , P.E. 1988 . Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time . In Proceedings of the 3rd IEEE Symposium on Logic in Computer Science ( Edinburgh, Scotland, July). IEEE Computer Society Press, Los Alamitos, Calif. , pp. 422 - 427 .]] MULLER, D. E., SAOUDI, A., AND SCHUPP, P.E. 1988. Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In Proceedings of the 3rd IEEE Symposium on Logic in Computer Science (Edinburgh, Scotland, July). IEEE Computer Society Press, Los Alamitos, Calif., pp. 422-427.]]"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90133-2"},{"key":"e_1_2_1_52_1","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","article-title":"The temporal semantics of concurrent programs","volume":"13","author":"PNUELI A.","year":"1981","unstructured":"PNUELI , A. 1981 . The temporal semantics of concurrent programs . Theoret. Comput. Sci. 13 , 45 - 60 .]] PNUELI, A. 1981. The temporal semantics of concurrent programs. Theoret. Comput. Sci. 13, 45-60.]]","journal-title":"Theoret. Comput. Sci."},{"key":"e_1_2_1_53_1","series-title":"Lecture Notes in Computer Science","first-page":"337","volume-title":"Proceedings of the 5th International Symposium on Programming","author":"QUEILLE J. P.","unstructured":"QUEILLE , J. P. , AND SIFAKIS , J. 1981. Specification and verification of concurrent systems in Cesar . In Proceedings of the 5th International Symposium on Programming . Lecture Notes in Computer Science , vol. 137 . Springer-Verlag , New York , pp. 337 - 351 .]] QUEILLE, J. P., AND SIFAKIS, J. 1981. Specification and verification of concurrent systems in Cesar. In Proceedings of the 5th International Symposium on Programming. Lecture Notes in Computer Science, vol. 137. Springer-Verlag, New York, pp. 337-351.]]"},{"key":"e_1_2_1_54_1","first-page":"1","article-title":"Decidability of second order theories and automata on infinite trees","volume":"141","author":"RABIN M.O.","year":"1969","unstructured":"RABIN , M.O. 1969 . Decidability of second order theories and automata on infinite trees . Trans. AMS 141 , 1 - 35 .]] RABIN, M.O. 1969. Decidability of second order theories and automata on infinite trees. Trans. AMS 141, 1-35.]]","journal-title":"Trans. AMS"},{"key":"e_1_2_1_55_1","first-page":"1","volume-title":"Proceedings of the Symposium on Mathematical Logic and Foundations of Set Theory. North Holland","author":"RABIN M. O.","year":"1970","unstructured":"RABIN , M. O. 1970 . Weakly definable relations and special automata . In Proceedings of the Symposium on Mathematical Logic and Foundations of Set Theory. North Holland , Amsterdam, New York , pp. 1 - 23 .]] RABIN, M. O. 1970. Weakly definable relations and special automata. In Proceedings of the Symposium on Mathematical Logic and Foundations of Set Theory. North Holland, Amsterdam, New York, pp. 1-23.]]"},{"key":"e_1_2_1_56_1","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0022-0000(70)80006-X","article-title":"Relationship between nondeterministic and deterministic tape complexities","volume":"4","author":"SAVITCH W.J.","year":"1970","unstructured":"SAVITCH , W.J. 1970 . Relationship between nondeterministic and deterministic tape complexities . J. Comput. Syst. Sci. 4 , 177 - 192 .]] SAVITCH, W.J. 1970. Relationship between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci. 4, 177-192.]]","journal-title":"J. Comput. Syst. Sci."},{"key":"e_1_2_1_57_1","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1016\/0304-3975(85)90077-5","article-title":"Alternating tree automata","volume":"41","author":"SLUTZKI G.","year":"1985","unstructured":"SLUTZKI , G. 1985 . Alternating tree automata . Theoret. Comput. Sci. 41 , 305 - 318 .]] SLUTZKI, G. 1985. Alternating tree automata. Theoret. Comput. Sci. 41, 305-318.]]","journal-title":"Theoret. Comput. Sci."},{"key":"e_1_2_1_58_1","series-title":"Lecture Notes in Computer Science","first-page":"298","volume-title":"Proceedings of the 13th Symposium on Theoretical Aspects of Computer Science","author":"STIRLING C.","unstructured":"STIRLING , C. 1996. Games and modal mu-calculus . In Proceedings of the 13th Symposium on Theoretical Aspects of Computer Science . Lecture Notes in Computer Science , vol. 1055 . Springer- Verlag , New York , pp. 298 - 312 .]] STIRLING, C. 1996. Games and modal mu-calculus. In Proceedings of the 13th Symposium on Theoretical Aspects of Computer Science. Lecture Notes in Computer Science, vol. 1055. Springer- Verlag, New York, pp. 298-312.]]"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90110-4"},{"key":"e_1_2_1_60_1","series-title":"Lecture Notes in Computer Science","first-page":"465","volume-title":"Proceedings of the llth International Colloquium on Automata, Languages and Programming","author":"STREET R. S.","unstructured":"STREET , R. S. , AND EMERSON , E.A. 1984. An elementary decision procedure for the\/x-calculus . In Proceedings of the llth International Colloquium on Automata, Languages and Programming . Lecture Notes in Computer Science , vol. 172 . Springer-Verlag , New York , pp. 465 - 472 .]] STREET, R. S., AND EMERSON, E.A. 1984. An elementary decision procedure for the\/x-calculus. In Proceedings of the llth International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 172. Springer-Verlag, New York, pp. 465-472.]]"},{"issue":"2","key":"e_1_2_1_61_1","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1137\/0201010","article-title":"Depth first search and linear graph algorithms","volume":"1","author":"TARJAN R. E.","year":"1972","unstructured":"TARJAN , R. E. 1972 . Depth first search and linear graph algorithms . SIAM J. Comput. 1 , 2 , 146 - 160 .]] TARJAN, R. E. 1972. Depth first search and linear graph algorithms. SIAM J. Comput. 1, 2, 146-160.]]","journal-title":"SIAM J. Comput."},{"key":"e_1_2_1_62_1","first-page":"165","article-title":"Automata on infinite objects","author":"THOMAS W.","year":"1990","unstructured":"THOMAS , W. 1990 . Automata on infinite objects . Handb. Theoret. Comput. Sci. , 165 - 191 .]] THOMAS, W. 1990. Automata on infinite objects. Handb. Theoret. Comput. Sci., 165-191.]]","journal-title":"Handb. Theoret. Comput. Sci."},{"key":"e_1_2_1_63_1","first-page":"137","volume-title":"Proceedings of the 14th Annual ACM Symposium on Theory of Computing","author":"VARDI M. Y.","year":"1982","unstructured":"VARDI , M. Y. 1982 . The complexity of relational query languages . In Proceedings of the 14th Annual ACM Symposium on Theory of Computing ( San Francisco, Calif., May 5-7). ACM, New York , pp. 137 - 146 .]] 10.1145\/800070.802186 VARDI, M. Y. 1982. The complexity of relational query languages. In Proceedings of the 14th Annual ACM Symposium on Theory of Computing (San Francisco, Calif., May 5-7). ACM, New York, pp. 137-146.]] 10.1145\/800070.802186"},{"key":"e_1_2_1_64_1","first-page":"101","volume-title":"Proceedings of the 10th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif.","author":"VARDI M. Y.","year":"1995","unstructured":"VARDI , M. Y. 1995 . On the complexity of modular model checking . In Proceedings of the 10th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif. , pp. 101 - 111 .]] VARDI, M. Y. 1995. On the complexity of modular model checking. In Proceedings of the 10th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., pp. 101-111.]]"},{"key":"e_1_2_1_65_1","first-page":"240","volume-title":"Proceedings of the 17th Annual ACM Symposium on Theory of Computing (Providence, R.I., May 6-8). ACM","author":"VARDI M. Y.","year":"1985","unstructured":"VARDI , M. Y. , AND STOCKMEYER , L. 1985 . Improved upper and lower bounds for modal logics of programs . In Proceedings of the 17th Annual ACM Symposium on Theory of Computing (Providence, R.I., May 6-8). ACM , New York , pp. 240 - 251 .]] 10.1145\/22145.22173 VARDI, M. Y., AND STOCKMEYER, L. 1985. Improved upper and lower bounds for modal logics of programs. In Proceedings of the 17th Annual ACM Symposium on Theory of Computing (Providence, R.I., May 6-8). ACM, New York, pp. 240-251.]] 10.1145\/22145.22173"},{"key":"e_1_2_1_66_1","series-title":"Lecture Notes in Computer Science","first-page":"501","volume-title":"Logics of Programs","author":"VARDI M. Y.","unstructured":"VARDI , M. Y. , AND WOLPER , P. 1984. Yet another process logic . In Logics of Programs . Lecture Notes in Computer Science , vol. 164 . Springer-Verlag , New York , pp. 501 - 512 .]] VARDI, M. Y., AND WOLPER, P. 1984. Yet another process logic. In Logics of Programs. Lecture Notes in Computer Science, vol. 164. Springer-Verlag, New York, pp. 501-512.]]"},{"key":"e_1_2_1_67_1","first-page":"322","volume-title":"Proceedings of the 1st Symposium on Logic in Computer Science","author":"VARDI M. Y.","year":"1986","unstructured":"VARDI , M. Y. , AND WOLPER , P. 1986 a. An automata-theoretic approach to automatic program verification . In Proceedings of the 1st Symposium on Logic in Computer Science ( Cambridge, Mass., June). pp. 322 - 331 .]] VARDI, M. Y., AND WOLPER, P. 1986a. An automata-theoretic approach to automatic program verification. In Proceedings of the 1st Symposium on Logic in Computer Science (Cambridge, Mass., June). pp. 322-331.]]"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(86)90026-7"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1092"},{"key":"e_1_2_1_70_1","series-title":"Lecture Notes in Computer Science","first-page":"447","volume-title":"Proceedings of the 4th Conference on Concurrency Theory (Hildesheim, Aug.)","author":"VERGAUWEN B.","unstructured":"VERGAUWEN , B. , AND LEWIS , J. 1993. A linear local model checking algorithm for CTL . In Proceedings of the 4th Conference on Concurrency Theory (Hildesheim, Aug.) . Lecture Notes in Computer Science , vol. 715 . Springer-Verlag , New York , pp. 447 - 461 .]] VERGAUWEN, B., AND LEWIS, J. 1993. A linear local model checking algorithm for CTL. In Proceedings of the 4th Conference on Concurrency Theory (Hildesheim, Aug.). Lecture Notes in Computer Science, vol. 715. Springer-Verlag, New York, pp. 447-461.]]"},{"key":"e_1_2_1_71_1","volume-title":"dissertation","author":"VISSER W.","unstructured":"VISSER , W. 1998. Efficient CTL * model checking using games and automata. Ph. D. dissertation . Manchester University .]] VISSER, W. 1998. Efficient CTL* model checking using games and automata. Ph.D. dissertation. Manchester University.]]"},{"key":"e_1_2_1_72_1","series-title":"Lecture Notes in Computer Science","volume-title":"Software Tools for Technology Transfer","author":"VISSER W.","unstructured":"VISSER , W. , AND BARRINGER , H. 1999. CTL * model checking for SPIN . In Software Tools for Technology Transfer . Lecture Notes in Computer Science , Springer-Verlag , New York .]] VISSER, W., AND BARRINGER, H. 1999. CTL* model checking for SPIN. In Software Tools for Technology Transfer. Lecture Notes in Computer Science, Springer-Verlag, New York.]]"},{"key":"e_1_2_1_73_1","volume-title":"Proceedings of the l lth Annual Symposium on Logic in Computer Science.","author":"WILLEMS B.","year":"1996","unstructured":"WILLEMS , B. , AND WOLPER , P. 1996 . Partial-order methods for model checking: From linear time to branching time . In Proceedings of the l lth Annual Symposium on Logic in Computer Science. ( New Brunswick, N.J., July).]] WILLEMS, B., AND WOLPER, P. 1996. Partial-order methods for model checking: From linear time to branching time. In Proceedings of the l lth Annual Symposium on Logic in Computer Science. (New Brunswick, N.J., July).]]"},{"key":"e_1_2_1_74_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0019-9958(83)80051-5","article-title":"Temporal logic can be more expressive","volume":"56","author":"WOLPER P.","year":"1983","unstructured":"WOLPER , P. 1983 . Temporal logic can be more expressive . Inf. Control , 56 , 1 - 2 , 72-99.]] WOLPER, P. 1983. Temporal logic can be more expressive. Inf. Control, 56, 1-2, 72-99.]]","journal-title":"Inf. Control"},{"key":"e_1_2_1_75_1","first-page":"75","volume-title":"Proceedings of the Temporal Logic in Specification, B. Banieqbal, H. Barringer, and A. Pnueli, Eds. Lecture Notes in Computer Science, Springer-Verlag","author":"WOLPER P.","year":"1989","unstructured":"WOLPER , P. 1989 . On the relation of programs and computations to models of temporal logic . In Proceedings of the Temporal Logic in Specification, B. Banieqbal, H. Barringer, and A. Pnueli, Eds. Lecture Notes in Computer Science, Springer-Verlag , New York , pp. 75 - 123 .]] WOLPER, P. 1989. On the relation of programs and computations to models of temporal logic. In Proceedings of the Temporal Logic in Specification, B. Banieqbal, H. Barringer, and A. Pnueli, Eds. Lecture Notes in Computer Science, Springer-Verlag, New York, pp. 75-123.]]"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/333979.333987","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T12:56:19Z","timestamp":1672577779000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/333979.333987"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,3]]},"references-count":74,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2000,3]]}},"alternative-id":["10.1145\/333979.333987"],"URL":"http:\/\/dx.doi.org\/10.1145\/333979.333987","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":["Artificial Intelligence","Hardware and Architecture","Information Systems","Control and Systems Engineering","Software"],"published":{"date-parts":[[2000,3]]},"assertion":[{"value":"2000-03-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}