{"entities":{"Q40947":{"pageid":41003,"ns":120,"title":"Item:Q40947","lastrevid":105427433,"modified":"2026-10-09T10:07:36Z","type":"item","id":"Q40947","labels":{"en":{"language":"en","value":"AWN"}},"descriptions":{"en":{"language":"en","value":"AFP entry AWN"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"8a4ca87ef38e283df56354fc545fec60668f5521","datavalue":{"value":"29233","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40947$A1385A95-1B63-49A3-A910-5FD97BECD8FD","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":"Q40947$FAFA4545-0D02-4D46-BBA8-D00931DE5741","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"96478dcdd90b5a2578c38e28128c5e8cf6737b5c","datavalue":{"value":"https://www.isa-afp.org/entries/AWN.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40947$64CEC1F5-A98D-4B70-9C90-40158C5CE44A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40947$D631BC75-F88C-40CF-BC1F-B46189AC9C0A","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"d6d29b9e294eea1a26ce05a4d8663847cfc55575","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40947$D7C8C16E-6200-49CE-A54D-C0F0559D807A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"dc75b1f4f41a196c347c039c5eec89b08662123b","datavalue":{"value":{"entity-type":"item","numeric-id":18543,"id":"Q18543"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40947$3EE4F1EB-C971-4367-878F-454D97C4DFA3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"9ec1fbb0215e78def1ae9dec82cef015c02ce483","datavalue":{"value":{"entity-type":"item","numeric-id":27099,"id":"Q27099"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40947$970B9872-C007-450E-B2EB-3F9C93B1E1BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a2a767ccd0e9bdc5b1b4a2069a6679f9340a857a","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40947$1265FB8A-498B-40D3-A3A8-736261A91CB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ed15eb8701a335444fde1bcc3327d1067ce64751","datavalue":{"value":{"entity-type":"item","numeric-id":24376,"id":"Q24376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40947$EB2E5A9C-4A61-441C-8186-F0308A7746AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"7f5ca315779da8f3ad5a2fbb8c2eab4dc7726a92","datavalue":{"value":{"entity-type":"item","numeric-id":40287,"id":"Q40287"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40947$60528C0E-A21A-43B0-A5AD-CDD66A39493F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"1a13081736616da9f90fce82f89953fc6e18e56a","datavalue":{"value":{"entity-type":"item","numeric-id":25375,"id":"Q25375"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40947$F72E5DBE-54FB-49E0-9D63-3EBFC3F2BBDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8661f4bda66b64d0131f99fd0c519d83e73dfbcf","datavalue":{"value":{"entity-type":"item","numeric-id":40946,"id":"Q40946"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40947$0717D15A-87CE-4048-8054-A3BA9862FF0B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"41b2555b2c8c445e3ef6abe54038169a46d2c4bc","datavalue":{"value":{"entity-type":"item","numeric-id":18521,"id":"Q18521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40947$24F758A8-1CF5-4B76-80ED-9C7327581094","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40947$CA55032F-2B5A-4807-938F-2D259F04AF02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"331995fe532c23e24d72d01a1bd6245fafcd9671","datavalue":{"value":{"entity-type":"item","numeric-id":19106,"id":"Q19106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40947$DB7F94B5-C60E-4E4B-A53C-90699C7871AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"03281999c3208b8f3a62eaceadadf1ce834fe219","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40947$8BD1BCCA-E68A-4852-B140-B942F9344D17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc41d9364226bfa8139f8dbc43b1b77967245f13","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40947$26A4BCFD-AE35-4FB2-B4FC-67E4579149A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ecda3e6d8e971c0b93d4cf3afb41990e853f830f","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40947$49FBB50C-130B-4023-88ED-BEDFEC929736","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"99d0e6fb9cd46dbb2589838c0bfc192273d3e82e","datavalue":{"value":"https://isa-afp.org/entries/AWN.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40947$5333C43C-DD38-4515-BED2-095E63626B23","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"036f489f1dc46b1f48c264ce34d5fc443dd97960","datavalue":{"value":"Timothy Bourke","type":"string"},"datatype":"string"},"type":"statement","id":"Q40947$46FEE2BE-3535-4588-B9CE-6638E7C060BD","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"6b25a3f004a314fc082805d5553b1cd8088d60da","datavalue":{"value":"AWN is a process algebra developed for modelling and analysing protocols for Mobile Ad hoc Networks (MANETs) and Wireless Mesh Networks (WMNs). AWN models comprise five distinct layers: sequential processes, local parallel compositions, nodes, partial networks, and complete networks. This development mechanises the original operational semantics of AWN and introduces a variant 'open' operational semantics that enables the compositional statement and proof of invariants across distinct network nodes. It supports labels (for weakening invariants) and (abstract) data state manipulations. A framework for compositional invariant proofs is developed, including a tactic (inv_cterms) for inductive invariant proofs of sequential processes, lifting rules for the open versions of the higher layers, and a rule for transferring lifted properties back to the standard semantics. A notion of 'control terms' reduces proof obligations to the subset of subterms that act directly (in contrast to operators for combining terms and joining processes).","type":"string"},"datatype":"string"},"type":"statement","id":"Q40947$F1DD90BE-8E8C-4095-B386-7A3D005D6504","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c20d8c327f45ddce8ee8924449a429cc44874390","datavalue":{"value":{"time":"+2014-03-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q40947$42D41846-F432-4C14-B677-77D2A846B7AD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8414b6a3ec307c5b8b630762eb8a4ae1ed30cae7","datavalue":{"value":{"text":"Mechanization of the Algebra for Wireless Networks (AWN)","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q40947$A63029B2-7AA7-4D65-83FA-194F019E9B4A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"905f170f8e42e6203f058d3f7d4bc86d94d9f927","datavalue":{"value":{"entity-type":"item","numeric-id":2879249,"id":"Q2879249"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40947$14C33BBD-5B09-4F62-8603-FC4AA5E91006","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":"Q40947$057FE2D7-F39D-4E80-87D9-F2368916AB1F","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"147d947971425f6e481a02787827e4705017a40a","datavalue":{"value":{"entity-type":"item","numeric-id":7360786,"id":"Q7360786"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40947$D17AE999-9180-4F3E-95B9-B2A43FE37E86","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"AWN","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/AWN"}}}}}