{"entities":{"Q7361664":{"pageid":31520531,"ns":120,"title":"Item:Q7361664","lastrevid":105366857,"modified":"2026-10-07T13:36:43Z","type":"item","id":"Q7361664","labels":{"en":{"language":"en","value":"The Weak Spectroscopy Game to Characterize Behavioral Equivalences"}},"descriptions":{"en":{"language":"en","value":"AFP entry Weak_Spectroscopy"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"548859603014d3fc7601d552f6b4bf03596c6327","datavalue":{"value":"https://isa-afp.org/entries/Weak_Spectroscopy.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361664$A9AE7501-8999-4768-8DF5-0DED16746EEB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f652ec88ec3e1fe6ec4cd63a853e8f8dcb5fd2bd","datavalue":{"value":{"time":"+2025-11-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361664$33DF834A-810D-4199-8E01-6B12DD91DAB7","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"eecae46ff9623cbc159d6d906d3ea48ccdb9cb3e","datavalue":{"value":"Lisa A. Barthel","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361664$9ADCE187-AFDC-4702-AB1D-FC9C9F65D7F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"15beee96a42c101781f14b11b129954d6cea277b","datavalue":{"value":"Leonard M. H\u00fcbner","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361664$2C15420E-1A69-4F48-91C5-AE68396325EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"8839ada749fd7fa5bdc65bc4d2e3547f6f692ea3","datavalue":{"value":"Caroline Lemke","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361664$78D8676F-FAA0-4DD9-A524-1FDC089E2DBD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"026e4b4890185c0fb29221328eae59ade9f93599","datavalue":{"value":"Karl P. P. Mattes","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361664$BCCF7F49-BC0A-4CC4-BBE4-05EBF7331413","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"e16ec6509889f63aa9e51ac093be9c873bc55b0a","datavalue":{"value":"Lenard Mollenkopf","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361664$590D9F37-8689-4FFC-B2E9-3919DD3BF621","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"f9ca340aa87216db3545ff3ff7b803c99d91513c","datavalue":{"value":"Benjamin Bisping","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361664$4B95FA06-07CC-4583-AAB2-6C87E07AFAF4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cf14ea6b809715b9c509ac4bd9b29034d64ff493","datavalue":{"value":{"text":"The Weak Spectroscopy Game to Characterize Behavioral Equivalences","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361664$88F9F742-F744-4844-871D-89DE2D9CD8BD","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"fdbc9f493c7e89ee9dfc000e04e80d1e28058671","datavalue":{"value":"We provide an Isabelle/HOL formalization of Bisping and Jansen's weak spectroscopy game (2024), which can be used to simultaneously characterize and decide a hierarchy of behavioral equivalences for systems with internal behavior. This is valuable for applications in concurrency theory and formal verification where equivalences and distinctions of the \u201clinear-time\u2013branching-time spectrum\u201d are a recurring topic. This entry contains a game characterization of most behavioral equivalences from stability-respecting branching bisimilarity to weak trace equivalence. Technically, the results link distinguishing sublanguages of Hennessy\u2013Milner logic to winning attacker budgets in an energy game through an eight-dimensional measurement of syntactic features appearing in formulas.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361664$5E4825E4-0412-4431-95DD-BDD158704E0A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"6910420cfeb202403aca68fb46accf72d94f7850","datavalue":{"value":{"entity-type":"item","numeric-id":6535628,"id":"Q6535628"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361664$44E8E2E8-6154-4015-909B-F81CF63FEBE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6c0bb5644ae2f5cd5e29f5e00d0fd59022de0741","datavalue":{"value":{"entity-type":"item","numeric-id":6940577,"id":"Q6940577"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361664$2BBB105B-BA82-4342-BE3E-8B09D504DD41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b327263919aa555338c22c3161dbf4ddc1f5c43f","datavalue":{"value":{"entity-type":"item","numeric-id":2272990,"id":"Q2272990"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361664$6B4B81DB-A6B6-4D6E-9D7D-D75591D54047","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"12062be6bcc6b2165d16902eff3a372a4b12e161","datavalue":{"value":{"entity-type":"item","numeric-id":3883467,"id":"Q3883467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361664$7D12E57C-5D09-4592-9162-D3725BB028B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f107e1284a9b69e3a2313319c53bf476c648394a","datavalue":{"value":{"entity-type":"item","numeric-id":7310305,"id":"Q7310305"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361664$C3A711FF-ADE3-41FA-A2A9-F48A99F71E48","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":"Q7361664$81542B9C-55F2-4B76-99DB-7AA1C892EBCB","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"d4e45a44d8cb21e0bc3c4e18fb1edc38a1545452","datavalue":{"value":{"entity-type":"item","numeric-id":7360785,"id":"Q7360785"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361664$928858C1-9F3E-4A0A-B5BD-F67E06546622","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P2651","hash":"76ebf0a881644521425e5e5631f4667be29e9869","datavalue":{"value":{"entity-type":"item","numeric-id":7360813,"id":"Q7360813"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361664$F896D3C4-F8CF-477F-B364-728D5C4DAD53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P2651","hash":"a72569ac3fa7d166ec3d63a25d7f4970dd09f6f6","datavalue":{"value":{"entity-type":"item","numeric-id":7360825,"id":"Q7360825"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361664$73ECE886-1C9C-4451-BE7D-E626686CCE4C","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":"Q7361664$E75916DA-8194-46AD-B5E4-E224D8DD4EC1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The Weak Spectroscopy Game to Characterize Behavioral Equivalences","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_Weak_Spectroscopy_Game_to_Characterize_Behavioral_Equivalences"}}}}}