{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:05:33Z","timestamp":1725483933385},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540678397"},{"type":"electronic","value":"9783540449140"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44914-0_12","type":"book-chapter","created":{"date-parts":[[2007,5,22]],"date-time":"2007-05-22T21:26:14Z","timestamp":1179869174000},"page":"202-218","source":"Crossref","is-referenced-by-count":1,"title":["Reformulation and Approximation in Model Checking"],"prefix":"10.1007","author":[{"given":"Peter Z.","family":"Revesz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2000,8,11]]},"reference":[{"key":"12_CR1","unstructured":"S. Abiteboul, R. Hull, and V. Vianu. Foundations of Databases. Addison-Wesley, 1995."},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"B. Boigelot and P. Wolper. Symbolic verification with periodic sets. In Proc. Conf. on Computer-Aided Verification, pages 55\u201367, 1994.","DOI":"10.1007\/3-540-58179-0_43"},{"key":"12_CR3","series-title":"Lect Notes Comput Sci","first-page":"68","volume-title":"Proc. Workshop on Constraint Databases and Applications","author":"J.-H. Byon","year":"1995","unstructured":"J.-H. Byon and P.Z. Revesz. DISCO: A constraint database system with sets. In Proc. Workshop on Constraint Databases and Applications, number 1034 in LNCS, pages 68\u201383. Springer-Verlag, September 1995."},{"key":"12_CR4","unstructured":"A. Cimatti, F. Giunchiglia, and M. Roveri. Abstraction in planning via model checking. In Proc. Symposium on Abstraction, Reformulation and Approximation, pages 37\u201341, 1998."},{"key":"12_CR5","series-title":"Lect Notes Comput Sci","volume-title":"Proc. Industrial Benefit and Advances in Formal Methods","author":"J.J. Comuzzi","year":"1996","unstructured":"J.J. Comuzzi and J.M. Hart. Program slicing using weakest precondition. In Proc. Industrial Benefit and Advances in Formal Methods, number 1051 in LNCS. Springer-Verlag, 1996."},{"key":"12_CR6","series-title":"Lect Notes Comput Sci","volume-title":"Second International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Delzanno","year":"1999","unstructured":"G. Delzanno and A. Podelski. Model checking in clp. In Second International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer LNCS, 1999."},{"key":"12_CR7","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1023\/A:1009747629591","volume":"3","author":"L. Fribourg","year":"1997","unstructured":"L. Fribourg and H. Ols\u00e9n. A decompositional approach for computing least fixed-points of datalog programs with z-counters. Constraints, 3\u20134:305\u2013336, 1997.","journal-title":"Constraints"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"L. Fribourg and J.D.C. Richardson. Symbolic verification with gap-order constraints. In Prof. LOPSTR, 1996.","DOI":"10.1007\/3-540-62718-9_2"},{"key":"12_CR9","series-title":"Lect Notes Comput Sci","volume-title":"Proc. Computer Aided Verification","author":"S. Graf","year":"1996","unstructured":"S. Graf and H. Saidi. Constructing abstract graphs using pvs. In Proc. Computer Aided Verification, number 1102 in LNCS. Springer-Verlag, 1996."},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"N. Halbwachs. Delay analysis in synchronous programs. In Proc. Conf. on Computer-Aided Verification, pages 333\u2013346, 1993.","DOI":"10.1007\/3-540-56922-7_28"},{"key":"12_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"460","DOI":"10.1007\/3-540-63166-6_48","volume-title":"Proc. Computer Aided Verification","author":"T.A. Henzinger","year":"1997","unstructured":"T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. Hytech: A model checker for hybrid systems. In Proc. Computer Aided Verification, number 1254 in LNCS, pages 460\u2013463. Springer-Verlag, 1997."},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"J. Jaffar and J.-L. Lassez. Constraint logic programming. In Proc. 14th ACM POPL, pages 111\u2013119, 1987.","DOI":"10.1145\/41625.41635"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"P.C. Kanellakis, G.M. Kuper, and P.Z. Revesz. Constraint query languages. In Proc. of the 9th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, pages 299\u2013313, New York, 1990. ACM Press.","DOI":"10.1145\/298514.298582"},{"key":"12_CR14","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1006\/jcss.1995.1051","volume":"51","author":"P.C. Kanellakis","year":"1995","unstructured":"P.C. Kanellakis, G.M. Kuper, and P.Z. Revesz. Constraint query languages. Journal of Computer and System Sciences, 51:26\u201352, 1995.","journal-title":"Journal of Computer and System Sciences"},{"key":"12_CR15","unstructured":"A. Kerbrat. Reachable state space analysis of lotos specifications. In Proc. 7th International Conference on Formal Description Techniques, pages 161\u2013176, 1994."},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"R. Kosaraju. Decidability of reachability in vector addition systems. In Proc. of the 14th Annual ACM Symposium on Theory of Computing, pages 267\u2013280, 1982.","DOI":"10.1145\/800070.802201"},{"key":"12_CR17","unstructured":"M. Lowry and M. Subramaniam. Abstraction for analytic verification of concurrent software systems. In Proc. Symposium on Abstraction, Reformulation and Approximation, pages 85\u201394, 1998."},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"E. Mayr. An algorithm for the general petri net reachability problem. In Proc. of the 13th Annual ACM Symposium on Theory of Computing, pages 238\u2013246, 1981.","DOI":"10.1145\/800076.802477"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"K. McMillan. Symbolic Model Checking. Kluwer, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"issue":"3","key":"12_CR20","doi-asserted-by":"publisher","first-page":"437","DOI":"10.2307\/1970290","volume":"74","author":"M.L. Minsky","year":"1961","unstructured":"M.L. Minsky. Recursive unsolvability of post\u2019s problem of \u2018tag\u2019 and other topics in the theory of turing machines. Annals of Mathematics, 74(3):437\u2013455, 1961.","journal-title":"Annals of Mathematics"},{"key":"12_CR21","unstructured":"M. L. Minsky. Computation: Finite and Infinite Machines. Prentice Hall, 1967."},{"key":"12_CR22","unstructured":"J. Peterson. Petri Net Theory and Modeling of Systems. Prentice-Hall,Inc., 1981."},{"key":"12_CR23","unstructured":"R. Ramakrishnan. Database Management Systems. McGraw-Hill, 1998."},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"W. Reisig. Petri Nets: an Introduction. Springer, 1985.","DOI":"10.1007\/978-3-642-69968-9"},{"key":"12_CR25","series-title":"Lect Notes Comput Sci","volume-title":"Proc. Fourth International Conference on Principles and Practice of Constraint Programming","author":"P.Z. Revesz","year":"1998","unstructured":"P.Z. Revesz. Safe datalog queries with linear constraints. In M. Maher and J.-F. Puget, editors, Proc. Fourth International Conference on Principles and Practice of Constraint Programming, number 1520 in LNCS. Springer-Verlag, 1998."},{"key":"12_CR26","unstructured":"P.Z. Revesz. Datalog programs with difference constraints. In Proc. Twelfth International Conference on Applications of Prolog, pages 69\u201376, September 1999."},{"key":"12_CR27","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/0304-3975(93)90222-F","volume":"116","author":"P.Z. Revesz","year":"1993","unstructured":"P.Z. Revesz. A closed-form evaluation for Datalog queries with integer (gap)-order constraints. Theoretical Computer Science, 116:117\u2013149, 1993.","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Abstraction, Reformulation, and Approximation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44914-0_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T07:01:26Z","timestamp":1556434886000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44914-0_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540678397","9783540449140"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-44914-0_12","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}