{"entities":{"Q7361264":{"pageid":31519331,"ns":120,"title":"Item:Q7361264","lastrevid":105364421,"modified":"2026-10-07T13:35:20Z","type":"item","id":"Q7361264","labels":{"en":{"language":"en","value":"Mission-time Linear Temporal Logic Formula Progression"}},"descriptions":{"en":{"language":"en","value":"AFP entry Mission_Time_LTL_Formula_Progression"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"0106df8969631fc420ca55042ac40a6982362774","datavalue":{"value":"https://isa-afp.org/entries/Mission_Time_LTL_Formula_Progression.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361264$3FE613DC-D7FE-41B5-BBE4-1FD7FAB076C6","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5a9811af95d74677c616838320cac001d09e488b","datavalue":{"value":{"time":"+2025-07-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":"Q7361264$E4C4BA90-4E03-42F9-81BB-C627253AB3E0","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"e930e6f6a933f5f4f03863d552f0013c9401bf23","datavalue":{"value":"Katherine Kosaian","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361264$8C9147A6-5A00-4E22-ACE0-AA6967D90503","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"a0cb2da1b6cf06bf6a856922c95cf1d75849aa7d","datavalue":{"value":"Zili Wang","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361264$362485BF-425E-4D06-9556-3443F78668F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"2b6a684ad49da14c1dbceed6a3acfd0d591ea650","datavalue":{"value":"Elizabeth Sloan","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361264$43CC8EB4-CD03-4BBE-9638-72B616075F3E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4d4b6d4631559d1870dbff1c4a13c5023a58472f","datavalue":{"value":{"text":"Mission-time Linear Temporal Logic Formula Progression","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361264$EC758065-082E-456F-818C-26CDBB6E569F","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"0bcf31aed6a2c5d6faa6bc19f858ed9fbf8bfac9","datavalue":{"value":"We build on the Isabelle/HOL formalization of Mission-time Linear Temporal Logic (MLTL) to formalize a formula progression algorithm for MLTL formulas (https://dblp.org/rec/conf/rv/LiR18.html), a key algorithm in the FPROGG tool for generating MLTL benchmarks. The formula progression algorithm takes a MLTL formula and steps through a given trace to partially evaluate a logically equivalent simpler formula at each step, ultimately checking whether or not the trace satisfies the original formula. Our formalization is executable and we export it to code in SML.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361264$FA486356-9F93-4013-8172-56F2D0EFDA08","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":"Q7361264$6A03D9B2-696C-4CC2-9BB0-9F922868D30C","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":"Q7361264$9A87B1C0-EEE6-40C6-BF53-D7081EEDC749","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"ec084f2f33463e96367d261c341919d2f3128032","datavalue":{"value":{"entity-type":"item","numeric-id":7360771,"id":"Q7360771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361264$7C9FD2EF-697B-4D44-8411-5EB6764EB9B3","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":"Q7361264$0A6951AE-49E9-4EFE-B0D2-AEF518B50DD9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Mission-time Linear Temporal Logic Formula Progression","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Mission-time_Linear_Temporal_Logic_Formula_Progression"}}}}}