{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T22:34:27Z","timestamp":1784241267656,"version":"3.55.0"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2000,3,1]],"date-time":"2000-03-01T00:00:00Z","timestamp":951868800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2000,3,1]],"date-time":"2000-03-01T00:00:00Z","timestamp":951868800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2000,3]]},"DOI":"10.1023\/a:1008743212620","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T11:37:32Z","timestamp":1040557052000},"page":"159-189","source":"Crossref","is-referenced-by-count":40,"title":["Verification of Safety Properties Using Integer Programming: Beyond the State Equation"],"prefix":"10.1007","volume":"16","author":[{"given":"Javier","family":"Esparza","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stephan","family":"Melzer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"1","key":"254638_CR1","first-page":"103","volume":"4","author":"H. Alaiwan","year":"1985","unstructured":"H. Alaiwan and J.F. Toudic, \u201cRecherche des Semi-flots, des Verrous et des Trappes dans les R\u00e9seaux de Petri,\u201d Technique et Science Informatique, Vol. 4, No. 1, pp. 103\u2013112, 1985.","journal-title":"Technique et Science Informatique"},{"key":"254638_CR2","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(94)90266-6","volume":"126","author":"H.R. Andersen","year":"1994","unstructured":"H.R. Andersen, \u201cModel checking and boolean graphs,\u201d Theoretical Computer Science, Vol. 126, pp. 3\u201330, 1994.","journal-title":"Theoretical Computer Science"},{"issue":"11","key":"254638_CR3","doi-asserted-by":"crossref","first-page":"1204","DOI":"10.1109\/32.106975","volume":"17","author":"G.S. Avrunin","year":"1991","unstructured":"G.S. Avrunin, U.A. Buy, J.C. Corbett, L.K. Dillon, and J.C. Wileden, \u201cAutomated analysis of concurrent systems with the constrained expression toolset,\u201d IEEE Transactions in Software Engineering, Vol. 17, No. 11, pp. 1204\u20131222, 1991.","journal-title":"IEEE Transactions in Software Engineering"},{"key":"254638_CR4","doi-asserted-by":"crossref","unstructured":"G.S. Avrunin, J.C. Corbett, and U.A. Buy, \u201cInteger programming in the analysis of concurrent systems,\u201d in K.G. Larsen and A. Skou (Eds.), CAV '91, Lecture Notes in Computer Science, Vol. 575, pp. 92\u2013102, 1991.","DOI":"10.1007\/3-540-55179-4_10"},{"key":"254638_CR5","series-title":"Technical Report","volume-title":"Modelling mixed-integer optimisation problems in constraint logic programming","author":"P. Barth","year":"1995","unstructured":"P. Barth and A. Bockmayr, \u201cModelling mixed-integer optimisation problems in constraint logic programming,\u201d Technical Report MPI-I-95-2-011, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, 1995."},{"key":"254638_CR6","volume-title":"PEP: Programming Environment based on Petri Nets","year":"1995","unstructured":"E. Best and H. Fleischhack (Eds.), PEP: Programming Environment based on Petri Nets, Hildesheimer Informatikbericht 14\/95, University of Hildesheim, Germany, 1995."},{"key":"254638_CR7","doi-asserted-by":"crossref","unstructured":"E. Best and R.P. Hopkins, B(PN)2\u2013A Basic Petri Net Programming Notation, in Proceedings of PARLE '93, Springer-Verlag, 1993. Lecture Notes in Computer Science, Vol. 694, pp. 379\u2013390. Also: Hildesheimer Informatikbericht 27\/92, University of Hildesheim, Germany, 1992.","DOI":"10.1007\/3-540-56891-3_30"},{"key":"254638_CR8","unstructured":"G.V. Brams, R\u00e9seaux de Petri: Theorie et Practique, Vols.I and II, Masson, 1982."},{"key":"254638_CR9","unstructured":"CCITT Recommendations Q.1200, \u201cIntelligent networks,\u201d final version, Technical report, 1992."},{"key":"254638_CR10","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/0304-3975(94)00231-7","volume":"147","author":"A. Cheng","year":"1995","unstructured":"A. Cheng, J. Esparza, and J. Palsberg, \u201ccomplexity results for 1-safe Petri nets,\u201d Theoretical Computer Science, Vol. 147, pp. 117\u2013136, 1995.","journal-title":"Theoretical Computer Science"},{"key":"254638_CR11","doi-asserted-by":"crossref","unstructured":"J.C. Corbett, \u201cEvaluating deadlock detection methods for concurrent software,\u201d in T. Ostrand, (Ed.), Proceedings of the 1994 International Symposium on Software Testing and Analysis, New York, 1994, pp. 204\u2013215.","DOI":"10.1145\/186258.187206"},{"issue":"1","key":"254638_CR12","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/BF01384316","volume":"61","author":"J.C. Corbett","year":"1995","unstructured":"J.C. Corbett and G.S. Avrunin, \u201cUsing integer programming to verify general safety and liveness properties,\u201d Formal Methods in System Design, Vol. 61, No. 1, pp. 97\u2013123, 1995.","journal-title":"Formal Methods in System Design"},{"key":"254638_CR13","unstructured":"J. Cortadella, M. Kishinevsky, A. Kondratyev, L. Lavagno, and A. Yakovlev, \u201cPetrify: a tool for manipulating concurrent specifications and synthesis of asynchronous controllers,\u201d IEICE Transactions on Information and Systems, E80-D(3), pp. 315\u2013325, 1997. Technical report version available at http:\/\/www.lsi.upc.es\/ jordic\/ petrify\/refs\/."},{"key":"254638_CR14","doi-asserted-by":"crossref","unstructured":"P. Cousot and N. Halbwachs, \u201cAutomatic discovery of linear restraints among variables of a program,\u201d in 5th ACM Symposium on Principles of Programming Languages, ACM-Press, 1978.","DOI":"10.1145\/512760.512770"},{"key":"254638_CR15","unstructured":"CPLEX Optimization Inc, Using the CPLEXTM Callable Library and CPLEXTM Mixed Integer Library."},{"key":"254638_CR16","doi-asserted-by":"crossref","unstructured":"J. Desel, Petrinetze, lineare Algebra und lineare Programmierung, Teubner-Texte zur Informatik 26, 1998.","DOI":"10.1007\/978-3-322-95382-7"},{"key":"254638_CR17","doi-asserted-by":"crossref","unstructured":"J. Desel and J. Esparza, Free-choice Petri Nets, volume 40 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1995.","DOI":"10.1017\/CBO9780511526558"},{"key":"254638_CR18","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","volume":"1","author":"W.F. Dowling","year":"1984","unstructured":"W.F. Dowling and J.H. Gallier, \u201clinear-time algorithms for testing the satisfiability of propositional horn formulae,\u201d journal of Logic Programming, Vol. 1, pp. 267\u2013284, 1984.","journal-title":"journal of Logic Programming"},{"key":"254638_CR19","doi-asserted-by":"crossref","unstructured":"J. Ezpeleta, J.M. Couvreur, and M. Silva, \u201cA new technique for finding a generating family of siphons, traps and ST-components. Application to colored Petri nets,\u201d in G. Rozenberg (Ed.), Advances in Petri Nets, Springer Verlag, 1993. Lecture Notes in Computer Science, Vol. 674, pp. 126\u2013147.","DOI":"10.1007\/3-540-56689-9_42"},{"key":"254638_CR20","unstructured":"M.R. Garey and D.S. Johnson, Computers and Intractability. Freeman and Company, 1979."},{"key":"254638_CR21","unstructured":"B. Grahlmann, \u201cVerifying telecommunication protocols with PEP,\u201d in Proceedings of RELECTRONIC '95, 9th Symposium on Quality and Reliability in Electronics, Scientific Society for Telecommunications, pp. 251\u2013256, 1995."},{"key":"254638_CR22","doi-asserted-by":"crossref","first-page":"1195","DOI":"10.1287\/opre.32.6.1195","volume":"32","author":"M. Gr\u00f6tschel","year":"1984","unstructured":"M. Gr\u00f6tschel, M. J\u00fcnger, and G. Reinelt, \u201cA cutting plane algorithm for the linear ordering problem,\u201d Operations Research, Vol. 32, pp. 1195\u20131220, 1984.","journal-title":"Operations Research"},{"key":"254638_CR23","doi-asserted-by":"crossref","unstructured":"N. Halbwachs, \u201cAbout synchronous programming and abstract interpretation,\u201d in B. Le Charlier (Ed.), SAS '94: Static Analysis Symposium, Springer-Verlag, 1994. Lecture Notes in Computer Science, Vol. 864, pp. 179\u2013192.","DOI":"10.1007\/3-540-58485-4_40"},{"key":"254638_CR24","unstructured":"M. Heiner and P. Deussen, \u201cPetri net based qualitative analysis\u2013a case study,\u201d Technical Report BTU Cottbus, I-08\/1995, 1996. A short version appeared in: Petri Net Based Design and Analysis of Reactive Systems, in the Proc. of WODES'96, Workshop on Discrete Event Systems, Edinburgh, 1996."},{"key":"254638_CR25","unstructured":"C. Holzbaur, \u201cA specialized, incremental solved form algorithm for systems of linear inequalities,\u201d Technical Report Austrian Research Institute for Artificial Intelligence, Vienna, TR-94-07, 1994."},{"key":"254638_CR26","unstructured":"L. Jenner, \u201cEin Prozedurkonzept f\u00fcr die parallele Hochsprache B(PN)2,\u201d Master Thesis. University of Hildesheim, 1994."},{"key":"254638_CR27","doi-asserted-by":"crossref","unstructured":"S. Kleuker, \u201cA gentle introduction to specification engineering using a case study in telecommunications,\u201d in P.D. Mosses, M. Nielsen, and M.I. Schwartzbach (Eds.), TAPSOFT '95, Springer-Verlag, 1995. Lecture Notes in Computer Science, Vol. 915, pp.636\u2013650.","DOI":"10.1007\/3-540-59293-8_225"},{"key":"254638_CR28","doi-asserted-by":"crossref","unstructured":"K. Lautenbach, \u201cLinear algebraic calculation of deadlocks and traps,\u201d in H.J. Genrich, K. Voss, and G. Rozenberg (Eds.) Concurrency and Nets. Springer-Verlag, pp. 315\u2013336, 1987.","DOI":"10.1007\/978-3-642-72822-8_21"},{"key":"254638_CR29","doi-asserted-by":"crossref","unstructured":"C. Lewerentz and T. Lindner, \u201cFormal development of reactive systems\u2013case study production cell,\u201d Springer-Verlag, 1995. Lecture Notes in Computer Science, Vol. 254.","DOI":"10.1007\/3-540-58867-1"},{"key":"254638_CR30","doi-asserted-by":"crossref","unstructured":"S. Melzer and J. Esparza, \u201cChecking system properties via integer programming,\u201d in H.R. Nielson (Ed.), Springer-Verlag, 1996. Lecture Notes in Computer Science, Vol. 1058, pp. 250\u2013264.","DOI":"10.1007\/3-540-61055-3_41"},{"key":"254638_CR31","doi-asserted-by":"crossref","unstructured":"S. Melzer and S. R\u00f6mer, Deadlock Checking using Net Unfoldings. in O. Grumberg (Ed.), CAV '97, Springer-Verlag, 1997. Lecture Notes in Computer Science, Vol. 1254, pp. 352\u2013363.","DOI":"10.1007\/3-540-63166-6_35"},{"key":"254638_CR32","doi-asserted-by":"crossref","unstructured":"G. Memmi and G. Roucairol, Linear Algebra in Net Theory. in W. Brauer (Ed.), Net Theory and Applications, Springer-Verlag, 1980. Lecture Notes in Computer Science, Vol. 84, pp. 213\u2013223.","DOI":"10.1007\/3-540-10001-6_24"},{"key":"254638_CR33","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0020-0190(88)90124-X","volume":"29","author":"M. Minoux","year":"1988","unstructured":"M. Minoux, \u201cLTUR: a simplified linear-time unit resolution algorithm for Horn formulae and computer implementation,\u201d Information Processing Letters, Vol. 29, pp. 1\u201312, 1988.","journal-title":"Information Processing Letters"},{"key":"254638_CR34","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1016\/0166-218X(90)90144-2","volume":"29","author":"M. Minoux","year":"1990","unstructured":"M. Minoux and K. Barkaoui, \u201cDeadlocks and traps in Petri nets as horn-satisfiability solutions and some related polynomially solvable problems,\u201d Discrete Applied Mathematics, Vol. 29, pp. 195\u2013210, 1990.","journal-title":"Discrete Applied Mathematics"},{"issue":"4","key":"254638_CR35","doi-asserted-by":"crossref","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T. Murata","year":"1989","unstructured":"T. Murata, \u201cPetri nets: properties, analysis and applications,\u201d Proceedings of the IEEE, Vol. 77, No. 4, pp. 541\u2013580, 1989.","journal-title":"Proceedings of the IEEE"},{"key":"254638_CR36","doi-asserted-by":"crossref","unstructured":"E. Pastor, O. Roig, J. Cortadella, and R.M. Badia, \u201cPetri net analysis using boolean manipulation,\u201d in Robert Valette (Ed.), Application and Theory of Petri Nets 1994, Springer-Verlag, 1994. Lecture Notes in Computer Science, Vol. 815, pp. 16\u2013435.","DOI":"10.1007\/3-540-58152-9_23"},{"key":"254638_CR37","unstructured":"M. Raynal, Algorithms for Mutual Exclusion, North Oxford Academic, 1986."},{"key":"254638_CR38","unstructured":"W. Reisig, Petri Nets, volume 4 of EATCS Monographs on Theoretical Computer Science, Springer Verlag, 1985."},{"key":"254638_CR39","unstructured":"A. Schrijver, Theory of Linear and Integer Programming, Series in Discrete Mathematics, Wiley, 1986."},{"key":"254638_CR40","doi-asserted-by":"crossref","unstructured":"P. Starke, Analyse von Petri-Netz-Modellen, Teubner, 1990.","DOI":"10.1007\/978-3-663-09262-9"},{"key":"254638_CR41","unstructured":"S. Thienel, \u201cABACUS\u2013A Branch And CUt System,\u201d PhD thesis, University of Cologne, 1995."},{"key":"254638_CR42","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/BF00709154","volume":"1","author":"A. Valmari","year":"1992","unstructured":"A. Valmari, \u201cA stubborn attack on state explosion,\u201d Formal Methods in System Design, Vol. 1, pp. 297\u2013322, 1992.","journal-title":"Formal Methods in System Design"},{"key":"254638_CR43","unstructured":"K. Varpaaniemi, J. Halme, K. Hiekkanen, and T. Pyssysalo, \u201cPROD reference manual,\u201d Technical Report 13, B Series, Department of Computer Science, Helsinki University of Technology, 1995."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008743212620.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008743212620\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008743212620.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T04:15:00Z","timestamp":1754367300000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008743212620"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,3]]},"references-count":43,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2000,3]]}},"alternative-id":["254638"],"URL":"https:\/\/doi.org\/10.1023\/a:1008743212620","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2000,3]]}}}