{"entities":{"Q7361868":{"pageid":31521143,"ns":120,"title":"Item:Q7361868","lastrevid":105369935,"modified":"2026-10-07T13:38:44Z","type":"item","id":"Q7361868","labels":{"en":{"language":"en","value":"Markov Models"}},"descriptions":{"en":{"language":"en","value":"AFP entry Markov_Models"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d718cfd3301586cb6c334523250013ba8df3a0bd","datavalue":{"value":"https://isa-afp.org/entries/Markov_Models.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361868$678B8710-031D-43F3-8E42-599C3CC90F83","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"871362ac18f9a189e8200fce4532cbdae8066779","datavalue":{"value":{"time":"+2012-01-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361868$2C7885A9-91FA-4DA9-B0CE-01293D713D63","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"01b202f25e5390ba0104cc409e25272c5fbddba4","datavalue":{"value":"Johannes H\u00f6lzl","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361868$F7A5BD4C-FEB4-4AFA-A920-2BAE83976D5E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"78083bbf5b06a4f292e9e00ee445948e4fa51db5","datavalue":{"value":"Tobias Nipkow","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361868$CC315C4A-9C1D-42F9-B341-69874223E712","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"188414ba2c048d1aaccd1524ef4f06896517d4af","datavalue":{"value":{"text":"Markov Models","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361868$692FAB57-666E-4639-8D9F-7C21FF03952E","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"4adac158bd253d5f139d38e12a11ece8d094deff","datavalue":{"value":"This is a formalization of Markov models in Isabelle/HOL. It builds on Isabelle's probability theory. The available models are currently Discrete-Time Markov Chains and a extensions of them with rewards. As application of these models we formalize probabilistic model checking of pCTL formulas, analysis of IPv4 address allocation in ZeroConf and an analysis of the anonymity of the Crowds protocol. See here for the corresponding paper.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361868$13D06C9C-7AE3-461F-98B3-AE3FDA05E415","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b29ad255f0f1fc43ea69d59d95eb9a24cc08b4d4","datavalue":{"value":{"entity-type":"item","numeric-id":2894281,"id":"Q2894281"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361868$5D4FC04D-51C4-467A-8366-61009298524B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3710c9b6ddf8dbb24e135f3387ab935865a76ef6","datavalue":{"value":{"entity-type":"item","numeric-id":2829281,"id":"Q2829281"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361868$1C4AAA0A-CD11-4FD0-B373-1007F47C719C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e2ce2556dd2c787e12076af0e059323648aa5a8f","datavalue":{"value":{"entity-type":"item","numeric-id":1701041,"id":"Q1701041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361868$CBFE888B-2A46-4EB5-BC62-57373E78A05F","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":"Q7361868$C2427D0B-BA4A-4695-982C-D632071F9CFA","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"c9d73c02403c0af647a73b8da7299dbef78ebf0b","datavalue":{"value":{"entity-type":"item","numeric-id":7361764,"id":"Q7361764"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361868$354AB26D-DE4B-4537-8931-D0C47C82B1EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"c284fafd8ee27c174064ad310b42f9dc3309e26e","datavalue":{"value":{"entity-type":"item","numeric-id":7361848,"id":"Q7361848"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361868$DCA93ABD-ABCB-4191-8D06-64629DBE0BBA","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"8efbe8612495bcc999dc22ed8b71d2801a69cc6a","datavalue":{"value":{"entity-type":"item","numeric-id":7360834,"id":"Q7360834"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361868$21944CE4-410A-4247-BF0C-F68EDA99B143","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":"Q7361868$0B776040-4483-4075-897F-B403AEA51C81","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Markov Models (AFP entry Markov Models)","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Markov_Models_(AFP_entry_Markov_Models)"}}}}}