{"entities":{"Q7361622":{"pageid":31520405,"ns":120,"title":"Item:Q7361622","lastrevid":105367763,"modified":"2026-10-07T13:37:17Z","type":"item","id":"Q7361622","labels":{"en":{"language":"en","value":"Mission-time Linear Temporal Logic"}},"descriptions":{"en":{"language":"en","value":"AFP entry Mission_Time_LTL"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e8f789053fc48c94f67fc44cda10f7951edf599b","datavalue":{"value":"https://isa-afp.org/entries/Mission_Time_LTL.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361622$15CAFC15-9E1B-4E24-B90A-906EA289ED50","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":"Q7361622$7497DC91-834D-429D-AA42-9EF843346D5F","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"e930e6f6a933f5f4f03863d552f0013c9401bf23","datavalue":{"value":"Katherine Kosaian","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361622$602E48E3-EA31-409C-8597-30FC5C1DFAA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"a0cb2da1b6cf06bf6a856922c95cf1d75849aa7d","datavalue":{"value":"Zili Wang","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361622$91D2C846-A122-49C4-A9EE-D4858174B087","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"2b6a684ad49da14c1dbceed6a3acfd0d591ea650","datavalue":{"value":"Elizabeth Sloan","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361622$20B2602D-CB9C-491D-B1A5-5B8710D235F2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b7abd3c92be9c205bc60c08864f5cdc5dabe68b2","datavalue":{"value":{"text":"Mission-time Linear Temporal Logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361622$6BBFF63C-A511-4FD6-AE9B-E95DC3F0AA3A","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"a3c2a5c303436a2a1bed56f3af5ddf8fe61f6bdc","datavalue":{"value":"We formalize the syntax, semantics, and some useful properties of Mission-time Linear Temporal Logic (MLTL), following the literature. MLTL is a variant of Linear Temporal Logic, which has already been formalized in Isabelle/HOL. In contrast to LTL, MLTL includes finite discrete time bounds on the temporal operators. We do not directly build on the LTL AFP entry, but aim to mirror its style; in particular, we found it useful when defining our syntactic sugar binding precedences. Another closely related AFP entry is the formalization of MFOTL.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361622$45AA58A9-B626-40F2-A6E5-B01199854F9F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"9eae62c058d6c3b073105abf4e6cf5e325aa8014","datavalue":{"value":{"entity-type":"item","numeric-id":6154870,"id":"Q6154870"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361622$782AEAA8-ABCD-4909-B84C-1AF99F2C6771","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":"Q7361622$351A5234-97E5-47B4-8D08-1CD45C8174B6","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":"Q7361622$12938E37-C148-4BAA-B139-8F75FF892136","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":"Q7361622$E351C353-00AE-4389-82AF-932B139B71EC","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Mission-time Linear Temporal Logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Mission-time_Linear_Temporal_Logic"}}}}}