{"entities":{"Q40289":{"pageid":40345,"ns":120,"title":"Item:Q40289","lastrevid":105428189,"modified":"2026-10-09T10:09:15Z","type":"item","id":"Q40289","labels":{"en":{"language":"en","value":"Stuttering Equivalence"}},"descriptions":{"en":{"language":"en","value":"AFP entry Stuttering_Equivalence"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"9a7b36e3f8833191524a12e76e31167b2f0639f9","datavalue":{"value":"28575","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40289$C1DE43FB-567D-48EA-9D8A-0E05DD395555","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":"Q40289$E47BCC43-50AD-40C2-B0D6-763B176B1EFE","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"5804c9032b01d40ba43f6cb2019dda8d382d84d7","datavalue":{"value":"https://www.isa-afp.org/entries/Stuttering_Equivalence.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40289$875FE86E-4ABD-443E-BA0B-AAA4D66BFE33","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40289$E7B4E51D-04BC-4AF8-A824-06E9DEE20B50","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"587eb1ff352d74d75ec39594cac10abdfc1440c2","datavalue":{"value":{"entity-type":"item","numeric-id":40265,"id":"Q40265"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40289$33A87D41-A000-4EF5-B04F-EB3A8C45D3AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"aedeaf0144ca38f7cb9a3b8f0e43e0ed5b0f0353","datavalue":{"value":{"entity-type":"item","numeric-id":40283,"id":"Q40283"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40289$4DBE10B4-D9F2-4FD5-9AC9-91E3246E601D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ac6e4b2309e3317f96b1f72a4f626411283f5bc5","datavalue":{"value":{"entity-type":"item","numeric-id":40629,"id":"Q40629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40289$8137F97D-5540-4443-9555-8C8E1F28857A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"fb0918295880c75ce7e6107c7f8260e1eb005ccf","datavalue":{"value":{"entity-type":"item","numeric-id":40284,"id":"Q40284"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40289$72506CDF-4732-433C-958F-D24EA713C511","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"27b35591f9a1d87570b3e9ffb19e51ff7cd09a28","datavalue":{"value":{"entity-type":"item","numeric-id":40544,"id":"Q40544"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40289$98918210-43D9-47F5-A3DE-C83F831D6AED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a5226fd137c2167e439294ca4cdc09da6fe13411","datavalue":{"value":{"entity-type":"item","numeric-id":40324,"id":"Q40324"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40289$A912AF4E-2DFA-4FAA-B048-03A7D2810F93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"5e206e7a803121c179c257c0b4386d68cd679bdc","datavalue":{"value":{"entity-type":"item","numeric-id":40949,"id":"Q40949"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40289$89E2A0D9-F19F-4875-BD86-14EA324F63B4","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":"Q40289$14A271BB-BC12-4D2C-8657-02D899510E56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"2f0eb5498f624eca19e760cd08d6ae2738f933e4","datavalue":{"value":{"entity-type":"item","numeric-id":40251,"id":"Q40251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40289$E043AC19-ED96-40B1-895C-3C1531E88E14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"0566ad334499237f2689386a24c3ff4452487d83","datavalue":{"value":{"entity-type":"item","numeric-id":15987,"id":"Q15987"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40289$36E61213-2120-4016-9CA8-49B68E0B0669","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"f349865de5c29264842bf478dc01d3ee732ed741","datavalue":{"value":{"entity-type":"item","numeric-id":19657,"id":"Q19657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40289$C4AAC3F9-A0AD-4C98-95D3-BDF0E82DA686","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":"Q40289$8B51662A-77AC-4528-A67F-5D2171165044","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":"Q40289$F9ACCF9E-1097-4E18-9A63-193ABEA6C36E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1b2e9b15269ef09e5a70fe2ec85a48ad2e8e4a72","datavalue":{"value":"https://isa-afp.org/entries/Stuttering_Equivalence.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40289$CCB406DA-A378-409E-A9FF-E5B6760359B8","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"cc9e79466e658b1f2029f03a95cc9639795afc16","datavalue":{"value":"Stephan Merz","type":"string"},"datatype":"string"},"type":"statement","id":"Q40289$3F792EF2-B87F-473D-9E7A-CD89475B5D78","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"ce82fd665cbbb920e0b932a9ba11bf4ceeef0718","datavalue":{"value":"Two omega-sequences are stuttering equivalent if they differ only by finite repetitions of elements. Stuttering equivalence is a fundamental concept in the theory of concurrent and distributed systems. Notably, Lamport argues that refinement notions for such systems should be insensitive to finite stuttering. Peled and Wilke showed that all PLTL (propositional linear-time temporal logic) properties that are insensitive to stuttering equivalence can be expressed without the next-time operator. Stuttering equivalence is also important for certain verification techniques such as partial-order reduction for model checking. We formalize stuttering equivalence in Isabelle/HOL. Our development relies on the notion of stuttering sampling functions that may skip blocks of identical sequence elements. We also encode PLTL and prove the theorem due to Peled and Wilke.","type":"string"},"datatype":"string"},"type":"statement","id":"Q40289$E82B5B69-3AF8-484C-AE03-FF3CE94F4932","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c7a1c120dc379e55cc80f89048abc2e9af9a7f71","datavalue":{"value":{"time":"+2012-05-07T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q40289$88F24DC8-DB20-425A-9E19-6DAF56DF7A2B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a13c46e4fea3c3dfb4c88ba123144ea508031024","datavalue":{"value":{"text":"Stuttering Equivalence","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q40289$53DF5611-5259-4BB0-8A7F-6405E3057F77","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"857799d8f0c80d23f1693fb90d554f48eb5bb5a0","datavalue":{"value":{"entity-type":"item","numeric-id":290250,"id":"Q290250"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40289$DAEAEB05-E38F-49D2-98E8-F3010CE74815","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":"Q40289$EAD8FC85-8E37-4A0E-BFEF-BB7E4472898C","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"8ac34df43fbb99027916440c753dc68e36985fe2","datavalue":{"value":{"entity-type":"item","numeric-id":7361475,"id":"Q7361475"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40289$D24ECFC4-E122-4031-A989-6D811C62432B","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"73d93a21b0749f7f2c51d7daeb11b162660cd756","datavalue":{"value":{"entity-type":"item","numeric-id":7360784,"id":"Q7360784"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40289$EBA42089-82E4-4AA1-A07B-15826A387DA4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Stuttering Equivalence","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Stuttering_Equivalence"}}}}}