{"entities":{"Q1377904":{"pageid":1388644,"ns":120,"title":"Item:Q1377904","lastrevid":67287765,"modified":"2026-04-12T16:36:54Z","type":"item","id":"Q1377904","labels":{"en":{"language":"en","value":"Automatic verification of sequential infinite-state processes"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1110379"}},"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":"Q1377904$793876C7-93FF-4A0C-B3DE-C7C70565657E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"484d2412148e6cb9a7c566a46eaf532b687a0b8e","datavalue":{"value":{"text":"Automatic verification of sequential infinite-state processes","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1377904$8050AA49-9517-44BC-910E-580BCB3B1038","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"3ba3bc740bd50ecc40e95e315d50003fe17d4048","datavalue":{"value":"1049.68001","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1377904$D8B4C79B-E49F-41B5-B350-AE93A8817CED","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d46c53f936687b8df4a47013b8cf33c0c46ee261","datavalue":{"value":{"entity-type":"item","numeric-id":1377903,"id":"Q1377903"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1377904$0A75F5F9-E832-4410-B3E3-008B31E282FC","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1377904$6FF0FC64-2E99-4A09-B2F3-0EA40B1EA72E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f4792ae2ab319fd603aad0c994faff1f40f5e4ae","datavalue":{"value":{"time":"+1998-01-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1377904$AA226713-4A0D-44DF-9F46-07C0EF7DAD3D","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"80c0891f7135c72158176db600a927af62565f8c","datavalue":{"value":"The short monograph -- based on the author's doctoral thesis -- discusses a theoretical framework for the verification of reactive, sequential infinite-state systems. These are typically nonterminating systems. The \\textit{invariance} is key concept: it records what remains true throughout the execution of the program.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1377904$16E99A28-BB7D-472C-B663-554E116682AD","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"24aafcf24a21bd70cd3b62d3f5f72a6d0d82d816","datavalue":{"value":"68-02","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1377904$C5ACD344-52B5-4E00-A45E-4D5E58CCF24A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d23157792ba791094e38028c088117b4d3b3a45c","datavalue":{"value":"1110379","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1377904$AD15C99E-8F93-4FDE-A2E4-6A0FA597159E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8cf2a44934d806d738320c00b178d2aeb36d6d2f","datavalue":{"value":"sequential processes","type":"string"},"datatype":"string"},"type":"statement","id":"Q1377904$379D53F7-A452-4F97-AA24-D450316776B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb9f8004d477a3922fe8bde53d670f8b57c48852","datavalue":{"value":"model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q1377904$A6286916-BA63-4819-93E0-216698AABD27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"94a460cf012fa9356569b14e64b0464838067e30","datavalue":{"value":"equivalence checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q1377904$211045BF-B95B-459D-941A-F798F6AF80FA","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"21fa9a9223cebca47884c37548205488b3400e7b","datavalue":{"value":{"entity-type":"item","numeric-id":235567,"id":"Q235567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1377904$3F3B95A8-83DE-4073-A633-2600DE461AB9","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":"Q1377904$2205791B-4AA6-4B37-80E4-5D5E1A11AC25","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cf5b43b408b2da4a683dba83631a428854b25f1e","datavalue":{"value":{"entity-type":"item","numeric-id":5491850,"id":"Q5491850"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3dcf64266c2a161eb805b042d30ba65c0c49f6a8","datavalue":{"value":{"amount":"+0.7986478805541992","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":"Q1377904$9D9457F9-CEA1-4DB5-88F7-948A4E3D53E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a5979cfe658453256f286c1ae7050f9bd04c5570","datavalue":{"value":{"entity-type":"item","numeric-id":2754072,"id":"Q2754072"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ebabbc6ad4288baf0617b06b8a2a0faaee0409ec","datavalue":{"value":{"amount":"+0.7836513519287109","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":"Q1377904$1EF171DC-0557-4474-9B71-DC27E53D38CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d28b0b11fc8f86118e03d0ab936f51f7e124784b","datavalue":{"value":{"entity-type":"item","numeric-id":2767987,"id":"Q2767987"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a7889c7386d16e58137201728bef92bee2676c73","datavalue":{"value":{"amount":"+0.7827950716018677","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":"Q1377904$294D7830-1FA3-47D5-9E81-CBDA766AA313","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"024cbed37b7fde1e1dac412cf215393e649fe204","datavalue":{"value":{"entity-type":"item","numeric-id":1407321,"id":"Q1407321"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"885756e95158dd0ca996fc92eaa5ca28f3dbe1eb","datavalue":{"value":{"amount":"+0.7747703790664673","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":"Q1377904$71C783A2-4D7D-4464-95CE-27D2B49AE8D2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Automatic verification of sequential infinite-state processes","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Automatic_verification_of_sequential_infinite-state_processes"}}}}}