{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,29]],"date-time":"2024-06-29T13:24:48Z","timestamp":1719667488692},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2006,8,31]],"date-time":"2006-08-31T00:00:00Z","timestamp":1156982400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[2007,2,23]]},"DOI":"10.1007\/s10703-006-0022-1","type":"journal-article","created":{"date-parts":[[2006,8,30]],"date-time":"2006-08-30T13:25:55Z","timestamp":1156944355000},"page":"143-176","source":"Crossref","is-referenced-by-count":5,"title":["Verification of bounded Petri nets using integer programming"],"prefix":"10.1007","volume":"30","author":[{"given":"Victor","family":"Khomenko","sequence":"first","affiliation":[]},{"given":"Maciej","family":"Koutny","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,8,31]]},"reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"Ajili F, Contejean E (1997) Avoiding slack variables in the solving of linear diophantine equations and inequations. Theor Comput Sci 173:183\u2013208","DOI":"10.1016\/S0304-3975(96)00195-8"},{"key":"22_CR2","unstructured":"Best E, Grahlmann B (1996) PEP \u2014More than a Petri net tool. In: Proc TACAS'96, Lecture Notes in Computer Science, Springer-Verlag, Vol. 1055, pp 397\u2013401"},{"key":"22_CR3","unstructured":"Clarke EM, Grumberg O, Peled D (1999) Model checking. MIT Press"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Contejean E, Devie H (1994) An efficient incremental algorithm for solving systems of linear diophantine equations. Inf Comput 113:143\u2013172","DOI":"10.1006\/inco.1994.1067"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"Corbett JC (1996) Evaluating deadlock detection methods for concurrent software. IEEE Trans Soft Eng SE-22(3):161\u2013180","DOI":"10.1109\/32.489078"},{"key":"22_CR6","unstructured":"CPLEX Corporation (1995) CPLEX 3.0 Manual"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"Engelfriet J (1991) Branching processes of Petri nets. Acta Inform 28:575\u2013591","DOI":"10.1007\/BF01463946"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Esparza J, R\u00f6mer S, Vogler W (2002) An improvement of McMillan's unfolding algorithm. Form Method Syst Des 20(3):285\u2013310","DOI":"10.1023\/A:1014746130920"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Esparza J (1994) Model checking based on branching processes. Sci Comput Program 23:151\u2013195","DOI":"10.1016\/0167-6423(94)00019-0"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Heljanko K (1999) Using logic programs with stable model semantics to solve deadlock and reachability problems for 1-safe Petri nets. IOS Press, Fundamenta Inform 37(3):247\u2013268","DOI":"10.1007\/3-540-49059-0_17"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Khomenko V (2003) Model checking based on prefixes of Petri net unfoldings. PhD Thesis, School of Computing Science, University of Newcastle","DOI":"10.1007\/3-540-45657-0_49"},{"key":"22_CR12","unstructured":"Khomenko V, Koutny M (2000) Deadlock checking using liner programming and partial order dependencies. Technical Report CS-TR-695, School of Computing Science, University of Newcastle"},{"key":"22_CR13","unstructured":"Khomenko V, Koutny M (2000) Verification of bounded Petri Nets using integer programming. Technical Report CS-TR-711, School of Computing Science, University of Newcastle"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Koutny M, Best E (1999) Fundamental study: operational and denotational semantics for the box algebra. Theor Comput Sci 211:1\u201383","DOI":"10.1016\/S0304-3975(97)00180-1"},{"key":"22_CR15","unstructured":"Krivoi S (1999) About some methods of solving and feasibility criteria of linear diophantine equations over the natural numbers domain (in Russian). Cybern Syst Anal 4:12\u201336"},{"key":"22_CR16","unstructured":"McMillan KL (1992) Using unfoldings to avoid state explosion problem in the verification of asynchronous circuits. In: Proc CAV'92, Lecture Notes in Computer Science, Springer-Verlag, Vol 663, pp 164\u2013174"},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"McMillan KL (1992) Symbolic model checking: an approach to the state explosion problem. PhD Thesis, School of Computer Science, Carnegie Mellon University","DOI":"10.1007\/978-1-4615-3190-6_3"},{"key":"22_CR18","unstructured":"Melzer S (1998) Verifikation verteilter systeme mit linearer\u2014und constraint-programmierung. PhD Thesis. Technische Universit\u00e4t M\u00fcnchen"},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"Melzer S, R\u00f6mer S (1997) Deadlock checking using net unfoldings. In: Proc CAV'97, Lecture Notes in Computer Science, Springer-Verlag, vol 1254, pp 352\u2013363","DOI":"10.1007\/3-540-63166-6_35"},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"Murata T (1989) Petri nets: properties, analysis and applications. In: Proc IEEE vol. 77 no. 4, pp. 541\u2013580","DOI":"10.1109\/5.24143"},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"Niemel\u00e4 I, Simons P (1997) smodels \u2014An implementation of the stable model and well-founded semantics for normal logic programs. In: Proc LPNMR'97, Lecture Notes in Artificial Intelligence, Springer-Verlag, vol 1265, pp 420\u2013429","DOI":"10.1007\/3-540-63255-7_32"},{"key":"22_CR22","doi-asserted-by":"crossref","unstructured":"Silva M, Teruel E, Colom J-M (1998) Linear algebraic and linear programming techniques for the analysis of place\/transition net systems. In: Reisig W, Rozenberg G (eds) Lectures on Petri nets I: basic models. Springer-Verlag, pp 309\u2013373","DOI":"10.1007\/3-540-65306-6_19"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"Simons P (1999) Extending the stable model semantics with more expressive rules. In: Proc LPNMR'99, Lecture Notes in artificial intelligence, Springer-Verlag vol 1730.","DOI":"10.1007\/3-540-46767-X_22"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-0022-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-006-0022-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-0022-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T18:01:02Z","timestamp":1559239262000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-006-0022-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,8,31]]},"references-count":23,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2007,2,23]]}},"alternative-id":["22"],"URL":"https:\/\/doi.org\/10.1007\/s10703-006-0022-1","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,8,31]]}}}