{"entities":{"Q7361026":{"pageid":31518617,"ns":120,"title":"Item:Q7361026","lastrevid":105362441,"modified":"2026-10-07T13:34:13Z","type":"item","id":"Q7361026","labels":{"en":{"language":"en","value":"Verification Components for Hybrid Systems"}},"descriptions":{"en":{"language":"en","value":"AFP entry Hybrid_Systems_VCs"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6b3d9014751f9dcd991f6d8b075e86a91c0cc2e0","datavalue":{"value":"https://isa-afp.org/entries/Hybrid_Systems_VCs.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361026$1FEA5753-BB6B-424A-92E9-D8C9853C3320","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"bc84744ff137a14a0f2c32fabac998ce0cb5e5fa","datavalue":{"value":{"time":"+2019-09-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":"Q7361026$60696122-D3BD-4E3F-AB12-D45C566BA952","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"5794d91a39dde2e8f368834014ac9f67037fb91a","datavalue":{"value":"Jonathan Julian Huerta y Munive","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361026$56267796-98E9-439E-A442-2B50D9AF3415","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"be1f6f6a9e01121a43e4f16a89f897fd6d796619","datavalue":{"value":{"text":"Verification Components for Hybrid Systems","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361026$6916C668-466F-4A76-8B54-33F1C9A9E821","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"9bbabec4969f631f10c813177d354d7161cb1742","datavalue":{"value":"These components formalise a semantic framework for the deductive verification of hybrid systems. They support reasoning about continuous evolutions of hybrid programs in the style of differential dynamics logic. Vector fields or flows model these evolutions, and their verification is done with invariants for the former or orbits for the latter. Laws of modal Kleene algebra or categorical predicate transformers implement the verification condition generation. Examples show the approach at work.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361026$DE102791-AA48-47C9-9D2A-9B777F713BEE","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"6fc62f32ebe5f2c566c09500f98ee202c262830a","datavalue":{"value":{"entity-type":"item","numeric-id":736461,"id":"Q736461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361026$0C9A8959-9E92-4B4C-BF5F-D94A9C2403A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5d5703d8b9ac3f2ec42c5cea3cb6310bb02f051a","datavalue":{"value":{"entity-type":"item","numeric-id":627202,"id":"Q627202"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361026$EEE9EC2E-F8A7-4110-B1E6-107F8A3229D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"12bcad11fe97484505c727089d3af542344d4df9","datavalue":{"value":{"entity-type":"item","numeric-id":4930176,"id":"Q4930176"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361026$1B2C9EA8-FD1D-4B17-96F3-E6D41A32E9CC","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361026$9764C7EF-DEE5-437B-8BA3-770D0B14CB86","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"842345d524917a859fbf25bdbec5eafcad9e81bc","datavalue":{"value":{"entity-type":"item","numeric-id":7361028,"id":"Q7361028"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361026$3415A65A-8DB4-4C53-ABCC-F558799E10CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"422342c3fb34631af5f61097819a09568775a669","datavalue":{"value":{"entity-type":"item","numeric-id":7361454,"id":"Q7361454"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361026$1BE11B20-CF98-4DD6-867F-077FE55D9DE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"eadaad3e8c289407562ca1c737ca67733c4b6104","datavalue":{"value":{"entity-type":"item","numeric-id":7361890,"id":"Q7361890"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361026$77C3ACFA-9335-457F-95F0-A98EB25EDDD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"a0111f8bfafa44019b8315fe65694a717c6a568d","datavalue":{"value":{"entity-type":"item","numeric-id":7361478,"id":"Q7361478"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361026$ED9D2D7D-A912-4D16-910E-9137903C55B9","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"65292b3c42fa1bd5c21e4c91fe94fdc3f630f232","datavalue":{"value":{"entity-type":"item","numeric-id":7360821,"id":"Q7360821"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361026$41282AB3-3C5C-41EB-9143-6778AAFB3F6D","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361026$46702318-F28C-4F77-AC00-24AFE415D891","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Verification Components for Hybrid Systems","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Verification_Components_for_Hybrid_Systems"}}}}}