{"entities":{"Q7361954":{"pageid":31521401,"ns":120,"title":"Item:Q7361954","lastrevid":105369545,"modified":"2026-10-07T13:38:06Z","type":"item","id":"Q7361954","labels":{"en":{"language":"en","value":"Converting Linear-Time Temporal Logic to Generalized B\u00fcchi Automata"}},"descriptions":{"en":{"language":"en","value":"AFP entry LTL_to_GBA"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7aab7b2edd27954e83681d23247b55d0dee5e764","datavalue":{"value":"https://isa-afp.org/entries/LTL_to_GBA.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361954$A9854AFF-FE11-424E-9E85-708099559FCF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"a696f05378d1338ede6149124bc9da54876abcc7","datavalue":{"value":{"time":"+2014-05-28T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361954$CE471965-358B-4482-A6F2-91FD1FD25516","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"493dbd4a2996bd8d532db178e854c885e9335058","datavalue":{"value":"Alexander Schimpf","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361954$A27BD6A7-FAE6-4E40-AEE9-22CD3C051D94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"7545c5768cca6bd4b47e52bfec18c22cb81849df","datavalue":{"value":"Peter Lammich","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361954$AB622047-8BD0-4E01-9282-E4D96BD6BF03","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cf383f622e764c3e968d461b250ee512162deec3","datavalue":{"value":{"text":"Converting Linear-Time Temporal Logic to Generalized B\u00fcchi Automata","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361954$E70BAF0E-D6B9-4E3E-A1D3-BB2C1C8939F9","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"b101c7617df75a9c84583771121299c015500ddf","datavalue":{"value":"We formalize linear-time temporal logic (LTL) and the algorithm by Gerth et al. to convert LTL formulas to generalized B\u00fcchi automata. We also formalize some syntactic rewrite rules that can be applied to optimize the LTL formula before conversion. Moreover, we integrate the Stuttering Equivalence AFP-Entry by Stefan Merz, adapting the lemma that next-free LTL formula cannot distinguish between stuttering equivalent runs to our setting. We use the Isabelle Refinement and Collection framework, as well as the Autoref tool, to obtain a refined version of our algorithm, from which efficiently executable code can be extracted.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361954$BADBAC55-E541-423D-90F6-FBE7EC338B79","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":"Q7361954$3E212992-AFC8-42DE-9F37-2B0CD32BD8B0","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"57153f9096aa0dddca483f863db49f1a20c72ecc","datavalue":{"value":{"entity-type":"item","numeric-id":7361530,"id":"Q7361530"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361954$69622C0E-4782-426A-AE0B-7AC5FDB97E92","rank":"normal"},{"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":"Q7361954$207010A2-D0BA-4001-90C3-041B6CD8715B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"e311985e283a0fa73130406ac266a6c4f80c0424","datavalue":{"value":{"entity-type":"item","numeric-id":7361873,"id":"Q7361873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361954$17154C31-9FA4-46E9-AB0F-9F1113199C5F","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":"Q7361954$02DF5F9A-E4B9-411D-98EA-CFBB0C2AE841","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":"Q7361954$65A11FAE-267C-47FA-9BB2-A5B5BC8526AF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Converting Linear-Time Temporal Logic to Generalized B\u00fcchi Automata","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Converting_Linear-Time_Temporal_Logic_to_Generalized_B%C3%BCchi_Automata"}}}}}