{"entities":{"Q7361278":{"pageid":31519373,"ns":120,"title":"Item:Q7361278","lastrevid":105364490,"modified":"2026-10-07T13:35:20Z","type":"item","id":"Q7361278","labels":{"en":{"language":"en","value":"Mission-time Linear Temporal Logic to Regular Expressions"}},"descriptions":{"en":{"language":"en","value":"AFP entry Mission_Time_LTL_to_Regular_Expression"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a6b55eff50873682d76566f1cf5cb06729bafae4","datavalue":{"value":"https://isa-afp.org/entries/Mission_Time_LTL_to_Regular_Expression.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361278$0F233476-589F-47C5-B39D-04DCA4F958EA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"80b205d07bea2ab271294e7a9fbb7ed69b706f14","datavalue":{"value":{"time":"+2025-01-24T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361278$DE0536D7-8826-463F-A735-871B87EBB2CD","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"a0cb2da1b6cf06bf6a856922c95cf1d75849aa7d","datavalue":{"value":"Zili Wang","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361278$A26DB127-9BA0-4F70-B3E4-9830E9733ADB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"e930e6f6a933f5f4f03863d552f0013c9401bf23","datavalue":{"value":"Katherine Kosaian","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361278$4030CDF6-BD4C-4CC1-A79A-1F895BFD7AA6","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c9e406bfb0731d8d0699a161810a9e129bbe824f","datavalue":{"value":{"text":"Mission-time Linear Temporal Logic to Regular Expressions","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361278$98AD165B-D595-4290-9C12-5E72643AC800","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"f6317edd73142ec4c37c2ac0839612627f38fcb5","datavalue":{"value":"We formalize the WEST algorithm for translating from Mission-time Linear Temporal Logic Formulas to regular expressions and prove it correct, building upon the previous Mission_time_LTL entry in Isabelle/HOL. Additionally, we formalize an algorithm for checking the equivalence of a restricted subset of regular expressions. Both of these algorithms are executable, and the code export is used to validate the existing (previously unverified) WEST tool.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361278$0D01B7F2-2784-42A9-A7D8-C34080E89E22","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"a7949e18a63359cd573d54a1d133e5f25de2159e","datavalue":{"value":{"entity-type":"item","numeric-id":6125795,"id":"Q6125795"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361278$88541633-0CA0-4631-8B0B-1B795D9B0186","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"36b5a38dc5cd54a8d1bc6afe9fdf9d5401ed1605","datavalue":{"value":{"entity-type":"item","numeric-id":6856402,"id":"Q6856402"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361278$98DFB20B-4CCB-4FD4-9AEA-E5C7561CE075","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":"Q7361278$426F1C35-4DC8-4C46-975F-312C9F8782C3","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"578133f3dd196873c1590f77b4ba1497209908e9","datavalue":{"value":{"entity-type":"item","numeric-id":7361622,"id":"Q7361622"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361278$68FA5A99-8CAC-447E-822F-2E8037202A50","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":"Q7361278$36331748-F591-4E1E-95C4-9D867FE32B0E","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":"Q7361278$AF4407B7-2785-4F0C-8AD2-B1A0FEC12360","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Mission-time Linear Temporal Logic to Regular Expressions","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Mission-time_Linear_Temporal_Logic_to_Regular_Expressions"}}}}}