{"entities":{"Q364388":{"pageid":366155,"ns":120,"title":"Item:Q364388","lastrevid":61419699,"modified":"2026-04-10T23:15:11Z","type":"item","id":"Q364388","labels":{"en":{"language":"en","value":"Bounded model checking of ETL cooperating with finite and looping automata connectives"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6206804"}},"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":"Q364388$C5F2FF1F-05B5-4988-A806-1C1B0E1113A7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b103a71725ce2a9e862db5d8f61a50a9509748e7","datavalue":{"value":{"text":"Bounded model checking of ETL cooperating with finite and looping automata connectives","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q364388$95CE59D6-48AD-4486-8023-A0C0776191F7","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5dd9a7c8f5c376b97bfc61ea064ba934b4555dfa","datavalue":{"value":"1311.68090","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q364388$49CBD6E7-5EC0-4E35-B181-A7F3183B4CED","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"81b662e7e606c72de5969679196c091e76c2e114","datavalue":{"value":"10.1155/2013/462532","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q364388$FA851A99-4AAC-41DF-B225-5F10D0142530","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"516f52fd1e79844cbe7b2f5aeb3aef6232b4b628","datavalue":{"value":{"entity-type":"item","numeric-id":364385,"id":"Q364385"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364388$F458A66B-C8F0-4D6A-B725-E2BFC46A268F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"83bc908bde29d7fb9807a195933068fc2c38b4c5","datavalue":{"value":{"entity-type":"item","numeric-id":364386,"id":"Q364386"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364388$95BBC6A8-417A-4201-966A-6F8385F5EC2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"fd013030da45f468fbef74955f8c67832b7b2ff3","datavalue":{"value":{"entity-type":"item","numeric-id":364387,"id":"Q364387"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364388$5BBE9930-8A44-43FC-890E-D611A35AD5FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a987699fd23888733c3cf6186ec5b68180cd27f8","datavalue":{"value":{"entity-type":"item","numeric-id":281290,"id":"Q281290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364388$832053F8-BFED-437B-BA8C-E3DCD3202550","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"da90f21edc8aedcea520f32e6546eaba263a853f","datavalue":{"value":{"entity-type":"item","numeric-id":6065814,"id":"Q6065814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364388$8275AFB1-1B15-426F-A4E4-46C9B4D4E987","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"bb299feb2b87699ac8beef494c52fd2765eaf609","datavalue":{"value":{"entity-type":"item","numeric-id":118601,"id":"Q118601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364388$6BF02D94-ECA2-4818-8AC1-6CC91D9A5F34","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6e8c017497806797f217f1d658e3d224a2498206","datavalue":{"value":{"time":"+2013-09-09T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q364388$AACD4476-9622-478F-BA4C-CD7A77E2B9C4","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"3e6cd269dee417417eba95f1be9482e79ff4f692","datavalue":{"value":"Summary: As a complementary technique of the BDD-based approach, bounded model checking (BMC) has been successfully applied to LTL symbolic model checking. However, the expressiveness of LTL is rather limited, and some important properties cannot be captured by such logic. In this paper, we present a semantic BMC encoding approach to deal with the mixture of \\(\\text{ETL}_f\\) and \\(\\text{ETL}_l\\). Since such kind of temporal logic involves both finite and looping automata as connectives, all regular properties can be succinctly specified with it. The presented algorithm is integrated into the model checker ENuSMV, and the approach is evaluated via conducting a series of imperial experiments.","type":"string"},"datatype":"string"},"type":"statement","id":"Q364388$CAFB0B7C-B6BC-41FE-B2C6-B1A17E2050A0","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q364388$013088FC-13BA-4109-AA24-381C328A69AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e2244b32b83bf71a9c045223e635ab074452b389","datavalue":{"value":"03B44","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q364388$969CDA9F-6A8A-442D-BE22-64EB8A254CD0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9b78776a56fc28cdd893baa47605a105412b838a","datavalue":{"value":"68Q45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q364388$DA22DED1-6985-4964-9B03-A3B0D3B8FBBC","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e3852d706d54223a5cc033a3224b6e0425584f86","datavalue":{"value":"6206804","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q364388$6F3B1432-6CFE-47EF-B3F4-D1464D9866CD","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"efa7dfee3dd74aae04647605d0a9a987c7d566cf","datavalue":{"value":{"entity-type":"item","numeric-id":16316,"id":"Q16316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364388$8FDCA747-9E2A-45BD-BCAE-A07FD3E9446C","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":"Q364388$8380C218-3195-4DFC-9348-921117095709","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f062ec5a9da4db58a57f1c2395f7aa23620ff9f3","datavalue":{"value":"https://doi.org/10.1155/2013/462532","type":"string"},"datatype":"url"},"type":"statement","id":"Q364388$C22550D8-9DE3-4F65-8265-70F0211F7669","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"37abea5868dd83c470056224821ad7293d52bb8a","datavalue":{"value":"W2053008981","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q364388$BF1A3083-1C4A-4D6E-BB6E-116D6B4B6620","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"a61706b65986b44411d0183d63afeda8d278e652","datavalue":{"value":"Q59006099","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q364388$19E2ABAB-88D5-4E20-9FF3-13BE8F5EEA63","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d0863918228d158fae088a6efc6f79f2c8e8057","datavalue":{"value":{"entity-type":"item","numeric-id":3724245,"id":"Q3724245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364388$4CF41690-A1EE-4621-B067-2B4D584916E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1d6a31e0cf3ff6a73ad4ee5a92d1ed62572bdd89","datavalue":{"value":{"entity-type":"item","numeric-id":3317085,"id":"Q3317085"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364388$EA68A003-E917-4935-9FD7-95283072576D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5f45f552829e448fdb1f5d0c5585c08bd5972555","datavalue":{"value":{"entity-type":"item","numeric-id":3694687,"id":"Q3694687"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364388$FABE99D6-1BE4-407E-933D-96F4870355C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9a905ba949a06cde66174f0d589d9794d6c05423","datavalue":{"value":{"entity-type":"item","numeric-id":3711745,"id":"Q3711745"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364388$545F0696-5C54-4449-9B81-7305F090BBC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8d079b47cf1ba2d598f964b28ddec583cafa7821","datavalue":{"value":{"entity-type":"item","numeric-id":1088653,"id":"Q1088653"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364388$E7E8C385-8B45-4E03-B5D5-090EC9C93E93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a01840145b645722449aa29d23c00ba5f807150","datavalue":{"value":{"entity-type":"item","numeric-id":3525092,"id":"Q3525092"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364388$34B7D797-9CCE-41A7-91B1-4E91B782157F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e23095c9e979a8ccbe1d8e5e4d4b937b8eb36cf7","datavalue":{"value":{"entity-type":"item","numeric-id":4472249,"id":"Q4472249"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364388$E8E9BDDF-2D97-4F89-9FED-66BD03E082BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"26e30b87f6e3f7618cfea7524c097e8adbdcbcd4","datavalue":{"value":{"entity-type":"item","numeric-id":4551164,"id":"Q4551164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364388$2245177C-7D7F-48F9-AA18-EEB5CE7D415D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9be1d7bb0141c600a3415908525c502c9ffc451c","datavalue":{"value":{"entity-type":"item","numeric-id":1341752,"id":"Q1341752"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364388$153801AE-53C4-43B6-8A63-3FDE2D4B82E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8d0ba3078dc0571f8571cfdef6334bc3060b114e","datavalue":{"value":{"entity-type":"item","numeric-id":2848673,"id":"Q2848673"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364388$EA22D3C9-3F2B-4ADD-A133-084E2386EFC3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d9989385b6d21787669f1b90c6937d74a8a738ea","datavalue":{"value":{"entity-type":"item","numeric-id":5310676,"id":"Q5310676"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364388$1547398C-3A9D-4AC6-8C6D-DE7FC8B089A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"61774d9849f10e1dd86ae551842bcf10d090eb09","datavalue":{"value":{"entity-type":"item","numeric-id":5901905,"id":"Q5901905"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364388$73BD7A63-505F-4258-8EC4-90147FAB553B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"521fcf11de7d8721521e1e478560508699e8a82f","datavalue":{"value":{"entity-type":"item","numeric-id":5492980,"id":"Q5492980"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364388$0BBD57DA-926E-4B9B-93CA-830DB75442F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77feb9554f98250a94e59cd9498073fd0d68d88e","datavalue":{"value":{"entity-type":"item","numeric-id":5711503,"id":"Q5711503"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364388$AB2111E4-377F-446E-B190-232E0E294C85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7f5f3cd0c0fdd70d2eae3e5f69e2ee0aa687d8a4","datavalue":{"value":{"entity-type":"item","numeric-id":5716540,"id":"Q5716540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364388$51CD3B25-ABB6-4562-B1BA-C8664B80890B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a4653c4bce41e453d944c01560a098b2b498c9c7","datavalue":{"value":{"entity-type":"item","numeric-id":3518271,"id":"Q3518271"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364388$F6726D43-4916-4BBA-8F75-12384E2F6654","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fdbace6415d89fca5d9ba31adb1a3b4e1ba6373e","datavalue":{"value":{"entity-type":"item","numeric-id":3549125,"id":"Q3549125"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364388$B3181E6E-DDE2-4820-BB3F-48140D77F5F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"befac40fe1cb8125522cebeee5546ac3f483c4d3","datavalue":{"value":{"entity-type":"item","numeric-id":5394176,"id":"Q5394176"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364388$96C7984B-ED30-48B5-A9C9-196E09E2792B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"66c3da6e8e22eb9ce673b708daba3d803e9c1df4","datavalue":{"value":{"entity-type":"item","numeric-id":5390016,"id":"Q5390016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364388$B460B731-A3E3-4A79-805C-42CAA70DBD6E","rank":"normal"}],"P1635":[{"mainsnak":{"snaktype":"value","property":"P1635","hash":"7c6837a2875bd54e2907beca8bd5a614e19a6156","datavalue":{"value":"journals/jam/WangLLMW13","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q364388$59BB60BD-A39C-42CA-B27B-F8D55B2FD171","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"297f9a57f303c8c036d110ba8003ae3808693f2e","datavalue":{"value":{"entity-type":"item","numeric-id":5422273,"id":"Q5422273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dfc6b776f271b4ecd2e31430d3feb01b417d70ac","datavalue":{"value":{"amount":"+0.8289042115211487","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":"Q364388$700C2D50-7A58-4391-AF2D-0CFD25FF2C76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2d9353b3b3b24b338fcae1b5a7af1977ccf4b16b","datavalue":{"value":{"entity-type":"item","numeric-id":2848673,"id":"Q2848673"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3e9d42f9ed32b69dc4fd20c71c285273b13e773b","datavalue":{"value":{"amount":"+0.8098887205123901","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":"Q364388$5DE18F0D-FB8E-4527-8060-5BC6EA4C142E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"825c9aaa727f79c201debbf710b791dcfdd806b0","datavalue":{"value":{"entity-type":"item","numeric-id":4736997,"id":"Q4736997"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2e2e8a824bb218d95f3bc255f5eaa577b5614232","datavalue":{"value":{"amount":"+0.8027362823486328","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":"Q364388$53CB8BC6-EB3E-46CB-AAEE-09305933707F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"04bdf0742bdd522dee8d4e004977de201c067fa6","datavalue":{"value":{"entity-type":"item","numeric-id":2369883,"id":"Q2369883"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eccfc4e71d118640f1a4b83c471c227092619134","datavalue":{"value":{"amount":"+0.8017090559005737","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":"Q364388$53EDA339-B187-429A-9391-E38848B16CC4","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":"34d1347f29d07819adede720c4f8960cffe6e679","datavalue":{"value":{"amount":"+0.7944002151489258","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":"Q364388$DAC05CC9-5B43-448C-938E-CB566C00B69B","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q364388$C480C76A-E940-4A66-B2E7-EE46222A2366","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Bounded model checking of ETL cooperating with finite and looping automata connectives","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Bounded_model_checking_of_ETL_cooperating_with_finite_and_looping_automata_connectives"}}}}}