{"entities":{"Q7361665":{"pageid":31520534,"ns":120,"title":"Item:Q7361665","lastrevid":105366875,"modified":"2026-10-07T13:36:43Z","type":"item","id":"Q7361665","labels":{"en":{"language":"en","value":"Language Partitioning for Mission-time Linear Temporal Logic"}},"descriptions":{"en":{"language":"en","value":"AFP entry Mission_Time_LTL_Language_Partition"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d154445f581d708b6b77f3d2677c8977e1b43ecd","datavalue":{"value":"https://isa-afp.org/entries/Mission_Time_LTL_Language_Partition.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361665$74346EC5-7B69-4B54-BB47-F3CE0EC50081","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"92b0a54170ef38538e67b3e11bb7f54cac540996","datavalue":{"value":{"time":"+2025-03-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361665$E64DD1C8-30B5-4DDA-9E87-38375772C6E7","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"a0cb2da1b6cf06bf6a856922c95cf1d75849aa7d","datavalue":{"value":"Zili Wang","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361665$EE3883A2-9831-41BB-84ED-09A7FE40CF3D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"e930e6f6a933f5f4f03863d552f0013c9401bf23","datavalue":{"value":"Katherine Kosaian","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361665$D300B9BD-0F8D-4FF2-8514-D8CEB97F5ECB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"008696ca36787f7c60f83a0de30f7dfc989c3824","datavalue":{"value":"Alec Rosentrater","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361665$F5518532-0722-4F74-A268-07A7B3AA72AB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"fb80e4b240540799e646efc6f306d27db8865501","datavalue":{"value":{"text":"Language Partitioning for Mission-time Linear Temporal Logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361665$C342BB02-FA39-435D-BB7F-D50BF70DAA66","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"85ff773ba21f9879dd854310d3708269ce8f8296","datavalue":{"value":"Building on the existing formalization of Mission-time Linear Temporal Logic (MLTL), we formalize the notions of language decomposition and language partition for MLTL. More specifically, we formalize an algorithm to compute a language partition for MLTL and formally prove its correctness. Our algorithm is executable, and we export it to Haskell via Isabelle/HOL's code generator.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361665$65DDE3D3-DEF2-4872-AF6B-1C7F263179CD","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":"Q7361665$6EF6E552-F516-4990-AE62-EC454CFF4A18","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":"Q7361665$22867554-5A63-47B6-8EC5-90E543EE2656","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"c8b055357156b513ebffa05abff4ab0fc053c1d6","datavalue":{"value":{"entity-type":"item","numeric-id":7361662,"id":"Q7361662"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361665$A486C1FD-E6D7-4D3D-AA97-BA97D088A543","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":"Q7361665$BE27B44D-2756-4603-9BB4-4541DB4C01AB","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":"Q7361665$3F090410-49C1-4B90-80C2-BA5B57CD60B8","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Language Partitioning for Mission-time Linear Temporal Logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Language_Partitioning_for_Mission-time_Linear_Temporal_Logic"}}}}}