{"entities":{"Q3097968":{"pageid":3108683,"ns":120,"title":"Item:Q3097968","lastrevid":86201510,"modified":"2026-06-03T16:28:00Z","type":"item","id":"Q3097968","labels":{"en":{"language":"en","value":"BDD-based bounded model checking for temporal properties of 1-safe Petri nets"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5970248"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3097968$974FA670-5ABB-4C18-AC64-D559B1C8070C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d8f203b3e7e1717b0673efc4d2dd980965b123d7","datavalue":{"value":{"text":"BDD-based Bounded Model Checking for Temporal Properties of 1-Safe Petri Nets","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3097968$149CA454-95B0-42A7-BDB6-2943A8E619E6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"778921017f70780ffc6c37ddbb8b25c8c0ae2343","datavalue":{"value":"1238.68086","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3097968$21FD96B6-A424-415E-98FB-EFB9BE404F7B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"852ebe388e8c119a347349dbfddffb075a9869b6","datavalue":{"value":"10.3233/FI-2011-513","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3097968$63DAAD3A-41F9-40FB-BBDC-EDABCB2797EA","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"cb073cee3f17fc5d531df433f94b283501d8f60f","datavalue":{"value":{"entity-type":"item","numeric-id":1749192,"id":"Q1749192"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3097968$42E26D2C-DA42-46A1-98B2-FAE0B4235D35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"00e4afc18902a1591d00a05876e3070d819defde","datavalue":{"value":{"entity-type":"item","numeric-id":1028968,"id":"Q1028968"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3097968$27F4F440-9E20-4518-A8D5-78AAC6C2E547","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e8e8e51edb23208f92526e006503dcdd3fefdffb","datavalue":{"value":{"entity-type":"item","numeric-id":2493433,"id":"Q2493433"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3097968$56809198-6572-4624-BB42-84642CD9E6EF","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"1529db038bde6a8aed76ac5e8432917aee1a9200","datavalue":{"value":{"entity-type":"item","numeric-id":2803574,"id":"Q2803574"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3097968$3F01A5B9-A99C-417E-9534-ABF2E01339D0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"eaa681f595e5adaa3f79c590c5e5c1e3273415a6","datavalue":{"value":{"time":"+2011-11-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3097968$B338D4B1-4E56-4E43-8B3F-F46F38D400A8","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3097968$DA6034AC-1F4C-40BD-9EC3-853EEC15366B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8f412c62952107f7ff74e77578c2ab25d3e121a","datavalue":{"value":"68Q85","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3097968$D1F935B8-1930-42B8-99DD-0CA9D14B8EC7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"23e7cdaf2e82f5cc864274e843d1c5be36653b9f","datavalue":{"value":"68Q01","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3097968$0FB457B0-030C-45A6-AECB-F5A7381917BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e2244b32b83bf71a9c045223e635ab074452b389","datavalue":{"value":"03B44","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3097968$5CBB2FCD-AE72-48A0-8013-AE8D731CD48D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"35c3f01235ccba091e1644bb05c86f53d45fd7f7","datavalue":{"value":"68N19","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3097968$177EF31F-2C82-4594-B97A-6D8B43F323D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"62ff42057022552eaa82447a5a1563ef3bf93acd","datavalue":{"value":"68M14","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3097968$EEF0CA9B-4774-431B-BA09-16B468D90E27","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5cc0a275f0d1be55efb426d06cb89906805a3687","datavalue":{"value":"5970248","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3097968$D2CC303B-ECD1-4BDA-AE99-A5DB0B1DD8E9","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb9f8004d477a3922fe8bde53d670f8b57c48852","datavalue":{"value":"model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q3097968$7F170810-6E9A-4C2F-8866-A6528FAA30E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"01a2e30b6f10c98d548518426a25a350ad19ecc5","datavalue":{"value":"Petri nets","type":"string"},"datatype":"string"},"type":"statement","id":"Q3097968$813C12D7-36BD-4011-894C-1F944D4973F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a4a6f11756e1720f07cda5a080ef0476786d909b","datavalue":{"value":"temporal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q3097968$D75B93DE-80CC-486E-9369-E33FD04D54AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"85a839a7ba93b7be8ef2a01122562abb5ca55aa9","datavalue":{"value":"LTL","type":"string"},"datatype":"string"},"type":"statement","id":"Q3097968$FF59DF7C-52CD-4940-8E8C-4D901C0CA92D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"af948ab56df44408fff2ba197f928e63c9954960","datavalue":{"value":"CTL","type":"string"},"datatype":"string"},"type":"statement","id":"Q3097968$A049D197-01BD-42CA-B4A6-708376D74488","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5670d071866a3d53f623260620b05efb6ac7d49b","datavalue":{"value":"binary decision diagram","type":"string"},"datatype":"string"},"type":"statement","id":"Q3097968$30F5BDDA-A0E5-4F00-951D-E1CC9CA8A498","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e6ab41959fd9494b5548d09c762ca90a9336e1c7","datavalue":{"value":"bounded model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q3097968$8E71E48B-C87C-4A5A-AD1D-F2EC8BBD4270","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66824d9cf653f7dee3c76f98a8ea1aa06432fa7c","datavalue":{"value":"verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q3097968$CD28F842-5272-4687-849D-828F46D7D1B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f9ac4ef6ef6c5f8856ee80195276e724e0b6225a","datavalue":{"value":"correctness","type":"string"},"datatype":"string"},"type":"statement","id":"Q3097968$0D80232B-6FF2-4F10-B230-CDE9BCCDC078","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"445a4fbc6b6bbba6e3c2169de8e334950d4f0826","datavalue":{"value":"concurrency","type":"string"},"datatype":"string"},"type":"statement","id":"Q3097968$4DF52B62-A4D9-4937-94F6-88EF0154364C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e225ac4aec700ae2c67cab0cb7802b0627e7a3da","datavalue":{"value":"distributed system","type":"string"},"datatype":"string"},"type":"statement","id":"Q3097968$838260C9-E439-4104-85A6-D4850E883067","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f230c47ce693e1ef568cdbf7a69f561dbd91484a","datavalue":{"value":"SAT-solver","type":"string"},"datatype":"string"},"type":"statement","id":"Q3097968$07C7E34C-D7A2-4A04-BAD1-AB4A4D22668E","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3097968$F6F9D19C-6EBF-4FDF-AEB5-B2AB558A2ED8","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f03125fa0aab45a166f1c1a1f28d506581b47ca7","datavalue":{"value":"https://doi.org/10.3233/fi-2011-513","type":"string"},"datatype":"url"},"type":"statement","id":"Q3097968$70470283-B62B-4F0F-9CB3-176FF310F44D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e40a30108b5eb3647446d7364e918a183ea9f28f","datavalue":{"value":"W1666176304","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3097968$8D1F8D18-32BE-4AF0-91CE-F9A70590C316","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9887b7cea0f2c68bf55acdd17a5d473efff2dc8b","datavalue":{"value":{"entity-type":"item","numeric-id":5394178,"id":"Q5394178"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4a3ff378dc7c3dc6d5af5648044599b17228aa0a","datavalue":{"value":{"amount":"+0.8341907858848572","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3097968$12D2CA4E-EE7F-4D84-89A0-737B5FC7C14C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9b9ec0decb7be3be1b5b97b74f6d05bf61c3d572","datavalue":{"value":{"entity-type":"item","numeric-id":6487366,"id":"Q6487366"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0d2838d050334a26c80b611ed6e9aa326e4ddf58","datavalue":{"value":{"amount":"+0.8115584850311279","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3097968$45166105-235E-4B6C-A77F-8B82C6F696B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"18ca58fba2f3f6c452d2fc675d43a44bd6661103","datavalue":{"value":{"entity-type":"item","numeric-id":3146278,"id":"Q3146278"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"63a805cffc1eab393d10ffbe531930f153844141","datavalue":{"value":{"amount":"+0.8102489709854126","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3097968$2D211F40-ECB8-469A-B2F4-59D1DE47462C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d9bc0d0a982a32d3b01e7797b4f0d8f4a290eca8","datavalue":{"value":{"entity-type":"item","numeric-id":4925273,"id":"Q4925273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"49c0a3d93c372667b8b6b04dc6c1f4b770ec75de","datavalue":{"value":{"amount":"+0.7941869497299194","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3097968$7CEAB7AA-60B0-45EC-AEB5-E1E833A22217","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8540a29c3fb7bd77b1d3cc719c320dd87f1cc694","datavalue":{"value":{"entity-type":"item","numeric-id":5259305,"id":"Q5259305"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"faf3c983512b62546f43f3023da867e34a7892ed","datavalue":{"value":{"amount":"+0.7868899703025818","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3097968$8D92D912-588A-43F2-82AA-5F4E09558595","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"BDD-based bounded model checking for temporal properties of 1-safe Petri nets","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/BDD-based_bounded_model_checking_for_temporal_properties_of_1-safe_Petri_nets"}}}}}